Skip to content

Commit feaa85f

Browse files
peterschrammelpeterschrammel
authored
Merge pull request diffblue#1455 from romainbrenguier/doc/string-solver-documentation
TG-838 Documentation of the string solver
2 parents c5ab866 + 7736672 commit feaa85f

15 files changed

+1028
-456
lines changed

‎src/solvers/refinement/README.md

+211
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,211 @@
1+
\page string-solver String solver
2+
3+
\author Romain Brenguier
4+
5+
\tableofcontents
6+
7+
\section string_solver_interface String solver interface
8+
9+
\subsection general_interface General interface
10+
11+
The common interface for solvers in CProver is inherited from
12+
`decision_proceduret` and is the common interface for all solvers.
13+
It is essentially composed of these three functions:
14+
15+
- `string_refinementt::set_to(const exprt &expr, bool value)`:
16+
\copybrief string_refinementt::set_to
17+
- `string_refinementt::dec_solve()`:
18+
\copybrief string_refinementt::dec_solve
19+
- `string_refinementt::get(const exprt &expr) const`:
20+
\copybrief string_refinementt::get
21+
22+
For each goal given to CProver:
23+
- `set_to` is called on several equations, roughly one for each step of the
24+
symbolic execution that leads to that goal;
25+
- `dec_solve` is called to determine whether the goal is reachable given these
26+
equations;
27+
- `get` is called by the interpreter to obtain concrete value to build a trace
28+
leading to the goal;
29+
- The same process can be repeated for further goals, in that case the
30+
constraints added by previous calls to `set_to` remain valid.
31+
32+
\subsection specificity Specificity of the string solver
33+
34+
The specificity of the solver is in what kind of expressions `set_to` accepts
35+
and understands. `string_refinementt::set_to` accepts all constraints that are
36+
normally accepted by `bv_refinementt`.
37+
38+
`string_refinementt::set_to` also understands constraints of the form:
39+
* `char_pointer1 = b ? char_pointer2 : char_pointer3` where `char_pointer<i>`
40+
variables are of type pointer to characters and `b` is a Boolean
41+
expression.
42+
* `i = cprover_primitive(args)` where `i` is of signed bit vector type.
43+
String primitives are listed in the next section.
44+
45+
\note In the implementation, equations that are not of these forms are passed
46+
to an embedded `bv_refinementt` solver.
47+
48+
\subsection string-representation String representation in the solver
49+
50+
String primitives can have arguments which are pointers to characters.
51+
These pointers represent strings.
52+
To each of these pointers the string solver associate a char array
53+
which represents the content of the string.
54+
If the pointer is the address of an actual array in the program they should be
55+
linked by using the primitive `cprover_string_associate_array_to_pointer`.
56+
The length of the array can also be linked to a variable of the program using
57+
`cprover_string_associate_length_to_array`.
58+
59+
\warning The solver assumes the memory pointed by the arguments is immutable
60+
which is not something that is true in general for C pointers for instance.
61+
Therefore for each transformation on a string, it is assumed the program
62+
allocates a new string before calling a primitive.
63+
64+
\section primitives String primitives
65+
66+
\subsection basic-primitives Basic access:
67+
68+
* `cprover_string_associate_array_to_pointer` : Link with an array of
69+
characters of the program.
70+
* `cprover_string_associate_length_to_array` : Link the length of the array
71+
with the given integer value.
72+
* `cprover_string_char_at` :
73+
\copybrief string_constraint_generatort::add_axioms_for_char_at(const function_application_exprt &f)
74+
\link string_constraint_generatort::add_axioms_for_char_at(const function_application_exprt &f) More... \endlink
75+
* `cprover_string_length` :
76+
\copybrief string_constraint_generatort::add_axioms_for_length(const function_application_exprt &f)
77+
\link string_constraint_generatort::add_axioms_for_length(const function_application_exprt &f) More... \endlink
78+
79+
\subsection comparisons Comparisons:
80+
81+
* `cprover_string_compare_to` :
82+
\copybrief string_constraint_generatort::add_axioms_for_compare_to(const function_application_exprt &f)
83+
\link string_constraint_generatort::add_axioms_for_compare_to(const function_application_exprt &f) More... \endlink
84+
* `cprover_string_contains` :
85+
\copybrief string_constraint_generatort::add_axioms_for_contains(const function_application_exprt &f)
86+
\link string_constraint_generatort::add_axioms_for_contains(const function_application_exprt &f) More... \endlink
87+
* `cprover_string_equals` :
88+
\copybrief string_constraint_generatort::add_axioms_for_equals(const function_application_exprt &f)
89+
\link string_constraint_generatort::add_axioms_for_equals(const function_application_exprt &f) More... \endlink
90+
* `cprover_string_equals_ignore_case` :
91+
\copybrief string_constraint_generatort::add_axioms_for_equals_ignore_case(const function_application_exprt &f)
92+
\link string_constraint_generatort::add_axioms_for_equals_ignore_case(const function_application_exprt &f) More... \endlink
93+
* `cprover_string_hash_code` :
94+
\copybrief string_constraint_generatort::add_axioms_for_hash_code
95+
\link string_constraint_generatort::add_axioms_for_hash_code More... \endlink
96+
* `cprover_string_is_prefix` :
97+
\copybrief string_constraint_generatort::add_axioms_for_is_prefix
98+
\link string_constraint_generatort::add_axioms_for_is_prefix More... \endlink
99+
* `cprover_string_is_suffix` :
100+
\copybrief string_constraint_generatort::add_axioms_for_is_suffix
101+
\link string_constraint_generatort::add_axioms_for_is_suffix More... \endlink
102+
* `cprover_string_index_of` :
103+
\copybrief string_constraint_generatort::add_axioms_for_index_of(const function_application_exprt &f)
104+
\link string_constraint_generatort::add_axioms_for_index_of(const function_application_exprt &f) More... \endlink
105+
* `cprover_string_last_index_of` :
106+
\copybrief string_constraint_generatort::add_axioms_for_last_index_of(const function_application_exprt &f)
107+
\link string_constraint_generatort::add_axioms_for_last_index_of(const function_application_exprt &f) More... \endlink
108+
109+
\subsection transformations Transformations:
110+
111+
* `cprover_string_char_set` :
112+
\copybrief string_constraint_generatort::add_axioms_for_char_set(const function_application_exprt &f)
113+
\link string_constraint_generatort::add_axioms_for_char_set(const function_application_exprt &f) More... \endlink
114+
* `cprover_string_concat` :
115+
\copybrief string_constraint_generatort::add_axioms_for_concat(const function_application_exprt &f)
116+
\link string_constraint_generatort::add_axioms_for_concat(const function_application_exprt &f) More... \endlink
117+
* `cprover_string_delete` :
118+
\copybrief string_constraint_generatort::add_axioms_for_delete(const function_application_exprt &f)
119+
\link string_constraint_generatort::add_axioms_for_delete(const function_application_exprt &f) More... \endlink
120+
* `cprover_string_insert` :
121+
\copybrief string_constraint_generatort::add_axioms_for_insert(const function_application_exprt &f)
122+
\link string_constraint_generatort::add_axioms_for_insert(const function_application_exprt &f) More... \endlink
123+
* `cprover_string_replace` :
124+
\copybrief string_constraint_generatort::add_axioms_for_replace(const function_application_exprt &f)
125+
\link string_constraint_generatort::add_axioms_for_replace(const function_application_exprt &f) More... \endlink
126+
* `cprover_string_set_length` :
127+
\copybrief string_constraint_generatort::add_axioms_for_set_length(const function_application_exprt &f)
128+
\link string_constraint_generatort::add_axioms_for_set_length(const function_application_exprt &f) More... \endlink
129+
* `cprover_string_substring` :
130+
\copybrief string_constraint_generatort::add_axioms_for_substring(const function_application_exprt &f)
131+
\link string_constraint_generatort::add_axioms_for_substring(const function_application_exprt &f) More... \endlink
132+
* `cprover_string_to_lower_case` :
133+
\copybrief string_constraint_generatort::add_axioms_for_to_lower_case(const function_application_exprt &f)
134+
\link string_constraint_generatort::add_axioms_for_to_lower_case(const function_application_exprt &f) More... \endlink
135+
* `cprover_string_to_upper_case` :
136+
\copybrief string_constraint_generatort::add_axioms_for_to_upper_case(const function_application_exprt &f)
137+
\link string_constraint_generatort::add_axioms_for_to_upper_case(const function_application_exprt &f) More... \endlink
138+
* `cprover_string_trim` :
139+
\copybrief string_constraint_generatort::add_axioms_for_trim(const function_application_exprt &f)
140+
\link string_constraint_generatort::add_axioms_for_trim(const function_application_exprt &f) More... \endlink
141+
142+
\subsection conversions Conversions:
143+
144+
* `cprover_string_format` :
145+
\copybrief string_constraint_generatort::add_axioms_for_format(const function_application_exprt &f)
146+
\link string_constraint_generatort::add_axioms_for_format(const function_application_exprt &f) More... \endlink
147+
* `cprover_string_from_literal` :
148+
\copybrief string_constraint_generatort::add_axioms_from_literal(const function_application_exprt &f)
149+
\link string_constraint_generatort::add_axioms_from_literal(const function_application_exprt &f) More... \endlink
150+
* `cprover_string_of_int` :
151+
\copybrief string_constraint_generatort::add_axioms_from_int(const function_application_exprt &f)
152+
\link string_constraint_generatort::add_axioms_from_int(const function_application_exprt &f) More... \endlink
153+
* `cprover_string_of_float` :
154+
\copybrief string_constraint_generatort::add_axioms_for_string_of_float(const function_application_exprt &f)
155+
\link string_constraint_generatort::add_axioms_for_string_of_float(const function_application_exprt &f) More... \endlink
156+
* `cprover_string_of_float_scientific_notation` :
157+
\copybrief string_constraint_generatort::add_axioms_from_float_scientific_notation(const function_application_exprt &f)
158+
\link string_constraint_generatort::add_axioms_from_float_scientific_notation(const function_application_exprt &f) More... \endlink
159+
* `cprover_string_of_char` :
160+
\copybrief string_constraint_generatort::add_axioms_from_char(const function_application_exprt &f)
161+
\link string_constraint_generatort::add_axioms_from_char(const function_application_exprt &f) More... \endlink
162+
* `cprover_string_parse_int` :
163+
\copybrief string_constraint_generatort::add_axioms_for_parse_int(const function_application_exprt &f)
164+
\link string_constraint_generatort::add_axioms_for_parse_int(const function_application_exprt &f) More... \endlink
165+
166+
\subsection deprecated Deprecated primitives:
167+
168+
* `cprover_string_concat_code_point`, `cprover_string_code_point_at`,
169+
`cprover_string_code_point_before`, `cprover_string_code_point_count`:
170+
Java specific, should be part of Java models.
171+
* `cprover_string_offset_by_code_point`, `cprover_string_concat_char`,
172+
`cprover_string_concat_int`, `cprover_string_concat_long`,
173+
`cprover_string_concat_bool`, `cprover_string_concat_double`,
174+
`cprover_string_concat_float`, `cprover_string_insert_int`,
175+
`cprover_string_insert_long`, `cprover_string_insert_bool`,
176+
`cprover_string_insert_char`, `cprover_string_insert_double`,
177+
`cprover_string_insert_float` :
178+
Should be done in two steps: conversion from primitive type and call
179+
to the string primitive.
180+
* `cprover_string_array_of_char_pointer`, `cprover_string_to_char_array` :
181+
Pointer to char array association
182+
is now handled by `string_constraint_generatort`, there is no need for
183+
explicit conversion.
184+
* `cprover_string_intern` : Never tested.
185+
* `cprover_string_is_empty` :
186+
Should use `cprover_string_length(s) == 0` instead.
187+
* `cprover_string_empty_string` : Can use literal of empty string instead.
188+
* `cprover_string_of_long` : Should be the same as `cprover_string_of_int`.
189+
* `cprover_string_delete_char_at` : A call to
190+
`cprover_string_delete_char_at(s, i)` would be the same thing as
191+
`cprover_string_delete(s, i, i+1)`.
192+
* `cprover_string_of_bool` :
193+
Language dependent, should be implemented in the models.
194+
* `cprover_string_copy` : Same as `cprover_string_substring(s, 0)`.
195+
* `cprover_string_of_int_hex` : Same as `cprover_string_of_int(s, 16)`.
196+
* `cprover_string_of_double` : Same as `cprover_string_of_float`.
197+
198+
\section algorithm Decision algorithm
199+
200+
\copydetails string_refinementt::dec_solve
201+
202+
\subsection instantiation Instantiation
203+
204+
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).
205+
\copydetails generate_instantiations(messaget::mstreamt &stream, const namespacet &ns, const string_constraint_generatort &generator, const index_set_pairt &index_set, const string_axiomst &axioms)
206+
207+
\subsection axiom-check Axiom check
208+
209+
\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)
210+
\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)
211+
(See function documentation...) \endlink

‎src/solvers/refinement/string_constraint.h

+27-23
Original file line numberDiff line numberDiff line change
@@ -26,29 +26,32 @@ Author: Romain Brenguier, [email protected]
2626
#include <util/string_expr.h>
2727
#include <langapi/language_util.h>
2828

29-
/*! \brief Universally quantified string constraint
30-
31-
This represents a universally quantified string constraint as laid out in
32-
DOI: 10.1007/978-3-319-03077-7. The paper seems to specify a universal
33-
constraint as follows.
34-
35-
A universal constraint is of the form \f$\forall n. L(n) \rightarrow
36-
P(n, s_0,\ldots, s_k)\f$ where
37-
38-
1. \f$L(n)\f$ does not contain string indices [possibly not required, but
39-
implied by examples]
40-
2. \f$\forall n. L(n) \rightarrow P'\left(s_0[f_0(n)],\ldots, s_k[f_k(n)]
41-
\right)\f$, i.e. when focusing on one specific string, all indices are
42-
the same [stated in a roundabout manner]
43-
3. Each \f$f\f$ is linear and therefore has an inverse [explicitly stated]
44-
4. \f$L(n)\f$ and \f$P(n, s_0,\ldots, s_k)\f$ may contain other (free)
45-
variables, but in \f$P\f$, \f$n\f$ can only occur as an argument to an
46-
\f$f\f$ [explicitly stated, implied]
47-
48-
We extend this slightly by restricting n to be in a specific range, but this
49-
is another implication which can be pushed in to \f$L(n)\f$.
50-
*/
51-
29+
/// ### Universally quantified string constraint
30+
///
31+
/// This represents a universally quantified string constraint as laid out in
32+
/// DOI: 10.1007/978-3-319-03077-7. The paper seems to specify a universal
33+
/// constraint as follows.
34+
///
35+
/// A universal constraint is of the form
36+
/// \f$ \forall i.\ PI(i) \Rightarrow PV(i)\f$
37+
/// where \f$PI\f$ and \f$PV\f$ satisfies the following conditions:
38+
///
39+
/// * The predicate `PI` , called the index guard, must follow the grammar
40+
/// * \f$iguard : iguard \land iguard \mid iguard \lor iguard \mid
41+
/// iterm \le iterm \mid iterm = iterm \f$
42+
/// * \f$iterm : integer\_constant1 \times i + integer\_constant2 \f$
43+
///
44+
/// * The predicate `PV` is called the value constraint.
45+
/// The index variable `i` can only be used in array read expressions of
46+
/// the form `a[i]`.
47+
/// ie. `PV` is of the form \f$P'(s_0[f_0(i)],\ldots, s_k[f_k(i)]
48+
/// )\f$, moreover when focusing on one specific string, all indices are
49+
/// the same [stated in a roundabout manner].
50+
/// \f$L(n)\f$ and \f$P(n, s_0,\ldots, s_k)\f$ may contain other (free)
51+
/// variables, but in \f$P\f$, \f$n\f$ can only occur as an argument to an
52+
/// \f$f\f$ [explicitly stated, implied].
53+
///
54+
/// \todo The fact that we follow this grammar is not enforced at the moment.
5255
class string_constraintt: public exprt
5356
{
5457
public:
@@ -155,6 +158,7 @@ inline std::string from_expr(
155158
from_expr(ns, identifier, expr.body());
156159
}
157160

161+
/// Constraints to encode non containement of strings.
158162
class string_not_contains_constraintt: public exprt
159163
{
160164
public:

0 commit comments

Comments
 (0)