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(qvar, prefix.length(), body);
58  }());
59 
60  // Axiom 3.
61  lemmas.push_back([&] {
62  const exprt witness = fresh_exist_index("witness_not_isprefix", index_type);
63  const exprt strings_differ_at_witness = and_exprt(
66  notequal_exprt(str[plus_exprt(witness, offset)], prefix[witness]));
67  const exprt s1_does_not_start_with_s0 = or_exprt(
68  not_exprt(offset_within_bounds),
69  not_exprt(str.axiom_for_length_ge(plus_exprt(prefix.length(), offset))),
70  strings_differ_at_witness);
71  return implies_exprt(not_exprt(isprefix), s1_does_not_start_with_s0);
72  }());
73 
74  return isprefix;
75 }
76 
82 // NOLINTNEXTLINE
93  const function_application_exprt &f, bool swap_arguments)
94 {
96  PRECONDITION(f.type()==bool_typet() || f.type().id()==ID_c_bool);
97  PRECONDITION(args.size() == 2 || args.size() == 3);
98  const array_string_exprt s0 = get_string_expr(args[swap_arguments ? 1 : 0]);
99  const array_string_exprt s1 = get_string_expr(args[swap_arguments ? 0 : 1]);
100  const exprt offset =
101  args.size() == 2 ? from_integer(0, s0.length().type()) : args[2];
102  return typecast_exprt(add_axioms_for_is_prefix(s0, s1, offset), f.type());
103 }
104 
110 DEPRECATED("should use `string_length(s)==0` instead")
111 exprt string_constraint_generatort::add_axioms_for_is_empty(
113 {
114  PRECONDITION(f.type()==bool_typet() || f.type().id()==ID_c_bool);
115  PRECONDITION(f.arguments().size() == 1);
116  // We add axioms:
117  // a1 : is_empty => |s0| = 0
118  // a2 : s0 => is_empty
119 
120  symbol_exprt is_empty=fresh_boolean("is_empty");
121  array_string_exprt s0 = get_string_expr(f.arguments()[0]);
122  lemmas.push_back(implies_exprt(is_empty, s0.axiom_for_has_length(0)));
123  lemmas.push_back(implies_exprt(s0.axiom_for_has_length(0), is_empty));
124  return typecast_exprt(is_empty, f.type());
125 }
126 
147 DEPRECATED("should use `strings_startwith(s0, s1, s1.length - s0.length)`")
148 exprt string_constraint_generatort::add_axioms_for_is_suffix(
149  const function_application_exprt &f, bool swap_arguments)
150 {
151  const function_application_exprt::argumentst &args=f.arguments();
152  PRECONDITION(args.size()==2); // bad args to string issuffix?
153  PRECONDITION(f.type()==bool_typet() || f.type().id()==ID_c_bool);
154 
155  symbol_exprt issuffix=fresh_boolean("issuffix");
156  typecast_exprt tc_issuffix(issuffix, f.type());
157  const array_string_exprt &s0 = get_string_expr(args[swap_arguments ? 1 : 0]);
158  const array_string_exprt &s1 = get_string_expr(args[swap_arguments ? 0 : 1]);
159  const typet &index_type=s0.length().type();
160 
161  implies_exprt a1(issuffix, s1.axiom_for_length_ge(s0.length()));
162  lemmas.push_back(a1);
163 
164  symbol_exprt qvar=fresh_univ_index("QA_suffix", index_type);
165  const plus_exprt qvar_shifted(qvar, minus_exprt(s1.length(), s0.length()));
167  qvar,
168  s0.length(),
169  implies_exprt(issuffix, equal_exprt(s0[qvar], s1[qvar_shifted])));
170  constraints.push_back(a2);
171 
172  symbol_exprt witness=fresh_exist_index("witness_not_suffix", index_type);
173  const plus_exprt shifted(witness, minus_exprt(s1.length(), s0.length()));
174  or_exprt constr3(
175  and_exprt(
176  s0.axiom_for_length_gt(s1.length()),
177  equal_exprt(witness, from_integer(-1, index_type))),
178  and_exprt(
179  notequal_exprt(s0[witness], s1[shifted]),
180  and_exprt(
181  s0.axiom_for_length_gt(witness),
182  axiom_for_is_positive_index(witness))));
183  implies_exprt a3(not_exprt(issuffix), constr3);
184 
185  lemmas.push_back(a3);
186  return tc_issuffix;
187 }
188 
209 {
210  PRECONDITION(f.arguments().size() == 2);
211  PRECONDITION(f.type()==bool_typet() || f.type().id()==ID_c_bool);
212  const array_string_exprt s0 = get_string_expr(f.arguments()[0]);
214  const typet &index_type = s0.length().type();
215  const symbol_exprt contains = fresh_boolean("contains");
216  const symbol_exprt startpos =
217  fresh_exist_index("startpos_contains", index_type);
218 
219  const implies_exprt a1(contains, s0.axiom_for_length_ge(s1.length()));
220  lemmas.push_back(a1);
221 
222  minus_exprt length_diff(s0.length(), s1.length());
223  and_exprt bounds(
224  axiom_for_is_positive_index(startpos),
225  binary_relation_exprt(startpos, ID_le, length_diff));
226  implies_exprt a2(contains, bounds);
227  lemmas.push_back(a2);
228 
229  implies_exprt a3(
230  not_exprt(contains),
231  equal_exprt(startpos, from_integer(-1, index_type)));
232  lemmas.push_back(a3);
233 
234  symbol_exprt qvar=fresh_univ_index("QA_contains", index_type);
235  const plus_exprt qvar_shifted(qvar, startpos);
237  qvar,
238  s1.length(),
239  implies_exprt(contains, equal_exprt(s1[qvar], s0[qvar_shifted])));
240  constraints.push_back(a4);
241 
244  plus_exprt(from_integer(1, index_type), length_diff),
245  and_exprt(not_exprt(contains), s0.axiom_for_length_ge(s1.length())),
247  s1.length(),
248  s0,
249  s1);
250  not_contains_constraints.push_back(a5);
251 
252  return typecast_exprt(contains, f.type());
253 }
The type of an expression.
Definition: type.h:22
Boolean negation.
Definition: std_expr.h:3230
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:4531
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:4564
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:189
Constraints to encode non containement of strings.
DEPRECATED("use instrument_cover_goals(goto_programt &goto_program," "const cover_instrumenterst &instrumenters," "message_handlert &message_handler, const irep_idt mode) instead") void instrument_cover_goals(const symbol_tablet &symbol_table
Instruments goto program for a given coverage criterion.
exprt::operandst argumentst
Definition: std_expr.h:4562
boolean AND
Definition: std_expr.h:2255
inequality
Definition: std_expr.h:1406
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
The plus expression.
Definition: std_expr.h:893
bitvector_typet index_type()
Definition: c_types.cpp:16
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