From da7a1fd917db3087a8146af40528bf32bbc817ad Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 27 Feb 2020 10:15:20 +0000 Subject: [PATCH 1/7] Add a define for XFAIL These tests won't be run by default (de-cluttering the output with expected failures). When run, they will fail if they pass --- unit/testing-utils/use_catch.h | 3 +++ 1 file changed, 3 insertions(+) diff --git a/unit/testing-utils/use_catch.h b/unit/testing-utils/use_catch.h index 4055b62a8c3..430c8a51c02 100644 --- a/unit/testing-utils/use_catch.h +++ b/unit/testing-utils/use_catch.h @@ -36,4 +36,7 @@ Author: Michael Tautschnig #include #endif +/// Add to the end of test tags to mark a test that is expected to fail +#define XFAIL "[.][!shouldfail]" + #endif // CPROVER_TESTING_UTILS_USE_CATCH_H From 186855f56c636dc5dd20c2b87541e3073eedc671 Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 27 Feb 2020 10:15:50 +0000 Subject: [PATCH 2/7] Enable two tests that pass These don't fail, so no reason not to have them running --- jbmc/unit/java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/jbmc/unit/java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp b/jbmc/unit/java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp index c5fba3cf4c3..c5dbcf2cc0d 100644 --- a/jbmc/unit/java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp +++ b/jbmc/unit/java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp @@ -12,7 +12,7 @@ Author: Diffblue Limited. SCENARIO( "Lazy load lambda methods", - "[core][java_bytecode][ci_lazy_methods][lambdas][!mayfail]") + "[core][java_bytecode][ci_lazy_methods][lambdas]") { GIVEN("A class with some locally declared lambdas") { @@ -192,7 +192,7 @@ SCENARIO( SCENARIO( "Lazy load lambda methods in seperate class", - "[core][java_bytecode][ci_lazy_methods][lambdas][!mayfail]") + "[core][java_bytecode][ci_lazy_methods][lambdas]") { const symbol_tablet symbol_table = load_java_class_lazy( "ExternalLambdaAccessor", From a2c45e8b8481312f9f31c1ec48b733828089fd1d Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 27 Feb 2020 10:16:26 +0000 Subject: [PATCH 3/7] Replace mayfail with XFAIL --- .../java_bytecode_convert_method/convert_invoke_dynamic.cpp | 6 +++--- .../instantiate_not_contains.cpp | 3 +-- unit/util/irep_sharing.cpp | 4 ++-- 3 files changed, 6 insertions(+), 7 deletions(-) diff --git a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp index bc0846681f2..a63f32a0c7e 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_convert_method/convert_invoke_dynamic.cpp @@ -188,7 +188,7 @@ void validate_local_variable_lambda_assignment( SCENARIO( "Converting invokedynamic with a local lambda", "[core]" - "[lambdas][java_bytecode][java_bytecode_convert_method][!mayfail]") + "[lambdas][java_bytecode][java_bytecode_convert_method]" XFAIL) { // NOLINTNEXTLINE(whitespace/braces) run_test_with_compilers([](const std::string &compiler) { @@ -380,7 +380,7 @@ void validate_member_variable_lambda_assignment( SCENARIO( "Converting invokedynamic with a member lambda", "[core]" - "[lamdba][java_bytecode][java_bytecode_convert_method][!mayfail]") + "[lamdba][java_bytecode][java_bytecode_convert_method]" XFAIL) { // NOLINTNEXTLINE(whitespace/braces) run_test_with_compilers([](const std::string &compiler) { @@ -548,7 +548,7 @@ void validate_static_member_variable_lambda_assignment( SCENARIO( "Converting invokedynamic with a static member lambda", "[core]" - "[lamdba][java_bytecode][java_bytecode_convert_method][!mayfail]") + "[lamdba][java_bytecode][java_bytecode_convert_method]" XFAIL) { // NOLINTNEXTLINE(whitespace/braces) run_test_with_compilers([](const std::string &compiler) { diff --git a/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp b/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp index 6f1ec9f1ca8..cdcfe9129c2 100644 --- a/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp +++ b/jbmc/unit/solvers/strings/string_constraint_instantiation/instantiate_not_contains.cpp @@ -172,10 +172,9 @@ decision_proceduret::resultt check_sat(const exprt &expr, const namespacet &ns) return solver(); } -// The [!mayfail] tag allows tests to fail while reporting the failure SCENARIO( "instantiate_not_contains", - "[!mayfail][core][solvers][refinement][string_constraint_instantiation]") + "[core][solvers][refinement][string_constraint_instantiation]" XFAIL) { // For printing expression register_language(new_java_bytecode_language); diff --git a/unit/util/irep_sharing.cpp b/unit/util/irep_sharing.cpp index 92536974420..aebbed6b5fa 100644 --- a/unit/util/irep_sharing.cpp +++ b/unit/util/irep_sharing.cpp @@ -9,7 +9,7 @@ #ifdef SHARING -SCENARIO("irept_sharing_trade_offs", "[!mayfail][core][utils][irept]") +SCENARIO("irept_sharing_trade_offs", "[core][utils][irept]" XFAIL) { GIVEN("An irept created with move_to_sub") { @@ -116,7 +116,7 @@ SCENARIO("irept_sharing", "[core][utils][irept]") #include -SCENARIO("exprt_sharing_trade_offs", "[!mayfail][core][utils][exprt]") +SCENARIO("exprt_sharing_trade_offs", "[core][utils][exprt]" XFAIL) { GIVEN("An expression created with add_to_operands(std::move(...))") { From 9fcd171078869c433f69b6c9e4f3b2fa5467ceeb Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 27 Feb 2020 10:49:40 +0000 Subject: [PATCH 4/7] Running expected failure tests after running regular unit tests This ensures that failed tests don't get inadvertently fixed, without cluttering the normal output --- .travis.yml | 4 ++++ jbmc/unit/Makefile | 2 +- unit/Makefile | 2 +- 3 files changed, 6 insertions(+), 2 deletions(-) diff --git a/.travis.yml b/.travis.yml index b77d06bdd95..ec23ed01e0e 100644 --- a/.travis.yml +++ b/.travis.yml @@ -355,9 +355,13 @@ script: - env PATH=$PATH:`pwd`/src/solvers UBSAN_OPTIONS=print_stacktrace=1 make -C regression/cbmc test-cprover-smt2 - make -C unit "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2 - make -C unit test + - echo "Running expected failure tests" + - make TAGS="[!shouldfail]" -C unit test - env UBSAN_OPTIONS=print_stacktrace=1 make -C jbmc/regression test-parallel "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2 JOBS=2 - make -C jbmc/unit "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2 - make -C jbmc/unit test + - echo "Running expected failure tests" + - make TAGS="[!shouldfail]" -C jbmc/unit test before_cache: - ccache -s diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index dd03b3266e4..4802b5d123d 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -146,7 +146,7 @@ clean: java-testing-utils-clean test: $(CATCH_TEST) if ! ./$(CATCH_TEST) -l | grep -q "^$(N_CATCH_TESTS) test cases" ; then \ ./$(CATCH_TEST) -l ; fi - ./$(CATCH_TEST) + ./$(CATCH_TEST) ${TAGS} ############################################################################### diff --git a/unit/Makefile b/unit/Makefile index ccbe365b11f..fdda40a9b25 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -206,7 +206,7 @@ clean: testing-utils-clean test: $(CATCH_TEST) if ! ./$(CATCH_TEST) -l | grep -q "^$(N_CATCH_TESTS) test cases" ; then \ ./$(CATCH_TEST) -l ; fi - ./$(CATCH_TEST) + ./$(CATCH_TEST) ${TAGS} ############################################################################### From 44d1ee4a716fc856230e17855ee4b4d0f2014dec Mon Sep 17 00:00:00 2001 From: Thomas Kiley Date: Thu, 27 Feb 2020 11:16:26 +0000 Subject: [PATCH 5/7] Include hidden tests when counting tests --- jbmc/unit/Makefile | 5 +++-- unit/Makefile | 5 +++-- 2 files changed, 6 insertions(+), 4 deletions(-) diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index 4802b5d123d..d18567da013 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -144,8 +144,9 @@ all: $(CATCH_TEST) clean: java-testing-utils-clean test: $(CATCH_TEST) - if ! ./$(CATCH_TEST) -l | grep -q "^$(N_CATCH_TESTS) test cases" ; then \ - ./$(CATCH_TEST) -l ; fi + # Include hidden tests by specifying "*,[.]" for tests to count + if ! ./$(CATCH_TEST) "*,[.]" -l | grep -q "^$(N_CATCH_TESTS) matching test cases" ; then \ + ./$(CATCH_TEST) "*,[.]" -l ; fi ./$(CATCH_TEST) ${TAGS} diff --git a/unit/Makefile b/unit/Makefile index fdda40a9b25..dbabd7da465 100644 --- a/unit/Makefile +++ b/unit/Makefile @@ -204,8 +204,9 @@ all: $(CATCH_TEST) clean: testing-utils-clean test: $(CATCH_TEST) - if ! ./$(CATCH_TEST) -l | grep -q "^$(N_CATCH_TESTS) test cases" ; then \ - ./$(CATCH_TEST) -l ; fi + # Include hidden tests by specifying "*,[.]" for tests to count + if ! ./$(CATCH_TEST) "*,[.]" -l | grep -q "^$(N_CATCH_TESTS) matching test cases" ; then \ + ./$(CATCH_TEST) "*,[.]" -l ; fi ./$(CATCH_TEST) ${TAGS} From 18cca674642faad70f7b0862ce15860f5025493e Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 27 Feb 2020 13:52:41 +0000 Subject: [PATCH 6/7] Add running XFAIL tests to other jobs --- buildspec-linux-clang.yml | 4 ++++ buildspec-windows.yml | 8 ++++++++ buildspec.yml | 4 ++++ 3 files changed, 16 insertions(+) diff --git a/buildspec-linux-clang.yml b/buildspec-linux-clang.yml index 5ef62595ad8..ec78098a47f 100644 --- a/buildspec-linux-clang.yml +++ b/buildspec-linux-clang.yml @@ -27,10 +27,14 @@ phases: post_build: commands: - make -C unit test + - echo "Running expected failure tests" + - make TAGS="[!shouldfail]" -C unit test - make -C regression test CXX='ccache /usr/bin/clang++-8' CXX_FLAGS='-Qunused-arguments' - make -C regression/cbmc test-paths-lifo - env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2 - make -C jbmc/unit test + - echo "Running expected failure tests" + - make TAGS="[!shouldfail]" -C jbmc/unit test - make -C jbmc/regression test - echo Build completed on `date` cache: diff --git a/buildspec-windows.yml b/buildspec-windows.yml index c98fdfe002e..47e8dc3c31c 100644 --- a/buildspec-windows.yml +++ b/buildspec-windows.yml @@ -57,6 +57,10 @@ phases: $env:Path = "C:\tools\cygwin\bin;$env:Path" cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C unit test BUILD_ENV=MSVC" ' + - | + $env:Path = "C:\tools\cygwin\bin;$env:Path" + cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make TAGS=[!shouldfail] -C unit test BUILD_ENV=MSVC" ' + - | $env:Path = "C:\tools\cygwin\bin;$env:Path" cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C jbmc/regression test BUILD_ENV=MSVC" ' @@ -65,6 +69,10 @@ phases: $env:Path = "C:\tools\cygwin\bin;$env:Path" cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make -C jbmc/unit test BUILD_ENV=MSVC" ' + - | + $env:Path = "C:\tools\cygwin\bin;$env:Path" + cmd /c 'call "C:\Program Files (x86)\Microsoft Visual Studio 14.0\VC\vcvarsall.bat" x64 && bash -c "make TAGS=[!shouldfail] -C jbmc/unit test BUILD_ENV=MSVC" ' + cache: paths: - 'c:\clcache\**\*' diff --git a/buildspec.yml b/buildspec.yml index 62fcdfd0428..3348cb54515 100644 --- a/buildspec.yml +++ b/buildspec.yml @@ -26,10 +26,14 @@ phases: post_build: commands: - make -C unit test + - echo "Running expected failure tests" + - make TAGS="[!shouldfail]" -C unit test - make -C regression test - make -C regression/cbmc test-paths-lifo - env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2 - make -C jbmc/unit test + - echo "Running expected failure tests" + - make TAGS="[!shouldfail]" -C jbmc/unit test - make -C jbmc/regression test - echo Build completed on `date` cache: From 617687162dc1a7ef23c9720d90878f4cf8d191a7 Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 3 Mar 2020 12:05:47 +0000 Subject: [PATCH 7/7] Add and invoke a ctest target for checking expected failure unit tests --- .travis.yml | 6 +++--- buildspec-linux-cmake-gcc.yml | 1 + jbmc/unit/CMakeLists.txt | 7 +++++++ unit/CMakeLists.txt | 7 +++++++ 4 files changed, 18 insertions(+), 3 deletions(-) diff --git a/.travis.yml b/.travis.yml index ec23ed01e0e..96eaf09200f 100644 --- a/.travis.yml +++ b/.travis.yml @@ -243,7 +243,7 @@ jobs: - cmake -S . -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/g++-7' '-DCMAKE_USE_CUDD=true' -DCMAKE_CXX_FLAGS="-DBDD_GUARDS" '-DWITH_MEMORY_ANALYZER=On' - git submodule update --init --recursive - cmake --build build -- -j4 - script: (cd build; ctest -V -L CORE -j2) + script: (cd build; ctest -V -L CORE -j2; ctest -V -R unit-xfail -j2) # cmake build using clang++-6 - stage: Test different OS/CXX/Flags @@ -280,7 +280,7 @@ jobs: - cmake -S . -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_CXX_COMPILER=/usr/bin/clang++-7' '-DCMAKE_CXX_FLAGS=-Qunused-arguments' '-DWITH_MEMORY_ANALYZER=On' - git submodule update --init --recursive - cmake --build build -- -j4 - script: (cd build; ctest -V -L CORE -j2) + script: (cd build; ctest -V -L CORE -j2; ctest -V -R unit-xfail -j2) # cmake build on OSX, using default clang - stage: Test different OS/CXX/Flags @@ -300,7 +300,7 @@ jobs: - cmake -S . -Bbuild '-DCMAKE_BUILD_TYPE=Release' '-DCMAKE_OSX_ARCHITECTURES=x86_64' - git submodule update --init --recursive - cmake --build build -- -j4 - script: (cd build; ctest -V -L CORE -j2) + script: (cd build; ctest -V -L CORE -j2; ctest -V -R unit-xfail -j2) # Run Coverity diff --git a/buildspec-linux-cmake-gcc.yml b/buildspec-linux-cmake-gcc.yml index d475c985ea2..9f4d176571e 100644 --- a/buildspec-linux-cmake-gcc.yml +++ b/buildspec-linux-cmake-gcc.yml @@ -22,6 +22,7 @@ phases: post_build: commands: - cd build; ctest -V -L CORE -j2 + - cd build; ctest -V -R unit-xfail -j2 - echo Build completed on `date` cache: paths: diff --git a/jbmc/unit/CMakeLists.txt b/jbmc/unit/CMakeLists.txt index 6ba62de4903..781e39b66ac 100644 --- a/jbmc/unit/CMakeLists.txt +++ b/jbmc/unit/CMakeLists.txt @@ -36,4 +36,11 @@ add_test( COMMAND $ WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR} ) + +add_test( + NAME java-unit-xfail + COMMAND $ "[!shouldfail]" + WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR} +) + set_tests_properties(java-unit PROPERTIES LABELS "CORE;CBMC") diff --git a/unit/CMakeLists.txt b/unit/CMakeLists.txt index 6a765e74e95..6372702081a 100644 --- a/unit/CMakeLists.txt +++ b/unit/CMakeLists.txt @@ -65,4 +65,11 @@ add_test( COMMAND $ WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR} ) + +add_test( + NAME unit-xfail + COMMAND $ "[!shouldfail]" + WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR} +) + set_tests_properties(unit PROPERTIES LABELS "CORE;CBMC")