cprover
solvers/README.md
Go to the documentation of this file.
1 \ingroup module_hidden
2 \defgroup solvers solvers
3 # Folder solvers
4 
5 \authors Romain Brenguier, Kareem Khazem, Martin Brain
6 
7 \section overview Overview
8 
9 The basic role of solvers is to answer whether the set of equations given
10 is satisfiable.
11 One example usage, is to determine whether an assertion in a
12 program can be violated.
13 We refer to \ref goto-symex for how CBMC and JBMC convert a input program
14 and property to a set of equations.
15 
16 The secondary role of solvers is to provide a satisfying assignment of
17 the variables of the equations, this can for instance be used to construct
18 a trace.
19 
20 The `solvers/` directory contains interfaces to a number of
21 different decision procedures, roughly one per directory.
22 
23 * prop/: The basic and common functionality. The key file is
24  `prop_conv.h` which defines `prop_convt`. This is the base class that
25  is used to interface to the decision procedures. The key functions are
26  `convert` which takes an `exprt` and converts it to the appropriate,
27  solver specific, data structures and `dec_solve` (inherited from
28  `decision_proceduret`) which invokes the actual decision procedures.
29  Individual decision procedures (named `*_dect`) objects can be created
30  but `prop_convt` is the preferred interface for code that uses them.
31 
32 * flattening/: A library that converts operations to bit-vectors,
33  including calling the conversions in `floatbv` as necessary. Is
34  implemented as a simple conversion (with caching) and then a
35  post-processing function that adds extra constraints. This is not used
36  by the SMT or CVC back-ends.
37 
38 * dplib/: Provides the `dplib_dect` object which used the decision
39  procedure library from “Decision Procedures : An Algorithmic Point of
40  View”.
41 
42 * cvc/: Provides the `cvc_dect` type which interfaces to the old (pre
43  SMTLib) input format for the CVC family of solvers. This format is
44  still supported by depreciated in favour of SMTLib 2.
45 
46 * smt1/: Provides the `smt1_dect` type which converts the formulae to
47  SMTLib version 1 and then invokes one of Boolector, CVC3, OpenSMT,
48  Yices, MathSAT or Z3. Again, note that this format is depreciated.
49 
50 * smt2/: Provides the `smt2_dect` type which functions in a similar
51  way to `smt1_dect`, calling Boolector, CVC3, MathSAT, Yices or Z3.
52  Note that the interaction with the solver is batched and uses
53  temporary files rather than using the interactive command supported by
54  SMTLib 2. With the `–fpa` option, this output mode will not flatten
55  the floating point arithmetic and instead output the proposed SMTLib
56  floating point standard.
57 
58 * qbf/: Back-ends for a variety of QBF solvers. Appears to be no
59  longer used or maintained.
60 
61 * sat/: Back-ends for a variety of SAT solvers and DIMACS output.
62 
63 \section sat-smt-encoding SAT/SMT Encoding
64 
65 In the \ref solvers directory.
66 
67 **Key classes:**
68 * \ref literalt
69 * \ref boolbvt
70 * \ref propt
71 
72 \dot
73 digraph G {
74  node [shape=box];
75  rankdir="LR";
76  1 [shape=none, label=""];
77  2 [label="goto conversion"];
78  3 [shape=none, label=""];
79  1 -> 2 [label="equations"];
80  2 -> 3 [label="propositional variables as bitvectors, constraints"];
81 }
82 \enddot
83 
84 
85 ---
86 
87 \section decision-procedure Decision Procedure
88 
89 In the \ref solvers directory.
90 
91 **Key classes:**
92 * symex_target_equationt
93 * \ref propt
94 * \ref bmct
95 
96 \dot
97 digraph G {
98  node [shape=box];
99  rankdir="LR";
100  1 [shape=none, label=""];
101  2 [label="goto conversion"];
102  3 [shape=none, label=""];
103  1 -> 2 [label="propositional variables as bitvectors, constraints"];
104  2 -> 3 [label="solutions"];
105 }
106 \enddot
107 
108 \section string-solver-interface String Solver Interface
109 
110 The string solver is particularly aimed at string logic, but since it inherits
111 from \ref bv_refinementt it is also capable of handling arithmetic, array logic,
112 floating point operations etc.
113 The backend uses the flattening of \ref boolbvt to convert expressions to boolean formula.
114 
115 An example of a problem given to string solver could look like this:
116 
117 ~~~~~
118 return_code == cprover_string_concat_func(
119  length1, array1,
120  { .length=length2, .content=content2 },
121  { .length=length3, .content=content3 })
122 length3 == length2
123 content3 == content2
124 is_equal == cprover_string_equals_func(length1, array1, 2, {'a', 'a'})
125 is_equal == 1
126 ~~~~~
127 
128 Details about the meaning of the primitives `cprover_string_concat_func` and
129 `cprover_string_equals_func` are given in section \ref primitives "String Primitives".
130 
131 The first equality means that the string represented by `{length1, array1}` is
132 the concatanation of the string represented by `{length2, array2}` and
133 `{length3, array3}`. The second and third mean that `{length2, array2}` and
134 `{length3, array3}` represent the same string. The fourth means that `is_equal`
135 is 1 if and only if `{length1, array1}` is the string "aa". The last equation
136 ensures that `is_equal` has to be equal to 1 in the solution.
137 
138 For this system of equations the string solver should answer that it is
139 satisfiable. It is then possible to recover which assignments make all
140 equation true, in that case `length2 = length3 = 1` and
141 `content2 = content3 = {'a'}`.
142 
143 
144 \subsection general_interface General interface
145 
146 The common interface for solvers in CProver is inherited from
147 `decision_proceduret` and is the common interface for all solvers.
148 It is essentially composed of these three functions:
149 
150  - `string_refinementt::set_to(const exprt &expr, bool value)`:
151  \copybrief string_refinementt::set_to
152  - `string_refinementt::dec_solve()`:
153  \copybrief string_refinementt::dec_solve
154  - `string_refinementt::get(const exprt &expr) const`:
155  \copybrief string_refinementt::get
156 
157 For each goal given to CProver:
158  - `set_to` is called on several equations, roughly one for each step of the
159  symbolic execution that leads to that goal;
160  - `dec_solve` is called to determine whether the goal is reachable given these
161  equations;
162  - `get` is called by the interpreter to obtain concrete value to build a trace
163  leading to the goal;
164  - The same process can be repeated for further goals, in that case the
165  constraints added by previous calls to `set_to` remain valid.
166 
167 \subsection specificity Specificity of the string solver
168 
169 The specificity of the solver is in what kind of expressions `set_to` accepts
170 and understands. `string_refinementt::set_to` accepts all constraints that are
171 normally accepted by `bv_refinementt`.
172 
173 `string_refinementt::set_to` also understands constraints of the form:
174  * `char_pointer1 = b ? char_pointer2 : char_pointer3` where `char_pointer<i>`
175  variables are of type pointer to characters and `b` is a Boolean
176  expression.
177  * `i = cprover_primitive(args)` where `i` is of signed bit vector type.
178  String primitives are listed in the next section.
179 
180 \note In the implementation, equations that are not of these forms are passed
181  to an embedded `bv_refinementt` solver.
182 
183 \subsection string-representation String representation in the solver
184 
185 String primitives can have arguments which are pointers to characters.
186 These pointers represent strings.
187 To each of these pointers the string solver associate a char array
188 which represents the content of the string.
189 If the pointer is the address of an actual array in the program they should be
190 linked by using the primitive `cprover_string_associate_array_to_pointer`.
191 The length of the array can also be linked to a variable of the program using
192  `cprover_string_associate_length_to_array`.
193 
194 \warning The solver assumes the memory pointed by the arguments is immutable
195 which is not something that is true in general for C pointers for instance.
196 Therefore for each transformation on a string, it is assumed the program
197 allocates a new string before calling a primitive.
198 
199 \section primitives String primitives
200 
201 \subsection basic-primitives Basic access:
202 
203  * `cprover_string_associate_array_to_pointer` : Link with an array of
204  characters of the program.
205  * `cprover_string_associate_length_to_array` : Link the length of the array
206  with the given integer value.
207  * `cprover_string_char_at` :
208  \copybrief string_constraint_generatort::add_axioms_for_char_at(const function_application_exprt &f)
209  \link string_constraint_generatort::add_axioms_for_char_at(const function_application_exprt &f) More... \endlink
210  * `cprover_string_length` :
211  \copybrief string_constraint_generatort::add_axioms_for_length(const function_application_exprt &f)
212  \link string_constraint_generatort::add_axioms_for_length(const function_application_exprt &f) More... \endlink
213 
214 \subsection comparisons Comparisons:
215 
216  * `cprover_string_compare_to` :
217  \copybrief string_constraint_generatort::add_axioms_for_compare_to(const function_application_exprt &f)
218  \link string_constraint_generatort::add_axioms_for_compare_to(const function_application_exprt &f) More... \endlink
219  * `cprover_string_contains` :
220  \copybrief string_constraint_generatort::add_axioms_for_contains(const function_application_exprt &f)
221  \link string_constraint_generatort::add_axioms_for_contains(const function_application_exprt &f) More... \endlink
222  * `cprover_string_equals` :
223  \copybrief string_constraint_generatort::add_axioms_for_equals(const function_application_exprt &f)
224  \link string_constraint_generatort::add_axioms_for_equals(const function_application_exprt &f) More... \endlink
225  * `cprover_string_equals_ignore_case` :
226  \copybrief string_constraint_generatort::add_axioms_for_equals_ignore_case(const function_application_exprt &f)
227  \link string_constraint_generatort::add_axioms_for_equals_ignore_case(const function_application_exprt &f) More... \endlink
228  * `cprover_string_hash_code` :
229  \copybrief string_constraint_generatort::add_axioms_for_hash_code
230  \link string_constraint_generatort::add_axioms_for_hash_code More... \endlink
231  * `cprover_string_is_prefix` :
232  \copybrief string_constraint_generatort::add_axioms_for_is_prefix
233  \link string_constraint_generatort::add_axioms_for_is_prefix More... \endlink
234  * `cprover_string_index_of` :
235  \copybrief string_constraint_generatort::add_axioms_for_index_of(const function_application_exprt &f)
236  \link string_constraint_generatort::add_axioms_for_index_of(const function_application_exprt &f) More... \endlink
237  * `cprover_string_last_index_of` :
238  \copybrief string_constraint_generatort::add_axioms_for_last_index_of(const function_application_exprt &f)
239  \link string_constraint_generatort::add_axioms_for_last_index_of(const function_application_exprt &f) More... \endlink
240 
241 \subsection transformations Transformations:
242 
243  * `cprover_string_char_set` :
244  \copybrief string_constraint_generatort::add_axioms_for_char_set(const function_application_exprt &f)
245  \link string_constraint_generatort::add_axioms_for_char_set(const function_application_exprt &f) More... \endlink
246  * `cprover_string_concat` :
247  \copybrief string_constraint_generatort::add_axioms_for_concat(const function_application_exprt &f)
248  \link string_constraint_generatort::add_axioms_for_concat(const function_application_exprt &f) More... \endlink
249  * `cprover_string_delete` :
250  \copybrief string_constraint_generatort::add_axioms_for_delete(const function_application_exprt &f)
251  \link string_constraint_generatort::add_axioms_for_delete(const function_application_exprt &f) More... \endlink
252  * `cprover_string_insert` :
253  \copybrief string_constraint_generatort::add_axioms_for_insert(const function_application_exprt &f)
254  \link string_constraint_generatort::add_axioms_for_insert(const function_application_exprt &f) More... \endlink
255  * `cprover_string_replace` :
256  \copybrief string_constraint_generatort::add_axioms_for_replace(const function_application_exprt &f)
257  \link string_constraint_generatort::add_axioms_for_replace(const function_application_exprt &f) More... \endlink
258  * `cprover_string_set_length` :
259  \copybrief string_constraint_generatort::add_axioms_for_set_length(const function_application_exprt &f)
260  \link string_constraint_generatort::add_axioms_for_set_length(const function_application_exprt &f) More... \endlink
261  * `cprover_string_substring` :
262  \copybrief string_constraint_generatort::add_axioms_for_substring(const function_application_exprt &f)
263  \link string_constraint_generatort::add_axioms_for_substring(const function_application_exprt &f) More... \endlink
264  * `cprover_string_to_lower_case` :
265  \copybrief string_constraint_generatort::add_axioms_for_to_lower_case(const function_application_exprt &f)
266  \link string_constraint_generatort::add_axioms_for_to_lower_case(const function_application_exprt &f) More... \endlink
267  * `cprover_string_to_upper_case` :
268  \copybrief string_constraint_generatort::add_axioms_for_to_upper_case(const function_application_exprt &f)
269  \link string_constraint_generatort::add_axioms_for_to_upper_case(const function_application_exprt &f) More... \endlink
270  * `cprover_string_trim` :
271  \copybrief string_constraint_generatort::add_axioms_for_trim(const function_application_exprt &f)
272  \link string_constraint_generatort::add_axioms_for_trim(const function_application_exprt &f) More... \endlink
273 
274 \subsection conversions Conversions:
275 
276  * `cprover_string_format` :
277  \copybrief string_constraint_generatort::add_axioms_for_format(const function_application_exprt &f)
278  \link string_constraint_generatort::add_axioms_for_format(const function_application_exprt &f) More... \endlink
279  * `cprover_string_from_literal` :
280  \copybrief string_constraint_generatort::add_axioms_from_literal(const function_application_exprt &f)
281  \link string_constraint_generatort::add_axioms_from_literal(const function_application_exprt &f) More... \endlink
282  * `cprover_string_of_int` :
283  \copybrief string_constraint_generatort::add_axioms_from_int(const function_application_exprt &f)
284  \link string_constraint_generatort::add_axioms_from_int(const function_application_exprt &f) More... \endlink
285  * `cprover_string_of_float` :
286  \copybrief string_constraint_generatort::add_axioms_for_string_of_float(const function_application_exprt &f)
287  \link string_constraint_generatort::add_axioms_for_string_of_float(const function_application_exprt &f) More... \endlink
288  * `cprover_string_of_float_scientific_notation` :
289  \copybrief string_constraint_generatort::add_axioms_from_float_scientific_notation(const function_application_exprt &f)
290  \link string_constraint_generatort::add_axioms_from_float_scientific_notation(const function_application_exprt &f) More... \endlink
291  * `cprover_string_of_char` :
292  \copybrief string_constraint_generatort::add_axioms_from_char(const function_application_exprt &f)
293  \link string_constraint_generatort::add_axioms_from_char(const function_application_exprt &f) More... \endlink
294  * `cprover_string_parse_int` :
295  \copybrief string_constraint_generatort::add_axioms_for_parse_int(const function_application_exprt &f)
296  \link string_constraint_generatort::add_axioms_for_parse_int(const function_application_exprt &f) More... \endlink
297 
298 \subsection deprecated Deprecated primitives:
299 
300  * `cprover_string_concat_code_point`, `cprover_string_code_point_at`,
301  `cprover_string_code_point_before`, `cprover_string_code_point_count`:
302  Java specific, should be part of Java models.
303  * `cprover_string_offset_by_code_point`, `cprover_string_concat_char`,
304  `cprover_string_concat_int`, `cprover_string_concat_long`,
305  `cprover_string_concat_bool`, `cprover_string_concat_double`,
306  `cprover_string_concat_float`, `cprover_string_insert_int`,
307  `cprover_string_insert_long`, `cprover_string_insert_bool`,
308  `cprover_string_insert_char`, `cprover_string_insert_double`,
309  `cprover_string_insert_float` :
310  Should be done in two steps: conversion from primitive type and call
311  to the string primitive.
312  * `cprover_string_array_of_char_pointer`, `cprover_string_to_char_array` :
313  Pointer to char array association
314  is now handled by `string_constraint_generatort`, there is no need for
315  explicit conversion.
316  * `cprover_string_intern` : Never tested.
317  * `cprover_string_is_empty` :
318  Should use `cprover_string_length(s) == 0` instead.
319  * `cprover_string_is_suffix` : Should use `cprover_string_is_prefix` with an
320  offset argument.
321  * `cprover_string_empty_string` : Can use literal of empty string instead.
322  * `cprover_string_of_long` : Should be the same as `cprover_string_of_int`.
323  * `cprover_string_delete_char_at` : A call to
324  `cprover_string_delete_char_at(s, i)` would be the same thing as
325  `cprover_string_delete(s, i, i+1)`.
326  * `cprover_string_of_bool` :
327  Language dependent, should be implemented in the models.
328  * `cprover_string_copy` : Same as `cprover_string_substring(s, 0)`.
329  * `cprover_string_of_int_hex` : Same as `cprover_string_of_int(s, 16)`.
330  * `cprover_string_of_double` : Same as `cprover_string_of_float`.
331 
332 \section algorithm Decision algorithm
333 
334 \copydetails string_refinementt::dec_solve
335 
336 \subsection instantiation Instantiation
337 
338 This is done by generate_instantiations(messaget::mstreamt &stream, const namespacet &ns, const string_constraint_generatort &generator, const index_set_pairt &index_set, const string_axiomst &axioms).
339 \copydetails generate_instantiations(messaget::mstreamt &stream, const namespacet &ns, const string_constraint_generatort &generator, const index_set_pairt &index_set, const string_axiomst &axioms)
340 
341 \subsection axiom-check Axiom check
342 
343 \copydetails check_axioms(const string_axiomst &axioms, string_constraint_generatort &generator, const std::function<exprt(const exprt &)> &get, messaget::mstreamt &stream, const namespacet &ns, std::size_t max_string_length, bool use_counter_example, ui_message_handlert::uit ui, const union_find_replacet &symbol_resolve)
344 \link check_axioms(const string_axiomst &axioms, string_constraint_generatort &generator, const std::function<exprt(const exprt &)> &get, messaget::mstreamt &stream, const namespacet &ns, std::size_t max_string_length, bool use_counter_example, ui_message_handlert::uit ui, const union_find_replacet &symbol_resolve)
345  (See function documentation...) \endlink
346 
347 \section floatbv Floatbv Directory
348 
349 This library contains the code that is used to convert floating point
350 variables (`floatbv`) to bit vectors (`bv`). This is referred to as
351 ‘bit-blasting’ and is called in the `solver` code during conversion to
352 SAT or SMT. It also contains the abstraction code described in the
353 FMCAD09 paper.