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),
161 generator(*
info.ns, *
info.message_handler)
174 std::size_t count = 0;
176 for(
const auto &i :
index_set.cumulative)
178 const exprt &s = i.first;
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)
302 const std::vector<exprt> &equations,
307 "WARNING string_refinement.cpp generate_symbol_resolution_from_equations:";
308 auto equalities =
make_range(equations).filter(
310 for(
const exprt &e : equalities)
325 <<
"\n####################### rhs: " <<
format(rhs)
372static std::vector<exprt>
375 std::vector<exprt> result;
377 result.push_back(lhs);
397static std::vector<exprt>
400 std::vector<exprt> result;
405 result.push_back(*it);
406 it.next_sibling_or_parent();
412 it.next_sibling_or_parent();
463 const std::vector<equal_exprt> &equations,
468 "WARNING string_refinement.cpp "
469 "string_identifiers_resolution_from_equations:";
477 for(std::size_t i = 0; i < equations.size(); ++i)
501 <<
format(
eq.lhs()) <<
"\n * of type "
517 for(
const std::size_t j :
equation_map.find_equations(
string))
537 for(std::size_t i = 0; i < equations.size(); ++i)
538 output <<
" [" << i <<
"] " <<
format(equations[i]) << std::endl;
613 log.
debug() <<
"dec_solve: Build symbol solver from equations"
629 std::vector<equal_exprt> equalities;
648 log.
debug() <<
"dec_solve: Replacing string ids and simplifying arguments"
649 " in function applications"
653 auto it = expr.depth_begin();
654 while(it != expr.depth_end())
664 it.next_sibling_or_parent();
680 log.
debug() <<
"dec_solve: compute dependency graph and remove function "
681 <<
"applications captured by the dependencies:" <<
messaget::eom;
737 constraint.replace_expr(symbol_resolve);
739 is_valid_string_constraint(log.error(), ns, constraint),
740 string_refinement_invariantt(
741 "string constraints satisfy their invariant"));
750 replace(symbol_resolve, axiom);
755 std::unordered_map<string_not_contains_constraintt, symbol_exprt>
782 const auto get = [
this](
const exprt &expr) {
return this->
get(expr); };
803 log.
debug() <<
"check_SAT: got SAT but the model is not correct"
847 <<
"check_SAT: got SAT but the model is not correct, refining..."
863 log.
error() <<
"dec_solve: current index set is empty, "
869 log.
debug() <<
"dec_solve: current index set is empty, "
876 const auto instances =
878 for(
const auto &
instance : instances)
884 log.
debug() <<
"check_SAT: default return "
889 log.
debug() <<
"string_refinementt::dec_solve reached the maximum number"
926 if(it->id() ==
ID_array && it->operands().empty())
932 it.next_sibling_or_parent();
972 stream <<
"(sr::get_valid_array_size) string of unknown size: "
1010 if(!size.has_value())
1019 stream <<
"(sr::get_valid_array_size) long string (size "
1021 stream <<
"(sr::get_valid_array_size) consider reducing "
1022 "max-nondet-string-length so "
1023 "that no string exceeds "
1025 <<
" in length and "
1026 "make sure all functions returning strings are loaded"
1028 stream <<
"(sr::get_valid_array_size) this can also happen on invalid "
1052 return std::string(
"");
1082 stream << std::string(4,
' ')
1085 stream << std::string(4,
' ')
1091 stream << std::string(4,
' ')
1099 stream << std::string(4,
' ') <<
"- as_string: \""
1103 stream << std::string(2,
' ') <<
"- warning: not an array"
1120 const std::vector<symbol_exprt> &symbols,
1123 stream <<
"debug_model:" <<
'\n';
1135 for(
const auto &symbol : symbols)
1137 stream <<
" - " << symbol.get_identifier() <<
": "
1223 "in case the array is unknown, it should be a symbol or nil, id: ") +
1246 it.mutate() = *result;
1292 const std::function<
exprt(
const exprt &)> &get)
1329template <
typename T>
1337 stream << std::string(4,
' ') <<
"- axiom:\n" << std::string(6,
' ');
1340 << std::string(4,
' ') <<
"- axiom_in_model:\n"
1341 << std::string(6,
' ');
1343 << std::string(4,
' ') <<
"- negated_axiom:\n"
1345 stream << std::string(4,
' ') <<
"- negated_axiom_with_concretized_arrays:\n"
1353 const std::function<
exprt(
const exprt &)> &get,
1356 bool use_counter_example,
1358 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
1364 auto pairs = symbol_resolve.
to_vector();
1365 for(
const auto &
pair : pairs)
1382 stream <<
"string_refinement::check_axioms: " << axioms.
universal.size()
1384 for(
size_t i = 0; i < axioms.
universal.size(); i++)
1389 get(
axiom.lower_bound),
1390 get(
axiom.upper_bound),
1392 stream.message.get_message_handler());
1397 stream << std::string(2,
' ') << i <<
".\n";
1408 stream.message.get_message_handler()))
1410 stream << std::string(4,
' ')
1411 <<
"- violated_for: " <<
format(
axiom.univ_var) <<
"="
1424 for(std::size_t i = 0; i < axioms.
not_contains.size(); i++)
1428 "not_contains_univ_var",
nc_axiom.s0.length_type());
1434 stream << std::string(2,
' ') << i <<
".\n";
1442 stream << std::string(4,
' ')
1452 return {
true, std::vector<exprt>()};
1456 stream <<
violated.size() <<
" universal string axioms can be violated"
1459 <<
" not_contains string axioms can be violated" <<
messaget::eom;
1461 if(use_counter_example)
1463 std::vector<exprt>
lemmas;
1474 axiom.univ_within_bounds(),
1478 lemmas.push_back(counter);
1491 std::set<std::pair<exprt, exprt>> indices;
1493 const exprt counter =
1495 lemmas.push_back(counter);
1500 return {
false, std::vector<exprt>()};
1533 const std::vector<exprt> ¤t_constraints)
1535 for(
const auto &
axiom : current_constraints)
1585 if(
index_set.cumulative[sub].insert(i).second)
1609 const exprt &upper_bound,
1618 for(std::size_t j = 0; j < s.
operands().size(); ++j)
1641 auto it =
axiom.body.depth_begin();
1642 const auto end =
axiom.body.depth_end();
1650 it.next_sibling_or_parent();
1662 auto it =
axiom.premise.depth_begin();
1663 const auto end =
axiom.premise.depth_end();
1674 it.next_sibling_or_parent();
1714 for(
const auto &op :
as_const(cur).operands())
1741 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
1758 typedef std::pair<exprt, exprt> expr_pairt;
1795 for(
size_t i = 0; i < expr.
operands().size(); i += 2)
1830 std::reference_wrapper<const exprt> current(
index_expr->array());
1831 while(current.get().id() ==
ID_if)
1836 current = std::cref(
if_expr.true_case());
1838 current = std::cref(
if_expr.false_case());
1850 const exprt unknown =
1861 "Apart from symbols, array valuations can be interpreted as "
1862 "sparse arrays. Array model : " + array.pretty());
1934 [&](
const exprt &expr)
1936 const auto index_expr = expr_try_dynamic_cast<const index_exprt>(expr);
1938 indices[index_expr->array()].push_back(index_expr->index());
1958 if(std::find(it->depth_begin(), it->depth_end(), var) != it->depth_end())
1961 it.next_sibling_or_parent();
1978 for(
auto it =
constr.body.depth_begin(); it !=
constr.body.depth_end();)
1980 if(*it ==
constr.univ_var)
1983 it.next_sibling_or_parent();
2008 for(
size_t j = 0; j <
pair.second.size() - 1; j++)
2022 if(!is_linear_arithmetic_expr(rep, constraint.
univ_var))
2031 if(!universal_only_in_index(constraint))
2033 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_table_baset &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.
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()
bool is_boolean() const
Return whether the expression represents a Boolean.
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.
message_handlert & get_message_handler()
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, message_handlert &message_handler)
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.
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.
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)
void solver(std::vector< framet > &frames, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const solver_optionst &solver_options, const namespacet &ns, std::vector< propertyt > &properties, std::size_t property_index)
#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