cprover
Loading...
Searching...
No Matches
string_constraint_generator_comparison.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Generates string constraints for function comparing strings,
4 such as: equals, equalsIgnoreCase, compareTo, hashCode, intern
5
6Author: Romain Brenguier, romain.brenguier@diffblue.com
7
8\*******************************************************************/
9
13
15
17
30std::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");
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,
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);
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{
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);
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 =
116 const exprt p3 =
118 return or_exprt(p1, p2, p3);
119}
120
134std::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 = to_type_with_subtype(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,
155 constraints.existential.push_back(a1);
156
157 const symbol_exprt qvar = fresh_symbol("QA_equal_ignore_case", index_type);
158 const exprt constr2 =
161 qvar,
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());
175 const implies_exprt a3(
176 not_exprt(eq),
177 or_exprt(
182 constraints.existential.push_back(a3);
183
184 return {typecast_exprt(eq, f.type()), std::move(constraints)};
185}
186
206std::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,
225 constraints.existential.push_back(a1);
226
227 const symbol_exprt i = fresh_symbol("QA_compare_to", index_type);
229 i,
232 constraints.universal.push_back(a2);
233
234 const symbol_exprt x = fresh_symbol("index_compare_to", index_type);
236 res,
238 typecast_exprt(s1[x], return_type), typecast_exprt(s2[x], return_type)));
240 res,
244 const or_exprt guard1(
245 and_exprt(
250 and_exprt(
256 const or_exprt guard2(
257 and_exprt(
262 and_exprt(
268
269 const implies_exprt a3(
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);
278 i2,
281 constraints.universal.push_back(a4);
282
283 return {res, std::move(constraints)};
284}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
array_string_exprt get_string_expr(array_poolt &array_pool, const exprt &expr)
Fetch the string_exprt corresponding to the given refined_string_exprt.
bitvector_typet index_type()
Definition c_types.cpp:22
bitvector_typet char_type()
Definition c_types.cpp:124
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
Boolean AND.
Definition std_expr.h:1974
exprt get_or_create_length(const array_string_exprt &s)
Get the length of an array_string_exprt from the array_pool.
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:674
The Boolean type.
Definition std_types.h:36
Equality.
Definition std_expr.h:1225
Base class for all expressions.
Definition expr.h:54
typet & type()
Return the type of the expression.
Definition expr.h:82
Application of (mathematical) function.
Boolean implication.
Definition std_expr.h:2037
const irep_idt & id() const
Definition irep.h:396
Binary minus.
Definition std_expr.h:973
Boolean negation.
Definition std_expr.h:2181
Disequality.
Definition std_expr.h:1283
Boolean OR.
Definition std_expr.h:2082
The plus expression Associativity is not specified.
Definition std_expr.h:914
std::pair< exprt, string_constraintst > add_axioms_for_compare_to(const function_application_exprt &f)
Lexicographic comparison of two strings.
std::pair< exprt, string_constraintst > add_axioms_for_equals_ignore_case(const function_application_exprt &f)
Equality of the content ignoring case of characters.
std::pair< exprt, string_constraintst > add_axioms_for_equals(const function_application_exprt &f)
Equality of the content of two strings.
Expression to hold a symbol (variable)
Definition std_expr.h:80
const typet & subtype() const
Definition type.h:156
Semantic type conversion.
Definition std_expr.h:1920
The type of an expression, extends irept.
Definition type.h:29
API to expression classes for 'mathematical' expressions.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
Generates string constraints to link results from string functions with their arguments.
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
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...
binary_relation_exprt less_than_or_equal_to(exprt lhs, exprt rhs)
Definition string_expr.h:36
binary_relation_exprt greater_or_equal_to(exprt lhs, exprt rhs)
Definition string_expr.h:19
binary_relation_exprt greater_than(exprt lhs, exprt rhs)
Definition string_expr.h:25
equal_exprt equal_to(exprt lhs, exprt rhs)
Definition string_expr.h:54
Collection of constraints of different types: existential formulas, universal formulas,...
std::vector< exprt > existential
std::vector< string_constraintt > universal
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition type.h:177