|
| 1 | +[CPROVER Manual TOC](../) |
| 2 | + |
| 3 | +## SMT 2 incremental backend |
| 4 | + |
| 5 | +CBMC supports many different smt solver backends. This document describes how to use the incremental |
| 6 | +smt2 solver. For other solver usages use `cbmc --help`. |
| 7 | + |
| 8 | +The incremental smt2 solver backend of CBMC is a solver-agnostic smt backend that allows the user to |
| 9 | +specify which smtlib 2.6 compliant solver CBMC should use. This choice increases the flexibility of |
| 10 | +CBMC as the user can easily switch solver at runtime also allowing custom parametrization of the |
| 11 | +solver to be used. Further, the backend exploits the incremental mode of the smt solver, so |
| 12 | +subsequent incremental SMT solver queries do not require a full re-evaluation of the entire SMT |
| 13 | +formula. |
| 14 | + |
| 15 | +### Supported features |
| 16 | + |
| 17 | +The incremental smt2 solver supports the following CBMC C features: |
| 18 | + |
| 19 | +* Integral types (including integers, characters and boolean). These are encoded into smt by using |
| 20 | + bit-vectors, |
| 21 | +* Pointers. Encoded by using smt bit-vectors. This includes support for pointers to both stack and |
| 22 | + heap-allocated memory, |
| 23 | +* Arrays. Encoded by using smt array theory. |
| 24 | + |
| 25 | +Currently, unsupported features include floating-point types, structs and unions. |
| 26 | + |
| 27 | +For more details on which features are supported see regression |
| 28 | +tests in [`regression/cbmc-incr-smt2`](../regression/cbmc-incr-smt2). |
| 29 | + |
| 30 | +The backend has been tested with these instrumentation passes: |
| 31 | + |
| 32 | +* `--bounds-check`, |
| 33 | +* `--conversion-check`, |
| 34 | +* `--div-by-zero-check`, |
| 35 | +* `--pointer-check`, |
| 36 | +* `--pointer-overflow-check`, |
| 37 | +* `--signed-overflow-check`, |
| 38 | +* `--unsigned-overflow-check`, |
| 39 | +* `--unwinding-assertions`. |
| 40 | + |
| 41 | +### Requisites |
| 42 | + |
| 43 | +To run the incremental smt2 backend it is necessary to have an smt solver that: |
| 44 | + |
| 45 | +* is runnable from the command line, |
| 46 | +* supports interactive mode from the command line, |
| 47 | +* supports smtlib 2.6 input, |
| 48 | +* supports incremental mode. |
| 49 | + |
| 50 | +Because of the way supported features are encoded the smt solver should be capable to handle arrays, |
| 51 | +bit-vectors, uninterpreted functions and quantifiers. Also, the solver should work with the `ALL` |
| 52 | +smt theory. |
| 53 | + |
| 54 | +At the time of writing the smt solvers tested in CI |
| 55 | +are [Z3](https://github.com/Z3Prover/z3) |
| 56 | +and [CVC5](https://cvc5.github.io/). |
| 57 | + |
| 58 | +### Usage |
| 59 | + |
| 60 | +To use the incremental SMT2 backend it is enough to add the `--incremental-smt2-solver` argument to |
| 61 | +the CBMC command line followed by the command to invoke the chosen solver using smtlib 2.6 input in |
| 62 | +interactive mode. |
| 63 | + |
| 64 | +Note that the use of the `--slice-formula` option is recommended at this time to slice out |
| 65 | +unnecessary code (that may not be supported at the moment) and this can also improve performance. |
| 66 | + |
| 67 | +Here are two examples to show how to analyse a file `program.c` using Z3 and CVC5 solvers. |
| 68 | + |
| 69 | +To use the Z3 SMT solver: |
| 70 | + |
| 71 | +```shell |
| 72 | +cbmc --slice-formula --incremental-smt2-solver 'z3 -smt2 -in' program.c |
| 73 | +``` |
| 74 | + |
| 75 | +If `z3` is not on the `PATH`, then it is enough to replace `'z3 -smt2 -in'` |
| 76 | +with `'<command-to-execute-z3> -smt2 -in'`, |
| 77 | + |
| 78 | +Similarly to execute CBMC using the CVC5 solver: |
| 79 | + |
| 80 | +```shell |
| 81 | +cbmc --slice-formula --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' program.c |
| 82 | +``` |
| 83 | + |
| 84 | +As the command to execute the solver is left to the user, it is possible to fine-tune it by passing |
| 85 | +extra parameters (when the solver allows so). For example Z3 allows to set certain parameters by |
| 86 | +adding `param_name=value` to the command line, so to use the Z3 solver with `well_sorted_check` |
| 87 | +property set to `false` the following has to be run: |
| 88 | + |
| 89 | +```shell |
| 90 | +cbmc --slice-formula --incremental-smt2-solver 'z3 -smt2 -in well_sorted_check=false' program.c |
| 91 | +``` |
| 92 | + |
| 93 | +### Examples |
| 94 | + |
| 95 | +Given a C program `program.c` as follows: |
| 96 | + |
| 97 | +```C |
| 98 | +int main() |
| 99 | +{ |
| 100 | + int x, y; |
| 101 | + if(x != 0) |
| 102 | + __CPROVER_assert(y != 4, "Assert of inequality to 4."); |
| 103 | + else |
| 104 | + __CPROVER_assert(y != 2, "Assert of inequality to 2."); |
| 105 | + int z = y; |
| 106 | + return 0; |
| 107 | +} |
| 108 | +``` |
| 109 | + |
| 110 | +To analyze it we should run: |
| 111 | + |
| 112 | +```shell |
| 113 | +cbmc --incremental-smt2-solver 'z3 -smt2 -in' --slice-formula program.c |
| 114 | +``` |
| 115 | + |
| 116 | +We will get the verification results as follows: |
| 117 | + |
| 118 | +```text |
| 119 | +CBMC version 5.70.0 (cbmc-5.70.0-53-g20535ad14d) 64-bit x86_64 macos |
| 120 | +Parsing program.c |
| 121 | +Converting |
| 122 | +Type-checking program |
| 123 | +Generating GOTO Program |
| 124 | +Adding CPROVER library (x86_64) |
| 125 | +Removal of function pointers and virtual functions |
| 126 | +Generic Property Instrumentation |
| 127 | +Running with 8 object bits, 56 offset bits (default) |
| 128 | +Starting Bounded Model Checking |
| 129 | +Runtime Symex: 0.00168879s |
| 130 | +size of program expression: 45 steps |
| 131 | +slicing removed 23 assignments |
| 132 | +Generated 2 VCC(s), 2 remaining after simplification |
| 133 | +Runtime Postprocess Equation: 2.1865e-05s |
| 134 | +Passing problem to incremental SMT2 solving via "z3 -smt2 -in" |
| 135 | +``` |
| 136 | + |
| 137 | +Note here that the solver used by CBMC is `"z3 -smt2 -in"` as specified by the user. |
| 138 | + |
| 139 | +```text |
| 140 | +[continues] |
| 141 | +converting SSA |
| 142 | +Runtime Convert SSA: 0.00130809s |
| 143 | +Running incremental SMT2 solving via "z3 -smt2 -in" |
| 144 | +Runtime Solver: 0.0738685s |
| 145 | +Runtime decision procedure: 0.0765297s |
| 146 | +Running incremental SMT2 solving via "z3 -smt2 -in" |
| 147 | +Runtime Solver: 0.00535358s |
| 148 | +Runtime decision procedure: 0.00570765s |
| 149 | +
|
| 150 | +** Results: |
| 151 | +program.c function main |
| 152 | +[main.assertion.1] line 5 Assert of inequality to 4.: FAILURE |
| 153 | +[main.assertion.2] line 7 Assert of inequality to 2.: FAILURE |
| 154 | +
|
| 155 | +** 2 of 2 failed (3 iterations) |
| 156 | +VERIFICATION FAILED |
| 157 | +``` |
| 158 | + |
| 159 | +As expected CBMC returns `FAILURE` for both assertions at lines `5` and `7`. |
| 160 | + |
| 161 | +The incremental smt2 backend also supports trace generation, so to get a trace that fails the |
| 162 | +assertions the `--trace` argument should be added, so the command to run is: |
| 163 | + |
| 164 | +```shell |
| 165 | +cbmc --incremental-smt2-solver 'z3 -smt2 -in' --slice-formula --trace program.c |
| 166 | +``` |
| 167 | + |
| 168 | +This will append the trace to CBMC's output as follows: |
| 169 | + |
| 170 | +```text |
| 171 | +CBMC version 5.70.0 (cbmc-5.70.0-53-g20535ad14d) 64-bit x86_64 macos |
| 172 | +Parsing program.c |
| 173 | +[...] |
| 174 | +[main.assertion.1] line 5 Assert of inequality to 4.: FAILURE |
| 175 | +[main.assertion.2] line 7 Assert of inequality to 2.: FAILURE |
| 176 | +
|
| 177 | +Trace for main.assertion.1: |
| 178 | +
|
| 179 | +State 6 file program.c function main line 3 thread 0 |
| 180 | +---------------------------------------------------- |
| 181 | + x=-1 (11111111 11111111 11111111 11111111) |
| 182 | +
|
| 183 | +State 7 file program.c function main line 3 thread 0 |
| 184 | +---------------------------------------------------- |
| 185 | + y=4 (00000000 00000000 00000000 00000100) |
| 186 | +
|
| 187 | +Violated property: |
| 188 | + file program.c function main line 5 thread 0 |
| 189 | + Assert of inequality to 4. |
| 190 | + y != 4 |
| 191 | +
|
| 192 | +
|
| 193 | +
|
| 194 | +Trace for main.assertion.2: |
| 195 | +
|
| 196 | +State 6 file program.c function main line 3 thread 0 |
| 197 | +---------------------------------------------------- |
| 198 | + x=0 (00000000 00000000 00000000 00000000) |
| 199 | +
|
| 200 | +State 7 file program.c function main line 3 thread 0 |
| 201 | +---------------------------------------------------- |
| 202 | + y=2 (00000000 00000000 00000000 00000010) |
| 203 | +
|
| 204 | +Violated property: |
| 205 | + file program.c function main line 7 thread 0 |
| 206 | + Assert of inequality to 2. |
| 207 | + y != 2 |
| 208 | +
|
| 209 | +
|
| 210 | +
|
| 211 | +** 2 of 2 failed (3 iterations) |
| 212 | +VERIFICATION FAILED |
| 213 | +``` |
0 commit comments