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 
37 std::pair<exprt, string_constraintst>
39  const array_string_exprt &str,
40  const exprt &c,
41  const exprt &from_index)
42 {
43  string_constraintst constraints;
44  const typet &index_type = str.length_type();
45  symbol_exprt index = fresh_symbol("index_of", index_type);
46  symbol_exprt contains = fresh_symbol("contains_in_index_of");
47 
48  exprt minus1 = from_integer(-1, index_type);
49  and_exprt a1(
50  binary_relation_exprt(index, ID_ge, minus1),
52  constraints.existential.push_back(a1);
53 
54  equal_exprt a2(not_exprt(contains), equal_exprt(index, minus1));
55  constraints.existential.push_back(a2);
56 
57  implies_exprt a3(
58  contains,
59  and_exprt(
60  binary_relation_exprt(from_index, ID_le, index),
61  equal_exprt(str[index], c)));
62  constraints.existential.push_back(a3);
63 
64  const exprt lower_bound(zero_if_negative(from_index));
65 
66  symbol_exprt n = fresh_symbol("QA_index_of", index_type);
68  n,
69  lower_bound,
70  zero_if_negative(index),
72  constraints.universal.push_back(a4);
73 
74  symbol_exprt m = fresh_symbol("QA_index_of", index_type);
76  m,
77  lower_bound,
80  constraints.universal.push_back(a5);
81 
82  return {index, std::move(constraints)};
83 }
84 
109 std::pair<exprt, string_constraintst>
111  const array_string_exprt &haystack,
112  const array_string_exprt &needle,
113  const exprt &from_index)
114 {
115  string_constraintst constraints;
116  const typet &index_type = haystack.length_type();
117  symbol_exprt offset = fresh_symbol("index_of", index_type);
118  symbol_exprt contains = fresh_symbol("contains_substring");
119 
120  implies_exprt a1(
121  contains,
122  and_exprt(
123  binary_relation_exprt(from_index, ID_le, offset),
125  offset,
126  ID_le,
127  minus_exprt(
129  array_pool.get_or_create_length(needle)))));
130  constraints.existential.push_back(a1);
131 
132  equal_exprt a2(
134  constraints.existential.push_back(a2);
135 
136  symbol_exprt qvar = fresh_symbol("QA_index_of_string", index_type);
138  qvar,
141  contains, equal_exprt(haystack[plus_exprt(qvar, offset)], needle[qvar])));
142  constraints.universal.push_back(a3);
143 
144  // string_not contains_constraintt are formulas of the form:
145  // forall x in [lb,ub[. p(x) => exists y in [lb,ub[. s1[x+y] != s2[y]
147  from_index,
148  offset,
149  contains,
152  haystack,
153  needle};
154  constraints.not_contains.push_back(a4);
155 
157  from_index,
158  plus_exprt( // Add 1 for inclusive upper bound.
159  minus_exprt(
166  haystack,
167  needle};
168  constraints.not_contains.push_back(a5);
169 
170  const implies_exprt a6(
171  equal_exprt(
173  equal_exprt(offset, from_index));
174  constraints.existential.push_back(a6);
175 
176  return {offset, std::move(constraints)};
177 }
178 
209 std::pair<exprt, string_constraintst>
211  const array_string_exprt &haystack,
212  const array_string_exprt &needle,
213  const exprt &from_index)
214 {
215  string_constraintst constraints;
216  const typet &index_type = haystack.length_type();
217  symbol_exprt offset = fresh_symbol("index_of", index_type);
218  symbol_exprt contains = fresh_symbol("contains_substring");
219 
220  implies_exprt a1(
221  contains,
222  and_exprt(
223  binary_relation_exprt(from_integer(-1, index_type), ID_le, offset),
225  offset,
226  ID_le,
227  minus_exprt(
230  binary_relation_exprt(offset, ID_le, from_index)));
231  constraints.existential.push_back(a1);
232 
233  equal_exprt a2(
235  constraints.existential.push_back(a2);
236 
237  symbol_exprt qvar = fresh_symbol("QA_index_of_string", index_type);
238  equal_exprt constr3(haystack[plus_exprt(qvar, offset)], needle[qvar]);
239  const string_constraintt a3(
240  qvar,
242  implies_exprt(contains, constr3));
243  constraints.universal.push_back(a3);
244 
245  // end_index is min(from_index, |str| - |substring|)
246  minus_exprt length_diff(
249  if_exprt end_index(
250  binary_relation_exprt(from_index, ID_le, length_diff),
251  from_index,
252  length_diff);
253 
255  plus_exprt(offset, from_integer(1, index_type)),
256  plus_exprt(end_index, from_integer(1, index_type)),
257  contains,
260  haystack,
261  needle};
262  constraints.not_contains.push_back(a4);
263 
266  plus_exprt(end_index, from_integer(1, index_type)),
270  haystack,
271  needle};
272  constraints.not_contains.push_back(a5);
273 
274  const implies_exprt a6(
275  equal_exprt(
277  equal_exprt(offset, from_index));
278  constraints.existential.push_back(a6);
279 
280  return {offset, std::move(constraints)};
281 }
282 
286 // NOLINTNEXTLINE
288 // NOLINTNEXTLINE
301 std::pair<exprt, string_constraintst>
304 {
306  PRECONDITION(args.size() == 2 || args.size() == 3);
307  const array_string_exprt str = get_string_expr(array_pool, args[0]);
308  const exprt &c = args[1];
309  const typet &index_type = str.length_type();
310  const typet &char_type = str.content().type().subtype();
311  PRECONDITION(f.type() == index_type);
312  const exprt from_index =
313  args.size() == 2 ? from_integer(0, index_type) : args[2];
314 
315  if(c.type().id() == ID_unsignedbv || c.type().id() == ID_signedbv)
316  {
318  str, typecast_exprt(c, char_type), from_index);
319  }
320  else
321  {
322  INVARIANT(
325  "c can only be a (un)signedbv or a refined "
326  "string and the (un)signedbv case is already handled"));
328  return add_axioms_for_index_of_string(str, sub, from_index);
329  }
330 }
331 
355 std::pair<exprt, string_constraintst>
357  const array_string_exprt &str,
358  const exprt &c,
359  const exprt &from_index)
360 {
361  string_constraintst constraints;
362  const typet &index_type = str.length_type();
363  const symbol_exprt index = fresh_symbol("last_index_of", index_type);
364  const symbol_exprt contains = fresh_symbol("contains_in_last_index_of");
365 
366  const exprt minus1 = from_integer(-1, index_type);
367  const and_exprt a1(
368  binary_relation_exprt(index, ID_ge, minus1),
369  binary_relation_exprt(index, ID_le, from_index),
371  constraints.existential.push_back(a1);
372 
373  const notequal_exprt a2(contains, equal_exprt(index, minus1));
374  constraints.existential.push_back(a2);
375 
376  const implies_exprt a3(contains, equal_exprt(str[index], c));
377  constraints.existential.push_back(a3);
378 
379  const exprt index1 = from_integer(1, index_type);
380  const plus_exprt from_index_plus_one(from_index, index1);
381  const if_exprt end_index(
383  from_index_plus_one, ID_le, array_pool.get_or_create_length(str)),
384  from_index_plus_one,
386 
387  const symbol_exprt n = fresh_symbol("QA_last_index_of1", index_type);
388  const string_constraintt a4(
389  n,
390  zero_if_negative(plus_exprt(index, index1)),
391  zero_if_negative(end_index),
392  implies_exprt(contains, notequal_exprt(str[n], c)));
393  constraints.universal.push_back(a4);
394 
395  const symbol_exprt m = fresh_symbol("QA_last_index_of2", index_type);
396  const string_constraintt a5(
397  m,
398  zero_if_negative(end_index),
400  constraints.universal.push_back(a5);
401 
402  return {index, std::move(constraints)};
403 }
404 
408 // NOLINTNEXTLINE
410 // NOLINTNEXTLINE
423 std::pair<exprt, string_constraintst>
426 {
428  PRECONDITION(args.size() == 2 || args.size() == 3);
429  const array_string_exprt str = get_string_expr(array_pool, args[0]);
430  const exprt c = args[1];
431  const typet &index_type = str.length_type();
432  const typet &char_type = str.content().type().subtype();
433  PRECONDITION(f.type() == index_type);
434 
435  const exprt from_index =
436  args.size() == 2 ? array_pool.get_or_create_length(str) : args[2];
437 
438  if(c.type().id() == ID_unsignedbv || c.type().id() == ID_signedbv)
439  {
441  str, typecast_exprt(c, char_type), from_index);
442  }
443  else
444  {
446  return add_axioms_for_last_index_of_string(str, sub, from_index);
447  }
448 }
function_application_exprt::arguments
argumentst & arguments()
Definition: mathematical_expr.h:221
array_string_exprt::length_type
const typet & length_type() const
Definition: string_expr.h:69
typet::subtype
const typet & subtype() const
Definition: type.h:47
string_constraint_generatort::add_axioms_for_index_of
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...
Definition: string_constraint_generator_indexof.cpp:38
exprt::size
std::size_t size() const
Amount of nodes this expression tree contains.
Definition: expr.cpp:26
typet
The type of an expression, extends irept.
Definition: type.h:29
string_constraintt
Definition: string_constraint.h:60
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
string_constraint_generatort::fresh_symbol
symbol_generatort fresh_symbol
Definition: string_constraint_generator.h:56
and_exprt
Boolean AND.
Definition: std_expr.h:2137
array_poolt::get_or_create_length
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:24
get_string_expr
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:196
string_refinement_invariant.h
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:881
exprt
Base class for all expressions.
Definition: expr.h:53
string_constraintst
Collection of constraints of different types: existential formulas, universal formulas,...
Definition: string_constraint_generator.h:36
array_string_exprt::content
exprt & content()
Definition: string_expr.h:74
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
equal_exprt
Equality.
Definition: std_expr.h:1190
function_application_exprt::argumentst
exprt::operandst argumentst
Definition: mathematical_expr.h:193
string_constraint_generatort::array_pool
array_poolt array_pool
Definition: string_constraint_generator.h:58
notequal_exprt
Disequality.
Definition: std_expr.h:1248
string_constraint_generatort::add_axioms_for_last_index_of_string
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...
Definition: string_constraint_generator_indexof.cpp:210
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
function_application_exprt
Application of (mathematical) function.
Definition: mathematical_expr.h:191
irept::id
const irep_idt & id() const
Definition: irep.h:418
string_constraint_generatort::add_axioms_for_last_index_of
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 ...
Definition: string_constraint_generator_indexof.cpp:356
minus_exprt
Binary minus.
Definition: std_expr.h:940
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
string_refinement_invariantt
#define string_refinement_invariantt(reason)
Definition: string_refinement_invariant.h:12
zero_if_negative
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
Definition: string_constraint_generator_main.cpp:408
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:725
is_refined_string_type
bool is_refined_string_type(const typet &type)
Definition: refined_string_type.h:52
contains
static bool contains(const exprt &index, const symbol_exprt &qvar)
Look for symbol qvar in the expression index and return true if found.
Definition: string_constraint_instantiation.cpp:19
string_constraintst::not_contains
std::vector< string_not_contains_constraintt > not_contains
Definition: string_constraint_generator.h:39
implies_exprt
Boolean implication.
Definition: std_expr.h:2200
string_not_contains_constraintt
Constraints to encode non containement of strings.
Definition: string_constraint.h:127
string_constraint_generatort::add_axioms_for_index_of_string
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...
Definition: string_constraint_generator_indexof.cpp:110
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
string_constraint_generator.h
Generates string constraints to link results from string functions with their arguments.
array_string_exprt
Definition: string_expr.h:67
validation_modet::INVARIANT
@ INVARIANT
string_constraintst::existential
std::vector< exprt > existential
Definition: string_constraint_generator.h:37
not_exprt
Boolean negation.
Definition: std_expr.h:2843
string_constraintst::universal
std::vector< string_constraintt > universal
Definition: string_constraint_generator.h:38