cprover
Loading...
Searching...
No Matches
string_constraint_generator_testing.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Generates string constraints for string functions that return
4 Boolean values
5
6Author: Romain Brenguier, romain.brenguier@diffblue.com
7
8\*******************************************************************/
9
12
14
15#include <util/deprecate.h>
17
37std::pair<exprt, string_constraintst>
39 const array_string_exprt &prefix,
40 const array_string_exprt &str,
41 const exprt &offset)
42{
43 string_constraintst constraints;
44 const symbol_exprt isprefix = fresh_symbol("isprefix");
45 const typet &index_type = str.length_type();
47 binary_relation_exprt(offset, ID_ge, from_integer(0, offset.type())),
51 ID_ge,
53
54 // Axiom 1.
55 constraints.existential.push_back(
57
58 // Axiom 2.
59 constraints.universal.push_back([&] {
60 const symbol_exprt qvar = fresh_symbol("QA_isprefix", index_type);
61 const exprt body = implies_exprt(
62 isprefix, equal_exprt(str[plus_exprt(qvar, offset)], prefix[qvar]));
63 return string_constraintt(
64 qvar,
65 maximum(
67 body);
68 }());
69
70 // Axiom 3.
71 constraints.existential.push_back([&] {
72 const exprt witness = fresh_symbol("witness_not_isprefix", index_type);
76 notequal_exprt(str[plus_exprt(witness, offset)], prefix[witness]));
84 }());
85
86 return {isprefix, std::move(constraints)};
87}
88
94// NOLINTNEXTLINE
104std::pair<exprt, string_constraintst>
107 bool swap_arguments)
108{
110 PRECONDITION(f.type() == bool_typet() || f.type().id() == ID_c_bool);
111 PRECONDITION(args.size() == 2 || args.size() == 3);
112 const array_string_exprt &s0 =
114 const array_string_exprt &s1 =
116 const exprt offset =
117 args.size() == 2 ? from_integer(0, s0.length_type()) : args[2];
118 auto pair = add_axioms_for_is_prefix(s0, s1, offset);
119 return {typecast_exprt(pair.first, f.type()), std::move(pair.second)};
120}
121
127DEPRECATED(SINCE(2017, 10, 5, "should use `string_length s == 0` instead"))
129string_constraint_generatort::add_axioms_for_is_empty(
131{
132 PRECONDITION(f.type() == bool_typet() || f.type().id() == ID_c_bool);
133 PRECONDITION(f.arguments().size() == 1);
134 // We add axioms:
135 // a1 : is_empty => |s0| = 0
136 // a2 : s0 => is_empty
137
138 symbol_exprt is_empty = fresh_symbol("is_empty");
139 array_string_exprt s0 = get_string_expr(array_pool, f.arguments()[0]);
140 string_constraintst constraints;
141 constraints.existential = {
142 implies_exprt(is_empty, equal_to(array_pool.get_or_create_length(s0), 0)),
143 implies_exprt(equal_to(array_pool.get_or_create_length(s0), 0), is_empty)};
144 return {typecast_exprt(is_empty, f.type()), std::move(constraints)};
145}
146
168DEPRECATED(SINCE(2018, 6, 6, "should use strings_startwith"))
170string_constraint_generatort::add_axioms_for_is_suffix(
172 bool swap_arguments)
173{
174 const function_application_exprt::argumentst &args = f.arguments();
175 PRECONDITION(args.size() == 2); // bad args to string issuffix?
176 PRECONDITION(f.type() == bool_typet() || f.type().id() == ID_c_bool);
177
178 string_constraintst constraints;
179 symbol_exprt issuffix = fresh_symbol("issuffix");
181 const array_string_exprt &s0 =
182 get_string_expr(array_pool, args[swap_arguments ? 1u : 0u]);
183 const array_string_exprt &s1 =
184 get_string_expr(array_pool, args[swap_arguments ? 0u : 1u]);
185 const typet &index_type = s0.length_type();
186
188 issuffix,
190 array_pool.get_or_create_length(s1),
191 array_pool.get_or_create_length(s0)));
192 constraints.existential.push_back(a1);
193
194 symbol_exprt qvar = fresh_symbol("QA_suffix", index_type);
196 qvar,
198 array_pool.get_or_create_length(s1),
199 array_pool.get_or_create_length(s0)));
201 qvar,
202 zero_if_negative(array_pool.get_or_create_length(s0)),
204 constraints.universal.push_back(a2);
205
206 symbol_exprt witness = fresh_symbol("witness_not_suffix", index_type);
207 const plus_exprt shifted(
208 witness,
210 array_pool.get_or_create_length(s1),
211 array_pool.get_or_create_length(s0)));
213 and_exprt(
215 array_pool.get_or_create_length(s0),
216 array_pool.get_or_create_length(s1)),
218 and_exprt(
220 and_exprt(
221 greater_than(array_pool.get_or_create_length(s0), witness),
224
225 constraints.existential.push_back(a3);
226 return {tc_issuffix, std::move(constraints)};
227}
228
247std::pair<exprt, string_constraintst>
250{
251 PRECONDITION(f.arguments().size() == 2);
252 PRECONDITION(f.type() == bool_typet() || f.type().id() == ID_c_bool);
253 string_constraintst constraints;
256 const typet &index_type = s0.length_type();
257 const symbol_exprt contains = fresh_symbol("contains");
258 const symbol_exprt startpos = fresh_symbol("startpos_contains", index_type);
259
260 const implies_exprt a1(
261 contains,
265 constraints.existential.push_back(a1);
266
272 constraints.existential.push_back(a2);
273
276 constraints.existential.push_back(a3);
277
278 symbol_exprt qvar = fresh_symbol("QA_contains", index_type);
281 qvar,
284 constraints.universal.push_back(a4);
285
289 and_exprt(
296 s0,
297 s1};
298 constraints.not_contains.push_back(a5);
299
300 return {typecast_exprt(contains, f.type()), std::move(constraints)};
301}
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
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.
const typet & length_type() const
Definition string_expr.h:69
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_is_prefix(const array_string_exprt &prefix, const array_string_exprt &str, const exprt &offset)
Add axioms stating that the returned expression is true exactly when the offset is greater or equal t...
std::pair< exprt, string_constraintst > add_axioms_for_contains(const function_application_exprt &f)
Test whether a string contains another.
Expression to hold a symbol (variable)
Definition std_expr.h:80
Semantic type conversion.
Definition std_expr.h:1920
The type of an expression, extends irept.
Definition type.h:29
#define SINCE(year, month, day, msg)
Definition deprecate.h:26
#define DEPRECATED(msg)
Definition deprecate.h:23
bool is_empty(const std::string &s)
API to expression classes for 'mathematical' expressions.
STL namespace.
#define PRECONDITION(CONDITION)
Definition invariant.h:463
Generates string constraints to link results from string functions with their arguments.
exprt is_positive(const exprt &x)
exprt maximum(const exprt &a, const exprt &b)
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
static bool contains(const exprt &index, const symbol_exprt &qvar)
Look for symbol qvar in the expression index and return true if found.
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< string_not_contains_constraintt > not_contains
std::vector< exprt > existential
std::vector< string_constraintt > universal
Constraints to encode non containement of strings.