Go to the documentation of this file.
16 const std::function<
exprt(
const exprt &)> &get_value);
20 const std::vector<mp_integer> &array,
25 const exprt &return_code,
26 const std::vector<exprt> &fun_args,
31 const auto arg1 = expr_checked_cast<struct_exprt>(fun_args[2]);
32 input = array_pool.
find(arg1.op1(), arg1.op0());
33 result = array_pool.
find(fun_args[1], fun_args[0]);
37 const exprt &return_code,
38 const std::vector<exprt> &fun_args,
43 const auto arg1 = expr_checked_cast<struct_exprt>(fun_args[2]);
44 input1 = array_pool.
find(arg1.op1(), arg1.op0());
45 const auto arg2 = expr_checked_cast<struct_exprt>(fun_args[4]);
46 input2 = array_pool.
find(arg2.op1(), arg2.op0());
47 result = array_pool.
find(fun_args[1], fun_args[0]);
48 args.push_back(fun_args[3]);
49 args.insert(
args.end(), fun_args.begin() + 5, fun_args.end());
53 const exprt &return_code,
54 const std::vector<exprt> &fun_args,
58 PRECONDITION(fun_args.size() >= 4 && fun_args.size() <= 6);
59 const auto arg1 = expr_checked_cast<struct_exprt>(fun_args[2]);
60 input1 = array_pool.
find(arg1.op1(), arg1.op0());
61 const auto arg2 = expr_checked_cast<struct_exprt>(fun_args[3]);
62 input2 = array_pool.
find(arg2.op1(), arg2.op0());
63 result = array_pool.
find(fun_args[1], fun_args[0]);
64 args.insert(
args.end(), fun_args.begin() + 4, fun_args.end());
69 const std::function<
exprt(
const exprt &)> &get_value)
83 const auto &array = expr_try_dynamic_cast<array_exprt>(content);
87 const auto &ops = array->operands();
88 std::vector<mp_integer> result;
90 const auto &insert = std::back_inserter(result);
92 ops.begin(), ops.end(), insert, [unknown](
const exprt &e) {
93 if(const auto i = numeric_cast<mp_integer>(e))
100 template <
typename Iter>
106 const auto &insert = std::back_inserter(array_expr.
operands());
107 std::transform(begin, end, insert, [&](
const mp_integer &i) {
116 return make_string(array.begin(), array.end(), array_type);
120 const std::vector<mp_integer> &input1_value,
121 const std::vector<mp_integer> &input2_value,
122 const std::vector<mp_integer> &args_value)
const
124 const auto start_index =
125 args_value.size() > 0 && args_value[0] > 0 ? args_value[0] :
mp_integer(0);
126 const mp_integer input2_size(input2_value.size());
127 const auto end_index =
128 args_value.size() > 1
129 ? std::max(std::min(args_value[1], input2_size), start_index)
132 std::vector<mp_integer>
result(input1_value);
135 input2_value.begin() + numeric_cast_v<std::size_t>(start_index),
136 input2_value.begin() + numeric_cast_v<std::size_t>(end_index));
144 auto pair = [&]() -> std::pair<exprt, string_constraintst> {
170 const std::function<
exprt(
const exprt &)> &get_value)
const
173 if(!input_opt.has_value())
176 if(
const auto val = numeric_cast<mp_integer>(get_value(
character)))
180 "character valuation should only contain constants and unknown");
183 input_opt.value().push_back(char_val);
221 const std::function<
exprt(
const exprt &)> &get_value)
const
224 const auto char_opt = numeric_cast<mp_integer>(get_value(
character));
225 const auto position_opt = numeric_cast<mp_integer>(get_value(
position));
226 if(!input_opt || !char_opt || !position_opt)
228 if(0 <= *position_opt && *position_opt < input_opt.value().size())
229 input_opt.value()[numeric_cast_v<std::size_t>(*position_opt)] = *char_opt;
297 return (
'A' <= c && c <=
'Z') || (0xc0 <= c && c <= 0xd6) ||
298 (0xd8 <= c && c <= 0xde);
302 const std::function<
exprt(
const exprt &)> &get_value)
const
326 upper_case.push_back(
333 upper_case.push_back(
342 upper_case.push_back(
380 const exprt conditional_convert = [&] {
383 const typet &char_type = result.type().subtype();
384 const exprt diff = from_integer(0x20, char_type);
385 const exprt converted =
386 equal_exprt(result[idx], plus_exprt(input[idx], diff));
387 const exprt non_converted = equal_exprt(result[idx], input[idx]);
388 return if_exprt(is_upper_case(input[idx]), converted, non_converted);
397 const std::function<
exprt(
const exprt &)> &get_value)
const
431 const exprt converted =
444 const std::vector<mp_integer> &input1_value,
445 const std::vector<mp_integer> &input2_value,
446 const std::vector<mp_integer> &args_value)
const
448 PRECONDITION(args_value.size() >= 1 || args_value.size() <= 3);
449 const auto offset = std::min(
451 const auto start = args_value.size() > 1
455 const mp_integer input2_size(input2_value.size());
457 args_value.size() > 2
458 ? std::max(std::min(args_value[2], input2_size),
mp_integer(0))
461 std::vector<mp_integer>
result(input1_value);
463 result.begin() + numeric_cast_v<std::size_t>(offset),
464 input2_value.begin() + numeric_cast_v<std::size_t>(start),
465 input2_value.begin() + numeric_cast_v<std::size_t>(end));
470 const std::function<
exprt(
const exprt &)> &get_value)
const
474 if(!input2_value.has_value() || !input1_value.has_value())
477 std::vector<mp_integer> arg_values;
478 const auto &insert = std::back_inserter(arg_values);
482 if(const auto val = numeric_cast<mp_integer>(get_value(e)))
487 const auto result_value =
eval(*input1_value, *input2_value, arg_values);
523 const exprt &return_code,
524 const std::vector<exprt> &fun_args,
529 result = array_pool.
find(fun_args[1], fun_args[0]);
534 const std::function<
exprt(
const exprt &)> &get_value)
const
536 const auto arg_value = numeric_cast<mp_integer>(get_value(
arg));
539 static std::string digits =
"0123456789abcdefghijklmnopqrstuvwxyz";
540 const auto radix_value = numeric_cast<mp_integer>(get_value(
radix));
541 if(!radix_value || *radix_value > digits.length())
545 std::vector<mp_integer> right_to_left_characters;
546 if(current_value < 0)
547 current_value = -current_value;
548 if(current_value == 0)
549 right_to_left_characters.emplace_back(
'0');
550 while(current_value > 0)
552 const auto digit_value = (current_value % *radix_value).to_ulong();
553 right_to_left_characters.emplace_back(digits.at(digit_value));
554 current_value /= *radix_value;
557 right_to_left_characters.emplace_back(
'-');
559 const auto length = right_to_left_characters.size();
563 right_to_left_characters.rbegin(), right_to_left_characters.rend(), type);
578 const auto radix_opt = numeric_cast<std::size_t>(
radix);
579 const auto radix_value = radix_opt.has_value() ? radix_opt.value() : 2;
580 const std::size_t upper_bound =
582 const exprt negative_arg =
584 const exprt absolute_arg =
589 for(std::size_t current_size = 2; current_size <= upper_bound + 1;
592 min_int_with_current_size =
mult_exprt(
radix, min_int_with_current_size);
593 const exprt at_least_current_size =
596 at_least_current_size,
from_integer(current_size, type), size_expr);
605 const exprt &return_code,
610 const std::vector<exprt> &fun_args = f.
arguments();
612 if(fun_args.size() >= 2 && fun_args[1].type().id() == ID_pointer)
618 for(; i < fun_args.size(); ++i)
620 const auto arg = expr_try_dynamic_cast<struct_exprt>(fun_args[i]);
623 arg && arg->operands().size() == 2 &&
624 arg->op1().type().id() == ID_pointer)
630 args.push_back(fun_args[i]);
string_constraintst constraints(string_constraint_generatort &generator) const override
Set of constraints enforcing that result is the concatenation of input with character.
#define PRECONDITION(CONDITION)
string_concatenation_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_for_concat_substr(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &start_index, const exprt &end_index)
Add axioms enforcing that the length of res is that of the concatenation of s1 with the substring of ...
const typet & subtype() const
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...
String inserting a string into another one.
static bool eval_is_upper_case(const mp_integer &c)
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
exprt minimum(const exprt &a, const exprt &b)
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
The type of an expression, extends irept.
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...
string_constraintst constraints(class symbol_generatort &fresh_symbol) const
Set of constraints ensuring result corresponds to input in which lowercase characters of Basic Latin ...
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Correspondance between arrays and pointers string representations.
The trinary if-then-else operator.
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
symbol_generatort fresh_symbol
The plus expression Associativity is not specified.
function_application_exprt function_application
Base class for all expressions.
exprt length_constraint_for_insert(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
Add axioms ensuring the length of res corresponds to that of s1 where we inserted 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, const namespacet &ns)
Add axioms enforcing that the string corresponds to the result of String.valueOf(II) or String....
std::vector< array_string_exprt > string_args
std::pair< exprt, string_constraintst > add_axioms_for_function_application(symbol_generatort &fresh_symbol, const function_application_exprt &expr)
strings contained in this call are converted to objects of type string_exprt, through adding axioms.
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 ...
Collection of constraints of different types: existential formulas, universal formulas,...
std::vector< exprt > args
bool is_true() const
Return whether the expression is a constant representing true.
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 ...
static optionalt< std::vector< mp_integer > > eval_string(const array_string_exprt &a, const std::function< exprt(const exprt &)> &get_value)
Module: String solver Author: Diffblue Ltd.
Expression to hold a symbol (variable)
#define UNREACHABLE
This should be used to mark dead code.
array_string_exprt input1
virtual std::vector< mp_integer > eval(const std::vector< mp_integer > &input1_value, const std::vector< mp_integer > &input2_value, const std::vector< mp_integer > &args_value) const
Evaluate the result from a concrete valuation of the arguments.
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
typet & type()
Return the type of the expression.
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
array_string_exprt result
Generation of fresh symbols of a given type.
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
string_builtin_function_with_no_evalt(const exprt &return_code, const function_application_exprt &f, array_poolt &array_pool)
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...
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
#define CHARACTER_FOR_UNKNOWN
exprt length_constraint_for_concat_char(const array_string_exprt &res, const array_string_exprt &s1)
Add axioms enforcing that the length of res is that of the concatenation of s1 with.
string_insertion_builtin_functiont(const exprt &return_code, const std::vector< exprt > &fun_args, array_poolt &array_pool)
Constructor from arguments of a function application.
std::pair< exprt, string_constraintst > add_axioms_for_concat_substr(symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &start_index, const exprt &end_index)
Add axioms enforcing that res is the concatenation of s1 with the substring of s2 starting at index ‘...
Application of (mathematical) function.
Binary multiplication Associativity is not specified.
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...
The unary minus expression.
const irep_idt & id() const
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 ...
std::vector< exprt > operandst
array_string_exprt & to_array_string_expr(exprt &expr)
nonstd::optional< T > optionalt
Base class for string functions that are built in the solver.
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...
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...
bitvector_typet char_type()
static array_string_exprt make_string(const std::vector< mp_integer > &array, const array_typet &array_type)
Make a string from a constant array.
optionalt< array_string_exprt > string_res
const array_string_exprt & find(const exprt &pointer, const exprt &length)
Creates a new array if the pointer is not pointing to an array.
array_string_exprt result
std::pair< exprt, string_constraintst > add_axioms_for_insert(symbol_generatort &fresh_symbol, const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2, const exprt &offset)
Add axioms ensuring the result res corresponds to s1 where we inserted s2 at position offset.
exprt zero_if_negative(const exprt &expr)
Returns a non-negative version of the argument.
bool is_constant() const
Return whether the expression is a constant.
A base class for relations, i.e., binary predicates.
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 ...
bool is_refined_string_type(const typet &type)
std::pair< exprt, string_constraintst > add_axioms_for_concat(symbol_generatort &fresh_symbol, 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.
array_string_exprt input2
std::vector< exprt > args
exprt length_constraint_for_concat(const array_string_exprt &res, const array_string_exprt &s1, const array_string_exprt &s2)
Add axioms enforcing that the length of res is that of the concatenation of s1 with s2
exprt length_constraint() const override
Constraint ensuring that the length of the strings are coherent with the function call.
std::vector< mp_integer > eval(const std::vector< mp_integer > &input1_value, const std::vector< mp_integer > &input2_value, const std::vector< mp_integer > &args_value) const override
Evaluate the result from a concrete valuation of the arguments.
Array constructor from list of elements.
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.
string_constraintst constraints(string_constraint_generatort &generator) const override
Set of constraints ensuring result corresponds to input in which uppercase characters have been conve...
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.
std::vector< exprt > existential
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 ...
std::vector< string_constraintt > universal