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 exprt lower_bound(zero_if_negative(from_index));
63 
64  symbol_exprt n=fresh_univ_index("QA_index_of", index_type);
66  n,
67  lower_bound,
68  zero_if_negative(index),
69  implies_exprt(contains, notequal_exprt(str[n], c)));
70  constraints.push_back(a4);
71 
72  symbol_exprt m=fresh_univ_index("QA_index_of", index_type);
74  m,
75  lower_bound,
76  zero_if_negative(str.length()),
77  implies_exprt(not_exprt(contains), not_exprt(equal_exprt(str[m], c))));
78  constraints.push_back(a5);
79 
80  return index;
81 }
82 
108  const array_string_exprt &haystack,
109  const array_string_exprt &needle,
110  const exprt &from_index)
111 {
112  const typet &index_type=haystack.length().type();
113  symbol_exprt offset=fresh_exist_index("index_of", index_type);
114  symbol_exprt contains=fresh_boolean("contains_substring");
115 
116  implies_exprt a1(
117  contains,
118  and_exprt(
119  binary_relation_exprt(from_index, ID_le, offset),
121  offset, ID_le, minus_exprt(haystack.length(), needle.length()))));
122  lemmas.push_back(a1);
123 
124  equal_exprt a2(
125  not_exprt(contains),
126  equal_exprt(offset, from_integer(-1, index_type)));
127  lemmas.push_back(a2);
128 
129  symbol_exprt qvar=fresh_univ_index("QA_index_of_string", index_type);
131  qvar,
132  zero_if_negative(needle.length()),
134  contains, equal_exprt(haystack[plus_exprt(qvar, offset)], needle[qvar])));
135  constraints.push_back(a3);
136 
137  // string_not contains_constraintt are formulas of the form:
138  // forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s1[x+y] != s2[y]
140  from_index,
141  offset,
142  contains,
144  needle.length(),
145  haystack,
146  needle);
147  not_contains_constraints.push_back(a4);
148 
150  from_index,
151  plus_exprt( // Add 1 for inclusive upper bound.
152  minus_exprt(haystack.length(), needle.length()),
154  not_exprt(contains),
156  needle.length(),
157  haystack,
158  needle);
159  not_contains_constraints.push_back(a5);
160 
161  const implies_exprt a6(
162  equal_exprt(needle.length(), from_integer(0, index_type)),
163  equal_exprt(offset, from_index));
164  lemmas.push_back(a6);
165 
166  return offset;
167 }
168 
200  const array_string_exprt &haystack,
201  const array_string_exprt &needle,
202  const exprt &from_index)
203 {
204  const typet &index_type=haystack.length().type();
205  symbol_exprt offset=fresh_exist_index("index_of", index_type);
206  symbol_exprt contains=fresh_boolean("contains_substring");
207 
208  implies_exprt a1(
209  contains,
210  and_exprt(
211  binary_relation_exprt(from_integer(-1, index_type), ID_le, offset),
213  offset, ID_le, minus_exprt(haystack.length(), needle.length())),
214  binary_relation_exprt(offset, ID_le, from_index)));
215  lemmas.push_back(a1);
216 
217  equal_exprt a2(
218  not_exprt(contains),
219  equal_exprt(offset, from_integer(-1, index_type)));
220  lemmas.push_back(a2);
221 
222  symbol_exprt qvar=fresh_univ_index("QA_index_of_string", index_type);
223  equal_exprt constr3(haystack[plus_exprt(qvar, offset)], needle[qvar]);
224  const string_constraintt a3(
225  qvar, zero_if_negative(needle.length()), implies_exprt(contains, constr3));
226  constraints.push_back(a3);
227 
228  // end_index is min(from_index, |str| - |substring|)
229  minus_exprt length_diff(haystack.length(), needle.length());
230  if_exprt end_index(
231  binary_relation_exprt(from_index, ID_le, length_diff),
232  from_index,
233  length_diff);
234 
236  plus_exprt(offset, from_integer(1, index_type)),
237  plus_exprt(end_index, from_integer(1, index_type)),
238  contains,
240  needle.length(),
241  haystack,
242  needle);
243  not_contains_constraints.push_back(a4);
244 
247  plus_exprt(end_index, from_integer(1, index_type)),
248  not_exprt(contains),
250  needle.length(),
251  haystack,
252  needle);
253  not_contains_constraints.push_back(a5);
254 
255  const implies_exprt a6(
256  equal_exprt(needle.length(), from_integer(0, index_type)),
257  equal_exprt(offset, from_index));
258  lemmas.push_back(a6);
259 
260  return offset;
261 }
262 
266 // NOLINTNEXTLINE
283 {
285  PRECONDITION(args.size() == 2 || args.size() == 3);
286  const array_string_exprt str = get_string_expr(args[0]);
287  const exprt &c=args[1];
288  const typet &index_type = str.length().type();
289  const typet &char_type = str.content().type().subtype();
290  PRECONDITION(f.type() == index_type);
291  const exprt from_index =
292  args.size() == 2 ? from_integer(0, index_type) : args[2];
293 
294  if(c.type().id()==ID_unsignedbv || c.type().id()==ID_signedbv)
295  {
297  str, typecast_exprt(c, char_type), from_index);
298  }
299  else
300  {
301  INVARIANT(
303  string_refinement_invariantt("c can only be a (un)signedbv or a refined "
304  "string and the (un)signedbv case is already handled"));
306  return add_axioms_for_index_of_string(str, sub, from_index);
307  }
308 }
309 
334  const array_string_exprt &str,
335  const exprt &c,
336  const exprt &from_index)
337 {
338  const typet &index_type = str.length().type();
339  const symbol_exprt index = fresh_exist_index("last_index_of", index_type);
340  const symbol_exprt contains = fresh_boolean("contains_in_last_index_of");
341 
342  const exprt minus1 = from_integer(-1, index_type);
343  const and_exprt a1(
344  binary_relation_exprt(index, ID_ge, minus1),
345  binary_relation_exprt(index, ID_le, from_index),
346  binary_relation_exprt(index, ID_lt, str.length()));
347  lemmas.push_back(a1);
348 
349  const notequal_exprt a2(contains, equal_exprt(index, minus1));
350  lemmas.push_back(a2);
351 
352  const implies_exprt a3(contains, equal_exprt(str[index], c));
353  lemmas.push_back(a3);
354 
355  const exprt index1 = from_integer(1, index_type);
356  const plus_exprt from_index_plus_one(from_index, index1);
357  const if_exprt end_index(
358  binary_relation_exprt(from_index_plus_one, ID_le, str.length()),
359  from_index_plus_one,
360  str.length());
361 
362  const symbol_exprt n = fresh_univ_index("QA_last_index_of1", index_type);
363  const string_constraintt a4(
364  n,
365  zero_if_negative(plus_exprt(index, index1)),
366  zero_if_negative(end_index),
367  implies_exprt(contains, notequal_exprt(str[n], c)));
368  constraints.push_back(a4);
369 
370  const symbol_exprt m = fresh_univ_index("QA_last_index_of2", index_type);
371  const string_constraintt a5(
372  m,
373  zero_if_negative(end_index),
374  implies_exprt(not_exprt(contains), notequal_exprt(str[m], c)));
375  constraints.push_back(a5);
376 
377  return index;
378 }
379 
383 // NOLINTNEXTLINE
385 // NOLINTNEXTLINE
400 {
402  PRECONDITION(args.size() == 2 || args.size() == 3);
403  const array_string_exprt str = get_string_expr(args[0]);
404  const exprt c = args[1];
405  const typet &index_type = str.length().type();
406  const typet &char_type = str.content().type().subtype();
407  PRECONDITION(f.type() == index_type);
408 
409  const exprt from_index = args.size() == 2 ? str.length() : args[2];
410 
411  if(c.type().id()==ID_unsignedbv || c.type().id()==ID_signedbv)
412  {
414  str, typecast_exprt(c, char_type), from_index);
415  }
416  else
417  {
418  const array_string_exprt sub = get_string_expr(c);
419  return add_axioms_for_last_index_of_string(str, sub, from_index);
420  }
421 }
The type of an expression.
Definition: type.h:22
Boolean negation.
Definition: std_expr.h:3228
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:4529
argumentst & arguments()
Definition: std_expr.h:4562
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:3359
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:204
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:259
Constraints to encode non containement of strings.
exprt::operandst argumentst
Definition: std_expr.h:4560
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:242
The plus expression.
Definition: std_expr.h:893
bitvector_typet index_type()
Definition: c_types.cpp:16
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
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
exprt add_axioms_for_index_of(const function_application_exprt &f)
Index of the first occurence of a target inside the string.
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 ...