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 #include <util/range.h>
20 #include <util/simplify_expr.h>
21 #include <util/symbol_table.h>
22 
24  const array_string_exprt &string,
25  const irep_idt &id,
26  array_poolt &array_pool);
27 
29  const exprt &return_code,
30  const std::vector<exprt> &fun_args,
31  array_poolt &array_pool)
32  : string_builtin_functiont(return_code, array_pool)
33 {
34  PRECONDITION(fun_args.size() >= 3);
35  result = array_pool.find(fun_args[1], fun_args[0]);
36  const array_string_exprt format_string_expr =
37  get_string_expr(array_pool, fun_args[2]);
38 
39  // List of arguments after the format string
40  inputs = make_range(fun_args.begin() + 3, fun_args.end())
41  .map([&](const exprt &arg) {
42  INVARIANT(
44  "arguments of format should be strings");
45  return get_string_expr(array_pool, arg);
46  })
47  .collect<std::vector<array_string_exprt>>();
48 
49  // format_string is only initialized if the expression is constant
50  if(
51  array_pool.get_or_create_length(format_string_expr).id() == ID_constant &&
52  format_string_expr.content().id() == ID_array)
53  {
54  const auto length = numeric_cast_v<std::size_t>(
55  to_constant_expr(array_pool.get_or_create_length(format_string_expr)));
57  to_array_expr(format_string_expr.content()), length);
58  }
59 }
60 
61 #if 0
62 // This code is deactivated as it is not used for now, but ultimalety this
63 // should be used to throw an exception when the format string is not correct
68 static bool check_format_string(std::string s)
69 {
70  std::string format_specifier=
71  "%(\\d+\\$)?([-#+ 0,(\\<]*)?(\\d+)?(\\.\\d+)?([tT])?([a-zA-Z%])";
72  std::regex regex(format_specifier);
73  std::smatch match;
74 
75  while(std::regex_search(s, match, regex))
76  {
77  if(match.position()!= 0)
78  for(const auto &c : match.str())
79  if(c=='%')
80  return false;
81  s=match.suffix();
82  }
83 
84  for(const auto &c : s)
85  if(c=='%')
86  return false;
87 
88  return true;
89 }
90 #endif
91 
93 static exprt is_null(const array_string_exprt &string, array_poolt &array_pool)
94 {
95  return and_exprt{
96  equal_exprt{array_pool.get_or_create_length(string),
97  from_integer(4, string.length_type())},
98  and_exprt{equal_exprt{string[0], from_integer('n', string[0].type())},
99  equal_exprt{string[1], from_integer('u', string[0].type())},
100  equal_exprt{string[2], from_integer('l', string[0].type())},
101  equal_exprt{string[3], from_integer('l', string[0].type())}}};
102 }
103 
116 static std::pair<array_string_exprt, string_constraintst>
118  string_constraint_generatort &generator,
119  const format_specifiert &fs,
120  const array_string_exprt &string_arg,
121  const typet &index_type,
122  const typet &char_type,
123  const messaget &message)
124 {
125  string_constraintst constraints;
126  array_poolt &array_pool = generator.array_pool;
127  const array_string_exprt res = array_pool.fresh_string(index_type, char_type);
128  std::pair<exprt, string_constraintst> return_code;
129  switch(fs.conversion)
130  {
132  return_code = generator.add_axioms_for_string_of_int(
133  res, format_arg_from_string(string_arg, ID_int, array_pool), 0);
134  return {res, std::move(return_code.second)};
136  return_code = generator.add_axioms_for_string_of_int_with_radix(
137  res,
138  format_arg_from_string(string_arg, ID_int, array_pool),
140  16);
141  return {res, std::move(return_code.second)};
143  return_code = generator.add_axioms_from_float_scientific_notation(
144  res, format_arg_from_string(string_arg, ID_float, array_pool));
145  return {res, std::move(return_code.second)};
147  return_code = generator.add_axioms_for_string_of_float(
148  res, format_arg_from_string(string_arg, ID_float, array_pool));
149  return {res, std::move(return_code.second)};
151  {
152  exprt arg_string = format_arg_from_string(string_arg, ID_char, array_pool);
153  array_string_exprt &string_expr = to_array_string_expr(arg_string);
154  // In the case the arg is null, the result will be equal to "null" and
155  // and otherwise we just take the 4th character of the string.
156  const exprt is_null_literal = is_null(string_expr, array_pool);
157  constraints.existential.push_back(
158  equal_exprt{array_pool.get_or_create_length(res),
159  if_exprt{is_null_literal,
161  from_integer(1, index_type)}});
162  constraints.existential.push_back(implies_exprt{
163  is_null_literal,
165  equal_exprt{res[1], from_integer('u', char_type)},
166  equal_exprt{res[2], from_integer('l', char_type)},
167  equal_exprt{res[3], from_integer('l', char_type)}}});
168  constraints.existential.push_back(implies_exprt{
169  not_exprt{is_null_literal},
170  equal_exprt{res[0], typecast_exprt{string_expr[3], char_type}}});
171  return {res, constraints};
172  }
174  return_code = generator.add_axioms_from_bool(
175  res, format_arg_from_string(string_arg, ID_boolean, array_pool));
176  return {res, std::move(return_code.second)};
178  {
179  const exprt arg_string = string_arg;
180  const array_string_exprt string_expr = to_array_string_expr(arg_string);
181  return {std::move(string_expr), {}};
182  }
184  return_code = generator.add_axioms_for_string_of_int(
185  res, format_arg_from_string(string_arg, "hashcode", array_pool), 0);
186  return {res, std::move(return_code.second)};
188  // TODO: the constant should depend on the system: System.lineSeparator()
189  return_code = generator.add_axioms_for_constant(res, "\n");
190  return {res, std::move(return_code.second)};
192  return_code = generator.add_axioms_for_constant(res, "%");
193  return {res, std::move(return_code.second)};
202  {
203  format_specifiert fs_lower = fs;
204  fs_lower.conversion = tolower(fs.conversion);
205  auto format_specifier_result = add_axioms_for_format_specifier(
206  generator, fs_lower, string_arg, index_type, char_type, message);
207 
208  const exprt return_code_upper_case =
209  generator.fresh_symbol("return_code_upper_case", get_return_code_type());
210  const string_to_upper_case_builtin_functiont upper_case_function(
211  return_code_upper_case, res, format_specifier_result.first, array_pool);
212  auto upper_case_constraints =
213  upper_case_function.constraints(generator.fresh_symbol);
214  merge(upper_case_constraints, std::move(format_specifier_result.second));
215  return {res, std::move(upper_case_constraints)};
216  }
225  // For all these unimplemented cases we return a non-deterministic string
226  message.warning() << "unimplemented format specifier: " << fs.conversion
227  << message.eom;
228  return {array_pool.fresh_string(index_type, char_type), {}};
229  }
230 
231  INVARIANT(false, "format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
232 }
233 
239  const array_string_exprt &string,
240  const irep_idt &id,
241  array_poolt &array_pool)
242 {
243  PRECONDITION(
244  to_array_type(string.content().type()).subtype() == unsignedbv_typet(16));
245 
246  if(id == "string_expr")
247  return string;
248  if(id == ID_int)
249  {
250  // Assume the string has length 4
251  // (int64)string.content[0] << 48 | (int64) string.content[1] << 32 |
252  // (int64)string.content[2] << 16 | (int64) string.content[3]
253  const signedbv_typet type{64};
254  return bitor_exprt{
255  bitor_exprt{shl_exprt{typecast_exprt{string[0], type}, 48},
256  shl_exprt{typecast_exprt{string[1], type}, 32}},
257  bitor_exprt{shl_exprt{typecast_exprt{string[2], type}, 16},
258  typecast_exprt{string[3], type}}};
259  }
260 
261  if(id == ID_char)
262  {
263  // Leave the string unchanged as the "null" string is used to represent null
264  return string;
265  }
266  if(id == ID_boolean)
267  {
268  // We assume the string has length exactly 4, if it is "null" return false
269  // and otherwise ignore the first 3 and return (bool)string.content[3]
270  return if_exprt{is_null(string, array_pool),
271  false_exprt{},
272  typecast_exprt{string[3], bool_typet()}};
273  }
274  if(id == ID_float)
275  {
276  // Deserialize an int and cast to float
277  const exprt as_int = format_arg_from_string(string, ID_int, array_pool);
278  return typecast_exprt{as_int, floatbv_typet{}};
279  }
281 }
282 
291 static std::pair<exprt, string_constraintst> add_axioms_for_format(
292  string_constraint_generatort &generator,
293  const array_string_exprt &res,
294  const std::string &s,
295  const std::vector<array_string_exprt> &args,
296  const messaget &message)
297 {
298  string_constraintst constraints;
299  array_poolt &array_pool = generator.array_pool;
300  const std::vector<format_elementt> format_strings = parse_format_string(s);
301  std::vector<array_string_exprt> intermediary_strings;
302  std::size_t arg_count = 0;
303  const typet &char_type = res.content().type().subtype();
304  const typet &index_type = res.length_type();
305 
306  array_string_exprt string_arg;
307 
308  for(const format_elementt &fe : format_strings)
309  {
310  if(fe.is_format_specifier())
311  {
312  const format_specifiert &fs = fe.get_format_specifier();
313 
314  if(
317  {
318  if(fs.index == -1)
319  {
320  INVARIANT(
321  arg_count < args.size(), "number of format must match specifiers");
322  string_arg = args[arg_count++];
323  }
324  else
325  {
326  INVARIANT(fs.index > 0, "index in format should be positive");
327  INVARIANT(
328  static_cast<std::size_t>(fs.index) <= args.size(),
329  "number of format must match specifiers");
330 
331  // first argument `args[0]` corresponds to index 1
332  string_arg = args[fs.index - 1];
333  }
334  }
335 
336  auto result = add_axioms_for_format_specifier(
337  generator, fs, string_arg, index_type, char_type, message);
338  merge(constraints, std::move(result.second));
339  intermediary_strings.push_back(result.first);
340  }
341  else
342  {
343  const array_string_exprt str =
344  array_pool.fresh_string(index_type, char_type);
345  auto result = generator.add_axioms_for_constant(
346  str, fe.get_format_text().get_content());
347  merge(constraints, result.second);
348  intermediary_strings.push_back(str);
349  }
350  }
351 
352  exprt return_code = from_integer(0, get_return_code_type());
353 
354  if(intermediary_strings.empty())
355  {
356  constraints.existential.push_back(equal_exprt(
357  array_pool.get_or_create_length(res), from_integer(0, index_type)));
358  return {return_code, constraints};
359  }
360 
361  array_string_exprt str = intermediary_strings[0];
362 
363  if(intermediary_strings.size() == 1)
364  {
365  // Copy the first string
366  auto result = generator.add_axioms_for_substring(
367  res,
368  str,
370  generator.array_pool.get_or_create_length(str));
371  merge(constraints, std::move(result.second));
372  return {result.first, std::move(constraints)};
373  }
374 
375  // start after the first string and stop before the last
376  for(std::size_t i = 1; i < intermediary_strings.size() - 1; ++i)
377  {
378  const array_string_exprt &intermediary = intermediary_strings[i];
379  const array_string_exprt fresh =
380  array_pool.fresh_string(index_type, char_type);
381  auto result = generator.add_axioms_for_concat(fresh, str, intermediary);
382  return_code = maximum(return_code, result.first);
383  merge(constraints, std::move(result.second));
384  str = fresh;
385  }
386 
387  auto result =
388  generator.add_axioms_for_concat(res, str, intermediary_strings.back());
389  merge(constraints, std::move(result.second));
390  return {maximum(result.first, return_code), std::move(constraints)};
391 }
392 
393 static std::vector<mp_integer> deserialize_constant_int_arg(
394  const std::vector<mp_integer> serialized,
395  const unsigned base)
396 {
397  PRECONDITION(serialized.size() == 4);
398 
399  // long value, to be used for other formats?
400  for(std::size_t i = 0; i < 4; i++)
401  {
403  serialized[i] <= 0xFFFF,
404  "Component of serialized value to"
405  "format must be bounded by 0xFFFF");
406  }
407 
408  const int64_t int64_value =
409  (serialized[0] << 48).to_long() | (serialized[1] << 32).to_long() |
410  (serialized[2] << 16).to_long() | serialized[3].to_long();
411  const mp_integer mp_integer_value{int64_value};
412  const std::string long_as_string = integer2string(mp_integer_value, base);
413 
414  return make_range(long_as_string).map([&](char c) { return mp_integer{c}; });
415 }
416 
417 static bool eval_is_null(const std::vector<mp_integer> &string)
418 {
419  return string.size() == 4 && string[0] == 'n' && string[1] == 'u' &&
420  string[2] == 'l' && string[3] == 'l';
421 }
422 
425 static std::vector<mp_integer> eval_format_specifier(
426  const format_specifiert &fs,
427  const std::vector<mp_integer> &arg)
428 {
429  switch(fs.conversion)
430  {
432  {
433  if(eval_is_null(arg))
434  return std::vector<mp_integer>{'n', 'u', 'l', 'l'};
435  return deserialize_constant_int_arg(arg, 10);
436  }
438  {
439  if(eval_is_null(arg))
440  return std::vector<mp_integer>{'n', 'u', 'l', 'l'};
441  auto upper_case_hex = deserialize_constant_int_arg(arg, 16);
442  // convert to lower case
443  return make_range(upper_case_hex).map([](const mp_integer &c) {
444  if('A' <= c && c <= 'Z')
445  return c + 0x20;
446  return c;
447  });
448  }
450  {
451  if(eval_is_null(arg))
452  return std::vector<mp_integer>{'n', 'u', 'l', 'l'};
453  return deserialize_constant_int_arg(arg, 16);
454  }
460  {
461  if(eval_is_null(arg))
462  return std::vector<mp_integer>{'n', 'u', 'l', 'l'};
463  return std::vector<mp_integer>{arg[3]};
464  }
466  {
467  if(arg[3] == 1)
468  return std::vector<mp_integer>{'t', 'r', 'u', 'e'};
469  return std::vector<mp_integer>{'f', 'a', 'l', 's', 'e'};
470  }
472  return arg;
476  // TODO: the constant should depend on the system: System.lineSeparator()
477  return std::vector<mp_integer>{'\n'};
479  return std::vector<mp_integer>{'%'};
488  {
489  format_specifiert fs_lower = fs;
490  fs_lower.conversion = tolower(fs.conversion);
491  auto lower_case = eval_format_specifier(fs_lower, arg);
492  return make_range(lower_case).map([](const mp_integer &c) {
493  // TODO: incomplete
494  if('a' <= c && c <= 'z')
495  return c - 0x20;
496  return c;
497  });
498  }
508  }
509 
510  INVARIANT(false, "format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
511 }
512 
514  const std::function<exprt(const exprt &)> &get_value) const
515 {
516  if(!format_string.has_value())
517  return {};
518 
519  const std::vector<format_elementt> format_strings =
521  std::vector<mp_integer> result_vector;
522  std::size_t arg_count = 0;
523 
524  for(const format_elementt &fe : format_strings)
525  {
526  if(fe.is_format_specifier())
527  {
528  const format_specifiert &fs = fe.get_format_specifier();
529  if(
532  {
533  std::vector<mp_integer> evaluated_char_vector;
534 
535  if(fs.index == -1)
536  {
537  INVARIANT(
538  arg_count < inputs.size(),
539  "number of format must match specifiers");
540  if(auto arg_value = eval_string(inputs[arg_count++], get_value))
541  evaluated_char_vector = eval_format_specifier(fs, *arg_value);
542  else
543  return {};
544  }
545  else
546  {
547  INVARIANT(fs.index > 0, "index in format should be positive");
548  INVARIANT(
549  static_cast<std::size_t>(fs.index) <= inputs.size(),
550  "number of format must match specifiers");
551 
552  // first argument `args[0]` corresponds to index 1
553  if(auto arg_value = eval_string(inputs[fs.index - 1], get_value))
554  evaluated_char_vector = eval_format_specifier(fs, *arg_value);
555  else
556  return {};
557  }
558  std::move(
559  evaluated_char_vector.begin(),
560  evaluated_char_vector.end(),
561  std::back_inserter(result_vector));
562  }
564  {
565  result_vector.push_back('%');
566  }
567  else
568  {
569  // TODO: the character should depend on the system:
570  // System.lineSeparator()
571  result_vector.push_back('\n');
572  }
573  }
574  else
575  {
576  for(char c : fe.get_format_text().get_content())
577  result_vector.emplace_back(c);
578  }
579  }
580  return make_string(result_vector, to_array_type(result.type()));
581 }
582 
584  string_constraint_generatort &generator) const
585 {
586  // When `format_string` was not set, leave the result non-deterministic
587  if(!format_string.has_value())
588  return {};
589 
590  null_message_handlert message_handler;
591  auto result_constraint_pair = add_axioms_for_format(
592  generator,
593  result,
594  format_string.value(),
595  inputs,
596  // TODO: get rid of this argument
597  messaget{message_handler});
598  INVARIANT(
599  simplify_expr(result_constraint_pair.first, generator.ns).is_zero(),
600  "add_axioms_for_format should return 0, meaning that formatting was"
601  "successful");
602  result_constraint_pair.second.existential.push_back(
604  return result_constraint_pair.second;
605 }
606 
623  const exprt &pos_integer,
624  int max_length,
625  const typet &length_type,
626  const unsigned long radix)
627 {
628  if(max_length <= 1)
629  return from_integer(1, length_type);
630 
631  // If the current value doesn't fit in a smaller size representation, we have
632  // found the number of digits needed to represent that value.
633  const mp_integer max_value_for_smaller_size =
634  pow((mp_integer)radix, max_length - 1);
635  return if_exprt{
636  less_than(
637  pos_integer,
638  from_integer(max_value_for_smaller_size, pos_integer.type())),
640  pos_integer, max_length - 1, length_type, radix),
641  from_integer(max_length, length_type)};
642 }
643 
651  const exprt &integer,
652  const typet &length_type,
653  const unsigned long radix)
654 {
655  int max_pos_int_length;
656  if(length_type == signedbv_typet(32))
657  {
658  if(radix == 10)
659  max_pos_int_length = 10;
660  else if(radix == 16)
661  max_pos_int_length = 8;
662  else
664  }
665  else
666  {
667  // We only handle 32-bit signed integer type for now.
669  }
670 
671  return if_exprt{
672  greater_or_equal_to(integer, from_integer(0, integer.type())),
674  integer, max_pos_int_length, length_type, radix),
675  plus_exprt{
677  unary_minus_exprt{integer}, max_pos_int_length, length_type, radix),
678  from_integer(1, length_type)}};
679 }
680 
684  const format_specifiert &fs,
685  const array_string_exprt &arg,
686  const typet &index_type,
687  array_poolt &array_pool)
688 {
689  switch(fs.conversion)
690  {
692  {
693  return if_exprt(
694  is_null(arg, array_pool),
697  format_arg_from_string(arg, ID_int, array_pool), index_type, 10));
698  }
701  {
702  return length_of_decimal_int(
703  format_arg_from_string(arg, ID_int, array_pool), index_type, 16);
704  }
711  {
712  const exprt arg_string = format_arg_from_string(arg, ID_char, array_pool);
713  const array_string_exprt &string_expr = to_array_string_expr(arg_string);
714  // In the case the arg is null, the result will be equal to "null" and
715  // and otherwise we just take the 4th character of the string.
716  return if_exprt{is_null(string_expr, array_pool),
719  }
722  {
723  return if_exprt{format_arg_from_string(arg, ID_boolean, array_pool),
726  }
729  {
730  const exprt arg_string =
731  format_arg_from_string(arg, "string_expr", array_pool);
732  const array_string_exprt string_expr = to_array_string_expr(arg_string);
733  return array_pool.get_or_create_length(string_expr);
734  }
738  // TODO: the constant should depend on the system: System.lineSeparator()
739  return from_integer(1, index_type);
741  return from_integer(1, index_type);
747  {
748  return length_for_format_specifier(fs, arg, index_type, array_pool);
749  }
758  // For all these unimplemented cases we return a non-deterministic string
760  }
761 
762  INVARIANT(false, "format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
763 }
764 
766 {
767  if(!format_string.has_value())
768  return true_exprt{};
769 
771  const std::vector<format_elementt> format_strings =
773  std::vector<exprt> intermediary_string_lengths;
774  std::size_t arg_count = 0;
775  const typet &index_type = result.length_type();
776 
777  for(const format_elementt &fe : format_strings)
778  {
779  if(fe.is_format_specifier())
780  {
781  const format_specifiert &fs = fe.get_format_specifier();
782  array_string_exprt arg;
783  if(
786  {
787  if(fs.index == -1)
788  {
789  INVARIANT(
790  arg_count < inputs.size(),
791  "number of format must match specifiers");
792  arg = inputs[arg_count++];
793  }
794  else
795  {
796  INVARIANT(fs.index > 0, "index in format should be positive");
797  INVARIANT(
798  static_cast<std::size_t>(fs.index) <= inputs.size(),
799  "number of format must match specifiers");
800 
801  // first argument `args[0]` corresponds to index 1
802  arg = inputs[fs.index - 1];
803  }
804  }
805  intermediary_string_lengths.push_back(
807  }
808  else
809  {
810  intermediary_string_lengths.push_back(from_integer(
811  fe.get_format_text().get_content().size(), result.length_type()));
812  }
813  }
814 
815  constraints.push_back(
817 
818  if(intermediary_string_lengths.empty())
819  {
820  constraints.push_back(equal_exprt(
822  return conjunction(constraints);
823  }
824 
825  exprt total_length = intermediary_string_lengths[0];
826  for(std::size_t i = 1; i < intermediary_string_lengths.size(); ++i)
827  {
828  total_length =
829  plus_exprt{std::move(total_length), intermediary_string_lengths[i]};
830  }
832  std::move(total_length)});
833 
834  return conjunction(constraints);
835 }
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:51
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:1462
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:182
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:683
typet
The type of an expression, extends irept.
Definition: type.h:29
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:393
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2964
floatbv_typet
Fixed-width bit-vector with IEEE floating-point interpretation.
Definition: std_types.h:1379
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:2137
array_poolt::get_or_create_length
exprt get_or_create_length(const array_string_exprt &s)
Get the length of an array_string_exprt from the array_pool.
Definition: array_pool.cpp:24
get_string_expr
array_string_exprt get_string_expr(array_poolt &array_pool, const exprt &expr)
Fetch the string_exprt corresponding to the given refined_string_exprt.
Definition: array_pool.cpp:196
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:881
format_specifiert::STRING_UPPER
static const char STRING_UPPER
Definition: format_specifier.h:44
exprt
Base class for all expressions.
Definition: expr.h:53
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:28
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:37
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:159
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:291
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:1190
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:117
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: std_types.h:1216
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
message
static const char * message(const static_verifier_resultt::statust &status)
Makes a status message string from a status.
Definition: static_verifier.cpp:74
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
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: std_expr.h:2388
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:583
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:622
string_refinement_util.h
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: std_types.h:1265
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:650
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:2698
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:378
irept::id
const irep_idt & id() const
Definition: irep.h:418
range.h
Ranges: pair of begin and end iterators, which can be initialized from containers,...
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
format_specifiert::SCIENTIFIC_UPPER
static const char SCIENTIFIC_UPPER
Definition: format_specifier.h:31
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
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:425
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:132
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:238
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:93
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:99
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:1011
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:417
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:335
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:2200
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:2013
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
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:513
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
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:765
validation_modet::INVARIANT
@ INVARIANT
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:55
shl_exprt
Left shift.
Definition: std_expr.h:2561
string_constraintst::existential
std::vector< exprt > existential
Definition: string_constraint_generator.h:37
not_exprt
Boolean negation.
Definition: std_expr.h:2843
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3939
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:106