cprover
string_constraint_generator_indexof.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Generates string constraints for the family of indexOf and
4 lastIndexOf java functions
5
6Author: Romain Brenguier, romain.brenguier@diffblue.com
7
8\*******************************************************************/
9
13
15
17
19
40std::pair<exprt, string_constraintst>
42 const array_string_exprt &str,
43 const exprt &c,
44 const exprt &from_index)
45{
46 string_constraintst constraints;
47 const typet &index_type = str.length_type();
48 symbol_exprt index = fresh_symbol("index_of", index_type);
49 symbol_exprt contains = fresh_symbol("contains_in_index_of");
50
51 exprt minus1 = from_integer(-1, index_type);
52 and_exprt a1(
53 binary_relation_exprt(index, ID_ge, minus1),
55 constraints.existential.push_back(a1);
56
57 equal_exprt a2(not_exprt(contains), equal_exprt(index, minus1));
58 constraints.existential.push_back(a2);
59
63 binary_relation_exprt(from_index, ID_le, index),
64 equal_exprt(str[index], c)));
65 constraints.existential.push_back(a3);
66
67 const exprt lower_bound(zero_if_negative(from_index));
68
69 symbol_exprt n = fresh_symbol("QA_index_of", index_type);
71 n,
72 lower_bound,
73 zero_if_negative(index),
75 constraints.universal.push_back(a4);
76
77 symbol_exprt m = fresh_symbol("QA_index_of", index_type);
79 m,
80 lower_bound,
83 constraints.universal.push_back(a5);
84
85 return {index, std::move(constraints)};
86}
87
112std::pair<exprt, string_constraintst>
114 const array_string_exprt &haystack,
115 const array_string_exprt &needle,
116 const exprt &from_index)
117{
118 string_constraintst constraints;
119 const typet &index_type = haystack.length_type();
120 symbol_exprt offset = fresh_symbol("index_of", index_type);
121 symbol_exprt contains = fresh_symbol("contains_substring");
122
123 implies_exprt a1(
124 contains,
125 and_exprt(
126 binary_relation_exprt(from_index, ID_le, offset),
128 offset,
129 ID_le,
133 constraints.existential.push_back(a1);
134
135 equal_exprt a2(
137 constraints.existential.push_back(a2);
138
139 symbol_exprt qvar = fresh_symbol("QA_index_of_string", index_type);
141 qvar,
144 contains, equal_exprt(haystack[plus_exprt(qvar, offset)], needle[qvar])));
145 constraints.universal.push_back(a3);
146
147 // string_not contains_constraintt are formulas of the form:
148 // forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s1[x+y] != s2[y]
150 from_index,
151 offset,
152 contains,
155 haystack,
156 needle};
157 constraints.not_contains.push_back(a4);
158
160 from_index,
161 plus_exprt( // Add 1 for inclusive upper bound.
169 haystack,
170 needle};
171 constraints.not_contains.push_back(a5);
172
173 const implies_exprt a6(
176 equal_exprt(offset, from_index));
177 constraints.existential.push_back(a6);
178
179 return {offset, std::move(constraints)};
180}
181
212std::pair<exprt, string_constraintst>
214 const array_string_exprt &haystack,
215 const array_string_exprt &needle,
216 const exprt &from_index)
217{
218 string_constraintst constraints;
219 const typet &index_type = haystack.length_type();
220 symbol_exprt offset = fresh_symbol("index_of", index_type);
221 symbol_exprt contains = fresh_symbol("contains_substring");
222
223 implies_exprt a1(
224 contains,
225 and_exprt(
226 binary_relation_exprt(from_integer(-1, index_type), ID_le, offset),
228 offset,
229 ID_le,
233 binary_relation_exprt(offset, ID_le, from_index)));
234 constraints.existential.push_back(a1);
235
236 equal_exprt a2(
238 constraints.existential.push_back(a2);
239
240 symbol_exprt qvar = fresh_symbol("QA_index_of_string", index_type);
241 equal_exprt constr3(haystack[plus_exprt(qvar, offset)], needle[qvar]);
242 const string_constraintt a3(
243 qvar,
245 implies_exprt(contains, constr3));
246 constraints.universal.push_back(a3);
247
248 // end_index is min(from_index, |str| - |substring|)
249 minus_exprt length_diff(
252 if_exprt end_index(
253 binary_relation_exprt(from_index, ID_le, length_diff),
254 from_index,
255 length_diff);
256
259 plus_exprt(end_index, from_integer(1, index_type)),
260 contains,
263 haystack,
264 needle};
265 constraints.not_contains.push_back(a4);
266
269 plus_exprt(end_index, from_integer(1, index_type)),
273 haystack,
274 needle};
275 constraints.not_contains.push_back(a5);
276
277 const implies_exprt a6(
280 equal_exprt(offset, from_index));
281 constraints.existential.push_back(a6);
282
283 return {offset, std::move(constraints)};
284}
285
289// NOLINTNEXTLINE
291// NOLINTNEXTLINE
304std::pair<exprt, string_constraintst>
307{
309 PRECONDITION(args.size() == 2 || args.size() == 3);
310 const array_string_exprt str = get_string_expr(array_pool, args[0]);
311 const exprt &c = args[1];
312 const typet &index_type = str.length_type();
315 const exprt from_index =
316 args.size() == 2 ? from_integer(0, index_type) : args[2];
317
318 if(c.type().id() == ID_unsignedbv || c.type().id() == ID_signedbv)
319 {
321 str, typecast_exprt(c, char_type), from_index);
322 }
323 else
324 {
325 INVARIANT(
328 "c can only be a (un)signedbv or a refined "
329 "string and the (un)signedbv case is already handled"));
331 return add_axioms_for_index_of_string(str, sub, from_index);
332 }
333}
334
358std::pair<exprt, string_constraintst>
360 const array_string_exprt &str,
361 const exprt &c,
362 const exprt &from_index)
363{
364 string_constraintst constraints;
365 const typet &index_type = str.length_type();
366 const symbol_exprt index = fresh_symbol("last_index_of", index_type);
367 const symbol_exprt contains = fresh_symbol("contains_in_last_index_of");
368
369 const exprt minus1 = from_integer(-1, index_type);
370 const and_exprt a1(
371 binary_relation_exprt(index, ID_ge, minus1),
372 binary_relation_exprt(index, ID_le, from_index),
374 constraints.existential.push_back(a1);
375
376 const notequal_exprt a2(contains, equal_exprt(index, minus1));
377 constraints.existential.push_back(a2);
378
379 const implies_exprt a3(contains, equal_exprt(str[index], c));
380 constraints.existential.push_back(a3);
381
382 const exprt index1 = from_integer(1, index_type);
383 const plus_exprt from_index_plus_one(from_index, index1);
384 const if_exprt end_index(
386 from_index_plus_one, ID_le, array_pool.get_or_create_length(str)),
387 from_index_plus_one,
389
390 const symbol_exprt n = fresh_symbol("QA_last_index_of1", index_type);
391 const string_constraintt a4(
392 n,
393 zero_if_negative(plus_exprt(index, index1)),
394 zero_if_negative(end_index),
396 constraints.universal.push_back(a4);
397
398 const symbol_exprt m = fresh_symbol("QA_last_index_of2", index_type);
399 const string_constraintt a5(
400 m,
401 zero_if_negative(end_index),
403 constraints.universal.push_back(a5);
404
405 return {index, std::move(constraints)};
406}
407
411// NOLINTNEXTLINE
413// NOLINTNEXTLINE
426std::pair<exprt, string_constraintst>
429{
431 PRECONDITION(args.size() == 2 || args.size() == 3);
432 const array_string_exprt str = get_string_expr(array_pool, args[0]);
433 const exprt c = args[1];
434 const typet &index_type = str.length_type();
437
438 const exprt from_index =
439 args.size() == 2 ? array_pool.get_or_create_length(str) : args[2];
440
441 if(c.type().id() == ID_unsignedbv || c.type().id() == ID_signedbv)
442 {
444 str, typecast_exprt(c, char_type), from_index);
445 }
446 else
447 {
449 return add_axioms_for_last_index_of_string(str, sub, from_index);
450 }
451}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
array_string_exprt get_string_expr(array_poolt &array_pool, const exprt &expr)
Fetch the string_exprt corresponding to the given refined_string_exprt.
Definition: array_pool.cpp:199
bitvector_typet index_type()
Definition: c_types.cpp:22
bitvector_typet char_type()
Definition: c_types.cpp:124
Boolean AND.
Definition: std_expr.h:1974
exprt get_or_create_length(const array_string_exprt &s)
Get the length of an array_string_exprt from the array_pool.
Definition: array_pool.cpp:26
const typet & length_type() const
Definition: string_expr.h:69
exprt & content()
Definition: string_expr.h:74
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.
The trinary if-then-else operator.
Definition: std_expr.h:2226
Boolean implication.
Definition: std_expr.h:2037
const irep_idt & id() const
Definition: irep.h:396
Binary minus.
Definition: std_expr.h:973
Boolean negation.
Definition: std_expr.h:2181
Disequality.
Definition: std_expr.h:1283
The plus expression Associativity is not specified.
Definition: std_expr.h:914
std::pair< exprt, string_constraintst > add_axioms_for_last_index_of(const array_string_exprt &str, const exprt &c, const exprt &from_index)
Add axioms stating that the returned value is the index within haystack (str) of the last occurrence ...
std::pair< exprt, string_constraintst > add_axioms_for_last_index_of_string(const array_string_exprt &haystack, const array_string_exprt &needle, const exprt &from_index)
Add axioms stating that the returned value is the index within haystack of the last occurrence of nee...
std::pair< exprt, string_constraintst > add_axioms_for_index_of(const array_string_exprt &str, const exprt &c, const exprt &from_index)
Add axioms stating that the returned value is the index within haystack (str) of the first occurrence...
std::pair< exprt, string_constraintst > add_axioms_for_index_of_string(const array_string_exprt &haystack, const array_string_exprt &needle, const exprt &from_index)
Add axioms stating that the returned value index is the index within haystack of the first occurrence...
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const typet & subtype() const
Definition: type.h:156
Semantic type conversion.
Definition: std_expr.h:1920
The type of an expression, extends irept.
Definition: type.h:29
API to expression classes for 'mathematical' expressions.
bool is_refined_string_type(const typet &type)
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
Generates string constraints to link results from string functions with their arguments.
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
static bool contains(const exprt &index, const symbol_exprt &qvar)
Look for symbol qvar in the expression index and return true if found.
#define string_refinement_invariantt(reason)
Collection of constraints of different types: existential formulas, universal formulas,...
std::vector< string_not_contains_constraintt > not_contains
std::vector< exprt > existential
std::vector< string_constraintt > universal
Constraints to encode non containement of strings.
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:177