cprover
string_concatenation_builtin_function.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Builtin functions for string concatenations
4 
5 Author: 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 
52 std::pair<exprt, string_constraintst>
54  const array_string_exprt &res,
55  const array_string_exprt &s1,
56  const array_string_exprt &s2,
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),
131  plus_exprt(
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),
145  plus_exprt(
146  array_pool.get_or_create_length(s1), from_integer(1, s1.length_type())));
147 }
148 
157 std::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 
172 std::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 = 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  }
222  UNREACHABLE;
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)
234  result, input1, input2, args[0], args[1], array_pool);
235  UNREACHABLE;
236 }
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:504
function_application_exprt::arguments
argumentst & arguments()
Definition: mathematical_expr.h:221
sum_overflows
exprt sum_overflows(const plus_exprt &sum)
Definition: string_constraint_generator_main.cpp:39
length_constraint_for_concat
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
Definition: string_concatenation_builtin_function.cpp:123
string_concatenation_builtin_functiont::string_concatenation_builtin_functiont
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.
Definition: string_concatenation_builtin_function.cpp:16
string_concatenation_builtin_function.h
Builtin functions for string concatenations.
array_string_exprt::length_type
const typet & length_type() const
Definition: string_expr.h:69
typet::subtype
const typet & subtype() const
Definition: type.h:47
string_insertion_builtin_functiont
String inserting a string into another one.
Definition: string_insertion_builtin_function.h:16
array_poolt::find
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:182
minimum
exprt minimum(const exprt &a, const exprt &b)
Definition: string_constraint_generator_main.cpp:395
integer_bitvector_typet::largest_expr
constant_exprt largest_expr() const
Return an expression representing the largest value of this type.
Definition: std_types.cpp:186
typet
The type of an expression, extends irept.
Definition: type.h:29
array_poolt
Correspondance between arrays and pointers string representations.
Definition: array_pool.h:43
string_builtin_functiont::return_code
exprt return_code
Definition: string_builtin_function.h:112
string_constraintt
Definition: string_constraint.h:60
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
string_constraint_generatort::fresh_symbol
symbol_generatort fresh_symbol
Definition: string_constraint_generator.h:56
s1
int8_t s1
Definition: bytecode_info.h:59
array_poolt::get_or_create_length
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:24
get_string_expr
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:196
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:881
exprt
Base class for all expressions.
Definition: expr.h:53
string_constraintst
Collection of constraints of different types: existential formulas, universal formulas,...
Definition: string_constraint_generator.h:36
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
equal_exprt
Equality.
Definition: std_expr.h:1190
string_constraint_generatort::array_pool
array_poolt array_pool
Definition: string_constraint_generator.h:58
string_constraint_generatort
Definition: string_constraint_generator.h:45
string_builtin_functiont::array_pool
array_poolt & array_pool
Definition: string_builtin_function.h:123
string_insertion_builtin_functiont::input1
array_string_exprt input1
Definition: string_insertion_builtin_function.h:19
string_concatenation_builtin_functiont::length_constraint
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
Definition: string_concatenation_builtin_function.cpp:228
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
string_constraint_generatort::add_axioms_for_concat_code_point
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.
Definition: string_concatenation_builtin_function.cpp:173
string_insertion_builtin_functiont::result
array_string_exprt result
Definition: string_insertion_builtin_function.h:18
maximum
exprt maximum(const exprt &a, const exprt &b)
Definition: string_constraint_generator_main.cpp:400
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
function_application_exprt
Application of (mathematical) function.
Definition: mathematical_expr.h:191
irept::id
const irep_idt & id() const
Definition: irep.h:418
get_return_code_type
signedbv_typet get_return_code_type()
Definition: string_constraint_generator_main.cpp:180
length_constraint_for_concat_char
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.
Definition: string_concatenation_builtin_function.cpp:138
minus_exprt
Binary minus.
Definition: std_expr.h:940
string_concatenation_builtin_functiont::constraints
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...
Definition: string_concatenation_builtin_function.cpp:210
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
zero_if_negative
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
Definition: string_constraint_generator_main.cpp:408
to_signedbv_type
const signedbv_typet & to_signedbv_type(const typet &type)
Cast a typet to a signedbv_typet.
Definition: std_types.h:1298
string_constraint_generatort::add_axioms_for_concat_substr
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 ‘...
Definition: string_concatenation_builtin_function.cpp:53
string_constraint_generatort::combine_results
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 ...
Definition: string_constraint_generator_main.cpp:416
string_constraint_generatort::add_axioms_for_concat
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.
Definition: string_concatenation_builtin_function.cpp:158
length_constraint_for_concat_substr
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 ...
Definition: string_concatenation_builtin_function.cpp:100
string_insertion_builtin_functiont::input2
array_string_exprt input2
Definition: string_insertion_builtin_function.h:20
string_insertion_builtin_functiont::args
std::vector< exprt > args
Definition: string_insertion_builtin_function.h:21
s2
int16_t s2
Definition: bytecode_info.h:60
string_concatenation_builtin_functiont::eval
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.
Definition: string_concatenation_builtin_function.cpp:189
string_constraint_generatort::add_axioms_for_code_point
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
Definition: string_constraint_generator_code_points.cpp:21
array_string_exprt
Definition: string_expr.h:67
array_poolt::fresh_string
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:55
string_constraintst::existential
std::vector< exprt > existential
Definition: string_constraint_generator.h:37
string_constraintst::universal
std::vector< string_constraintt > universal
Definition: string_constraint_generator.h:38