cprover
string_constraint_generator_concat.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Generates string constraints for functions adding content
4  add the end of strings
5 
6 Author: Romain Brenguier, romain.brenguier@diffblue.com
7 
8 \*******************************************************************/
9 
13 
15 
38  const array_string_exprt &res,
39  const array_string_exprt &s1,
40  const array_string_exprt &s2,
41  const exprt &start_index,
42  const exprt &end_index)
43 {
44  const typet &index_type = start_index.type();
45  const exprt start1 = maximum(start_index, from_integer(0, index_type));
46  const exprt end1 = maximum(minimum(end_index, s2.length()), start1);
47 
48  // Axiom 1.
49  lemmas.push_back(
50  length_constraint_for_concat_substr(res, s1, s2, start_index, end_index));
51 
52  // Axiom 2.
53  constraints.push_back([&] { // NOLINT
54  const symbol_exprt idx =
55  fresh_univ_index("QA_index_concat", res.length().type());
56  return string_constraintt(idx, s1.length(), equal_exprt(s1[idx], res[idx]));
57  }());
58 
59  // Axiom 3.
60  constraints.push_back([&] { // NOLINT
61  const symbol_exprt idx2 =
62  fresh_univ_index("QA_index_concat2", res.length().type());
63  const equal_exprt res_eq(
64  res[plus_exprt(idx2, s1.length())], s2[plus_exprt(start1, idx2)]);
65  const minus_exprt upper_bound(res.length(), s1.length());
66  return string_constraintt(idx2, upper_bound, res_eq);
67  }());
68 
70 }
71 
78  const array_string_exprt &res,
79  const array_string_exprt &s1,
80  const array_string_exprt &s2,
81  const exprt &start,
82  const exprt &end)
83 {
84  PRECONDITION(res.length().type().id() == ID_signedbv);
85  const exprt start1 = maximum(start, from_integer(0, start.type()));
86  const exprt end1 = maximum(minimum(end, s2.length()), start1);
87  const plus_exprt res_length(s1.length(), minus_exprt(end1, start1));
88  const exprt overflow = sum_overflows(res_length);
89  const exprt max_int = to_signedbv_type(res.length().type()).largest_expr();
90  return equal_exprt(res.length(), if_exprt(overflow, max_int, res_length));
91 }
92 
96  const array_string_exprt &res,
97  const array_string_exprt &s1,
98  const array_string_exprt &s2)
99 {
100  return equal_exprt(res.length(), plus_exprt(s1.length(), s2.length()));
101 }
102 
115  const array_string_exprt &res,
116  const array_string_exprt &s1,
117  const exprt &c)
118 {
119  const typet &index_type = res.length().type();
121 
122  symbol_exprt idx = fresh_univ_index("QA_index_concat_char", index_type);
123  string_constraintt a2(idx, s1.length(), equal_exprt(s1[idx], res[idx]));
124  constraints.push_back(a2);
125 
126  equal_exprt a3(res[s1.length()], c);
127  lemmas.push_back(a3);
128 
129  // We should have a enum type for the possible error codes
130  return from_integer(0, get_return_code_type());
131 }
132 
136  const array_string_exprt &res,
137  const array_string_exprt &s1)
138 {
139  return equal_exprt(
140  res.length(), plus_exprt(s1.length(), from_integer(1, s1.length().type())));
141 }
142 
152  const array_string_exprt &res,
153  const array_string_exprt &s1,
154  const array_string_exprt &s2)
155 {
156  exprt index_zero=from_integer(0, s2.length().type());
157  return add_axioms_for_concat_substr(res, s1, s2, index_zero, s2.length());
158 }
159 
173 {
175  PRECONDITION(args.size() == 4 || args.size() == 6);
176  const array_string_exprt s1 = get_string_expr(args[2]);
177  const array_string_exprt s2 = get_string_expr(args[3]);
178  const array_string_exprt res = char_array_of_pointer(args[1], args[0]);
179  if(args.size() == 6)
180  return add_axioms_for_concat_substr(res, s1, s2, args[4], args[5]);
181  else // args.size()==4
182  return add_axioms_for_concat(res, s1, s2);
183 }
184 
194 {
196  PRECONDITION(args.size() == 4);
197  const array_string_exprt s1 = get_string_expr(args[2]);
198  const exprt &c = args[3];
199  const array_string_exprt res = char_array_of_pointer(args[1], args[0]);
200  return add_axioms_for_concat_char(res, s1, c);
201 }
202 
209 {
210  PRECONDITION(f.arguments().size() == 4);
211  const array_string_exprt res =
212  char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
214  const typet &char_type = s1.content().type().subtype();
215  const typet &index_type = s1.length().type();
217  const exprt return_code1 =
218  add_axioms_for_code_point(code_point, f.arguments()[3]);
219  return add_axioms_for_concat(res, s1, code_point);
220 }
The type of an expression.
Definition: type.h:22
Generates string constraints to link results from string functions with their arguments.
application of (mathematical) function
Definition: std_expr.h:4531
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
Definition: std_types.h:1287
argumentst & arguments()
Definition: std_expr.h:4564
symbol_exprt fresh_univ_index(const irep_idt &prefix, const typet &type)
generate an index symbol to be used as an universaly quantified variable
The trinary if-then-else operator.
Definition: std_expr.h:3361
typet & type()
Definition: expr.h:56
exprt length_constraint_for_concat_substr(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &start, const exprt &end)
Add axioms enforcing that the length of res is that of the concatenation of s1 with the substring of ...
exprt minimum(const exprt &a, const exprt &b)
equality
Definition: std_expr.h:1354
const irep_idt & id() const
Definition: irep.h:189
exprt::operandst argumentst
Definition: std_expr.h:4562
exprt length_constraint_for_concat_char(const array_string_exprt &res, const array_string_exprt &s1)
Add axioms enforcing that the length of res is that of the concatenation of s1 with.
#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 add_axioms_for_concat_substr(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &start_index, const exprt &end_index)
Add axioms enforcing that res is the concatenation of s1 with the substring of s2 starting at index â...
exprt maximum(const exprt &a, const exprt &b)
exprt length_constraint_for_concat(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
Add axioms enforcing that the length of res is that of the concatenation of s1 with s2 ...
Base class for all expressions.
Definition: expr.h:42
exprt add_axioms_for_code_point(const array_string_exprt &res, const exprt &code_point)
add axioms for the conversion of an integer representing a java code point to a utf-16 string ...
Universally quantified string constraint
exprt sum_overflows(const plus_exprt &sum)
binary minus
Definition: std_expr.h:959
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
exprt add_axioms_for_concat_char(const array_string_exprt &res, const array_string_exprt &s1, const exprt &c)
Add axioms enforcing that res is the concatenation of s1 with character c.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
bitvector_typet char_type()
Definition: c_types.cpp:114
exprt add_axioms_for_concat(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
Add axioms enforcing that res is equal to the concatenation of s1 and s2.
exprt add_axioms_for_concat_code_point(const function_application_exprt &f)
Add axioms corresponding to the StringBuilder.appendCodePoint(I) function.
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...