From c4205447a7bb35b584c1e1c8c87985a4b916d054 Mon Sep 17 00:00:00 2001 From: Enrico Steffinlongo Date: Mon, 11 Jul 2022 14:03:30 +0100 Subject: [PATCH 1/2] Add README.md for new incremental smt backend --- src/solvers/smt2_incremental/README.md | 42 ++++++++++++++++++++++++++ 1 file changed, 42 insertions(+) create mode 100644 src/solvers/smt2_incremental/README.md diff --git a/src/solvers/smt2_incremental/README.md b/src/solvers/smt2_incremental/README.md new file mode 100644 index 00000000000..6ec2746fd89 --- /dev/null +++ b/src/solvers/smt2_incremental/README.md @@ -0,0 +1,42 @@ +# Incremental SMT backend + +CBMC comes with a solver-agnostic incremental SMT backend. + +The SMT incremental backend supports the following `C` features: + +- Integers (via Bit vector arithmetics) +- Pointers +- Arrays (support is currently incomplete) + +Primitive not supported are: + +- Floating point values and arithmetics +- Structs + +Usage of the incremental SMT backend requires a SMT solver compatible with +incremental SMTlib v2.6 formatted input from the standard input and that +supports the `QF_AUFBV` (Quantifier Free Array Uninterpreted Functions and Bit +Vectors) logic. + +To use this functionality it is enough to add the argument +`--incremental-smt2-solver ` where `` is the command to invoke the SMT +solver of choice using the incremental mode and accepting input from the +standard input. + +Examples of invocations with various solvers: + +1. `--incremental-smt2-solver 'z3 -smt2 -in'` to use the Z3 solver. +2. `--incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental'` to use the + CVC5 solver. + +The new incremental SMT backend has been designed to interoperate with external +solvers, so the solver name must be in the `PATH` or an executable with full +path must be provided. + +Due to lack of support for conversion of `array_of` expressions that are added +by CBMC in the before the new SMT backend is invoked, it is necessary to supply +an extra argument `--slice-formula` so that instances of `arrayof_exprt` are +removed from the formula to be converted. + +As we move forward with our array-support implementation, we anticipate that the +need for this extra flag will be diminished. From 2610713bda4a0ba32c8a10faa9087540e910749b Mon Sep 17 00:00:00 2001 From: Enrico Steffinlongo Date: Tue, 12 Jul 2022 18:05:38 +0100 Subject: [PATCH 2/2] Added man entry for --incremental-smt2-solver --- doc/man/cbmc.1 | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) diff --git a/doc/man/cbmc.1 b/doc/man/cbmc.1 index 6175bd41f49..0708197ac4a 100644 --- a/doc/man/cbmc.1 +++ b/doc/man/cbmc.1 @@ -176,6 +176,25 @@ Output formula to given file Never turn arrays into uninterpreted functions .IP --arrays-uf-always Always turn arrays into uninterpreted functions +.IP "--incremental-smt2-solver " +Use the incremental SMT backend where is the command to invoke the SMT +solver of choice. +.br +Examples invocations: +.br + --incremental-smt2-solver 'z3 -smt2 -in' (use the Z3 solver). +.br + --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' (use the CVC5 solver). +.sp +Note that: +.br +The solver name must be in the "PATH" or be an executable with full path. +.br +The SMT solver should accept incremental SMTlib v2.6 formatted input from the stdin. +.br +The SMT solver should support the QF_AUFBV logic. +.br +The flag --slice-formula should be added to remove some not-yet supported features. .SH ENVIRONMENT All tools honor the TMPDIR environment variable when generating temporary files and directories. Furthermore note that