2 \defgroup solvers solvers
5 \authors Romain Brenguier, Kareem Khazem, Martin Brain
7 \section overview Overview
9 The basic role of solvers is to answer whether the set of equations given
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.
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
20 The `solvers/` directory contains interfaces to a number of
21 different decision procedures, roughly one per directory.
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.
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.
38 * dplib/: Provides the `dplib_dect` object which used the decision
39 procedure library from “Decision Procedures : An Algorithmic Point of
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.
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.
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.
58 * qbf/: Back-ends for a variety of QBF solvers. Appears to be no
59 longer used or maintained.
61 * sat/: Back-ends for a variety of SAT solvers and DIMACS output.
63 \section sat-smt-encoding SAT/SMT Encoding
65 In the \ref solvers directory.
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"];
87 \section decision-procedure Decision Procedure
89 In the \ref solvers directory.
92 * symex_target_equationt
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"];
108 \section string-solver-interface String Solver Interface
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.
115 An example of a problem given to string solver could look like this:
118 return_code == cprover_string_concat_func(
120 { .length=length2, .content=content2 },
121 { .length=length3, .content=content3 })
124 is_equal == cprover_string_equals_func(length1, array1, 2, {'a', 'a'})
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".
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.
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'}`.
144 \subsection general_interface General interface
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:
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
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
162 - `get` is called by the interpreter to obtain concrete value to build a trace
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.
167 \subsection specificity Specificity of the string solver
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`.
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
177 * `i = cprover_primitive(args)` where `i` is of signed bit vector type.
178 String primitives are listed in the next section.
180 \note In the implementation, equations that are not of these forms are passed
181 to an embedded `bv_refinementt` solver.
183 \subsection string-representation String representation in the solver
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`.
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.
199 \section primitives String primitives
201 \subsection basic-primitives Basic access:
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
214 \subsection comparisons Comparisons:
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
241 \subsection transformations Transformations:
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
274 \subsection conversions Conversions:
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_for_string_of_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
298 \subsection deprecated Deprecated primitives:
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
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
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`.
332 \section algorithm Decision algorithm
334 \copydetails string_refinementt::dec_solve
336 \subsection instantiation Instantiation
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)
341 \subsection axiom-check Axiom check
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
347 \section floatbv Floatbv Directory
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