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 
14 
20  const string_exprt &prefix, const string_exprt &str, const exprt &offset)
21 {
22  symbol_exprt isprefix=fresh_boolean("isprefix");
23  const typet &index_type=str.length().type();
24 
25  // We add axioms:
26  // a1 : isprefix => |str| >= |prefix|+offset
27  // a2 : forall 0<=qvar<prefix.length. isprefix =>
28  // s0[witness+offset]=s2[witness]
29  // a3 : !isprefix => |str| < |prefix|+offset
30  // || (|str| >= |prefix|+offset &&0<=witness<|prefix|
31  // &&str[witness+ofsset]!=prefix[witness])
32 
33  implies_exprt a1(
34  isprefix,
35  str.axiom_for_is_longer_than(plus_exprt(prefix.length(), offset)));
36  axioms.push_back(a1);
37 
38  symbol_exprt qvar=fresh_univ_index("QA_isprefix", index_type);
40  qvar,
41  prefix.length(),
42  isprefix,
43  equal_exprt(str[plus_exprt(qvar, offset)], prefix[qvar]));
44  axioms.push_back(a2);
45 
46  symbol_exprt witness=fresh_exist_index("witness_not_isprefix", index_type);
47  and_exprt witness_diff(
49  and_exprt(
50  prefix.axiom_for_is_strictly_longer_than(witness),
51  notequal_exprt(str[plus_exprt(witness, offset)], prefix[witness])));
52  or_exprt s0_notpref_s1(
53  not_exprt(
54  str.axiom_for_is_longer_than(plus_exprt(prefix.length(), offset))),
55  and_exprt(
56  witness_diff,
58  plus_exprt(prefix.length(), offset))));
59 
60  implies_exprt a3(not_exprt(isprefix), s0_notpref_s1);
61  axioms.push_back(a3);
62  return isprefix;
63 }
64 
72  const function_application_exprt &f, bool swap_arguments)
73 {
75  assert(f.type()==bool_typet() || f.type().id()==ID_c_bool);
76  string_exprt s0=add_axioms_for_string_expr(args[swap_arguments?1:0]);
77  string_exprt s1=add_axioms_for_string_expr(args[swap_arguments?0:1]);
78  exprt offset;
79  if(args.size()==2)
80  offset=from_integer(0, s0.length().type());
81  else if(args.size()==3)
82  offset=args[2];
83  return typecast_exprt(add_axioms_for_is_prefix(s0, s1, offset), f.type());
84 }
85 
92 {
93  assert(f.type()==bool_typet() || f.type().id()==ID_c_bool);
94 
95  // We add axioms:
96  // a1 : is_empty => |s0| = 0
97  // a2 : s0 => is_empty
98 
101  axioms.push_back(implies_exprt(is_empty, s0.axiom_for_has_length(0)));
103  return typecast_exprt(is_empty, f.type());
104 }
105 
113  const function_application_exprt &f, bool swap_arguments)
114 {
116  assert(args.size()==2); // bad args to string issuffix?
117  assert(f.type()==bool_typet() || f.type().id()==ID_c_bool);
118 
119  symbol_exprt issuffix=fresh_boolean("issuffix");
120  typecast_exprt tc_issuffix(issuffix, f.type());
121  string_exprt s0=add_axioms_for_string_expr(args[swap_arguments?1:0]);
122  string_exprt s1=add_axioms_for_string_expr(args[swap_arguments?0:1]);
123  const typet &index_type=s0.length().type();
124 
125  // We add axioms:
126  // a1 : issufix => s0.length >= s1.length
127  // a2 : forall witness<s1.length.
128  // issufix => s1[witness]=s0[witness + s0.length-s1.length]
129  // a3 : !issuffix =>
130  // s1.length > s0.length
131  // || (s1.length > witness>=0
132  // &&s1[witness]!=s0[witness + s0.length-s1.length]
133 
134  implies_exprt a1(issuffix, s1.axiom_for_is_longer_than(s0));
135  axioms.push_back(a1);
136 
137  symbol_exprt qvar=fresh_univ_index("QA_suffix", index_type);
138  exprt qvar_shifted=plus_exprt(
139  qvar, minus_exprt(s1.length(), s0.length()));
141  qvar, s0.length(), issuffix, equal_exprt(s0[qvar], s1[qvar_shifted]));
142  axioms.push_back(a2);
143 
144  symbol_exprt witness=fresh_exist_index("witness_not_suffix", index_type);
145  exprt shifted=plus_exprt(
146  witness, minus_exprt(s1.length(), s0.length()));
147  or_exprt constr3(
148  s0.axiom_for_is_strictly_longer_than(s1),
149  and_exprt(
150  notequal_exprt(s0[witness], s1[shifted]),
151  and_exprt(
152  s0.axiom_for_is_strictly_longer_than(witness),
153  axiom_for_is_positive_index(witness))));
154  implies_exprt a3(not_exprt(issuffix), constr3);
155 
156  axioms.push_back(a3);
157  return tc_issuffix;
158 }
159 
165 {
166  assert(f.type()==bool_typet() || f.type().id()==ID_c_bool);
167  symbol_exprt contains=fresh_boolean("contains");
168  typecast_exprt tc_contains(contains, f.type());
171  const typet &index_type=s0.type();
172 
173  // We add axioms:
174  // a1 : contains => s0.length >= s1.length
175  // a2 : 0 <= startpos <= s0.length-s1.length
176  // a3 : forall qvar<s1.length. contains => s1[qvar]=s0[startpos + qvar]
177  // a4 : !contains => s1.length > s0.length
178  // || (forall startpos <= s0.length-s1.length.
179  // exists witness<s1.length &&s1[witness]!=s0[witness + startpos]
180 
181  implies_exprt a1(contains, s0.axiom_for_is_longer_than(s1));
182  axioms.push_back(a1);
183 
184  symbol_exprt startpos=fresh_exist_index("startpos_contains", index_type);
185  minus_exprt length_diff(s0.length(), s1.length());
186  and_exprt a2(
187  axiom_for_is_positive_index(startpos),
188  binary_relation_exprt(startpos, ID_le, length_diff));
189  axioms.push_back(a2);
190 
191  symbol_exprt qvar=fresh_univ_index("QA_contains", index_type);
192  exprt qvar_shifted=plus_exprt(qvar, startpos);
194  qvar, s1.length(), contains, equal_exprt(s1[qvar], s0[qvar_shifted]));
195  axioms.push_back(a3);
196 
197  // We rewrite the axiom for !contains as:
198  // forall startpos <= |s0|-|s1|. (!contains &&|s0| >= |s1| )
199  // ==> exists witness<|s1|. s1[witness]!=s0[startpos+witness]
201  from_integer(0, index_type),
202  plus_exprt(from_integer(1, index_type), length_diff),
203  and_exprt(not_exprt(contains), s0.axiom_for_is_longer_than(s1)),
204  from_integer(0, index_type), s1.length(), s0, s1);
205  axioms.push_back(a4);
206 
207  return tc_contains;
208 }
The type of an expression.
Definition: type.h:20
Boolean negation.
Definition: std_expr.h:2648
exprt add_axioms_for_is_prefix(const string_exprt &prefix, const string_exprt &str, const exprt &offset)
add axioms stating that the returned expression is true exactly when the first string is a prefix of ...
semantic type conversion
Definition: std_expr.h:1725
Generates string constraints to link results from string functions with their arguments.
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:568
application of (mathematical) function
Definition: std_expr.h:3785
boolean OR
Definition: std_expr.h:1968
argumentst & arguments()
Definition: std_expr.h:3805
exprt add_axioms_for_contains(const function_application_exprt &f)
add axioms corresponding to the String.contains java function
equal_exprt axiom_for_has_length(const exprt &rhs) const
Definition: string_expr.h:120
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:60
The proper Booleans.
Definition: std_types.h:33
exprt add_axioms_for_is_empty(const function_application_exprt &f)
add axioms stating that the returned value is true exactly when the argument string is empty ...
boolean implication
Definition: std_expr.h:1926
equality
Definition: std_expr.h:1082
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
const exprt & length() const
Definition: string_expr.h:35
exprt::operandst argumentst
Definition: std_expr.h:3803
string_exprt add_axioms_for_string_expr(const exprt &expr)
obtain a refined string expression corresponding to string variable of string function call ...
boolean AND
Definition: std_expr.h:1852
exprt add_axioms_for_is_suffix(const function_application_exprt &f, bool swap_arguments=false)
add axioms corresponding to the String.isSuffix java function
inequality
Definition: std_expr.h:1124
The plus expression.
Definition: std_expr.h:702
bitvector_typet index_type()
Definition: c_types.cpp:15
binary_relation_exprt axiom_for_is_longer_than(const string_exprt &rhs) const
Definition: string_expr.h:56
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:46
bool is_empty(const std::string &s)
binary_relation_exprt axiom_for_is_strictly_longer_than(const exprt &rhs) const
Definition: string_expr.h:68
binary minus
Definition: std_expr.h:758
Expression to hold a symbol (variable)
Definition: std_expr.h:82
int8_t s1
Definition: bytecode_info.h:59
std::map< string_not_contains_constraintt, symbol_exprt > witness
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
static const function_application_exprt::argumentst & args(const function_application_exprt &expr, size_t nb)
exprt axiom_for_is_positive_index(const exprt &x)
expression true exactly when the index is positive