cprover
string_constraint_generator_indexof.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Generates string constraints for the family of indexOf and
4  lastIndexOf java functions
5 
6 Author: Romain Brenguier, romain.brenguier@diffblue.com
7 
8 \*******************************************************************/
9 
13 
15 
16 #include <util/mathematical_expr.h>
17 
19 
40 std::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 
60  implies_exprt a3(
61  contains,
62  and_exprt(
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 
112 std::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,
130  minus_exprt(
132  array_pool.get_or_create_length(needle)))));
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.
162  minus_exprt(
169  haystack,
170  needle};
171  constraints.not_contains.push_back(a5);
172 
173  const implies_exprt a6(
174  equal_exprt(
176  equal_exprt(offset, from_index));
177  constraints.existential.push_back(a6);
178 
179  return {offset, std::move(constraints)};
180 }
181 
212 std::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,
230  minus_exprt(
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 
258  plus_exprt(offset, from_integer(1, index_type)),
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(
278  equal_exprt(
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
304 std::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();
313  const typet &char_type = str.content().type().subtype();
314  PRECONDITION(f.type() == index_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 
358 std::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),
395  implies_exprt(contains, notequal_exprt(str[n], c)));
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
426 std::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();
435  const typet &char_type = str.content().type().subtype();
436  PRECONDITION(f.type() == index_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:198
bitvector_typet index_type()
Definition: c_types.cpp:16
bitvector_typet char_type()
Definition: c_types.cpp:114
Boolean AND.
Definition: std_expr.h:1920
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:2172
Boolean implication.
Definition: std_expr.h:1983
const irep_idt & id() const
Definition: irep.h:407
Binary minus.
Definition: std_expr.h:973
Boolean negation.
Definition: std_expr.h:2127
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
Semantic type conversion.
Definition: std_expr.h:1866
The type of an expression, extends irept.
Definition: type.h:28
const typet & subtype() const
Definition: type.h:47
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.