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  const array_string_exprt &str,
39  const exprt &c,
40  const exprt &from_index)
41 {
42  const typet &index_type=str.length().type();
43  symbol_exprt index=fresh_exist_index("index_of", index_type);
44  symbol_exprt contains=fresh_boolean("contains_in_index_of");
45 
46  exprt minus1=from_integer(-1, index_type);
47  and_exprt a1(
48  binary_relation_exprt(index, ID_ge, minus1),
49  binary_relation_exprt(index, ID_lt, str.length()));
50  lemmas.push_back(a1);
51 
52  equal_exprt a2(not_exprt(contains), equal_exprt(index, minus1));
53  lemmas.push_back(a2);
54 
55  implies_exprt a3(
56  contains,
57  and_exprt(
58  binary_relation_exprt(from_index, ID_le, index),
59  equal_exprt(str[index], c)));
60  lemmas.push_back(a3);
61 
62  const auto zero = from_integer(0, index_type);
63  const if_exprt lower_bound(
64  binary_relation_exprt(from_index, ID_le, zero), zero, from_index);
65 
66  symbol_exprt n=fresh_univ_index("QA_index_of", index_type);
68  n, lower_bound, index, implies_exprt(contains, notequal_exprt(str[n], c)));
69  constraints.push_back(a4);
70 
71  symbol_exprt m=fresh_univ_index("QA_index_of", index_type);
73  m,
74  lower_bound,
75  str.length(),
76  implies_exprt(not_exprt(contains), not_exprt(equal_exprt(str[m], c))));
77  constraints.push_back(a5);
78 
79  return index;
80 }
81 
107  const array_string_exprt &haystack,
108  const array_string_exprt &needle,
109  const exprt &from_index)
110 {
111  const typet &index_type=haystack.length().type();
112  symbol_exprt offset=fresh_exist_index("index_of", index_type);
113  symbol_exprt contains=fresh_boolean("contains_substring");
114 
115  implies_exprt a1(
116  contains,
117  and_exprt(
118  binary_relation_exprt(from_index, ID_le, offset),
120  offset, ID_le, minus_exprt(haystack.length(), needle.length()))));
121  lemmas.push_back(a1);
122 
123  equal_exprt a2(
124  not_exprt(contains),
125  equal_exprt(offset, from_integer(-1, index_type)));
126  lemmas.push_back(a2);
127 
128  symbol_exprt qvar=fresh_univ_index("QA_index_of_string", index_type);
130  qvar,
131  needle.length(),
133  contains, equal_exprt(haystack[plus_exprt(qvar, offset)], needle[qvar])));
134  constraints.push_back(a3);
135 
136  // string_not contains_constraintt are formulas of the form:
137  // forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s1[x+y] != s2[y]
139  from_index,
140  offset,
141  contains,
143  needle.length(),
144  haystack,
145  needle);
146  not_contains_constraints.push_back(a4);
147 
149  from_index,
150  plus_exprt( // Add 1 for inclusive upper bound.
151  minus_exprt(haystack.length(), needle.length()),
153  not_exprt(contains),
155  needle.length(),
156  haystack,
157  needle);
158  not_contains_constraints.push_back(a5);
159 
160  const implies_exprt a6(
161  equal_exprt(needle.length(), from_integer(0, index_type)),
162  equal_exprt(offset, from_index));
163  lemmas.push_back(a6);
164 
165  return offset;
166 }
167 
199  const array_string_exprt &haystack,
200  const array_string_exprt &needle,
201  const exprt &from_index)
202 {
203  const typet &index_type=haystack.length().type();
204  symbol_exprt offset=fresh_exist_index("index_of", index_type);
205  symbol_exprt contains=fresh_boolean("contains_substring");
206 
207  implies_exprt a1(
208  contains,
209  and_exprt(
210  binary_relation_exprt(from_integer(-1, index_type), ID_le, offset),
212  offset, ID_le, minus_exprt(haystack.length(), needle.length())),
213  binary_relation_exprt(offset, ID_le, from_index)));
214  lemmas.push_back(a1);
215 
216  equal_exprt a2(
217  not_exprt(contains),
218  equal_exprt(offset, from_integer(-1, index_type)));
219  lemmas.push_back(a2);
220 
221  symbol_exprt qvar=fresh_univ_index("QA_index_of_string", index_type);
222  equal_exprt constr3(haystack[plus_exprt(qvar, offset)], needle[qvar]);
223  const string_constraintt a3(
224  qvar, needle.length(), implies_exprt(contains, constr3));
225  constraints.push_back(a3);
226 
227  // end_index is min(from_index, |str| - |substring|)
228  minus_exprt length_diff(haystack.length(), needle.length());
229  if_exprt end_index(
230  binary_relation_exprt(from_index, ID_le, length_diff),
231  from_index,
232  length_diff);
233 
235  plus_exprt(offset, from_integer(1, index_type)),
236  plus_exprt(end_index, from_integer(1, index_type)),
237  contains,
239  needle.length(),
240  haystack,
241  needle);
242  not_contains_constraints.push_back(a4);
243 
246  plus_exprt(end_index, from_integer(1, index_type)),
247  not_exprt(contains),
249  needle.length(),
250  haystack,
251  needle);
252  not_contains_constraints.push_back(a5);
253 
254  const implies_exprt a6(
255  equal_exprt(needle.length(), from_integer(0, index_type)),
256  equal_exprt(offset, from_index));
257  lemmas.push_back(a6);
258 
259  return offset;
260 }
261 
265 // NOLINTNEXTLINE
282 {
284  PRECONDITION(args.size() == 2 || args.size() == 3);
285  const array_string_exprt str = get_string_expr(args[0]);
286  const exprt &c=args[1];
287  const typet &index_type = str.length().type();
288  const typet &char_type = str.content().type().subtype();
289  PRECONDITION(f.type() == index_type);
290  const exprt from_index =
291  args.size() == 2 ? from_integer(0, index_type) : args[2];
292 
293  if(c.type().id()==ID_unsignedbv || c.type().id()==ID_signedbv)
294  {
296  str, typecast_exprt(c, char_type), from_index);
297  }
298  else
299  {
300  INVARIANT(
302  string_refinement_invariantt("c can only be a (un)signedbv or a refined "
303  "string and the (un)signedbv case is already handled"));
305  return add_axioms_for_index_of_string(str, sub, from_index);
306  }
307 }
308 
333  const array_string_exprt &str,
334  const exprt &c,
335  const exprt &from_index)
336 {
337  const typet &index_type = str.length().type();
338  const symbol_exprt index = fresh_exist_index("last_index_of", index_type);
339  const symbol_exprt contains = fresh_boolean("contains_in_last_index_of");
340 
341  const exprt minus1 = from_integer(-1, index_type);
342  const and_exprt a1(
343  binary_relation_exprt(index, ID_ge, minus1),
344  binary_relation_exprt(index, ID_le, from_index),
345  binary_relation_exprt(index, ID_lt, str.length()));
346  lemmas.push_back(a1);
347 
348  const notequal_exprt a2(contains, equal_exprt(index, minus1));
349  lemmas.push_back(a2);
350 
351  const implies_exprt a3(contains, equal_exprt(str[index], c));
352  lemmas.push_back(a3);
353 
354  const exprt index1 = from_integer(1, index_type);
355  const plus_exprt from_index_plus_one(from_index, index1);
356  const if_exprt end_index(
357  binary_relation_exprt(from_index_plus_one, ID_le, str.length()),
358  from_index_plus_one,
359  str.length());
360 
361  const symbol_exprt n = fresh_univ_index("QA_last_index_of1", index_type);
362  const string_constraintt a4(
363  n,
364  plus_exprt(index, index1),
365  end_index,
366  implies_exprt(contains, notequal_exprt(str[n], c)));
367  constraints.push_back(a4);
368 
369  const symbol_exprt m = fresh_univ_index("QA_last_index_of2", index_type);
370  const string_constraintt a5(
371  m,
372  end_index,
373  implies_exprt(not_exprt(contains), notequal_exprt(str[m], c)));
374  constraints.push_back(a5);
375 
376  return index;
377 }
378 
382 // NOLINTNEXTLINE
384 // NOLINTNEXTLINE
399 {
401  PRECONDITION(args.size() == 2 || args.size() == 3);
402  const array_string_exprt str = get_string_expr(args[0]);
403  const exprt c = args[1];
404  const typet &index_type = str.length().type();
405  const typet &char_type = str.content().type().subtype();
406  PRECONDITION(f.type() == index_type);
407 
408  const exprt from_index = args.size() == 2 ? str.length() : args[2];
409 
410  if(c.type().id()==ID_unsignedbv || c.type().id()==ID_signedbv)
411  {
413  str, typecast_exprt(c, char_type), from_index);
414  }
415  else
416  {
417  const array_string_exprt sub = get_string_expr(c);
418  return add_axioms_for_last_index_of_string(str, sub, from_index);
419  }
420 }
The type of an expression.
Definition: type.h:22
Boolean negation.
Definition: std_expr.h:3230
semantic type conversion
Definition: std_expr.h:2111
Generates string constraints to link results from string functions with their arguments.
std::vector< string_not_contains_constraintt > not_contains_constraints
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
application of (mathematical) function
Definition: std_expr.h:4531
argumentst & arguments()
Definition: std_expr.h:4564
symbol_exprt fresh_univ_index(const irep_idt &prefix, const typet &type)
generate an index symbol to be used as an universaly quantified variable
The trinary if-then-else operator.
Definition: std_expr.h:3361
typet & type()
Definition: expr.h:56
exprt 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...
boolean implication
Definition: std_expr.h:2339
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
equality
Definition: std_expr.h:1354
symbol_exprt fresh_boolean(const irep_idt &prefix)
generate a Boolean symbol which is existentially quantified
const irep_idt & id() const
Definition: irep.h:189
Constraints to encode non containement of strings.
exprt::operandst argumentst
Definition: std_expr.h:4562
exprt 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...
boolean AND
Definition: std_expr.h:2255
exprt 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...
inequality
Definition: std_expr.h:1406
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
The plus expression.
Definition: std_expr.h:893
bitvector_typet index_type()
Definition: c_types.cpp:16
symbol_exprt fresh_exist_index(const irep_idt &prefix, const typet &type)
generate an index symbol which is existentially quantified
Base class for all expressions.
Definition: expr.h:42
bool is_refined_string_type(const typet &type)
#define string_refinement_invariantt(reason)
Universally quantified string constraint
binary minus
Definition: std_expr.h:959
Expression to hold a symbol (variable)
Definition: std_expr.h:90
const typet & subtype() const
Definition: type.h:33
std::vector< string_constraintt > constraints
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bitvector_typet char_type()
Definition: c_types.cpp:114
array_string_exprt get_string_expr(const exprt &expr)
casts an expression to a string expression, or fetches the actual string_exprt in the case of a symbo...
exprt 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 ...