diff --git a/.github/workflows/pull-request-checks.yaml b/.github/workflows/pull-request-checks.yaml index 8ab4a9e7e86..0a9f9c4edd5 100644 --- a/.github/workflows/pull-request-checks.yaml +++ b/.github/workflows/pull-request-checks.yaml @@ -263,11 +263,7 @@ jobs: run: cd build; ctest . -V -L CORE -j${{env.linux-vcpus}} - name: Check cleanup run: | - rm -r build - rm scripts/bash-autocomplete/cbmc.sh - make -C unit clean - make -C regression clean - make -C jbmc/regression clean + cmake --build build --target clean if [[ $(git status --ignored --porcelain | grep -v .ccache/) ]] ; then git status --ignored exit 1 diff --git a/jbmc/CMakeLists.txt b/jbmc/CMakeLists.txt index 9b606f01185..fc96e0b274a 100644 --- a/jbmc/CMakeLists.txt +++ b/jbmc/CMakeLists.txt @@ -31,8 +31,36 @@ add_custom_target(java-models-library ALL ) install( - FILES - "${CMAKE_CURRENT_SOURCE_DIR}/lib/java-models-library/target/core-models.jar" - "${CMAKE_CURRENT_SOURCE_DIR}/lib/java-models-library/target/cprover-api.jar" - DESTINATION ${CMAKE_INSTALL_LIBDIR} + FILES + "${CMAKE_CURRENT_SOURCE_DIR}/lib/java-models-library/target/core-models.jar" + "${CMAKE_CURRENT_SOURCE_DIR}/lib/java-models-library/target/cprover-api.jar" + DESTINATION ${CMAKE_INSTALL_LIBDIR} ) + +# java regression tests +file(GLOB_RECURSE java_regression_sources "regression/**/*.java,regression/**/*.kt,regression/**/*.j,regression/**/pom.xml") +file(GLOB java_regression_test_dirs LIST_DIRECTORIES true "regression/*/*") +foreach(dir ${java_regression_test_dirs}) + # TODO: remove the last condition as soon as jbmc/deterministic_assignments_json has been converted + IF(IS_DIRECTORY ${dir} AND EXISTS "${dir}/pom.xml" AND NOT EXISTS "${dir}/Foo.class") + list(APPEND java_regression_compiled_sources "${dir}/target") + ENDIF() +endforeach() + +add_custom_command(OUTPUT ${java_regression_compiled_sources} + COMMAND ${MAVEN_PROGRAM} --quiet clean package -T1C + WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}/regression + DEPENDS ${java_regression_sources} +) + +add_custom_target(java-regression ALL + DEPENDS ${java_regression_compiled_sources} +) + +# Clean up +file(GLOB_RECURSE out_files "regression/**/*.out") +file(GLOB_RECURSE goto_binary_files "regression/**/*.gb") +set_property( + TARGET java-regression + APPEND + PROPERTY ADDITIONAL_CLEAN_FILES ${java_regression_compiled_sources} ${out_files} ${goto_binary_files} regression/tests.log regression/tests-symex-driven-loading.log) diff --git a/jbmc/regression/Makefile b/jbmc/regression/Makefile index 4a052c618d7..c0f14f105c6 100644 --- a/jbmc/regression/Makefile +++ b/jbmc/regression/Makefile @@ -16,6 +16,7 @@ DIRS = janalyzer \ # Run all test directories in sequence .PHONY: test test: + mvn --quiet clean package -T1C @for dir in $(DIRS); do \ $(MAKE) "$$dir" || exit 1; \ done; @@ -30,6 +31,7 @@ $(DIRS): .PHONY: test-parallel .NOTPARALLEL: test-parallel test-parallel: + mvn --quiet clean package -T1C @echo "Building with $(JOBS) jobs" parallel \ --halt soon,fail=1 \ @@ -43,6 +45,7 @@ test-parallel: .PHONY: clean clean: + mvn --quiet clean -T1C @for dir in *; do \ if [ -d "$$dir" ]; then \ $(MAKE) -C "$$dir" clean; \ diff --git a/jbmc/regression/jbmc/ArithmeticException1/ArithmeticExceptionTest.class b/jbmc/regression/jbmc/ArithmeticException1/ArithmeticExceptionTest.class deleted file mode 100644 index 3ad4e6ebe86..00000000000 Binary files a/jbmc/regression/jbmc/ArithmeticException1/ArithmeticExceptionTest.class and /dev/null differ diff --git a/jbmc/regression/jbmc/ArithmeticException1/pom.xml b/jbmc/regression/jbmc/ArithmeticException1/pom.xml new file mode 100644 index 00000000000..5c2c9c85ddb --- /dev/null +++ b/jbmc/regression/jbmc/ArithmeticException1/pom.xml @@ -0,0 +1,30 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc.ArithmeticException1 + 1.0-SNAPSHOT + + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + + + + + maven-jar-plugin + + + default-jar + none + + + + + + + \ No newline at end of file diff --git a/jbmc/regression/jbmc/ArithmeticException1/ArithmeticExceptionTest.java b/jbmc/regression/jbmc/ArithmeticException1/src/main/java/ArithmeticExceptionTest.java similarity index 100% rename from jbmc/regression/jbmc/ArithmeticException1/ArithmeticExceptionTest.java rename to jbmc/regression/jbmc/ArithmeticException1/src/main/java/ArithmeticExceptionTest.java diff --git a/jbmc/regression/jbmc/ArithmeticException1/test.desc b/jbmc/regression/jbmc/ArithmeticException1/test.desc index 0577e08a51b..a07a8ddb801 100644 --- a/jbmc/regression/jbmc/ArithmeticException1/test.desc +++ b/jbmc/regression/jbmc/ArithmeticException1/test.desc @@ -1,6 +1,6 @@ CORE ArithmeticExceptionTest ---throw-runtime-exceptions +--throw-runtime-exceptions -cp target/classes ^EXIT=10$ ^SIGNAL=0$ ^.*assertion at file ArithmeticExceptionTest.java line 8 function.*: FAILURE$ diff --git a/jbmc/regression/jbmc/classpath-jar-load-whole-jar/pom.xml b/jbmc/regression/jbmc/classpath-jar-load-whole-jar/pom.xml index ec40251b157..a87d85ac3bd 100644 --- a/jbmc/regression/jbmc/classpath-jar-load-whole-jar/pom.xml +++ b/jbmc/regression/jbmc/classpath-jar-load-whole-jar/pom.xml @@ -4,9 +4,15 @@ xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd"> 4.0.0 org.cprover.regression - regression + regression.jbmc.classpath-jar-load-whole-jar 1.0-SNAPSHOT + + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + + jar-file @@ -24,9 +30,4 @@ - - 1.8 - 1.8 - - diff --git a/jbmc/regression/jbmc/classpath-jar-load-whole-jar/target/jar-file.jar b/jbmc/regression/jbmc/classpath-jar-load-whole-jar/target/jar-file.jar deleted file mode 100644 index d78794d6973..00000000000 Binary files a/jbmc/regression/jbmc/classpath-jar-load-whole-jar/target/jar-file.jar and /dev/null differ diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml new file mode 100644 index 00000000000..2adebdfa2d4 --- /dev/null +++ b/jbmc/regression/jbmc/pom.xml @@ -0,0 +1,22 @@ + + + 4.0.0 + org.cprover.regression + regression.jbmc + 1.0-SNAPSHOT + pom + + + org.cprover.regression + regression + 1.0-SNAPSHOT + + + + ArithmeticException1 + classpath-jar-load-whole-jar + + + \ No newline at end of file diff --git a/jbmc/regression/pom.xml b/jbmc/regression/pom.xml new file mode 100644 index 00000000000..9cb0f685389 --- /dev/null +++ b/jbmc/regression/pom.xml @@ -0,0 +1,68 @@ + + + 4.0.0 + org.cprover.regression + regression + 1.0-SNAPSHOT + pom + + + 1.8 + 1.8 + + + + jbmc + + + + + + + org.apache.maven.plugins + maven-jar-plugin + 3.4.2 + + + + org.apache.maven.plugins + maven-surefire-plugin + 3.5.2 + + true + + + + + org.apache.maven.plugins + maven-compiler-plugin + 3.13.0 + + + default-testCompile + test-compile + + testCompile + + + true + + + + + + + org.apache.maven.plugins + maven-resources-plugin + 3.3.1 + + true + + + + + + + diff --git a/jbmc/src/jbmc/CMakeLists.txt b/jbmc/src/jbmc/CMakeLists.txt index 9010f0dd975..c1735e3ed94 100644 --- a/jbmc/src/jbmc/CMakeLists.txt +++ b/jbmc/src/jbmc/CMakeLists.txt @@ -32,8 +32,8 @@ add_executable(jbmc jbmc_main.cpp) target_link_libraries(jbmc jbmc-lib) install(TARGETS jbmc DESTINATION ${CMAKE_INSTALL_BINDIR}) -# make sure java-models-library is built at least once -add_dependencies(jbmc java-models-library) +# make sure java-models-library and java-regression is built at least once +add_dependencies(jbmc java-models-library java-regression) # Man page if(NOT WIN32) diff --git a/regression/CMakeLists.txt b/regression/CMakeLists.txt index ea9c02a753d..964d2b3e2b6 100644 --- a/regression/CMakeLists.txt +++ b/regression/CMakeLists.txt @@ -99,3 +99,16 @@ if(WITH_MEMORY_ANALYZER) add_subdirectory(memory-analyzer) add_subdirectory(extract_type_header) endif() + +# Clean up +add_custom_target(cbmc-regression ALL) + +add_dependencies(cbmc cbmc-regression) + +file(GLOB_RECURSE out_files "**/*.out") +file(GLOB_RECURSE solver_files "**/*.dimacs,**/*.json") +file(GLOB_RECURSE goto_binary_files "**/*.gb,**/*.goto") +set_property( + TARGET cbmc-regression + APPEND + PROPERTY ADDITIONAL_CLEAN_FILES ${out_files} ${goto_binary_files} ${solver_files} tests.log)