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 <math.h>
14 #include <string>
15 
16 #include "format_specifier.h"
18 #include "string_refinement_util.h"
19 
20 #include <util/bitvector_expr.h>
21 #include <util/range.h>
22 #include <util/simplify_expr.h>
23 #include <util/symbol_table.h>
24 
26  const array_string_exprt &string,
27  const irep_idt &id,
28  array_poolt &array_pool);
29 
31  const exprt &return_code,
32  const std::vector<exprt> &fun_args,
33  array_poolt &array_pool)
34  : string_builtin_functiont(return_code, array_pool)
35 {
36  PRECONDITION(fun_args.size() >= 3);
37  result = array_pool.find(fun_args[1], fun_args[0]);
38  const array_string_exprt format_string_expr =
39  get_string_expr(array_pool, fun_args[2]);
40 
41  // List of arguments after the format string
42  inputs = make_range(fun_args.begin() + 3, fun_args.end())
43  .map([&](const exprt &arg) {
44  INVARIANT(
46  "arguments of format should be strings");
47  return get_string_expr(array_pool, arg);
48  })
49  .collect<std::vector<array_string_exprt>>();
50 
51  // format_string is only initialized if the expression is constant
52  if(
53  array_pool.get_or_create_length(format_string_expr).id() == ID_constant &&
54  format_string_expr.content().id() == ID_array)
55  {
56  const auto length = numeric_cast_v<std::size_t>(
57  to_constant_expr(array_pool.get_or_create_length(format_string_expr)));
59  to_array_expr(format_string_expr.content()), length);
60  }
61 }
62 
63 #if 0
64 // This code is deactivated as it is not used for now, but ultimalety this
65 // should be used to throw an exception when the format string is not correct
70 static bool check_format_string(std::string s)
71 {
72  std::string format_specifier=
73  "%(\\d+\\$)?([-#+ 0,(\\<]*)?(\\d+)?(\\.\\d+)?([tT])?([a-zA-Z%])";
74  std::regex regex(format_specifier);
75  std::smatch match;
76 
77  while(std::regex_search(s, match, regex))
78  {
79  if(match.position()!= 0)
80  for(const auto &c : match.str())
81  if(c=='%')
82  return false;
83  s=match.suffix();
84  }
85 
86  for(const auto &c : s)
87  if(c=='%')
88  return false;
89 
90  return true;
91 }
92 #endif
93 
95 static exprt is_null(const array_string_exprt &string, array_poolt &array_pool)
96 {
97  return and_exprt{
98  equal_exprt{array_pool.get_or_create_length(string),
99  from_integer(4, string.length_type())},
100  and_exprt{equal_exprt{string[0], from_integer('n', string[0].type())},
101  equal_exprt{string[1], from_integer('u', string[0].type())},
102  equal_exprt{string[2], from_integer('l', string[0].type())},
103  equal_exprt{string[3], from_integer('l', string[0].type())}}};
104 }
105 
118 static std::pair<array_string_exprt, string_constraintst>
120  string_constraint_generatort &generator,
121  const format_specifiert &fs,
122  const array_string_exprt &string_arg,
123  const typet &index_type,
124  const typet &char_type,
125  const messaget &message)
126 {
127  string_constraintst constraints;
128  array_poolt &array_pool = generator.array_pool;
129  const array_string_exprt res = array_pool.fresh_string(index_type, char_type);
130  std::pair<exprt, string_constraintst> return_code;
131  switch(fs.conversion)
132  {
134  return_code = generator.add_axioms_for_string_of_int(
135  res, format_arg_from_string(string_arg, ID_int, array_pool), 0);
136  return {res, std::move(return_code.second)};
138  return_code = generator.add_axioms_for_string_of_int_with_radix(
139  res,
140  format_arg_from_string(string_arg, ID_int, array_pool),
142  16);
143  return {res, std::move(return_code.second)};
145  return_code = generator.add_axioms_from_float_scientific_notation(
146  res, format_arg_from_string(string_arg, ID_float, array_pool));
147  return {res, std::move(return_code.second)};
149  return_code = generator.add_axioms_for_string_of_float(
150  res, format_arg_from_string(string_arg, ID_float, array_pool));
151  return {res, std::move(return_code.second)};
153  {
154  exprt arg_string = format_arg_from_string(string_arg, ID_char, array_pool);
155  array_string_exprt &string_expr = to_array_string_expr(arg_string);
156  // In the case the arg is null, the result will be equal to "null" and
157  // and otherwise we just take the 4th character of the string.
158  const exprt is_null_literal = is_null(string_expr, array_pool);
159  constraints.existential.push_back(
160  equal_exprt{array_pool.get_or_create_length(res),
161  if_exprt{is_null_literal,
163  from_integer(1, index_type)}});
164  constraints.existential.push_back(implies_exprt{
165  is_null_literal,
167  equal_exprt{res[1], from_integer('u', char_type)},
168  equal_exprt{res[2], from_integer('l', char_type)},
169  equal_exprt{res[3], from_integer('l', char_type)}}});
170  constraints.existential.push_back(implies_exprt{
171  not_exprt{is_null_literal},
172  equal_exprt{res[0], typecast_exprt{string_expr[3], char_type}}});
173  return {res, constraints};
174  }
176  return_code = generator.add_axioms_from_bool(
177  res, format_arg_from_string(string_arg, ID_boolean, array_pool));
178  return {res, std::move(return_code.second)};
180  {
181  const exprt arg_string = string_arg;
182  const array_string_exprt string_expr = to_array_string_expr(arg_string);
183  return {std::move(string_expr), {}};
184  }
186  return_code = generator.add_axioms_for_string_of_int(
187  res, format_arg_from_string(string_arg, "hashcode", array_pool), 0);
188  return {res, std::move(return_code.second)};
190  // TODO: the constant should depend on the system: System.lineSeparator()
191  return_code = generator.add_axioms_for_constant(res, "\n");
192  return {res, std::move(return_code.second)};
194  return_code = generator.add_axioms_for_constant(res, "%");
195  return {res, std::move(return_code.second)};
204  {
205  format_specifiert fs_lower = fs;
206  fs_lower.conversion = tolower(fs.conversion);
207  auto format_specifier_result = add_axioms_for_format_specifier(
208  generator, fs_lower, string_arg, index_type, char_type, message);
209 
210  const exprt return_code_upper_case =
211  generator.fresh_symbol("return_code_upper_case", get_return_code_type());
212  const string_to_upper_case_builtin_functiont upper_case_function(
213  return_code_upper_case, res, format_specifier_result.first, array_pool);
214  auto upper_case_constraints =
215  upper_case_function.constraints(generator.fresh_symbol);
216  merge(upper_case_constraints, std::move(format_specifier_result.second));
217  return {res, std::move(upper_case_constraints)};
218  }
227  // For all these unimplemented cases we return a non-deterministic string
228  message.warning() << "unimplemented format specifier: " << fs.conversion
229  << message.eom;
230  return {array_pool.fresh_string(index_type, char_type), {}};
231  }
232 
233  INVARIANT(false, "format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
234 }
235 
241  const array_string_exprt &string,
242  const irep_idt &id,
243  array_poolt &array_pool)
244 {
245  PRECONDITION(
246  to_array_type(string.content().type()).subtype() == 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;
305  const typet &char_type = res.content().type().subtype();
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 }
messaget
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
format_specifiert::LINE_SEPARATOR
static const char LINE_SEPARATOR
Definition: format_specifier.h:47
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
UNIMPLEMENTED
#define UNIMPLEMENTED
Definition: invariant.h:523
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:41
format_specifiert::BOOLEAN
static const char BOOLEAN
Definition: format_specifier.h:41
parse_format_string
format_token_listt parse_format_string(const std::string &arg_string)
Definition: format_strings.cpp:187
greater_or_equal_to
binary_relation_exprt greater_or_equal_to(exprt lhs, exprt rhs)
Definition: string_expr.h:19
format_specifiert::DECIMAL_FLOAT
static const char DECIMAL_FLOAT
Definition: format_specifier.h:34
string_constraint_generatort::add_axioms_for_substring
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,...
Definition: string_constraint_generator_transformation.cpp:122
to_array_expr
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1411
format_specifiert::HEXADECIMAL_FLOAT
static const char HEXADECIMAL_FLOAT
Definition: format_specifier.h:35
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:184
format_specifiert::CHARACTER
static const char CHARACTER
Definition: format_specifier.h:37
length_for_format_specifier
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...
Definition: string_format_builtin_function.cpp:685
typet
The type of an expression, extends irept.
Definition: type.h:28
format_specifiert::PERCENT_SIGN
static const char PERCENT_SIGN
Definition: format_specifier.h:48
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:336
array_poolt
Correspondance between arrays and pointers string representations.
Definition: array_pool.h:43
string_builtin_functiont::return_code
exprt return_code
Definition: string_builtin_function.h:112
deserialize_constant_int_arg
static std::vector< mp_integer > deserialize_constant_int_arg(const std::vector< mp_integer > serialized, const unsigned base)
Definition: string_format_builtin_function.cpp:395
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2086
floatbv_typet
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: bitvector_types.h:322
format_specifiert::conversion
char conversion
Definition: format_specifier.h:56
string_constraint_generatort::fresh_symbol
symbol_generatort fresh_symbol
Definition: string_constraint_generator.h:56
format_specifiert::DATE_TIME_UPPER
static const char DATE_TIME_UPPER
Definition: format_specifier.h:40
and_exprt
Boolean AND.
Definition: std_expr.h:1834
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:26
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:198
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:830
format_specifiert::STRING_UPPER
static const char STRING_UPPER
Definition: format_specifier.h:44
exprt
Base class for all expressions.
Definition: expr.h:54
string_format_builtin_functiont::string_format_builtin_functiont
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.
Definition: string_format_builtin_function.cpp:30
format_specifiert::HEXADECIMAL_FLOAT_UPPER
static const char HEXADECIMAL_FLOAT_UPPER
Definition: format_specifier.h:36
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
format_specifier.h
Format specifiers for String.format.
bool_typet
The Boolean type.
Definition: std_types.h:36
messaget::eom
static eomt eom
Definition: message.h:297
format_elementt
Definition: format_specifier.h:100
string_constraint_generatort::add_axioms_for_string_of_float
std::pair< exprt, string_constraintst > add_axioms_for_string_of_float(const function_application_exprt &f)
String representation of a float value.
Definition: string_constraint_generator_float.cpp:162
add_axioms_for_format
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.
Definition: string_format_builtin_function.cpp:293
format_specifiert::STRING
static const char STRING
Definition: format_specifier.h:43
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
equal_exprt
Equality.
Definition: std_expr.h:1139
format_specifiert::HASHCODE_UPPER
static const char HASHCODE_UPPER
Definition: format_specifier.h:46
string_format_builtin_functiont::result
array_string_exprt result
Definition: string_format_builtin_function.h:65
format_specifiert::HEXADECIMAL_INTEGER_UPPER
static const char HEXADECIMAL_INTEGER_UPPER
Definition: format_specifier.h:29
utf16_constant_array_to_java
std::string utf16_constant_array_to_java(const array_exprt &arr, std::size_t length)
Construct a string from a constant array.
Definition: string_refinement_util.cpp:56
add_axioms_for_format_specifier
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.
Definition: string_format_builtin_function.cpp:119
UNHANDLED_CASE
#define UNHANDLED_CASE
Definition: invariant.h:524
string_constraint_generatort::array_pool
array_poolt array_pool
Definition: string_constraint_generator.h:58
string_constraint_generatort
Definition: string_constraint_generator.h:45
format_specifiert::HASHCODE
static const char HASHCODE
Definition: format_specifier.h:45
unsignedbv_typet
Fixed-width bit-vector with unsigned binary interpretation.
Definition: bitvector_types.h:159
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_builtin_functiont::array_pool
array_poolt & array_pool
Definition: string_builtin_function.h:123
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:82
format_specifiert::index
int index
Definition: format_specifier.h:50
format_specifiert::DATE_TIME
static const char DATE_TIME
Definition: format_specifier.h:39
maximum
exprt maximum(const exprt &a, const exprt &b)
Definition: string_constraint_generator_main.cpp:400
string_to_upper_case_builtin_functiont
Converting each lowercase character of Basic Latin and Latin-1 supplement to the corresponding upperc...
Definition: string_builtin_function.h:286
bitor_exprt
Bit-wise OR.
Definition: bitvector_expr.h:125
string_constraint_generatort::ns
const namespacet ns
Definition: string_constraint_generator.h:60
string_format_builtin_functiont::inputs
std::vector< array_string_exprt > inputs
Definition: string_format_builtin_function.h:69
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
string_format_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_format_builtin_function.cpp:585
length_of_positive_decimal_int
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.
Definition: string_format_builtin_function.cpp:624
string_refinement_util.h
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: bitvector_types.h:208
length_of_decimal_int
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.
Definition: string_format_builtin_function.cpp:652
make_string
static array_string_exprt make_string(Iter begin, Iter end, const array_typet &array_type)
Definition: string_builtin_function.cpp:59
simplify_expr
exprt simplify_expr(exprt src, const namespacet &ns)
Definition: simplify_expr.cpp:2557
format_specifiert::GENERAL
static const char GENERAL
Definition: format_specifier.h:32
format_specifiert::DECIMAL_INTEGER
static const char DECIMAL_INTEGER
Definition: format_specifier.h:26
unary_minus_exprt
The unary minus expression.
Definition: std_expr.h:390
irept::id
const irep_idt & id() const
Definition: irep.h:407
range.h
Ranges: pair of begin and end iterators, which can be initialized from containers,...
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:56
format_specifiert::SCIENTIFIC_UPPER
static const char SCIENTIFIC_UPPER
Definition: format_specifier.h:31
false_exprt
The Boolean constant false.
Definition: std_expr.h:2725
eval_format_specifier
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.
Definition: string_format_builtin_function.cpp:427
to_array_string_expr
array_string_exprt & to_array_string_expr(exprt &expr)
Definition: string_expr.h:95
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
string_builtin_functiont
Base class for string functions that are built in the solver.
Definition: string_builtin_function.h:74
string_format_builtin_function.h
Built-in function for String.format.
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
simplify_expr.h
null_message_handlert
Definition: message.h:77
format_specifiert::GENERAL_UPPER
static const char GENERAL_UPPER
Definition: format_specifier.h:33
exprt::is_zero
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:91
string_constraint_generatort::add_axioms_for_constant
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.
Definition: string_constraint_generator_constants.cpp:24
format_arg_from_string
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.
Definition: string_format_builtin_function.cpp:240
eval_string
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 ...
Definition: string_builtin_function.cpp:24
format_specifiert::OCTAL_INTEGER
static const char OCTAL_INTEGER
Definition: format_specifier.h:27
is_null
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".
Definition: string_format_builtin_function.cpp:95
format_specifiert
Field names follow the OpenJDK implementation: http://hg.openjdk.java.net/jdk7/jdk7/jdk/file/9b8c96f9...
Definition: format_specifier.h:23
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:100
format_specifiert::SCIENTIFIC
static const char SCIENTIFIC
Definition: format_specifier.h:30
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:807
is_refined_string_type
bool is_refined_string_type(const typet &type)
Definition: refined_string_type.h:52
string_constraint_generatort::add_axioms_from_bool
std::pair< exprt, string_constraintst > add_axioms_from_bool(const function_application_exprt &f)
eval_is_null
static bool eval_is_null(const std::vector< mp_integer > &string)
Definition: string_format_builtin_function.cpp:419
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
string_constraint_generatort::add_axioms_from_float_scientific_notation
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.
Definition: string_constraint_generator_float.cpp:338
string_constraint_generatort::add_axioms_for_concat
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.
Definition: string_concatenation_builtin_function.cpp:158
implies_exprt
Boolean implication.
Definition: std_expr.h:1897
string_format_builtin_functiont::format_string
optionalt< std::string > format_string
Only set when the format string is a constant.
Definition: string_format_builtin_function.h:68
format_specifiert::CHARACTER_UPPER
static const char CHARACTER_UPPER
Definition: format_specifier.h:38
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:424
symbol_table.h
Author: Diffblue Ltd.
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1780
true_exprt
The Boolean constant true.
Definition: std_expr.h:2716
messaget::warning
mstreamt & warning() const
Definition: message.h:404
format_specifiert::BOOLEAN_UPPER
static const char BOOLEAN_UPPER
Definition: format_specifier.h:42
format_specifiert::HEXADECIMAL_INTEGER
static const char HEXADECIMAL_INTEGER
Definition: format_specifier.h:28
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
string_format_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_format_builtin_function.cpp:515
less_than
binary_relation_exprt less_than(exprt lhs, exprt rhs)
Definition: string_expr.h:48
make_range
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
array_string_exprt
Definition: string_expr.h:67
bitvector_expr.h
API to expression classes for bitvectors.
string_format_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_format_builtin_function.cpp:767
array_poolt::fresh_string
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
shl_exprt
Left shift.
Definition: bitvector_expr.h:295
string_constraintst::existential
std::vector< exprt > existential
Definition: string_constraint_generator.h:37
not_exprt
Boolean negation.
Definition: std_expr.h:2041
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2700
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106