cprover
string_constraint_generator_valueof.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Generates string constraints for functions generating strings
4  from other types, in particular int, long, float, double, char, bool
5 
6 Author: Romain Brenguier, romain.brenguier@diffblue.com
7 
8 \*******************************************************************/
9 
13 
16 
17 #include <util/deprecate.h>
18 #include <util/simplify_expr.h>
19 
20 #include <cmath>
22 
29 static unsigned long to_integer_or_default(
30  const exprt &expr,
31  unsigned long def,
32  const namespacet &ns)
33 {
34  if(const auto i = numeric_cast<unsigned long>(simplify_expr(expr, ns)))
35  return *i;
36  return def;
37 }
38 
43 DEPRECATED(SINCE(2017, 10, 5, "use add_axioms_for_string_of_int instead"))
44 std::pair<exprt, string_constraintst>
45 string_constraint_generatort::add_axioms_from_long(
47 {
48  PRECONDITION(f.arguments().size() == 3 || f.arguments().size() == 4);
49  const array_string_exprt res =
50  array_pool.find(f.arguments()[1], f.arguments()[0]);
51  if(f.arguments().size() == 4)
52  return add_axioms_for_string_of_int_with_radix(
53  res, f.arguments()[2], f.arguments()[3], 0);
54  else
55  return add_axioms_for_string_of_int(res, f.arguments()[2], 0);
56 }
57 
64 DEPRECATED(SINCE(2017, 10, 5, "Java specific, should be implemented in Java"))
65 std::pair<exprt, string_constraintst>
66 string_constraint_generatort::add_axioms_from_bool(
67  const array_string_exprt &res,
68  const exprt &b)
69 {
70  const typet &char_type = res.content().type().subtype();
71  PRECONDITION(b.type() == bool_typet() || b.type().id() == ID_c_bool);
72  string_constraintst constraints;
73  typecast_exprt eq(b, bool_typet());
74 
75  // We add axioms:
76  // a1 : eq => res = |"true"|
77  // a2 : forall i < |"true"|. eq => res[i]="true"[i]
78  // a3 : !eq => res = |"false"|
79  // a4 : forall i < |"false"|. !eq => res[i]="false"[i]
80 
81  std::string str_true = "true";
82  const implies_exprt a1(
83  eq, equal_to(array_pool.get_or_create_length(res), str_true.length()));
84  constraints.existential.push_back(a1);
85 
86  for(std::size_t i = 0; i < str_true.length(); i++)
87  {
88  exprt chr = from_integer(str_true[i], char_type);
89  implies_exprt a2(eq, equal_exprt(res[i], chr));
90  constraints.existential.push_back(a2);
91  }
92 
93  std::string str_false = "false";
94  const implies_exprt a3(
95  not_exprt(eq),
96  equal_to(array_pool.get_or_create_length(res), str_false.length()));
97  constraints.existential.push_back(a3);
98 
99  for(std::size_t i = 0; i < str_false.length(); i++)
100  {
101  exprt chr = from_integer(str_false[i], char_type);
102  implies_exprt a4(not_exprt(eq), equal_exprt(res[i], chr));
103  constraints.existential.push_back(a4);
104  }
105 
106  return {from_integer(0, get_return_code_type()), std::move(constraints)};
107 }
108 
117 std::pair<exprt, string_constraintst>
119  const array_string_exprt &res,
120  const exprt &input_int,
121  size_t max_size)
122 {
123  const constant_exprt radix = from_integer(10, input_int.type());
125  res, input_int, radix, max_size);
126 }
127 
137 std::pair<exprt, string_constraintst>
139  const array_string_exprt &res,
140  const exprt &input_int,
141  const exprt &radix,
142  size_t max_size)
143 {
144  PRECONDITION(max_size < std::numeric_limits<size_t>::max());
145  const typet &type = input_int.type();
146  PRECONDITION(type.id() == ID_signedbv);
147 
150  const unsigned long radix_ul = to_integer_or_default(radix, 0, ns);
151  CHECK_RETURN((radix_ul >= 2 && radix_ul <= 36) || radix_ul == 0);
152 
153  if(max_size == 0)
154  {
155  max_size = max_printed_string_length(type, radix_ul);
156  CHECK_RETURN(max_size < std::numeric_limits<size_t>::max());
157  }
158 
159  const typet &char_type = res.content().type().subtype();
160  const typecast_exprt radix_as_char(radix, char_type);
161  const typecast_exprt radix_input_type(radix, type);
162  const bool strict_formatting = true;
163 
165  res, radix_as_char, radix_ul, max_size, strict_formatting);
167  input_int,
168  type,
169  strict_formatting,
170  res,
171  max_size,
172  radix_input_type,
173  radix_ul);
174  result2.existential.push_back(conjunction(std::move(result1)));
175  return {from_integer(0, get_return_code_type()), std::move(result2)};
176 }
177 
182 static exprt int_of_hex_char(const exprt &chr)
183 {
184  const exprt zero_char = from_integer('0', chr.type());
185  const exprt nine_char = from_integer('9', chr.type());
186  const exprt a_char = from_integer('a', chr.type());
187  return if_exprt(
188  binary_relation_exprt(chr, ID_gt, nine_char),
189  plus_exprt(from_integer(10, chr.type()), minus_exprt(chr, a_char)),
190  minus_exprt(chr, zero_char));
191 }
192 
199 DEPRECATED(SINCE(2017, 10, 5, "use add_axioms_for_string_of_int_with_radix"))
200 std::pair<exprt, string_constraintst>
201 string_constraint_generatort::add_axioms_from_int_hex(
202  const array_string_exprt &res,
203  const exprt &i)
204 {
205  const typet &type = i.type();
206  PRECONDITION(type.id() == ID_signedbv);
207  string_constraintst constraints;
208  const typet &index_type = res.length_type();
209  const typet &char_type = res.content().type().subtype();
210  exprt sixteen = from_integer(16, index_type);
211  exprt minus_char = from_integer('-', char_type);
212  exprt zero_char = from_integer('0', char_type);
213  exprt nine_char = from_integer('9', char_type);
214  exprt a_char = from_integer('a', char_type);
215  exprt f_char = from_integer('f', char_type);
216 
217  size_t max_size = 8;
218  constraints.existential.push_back(and_exprt(
219  greater_than(array_pool.get_or_create_length(res), 0),
220  less_than_or_equal_to(array_pool.get_or_create_length(res), max_size)));
221 
222  for(size_t size = 1; size <= max_size; size++)
223  {
224  exprt sum = from_integer(0, type);
225  exprt all_numbers = true_exprt();
226  exprt chr = res[0];
227 
228  for(size_t j = 0; j < size; j++)
229  {
230  chr = res[j];
231  exprt chr_int = int_of_hex_char(chr);
232  sum = plus_exprt(mult_exprt(sum, sixteen), typecast_exprt(chr_int, type));
234  and_exprt(
235  binary_relation_exprt(chr, ID_ge, zero_char),
236  binary_relation_exprt(chr, ID_le, nine_char)),
237  and_exprt(
238  binary_relation_exprt(chr, ID_ge, a_char),
239  binary_relation_exprt(chr, ID_le, f_char)));
240  all_numbers = and_exprt(all_numbers, is_number);
241  }
242 
243  const equal_exprt premise =
244  equal_to(array_pool.get_or_create_length(res), size);
245  constraints.existential.push_back(
246  implies_exprt(premise, and_exprt(equal_exprt(i, sum), all_numbers)));
247 
248  // disallow 0s at the beginning
249  if(size > 1)
250  constraints.existential.push_back(
251  implies_exprt(premise, not_exprt(equal_exprt(res[0], zero_char))));
252  }
253  return {from_integer(0, get_return_code_type()), std::move(constraints)};
254 }
255 
259 std::pair<exprt, string_constraintst>
262 {
263  PRECONDITION(f.arguments().size() == 3);
264  const array_string_exprt res =
265  array_pool.find(f.arguments()[1], f.arguments()[0]);
266  return add_axioms_from_int_hex(res, f.arguments()[2]);
267 }
268 
279 std::vector<exprt>
281  const array_string_exprt &str,
282  const exprt &radix_as_char,
283  const unsigned long radix_ul,
284  const std::size_t max_size,
285  const bool strict_formatting)
286 {
287  std::vector<exprt> conjuncts;
288  const typet &char_type = str.content().type().subtype();
289  const typet &index_type = str.length_type();
290 
291  const exprt &chr = str[0];
292  const equal_exprt starts_with_minus(chr, from_integer('-', char_type));
293  const equal_exprt starts_with_plus(chr, from_integer('+', char_type));
294  const exprt starts_with_digit =
295  is_digit_with_radix(chr, strict_formatting, radix_as_char, radix_ul);
296 
297  // |str| > 0
298  const exprt non_empty = greater_or_equal_to(
300  conjuncts.push_back(non_empty);
301 
302  if(strict_formatting)
303  {
304  // str[0] = '-' || is_digit_with_radix(str[0], radix)
305  const or_exprt correct_first(starts_with_minus, starts_with_digit);
306  conjuncts.push_back(correct_first);
307  }
308  else
309  {
310  // str[0] = '-' || str[0] = '+' || is_digit_with_radix(str[0], radix)
311  const or_exprt correct_first(
312  starts_with_minus, starts_with_digit, starts_with_plus);
313  conjuncts.push_back(correct_first);
314  }
315 
316  // str[0]='+' or '-' ==> |str| > 1
317  const implies_exprt contains_digit(
318  or_exprt(starts_with_minus, starts_with_plus),
321  conjuncts.push_back(contains_digit);
322 
323  // |str| <= max_size
324  conjuncts.push_back(
326 
327  // forall 1 <= i < |str| . is_digit_with_radix(str[i], radix)
328  // We unfold the above because we know that it will be used for all i up to
329  // |str|, and |str| <= max_size.
330  for(std::size_t index = 1; index < max_size; ++index)
331  {
333  const implies_exprt character_at_index_is_digit(
336  from_integer(index + 1, index_type)),
338  str[index], strict_formatting, radix_as_char, radix_ul));
339  conjuncts.push_back(character_at_index_is_digit);
340  }
341 
342  if(strict_formatting)
343  {
344  const exprt zero_char = from_integer('0', char_type);
345 
346  // no_leading_zero : str[0] = '0' => |str| = 1
347  const implies_exprt no_leading_zero(
348  equal_exprt(chr, zero_char),
349  equal_to(
351  conjuncts.push_back(no_leading_zero);
352 
353  // no_leading_zero_after_minus : str[0]='-' => str[1]!='0'
354  implies_exprt no_leading_zero_after_minus(
355  starts_with_minus, not_exprt(equal_exprt(str[1], zero_char)));
356  conjuncts.push_back(no_leading_zero_after_minus);
357  }
358  return conjuncts;
359 }
360 
375  const exprt &input_int,
376  const typet &type,
377  const bool strict_formatting,
378  const array_string_exprt &str,
379  const std::size_t max_string_length,
380  const exprt &radix,
381  const unsigned long radix_ul)
382 {
383  string_constraintst constraints;
384  const typet &char_type = str.content().type().subtype();
385 
386  const equal_exprt starts_with_minus(str[0], from_integer('-', char_type));
387  const constant_exprt zero_expr = from_integer(0, type);
388 
390  str[0], char_type, type, strict_formatting, radix_ul);
391 
395  constraints.existential.push_back(implies_exprt(
397  equal_exprt(input_int, sum)));
398 
399  for(size_t size = 2; size <= max_string_length; size++)
400  {
401  // sum_0 := numeric value of res[0] (which is 0 if res[0] is '-')
402  // For each 1<=j<max_string_length, we have:
403  // sum_j := radix * sum_{j-1} + numeric value of res[j]
404  // no_overflow_j := sum_{j-1} == (radix * sum_{j-1} / radix)
405  // && sum_j >= sum_{j - 1}
406  // (the first part avoid overflows in the multiplication and the second
407  // one in the addition of the definition of sum_j)
408  // For all 1<=size<=max_string_length we add axioms:
409  // a5 : |res| >= size => no_overflow_j (only added when overflow possible)
410  // a6 : |res| == size && res[0] is a digit for radix =>
411  // input_int == sum_{size-1}
412  // a7 : |res| == size && res[0] == '-' => input_int == -sum_{size-1}
413 
414  const mult_exprt radix_sum(sum, radix);
415  // new_sum = radix * sum + (numeric value of res[j])
416  const exprt new_sum = plus_exprt(
417  radix_sum,
419  str[size - 1], char_type, type, strict_formatting, radix_ul));
420 
421  // An overflow can happen when reaching the last index which can contain
422  // a digit, which is `max_string_length - 2` because of the space left for
423  // a minus sign. That assumes that we were able to identify the radix. If we
424  // weren't then we check for overflow on every index.
425  optionalt<exprt> no_overflow;
426  if(size - 1 >= max_string_length - 2 || radix_ul == 0)
427  {
428  no_overflow = and_exprt{equal_exprt(sum, div_exprt(radix_sum, radix)),
429  binary_relation_exprt(new_sum, ID_ge, radix_sum)};
430  }
431  sum = new_sum;
432 
433  exprt length_expr = array_pool.get_or_create_length(str);
434 
435  if(no_overflow.has_value())
436  {
437  const binary_predicate_exprt string_length_ge_size{
438  length_expr, ID_ge, from_integer(size, length_expr.type())};
439  const implies_exprt a5(string_length_ge_size, *no_overflow);
440  constraints.existential.push_back(a5);
441  }
442 
443  const equal_exprt string_length_equals_size = equal_to(length_expr, size);
444 
445  const implies_exprt a6(
446  and_exprt(string_length_equals_size, not_exprt(starts_with_minus)),
447  equal_exprt(input_int, sum));
448  constraints.existential.push_back(a6);
449 
450  const implies_exprt a7(
451  and_exprt(string_length_equals_size, starts_with_minus),
452  equal_exprt(input_int, unary_minus_exprt(sum)));
453  constraints.existential.push_back(a7);
454  }
455  return constraints;
456 }
457 
461  const typet &target_int_type)
462 {
463  PRECONDITION(f.arguments().size() == 1 || f.arguments().size() == 2);
464  PRECONDITION(target_int_type.id() == ID_signedbv);
466 
467  const exprt radix =
468  f.arguments().size() == 1
469  ? static_cast<exprt>(from_integer(10, target_int_type))
470  : static_cast<exprt>(typecast_exprt(f.arguments()[1], target_int_type));
471  // Most of the time we can evaluate radix as an integer. The value 0 is used
472  // to indicate when we can't tell what the radix is.
473  const unsigned long radix_ul = to_integer_or_default(radix, 0, ns);
474  PRECONDITION((radix_ul >= 2 && radix_ul <= 36) || radix_ul == 0);
475 
476  const std::size_t max_string_length =
477  max_printed_string_length(target_int_type, radix_ul);
478 
479  return {str, radix, radix_ul, max_string_length};
480 }
481 
489 std::pair<exprt, string_constraintst>
492 {
493  irep_idt called_function = to_symbol_expr(f.function()).get_identifier();
494  PRECONDITION(
495  called_function == ID_cprover_string_is_valid_int_func ||
496  called_function == ID_cprover_string_is_valid_long_func);
497  const signedbv_typet target_int_type{static_cast<size_t>(
498  called_function == ID_cprover_string_is_valid_int_func ? 32 : 64)};
499  auto args = unpack_parseint_arguments(f, target_int_type);
500 
501  const typet &char_type = args.str.content().type().subtype();
502  const typecast_exprt radix_as_char(args.radix, char_type);
503  const bool strict_formatting = false;
504 
508  args.str,
509  radix_as_char,
510  args.radix_ul,
511  args.max_string_length,
512  strict_formatting);
513 
514  return {typecast_exprt{conjunction(conjuncts), f.type()}, {}};
515 }
516 
524 std::pair<exprt, string_constraintst>
527 {
528  auto args = unpack_parseint_arguments(f, f.type());
529 
530  const typet &type = f.type();
531 
532  const symbol_exprt input_int = fresh_symbol("parsed_int", type);
533  const bool strict_formatting = false;
534 
536  input_int,
537  type,
538  strict_formatting,
539  args.str,
540  args.max_string_length,
541  args.radix,
542  args.radix_ul);
543 
544  return {input_int, std::move(constraints2)};
545 }
546 
556  const exprt &chr,
557  const bool strict_formatting,
558  const exprt &radix_as_char,
559  const unsigned long radix_ul)
560 {
561  PRECONDITION((radix_ul >= 2 && radix_ul <= 36) || radix_ul == 0);
562  const typet &char_type = chr.type();
563  const exprt zero_char = from_integer('0', char_type);
564 
565  const and_exprt is_digit_when_radix_le_10(
566  binary_relation_exprt(chr, ID_ge, zero_char),
567  binary_relation_exprt(chr, ID_lt, plus_exprt(zero_char, radix_as_char)));
568 
569  if(radix_ul <= 10 && radix_ul != 0)
570  {
571  return is_digit_when_radix_le_10;
572  }
573  else
574  {
575  const exprt nine_char = from_integer('9', char_type);
576  const exprt a_char = from_integer('a', char_type);
577  const constant_exprt ten_char_type = from_integer(10, char_type);
578 
579  const minus_exprt radix_minus_ten(radix_as_char, ten_char_type);
580 
581  or_exprt is_digit_when_radix_gt_10(
582  and_exprt(
583  binary_relation_exprt(chr, ID_ge, zero_char),
584  binary_relation_exprt(chr, ID_le, nine_char)),
585  and_exprt(
586  binary_relation_exprt(chr, ID_ge, a_char),
588  chr, ID_lt, plus_exprt(a_char, radix_minus_ten))));
589 
590  if(!strict_formatting)
591  {
592  exprt A_char = from_integer('A', char_type);
593  is_digit_when_radix_gt_10.copy_to_operands(and_exprt(
594  binary_relation_exprt(chr, ID_ge, A_char),
596  chr, ID_lt, plus_exprt(A_char, radix_minus_ten))));
597  }
598 
599  if(radix_ul == 0)
600  {
601  return if_exprt(
602  binary_relation_exprt(radix_as_char, ID_le, ten_char_type),
603  is_digit_when_radix_le_10,
604  is_digit_when_radix_gt_10);
605  }
606  else
607  {
608  return std::move(is_digit_when_radix_gt_10);
609  }
610  }
611 }
612 
624  const exprt &chr,
625  const typet &char_type,
626  const typet &type,
627  const bool strict_formatting,
628  const unsigned long radix_ul)
629 {
630  const constant_exprt zero_char = from_integer('0', char_type);
631 
634  const binary_relation_exprt upper_case_lower_case_or_digit(
635  chr, ID_ge, zero_char);
636 
637  if(radix_ul <= 10 && radix_ul != 0)
638  {
640  return typecast_exprt(
641  if_exprt(
642  upper_case_lower_case_or_digit,
643  minus_exprt(chr, zero_char),
644  from_integer(0, char_type)),
645  type);
646  }
647  else
648  {
649  const constant_exprt a_char = from_integer('a', char_type);
650  const binary_relation_exprt lower_case(chr, ID_ge, a_char);
651  const constant_exprt A_char = from_integer('A', char_type);
652  const binary_relation_exprt upper_case_or_lower_case(chr, ID_ge, A_char);
653  const constant_exprt ten_int = from_integer(10, char_type);
654 
655  if(strict_formatting)
656  {
659  return typecast_exprt(
660  if_exprt(
661  lower_case,
662  plus_exprt(minus_exprt(chr, a_char), ten_int),
663  if_exprt(
664  upper_case_lower_case_or_digit,
665  minus_exprt(chr, zero_char),
666  from_integer(0, char_type))),
667  type);
668  }
669  else
670  {
674  return typecast_exprt(
675  if_exprt(
676  lower_case,
677  plus_exprt(minus_exprt(chr, a_char), ten_int),
678  if_exprt(
679  upper_case_or_lower_case,
680  plus_exprt(minus_exprt(chr, A_char), ten_int),
681  if_exprt(
682  upper_case_lower_case_or_digit,
683  minus_exprt(chr, zero_char),
684  from_integer(0, char_type)))),
685  type);
686  }
687  }
688 }
689 
697 size_t max_printed_string_length(const typet &type, unsigned long radix_ul)
698 {
699  if(radix_ul == 0)
700  {
701  radix_ul = 2;
702  }
703  double n_bits = static_cast<double>(to_bitvector_type(type).get_width());
704  double radix = static_cast<double>(radix_ul);
705  bool signed_type = type.id() == ID_signedbv;
724  double max = signed_type
725  ? floor(static_cast<double>(n_bits - 1) / log2(radix)) + 2.0
726  : ceil(static_cast<double>(n_bits) / log2(radix));
727  return static_cast<size_t>(max);
728 }
exprt::copy_to_operands
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:150
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
function_application_exprt::arguments
argumentst & arguments()
Definition: mathematical_expr.h:221
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
conjunction
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:51
greater_or_equal_to
binary_relation_exprt greater_or_equal_to(exprt lhs, exprt rhs)
Definition: string_expr.h:19
get_numeric_value_from_character
exprt get_numeric_value_from_character(const exprt &chr, const typet &char_type, const typet &type, const bool strict_formatting, const unsigned long radix_ul)
Get the numeric value of a character, assuming that the radix is large enough.
Definition: string_constraint_generator_valueof.cpp:623
is_number
bool is_number(const typet &type)
Returns true if the type is a rational, real, integer, natural, complex, unsignedbv,...
Definition: mathematical_types.cpp:17
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
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:496
typet
The type of an expression, extends irept.
Definition: type.h:29
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
irept::find
const irept & find(const irep_namet &name) const
Definition: irep.cpp:103
string_constraint_generatort::fresh_symbol
symbol_generatort fresh_symbol
Definition: string_constraint_generator.h:56
and_exprt
Boolean AND.
Definition: std_expr.h:2137
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
string_refinement_invariant.h
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:881
exprt
Base class for all expressions.
Definition: expr.h:53
max_printed_string_length
size_t max_printed_string_length(const typet &type, unsigned long radix_ul)
Calculate the string length needed to represent any value of the given type using the given radix.
Definition: string_constraint_generator_valueof.cpp:697
string_constraintst
Collection of constraints of different types: existential formulas, universal formulas,...
Definition: string_constraint_generator.h:36
array_string_exprt::content
exprt & content()
Definition: string_expr.h:74
bool_typet
The Boolean type.
Definition: std_types.h:37
div_exprt
Division.
Definition: std_expr.h:1031
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::get_conjuncts_for_correct_number_format
std::vector< exprt > get_conjuncts_for_correct_number_format(const array_string_exprt &str, const exprt &radix_as_char, const unsigned long radix_ul, const std::size_t max_size, const bool strict_formatting)
Add axioms making the return value true if the given string is a correct number in the given radix.
Definition: string_constraint_generator_valueof.cpp:280
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_constraint_generatort::add_axioms_for_characters_in_integer_string
string_constraintst add_axioms_for_characters_in_integer_string(const exprt &input_int, const typet &type, const bool strict_formatting, const array_string_exprt &str, const std::size_t max_string_length, const exprt &radix, const unsigned long radix_ul)
Add axioms connecting the characters in the input string to the value of the output integer.
Definition: string_constraint_generator_valueof.cpp:374
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
or_exprt
Boolean OR.
Definition: std_expr.h:2245
string_constraint_generatort::ns
const namespacet ns
Definition: string_constraint_generator.h:60
deprecate.h
string_constraint_generatort::add_axioms_for_parse_int
std::pair< exprt, string_constraintst > add_axioms_for_parse_int(const function_application_exprt &f)
Integer value represented by a string.
Definition: string_constraint_generator_valueof.cpp:525
string_constraint_generatort::unpack_parseint_arguments
parseint_argumentst unpack_parseint_arguments(const function_application_exprt &f, const typet &target_int_type)
Definition: string_constraint_generator_valueof.cpp:459
binary_predicate_exprt
A base class for expressions that are predicates, i.e., Boolean-typed, and that take exactly two argu...
Definition: std_expr.h:694
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
string_constraint_generatort::add_axioms_for_is_valid_int
std::pair< exprt, string_constraintst > add_axioms_for_is_valid_int(const function_application_exprt &f)
Check a string is a valid integer, using the same rules as Java Integer.parseInt.
Definition: string_constraint_generator_valueof.cpp:490
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: std_types.h:1265
function_application_exprt
Application of (mathematical) function.
Definition: mathematical_expr.h:191
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:986
less_than_or_equal_to
binary_relation_exprt less_than_or_equal_to(exprt lhs, exprt rhs)
Definition: string_expr.h:36
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2698
unary_minus_exprt
The unary minus expression.
Definition: std_expr.h:378
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
irept::id
const irep_idt & id() const
Definition: irep.h:418
SINCE
#define SINCE(year, month, day, msg)
Definition: deprecate.h:26
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
get_return_code_type
signedbv_typet get_return_code_type()
Definition: string_constraint_generator_main.cpp:180
is_digit_with_radix
exprt is_digit_with_radix(const exprt &chr, const bool strict_formatting, const exprt &radix_as_char, const unsigned long radix_ul)
Check if a character is a digit with respect to the given radix, e.g.
Definition: string_constraint_generator_valueof.cpp:555
minus_exprt
Binary minus.
Definition: std_expr.h:940
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
simplify_expr.h
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1041
DEPRECATED
#define DEPRECATED(msg)
Definition: deprecate.h:23
function_application_exprt::function
exprt & function()
Definition: mathematical_expr.h:211
string_constraint_generatort::parseint_argumentst
Argument block for parseInt and cousins, common to parseInt itself and CProverString....
Definition: string_constraint_generator.h:311
int_of_hex_char
static exprt int_of_hex_char(const exprt &chr)
Returns the integer value represented by the character.
Definition: string_constraint_generator_valueof.cpp:182
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:725
string_constraint_generatort::add_axioms_from_int_hex
std::pair< exprt, string_constraintst > add_axioms_from_int_hex(const array_string_exprt &res, const exprt &i)
Add axioms stating that the string res corresponds to the integer argument written in hexadecimal.
Definition: string_constraint_generator_valueof.cpp:201
string_constraint_generatort::add_axioms_for_string_of_int
std::pair< exprt, string_constraintst > add_axioms_for_string_of_int(const array_string_exprt &res, const exprt &input_int, size_t max_size)
Add axioms enforcing that the string corresponds to the result of String.valueOf(I) or String....
Definition: string_constraint_generator_valueof.cpp:118
to_integer_or_default
static unsigned long to_integer_or_default(const exprt &expr, unsigned long def, const namespacet &ns)
If the expression is a constant expression then we get the value of it as an unsigned long.
Definition: string_constraint_generator_valueof.cpp:29
implies_exprt
Boolean implication.
Definition: std_expr.h:2200
equal_to
equal_exprt equal_to(exprt lhs, exprt rhs)
Definition: string_expr.h:54
float_bv.h
greater_than
binary_relation_exprt greater_than(exprt lhs, exprt rhs)
Definition: string_expr.h:25
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
string_constraint_generator.h
Generates string constraints to link results from string functions with their arguments.
string_constraint_generatort::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)
Add axioms enforcing that the string corresponds to the result of String.valueOf(II) or String....
Definition: string_constraint_generator_valueof.cpp:138
array_string_exprt
Definition: string_expr.h:67
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1089
string_constraintst::existential
std::vector< exprt > existential
Definition: string_constraint_generator.h:37
not_exprt
Boolean negation.
Definition: std_expr.h:2843