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;
44 const array_string_exprt res =
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);
60 const string_constraintt a2(
61 idx,
63 equal_exprt(s1[idx], res[idx]),
65 constraints.universal.push_back(a2);
66
67 symbol_exprt idx2 = fresh_symbol("QA_index_set_length2", index_type);
69 idx2,
72 equal_exprt(res[idx2], from_integer(0, char_type)),
74 constraints.universal.push_back(a3);
75
76 return {from_integer(0, get_return_code_type()), std::move(constraints)};
77}
78
81// NOLINTNEXTLINE
83// NOLINTNEXTLINE
95std::pair<exprt, string_constraintst>
98{
100 PRECONDITION(args.size() == 4 || args.size() == 5);
101 const array_string_exprt str = get_string_expr(array_pool, args[2]);
102 const array_string_exprt res = array_pool.find(args[1], args[0]);
103 const exprt &i = args[3];
104 const exprt j =
105 args.size() == 5 ? args[4] : array_pool.get_or_create_length(str);
106 return add_axioms_for_substring(res, str, i, j);
107}
108
123std::pair<exprt, string_constraintst>
125 const array_string_exprt &res,
126 const array_string_exprt &str,
127 const exprt &start,
128 const exprt &end)
129{
130 const typet &index_type = str.length_type();
131 PRECONDITION(start.type() == index_type);
132 PRECONDITION(end.type() == index_type);
133
134 string_constraintst constraints;
135 const exprt start1 = maximum(start, from_integer(0, start.type()));
136 const exprt end1 =
138
139 // Axiom 1.
140 constraints.existential.push_back(equal_exprt(
141 array_pool.get_or_create_length(res), minus_exprt(end1, start1)));
142
143 // Axiom 2.
144 constraints.universal.push_back([&] {
145 const symbol_exprt idx = fresh_symbol("QA_index_substring", index_type);
146 return string_constraintt(
147 idx,
149 equal_exprt(res[idx], str[plus_exprt(start1, idx)]),
151 }());
152
153 return {from_integer(0, get_return_code_type()), std::move(constraints)};
154}
155
182std::pair<exprt, string_constraintst>
185{
186 PRECONDITION(f.arguments().size() == 3);
187 string_constraintst constraints;
189 const array_string_exprt &res =
190 array_pool.find(f.arguments()[1], f.arguments()[0]);
191 const typet &index_type = str.length_type();
193 const symbol_exprt idx = fresh_symbol("index_trim", index_type);
194 const exprt space_char = from_integer(' ', char_type);
195
196 // Axiom 1.
197 constraints.existential.push_back(greater_or_equal_to(
200
202 constraints.existential.push_back(a2);
203
204 const exprt a3 =
206 constraints.existential.push_back(a3);
207
208 const exprt a4 = greater_or_equal_to(
210 constraints.existential.push_back(a4);
211
212 const exprt a5 = less_than_or_equal_to(
214 constraints.existential.push_back(a5);
215
216 symbol_exprt n = fresh_symbol("QA_index_trim", index_type);
217 binary_relation_exprt non_print(str[n], ID_le, space_char);
219 constraints.universal.push_back(a6);
220
221 // Axiom 7.
222 constraints.universal.push_back([&] {
223 const symbol_exprt n2 = fresh_symbol("QA_index_trim2", index_type);
224 const minus_exprt bound(
227 const binary_relation_exprt eqn2(
228 str[plus_exprt(
230 ID_le,
231 space_char);
232 return string_constraintt(
233 n2, zero_if_negative(bound), eqn2, message_handler);
234 }());
235
236 symbol_exprt n3 = fresh_symbol("QA_index_trim3", index_type);
237 equal_exprt eqn3(res[n3], str[plus_exprt(n3, idx)]);
239 n3,
241 eqn3,
243 constraints.universal.push_back(a8);
244
245 // Axiom 9.
246 constraints.existential.push_back([&] {
247 const plus_exprt index_before(
248 idx,
251 const binary_relation_exprt no_space_before(
252 str[index_before], ID_gt, space_char);
253 return or_exprt(
255 and_exprt(
256 binary_relation_exprt(str[idx], ID_gt, space_char), no_space_before));
257 }());
258 return {from_integer(0, f.type()), constraints};
259}
260
273 exprt expr1,
274 exprt expr2,
275 std::function<array_string_exprt(const exprt &)> get_string_expr,
276 array_poolt &array_pool)
277{
278 if(
279 (expr1.type().id() == ID_unsignedbv || expr1.type().id() == ID_char) &&
280 (expr2.type().id() == ID_char || expr2.type().id() == ID_unsignedbv))
281 return std::make_pair(expr1, expr2);
282 const auto expr1_str = get_string_expr(expr1);
283 const auto expr2_str = get_string_expr(expr2);
284 const auto expr1_length =
285 numeric_cast<std::size_t>(array_pool.get_or_create_length(expr1_str));
286 const auto expr2_length =
287 numeric_cast<std::size_t>(array_pool.get_or_create_length(expr2_str));
288 if(expr1_length && expr2_length && *expr1_length == 1 && *expr2_length == 1)
289 return std::make_pair(exprt(expr1_str[0]), exprt(expr2_str[0]));
290 return {};
291}
292
312std::pair<exprt, string_constraintst>
315{
316 PRECONDITION(f.arguments().size() == 5);
317 string_constraintst constraints;
320 if(
321 const auto maybe_chars = to_char_pair(
322 f.arguments()[3],
323 f.arguments()[4],
324 [&](const exprt &e) { return get_string_expr(array_pool, e); },
325 array_pool))
326 {
327 const auto old_char = maybe_chars->first;
328 const auto new_char = maybe_chars->second;
329
330 constraints.existential.push_back(equal_exprt(
333
334 symbol_exprt qvar = fresh_symbol("QA_replace", str.length_type());
335 implies_exprt case1(
336 equal_exprt(str[qvar], old_char), equal_exprt(res[qvar], new_char));
337 implies_exprt case2(
338 not_exprt(equal_exprt(str[qvar], old_char)),
339 equal_exprt(res[qvar], str[qvar]));
341 qvar,
343 and_exprt(case1, case2),
345 constraints.universal.push_back(a2);
346 return {from_integer(0, f.type()), std::move(constraints)};
347 }
348 return {from_integer(1, f.type()), std::move(constraints)};
349}
350
355std::pair<exprt, string_constraintst>
358{
359 PRECONDITION(f.arguments().size() == 4);
360 const array_string_exprt res =
361 array_pool.find(f.arguments()[1], f.arguments()[0]);
363 exprt index_one = from_integer(1, str.length_type());
365 res, str, f.arguments()[3], plus_exprt(f.arguments()[3], index_one));
366}
367
382std::pair<exprt, string_constraintst>
384 const array_string_exprt &res,
385 const array_string_exprt &str,
386 const exprt &start,
387 const exprt &end)
388{
389 PRECONDITION(start.type() == str.length_type());
390 PRECONDITION(end.type() == str.length_type());
391 const typet &index_type = str.length_type();
393 const array_string_exprt sub1 =
395 const array_string_exprt sub2 =
397 return combine_results(
399 sub1, str, from_integer(0, str.length_type()), start),
402 sub2, str, end, array_pool.get_or_create_length(str)),
403 add_axioms_for_concat(res, sub1, sub2)));
404}
405
408// NOLINTNEXTLINE
410// NOLINTNEXTLINE
417std::pair<exprt, string_constraintst>
420{
421 PRECONDITION(f.arguments().size() == 5);
422 const array_string_exprt res =
423 array_pool.find(f.arguments()[1], f.arguments()[0]);
425 return add_axioms_for_delete(res, arg, f.arguments()[3], f.arguments()[4]);
426}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
optionalt< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral 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.
int8_t s1
bitvector_typet index_type()
Definition c_types.cpp:22
bitvector_typet char_type()
Definition c_types.cpp:111
Boolean AND.
Definition std_expr.h:2071
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:70
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:707
Equality.
Definition std_expr.h:1306
Base class for all expressions.
Definition expr.h:56
typet & type()
Return the type of the expression.
Definition expr.h:84
Application of (mathematical) function.
Boolean implication.
Definition std_expr.h:2134
const irep_idt & id() const
Definition irep.h:396
Binary minus.
Definition std_expr.h:1006
Boolean negation.
Definition std_expr.h:2278
Boolean OR.
Definition std_expr.h:2179
The plus expression Associativity is not specified.
Definition std_expr.h:947
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:113
const typet & subtype() const
Definition type.h:154
The type of an expression, extends irept.
Definition type.h:29
API to expression classes for 'mathematical' expressions.
nonstd::optional< T > optionalt
Definition optional.h:35
#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:37
binary_relation_exprt greater_or_equal_to(exprt lhs, exprt rhs)
Definition string_expr.h:20
equal_exprt equal_to(exprt lhs, exprt rhs)
Definition string_expr.h:55
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:175