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 #include <util/deprecate.h>
16 
37 std::pair<exprt, string_constraintst> add_axioms_for_is_prefix(
38  symbol_generatort &fresh_symbol,
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())),
48  binary_relation_exprt(offset, ID_le, str.length()),
50  minus_exprt(str.length(), offset), ID_ge, prefix.length()));
51 
52  // Axiom 1.
53  constraints.existential.push_back(
54  implies_exprt(isprefix, offset_within_bounds));
55 
56  // Axiom 2.
57  constraints.universal.push_back([&] {
58  const symbol_exprt qvar = fresh_symbol("QA_isprefix", index_type);
59  const exprt body = implies_exprt(
60  isprefix, equal_exprt(str[plus_exprt(qvar, offset)], prefix[qvar]));
61  return string_constraintt(
62  qvar, maximum(from_integer(0, index_type), prefix.length()), body);
63  }());
64 
65  // Axiom 3.
66  constraints.existential.push_back([&] {
67  const exprt witness = fresh_symbol("witness_not_isprefix", index_type);
68  const exprt strings_differ_at_witness = and_exprt(
69  is_positive(witness),
70  length_gt(prefix, witness),
71  notequal_exprt(str[plus_exprt(witness, offset)], prefix[witness]));
72  const exprt s1_does_not_start_with_s0 = or_exprt(
73  not_exprt(offset_within_bounds),
74  not_exprt(length_ge(str, plus_exprt(prefix.length(), offset))),
75  strings_differ_at_witness);
76  return implies_exprt(not_exprt(isprefix), s1_does_not_start_with_s0);
77  }());
78 
79  return {isprefix, std::move(constraints)};
80 }
81 
87 // NOLINTNEXTLINE
99 std::pair<exprt, string_constraintst> add_axioms_for_is_prefix(
100  symbol_generatort &fresh_symbol,
102  bool swap_arguments,
103  array_poolt &array_pool)
104 {
106  PRECONDITION(f.type()==bool_typet() || f.type().id()==ID_c_bool);
107  PRECONDITION(args.size() == 2 || args.size() == 3);
108  const array_string_exprt &s0 =
109  get_string_expr(array_pool, args[swap_arguments ? 1u : 0u]);
110  const array_string_exprt &s1 =
111  get_string_expr(array_pool, args[swap_arguments ? 0u : 1u]);
112  const exprt offset =
113  args.size() == 2 ? from_integer(0, s0.length().type()) : args[2];
114  auto pair = add_axioms_for_is_prefix(fresh_symbol, s0, s1, offset);
115  return {typecast_exprt(pair.first, f.type()), std::move(pair.second)};
116 }
117 
125 DEPRECATED("should use `string_length(s)==0` instead")
127  symbol_generatort &fresh_symbol,
129  array_poolt &array_pool)
130 {
131  PRECONDITION(f.type()==bool_typet() || f.type().id()==ID_c_bool);
132  PRECONDITION(f.arguments().size() == 1);
133  // We add axioms:
134  // a1 : is_empty => |s0| = 0
135  // a2 : s0 => is_empty
136 
137  symbol_exprt is_empty = fresh_symbol("is_empty");
138  array_string_exprt s0 = get_string_expr(array_pool, f.arguments()[0]);
139  std::vector<exprt> constraints;
140  constraints.push_back(implies_exprt(is_empty, length_eq(s0, 0)));
141  constraints.push_back(implies_exprt(length_eq(s0, 0), is_empty));
142  return {typecast_exprt(is_empty, f.type()), {constraints}};
143 }
144 
167 DEPRECATED("should use `strings_startwith(s0, s1, s1.length - s0.length)`")
169  symbol_generatort &fresh_symbol,
171  bool swap_arguments,
172  array_poolt &array_pool)
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(issuffix, length_ge(s1, s0.length()));
188  constraints.existential.push_back(a1);
189 
190  symbol_exprt qvar = fresh_symbol("QA_suffix", index_type);
191  const plus_exprt qvar_shifted(qvar, minus_exprt(s1.length(), s0.length()));
193  qvar,
194  zero_if_negative(s0.length()),
195  implies_exprt(issuffix, equal_exprt(s0[qvar], s1[qvar_shifted])));
196  constraints.universal.push_back(a2);
197 
198  symbol_exprt witness = fresh_symbol("witness_not_suffix", index_type);
199  const plus_exprt shifted(witness, minus_exprt(s1.length(), s0.length()));
200  or_exprt constr3(
201  and_exprt(
202  length_gt(s0, s1.length()),
203  equal_exprt(witness, from_integer(-1, index_type))),
204  and_exprt(
205  notequal_exprt(s0[witness], s1[shifted]),
206  and_exprt(length_gt(s0, witness), is_positive(witness))));
207  implies_exprt a3(not_exprt(issuffix), constr3);
208 
209  constraints.existential.push_back(a3);
210  return {tc_issuffix, std::move(constraints)};
211 }
212 
233 std::pair<exprt, string_constraintst> add_axioms_for_contains(
234  symbol_generatort &fresh_symbol,
236  array_poolt &array_pool)
237 {
238  PRECONDITION(f.arguments().size() == 2);
239  PRECONDITION(f.type()==bool_typet() || f.type().id()==ID_c_bool);
240  string_constraintst constraints;
241  const array_string_exprt s0 = get_string_expr(array_pool, f.arguments()[0]);
242  const array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[1]);
243  const typet &index_type = s0.length().type();
244  const symbol_exprt contains = fresh_symbol("contains");
245  const symbol_exprt startpos = fresh_symbol("startpos_contains", index_type);
246 
247  const implies_exprt a1(contains, length_ge(s0, s1.length()));
248  constraints.existential.push_back(a1);
249 
250  minus_exprt length_diff(s0.length(), s1.length());
251  and_exprt bounds(
252  is_positive(startpos), binary_relation_exprt(startpos, ID_le, length_diff));
253  implies_exprt a2(contains, bounds);
254  constraints.existential.push_back(a2);
255 
256  implies_exprt a3(
257  not_exprt(contains),
258  equal_exprt(startpos, from_integer(-1, index_type)));
259  constraints.existential.push_back(a3);
260 
261  symbol_exprt qvar = fresh_symbol("QA_contains", index_type);
262  const plus_exprt qvar_shifted(qvar, startpos);
264  qvar,
265  zero_if_negative(s1.length()),
266  implies_exprt(contains, equal_exprt(s1[qvar], s0[qvar_shifted])));
267  constraints.universal.push_back(a4);
268 
271  plus_exprt(from_integer(1, index_type), length_diff),
272  and_exprt(not_exprt(contains), length_ge(s0, s1.length())),
274  s1.length(),
275  s0,
276  s1};
277  constraints.not_contains.push_back(a5);
278 
279  return {typecast_exprt(contains, f.type()), std::move(constraints)};
280 }
function_application_exprt::arguments
argumentst & arguments()
Definition: std_expr.h:4506
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
length_ge
binary_relation_exprt length_ge(const T &lhs, const exprt &rhs)
Definition: string_expr.h:21
length_eq
equal_exprt length_eq(const T &lhs, const exprt &rhs)
Definition: string_expr.h:54
typet
The type of an expression, extends irept.
Definition: type.h:27
array_poolt
Correspondance between arrays and pointers string representations.
Definition: string_constraint_generator.h:49
string_constraintt
Definition: string_constraint.h:58
length_gt
binary_relation_exprt length_gt(const T &lhs, const exprt &rhs)
Definition: string_expr.h:28
and_exprt
Boolean AND.
Definition: std_expr.h:2409
s1
int8_t s1
Definition: bytecode_info.h:59
string_refinement_invariant.h
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
exprt
Base class for all expressions.
Definition: expr.h:54
string_constraintst
Collection of constraints of different types: existential formulas, universal formulas,...
Definition: string_constraint_generator.h:108
bool_typet
The Boolean type.
Definition: std_types.h:28
add_axioms_for_contains
std::pair< exprt, string_constraintst > add_axioms_for_contains(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Test whether a string contains another.
Definition: string_constraint_generator_testing.cpp:233
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
equal_exprt
Equality.
Definition: std_expr.h:1484
function_application_exprt::argumentst
exprt::operandst argumentst
Definition: std_expr.h:4484
notequal_exprt
Disequality.
Definition: std_expr.h:1545
get_string_expr
array_string_exprt get_string_expr(array_poolt &pool, const exprt &expr)
casts an expression to a string expression, or fetches the actual string_exprt in the case of a symbo...
Definition: string_constraint_generator_main.cpp:210
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
is_empty
bool is_empty(const std::string &s)
Definition: document_properties.cpp:142
symbol_generatort
Generation of fresh symbols of a given type.
Definition: string_constraint_generator.h:32
maximum
exprt maximum(const exprt &a, const exprt &b)
Definition: string_constraint_generator_main.cpp:583
or_exprt
Boolean OR.
Definition: std_expr.h:2531
add_axioms_for_is_prefix
std::pair< exprt, string_constraintst > add_axioms_for_is_prefix(symbol_generatort &fresh_symbol, 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:37
deprecate.h
function_application_exprt
Application of (mathematical) function.
Definition: std_expr.h:4481
irept::id
const irep_idt & id() const
Definition: irep.h:259
minus_exprt
Binary minus.
Definition: std_expr.h:1106
add_axioms_for_is_empty
std::pair< exprt, string_constraintst > add_axioms_for_is_empty(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Add axioms stating that the returned value is true exactly when the argument string is empty.
Definition: string_constraint_generator_testing.cpp:126
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
add_axioms_for_is_suffix
std::pair< exprt, string_constraintst > add_axioms_for_is_suffix(symbol_generatort &fresh_symbol, const function_application_exprt &f, bool swap_arguments, array_poolt &array_pool)
Test if the target is a suffix of the string.
Definition: string_constraint_generator_testing.cpp:168
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
zero_if_negative
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
Definition: string_constraint_generator_main.cpp:591
is_positive
exprt is_positive(const exprt &x)
Definition: string_constraint_generator_main.cpp:524
array_string_exprt::length
exprt & length()
Definition: string_expr.h:70
binary_relation_exprt
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:878
string_constraintst::not_contains
std::vector< string_not_contains_constraintt > not_contains
Definition: string_constraint_generator.h:112
implies_exprt
Boolean implication.
Definition: std_expr.h:2485
string_not_contains_constraintt
Constraints to encode non containement of strings.
Definition: string_constraint.h:125
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2277
string_constraint_generator.h
array_string_exprt
Definition: string_expr.h:67
string_constraintst::existential
std::vector< exprt > existential
Definition: string_constraint_generator.h:110
not_exprt
Boolean negation.
Definition: std_expr.h:3308
string_constraintst::universal
std::vector< string_constraintt > universal
Definition: string_constraint_generator.h:111