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()).subtype() == unsignedbv_typet(16));
246 
247  if(id == "string_expr")
248  return string;
249  if(id == ID_int)
250  {
251  // Assume the string has length 4
252  // (int64)string.content[0] << 48 | (int64) string.content[1] << 32 |
253  // (int64)string.content[2] << 16 | (int64) string.content[3]
254  const signedbv_typet type{64};
255  return bitor_exprt{
256  bitor_exprt{shl_exprt{typecast_exprt{string[0], type}, 48},
257  shl_exprt{typecast_exprt{string[1], type}, 32}},
258  bitor_exprt{shl_exprt{typecast_exprt{string[2], type}, 16},
259  typecast_exprt{string[3], type}}};
260  }
261 
262  if(id == ID_char)
263  {
264  // Leave the string unchanged as the "null" string is used to represent null
265  return string;
266  }
267  if(id == ID_boolean)
268  {
269  // We assume the string has length exactly 4, if it is "null" return false
270  // and otherwise ignore the first 3 and return (bool)string.content[3]
271  return if_exprt{is_null(string, array_pool),
272  false_exprt{},
273  typecast_exprt{string[3], bool_typet()}};
274  }
275  if(id == ID_float)
276  {
277  // Deserialize an int and cast to float
278  const exprt as_int = format_arg_from_string(string, ID_int, array_pool);
279  return typecast_exprt{as_int, floatbv_typet{}};
280  }
282 }
283 
292 static std::pair<exprt, string_constraintst> add_axioms_for_format(
293  string_constraint_generatort &generator,
294  const array_string_exprt &res,
295  const std::string &s,
296  const std::vector<array_string_exprt> &args,
297  const messaget &message)
298 {
299  string_constraintst constraints;
300  array_poolt &array_pool = generator.array_pool;
301  const std::vector<format_elementt> format_strings = parse_format_string(s);
302  std::vector<array_string_exprt> intermediary_strings;
303  std::size_t arg_count = 0;
304  const typet &char_type = res.content().type().subtype();
305  const typet &index_type = res.length_type();
306 
307  array_string_exprt string_arg;
308 
309  for(const format_elementt &fe : format_strings)
310  {
311  if(fe.is_format_specifier())
312  {
313  const format_specifiert &fs = fe.get_format_specifier();
314 
315  if(
318  {
319  if(fs.index == -1)
320  {
321  INVARIANT(
322  arg_count < args.size(), "number of format must match specifiers");
323  string_arg = args[arg_count++];
324  }
325  else
326  {
327  INVARIANT(fs.index > 0, "index in format should be positive");
328  INVARIANT(
329  static_cast<std::size_t>(fs.index) <= args.size(),
330  "number of format must match specifiers");
331 
332  // first argument `args[0]` corresponds to index 1
333  string_arg = args[fs.index - 1];
334  }
335  }
336 
337  auto result = add_axioms_for_format_specifier(
338  generator, fs, string_arg, index_type, char_type, message);
339  merge(constraints, std::move(result.second));
340  intermediary_strings.push_back(result.first);
341  }
342  else
343  {
344  const array_string_exprt str =
345  array_pool.fresh_string(index_type, char_type);
346  auto result = generator.add_axioms_for_constant(
347  str, fe.get_format_text().get_content());
348  merge(constraints, result.second);
349  intermediary_strings.push_back(str);
350  }
351  }
352 
353  exprt return_code = from_integer(0, get_return_code_type());
354 
355  if(intermediary_strings.empty())
356  {
357  constraints.existential.push_back(equal_exprt(
358  array_pool.get_or_create_length(res), from_integer(0, index_type)));
359  return {return_code, constraints};
360  }
361 
362  array_string_exprt str = intermediary_strings[0];
363 
364  if(intermediary_strings.size() == 1)
365  {
366  // Copy the first string
367  auto result = generator.add_axioms_for_substring(
368  res,
369  str,
371  generator.array_pool.get_or_create_length(str));
372  merge(constraints, std::move(result.second));
373  return {result.first, std::move(constraints)};
374  }
375 
376  // start after the first string and stop before the last
377  for(std::size_t i = 1; i < intermediary_strings.size() - 1; ++i)
378  {
379  const array_string_exprt &intermediary = intermediary_strings[i];
380  const array_string_exprt fresh =
381  array_pool.fresh_string(index_type, char_type);
382  auto result = generator.add_axioms_for_concat(fresh, str, intermediary);
383  return_code = maximum(return_code, result.first);
384  merge(constraints, std::move(result.second));
385  str = fresh;
386  }
387 
388  auto result =
389  generator.add_axioms_for_concat(res, str, intermediary_strings.back());
390  merge(constraints, std::move(result.second));
391  return {maximum(result.first, return_code), std::move(constraints)};
392 }
393 
394 static std::vector<mp_integer> deserialize_constant_int_arg(
395  const std::vector<mp_integer> serialized,
396  const unsigned base)
397 {
398  PRECONDITION(serialized.size() == 4);
399 
400  // long value, to be used for other formats?
401  for(std::size_t i = 0; i < 4; i++)
402  {
404  serialized[i] <= 0xFFFF,
405  "Component of serialized value to"
406  "format must be bounded by 0xFFFF");
407  }
408 
409  const int64_t int64_value =
410  (serialized[0] << 48).to_long() | (serialized[1] << 32).to_long() |
411  (serialized[2] << 16).to_long() | serialized[3].to_long();
412  const mp_integer mp_integer_value{int64_value};
413  const std::string long_as_string = integer2string(mp_integer_value, base);
414 
415  return make_range(long_as_string).map([&](char c) { return mp_integer{c}; });
416 }
417 
418 static bool eval_is_null(const std::vector<mp_integer> &string)
419 {
420  return string.size() == 4 && string[0] == 'n' && string[1] == 'u' &&
421  string[2] == 'l' && string[3] == 'l';
422 }
423 
426 static std::vector<mp_integer> eval_format_specifier(
427  const format_specifiert &fs,
428  const std::vector<mp_integer> &arg)
429 {
430  switch(fs.conversion)
431  {
433  {
434  if(eval_is_null(arg))
435  return std::vector<mp_integer>{'n', 'u', 'l', 'l'};
436  return deserialize_constant_int_arg(arg, 10);
437  }
439  {
440  if(eval_is_null(arg))
441  return std::vector<mp_integer>{'n', 'u', 'l', 'l'};
442  auto upper_case_hex = deserialize_constant_int_arg(arg, 16);
443  // convert to lower case
444  return make_range(upper_case_hex).map([](const mp_integer &c) {
445  if('A' <= c && c <= 'Z')
446  return c + 0x20;
447  return c;
448  });
449  }
451  {
452  if(eval_is_null(arg))
453  return std::vector<mp_integer>{'n', 'u', 'l', 'l'};
454  return deserialize_constant_int_arg(arg, 16);
455  }
461  {
462  if(eval_is_null(arg))
463  return std::vector<mp_integer>{'n', 'u', 'l', 'l'};
464  return std::vector<mp_integer>{arg[3]};
465  }
467  {
468  if(arg[3] == 1)
469  return std::vector<mp_integer>{'t', 'r', 'u', 'e'};
470  return std::vector<mp_integer>{'f', 'a', 'l', 's', 'e'};
471  }
473  return arg;
477  // TODO: the constant should depend on the system: System.lineSeparator()
478  return std::vector<mp_integer>{'\n'};
480  return std::vector<mp_integer>{'%'};
489  {
490  format_specifiert fs_lower = fs;
491  fs_lower.conversion = tolower(fs.conversion);
492  auto lower_case = eval_format_specifier(fs_lower, arg);
493  return make_range(lower_case).map([](const mp_integer &c) {
494  // TODO: incomplete
495  if('a' <= c && c <= 'z')
496  return c - 0x20;
497  return c;
498  });
499  }
509  }
510 
511  INVARIANT(false, "format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
512 }
513 
515  const std::function<exprt(const exprt &)> &get_value) const
516 {
517  if(!format_string.has_value())
518  return {};
519 
520  const std::vector<format_elementt> format_strings =
522  std::vector<mp_integer> result_vector;
523  std::size_t arg_count = 0;
524 
525  for(const format_elementt &fe : format_strings)
526  {
527  if(fe.is_format_specifier())
528  {
529  const format_specifiert &fs = fe.get_format_specifier();
530  if(
533  {
534  std::vector<mp_integer> evaluated_char_vector;
535 
536  if(fs.index == -1)
537  {
538  INVARIANT(
539  arg_count < inputs.size(),
540  "number of format must match specifiers");
541  if(auto arg_value = eval_string(inputs[arg_count++], get_value))
542  evaluated_char_vector = eval_format_specifier(fs, *arg_value);
543  else
544  return {};
545  }
546  else
547  {
548  INVARIANT(fs.index > 0, "index in format should be positive");
549  INVARIANT(
550  static_cast<std::size_t>(fs.index) <= inputs.size(),
551  "number of format must match specifiers");
552 
553  // first argument `args[0]` corresponds to index 1
554  if(auto arg_value = eval_string(inputs[fs.index - 1], get_value))
555  evaluated_char_vector = eval_format_specifier(fs, *arg_value);
556  else
557  return {};
558  }
559  std::move(
560  evaluated_char_vector.begin(),
561  evaluated_char_vector.end(),
562  std::back_inserter(result_vector));
563  }
565  {
566  result_vector.push_back('%');
567  }
568  else
569  {
570  // TODO: the character should depend on the system:
571  // System.lineSeparator()
572  result_vector.push_back('\n');
573  }
574  }
575  else
576  {
577  for(char c : fe.get_format_text().get_content())
578  result_vector.emplace_back(c);
579  }
580  }
581  return make_string(result_vector, to_array_type(result.type()));
582 }
583 
585  string_constraint_generatort &generator) const
586 {
587  // When `format_string` was not set, leave the result non-deterministic
588  if(!format_string.has_value())
589  return {};
590 
591  null_message_handlert message_handler;
592  auto result_constraint_pair = add_axioms_for_format(
593  generator,
594  result,
595  format_string.value(),
596  inputs,
597  // TODO: get rid of this argument
598  messaget{message_handler});
599  INVARIANT(
600  simplify_expr(result_constraint_pair.first, generator.ns).is_zero(),
601  "add_axioms_for_format should return 0, meaning that formatting was"
602  "successful");
603  result_constraint_pair.second.existential.push_back(
605  return result_constraint_pair.second;
606 }
607 
624  const exprt &pos_integer,
625  int max_length,
626  const typet &length_type,
627  const unsigned long radix)
628 {
629  if(max_length <= 1)
630  return from_integer(1, length_type);
631 
632  // If the current value doesn't fit in a smaller size representation, we have
633  // found the number of digits needed to represent that value.
634  const mp_integer max_value_for_smaller_size =
635  pow((mp_integer)radix, max_length - 1);
636  return if_exprt{
637  less_than(
638  pos_integer,
639  from_integer(max_value_for_smaller_size, pos_integer.type())),
641  pos_integer, max_length - 1, length_type, radix),
642  from_integer(max_length, length_type)};
643 }
644 
652  const exprt &integer,
653  const typet &length_type,
654  const unsigned long radix)
655 {
656  int max_pos_int_length;
657  if(length_type == signedbv_typet(32))
658  {
659  if(radix == 10)
660  max_pos_int_length = 10;
661  else if(radix == 16)
662  max_pos_int_length = 8;
663  else
665  }
666  else
667  {
668  // We only handle 32-bit signed integer type for now.
670  }
671 
672  return if_exprt{
673  greater_or_equal_to(integer, from_integer(0, integer.type())),
675  integer, max_pos_int_length, length_type, radix),
676  plus_exprt{
678  unary_minus_exprt{integer}, max_pos_int_length, length_type, radix),
679  from_integer(1, length_type)}};
680 }
681 
685  const format_specifiert &fs,
686  const array_string_exprt &arg,
687  const typet &index_type,
688  array_poolt &array_pool)
689 {
690  switch(fs.conversion)
691  {
693  {
694  return if_exprt(
695  is_null(arg, array_pool),
698  format_arg_from_string(arg, ID_int, array_pool), index_type, 10));
699  }
702  {
703  return length_of_decimal_int(
704  format_arg_from_string(arg, ID_int, array_pool), index_type, 16);
705  }
712  {
713  const exprt arg_string = format_arg_from_string(arg, ID_char, array_pool);
714  const array_string_exprt &string_expr = to_array_string_expr(arg_string);
715  // In the case the arg is null, the result will be equal to "null" and
716  // and otherwise we just take the 4th character of the string.
717  return if_exprt{is_null(string_expr, array_pool),
720  }
723  {
724  return if_exprt{format_arg_from_string(arg, ID_boolean, array_pool),
727  }
730  {
731  const exprt arg_string =
732  format_arg_from_string(arg, "string_expr", array_pool);
733  const array_string_exprt string_expr = to_array_string_expr(arg_string);
734  return array_pool.get_or_create_length(string_expr);
735  }
739  // TODO: the constant should depend on the system: System.lineSeparator()
740  return from_integer(1, index_type);
742  return from_integer(1, index_type);
748  {
749  return length_for_format_specifier(fs, arg, index_type, array_pool);
750  }
759  // For all these unimplemented cases we return a non-deterministic string
761  }
762 
763  INVARIANT(false, "format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
764 }
765 
767 {
768  if(!format_string.has_value())
769  return true_exprt{};
770 
772  const std::vector<format_elementt> format_strings =
774  std::vector<exprt> intermediary_string_lengths;
775  std::size_t arg_count = 0;
776  const typet &index_type = result.length_type();
777 
778  for(const format_elementt &fe : format_strings)
779  {
780  if(fe.is_format_specifier())
781  {
782  const format_specifiert &fs = fe.get_format_specifier();
783  array_string_exprt arg;
784  if(
787  {
788  if(fs.index == -1)
789  {
790  INVARIANT(
791  arg_count < inputs.size(),
792  "number of format must match specifiers");
793  arg = inputs[arg_count++];
794  }
795  else
796  {
797  INVARIANT(fs.index > 0, "index in format should be positive");
798  INVARIANT(
799  static_cast<std::size_t>(fs.index) <= inputs.size(),
800  "number of format must match specifiers");
801 
802  // first argument `args[0]` corresponds to index 1
803  arg = inputs[fs.index - 1];
804  }
805  }
806  intermediary_string_lengths.push_back(
808  }
809  else
810  {
811  intermediary_string_lengths.push_back(from_integer(
812  fe.get_format_text().get_content().size(), result.length_type()));
813  }
814  }
815 
816  constraints.push_back(
818 
819  if(intermediary_string_lengths.empty())
820  {
821  constraints.push_back(equal_exprt(
823  return conjunction(constraints);
824  }
825 
826  exprt total_length = intermediary_string_lengths[0];
827  for(std::size_t i = 1; i < intermediary_string_lengths.size(); ++i)
828  {
829  total_length =
830  plus_exprt{std::move(total_length), intermediary_string_lengths[i]};
831  }
833  std::move(total_length)});
834 
835  return conjunction(constraints);
836 }
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:525
mp_integer
BigInt mp_integer
Definition: smt_terms.h:12
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:34
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:186
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:1497
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:684
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:42
string_builtin_functiont::return_code
exprt return_code
Definition: string_builtin_function.h:111
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:394
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:2172
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:59
format_specifiert::DATE_TIME_UPPER
static const char DATE_TIME_UPPER
Definition: format_specifier.h:40
and_exprt
Boolean AND.
Definition: std_expr.h:1920
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:914
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:29
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:39
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:292
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:1225
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:52
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:118
UNHANDLED_CASE
#define UNHANDLED_CASE
Definition: invariant.h:526
string_constraint_generatort::array_pool
array_poolt array_pool
Definition: string_constraint_generator.h:61
string_constraint_generatort
Definition: string_constraint_generator.h:48
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:99
string_builtin_functiont::array_pool
array_poolt & array_pool
Definition: string_builtin_function.h:122
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:399
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:285
bitor_exprt
Bit-wise OR.
Definition: bitvector_expr.h:125
string_constraint_generatort::ns
const namespacet ns
Definition: string_constraint_generator.h:63
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:510
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:584
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:623
string_refinement_util.h
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
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:651
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:2659
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:2811
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:426
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:179
string_builtin_functiont
Base class for string functions that are built in the solver.
Definition: string_builtin_function.h:73
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:64
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:239
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:94
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:813
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:418
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:117
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:1983
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:423
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:1866
message.h
true_exprt
The Boolean constant true.
Definition: std_expr.h:2802
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:137
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:514
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:766
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:40
not_exprt
Boolean negation.
Definition: std_expr.h:2127
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2786
integer2string
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:103