cprover
Loading...
Searching...
No Matches
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),
54 binary_relation_exprt(index, ID_lt, array_pool.get_or_create_length(str)));
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),
76 constraints.universal.push_back(a4);
77
78 symbol_exprt m = fresh_symbol("QA_index_of", index_type);
80 m,
81 lower_bound,
82 zero_if_negative(array_pool.get_or_create_length(str)),
85 constraints.universal.push_back(a5);
86
87 return {index, std::move(constraints)};
88}
89
114std::pair<exprt, string_constraintst>
116 const array_string_exprt &haystack,
117 const array_string_exprt &needle,
118 const exprt &from_index)
119{
120 string_constraintst constraints;
121 const typet &index_type = haystack.length_type();
122 symbol_exprt offset = fresh_symbol("index_of", index_type);
123 symbol_exprt contains = fresh_symbol("contains_substring");
124
125 implies_exprt a1(
126 contains,
127 and_exprt(
128 binary_relation_exprt(from_index, ID_le, offset),
130 offset,
131 ID_le,
133 array_pool.get_or_create_length(haystack),
134 array_pool.get_or_create_length(needle)))));
135 constraints.existential.push_back(a1);
136
137 equal_exprt a2(
138 not_exprt(contains), equal_exprt(offset, from_integer(-1, index_type)));
139 constraints.existential.push_back(a2);
140
141 symbol_exprt qvar = fresh_symbol("QA_index_of_string", index_type);
143 qvar,
144 zero_if_negative(array_pool.get_or_create_length(needle)),
146 contains, equal_exprt(haystack[plus_exprt(qvar, offset)], needle[qvar])),
148 constraints.universal.push_back(a3);
149
150 // string_not contains_constraintt are formulas of the form:
151 // forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s1[x+y] != s2[y]
153 from_index,
154 offset,
155 contains,
156 from_integer(0, index_type),
157 array_pool.get_or_create_length(needle),
158 haystack,
159 needle};
160 constraints.not_contains.push_back(a4);
161
163 from_index,
164 plus_exprt( // Add 1 for inclusive upper bound.
166 array_pool.get_or_create_length(haystack),
167 array_pool.get_or_create_length(needle)),
168 from_integer(1, index_type)),
170 from_integer(0, index_type),
171 array_pool.get_or_create_length(needle),
172 haystack,
173 needle};
174 constraints.not_contains.push_back(a5);
175
176 const implies_exprt a6(
178 array_pool.get_or_create_length(needle), from_integer(0, index_type)),
179 equal_exprt(offset, from_index));
180 constraints.existential.push_back(a6);
181
182 return {offset, std::move(constraints)};
183}
184
215std::pair<exprt, string_constraintst>
217 const array_string_exprt &haystack,
218 const array_string_exprt &needle,
219 const exprt &from_index)
220{
221 string_constraintst constraints;
222 const typet &index_type = haystack.length_type();
223 symbol_exprt offset = fresh_symbol("index_of", index_type);
224 symbol_exprt contains = fresh_symbol("contains_substring");
225
226 implies_exprt a1(
227 contains,
228 and_exprt(
229 binary_relation_exprt(from_integer(-1, index_type), ID_le, offset),
231 offset,
232 ID_le,
234 array_pool.get_or_create_length(haystack),
235 array_pool.get_or_create_length(needle))),
236 binary_relation_exprt(offset, ID_le, from_index)));
237 constraints.existential.push_back(a1);
238
239 equal_exprt a2(
240 not_exprt(contains), equal_exprt(offset, from_integer(-1, index_type)));
241 constraints.existential.push_back(a2);
242
243 symbol_exprt qvar = fresh_symbol("QA_index_of_string", index_type);
244 equal_exprt constr3(haystack[plus_exprt(qvar, offset)], needle[qvar]);
245 const string_constraintt a3(
246 qvar,
247 zero_if_negative(array_pool.get_or_create_length(needle)),
248 implies_exprt(contains, constr3),
250 constraints.universal.push_back(a3);
251
252 // end_index is min(from_index, |str| - |substring|)
253 minus_exprt length_diff(
254 array_pool.get_or_create_length(haystack),
255 array_pool.get_or_create_length(needle));
256 if_exprt end_index(
257 binary_relation_exprt(from_index, ID_le, length_diff),
258 from_index,
259 length_diff);
260
262 plus_exprt(offset, from_integer(1, index_type)),
263 plus_exprt(end_index, from_integer(1, index_type)),
264 contains,
265 from_integer(0, index_type),
266 array_pool.get_or_create_length(needle),
267 haystack,
268 needle};
269 constraints.not_contains.push_back(a4);
270
272 from_integer(0, index_type),
273 plus_exprt(end_index, from_integer(1, index_type)),
275 from_integer(0, index_type),
276 array_pool.get_or_create_length(needle),
277 haystack,
278 needle};
279 constraints.not_contains.push_back(a5);
280
281 const implies_exprt a6(
283 array_pool.get_or_create_length(needle), from_integer(0, index_type)),
284 equal_exprt(offset, from_index));
285 constraints.existential.push_back(a6);
286
287 return {offset, std::move(constraints)};
288}
289
293// NOLINTNEXTLINE
295// NOLINTNEXTLINE
308std::pair<exprt, string_constraintst>
311{
313 PRECONDITION(args.size() == 2 || args.size() == 3);
314 const array_string_exprt str = get_string_expr(array_pool, args[0]);
315 const exprt &c = args[1];
316 const typet &index_type = str.length_type();
318 PRECONDITION(f.type() == index_type);
319 const exprt from_index =
320 args.size() == 2 ? from_integer(0, index_type) : args[2];
321
322 if(c.type().id() == ID_unsignedbv || c.type().id() == ID_signedbv)
323 {
325 str, typecast_exprt(c, char_type), from_index);
326 }
327 else
328 {
329 INVARIANT(
332 "c can only be a (un)signedbv or a refined "
333 "string and the (un)signedbv case is already handled"));
335 return add_axioms_for_index_of_string(str, sub, from_index);
336 }
337}
338
362std::pair<exprt, string_constraintst>
364 const array_string_exprt &str,
365 const exprt &c,
366 const exprt &from_index)
367{
368 string_constraintst constraints;
369 const typet &index_type = str.length_type();
370 const symbol_exprt index = fresh_symbol("last_index_of", index_type);
371 const symbol_exprt contains = fresh_symbol("contains_in_last_index_of");
372
373 const exprt minus1 = from_integer(-1, index_type);
374 const and_exprt a1(
375 binary_relation_exprt(index, ID_ge, minus1),
376 binary_relation_exprt(index, ID_le, from_index),
377 binary_relation_exprt(index, ID_lt, array_pool.get_or_create_length(str)));
378 constraints.existential.push_back(a1);
379
380 const notequal_exprt a2(contains, equal_exprt(index, minus1));
381 constraints.existential.push_back(a2);
382
383 const implies_exprt a3(contains, equal_exprt(str[index], c));
384 constraints.existential.push_back(a3);
385
386 const exprt index1 = from_integer(1, index_type);
387 const plus_exprt from_index_plus_one(from_index, index1);
388 const if_exprt end_index(
390 from_index_plus_one, ID_le, array_pool.get_or_create_length(str)),
391 from_index_plus_one,
392 array_pool.get_or_create_length(str));
393
394 const symbol_exprt n = fresh_symbol("QA_last_index_of1", index_type);
395 const string_constraintt a4(
396 n,
397 zero_if_negative(plus_exprt(index, index1)),
398 zero_if_negative(end_index),
401 constraints.universal.push_back(a4);
402
403 const symbol_exprt m = fresh_symbol("QA_last_index_of2", index_type);
404 const string_constraintt a5(
405 m,
406 zero_if_negative(end_index),
409 constraints.universal.push_back(a5);
410
411 return {index, std::move(constraints)};
412}
413
417// NOLINTNEXTLINE
419// NOLINTNEXTLINE
432std::pair<exprt, string_constraintst>
435{
437 PRECONDITION(args.size() == 2 || args.size() == 3);
438 const array_string_exprt str = get_string_expr(array_pool, args[0]);
439 const exprt c = args[1];
440 const typet &index_type = str.length_type();
442 PRECONDITION(f.type() == index_type);
443
444 const exprt from_index =
445 args.size() == 2 ? array_pool.get_or_create_length(str) : args[2];
446
447 if(c.type().id() == ID_unsignedbv || c.type().id() == ID_signedbv)
448 {
450 str, typecast_exprt(c, char_type), from_index);
451 }
452 else
453 {
455 return add_axioms_for_last_index_of_string(str, sub, from_index);
456 }
457}
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 char_type()
Definition c_types.cpp:106
Boolean AND.
Definition std_expr.h:2125
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:762
Equality.
Definition std_expr.h:1366
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.
The trinary if-then-else operator.
Definition std_expr.h:2497
Boolean implication.
Definition std_expr.h:2225
const irep_idt & id() const
Definition irep.h:388
Binary minus.
Definition std_expr.h:1061
Boolean negation.
Definition std_expr.h:2454
Disequality.
Definition std_expr.h:1425
The plus expression Associativity is not specified.
Definition std_expr.h:1002
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:131
const typet & subtype() const
Definition type.h:187
Semantic type conversion.
Definition std_expr.h:2073
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
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
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:208