13 const exprt &return_code,
14 const std::vector<exprt> &fun_args,
19 const auto arg1 = expr_checked_cast<struct_exprt>(fun_args[2]);
26 const std::function<
exprt(
const exprt &)> &get_value)
40 const auto &array = expr_try_dynamic_cast<array_exprt>(content);
44 const auto &ops = array->operands();
45 std::vector<mp_integer> result;
47 const auto &insert = std::back_inserter(result);
49 ops.begin(), ops.end(), insert, [unknown](
const exprt &e) {
50 if(const auto i = numeric_cast<mp_integer>(e))
57 template <
typename Iter>
63 const auto &insert = std::back_inserter(array_expr.operands());
73 return make_string(array.begin(), array.end(), array_type);
77 const std::function<
exprt(
const exprt &)> &get_value)
const
80 if(!input_opt.has_value())
83 if(
const auto val = numeric_cast<mp_integer>(get_value(
character)))
87 "character valuation should only contain constants and unknown");
90 input_opt.value().push_back(char_val);
111 const exprt upper_bound =
129 const std::function<
exprt(
const exprt &)> &get_value)
const
132 const auto char_opt = numeric_cast<mp_integer>(get_value(
character));
133 const auto position_opt = numeric_cast<mp_integer>(get_value(
position));
134 if(!input_opt || !char_opt || !position_opt)
136 if(0 <= *position_opt && *position_opt < input_opt.value().size())
137 input_opt.value()[numeric_cast_v<std::size_t>(*position_opt)] = *char_opt;
212 return (
'A' <= c && c <=
'Z') || (0xc0 <= c && c <= 0xd6) ||
213 (0xd8 <= c && c <= 0xde);
217 const std::function<
exprt(
const exprt &)> &get_value)
const
292 const exprt conditional_convert = [&] {
295 const typet &char_type = to_type_with_subtype(result.type()).subtype();
296 const exprt diff = from_integer(0x20, char_type);
297 const exprt converted =
298 equal_exprt(result[idx], plus_exprt(input[idx], diff));
299 const exprt non_converted = equal_exprt(result[idx], input[idx]);
300 return if_exprt(is_upper_case(input[idx]), converted, non_converted);
305 conditional_convert);
311 const std::function<
exprt(
const exprt &)> &get_value)
const
346 const exprt converted =
364 const exprt &return_code,
365 const std::vector<exprt> &fun_args,
375 const std::function<
exprt(
const exprt &)> &get_value)
const
377 const auto arg_value = numeric_cast<mp_integer>(get_value(
arg));
380 static std::string digits =
"0123456789abcdefghijklmnopqrstuvwxyz";
381 const auto radix_value = numeric_cast<mp_integer>(get_value(
radix));
382 if(!radix_value || *radix_value > digits.length())
386 std::vector<mp_integer> right_to_left_characters;
387 if(current_value < 0)
388 current_value = -current_value;
389 if(current_value == 0)
390 right_to_left_characters.emplace_back(
'0');
391 while(current_value > 0)
393 const auto digit_value = (current_value % *radix_value).to_ulong();
394 right_to_left_characters.emplace_back(digits.at(digit_value));
395 current_value /= *radix_value;
398 right_to_left_characters.emplace_back(
'-');
400 const auto length = right_to_left_characters.size();
405 right_to_left_characters.rbegin(), right_to_left_characters.rend(), type);
420 const auto radix_opt = numeric_cast<std::size_t>(
radix);
421 const auto radix_value = radix_opt.has_value() ? radix_opt.value() : 2;
422 const std::size_t upper_bound =
424 const exprt negative_arg =
426 const exprt absolute_arg =
431 for(std::size_t current_size = 2; current_size <= upper_bound + 1;
434 min_int_with_current_size =
mult_exprt(
radix, min_int_with_current_size);
435 const exprt at_least_current_size =
438 at_least_current_size,
from_integer(current_size, type), size_expr);
448 const exprt &return_code,
453 const std::vector<exprt> &fun_args = f.
arguments();
455 if(fun_args.size() >= 2 && fun_args[1].type().id() == ID_pointer)
461 for(; i < fun_args.size(); ++i)
463 const auto arg = expr_try_dynamic_cast<struct_exprt>(fun_args[i]);
466 arg && arg->operands().size() == 2 &&
467 arg->op1().type().id() == ID_pointer)
473 args.push_back(fun_args[i]);
static abstract_object_pointert transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
bitvector_typet char_type()
Array constructor from list of elements.
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 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
const typet & element_type() const
The type of the elements of the array.
A base class for relations, i.e., binary predicates whose two operands have the same type.
Base class for all expressions.
std::vector< exprt > operandst
bool is_true() const
Return whether the expression is a constant representing true.
typet & type()
Return the type of the expression.
bool is_constant() const
Return whether the expression is a constant.
Application of (mathematical) function.
The trinary if-then-else operator.
const irep_idt & id() const
Binary multiplication Associativity is not specified.
The plus expression Associativity is not specified.
std::vector< array_string_exprt > string_args
std::vector< exprt > args
optionalt< array_string_exprt > string_res
string_builtin_function_with_no_evalt(const exprt &return_code, const function_application_exprt &f, array_poolt &array_pool)
function_application_exprt function_application
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...
Base class for string functions that are built in the solver.
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 ...
string_constraintst constraints(string_constraint_generatort &generator) const override
Set of constraints enforcing that result is the concatenation of input with character.
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
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_function_application(const function_application_exprt &expr)
strings contained in this call are converted to objects of type string_exprt, through adding axioms.
symbol_generatort fresh_symbol
array_string_exprt result
string_creation_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Constructor from arguments of a function application.
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) const override
Add constraints ensuring that the value of result expression of the builtin function corresponds to t...
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 ...
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
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 ...
string_constraintst constraints(string_constraint_generatort &generator) const override
Set of constraints ensuring that result is similar to input where the character at index position is ...
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 ...
string_constraintst constraints(string_constraint_generatort &generator) const override
Set of constraints ensuring result corresponds to input in which uppercase characters have been conve...
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
string_constraintst constraints(class symbol_generatort &fresh_symbol) const
Set of constraints ensuring result corresponds to input in which lowercase characters of Basic Latin ...
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 ...
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
Expression to hold a symbol (variable)
Generation of fresh symbols of a given type.
const typet & subtype() const
The type of an expression, extends irept.
The unary minus expression.
nonstd::optional< T > optionalt
bool is_refined_string_type(const typet &type)
#define PRECONDITION(CONDITION)
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
static exprt is_lower_case(const exprt &character)
Expression which is true for lower_case characters of the Basic Latin and Latin-1 supplement of unico...
static array_string_exprt make_string(Iter begin, Iter end, const array_typet &array_type)
static exprt is_upper_case(const exprt &character)
Expression which is true for uppercase characters of the Basic Latin and Latin-1 supplement of unicod...
static bool eval_is_upper_case(const mp_integer &c)
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 ...
#define CHARACTER_FOR_UNKNOWN
Module: String solver Author: Diffblue Ltd.
exprt length_constraint_for_concat_char(const array_string_exprt &res, const array_string_exprt &s1, array_poolt &array_pool)
Add axioms enforcing that the length of res is that of the concatenation of s1 with.
Generates string constraints to link results from string functions with their arguments.
exprt minimum(const exprt &a, const exprt &b)
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
size_t max_printed_string_length(const typet &type, unsigned long ul_radix)
Calculate the string length needed to represent any value of the given type using the given radix.
array_string_exprt & to_array_string_expr(exprt &expr)
Collection of constraints of different types: existential formulas, universal formulas,...
std::vector< exprt > existential
std::vector< string_constraintt > universal
const type_with_subtypet & to_type_with_subtype(const typet &type)