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  string_constraint_generatort &generator) const
142 
143 {
144  auto pair = [&]() -> std::pair<exprt, string_constraintst> {
145  if(args.size() == 0)
146  return add_axioms_for_concat(
147  generator.fresh_symbol, result, input1, input2);
148  if(args.size() == 2)
149  {
151  generator.fresh_symbol, result, input1, input2, args[0], args[1]);
152  }
153  UNREACHABLE;
154  }();
155  pair.second.existential.push_back(equal_exprt(pair.first, return_code));
156  return pair.second;
157 }
158 
160 {
161  if(args.size() == 0)
163  if(args.size() == 2)
165  result, input1, input2, args[0], args[1]);
166  UNREACHABLE;
167 }
168 
170  const std::function<exprt(const exprt &)> &get_value) const
171 {
172  auto input_opt = eval_string(input, get_value);
173  if(!input_opt.has_value())
174  return {};
175  const mp_integer char_val = [&] {
176  if(const auto val = numeric_cast<mp_integer>(get_value(character)))
177  return *val;
178  INVARIANT(
179  get_value(character).id() == ID_unknown,
180  "character valuation should only contain constants and unknown");
182  }();
183  input_opt.value().push_back(char_val);
184  const auto length =
185  from_integer(input_opt.value().size(), result.length().type());
186  const array_typet type(result.type().subtype(), length);
187  return make_string(input_opt.value(), type);
188 }
189 
197  string_constraint_generatort &generator) const
198 {
201  constraints.universal.push_back([&] {
202  const symbol_exprt idx =
203  generator.fresh_symbol("QA_index_concat_char", result.length().type());
204  const exprt upper_bound = zero_if_negative(input.length());
205  return string_constraintt(
206  idx, upper_bound, equal_exprt(input[idx], result[idx]));
207  }());
208  constraints.existential.push_back(
210  constraints.existential.push_back(
212  return constraints;
213 }
214 
216 {
218 }
219 
221  const std::function<exprt(const exprt &)> &get_value) const
222 {
223  auto input_opt = eval_string(input, get_value);
224  const auto char_opt = numeric_cast<mp_integer>(get_value(character));
225  const auto position_opt = numeric_cast<mp_integer>(get_value(position));
226  if(!input_opt || !char_opt || !position_opt)
227  return {};
228  if(0 <= *position_opt && *position_opt < input_opt.value().size())
229  input_opt.value()[numeric_cast_v<std::size_t>(*position_opt)] = *char_opt;
230  const auto length =
231  from_integer(input_opt.value().size(), result.length().type());
232  const array_typet type(result.type().subtype(), length);
233  return make_string(input_opt.value(), type);
234 }
235 
246  string_constraint_generatort &generator) const
247 {
250  constraints.existential.push_back(
252  and_exprt(
254  from_integer(0, position.type()), ID_le, position),
257  constraints.universal.push_back([&] {
258  const symbol_exprt q =
259  generator.fresh_symbol("QA_char_set", position.type());
260  const equal_exprt a3_body(result[q], input[q]);
261  return string_constraintt(
262  q, minimum(zero_if_negative(result.length()), position), a3_body);
263  }());
264  constraints.universal.push_back([&] {
265  const symbol_exprt q2 =
266  generator.fresh_symbol("QA_char_set2", position.type());
267  const plus_exprt lower_bound(position, from_integer(1, position.type()));
268  const equal_exprt a4_body(result[q2], input[q2]);
269  return string_constraintt(
270  q2, lower_bound, zero_if_negative(result.length()), a4_body);
271  }());
272  return constraints;
273 }
274 
276 {
277  const exprt out_of_bounds = or_exprt(
280  position, ID_lt, from_integer(0, input.length().type())));
281  const exprt return_value = if_exprt(
282  out_of_bounds,
285  return and_exprt(
287  equal_exprt(return_code, return_value));
288 }
289 
290 static bool eval_is_upper_case(const mp_integer &c)
291 {
292  // Characters between 'A' and 'Z' are upper-case
293  // Characters between 0xc0 (latin capital A with grave)
294  // and 0xd6 (latin capital O with diaeresis) are upper-case
295  // Characters between 0xd8 (latin capital O with stroke)
296  // and 0xde (latin capital thorn) are upper-case
297  return ('A' <= c && c <= 'Z') || (0xc0 <= c && c <= 0xd6) ||
298  (0xd8 <= c && c <= 0xde);
299 }
300 
302  const std::function<exprt(const exprt &)> &get_value) const
303 {
304  auto input_opt = eval_string(input, get_value);
305  if(!input_opt)
306  return {};
307  for(mp_integer &c : input_opt.value())
308  {
309  if(eval_is_upper_case(c))
310  c += 0x20;
311  }
312  const auto length =
313  from_integer(input_opt.value().size(), result.length().type());
314  const array_typet type(result.type().subtype(), length);
315  return make_string(input_opt.value(), type);
316 }
317 
320 static exprt is_upper_case(const exprt &character)
321 {
322  const exprt char_A = from_integer('A', character.type());
323  const exprt char_Z = from_integer('Z', character.type());
324  exprt::operandst upper_case;
325  // Characters between 'A' and 'Z' are upper-case
326  upper_case.push_back(
327  and_exprt(
328  binary_relation_exprt(char_A, ID_le, character),
329  binary_relation_exprt(character, ID_le, char_Z)));
330 
331  // Characters between 0xc0 (latin capital A with grave)
332  // and 0xd6 (latin capital O with diaeresis) are upper-case
333  upper_case.push_back(
334  and_exprt(
336  from_integer(0xc0, character.type()), ID_le, character),
338  character, ID_le, from_integer(0xd6, character.type()))));
339 
340  // Characters between 0xd8 (latin capital O with stroke)
341  // and 0xde (latin capital thorn) are upper-case
342  upper_case.push_back(
343  and_exprt(
345  from_integer(0xd8, character.type()), ID_le, character),
347  character, ID_le, from_integer(0xde, character.type()))));
348  return disjunction(upper_case);
349 }
350 
353 static exprt is_lower_case(const exprt &character)
354 {
355  return is_upper_case(
356  minus_exprt(character, from_integer(0x20, character.type())));
357 }
358 
370  string_constraint_generatort &generator) const
371 {
372  // \todo for now, only characters in Basic Latin and Latin-1 supplement
373  // are supported (up to 0x100), we should add others using case mapping
374  // information from the UnicodeData file.
377  constraints.universal.push_back([&] {
378  const symbol_exprt idx =
379  generator.fresh_symbol("QA_lower_case", result.length().type());
380  const exprt conditional_convert = [&] {
381  // The difference between upper-case and lower-case for the basic
382  // latin and latin-1 supplement is 0x20.
383  const typet &char_type = result.type().subtype();
384  const exprt diff = from_integer(0x20, char_type);
385  const exprt converted =
386  equal_exprt(result[idx], plus_exprt(input[idx], diff));
387  const exprt non_converted = equal_exprt(result[idx], input[idx]);
388  return if_exprt(is_upper_case(input[idx]), converted, non_converted);
389  }();
390  return string_constraintt(
391  idx, zero_if_negative(result.length()), conditional_convert);
392  }());
393  return constraints;
394 }
395 
397  const std::function<exprt(const exprt &)> &get_value) const
398 {
399  auto input_opt = eval_string(input, get_value);
400  if(!input_opt)
401  return {};
402  for(mp_integer &c : input_opt.value())
403  {
404  if(eval_is_upper_case(c - 0x20))
405  c -= 0x20;
406  }
407  const auto length =
408  from_integer(input_opt.value().size(), result.length().type());
409  const array_typet type(result.type().subtype(), length);
410  return make_string(input_opt.value(), type);
411 }
412 
423  symbol_generatort &fresh_symbol) const
424 {
427  constraints.universal.push_back([&] {
428  const symbol_exprt idx =
429  fresh_symbol("QA_upper_case", result.length().type());
430  const typet &char_type = input.content().type().subtype();
431  const exprt converted =
432  minus_exprt(input[idx], from_integer(0x20, char_type));
433  return string_constraintt(
434  idx,
436  equal_exprt(
437  result[idx],
438  if_exprt(is_lower_case(input[idx]), converted, input[idx])));
439  }());
440  return constraints;
441 }
442 
444  const std::vector<mp_integer> &input1_value,
445  const std::vector<mp_integer> &input2_value,
446  const std::vector<mp_integer> &args_value) const
447 {
448  PRECONDITION(args_value.size() >= 1 || args_value.size() <= 3);
449  const auto offset = std::min(
450  std::max(args_value[0], mp_integer(0)), mp_integer(input1_value.size()));
451  const auto start = args_value.size() > 1
452  ? std::max(args_value[1], mp_integer(0))
453  : mp_integer(0);
454 
455  const mp_integer input2_size(input2_value.size());
456  const auto end =
457  args_value.size() > 2
458  ? std::max(std::min(args_value[2], input2_size), mp_integer(0))
459  : input2_size;
460 
461  std::vector<mp_integer> result(input1_value);
462  result.insert(
463  result.begin() + numeric_cast_v<std::size_t>(offset),
464  input2_value.begin() + numeric_cast_v<std::size_t>(start),
465  input2_value.begin() + numeric_cast_v<std::size_t>(end));
466  return result;
467 }
468 
470  const std::function<exprt(const exprt &)> &get_value) const
471 {
472  const auto &input1_value = eval_string(input1, get_value);
473  const auto &input2_value = eval_string(input2, get_value);
474  if(!input2_value.has_value() || !input1_value.has_value())
475  return {};
476 
477  std::vector<mp_integer> arg_values;
478  const auto &insert = std::back_inserter(arg_values);
479  const mp_integer unknown('?');
480  std::transform(
481  args.begin(), args.end(), insert, [&](const exprt &e) { // NOLINT
482  if(const auto val = numeric_cast<mp_integer>(get_value(e)))
483  return *val;
484  return unknown;
485  });
486 
487  const auto result_value = eval(*input1_value, *input2_value, arg_values);
488  const auto length = from_integer(result_value.size(), result.length().type());
489  const array_typet type(result.type().subtype(), length);
490  return make_string(result_value, type);
491 }
492 
494  string_constraint_generatort &generator) const
495 {
496  if(args.size() == 1)
497  {
498  auto pair = add_axioms_for_insert(
499  generator.fresh_symbol, result, input1, input2, args[0]);
500  pair.second.existential.push_back(equal_exprt(pair.first, return_code));
501  return pair.second;
502  }
503  if(args.size() == 3)
505  UNREACHABLE;
506 }
507 
509 {
510  if(args.size() == 1)
512  if(args.size() == 3)
514  UNREACHABLE;
515 }
516 
523  const exprt &return_code,
524  const std::vector<exprt> &fun_args,
525  array_poolt &array_pool)
526  : string_builtin_functiont(return_code)
527 {
528  PRECONDITION(fun_args.size() >= 3);
529  result = array_pool.find(fun_args[1], fun_args[0]);
530  arg = fun_args[2];
531 }
532 
534  const std::function<exprt(const exprt &)> &get_value) const
535 {
536  const auto arg_value = numeric_cast<mp_integer>(get_value(arg));
537  if(!arg_value)
538  return {};
539  static std::string digits = "0123456789abcdefghijklmnopqrstuvwxyz";
540  const auto radix_value = numeric_cast<mp_integer>(get_value(radix));
541  if(!radix_value || *radix_value > digits.length())
542  return {};
543 
544  mp_integer current_value = *arg_value;
545  std::vector<mp_integer> right_to_left_characters;
546  if(current_value < 0)
547  current_value = -current_value;
548  if(current_value == 0)
549  right_to_left_characters.emplace_back('0');
550  while(current_value > 0)
551  {
552  const auto digit_value = (current_value % *radix_value).to_ulong();
553  right_to_left_characters.emplace_back(digits.at(digit_value));
554  current_value /= *radix_value;
555  }
556  if(*arg_value < 0)
557  right_to_left_characters.emplace_back('-');
558 
559  const auto length = right_to_left_characters.size();
560  const auto length_expr = from_integer(length, result.length().type());
561  const array_typet type(result.type().subtype(), length_expr);
562  return make_string(
563  right_to_left_characters.rbegin(), right_to_left_characters.rend(), type);
564 }
565 
567  string_constraint_generatort &generator) const
568 {
570  result, arg, radix, 0, generator.ns);
571  pair.second.existential.push_back(equal_exprt(pair.first, return_code));
572  return pair.second;
573 }
574 
576 {
577  const typet &type = result.length().type();
578  const auto radix_opt = numeric_cast<std::size_t>(radix);
579  const auto radix_value = radix_opt.has_value() ? radix_opt.value() : 2;
580  const std::size_t upper_bound =
581  max_printed_string_length(arg.type(), radix_value);
582  const exprt negative_arg =
583  binary_relation_exprt(arg, ID_le, from_integer(0, type));
584  const exprt absolute_arg =
585  if_exprt(negative_arg, unary_minus_exprt(arg), arg);
586 
587  exprt size_expr = from_integer(1, type);
588  exprt min_int_with_current_size = from_integer(1, radix.type());
589  for(std::size_t current_size = 2; current_size <= upper_bound + 1;
590  ++current_size)
591  {
592  min_int_with_current_size = mult_exprt(radix, min_int_with_current_size);
593  const exprt at_least_current_size =
594  binary_relation_exprt(absolute_arg, ID_ge, min_int_with_current_size);
595  size_expr = if_exprt(
596  at_least_current_size, from_integer(current_size, type), size_expr);
597  }
598 
599  const exprt size_expr_with_sign = if_exprt(
600  negative_arg, plus_exprt(size_expr, from_integer(1, type)), size_expr);
601  return equal_exprt(result.length(), size_expr_with_sign);
602 }
603 
605  const exprt &return_code,
607  array_poolt &array_pool)
608  : string_builtin_functiont(return_code), function_application(f)
609 {
610  const std::vector<exprt> &fun_args = f.arguments();
611  std::size_t i = 0;
612  if(fun_args.size() >= 2 && fun_args[1].type().id() == ID_pointer)
613  {
614  string_res = array_pool.find(fun_args[1], fun_args[0]);
615  i = 2;
616  }
617 
618  for(; i < fun_args.size(); ++i)
619  {
620  const auto arg = expr_try_dynamic_cast<struct_exprt>(fun_args[i]);
621  // TODO: use is_refined_string_type ?
622  if(
623  arg && arg->operands().size() == 2 &&
624  arg->op1().type().id() == ID_pointer)
625  {
626  INVARIANT(is_refined_string_type(arg->type()), "should be a string");
627  string_args.push_back(array_pool.find(arg->op1(), arg->op0()));
628  }
629  else
630  args.push_back(fun_args[i]);
631  }
632 }
633 
635  string_constraint_generatort &generator) const
636 {
637  auto pair = generator.add_axioms_for_function_application(
639  pair.second.existential.push_back(equal_exprt(pair.first, return_code));
640  return pair.second;
641 }
string_concat_char_builtin_functiont::constraints
string_constraintst constraints(string_constraint_generatort &generator) const override
Set of constraints enforcing that result is the concatenation of input with character.
Definition: string_builtin_function.cpp:196
function_application_exprt::arguments
argumentst & arguments()
Definition: std_expr.h:4506
string_of_int_builtin_functiont::radix
exprt radix
Definition: string_builtin_function.h:415
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
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_builtin_function.cpp:52
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_index, const exprt &end_index)
Add axioms enforcing that the length of res is that of the concatenation of s1 with the substring of ...
Definition: string_constraint_generator_concat.cpp:81
string_builtin_function.h
typet::subtype
const typet & subtype() const
Definition: type.h:38
is_lower_case
static exprt is_lower_case(const exprt &character)
Expression which is true for lower_case characters of the Basic Latin and Latin-1 supplement of unico...
Definition: string_builtin_function.cpp:353
string_insertion_builtin_functiont
String inserting a string into another one.
Definition: string_builtin_function.h:271
eval_is_upper_case
static bool eval_is_upper_case(const mp_integer &c)
Definition: string_builtin_function.cpp:290
string_to_lower_case_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_builtin_function.h:213
minimum
exprt minimum(const exprt &a, const exprt &b)
Definition: string_constraint_generator_main.cpp:578
string_insertion_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_builtin_function.cpp:508
typet
The type of an expression, extends irept.
Definition: type.h:27
is_upper_case
static exprt is_upper_case(const exprt &character)
Expression which is true for uppercase characters of the Basic Latin and Latin-1 supplement of unicod...
Definition: string_builtin_function.cpp:320
string_to_upper_case_builtin_functiont::constraints
string_constraintst constraints(class symbol_generatort &fresh_symbol) const
Set of constraints ensuring result corresponds to input in which lowercase characters of Basic Latin ...
Definition: string_builtin_function.cpp:422
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
array_poolt
Correspondance between arrays and pointers string representations.
Definition: string_constraint_generator.h:49
string_builtin_functiont::return_code
exprt return_code
Definition: string_builtin_function.h:53
string_constraintt
Definition: string_constraint.h:58
mp_integer
BigInt mp_integer
Definition: mp_arith.h:22
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:3427
string_of_int_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_builtin_function.cpp:575
string_constraint_generatort::fresh_symbol
symbol_generatort fresh_symbol
Definition: string_constraint_generator.h:133
and_exprt
Boolean AND.
Definition: std_expr.h:2409
string_set_char_builtin_functiont::position
exprt position
Definition: string_builtin_function.h:154
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
string_builtin_function_with_no_evalt::function_application
function_application_exprt function_application
Definition: string_builtin_function.h:438
exprt
Base class for all expressions.
Definition: expr.h:54
length_constraint_for_insert
exprt length_constraint_for_insert(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
Add axioms ensuring the length of res corresponds to that of s1 where we inserted s2.
Definition: string_constraint_generator_insert.cpp:80
add_axioms_for_string_of_int_with_radix
std::pair< exprt, string_constraintst > add_axioms_for_string_of_int_with_radix(const array_string_exprt &res, const exprt &input_int, const exprt &radix, size_t max_size, const namespacet &ns)
Add axioms enforcing that the string corresponds to the result of String.valueOf(II) or String....
Definition: string_constraint_generator_valueof.cpp:153
string_builtin_function_with_no_evalt::string_args
std::vector< array_string_exprt > string_args
Definition: string_builtin_function.h:440
string_constraint_generatort::add_axioms_for_function_application
std::pair< exprt, string_constraintst > add_axioms_for_function_application(symbol_generatort &fresh_symbol, const function_application_exprt &expr)
strings contained in this call are converted to objects of type string_exprt, through adding axioms.
Definition: string_constraint_generator_main.cpp:370
string_to_upper_case_builtin_functiont::eval
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 ...
Definition: string_builtin_function.cpp:396
string_constraintst
Collection of constraints of different types: existential formulas, universal formulas,...
Definition: string_constraint_generator.h:108
array_string_exprt::content
exprt & content()
Definition: string_expr.h:80
string_builtin_function_with_no_evalt::args
std::vector< exprt > args
Definition: string_builtin_function.h:441
string_transformation_builtin_functiont::string_transformation_builtin_functiont
string_transformation_builtin_functiont(exprt return_code, array_string_exprt result, array_string_exprt input)
Definition: string_builtin_function.h:80
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
string_to_lower_case_builtin_functiont::eval
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 ...
Definition: string_builtin_function.cpp:301
eval_string
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.
Definition: string_builtin_function.cpp:67
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
equal_exprt
Equality.
Definition: std_expr.h:1484
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3465
string_constraint_generatort
Definition: string_constraint_generator.h:120
string_insertion_builtin_functiont::input1
array_string_exprt input1
Definition: string_builtin_function.h:275
string_insertion_builtin_functiont::eval
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.
Definition: string_builtin_function.cpp:443
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_builtin_function.cpp:159
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
string_concat_char_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_builtin_function.cpp:215
string_transformation_builtin_functiont::input
array_string_exprt input
Definition: string_builtin_function.h:78
string_insertion_builtin_functiont::result
array_string_exprt result
Definition: string_builtin_function.h:274
symbol_generatort
Generation of fresh symbols of a given type.
Definition: string_constraint_generator.h:32
disjunction
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:26
string_builtin_function_with_no_evalt::string_builtin_function_with_no_evalt
string_builtin_function_with_no_evalt(const exprt &return_code, const function_application_exprt &f, array_poolt &array_pool)
Definition: string_builtin_function.cpp:604
string_insertion_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_builtin_function.cpp:493
or_exprt
Boolean OR.
Definition: std_expr.h:2531
string_constraint_generatort::ns
const namespacet ns
Definition: string_constraint_generator.h:139
string_set_char_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_builtin_function.cpp:275
CHARACTER_FOR_UNKNOWN
#define CHARACTER_FOR_UNKNOWN
Definition: string_builtin_function.h:16
length_constraint_for_concat_char
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.
Definition: string_constraint_generator_concat.cpp:109
string_insertion_builtin_functiont::string_insertion_builtin_functiont
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.
Definition: string_builtin_function.cpp:36
add_axioms_for_concat_substr
std::pair< exprt, string_constraintst > add_axioms_for_concat_substr(symbol_generatort &fresh_symbol, 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_constraint_generator_concat.cpp:38
function_application_exprt
Application of (mathematical) function.
Definition: std_expr.h:4481
string_concat_char_builtin_functiont::character
exprt character
Definition: string_builtin_function.h:119
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1159
string_builtin_function_with_no_evalt::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_builtin_function.cpp:634
unary_minus_exprt
The unary minus expression.
Definition: std_expr.h:469
irept::id
const irep_idt & id() const
Definition: irep.h:259
string_concat_char_builtin_functiont::eval
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 ...
Definition: string_builtin_function.cpp:169
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
to_array_string_expr
array_string_exprt & to_array_string_expr(exprt &expr)
Definition: string_expr.h:101
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
string_builtin_functiont
Base class for string functions that are built in the solver.
Definition: string_builtin_function.h:19
minus_exprt
Binary minus.
Definition: std_expr.h:1106
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_builtin_function.cpp:140
string_of_int_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_builtin_function.cpp:566
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
make_string
static array_string_exprt make_string(const std::vector< mp_integer > &array, const array_typet &array_type)
Make a string from a constant array.
Definition: string_builtin_function.cpp:114
string_builtin_function_with_no_evalt::string_res
optionalt< array_string_exprt > string_res
Definition: string_builtin_function.h:439
array_typet
Arrays with given size.
Definition: std_types.h:1000
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:3455
array_poolt::find
const array_string_exprt & find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
Definition: string_constraint_generator_main.cpp:314
UNIMPLEMENTED
#define UNIMPLEMENTED
Definition: invariant.h:497
string_creation_builtin_functiont::result
array_string_exprt result
Definition: string_builtin_function.h:365
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
add_axioms_for_insert
std::pair< exprt, string_constraintst > add_axioms_for_insert(symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &offset)
Add axioms ensuring the result res corresponds to s1 where we inserted s2 at position offset.
Definition: string_constraint_generator_insert.cpp:33
zero_if_negative
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
Definition: string_constraint_generator_main.cpp:591
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:83
string_creation_builtin_functiont::arg
exprt arg
Definition: string_builtin_function.h:366
if_exprt::cond
exprt & cond()
Definition: std_expr.h:3445
array_string_exprt::length
exprt & length()
Definition: string_expr.h:70
binary_relation_exprt
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:878
string_set_char_builtin_functiont::eval
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 ...
Definition: string_builtin_function.cpp:220
is_refined_string_type
bool is_refined_string_type(const typet &type)
Definition: refined_string_type.h:52
add_axioms_for_concat
std::pair< exprt, string_constraintst > add_axioms_for_concat(symbol_generatort &fresh_symbol, 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_constraint_generator_concat.cpp:126
implies_exprt
Boolean implication.
Definition: std_expr.h:2485
string_insertion_builtin_functiont::input2
array_string_exprt input2
Definition: string_builtin_function.h:276
exprt::operands
operandst & operands()
Definition: expr.h:78
string_set_char_builtin_functiont::character
exprt character
Definition: string_builtin_function.h:155
string_insertion_builtin_functiont::args
std::vector< exprt > args
Definition: string_builtin_function.h:277
length_constraint_for_concat
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
Definition: string_constraint_generator_concat.cpp:99
string_to_upper_case_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_builtin_function.h:262
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_builtin_function.cpp:119
string_constraint_generator.h
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1739
string_transformation_builtin_functiont::result
array_string_exprt result
Definition: string_builtin_function.h:77
array_string_exprt
Definition: string_expr.h:67
max_printed_string_length
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.
Definition: string_constraint_generator_valueof.cpp:704
string_to_lower_case_builtin_functiont::constraints
string_constraintst constraints(string_constraint_generatort &generator) const override
Set of constraints ensuring result corresponds to input in which uppercase characters have been conve...
Definition: string_builtin_function.cpp:369
validation_modet::INVARIANT
string_creation_builtin_functiont::string_creation_builtin_functiont
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.
Definition: string_builtin_function.cpp:522
string_constraintst::existential
std::vector< exprt > existential
Definition: string_constraint_generator.h:110
string_set_char_builtin_functiont::constraints
string_constraintst constraints(string_constraint_generatort &generator) const override
Set of constraints ensuring that result is similar to input where the character at index position is ...
Definition: string_builtin_function.cpp:245
string_of_int_builtin_functiont::eval
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 ...
Definition: string_builtin_function.cpp:533
string_constraintst::universal
std::vector< string_constraintt > universal
Definition: string_constraint_generator.h:111