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 
22  const string_exprt &str, const exprt &c, const exprt &from_index)
23 {
24  const typet &index_type=str.length().type();
25  symbol_exprt index=fresh_exist_index("index_of", index_type);
26  symbol_exprt contains=fresh_boolean("contains_in_index_of");
27 
28  // We add axioms:
29  // a1 : -1 <= index<|str|
30  // a2 : !contains <=> index=-1
31  // a3 : contains => from_index<=index&&str[index]=c
32  // a4 : forall n, from_index<=n<index. contains => str[n]!=c
33  // a5 : forall m, from_index<=n<|str|. !contains => str[m]!=c
34 
35  exprt minus1=from_integer(-1, index_type);
36  and_exprt a1(
37  binary_relation_exprt(index, ID_ge, minus1),
38  binary_relation_exprt(index, ID_lt, str.length()));
39  axioms.push_back(a1);
40 
41  equal_exprt a2(not_exprt(contains), equal_exprt(index, minus1));
42  axioms.push_back(a2);
43 
44  implies_exprt a3(
45  contains,
46  and_exprt(
47  binary_relation_exprt(from_index, ID_le, index),
48  equal_exprt(str[index], c)));
49  axioms.push_back(a3);
50 
51  symbol_exprt n=fresh_univ_index("QA_index_of", index_type);
53  n, from_index, index, contains, not_exprt(equal_exprt(str[n], c)));
54  axioms.push_back(a4);
55 
56  symbol_exprt m=fresh_univ_index("QA_index_of", index_type);
58  m,
59  from_index,
60  str.length(),
61  not_exprt(contains),
62  not_exprt(equal_exprt(str[m], c)));
63  axioms.push_back(a5);
64 
65  return index;
66 }
67 
73  const string_exprt &str,
74  const string_exprt &substring,
75  const exprt &from_index)
76 {
77  const typet &index_type=str.length().type();
78  symbol_exprt offset=fresh_exist_index("index_of", index_type);
79  symbol_exprt contains=fresh_boolean("contains_substring");
80 
81  // We add axioms:
82  // a1 : contains => |substring|>=offset>=from_index
83  // a2 : !contains => offset=-1
84  // a3 : forall 0 <= witness<substring.length.
85  // contains => str[witness+offset]=substring[witness]
86 
87  implies_exprt a1(
88  contains,
89  and_exprt(
90  str.axiom_for_is_longer_than(plus_exprt(substring.length(), offset)),
91  binary_relation_exprt(offset, ID_ge, from_index)));
92  axioms.push_back(a1);
93 
94  implies_exprt a2(
95  not_exprt(contains),
96  equal_exprt(offset, from_integer(-1, index_type)));
97  axioms.push_back(a2);
98 
99  symbol_exprt qvar=fresh_univ_index("QA_index_of_string", index_type);
101  qvar,
102  substring.length(),
103  contains,
104  equal_exprt(str[plus_exprt(qvar, offset)], substring[qvar]));
105  axioms.push_back(a3);
106 
107  return offset;
108 }
109 
111  const string_exprt &str,
112  const string_exprt &substring,
113  const exprt &from_index)
114 {
115  const typet &index_type=str.length().type();
116  symbol_exprt offset=fresh_exist_index("index_of", index_type);
117  symbol_exprt contains=fresh_boolean("contains_substring");
118 
119  // We add axioms:
120  // a1 : contains => |substring| >= length &&offset <= from_index
121  // a2 : !contains => offset=-1
122  // a3 : forall 0 <= witness<substring.length,
123  // contains => str[witness+offset]=substring[witness]
124 
125  implies_exprt a1(
126  contains,
127  and_exprt(
128  str.axiom_for_is_longer_than(plus_exprt(substring.length(), offset)),
129  binary_relation_exprt(offset, ID_le, from_index)));
130  axioms.push_back(a1);
131 
132  implies_exprt a2(
133  not_exprt(contains),
134  equal_exprt(offset, from_integer(-1, index_type)));
135  axioms.push_back(a2);
136 
137  symbol_exprt qvar=fresh_univ_index("QA_index_of_string", index_type);
138  equal_exprt constr3(str[plus_exprt(qvar, offset)], substring[qvar]);
139  string_constraintt a3(qvar, substring.length(), contains, constr3);
140  axioms.push_back(a3);
141 
142  return offset;
143 }
144 
151 {
154  const exprt &c=args[1];
155  const refined_string_typet &ref_type=to_refined_string_type(str.type());
156  assert(f.type()==ref_type.get_index_type());
157  exprt from_index;
158 
159  if(args.size()==2)
160  from_index=from_integer(0, ref_type.get_index_type());
161  else if(args.size()==3)
162  from_index=args[2];
163  else
164  assert(false);
165 
167  {
169  return add_axioms_for_index_of_string(str, sub, from_index);
170  }
171  else
173  str, typecast_exprt(c, ref_type.get_char_type()), from_index);
174 }
175 
177  const string_exprt &str, const exprt &c, const exprt &from_index)
178 {
179  const refined_string_typet &ref_type=to_refined_string_type(str.type());
180  const typet &index_type=ref_type.get_index_type();
181  symbol_exprt index=fresh_exist_index("last_index_of", index_type);
182  symbol_exprt contains=fresh_boolean("contains_in_last_index_of");
183 
184  // We add axioms:
185  // a1 : -1 <= i <= from_index
186  // a2 : (i=-1 <=> !contains)
187  // a3 : (contains => i <= from_index &&s[i]=c)
188  // a4 : forall n. i+1 <= n < from_index +1 &&contains => s[n]!=c
189  // a5 : forall m. 0 <= m < from_index +1 &&!contains => s[m]!=c
190 
191  exprt index1=from_integer(1, index_type);
192  exprt minus1=from_integer(-1, index_type);
193  exprt from_index_plus_one=plus_exprt(from_index, index1);
194  and_exprt a1(
195  binary_relation_exprt(index, ID_ge, minus1),
196  binary_relation_exprt(index, ID_lt, from_index_plus_one));
197  axioms.push_back(a1);
198 
199  equal_exprt a2(not_exprt(contains), equal_exprt(index, minus1));
200  axioms.push_back(a2);
201 
202  implies_exprt a3(
203  contains,
204  and_exprt(
205  binary_relation_exprt(from_index, ID_ge, index),
206  equal_exprt(str[index], c)));
207  axioms.push_back(a3);
208 
209  symbol_exprt n=fresh_univ_index("QA_last_index_of", index_type);
211  n,
212  plus_exprt(index, index1),
213  from_index_plus_one,
214  contains,
215  not_exprt(equal_exprt(str[n], c)));
216  axioms.push_back(a4);
217 
218  symbol_exprt m=fresh_univ_index("QA_last_index_of", index_type);
220  m,
221  from_index_plus_one,
222  not_exprt(contains),
223  not_exprt(equal_exprt(str[m], c)));
224  axioms.push_back(a5);
225 
226  return index;
227 }
228 
236 {
239  exprt c=args[1];
240  const refined_string_typet &ref_type=to_refined_string_type(str.type());
241  exprt from_index;
242  assert(f.type()==ref_type.get_index_type());
243 
244  if(args.size()==2)
245  from_index=minus_exprt(str.length(), from_integer(1, str.length().type()));
246  else if(args.size()==3)
247  from_index=args[2];
248  else
249  assert(false);
250 
252  {
254  return add_axioms_for_last_index_of_string(str, sub, from_index);
255  }
256  else
258  str, typecast_exprt(c, ref_type.get_char_type()), from_index);
259 }
The type of an expression.
Definition: type.h:20
Boolean negation.
Definition: std_expr.h:2648
semantic type conversion
Definition: std_expr.h:1725
Generates string constraints to link results from string functions with their arguments.
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:568
static bool is_java_string_pointer_type(const typet &type)
application of (mathematical) function
Definition: std_expr.h:3785
const typet & get_char_type() const
argumentst & arguments()
Definition: std_expr.h:3805
symbol_exprt fresh_univ_index(const irep_idt &prefix, const typet &type)
generate an index symbol to be used as an universaly quantified variable
typet & type()
Definition: expr.h:60
exprt add_axioms_for_last_index_of_string(const string_exprt &str, const string_exprt &substring, const exprt &from_index)
boolean implication
Definition: std_expr.h:1926
exprt add_axioms_for_index_of(const string_exprt &str, const exprt &c, const exprt &from_index)
add axioms that the returned value is either -1 or greater than from_index and the character at that ...
exprt add_axioms_for_last_index_of(const string_exprt &str, const exprt &c, const exprt &from_index)
equality
Definition: std_expr.h:1082
symbol_exprt fresh_boolean(const irep_idt &prefix)
generate a Boolean symbol which is existentially quantified
const exprt & length() const
Definition: string_expr.h:35
exprt::operandst argumentst
Definition: std_expr.h:3803
string_exprt add_axioms_for_string_expr(const exprt &expr)
obtain a refined string expression corresponding to string variable of string function call ...
const refined_string_typet & to_refined_string_type(const typet &type)
boolean AND
Definition: std_expr.h:1852
The plus expression.
Definition: std_expr.h:702
const typet & get_index_type() const
bitvector_typet index_type()
Definition: c_types.cpp:15
binary_relation_exprt axiom_for_is_longer_than(const string_exprt &rhs) const
Definition: string_expr.h:56
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:46
binary minus
Definition: std_expr.h:758
Expression to hold a symbol (variable)
Definition: std_expr.h:82
exprt add_axioms_for_index_of_string(const string_exprt &str, const string_exprt &substring, const exprt &from_index)
add axioms stating that the returned value is either -1 or greater than from_index and the string beg...
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
static const function_application_exprt::argumentst & args(const function_application_exprt &expr, size_t nb)