From 7c784424b5ca43d5c35c8ac21b87c2b8ab584b2d Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 24 Nov 2021 14:02:05 -0800 Subject: [PATCH] Always enable API black box unit tests (#7696) Currently, when assertions are disabled, we do not enable any unit tests. However, we have decided that it would be beneficial to do black box unit testing of the API even when building cvc5 without assertions, because the API is user facing. This commit makes the following changes: - Always enables API black box unit tests - Adds a test to check whether a buggy version of Clang is being used, which prevents the use of `-fno-access-control` for white box tests - Fixes a spooky variable name in a Python unit test --- .github/workflows/ci.yml | 2 +- CMakeLists.txt | 14 +++- test/CMakeLists.txt | 5 +- test/api/python/CMakeLists.txt | 4 +- test/unit/CMakeLists.txt | 100 +++++++++++++++------------- test/unit/api/python/test_solver.py | 2 +- 6 files changed, 72 insertions(+), 55 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index f28309652..723752eb8 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -19,7 +19,7 @@ jobs: - name: macos:production os: macos-11 - config: production --auto-download --all-bindings --editline + config: production --auto-download --python-bindings --editline cache-key: production python-bindings: true check-examples: true diff --git a/CMakeLists.txt b/CMakeLists.txt index 9e70f4c3d..6adb6241e 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -251,10 +251,22 @@ endif() # https://gitlab.kitware.com/cmake/community/wikis/doc/cmake/RPATH-handling set(CMAKE_INSTALL_RPATH "${CMAKE_INSTALL_PREFIX}/${CMAKE_INSTALL_LIBDIR};${PROJECT_SOURCE_DIR}/deps/install/lib") -# Set visibility to default if unit tests are enabled +# Set visibility to default if unit tests are enabled. If unit tests are +# enabled, we also check if we can execute white box unit tests (some versions +# of Clang have issues with the required flag). +set(ENABLE_WHITEBOX_UNIT_TESTING OFF) if(ENABLE_UNIT_TESTING) set(CMAKE_CXX_VISIBILITY_PRESET default) set(CMAKE_VISIBILITY_INLINES_HIDDEN 0) + + # Check if Clang version has the bug that was fixed in + # https://reviews.llvm.org/D93104 + set(ENABLE_WHITEBOX_UNIT_TESTING ON) + check_cxx_compiler_flag("-faccess-control" HAVE_CXX_FLAGfaccess_control) + if(NOT HAVE_CXX_FLAGfaccess_control) + set(ENABLE_WHITEBOX_UNIT_TESTING OFF) + message(STATUS "Disabling white box unit tests") + endif() endif() #-----------------------------------------------------------------------------# diff --git a/test/CMakeLists.txt b/test/CMakeLists.txt index 3108582d9..feafc418a 100644 --- a/test/CMakeLists.txt +++ b/test/CMakeLists.txt @@ -38,7 +38,4 @@ add_custom_target(check add_subdirectory(regress) add_subdirectory(api EXCLUDE_FROM_ALL) add_subdirectory(binary EXCLUDE_FROM_ALL) - -if(ENABLE_UNIT_TESTING) - add_subdirectory(unit EXCLUDE_FROM_ALL) -endif() +add_subdirectory(unit EXCLUDE_FROM_ALL) diff --git a/test/api/python/CMakeLists.txt b/test/api/python/CMakeLists.txt index c9e00213a..e58ada545 100644 --- a/test/api/python/CMakeLists.txt +++ b/test/api/python/CMakeLists.txt @@ -24,8 +24,8 @@ macro(cvc5_add_python_api_test name filename) # directory for importing the python bindings WORKING_DIRECTORY ${CMAKE_BINARY_DIR}/src/api/python) set_tests_properties(${test_name} - PROPERTIES LABELS "api" - ENVIRONMENT PYTHONPATH=${PYTHON_MODULE_PATH}:${CMAKE_SOURCE_DIR}/api/python) + PROPERTIES LABELS "api" + ENVIRONMENT PYTHONPATH=${PYTHON_MODULE_PATH}:${CMAKE_SOURCE_DIR}/api/python) endmacro() # add specific test files diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt index 9be9dcefa..725827abe 100644 --- a/test/unit/CMakeLists.txt +++ b/test/unit/CMakeLists.txt @@ -36,48 +36,52 @@ set(CVC5_UNIT_TEST_FLAGS_BLACK # Generate and add unit test. macro(cvc5_add_unit_test is_white name output_dir) - set(test_src ${CMAKE_CURRENT_LIST_DIR}/${name}.cpp) - add_executable(${name} ${test_src}) - target_compile_definitions(${name} PRIVATE ${CVC5_UNIT_TEST_FLAGS_BLACK}) - target_link_libraries(${name} PUBLIC main-test GMP) - target_link_libraries(${name} PUBLIC GTest::Main) - target_link_libraries(${name} PUBLIC GTest::GTest) + # Only enable white box unit tests if the compiler supports it and the build + # requires it + if((NOT ${is_white}) OR ENABLE_WHITEBOX_UNIT_TESTING) + set(test_src ${CMAKE_CURRENT_LIST_DIR}/${name}.cpp) + add_executable(${name} ${test_src}) + target_compile_definitions(${name} PRIVATE ${CVC5_UNIT_TEST_FLAGS_BLACK}) + target_link_libraries(${name} PUBLIC main-test GMP) + target_link_libraries(${name} PUBLIC GTest::Main) + target_link_libraries(${name} PUBLIC GTest::GTest) - if(USE_POLY) - # Make libpoly headers available for tests - target_include_directories(${name} PRIVATE "${Poly_INCLUDE_DIR}") - endif() + if(USE_POLY) + # Make libpoly headers available for tests + target_include_directories(${name} PRIVATE "${Poly_INCLUDE_DIR}") + endif() - if(${is_white}) - target_compile_options(${name} PRIVATE -fno-access-control) - endif() + if(${is_white}) + target_compile_options(${name} PRIVATE -fno-access-control) + endif() - # Disable the Wunused-comparison warnings for the unit tests. - # We check for `-Wunused-comparison` and then add `-Wno-unused-comparison` - check_cxx_compiler_flag("-Wunused-comparison" HAVE_CXX_FLAGWunused_comparison) - if(HAVE_CXX_FLAGWunused_comparison) - target_compile_options(${name} PRIVATE -Wno-unused-comparison) - endif() - add_dependencies(build-units ${name}) - # Generate into bin/test/unit/. - set(test_bin_dir ${CMAKE_BINARY_DIR}/bin/test/unit/${output_dir}) - set_target_properties(${name} - PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${test_bin_dir}) - # The test target is prefixed with test identifier 'unit/' and the path, - # e.g., for '/myunittest.h' - # we create test target 'unit//myunittest' - # and run it with 'ctest -R "example//myunittest"'. - if("${output_dir}" STREQUAL "") - set(test_name unit/${name}) - else() - if("${output_dir}" STREQUAL "api") - set(test_name unit/${output_dir}/cpp/${name}) + # Disable the Wunused-comparison warnings for the unit tests. + # We check for `-Wunused-comparison` and then add `-Wno-unused-comparison` + check_cxx_compiler_flag("-Wunused-comparison" HAVE_CXX_FLAGWunused_comparison) + if(HAVE_CXX_FLAGWunused_comparison) + target_compile_options(${name} PRIVATE -Wno-unused-comparison) + endif() + add_dependencies(build-units ${name}) + # Generate into bin/test/unit/. + set(test_bin_dir ${CMAKE_BINARY_DIR}/bin/test/unit/${output_dir}) + set_target_properties(${name} + PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${test_bin_dir}) + # The test target is prefixed with test identifier 'unit/' and the path, + # e.g., for '/myunittest.h' + # we create test target 'unit//myunittest' + # and run it with 'ctest -R "example//myunittest"'. + if("${output_dir}" STREQUAL "") + set(test_name unit/${name}) else() - set(test_name unit/${output_dir}/${name}) + if("${output_dir}" STREQUAL "api") + set(test_name unit/${output_dir}/cpp/${name}) + else() + set(test_name unit/${output_dir}/${name}) + endif() endif() + add_test(${test_name} ${test_bin_dir}/${name}) + set_tests_properties(${test_name} PROPERTIES LABELS "unit") endif() - add_test(${test_name} ${test_bin_dir}/${name}) - set_tests_properties(${test_name} PROPERTIES LABELS "unit") endmacro() macro(cvc5_add_unit_test_black name output_dir) @@ -87,14 +91,18 @@ macro(cvc5_add_unit_test_white name output_dir) cvc5_add_unit_test(TRUE ${name} ${output_dir}) endmacro() +# API black box unit tests are always enabled add_subdirectory(api) -add_subdirectory(base) -add_subdirectory(context) -add_subdirectory(node) -add_subdirectory(main) -add_subdirectory(parser) -add_subdirectory(printer) -add_subdirectory(prop) -add_subdirectory(theory) -add_subdirectory(preprocessing) -add_subdirectory(util) + +if(ENABLE_UNIT_TESTING) + add_subdirectory(base) + add_subdirectory(context) + add_subdirectory(node) + add_subdirectory(main) + add_subdirectory(parser) + add_subdirectory(printer) + add_subdirectory(prop) + add_subdirectory(theory) + add_subdirectory(preprocessing) + add_subdirectory(util) +endif() diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index c163e1094..95ee9826f 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -749,7 +749,7 @@ def test_mk_term(solver): # Test cases that are nary via the API but have arity = 2 internally s_bool = solver.getBooleanSort() - t_bool = solver.mkConst(s_boo, "t_bool") + t_bool = solver.mkConst(s_bool, "t_bool") solver.mkTerm(kinds.Implies, [t_bool, t_bool, t_bool]) solver.mkTerm(kinds.Xor, [t_bool, t_bool, t_bool]) solver.mkTerm(solver.mkOp(kinds.Xor), [t_bool, t_bool, t_bool]) -- 2.30.2