Go to the documentation of this file.
30 #include <unordered_set>
62 const std::function<
exprt(
const exprt &)> &get,
65 bool use_counter_example,
67 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
68 ¬_contain_witnesses);
90 const std::vector<exprt> ¤t_constraints);
95 const exprt &formula);
114 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
118 const std::function<
exprt(
const exprt &)> &super_get,
127 const bool left_propagate);
136 template <
typename T>
138 const std::map<std::size_t, T> &index_value)
140 std::vector<T> result;
141 if(!index_value.empty())
143 result.resize(index_value.rbegin()->first+1);
144 for(
auto it=index_value.rbegin(); it!=index_value.rend(); ++it)
146 const std::size_t index=it->first;
147 const T &value = it->second;
148 const auto next=std::next(it);
149 const std::size_t leftmost_index_to_pad=
150 next!=index_value.rend()
153 for(std::size_t j=leftmost_index_to_pad; j<=index; j++)
170 loop_bound_(info.refinement_bound),
185 std::size_t count_current=0;
188 const exprt &s=i.first;
189 stream <<
"IS(" <<
format(s) <<
")=={" << eom;
191 for(
const auto &j : i.second)
193 const auto it=index_set.
current.find(i.first);
194 if(it!=index_set.
current.end() && it->second.find(j)!=it->second.end())
199 stream <<
" " <<
format(j) <<
";" << eom;
202 stream <<
"}" << eom;
204 stream << count <<
" elements in index set (" << count_current
205 <<
" newly added)" << eom;
232 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
233 ¬_contain_witnesses)
235 std::vector<exprt> lemmas;
236 for(
const auto &i : index_set.
current)
238 for(
const auto &univ_axiom : axioms.
universal)
240 for(
const auto &j : i.second)
241 lemmas.push_back(
instantiate(univ_axiom, i.first, j));
246 for(
const auto &instance :
247 instantiate(nc_axiom, index_set, not_contain_witnesses))
248 lemmas.push_back(instance);
257 std::vector<equal_exprt> &equations)
263 expr_try_dynamic_cast<function_application_exprt>(eq.rhs()))
291 if(expr.
id() == ID_equal && value)
314 const std::vector<equal_exprt> &equations,
319 const std::string log_message =
320 "WARNING string_refinement.cpp generate_symbol_resolution_from_equations:";
323 const exprt &lhs = eq.lhs();
324 const exprt &rhs = eq.rhs();
325 if(lhs.
id()!=ID_symbol)
327 stream << log_message <<
"non symbol lhs: " <<
format(lhs)
328 <<
" with rhs: " <<
format(rhs) << eom;
334 stream << log_message <<
"non equal types lhs: " <<
format(lhs)
335 <<
"\n####################### rhs: " <<
format(rhs) << eom;
343 else if(rhs.
id() == ID_function_application)
351 if(rhs.
type().
id() == ID_struct)
354 for(
const auto &comp : struct_type.
components())
367 stream << log_message <<
"non struct with char pointer subexpr "
381 std::vector<exprt> result;
383 result.push_back(lhs);
384 else if(lhs.
type().
id() == ID_struct)
387 for(
const auto &comp : struct_type.
components())
392 result.end(), strings_in_comp.begin(), strings_in_comp.end());
404 std::vector<exprt> result;
409 result.push_back(*it);
410 it.next_sibling_or_parent();
412 else if(it->id() == ID_symbol)
416 it.next_sibling_or_parent();
444 for(
const auto &comp : struct_type.
components())
450 equal_exprt(lhs_data, rhs_data), symbol_resolve, ns);
464 std::vector<equal_exprt> &equations,
469 const std::string log_message =
470 "WARNING string_refinement.cpp "
471 "string_identifiers_resolution_from_equations:";
476 std::unordered_set<size_t> required_equations;
477 std::stack<size_t> equations_to_treat;
479 for(std::size_t i = 0; i < equations.size(); ++i)
482 if(eq.
rhs().
id() == ID_function_application)
484 if(required_equations.insert(i).second)
485 equations_to_treat.push(i);
488 for(
const auto &expr : rhs_strings)
489 equation_map.
add(i, expr);
497 for(
const auto &expr : lhs_strings)
498 equation_map.
add(i, expr);
500 if(lhs_strings.empty())
502 stream << log_message <<
"non struct with string subtype "
508 equation_map.
add(i, expr);
513 while(!equations_to_treat.empty())
515 const std::size_t i = equations_to_treat.top();
516 equations_to_treat.pop();
521 if(required_equations.insert(j).second)
522 equations_to_treat.push(j);
528 for(
const std::size_t i : required_equations)
535 static void output_equations(
537 std::ostream &output,
538 const std::vector<equal_exprt> &equations)
540 for(std::size_t i = 0; i < equations.size(); ++i)
541 output <<
" [" << i <<
"] " <<
format(equations[i].lhs())
542 <<
" == " <<
format(equations[i].rhs()) << std::endl;
613 debug() <<
"dec_solve: Initial set of equations" <<
eom;
617 debug() <<
"dec_solve: Build symbol solver from equations" <<
eom;
622 debug() <<
"symbol resolve:" <<
eom;
630 debug() <<
"symbol resolve string:" <<
eom;
631 for(
const auto &pair : string_id_symbol_resolve.
to_vector())
637 debug() <<
"dec_solve: Replacing string ids in function applications" <<
eom;
653 debug() <<
"dec_solve: compute dependency graph and remove function "
654 <<
"applications captured by the dependencies:" <<
eom;
655 std::vector<equal_exprt> local_equations;
660 const equal_exprt eq_with_char_array_replaced_with_representative_elements =
664 eq_with_char_array_replaced_with_representative_elements,
667 local_equations.push_back(eq);
675 debug() <<
"dec_solve: add constraints" <<
eom;
683 debug() <<
"dec_solve: arrays_of_pointers:" <<
eom;
687 <<
" : " <<
format(pair.second.type()) <<
eom;
691 for(
const auto &eq : local_equations)
708 "string constraints satisfy their invariant"));
722 std::unordered_map<string_not_contains_constraintt, symbol_exprt>
723 not_contain_witnesses;
726 const auto &witness_type = [&] {
731 not_contain_witnesses[nc_axiom] =
739 const auto get = [
this](
const exprt &expr) {
return this->
get(expr); };
745 std::vector<exprt> counter_examples;
754 not_contain_witnesses);
757 debug() <<
"check_SAT: the model is correct" <<
eom;
760 debug() <<
"check_SAT: got SAT but the model is not correct" <<
eom;
764 debug() <<
"check_SAT: got UNSAT or ERROR" <<
eom;
771 const auto instances =
773 for(
const auto &instance : instances)
784 std::vector<exprt> counter_examples;
793 not_contain_witnesses);
796 debug() <<
"check_SAT: the model is correct" <<
eom;
800 debug() <<
"check_SAT: got SAT but the model is not correct, refining..."
816 error() <<
"dec_solve: current index set is empty, "
817 <<
"this should not happen" <<
eom;
822 debug() <<
"dec_solve: current index set is empty, "
823 <<
"adding counter examples" <<
eom;
824 for(
const auto &counter : counter_examples)
829 const auto instances =
831 for(
const auto &instance : instances)
836 debug() <<
"check_SAT: default return " << static_cast<int>(res) <<
eom;
840 debug() <<
"string_refinementt::dec_solve reached the maximum number"
841 <<
"of steps allowed" <<
eom;
851 const bool simplify_lemma)
858 exprt simple_lemma=lemma;
865 debug() <<
"string_refinementt::add_lemma : tautology" <<
eom;
876 if(it->id() == ID_array && it->operands().empty())
881 it.next_sibling_or_parent();
901 const std::function<
exprt(
const exprt &)> &super_get,
909 exprt size_val=super_get(size);
916 if(size_val.
id()!=ID_constant)
918 stream <<
"(sr::get_array) string of unknown size: " <<
format(size_val)
923 auto n_opt = numeric_cast<std::size_t>(size_val);
926 stream <<
"(sr::get_array) size is not valid" << eom;
929 std::size_t n = *n_opt;
933 stream <<
"(sr::get_array) long string (size " <<
format(arr.
length())
934 <<
" = " << n <<
") " <<
format(arr) << eom;
935 stream <<
"(sr::get_array) consider reducing max-nondet-string-length so "
936 "that no string exceeds "
939 "make sure all functions returning strings are loaded"
941 stream <<
"(sr::get_array) this can also happen on invalid object access"
959 if(arr.
type().
id()!=ID_array)
960 return std::string(
"");
963 auto n = numeric_cast_v<std::size_t>(size_expr);
975 const std::function<
exprt(
const exprt &)> &super_get,
981 stream <<
"- " <<
format(arr) <<
":\n";
982 stream << std::string(4,
' ') <<
"- type: " <<
format(arr.
type()) << eom;
983 const auto arr_model_opt =
987 stream << std::string(4,
' ') <<
"- char_array: " <<
format(*arr_model_opt)
989 stream << std::string(4,
' ') <<
"- type : " <<
format(arr_model_opt->type())
992 stream << std::string(4,
' ') <<
"- simplified_char_array: " <<
format(simple)
995 const auto concretized_array =
get_array(
998 stream << std::string(4,
' ')
999 <<
"- concretized_char_array: " <<
format(*concretized_array)
1003 const auto array_expr =
1004 expr_try_dynamic_cast<array_exprt>(*concretized_array))
1006 stream << std::string(4,
' ') <<
"- as_string: \""
1010 stream << std::string(2,
' ') <<
"- warning: not an array" << eom;
1011 return *concretized_array;
1015 stream << std::string(4,
' ') <<
"- incomplete model" << eom;
1025 const std::function<
exprt(
const exprt &)> &super_get,
1026 const std::vector<symbol_exprt> &symbols)
1028 stream <<
"debug_model:" <<
'\n';
1031 const auto arr = pointer_array.second;
1033 super_get, ns, stream, arr);
1035 stream <<
"- " <<
format(arr) <<
":\n"
1036 <<
" - pointer: " <<
format(pointer_array.first) <<
"\n"
1040 for(
const auto &symbol : symbols)
1042 stream <<
" - " << symbol.get_identifier() <<
": "
1043 <<
format(super_get(symbol)) <<
'\n';
1063 const bool left_propagate)
1082 const exprt default_val = symbol_generator(
"out_of_bound_access",
char_type);
1092 const bool left_propagate)
1100 return if_exprt(if_expr.
cond(), true_case, false_case);
1107 const bool left_propagate)
1110 if(
auto array_of = expr_try_dynamic_cast<array_of_exprt>(array))
1111 return array_of->op();
1112 if(
auto array_with = expr_try_dynamic_cast<with_exprt>(array))
1114 *array_with, index_expr.
index(), left_propagate);
1115 if(
auto array_expr = expr_try_dynamic_cast<array_exprt>(array))
1117 *array_expr, index_expr.
index(), symbol_generator);
1118 if(
auto if_expr = expr_try_dynamic_cast<if_exprt>(array))
1120 *if_expr, index_expr.
index(), symbol_generator, left_propagate);
1123 array.
is_nil() || array.
id() == ID_symbol,
1125 "in case the array is unknown, it should be a symbol or nil, id: ")
1137 const bool left_propagate)
1139 if(
const auto index_expr = expr_try_dynamic_cast<index_exprt>(expr))
1173 const bool left_propagate)
1192 const std::function<
exprt(
const exprt &)> &get)
1205 std::vector<exprt> conjuncts;
1206 conjuncts.reserve(numeric_cast_v<std::size_t>(ube - lbe));
1210 const exprt s0_char =
1213 conjuncts.push_back(
equal_exprt(s0_char, s1_char));
1223 template <
typename T>
1227 const T &axiom_in_model,
1228 const exprt &negaxiom,
1229 const exprt &with_concretized_arrays)
1231 stream << std::string(4,
' ') <<
"- axiom:\n" << std::string(6,
' ');
1233 stream <<
'\n' << std::string(4,
' ') <<
"- axiom_in_model:\n"
1234 << std::string(6,
' ');
1235 stream <<
to_string(axiom_in_model) <<
'\n'
1236 << std::string(4,
' ') <<
"- negated_axiom:\n"
1237 << std::string(6,
' ') <<
format(negaxiom) <<
'\n';
1238 stream << std::string(4,
' ') <<
"- negated_axiom_with_concretized_arrays:\n"
1239 << std::string(6,
' ') <<
format(with_concretized_arrays) <<
'\n';
1246 const std::function<
exprt(
const exprt &)> &get,
1249 bool use_counter_example,
1251 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
1252 ¬_contain_witnesses)
1256 const auto gen_symbol = [&](
const irep_idt &id,
const typet &type)
1262 stream <<
"string_refinementt::check_axioms:" << eom;
1264 stream <<
"symbol_resolve:" << eom;
1265 auto pairs = symbol_resolve.
to_vector();
1266 for(
const auto &pair : pairs)
1267 stream <<
" - " <<
format(pair.first) <<
" --> " <<
format(pair.second)
1272 generator, stream, ns, get, generator.
fresh_symbol.created_symbols);
1276 std::map<size_t, exprt> violated;
1278 stream <<
"string_refinement::check_axioms: " << axioms.
universal.size()
1279 <<
" universal axioms:" << eom;
1280 for(
size_t i=0; i<axioms.
universal.size(); i++)
1292 stream << std::string(2,
' ') << i <<
".\n";
1293 const exprt with_concretized_arrays =
1296 stream, axiom, axiom_in_model, negaxiom, with_concretized_arrays);
1299 const auto &witness =
1302 stream << std::string(4,
' ') <<
"- violated_for: "
1304 violated[i]=*witness;
1307 stream << std::string(4,
' ') <<
"- correct" << eom;
1311 std::map<std::size_t, exprt> violated_not_contains;
1314 <<
" not_contains axioms" << eom;
1315 for(std::size_t i = 0; i < axioms.
not_contains.size(); i++)
1321 nc_axiom, univ_var, [&](
const exprt &expr) {
1324 stream << std::string(2,
' ') << i <<
".\n";
1326 stream, nc_axiom, nc_axiom, negated_axiom, negated_axiom);
1329 const auto witness =
1332 stream << std::string(4,
' ') <<
"- violated_for: "
1334 violated_not_contains[i]=*witness;
1338 if(violated.empty() && violated_not_contains.empty())
1340 stream <<
"no violated property" << eom;
1341 return {
true, std::vector<exprt>() };
1345 stream << violated.size()
1346 <<
" universal string axioms can be violated" << eom;
1347 stream << violated_not_contains.size()
1348 <<
" not_contains string axioms can be violated" << eom;
1350 if(use_counter_example)
1352 std::vector<exprt> lemmas;
1354 for(
const auto &v : violated)
1356 const exprt &val=v.second;
1367 lemmas.push_back(counter);
1370 for(
const auto &v : violated_not_contains)
1372 const exprt &val=v.second;
1376 const exprt func_val =
1377 index_exprt(not_contain_witnesses.at(axiom), val);
1380 std::set<std::pair<exprt, exprt>> indices;
1381 indices.insert(std::pair<exprt, exprt>(comp_val, func_val));
1382 const exprt counter =
1384 lemmas.push_back(counter);
1386 return {
false, lemmas };
1389 return {
false, std::vector<exprt>() };
1399 std::map<exprt, int> elems;
1401 std::list<std::pair<exprt, bool> > to_process;
1402 to_process.emplace_back(f,
true);
1404 while(!to_process.empty())
1406 exprt cur=to_process.back().first;
1407 bool positive=to_process.back().second;
1408 to_process.pop_back();
1409 if(cur.
id()==ID_plus)
1411 for(
const auto &op : cur.
operands())
1412 to_process.emplace_back(op, positive);
1414 else if(cur.
id()==ID_minus)
1416 to_process.emplace_back(cur.
op1(), !positive);
1417 to_process.emplace_back(cur.
op0(), positive);
1419 else if(cur.
id()==ID_unary_minus)
1421 to_process.emplace_back(cur.
op0(), !positive);
1426 elems[cur]=elems[cur]+1;
1428 elems[cur]=elems[cur]-1;
1441 std::map<exprt, int> &m,
1453 for(
const auto &term : m)
1456 const exprt &t=term.first;
1457 int second=negated?(-term.second):term.second;
1458 if(t.
id()==ID_constant)
1461 constants += int_value * second;
1488 for(
int i=1; i<second; i++)
1497 for(
int i=-1; i>second; i--)
1533 exprt positive, negative;
1543 auto it=elems.find(qvar);
1547 if(it->second==1 || it->second==-1)
1549 neg=(it->second==1);
1556 "a proper function must have exactly one "
1557 "occurrences after reduction, or it cancelled out, and it does not"
1603 for(
const auto &axiom : axioms.
universal)
1616 const std::vector<exprt> ¤t_constraints)
1618 for(
const auto &axiom : current_constraints)
1630 if(array_expr.
id()==ID_if)
1637 if(array_expr.
type().
id() == ID_array)
1640 accu.push_back(array_expr);
1644 for(
const auto &operand : array_expr.
operands())
1662 const bool is_size_t = numeric_cast<std::size_t>(i).has_value();
1663 if(i.
id()!=ID_constant || is_size_t)
1665 std::vector<exprt> sub_arrays;
1667 for(
const auto &sub : sub_arrays)
1668 if(index_set.
cumulative[sub].insert(i).second)
1669 index_set.
current[sub].insert(i);
1692 const exprt &upper_bound,
1697 if(s.
id() == ID_array)
1699 for(std::size_t j = 0; j < s.
operands().size(); ++j)
1703 if(
auto ite = expr_try_dynamic_cast<if_exprt>(s))
1729 const auto &s = index_expr.
array();
1731 it.next_sibling_or_parent();
1755 it.next_sibling_or_parent();
1773 const exprt &formula)
1775 std::list<exprt> to_process;
1776 to_process.push_back(formula);
1778 while(!to_process.empty())
1780 exprt cur=to_process.back();
1781 to_process.pop_back();
1790 if(s.
id() != ID_array)
1796 to_process.push_back(*it);
1808 static std::unordered_set<exprt, irep_hash>
1812 auto index_str_containing_qvar = [&](
const exprt &e) {
1813 if(
auto index_expr = expr_try_dynamic_cast<index_exprt>(e))
1815 const auto &arr = index_expr->
array();
1816 const auto str_it = std::find(arr.depth_begin(), arr.depth_end(), str);
1823 if(index_str_containing_qvar(e))
1852 const exprt univ_var_value =
1860 conjuncts.push_back(instance);
1886 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
1893 const auto &index_set1=index_set.
cumulative.find(
s1.content());
1894 const auto ¤t_index_set0=index_set.
current.find(s0.
content());
1895 const auto ¤t_index_set1=index_set.
current.find(
s1.content());
1899 current_index_set0!=index_set.
current.end() &&
1900 current_index_set1!=index_set.
current.end())
1902 typedef std::pair<exprt, exprt> expr_pairt;
1903 std::set<expr_pairt> index_pairs;
1905 for(
const auto &ic0 : current_index_set0->second)
1906 for(
const auto &i1 : index_set1->second)
1907 index_pairs.insert(expr_pairt(ic0, i1));
1908 for(
const auto &ic1 : current_index_set1->second)
1909 for(
const auto &i0 : index_set0->second)
1910 index_pairs.insert(expr_pairt(i0, ic1));
1926 for(
auto &operand : expr.
operands())
1929 if(expr.
id() == ID_array_list)
1939 for(
size_t i=0; i<expr.
operands().size(); i+=2)
1943 const auto index_value = numeric_cast<std::size_t>(index);
1945 (index_value && *index_value<string_max_length))
1963 const auto super_get = [
this](
const exprt &expr) {
1970 const auto &index_expr = expr_try_dynamic_cast<index_exprt>(ecopy);
1973 std::reference_wrapper<const exprt> current(index_expr->
array());
1974 while(current.get().id() == ID_if)
1976 const auto &if_expr = expr_dynamic_cast<if_exprt>(current.get());
1979 current = std::cref(if_expr.
true_case());
1980 else if(cond.is_false())
1986 const auto index =
get(index_expr->
index());
1987 const exprt unknown =
1992 if(
const auto index_value = numeric_cast<std::size_t>(index))
1993 return sparse_array->at(*index_value);
1994 return sparse_array->to_if_expression(index);
1998 array.is_nil() || array.id() == ID_symbol,
2000 "apart from symbols, array valuations can be interpreted as "
2001 "sparse arrays, id: ") +
2012 const auto from_dependencies =
2014 return *from_dependencies;
2017 const auto arr_model_opt =
2019 return *arr_model_opt;
2024 if(
const auto n = numeric_cast<std::size_t>(length))
2049 satcheck_no_simplifiert sat_check;
2070 [&](
const exprt &expr)
2072 const auto index_expr = expr_try_dynamic_cast<const index_exprt>(expr);
2074 indices[index_expr->
array()].push_back(index_expr->
index());
2091 it->id() != ID_plus && it->id() != ID_minus &&
2092 it->id() != ID_unary_minus && *it != var)
2097 it.next_sibling_or_parent();
2118 if(it->id() == ID_index)
2119 it.next_sibling_or_parent();
2141 for(
const auto &pair : body_indices)
2144 const exprt rep=pair.second.back();
2145 for(
size_t j=0; j<pair.second.size()-1; j++)
2147 const exprt i=pair.second[j];
2152 stream <<
"Indices not equal: " <<
to_string(constraint)
2153 <<
", str: " <<
format(pair.first) << eom;
2161 stream <<
"f is not linear: " <<
to_string(constraint)
2162 <<
", str: " <<
format(pair.first) << eom;
2170 stream <<
"Universal variable outside of index:" <<
to_string(constraint)
Operator to update elements in structs and arrays.
std::vector< string_constraintt > universal
const componentst & components() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool equality_propagation
#define PRECONDITION(CONDITION)
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 & 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.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
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 std::vector< exprt > extract_strings(const exprt &expr)
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 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.
exprt get_length(const array_string_exprt &s) const
Associate an actual finite length to infinite arrays.
void set_to(const exprt &expr, bool value) override
std::vector< exprt > current_constraints
bool add_node(string_dependenciest &dependencies, const equal_exprt &equation, array_poolt &array_pool)
When right hand side of equation is a builtin_function add a "string_builtin_function" node to the gr...
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.
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
symbol_generatort fresh_symbol
exprt to_if_expression(const exprt &index) const
std::vector< equal_exprt > equations
bool replace_expr(exprt &expr) const
Replace subexpressions of expr by the representative element of the set they belong to.
const std::size_t MAX_CONCRETE_STRING_SIZE
The plus expression Associativity is not specified.
Base class for all expressions.
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
void l_set_to_true(literalt a)
optionalt< exprt > make_array_pointer_association(const function_application_exprt &expr)
Associate array to pointer, and array to length.
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.
bool is_true() const
Return whether the expression is a constant representing true.
index_set_pairt index_sets
Expression to hold a symbol (variable)
exprt simplify_expr(const exprt &src, const namespacet &ns)
bitvector_typet index_type()
Magic numbers used throughout the codebase.
void visit(class expr_visitort &visitor)
#define UNREACHABLE
This should be used to mark dead code.
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)
static exprt substitute_array_access(const index_exprt &index_expr, const std::function< symbol_exprt(const irep_idt &, const typet &)> &symbol_generator, const bool left_propagate)
std::map< exprt, std::vector< exprt > > array_index_mapt
static std::unordered_set< exprt, irep_hash > find_indexes(const exprt &expr, const exprt &str, const symbol_exprt &qvar)
Find indexes of str used in expr that contains qvar, for instance with arguments (str[k+1]=='a'),...
static exprt instantiate(const string_constraintt &axiom, const exprt &str, const exprt &val)
Substitute qvar the universally quantified variable of axiom, by an index val, in axiom,...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
static optionalt< exprt > get_array(const std::function< exprt(const exprt &)> &super_get, const namespacet &ns, messaget::mstreamt &stream, const array_string_exprt &arr)
Get a model of an array and put it in a certain form.
typet & type()
Return the type of the expression.
static bool is_valid_string_constraint(messaget::mstreamt &stream, const namespacet &ns, const string_constraintt &constraint)
static bool find_qvar(const exprt &index, const symbol_exprt &qvar)
look for the symbol and return true if it is found
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
void clean_cache()
Clean the cache used by eval
#define CHARACTER_FOR_UNKNOWN
union_find_replacet string_identifiers_resolution_from_equations(std::vector< equal_exprt > &equations, const namespacet &ns, messaget::mstreamt &stream)
Symbol resolution for expressions of type string typet.
const std::string & id2string(const irep_idt &d)
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...
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
string_constraintst constraints
void output_dot(std::ostream &stream) const
Array constructor from single element.
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)
bool is_char_array_type(const typet &type, const namespacet &ns)
Distinguish char array from other types.
static void make_char_array_pointer_associations(string_constraint_generatort &generator, std::vector< equal_exprt > &equations)
Fill the array_pointer correspondence and replace the right hand sides of the corresponding equations...
void add_constraints(string_constraint_generatort &generatort)
For all builtin call on which a test (or an unsupported buitin) result depends, add the corresponding...
The unary minus expression.
void clear()
Clear all constraints.
const irep_idt & id() const
std::vector< exprt > operandst
void add(const std::size_t i, const exprt &expr)
Record the fact that equation i contains expression expr
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.
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)
Display part of the current model by mapping the variables created by the solver to constant expressi...
array_string_exprt & to_array_string_expr(exprt &expr)
static exprt compute_inverse_function(const exprt &qvar, const exprt &val, const exprt &f)
nonstd::optional< T > optionalt
union_find_replacet symbol_resolve
static optionalt< exprt > find_counter_example(const namespacet &ns, const exprt &axiom, const symbol_exprt &var)
Creates a solver with axiom as the only formula added and runs it.
literalt convert(const exprt &expr) override
std::string utf16_constant_array_to_java(const array_exprt &arr, std::size_t length)
Construct a string from a constant array.
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()
static void add_equations_for_symbol_resolution(union_find_replacet &symbol_solver, const std::vector< equal_exprt > &equations, const namespacet &ns, messaget::mstreamt &stream)
Add association for each char pointer in the equation.
Extract member of struct or union.
Deprecated expression utility functions.
exprt univ_within_bounds() const
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.
static exprt sum_over_map(std::map< exprt, int > &m, const typet &type, bool negated=false)
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...
static void substitute_array_access_in_place(exprt &expr, const std::function< symbol_exprt(const irep_idt &, const typet &)> &symbol_generator, const bool left_propagate)
Auxiliary function for substitute_array_access Performs the same operation but modifies the argument ...
void operator()(const exprt &expr) override
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)
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.
A base class for relations, i.e., binary predicates.
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 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)
Debugging function which finds the valuation of the given array in super_get and concretize unknown c...
find_qvar_visitort(const exprt &qvar)
const std::set< array_string_exprt > & created_strings() const
std::map< exprt, std::set< exprt > > current
std::vector< exprt > find_expressions(const std::size_t i)
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...
A constant literal expression.
static std::vector< exprt > extract_strings_from_lhs(const exprt &lhs)
This is meant to be used on the lhs of an equation with string subtype.
depth_iteratort depth_end()
static std::map< exprt, int > map_representation_of_sum(const exprt &f)
string_refinementt(const infot &)
bool has_char_array_subexpr(const exprt &expr, const namespacet &ns)
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...
std::vector< string_not_contains_constraintt > not_contains
exprt get(const exprt &expr) const override
bool can_cast_expr< function_application_exprt >(const exprt &base)
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