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>
74 ¬_contain_witnesses);
96 const std::vector<exprt> ¤t_constraints);
101 const exprt &formula);
106 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
110 const std::function<
exprt(
const exprt &)> &super_get,
119 const bool left_propagate);
132 std::vector<T> result;
133 if(!index_value.empty())
135 result.resize(index_value.rbegin()->first + 1);
136 for(
auto it = index_value.rbegin(); it != index_value.rend(); ++it)
138 const std::size_t index = it->first;
139 const T &value = it->second;
140 const auto next = std::next(it);
141 const std::size_t leftmost_index_to_pad =
142 next != index_value.rend() ? next->first + 1 : 0;
143 for(std::size_t j = leftmost_index_to_pad; j <= index; j++)
174 std::size_t count = 0;
175 std::size_t count_current = 0;
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())
195 stream << count <<
" elements in index set (" << count_current
223 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
224 ¬_contain_witnesses)
226 std::vector<exprt> lemmas;
227 for(
const auto &i : index_set.
current)
229 for(
const auto &univ_axiom : axioms.
universal)
231 for(
const auto &j : i.second)
232 lemmas.push_back(
instantiate(univ_axiom, i.first, j));
237 for(
const auto &instance :
238 instantiate(nc_axiom, index_set, not_contain_witnesses))
239 lemmas.push_back(instance);
257 const auto new_equation =
302 const std::vector<exprt> &equations,
306 const std::string log_message =
307 "WARNING string_refinement.cpp generate_symbol_resolution_from_equations:";
308 auto equalities =
make_range(equations).filter(
310 for(
const exprt &e : equalities)
315 if(lhs.
id() != ID_symbol)
317 stream << log_message <<
"non symbol lhs: " <<
format(lhs)
324 stream << log_message <<
"non equal types lhs: " <<
format(lhs)
325 <<
"\n####################### rhs: " <<
format(rhs)
334 else if(rhs.
id() == ID_function_application)
342 if(rhs.
type().
id() == ID_struct || rhs.
type().
id() == ID_struct_tag)
345 rhs.
type().
id() == ID_struct_tag
348 for(
const auto &comp : struct_type.
components())
361 stream << log_message <<
"non struct with char pointer subexpr "
375static std::vector<exprt>
378 std::vector<exprt> result;
380 result.push_back(lhs);
381 else if(lhs.
type().
id() == ID_struct || lhs.
type().
id() == ID_struct_tag)
384 lhs.
type().
id() == ID_struct_tag
387 for(
const auto &comp : struct_type.
components())
392 result.end(), strings_in_comp.begin(), strings_in_comp.end());
403static std::vector<exprt>
406 std::vector<exprt> result;
411 result.push_back(*it);
412 it.next_sibling_or_parent();
414 else if(it->id() == ID_symbol)
418 it.next_sibling_or_parent();
451 for(
const auto &comp : struct_type.
components())
457 equal_exprt(lhs_data, rhs_data), symbol_resolve, ns);
471 const std::vector<equal_exprt> &equations,
475 const std::string log_message =
476 "WARNING string_refinement.cpp "
477 "string_identifiers_resolution_from_equations:";
482 std::unordered_set<size_t> required_equations;
483 std::stack<size_t> equations_to_treat;
485 for(std::size_t i = 0; i < equations.size(); ++i)
488 if(eq.
rhs().
id() == ID_function_application)
490 if(required_equations.insert(i).second)
491 equations_to_treat.push(i);
494 for(
const auto &expr : rhs_strings)
495 equation_map.
add(i, expr);
503 for(
const auto &expr : lhs_strings)
504 equation_map.
add(i, expr);
506 if(lhs_strings.empty())
508 stream << log_message <<
"non struct with string subtype "
514 equation_map.
add(i, expr);
519 while(!equations_to_treat.empty())
521 const std::size_t i = equations_to_treat.top();
522 equations_to_treat.pop();
527 if(required_equations.insert(j).second)
528 equations_to_treat.push(j);
534 for(
const std::size_t i : required_equations)
543output_equations(std::ostream &output,
const std::vector<exprt> &equations)
545 for(std::size_t i = 0; i < equations.size(); ++i)
546 output <<
" [" << i <<
"] " <<
format(equations[i]) << std::endl;
622 log.debug() <<
"dec_solve: Build symbol solver from equations"
638 std::vector<equal_exprt> equalities;
642 equalities.push_back(*equal_expr);
650 for(
const auto &pair : string_id_symbol_resolve.
to_vector())
657 log.debug() <<
"dec_solve: Replacing string ids and simplifying arguments"
658 " in function applications"
662 auto it = expr.depth_begin();
663 while(it != expr.depth_end())
673 it.next_sibling_or_parent();
689 log.debug() <<
"dec_solve: compute dependency graph and remove function "
690 <<
"applications captured by the dependencies:" <<
messaget::eom;
691 std::vector<exprt> local_equations;
696 const exprt eq_with_char_array_replaced_with_representative_elements =
698 const std::optional<exprt> new_equation =
add_node(
700 eq_with_char_array_replaced_with_representative_elements,
704 local_equations.push_back(*new_equation);
706 local_equations.push_back(eq);
725 for(
auto pair :
generator.array_pool.get_arrays_of_pointers())
727 log.debug() <<
" * " <<
format(pair.first) <<
"\t--> "
728 <<
format(pair.second) <<
" : " <<
format(pair.second.type())
733 for(
const auto &eq : local_equations)
744 std::back_inserter(
axioms.universal),
746 constraint.replace_expr(symbol_resolve);
748 is_valid_string_constraint(log.error(), ns, constraint),
749 string_refinement_invariantt(
750 "string constraints satisfy their invariant"));
757 std::back_inserter(
axioms.not_contains),
759 replace(symbol_resolve, axiom);
764 std::unordered_map<string_not_contains_constraintt, symbol_exprt>
765 not_contain_witnesses;
766 for(
const auto &nc_axiom :
axioms.not_contains)
768 const auto &witness_type = [&] {
770 const typet &index_type = rtype.size().type();
773 not_contain_witnesses.emplace(
774 nc_axiom,
generator.fresh_symbol(
"not_contains_witness", witness_type));
783 for(
const auto &pair :
generator.array_pool.created_strings())
785 exprt length =
generator.array_pool.get_or_create_length(pair.first);
791 const auto get = [
this](
const exprt &expr) {
return this->
get(expr); };
798 std::vector<exprt> counter_examples;
807 not_contain_witnesses);
813 log.debug() <<
"check_SAT: got SAT but the model is not correct"
819 return initial_result;
825 const auto initial_instances =
827 for(
const auto &instance : initial_instances)
841 std::vector<exprt> counter_examples;
850 not_contain_witnesses);
858 <<
"check_SAT: got SAT but the model is not correct, refining..."
872 if(
axioms.not_contains.empty())
874 log.error() <<
"dec_solve: current index set is empty, "
880 log.debug() <<
"dec_solve: current index set is empty, "
882 for(
const auto &counter : counter_examples)
887 const auto instances =
889 for(
const auto &instance : instances)
895 log.debug() <<
"check_SAT: default return "
897 return refined_result;
900 log.debug() <<
"string_refinementt::dec_solve reached the maximum number"
910 const bool simplify_lemma)
917 exprt simple_lemma = lemma;
926 log.debug() <<
"string_refinementt::add_lemma : tautology" <<
messaget::eom;
937 if(it->id() == ID_array && it->operands().empty())
943 it.next_sibling_or_parent();
969 const std::function<
exprt(
const exprt &)> &super_get,
977 if(size_from_pool.has_value())
979 const exprt size = size_from_pool.value();
983 stream <<
"(sr::get_valid_array_size) string of unknown size: "
996 stream <<
"(sr::get_valid_array_size) size is not valid" <<
messaget::eom;
1013 const std::function<
exprt(
const exprt &)> &super_get,
1021 if(!size.has_value())
1030 stream <<
"(sr::get_valid_array_size) long string (size "
1032 stream <<
"(sr::get_valid_array_size) consider reducing "
1033 "max-nondet-string-length so "
1034 "that no string exceeds "
1036 <<
" in length and "
1037 "make sure all functions returning strings are loaded"
1039 stream <<
"(sr::get_valid_array_size) this can also happen on invalid "
1047 const typet &index_type = size.value().type();
1052 return array->concretize(n, index_type);
1062 if(arr.
type().
id() != ID_array)
1063 return std::string(
"");
1079 const std::function<
exprt(
const exprt &)> &super_get,
1085 stream <<
"- " <<
format(arr) <<
":\n";
1086 stream << std::string(4,
' ') <<
"- type: " <<
format(arr.
type())
1088 const auto arr_model_opt =
get_array(super_get, ns, stream, arr, array_pool);
1091 stream << std::string(4,
' ') <<
"- char_array: " <<
format(*arr_model_opt)
1093 stream << std::string(4,
' ')
1096 stream << std::string(4,
' ')
1099 const auto concretized_array =
get_array(
1102 stream << std::string(4,
' ')
1103 <<
"- concretized_char_array: " <<
format(*concretized_array)
1107 const auto array_expr =
1110 stream << std::string(4,
' ') <<
"- as_string: \""
1114 stream << std::string(2,
' ') <<
"- warning: not an array"
1116 return *concretized_array;
1120 stream << std::string(4,
' ') <<
"- incomplete model" <<
messaget::eom;
1130 const std::function<
exprt(
const exprt &)> &super_get,
1131 const std::vector<symbol_exprt> &symbols,
1134 stream <<
"debug_model:" <<
'\n';
1137 const auto arr = pointer_array.second;
1141 stream <<
"- " <<
format(arr) <<
":\n"
1142 <<
" - pointer: " <<
format(pointer_array.first) <<
"\n"
1146 for(
const auto &symbol : symbols)
1148 stream <<
" - " << symbol.get_identifier() <<
": "
1149 <<
format(super_get(symbol)) <<
'\n';
1169 const bool left_propagate)
1187 const exprt default_val = symbol_generator(
"out_of_bound_access",
char_type);
1196 const bool left_propagate)
1202 std::optional<exprt> substituted_true_case =
1204 std::optional<exprt> substituted_false_case =
1209 substituted_true_case ? *substituted_true_case : true_index,
1210 substituted_false_case ? *substituted_false_case : false_index);
1216 const bool left_propagate)
1220 return array_of->op();
1223 *array_with, index_expr.
index(), left_propagate);
1226 *array_expr, index_expr.
index(), symbol_generator);
1229 *if_expr, index_expr.
index(), symbol_generator, left_propagate);
1232 array.
is_nil() || array.
id() == ID_symbol || array.
id() == ID_nondet_symbol,
1234 "in case the array is unknown, it should be a symbol or nil, id: ") +
1245 const bool left_propagate)
1252 std::optional<exprt> result =
1257 it.mutate() = *result;
1284 const bool left_propagate)
1303 const std::function<
exprt(
const exprt &)> &get)
1322 std::vector<exprt> conjuncts;
1327 const exprt s0_char =
1330 conjuncts.push_back(
equal_exprt(s0_char, s1_char));
1340template <
typename T>
1344 const T &axiom_in_model,
1345 const exprt &negaxiom,
1346 const exprt &with_concretized_arrays)
1348 stream << std::string(4,
' ') <<
"- axiom:\n" << std::string(6,
' ');
1351 << std::string(4,
' ') <<
"- axiom_in_model:\n"
1352 << std::string(6,
' ');
1353 stream <<
to_string(axiom_in_model) <<
'\n'
1354 << std::string(4,
' ') <<
"- negated_axiom:\n"
1355 << std::string(6,
' ') <<
format(negaxiom) <<
'\n';
1356 stream << std::string(4,
' ') <<
"- negated_axiom_with_concretized_arrays:\n"
1357 << std::string(6,
' ') <<
format(with_concretized_arrays) <<
'\n';
1364 const std::function<
exprt(
const exprt &)> &get,
1367 bool use_counter_example,
1369 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
1370 ¬_contain_witnesses)
1372 stream <<
"string_refinementt::check_axioms:" <<
messaget::eom;
1375 auto pairs = symbol_resolve.
to_vector();
1376 for(
const auto &pair : pairs)
1377 stream <<
" - " <<
format(pair.first) <<
" --> " <<
format(pair.second)
1391 std::map<size_t, exprt> violated;
1393 stream <<
"string_refinement::check_axioms: " << axioms.
universal.size()
1395 for(
size_t i = 0; i < axioms.
universal.size(); i++)
1408 stream << std::string(2,
' ') << i <<
".\n";
1409 const exprt with_concretized_arrays =
1412 stream, axiom, axiom_in_model, negaxiom, with_concretized_arrays);
1417 with_concretized_arrays,
1421 stream << std::string(4,
' ')
1424 violated[i] = *witness;
1427 stream << std::string(4,
' ') <<
"- correct" <<
messaget::eom;
1431 std::map<std::size_t, exprt> violated_not_contains;
1433 stream <<
"there are " << axioms.
not_contains.size() <<
" not_contains axioms"
1435 for(std::size_t i = 0; i < axioms.
not_contains.size(); i++)
1441 nc_axiom, univ_var, [&](
const exprt &expr) {
1445 stream << std::string(2,
' ') << i <<
".\n";
1447 stream, nc_axiom, nc_axiom, negated_axiom, negated_axiom);
1453 stream << std::string(4,
' ')
1456 violated_not_contains[i] = *witness;
1460 if(violated.empty() && violated_not_contains.empty())
1463 return {
true, std::vector<exprt>()};
1467 stream << violated.size() <<
" universal string axioms can be violated"
1469 stream << violated_not_contains.size()
1470 <<
" not_contains string axioms can be violated" <<
messaget::eom;
1472 if(use_counter_example)
1474 std::vector<exprt> lemmas;
1476 for(
const auto &v : violated)
1478 const exprt &val = v.second;
1489 lemmas.push_back(counter);
1492 for(
const auto &v : violated_not_contains)
1494 const exprt &val = v.second;
1498 const exprt func_val =
1499 index_exprt(not_contain_witnesses.at(axiom), val);
1502 std::set<std::pair<exprt, exprt>> indices;
1503 indices.insert(std::pair<exprt, exprt>(comp_val, func_val));
1504 const exprt counter =
1506 lemmas.push_back(counter);
1508 return {
false, lemmas};
1511 return {
false, std::vector<exprt>()};
1531 for(
const auto &axiom : axioms.
universal)
1544 const std::vector<exprt> ¤t_constraints)
1546 for(
const auto &axiom : current_constraints)
1558 if(array_expr.
id() == ID_if)
1565 if(array_expr.
type().
id() == ID_array)
1568 accu.push_back(array_expr);
1572 for(
const auto &operand : array_expr.
operands())
1593 std::vector<exprt> sub_arrays;
1595 for(
const auto &sub : sub_arrays)
1596 if(index_set.
cumulative[sub].insert(i).second)
1597 index_set.
current[sub].insert(i);
1620 const exprt &upper_bound,
1625 s.
id() == ID_symbol || s.
id() == ID_nondet_symbol || s.
id() == ID_array ||
1627 if(s.
id() == ID_array)
1629 for(std::size_t j = 0; j < s.
operands().size(); ++j)
1659 const auto &s = index_expr.array();
1661 it.next_sibling_or_parent();
1685 it.next_sibling_or_parent();
1703 const exprt &formula)
1705 std::list<exprt> to_process;
1706 to_process.push_back(formula);
1708 while(!to_process.empty())
1710 exprt cur = to_process.back();
1711 to_process.pop_back();
1717 s.
type().
id() == ID_array,
1720 if(s.
id() != ID_array)
1725 for(
const auto &op :
as_const(cur).operands())
1726 to_process.push_back(op);
1752 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
1759 const auto &index_set1 = index_set.
cumulative.find(
s1.content());
1760 const auto ¤t_index_set0 = index_set.
current.find(s0.
content());
1761 const auto ¤t_index_set1 = index_set.
current.find(
s1.content());
1766 current_index_set0 != index_set.
current.end() &&
1767 current_index_set1 != index_set.
current.end())
1769 typedef std::pair<exprt, exprt> expr_pairt;
1770 std::set<expr_pairt> index_pairs;
1772 for(
const auto &ic0 : current_index_set0->second)
1773 for(
const auto &i1 : index_set1->second)
1774 index_pairs.insert(expr_pairt(ic0, i1));
1775 for(
const auto &ic1 : current_index_set1->second)
1776 for(
const auto &i0 : index_set0->second)
1777 index_pairs.insert(expr_pairt(i0, ic1));
1779 return ::instantiate_not_contains(axiom, index_pairs, witnesses);
1793 for(
auto &operand : expr.
operands())
1796 if(expr.
id() == ID_array_list)
1806 for(
size_t i = 0; i < expr.
operands().size(); i += 2)
1813 (index_value && *index_value < string_max_length))
1814 ret_expr =
with_exprt(ret_expr, index, value);
1831 const auto super_get = [
this](
const exprt &expr) {
1841 std::reference_wrapper<const exprt> current(index_expr->array());
1842 while(current.get().id() == ID_if)
1845 const exprt cond =
get(if_expr.cond());
1847 current = std::cref(if_expr.true_case());
1849 current = std::cref(if_expr.false_case());
1854 const auto index =
get(index_expr->index());
1861 const exprt unknown =
1867 return sparse_array->at(*index_value);
1868 return sparse_array->to_if_expression(index);
1871 INVARIANT(array.id() == ID_symbol || array.id() == ID_nondet_symbol,
1872 "Apart from symbols, array valuations can be interpreted as "
1873 "sparse arrays. Array model : " + array.pretty());
1882 const auto from_dependencies =
1884 return *from_dependencies;
1887 const auto arr_model_opt =
1889 return *arr_model_opt;
1892 const auto &length_from_pool =
1893 generator.array_pool.get_length_if_exists(arr))
1895 const exprt length = super_get(length_from_pool.value());
1924 satcheck_no_simplifiert sat_check(message_handler);
1945 [&](
const exprt &expr)
1947 const auto index_expr = expr_try_dynamic_cast<const index_exprt>(expr);
1949 indices[index_expr->array()].push_back(index_expr->index());
1966 it->id() != ID_plus && it->id() != ID_minus &&
1967 it->id() != ID_unary_minus && *it != var)
1969 if(std::find(it->depth_begin(), it->depth_end(), var) != it->depth_end())
1972 it.next_sibling_or_parent();
1993 if(it->id() == ID_index)
1994 it.next_sibling_or_parent();
2015 for(
const auto &pair : body_indices)
2018 const exprt rep = pair.second.back();
2019 for(
size_t j = 0; j < pair.second.size() - 1; j++)
2021 const exprt i = pair.second[j];
2026 stream <<
"Indices not equal: " <<
to_string(constraint)
2035 stream <<
"f is not linear: " <<
to_string(constraint)
2044 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 char_type()
Array constructor from list of elements.
const array_typet & type() const
Array constructor from single element.
Correspondance between arrays and pointers string representations.
std::optional< 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< exprt, array_string_exprt, irep_hash > & get_arrays_of_pointers() const
const typet & length_type() const
const exprt & size() const
const typet & element_type() const
The type of the elements of the array.
message_handlert & message_handler
A base class for relations, i.e., binary predicates whose two operands have the same type.
decision_proceduret::resultt dec_solve(const exprt &) override
Implementation of the decision procedure.
A constant literal expression.
virtual exprt get(const exprt &) const =0
Return expr with variables replaced by values from satisfying assignment if available.
resultt
Result of running the decision procedure.
virtual void set_to(const exprt &, 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...
void add(const std::size_t i, const exprt &expr)
Record the fact that equation i contains expression expr
std::vector< std::size_t > find_equations(const exprt &expr)
std::vector< exprt > find_expressions(const std::size_t i)
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 std::optional< 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,...
array_exprt concretize(std::size_t size, const typet &index_type) const
Convert to an array representation, ignores elements at index >= size.
const irep_idt & id() const
Canonical representation of linear function, for instance, expression $x + x - y + 5 - 3$ would given...
exprt to_expr(bool negated=false) const
Extract member of struct or union.
message_handlert & get_message_handler()
const union_typet & follow_tag(const union_tag_typet &) const
Follow type tag of union type.
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.
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.
std::optional< 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.
exprt univ_within_bounds() const
string_constraintt(const symbol_exprt &_univ_var, const exprt &lower_bound, const exprt &upper_bound, const exprt &body, message_handlert &message_handler)
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
string_constraint_generatort generator
union_find_replacet symbol_resolve
std::vector< exprt > equations
decision_proceduret::resultt dec_solve(const exprt &) override
Main decision procedure of the solver.
string_refinementt(const infot &)
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.
const componentst & components() const
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.
void equality_propagation(std::vector< exprt > &constraints)
bool can_cast_expr(const exprt &base)
Check whether a reference to a generic exprt is of a specific derived class.
auto expr_try_dynamic_cast(TExpr &base) -> typename detail::expr_try_dynamic_cast_return_typet< T, TExpr >::type
Try to cast a reference to a generic exprt to a specific derived class.
auto expr_dynamic_cast(TExpr &base) -> typename detail::expr_dynamic_cast_return_typet< T, TExpr >::type
Cast a reference to a generic exprt to a specific derived class.
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(exprt a, exprt b)
Conjunction of two expressions.
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 struct_tag_typet & to_struct_tag_type(const typet &type)
Cast a typet to a struct_tag_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)
std::optional< 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 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::optional< exprt > substitute_array_access(const index_exprt &index_expr, symbol_generatort &symbol_generator, const bool left_propagate)
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 std::optional< 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.
static std::optional< 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.
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 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 std::optional< 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 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::map< exprt, std::set< exprt > > cumulative
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