cprover
Loading...
Searching...
No Matches
string_constraint_generator_transformation.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Generates string constraints for string transformations,
4 that is, functions taking one string and returning another
5
6Author: Romain Brenguier, romain.brenguier@diffblue.com
7
8\*******************************************************************/
9
13
15
16#include <util/arith_tools.h>
18
38std::pair<exprt, string_constraintst>
41{
42 PRECONDITION(f.arguments().size() == 4);
43 string_constraintst constraints;
45 array_pool.find(f.arguments()[1], f.arguments()[0]);
47 const exprt &k = f.arguments()[3];
48 const typet &index_type = s1.length_type();
49 const typet &char_type = to_type_with_subtype(s1.content().type()).subtype();
50
51 // We add axioms:
52 // a1 : |res|=max(k, 0)
53 // a2 : forall i< min(|s1|, k) .res[i] = s1[i]
54 // a3 : forall |s1| <= i < |res|. res[i] = 0
55
56 constraints.existential.push_back(
58
59 const symbol_exprt idx = fresh_symbol("QA_index_set_length", index_type);
61 idx,
63 equal_exprt(s1[idx], res[idx]));
64 constraints.universal.push_back(a2);
65
66 symbol_exprt idx2 = fresh_symbol("QA_index_set_length2", index_type);
68 idx2,
72 constraints.universal.push_back(a3);
73
74 return {from_integer(0, get_return_code_type()), std::move(constraints)};
75}
76
79// NOLINTNEXTLINE
81// NOLINTNEXTLINE
93std::pair<exprt, string_constraintst>
96{
98 PRECONDITION(args.size() == 4 || args.size() == 5);
99 const array_string_exprt str = get_string_expr(array_pool, args[2]);
100 const array_string_exprt res = array_pool.find(args[1], args[0]);
101 const exprt &i = args[3];
102 const exprt j =
103 args.size() == 5 ? args[4] : array_pool.get_or_create_length(str);
104 return add_axioms_for_substring(res, str, i, j);
105}
106
121std::pair<exprt, string_constraintst>
123 const array_string_exprt &res,
124 const array_string_exprt &str,
125 const exprt &start,
126 const exprt &end)
127{
128 const typet &index_type = str.length_type();
129 PRECONDITION(start.type() == index_type);
130 PRECONDITION(end.type() == index_type);
131
132 string_constraintst constraints;
133 const exprt start1 = maximum(start, from_integer(0, start.type()));
134 const exprt end1 =
136
137 // Axiom 1.
138 constraints.existential.push_back(equal_exprt(
140
141 // Axiom 2.
142 constraints.universal.push_back([&] {
143 const symbol_exprt idx = fresh_symbol("QA_index_substring", index_type);
144 return string_constraintt(
145 idx,
147 equal_exprt(res[idx], str[plus_exprt(start1, idx)]));
148 }());
149
150 return {from_integer(0, get_return_code_type()), std::move(constraints)};
151}
152
179std::pair<exprt, string_constraintst>
182{
183 PRECONDITION(f.arguments().size() == 3);
184 string_constraintst constraints;
186 const array_string_exprt &res =
187 array_pool.find(f.arguments()[1], f.arguments()[0]);
188 const typet &index_type = str.length_type();
190 const symbol_exprt idx = fresh_symbol("index_trim", index_type);
192
193 // Axiom 1.
194 constraints.existential.push_back(greater_or_equal_to(
197
199 constraints.existential.push_back(a2);
200
201 const exprt a3 =
203 constraints.existential.push_back(a3);
204
207 constraints.existential.push_back(a4);
208
211 constraints.existential.push_back(a5);
212
213 symbol_exprt n = fresh_symbol("QA_index_trim", index_type);
216 constraints.universal.push_back(a6);
217
218 // Axiom 7.
219 constraints.universal.push_back([&] {
220 const symbol_exprt n2 = fresh_symbol("QA_index_trim2", index_type);
221 const minus_exprt bound(
225 str[plus_exprt(
227 ID_le,
228 space_char);
230 }());
231
232 symbol_exprt n3 = fresh_symbol("QA_index_trim3", index_type);
233 equal_exprt eqn3(res[n3], str[plus_exprt(n3, idx)]);
236 constraints.universal.push_back(a8);
237
238 // Axiom 9.
239 constraints.existential.push_back([&] {
241 idx,
246 return or_exprt(
248 and_exprt(
250 }());
251 return {from_integer(0, f.type()), constraints};
252}
253
266 exprt expr1,
267 exprt expr2,
268 std::function<array_string_exprt(const exprt &)> get_string_expr,
269 array_poolt &array_pool)
270{
271 if(
272 (expr1.type().id() == ID_unsignedbv || expr1.type().id() == ID_char) &&
273 (expr2.type().id() == ID_char || expr2.type().id() == ID_unsignedbv))
274 return std::make_pair(expr1, expr2);
275 const auto expr1_str = get_string_expr(expr1);
276 const auto expr2_str = get_string_expr(expr2);
277 const auto expr1_length =
279 const auto expr2_length =
281 if(expr1_length && expr2_length && *expr1_length == 1 && *expr2_length == 1)
282 return std::make_pair(exprt(expr1_str[0]), exprt(expr2_str[0]));
283 return {};
284}
285
305std::pair<exprt, string_constraintst>
308{
309 PRECONDITION(f.arguments().size() == 5);
310 string_constraintst constraints;
313 if(
314 const auto maybe_chars = to_char_pair(
315 f.arguments()[3],
316 f.arguments()[4],
317 [&](const exprt &e) { return get_string_expr(array_pool, e); },
318 array_pool))
319 {
320 const auto old_char = maybe_chars->first;
321 const auto new_char = maybe_chars->second;
322
323 constraints.existential.push_back(equal_exprt(
326
327 symbol_exprt qvar = fresh_symbol("QA_replace", str.length_type());
332 equal_exprt(res[qvar], str[qvar]));
334 qvar,
337 constraints.universal.push_back(a2);
338 return {from_integer(0, f.type()), std::move(constraints)};
339 }
340 return {from_integer(1, f.type()), std::move(constraints)};
341}
342
347std::pair<exprt, string_constraintst>
359
374std::pair<exprt, string_constraintst>
397
400// NOLINTNEXTLINE
402// NOLINTNEXTLINE
409std::pair<exprt, string_constraintst>
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
array_string_exprt get_string_expr(array_poolt &array_pool, const exprt &expr)
Fetch the string_exprt corresponding to the given refined_string_exprt.
bitvector_typet index_type()
Definition c_types.cpp:22
bitvector_typet char_type()
Definition c_types.cpp:124
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Boolean AND.
Definition std_expr.h:1974
Correspondance between arrays and pointers string representations.
Definition array_pool.h:42
exprt get_or_create_length(const array_string_exprt &s)
Get the length of an array_string_exprt from the array_pool.
array_string_exprt fresh_string(const typet &index_type, const typet &char_type)
Construct a string expression whose length and content are new variables.
array_string_exprt find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
const typet & length_type() const
Definition string_expr.h:69
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:674
Equality.
Definition std_expr.h:1225
Base class for all expressions.
Definition expr.h:54
typet & type()
Return the type of the expression.
Definition expr.h:82
Application of (mathematical) function.
Boolean implication.
Definition std_expr.h:2037
Binary minus.
Definition std_expr.h:973
Boolean negation.
Definition std_expr.h:2181
Boolean OR.
Definition std_expr.h:2082
The plus expression Associativity is not specified.
Definition std_expr.h:914
std::pair< exprt, string_constraintst > add_axioms_for_delete(const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end)
Add axioms stating that res corresponds to the input str where we removed characters between the posi...
std::pair< exprt, string_constraintst > add_axioms_for_substring(const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end)
Add axioms ensuring that res corresponds to the substring of str between indexes ‘start’ = max(start,...
std::pair< exprt, string_constraintst > add_axioms_for_concat(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
Add axioms enforcing that res is equal to the concatenation of s1 and s2.
std::pair< exprt, string_constraintst > add_axioms_for_set_length(const function_application_exprt &f)
Reduce or extend a string to have the given length.
std::pair< exprt, string_constraintst > add_axioms_for_trim(const function_application_exprt &f)
Remove leading and trailing whitespaces.
std::pair< exprt, string_constraintst > add_axioms_for_replace(const function_application_exprt &f)
Replace a character by another in a string.
std::pair< exprt, string_constraintst > add_axioms_for_delete_char_at(const function_application_exprt &expr)
add axioms corresponding to the StringBuilder.deleteCharAt java function
std::pair< exprt, string_constraintst > combine_results(std::pair< exprt, string_constraintst > result1, std::pair< exprt, string_constraintst > result2)
Combine the results of two add_axioms function by taking the maximum of the return codes and merging ...
Expression to hold a symbol (variable)
Definition std_expr.h:80
const typet & subtype() const
Definition type.h:156
The type of an expression, extends irept.
Definition type.h:29
API to expression classes for 'mathematical' expressions.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
Generates string constraints to link results from string functions with their arguments.
exprt maximum(const exprt &a, const exprt &b)
exprt minimum(const exprt &a, const exprt &b)
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
signedbv_typet get_return_code_type()
static optionalt< std::pair< exprt, exprt > > to_char_pair(exprt expr1, exprt expr2, std::function< array_string_exprt(const exprt &)> get_string_expr, array_poolt &array_pool)
Convert two expressions to pair of chars If both expressions are characters, return pair of them If b...
binary_relation_exprt less_than_or_equal_to(exprt lhs, exprt rhs)
Definition string_expr.h:36
binary_relation_exprt greater_or_equal_to(exprt lhs, exprt rhs)
Definition string_expr.h:19
equal_exprt equal_to(exprt lhs, exprt rhs)
Definition string_expr.h:54
Collection of constraints of different types: existential formulas, universal formulas,...
std::vector< exprt > existential
std::vector< string_constraintt > universal
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:177