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, offset));
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, s2.length(), equal_exprt(res[plus_exprt(i, offset1)], s2[i]));
57  }());
58 
59  // Axiom 4.
60  constraints.push_back([&] { // NOLINT
61  const symbol_exprt i = fresh_symbol("QA_insert3", index_type);
62  return string_constraintt(
63  i,
64  offset1,
65  s1.length(),
66  equal_exprt(res[plus_exprt(i, s2.length())], s1[i]));
67  }());
68 
70 }
71 
75  const array_string_exprt &res,
76  const array_string_exprt &s1,
77  const array_string_exprt &s2,
78  const exprt &offset)
79 {
80  return equal_exprt(res.length(), plus_exprt(s1.length(), s2.length()));
81 }
82 
88 // NOLINTNEXTLINE
102 {
103  PRECONDITION(f.arguments().size() == 5 || f.arguments().size() == 7);
106  array_string_exprt res =
107  char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
108  const exprt &offset = f.arguments()[3];
109  if(f.arguments().size() == 7)
110  {
111  const exprt &start = f.arguments()[5];
112  const exprt &end = f.arguments()[6];
113  const typet &char_type = s1.content().type().subtype();
114  const typet &index_type = s1.length().type();
116  exprt return_code1 = add_axioms_for_substring(substring, s2, start, end);
117  exprt return_code2 = add_axioms_for_insert(res, s1, substring, offset);
118  return if_exprt(
119  equal_exprt(return_code1, from_integer(0, return_code1.type())),
120  return_code2,
121  return_code1);
122  }
123  else // 5 arguments
124  {
125  return add_axioms_for_insert(res, s1, s2, offset);
126  }
127 }
128 
134 DEPRECATED("should convert the value to string and call insert")
135 exprt string_constraint_generatort::add_axioms_for_insert_int(
137 {
138  PRECONDITION(f.arguments().size() == 5);
139  const array_string_exprt s1 = get_string_expr(f.arguments()[2]);
140  const array_string_exprt res =
141  char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
142  const exprt &offset = f.arguments()[3];
143  const typet &index_type = s1.length().type();
144  const typet &char_type = s1.content().type().subtype();
145  array_string_exprt s2 = fresh_string(index_type, char_type);
146  exprt return_code = add_axioms_from_int(s2, f.arguments()[4]);
147  return add_axioms_for_insert(res, s1, s2, offset);
148 }
149 
155 DEPRECATED("should convert the value to string and call insert")
156 exprt string_constraint_generatort::add_axioms_for_insert_bool(
158 {
159  PRECONDITION(f.arguments().size() == 5);
160  const array_string_exprt s1 = get_string_expr(f.arguments()[0]);
161  const array_string_exprt res =
162  char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
163  const exprt &offset = f.arguments()[3];
164  const typet &index_type = s1.length().type();
165  const typet &char_type = s1.content().type().subtype();
166  array_string_exprt s2 = fresh_string(index_type, char_type);
167  exprt return_code = add_axioms_from_bool(s2, f.arguments()[4]);
168  return add_axioms_for_insert(res, s1, s2, offset);
169 }
170 
178 {
179  PRECONDITION(f.arguments().size() == 5);
180  const array_string_exprt res =
181  char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
183  const exprt &offset = f.arguments()[3];
184  const typet &index_type = s1.length().type();
185  const typet &char_type = s1.content().type().subtype();
187  exprt return_code = add_axioms_from_char(s2, f.arguments()[4]);
188  return add_axioms_for_insert(res, s1, s2, offset);
189 }
190 
196 DEPRECATED("should convert the value to string and call insert")
197 exprt string_constraint_generatort::add_axioms_for_insert_double(
199 {
200  PRECONDITION(f.arguments().size() == 5);
201  const array_string_exprt res =
202  char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
203  const array_string_exprt s1 = get_string_expr(f.arguments()[2]);
204  const exprt &offset = f.arguments()[3];
205  const typet &index_type = s1.length().type();
206  const typet &char_type = s1.content().type().subtype();
207  const array_string_exprt s2 = fresh_string(index_type, char_type);
208  const exprt return_code =
209  add_axioms_for_string_of_float(s2, f.arguments()[4]);
210  return add_axioms_for_insert(res, s1, s2, offset);
211 }
212 
218 DEPRECATED("should convert the value to string and call insert")
219 exprt string_constraint_generatort::add_axioms_for_insert_float(
221 {
222  return add_axioms_for_insert_double(f);
223 }
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:4531
argumentst & arguments()
Definition: std_expr.h:4564
The trinary if-then-else operator.
Definition: std_expr.h:3361
typet & type()
Definition: expr.h:56
exprt minimum(const exprt &a, const exprt &b)
equality
Definition: std_expr.h:1354
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.
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
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)
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, const exprt &offset)
Add axioms ensuring the length of res corresponds that of s1 where we inserted s2 at position offset...
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.