Merge branch 'diffblue:develop' into develop

Author: yvizel

.clang-format-ignore

@@ -1,3 +1,4 @@
 jbmc/src/miniz/miniz.cpp
+jbmc/src/miniz/miniz.h
 src/cprover/wcwidth.c
 unit/catch/catch.hpp

.github/workflows/doxygen-check.yaml

@@ -8,7 +8,7 @@ jobs:
   check-doxygen:
     # Note that the versions used for this `check-doxygen` job should be kept in
     # sync with the `publish` job.
-    runs-on: ubuntu-22.04
+    runs-on: ubuntu-24.04
     steps:
     - uses: actions/checkout@v4
     - name: Fetch dependencies

.github/workflows/publish.yaml

@@ -6,31 +6,28 @@ jobs:
   publish:
     # Note that the versions used for this `publish` job should be kept in sync
     # with the `check-doxygen` job.
-    runs-on: ubuntu-22.04
+    runs-on: ubuntu-24.04
     steps:
       - name: Checkout repository
         uses: actions/checkout@v4
 
       - name: Install doxygen
         run: |
           sudo apt update
-          sudo apt install doxygen graphviz pandoc npm
-
-      - name: Install python modules
-        run: sudo python3 -m pip install gitpython pandocfilters
+          sudo apt-get install --no-install-recommends -y doxygen graphviz pandoc npm python3-git python3-pandocfilters
 
       - name: Install mermaid diagram filter
         run: |
           git clone https://github.com/raghur/mermaid-filter/
           cd mermaid-filter
-          sed -i '1s/{/{ "overrides": { "puppeteer": "^21" },/' package.json
-          sed -i '1s/^\/\/ //' index.js
           npm install --loglevel verbose
           sudo npm link --loglevel verbose
           cd ..
 
       - name: Build documentation
-        run: cd doc/doxygen-root && make && touch html/.nojekyll
+        run: |
+          echo 0 | sudo tee /proc/sys/kernel/apparmor_restrict_unprivileged_userns
+          cd doc/doxygen-root && make && touch html/.nojekyll
 
       - name: Publish documentation
         if: ${{ github.event_name == 'push' && startsWith('refs/heads/develop', github.ref) }}

CODEOWNERS

@@ -24,7 +24,7 @@
 /src/langapi/ @kroening @tautschnig @peterschrammel
 /src/xmllang/ @kroening @tautschnig @peterschrammel
 /src/solvers/flattening @martin-cs @kroening @tautschnig @peterschrammel
-/src/solvers/floatbv @martin-cs @kroening
+/src/solvers/floatbv @martin-cs @kroening @peterschrammel
 /src/solvers/miniBDD @tautschnig @kroening
 /src/solvers/prop @martin-cs @kroening @tautschnig @peterschrammel
 /src/solvers/sat @martin-cs @kroening @tautschnig @peterschrammel
@@ -43,13 +43,13 @@
 /jbmc/src/java_bytecode/ @peterschrammel @TGWDB
 /src/analyses/ @martin-cs @peterschrammel
 /src/pointer-analysis/ @martin-cs @peterschrammel
-/src/libcprover-cpp @esteffin @TGWDB @peterschrammel
-/src/libcprover-rust @TGWDB @peterschrammel @esteffin
+/src/libcprover-cpp @TGWDB @peterschrammel
+/src/libcprover-rust @TGWDB @peterschrammel
 
 # These files change frequently and changes are medium-risk
 
 /src/goto-analyzer/ @martin-cs @peterschrammel
-/src/goto-bmc/ @esteffin @TGWDB @peterschrammel
+/src/goto-bmc/ @TGWDB @peterschrammel
 /src/goto-harness/ @martin-cs @peterschrammel
 /src/goto-instrument/ @martin-cs @peterschrammel @tautschnig @kroening
 /src/goto-instrument/contracts/ @tautschnig @feliperodri @remi-delmas-3000
@@ -62,8 +62,8 @@
 /jbmc/src/jdiff/ @peterschrammel
 /src/cpp/ @kroening @tautschnig @peterschrammel
 /src/solvers/smt2 @kroening @martin-cs @peterschrammel @TGWDB
-/src/solvers/smt2_incremental @peterschrammel @thomasspriggs @TGWDB @esteffin
-/src/solvers/Makefile @kroening @tautschnig @peterschrammel @TGWDB @esteffin
+/src/solvers/smt2_incremental @peterschrammel @thomasspriggs @TGWDB
+/src/solvers/Makefile @kroening @tautschnig @peterschrammel @TGWDB
 /src/statement-list/ @kroening @tautschnig @peterschrammel
 
 /cmake/        @diffblue/diffblue-opensource

doc/API/util/piped_process.md

@@ -1,6 +1,7 @@
-\page piped-process `src/util/piped_process.{cpp, h}`
+\page piped-process The `piped_process` API
 
-To utilise the `piped_process` API for interprocess communication with any binary:
+To utilise the `piped_process` API (`src/util/piped_process.{cpp, h}`) for
+interprocess communication with any binary:
 
 * You need to initialise it by calling the construct `piped_processt("binary with args")`.
   * If IPC fails before child process creation, you will get a `system_exceptiont`.

doc/architectural/front-page.md

@@ -54,7 +54,7 @@ license</a>.
 Overview of Documentation
 =======
 
-### For users:
+## For users:
 
 * The [CPROVER User Manual](http://www.cprover.org/cprover-manual/) details the
   capabilities of CBMC and describes how to install and use these tools. It
@@ -68,7 +68,7 @@ you can access it <a href=
 * \subpage memory-bounds-checking
 * \subpage satabs
 
-### For contributors:
+## For contributors:
 
 The following pages attempt to provide the information that a developer needs to
 work on CBMC, in a sensible order. In many cases they link to the appropriate

doc/architectural/goto-program-transformations.md

@@ -176,7 +176,7 @@ This pass adds failed symbols to the symbol table. See
 `src/pointer-analysis/add_failed_symbols.h` for details. The implementation of
 this pass is called via \ref add_failed_symbols(symbol_table_baset &) . The
 purpose of failed symbols is explained in the documentation of the function \ref
-goto_symext::dereference(exprt &, statet &, bool)
+goto_symext::dereference(exprt &, goto_symex_statet &, bool)
 
 <em>Predecessor pass is \ref update-transform or the optional \ref
 nondet-transform if it is being used.</em>

doc/assets/xml_spec.md

@@ -475,7 +475,7 @@ The path from the input C code to XML trace goes through the following
 steps:\
 `C` → `GOTO` → `SSA` → `GOTO Trace` → `XML Trace`
 
-#### SSA to GOTO Trace
+### SSA to GOTO Trace
 
 SSA steps are sorted by clocks and the following steps are skipped: PHI,
 GUARD assignments; shared-read, shared-write, constraint, spawn,

doc/man/cbmc.1

@@ -334,6 +334,13 @@ set malloc failure mode to return null
 \fB\-\-string\-abstraction\fR
 track C string lengths and zero\-termination
 .TP
+\fB\-\-dfcc\-debug\-lib\fR
+enable debug assertions in the cprover contracts library
+.TP
+\fB\-\-dfcc\-simple\-invalid\-pointer\-model\fR
+use simplified invalid pointer model in the cprover contracts library
+(faster, unsound)
+.TP
 \fB\-\-reachability\-slice\fR
 remove instructions that cannot appear on a trace
 from entry point to a property

doc/man/goto-analyzer.1

@@ -409,6 +409,9 @@ perform taint analysis using rules in given file
 \fB\-\-show\-taint\fR
 print taint analysis results on stdout
 .TP
+\fB\-\-show\-local\-bitvector\fR
+perform procedure\-local bitvector analysis
+.TP
 \fB\-\-show\-local\-may\-alias\fR
 perform procedure\-local may alias analysis
 .SS "C/C++ frontend options:"
@@ -582,6 +585,13 @@ set malloc failure mode to return null
 .TP
 \fB\-\-string\-abstraction\fR
 track C string lengths and zero\-termination
+.TP
+\fB\-\-dfcc\-debug\-lib\fR
+enable debug assertions in the cprover contracts library
+.TP
+\fB\-\-dfcc\-simple\-invalid\-pointer\-model\fR
+use simplified invalid pointer model in the cprover contracts library
+(faster, unsound)
 .SS "Standard Checks"
 From version \fB6.0\fR onwards, \fBcbmc\fR, \fBgoto-analyzer\fR and some other tools
 apply some checks to the program by default (called the "standard checks"), with the

doc/man/goto-instrument.1

@@ -706,6 +706,13 @@ do not allow malloc calls to fail by default
 \fB\-\-string\-abstraction\fR
 track C string lengths and zero\-termination
 .TP
+\fB\-\-dfcc\-debug\-lib\fR
+enable debug assertions in the cprover contracts library
+.TP
+\fB\-\-dfcc\-simple\-invalid\-pointer\-model\fR
+use simplified invalid pointer model in the cprover contracts library
+(faster, unsound)
+.TP
 \fB\-\-model\-argc\-argv\fR \fIn\fR
 Create up to \fIn\fR non-deterministic C strings as entries to \fIargv\fR and
 set \fIargc\fR accordingly. In absence of such modelling, \fIargv\fR is left

jbmc/CMakeLists.txt

@@ -31,8 +31,30 @@ 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}
+)
+
+add_dependencies(java-regression java-models-library)

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; \

jbmc/regression/book-examples/BinarySearch/BinarySearch.class

@@ -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.book-examples.BinarySearch</artifactId>
+    <version>1.0-SNAPSHOT</version>
+
+    <parent>
+        <groupId>org.cprover.regression</groupId>
+        <artifactId>regression.book-examples</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>

jbmc/regression/book-examples/BinarySearch/pom.xml

@@ -1,6 +1,6 @@
 CORE
 BinarySearch.binarySearch
- --throw-runtime-exceptions --unwind 2
+ --throw-runtime-exceptions --unwind 2 -cp target/classes
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/book-examples/BinarySearch/runtime_exception.desc

@@ -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.book-examples.LocatorHandler</artifactId>
+    <version>1.0-SNAPSHOT</version>
+
+    <parent>
+        <groupId>org.cprover.regression</groupId>
+        <artifactId>regression.book-examples</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>

jbmc/regression/book-examples/BinarySearch/BinarySearch.java renamed to jbmc/regression/book-examples/BinarySearch/src/main/java/BinarySearch.java

@@ -1,6 +1,6 @@
 CORE
 LocatorHandler.autoLocator
---max-nondet-string-length 10 --unwind 10 --classpath `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
+--max-nondet-string-length 10 --unwind 10 --classpath `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$

jbmc/regression/book-examples/LocatorHandler/IdLocator.class

@@ -1,6 +1,6 @@
 CORE
 EquivalenceCheck.check
-
+-cp target/classes
 ^EXIT=0$
 ^SIGNAL=0$
 ^VERIFICATION SUCCESSFUL$

jbmc/regression/book-examples/LocatorHandler/Locator.class

@@ -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.book-examples.SignalUtil</artifactId>
+    <version>1.0-SNAPSHOT</version>
+
+    <parent>
+        <groupId>org.cprover.regression</groupId>
+        <artifactId>regression.book-examples</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>

jbmc/regression/book-examples/LocatorHandler/LocatorHandler$1.class

@@ -1,6 +1,6 @@
 CORE
 StringUtil.getLastToken
---max-nondet-string-length 100 --unwind 2 --classpath `../../../../scripts/format_classpath.sh . ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
+--max-nondet-string-length 100 --unwind 2 --classpath `../../../../scripts/format_classpath.sh target/classes ../../../lib/java-models-library/target/core-models.jar ../../../lib/java-models-library/target/cprover-api.jar`
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$