cprover
string_constraint_generator_insert.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Generates string constraints for the family of insert Java functions
4 
5 Author: Romain Brenguier, romain.brenguier@diffblue.com
6 
7 \*******************************************************************/
8 
11 
14 #include <util/deprecate.h>
15 
33  const array_string_exprt &res,
34  const array_string_exprt &s1,
35  const array_string_exprt &s2,
36  const exprt &offset)
37 {
38  PRECONDITION(offset.type()==s1.length().type());
39  const typet &index_type = s1.length().type();
40  const exprt offset1 =
41  maximum(from_integer(0, index_type), minimum(s1.length(), offset));
42 
43  // Axiom 1.
44  lemmas.push_back(length_constraint_for_insert(res, s1, s2));
45 
46  // Axiom 2.
47  constraints.push_back([&] { // NOLINT
48  const symbol_exprt i = fresh_symbol("QA_insert1", index_type);
49  return string_constraintt(i, offset1, equal_exprt(res[i], s1[i]));
50  }());
51 
52  // Axiom 3.
53  constraints.push_back([&] { // NOLINT
54  const symbol_exprt i = fresh_symbol("QA_insert2", index_type);
55  return string_constraintt(
56  i,
57  zero_if_negative(s2.length()),
58  equal_exprt(res[plus_exprt(i, offset1)], s2[i]));
59  }());
60 
61  // Axiom 4.
62  constraints.push_back([&] { // NOLINT
63  const symbol_exprt i = fresh_symbol("QA_insert3", index_type);
64  return string_constraintt(
65  i,
66  offset1,
67  zero_if_negative(s1.length()),
68  equal_exprt(res[plus_exprt(i, s2.length())], s1[i]));
69  }());
70 
72 }
73 
77  const array_string_exprt &res,
78  const array_string_exprt &s1,
79  const array_string_exprt &s2)
80 {
81  return equal_exprt(res.length(), plus_exprt(s1.length(), s2.length()));
82 }
83 
89 // NOLINTNEXTLINE
103 {
104  PRECONDITION(f.arguments().size() == 5 || f.arguments().size() == 7);
107  array_string_exprt res =
108  char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
109  const exprt &offset = f.arguments()[3];
110  if(f.arguments().size() == 7)
111  {
112  const exprt &start = f.arguments()[5];
113  const exprt &end = f.arguments()[6];
114  const typet &char_type = s1.content().type().subtype();
115  const typet &index_type = s1.length().type();
117  exprt return_code1 = add_axioms_for_substring(substring, s2, start, end);
118  exprt return_code2 = add_axioms_for_insert(res, s1, substring, offset);
119  return if_exprt(
120  equal_exprt(return_code1, from_integer(0, return_code1.type())),
121  return_code2,
122  return_code1);
123  }
124  else // 5 arguments
125  {
126  return add_axioms_for_insert(res, s1, s2, offset);
127  }
128 }
129 
135 DEPRECATED("should convert the value to string and call insert")
136 exprt string_constraint_generatort::add_axioms_for_insert_int(
138 {
139  PRECONDITION(f.arguments().size() == 5);
140  const array_string_exprt s1 = get_string_expr(f.arguments()[2]);
141  const array_string_exprt res =
142  char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
143  const exprt &offset = f.arguments()[3];
144  const typet &index_type = s1.length().type();
145  const typet &char_type = s1.content().type().subtype();
146  array_string_exprt s2 = fresh_string(index_type, char_type);
147  exprt return_code = add_axioms_for_string_of_int(s2, f.arguments()[4]);
148  return add_axioms_for_insert(res, s1, s2, offset);
149 }
150 
156 DEPRECATED("should convert the value to string and call insert")
157 exprt string_constraint_generatort::add_axioms_for_insert_bool(
159 {
160  PRECONDITION(f.arguments().size() == 5);
161  const array_string_exprt s1 = get_string_expr(f.arguments()[0]);
162  const array_string_exprt res =
163  char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
164  const exprt &offset = f.arguments()[3];
165  const typet &index_type = s1.length().type();
166  const typet &char_type = s1.content().type().subtype();
167  array_string_exprt s2 = fresh_string(index_type, char_type);
168  exprt return_code = add_axioms_from_bool(s2, f.arguments()[4]);
169  return add_axioms_for_insert(res, s1, s2, offset);
170 }
171 
179 {
180  PRECONDITION(f.arguments().size() == 5);
181  const array_string_exprt res =
182  char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
184  const exprt &offset = f.arguments()[3];
185  const typet &index_type = s1.length().type();
186  const typet &char_type = s1.content().type().subtype();
188  exprt return_code = add_axioms_from_char(s2, f.arguments()[4]);
189  return add_axioms_for_insert(res, s1, s2, offset);
190 }
191 
197 DEPRECATED("should convert the value to string and call insert")
198 exprt string_constraint_generatort::add_axioms_for_insert_double(
200 {
201  PRECONDITION(f.arguments().size() == 5);
202  const array_string_exprt res =
203  char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
204  const array_string_exprt s1 = get_string_expr(f.arguments()[2]);
205  const exprt &offset = f.arguments()[3];
206  const typet &index_type = s1.length().type();
207  const typet &char_type = s1.content().type().subtype();
208  const array_string_exprt s2 = fresh_string(index_type, char_type);
209  const exprt return_code =
210  add_axioms_for_string_of_float(s2, f.arguments()[4]);
211  return add_axioms_for_insert(res, s1, s2, offset);
212 }
213 
219 DEPRECATED("should convert the value to string and call insert")
220 exprt string_constraint_generatort::add_axioms_for_insert_float(
222 {
223  return add_axioms_for_insert_double(f);
224 }
The type of an expression.
Definition: type.h:22
exprt add_axioms_for_insert(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &offset)
Add axioms ensuring the result res corresponds to s1 where we inserted s2 at position offset...
Generates string constraints to link results from string functions with their arguments.
application of (mathematical) function
Definition: std_expr.h:4529
argumentst & arguments()
Definition: std_expr.h:4562
The trinary if-then-else operator.
Definition: std_expr.h:3359
typet & type()
Definition: expr.h:56
exprt minimum(const exprt &a, const exprt &b)
equality
Definition: std_expr.h:1354
#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.
exprt add_axioms_for_substring(const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end)
Add axioms ensuring that res corresponds to the substring of str between indexes ‘start’ = max(st...
Base class for all expressions.
Definition: expr.h:42
exprt length_constraint_for_insert(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
Add axioms ensuring the length of res corresponds to that of s1 where we inserted s2...
Universally quantified string constraint
Expression to hold a symbol (variable)
Definition: std_expr.h:90
int8_t s1
Definition: bytecode_info.h:59
int16_t s2
Definition: bytecode_info.h:60
const array_string_exprt & char_array_of_pointer(const exprt &pointer, const exprt &length)
Adds creates a new array if it does not already exists.
const typet & subtype() const
Definition: type.h:33
std::vector< string_constraintt > constraints
array_string_exprt fresh_string(const typet &index_type, const typet &char_type)
construct a string expression whose length and content are new variables
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
exprt add_axioms_from_char(const function_application_exprt &f)
Conversion from char to string.
bitvector_typet char_type()
Definition: c_types.cpp:114
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 add_axioms_for_insert_char(const function_application_exprt &f)
Add axioms corresponding to the StringBuilder.insert(C) java function.