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 
16 
38 std::pair<exprt, string_constraintst> add_axioms_for_index_of(
39  symbol_generatort &fresh_symbol,
40  const array_string_exprt &str,
41  const exprt &c,
42  const exprt &from_index)
43 {
44  string_constraintst constraints;
45  const typet &index_type=str.length().type();
46  symbol_exprt index = fresh_symbol("index_of", index_type);
47  symbol_exprt contains = fresh_symbol("contains_in_index_of");
48 
49  exprt minus1=from_integer(-1, index_type);
50  and_exprt a1(
51  binary_relation_exprt(index, ID_ge, minus1),
52  binary_relation_exprt(index, ID_lt, str.length()));
53  constraints.existential.push_back(a1);
54 
55  equal_exprt a2(not_exprt(contains), equal_exprt(index, minus1));
56  constraints.existential.push_back(a2);
57 
58  implies_exprt a3(
59  contains,
60  and_exprt(
61  binary_relation_exprt(from_index, ID_le, index),
62  equal_exprt(str[index], c)));
63  constraints.existential.push_back(a3);
64 
65  const exprt lower_bound(zero_if_negative(from_index));
66 
67  symbol_exprt n = fresh_symbol("QA_index_of", index_type);
69  n,
70  lower_bound,
71  zero_if_negative(index),
72  implies_exprt(contains, notequal_exprt(str[n], c)));
73  constraints.universal.push_back(a4);
74 
75  symbol_exprt m = fresh_symbol("QA_index_of", index_type);
77  m,
78  lower_bound,
79  zero_if_negative(str.length()),
80  implies_exprt(not_exprt(contains), not_exprt(equal_exprt(str[m], c))));
81  constraints.universal.push_back(a5);
82 
83  return {index, std::move(constraints)};
84 }
85 
111 std::pair<exprt, string_constraintst> add_axioms_for_index_of_string(
112  symbol_generatort &fresh_symbol,
113  const array_string_exprt &haystack,
114  const array_string_exprt &needle,
115  const exprt &from_index)
116 {
117  string_constraintst constraints;
118  const typet &index_type=haystack.length().type();
119  symbol_exprt offset = fresh_symbol("index_of", index_type);
120  symbol_exprt contains = fresh_symbol("contains_substring");
121 
122  implies_exprt a1(
123  contains,
124  and_exprt(
125  binary_relation_exprt(from_index, ID_le, offset),
127  offset, ID_le, minus_exprt(haystack.length(), needle.length()))));
128  constraints.existential.push_back(a1);
129 
130  equal_exprt a2(
131  not_exprt(contains),
132  equal_exprt(offset, from_integer(-1, index_type)));
133  constraints.existential.push_back(a2);
134 
135  symbol_exprt qvar = fresh_symbol("QA_index_of_string", index_type);
137  qvar,
138  zero_if_negative(needle.length()),
140  contains, equal_exprt(haystack[plus_exprt(qvar, offset)], needle[qvar])));
141  constraints.universal.push_back(a3);
142 
143  // string_not contains_constraintt are formulas of the form:
144  // forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s1[x+y] != s2[y]
145  const string_not_contains_constraintt a4 = {from_index,
146  offset,
147  contains,
149  needle.length(),
150  haystack,
151  needle};
152  constraints.not_contains.push_back(a4);
153 
155  from_index,
156  plus_exprt( // Add 1 for inclusive upper bound.
157  minus_exprt(haystack.length(), needle.length()),
159  not_exprt(contains),
161  needle.length(),
162  haystack,
163  needle};
164  constraints.not_contains.push_back(a5);
165 
166  const implies_exprt a6(
167  equal_exprt(needle.length(), from_integer(0, index_type)),
168  equal_exprt(offset, from_index));
169  constraints.existential.push_back(a6);
170 
171  return {offset, std::move(constraints)};
172 }
173 
205 std::pair<exprt, string_constraintst> add_axioms_for_last_index_of_string(
206  symbol_generatort &fresh_symbol,
207  const array_string_exprt &haystack,
208  const array_string_exprt &needle,
209  const exprt &from_index)
210 {
211  string_constraintst constraints;
212  const typet &index_type=haystack.length().type();
213  symbol_exprt offset = fresh_symbol("index_of", index_type);
214  symbol_exprt contains = fresh_symbol("contains_substring");
215 
216  implies_exprt a1(
217  contains,
218  and_exprt(
219  binary_relation_exprt(from_integer(-1, index_type), ID_le, offset),
221  offset, ID_le, minus_exprt(haystack.length(), needle.length())),
222  binary_relation_exprt(offset, ID_le, from_index)));
223  constraints.existential.push_back(a1);
224 
225  equal_exprt a2(
226  not_exprt(contains),
227  equal_exprt(offset, from_integer(-1, index_type)));
228  constraints.existential.push_back(a2);
229 
230  symbol_exprt qvar = fresh_symbol("QA_index_of_string", index_type);
231  equal_exprt constr3(haystack[plus_exprt(qvar, offset)], needle[qvar]);
232  const string_constraintt a3(
233  qvar, zero_if_negative(needle.length()), implies_exprt(contains, constr3));
234  constraints.universal.push_back(a3);
235 
236  // end_index is min(from_index, |str| - |substring|)
237  minus_exprt length_diff(haystack.length(), needle.length());
238  if_exprt end_index(
239  binary_relation_exprt(from_index, ID_le, length_diff),
240  from_index,
241  length_diff);
242 
244  plus_exprt(offset, from_integer(1, index_type)),
245  plus_exprt(end_index, from_integer(1, index_type)),
246  contains,
248  needle.length(),
249  haystack,
250  needle};
251  constraints.not_contains.push_back(a4);
252 
255  plus_exprt(end_index, from_integer(1, index_type)),
256  not_exprt(contains),
258  needle.length(),
259  haystack,
260  needle};
261  constraints.not_contains.push_back(a5);
262 
263  const implies_exprt a6(
264  equal_exprt(needle.length(), from_integer(0, index_type)),
265  equal_exprt(offset, from_index));
266  constraints.existential.push_back(a6);
267 
268  return {offset, std::move(constraints)};
269 }
270 
274 // NOLINTNEXTLINE
276 // NOLINTNEXTLINE
291 std::pair<exprt, string_constraintst> add_axioms_for_index_of(
292  symbol_generatort &fresh_symbol,
294  array_poolt &array_pool)
295 {
297  PRECONDITION(args.size() == 2 || args.size() == 3);
298  const array_string_exprt str = get_string_expr(array_pool, args[0]);
299  const exprt &c=args[1];
300  const typet &index_type = str.length().type();
301  const typet &char_type = str.content().type().subtype();
302  PRECONDITION(f.type() == index_type);
303  const exprt from_index =
304  args.size() == 2 ? from_integer(0, index_type) : args[2];
305 
306  if(c.type().id()==ID_unsignedbv || c.type().id()==ID_signedbv)
307  {
309  fresh_symbol, str, typecast_exprt(c, char_type), from_index);
310  }
311  else
312  {
313  INVARIANT(
315  string_refinement_invariantt("c can only be a (un)signedbv or a refined "
316  "string and the (un)signedbv case is already handled"));
317  array_string_exprt sub = get_string_expr(array_pool, c);
318  return add_axioms_for_index_of_string(fresh_symbol, str, sub, from_index);
319  }
320 }
321 
346 std::pair<exprt, string_constraintst> add_axioms_for_last_index_of(
347  symbol_generatort &fresh_symbol,
348  const array_string_exprt &str,
349  const exprt &c,
350  const exprt &from_index)
351 {
352  string_constraintst constraints;
353  const typet &index_type = str.length().type();
354  const symbol_exprt index = fresh_symbol("last_index_of", index_type);
355  const symbol_exprt contains = fresh_symbol("contains_in_last_index_of");
356 
357  const exprt minus1 = from_integer(-1, index_type);
358  const and_exprt a1(
359  binary_relation_exprt(index, ID_ge, minus1),
360  binary_relation_exprt(index, ID_le, from_index),
361  binary_relation_exprt(index, ID_lt, str.length()));
362  constraints.existential.push_back(a1);
363 
364  const notequal_exprt a2(contains, equal_exprt(index, minus1));
365  constraints.existential.push_back(a2);
366 
367  const implies_exprt a3(contains, equal_exprt(str[index], c));
368  constraints.existential.push_back(a3);
369 
370  const exprt index1 = from_integer(1, index_type);
371  const plus_exprt from_index_plus_one(from_index, index1);
372  const if_exprt end_index(
373  binary_relation_exprt(from_index_plus_one, ID_le, str.length()),
374  from_index_plus_one,
375  str.length());
376 
377  const symbol_exprt n = fresh_symbol("QA_last_index_of1", index_type);
378  const string_constraintt a4(
379  n,
380  zero_if_negative(plus_exprt(index, index1)),
381  zero_if_negative(end_index),
382  implies_exprt(contains, notequal_exprt(str[n], c)));
383  constraints.universal.push_back(a4);
384 
385  const symbol_exprt m = fresh_symbol("QA_last_index_of2", index_type);
386  const string_constraintt a5(
387  m,
388  zero_if_negative(end_index),
389  implies_exprt(not_exprt(contains), notequal_exprt(str[m], c)));
390  constraints.universal.push_back(a5);
391 
392  return {index, std::move(constraints)};
393 }
394 
398 // NOLINTNEXTLINE
400 // NOLINTNEXTLINE
415 std::pair<exprt, string_constraintst> add_axioms_for_last_index_of(
416  symbol_generatort &fresh_symbol,
418  array_poolt &array_pool)
419 {
421  PRECONDITION(args.size() == 2 || args.size() == 3);
422  const array_string_exprt str = get_string_expr(array_pool, args[0]);
423  const exprt c = args[1];
424  const typet &index_type = str.length().type();
425  const typet &char_type = str.content().type().subtype();
426  PRECONDITION(f.type() == index_type);
427 
428  const exprt from_index = args.size() == 2 ? str.length() : args[2];
429 
430  if(c.type().id()==ID_unsignedbv || c.type().id()==ID_signedbv)
431  {
433  fresh_symbol, str, typecast_exprt(c, char_type), from_index);
434  }
435  else
436  {
437  const array_string_exprt sub = get_string_expr(array_pool, c);
439  fresh_symbol, str, sub, from_index);
440  }
441 }
The type of an expression, extends irept.
Definition: type.h:27
Boolean negation.
Definition: std_expr.h:3308
Semantic type conversion.
Definition: std_expr.h:2277
Generates string constraints to link results from string functions with their arguments.
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:878
Application of (mathematical) function.
Definition: std_expr.h:4481
Generation of fresh symbols of a given type.
argumentst & arguments()
Definition: std_expr.h:4506
std::pair< exprt, string_constraintst > add_axioms_for_index_of_string(symbol_generatort &fresh_symbol, 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...
The trinary if-then-else operator.
Definition: std_expr.h:3427
typet & type()
Return the type of the expression.
Definition: expr.h:68
Correspondance between arrays and pointers string representations.
Collection of constraints of different types: existential formulas, universal formulas, and "not contains" (universal with one alternation).
Boolean implication.
Definition: std_expr.h:2485
std::pair< exprt, string_constraintst > add_axioms_for_last_index_of_string(symbol_generatort &fresh_symbol, 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...
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function &#39;invariant_violated_string&#39;.
Definition: invariant.h:400
Equality.
Definition: std_expr.h:1484
const irep_idt & id() const
Definition: irep.h:259
array_string_exprt get_string_expr(array_poolt &pool, const exprt &expr)
casts an expression to a string expression, or fetches the actual string_exprt in the case of a symbo...
Constraints to encode non containement of strings.
Boolean AND.
Definition: std_expr.h:2409
std::vector< string_not_contains_constraintt > not_contains
Disequality.
Definition: std_expr.h:1545
exprt::operandst argumentst
Definition: std_expr.h:4484
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
bitvector_typet index_type()
Definition: c_types.cpp:16
std::pair< exprt, string_constraintst > add_axioms_for_last_index_of(symbol_generatort &fresh_symbol, 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::vector< exprt > existential
exprt & length()
Definition: string_expr.h:70
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
Base class for all expressions.
Definition: expr.h:54
bool is_refined_string_type(const typet &type)
std::vector< string_constraintt > universal
#define string_refinement_invariantt(reason)
Universally quantified string constraint
std::pair< exprt, string_constraintst > add_axioms_for_index_of(symbol_generatort &fresh_symbol, 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...
Binary minus.
Definition: std_expr.h:1106
Expression to hold a symbol (variable)
Definition: std_expr.h:143
const typet & subtype() const
Definition: type.h:38
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bitvector_typet char_type()
Definition: c_types.cpp:114