cprover
string_constraint_generator_testing.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Generates string constraints for string functions that return
4  Boolean values
5 
6 Author: Romain Brenguier, romain.brenguier@diffblue.com
7 
8 \*******************************************************************/
9 
12 
15 
16 #include <util/deprecate.h>
17 
37 std::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();
46  const exprt offset_within_bounds = and_exprt(
47  binary_relation_exprt(offset, ID_ge, from_integer(0, offset.type())),
51  ID_ge,
53 
54  // Axiom 1.
55  constraints.existential.push_back(
56  implies_exprt(isprefix, offset_within_bounds));
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);
73  const exprt strings_differ_at_witness = and_exprt(
74  is_positive(witness),
76  notequal_exprt(str[plus_exprt(witness, offset)], prefix[witness]));
77  const exprt s1_does_not_start_with_s0 = or_exprt(
78  not_exprt(offset_within_bounds),
81  plus_exprt(array_pool.get_or_create_length(prefix), offset))),
82  strings_differ_at_witness);
83  return implies_exprt(not_exprt(isprefix), s1_does_not_start_with_s0);
84  }());
85 
86  return {isprefix, std::move(constraints)};
87 }
88 
94 // NOLINTNEXTLINE
104 std::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 =
113  get_string_expr(array_pool, args[swap_arguments ? 1u : 0u]);
114  const array_string_exprt &s1 =
115  get_string_expr(array_pool, args[swap_arguments ? 0u : 1u]);
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 
127 DEPRECATED(SINCE(2017, 10, 5, "should use `string_length s == 0` instead"))
128 std::pair<exprt, string_constraintst>
129 string_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 
168 DEPRECATED(SINCE(2018, 6, 6, "should use strings_startwith"))
169 std::pair<exprt, string_constraintst>
170 string_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");
180  typecast_exprt tc_issuffix(issuffix, f.type());
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 
187  implies_exprt a1(
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);
195  const plus_exprt qvar_shifted(
196  qvar,
197  minus_exprt(
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)),
203  implies_exprt(issuffix, equal_exprt(s0[qvar], s1[qvar_shifted])));
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,
209  minus_exprt(
210  array_pool.get_or_create_length(s1),
211  array_pool.get_or_create_length(s0)));
212  or_exprt constr3(
213  and_exprt(
214  greater_than(
215  array_pool.get_or_create_length(s0),
216  array_pool.get_or_create_length(s1)),
217  equal_exprt(witness, from_integer(-1, index_type))),
218  and_exprt(
219  notequal_exprt(s0[witness], s1[shifted]),
220  and_exprt(
221  greater_than(array_pool.get_or_create_length(s0), witness),
222  is_positive(witness))));
223  implies_exprt a3(not_exprt(issuffix), constr3);
224 
225  constraints.existential.push_back(a3);
226  return {tc_issuffix, std::move(constraints)};
227 }
228 
247 std::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 
267  minus_exprt length_diff(
269  and_exprt bounds(
270  is_positive(startpos), binary_relation_exprt(startpos, ID_le, length_diff));
271  implies_exprt a2(contains, bounds);
272  constraints.existential.push_back(a2);
273 
274  implies_exprt a3(
276  constraints.existential.push_back(a3);
277 
278  symbol_exprt qvar = fresh_symbol("QA_contains", index_type);
279  const plus_exprt qvar_shifted(qvar, startpos);
281  qvar,
283  implies_exprt(contains, equal_exprt(s1[qvar], s0[qvar_shifted])));
284  constraints.universal.push_back(a4);
285 
288  plus_exprt(from_integer(1, index_type), length_diff),
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 }
function_application_exprt::arguments
argumentst & arguments()
Definition: mathematical_expr.h:221
array_string_exprt::length_type
const typet & length_type() const
Definition: string_expr.h:69
greater_or_equal_to
binary_relation_exprt greater_or_equal_to(exprt lhs, exprt rhs)
Definition: string_expr.h:19
exprt::size
std::size_t size() const
Amount of nodes this expression tree contains.
Definition: expr.cpp:26
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
string_constraint_generatort::add_axioms_for_contains
std::pair< exprt, string_constraintst > add_axioms_for_contains(const function_application_exprt &f)
Test whether a string contains another.
Definition: string_constraint_generator_testing.cpp:248
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
string_refinement_invariant.h
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
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
function_application_exprt::argumentst
exprt::operandst argumentst
Definition: mathematical_expr.h:193
string_constraint_generatort::array_pool
array_poolt array_pool
Definition: string_constraint_generator.h:58
string_constraint_generatort
Definition: string_constraint_generator.h:45
notequal_exprt
Disequality.
Definition: std_expr.h:1248
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
is_empty
bool is_empty(const std::string &s)
Definition: document_properties.cpp:140
maximum
exprt maximum(const exprt &a, const exprt &b)
Definition: string_constraint_generator_main.cpp:400
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
irept::id
const irep_idt & id() const
Definition: irep.h:418
SINCE
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
minus_exprt
Binary minus.
Definition: std_expr.h:940
string_constraint_generatort::add_axioms_for_is_prefix
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...
Definition: string_constraint_generator_testing.cpp:38
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
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
is_positive
exprt is_positive(const exprt &x)
Definition: string_constraint_generator_main.cpp:338
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:725
contains
static bool contains(const exprt &index, const symbol_exprt &qvar)
Look for symbol qvar in the expression index and return true if found.
Definition: string_constraint_instantiation.cpp:19
string_constraintst::not_contains
std::vector< string_not_contains_constraintt > not_contains
Definition: string_constraint_generator.h:39
implies_exprt
Boolean implication.
Definition: std_expr.h:2200
string_not_contains_constraintt
Constraints to encode non containement of strings.
Definition: string_constraint.h:127
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
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