cprover
string_format_builtin_function.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Built-in function for String.format
4 
5 Author: Romain Brenguier, Joel Allred
6 
7 \*******************************************************************/
8 
11 
12 #include <iterator>
13 #include <string>
14 
15 #include "format_specifier.h"
17 #include "string_refinement_util.h"
18 
19 #include <util/bitvector_expr.h>
20 #include <util/message.h>
21 #include <util/range.h>
22 #include <util/simplify_expr.h>
23 
25  const array_string_exprt &string,
26  const irep_idt &id,
27  array_poolt &array_pool);
28 
30  const exprt &return_code,
31  const std::vector<exprt> &fun_args,
32  array_poolt &array_pool)
33  : string_builtin_functiont(return_code, array_pool)
34 {
35  PRECONDITION(fun_args.size() >= 3);
36  result = array_pool.find(fun_args[1], fun_args[0]);
37  const array_string_exprt format_string_expr =
38  get_string_expr(array_pool, fun_args[2]);
39 
40  // List of arguments after the format string
41  inputs = make_range(fun_args.begin() + 3, fun_args.end())
42  .map([&](const exprt &arg) {
43  INVARIANT(
45  "arguments of format should be strings");
46  return get_string_expr(array_pool, arg);
47  })
48  .collect<std::vector<array_string_exprt>>();
49 
50  // format_string is only initialized if the expression is constant
51  if(
52  array_pool.get_or_create_length(format_string_expr).id() == ID_constant &&
53  format_string_expr.content().id() == ID_array)
54  {
55  const auto length = numeric_cast_v<std::size_t>(
56  to_constant_expr(array_pool.get_or_create_length(format_string_expr)));
58  to_array_expr(format_string_expr.content()), length);
59  }
60 }
61 
62 #if 0
63 // This code is deactivated as it is not used for now, but ultimalety this
64 // should be used to throw an exception when the format string is not correct
69 static bool check_format_string(std::string s)
70 {
71  std::string format_specifier=
72  "%(\\d+\\$)?([-#+ 0,(\\<]*)?(\\d+)?(\\.\\d+)?([tT])?([a-zA-Z%])";
73  std::regex regex(format_specifier);
74  std::smatch match;
75 
76  while(std::regex_search(s, match, regex))
77  {
78  if(match.position()!= 0)
79  for(const auto &c : match.str())
80  if(c=='%')
81  return false;
82  s=match.suffix();
83  }
84 
85  for(const auto &c : s)
86  if(c=='%')
87  return false;
88 
89  return true;
90 }
91 #endif
92 
94 static exprt is_null(const array_string_exprt &string, array_poolt &array_pool)
95 {
96  return and_exprt{
97  equal_exprt{array_pool.get_or_create_length(string),
98  from_integer(4, string.length_type())},
99  and_exprt{equal_exprt{string[0], from_integer('n', string[0].type())},
100  equal_exprt{string[1], from_integer('u', string[0].type())},
101  equal_exprt{string[2], from_integer('l', string[0].type())},
102  equal_exprt{string[3], from_integer('l', string[0].type())}}};
103 }
104 
117 static std::pair<array_string_exprt, string_constraintst>
119  string_constraint_generatort &generator,
120  const format_specifiert &fs,
121  const array_string_exprt &string_arg,
122  const typet &index_type,
123  const typet &char_type,
124  const messaget &message)
125 {
126  string_constraintst constraints;
127  array_poolt &array_pool = generator.array_pool;
128  const array_string_exprt res = array_pool.fresh_string(index_type, char_type);
129  std::pair<exprt, string_constraintst> return_code;
130  switch(fs.conversion)
131  {
133  return_code = generator.add_axioms_for_string_of_int(
134  res, format_arg_from_string(string_arg, ID_int, array_pool), 0);
135  return {res, std::move(return_code.second)};
137  return_code = generator.add_axioms_for_string_of_int_with_radix(
138  res,
139  format_arg_from_string(string_arg, ID_int, array_pool),
141  16);
142  return {res, std::move(return_code.second)};
144  return_code = generator.add_axioms_from_float_scientific_notation(
145  res, format_arg_from_string(string_arg, ID_float, array_pool));
146  return {res, std::move(return_code.second)};
148  return_code = generator.add_axioms_for_string_of_float(
149  res, format_arg_from_string(string_arg, ID_float, array_pool));
150  return {res, std::move(return_code.second)};
152  {
153  exprt arg_string = format_arg_from_string(string_arg, ID_char, array_pool);
154  array_string_exprt &string_expr = to_array_string_expr(arg_string);
155  // In the case the arg is null, the result will be equal to "null" and
156  // and otherwise we just take the 4th character of the string.
157  const exprt is_null_literal = is_null(string_expr, array_pool);
158  constraints.existential.push_back(
159  equal_exprt{array_pool.get_or_create_length(res),
160  if_exprt{is_null_literal,
162  from_integer(1, index_type)}});
163  constraints.existential.push_back(implies_exprt{
164  is_null_literal,
166  equal_exprt{res[1], from_integer('u', char_type)},
167  equal_exprt{res[2], from_integer('l', char_type)},
168  equal_exprt{res[3], from_integer('l', char_type)}}});
169  constraints.existential.push_back(implies_exprt{
170  not_exprt{is_null_literal},
171  equal_exprt{res[0], typecast_exprt{string_expr[3], char_type}}});
172  return {res, constraints};
173  }
175  return_code = generator.add_axioms_from_bool(
176  res, format_arg_from_string(string_arg, ID_boolean, array_pool));
177  return {res, std::move(return_code.second)};
179  {
180  const exprt arg_string = string_arg;
181  const array_string_exprt string_expr = to_array_string_expr(arg_string);
182  return {std::move(string_expr), {}};
183  }
185  return_code = generator.add_axioms_for_string_of_int(
186  res, format_arg_from_string(string_arg, "hashcode", array_pool), 0);
187  return {res, std::move(return_code.second)};
189  // TODO: the constant should depend on the system: System.lineSeparator()
190  return_code = generator.add_axioms_for_constant(res, "\n");
191  return {res, std::move(return_code.second)};
193  return_code = generator.add_axioms_for_constant(res, "%");
194  return {res, std::move(return_code.second)};
203  {
204  format_specifiert fs_lower = fs;
205  fs_lower.conversion = tolower(fs.conversion);
206  auto format_specifier_result = add_axioms_for_format_specifier(
207  generator, fs_lower, string_arg, index_type, char_type, message);
208 
209  const exprt return_code_upper_case =
210  generator.fresh_symbol("return_code_upper_case", get_return_code_type());
211  const string_to_upper_case_builtin_functiont upper_case_function(
212  return_code_upper_case, res, format_specifier_result.first, array_pool);
213  auto upper_case_constraints =
214  upper_case_function.constraints(generator.fresh_symbol);
215  merge(upper_case_constraints, std::move(format_specifier_result.second));
216  return {res, std::move(upper_case_constraints)};
217  }
226  // For all these unimplemented cases we return a non-deterministic string
227  message.warning() << "unimplemented format specifier: " << fs.conversion
228  << message.eom;
229  return {array_pool.fresh_string(index_type, char_type), {}};
230  }
231 
232  INVARIANT(false, "format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
233 }
234 
240  const array_string_exprt &string,
241  const irep_idt &id,
242  array_poolt &array_pool)
243 {
244  PRECONDITION(
245  to_array_type(string.content().type()).element_type() ==
246  unsignedbv_typet(16));
247 
248  if(id == "string_expr")
249  return string;
250  if(id == ID_int)
251  {
252  // Assume the string has length 4
253  // (int64)string.content[0] << 48 | (int64) string.content[1] << 32 |
254  // (int64)string.content[2] << 16 | (int64) string.content[3]
255  const signedbv_typet type{64};
256  return bitor_exprt{
257  bitor_exprt{shl_exprt{typecast_exprt{string[0], type}, 48},
258  shl_exprt{typecast_exprt{string[1], type}, 32}},
259  bitor_exprt{shl_exprt{typecast_exprt{string[2], type}, 16},
260  typecast_exprt{string[3], type}}};
261  }
262 
263  if(id == ID_char)
264  {
265  // Leave the string unchanged as the "null" string is used to represent null
266  return string;
267  }
268  if(id == ID_boolean)
269  {
270  // We assume the string has length exactly 4, if it is "null" return false
271  // and otherwise ignore the first 3 and return (bool)string.content[3]
272  return if_exprt{is_null(string, array_pool),
273  false_exprt{},
274  typecast_exprt{string[3], bool_typet()}};
275  }
276  if(id == ID_float)
277  {
278  // Deserialize an int and cast to float
279  const exprt as_int = format_arg_from_string(string, ID_int, array_pool);
280  return typecast_exprt{as_int, floatbv_typet{}};
281  }
283 }
284 
293 static std::pair<exprt, string_constraintst> add_axioms_for_format(
294  string_constraint_generatort &generator,
295  const array_string_exprt &res,
296  const std::string &s,
297  const std::vector<array_string_exprt> &args,
298  const messaget &message)
299 {
300  string_constraintst constraints;
301  array_poolt &array_pool = generator.array_pool;
302  const std::vector<format_elementt> format_strings = parse_format_string(s);
303  std::vector<array_string_exprt> intermediary_strings;
304  std::size_t arg_count = 0;
306  const typet &index_type = res.length_type();
307 
308  array_string_exprt string_arg;
309 
310  for(const format_elementt &fe : format_strings)
311  {
312  if(fe.is_format_specifier())
313  {
314  const format_specifiert &fs = fe.get_format_specifier();
315 
316  if(
319  {
320  if(fs.index == -1)
321  {
322  INVARIANT(
323  arg_count < args.size(), "number of format must match specifiers");
324  string_arg = args[arg_count++];
325  }
326  else
327  {
328  INVARIANT(fs.index > 0, "index in format should be positive");
329  INVARIANT(
330  static_cast<std::size_t>(fs.index) <= args.size(),
331  "number of format must match specifiers");
332 
333  // first argument `args[0]` corresponds to index 1
334  string_arg = args[fs.index - 1];
335  }
336  }
337 
338  auto result = add_axioms_for_format_specifier(
339  generator, fs, string_arg, index_type, char_type, message);
340  merge(constraints, std::move(result.second));
341  intermediary_strings.push_back(result.first);
342  }
343  else
344  {
345  const array_string_exprt str =
346  array_pool.fresh_string(index_type, char_type);
347  auto result = generator.add_axioms_for_constant(
348  str, fe.get_format_text().get_content());
349  merge(constraints, result.second);
350  intermediary_strings.push_back(str);
351  }
352  }
353 
354  exprt return_code = from_integer(0, get_return_code_type());
355 
356  if(intermediary_strings.empty())
357  {
358  constraints.existential.push_back(equal_exprt(
359  array_pool.get_or_create_length(res), from_integer(0, index_type)));
360  return {return_code, constraints};
361  }
362 
363  array_string_exprt str = intermediary_strings[0];
364 
365  if(intermediary_strings.size() == 1)
366  {
367  // Copy the first string
368  auto result = generator.add_axioms_for_substring(
369  res,
370  str,
372  generator.array_pool.get_or_create_length(str));
373  merge(constraints, std::move(result.second));
374  return {result.first, std::move(constraints)};
375  }
376 
377  // start after the first string and stop before the last
378  for(std::size_t i = 1; i < intermediary_strings.size() - 1; ++i)
379  {
380  const array_string_exprt &intermediary = intermediary_strings[i];
381  const array_string_exprt fresh =
382  array_pool.fresh_string(index_type, char_type);
383  auto result = generator.add_axioms_for_concat(fresh, str, intermediary);
384  return_code = maximum(return_code, result.first);
385  merge(constraints, std::move(result.second));
386  str = fresh;
387  }
388 
389  auto result =
390  generator.add_axioms_for_concat(res, str, intermediary_strings.back());
391  merge(constraints, std::move(result.second));
392  return {maximum(result.first, return_code), std::move(constraints)};
393 }
394 
395 static std::vector<mp_integer> deserialize_constant_int_arg(
396  const std::vector<mp_integer> serialized,
397  const unsigned base)
398 {
399  PRECONDITION(serialized.size() == 4);
400 
401  // long value, to be used for other formats?
402  for(std::size_t i = 0; i < 4; i++)
403  {
405  serialized[i] <= 0xFFFF,
406  "Component of serialized value to"
407  "format must be bounded by 0xFFFF");
408  }
409 
410  const int64_t int64_value =
411  (serialized[0] << 48).to_long() | (serialized[1] << 32).to_long() |
412  (serialized[2] << 16).to_long() | serialized[3].to_long();
413  const mp_integer mp_integer_value{int64_value};
414  const std::string long_as_string = integer2string(mp_integer_value, base);
415 
416  return make_range(long_as_string).map([&](char c) { return mp_integer{c}; });
417 }
418 
419 static bool eval_is_null(const std::vector<mp_integer> &string)
420 {
421  return string.size() == 4 && string[0] == 'n' && string[1] == 'u' &&
422  string[2] == 'l' && string[3] == 'l';
423 }
424 
427 static std::vector<mp_integer> eval_format_specifier(
428  const format_specifiert &fs,
429  const std::vector<mp_integer> &arg)
430 {
431  switch(fs.conversion)
432  {
434  {
435  if(eval_is_null(arg))
436  return std::vector<mp_integer>{'n', 'u', 'l', 'l'};
437  return deserialize_constant_int_arg(arg, 10);
438  }
440  {
441  if(eval_is_null(arg))
442  return std::vector<mp_integer>{'n', 'u', 'l', 'l'};
443  auto upper_case_hex = deserialize_constant_int_arg(arg, 16);
444  // convert to lower case
445  return make_range(upper_case_hex).map([](const mp_integer &c) {
446  if('A' <= c && c <= 'Z')
447  return c + 0x20;
448  return c;
449  });
450  }
452  {
453  if(eval_is_null(arg))
454  return std::vector<mp_integer>{'n', 'u', 'l', 'l'};
455  return deserialize_constant_int_arg(arg, 16);
456  }
462  {
463  if(eval_is_null(arg))
464  return std::vector<mp_integer>{'n', 'u', 'l', 'l'};
465  return std::vector<mp_integer>{arg[3]};
466  }
468  {
469  if(arg[3] == 1)
470  return std::vector<mp_integer>{'t', 'r', 'u', 'e'};
471  return std::vector<mp_integer>{'f', 'a', 'l', 's', 'e'};
472  }
474  return arg;
478  // TODO: the constant should depend on the system: System.lineSeparator()
479  return std::vector<mp_integer>{'\n'};
481  return std::vector<mp_integer>{'%'};
490  {
491  format_specifiert fs_lower = fs;
492  fs_lower.conversion = tolower(fs.conversion);
493  auto lower_case = eval_format_specifier(fs_lower, arg);
494  return make_range(lower_case).map([](const mp_integer &c) {
495  // TODO: incomplete
496  if('a' <= c && c <= 'z')
497  return c - 0x20;
498  return c;
499  });
500  }
510  }
511 
512  INVARIANT(false, "format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
513 }
514 
516  const std::function<exprt(const exprt &)> &get_value) const
517 {
518  if(!format_string.has_value())
519  return {};
520 
521  const std::vector<format_elementt> format_strings =
523  std::vector<mp_integer> result_vector;
524  std::size_t arg_count = 0;
525 
526  for(const format_elementt &fe : format_strings)
527  {
528  if(fe.is_format_specifier())
529  {
530  const format_specifiert &fs = fe.get_format_specifier();
531  if(
534  {
535  std::vector<mp_integer> evaluated_char_vector;
536 
537  if(fs.index == -1)
538  {
539  INVARIANT(
540  arg_count < inputs.size(),
541  "number of format must match specifiers");
542  if(auto arg_value = eval_string(inputs[arg_count++], get_value))
543  evaluated_char_vector = eval_format_specifier(fs, *arg_value);
544  else
545  return {};
546  }
547  else
548  {
549  INVARIANT(fs.index > 0, "index in format should be positive");
550  INVARIANT(
551  static_cast<std::size_t>(fs.index) <= inputs.size(),
552  "number of format must match specifiers");
553 
554  // first argument `args[0]` corresponds to index 1
555  if(auto arg_value = eval_string(inputs[fs.index - 1], get_value))
556  evaluated_char_vector = eval_format_specifier(fs, *arg_value);
557  else
558  return {};
559  }
560  std::move(
561  evaluated_char_vector.begin(),
562  evaluated_char_vector.end(),
563  std::back_inserter(result_vector));
564  }
566  {
567  result_vector.push_back('%');
568  }
569  else
570  {
571  // TODO: the character should depend on the system:
572  // System.lineSeparator()
573  result_vector.push_back('\n');
574  }
575  }
576  else
577  {
578  for(char c : fe.get_format_text().get_content())
579  result_vector.emplace_back(c);
580  }
581  }
582  return make_string(result_vector, to_array_type(result.type()));
583 }
584 
586  string_constraint_generatort &generator) const
587 {
588  // When `format_string` was not set, leave the result non-deterministic
589  if(!format_string.has_value())
590  return {};
591 
592  null_message_handlert message_handler;
593  auto result_constraint_pair = add_axioms_for_format(
594  generator,
595  result,
596  format_string.value(),
597  inputs,
598  // TODO: get rid of this argument
599  messaget{message_handler});
600  INVARIANT(
601  simplify_expr(result_constraint_pair.first, generator.ns).is_zero(),
602  "add_axioms_for_format should return 0, meaning that formatting was"
603  "successful");
604  result_constraint_pair.second.existential.push_back(
606  return result_constraint_pair.second;
607 }
608 
625  const exprt &pos_integer,
626  int max_length,
627  const typet &length_type,
628  const unsigned long radix)
629 {
630  if(max_length <= 1)
631  return from_integer(1, length_type);
632 
633  // If the current value doesn't fit in a smaller size representation, we have
634  // found the number of digits needed to represent that value.
635  const mp_integer max_value_for_smaller_size =
636  pow((mp_integer)radix, max_length - 1);
637  return if_exprt{
638  less_than(
639  pos_integer,
640  from_integer(max_value_for_smaller_size, pos_integer.type())),
642  pos_integer, max_length - 1, length_type, radix),
643  from_integer(max_length, length_type)};
644 }
645 
653  const exprt &integer,
654  const typet &length_type,
655  const unsigned long radix)
656 {
657  int max_pos_int_length;
658  if(length_type == signedbv_typet(32))
659  {
660  if(radix == 10)
661  max_pos_int_length = 10;
662  else if(radix == 16)
663  max_pos_int_length = 8;
664  else
666  }
667  else
668  {
669  // We only handle 32-bit signed integer type for now.
671  }
672 
673  return if_exprt{
674  greater_or_equal_to(integer, from_integer(0, integer.type())),
676  integer, max_pos_int_length, length_type, radix),
677  plus_exprt{
679  unary_minus_exprt{integer}, max_pos_int_length, length_type, radix),
680  from_integer(1, length_type)}};
681 }
682 
686  const format_specifiert &fs,
687  const array_string_exprt &arg,
688  const typet &index_type,
689  array_poolt &array_pool)
690 {
691  switch(fs.conversion)
692  {
694  {
695  return if_exprt(
696  is_null(arg, array_pool),
699  format_arg_from_string(arg, ID_int, array_pool), index_type, 10));
700  }
703  {
704  return length_of_decimal_int(
705  format_arg_from_string(arg, ID_int, array_pool), index_type, 16);
706  }
713  {
714  const exprt arg_string = format_arg_from_string(arg, ID_char, array_pool);
715  const array_string_exprt &string_expr = to_array_string_expr(arg_string);
716  // In the case the arg is null, the result will be equal to "null" and
717  // and otherwise we just take the 4th character of the string.
718  return if_exprt{is_null(string_expr, array_pool),
721  }
724  {
725  return if_exprt{format_arg_from_string(arg, ID_boolean, array_pool),
728  }
731  {
732  const exprt arg_string =
733  format_arg_from_string(arg, "string_expr", array_pool);
734  const array_string_exprt string_expr = to_array_string_expr(arg_string);
735  return array_pool.get_or_create_length(string_expr);
736  }
740  // TODO: the constant should depend on the system: System.lineSeparator()
741  return from_integer(1, index_type);
743  return from_integer(1, index_type);
749  {
750  return length_for_format_specifier(fs, arg, index_type, array_pool);
751  }
760  // For all these unimplemented cases we return a non-deterministic string
762  }
763 
764  INVARIANT(false, "format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
765 }
766 
768 {
769  if(!format_string.has_value())
770  return true_exprt{};
771 
773  const std::vector<format_elementt> format_strings =
775  std::vector<exprt> intermediary_string_lengths;
776  std::size_t arg_count = 0;
777  const typet &index_type = result.length_type();
778 
779  for(const format_elementt &fe : format_strings)
780  {
781  if(fe.is_format_specifier())
782  {
783  const format_specifiert &fs = fe.get_format_specifier();
784  array_string_exprt arg;
785  if(
788  {
789  if(fs.index == -1)
790  {
791  INVARIANT(
792  arg_count < inputs.size(),
793  "number of format must match specifiers");
794  arg = inputs[arg_count++];
795  }
796  else
797  {
798  INVARIANT(fs.index > 0, "index in format should be positive");
799  INVARIANT(
800  static_cast<std::size_t>(fs.index) <= inputs.size(),
801  "number of format must match specifiers");
802 
803  // first argument `args[0]` corresponds to index 1
804  arg = inputs[fs.index - 1];
805  }
806  }
807  intermediary_string_lengths.push_back(
809  }
810  else
811  {
812  intermediary_string_lengths.push_back(from_integer(
813  fe.get_format_text().get_content().size(), result.length_type()));
814  }
815  }
816 
817  constraints.push_back(
819 
820  if(intermediary_string_lengths.empty())
821  {
822  constraints.push_back(equal_exprt(
824  return conjunction(constraints);
825  }
826 
827  exprt total_length = intermediary_string_lengths[0];
828  for(std::size_t i = 1; i < intermediary_string_lengths.size(); ++i)
829  {
830  total_length =
831  plus_exprt{std::move(total_length), intermediary_string_lengths[i]};
832  }
834  std::move(total_length)});
835 
836  return conjunction(constraints);
837 }
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
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:199
API to expression classes for bitvectors.
bitvector_typet index_type()
Definition: c_types.cpp:22
bitvector_typet char_type()
Definition: c_types.cpp:124
Boolean AND.
Definition: std_expr.h:1974
Correspondance between arrays and pointers string representations.
Definition: array_pool.h:42
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:26
array_string_exprt fresh_string(const typet &index_type, const typet &char_type)
Construct a string expression whose length and content are new variables.
Definition: array_pool.cpp:57
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:184
const typet & length_type() const
Definition: string_expr.h:69
exprt & content()
Definition: string_expr.h:74
Bit-wise OR.
The Boolean type.
Definition: std_types.h:36
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:64
typet & type()
Return the type of the expression.
Definition: expr.h:82
The Boolean constant false.
Definition: std_expr.h:2865
Fixed-width bit-vector with IEEE floating-point interpretation.
Field names follow the OpenJDK implementation: http://hg.openjdk.java.net/jdk7/jdk7/jdk/file/9b8c96f9...
static const char STRING_UPPER
static const char OCTAL_INTEGER
static const char SCIENTIFIC
static const char PERCENT_SIGN
static const char DATE_TIME_UPPER
static const char SCIENTIFIC_UPPER
static const char HEXADECIMAL_INTEGER
static const char DATE_TIME
static const char BOOLEAN_UPPER
static const char STRING
static const char CHARACTER
static const char HASHCODE
static const char GENERAL
static const char HEXADECIMAL_INTEGER_UPPER
static const char HASHCODE_UPPER
static const char HEXADECIMAL_FLOAT_UPPER
static const char BOOLEAN
static const char DECIMAL_FLOAT
static const char CHARACTER_UPPER
static const char GENERAL_UPPER
static const char DECIMAL_INTEGER
static const char HEXADECIMAL_FLOAT
static const char LINE_SEPARATOR
The trinary if-then-else operator.
Definition: std_expr.h:2226
Boolean implication.
Definition: std_expr.h:2037
const irep_idt & id() const
Definition: irep.h:396
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & warning() const
Definition: message.h:404
static eomt eom
Definition: message.h:297
Boolean negation.
Definition: std_expr.h:2181
The plus expression Associativity is not specified.
Definition: std_expr.h:914
Left shift.
Fixed-width bit-vector with two's complement interpretation.
Base class for string functions that are built in the solver.
std::pair< exprt, string_constraintst > add_axioms_for_substring(const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end)
Add axioms ensuring that res corresponds to the substring of str between indexes ‘start’ = max(start,...
std::pair< exprt, string_constraintst > add_axioms_for_concat(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
Add axioms enforcing that res is equal to the concatenation of s1 and s2.
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....
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....
std::pair< exprt, string_constraintst > add_axioms_from_bool(const function_application_exprt &f)
std::pair< exprt, string_constraintst > add_axioms_from_float_scientific_notation(const array_string_exprt &res, const exprt &f)
Add axioms to write the float in scientific notation.
std::pair< exprt, string_constraintst > add_axioms_for_string_of_float(const function_application_exprt &f)
String representation of a float value.
std::pair< exprt, string_constraintst > add_axioms_for_constant(const array_string_exprt &res, irep_idt sval, const exprt &guard=true_exprt())
Add axioms ensuring that the provided string expression and constant are equal.
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...
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
optionalt< std::string > format_string
Only set when the format string is a constant.
string_format_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Constructor from arguments of a function application.
std::vector< array_string_exprt > inputs
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 ...
Converting each lowercase character of Basic Latin and Latin-1 supplement to the corresponding upperc...
string_constraintst constraints(class symbol_generatort &fresh_symbol) const
Set of constraints ensuring result corresponds to input in which lowercase characters of Basic Latin ...
The Boolean constant true.
Definition: std_expr.h:2856
const typet & subtype() const
Definition: type.h:156
Semantic type conversion.
Definition: std_expr.h:1920
The type of an expression, extends irept.
Definition: type.h:29
The unary minus expression.
Definition: std_expr.h:390
Fixed-width bit-vector with unsigned binary interpretation.
Format specifiers for String.format.
format_token_listt parse_format_string(const std::string &arg_string)
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:103
nonstd::optional< T > optionalt
Definition: optional.h:35
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
bool is_refined_string_type(const typet &type)
exprt simplify_expr(exprt src, const namespacet &ns)
BigInt mp_integer
Definition: smt_terms.h:12
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define UNIMPLEMENTED
Definition: invariant.h:525
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
#define UNHANDLED_CASE
Definition: invariant.h:526
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:34
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1506
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
static array_string_exprt make_string(Iter begin, Iter end, const array_typet &array_type)
optionalt< std::vector< mp_integer > > eval_string(const array_string_exprt &a, const std::function< exprt(const exprt &)> &get_value)
Given a function get_value which gives a valuation to expressions, attempt to find the current value ...
exprt maximum(const exprt &a, const exprt &b)
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.
signedbv_typet get_return_code_type()
binary_relation_exprt less_than(exprt lhs, exprt rhs)
Definition: string_expr.h:48
array_string_exprt & to_array_string_expr(exprt &expr)
Definition: string_expr.h:95
binary_relation_exprt greater_or_equal_to(exprt lhs, exprt rhs)
Definition: string_expr.h:19
static std::pair< exprt, string_constraintst > add_axioms_for_format(string_constraint_generatort &generator, const array_string_exprt &res, const std::string &s, const std::vector< array_string_exprt > &args, const messaget &message)
Parse s and add axioms ensuring the output corresponds to the output of String.format.
static exprt format_arg_from_string(const array_string_exprt &string, const irep_idt &id, array_poolt &array_pool)
Deserialize an argument for format from string.
static std::pair< array_string_exprt, string_constraintst > add_axioms_for_format_specifier(string_constraint_generatort &generator, const format_specifiert &fs, const array_string_exprt &string_arg, const typet &index_type, const typet &char_type, const messaget &message)
Parse s and add axioms ensuring the output corresponds to the output of String.format.
static std::vector< mp_integer > eval_format_specifier(const format_specifiert &fs, const std::vector< mp_integer > &arg)
Return the string to replace the format specifier, as a vector of characters.
static exprt length_of_positive_decimal_int(const exprt &pos_integer, int max_length, const typet &length_type, const unsigned long radix)
Return an new expression representing the length of the representation of integer.
static bool eval_is_null(const std::vector< mp_integer > &string)
exprt length_of_decimal_int(const exprt &integer, const typet &length_type, const unsigned long radix)
Compute the length of the decimal representation of an integer.
static std::vector< mp_integer > deserialize_constant_int_arg(const std::vector< mp_integer > serialized, const unsigned base)
static exprt is_null(const array_string_exprt &string, array_poolt &array_pool)
Expression which is true when the string is equal to the literal "null".
exprt length_for_format_specifier(const format_specifiert &fs, const array_string_exprt &arg, const typet &index_type, array_poolt &array_pool)
Return an expression representing the length of the format specifier Does not assume that arg is cons...
Built-in function for String.format.
std::string utf16_constant_array_to_java(const array_exprt &arr, std::size_t length)
Construct a string from a constant array.
Collection of constraints of different types: existential formulas, universal formulas,...
std::vector< exprt > existential
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:177