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 
16 #include <util/deprecate.h>
17 
30 std::pair<exprt, string_constraintst>
33 {
34  PRECONDITION(f.type() == bool_typet() || f.type().id() == ID_c_bool);
35  PRECONDITION(f.arguments().size() == 2);
36 
37  string_constraintst constraints;
40  symbol_exprt eq = fresh_symbol("equal");
41  typecast_exprt tc_eq(eq, f.type());
42 
43  typet index_type = s1.length_type();
44 
45  // Axiom 1.
46  constraints.existential.push_back(implies_exprt(
47  eq,
51 
52  // Axiom 2.
53  constraints.universal.push_back([&] {
54  const symbol_exprt qvar = fresh_symbol("QA_equal", index_type);
55  return string_constraintt(
56  qvar,
58  implies_exprt(eq, equal_exprt(s1[qvar], s2[qvar])));
59  }());
60 
61  // Axiom 3.
62  constraints.existential.push_back([&] {
63  const symbol_exprt witness = fresh_symbol("witness_unequal", index_type);
64  const exprt zero = from_integer(0, index_type);
65  const and_exprt bound_witness(
67  witness, ID_lt, array_pool.get_or_create_length(s1)),
68  binary_relation_exprt(witness, ID_ge, zero));
69  const and_exprt witnessing(
70  bound_witness, notequal_exprt(s1[witness], s2[witness]));
71  const and_exprt diff_length(
75  equal_exprt(witness, from_integer(-1, index_type)));
76  return implies_exprt(not_exprt(eq), or_exprt(diff_length, witnessing));
77  }());
78 
79  return {tc_eq, std::move(constraints)};
80 }
81 
92  const exprt &char1,
93  const exprt &char2,
94  const exprt &char_a,
95  const exprt &char_A,
96  const exprt &char_Z)
97 {
98  const and_exprt is_upper_case_1(
99  binary_relation_exprt(char_A, ID_le, char1),
100  binary_relation_exprt(char1, ID_le, char_Z));
101  const and_exprt is_upper_case_2(
102  binary_relation_exprt(char_A, ID_le, char2),
103  binary_relation_exprt(char2, ID_le, char_Z));
104 
105  // Three possibilities:
106  // p1 : char1=char2
107  // p2 : (is_up1&&'a'-'A'+char1=char2)
108  // p3 : (is_up2&&'a'-'A'+char2=char1)
109  const equal_exprt p1(char1, char2);
110  const minus_exprt diff(char_a, char_A);
111 
112  // Overflow is not a problem here because is_upper_case conditions
113  // ensure that we are within a safe range.
114  const exprt p2 =
115  and_exprt(is_upper_case_1, equal_exprt(plus_exprt(diff, char1), char2));
116  const exprt p3 =
117  and_exprt(is_upper_case_2, equal_exprt(plus_exprt(diff, char2), char1));
118  return or_exprt(p1, p2, p3);
119 }
120 
134 std::pair<exprt, string_constraintst>
137 {
138  PRECONDITION(f.type() == bool_typet() || f.type().id() == ID_c_bool);
139  PRECONDITION(f.arguments().size() == 2);
140  string_constraintst constraints;
141  const symbol_exprt eq = fresh_symbol("equal_ignore_case");
144  const typet char_type = s1.content().type().subtype();
145  const exprt char_a = from_integer('a', char_type);
146  const exprt char_A = from_integer('A', char_type);
147  const exprt char_Z = from_integer('Z', char_type);
148  const typet index_type = s1.length_type();
149 
150  const implies_exprt a1(
151  eq,
152  equal_exprt(
155  constraints.existential.push_back(a1);
156 
157  const symbol_exprt qvar = fresh_symbol("QA_equal_ignore_case", index_type);
158  const exprt constr2 =
159  character_equals_ignore_case(s1[qvar], s2[qvar], char_a, char_A, char_Z);
160  const string_constraintt a2(
161  qvar,
163  implies_exprt(eq, constr2));
164  constraints.universal.push_back(a2);
165 
166  const symbol_exprt witness =
167  fresh_symbol("witness_unequal_ignore_case", index_type);
168  const exprt zero = from_integer(0, witness.type());
169  const and_exprt bound_witness(
171  binary_relation_exprt(witness, ID_ge, zero));
172  const exprt witness_eq = character_equals_ignore_case(
173  s1[witness], s2[witness], char_a, char_A, char_Z);
174  const not_exprt witness_diff(witness_eq);
175  const implies_exprt a3(
176  not_exprt(eq),
177  or_exprt(
181  and_exprt(bound_witness, witness_diff)));
182  constraints.existential.push_back(a3);
183 
184  return {typecast_exprt(eq, f.type()), std::move(constraints)};
185 }
186 
206 std::pair<exprt, string_constraintst>
209 {
210  PRECONDITION(f.arguments().size() == 2);
211  const typet &return_type = f.type();
212  PRECONDITION(return_type.id() == ID_signedbv);
213  string_constraintst constraints;
216  const symbol_exprt res = fresh_symbol("compare_to", return_type);
217  const typet &index_type = s1.length_type();
218 
219  const equal_exprt res_null(res, from_integer(0, return_type));
220  const implies_exprt a1(
221  res_null,
222  equal_exprt(
225  constraints.existential.push_back(a1);
226 
227  const symbol_exprt i = fresh_symbol("QA_compare_to", index_type);
228  const string_constraintt a2(
229  i,
231  implies_exprt(res_null, equal_exprt(s1[i], s2[i])));
232  constraints.universal.push_back(a2);
233 
234  const symbol_exprt x = fresh_symbol("index_compare_to", index_type);
235  const equal_exprt ret_char_diff(
236  res,
237  minus_exprt(
238  typecast_exprt(s1[x], return_type), typecast_exprt(s2[x], return_type)));
239  const equal_exprt ret_length_diff(
240  res,
241  minus_exprt(
244  const or_exprt guard1(
245  and_exprt(
250  and_exprt(
255  const and_exprt cond1(ret_char_diff, guard1);
256  const or_exprt guard2(
257  and_exprt(
258  greater_than(
262  and_exprt(
263  greater_than(
267  const and_exprt cond2(ret_length_diff, guard2);
268 
269  const implies_exprt a3(
270  not_exprt(res_null),
271  and_exprt(
272  binary_relation_exprt(x, ID_ge, from_integer(0, return_type)),
273  or_exprt(cond1, cond2)));
274  constraints.existential.push_back(a3);
275 
276  const symbol_exprt i2 = fresh_symbol("QA_compare_to", index_type);
277  const string_constraintt a4(
278  i2,
279  zero_if_negative(x),
280  implies_exprt(not_exprt(res_null), equal_exprt(s1[i2], s2[i2])));
281  constraints.universal.push_back(a4);
282 
283  return {res, std::move(constraints)};
284 }
function_application_exprt::arguments
argumentst & arguments()
Definition: mathematical_expr.h:221
typet::subtype
const typet & subtype() const
Definition: type.h:47
greater_or_equal_to
binary_relation_exprt greater_or_equal_to(exprt lhs, exprt rhs)
Definition: string_expr.h:19
typet
The type of an expression, extends irept.
Definition: type.h:29
string_constraintt
Definition: string_constraint.h:60
string_constraint_generatort::fresh_symbol
symbol_generatort fresh_symbol
Definition: string_constraint_generator.h:56
and_exprt
Boolean AND.
Definition: std_expr.h:2137
s1
int8_t s1
Definition: bytecode_info.h:59
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
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
bool_typet
The Boolean type.
Definition: std_types.h:37
string_constraint_generatort::add_axioms_for_equals
std::pair< exprt, string_constraintst > add_axioms_for_equals(const function_application_exprt &f)
Equality of the content of two strings.
Definition: string_constraint_generator_comparison.cpp:31
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
string_constraint_generatort::array_pool
array_poolt array_pool
Definition: string_constraint_generator.h:58
notequal_exprt
Disequality.
Definition: std_expr.h:1248
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
string_constraint_generatort::add_axioms_for_compare_to
std::pair< exprt, string_constraintst > add_axioms_for_compare_to(const function_application_exprt &f)
Lexicographic comparison of two strings.
Definition: string_constraint_generator_comparison.cpp:207
or_exprt
Boolean OR.
Definition: std_expr.h:2245
deprecate.h
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
function_application_exprt
Application of (mathematical) function.
Definition: mathematical_expr.h:191
less_than_or_equal_to
binary_relation_exprt less_than_or_equal_to(exprt lhs, exprt rhs)
Definition: string_expr.h:36
irept::id
const irep_idt & id() const
Definition: irep.h:418
minus_exprt
Binary minus.
Definition: std_expr.h:940
string_constraint_generatort::add_axioms_for_equals_ignore_case
std::pair< exprt, string_constraintst > add_axioms_for_equals_ignore_case(const function_application_exprt &f)
Equality of the content ignoring case of characters.
Definition: string_constraint_generator_comparison.cpp:135
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
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
implies_exprt
Boolean implication.
Definition: std_expr.h:2200
equal_to
equal_exprt equal_to(exprt lhs, exprt rhs)
Definition: string_expr.h:54
greater_than
binary_relation_exprt greater_than(exprt lhs, exprt rhs)
Definition: string_expr.h:25
s2
int16_t s2
Definition: bytecode_info.h:60
character_equals_ignore_case
static exprt character_equals_ignore_case(const exprt &char1, const exprt &char2, const exprt &char_a, const exprt &char_A, const exprt &char_Z)
Returns an expression which is true when the two given characters are equal when ignoring case for AS...
Definition: string_constraint_generator_comparison.cpp:91
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
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