cprover
string_constraint_generator_comparison.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Generates string constraints for function comparing strings,
4  such as: equals, equalsIgnoreCase, compareTo, hashCode, intern
5 
6 Author: Romain Brenguier, romain.brenguier@diffblue.com
7 
8 \*******************************************************************/
9 
13 
15 
22 {
23  assert(f.type()==bool_typet() || f.type().id()==ID_c_bool);
24  symbol_exprt eq=fresh_boolean("equal");
25  typecast_exprt tc_eq(eq, f.type());
26 
29  typet index_type=s1.length().type();
30 
31  // We want to write:
32  // eq <=> (s1.length=s2.length &&forall i<s1.length. s1[i]=s2[i])
33  // We add axioms:
34  // a1 : eq => s1.length=s2.length
35  // a2 : forall i<s1.length. eq => s1[i]=s2[i]
36  // a3 : !eq => s1.length!=s2.length
37  // || (witness<s1.length &&s1[witness]!=s2[witness])
38 
39  implies_exprt a1(eq, s1.axiom_for_has_same_length_as(s2));
40  axioms.push_back(a1);
41 
42  symbol_exprt qvar=fresh_univ_index("QA_equal", index_type);
43  string_constraintt a2(qvar, s1.length(), eq, equal_exprt(s1[qvar], s2[qvar]));
44  axioms.push_back(a2);
45 
46  symbol_exprt witness=fresh_exist_index("witness_unequal", index_type);
47  exprt zero=from_integer(0, index_type);
48  and_exprt bound_witness(
49  binary_relation_exprt(witness, ID_lt, s1.length()),
50  binary_relation_exprt(witness, ID_ge, zero));
51  and_exprt witnessing(bound_witness, notequal_exprt(s1[witness], s2[witness]));
52  implies_exprt a3(
53  not_exprt(eq),
54  or_exprt(notequal_exprt(s1.length(), s2.length()), witnessing));
55  axioms.push_back(a3);
56 
57  return tc_eq;
58 }
59 
67  exprt char1, exprt char2, exprt char_a, exprt char_A, exprt char_Z)
68 {
69  and_exprt is_upper_case_1(
70  binary_relation_exprt(char_A, ID_le, char1),
71  binary_relation_exprt(char1, ID_le, char_Z));
72  and_exprt is_upper_case_2(
73  binary_relation_exprt(char_A, ID_le, char2),
74  binary_relation_exprt(char2, ID_le, char_Z));
75 
76  // Three possibilities:
77  // p1 : char1=char2
78  // p2 : (is_up1&&'a'-'A'+char1=char2)
79  // p3 : (is_up2&&'a'-'A'+char2=char1)
80  equal_exprt p1(char1, char2);
81  minus_exprt diff=minus_exprt(char_a, char_A);
82  and_exprt p2(is_upper_case_1, equal_exprt(plus_exprt(diff, char1), char2));
83  and_exprt p3(is_upper_case_2, equal_exprt(plus_exprt(diff, char2), char1));
84  return or_exprt(or_exprt(p1, p2), p3);
85 }
86 
92 {
93  assert(f.type()==bool_typet() || f.type().id()==ID_c_bool);
94 
95  symbol_exprt eq=fresh_boolean("equal_ignore_case");
96  typecast_exprt tc_eq(eq, f.type());
99  typet char_type=to_refined_string_type(s1.type()).get_char_type();
100  exprt char_a=constant_char('a', char_type);
101  exprt char_A=constant_char('A', char_type);
102  exprt char_Z=constant_char('Z', char_type);
103  typet index_type=s1.length().type();
104 
105  // We add axioms:
106  // a1 : eq => |s1|=|s2|
107  // a2 : forall qvar, 0<=qvar<|s1|,
108  // eq => char_equal_ignore_case(s1[qvar],s2[qvar]);
109  // a3 : !eq => |s1|!=s2 || (0 <=witness<|s1| &&!char_equal_ignore_case)
110 
111  implies_exprt a1(eq, s1.axiom_for_has_same_length_as(s2));
112  axioms.push_back(a1);
113 
114  symbol_exprt qvar=fresh_univ_index("QA_equal_ignore_case", index_type);
116  s1[qvar], s2[qvar], char_a, char_A, char_Z);
117  string_constraintt a2(qvar, s1.length(), eq, constr2);
118  axioms.push_back(a2);
119 
121  "witness_unequal_ignore_case", index_type);
122  exprt zero=from_integer(0, witness.type());
123  and_exprt bound_witness(
124  binary_relation_exprt(witness, ID_lt, s1.length()),
125  binary_relation_exprt(witness, ID_ge, zero));
127  s1[witness], s2[witness], char_a, char_A, char_Z);
128  not_exprt witness_diff(witness_eq);
129  implies_exprt a3(
130  not_exprt(eq),
131  or_exprt(
132  notequal_exprt(s1.length(), s2.length()),
133  and_exprt(bound_witness, witness_diff)));
134  axioms.push_back(a3);
135 
136  return tc_eq;
137 }
138 
145 {
147  typet return_type=f.type();
148  typet index_type=str.length().type();
149 
150  // initialisation of the missing pool variable
151  std::map<irep_idt, string_exprt>::iterator it;
152  for(it=symbol_to_string.begin(); it!=symbol_to_string.end(); it++)
153  if(hash.find(it->second)==hash.end())
154  hash[it->second]=fresh_symbol("hash", return_type);
155 
156  // for each string s. either:
157  // c1: hash(str)=hash(s)
158  // c2: |str|!=|s|
159  // c3: (|str|==|s| &&exists i<|s|. s[i]!=str[i])
160 
161  // WARNING: the specification may be incomplete
162  for(it=symbol_to_string.begin(); it!=symbol_to_string.end(); it++)
163  {
164  symbol_exprt i=fresh_exist_index("index_hash", index_type);
165  equal_exprt c1(hash[it->second], hash[str]);
166  not_exprt c2(equal_exprt(it->second.length(), str.length()));
167  and_exprt c3(
168  equal_exprt(it->second.length(), str.length()),
169  and_exprt(
170  not_exprt(equal_exprt(str[i], it->second[i])),
171  and_exprt(
172  str.axiom_for_is_strictly_longer_than(i),
174  axioms.push_back(or_exprt(c1, or_exprt(c2, c3)));
175  }
176  return hash[str];
177 }
178 
184 {
187  const typet &return_type=f.type();
188  symbol_exprt res=fresh_symbol("compare_to", return_type);
189  typet index_type=s1.length().type();
190 
191  // In the lexicographic comparison, x is the first point where the two
192  // strings differ.
193  // We add axioms:
194  // a1 : res==0 => |s1|=|s2|
195  // a2 : forall i<|s1|. s1[i]==s2[i]
196  // a3 : exists x.
197  // res!=0 ==> x> 0 &&
198  // ((|s1| <= |s2| &&x<|s1|) || (|s1| >= |s2| &&x<|s2|)
199  // &&res=s1[x]-s2[x] )
200  // || cond2:
201  // (|s1|<|s2| &&x=|s1|) || (|s1| > |s2| &&x=|s2|) &&res=|s1|-|s2|)
202  // a4 : forall i<x. res!=0 => s1[i]=s2[i]
203 
204  assert(return_type.id()==ID_signedbv);
205 
206  equal_exprt res_null=equal_exprt(res, from_integer(0, return_type));
207  implies_exprt a1(res_null, s1.axiom_for_has_same_length_as(s2));
208  axioms.push_back(a1);
209 
210  symbol_exprt i=fresh_univ_index("QA_compare_to", index_type);
211  string_constraintt a2(i, s1.length(), res_null, equal_exprt(s1[i], s2[i]));
212  axioms.push_back(a2);
213 
214  symbol_exprt x=fresh_exist_index("index_compare_to", index_type);
215  equal_exprt ret_char_diff(
216  res,
217  minus_exprt(
218  typecast_exprt(s1[x], return_type),
219  typecast_exprt(s2[x], return_type)));
220  equal_exprt ret_length_diff(
221  res,
222  minus_exprt(
223  typecast_exprt(s1.length(), return_type),
224  typecast_exprt(s2.length(), return_type)));
225  or_exprt guard1(
230  and_exprt cond1(ret_char_diff, guard1);
231  or_exprt guard2(
233  s1.axiom_for_has_length(x)),
235  s2.axiom_for_has_length(x)));
236  and_exprt cond2(ret_length_diff, guard2);
237 
238  implies_exprt a3(
239  not_exprt(res_null),
240  and_exprt(
241  binary_relation_exprt(x, ID_ge, from_integer(0, return_type)),
242  or_exprt(cond1, cond2)));
243  axioms.push_back(a3);
244 
245  string_constraintt a4(i, x, not_exprt(res_null), equal_exprt(s1[i], s2[i]));
246  axioms.push_back(a4);
247 
248  return res;
249 }
250 
257 {
259  const typet &return_type=f.type();
260  typet index_type=str.length().type();
261 
262  // initialisation of the missing pool variable
263  std::map<irep_idt, string_exprt>::iterator it;
264  for(it=symbol_to_string.begin(); it!=symbol_to_string.end(); it++)
265  if(pool.find(it->second)==pool.end())
266  pool[it->second]=fresh_symbol("pool", return_type);
267 
268  // intern(str)=s_0 || s_1 || ...
269  // for each string s.
270  // intern(str)=intern(s) || |str|!=|s|
271  // || (|str|==|s| &&exists i<|s|. s[i]!=str[i])
272 
273  exprt disj=false_exprt();
274  for(it=symbol_to_string.begin(); it!=symbol_to_string.end(); it++)
275  disj=or_exprt(
276  disj, equal_exprt(pool[str], symbol_exprt(it->first, return_type)));
277 
278  axioms.push_back(disj);
279 
280 
281  // WARNING: the specification may be incomplete or incorrect
282  for(it=symbol_to_string.begin(); it!=symbol_to_string.end(); it++)
283  if(it->second!=str)
284  {
285  symbol_exprt i=fresh_exist_index("index_intern", index_type);
286  axioms.push_back(
287  or_exprt(
288  equal_exprt(pool[it->second], pool[str]),
289  or_exprt(
290  not_exprt(str.axiom_for_has_same_length_as(it->second)),
291  and_exprt(
292  str.axiom_for_has_same_length_as(it->second),
293  and_exprt(
294  not_exprt(equal_exprt(str[i], it->second[i])),
295  and_exprt(str.axiom_for_is_strictly_longer_than(i),
297  }
298 
299  return pool[str];
300 }
exprt add_axioms_for_compare_to(const function_application_exprt &f)
add axioms corresponding to the String.compareTo java function
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
application of (mathematical) function
Definition: std_expr.h:3785
boolean OR
Definition: std_expr.h:1968
exprt add_axioms_for_equals(const function_application_exprt &f)
add axioms stating that the result is true exactly when the strings represented by the arguments are ...
std::map< string_exprt, symbol_exprt > pool
static symbol_exprt fresh_symbol(const irep_idt &prefix, const typet &type=bool_typet())
generate a new symbol expression of the given type with some prefix
equal_exprt axiom_for_has_length(const exprt &rhs) const
Definition: string_expr.h:120
symbol_exprt fresh_univ_index(const irep_idt &prefix, const typet &type)
generate an index symbol to be used as an universaly quantified variable
equal_exprt axiom_for_has_same_length_as(const string_exprt &rhs) const
Definition: string_expr.h:114
typet & type()
Definition: expr.h:60
The proper Booleans.
Definition: std_types.h:33
binary_relation_exprt axiom_for_is_shorter_than(const string_exprt &rhs) const
Definition: string_expr.h:85
boolean implication
Definition: std_expr.h:1926
equality
Definition: std_expr.h:1082
symbol_exprt fresh_boolean(const irep_idt &prefix)
generate a Boolean symbol which is existentially quantified
std::map< irep_idt, string_exprt > symbol_to_string
const irep_idt & id() const
Definition: irep.h:189
const exprt & length() const
Definition: string_expr.h:35
exprt add_axioms_for_hash_code(const function_application_exprt &f)
add axioms stating that if two strings are equal then their hash codes are equals ...
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)
symbol_exprt add_axioms_for_intern(const function_application_exprt &f)
add axioms stating that the return value for two equal string should be the same
boolean AND
Definition: std_expr.h:1852
inequality
Definition: std_expr.h:1124
std::map< string_exprt, symbol_exprt > hash
exprt add_axioms_for_equals_ignore_case(const function_application_exprt &f)
add axioms corresponding to the String.equalsIgnoreCase java function
The plus expression.
Definition: std_expr.h:702
bitvector_typet index_type()
Definition: c_types.cpp:15
The boolean constant false.
Definition: std_expr.h:3753
binary_relation_exprt axiom_for_is_longer_than(const string_exprt &rhs) const
Definition: string_expr.h:56
static constant_exprt constant_char(int i, const typet &char_type)
generate constant character expression with character type.
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_relation_exprt axiom_for_is_strictly_longer_than(const exprt &rhs) const
Definition: string_expr.h:68
static exprt character_equals_ignore_case(exprt char1, exprt char2, exprt char_a, exprt char_A, exprt char_Z)
returns an expression which is true when the two given characters are equal when ignoring case for AS...
binary minus
Definition: std_expr.h:758
Expression to hold a symbol (variable)
Definition: std_expr.h:82
int8_t s1
Definition: bytecode_info.h:59
int16_t s2
Definition: bytecode_info.h:60
std::map< string_not_contains_constraintt, symbol_exprt > witness
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)
bitvector_typet char_type()
Definition: c_types.cpp:113
exprt axiom_for_is_positive_index(const exprt &x)
expression true exactly when the index is positive