CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
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);
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(
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=='%')
82 s=match.suffix();
83 }
84
85 for(const auto &c : s)
86 if(c=='%')
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,
122 const typet &index_type,
123 const typet &char_type,
124 message_handlert &message_handler)
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,
140 from_integer(16, index_type),
141 16);
142 return {res, std::move(return_code.second)};
144 return_code = generator.add_axioms_from_float_scientific_notation(
146 return {res, std::move(return_code.second)};
148 return_code = generator.add_axioms_for_string_of_float(
150 return {res, std::move(return_code.second)};
152 {
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(
161 from_integer(4, index_type),
162 from_integer(1, index_type)}});
163 constraints.existential.push_back(implies_exprt{
169 constraints.existential.push_back(implies_exprt{
172 return {res, constraints};
173 }
175 return_code = generator.add_axioms_from_bool(
177 return {res, std::move(return_code.second)};
179 {
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 {
205 fs_lower.conversion = tolower(fs.conversion);
207 generator, fs_lower, string_arg, index_type, char_type, message_handler);
208
210 generator.fresh_symbol("return_code_upper_case", get_return_code_type());
214 upper_case_function.constraints(generator.fresh_symbol, message_handler);
216 return {res, std::move(upper_case_constraints)};
217 }
225 {
227 // For all these unimplemented cases we return a non-deterministic string
228 messaget message{message_handler};
229 message.warning() << "unimplemented format specifier: " << fs.conversion
230 << message.eom;
231 return {array_pool.fresh_string(index_type, char_type), {}};
232 }
233 }
234
236 "format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
237}
238
244 const array_string_exprt &string,
245 const irep_idt &id,
246 array_poolt &array_pool)
247{
249 to_array_type(string.content().type()).element_type() ==
250 unsignedbv_typet(16));
251
252 if(id == "string_expr")
253 return string;
254 if(id == ID_int)
255 {
256 // Assume the string has length 4
257 // (int64)string.content[0] << 48 | (int64) string.content[1] << 32 |
258 // (int64)string.content[2] << 16 | (int64) string.content[3]
259 const signedbv_typet type{64};
260 return bitor_exprt{
261 bitor_exprt{shl_exprt{typecast_exprt{string[0], type}, 48},
262 shl_exprt{typecast_exprt{string[1], type}, 32}},
263 bitor_exprt{shl_exprt{typecast_exprt{string[2], type}, 16},
264 typecast_exprt{string[3], type}}};
265 }
266
267 if(id == ID_char)
268 {
269 // Leave the string unchanged as the "null" string is used to represent null
270 return string;
271 }
272 if(id == ID_boolean)
273 {
274 // We assume the string has length exactly 4, if it is "null" return false
275 // and otherwise ignore the first 3 and return (bool)string.content[3]
276 return if_exprt{is_null(string, array_pool),
277 false_exprt{},
278 typecast_exprt{string[3], bool_typet()}};
279 }
280 if(id == ID_float)
281 {
282 // Deserialize an int and cast to float
283 const exprt as_int = format_arg_from_string(string, ID_int, array_pool);
285 }
287}
288
297static std::pair<exprt, string_constraintst> add_axioms_for_format(
299 const array_string_exprt &res,
300 const std::string &s,
301 const std::vector<array_string_exprt> &args,
302 message_handlert &message_handler)
303{
304 string_constraintst constraints;
305 array_poolt &array_pool = generator.array_pool;
306 const std::vector<format_elementt> format_strings = parse_format_string(s);
307 std::vector<array_string_exprt> intermediary_strings;
308 std::size_t arg_count = 0;
309 const typet &char_type = to_type_with_subtype(res.content().type()).subtype();
310 const typet &index_type = res.length_type();
311
313
314 for(const format_elementt &fe : format_strings)
315 {
316 if(fe.is_format_specifier())
317 {
318 const format_specifiert &fs = fe.get_format_specifier();
319
320 if(
321 fs.conversion != format_specifiert::PERCENT_SIGN &&
323 {
324 if(fs.index == -1)
325 {
326 INVARIANT(
327 arg_count < args.size(), "number of format must match specifiers");
328 string_arg = args[arg_count++];
329 }
330 else
331 {
332 INVARIANT(fs.index > 0, "index in format should be positive");
333 INVARIANT(
334 static_cast<std::size_t>(fs.index) <= args.size(),
335 "number of format must match specifiers");
336
337 // first argument `args[0]` corresponds to index 1
338 string_arg = args[fs.index - 1];
339 }
340 }
341
343 generator, fs, string_arg, index_type, char_type, message_handler);
344 merge(constraints, std::move(result.second));
345 intermediary_strings.push_back(result.first);
346 }
347 else
348 {
349 const array_string_exprt str =
350 array_pool.fresh_string(index_type, char_type);
351 auto result = generator.add_axioms_for_constant(
352 str, fe.get_format_text().get_content());
353 merge(constraints, result.second);
354 intermediary_strings.push_back(str);
355 }
356 }
357
358 exprt return_code = from_integer(0, get_return_code_type());
359
360 if(intermediary_strings.empty())
361 {
362 constraints.existential.push_back(equal_exprt(
363 array_pool.get_or_create_length(res), from_integer(0, index_type)));
364 return {return_code, constraints};
365 }
366
368
369 if(intermediary_strings.size() == 1)
370 {
371 // Copy the first string
372 auto result = generator.add_axioms_for_substring(
373 res,
374 str,
375 from_integer(0, index_type),
376 generator.array_pool.get_or_create_length(str));
377 merge(constraints, std::move(result.second));
378 return {result.first, std::move(constraints)};
379 }
380
381 // start after the first string and stop before the last
382 for(std::size_t i = 1; i < intermediary_strings.size() - 1; ++i)
383 {
386 array_pool.fresh_string(index_type, char_type);
387 auto result = generator.add_axioms_for_concat(fresh, str, intermediary);
388 return_code = maximum(return_code, result.first);
389 merge(constraints, std::move(result.second));
390 str = fresh;
391 }
392
393 auto result =
394 generator.add_axioms_for_concat(res, str, intermediary_strings.back());
395 merge(constraints, std::move(result.second));
396 return {maximum(result.first, return_code), std::move(constraints)};
397}
398
399static std::vector<mp_integer> deserialize_constant_int_arg(
400 const std::vector<mp_integer> serialized,
401 const unsigned base)
402{
403 PRECONDITION(serialized.size() == 4);
404
405 // long value, to be used for other formats?
406 for(std::size_t i = 0; i < 4; i++)
407 {
409 serialized[i] <= 0xFFFF,
410 "Component of serialized value to"
411 "format must be bounded by 0xFFFF");
412 }
413
414 const int64_t int64_value =
415 (serialized[0] << 48).to_long() | (serialized[1] << 32).to_long() |
416 (serialized[2] << 16).to_long() | serialized[3].to_long();
418 const std::string long_as_string = integer2string(mp_integer_value, base);
419
420 return make_range(long_as_string).map([&](char c) { return mp_integer{c}; });
421}
422
423static bool eval_is_null(const std::vector<mp_integer> &string)
424{
425 return string.size() == 4 && string[0] == 'n' && string[1] == 'u' &&
426 string[2] == 'l' && string[3] == 'l';
427}
428
431static std::vector<mp_integer> eval_format_specifier(
432 const format_specifiert &fs,
433 const std::vector<mp_integer> &arg)
434{
435 switch(fs.conversion)
436 {
438 {
439 if(eval_is_null(arg))
440 return std::vector<mp_integer>{'n', 'u', 'l', 'l'};
441 return deserialize_constant_int_arg(arg, 10);
442 }
444 {
445 if(eval_is_null(arg))
446 return std::vector<mp_integer>{'n', 'u', 'l', 'l'};
448 // convert to lower case
449 return make_range(upper_case_hex).map([](const mp_integer &c) {
450 if('A' <= c && c <= 'Z')
451 return c + 0x20;
452 return c;
453 });
454 }
456 {
457 if(eval_is_null(arg))
458 return std::vector<mp_integer>{'n', 'u', 'l', 'l'};
459 return deserialize_constant_int_arg(arg, 16);
460 }
466 {
467 if(eval_is_null(arg))
468 return std::vector<mp_integer>{'n', 'u', 'l', 'l'};
469 return std::vector<mp_integer>{arg[3]};
470 }
472 {
473 if(arg[3] == 1)
474 return std::vector<mp_integer>{'t', 'r', 'u', 'e'};
475 return std::vector<mp_integer>{'f', 'a', 'l', 's', 'e'};
476 }
478 return arg;
482 // TODO: the constant should depend on the system: System.lineSeparator()
483 return std::vector<mp_integer>{'\n'};
485 return std::vector<mp_integer>{'%'};
494 {
496 fs_lower.conversion = tolower(fs.conversion);
498 return make_range(lower_case).map([](const mp_integer &c) {
499 // TODO: incomplete
500 if('a' <= c && c <= 'z')
501 return c - 0x20;
502 return c;
503 });
504 }
514 }
515
516 INVARIANT(false, "format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
517}
518
520 const std::function<exprt(const exprt &)> &get_value) const
521{
522 if(!format_string.has_value())
523 return {};
524
525 const std::vector<format_elementt> format_strings =
527 std::vector<mp_integer> result_vector;
528 std::size_t arg_count = 0;
529
530 for(const format_elementt &fe : format_strings)
531 {
532 if(fe.is_format_specifier())
533 {
534 const format_specifiert &fs = fe.get_format_specifier();
535 if(
536 fs.conversion != format_specifiert::PERCENT_SIGN &&
538 {
539 std::vector<mp_integer> evaluated_char_vector;
540
541 if(fs.index == -1)
542 {
543 INVARIANT(
544 arg_count < inputs.size(),
545 "number of format must match specifiers");
546 if(auto arg_value = eval_string(inputs[arg_count++], get_value))
548 else
549 return {};
550 }
551 else
552 {
553 INVARIANT(fs.index > 0, "index in format should be positive");
554 INVARIANT(
555 static_cast<std::size_t>(fs.index) <= inputs.size(),
556 "number of format must match specifiers");
557
558 // first argument `args[0]` corresponds to index 1
559 if(auto arg_value = eval_string(inputs[fs.index - 1], get_value))
561 else
562 return {};
563 }
564 std::move(
565 evaluated_char_vector.begin(),
567 std::back_inserter(result_vector));
568 }
569 else if(fs.conversion == format_specifiert::PERCENT_SIGN)
570 {
571 result_vector.push_back('%');
572 }
573 else
574 {
575 // TODO: the character should depend on the system:
576 // System.lineSeparator()
577 result_vector.push_back('\n');
578 }
579 }
580 else
581 {
582 for(char c : fe.get_format_text().get_content())
583 result_vector.emplace_back(c);
584 }
585 }
587}
588
591 message_handlert &message_handler) const
592{
593 // When `format_string` was not set, leave the result non-deterministic
594 if(!format_string.has_value())
595 return {};
596
598 generator, result, format_string.value(), inputs, message_handler);
599 INVARIANT(
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.
635 pow((mp_integer)radix, max_length - 1);
636 return if_exprt{
637 less_than(
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{
657 if(length_type == signedbv_typet(32))
658 {
659 if(radix == 10)
661 else if(radix == 16)
663 else
665 }
666 else
667 {
668 // We only handle 32-bit signed integer type for now.
670 }
671
672 return if_exprt{
675 integer, max_pos_int_length, length_type, radix),
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),
696 from_integer(4, index_type),
698 format_arg_from_string(arg, ID_int, array_pool), index_type, 10));
699 }
702 {
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);
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),
718 from_integer(4, index_type),
719 from_integer(1, index_type)};
720 }
723 {
724 return if_exprt{format_arg_from_string(arg, ID_boolean, array_pool),
725 from_integer(4, index_type),
726 from_integer(5, index_type)};
727 }
730 {
731 const exprt arg_string =
732 format_arg_from_string(arg, "string_expr", array_pool);
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();
784 if(
785 fs.conversion != format_specifiert::PERCENT_SIGN &&
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 }
807 length_for_format_specifier(fs, arg, index_type, array_pool));
808 }
809 else
810 {
812 fe.get_format_text().get_content().size(), result.length_type()));
813 }
814 }
815
816 constraints.push_back(
818
820 {
821 constraints.push_back(equal_exprt(
823 return conjunction(constraints);
824 }
825
827 for(std::size_t i = 1; i < intermediary_string_lengths.size(); ++i)
828 {
831 }
833 std::move(total_length)});
834
835 return conjunction(constraints);
836}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
array_string_exprt get_string_expr(array_poolt &array_pool, const exprt &expr)
Fetch the string_exprt corresponding to the given refined_string_exprt.
API to expression classes for bitvectors.
bitvector_typet char_type()
Definition c_types.cpp:106
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Boolean AND.
Definition std_expr.h:2125
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.
array_string_exprt fresh_string(const typet &index_type, const typet &char_type)
Construct a string expression whose length and content are new variables.
array_string_exprt find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
const typet & length_type() const
Definition string_expr.h:70
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:38
Equality.
Definition std_expr.h:1366
Base class for all expressions.
Definition expr.h:56
std::vector< exprt > operandst
Definition expr.h:58
bool is_zero() const
Return whether the expression is a constant representing 0.
Definition expr.cpp:47
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:212
typet & type()
Return the type of the expression.
Definition expr.h:84
The Boolean constant false.
Definition std_expr.h:3199
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:2497
Boolean implication.
Definition std_expr.h:2225
Class that provides messages with a built-in verbosity 'level'.
Definition message.h:154
Boolean negation.
Definition std_expr.h:2454
The plus expression Associativity is not specified.
Definition std_expr.h:1002
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.
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
string_constraintst constraints(string_constraint_generatort &generator, message_handlert &message_handler) const override
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
std::optional< 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
std::optional< 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...
The Boolean constant true.
Definition std_expr.h:3190
Semantic type conversion.
Definition std_expr.h:2073
The type of an expression, extends irept.
Definition type.h:29
The unary minus expression.
Definition std_expr.h:484
Fixed-width bit-vector with unsigned binary interpretation.
int tolower(int c)
Definition ctype.c:109
Format specifiers for String.format.
format_token_listt parse_format_string(const std::string &arg_string)
double pow(double x, double y)
Definition math.c:3082
const std::string integer2string(const mp_integer &n, unsigned base)
Definition mp_arith.cpp:103
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition range.h:522
bool is_refined_string_type(const typet &type)
exprt simplify_expr(exprt src, const namespacet &ns)
BigInt mp_integer
Definition smt_terms.h:17
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define UNIMPLEMENTED
Definition invariant.h:558
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
#define UNHANDLED_CASE
Definition invariant.h:559
#define UNREACHABLE_BECAUSE(REASON)
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:83
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
Definition std_expr.h:1665
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:3172
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:888
static array_string_exprt make_string(Iter begin, Iter end, const array_typet &array_type)
std::optional< 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:49
array_string_exprt & to_array_string_expr(exprt &expr)
Definition string_expr.h:96
binary_relation_exprt greater_or_equal_to(exprt lhs, exprt rhs)
Definition string_expr.h:20
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 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::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, message_handlert &message_handler)
Parse s and add axioms ensuring the output corresponds to the output of String.format.
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, message_handlert &message_handler)
Parse s and add axioms ensuring the output corresponds to the output of String.format.
Built-in function for String.format.
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...
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:208