cprover
string_builtin_function.cpp
Go to the documentation of this file.
1 
5 
6 #include <algorithm>
7 #include <iterator>
8 
10 
15  const array_string_exprt &a,
16  const std::function<exprt(const exprt &)> &get_value);
17 
20  const std::vector<mp_integer> &array,
21  const array_typet &array_type);
22 
25  const exprt &return_code,
26  const std::vector<exprt> &fun_args,
27  array_poolt &array_pool)
28  : string_builtin_functiont(return_code)
29 {
30  PRECONDITION(fun_args.size() > 2);
31  const auto arg1 = expr_checked_cast<struct_exprt>(fun_args[2]);
32  input = array_pool.find(arg1.op1(), arg1.op0());
33  result = array_pool.find(fun_args[1], fun_args[0]);
34 }
35 
37  const exprt &return_code,
38  const std::vector<exprt> &fun_args,
39  array_poolt &array_pool)
40  : string_builtin_functiont(return_code)
41 {
42  PRECONDITION(fun_args.size() > 4);
43  const auto arg1 = expr_checked_cast<struct_exprt>(fun_args[2]);
44  input1 = array_pool.find(arg1.op1(), arg1.op0());
45  const auto arg2 = expr_checked_cast<struct_exprt>(fun_args[4]);
46  input2 = array_pool.find(arg2.op1(), arg2.op0());
47  result = array_pool.find(fun_args[1], fun_args[0]);
48  args.push_back(fun_args[3]);
49  args.insert(args.end(), fun_args.begin() + 5, fun_args.end());
50 }
51 
53  const exprt &return_code,
54  const std::vector<exprt> &fun_args,
55  array_poolt &array_pool)
57 {
58  PRECONDITION(fun_args.size() >= 4 && fun_args.size() <= 6);
59  const auto arg1 = expr_checked_cast<struct_exprt>(fun_args[2]);
60  input1 = array_pool.find(arg1.op1(), arg1.op0());
61  const auto arg2 = expr_checked_cast<struct_exprt>(fun_args[3]);
62  input2 = array_pool.find(arg2.op1(), arg2.op0());
63  result = array_pool.find(fun_args[1], fun_args[0]);
64  args.insert(args.end(), fun_args.begin() + 4, fun_args.end());
65 }
66 
68  const array_string_exprt &a,
69  const std::function<exprt(const exprt &)> &get_value)
70 {
71  if(a.id() == ID_if)
72  {
73  const if_exprt &ite = to_if_expr(a);
74  const exprt cond = get_value(ite.cond());
75  if(!cond.is_constant())
76  return {};
77  return cond.is_true()
78  ? eval_string(to_array_string_expr(ite.true_case()), get_value)
79  : eval_string(to_array_string_expr(ite.false_case()), get_value);
80  }
81 
82  const exprt content = get_value(a.content());
83  const auto &array = expr_try_dynamic_cast<array_exprt>(content);
84  if(!array)
85  return {};
86 
87  const auto &ops = array->operands();
88  std::vector<mp_integer> result;
89  const mp_integer unknown('?');
90  const auto &insert = std::back_inserter(result);
91  std::transform(
92  ops.begin(), ops.end(), insert, [unknown](const exprt &e) { // NOLINT
93  if(const auto i = numeric_cast<mp_integer>(e))
94  return *i;
95  return unknown;
96  });
97  return result;
98 }
99 
100 template <typename Iter>
101 static array_string_exprt
102 make_string(Iter begin, Iter end, const array_typet &array_type)
103 {
104  const typet &char_type = array_type.subtype();
105  array_exprt array_expr(array_type);
106  const auto &insert = std::back_inserter(array_expr.operands());
107  std::transform(begin, end, insert, [&](const mp_integer &i) {
108  return from_integer(i, char_type);
109  });
110  return to_array_string_expr(array_expr);
111 }
112 
113 static array_string_exprt
114 make_string(const std::vector<mp_integer> &array, const array_typet &array_type)
115 {
116  return make_string(array.begin(), array.end(), array_type);
117 }
118 
120  const std::vector<mp_integer> &input1_value,
121  const std::vector<mp_integer> &input2_value,
122  const std::vector<mp_integer> &args_value) const
123 {
124  const auto start_index =
125  args_value.size() > 0 && args_value[0] > 0 ? args_value[0] : mp_integer(0);
126  const mp_integer input2_size(input2_value.size());
127  const auto end_index =
128  args_value.size() > 1
129  ? std::max(std::min(args_value[1], input2_size), start_index)
130  : input2_size;
131 
132  std::vector<mp_integer> result(input1_value);
133  result.insert(
134  result.end(),
135  input2_value.begin() + numeric_cast_v<std::size_t>(start_index),
136  input2_value.begin() + numeric_cast_v<std::size_t>(end_index));
137  return result;
138 }
139 
141  const std::function<exprt(const exprt &)> &get_value) const
142 {
143  auto input_opt = eval_string(input, get_value);
144  if(!input_opt.has_value())
145  return {};
146  const mp_integer char_val = [&] {
147  if(const auto val = numeric_cast<mp_integer>(get_value(character)))
148  return *val;
149  INVARIANT(
150  get_value(character).id() == ID_unknown,
151  "character valuation should only contain constants and unknown");
153  }();
154  input_opt.value().push_back(char_val);
155  const auto length =
156  from_integer(input_opt.value().size(), result.length().type());
157  const array_typet type(result.type().subtype(), length);
158  return make_string(input_opt.value(), type);
159 }
160 
162  const std::function<exprt(const exprt &)> &get_value) const
163 {
164  auto input_opt = eval_string(input, get_value);
165  const auto char_opt = numeric_cast<mp_integer>(get_value(character));
166  const auto position_opt = numeric_cast<mp_integer>(get_value(position));
167  if(!input_opt || !char_opt || !position_opt)
168  return {};
169  if(0 <= *position_opt && *position_opt < input_opt.value().size())
170  input_opt.value()[numeric_cast_v<std::size_t>(*position_opt)] = *char_opt;
171  const auto length =
172  from_integer(input_opt.value().size(), result.length().type());
173  const array_typet type(result.type().subtype(), length);
174  return make_string(input_opt.value(), type);
175 }
176 
178 {
179  const exprt out_of_bounds = or_exprt(
182  position, ID_le, from_integer(0, input.length().type())));
183  const exprt return_value = if_exprt(
184  out_of_bounds,
187  return and_exprt(
189  equal_exprt(return_code, return_value));
190 }
191 
192 static bool eval_is_upper_case(const mp_integer &c)
193 {
194  // Characters between 'A' and 'Z' are upper-case
195  // Characters between 0xc0 (latin capital A with grave)
196  // and 0xd6 (latin capital O with diaeresis) are upper-case
197  // Characters between 0xd8 (latin capital O with stroke)
198  // and 0xde (latin capital thorn) are upper-case
199  return ('A' <= c && c <= 'Z') || (0xc0 <= c && c <= 0xd6) ||
200  (0xd8 <= c && c <= 0xde);
201 }
202 
204  const std::function<exprt(const exprt &)> &get_value) const
205 {
206  auto input_opt = eval_string(input, get_value);
207  if(!input_opt)
208  return {};
209  for(mp_integer &c : input_opt.value())
210  {
211  if(eval_is_upper_case(c))
212  c += 0x20;
213  }
214  const auto length =
215  from_integer(input_opt.value().size(), result.length().type());
216  const array_typet type(result.type().subtype(), length);
217  return make_string(input_opt.value(), type);
218 }
219 
221  const std::function<exprt(const exprt &)> &get_value) const
222 {
223  auto input_opt = eval_string(input, get_value);
224  if(!input_opt)
225  return {};
226  for(mp_integer &c : input_opt.value())
227  {
228  if(eval_is_upper_case(c - 0x20))
229  c -= 0x20;
230  }
231  const auto length =
232  from_integer(input_opt.value().size(), result.length().type());
233  const array_typet type(result.type().subtype(), length);
234  return make_string(input_opt.value(), type);
235 }
236 
238  const std::vector<mp_integer> &input1_value,
239  const std::vector<mp_integer> &input2_value,
240  const std::vector<mp_integer> &args_value) const
241 {
242  PRECONDITION(args_value.size() >= 1 || args_value.size() <= 3);
243  const auto offset = std::min(
244  std::max(args_value[0], mp_integer(0)), mp_integer(input1_value.size()));
245  const auto start = args_value.size() > 1
246  ? std::max(args_value[1], mp_integer(0))
247  : mp_integer(0);
248 
249  const mp_integer input2_size(input2_value.size());
250  const auto end =
251  args_value.size() > 2
252  ? std::max(std::min(args_value[2], input2_size), mp_integer(0))
253  : input2_size;
254 
255  std::vector<mp_integer> result(input1_value);
256  result.insert(
257  result.begin() + numeric_cast_v<std::size_t>(offset),
258  input2_value.begin() + numeric_cast_v<std::size_t>(start),
259  input2_value.begin() + numeric_cast_v<std::size_t>(end));
260  return result;
261 }
262 
264  const std::function<exprt(const exprt &)> &get_value) const
265 {
266  const auto &input1_value = eval_string(input1, get_value);
267  const auto &input2_value = eval_string(input2, get_value);
268  if(!input2_value.has_value() || !input1_value.has_value())
269  return {};
270 
271  std::vector<mp_integer> arg_values;
272  const auto &insert = std::back_inserter(arg_values);
273  const mp_integer unknown('?');
274  std::transform(
275  args.begin(), args.end(), insert, [&](const exprt &e) { // NOLINT
276  if(const auto val = numeric_cast<mp_integer>(get_value(e)))
277  return *val;
278  return unknown;
279  });
280 
281  const auto result_value = eval(*input1_value, *input2_value, arg_values);
282  const auto length = from_integer(result_value.size(), result.length().type());
283  const array_typet type(result.type().subtype(), length);
284  return make_string(result_value, type);
285 }
286 
293  const exprt &return_code,
294  const std::vector<exprt> &fun_args,
295  array_poolt &array_pool)
296  : string_builtin_functiont(return_code)
297 {
298  PRECONDITION(fun_args.size() >= 3);
299  result = array_pool.find(fun_args[1], fun_args[0]);
300  arg = fun_args[2];
301 }
302 
304  const std::function<exprt(const exprt &)> &get_value) const
305 {
306  const auto arg_value = numeric_cast<mp_integer>(get_value(arg));
307  if(!arg_value)
308  return {};
309  static std::string digits = "0123456789abcdefghijklmnopqrstuvwxyz";
310  const auto radix_value = numeric_cast<mp_integer>(get_value(radix));
311  if(!radix_value || *radix_value > digits.length())
312  return {};
313 
314  mp_integer current_value = *arg_value;
315  std::vector<mp_integer> right_to_left_characters;
316  if(current_value < 0)
317  current_value = -current_value;
318  if(current_value == 0)
319  right_to_left_characters.emplace_back('0');
320  while(current_value > 0)
321  {
322  const auto digit_value = (current_value % *radix_value).to_ulong();
323  right_to_left_characters.emplace_back(digits.at(digit_value));
324  current_value /= *radix_value;
325  }
326  if(*arg_value < 0)
327  right_to_left_characters.emplace_back('-');
328 
329  const auto length = right_to_left_characters.size();
330  const auto length_expr = from_integer(length, result.length().type());
331  const array_typet type(result.type().subtype(), length_expr);
332  return make_string(
333  right_to_left_characters.rbegin(), right_to_left_characters.rend(), type);
334 }
335 
337 {
338  const typet &type = result.length().type();
339  const auto radix_opt = numeric_cast<std::size_t>(radix);
340  const auto radix_value = radix_opt.has_value() ? radix_opt.value() : 2;
341  const std::size_t upper_bound =
342  max_printed_string_length(arg.type(), radix_value);
343  const exprt negative_arg =
344  binary_relation_exprt(arg, ID_le, from_integer(0, type));
345  const exprt absolute_arg =
346  if_exprt(negative_arg, unary_minus_exprt(arg), arg);
347 
348  exprt size_expr = from_integer(1, type);
349  exprt min_int_with_current_size = from_integer(1, radix.type());
350  for(std::size_t current_size = 2; current_size <= upper_bound + 1;
351  ++current_size)
352  {
353  min_int_with_current_size = mult_exprt(radix, min_int_with_current_size);
354  const exprt at_least_current_size =
355  binary_relation_exprt(absolute_arg, ID_ge, min_int_with_current_size);
356  size_expr = if_exprt(
357  at_least_current_size, from_integer(current_size, type), size_expr);
358  }
359 
360  const exprt size_expr_with_sign = if_exprt(
361  negative_arg, plus_exprt(size_expr, from_integer(1, type)), size_expr);
362  return equal_exprt(result.length(), size_expr_with_sign);
363 }
364 
366  const exprt &return_code,
368  array_poolt &array_pool)
369  : string_builtin_functiont(return_code), function_application(f)
370 {
371  const std::vector<exprt> &fun_args = f.arguments();
372  std::size_t i = 0;
373  if(fun_args.size() >= 2 && fun_args[1].type().id() == ID_pointer)
374  {
375  string_res = array_pool.find(fun_args[1], fun_args[0]);
376  i = 2;
377  }
378 
379  for(; i < fun_args.size(); ++i)
380  {
381  const auto arg = expr_try_dynamic_cast<struct_exprt>(fun_args[i]);
382  // TODO: use is_refined_string_type ?
383  if(
384  arg && arg->operands().size() == 2 &&
385  arg->op1().type().id() == ID_pointer)
386  {
387  INVARIANT(is_refined_string_type(arg->type()), "should be a string");
388  string_args.push_back(array_pool.find(arg->op1(), arg->op0()));
389  }
390  else
391  args.push_back(fun_args[i]);
392  }
393 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3424
The type of an expression.
Definition: type.h:22
exprt & true_case()
Definition: std_expr.h:3393
BigInt mp_integer
Definition: mp_arith.h:22
Generates string constraints to link results from string functions with their arguments.
virtual 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
Evaluate the result from a concrete valuation of the arguments.
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
application of (mathematical) function
Definition: std_expr.h:4529
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.
optionalt< exprt > eval(const std::function< exprt(const exprt &)> &get_value) const override
Given a function get_value which gives a valuation to expressions, attempt to find the result of the ...
boolean OR
Definition: std_expr.h:2391
optionalt< exprt > eval(const std::function< exprt(const exprt &)> &get_value) const override
Given a function get_value which gives a valuation to expressions, attempt to find the result of the ...
argumentst & arguments()
Definition: std_expr.h:4562
String inserting a string into another one.
static array_string_exprt make_string(const std::vector< mp_integer > &array, const array_typet &array_type)
Make a string from a constant array.
std::vector< array_string_exprt > string_args
string_insertion_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Constructor from arguments of a function application.
static optionalt< std::vector< mp_integer > > eval_string(const array_string_exprt &a, const std::function< exprt(const exprt &)> &get_value)
Module: String solver Author: Diffblue Ltd.
The trinary if-then-else operator.
Definition: std_expr.h:3359
exprt & cond()
Definition: std_expr.h:3383
bool is_true() const
Definition: expr.cpp:124
typet & type()
Definition: expr.h:56
Correspondance between arrays and pointers string representations.
Base class for string functions that are built in the solver.
string_builtin_function_with_no_evalt(const exprt &return_code, const function_application_exprt &f, array_poolt &array_pool)
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:204
equality
Definition: std_expr.h:1354
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call...
const irep_idt & id() const
Definition: irep.h:259
array_string_exprt find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
#define CHARACTER_FOR_UNKNOWN
nonstd::optional< T > optionalt
Definition: optional.h:35
boolean AND
Definition: std_expr.h:2255
optionalt< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
Definition: arith_tools.h:122
#define PRECONDITION(CONDITION)
Definition: invariant.h:242
The plus expression.
Definition: std_expr.h:893
optionalt< exprt > eval(const std::function< exprt(const exprt &)> &get_value) const override
Given a function get_value which gives a valuation to expressions, attempt to find the result of the ...
string_creation_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Constructor from arguments of a function application.
auto expr_checked_cast(TExpr &base) -> typename detail::expr_dynamic_cast_return_typet< T, TExpr >::type
Cast a reference to a generic exprt to a specific derived class.
Definition: expr_cast.h:184
The unary minus expression.
Definition: std_expr.h:444
exprt & false_case()
Definition: std_expr.h:3403
bool is_constant() const
Definition: expr.cpp:119
string_transformation_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Constructor from arguments of a function application.
binary multiplication
Definition: std_expr.h:1017
Base class for all expressions.
Definition: expr.h:42
bool is_refined_string_type(const typet &type)
optionalt< array_string_exprt > string_res
size_t max_printed_string_length(const typet &type, unsigned long ul_radix)
Calculate the string length needed to represent any value of the given type using the given radix...
optionalt< exprt > eval(const std::function< exprt(const exprt &)> &get_value) const override
Given a function get_value which gives a valuation to expressions, attempt to find the result of the ...
arrays with given size
Definition: std_types.h:1013
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call...
const typet & subtype() const
Definition: type.h:33
operandst & operands()
Definition: expr.h:66
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
struct constructor from list of elements
Definition: std_expr.h:1815
optionalt< exprt > eval(const std::function< exprt(const exprt &)> &get_value) const override
Given a function get_value which gives a valuation to expressions, attempt to find the result of the ...
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.
bitvector_typet char_type()
Definition: c_types.cpp:114
static bool eval_is_upper_case(const mp_integer &c)
array constructor from list of elements
Definition: std_expr.h:1617
array_string_exprt & to_array_string_expr(exprt &expr)
Definition: string_expr.h:162
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
Definition: expr_cast.h:91