From db2f7b5631d9465b9ee8b2b5b32efb45fba01b0d Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 10 Nov 2024 22:20:51 +0000 Subject: [PATCH 1/5] Use Maven to compile all regression test sources upfront (CMake) This commit adds the CMake integration to call Maven to compile the test sources. --- jbmc/CMakeLists.txt | 28 ++++++++++++--- jbmc/regression/jbmc/pom.xml | 22 ++++++++++++ jbmc/regression/pom.xml | 68 ++++++++++++++++++++++++++++++++++++ jbmc/src/jbmc/CMakeLists.txt | 4 +-- 4 files changed, 116 insertions(+), 6 deletions(-) create mode 100644 jbmc/regression/jbmc/pom.xml create mode 100644 jbmc/regression/pom.xml diff --git a/jbmc/CMakeLists.txt b/jbmc/CMakeLists.txt index 9b606f01185..561f89a5799 100644 --- a/jbmc/CMakeLists.txt +++ b/jbmc/CMakeLists.txt @@ -31,8 +31,28 @@ 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} ) 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) From d878b5dcadbb4b1b328ee80a6a506948c715f5dc Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 24 Nov 2024 21:54:16 +0000 Subject: [PATCH 2/5] Use Maven to compile all regression test sources upfront (Make) This commit adds the Make integration to call Maven to compile the test sources. --- jbmc/regression/Makefile | 3 +++ 1 file changed, 3 insertions(+) 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; \ From e6e8fbf679c836a58882a05b67fbb1743114974e Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 10 Nov 2024 22:23:06 +0000 Subject: [PATCH 3/5] Compile jbmc/ArithmeticException1 test sources Add pom.xml for compilation, move sources remove obsolete pre-compiled class file. --- .../ArithmeticExceptionTest.class | Bin 818 -> 0 bytes .../jbmc/ArithmeticException1/pom.xml | 30 ++++++++++++++++++ .../main/java}/ArithmeticExceptionTest.java | 0 .../jbmc/ArithmeticException1/test.desc | 2 +- 4 files changed, 31 insertions(+), 1 deletion(-) delete mode 100644 jbmc/regression/jbmc/ArithmeticException1/ArithmeticExceptionTest.class create mode 100644 jbmc/regression/jbmc/ArithmeticException1/pom.xml rename jbmc/regression/jbmc/ArithmeticException1/{ => src/main/java}/ArithmeticExceptionTest.java (100%) diff --git a/jbmc/regression/jbmc/ArithmeticException1/ArithmeticExceptionTest.class b/jbmc/regression/jbmc/ArithmeticException1/ArithmeticExceptionTest.class deleted file mode 100644 index 3ad4e6ebe86e52587843990ffa9af01256fb2197..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 818 zcmZuvPfrs;6#u>Mw%cwCmR6w@5Kz#fwp0nF!GSUnVYczHeWE_8W~icmvy)g8 z^|!^441aIfUY`eqsGHerGtcfqreI zpT!CCQt~sYvVk|wcj7&}c@4Va zLk82l=F%kF@mZh@Kp8W<7f?Z!GeZ8%XovT@(<=K5;qyy=2VdY^p!fss;We_qu2QbY z#)1^(I%|VpV1^aFv?Pzq$zz@|;(ybE~lC0yq#od5e0jVv;ym(u+b2N^v43vqX+?f?J) 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$ From 3de45e9d6f28ac6bd5ca5a457dbc4d807016d62e Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Sun, 10 Nov 2024 22:24:17 +0000 Subject: [PATCH 4/5] Compile jbmc/classpath-jar-load-whole-jar test sources Fix pom.xml for compilation, remove obsolete pre-compiled jar file. --- .../jbmc/classpath-jar-load-whole-jar/pom.xml | 13 +++++++------ .../target/jar-file.jar | Bin 4456 -> 0 bytes 2 files changed, 7 insertions(+), 6 deletions(-) delete mode 100644 jbmc/regression/jbmc/classpath-jar-load-whole-jar/target/jar-file.jar 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 d78794d6973bfe2b92c149087edd0e89eb653ef9..0000000000000000000000000000000000000000 GIT binary patch literal 0 HcmV?d00001 literal 4456 zcmbVQ2{_c-8y+SxsZ6%GqHE8RrH#tXKDNtXEZt}sj3vupCe6qmm5e1WvQ@@XDQk;c z=-M(3k$q2g63TKdMRR|X82!@!f1iGyS)RxDzUQ3xeCPY#GsXtcOn@sc|9vI(x$!-yndt!+ z$wE%rz`fh^(ajvX4RUo3ul>%32vd6DDjibX&5Gzu^yONTmq^QizPezaSx*hVKEBV~ z#o>-n6`zzhUj4ifD$9IOvOQtIKB&Q?+Fca+&c2h~RCkJHbrBHA!K;GbtaTHx2&|{W z+A<-Kk0C3YXG({yV;!W!r2D|9%h0-#6W2Dul%y=8T?JQe5@dm6RP41z;$fmR|7UAUf3=zEP$vg3{buzoH?JuSHoy9rv zHon!rSzDibPLD6MHCyZ1Ij`JgLR-#kzajtI7Ec?yKaRnp6J9^DHautkZuw+{lBayv z6*$*s+8bf~y*!12dpW!6XYl&7DWR+C^wqG--NpQZq5907?WHovk77Imye*K7Dz? z=K`yH=*6u&=1^NvBsS`!oJUD;a?^vu!Z$i~wE1|SS`;Rk-(66TtCG1KlAWGl(2Az< z+Ron>DAz+1g|iNJS>zKMyOkAfEf9|iyilS^!&jr)T5BzwYwE&+$9vrVGF3XlEx4S2 zS{5UNs~qL3qQ!9`%H&D+clPI4XH}y~H~jbi&cS_EMZ%Bk1{FtJ;+btsK}G6GBHE{} zW4H1BI-^oLiCp08dK)w=!?%@a`FMWq=&Yy)#dgKk0E$UKArSEmRRad~D9NAbqL|UTv;(WP4rK9o9EV!cB^y3n%>T+V+xNFjakJa_i19Rbc37!5;mCZW3I*=swscsqhJg}7Vh{9GyP9llR1}$)X>3y2 zV$8;7@ULZg39-$`0wOhvgChj_dfrar&o_Shytu^d9^!F{t%5s^o3d%2&wTJ;RkK7l zCwYb%1V^5{3#;gE_I~WQ_o07W2*x4#sQ842chgul|K$uPwwUfk{X0tU4|RqiWGv(R zO|1CwhaVL<4WsWaR~Vc#d~u_@Q^wb!^D{N4en{VK5CStT?@+xAOM5JS|Gtc(yu}HY zWHN;Vx+G~cTS#)?pFbXI1YHi}s6QGbG{+xPM~YJ1{+U_%OlvDgQF8;RE^8*5r+x&4 z3IYUE*jO-7)d6W{T&53HAK#|*(C`KeY|u{ZiOLcJ%3F$iOW79v_eprY!ptJfgIa&0 zG~okuX^)2z&y;^e?8X=f>0DcDsB!QJtgg=6Wlv})`*SbEzGw3 zyYy7v$&qrEnPSgsr%d)!wNI`+qw#7M{dutONK>ZW^Qut@dxkz?U>sJrx!vHd>*sgwBSJ__w=R6!%GK;9(WC)1q68ubErNy2Ryb zp*;d4E(GLme<68Gcf7S>g`I&ueiel-KG5dJo~7yM|VYE#x|I~pM|1-x1bZn3~z(x_PA|Is! zInW1`QRSbZbH}>M5nNqDP=?3>1$fDbrPdRQ96PJo6NF<%i^!vZ$Kz*nt5VVtp@JPo zT{mB~dl&=-y`atvmn;&}@`_MhgRFT*{3X&kFUT*{4IZGLp5pO8?H614T=3O#hgt#M zo1#`l=K1r_tV}zvLLEhp2+ymLvfs`$UFwNqv7k=R>=dtwLGA3AB8XAm?ODh_Zrwmj z`iEEMA=#{xm?};hGTM9cWllKvv4}<2PfIdY)QQb`B$XhKvV4B$+U<${7dcdh`BKgV znpriS=QtV>dqvBjUdbl)aW8X71MZl6$Uj+}jkd~}q~22fI^2P0-N$-VvHq$h3f_nZ zYQzb1F6u(gpS-ncj)8x}tSqva5UP2BO$U9$k4@X5uP#1spz=}^%WkJ9k6$~Gme2Z0 zgBD05-cFA~SY}PSs&udlIa5oHl=88&!cUm@E^$Y|GW-vfKM9?PEvSo8tuIw~+&x3c zV?TEysg8#O=l@G^L&sfy!3%^48!ki>v0Oms9i${6RaL+`Hgn>Gah!6K6^t-ug&0BM zq~%?<`B}u8dXPNc%UE#9Lft> zYp_>eR?pBxH_PmUp{zmefa!MX9&>kDLraAMGlc_%%pzQxEVp~%ETT|NgPek9a{tRE z6)Vl(ps&xUQUcC!(BL_<J7cHMM8zw*$hx*a%$bOgiQGmv2GP51Wh>9U@W^z(&%o1-=lYSq zDHaS8@FeK|pFxrWB3Zi)tP*T|A6TVG53Bjy3V@`StWN_{VelS=&w<{C+0q2G}zHv)j w9Uwi>?Put}Hb{o58&_b)C>ZviSOk3(Mm;t*U;%Op0@(rl39~>TieF02zfICdtpET3 From fc8cfc254e462dd41163ef039c30159a8185bd8f Mon Sep 17 00:00:00 2001 From: Peter Schrammel Date: Tue, 12 Nov 2024 20:55:11 +0000 Subject: [PATCH 5/5] Use cmake for cleaning in cmake job which makes more sense than building with cmake and cleaning with make. --- .github/workflows/pull-request-checks.yaml | 6 +----- jbmc/CMakeLists.txt | 8 ++++++++ regression/CMakeLists.txt | 13 +++++++++++++ 3 files changed, 22 insertions(+), 5 deletions(-) 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 561f89a5799..fc96e0b274a 100644 --- a/jbmc/CMakeLists.txt +++ b/jbmc/CMakeLists.txt @@ -56,3 +56,11 @@ add_custom_command(OUTPUT ${java_regression_compiled_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/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)