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 }
function_application_exprt::arguments
argumentst & arguments()
Definition: std_expr.h:4506
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
typet::subtype
const typet & subtype() const
Definition: type.h:38
add_axioms_for_substring
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(start,...
Definition: string_constraint_generator_transformation.cpp:124
minimum
exprt minimum(const exprt &a, const exprt &b)
Definition: string_constraint_generator_main.cpp:578
length_constraint_for_insert
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.
Definition: string_constraint_generator_insert.cpp:80
typet
The type of an expression, extends irept.
Definition: type.h:27
add_axioms_from_char
std::pair< exprt, string_constraintst > add_axioms_from_char(const function_application_exprt &f, array_poolt &array_pool)
Conversion from char to string.
Definition: string_constraint_generator_valueof.cpp:294
add_axioms_for_string_of_float
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.
Definition: string_constraint_generator_float.cpp:158
array_poolt
Correspondance between arrays and pointers string representations.
Definition: string_constraint_generator.h:49
string_constraintt
Definition: string_constraint.h:58
s1
int8_t s1
Definition: bytecode_info.h:59
string_refinement_invariant.h
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
exprt
Base class for all expressions.
Definition: expr.h:54
char_array_of_pointer
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.
Definition: string_constraint_generator_main.cpp:325
string_constraintst
Collection of constraints of different types: existential formulas, universal formulas,...
Definition: string_constraint_generator.h:108
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
equal_exprt
Equality.
Definition: std_expr.h:1484
combine_results
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 ...
Definition: string_constraint_generator_main.cpp:598
get_string_expr
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...
Definition: string_constraint_generator_main.cpp:210
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
symbol_generatort
Generation of fresh symbols of a given type.
Definition: string_constraint_generator.h:32
maximum
exprt maximum(const exprt &a, const exprt &b)
Definition: string_constraint_generator_main.cpp:583
deprecate.h
add_axioms_for_insert_float
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.
Definition: string_constraint_generator_insert.cpp:252
add_axioms_for_insert_double
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
Definition: string_constraint_generator_insert.cpp:223
function_application_exprt
Application of (mathematical) function.
Definition: std_expr.h:4481
get_return_code_type
signedbv_typet get_return_code_type()
Definition: string_constraint_generator_main.cpp:339
add_axioms_for_insert_bool
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
Definition: string_constraint_generator_insert.cpp:171
add_axioms_for_insert_char
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.
Definition: string_constraint_generator_insert.cpp:196
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
add_axioms_for_insert_int
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
Definition: string_constraint_generator_insert.cpp:144
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
zero_if_negative
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
Definition: string_constraint_generator_main.cpp:591
array_string_exprt::length
exprt & length()
Definition: string_expr.h:70
add_axioms_from_bool
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.
Definition: string_constraint_generator_valueof.cpp:66
add_axioms_for_string_of_int
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....
Definition: string_constraint_generator_valueof.cpp:132
add_axioms_for_insert
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.
Definition: string_constraint_generator_insert.cpp:33
s2
int16_t s2
Definition: bytecode_info.h:60
string_constraint_generator.h
array_string_exprt
Definition: string_expr.h:67
array_poolt::fresh_string
array_string_exprt fresh_string(const typet &index_type, const typet &char_type)
construct a string expression whose length and content are new variables
Definition: string_constraint_generator_main.cpp:87
string_constraintst::existential
std::vector< exprt > existential
Definition: string_constraint_generator.h:110
string_constraintst::universal
std::vector< string_constraintt > universal
Definition: string_constraint_generator.h:111