30 const exprt &return_code,
31 const std::vector<exprt> &fun_args,
42 .map([&](
const exprt &arg) {
45 "arguments of format should be strings");
48 .collect<std::vector<array_string_exprt>>();
53 format_string_expr.
content().
id() == ID_array)
55 const auto length = numeric_cast_v<std::size_t>(
69 static bool check_format_string(std::string s)
71 std::string format_specifier=
72 "%(\\d+\\$)?([-#+ 0,(\\<]*)?(\\d+)?(\\.\\d+)?([tT])?([a-zA-Z%])";
73 std::regex regex(format_specifier);
76 while(std::regex_search(s, match, regex))
78 if(match.position()!= 0)
79 for(
const auto &c : match.str())
85 for(
const auto &c : s)
117 static std::pair<array_string_exprt, string_constraintst>
129 std::pair<exprt, string_constraintst> return_code;
135 return {res, std::move(return_code.second)};
142 return {res, std::move(return_code.second)};
146 return {res, std::move(return_code.second)};
150 return {res, std::move(return_code.second)};
157 const exprt is_null_literal =
is_null(string_expr, array_pool);
172 return {res, constraints};
177 return {res, std::move(return_code.second)};
180 const exprt arg_string = string_arg;
182 return {std::move(string_expr), {}};
187 return {res, std::move(return_code.second)};
191 return {res, std::move(return_code.second)};
194 return {res, std::move(return_code.second)};
209 const exprt return_code_upper_case =
212 return_code_upper_case, res, format_specifier_result.first, array_pool);
213 auto upper_case_constraints =
215 merge(upper_case_constraints, std::move(format_specifier_result.second));
216 return {res, std::move(upper_case_constraints)};
232 INVARIANT(
false,
"format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
247 if(
id ==
"string_expr")
295 const std::string &s,
296 const std::vector<array_string_exprt> &args,
302 std::vector<array_string_exprt> intermediary_strings;
303 std::size_t arg_count = 0;
311 if(fe.is_format_specifier())
322 arg_count < args.size(),
"number of format must match specifiers");
323 string_arg = args[arg_count++];
329 static_cast<std::size_t
>(fs.
index) <= args.size(),
330 "number of format must match specifiers");
333 string_arg = args[fs.
index - 1];
339 merge(constraints, std::move(result.second));
340 intermediary_strings.push_back(result.first);
347 str, fe.get_format_text().get_content());
348 merge(constraints, result.second);
349 intermediary_strings.push_back(str);
355 if(intermediary_strings.empty())
359 return {return_code, constraints};
364 if(intermediary_strings.size() == 1)
372 merge(constraints, std::move(result.second));
373 return {result.first, std::move(constraints)};
377 for(std::size_t i = 1; i < intermediary_strings.size() - 1; ++i)
383 return_code =
maximum(return_code, result.first);
384 merge(constraints, std::move(result.second));
390 merge(constraints, std::move(result.second));
391 return {
maximum(result.first, return_code), std::move(constraints)};
395 const std::vector<mp_integer> serialized,
401 for(std::size_t i = 0; i < 4; i++)
404 serialized[i] <= 0xFFFF,
405 "Component of serialized value to"
406 "format must be bounded by 0xFFFF");
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);
420 return string.size() == 4 &&
string[0] ==
'n' &&
string[1] ==
'u' &&
421 string[2] ==
'l' &&
string[3] ==
'l';
428 const std::vector<mp_integer> &arg)
435 return std::vector<mp_integer>{
'n',
'u',
'l',
'l'};
441 return std::vector<mp_integer>{
'n',
'u',
'l',
'l'};
445 if(
'A' <= c && c <=
'Z')
453 return std::vector<mp_integer>{
'n',
'u',
'l',
'l'};
463 return std::vector<mp_integer>{
'n',
'u',
'l',
'l'};
464 return std::vector<mp_integer>{arg[3]};
469 return std::vector<mp_integer>{
't',
'r',
'u',
'e'};
470 return std::vector<mp_integer>{
'f',
'a',
'l',
's',
'e'};
478 return std::vector<mp_integer>{
'\n'};
480 return std::vector<mp_integer>{
'%'};
495 if(
'a' <= c && c <=
'z')
511 INVARIANT(
false,
"format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
515 const std::function<
exprt(
const exprt &)> &get_value)
const
520 const std::vector<format_elementt> format_strings =
522 std::vector<mp_integer> result_vector;
523 std::size_t arg_count = 0;
527 if(fe.is_format_specifier())
534 std::vector<mp_integer> evaluated_char_vector;
539 arg_count <
inputs.size(),
540 "number of format must match specifiers");
550 static_cast<std::size_t
>(fs.
index) <=
inputs.size(),
551 "number of format must match specifiers");
560 evaluated_char_vector.begin(),
561 evaluated_char_vector.end(),
562 std::back_inserter(result_vector));
566 result_vector.push_back(
'%');
572 result_vector.push_back(
'\n');
577 for(
char c : fe.get_format_text().get_content())
578 result_vector.emplace_back(c);
601 "add_axioms_for_format should return 0, meaning that formatting was"
603 result_constraint_pair.second.existential.push_back(
605 return result_constraint_pair.second;
624 const exprt &pos_integer,
626 const typet &length_type,
627 const unsigned long radix)
641 pos_integer, max_length - 1, length_type, radix),
652 const exprt &integer,
653 const typet &length_type,
654 const unsigned long radix)
656 int max_pos_int_length;
660 max_pos_int_length = 10;
662 max_pos_int_length = 8;
675 integer, max_pos_int_length, length_type, radix),
731 const exprt arg_string =
763 INVARIANT(
false,
"format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
772 const std::vector<format_elementt> format_strings =
774 std::vector<exprt> intermediary_string_lengths;
775 std::size_t arg_count = 0;
780 if(fe.is_format_specifier())
791 arg_count <
inputs.size(),
792 "number of format must match specifiers");
793 arg =
inputs[arg_count++];
799 static_cast<std::size_t
>(fs.
index) <=
inputs.size(),
800 "number of format must match specifiers");
806 intermediary_string_lengths.push_back(
819 if(intermediary_string_lengths.empty())
826 exprt total_length = intermediary_string_lengths[0];
827 for(std::size_t i = 1; i < intermediary_string_lengths.size(); ++i)
830 plus_exprt{std::move(total_length), intermediary_string_lengths[i]};
833 std::move(total_length)});
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 index_type()
bitvector_typet char_type()
Correspondance between arrays and pointers string representations.
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
bool is_zero() const
Return whether the expression is a constant representing 0.
typet & type()
Return the type of the expression.
The Boolean constant false.
Fixed-width bit-vector with IEEE floating-point interpretation.
The trinary if-then-else operator.
const irep_idt & id() const
Class that provides messages with a built-in verbosity 'level'.
mstreamt & warning() const
The plus expression Associativity is not specified.
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_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_bool(const function_application_exprt &f)
symbol_generatort fresh_symbol
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.
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.
Semantic type conversion.
The type of an expression, extends irept.
const typet & subtype() const
The unary minus expression.
Fixed-width bit-vector with unsigned binary interpretation.
const std::string integer2string(const mp_integer &n, unsigned base)
nonstd::optional< T > optionalt
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
bool is_refined_string_type(const typet &type)
exprt simplify_expr(exprt src, const namespacet &ns)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
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)
array_string_exprt & to_array_string_expr(exprt &expr)
binary_relation_exprt greater_or_equal_to(exprt lhs, exprt rhs)
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