24#include <unordered_set>
68 const std::function<
exprt(
const exprt &)> &get,
71 bool use_counter_example,
73 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
96 const std::vector<exprt> ¤t_constraints);
106 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
132 std::vector<T> result;
138 const std::size_t index = it->first;
139 const T &value = it->second;
140 const auto next = std::next(it);
160 loop_bound_(
info.refinement_bound),
174 std::size_t count = 0;
181 for(
const auto &
j :
i.second)
183 const auto it =
index_set.current.find(
i.first);
185 it !=
index_set.current.end() && it->second.find(
j) != it->second.end())
223 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
226 std::vector<exprt>
lemmas;
231 for(
const auto &
j :
i.second)
303 const std::vector<exprt> &equations,
308 "WARNING string_refinement.cpp generate_symbol_resolution_from_equations:";
309 auto equalities =
make_range(equations).filter(
311 for(
const exprt &e : equalities)
326 <<
"\n####################### rhs: " <<
format(rhs)
373static std::vector<exprt>
376 std::vector<exprt> result;
378 result.push_back(lhs);
398static std::vector<exprt>
401 std::vector<exprt> result;
406 result.push_back(*it);
407 it.next_sibling_or_parent();
413 it.next_sibling_or_parent();
464 const std::vector<equal_exprt> &equations,
469 "WARNING string_refinement.cpp "
470 "string_identifiers_resolution_from_equations:";
478 for(std::size_t
i = 0;
i < equations.size(); ++
i)
502 <<
format(
eq.lhs()) <<
"\n * of type "
518 for(
const std::size_t
j :
equation_map.find_equations(
string))
538 for(std::size_t
i = 0;
i < equations.size(); ++
i)
539 output <<
" [" <<
i <<
"] " <<
format(equations[
i]) << std::endl;
614 log.
debug() <<
"dec_solve: Build symbol solver from equations"
630 std::vector<equal_exprt> equalities;
649 log.
debug() <<
"dec_solve: Replacing string ids and simplifying arguments"
650 " in function applications"
654 auto it = expr.depth_begin();
655 while(it != expr.depth_end())
665 it.next_sibling_or_parent();
681 log.
debug() <<
"dec_solve: compute dependency graph and remove function "
682 <<
"applications captured by the dependencies:" <<
messaget::eom;
736 constraint.replace_expr(symbol_resolve);
738 is_valid_string_constraint(log.error(), ns, constraint),
739 string_refinement_invariantt(
740 "string constraints satisfy their invariant"));
749 replace(symbol_resolve, axiom);
754 std::unordered_map<string_not_contains_constraintt, symbol_exprt>
781 const auto get = [
this](
const exprt &expr) {
return this->
get(expr); };
802 log.
debug() <<
"check_SAT: got SAT but the model is not correct"
846 <<
"check_SAT: got SAT but the model is not correct, refining..."
862 log.
error() <<
"dec_solve: current index set is empty, "
868 log.
debug() <<
"dec_solve: current index set is empty, "
875 const auto instances =
877 for(
const auto &
instance : instances)
883 log.
debug() <<
"check_SAT: default return "
888 log.
debug() <<
"string_refinementt::dec_solve reached the maximum number"
925 if(it->id() ==
ID_array && it->operands().empty())
931 it.next_sibling_or_parent();
971 stream <<
"(sr::get_valid_array_size) string of unknown size: "
1009 if(!size.has_value())
1018 stream <<
"(sr::get_valid_array_size) long string (size "
1020 stream <<
"(sr::get_valid_array_size) consider reducing "
1021 "max-nondet-string-length so "
1022 "that no string exceeds "
1024 <<
" in length and "
1025 "make sure all functions returning strings are loaded"
1027 stream <<
"(sr::get_valid_array_size) this can also happen on invalid "
1051 return std::string(
"");
1081 stream << std::string(4,
' ')
1084 stream << std::string(4,
' ')
1090 stream << std::string(4,
' ')
1098 stream << std::string(4,
' ') <<
"- as_string: \""
1102 stream << std::string(2,
' ') <<
"- warning: not an array"
1119 const std::vector<symbol_exprt> &symbols,
1122 stream <<
"debug_model:" <<
'\n';
1134 for(
const auto &symbol : symbols)
1136 stream <<
" - " << symbol.get_identifier() <<
": "
1222 "in case the array is unknown, it should be a symbol or nil, id: ") +
1245 it.mutate() = *result;
1291 const std::function<
exprt(
const exprt &)> &get)
1328template <
typename T>
1336 stream << std::string(4,
' ') <<
"- axiom:\n" << std::string(6,
' ');
1339 << std::string(4,
' ') <<
"- axiom_in_model:\n"
1340 << std::string(6,
' ');
1342 << std::string(4,
' ') <<
"- negated_axiom:\n"
1344 stream << std::string(4,
' ') <<
"- negated_axiom_with_concretized_arrays:\n"
1352 const std::function<
exprt(
const exprt &)> &get,
1355 bool use_counter_example,
1357 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
1363 auto pairs = symbol_resolve.
to_vector();
1364 for(
const auto &
pair : pairs)
1381 stream <<
"string_refinement::check_axioms: " << axioms.
universal.size()
1388 get(
axiom.lower_bound),
1389 get(
axiom.upper_bound),
1395 stream << std::string(2,
' ') <<
i <<
".\n";
1406 stream.message.get_message_handler()))
1408 stream << std::string(4,
' ')
1409 <<
"- violated_for: " <<
format(
axiom.univ_var) <<
"="
1426 "not_contains_univ_var",
nc_axiom.s0.length_type());
1432 stream << std::string(2,
' ') <<
i <<
".\n";
1440 stream << std::string(4,
' ')
1450 return {
true, std::vector<exprt>()};
1454 stream <<
violated.size() <<
" universal string axioms can be violated"
1457 <<
" not_contains string axioms can be violated" <<
messaget::eom;
1459 if(use_counter_example)
1461 std::vector<exprt>
lemmas;
1472 axiom.univ_within_bounds(),
1489 std::set<std::pair<exprt, exprt>> indices;
1498 return {
false, std::vector<exprt>()};
1531 const std::vector<exprt> ¤t_constraints)
1533 for(
const auto &
axiom : current_constraints)
1583 if(
index_set.cumulative[sub].insert(
i).second)
1607 const exprt &upper_bound,
1616 for(std::size_t
j = 0;
j < s.
operands().size(); ++
j)
1639 auto it =
axiom.body.depth_begin();
1640 const auto end =
axiom.body.depth_end();
1648 it.next_sibling_or_parent();
1660 auto it =
axiom.premise.depth_begin();
1661 const auto end =
axiom.premise.depth_end();
1672 it.next_sibling_or_parent();
1739 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
1756 typedef std::pair<exprt, exprt> expr_pairt;
1793 for(
size_t i = 0;
i < expr.
operands().size();
i += 2)
1828 std::reference_wrapper<const exprt> current(
index_expr->array());
1829 while(current.get().id() ==
ID_if)
1834 current = std::cref(
if_expr.true_case());
1836 current = std::cref(
if_expr.false_case());
1848 const exprt unknown =
1859 "Apart from symbols, array valuations can be interpreted as "
1860 "sparse arrays. Array model : " + array.pretty());
1932 [&](
const exprt &expr)
1934 const auto index_expr = expr_try_dynamic_cast<const index_exprt>(expr);
1936 indices[index_expr->array()].push_back(index_expr->index());
1956 if(std::find(it->depth_begin(), it->depth_end(), var) != it->depth_end())
1959 it.next_sibling_or_parent();
1976 for(
auto it =
constr.body.depth_begin(); it !=
constr.body.depth_end();)
1978 if(*it ==
constr.univ_var)
1981 it.next_sibling_or_parent();
2006 for(
size_t j = 0;
j <
pair.second.size() - 1;
j++)
2020 if(!is_linear_arithmetic_expr(rep, constraint.
univ_var))
2029 if(!universal_only_in_index(constraint))
2031 stream <<
"Universal variable outside of index:" <<
to_string(constraint)
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_tablet &symbol_table, message_handlert &message_handler)
bitvector_typet index_type()
bitvector_typet char_type()
virtual void clear()
Reset the abstract state.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Array constructor from list of elements.
Array constructor from single element.
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.
const std::unordered_map< exprt, array_string_exprt, irep_hash > & get_arrays_of_pointers() const
optionalt< exprt > get_length_if_exists(const array_string_exprt &s) const
As opposed to get_length(), do not create a new symbol if the length of the array_string_exprt does n...
const std::unordered_map< array_string_exprt, exprt, irep_hash > & created_strings() const
Return a map mapping all array_string_exprt of the array_pool to their length.
const exprt & size() const
A base class for relations, i.e., binary predicates whose two operands have the same type.
decision_proceduret::resultt dec_solve() override
Run the decision procedure to solve the problem.
A constant literal expression.
resultt
Result of running the decision procedure.
virtual exprt get(const exprt &expr) const =0
Return expr with variables replaced by values from satisfying assignment if available.
virtual void set_to(const exprt &expr, bool value)=0
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
Maps equation to expressions contained in them and conversely expressions to equations that contain t...
Base class for all expressions.
bool is_true() const
Return whether the expression is a constant representing true.
depth_iteratort depth_end()
depth_iteratort depth_begin()
bool is_false() const
Return whether the expression is a constant representing false.
bool is_constant() const
Return whether the expression is a constant.
typet & type()
Return the type of the expression.
The trinary if-then-else operator.
An expression denoting infinity.
Represents arrays by the indexes up to which the value remains the same.
exprt to_if_expression(const exprt &index) const
static optionalt< interval_sparse_arrayt > of_expr(const exprt &expr, const exprt &extra_value)
If the expression is an array_exprt or a with_exprt uses the appropriate constructor,...
const irep_idt & id() const
Canonical representation of linear function, for instance, expression $x + x - y + 5 - 3$ would given...
Extract member of struct or union.
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
The plus expression Associativity is not specified.
bool equality_propagation
void l_set_to_true(literalt a)
static exprt to_if_expression(const with_exprt &expr, const exprt &index)
Creates an if_expr corresponding to the result of accessing the array at the given index.
optionalt< exprt > make_array_pointer_association(const exprt &return_code, const function_application_exprt &expr)
Associate array to pointer, and array to length.
symbol_generatort fresh_symbol
static bool is_valid_string_constraint(messaget::mstreamt &stream, const namespacet &ns, const string_constraintt &constraint)
Checks the data invariant for string_constraintt.
static array_index_mapt gather_indices(const exprt &expr)
static bool universal_only_in_index(const string_constraintt &constr)
The universally quantified variable is only allowed to occur in index expressions in the body of a st...
static bool is_linear_arithmetic_expr(const exprt &expr, const symbol_exprt &var)
std::map< exprt, std::vector< exprt > > array_index_mapt
void output_dot(std::ostream &stream) const
void clean_cache()
Clean the cache used by eval
NODISCARD string_constraintst add_constraints(string_constraint_generatort &generatort)
For all builtin call on which a test (or an unsupported buitin) result depends, add the corresponding...
optionalt< exprt > eval(const array_string_exprt &s, const std::function< exprt(const exprt &)> &get_value) const
Attempt to evaluate the given string from the dependencies and valuation of strings on which it depen...
string_constraint_generatort generator
union_find_replacet symbol_resolve
std::vector< exprt > equations
string_refinementt(const infot &)
decision_proceduret::resultt dec_solve() override
Main decision procedure of the solver.
std::set< exprt > seen_instances
void set_to(const exprt &expr, bool value) override
Record the constraints to ensure that the expression is true when the boolean is true and false other...
string_dependenciest dependencies
index_set_pairt index_sets
exprt get(const exprt &expr) const override
Evaluates the given expression in the valuation found by string_refinementt::dec_solve.
std::vector< exprt > current_constraints
void add_lemma(const exprt &lemma, bool simplify_lemma=true)
Add the given lemma to the solver.
Structure type, corresponds to C style structs.
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
Generation of fresh symbols of a given type.
const typet & subtype() const
The type of an expression, extends irept.
Similar interface to union-find for expressions, with a function for replacing sub-expressions by the...
std::vector< std::pair< exprt, exprt > > to_vector() const
exprt make_union(const exprt &a, const exprt &b)
Merge the set containing a and the set containing b.
bool replace_expr(exprt &expr) const
Replace subexpressions of expr by the representative element of the set they belong to.
Operator to update elements in structs and arrays.
#define forall_operands(it, expr)
Forward depth-first search iterators These iterators' copy operations are expensive,...
bool has_subtype(const typet &type, const std::function< bool(const typet &)> &pred, const namespacet &ns)
returns true if any of the contained types satisfies pred
Deprecated expression utility functions.
const std::string & id2string(const irep_idt &d)
Magic numbers used throughout the codebase.
const std::size_t MAX_CONCRETE_STRING_SIZE
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
int solver(std::istream &in)
#define UNREACHABLE
This should be used to mark dead code.
#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...
bool can_cast_expr< equal_exprt >(const exprt &base)
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
#define CHARACTER_FOR_UNKNOWN
Module: String solver Author: Diffblue Ltd.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.
Defines related function for string constraints.
std::vector< exprt > instantiate_not_contains(const string_not_contains_constraintt &axiom, const std::set< std::pair< exprt, exprt > > &index_pairs, const std::unordered_map< string_not_contains_constraintt, symbol_exprt > &witnesses)
optionalt< exprt > add_node(string_dependenciest &dependencies, const exprt &expr, array_poolt &array_pool, symbol_generatort &fresh_symbol)
When a sub-expression of expr is a builtin_function, add a "string_builtin_function" node to the grap...
Keeps track of dependencies between strings.
array_string_exprt & to_array_string_expr(exprt &expr)
static void initial_index_set(index_set_pairt &index_set, const namespacet &ns, const string_constraintt &axiom)
static bool is_valid_string_constraint(messaget::mstreamt &stream, const namespacet &ns, const string_constraintt &constraint)
static std::string string_of_array(const array_exprt &arr)
convert the content of a string to a more readable representation.
static void update_index_set(index_set_pairt &index_set, const namespacet &ns, const std::vector< exprt > ¤t_constraints)
Add to the index set all the indices that appear in the formulas.
static optionalt< exprt > get_array(const std::function< exprt(const exprt &)> &super_get, const namespacet &ns, messaget::mstreamt &stream, const array_string_exprt &arr, const array_poolt &array_pool)
Get a model of an array and put it in a certain form.
static std::vector< exprt > extract_strings_from_lhs(const exprt &lhs, const namespacet &ns)
This is meant to be used on the lhs of an equation with string subtype.
exprt substitute_array_lists(exprt expr, size_t string_max_length)
Replace array-lists by 'with' expressions.
static std::vector< exprt > extract_strings(const exprt &expr, const namespacet &ns)
static std::pair< bool, std::vector< exprt > > check_axioms(const string_axiomst &axioms, string_constraint_generatort &generator, const std::function< exprt(const exprt &)> &get, messaget::mstreamt &stream, const namespacet &ns, bool use_counter_example, const union_find_replacet &symbol_resolve, const std::unordered_map< string_not_contains_constraintt, symbol_exprt > ¬_contain_witnesses)
Check axioms takes the model given by the underlying solver and answers whether it satisfies the stri...
static void add_equations_for_symbol_resolution(union_find_replacet &symbol_solver, const std::vector< exprt > &equations, const namespacet &ns, messaget::mstreamt &stream)
Add association for each char pointer in the equation.
static void make_char_array_pointer_associations(string_constraint_generatort &generator, exprt &expr)
If expr is an equation whose right-hand-side is a associate_array_to_pointer call,...
static void add_string_equation_to_symbol_resolution(const equal_exprt &eq, union_find_replacet &symbol_resolve, const namespacet &ns)
Given an equation on strings, mark these strings as belonging to the same set in the symbol_resolve s...
static bool validate(const string_refinementt::infot &info)
static void add_to_index_set(index_set_pairt &index_set, const namespacet &ns, const exprt &s, exprt i)
Add i to the index set all the indices that appear in the formula.
exprt simplify_sum(const exprt &f)
static optionalt< exprt > get_valid_array_size(const std::function< exprt(const exprt &)> &super_get, const namespacet &ns, messaget::mstreamt &stream, const array_string_exprt &arr, const array_poolt &array_pool)
Get a model of the size of the input string.
union_find_replacet string_identifiers_resolution_from_equations(const std::vector< equal_exprt > &equations, const namespacet &ns, messaget::mstreamt &stream)
Symbol resolution for expressions of type string typet.
static void display_index_set(messaget::mstreamt &stream, const index_set_pairt &index_set)
Write index set to the given stream, use for debugging.
static std::vector< T > fill_in_map_as_vector(const std::map< std::size_t, T > &index_value)
Convert index-value map to a vector of values.
static exprt negation_of_not_contains_constraint(const string_not_contains_constraintt &constraint, const symbol_exprt &univ_var, const std::function< exprt(const exprt &)> &get)
Negates the constraint to be fed to a solver.
static optionalt< exprt > find_counter_example(const namespacet &ns, const exprt &axiom, const symbol_exprt &var, message_handlert &message_handler)
Creates a solver with axiom as the only formula added and runs it.
static exprt replace_expr_copy(const union_find_replacet &symbol_resolve, exprt expr)
Substitute sub-expressions in equation by representative elements of symbol_resolve whenever possible...
static void substitute_array_access_in_place(exprt &expr, symbol_generatort &symbol_generator, const bool left_propagate)
Auxiliary function for substitute_array_access Performs the same operation but modifies the argument ...
static void get_sub_arrays(const exprt &array_expr, std::vector< exprt > &accu)
An expression representing an array of characters can be in the form of an if expression for instance...
void debug_model(const string_constraint_generatort &generator, messaget::mstreamt &stream, const namespacet &ns, const std::function< exprt(const exprt &)> &super_get, const std::vector< symbol_exprt > &symbols, array_poolt &array_pool)
Display part of the current model by mapping the variables created by the solver to constant expressi...
static std::vector< exprt > instantiate(const string_not_contains_constraintt &axiom, const index_set_pairt &index_set, const std::unordered_map< string_not_contains_constraintt, symbol_exprt > &witnesses)
Instantiates a quantified formula representing not_contains by substituting the quantifiers and gener...
static optionalt< exprt > substitute_array_access(const index_exprt &index_expr, symbol_generatort &symbol_generator, const bool left_propagate)
static void debug_check_axioms_step(messaget::mstreamt &stream, const T &axiom, const T &axiom_in_model, const exprt &negaxiom, const exprt &with_concretized_arrays)
Debugging function which outputs the different steps an axiom goes through to be checked in check axi...
static exprt get_char_array_and_concretize(const std::function< exprt(const exprt &)> &super_get, const namespacet &ns, messaget::mstreamt &stream, const array_string_exprt &arr, array_poolt &array_pool)
Debugging function which finds the valuation of the given array in super_get and concretize unknown c...
static std::vector< exprt > generate_instantiations(const index_set_pairt &index_set, const string_axiomst &axioms, const std::unordered_map< string_not_contains_constraintt, symbol_exprt > ¬_contain_witnesses)
Instantiation of all constraints.
String support via creating string constraints and progressively instantiating the universal constrai...
exprt substitute_array_access(exprt expr, symbol_generatort &symbol_generator, const bool left_propagate)
Create an equivalent expression where array accesses and 'with' expressions are replaced by 'if' expr...
union_find_replacet string_identifiers_resolution_from_equations(const std::vector< equal_exprt > &equations, const namespacet &ns, messaget::mstreamt &stream)
Symbol resolution for expressions of type string typet.
#define string_refinement_invariantt(reason)
std::string utf16_constant_array_to_java(const array_exprt &arr, std::size_t length)
Construct a string from a constant array.
bool is_char_type(const typet &type)
For now, any unsigned bitvector type of width smaller or equal to 16 is considered a character.
bool has_char_pointer_subtype(const typet &type, const namespacet &ns)
bool is_char_array_type(const typet &type, const namespacet &ns)
Distinguish char array from other types.
bool is_char_pointer_type(const typet &type)
For now, any unsigned bitvector type is considered a character.
std::map< exprt, std::set< exprt > > current
std::vector< string_constraintt > universal
std::vector< string_not_contains_constraintt > not_contains
Collection of constraints of different types: existential formulas, universal formulas,...
std::vector< string_not_contains_constraintt > not_contains
std::vector< exprt > existential
std::vector< string_constraintt > universal
Constraints to encode non containement of strings.
string_refinementt constructor arguments