cprover
string_format_builtin_function.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Built-in function for String.format
4
5Author: Romain Brenguier, Joel Allred
6
7\*******************************************************************/
8
11
12#include <iterator>
13#include <string>
14
15#include "format_specifier.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) {
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>(
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
69static 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
94static 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
117static std::pair<array_string_exprt, string_constraintst>
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,
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{
245 to_array_type(string.content().type()).element_type() ==
246 unsignedbv_typet(16));
247
248 if(id == "string_expr")
249 return string;
250 if(id == ID_int)
251 {
252 // Assume the string has length 4
253 // (int64)string.content[0] << 48 | (int64) string.content[1] << 32 |
254 // (int64)string.content[2] << 16 | (int64) string.content[3]
255 const signedbv_typet type{64};
256 return bitor_exprt{
257 bitor_exprt{shl_exprt{typecast_exprt{string[0], type}, 48},
258 shl_exprt{typecast_exprt{string[1], type}, 32}},
259 bitor_exprt{shl_exprt{typecast_exprt{string[2], type}, 16},
260 typecast_exprt{string[3], type}}};
261 }
262
263 if(id == ID_char)
264 {
265 // Leave the string unchanged as the "null" string is used to represent null
266 return string;
267 }
268 if(id == ID_boolean)
269 {
270 // We assume the string has length exactly 4, if it is "null" return false
271 // and otherwise ignore the first 3 and return (bool)string.content[3]
272 return if_exprt{is_null(string, array_pool),
273 false_exprt{},
274 typecast_exprt{string[3], bool_typet()}};
275 }
276 if(id == ID_float)
277 {
278 // Deserialize an int and cast to float
279 const exprt as_int = format_arg_from_string(string, ID_int, array_pool);
280 return typecast_exprt{as_int, floatbv_typet{}};
281 }
283}
284
293static std::pair<exprt, string_constraintst> add_axioms_for_format(
295 const array_string_exprt &res,
296 const std::string &s,
297 const std::vector<array_string_exprt> &args,
298 const messaget &message)
299{
300 string_constraintst constraints;
301 array_poolt &array_pool = generator.array_pool;
302 const std::vector<format_elementt> format_strings = parse_format_string(s);
303 std::vector<array_string_exprt> intermediary_strings;
304 std::size_t arg_count = 0;
306 const typet &index_type = res.length_type();
307
308 array_string_exprt string_arg;
309
310 for(const format_elementt &fe : format_strings)
311 {
312 if(fe.is_format_specifier())
313 {
314 const format_specifiert &fs = fe.get_format_specifier();
315
316 if(
319 {
320 if(fs.index == -1)
321 {
322 INVARIANT(
323 arg_count < args.size(), "number of format must match specifiers");
324 string_arg = args[arg_count++];
325 }
326 else
327 {
328 INVARIANT(fs.index > 0, "index in format should be positive");
329 INVARIANT(
330 static_cast<std::size_t>(fs.index) <= args.size(),
331 "number of format must match specifiers");
332
333 // first argument `args[0]` corresponds to index 1
334 string_arg = args[fs.index - 1];
335 }
336 }
337
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
395static 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
419static 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
427static 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),
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 {
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;
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();
785 if(
788 {
789 if(fs.index == -1)
790 {
791 INVARIANT(
792 arg_count < inputs.size(),
793 "number of format must match specifiers");
794 arg = inputs[arg_count++];
795 }
796 else
797 {
798 INVARIANT(fs.index > 0, "index in format should be positive");
799 INVARIANT(
800 static_cast<std::size_t>(fs.index) <= inputs.size(),
801 "number of format must match specifiers");
802
803 // first argument `args[0]` corresponds to index 1
804 arg = inputs[fs.index - 1];
805 }
806 }
807 intermediary_string_lengths.push_back(
809 }
810 else
811 {
812 intermediary_string_lengths.push_back(from_integer(
813 fe.get_format_text().get_content().size(), result.length_type()));
814 }
815 }
816
817 constraints.push_back(
819
820 if(intermediary_string_lengths.empty())
821 {
822 constraints.push_back(equal_exprt(
824 return conjunction(constraints);
825 }
826
827 exprt total_length = intermediary_string_lengths[0];
828 for(std::size_t i = 1; i < intermediary_string_lengths.size(); ++i)
829 {
830 total_length =
831 plus_exprt{std::move(total_length), intermediary_string_lengths[i]};
832 }
834 std::move(total_length)});
835
836 return conjunction(constraints);
837}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
array_string_exprt get_string_expr(array_poolt &array_pool, const exprt &expr)
Fetch the string_exprt corresponding to the given refined_string_exprt.
Definition: array_pool.cpp:199
API to expression classes for bitvectors.
bitvector_typet index_type()
Definition: c_types.cpp:22
bitvector_typet char_type()
Definition: c_types.cpp:124
Boolean AND.
Definition: std_expr.h:1974
Correspondance between arrays and pointers string representations.
Definition: array_pool.h:42
exprt get_or_create_length(const array_string_exprt &s)
Get the length of an array_string_exprt from the array_pool.
Definition: array_pool.cpp:26
array_string_exprt fresh_string(const typet &index_type, const typet &char_type)
Construct a string expression whose length and content are new variables.
Definition: array_pool.cpp:57
array_string_exprt find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
Definition: array_pool.cpp:184
const typet & length_type() const
Definition: string_expr.h:69
exprt & content()
Definition: string_expr.h:74
Bit-wise OR.
The Boolean type.
Definition: std_types.h:36
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
Equality.
Definition: std_expr.h:1225
Base class for all expressions.
Definition: expr.h:54
std::vector< exprt > operandst
Definition: expr.h:56
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition: expr.cpp:64
typet & type()
Return the type of the expression.
Definition: expr.h:82
The Boolean constant false.
Definition: std_expr.h:2865
Fixed-width bit-vector with IEEE floating-point interpretation.
Field names follow the OpenJDK implementation: http://hg.openjdk.java.net/jdk7/jdk7/jdk/file/9b8c96f9...
static const char STRING_UPPER
static const char OCTAL_INTEGER
static const char SCIENTIFIC
static const char PERCENT_SIGN
static const char DATE_TIME_UPPER
static const char SCIENTIFIC_UPPER
static const char HEXADECIMAL_INTEGER
static const char DATE_TIME
static const char BOOLEAN_UPPER
static const char STRING
static const char CHARACTER
static const char HASHCODE
static const char GENERAL
static const char HEXADECIMAL_INTEGER_UPPER
static const char HASHCODE_UPPER
static const char HEXADECIMAL_FLOAT_UPPER
static const char BOOLEAN
static const char DECIMAL_FLOAT
static const char CHARACTER_UPPER
static const char GENERAL_UPPER
static const char DECIMAL_INTEGER
static const char HEXADECIMAL_FLOAT
static const char LINE_SEPARATOR
The trinary if-then-else operator.
Definition: std_expr.h:2226
Boolean implication.
Definition: std_expr.h:2037
const irep_idt & id() const
Definition: irep.h:396
Class that provides messages with a built-in verbosity 'level'.
Definition: message.h:155
mstreamt & warning() const
Definition: message.h:404
static eomt eom
Definition: message.h:297
Boolean negation.
Definition: std_expr.h:2181
The plus expression Associativity is not specified.
Definition: std_expr.h:914
Left shift.
Fixed-width bit-vector with two's complement interpretation.
Base class for string functions that are built in the solver.
std::pair< exprt, string_constraintst > add_axioms_from_bool(const function_application_exprt &f)
std::pair< exprt, string_constraintst > add_axioms_for_substring(const array_string_exprt &res, const array_string_exprt &str, const exprt &start, const exprt &end)
Add axioms ensuring that res corresponds to the substring of str between indexes ‘start’ = max(start,...
std::pair< exprt, string_constraintst > add_axioms_for_concat(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
Add axioms enforcing that res is equal to the concatenation of s1 and s2.
std::pair< exprt, string_constraintst > add_axioms_for_string_of_int_with_radix(const array_string_exprt &res, const exprt &input_int, const exprt &radix, size_t max_size)
Add axioms enforcing that the string corresponds to the result of String.valueOf(II) or String....
std::pair< exprt, string_constraintst > add_axioms_for_string_of_int(const array_string_exprt &res, const exprt &input_int, size_t max_size)
Add axioms enforcing that the string corresponds to the result of String.valueOf(I) or String....
std::pair< exprt, string_constraintst > add_axioms_from_float_scientific_notation(const array_string_exprt &res, const exprt &f)
Add axioms to write the float in scientific notation.
std::pair< exprt, string_constraintst > add_axioms_for_string_of_float(const function_application_exprt &f)
String representation of a float value.
std::pair< exprt, string_constraintst > add_axioms_for_constant(const array_string_exprt &res, irep_idt sval, const exprt &guard=true_exprt())
Add axioms ensuring that the provided string expression and constant are equal.
string_constraintst constraints(string_constraint_generatort &generator) const override
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
optionalt< std::string > format_string
Only set when the format string is a constant.
string_format_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Constructor from arguments of a function application.
std::vector< array_string_exprt > inputs
optionalt< exprt > eval(const std::function< exprt(const exprt &)> &get_value) const override
Given a function get_value which gives a valuation to expressions, attempt to find the result of the ...
Converting each lowercase character of Basic Latin and Latin-1 supplement to the corresponding upperc...
string_constraintst constraints(class symbol_generatort &fresh_symbol) const
Set of constraints ensuring result corresponds to input in which lowercase characters of Basic Latin ...
The Boolean constant true.
Definition: std_expr.h:2856
const typet & subtype() const
Definition: type.h:156
Semantic type conversion.
Definition: std_expr.h:1920
The type of an expression, extends irept.
Definition: type.h:29
The unary minus expression.
Definition: std_expr.h:390
Fixed-width bit-vector with unsigned binary interpretation.
Format specifiers for String.format.
format_token_listt parse_format_string(const std::string &arg_string)
const std::string integer2string(const mp_integer &n, unsigned base)
Definition: mp_arith.cpp:103
nonstd::optional< T > optionalt
Definition: optional.h:35
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition: range.h:524
bool is_refined_string_type(const typet &type)
exprt simplify_expr(exprt src, const namespacet &ns)
BigInt mp_integer
Definition: smt_terms.h:12
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:510
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
#define UNIMPLEMENTED
Definition: invariant.h:525
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:423
#define UNHANDLED_CASE
Definition: invariant.h:526
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition: std_expr.cpp:34
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition: std_expr.h:1506
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:2840
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:832
static array_string_exprt make_string(Iter begin, Iter end, const array_typet &array_type)
optionalt< std::vector< mp_integer > > eval_string(const array_string_exprt &a, const std::function< exprt(const exprt &)> &get_value)
Given a function get_value which gives a valuation to expressions, attempt to find the current value ...
exprt maximum(const exprt &a, const exprt &b)
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.
signedbv_typet get_return_code_type()
binary_relation_exprt less_than(exprt lhs, exprt rhs)
Definition: string_expr.h:48
array_string_exprt & to_array_string_expr(exprt &expr)
Definition: string_expr.h:95
binary_relation_exprt greater_or_equal_to(exprt lhs, exprt rhs)
Definition: string_expr.h:19
static exprt format_arg_from_string(const array_string_exprt &string, const irep_idt &id, array_poolt &array_pool)
Deserialize an argument for format from string.
static std::pair< array_string_exprt, string_constraintst > add_axioms_for_format_specifier(string_constraint_generatort &generator, const format_specifiert &fs, const array_string_exprt &string_arg, const typet &index_type, const typet &char_type, const messaget &message)
Parse s and add axioms ensuring the output corresponds to the output of String.format.
static exprt length_of_positive_decimal_int(const exprt &pos_integer, int max_length, const typet &length_type, const unsigned long radix)
Return an new expression representing the length of the representation of integer.
static bool eval_is_null(const std::vector< mp_integer > &string)
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.
exprt length_of_decimal_int(const exprt &integer, const typet &length_type, const unsigned long radix)
Compute the length of the decimal representation of an integer.
static 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".
static std::vector< mp_integer > deserialize_constant_int_arg(const std::vector< mp_integer > serialized, const unsigned base)
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...
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.
Built-in function for String.format.
std::string utf16_constant_array_to_java(const array_exprt &arr, std::size_t length)
Construct a string from a constant array.
Collection of constraints of different types: existential formulas, universal formulas,...
std::vector< exprt > existential
const type_with_subtypet & to_type_with_subtype(const typet &type)
Definition: type.h:177