8 This contains the first full application. CBMC is a bounded model
9 checker that uses the front ends (`ansi-c`, `cpp`, goto-program or
10 others) to create a goto-program, `goto-symex` to unwind the loops the
11 given number of times and to produce and equation system and finally
12 `solvers` to find a counter-example (technically, `goto-symex` is then
13 used to construct the counter-example trace).
17 CBMC operates in three phases:
19 1. Parse command-line options; convert passed source files into a GOTO model
20 (for more detail see \ref AST_section).
21 2. Run `goto-symex` to turn the GOTO model into a SAT or SMT equation
22 (for more detail see \ref goto-symex).
23 3. Solve the equation and report results (described here, but see
24 \ref BMC_section for more information).
26 The GOTO model is generated using `initialize_goto_model`; see documentaton
27 in the `goto-programs/` directory. Goto-symex is similarly documented in its
32 The class `bmct` is responsible for solving the equation, generated by
33 goto-symex, which represents the assertions or goals it is being asked to show
34 can be hit or satisfied (or prove that can't be done).
36 For example, given an input program
37 `f(int x, int y) { assert(x + y % 3 == 1); assert(x % y == 0); }` then goto-
38 symex would produce a formula something like
39 `F1 + F2 % 3 != 1 OR (F1 + F2 % 3 == 1 AND F1 % F2 != 0), where F-variables
40 are free. The precise expression of that formula depends on CBMC's command-line
41 configuration: for some backends it will lower the arithmetic operations into
42 bitwise operations; other backends understand arithmetic and so they will remain
43 as-is. See `cbmc_solverst` for details of how a backend solver is selected,
44 constructed and configured.
46 Whatever precise backend representation is used, CBMC controls solving the
47 formula using two different possible procedures:
49 1. When `--stop-on-fail` is passed on the command-line, the formula is solved
50 once to find any violated assertion. This is implemented directly in
52 2. When `--stop-on-fail` is not passed, BMC is run in "all-properties" mode.
53 This categorises the assertions into groups that represent the same property,
54 and the solver is run repeatedly to try to satisfy each property at least
55 once. This is implemented in `bmc_all_propertiest`.
57 For example, in the all-properties case, if the provided formula had five
58 assertions, `A1 ... A5`, and `A1` and `A2` were instances of the same property
59 as were `A4` and `A5`, then initially the solver would simply be asked to
60 satisfy `A1 | A2 | A3 | A4 | A5`, but if its first solution gave an answer for
61 `A1` only, then the solver would be called again asking for a solution to
62 `A3 | A4 | A5`, `A1` having been satisfied and `A2` being considered irrelevant
63 because it is an instance of the same property as `A1`. If the solver came back
64 with a solution hitting `A3` then it would be asked again to solve for
65 `A4 | A5`, and so on until either every property is satisfied or the solver
66 responds that a solution is impossible.
68 Generally assertions are considered instances of the same property if they are
69 derived from the same source code statement: for example,
70 `assert(x == 1); assert(x == 2);` would be considered two distinct properties,
71 while `for(int i = 1; i <= 2; ++i) assert(x == i);` would generate two instances
72 of the same property. This is because assertions are categorised by their
73 `source_location->get_property_id()` field, which in turn is set per static
74 instruction by `goto-programs/set_properties.cpp`. Assertions that are generated
75 by other mechanism may categorise their properties differently.
79 There is one further BMC mode that differs more fundamentally: when `--cover` is
80 passed, assertions in the program text are converted into assumptions (these
81 must hold for control flow to proceed past them, but are not goals for the
82 equation solver), while new `assert(false)` statements are added throughout the
83 source program representing coverage goals. The equation solving process then
84 proceeds the same as in all-properties mode. Coverage solving is implemented by
85 `bmc_covert`, but is structurally practically identical to
86 `bmc_all_propertiest`-- only the reporting differs (goals are called "covered"
87 rather than "failed").
91 By default CBMC will report its findings by listing which assertions passed
92 (could not be violated) or failed (could be violated), or which coverage goals
93 were satisfiable or unsatisfiable, depending on its mode of operation. However
94 if `--trace` is passed then it will print a full program trace indicating how
95 each assertion was violated. This is constructed using `build_goto_trace`, which
96 queries the backend asking what value was chosen for each program variable on
97 the path from the start of the program to the relevant assertion. For more
98 details on how the trace is populated see the documentation for
99 `build_goto_trace` for `prop_convt::get`, the function used to query the
104 CBMC supports running goto-symex in "path explorer" mode, which alters the
105 simple GOTO model, goto-symex, equation solving sequence described above by
106 incrementally running goto-symex to produce a formula describing *part* of a
107 program, trying to solve that partial formula to satisfy some properties (or
108 achieve some coverage, as appropriate), before re-entering symex to examine
109 other properties. For example, given a simple program
110 `if(x) assert(y); else assert(z);`, standard CBMC would generate a single
111 formula of the form `(x && !y) || (!x && !z)`, while in path-explorer mode it
112 might generate a partial formula `x && !y` and try solving that before even
113 considering the `!x` case. This should have the same end result as without the
114 special path-explorer mode, but could achieve the result faster in
115 `--stop-on-fail` mode or allow salvaging a partial result from an otherwise
116 excessively time- or memory-consuming run in all-properties mode.
118 For more details on path-symex see the classes `goto_symext` and