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

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index f2830965224fe0a8c83c6a1ffe6561abb74db7d6..723752eb8f1e244603c532f0aab94aa7cc5e8c9b 100644 (file)
--- 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 9e70f4c3de16d899f64b66ef9651485bbfbcdd37..6adb6241e6159718057ea9a5bea39105bebfdbb0 100644 (file)
--- 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 3108582d9d5a9ec2ae51d7f00e25873763225039..feafc418afe342684f5de9001f12eeb11112eaf0 100644 (file)
--- 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 c9e00213ae83c47b6619aab678196944a459b142..e58ada5457cea3adc88991635faeb9c3cc4f5592 100644 (file)
--- 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 9be9dcefa8cb75757762c5bead9838fe68e8652a..725827abe8fbd9b91ba5d0124b7e6c57275a0440 100644 (file)
--- 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/<output_dir>.
-  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 '<output_dir>/myunittest.h'
-  #   we create test target 'unit/<output_dir>/myunittest'
-  #   and run it with 'ctest -R "example/<output_dir>/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/<output_dir>.
+    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 '<output_dir>/myunittest.h'
+    #   we create test target 'unit/<output_dir>/myunittest'
+    #   and run it with 'ctest -R "example/<output_dir>/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 c163e10945622bbdaf5784f89369f12c8c5af2f1..95ee9826f97c1f8017653fbd2b9db5c08ae22063 100644 (file)
--- 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])