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  merge(result2, 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 
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  string_constraintst constraints;
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  constraints.existential.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  constraints.existential.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  constraints.existential.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  constraints.existential.push_back(contains_digit);
322 
323  // |str| <= max_size
324  constraints.existential.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  constraints.existential.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  constraints.existential.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  constraints.existential.push_back(no_leading_zero_after_minus);
357  }
358  return constraints;
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 
465 std::pair<exprt, string_constraintst>
468 {
469  PRECONDITION(f.arguments().size() == 1 || f.arguments().size() == 2);
471  const typet &type = f.type();
472  PRECONDITION(type.id() == ID_signedbv);
473  const exprt radix =
474  f.arguments().size() == 1
475  ? static_cast<exprt>(from_integer(10, type))
476  : static_cast<exprt>(typecast_exprt(f.arguments()[1], type));
477  // Most of the time we can evaluate radix as an integer. The value 0 is used
478  // to indicate when we can't tell what the radix is.
479  const unsigned long radix_ul = to_integer_or_default(radix, 0, ns);
480  PRECONDITION((radix_ul >= 2 && radix_ul <= 36) || radix_ul == 0);
481 
482  const symbol_exprt input_int = fresh_symbol("parsed_int", type);
483  const typet &char_type = str.content().type().subtype();
484  const typecast_exprt radix_as_char(radix, char_type);
485  const bool strict_formatting = false;
486 
487  const std::size_t max_string_length =
488  max_printed_string_length(type, radix_ul);
489 
494  auto constraints1 = add_axioms_for_correct_number_format(
495  str, radix_as_char, radix_ul, max_string_length, strict_formatting);
496 
498  input_int,
499  type,
500  strict_formatting,
501  str,
502  max_string_length,
503  radix,
504  radix_ul);
505  merge(constraints2, std::move(constraints1));
506 
507  return {input_int, std::move(constraints2)};
508 }
509 
519  const exprt &chr,
520  const bool strict_formatting,
521  const exprt &radix_as_char,
522  const unsigned long radix_ul)
523 {
524  PRECONDITION((radix_ul >= 2 && radix_ul <= 36) || radix_ul == 0);
525  const typet &char_type = chr.type();
526  const exprt zero_char = from_integer('0', char_type);
527 
528  const and_exprt is_digit_when_radix_le_10(
529  binary_relation_exprt(chr, ID_ge, zero_char),
530  binary_relation_exprt(chr, ID_lt, plus_exprt(zero_char, radix_as_char)));
531 
532  if(radix_ul <= 10 && radix_ul != 0)
533  {
534  return is_digit_when_radix_le_10;
535  }
536  else
537  {
538  const exprt nine_char = from_integer('9', char_type);
539  const exprt a_char = from_integer('a', char_type);
540  const constant_exprt ten_char_type = from_integer(10, char_type);
541 
542  const minus_exprt radix_minus_ten(radix_as_char, ten_char_type);
543 
544  or_exprt is_digit_when_radix_gt_10(
545  and_exprt(
546  binary_relation_exprt(chr, ID_ge, zero_char),
547  binary_relation_exprt(chr, ID_le, nine_char)),
548  and_exprt(
549  binary_relation_exprt(chr, ID_ge, a_char),
551  chr, ID_lt, plus_exprt(a_char, radix_minus_ten))));
552 
553  if(!strict_formatting)
554  {
555  exprt A_char = from_integer('A', char_type);
556  is_digit_when_radix_gt_10.copy_to_operands(and_exprt(
557  binary_relation_exprt(chr, ID_ge, A_char),
559  chr, ID_lt, plus_exprt(A_char, radix_minus_ten))));
560  }
561 
562  if(radix_ul == 0)
563  {
564  return if_exprt(
565  binary_relation_exprt(radix_as_char, ID_le, ten_char_type),
566  is_digit_when_radix_le_10,
567  is_digit_when_radix_gt_10);
568  }
569  else
570  {
571  return std::move(is_digit_when_radix_gt_10);
572  }
573  }
574 }
575 
587  const exprt &chr,
588  const typet &char_type,
589  const typet &type,
590  const bool strict_formatting,
591  const unsigned long radix_ul)
592 {
593  const constant_exprt zero_char = from_integer('0', char_type);
594 
597  const binary_relation_exprt upper_case_lower_case_or_digit(
598  chr, ID_ge, zero_char);
599 
600  if(radix_ul <= 10 && radix_ul != 0)
601  {
603  return typecast_exprt(
604  if_exprt(
605  upper_case_lower_case_or_digit,
606  minus_exprt(chr, zero_char),
607  from_integer(0, char_type)),
608  type);
609  }
610  else
611  {
612  const constant_exprt a_char = from_integer('a', char_type);
613  const binary_relation_exprt lower_case(chr, ID_ge, a_char);
614  const constant_exprt A_char = from_integer('A', char_type);
615  const binary_relation_exprt upper_case_or_lower_case(chr, ID_ge, A_char);
616  const constant_exprt ten_int = from_integer(10, char_type);
617 
618  if(strict_formatting)
619  {
622  return typecast_exprt(
623  if_exprt(
624  lower_case,
625  plus_exprt(minus_exprt(chr, a_char), ten_int),
626  if_exprt(
627  upper_case_lower_case_or_digit,
628  minus_exprt(chr, zero_char),
629  from_integer(0, char_type))),
630  type);
631  }
632  else
633  {
637  return typecast_exprt(
638  if_exprt(
639  lower_case,
640  plus_exprt(minus_exprt(chr, a_char), ten_int),
641  if_exprt(
642  upper_case_or_lower_case,
643  plus_exprt(minus_exprt(chr, A_char), ten_int),
644  if_exprt(
645  upper_case_lower_case_or_digit,
646  minus_exprt(chr, zero_char),
647  from_integer(0, char_type)))),
648  type);
649  }
650  }
651 }
652 
660 size_t max_printed_string_length(const typet &type, unsigned long radix_ul)
661 {
662  if(radix_ul == 0)
663  {
664  radix_ul = 2;
665  }
666  double n_bits = static_cast<double>(to_bitvector_type(type).get_width());
667  double radix = static_cast<double>(radix_ul);
668  bool signed_type = type.id() == ID_signedbv;
687  double max = signed_type
688  ? floor(static_cast<double>(n_bits - 1) / log2(radix)) + 2.0
689  : ceil(static_cast<double>(n_bits) / log2(radix));
690  return static_cast<size_t>(max);
691 }
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:148
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
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:586
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:2993
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:2166
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:887
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:660
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:1037
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:1196
string_constraint_generatort::array_pool
array_poolt array_pool
Definition: string_constraint_generator.h:58
string_constraint_generatort
Definition: string_constraint_generator.h:45
merge
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.
Definition: string_constraint_generator_main.cpp:100
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:2274
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:466
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
function_application_exprt
Application of (mathematical) function.
Definition: mathematical_expr.h:191
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:992
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
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:518
minus_exprt
Binary minus.
Definition: std_expr.h:946
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
string_constraint_generatort::add_axioms_for_correct_number_format
string_constraintst add_axioms_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
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:2229
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:2042
true_exprt
The Boolean constant true.
Definition: std_expr.h:3984
constant_exprt
A constant literal expression.
Definition: std_expr.h:3935
string_constraint_generator.h
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:2872