Go to the documentation of this file.
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);
128 template <
typename T>
129 static std::vector<T>
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++)
160 loop_bound_(info.refinement_bound),
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);
251 if(
const auto equal_expr = expr_try_dynamic_cast<equal_exprt>(expr))
254 const auto fun_app = expr_try_dynamic_cast<function_application_exprt>(
257 const auto new_equation =
303 const std::vector<exprt> &equations,
307 const std::string log_message =
308 "WARNING string_refinement.cpp generate_symbol_resolution_from_equations:";
309 auto equalities =
make_range(equations).filter(
311 for(
const exprt &e : equalities)
316 if(lhs.
id() != ID_symbol)
318 stream << log_message <<
"non symbol lhs: " <<
format(lhs)
325 stream << log_message <<
"non equal types lhs: " <<
format(lhs)
326 <<
"\n####################### rhs: " <<
format(rhs)
335 else if(rhs.
id() == ID_function_application)
343 if(rhs.
type().
id() == ID_struct || rhs.
type().
id() == ID_struct_tag)
346 for(
const auto &comp : struct_type.
components())
359 stream << log_message <<
"non struct with char pointer subexpr "
373 static std::vector<exprt>
376 std::vector<exprt> result;
378 result.push_back(lhs);
379 else if(lhs.
type().
id() == ID_struct || lhs.
type().
id() == ID_struct_tag)
382 for(
const auto &comp : struct_type.
components())
387 result.end(), strings_in_comp.begin(), strings_in_comp.end());
398 static std::vector<exprt>
401 std::vector<exprt> result;
406 result.push_back(*it);
407 it.next_sibling_or_parent();
409 else if(it->id() == ID_symbol)
413 it.next_sibling_or_parent();
444 for(
const auto &comp : struct_type.
components())
450 equal_exprt(lhs_data, rhs_data), symbol_resolve, ns);
464 const std::vector<equal_exprt> &equations,
468 const std::string log_message =
469 "WARNING string_refinement.cpp "
470 "string_identifiers_resolution_from_equations:";
475 std::unordered_set<size_t> required_equations;
476 std::stack<size_t> equations_to_treat;
478 for(std::size_t i = 0; i < equations.size(); ++i)
481 if(eq.
rhs().
id() == ID_function_application)
483 if(required_equations.insert(i).second)
484 equations_to_treat.push(i);
487 for(
const auto &expr : rhs_strings)
488 equation_map.
add(i, expr);
496 for(
const auto &expr : lhs_strings)
497 equation_map.
add(i, expr);
499 if(lhs_strings.empty())
501 stream << log_message <<
"non struct with string subtype "
507 equation_map.
add(i, expr);
512 while(!equations_to_treat.empty())
514 const std::size_t i = equations_to_treat.top();
515 equations_to_treat.pop();
520 if(required_equations.insert(j).second)
521 equations_to_treat.push(j);
527 for(
const std::size_t i : required_equations)
536 output_equations(std::ostream &output,
const std::vector<exprt> &equations)
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;
633 if(
auto equal_expr = expr_try_dynamic_cast<equal_exprt>(eq))
634 equalities.push_back(*equal_expr);
642 for(
const auto &pair : string_id_symbol_resolve.
to_vector())
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;
683 std::vector<exprt> local_equations;
688 const exprt eq_with_char_array_replaced_with_representative_elements =
692 eq_with_char_array_replaced_with_representative_elements,
696 local_equations.push_back(*new_equation);
698 local_equations.push_back(eq);
718 <<
format(pair.second) <<
" : " <<
format(pair.second.type())
723 for(
const auto &eq : local_equations)
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>
755 not_contain_witnesses;
758 const auto &witness_type = [&] {
763 not_contain_witnesses.emplace(
781 const auto get = [
this](
const exprt &expr) {
return this->
get(expr); };
787 std::vector<exprt> counter_examples;
796 not_contain_witnesses);
802 log.
debug() <<
"check_SAT: got SAT but the model is not correct"
808 return initial_result;
814 const auto initial_instances =
816 for(
const auto &instance : initial_instances)
829 std::vector<exprt> counter_examples;
838 not_contain_witnesses);
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, "
870 for(
const auto &counter : counter_examples)
875 const auto instances =
877 for(
const auto &instance : instances)
883 log.
debug() <<
"check_SAT: default return "
885 return refined_result;
888 log.
debug() <<
"string_refinementt::dec_solve reached the maximum number"
898 const bool simplify_lemma)
905 exprt simple_lemma = lemma;
925 if(it->id() == ID_array && it->operands().empty())
930 it.next_sibling_or_parent();
956 const std::function<
exprt(
const exprt &)> &super_get,
964 if(size_from_pool.has_value())
966 const exprt size = size_from_pool.value();
968 if(size_val.
id() != ID_constant)
970 stream <<
"(sr::get_valid_array_size) string of unknown size: "
980 auto n_opt = numeric_cast<std::size_t>(size_val);
983 stream <<
"(sr::get_valid_array_size) size is not valid" <<
messaget::eom;
1000 const std::function<
exprt(
const exprt &)> &super_get,
1008 if(!size.has_value())
1013 const size_t n = numeric_cast<std::size_t>(size.value()).value();
1017 stream <<
"(sr::get_valid_array_size) long string (size "
1019 stream <<
"(sr::get_valid_array_size) consider reducing "
1020 "max-nondet-string-length so "
1021 "that no string exceeds "
1023 <<
" in length and "
1024 "make sure all functions returning strings are loaded"
1026 stream <<
"(sr::get_valid_array_size) this can also happen on invalid "
1049 if(arr.
type().
id() != ID_array)
1050 return std::string(
"");
1066 const std::function<
exprt(
const exprt &)> &super_get,
1072 stream <<
"- " <<
format(arr) <<
":\n";
1073 stream << std::string(4,
' ') <<
"- type: " <<
format(arr.
type())
1075 const auto arr_model_opt =
get_array(super_get, ns, stream, arr, array_pool);
1078 stream << std::string(4,
' ') <<
"- char_array: " <<
format(*arr_model_opt)
1080 stream << std::string(4,
' ')
1083 stream << std::string(4,
' ')
1086 const auto concretized_array =
get_array(
1089 stream << std::string(4,
' ')
1090 <<
"- concretized_char_array: " <<
format(*concretized_array)
1094 const auto array_expr =
1095 expr_try_dynamic_cast<array_exprt>(*concretized_array))
1097 stream << std::string(4,
' ') <<
"- as_string: \""
1101 stream << std::string(2,
' ') <<
"- warning: not an array"
1103 return *concretized_array;
1107 stream << std::string(4,
' ') <<
"- incomplete model" <<
messaget::eom;
1117 const std::function<
exprt(
const exprt &)> &super_get,
1118 const std::vector<symbol_exprt> &symbols,
1121 stream <<
"debug_model:" <<
'\n';
1124 const auto arr = pointer_array.second;
1128 stream <<
"- " <<
format(arr) <<
":\n"
1129 <<
" - pointer: " <<
format(pointer_array.first) <<
"\n"
1133 for(
const auto &symbol : symbols)
1135 stream <<
" - " << symbol.get_identifier() <<
": "
1136 <<
format(super_get(symbol)) <<
'\n';
1156 const bool left_propagate)
1174 const exprt default_val = symbol_generator(
"out_of_bound_access",
char_type);
1183 const bool left_propagate)
1196 substituted_true_case ? *substituted_true_case : true_index,
1197 substituted_false_case ? *substituted_false_case : false_index);
1203 const bool left_propagate)
1206 if(
auto array_of = expr_try_dynamic_cast<array_of_exprt>(array))
1207 return array_of->op();
1208 if(
auto array_with = expr_try_dynamic_cast<with_exprt>(array))
1210 *array_with, index_expr.
index(), left_propagate);
1211 if(
auto array_expr = expr_try_dynamic_cast<array_exprt>(array))
1213 *array_expr, index_expr.
index(), symbol_generator);
1214 if(
auto if_expr = expr_try_dynamic_cast<if_exprt>(array))
1216 *if_expr, index_expr.
index(), symbol_generator, left_propagate);
1219 array.
is_nil() || array.
id() == ID_symbol || array.
id() == ID_nondet_symbol,
1221 "in case the array is unknown, it should be a symbol or nil, id: ") +
1232 const bool left_propagate)
1237 if(
const auto index_expr = expr_try_dynamic_cast<index_exprt>(*it))
1244 it.mutate() = *result;
1271 const bool left_propagate)
1290 const std::function<
exprt(
const exprt &)> &get)
1293 const auto lbe = numeric_cast_v<mp_integer>(
1295 const auto ube = numeric_cast_v<mp_integer>(
1309 std::vector<exprt> conjuncts;
1310 conjuncts.reserve(numeric_cast_v<std::size_t>(ube - lbe));
1314 const exprt s0_char =
1317 conjuncts.push_back(
equal_exprt(s0_char, s1_char));
1327 template <
typename T>
1331 const T &axiom_in_model,
1332 const exprt &negaxiom,
1333 const exprt &with_concretized_arrays)
1335 stream << std::string(4,
' ') <<
"- axiom:\n" << std::string(6,
' ');
1338 << std::string(4,
' ') <<
"- axiom_in_model:\n"
1339 << std::string(6,
' ');
1340 stream <<
to_string(axiom_in_model) <<
'\n'
1341 << std::string(4,
' ') <<
"- negated_axiom:\n"
1342 << std::string(6,
' ') <<
format(negaxiom) <<
'\n';
1343 stream << std::string(4,
' ') <<
"- negated_axiom_with_concretized_arrays:\n"
1344 << std::string(6,
' ') <<
format(with_concretized_arrays) <<
'\n';
1351 const std::function<
exprt(
const exprt &)> &get,
1354 bool use_counter_example,
1356 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
1357 ¬_contain_witnesses)
1359 stream <<
"string_refinementt::check_axioms:" <<
messaget::eom;
1362 auto pairs = symbol_resolve.
to_vector();
1363 for(
const auto &pair : pairs)
1364 stream <<
" - " <<
format(pair.first) <<
" --> " <<
format(pair.second)
1378 std::map<size_t, exprt> violated;
1380 stream <<
"string_refinement::check_axioms: " << axioms.
universal.size()
1382 for(
size_t i = 0; i < axioms.
universal.size(); i++)
1394 stream << std::string(2,
' ') << i <<
".\n";
1395 const exprt with_concretized_arrays =
1398 stream, axiom, axiom_in_model, negaxiom, with_concretized_arrays);
1403 with_concretized_arrays,
1407 stream << std::string(4,
' ')
1410 violated[i] = *witness;
1413 stream << std::string(4,
' ') <<
"- correct" <<
messaget::eom;
1417 std::map<std::size_t, exprt> violated_not_contains;
1419 stream <<
"there are " << axioms.
not_contains.size() <<
" not_contains axioms"
1421 for(std::size_t i = 0; i < axioms.
not_contains.size(); i++)
1427 nc_axiom, univ_var, [&](
const exprt &expr) {
1431 stream << std::string(2,
' ') << i <<
".\n";
1433 stream, nc_axiom, nc_axiom, negated_axiom, negated_axiom);
1439 stream << std::string(4,
' ')
1442 violated_not_contains[i] = *witness;
1446 if(violated.empty() && violated_not_contains.empty())
1449 return {
true, std::vector<exprt>()};
1453 stream << violated.size() <<
" universal string axioms can be violated"
1455 stream << violated_not_contains.size()
1456 <<
" not_contains string axioms can be violated" <<
messaget::eom;
1458 if(use_counter_example)
1460 std::vector<exprt> lemmas;
1462 for(
const auto &v : violated)
1464 const exprt &val = v.second;
1475 lemmas.push_back(counter);
1478 for(
const auto &v : violated_not_contains)
1480 const exprt &val = v.second;
1484 const exprt func_val =
1485 index_exprt(not_contain_witnesses.at(axiom), val);
1488 std::set<std::pair<exprt, exprt>> indices;
1489 indices.insert(std::pair<exprt, exprt>(comp_val, func_val));
1490 const exprt counter =
1492 lemmas.push_back(counter);
1494 return {
false, lemmas};
1497 return {
false, std::vector<exprt>()};
1517 for(
const auto &axiom : axioms.
universal)
1530 const std::vector<exprt> ¤t_constraints)
1532 for(
const auto &axiom : current_constraints)
1544 if(array_expr.
id() == ID_if)
1551 if(array_expr.
type().
id() == ID_array)
1554 accu.push_back(array_expr);
1558 for(
const auto &operand : array_expr.
operands())
1576 const bool is_size_t = numeric_cast<std::size_t>(i).has_value();
1577 if(i.
id() != ID_constant || is_size_t)
1579 std::vector<exprt> sub_arrays;
1581 for(
const auto &sub : sub_arrays)
1582 if(index_set.
cumulative[sub].insert(i).second)
1583 index_set.
current[sub].insert(i);
1606 const exprt &upper_bound,
1611 s.
id() == ID_symbol || s.
id() == ID_nondet_symbol || s.
id() == ID_array ||
1613 if(s.
id() == ID_array)
1615 for(std::size_t j = 0; j < s.
operands().size(); ++j)
1619 if(
auto ite = expr_try_dynamic_cast<if_exprt>(s))
1645 const auto &s = index_expr.array();
1647 it.next_sibling_or_parent();
1671 it.next_sibling_or_parent();
1689 const exprt &formula)
1691 std::list<exprt> to_process;
1692 to_process.push_back(formula);
1694 while(!to_process.empty())
1696 exprt cur = to_process.back();
1697 to_process.pop_back();
1703 s.
type().
id() == ID_array,
1706 if(s.
id() != ID_array)
1712 to_process.push_back(*it);
1738 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
1745 const auto &index_set1 = index_set.
cumulative.find(
s1.content());
1746 const auto ¤t_index_set0 = index_set.
current.find(s0.
content());
1747 const auto ¤t_index_set1 = index_set.
current.find(
s1.content());
1752 current_index_set0 != index_set.
current.end() &&
1753 current_index_set1 != index_set.
current.end())
1755 typedef std::pair<exprt, exprt> expr_pairt;
1756 std::set<expr_pairt> index_pairs;
1758 for(
const auto &ic0 : current_index_set0->second)
1759 for(
const auto &i1 : index_set1->second)
1760 index_pairs.insert(expr_pairt(ic0, i1));
1761 for(
const auto &ic1 : current_index_set1->second)
1762 for(
const auto &i0 : index_set0->second)
1763 index_pairs.insert(expr_pairt(i0, ic1));
1779 for(
auto &operand : expr.
operands())
1782 if(expr.
id() == ID_array_list)
1792 for(
size_t i = 0; i < expr.
operands().size(); i += 2)
1796 const auto index_value = numeric_cast<std::size_t>(index);
1799 (index_value && *index_value < string_max_length))
1800 ret_expr =
with_exprt(ret_expr, index, value);
1817 const auto super_get = [
this](
const exprt &expr) {
1824 const auto &index_expr = expr_try_dynamic_cast<index_exprt>(ecopy);
1827 std::reference_wrapper<const exprt> current(index_expr->array());
1828 while(current.get().id() == ID_if)
1830 const auto &if_expr = expr_dynamic_cast<if_exprt>(current.get());
1831 const exprt cond =
get(if_expr.cond());
1833 current = std::cref(if_expr.true_case());
1835 current = std::cref(if_expr.false_case());
1840 const auto index =
get(index_expr->index());
1847 const exprt unknown =
1852 if(
const auto index_value = numeric_cast<std::size_t>(index))
1853 return sparse_array->at(*index_value);
1854 return sparse_array->to_if_expression(index);
1857 INVARIANT(array.id() == ID_symbol || array.id() == ID_nondet_symbol,
1858 "Apart from symbols, array valuations can be interpreted as "
1859 "sparse arrays. Array model : " + array.pretty());
1868 const auto from_dependencies =
1870 return *from_dependencies;
1873 const auto arr_model_opt =
1875 return *arr_model_opt;
1878 const auto &length_from_pool =
1881 const exprt length = super_get(length_from_pool.value());
1883 if(
const auto n = numeric_cast<std::size_t>(length))
1910 satcheck_no_simplifiert sat_check(message_handler);
1931 [&](
const exprt &expr)
1933 const auto index_expr = expr_try_dynamic_cast<const index_exprt>(expr);
1935 indices[index_expr->array()].push_back(index_expr->index());
1952 it->id() != ID_plus && it->id() != ID_minus &&
1953 it->id() != ID_unary_minus && *it != var)
1955 if(std::find(it->depth_begin(), it->depth_end(), var) != it->depth_end())
1958 it.next_sibling_or_parent();
1979 if(it->id() == ID_index)
1980 it.next_sibling_or_parent();
2001 for(
const auto &pair : body_indices)
2004 const exprt rep = pair.second.back();
2005 for(
size_t j = 0; j < pair.second.size() - 1; j++)
2007 const exprt i = pair.second[j];
2012 stream <<
"Indices not equal: " <<
to_string(constraint)
2021 stream <<
"f is not linear: " <<
to_string(constraint)
2030 stream <<
"Universal variable outside of index:" <<
to_string(constraint)
Operator to update elements in structs and arrays.
std::vector< string_constraintt > universal
#define UNREACHABLE
This should be used to mark dead code.
const componentst & components() const
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.
bool equality_propagation
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...
string_constraint_generatort generator
const typet & length_type() const
const typet & subtype() const
const std::unordered_map< exprt, array_string_exprt, irep_hash > & get_arrays_of_pointers() const
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
std::vector< std::pair< exprt, exprt > > to_vector() const
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 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.
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
depth_iteratort depth_begin()
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)
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.
The type of an expression, extends irept.
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 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 abstract_object_pointert transform(const exprt &expr, const std::vector< abstract_object_pointert > &operands, const abstract_environmentt &environment, const namespacet &ns)
static void display_index_set(messaget::mstreamt &stream, const index_set_pairt &index_set)
Write index set to the given stream, use for debugging.
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.
Correspondance between arrays and pointers string representations.
void set_to(const exprt &expr, bool value) override
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
std::vector< exprt > current_constraints
The trinary if-then-else operator.
bool is_char_type(const typet &type)
For now, any unsigned bitvector type of width smaller or equal to 16 is considered a character.
Represents arrays by the indexes up to which the value remains the same.
symbol_generatort fresh_symbol
exprt to_if_expression(const exprt &index) const
bool replace_expr(exprt &expr) const
Replace subexpressions of expr by the representative element of the set they belong to.
exprt get_or_create_length(const array_string_exprt &s)
Get the length of an array_string_exprt from the array_pool.
const std::size_t MAX_CONCRETE_STRING_SIZE
The plus expression Associativity is not specified.
Base class for all expressions.
void l_set_to_true(literalt a)
Collection of constraints of different types: existential formulas, universal formulas,...
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,...
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...
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Canonical representation of linear function, for instance, expression $x + x - y + 5 - 3$ would given...
bool is_true() const
Return whether the expression is a constant representing true.
index_set_pairt index_sets
Expression to hold a symbol (variable)
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,...
bitvector_typet index_type()
Keeps track of dependencies between strings.
Magic numbers used throughout the codebase.
std::string utf16_constant_array_to_java(const array_exprt &arr, std::size_t length)
Construct a string from a constant array.
bool can_cast_expr< equal_exprt >(const exprt &base)
An expression denoting infinity.
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.
bool is_false() const
Return whether the expression is a constant representing false.
static void initial_index_set(index_set_pairt &index_set, const namespacet &ns, const string_constraintt &axiom)
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.
std::map< exprt, std::vector< exprt > > array_index_mapt
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...
const exprt & size() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
typet & type()
Return the type of the expression.
const array_typet & type() const
Generation of fresh symbols of a given type.
static bool validate(const string_refinementt::infot &info)
bool is_char_pointer_type(const typet &type)
For now, any unsigned bitvector type is considered a character.
decision_proceduret::resultt dec_solve() override
Run the decision procedure to solve the problem.
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...
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
void clean_cache()
Clean the cache used by eval
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.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define CHARACTER_FOR_UNKNOWN
Module: String solver Author: Diffblue Ltd.
const std::string & id2string(const irep_idt &d)
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...
exprt substitute_array_lists(exprt expr, size_t string_max_length)
Replace array-lists by 'with' expressions.
#define forall_operands(it, expr)
static std::string string_of_array(const array_exprt &arr)
convert the content of a string to a more readable representation.
exprt get(const exprt &expr) const override
Evaluates the given expression in the valuation found by string_refinementt::dec_solve.
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...
#define PRECONDITION(CONDITION)
const irep_idt & get_identifier() const
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
void output_dot(std::ostream &stream) const
Array constructor from single element.
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 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 bool is_valid_string_constraint(messaget::mstreamt &stream, const namespacet &ns, const string_constraintt &constraint)
Checks the data invariant for string_constraintt.
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
bool is_char_array_type(const typet &type, const namespacet &ns)
Distinguish char array from other types.
const irep_idt & id() const
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 ...
Ranges: pair of begin and end iterators, which can be initialized from containers,...
void add(const std::size_t i, const exprt &expr)
Record the fact that equation i contains expression expr
String support via creating string constraints and progressively instantiating the universal constrai...
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.
Maps equation to expressions contained in them and conversely expressions to equations that contain t...
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.
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...
array_string_exprt & to_array_string_expr(exprt &expr)
optionalt< exprt > make_array_pointer_association(const exprt &return_code, const function_application_exprt &expr)
Associate array to pointer, and array to length.
nonstd::optional< T > optionalt
union_find_replacet symbol_resolve
literalt convert(const exprt &expr) override
Convert a Boolean expression and return the corresponding literal.
resultt
Result of running the decision procedure.
exprt make_union(const exprt &a, const exprt &b)
Merge the set containing a and the set containing b.
decision_proceduret::resultt dec_solve() override
Main decision procedure of the solver.
string_dependenciest dependencies
bitvector_typet char_type()
Extract member of struct or union.
Deprecated expression utility functions.
exprt univ_within_bounds() const
message_handlert & get_message_handler()
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.
array_exprt concretize(std::size_t size, const typet &index_type) const
Convert to an array representation, ignores elements at index >= size.
Structure type, corresponds to C style structs.
Forward depth-first search iterators These iterators' copy operations are expensive,...
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 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...
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
bool can_cast_expr< function_application_exprt >(const exprt &base)
Similar interface to union-find for expressions, with a function for replacing sub-expressions by the...
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
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)
Instantiates a quantified formula representing not_contains by substituting the quantifiers and gener...
#define string_refinement_invariantt(reason)
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...
int solver(std::istream &in)
bool has_char_pointer_subtype(const typet &type, const namespacet &ns)
bool is_constant() const
Return whether the expression is a constant.
Defines related function for string constraints.
A base class for relations, i.e., binary predicates whose two operands have the same type.
exprt simplify_sum(const exprt &f)
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
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.
static optionalt< exprt > substitute_array_access(const index_exprt &index_expr, symbol_generatort &symbol_generator, const bool left_propagate)
std::map< exprt, std::set< exprt > > current
std::vector< exprt > find_expressions(const std::size_t i)
std::vector< exprt > equations
std::vector< string_not_contains_constraintt > not_contains
void add_lemma(const exprt &lemma, bool simplify_lemma=true)
Add the given lemma to the solver.
Constraints to encode non containement of strings.
std::map< exprt, std::set< exprt > > cumulative
static bool is_linear_arithmetic_expr(const exprt &expr, const symbol_exprt &var)
string_refinementt constructor arguments
static array_index_mapt gather_indices(const exprt &expr)
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...
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
A constant literal expression.
depth_iteratort depth_end()
string_refinementt(const infot &)
std::vector< std::size_t > find_equations(const exprt &expr)
Array constructor from list of elements.
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...
ranget< iteratort > make_range(iteratort begin, iteratort end)
std::vector< string_not_contains_constraintt > not_contains
exprt get(const exprt &expr) const override
Return expr with variables replaced by values from satisfying assignment if available.
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...
std::set< exprt > seen_instances
std::vector< exprt > existential
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
std::vector< string_constraintt > universal