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 std::pair<exprt, string_constraintst> add_axioms_for_insert(
34  symbol_generatort &fresh_symbol,
35  const array_string_exprt &res,
36  const array_string_exprt &s1,
37  const array_string_exprt &s2,
38  const exprt &offset)
39 {
40  PRECONDITION(offset.type()==s1.length().type());
41 
42  string_constraintst constraints;
43  const typet &index_type = s1.length().type();
44  const exprt offset1 =
45  maximum(from_integer(0, index_type), minimum(s1.length(), offset));
46 
47  // Axiom 1.
48  constraints.existential.push_back(length_constraint_for_insert(res, s1, s2));
49 
50  // Axiom 2.
51  constraints.universal.push_back([&] { // NOLINT
52  const symbol_exprt i = fresh_symbol("QA_insert1", index_type);
53  return string_constraintt(i, offset1, equal_exprt(res[i], s1[i]));
54  }());
55 
56  // Axiom 3.
57  constraints.universal.push_back([&] { // NOLINT
58  const symbol_exprt i = fresh_symbol("QA_insert2", index_type);
59  return string_constraintt(
60  i,
61  zero_if_negative(s2.length()),
62  equal_exprt(res[plus_exprt(i, offset1)], s2[i]));
63  }());
64 
65  // Axiom 4.
66  constraints.universal.push_back([&] { // NOLINT
67  const symbol_exprt i = fresh_symbol("QA_insert3", index_type);
68  return string_constraintt(
69  i,
70  offset1,
71  zero_if_negative(s1.length()),
72  equal_exprt(res[plus_exprt(i, s2.length())], s1[i]));
73  }());
74 
75  return {from_integer(0, get_return_code_type()), std::move(constraints)};
76 }
77 
81  const array_string_exprt &res,
82  const array_string_exprt &s1,
83  const array_string_exprt &s2)
84 {
85  return equal_exprt(res.length(), plus_exprt(s1.length(), s2.length()));
86 }
87 
90 // NOLINTNEXTLINE
92 // NOLINTNEXTLINE
106 std::pair<exprt, string_constraintst> add_axioms_for_insert(
107  symbol_generatort &fresh_symbol,
109  array_poolt &pool)
110 {
111  PRECONDITION(f.arguments().size() == 5 || f.arguments().size() == 7);
114  array_string_exprt res =
115  char_array_of_pointer(pool, f.arguments()[1], f.arguments()[0]);
116  const exprt &offset = f.arguments()[3];
117  if(f.arguments().size() == 7)
118  {
119  const exprt &start = f.arguments()[5];
120  const exprt &end = f.arguments()[6];
121  const typet &char_type = s1.content().type().subtype();
122  const typet &index_type = s1.length().type();
123  const array_string_exprt substring =
125  return combine_results(
126  add_axioms_for_substring(fresh_symbol, substring, s2, start, end),
127  add_axioms_for_insert(fresh_symbol, res, s1, substring, offset));
128  }
129  else // 5 arguments
130  {
131  return add_axioms_for_insert(fresh_symbol, res, s1, s2, offset);
132  }
133 }
134 
143 DEPRECATED("should convert the value to string and call insert")
145  symbol_generatort &fresh_symbol,
147  array_poolt &array_pool,
148  const namespacet &ns)
149 {
150  PRECONDITION(f.arguments().size() == 5);
151  const array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[2]);
152  const array_string_exprt res =
153  char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
154  const exprt &offset = f.arguments()[3];
155  const typet &index_type = s1.length().type();
156  const typet &char_type = s1.content().type().subtype();
157  const array_string_exprt s2 = array_pool.fresh_string(index_type, char_type);
158  return combine_results(
159  add_axioms_for_string_of_int(s2, f.arguments()[4], 0, ns),
160  add_axioms_for_insert(fresh_symbol, res, s1, s2, offset));
161 }
162 
170 DEPRECATED("should convert the value to string and call insert")
172  symbol_generatort &fresh_symbol,
174  array_poolt &array_pool)
175 {
176  PRECONDITION(f.arguments().size() == 5);
177  const array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[0]);
178  const array_string_exprt res =
179  char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
180  const exprt &offset = f.arguments()[3];
181  const typet &index_type = s1.length().type();
182  const typet &char_type = s1.content().type().subtype();
183  const array_string_exprt s2 = array_pool.fresh_string(index_type, char_type);
184  return combine_results(
185  add_axioms_from_bool(s2, f.arguments()[4]),
186  add_axioms_for_insert(fresh_symbol, res, s1, s2, offset));
187 }
188 
196 std::pair<exprt, string_constraintst> add_axioms_for_insert_char(
197  symbol_generatort &fresh_symbol,
199  array_poolt &array_pool)
200 {
201  PRECONDITION(f.arguments().size() == 5);
202  const array_string_exprt res =
203  char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
204  const array_string_exprt s1 = get_string_expr(array_pool, 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();
209  return combine_results(
211  add_axioms_for_insert(fresh_symbol, res, s1, s2, offset));
212 }
213 
222 DEPRECATED("should convert the value to string and call insert")
224  symbol_generatort &fresh_symbol,
226  array_poolt &array_pool,
227  const namespacet &ns)
228 {
229  PRECONDITION(f.arguments().size() == 5);
230  const array_string_exprt res =
231  char_array_of_pointer(array_pool, f.arguments()[1], f.arguments()[0]);
232  const array_string_exprt s1 = get_string_expr(array_pool, f.arguments()[2]);
233  const exprt &offset = f.arguments()[3];
234  const typet &index_type = s1.length().type();
235  const typet &char_type = s1.content().type().subtype();
236  const array_string_exprt s2 = array_pool.fresh_string(index_type, char_type);
237  return combine_results(
239  fresh_symbol, s2, f.arguments()[4], array_pool, ns),
240  add_axioms_for_insert(fresh_symbol, res, s1, s2, offset));
241 }
242 
251 DEPRECATED("should convert the value to string and call insert")
253  symbol_generatort &fresh_symbol,
255  array_poolt &array_pool,
256  const namespacet &ns)
257 {
258  return add_axioms_for_insert_double(fresh_symbol, f, array_pool, ns);
259 }
The type of an expression, extends irept.
Definition: type.h:27
std::pair< exprt, string_constraintst > add_axioms_for_insert(symbol_generatort &fresh_symbol, 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:4481
array_string_exprt fresh_string(const typet &index_type, const typet &char_type)
construct a string expression whose length and content are new variables
std::pair< exprt, string_constraintst > add_axioms_for_string_of_float(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
String representation of a float value.
Generation of fresh symbols of a given type.
argumentst & arguments()
Definition: std_expr.h:4506
std::pair< exprt, string_constraintst > add_axioms_from_char(const function_application_exprt &f, array_poolt &array_pool)
Conversion from char to string.
typet & type()
Return the type of the expression.
Definition: expr.h:68
signedbv_typet get_return_code_type()
std::pair< exprt, string_constraintst > add_axioms_from_bool(const function_application_exprt &f, array_poolt &array_pool)
Add axioms corresponding to the String.valueOf(Z) java function.
Correspondance between arrays and pointers string representations.
Collection of constraints of different types: existential formulas, universal formulas,...
exprt minimum(const exprt &a, const exprt &b)
std::pair< exprt, string_constraintst > combine_results(std::pair< exprt, string_constraintst > result1, std::pair< exprt, string_constraintst > result2)
Combine the results of two add_axioms function by taking the maximum of the return codes and merging ...
Equality.
Definition: std_expr.h:1484
std::pair< exprt, string_constraintst > add_axioms_for_insert_double(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
add axioms corresponding to the StringBuilder.insert(D) java function
std::pair< exprt, string_constraintst > add_axioms_for_insert_float(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
Add axioms corresponding to the StringBuilder.insert(F) java function.
std::pair< exprt, string_constraintst > add_axioms_for_substring(symbol_generatort &fresh_symbol, 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...
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...
std::pair< exprt, string_constraintst > add_axioms_for_insert_bool(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
add axioms corresponding to the StringBuilder.insert(Z) java function
std::pair< exprt, string_constraintst > add_axioms_for_insert_int(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool, const namespacet &ns)
add axioms corresponding to the StringBuilder.insert(I) java function
std::pair< exprt, string_constraintst > add_axioms_for_string_of_int(const array_string_exprt &res, const exprt &input_int, size_t max_size, const namespacet &ns)
Add axioms enforcing that the string corresponds to the result of String.valueOf(I) or String....
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
std::pair< exprt, string_constraintst > add_axioms_for_insert_char(symbol_generatort &fresh_symbol, const function_application_exprt &f, array_poolt &array_pool)
Add axioms corresponding to the StringBuilder.insert(C) java function.
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
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 & length()
Definition: string_expr.h:70
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
const array_string_exprt & char_array_of_pointer(array_poolt &pool, const exprt &pointer, const exprt &length)
Adds creates a new array if it does not already exists.
Base class for all expressions.
Definition: expr.h:54
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.
Expression to hold a symbol (variable)
Definition: std_expr.h:143
int8_t s1
Definition: bytecode_info.h:59
int16_t s2
Definition: bytecode_info.h:60
const typet & subtype() const
Definition: type.h:38
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bitvector_typet char_type()
Definition: c_types.cpp:114