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  const array_string_exprt &prefix,
38  const array_string_exprt &str,
39  const exprt &offset)
40 {
41  const symbol_exprt isprefix = fresh_boolean("isprefix");
42  const typet &index_type = str.length().type();
43  const exprt offset_within_bounds = and_exprt(
44  binary_relation_exprt(offset, ID_ge, from_integer(0, offset.type())),
45  binary_relation_exprt(offset, ID_le, str.length()),
47  minus_exprt(str.length(), offset), ID_ge, prefix.length()));
48 
49  // Axiom 1.
50  lemmas.push_back(implies_exprt(isprefix, offset_within_bounds));
51 
52  // Axiom 2.
53  constraints.push_back([&] {
54  const symbol_exprt qvar = fresh_univ_index("QA_isprefix", index_type);
55  const exprt body = implies_exprt(
56  isprefix, equal_exprt(str[plus_exprt(qvar, offset)], prefix[qvar]));
57  return string_constraintt(
58  qvar, maximum(from_integer(0, index_type), prefix.length()), body);
59  }());
60 
61  // Axiom 3.
62  lemmas.push_back([&] {
63  const exprt witness = fresh_exist_index("witness_not_isprefix", index_type);
64  const exprt strings_differ_at_witness = and_exprt(
67  notequal_exprt(str[plus_exprt(witness, offset)], prefix[witness]));
68  const exprt s1_does_not_start_with_s0 = or_exprt(
69  not_exprt(offset_within_bounds),
70  not_exprt(str.axiom_for_length_ge(plus_exprt(prefix.length(), offset))),
71  strings_differ_at_witness);
72  return implies_exprt(not_exprt(isprefix), s1_does_not_start_with_s0);
73  }());
74 
75  return isprefix;
76 }
77 
83 // NOLINTNEXTLINE
94  const function_application_exprt &f, bool swap_arguments)
95 {
97  PRECONDITION(f.type()==bool_typet() || f.type().id()==ID_c_bool);
98  PRECONDITION(args.size() == 2 || args.size() == 3);
99  const array_string_exprt &s0 =
100  get_string_expr(args[swap_arguments ? 1u : 0u]);
101  const array_string_exprt &s1 =
102  get_string_expr(args[swap_arguments ? 0u : 1u]);
103  const exprt offset =
104  args.size() == 2 ? from_integer(0, s0.length().type()) : args[2];
105  return typecast_exprt(add_axioms_for_is_prefix(s0, s1, offset), f.type());
106 }
107 
113 DEPRECATED("should use `string_length(s)==0` instead")
114 exprt string_constraint_generatort::add_axioms_for_is_empty(
116 {
117  PRECONDITION(f.type()==bool_typet() || f.type().id()==ID_c_bool);
118  PRECONDITION(f.arguments().size() == 1);
119  // We add axioms:
120  // a1 : is_empty => |s0| = 0
121  // a2 : s0 => is_empty
122 
123  symbol_exprt is_empty=fresh_boolean("is_empty");
124  array_string_exprt s0 = get_string_expr(f.arguments()[0]);
125  lemmas.push_back(implies_exprt(is_empty, s0.axiom_for_has_length(0)));
126  lemmas.push_back(implies_exprt(s0.axiom_for_has_length(0), is_empty));
127  return typecast_exprt(is_empty, f.type());
128 }
129 
150 DEPRECATED("should use `strings_startwith(s0, s1, s1.length - s0.length)`")
151 exprt string_constraint_generatort::add_axioms_for_is_suffix(
152  const function_application_exprt &f, bool swap_arguments)
153 {
154  const function_application_exprt::argumentst &args=f.arguments();
155  PRECONDITION(args.size()==2); // bad args to string issuffix?
156  PRECONDITION(f.type()==bool_typet() || f.type().id()==ID_c_bool);
157 
158  symbol_exprt issuffix=fresh_boolean("issuffix");
159  typecast_exprt tc_issuffix(issuffix, f.type());
160  const array_string_exprt &s0 =
161  get_string_expr(args[swap_arguments ? 1u : 0u]);
162  const array_string_exprt &s1 =
163  get_string_expr(args[swap_arguments ? 0u : 1u]);
164  const typet &index_type=s0.length().type();
165 
166  implies_exprt a1(issuffix, s1.axiom_for_length_ge(s0.length()));
167  lemmas.push_back(a1);
168 
169  symbol_exprt qvar=fresh_univ_index("QA_suffix", index_type);
170  const plus_exprt qvar_shifted(qvar, minus_exprt(s1.length(), s0.length()));
172  qvar,
173  zero_if_negative(s0.length()),
174  implies_exprt(issuffix, equal_exprt(s0[qvar], s1[qvar_shifted])));
175  constraints.push_back(a2);
176 
177  symbol_exprt witness=fresh_exist_index("witness_not_suffix", index_type);
178  const plus_exprt shifted(witness, minus_exprt(s1.length(), s0.length()));
179  or_exprt constr3(
180  and_exprt(
181  s0.axiom_for_length_gt(s1.length()),
182  equal_exprt(witness, from_integer(-1, index_type))),
183  and_exprt(
184  notequal_exprt(s0[witness], s1[shifted]),
185  and_exprt(
186  s0.axiom_for_length_gt(witness),
187  axiom_for_is_positive_index(witness))));
188  implies_exprt a3(not_exprt(issuffix), constr3);
189 
190  lemmas.push_back(a3);
191  return tc_issuffix;
192 }
193 
214 {
215  PRECONDITION(f.arguments().size() == 2);
216  PRECONDITION(f.type()==bool_typet() || f.type().id()==ID_c_bool);
217  const array_string_exprt s0 = get_string_expr(f.arguments()[0]);
219  const typet &index_type = s0.length().type();
220  const symbol_exprt contains = fresh_boolean("contains");
221  const symbol_exprt startpos =
222  fresh_exist_index("startpos_contains", index_type);
223 
224  const implies_exprt a1(contains, s0.axiom_for_length_ge(s1.length()));
225  lemmas.push_back(a1);
226 
227  minus_exprt length_diff(s0.length(), s1.length());
228  and_exprt bounds(
229  axiom_for_is_positive_index(startpos),
230  binary_relation_exprt(startpos, ID_le, length_diff));
231  implies_exprt a2(contains, bounds);
232  lemmas.push_back(a2);
233 
234  implies_exprt a3(
235  not_exprt(contains),
236  equal_exprt(startpos, from_integer(-1, index_type)));
237  lemmas.push_back(a3);
238 
239  symbol_exprt qvar=fresh_univ_index("QA_contains", index_type);
240  const plus_exprt qvar_shifted(qvar, startpos);
242  qvar,
243  zero_if_negative(s1.length()),
244  implies_exprt(contains, equal_exprt(s1[qvar], s0[qvar_shifted])));
245  constraints.push_back(a4);
246 
249  plus_exprt(from_integer(1, index_type), length_diff),
250  and_exprt(not_exprt(contains), s0.axiom_for_length_ge(s1.length())),
252  s1.length(),
253  s0,
254  s1);
255  not_contains_constraints.push_back(a5);
256 
257  return typecast_exprt(contains, f.type());
258 }
The type of an expression.
Definition: type.h:22
Boolean negation.
Definition: std_expr.h:3228
semantic type conversion
Definition: std_expr.h:2111
Generates string constraints to link results from string functions with their arguments.
std::vector< string_not_contains_constraintt > not_contains_constraints
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
binary_relation_exprt axiom_for_length_ge(const string_exprt &rhs) const
Definition: string_expr.h:57
application of (mathematical) function
Definition: std_expr.h:4529
boolean OR
Definition: std_expr.h:2391
equal_exprt axiom_for_has_length(const exprt &rhs) const
Definition: string_expr.h:125
argumentst & arguments()
Definition: std_expr.h:4562
exprt add_axioms_for_contains(const function_application_exprt &f)
Test whether a string contains another.
symbol_exprt fresh_univ_index(const irep_idt &prefix, const typet &type)
generate an index symbol to be used as an universaly quantified variable
typet & type()
Definition: expr.h:56
The proper Booleans.
Definition: std_types.h:34
boolean implication
Definition: std_expr.h:2339
equality
Definition: std_expr.h:1354
symbol_exprt fresh_boolean(const irep_idt &prefix)
generate a Boolean symbol which is existentially quantified
const irep_idt & id() const
Definition: irep.h:259
Constraints to encode non containement of strings.
exprt::operandst argumentst
Definition: std_expr.h:4560
boolean AND
Definition: std_expr.h:2255
inequality
Definition: std_expr.h:1406
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
The plus expression.
Definition: std_expr.h:893
bitvector_typet index_type()
Definition: c_types.cpp:16
exprt maximum(const exprt &a, const exprt &b)
#define DEPRECATED(msg)
Definition: deprecate.h:23
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
symbol_exprt fresh_exist_index(const irep_idt &prefix, const typet &type)
generate an index symbol which is existentially quantified
Base class for all expressions.
Definition: expr.h:42
exprt 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...
binary_relation_exprt axiom_for_length_gt(const exprt &rhs) const
Definition: string_expr.h:70
bool is_empty(const std::string &s)
Universally quantified string constraint
binary minus
Definition: std_expr.h:959
Expression to hold a symbol (variable)
Definition: std_expr.h:90
int8_t s1
Definition: bytecode_info.h:59
std::vector< string_constraintt > constraints
std::map< string_not_contains_constraintt, symbol_exprt > witness
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
array_string_exprt get_string_expr(const exprt &expr)
casts an expression to a string expression, or fetches the actual string_exprt in the case of a symbo...
exprt axiom_for_is_positive_index(const exprt &x)
expression true exactly when the index is positive