From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 19 Sep 2018 16:21:31 +0000 (-0700)
Subject: cmake: Refactor cvc4_add_unit_test macro to support test names with '/'.
X-Git-Tag: cvc5-1.0.0~4535
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=65a713e53cefa95fcff1b2db30046edf943b3390;p=cvc5.git

cmake: Refactor cvc4_add_unit_test macro to support test names with '/'.

Required for consistent naming of tests, unit test names now also use
the test naming scheme <category>/<subdir>/<test name>, e.g.,
unit/theory/theory_bv_white.
---

diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt
index 920727e86..a37cb9276 100644
--- a/examples/CMakeLists.txt
+++ b/examples/CMakeLists.txt
@@ -36,7 +36,7 @@ add_custom_target(runexamples
 #         as arguments to the test executable.
 macro(cvc4_add_example name src_files libs output_dir)
   # The build target is created without the path prefix (not supported),
-  # e.g., for '<subdirs>/myexample.cpp'
+  # e.g., for '<output_dir>/myexample.cpp'
   #   we create build target 'myexample'
   #   and build it with 'make myexample'.
   # As a consequence, all build target names must be globally unique.
@@ -50,15 +50,14 @@ macro(cvc4_add_example name src_files libs output_dir)
   target_link_libraries(${name} ${libs})
   add_dependencies(examples ${name})
   # The test target is prefixed with test identifier 'example/' and the path,
-  # e.g., for '<subdirs>/myexample.cpp'
-  #   we create test target 'example/<subdirs>/myexample'
-  #   and run it with 'ctest -R "example/<subdirs>/<example>"'.
+  # e.g., for '<output_dir>/myexample.cpp'
+  #   we create test target 'example/<output_dir>/myexample'
+  #   and run it with 'ctest -R "example/<output_dir>/myunittest"'.
+  set(example_bin_dir ${EXAMPLES_BIN_DIR}/${output_dir})
   if("${output_dir}" STREQUAL "")
     set(example_test example/${name})
-    set(example_bin_dir ${EXAMPLES_BIN_DIR})
   else()
     set(example_test example/${output_dir}/${name})
-    set(example_bin_dir ${EXAMPLES_BIN_DIR}/${output_dir})
   endif()
   set_target_properties(${name}
     PROPERTIES RUNTIME_OUTPUT_DIRECTORY ${example_bin_dir})
diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt
index 5e45654a9..3e90fb333 100644
--- a/test/unit/CMakeLists.txt
+++ b/test/unit/CMakeLists.txt
@@ -15,15 +15,29 @@ set(CVC4_CXXTEST_FLAGS_BLACK
   -D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS)
 set(CVC4_CXXTEST_FLAGS_WHITE -fno-access-control ${CVC4_CXXTEST_FLAGS_BLACK})
 
-macro(cvc4_add_unit_test is_white name)
-  # cxxtest_add_test generates the unit test executables into directory
-  # CMAKE_BINARY_DIR/test/unit by default and does not allow to change this
-  # location (it's possible to set corresponding target properties with
-  # set_target_properties, but then the test environment does not find them).
-  # Hence, these are the only executables that are not generated into our
-  # default directory for executables (CMAKE_BINARY_DIR/bin).
-  cxxtest_add_test(${name} ${name}.cpp ${CMAKE_CURRENT_LIST_DIR}/${name}.h)
-  set_tests_properties(${name} PROPERTIES LABELS "unit")
+# Generate and add unit test.
+# Note: we do not use cxxtest_add_test from the FindCxxTest module since it
+#       does not allow test names containing '/'.
+macro(cvc4_add_unit_test is_white name output_dir)
+  # generate the test sources
+  set(test_src ${CMAKE_CURRENT_BINARY_DIR}/${name}.cpp)
+  set(test_header ${CMAKE_CURRENT_LIST_DIR}/${name}.h)
+  add_custom_command(
+      OUTPUT  ${test_src}
+      DEPENDS ${test_header}
+      COMMAND
+        ${CXXTEST_TESTGEN_INTERPRETER}
+          ${CXXTEST_TESTGEN_EXECUTABLE}
+          ${CXXTEST_TESTGEN_ARGS} -o ${test_src} ${test_header}
+  )
+  set_source_files_properties(${test_src} PROPERTIES GENERATED true)
+  # The build target is created without the path prefix (not supported),
+  # e.g., for '<output_dir>/myunittest.h'
+  #   we generate '${CMAKE_BINAR_DIR}/test/unit/<output_dir>/myunittest.cpp',
+  #   create build target 'myunittest'
+  #   and build it with 'make myunittest'.
+  # As a consequence, all build target names must be globally unique.
+  add_executable(${name} ${test_src} ${test_header})
   target_link_libraries(${name} main-test)
   target_compile_definitions(${name} PRIVATE ${CVC4_CXXTEST_FLAGS_BLACK})
   if(${is_white})
@@ -33,16 +47,31 @@ macro(cvc4_add_unit_test is_white name)
   # code that does not properly add the override keyword to runTest().
   target_compile_options(${name} PRIVATE -Wno-suggest-override)
   add_dependencies(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})
+  endif()
+  add_test(${test_name} ${test_bin_dir}/${name})
+  set_tests_properties(${test_name} PROPERTIES LABELS "unit")
   if(ENABLE_COVERAGE)
     add_dependencies(coverage ${name})
   endif()
 endmacro()
 
-macro(cvc4_add_unit_test_black name)
-  cvc4_add_unit_test(FALSE ${name})
+macro(cvc4_add_unit_test_black name output_dir)
+  cvc4_add_unit_test(FALSE ${name} ${output_dir})
 endmacro()
-macro(cvc4_add_unit_test_white name)
-  cvc4_add_unit_test(TRUE ${name})
+macro(cvc4_add_unit_test_white name output_dir)
+  cvc4_add_unit_test(TRUE ${name} ${output_dir})
 endmacro()
 
 add_subdirectory(base)
diff --git a/test/unit/base/CMakeLists.txt b/test/unit/base/CMakeLists.txt
index 139d6d577..0a308b7a9 100644
--- a/test/unit/base/CMakeLists.txt
+++ b/test/unit/base/CMakeLists.txt
@@ -1,4 +1,4 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(map_util_black)
+cvc4_add_unit_test_black(map_util_black base)
diff --git a/test/unit/context/CMakeLists.txt b/test/unit/context/CMakeLists.txt
index 3d556ff6d..f089ac5f3 100644
--- a/test/unit/context/CMakeLists.txt
+++ b/test/unit/context/CMakeLists.txt
@@ -1,10 +1,10 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(cdlist_black)
-cvc4_add_unit_test_black(cdmap_black)
-cvc4_add_unit_test_white(cdmap_white)
-cvc4_add_unit_test_black(cdo_black)
-cvc4_add_unit_test_black(context_black)
-cvc4_add_unit_test_black(context_mm_black)
-cvc4_add_unit_test_white(context_white)
+cvc4_add_unit_test_black(cdlist_black context)
+cvc4_add_unit_test_black(cdmap_black context)
+cvc4_add_unit_test_white(cdmap_white context)
+cvc4_add_unit_test_black(cdo_black context)
+cvc4_add_unit_test_black(context_black context)
+cvc4_add_unit_test_black(context_mm_black context)
+cvc4_add_unit_test_white(context_white context)
diff --git a/test/unit/expr/CMakeLists.txt b/test/unit/expr/CMakeLists.txt
index 816d3bd71..575268cae 100644
--- a/test/unit/expr/CMakeLists.txt
+++ b/test/unit/expr/CMakeLists.txt
@@ -1,18 +1,18 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(attribute_black)
-cvc4_add_unit_test_white(attribute_white)
-cvc4_add_unit_test_black(expr_manager_public)
-cvc4_add_unit_test_black(expr_public)
-cvc4_add_unit_test_black(kind_black)
-cvc4_add_unit_test_black(kind_map_black)
-cvc4_add_unit_test_black(node_black)
-cvc4_add_unit_test_black(node_builder_black)
-cvc4_add_unit_test_black(node_manager_black)
-cvc4_add_unit_test_white(node_manager_white)
-cvc4_add_unit_test_black(node_self_iterator_black)
-cvc4_add_unit_test_white(node_white)
-cvc4_add_unit_test_black(symbol_table_black)
-cvc4_add_unit_test_black(type_cardinality_public)
-cvc4_add_unit_test_white(type_node_white)
+cvc4_add_unit_test_black(attribute_black expr)
+cvc4_add_unit_test_white(attribute_white expr)
+cvc4_add_unit_test_black(expr_manager_public expr)
+cvc4_add_unit_test_black(expr_public expr)
+cvc4_add_unit_test_black(kind_black expr)
+cvc4_add_unit_test_black(kind_map_black expr)
+cvc4_add_unit_test_black(node_black expr)
+cvc4_add_unit_test_black(node_builder_black expr)
+cvc4_add_unit_test_black(node_manager_black expr)
+cvc4_add_unit_test_white(node_manager_white expr)
+cvc4_add_unit_test_black(node_self_iterator_black expr)
+cvc4_add_unit_test_white(node_white expr)
+cvc4_add_unit_test_black(symbol_table_black expr)
+cvc4_add_unit_test_black(type_cardinality_public expr)
+cvc4_add_unit_test_white(type_node_white expr)
diff --git a/test/unit/main/CMakeLists.txt b/test/unit/main/CMakeLists.txt
index 2b2497a4b..7dbd01bd2 100644
--- a/test/unit/main/CMakeLists.txt
+++ b/test/unit/main/CMakeLists.txt
@@ -1,4 +1,4 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(interactive_shell_black)
+cvc4_add_unit_test_black(interactive_shell_black main)
diff --git a/test/unit/parser/CMakeLists.txt b/test/unit/parser/CMakeLists.txt
index debe8a4ce..37204f0c3 100644
--- a/test/unit/parser/CMakeLists.txt
+++ b/test/unit/parser/CMakeLists.txt
@@ -1,5 +1,5 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(parser_black)
-cvc4_add_unit_test_black(parser_builder_black)
+cvc4_add_unit_test_black(parser_black parser)
+cvc4_add_unit_test_black(parser_builder_black parser)
diff --git a/test/unit/prop/CMakeLists.txt b/test/unit/prop/CMakeLists.txt
index 990422445..dbb6de01d 100644
--- a/test/unit/prop/CMakeLists.txt
+++ b/test/unit/prop/CMakeLists.txt
@@ -1,4 +1,4 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_white(cnf_stream_white)
+cvc4_add_unit_test_white(cnf_stream_white prop)
diff --git a/test/unit/theory/CMakeLists.txt b/test/unit/theory/CMakeLists.txt
index 6dc627db9..a5a67cfa2 100644
--- a/test/unit/theory/CMakeLists.txt
+++ b/test/unit/theory/CMakeLists.txt
@@ -1,11 +1,11 @@
-cvc4_add_unit_test_white(evaluator_white)
-cvc4_add_unit_test_white(logic_info_white)
-cvc4_add_unit_test_white(theory_arith_white)
-cvc4_add_unit_test_black(theory_black)
-cvc4_add_unit_test_white(theory_bv_white)
-cvc4_add_unit_test_white(theory_engine_white)
-cvc4_add_unit_test_white(theory_quantifiers_bv_instantiator_white)
-cvc4_add_unit_test_white(theory_quantifiers_bv_inverter_white)
-cvc4_add_unit_test_white(theory_strings_rewriter_white)
-cvc4_add_unit_test_white(theory_white)
-cvc4_add_unit_test_white(type_enumerator_white)
+cvc4_add_unit_test_white(evaluator_white theory)
+cvc4_add_unit_test_white(logic_info_white theory)
+cvc4_add_unit_test_white(theory_arith_white theory)
+cvc4_add_unit_test_black(theory_black theory)
+cvc4_add_unit_test_white(theory_bv_white theory)
+cvc4_add_unit_test_white(theory_engine_white theory)
+cvc4_add_unit_test_white(theory_quantifiers_bv_instantiator_white theory)
+cvc4_add_unit_test_white(theory_quantifiers_bv_inverter_white theory)
+cvc4_add_unit_test_white(theory_strings_rewriter_white theory)
+cvc4_add_unit_test_white(theory_white theory)
+cvc4_add_unit_test_white(type_enumerator_white theory)
diff --git a/test/unit/util/CMakeLists.txt b/test/unit/util/CMakeLists.txt
index 79e5e78ff..0748e1059 100644
--- a/test/unit/util/CMakeLists.txt
+++ b/test/unit/util/CMakeLists.txt
@@ -1,20 +1,20 @@
 #-----------------------------------------------------------------------------#
 # Add unit tests
 
-cvc4_add_unit_test_black(array_store_all_black)
-cvc4_add_unit_test_white(assert_white)
-cvc4_add_unit_test_black(binary_heap_black)
-cvc4_add_unit_test_black(bitvector_black)
-cvc4_add_unit_test_black(boolean_simplification_black)
-cvc4_add_unit_test_black(cardinality_public)
-cvc4_add_unit_test_white(check_white)
-cvc4_add_unit_test_black(configuration_black)
-cvc4_add_unit_test_black(datatype_black)
-cvc4_add_unit_test_black(exception_black)
-cvc4_add_unit_test_black(integer_black)
-cvc4_add_unit_test_white(integer_white)
-cvc4_add_unit_test_black(listener_black)
-cvc4_add_unit_test_black(output_black)
-cvc4_add_unit_test_black(rational_black)
-cvc4_add_unit_test_white(rational_white)
-cvc4_add_unit_test_black(stats_black)
+cvc4_add_unit_test_black(array_store_all_black util)
+cvc4_add_unit_test_white(assert_white util)
+cvc4_add_unit_test_black(binary_heap_black util)
+cvc4_add_unit_test_black(bitvector_black util)
+cvc4_add_unit_test_black(boolean_simplification_black util)
+cvc4_add_unit_test_black(cardinality_public util)
+cvc4_add_unit_test_white(check_white util)
+cvc4_add_unit_test_black(configuration_black util)
+cvc4_add_unit_test_black(datatype_black util)
+cvc4_add_unit_test_black(exception_black util)
+cvc4_add_unit_test_black(integer_black util)
+cvc4_add_unit_test_white(integer_white util)
+cvc4_add_unit_test_black(listener_black util)
+cvc4_add_unit_test_black(output_black util)
+cvc4_add_unit_test_black(rational_black util)
+cvc4_add_unit_test_white(rational_white util)
+cvc4_add_unit_test_black(stats_black util)