Merge branch 'diffblue:develop' into loop_invariant_synthesis

Author: qinheping

CODEOWNERS

@@ -12,7 +12,7 @@
 # These files should rarely change
 
 /src/big-int/ @kroening
-/src/ansi-c/ @kroening @tautschnig @chris-ryder
+/src/ansi-c/ @kroening @tautschnig @chris-ryder @peterschrammel @remi-delmas-3000
 /src/assembler/ @kroening @tautschnig @chris-ryder
 /src/goto-cc/ @kroening @tautschnig @chris-ryder
 /src/linking/ @kroening @tautschnig @chris-ryder
@@ -31,6 +31,7 @@
 /src/solvers/sat @martin-cs @kroening @tautschnig @peterschrammel
 /src/symtab2gb/ @martin-cs
 /jbmc/src/miniz/ @peterschrammel
+/src/crangler/ @kroening @tautschnig @qinheping
 
 
 # These files change frequently and changes are high-risk
@@ -51,7 +52,7 @@
 /src/goto-harness/ @martin-cs @chris-ryder @peterschrammel
 /src/goto-instrument/ @martin-cs @chris-ryder @peterschrammel @tautschnig @kroening
 /src/goto-instrument/contracts/ @tautschnig @feliperodri @remi-delmas-3000
-/doc/cprover-manual/contracts* @tautschnig @feliperodri @remi-delmas-3000
+/src/goto-instrument/synthesizer/ @qinheping @tautschnig @feliperodri @remi-delmas-3000
 /src/goto-diff/ @tautschnig @peterschrammel
 /src/jsil/ @kroening @tautschnig
 /src/memory-analyzer/ @tautschnig @chris-ryder @kroening
@@ -77,7 +78,6 @@ CMakeLists.txt @diffblue/diffblue-opensource
 /jbmc/regression/
 
 /scripts/ @diffblue/diffblue-opensource
-/scripts/expected_doxygen_warnings.txt
 
 # CI pipeline is the responsibility of the Open Source maintenance team at Diffblue.
 /.github/ @diffblue/diffblue-opensource

doc/architectural/folder-walkthrough.md

@@ -4,7 +4,7 @@
 
 \author Martin Brain, Peter Schrammel
 
-## `src/` ##
+## `src/`
 
 The source code is divided into a number of sub-directories, each
 containing the code for a different part of the system.
@@ -55,7 +55,7 @@ containing the code for a different part of the system.
 
 In the top level of `src` there are only a few files:
 
-* `config.inc`:   The user-editable configuration parameters for the
+* `config.inc`: The user-editable configuration parameters for the
   build process. The main use of this file is setting the paths for the
   various external SAT solvers that are used. As such, anyone building
   from source will likely need to edit this.
@@ -69,24 +69,24 @@ In the top level of `src` there are only a few files:
 
 * `doxygen.cfg`:   The config file for doxygen.cfg
 
-## `doc/` ##
+## `doc/`
 
 Contains the CBMC man page. Doxygen HTML pages are generated
 into the `doc/html` directory when running `doxygen` from `src`.
 
-## `regression/` ##
+## `regression/`
 
 The `regression/` directory contains the regression test suites. See
 \ref compilation-and-development for information on how to run and
 develop regression tests.
 
-## `unit/` ##
+## `unit/`
 
 The `unit/` directory contains the unit test suites. See
 \ref compilation-and-development for information on how to run and
 develop unit tests.
 
-## Directory dependencies ##
+## Directory dependencies
 
 This diagram shows *intended* directory dependencies.  Arrows should
 be read transitively - dependencies of dependencies are often used

doc/cprover-manual/index.md

@@ -32,4 +32,8 @@
    * [Integration into Build Systems with goto-cc](goto-cc/)
    * [Integration with Visual Studio builds](visual-studio/)
 
-10. [The CPROVER API Reference](api/)
+10. Solvers
+
+    * [Incremental SMT solver](smt2-incr/)
+
+11. [The CPROVER API Reference](api/)

doc/cprover-manual/smt2-incr.md

@@ -0,0 +1,213 @@
+[CPROVER Manual TOC](../)
+
+## SMT 2 incremental backend
+
+CBMC supports many different smt solver backends. This document describes how to use the incremental
+smt2 solver. For other solver usages use `cbmc --help`.
+
+The incremental smt2 solver backend of CBMC is a solver-agnostic smt backend that allows the user to
+specify which smtlib 2.6 compliant solver CBMC should use. This choice increases the flexibility of
+CBMC as the user can easily switch solver at runtime also allowing custom parametrization of the
+solver to be used. Further, the backend exploits the incremental mode of the smt solver, so
+subsequent incremental SMT solver queries do not require a full re-evaluation of the entire SMT
+formula.
+
+### Supported features
+
+The incremental smt2 solver supports the following CBMC C features:
+
+* Integral types (including integers, characters and boolean). These are encoded into smt by using
+  bit-vectors,
+* Pointers. Encoded by using smt bit-vectors. This includes support for pointers to both stack and
+  heap-allocated memory,
+* Arrays. Encoded by using smt array theory.
+
+Currently, unsupported features include floating-point types, structs and unions.
+
+For more details on which features are supported see regression
+tests in [`regression/cbmc-incr-smt2`](../regression/cbmc-incr-smt2).
+
+The backend has been tested with these instrumentation passes:
+
+* `--bounds-check`,
+* `--conversion-check`,
+* `--div-by-zero-check`,
+* `--pointer-check`,
+* `--pointer-overflow-check`,
+* `--signed-overflow-check`,
+* `--unsigned-overflow-check`,
+* `--unwinding-assertions`.
+
+### Requisites
+
+To run the incremental smt2 backend it is necessary to have an smt solver that:
+
+* is runnable from the command line,
+* supports interactive mode from the command line,
+* supports smtlib 2.6 input,
+* supports incremental mode.
+
+Because of the way supported features are encoded the smt solver should be capable to handle arrays,
+bit-vectors, uninterpreted functions and quantifiers. Also, the solver should work with the `ALL`
+smt theory.
+
+At the time of writing the smt solvers tested in CI
+are [Z3](https://github.com/Z3Prover/z3)
+and [CVC5](https://cvc5.github.io/).
+
+### Usage
+
+To use the incremental SMT2 backend it is enough to add the `--incremental-smt2-solver` argument to
+the CBMC command line followed by the command to invoke the chosen solver using smtlib 2.6 input in
+interactive mode.
+
+Note that the use of the `--slice-formula` option is recommended at this time to slice out
+unnecessary code (that may not be supported at the moment) and this can also improve performance.
+
+Here are two examples to show how to analyse a file `program.c` using Z3 and CVC5 solvers.
+
+To use the Z3 SMT solver:
+
+```shell 
+cbmc --slice-formula --incremental-smt2-solver 'z3 -smt2 -in' program.c
+```
+
+If `z3` is not on the `PATH`, then it is enough to replace `'z3 -smt2 -in'`
+with `'<command-to-execute-z3> -smt2 -in'`,
+
+Similarly to execute CBMC using the CVC5 solver:
+
+```shell
+cbmc --slice-formula --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' program.c
+```
+
+As the command to execute the solver is left to the user, it is possible to fine-tune it by passing
+extra parameters (when the solver allows so). For example Z3 allows to set certain parameters by
+adding `param_name=value` to the command line, so to use the Z3 solver with `well_sorted_check`
+property set to `false` the following has to be run:
+
+```shell
+cbmc --slice-formula --incremental-smt2-solver 'z3 -smt2 -in well_sorted_check=false' program.c
+```
+
+### Examples
+
+Given a C program `program.c` as follows:
+
+```C
+int main()
+{
+  int x, y;
+  if(x != 0)
+    __CPROVER_assert(y != 4, "Assert of inequality to 4.");
+  else
+    __CPROVER_assert(y != 2, "Assert of inequality to 2.");
+  int z = y;
+  return 0;
+}
+```
+
+To analyze it we should run:
+
+```shell
+cbmc --incremental-smt2-solver 'z3 -smt2 -in' --slice-formula program.c
+```
+
+We will get the verification results as follows:
+
+```text
+CBMC version 5.70.0 (cbmc-5.70.0-53-g20535ad14d) 64-bit x86_64 macos
+Parsing program.c
+Converting
+Type-checking program
+Generating GOTO Program
+Adding CPROVER library (x86_64)
+Removal of function pointers and virtual functions
+Generic Property Instrumentation
+Running with 8 object bits, 56 offset bits (default)
+Starting Bounded Model Checking
+Runtime Symex: 0.00168879s
+size of program expression: 45 steps
+slicing removed 23 assignments
+Generated 2 VCC(s), 2 remaining after simplification
+Runtime Postprocess Equation: 2.1865e-05s
+Passing problem to incremental SMT2 solving via "z3 -smt2 -in"
+```
+
+Note here that the solver used by CBMC is `"z3 -smt2 -in"` as specified by the user.
+
+```text
+[continues]
+converting SSA
+Runtime Convert SSA: 0.00130809s
+Running incremental SMT2 solving via "z3 -smt2 -in"
+Runtime Solver: 0.0738685s
+Runtime decision procedure: 0.0765297s
+Running incremental SMT2 solving via "z3 -smt2 -in"
+Runtime Solver: 0.00535358s
+Runtime decision procedure: 0.00570765s
+
+** Results:
+program.c function main
+[main.assertion.1] line 5 Assert of inequality to 4.: FAILURE
+[main.assertion.2] line 7 Assert of inequality to 2.: FAILURE
+
+** 2 of 2 failed (3 iterations)
+VERIFICATION FAILED
+```
+
+As expected CBMC returns `FAILURE` for both assertions at lines `5` and `7`.
+
+The incremental smt2 backend also supports trace generation, so to get a trace that fails the
+assertions the `--trace` argument should be added, so the command to run is:
+
+```shell
+cbmc --incremental-smt2-solver 'z3 -smt2 -in' --slice-formula --trace program.c
+```
+
+This will append the trace to CBMC's output as follows:
+
+```text
+CBMC version 5.70.0 (cbmc-5.70.0-53-g20535ad14d) 64-bit x86_64 macos
+Parsing program.c
+[...]
+[main.assertion.1] line 5 Assert of inequality to 4.: FAILURE
+[main.assertion.2] line 7 Assert of inequality to 2.: FAILURE
+
+Trace for main.assertion.1:
+
+State 6 file program.c function main line 3 thread 0
+----------------------------------------------------
+  x=-1 (11111111 11111111 11111111 11111111)
+
+State 7 file program.c function main line 3 thread 0
+----------------------------------------------------
+  y=4 (00000000 00000000 00000000 00000100)
+
+Violated property:
+  file program.c function main line 5 thread 0
+  Assert of inequality to 4.
+  y != 4
+
+
+
+Trace for main.assertion.2:
+
+State 6 file program.c function main line 3 thread 0
+----------------------------------------------------
+  x=0 (00000000 00000000 00000000 00000000)
+
+State 7 file program.c function main line 3 thread 0
+----------------------------------------------------
+  y=2 (00000000 00000000 00000000 00000010)
+
+Violated property:
+  file program.c function main line 7 thread 0
+  Assert of inequality to 2.
+  y != 2
+
+
+
+** 2 of 2 failed (3 iterations)
+VERIFICATION FAILED
+```

doc/man/symtab2gb.1

@@ -15,8 +15,12 @@ This is to support integration of external language frontends, such as Ada
 (using GNAT2GOTO: https://github.com/diffblue/gnat2goto) or Rust (using Kani:
 https://github.com/model-checking/kani).
 .SH OPTIONS
+.TP
 \fB\-\-out\fR \fIoutfile\fR
 Specify the filename of the resulting binary (default: a.out)
+.TP
+\fB\-\-verbosity\fR #
+verbosity level
 .SH ENVIRONMENT
 All tools honor the TMPDIR environment variable when generating temporary
 files and directories.

jbmc/regression/jbmc-generics/constant_propagation/test.desc

@@ -3,9 +3,9 @@ Test
 --function Test.main --show-vcc
 ^EXIT=0$
 ^SIGNAL=0$
-^\{-\d+\} symex_dynamic::dynamic_object1#2\.\.@Generic\.\[email protected]\.\.@class_identifier = "java::GenericSub"$
-^\{-\d+\} symex_dynamic::dynamic_object1#2\.\.@Generic\.\.key = NULL$
-^\{-\d+\} symex_dynamic::dynamic_object1#3\.\.@Generic\.\.x = 5$
+^\{-\d+\} symex_dynamic::dynamic_object#2\.\.@Generic\.\[email protected]\.\.@class_identifier = "java::GenericSub"$
+^\{-\d+\} symex_dynamic::dynamic_object#2\.\.@Generic\.\.key = NULL$
+^\{-\d+\} symex_dynamic::dynamic_object#3\.\.@Generic\.\.x = 5$
 --
 byte_extract_(big|little)_endian
 --

jbmc/regression/jbmc-strings/StringBuilderConstructors01/test-no-arg-fail.desc

@@ -4,9 +4,9 @@ StringBuilderConstructors01
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-dynamic_object2=\{\s*\}
+dynamic_object\$0=\{\s*\}
 --
 ^warning: ignoring
 --
-The check for dynamic_object2 is to make sure the array is created empty and
+The check for dynamic_object\$0 is to make sure the array is created empty and
 is not given arbitrary content before its final assignment.

jbmc/regression/jbmc-strings/long_string/test_abort.desc

@@ -3,7 +3,7 @@ Test
 --function Test.checkAbort --trace --max-nondet-string-length 100000000
 ^EXIT=10$
 ^SIGNAL=0$
-dynamic_object[0-9]*=\(assignment removed\)
+dynamic_object\$?[0-9]*=\(assignment removed\)
 --
 --
 This tests that the object does not appear in the trace, because concretizing

jbmc/regression/jbmc/VarLengthArrayTrace1/test.desc

@@ -3,7 +3,7 @@ VarLengthArrayTrace1
 --trace --function VarLengthArrayTrace1.main
 ^EXIT=10$
 ^SIGNAL=0$
-dynamic_3_array\[1.*\]=10
+dynamic_array\$?\d*\[1.*\]=10
 --
 ^warning: ignoring
 assignment removed

jbmc/regression/jbmc/array-cell-sensitivity1/test-max-array-size-10.desc

@@ -1,17 +1,17 @@
 CORE
 Test
 --function Test.main --show-vcc --max-field-sensitivity-array-size 10
-symex_dynamic::dynamic_2_array#2\[\[0\]\] =
-symex_dynamic::dynamic_2_array#2\[\[1\]\] =
-symex_dynamic::dynamic_2_array#2\[\[2\]\] =
-symex_dynamic::dynamic_2_array#2\[\[3\]\] =
-symex_dynamic::dynamic_2_array#2\[\[4\]\] =
-symex_dynamic::dynamic_2_array#2\[\[5\]\] =
-symex_dynamic::dynamic_2_array#2\[\[6\]\] =
-symex_dynamic::dynamic_2_array#2\[\[7\]\] =
-symex_dynamic::dynamic_2_array#2\[\[8\]\] =
-symex_dynamic::dynamic_2_array#2\[\[9\]\] =
-symex_dynamic::dynamic_2_array#3\[\[1\]\] = java::Test.main:\(I\)V::unknown!0@1#1
+symex_dynamic::dynamic_array#2\[\[0\]\] =
+symex_dynamic::dynamic_array#2\[\[1\]\] =
+symex_dynamic::dynamic_array#2\[\[2\]\] =
+symex_dynamic::dynamic_array#2\[\[3\]\] =
+symex_dynamic::dynamic_array#2\[\[4\]\] =
+symex_dynamic::dynamic_array#2\[\[5\]\] =
+symex_dynamic::dynamic_array#2\[\[6\]\] =
+symex_dynamic::dynamic_array#2\[\[7\]\] =
+symex_dynamic::dynamic_array#2\[\[8\]\] =
+symex_dynamic::dynamic_array#2\[\[9\]\] =
+symex_dynamic::dynamic_array#3\[\[1\]\] = java::Test.main:\(I\)V::unknown!0@1#1
 ^EXIT=0$
 ^SIGNAL=0$
 --