1/*******************************************************************\
3Module: Built-in function for String.format
5Author: Romain Brenguier, Joel Allred
7\*******************************************************************/
30 const exprt &return_code,
40 // List of arguments after the format string
42 .map([&](
const exprt &arg) {
45 "arguments of format should be strings");
48 .collect<std::vector<array_string_exprt>>();
50 // format_string is only initialized if the expression is constant
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
72 "%(\\d+\\$)?([-#+ 0,(\\<]*)?(\\d+)?(\\.\\d+)?([tT])?([a-zA-Z%])";
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)
117static std::pair<array_string_exprt, string_constraintst>
122 const typet &index_type,
129 std::pair<exprt, string_constraintst> return_code;
130 switch(
fs.conversion)
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)};
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.
172 return {
res, constraints};
177 return {
res, std::move(return_code.second)};
187 return {
res, std::move(return_code.second)};
189 // TODO: the constant should depend on the system: System.lineSeparator()
191 return {
res, std::move(return_code.second)};
194 return {
res, std::move(return_code.second)};
227 // For all these unimplemented cases we return a non-deterministic string
229 message.warning() <<
"unimplemented format specifier: " <<
fs.conversion
236 "format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
252 if(
id ==
"string_expr")
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]
269 // Leave the string unchanged as the "null" string is used to represent null
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]
282 // Deserialize an int and cast to float
300 const std::string &s,
301 const std::vector<array_string_exprt> &args,
310 const typet &index_type =
res.length_type();
316 if(
fe.is_format_specifier())
327 arg_count < args.size(),
"number of format must match specifiers");
332 INVARIANT(
fs.index > 0,
"index in format should be positive");
334 static_cast<std::size_t
>(
fs.index) <= args.size(),
335 "number of format must match specifiers");
337 // first argument `args[0]` corresponds to index 1
344 merge(constraints, std::move(result.second));
352 str,
fe.get_format_text().get_content());
353 merge(constraints, result.second);
364 return {return_code, constraints};
371 // Copy the first string
377 merge(constraints, std::move(result.second));
378 return {result.first, std::move(constraints)};
381 // start after the first string and stop before the last
388 return_code =
maximum(return_code, result.first);
389 merge(constraints, std::move(result.second));
395 merge(constraints, std::move(result.second));
396 return {
maximum(result.first, return_code), std::move(constraints)};
405 // long value, to be used for other formats?
406 for(std::size_t i = 0; i < 4; i++)
410 "Component of serialized value to"
411 "format must be bounded by 0xFFFF");
425 return string.size() == 4 &&
string[0] ==
'n' &&
string[1] ==
'u' &&
426 string[2] ==
'l' &&
string[3] ==
'l';
433 const std::vector<mp_integer> &arg)
435 switch(
fs.conversion)
440 return std::vector<mp_integer>{
'n',
'u',
'l',
'l'};
446 return std::vector<mp_integer>{
'n',
'u',
'l',
'l'};
448 // convert to lower case
450 if(
'A' <=
c &&
c <=
'Z')
458 return std::vector<mp_integer>{
'n',
'u',
'l',
'l'};
468 return std::vector<mp_integer>{
'n',
'u',
'l',
'l'};
469 return std::vector<mp_integer>{arg[3]};
474 return std::vector<mp_integer>{
't',
'r',
'u',
'e'};
475 return std::vector<mp_integer>{
'f',
'a',
'l',
's',
'e'};
482 // TODO: the constant should depend on the system: System.lineSeparator()
483 return std::vector<mp_integer>{
'\n'};
485 return std::vector<mp_integer>{
'%'};
500 if(
'a' <=
c &&
c <=
'z')
516 INVARIANT(
false,
"format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
520 const std::function<
exprt(
const exprt &)> &get_value)
const
532 if(
fe.is_format_specifier())
545 "number of format must match specifiers");
553 INVARIANT(
fs.index > 0,
"index in format should be positive");
555 static_cast<std::size_t
>(
fs.index) <=
inputs.size(),
556 "number of format must match specifiers");
558 // first argument `args[0]` corresponds to index 1
575 // TODO: the character should depend on the system:
576 // System.lineSeparator()
582 for(
char c :
fe.get_format_text().get_content())
593 // When `format_string` was not set, leave the result non-deterministic
601 "add_axioms_for_format should return 0, meaning that formatting was"
626 const typet &length_type,
627 const unsigned long radix)
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.
653 const typet &length_type,
654 const unsigned long radix)
668 // We only handle 32-bit signed integer type for now.
687 const typet &index_type,
690 switch(
fs.conversion)
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.
739 // TODO: the constant should depend on the system: System.lineSeparator()
759 // For all these unimplemented cases we return a non-deterministic string
763 INVARIANT(
false,
"format specifier must belong to [bBhHsScCdoxXeEfgGaAtT%n]");
780 if(
fe.is_format_specifier())
792 "number of format must match specifiers");
797 INVARIANT(
fs.index > 0,
"index in format should be positive");
799 static_cast<std::size_t
>(
fs.index) <=
inputs.size(),
800 "number of format must match specifiers");
802 // first argument `args[0]` corresponds to index 1
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()
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Boolean AND All operands must be boolean, and the result is always boolean.
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
Bit-wise OR Any number of operands that is greater or equal one.
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_constant() const
Return whether the expression is a constant.
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.
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_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....
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...
The Boolean constant true.
Semantic type conversion.
The type of an expression, extends irept.
The unary minus expression.
Fixed-width bit-vector with unsigned binary interpretation.
double pow(double x, double y)
const std::string integer2string(const mp_integer &n, unsigned base)
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'.
#define UNREACHABLE_BECAUSE(REASON)
exprt conjunction(exprt a, exprt b)
Conjunction of two expressions.
const array_exprt & to_array_expr(const exprt &expr)
Cast an exprt to an array_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_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)
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)
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
const type_with_subtypet & to_type_with_subtype(const typet &type)