cprover
Loading...
Searching...
No Matches
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);
24 input1 = array_pool.find(arg1.op1(), arg1.op0());
26 input2 = array_pool.find(arg2.op1(), arg2.op0());
28 args.insert(args.end(), fun_args.begin() + 4, fun_args.end());
29}
30
52std::pair<exprt, string_constraintst>
57 const exprt &start_index,
58 const exprt &end_index)
59{
60 string_constraintst constraints;
61 const typet &index_type = start_index.type();
63 const exprt end1 =
65
66 // Axiom 1.
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(
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);
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),
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>
167
172std::pair<exprt, string_constraintst>
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(),
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
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
array_string_exprt get_string_expr(array_poolt &array_pool, const exprt &expr)
Fetch the string_exprt corresponding to the given refined_string_exprt.
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
bitvector_typet index_type()
Definition c_types.cpp:22
bitvector_typet char_type()
Definition c_types.cpp:124
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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.
array_string_exprt fresh_string(const typet &index_type, const typet &char_type)
Construct a string expression whose length and content are new variables.
array_string_exprt find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
Equality.
Definition std_expr.h:1225
Base class for all expressions.
Definition expr.h:54
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.
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 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 ...
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