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([&] {
54  const symbol_exprt idx =
55  fresh_univ_index("QA_index_concat", res.length().type());
56  return string_constraintt(
57  idx, zero_if_negative(s1.length()), equal_exprt(s1[idx], res[idx]));
58  }());
59 
60  // Axiom 3.
61  constraints.push_back([&] {
62  const symbol_exprt idx2 =
63  fresh_univ_index("QA_index_concat2", res.length().type());
64  const equal_exprt res_eq(
65  res[plus_exprt(idx2, s1.length())], s2[plus_exprt(start1, idx2)]);
66  const minus_exprt upper_bound(res.length(), s1.length());
67  return string_constraintt(idx2, zero_if_negative(upper_bound), res_eq);
68  }());
69 
71 }
72 
79  const array_string_exprt &res,
80  const array_string_exprt &s1,
81  const array_string_exprt &s2,
82  const exprt &start,
83  const exprt &end)
84 {
85  PRECONDITION(res.length().type().id() == ID_signedbv);
86  const exprt start1 = maximum(start, from_integer(0, start.type()));
87  const exprt end1 = maximum(minimum(end, s2.length()), start1);
88  const plus_exprt res_length(s1.length(), minus_exprt(end1, start1));
89  const exprt overflow = sum_overflows(res_length);
90  const exprt max_int = to_signedbv_type(res.length().type()).largest_expr();
91  return equal_exprt(res.length(), if_exprt(overflow, max_int, res_length));
92 }
93 
97  const array_string_exprt &res,
98  const array_string_exprt &s1,
99  const array_string_exprt &s2)
100 {
101  return equal_exprt(res.length(), plus_exprt(s1.length(), s2.length()));
102 }
103 
116  const array_string_exprt &res,
117  const array_string_exprt &s1,
118  const exprt &c)
119 {
120  const typet &index_type = res.length().type();
122 
123  symbol_exprt idx = fresh_univ_index("QA_index_concat_char", index_type);
125  idx, zero_if_negative(s1.length()), equal_exprt(s1[idx], res[idx]));
126  constraints.push_back(a2);
127 
128  equal_exprt a3(res[s1.length()], c);
129  lemmas.push_back(a3);
130 
131  // We should have a enum type for the possible error codes
132  return from_integer(0, get_return_code_type());
133 }
134 
138  const array_string_exprt &res,
139  const array_string_exprt &s1)
140 {
141  return equal_exprt(
142  res.length(), plus_exprt(s1.length(), from_integer(1, s1.length().type())));
143 }
144 
154  const array_string_exprt &res,
155  const array_string_exprt &s1,
156  const array_string_exprt &s2)
157 {
158  exprt index_zero=from_integer(0, s2.length().type());
159  return add_axioms_for_concat_substr(res, s1, s2, index_zero, s2.length());
160 }
161 
175 {
177  PRECONDITION(args.size() == 4 || args.size() == 6);
178  const array_string_exprt s1 = get_string_expr(args[2]);
179  const array_string_exprt s2 = get_string_expr(args[3]);
180  const array_string_exprt res = char_array_of_pointer(args[1], args[0]);
181  if(args.size() == 6)
182  return add_axioms_for_concat_substr(res, s1, s2, args[4], args[5]);
183  else // args.size()==4
184  return add_axioms_for_concat(res, s1, s2);
185 }
186 
196 {
198  PRECONDITION(args.size() == 4);
199  const array_string_exprt s1 = get_string_expr(args[2]);
200  const exprt &c = args[3];
201  const array_string_exprt res = char_array_of_pointer(args[1], args[0]);
202  return add_axioms_for_concat_char(res, s1, c);
203 }
204 
211 {
212  PRECONDITION(f.arguments().size() == 4);
213  const array_string_exprt res =
214  char_array_of_pointer(f.arguments()[1], f.arguments()[0]);
216  const typet &char_type = s1.content().type().subtype();
217  const typet &index_type = s1.length().type();
219  const exprt return_code1 =
220  add_axioms_for_code_point(code_point, f.arguments()[3]);
221  return add_axioms_for_concat(res, s1, code_point);
222 }
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:4529
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a generic typet to a signedbv_typet.
Definition: std_types.h:1296
argumentst & arguments()
Definition: std_expr.h:4562
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:3359
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:259
exprt::operandst argumentst
Definition: std_expr.h:4560
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:242
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 zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
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...