31 const exprt &return_code,
32 const std::vector<exprt> &fun_args,
43 .map([&](
const exprt &arg) {
46 "arguments of format should be strings");
49 .collect<std::vector<array_string_exprt>>();
54 format_string_expr.
content().
id() == ID_array)
56 const auto length = numeric_cast_v<std::size_t>(
70 static bool check_format_string(std::string s)
72 std::string format_specifier=
73 "%(\\d+\\$)?([-#+ 0,(\\<]*)?(\\d+)?(\\.\\d+)?([tT])?([a-zA-Z%])";
74 std::regex regex(format_specifier);
77 while(std::regex_search(s, match, regex))
79 if(match.position()!= 0)
80 for(
const auto &c : match.str())
86 for(
const auto &c : s)
118 static std::pair<array_string_exprt, string_constraintst>
130 std::pair<exprt, string_constraintst> return_code;
136 return {res, std::move(return_code.second)};
143 return {res, std::move(return_code.second)};
147 return {res, std::move(return_code.second)};
151 return {res, std::move(return_code.second)};
158 const exprt is_null_literal =
is_null(string_expr, array_pool);
173 return {res, constraints};
178 return {res, std::move(return_code.second)};
181 const exprt arg_string = string_arg;
183 return {std::move(string_expr), {}};
188 return {res, std::move(return_code.second)};
192 return {res, std::move(return_code.second)};
195 return {res, std::move(return_code.second)};
210 const exprt return_code_upper_case =
213 return_code_upper_case, res, format_specifier_result.first, array_pool);
214 auto upper_case_constraints =
216 merge(upper_case_constraints, std::move(format_specifier_result.second));
217 return {res, std::move(upper_case_constraints)};
233 INVARIANT(
false,
"format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
248 if(
id ==
"string_expr")
296 const std::string &s,
297 const std::vector<array_string_exprt> &args,
303 std::vector<array_string_exprt> intermediary_strings;
304 std::size_t arg_count = 0;
312 if(fe.is_format_specifier())
323 arg_count < args.size(),
"number of format must match specifiers");
324 string_arg = args[arg_count++];
330 static_cast<std::size_t
>(fs.
index) <= args.size(),
331 "number of format must match specifiers");
334 string_arg = args[fs.
index - 1];
340 merge(constraints, std::move(result.second));
341 intermediary_strings.push_back(result.first);
348 str, fe.get_format_text().get_content());
349 merge(constraints, result.second);
350 intermediary_strings.push_back(str);
356 if(intermediary_strings.empty())
360 return {return_code, constraints};
365 if(intermediary_strings.size() == 1)
373 merge(constraints, std::move(result.second));
374 return {result.first, std::move(constraints)};
378 for(std::size_t i = 1; i < intermediary_strings.size() - 1; ++i)
384 return_code =
maximum(return_code, result.first);
385 merge(constraints, std::move(result.second));
391 merge(constraints, std::move(result.second));
392 return {
maximum(result.first, return_code), std::move(constraints)};
396 const std::vector<mp_integer> serialized,
402 for(std::size_t i = 0; i < 4; i++)
405 serialized[i] <= 0xFFFF,
406 "Component of serialized value to"
407 "format must be bounded by 0xFFFF");
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);
421 return string.size() == 4 &&
string[0] ==
'n' &&
string[1] ==
'u' &&
422 string[2] ==
'l' &&
string[3] ==
'l';
429 const std::vector<mp_integer> &arg)
436 return std::vector<mp_integer>{
'n',
'u',
'l',
'l'};
442 return std::vector<mp_integer>{
'n',
'u',
'l',
'l'};
446 if(
'A' <= c && c <=
'Z')
454 return std::vector<mp_integer>{
'n',
'u',
'l',
'l'};
464 return std::vector<mp_integer>{
'n',
'u',
'l',
'l'};
465 return std::vector<mp_integer>{arg[3]};
470 return std::vector<mp_integer>{
't',
'r',
'u',
'e'};
471 return std::vector<mp_integer>{
'f',
'a',
'l',
's',
'e'};
479 return std::vector<mp_integer>{
'\n'};
481 return std::vector<mp_integer>{
'%'};
496 if(
'a' <= c && c <=
'z')
512 INVARIANT(
false,
"format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
516 const std::function<
exprt(
const exprt &)> &get_value)
const
521 const std::vector<format_elementt> format_strings =
523 std::vector<mp_integer> result_vector;
524 std::size_t arg_count = 0;
528 if(fe.is_format_specifier())
535 std::vector<mp_integer> evaluated_char_vector;
540 arg_count <
inputs.size(),
541 "number of format must match specifiers");
551 static_cast<std::size_t
>(fs.
index) <=
inputs.size(),
552 "number of format must match specifiers");
561 evaluated_char_vector.begin(),
562 evaluated_char_vector.end(),
563 std::back_inserter(result_vector));
567 result_vector.push_back(
'%');
573 result_vector.push_back(
'\n');
578 for(
char c : fe.get_format_text().get_content())
579 result_vector.emplace_back(c);
602 "add_axioms_for_format should return 0, meaning that formatting was"
604 result_constraint_pair.second.existential.push_back(
606 return result_constraint_pair.second;
625 const exprt &pos_integer,
627 const typet &length_type,
628 const unsigned long radix)
642 pos_integer, max_length - 1, length_type, radix),
653 const exprt &integer,
654 const typet &length_type,
655 const unsigned long radix)
657 int max_pos_int_length;
661 max_pos_int_length = 10;
663 max_pos_int_length = 8;
676 integer, max_pos_int_length, length_type, radix),
732 const exprt arg_string =
764 INVARIANT(
false,
"format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
773 const std::vector<format_elementt> format_strings =
775 std::vector<exprt> intermediary_string_lengths;
776 std::size_t arg_count = 0;
781 if(fe.is_format_specifier())
792 arg_count <
inputs.size(),
793 "number of format must match specifiers");
794 arg =
inputs[arg_count++];
800 static_cast<std::size_t
>(fs.
index) <=
inputs.size(),
801 "number of format must match specifiers");
807 intermediary_string_lengths.push_back(
820 if(intermediary_string_lengths.empty())
827 exprt total_length = intermediary_string_lengths[0];
828 for(std::size_t i = 1; i < intermediary_string_lengths.size(); ++i)
831 plus_exprt{std::move(total_length), intermediary_string_lengths[i]};
834 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'.
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'.
static const char * message(const statust &status)
Makes a status message string from a status.
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