cprover
string_concatenation_builtin_function.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Builtin functions for string concatenations
4
5Author: Romain Brenguier, Joel Allred
6
7\*******************************************************************/
8
11
13
14#include <algorithm>
15
17 const exprt &return_code,
18 const std::vector<exprt> &fun_args,
19 array_poolt &array_pool)
20 : string_insertion_builtin_functiont(return_code, array_pool)
21{
22 PRECONDITION(fun_args.size() >= 4 && fun_args.size() <= 6);
23 const auto arg1 = expr_checked_cast<struct_exprt>(fun_args[2]);
24 input1 = array_pool.find(arg1.op1(), arg1.op0());
25 const auto arg2 = expr_checked_cast<struct_exprt>(fun_args[3]);
26 input2 = array_pool.find(arg2.op1(), arg2.op0());
27 result = array_pool.find(fun_args[1], fun_args[0]);
28 args.insert(args.end(), fun_args.begin() + 4, fun_args.end());
29}
30
52std::pair<exprt, string_constraintst>
54 const array_string_exprt &res,
57 const exprt &start_index,
58 const exprt &end_index)
59{
60 string_constraintst constraints;
61 const typet &index_type = start_index.type();
62 const exprt start1 = maximum(start_index, from_integer(0, index_type));
63 const exprt end1 =
64 maximum(minimum(end_index, array_pool.get_or_create_length(s2)), start1);
65
66 // Axiom 1.
68 res, s1, s2, start_index, end_index, array_pool));
69
70 // Axiom 2.
71 constraints.universal.push_back([&] {
72 const symbol_exprt idx = fresh_symbol("QA_index_concat", res.length_type());
73 return string_constraintt(
74 idx,
76 equal_exprt(s1[idx], res[idx]));
77 }());
78
79 // Axiom 3.
80 constraints.universal.push_back([&] {
81 const symbol_exprt idx2 =
82 fresh_symbol("QA_index_concat2", res.length_type());
83 const equal_exprt res_eq(
85 s2[plus_exprt(start1, idx2)]);
86 const minus_exprt upper_bound(
89 return string_constraintt(idx2, zero_if_negative(upper_bound), res_eq);
90 }());
91
92 return {from_integer(0, get_return_code_type()), std::move(constraints)};
93}
94
101 const array_string_exprt &res,
102 const array_string_exprt &s1,
103 const array_string_exprt &s2,
104 const exprt &start,
105 const exprt &end,
106 array_poolt &array_pool)
107{
108 PRECONDITION(res.length_type().id() == ID_signedbv);
109 const exprt start1 = maximum(start, from_integer(0, start.type()));
110 const exprt end1 =
111 maximum(minimum(end, array_pool.get_or_create_length(s2)), start1);
112 const plus_exprt res_length(
113 array_pool.get_or_create_length(s1), minus_exprt(end1, start1));
114 const exprt overflow = sum_overflows(res_length);
115 const exprt max_int = to_signedbv_type(res.length_type()).largest_expr();
116 return equal_exprt(
117 array_pool.get_or_create_length(res),
118 if_exprt(overflow, max_int, res_length));
119}
120
124 const array_string_exprt &res,
125 const array_string_exprt &s1,
126 const array_string_exprt &s2,
127 array_poolt &array_pool)
128{
129 return equal_exprt(
130 array_pool.get_or_create_length(res),
132 array_pool.get_or_create_length(s1),
133 array_pool.get_or_create_length(s2)));
134}
135
139 const array_string_exprt &res,
140 const array_string_exprt &s1,
141 array_poolt &array_pool)
142{
143 return equal_exprt(
144 array_pool.get_or_create_length(res),
146 array_pool.get_or_create_length(s1), from_integer(1, s1.length_type())));
147}
148
157std::pair<exprt, string_constraintst>
159 const array_string_exprt &res,
160 const array_string_exprt &s1,
161 const array_string_exprt &s2)
162{
163 exprt index_zero = from_integer(0, s2.length_type());
165 res, s1, s2, index_zero, array_pool.get_or_create_length(s2));
166}
167
172std::pair<exprt, string_constraintst>
175{
176 PRECONDITION(f.arguments().size() == 4);
177 const array_string_exprt res =
178 array_pool.find(f.arguments()[1], f.arguments()[0]);
180 const typet &char_type = to_type_with_subtype(s1.content().type()).subtype();
181 const typet &index_type = s1.length_type();
182 const array_string_exprt code_point =
184 return combine_results(
185 add_axioms_for_code_point(code_point, f.arguments()[3]),
186 add_axioms_for_concat(res, s1, code_point));
187}
188
190 const std::vector<mp_integer> &input1_value,
191 const std::vector<mp_integer> &input2_value,
192 const std::vector<mp_integer> &args_value) const
193{
194 const auto start_index =
195 args_value.size() > 0 && args_value[0] > 0 ? args_value[0] : mp_integer(0);
196 const mp_integer input2_size(input2_value.size());
197 const auto end_index =
198 args_value.size() > 1
199 ? std::max(std::min(args_value[1], input2_size), start_index)
200 : input2_size;
201
202 std::vector<mp_integer> eval_result(input1_value);
203 eval_result.insert(
204 eval_result.end(),
205 input2_value.begin() + numeric_cast_v<std::size_t>(start_index),
206 input2_value.begin() + numeric_cast_v<std::size_t>(end_index));
207 return eval_result;
208}
209
211 string_constraint_generatort &generator) const
212
213{
214 auto pair = [&]() -> std::pair<exprt, string_constraintst> {
215 if(args.size() == 0)
216 return generator.add_axioms_for_concat(result, input1, input2);
217 if(args.size() == 2)
218 {
219 return generator.add_axioms_for_concat_substr(
220 result, input1, input2, args[0], args[1]);
221 }
223 }();
224 pair.second.existential.push_back(equal_exprt(pair.first, return_code));
225 return pair.second;
226}
227
229{
230 if(args.size() == 0)
232 if(args.size() == 2)
236}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
array_string_exprt get_string_expr(array_poolt &array_pool, const exprt &expr)
Fetch the string_exprt corresponding to the given refined_string_exprt.
Definition: array_pool.cpp:199
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
int16_t s2
Definition: bytecode_info.h:60
int8_t s1
Definition: bytecode_info.h:59
bitvector_typet index_type()
Definition: c_types.cpp:22
bitvector_typet char_type()
Definition: c_types.cpp:124
Correspondance between arrays and pointers string representations.
Definition: array_pool.h:42
exprt get_or_create_length(const array_string_exprt &s)
Get the length of an array_string_exprt from the array_pool.
Definition: array_pool.cpp:26
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: array_pool.cpp:57
array_string_exprt find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
Definition: array_pool.cpp:184
const typet & length_type() const
Definition: string_expr.h:69
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
typet & type()
Return the type of the expression.
Definition: expr.h:82
Application of (mathematical) function.
The trinary if-then-else operator.
Definition: std_expr.h:2226
constant_exprt largest_expr() const
Return an expression representing the largest value of this type.
const irep_idt & id() const
Definition: irep.h:396
Binary minus.
Definition: std_expr.h:973
The plus expression Associativity is not specified.
Definition: std_expr.h:914
string_concatenation_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Constructor from arguments of a function application.
string_constraintst constraints(string_constraint_generatort &generator) const override
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
std::vector< mp_integer > eval(const std::vector< mp_integer > &input1_value, const std::vector< mp_integer > &input2_value, const std::vector< mp_integer > &args_value) const override
Evaluate the result from a concrete valuation of the arguments.
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
std::pair< exprt, string_constraintst > 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.
std::pair< exprt, string_constraintst > 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 ‘...
std::pair< exprt, string_constraintst > 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
std::pair< exprt, string_constraintst > add_axioms_for_concat_code_point(const function_application_exprt &f)
Add axioms corresponding to the StringBuilder.appendCodePoint(I) function.
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 ...
String inserting a string into another one.
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const typet & subtype() const
Definition: type.h:156
The type of an expression, extends irept.
Definition: type.h:29
BigInt mp_integer
Definition: smt_terms.h:12
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
exprt length_constraint_for_concat(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, array_poolt &array_pool)
Add axioms enforcing that the length of res is that of the concatenation of s1 with s2
exprt length_constraint_for_concat_char(const array_string_exprt &res, const array_string_exprt &s1, array_poolt &array_pool)
Add axioms enforcing that the length of res is that of the concatenation of s1 with.
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, array_poolt &array_pool)
Add axioms enforcing that the length of res is that of the concatenation of s1 with the substring of ...
Builtin functions for string concatenations.
exprt sum_overflows(const plus_exprt &sum)
exprt maximum(const exprt &a, const exprt &b)
exprt minimum(const exprt &a, const exprt &b)
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
signedbv_typet get_return_code_type()
Collection of constraints of different types: existential formulas, universal formulas,...
std::vector< exprt > existential
std::vector< string_constraintt > universal
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:177