Use Maven to compile all regression test sources upfront

and give two examples of how this works: - jbmc/ArithmeticException1 (single source file) - jbmc/classpath-jar-load-whole-jar (jar)
diffblue · Nov 10, 2024 · d2209c3 · d2209c3
1 parent 83f61a4
commit d2209c3
Show file tree

Hide file tree

Showing 10 changed files with 154 additions and 13 deletions.
diff --git 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 package
+    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/ArithmeticException1/ArithmeticExceptionTest.class b/jbmc/regression/jbmc/ArithmeticException1/ArithmeticExceptionTest.class
diff --git a/jbmc/regression/jbmc/ArithmeticException1/pom.xml b/jbmc/regression/jbmc/ArithmeticException1/pom.xml
@@ -0,0 +1,30 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project xmlns="http://maven.apache.org/POM/4.0.0"
+         xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+         xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
+    <modelVersion>4.0.0</modelVersion>
+    <groupId>org.cprover.regression</groupId>
+    <artifactId>regression.jbmc.ArithmeticException1</artifactId>
+    <version>1.0-SNAPSHOT</version>
+
+    <parent>
+        <groupId>org.cprover.regression</groupId>
+        <artifactId>regression.jbmc</artifactId>
+        <version>1.0-SNAPSHOT</version>
+    </parent>
+
+    <build>
+        <plugins>
+            <plugin>
+                <artifactId>maven-jar-plugin</artifactId>
+                <executions>
+                    <execution>
+                        <id>default-jar</id>
+                        <phase>none</phase>
+                    </execution>
+                </executions>
+            </plugin>
+        </plugins>
+    </build>
+
+</project>
diff --git a/...icException1/ArithmeticExceptionTest.java → ...rc/main/java/ArithmeticExceptionTest.java b/...icException1/ArithmeticExceptionTest.java → ...rc/main/java/ArithmeticExceptionTest.java
diff --git 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
@@ -4,9 +4,15 @@
          xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
   <modelVersion>4.0.0</modelVersion>
   <groupId>org.cprover.regression</groupId>
-  <artifactId>regression</artifactId>
+  <artifactId>regression.jbmc.classpath-jar-load-whole-jar</artifactId>
   <version>1.0-SNAPSHOT</version>
 
+  <parent>
+    <groupId>org.cprover.regression</groupId>
+    <artifactId>regression.jbmc</artifactId>
+    <version>1.0-SNAPSHOT</version>
+  </parent>
+
   <build>
     <finalName>jar-file</finalName>
     <plugins>
@@ -24,9 +30,4 @@
     </plugins>
   </build>
 
-  <properties>
-   <maven.compiler.source>1.8</maven.compiler.source>
-   <maven.compiler.target>1.8</maven.compiler.target>
-  </properties>
-
 </project>
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
diff --git a/jbmc/regression/jbmc/pom.xml b/jbmc/regression/jbmc/pom.xml
@@ -0,0 +1,22 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project xmlns="http://maven.apache.org/POM/4.0.0"
+         xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+         xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
+    <modelVersion>4.0.0</modelVersion>
+    <groupId>org.cprover.regression</groupId>
+    <artifactId>regression.jbmc</artifactId>
+    <version>1.0-SNAPSHOT</version>
+    <packaging>pom</packaging>
+
+    <parent>
+        <groupId>org.cprover.regression</groupId>
+        <artifactId>regression</artifactId>
+        <version>1.0-SNAPSHOT</version>
+    </parent>
+
+    <modules>
+        <module>ArithmeticException1</module>
+        <module>classpath-jar-load-whole-jar</module>
+    </modules>
+
+</project>
diff --git a/jbmc/regression/pom.xml b/jbmc/regression/pom.xml
@@ -0,0 +1,68 @@
+<?xml version="1.0" encoding="UTF-8"?>
+<project xmlns="http://maven.apache.org/POM/4.0.0"
+         xmlns:xsi="http://www.w3.org/2001/XMLSchema-instance"
+         xsi:schemaLocation="http://maven.apache.org/POM/4.0.0 http://maven.apache.org/xsd/maven-4.0.0.xsd">
+    <modelVersion>4.0.0</modelVersion>
+    <groupId>org.cprover.regression</groupId>
+    <artifactId>regression</artifactId>
+    <version>1.0-SNAPSHOT</version>
+    <packaging>pom</packaging>
+
+    <properties>
+        <maven.compiler.source>1.8</maven.compiler.source>
+        <maven.compiler.target>1.8</maven.compiler.target>
+    </properties>
+
+    <modules>
+        <module>jbmc</module>
+    </modules>
+
+    <build>
+        <pluginManagement>
+            <plugins>
+                <plugin>
+                    <groupId>org.apache.maven.plugins</groupId>
+                    <artifactId>maven-jar-plugin</artifactId>
+                    <version>3.4.2</version>
+                </plugin>
+                <!-- turn off test running to save some time -->
+                <plugin>
+                    <groupId>org.apache.maven.plugins</groupId>
+                    <artifactId>maven-surefire-plugin</artifactId>
+                    <version>3.5.2</version>
+                    <configuration>
+                        <skipTests>true</skipTests>
+                    </configuration>
+                </plugin>
+                <!-- turn off test compilation to save some time  -->
+                <plugin>
+                    <groupId>org.apache.maven.plugins</groupId>
+                    <artifactId>maven-compiler-plugin</artifactId>
+                    <version>3.13.0</version>
+                    <executions>
+                        <execution>
+                            <id>default-testCompile</id>
+                            <phase>test-compile</phase>
+                            <goals>
+                                <goal>testCompile</goal>
+                            </goals>
+                            <configuration>
+                                <skip>true</skip>
+                            </configuration>
+                        </execution>
+                    </executions>
+                </plugin>
+                <!-- turn off resources copying to save some time  -->
+                <plugin>
+                    <groupId>org.apache.maven.plugins</groupId>
+                    <artifactId>maven-resources-plugin</artifactId>
+                    <version>3.3.1</version>
+                    <configuration>
+                        <skip>true</skip>
+                    </configuration>
+                </plugin>
+            </plugins>
+        </pluginManagement>
+    </build>
+
+</project>
diff --git 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)