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)
704 constraint.replace_expr(symbol_resolve);
706 is_valid_string_constraint(error(), ns, constraint),
707 string_refinement_invariantt(
708 "string constraints satisfy their invariant"));
717 replace(symbol_resolve, axiom);
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);
1817 return str_it != arr.depth_end() &&
find_qvar(index_expr->
index(), qvar);
1823 if(index_str_containing_qvar(e))
1824 result.insert(to_index_expr(e).index());
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());
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)