2 \defgroup solvers solvers
5 \authors Romain Brenguier, Kareem Khazem, Martin Brain
7 \section solvers-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 SMT2 back-ends.
38 * smt2/: Provides the `smt2_dect` type which converts the formulae to
39 SMTLib 2 and then invokes one of Boolector, CVC3, CVC4, MathSAT, Yices or Z3.
40 Note that the interaction with the solver is batched and uses
41 temporary files rather than using the interactive command supported by
42 SMTLib 2. With the `–fpa` option, this output mode will not flatten
43 the floating point arithmetic and instead output the proposed SMTLib
44 floating point standard.
46 * qbf/: Back-ends for a variety of QBF solvers. Appears to be no
47 longer used or maintained.
49 * sat/: Back-ends for a variety of SAT solvers and DIMACS output.
51 \section flattening-section Flattening
55 \section solver-apis Solver APIs
57 \subsection smt-solving-api-section SMT solving API
61 \subsection sat-solving-api-section SAT solving API
65 \section sat-smt-encoding SAT/SMT Encoding
67 In the \ref solvers directory.
78 1 [shape=none, label=""];
79 2 [label="goto conversion"];
80 3 [shape=none, label=""];
81 1 -> 2 [label="equations"];
82 2 -> 3 [label="propositional variables as bitvectors, constraints"];
88 \section decision-procedure Decision Procedure
90 In the \ref solvers directory.
93 * symex_target_equationt
101 1 [shape=none, label=""];
102 2 [label="goto conversion"];
103 3 [shape=none, label=""];
104 1 -> 2 [label="propositional variables as bitvectors, constraints"];
105 2 -> 3 [label="solutions"];
109 \section string-solver-interface String Solver Interface
111 The string solver is particularly aimed at string logic, but since it inherits
112 from \ref bv_refinementt it is also capable of handling arithmetic, array logic,
113 floating point operations etc.
114 The backend uses the flattening of \ref boolbvt to convert expressions to boolean formula.
116 An example of a problem given to string solver could look like this:
119 return_code == cprover_string_concat_func(
121 { .length=length2, .content=content2 },
122 { .length=length3, .content=content3 })
125 is_equal == cprover_string_equals_func(length1, array1, 2, {'a', 'a'})
129 Details about the meaning of the primitives `cprover_string_concat_func` and
130 `cprover_string_equals_func` are given in section \ref primitives "String Primitives".
132 The first equality means that the string represented by `{length1, array1}` is
133 the concatanation of the string represented by `{length2, array2}` and
134 `{length3, array3}`. The second and third mean that `{length2, array2}` and
135 `{length3, array3}` represent the same string. The fourth means that `is_equal`
136 is 1 if and only if `{length1, array1}` is the string "aa". The last equation
137 ensures that `is_equal` has to be equal to 1 in the solution.
139 For this system of equations the string solver should answer that it is
140 satisfiable. It is then possible to recover which assignments make all
141 equation true, in that case `length2 = length3 = 1` and
142 `content2 = content3 = {'a'}`.
145 \subsection general_interface General interface
147 The common interface for solvers in CProver is inherited from
148 `decision_proceduret` and is the common interface for all solvers.
149 It is essentially composed of these three functions:
151 - `string_refinementt::set_to(const exprt &expr, bool value)`:
152 \copybrief string_refinementt::set_to
153 - `string_refinementt::dec_solve()`:
154 \copybrief string_refinementt::dec_solve
155 - `string_refinementt::get(const exprt &expr) const`:
156 \copybrief string_refinementt::get
158 For each goal given to CProver:
159 - `set_to` is called on several equations, roughly one for each step of the
160 symbolic execution that leads to that goal;
161 - `dec_solve` is called to determine whether the goal is reachable given these
163 - `get` is called by the interpreter to obtain concrete value to build a trace
165 - The same process can be repeated for further goals, in that case the
166 constraints added by previous calls to `set_to` remain valid.
168 \subsection specificity Specificity of the string solver
170 The specificity of the solver is in what kind of expressions `set_to` accepts
171 and understands. `string_refinementt::set_to` accepts all constraints that are
172 normally accepted by `bv_refinementt`.
174 `string_refinementt::set_to` also understands constraints of the form:
175 * `char_pointer1 = b ? char_pointer2 : char_pointer3` where `char_pointer<i>`
176 variables are of type pointer to characters and `b` is a Boolean
178 * `i = cprover_primitive(args)` where `i` is of signed bit vector type.
179 String primitives are listed in the next section.
181 \note In the implementation, equations that are not of these forms are passed
182 to an embedded `bv_refinementt` solver.
184 \subsection string-representation String representation in the solver
186 String primitives can have arguments which are pointers to characters.
187 These pointers represent strings.
188 To each of these pointers the string solver associate a char array
189 which represents the content of the string.
190 If the pointer is the address of an actual array in the program they should be
191 linked by using the primitive `cprover_string_associate_array_to_pointer`.
192 The length of the array can also be linked to a variable of the program using
193 `cprover_string_associate_length_to_array`.
195 \warning The solver assumes the memory pointed by the arguments is immutable
196 which is not something that is true in general for C pointers for instance.
197 Therefore for each transformation on a string, it is assumed the program
198 allocates a new string before calling a primitive.
200 \section primitives String primitives
202 \subsection basic-primitives Basic access:
204 * `cprover_string_associate_array_to_pointer` : Link with an array of
205 characters of the program.
206 * `cprover_string_associate_length_to_array` : Link the length of the array
207 with the given integer value.
208 * `cprover_string_char_at` :
209 \copybrief add_axioms_for_char_at(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
210 \link add_axioms_for_char_at More... \endlink
211 * `cprover_string_length` :
212 \copybrief add_axioms_for_length(const function_application_exprt &f, array_poolt &array_pool)
213 \link add_axioms_for_length More... \endlink
215 \subsection comparisons Comparisons:
217 * `cprover_string_compare_to` :
218 \copybrief add_axioms_for_compare_to(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool)
219 \link add_axioms_for_compare_to(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) More... \endlink
220 * `cprover_string_contains` :
221 \copybrief add_axioms_for_contains(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool)
222 \link add_axioms_for_contains(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) More... \endlink
223 * `cprover_string_equals` :
224 \copybrief add_axioms_for_equals(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool)
225 \link add_axioms_for_equals(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) More... \endlink
226 * `cprover_string_equals_ignore_case` :
227 \copybrief add_axioms_for_equals_ignore_case(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool)
228 \link add_axioms_for_equals_ignore_case(symbol_generatort &fresh_symbol,const function_application_exprt &f, array_poolt &array_pool) More... \endlink
229 * `cprover_string_hash_code` :
230 \copybrief string_constraint_generatort::add_axioms_for_hash_code
231 \link string_constraint_generatort::add_axioms_for_hash_code More... \endlink
232 * `cprover_string_is_prefix` :
233 \copybrief add_axioms_for_is_prefix
234 \link add_axioms_for_is_prefix More... \endlink
235 * `cprover_string_index_of` :
236 \copybrief add_axioms_for_index_of(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
237 \link add_axioms_for_index_of(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
238 * `cprover_string_last_index_of` :
239 \copybrief add_axioms_for_last_index_of(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
240 \link add_axioms_for_last_index_of(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
242 \subsection transformations Transformations:
244 * `cprover_string_char_set` :
245 \copybrief string_set_char_builtin_functiont::constraints
246 \link string_set_char_builtin_functiont::constraints More... \endlink
247 * `cprover_string_concat` :
248 \copybrief add_axioms_for_concat
249 \link add_axioms_for_concat More... \endlink
250 * `cprover_string_delete` :
251 \copybrief add_axioms_for_delete(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
252 \link add_axioms_for_delete(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
253 * `cprover_string_insert` :
254 \copybrief add_axioms_for_insert(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
255 \link add_axioms_for_insert(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
256 * `cprover_string_replace` :
257 \copybrief add_axioms_for_replace(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
258 \link add_axioms_for_replace(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
259 * `cprover_string_set_length` :
260 \copybrief add_axioms_for_set_length(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
261 \link add_axioms_for_set_length(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
262 * `cprover_string_substring` :
263 \copybrief add_axioms_for_substring(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
264 \link add_axioms_for_substring(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
265 * `cprover_string_to_lower_case` :
266 \copybrief string_to_lower_case_builtin_functiont::constraints
267 \link string_to_lower_case_builtin_functiont::constraints More... \endlink
268 * `cprover_string_to_upper_case` :
269 \copybrief string_to_upper_case_builtin_functiont::constraints
270 \link string_to_upper_case_builtin_functiont::constraints More... \endlink
271 * `cprover_string_trim` :
272 \copybrief add_axioms_for_trim(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
273 \link add_axioms_for_trim(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
275 \subsection conversions Conversions:
277 * `cprover_string_format` :
278 \copybrief add_axioms_for_format
279 \link add_axioms_for_format More... \endlink
280 * `cprover_string_from_literal` :
281 \copybrief add_axioms_from_literal(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
282 \link add_axioms_from_literal(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool) More... \endlink
283 * `cprover_string_of_int` :
284 \copybrief add_axioms_for_string_of_int
285 \link add_axioms_for_string_of_int More... \endlink
286 * `cprover_string_of_float` :
287 \copybrief add_axioms_for_string_of_float
288 \link add_axioms_for_string_of_float More... \endlink
289 * `cprover_string_of_float_scientific_notation` :
290 \copybrief add_axioms_from_float_scientific_notation
291 \link add_axioms_from_float_scientific_notation More... \endlink
292 * `cprover_string_of_char` :
293 \copybrief add_axioms_from_char(const function_application_exprt &f, array_poolt &array_pool)
294 \link add_axioms_from_char(const function_application_exprt &f, array_poolt &array_pool) More... \endlink
295 * `cprover_string_parse_int` :
296 \copybrief add_axioms_for_parse_int
297 \link add_axioms_for_parse_int More... \endlink
299 \subsection solvers-deprecated Deprecated primitives:
301 * `cprover_string_concat_code_point`, `cprover_string_code_point_at`,
302 `cprover_string_code_point_before`, `cprover_string_code_point_count`:
303 Java specific, should be part of Java models.
304 * `cprover_string_offset_by_code_point`, `cprover_string_concat_char`,
305 `cprover_string_concat_int`, `cprover_string_concat_long`,
306 `cprover_string_concat_bool`, `cprover_string_concat_double`,
307 `cprover_string_concat_float`, `cprover_string_insert_int`,
308 `cprover_string_insert_long`, `cprover_string_insert_bool`,
309 `cprover_string_insert_char`, `cprover_string_insert_double`,
310 `cprover_string_insert_float` :
311 Should be done in two steps: conversion from primitive type and call
312 to the string primitive.
313 * `cprover_string_array_of_char_pointer`, `cprover_string_to_char_array` :
314 Pointer to char array association
315 is now handled by `string_constraint_generatort`, there is no need for
317 * `cprover_string_intern` : Never tested.
318 * `cprover_string_is_empty` :
319 Should use `cprover_string_length(s) == 0` instead.
320 * `cprover_string_is_suffix` : Should use `cprover_string_is_prefix` with an
322 * `cprover_string_empty_string` : Can use literal of empty string instead.
323 * `cprover_string_of_long` : Should be the same as `cprover_string_of_int`.
324 * `cprover_string_delete_char_at` : A call to
325 `cprover_string_delete_char_at(s, i)` would be the same thing as
326 `cprover_string_delete(s, i, i+1)`.
327 * `cprover_string_of_bool` :
328 Language dependent, should be implemented in the models.
329 * `cprover_string_copy` : Same as `cprover_string_substring(s, 0)`.
330 * `cprover_string_of_int_hex` : Same as `cprover_string_of_int(s, 16)`.
331 * `cprover_string_of_double` : Same as `cprover_string_of_float`.
333 \section algorithm Decision algorithm
335 \copydetails string_refinementt::dec_solve
337 \subsection instantiation Instantiation
339 This is done by generate_instantiations(const index_set_pairt &index_set, const string_axiomst &axioms, const std::unordered_map<string_not_contains_constraintt, symbol_exprt> ¬_contain_witnesses).
340 \copydetails generate_instantiations(const index_set_pairt &index_set, const string_axiomst &axioms, const std::unordered_map<string_not_contains_constraintt, symbol_exprt> ¬_contain_witnesses).
342 \subsection axiom-check Axiom check
344 \copydetails check_axioms(const string_axiomst &axioms, string_constraint_generatort &generator, const std::function<exprt(const exprt &)> &get, messaget::mstreamt &stream, const namespacet &ns, bool use_counter_example, const union_find_replacet &symbol_resolve, const std::unordered_map<string_not_contains_constraintt, symbol_exprt> ¬_contain_witnesses)
345 \link check_axioms(const string_axiomst &axioms, string_constraint_generatort &generator, const std::function<exprt(const exprt &)> &get, messaget::mstreamt &stream, const namespacet &ns, bool use_counter_example, const union_find_replacet &symbol_resolve, const std::unordered_map<string_not_contains_constraintt, symbol_exprt> ¬_contain_witnesses)
346 (See function documentation...) \endlink
348 \section floatbv Floatbv Directory
350 This library contains the code that is used to convert floating point
351 variables (`floatbv`) to bit vectors (`bv`). This is referred to as
352 ‘bit-blasting’ and is called in the `solver` code during conversion to
353 SAT or SMT. It also contains the abstraction code described in the