30 #include <unordered_set> 63 const std::function<
exprt(
const exprt &)> &
get,
66 std::size_t max_string_length,
67 bool use_counter_example,
91 const std::vector<exprt> ¤t_constraints);
96 const exprt &formula);
120 const std::function<
exprt(
const exprt &)> &super_get,
122 const std::size_t max_string_length,
130 const bool left_propagate);
139 template <
typename T>
141 const std::map<std::size_t, T> &index_value)
143 std::vector<T> result;
144 if(!index_value.empty())
146 result.resize(index_value.rbegin()->first+1);
147 for(
auto it=index_value.rbegin(); it!=index_value.rend(); ++it)
149 const std::size_t index=it->first;
150 const T &value = it->second;
151 const auto next=std::next(it);
152 const std::size_t leftmost_index_to_pad=
153 next!=index_value.rend()
156 for(std::size_t j=leftmost_index_to_pad; j<=index; j++)
173 loop_bound_(info.refinement_bound),
174 max_string_length(info.max_string_length),
189 std::size_t count_current=0;
192 const exprt &s=i.first;
193 stream <<
"IS(" <<
format(s) <<
")=={" << eom;
195 for(
const auto &j : i.second)
197 const auto it=index_set.
current.find(i.first);
198 if(it!=index_set.
current.end() && it->second.find(j)!=it->second.end())
203 stream <<
" " <<
format(j) <<
";" << eom;
206 stream <<
"}" << eom;
208 stream << count <<
" elements in index set (" << count_current
209 <<
" newly added)" << eom;
240 std::vector<exprt> lemmas;
241 for(
const auto &i : index_set.
current)
243 for(
const auto &univ_axiom : axioms.
universal)
245 for(
const auto &j : i.second)
246 lemmas.push_back(
instantiate(stream, univ_axiom, i.first, j));
251 for(
const auto &instance :
253 lemmas.push_back(instance);
262 std::vector<equal_exprt> &equations)
268 expr_try_dynamic_cast<function_application_exprt>(eq.rhs()))
278 std::vector<equal_exprt> &equations)
293 if(expr.
id() == ID_equal && value)
313 const std::vector<equal_exprt> &equations,
318 const std::string log_message =
319 "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;
341 solver.make_union(lhs, rhs);
343 else if(rhs.
id() == ID_function_application)
351 if(rhs.
type().
id() == ID_struct)
354 for(
const auto &comp : struct_type.
components())
361 solver.make_union(lhs_data, rhs_data);
367 stream << log_message <<
"non struct with char pointer subexpr " 382 std::vector<exprt> result;
384 result.push_back(lhs);
385 else if(lhs.
type().
id() == ID_struct)
388 for(
const auto &comp : struct_type.
components())
393 result.end(), strings_in_comp.begin(), strings_in_comp.end());
405 std::vector<exprt> result;
410 result.push_back(*it);
411 it.next_sibling_or_parent();
413 else if(it->id() == ID_symbol)
417 it.next_sibling_or_parent();
445 for(
const auto &comp : struct_type.
components())
451 equal_exprt(lhs_data, rhs_data), symbol_resolve, ns);
465 std::vector<equal_exprt> &equations,
470 const std::string log_message =
471 "WARNING string_refinement.cpp " 472 "string_identifiers_resolution_from_equations:";
477 std::unordered_set<size_t> required_equations;
478 std::stack<size_t> equations_to_treat;
480 for(std::size_t i = 0; i < equations.size(); ++i)
483 if(eq.
rhs().
id() == ID_function_application)
485 if(required_equations.insert(i).second)
486 equations_to_treat.push(i);
489 for(
const auto &expr : rhs_strings)
490 equation_map.
add(i, expr);
498 for(
const auto &expr : lhs_strings)
499 equation_map.
add(i, expr);
501 if(lhs_strings.empty())
503 stream << log_message <<
"non struct with string subtype " 509 equation_map.
add(i, expr);
514 while(!equations_to_treat.empty())
516 const std::size_t i = equations_to_treat.top();
517 equations_to_treat.pop();
522 if(required_equations.insert(j).second)
523 equations_to_treat.push(j);
529 for(
const std::size_t i : required_equations)
537 std::ostream &output,
538 const std::vector<equal_exprt> &equations,
541 for(std::size_t i = 0; i < equations.size(); ++i)
542 output <<
" [" << i <<
"] " <<
format(equations[i].lhs())
543 <<
" == " <<
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 char pointer symbols" <<
eom;
640 debug() <<
"dec_solve: Replacing string ids in function applications" <<
eom;
656 debug() <<
"dec_solve: compute dependency graph and remove function " 657 <<
"applications captured by the dependencies:" <<
eom;
658 std::vector<exprt> local_equations;
662 local_equations.push_back(eq);
670 debug() <<
"dec_solve: add constraints" <<
eom;
678 debug() <<
"dec_solve: arrays_of_pointers:" <<
eom;
682 <<
" : " <<
format(pair.second.type()) <<
eom;
686 for(
const auto &eq : local_equations)
704 "string constraints satisfy their invariant"));
708 const auto not_contains_constraints =
711 not_contains_constraints.begin(),
712 not_contains_constraints.end(),
721 const auto &witness_type = [&] {
734 const auto get = [
this](
const exprt &expr) {
return this->
get(expr); };
740 std::vector<exprt> counter_examples;
753 debug() <<
"check_SAT: the model is correct" <<
eom;
756 debug() <<
"check_SAT: got SAT but the model is not correct" <<
eom;
760 debug() <<
"check_SAT: got UNSAT or ERROR" <<
eom;
767 for(
const auto &instance :
784 std::vector<exprt> counter_examples;
797 debug() <<
"check_SAT: the model is correct" <<
eom;
801 debug() <<
"check_SAT: got SAT but the model is not correct, refining..." 817 error() <<
"dec_solve: current index set is empty, " 818 <<
"this should not happen" <<
eom;
823 debug() <<
"dec_solve: current index set is empty, " 824 <<
"adding counter examples" <<
eom;
825 for(
const auto &counter : counter_examples)
830 for(
const auto &instance :
841 debug() <<
"check_SAT: default return " <<
static_cast<int>(res) <<
eom;
845 debug() <<
"string_refinementt::dec_solve reached the maximum number" 846 <<
"of steps allowed" <<
eom;
856 const bool simplify_lemma)
863 exprt simple_lemma=lemma;
870 debug() <<
"string_refinementt::add_lemma : tautology" <<
eom;
881 if(it->id() == ID_array && it->operands().empty())
886 it.next_sibling_or_parent();
907 const std::function<
exprt(
const exprt &)> &super_get,
909 const std::size_t max_string_length,
916 exprt size_val=super_get(size);
923 if(size_val.
id()!=ID_constant)
925 stream <<
"(sr::get_array) string of unknown size: " <<
format(size_val)
933 stream <<
"(sr::get_array) size is not valid" << eom;
936 std::size_t n = *n_opt;
940 stream <<
"(sr::get_array) long string (size " <<
format(arr.
length())
941 <<
" = " << n <<
") " <<
format(arr) << eom;
942 stream <<
"(sr::get_array) consider reducing string-max-input-length so " 943 "that no string exceeds " 946 "make sure all functions returning strings are loaded" 948 stream <<
"(sr::get_array) this can also happen on invalid object access" 966 if(arr.
type().
id()!=ID_array)
967 return std::string(
"");
970 auto n = numeric_cast_v<std::size_t>(size_expr);
983 const std::function<
exprt(
const exprt &)> &super_get,
985 const std::size_t max_string_length,
990 static const std::string indent(
" ");
991 stream <<
"- " <<
format(arr) <<
":\n";
992 stream << indent << indent <<
"- type: " <<
format(arr.
type()) << eom;
993 const auto arr_model_opt =
994 get_array(super_get, ns, max_string_length, stream, arr);
997 stream << indent << indent <<
"- char_array: " <<
format(*arr_model_opt)
999 stream << indent << indent <<
"- type : " <<
format(arr_model_opt->type())
1002 stream << indent << indent <<
"- simplified_char_array: " <<
format(simple)
1005 const auto concretized_array =
get_array(
1008 stream << indent << indent
1009 <<
"- concretized_char_array: " <<
format(*concretized_array)
1013 const auto array_expr =
1014 expr_try_dynamic_cast<array_exprt>(*concretized_array))
1016 stream << indent << indent <<
"- as_string: \"" 1020 stream << indent <<
"- warning: not an array" << eom;
1021 return *concretized_array;
1025 stream << indent << indent <<
"- incomplete model" << eom;
1035 const std::size_t max_string_length,
1036 const std::function<
exprt(
const exprt &)> &super_get,
1037 const std::vector<symbol_exprt> &boolean_symbols,
1038 const std::vector<symbol_exprt> &index_symbols)
1040 static const std::string indent(
" ");
1042 stream <<
"debug_model:" <<
'\n';
1045 const auto arr = pointer_array.second;
1047 super_get, ns, max_string_length, stream, arr);
1049 stream <<
"- " <<
format(arr) <<
":\n" 1050 << indent <<
"- pointer: " <<
format(pointer_array.first) <<
"\n" 1054 for(
const auto &symbol : boolean_symbols)
1056 stream <<
" - " << symbol.get_identifier() <<
": " 1057 <<
format(super_get(symbol)) <<
'\n';
1060 for(
const auto &symbol : index_symbols)
1062 stream <<
" - " << symbol.get_identifier() <<
": " 1063 <<
format(super_get(symbol)) <<
'\n';
1083 const bool left_propagate)
1102 const exprt default_val = symbol_generator(
"out_of_bound_access",
char_type);
1112 const bool left_propagate)
1120 return if_exprt(if_expr.
cond(), true_case, false_case);
1127 const bool left_propagate)
1130 if(
auto array_of = expr_try_dynamic_cast<array_of_exprt>(array))
1131 return array_of->op();
1132 if(
auto array_with = expr_try_dynamic_cast<with_exprt>(array))
1134 *array_with, index_expr.
index(), left_propagate);
1135 if(
auto array_expr = expr_try_dynamic_cast<array_exprt>(array))
1137 *array_expr, index_expr.
index(), symbol_generator);
1138 if(
auto if_expr = expr_try_dynamic_cast<if_exprt>(array))
1140 *if_expr, index_expr.
index(), symbol_generator, left_propagate);
1143 array.
is_nil() || array.
id() == ID_symbol,
1145 "in case the array is unknown, it should be a symbol or nil, id: ")
1157 const bool left_propagate)
1159 if(
const auto index_expr = expr_try_dynamic_cast<index_exprt>(expr))
1193 const bool left_propagate)
1212 const std::function<
exprt(
const exprt &)> &
get)
1225 std::vector<exprt> conjuncts;
1226 conjuncts.reserve(numeric_cast_v<std::size_t>(ube - lbe));
1230 const exprt s0_char =
1233 conjuncts.push_back(
equal_exprt(s0_char, s1_char));
1243 template <
typename T>
1248 const T &axiom_in_model,
1249 const exprt &negaxiom,
1250 const exprt &with_concretized_arrays)
1252 static const std::string indent =
" ";
1253 static const std::string indent2 =
" ";
1254 stream << indent2 <<
"- axiom:\n" << indent2 << indent;
1256 stream <<
'\n' << indent2 <<
"- axiom_in_model:\n" << indent2 << indent;
1257 stream <<
to_string(axiom_in_model) <<
'\n' 1258 << indent2 <<
"- negated_axiom:\n" 1259 << indent2 << indent <<
format(negaxiom) <<
'\n';
1260 stream << indent2 <<
"- negated_axiom_with_concretized_arrays:\n" 1261 << indent2 << indent <<
format(with_concretized_arrays) <<
'\n';
1269 const std::function<
exprt(
const exprt &)> &
get,
1272 std::size_t max_string_length,
1273 bool use_counter_example,
1278 static const std::string indent =
" ";
1279 static const std::string indent2 =
" ";
1281 const auto gen_symbol = [&](
const irep_idt &id,
const typet &type)
1287 stream <<
"string_refinementt::check_axioms:" << eom;
1289 stream <<
"symbol_resolve:" << eom;
1290 auto pairs = symbol_resolve.
to_vector();
1291 for(
const auto &pair : pairs)
1292 stream <<
" - " <<
format(pair.first) <<
" --> " <<
format(pair.second)
1307 std::map<size_t, exprt> violated;
1309 stream <<
"string_refinement::check_axioms: " << axioms.
universal.size()
1310 <<
" universal axioms:" << eom;
1311 for(
size_t i=0; i<axioms.
universal.size(); i++)
1323 stream << indent << i <<
".\n";
1324 const exprt with_concretized_arrays =
1327 stream, ns, axiom, axiom_in_model, negaxiom, with_concretized_arrays);
1330 const auto &witness =
1333 stream << indent2 <<
"- violated_for: " <<
format(axiom.
univ_var) <<
"=" 1334 <<
format(*witness) << eom;
1335 violated[i]=*witness;
1338 stream << indent2 <<
"- correct" << eom;
1342 std::map<std::size_t, exprt> violated_not_contains;
1345 <<
" not_contains axioms" << eom;
1346 for(std::size_t i = 0; i < axioms.
not_contains.size(); i++)
1350 "not_contains_univ_var", nc_axiom.
s0().
length().
type());
1352 nc_axiom, univ_var, [&](
const exprt &expr) {
1355 stream << indent << i <<
".\n";
1357 stream, ns, nc_axiom, nc_axiom, negated_axiom, negated_axiom);
1360 const auto witness =
1363 stream << indent2 <<
"- violated_for: " << univ_var.
get_identifier()
1364 <<
"=" <<
format(*witness) << eom;
1365 violated_not_contains[i]=*witness;
1369 if(violated.empty() && violated_not_contains.empty())
1371 stream <<
"no violated property" << eom;
1372 return {
true, std::vector<exprt>() };
1376 stream << violated.size()
1377 <<
" universal string axioms can be violated" << eom;
1378 stream << violated_not_contains.size()
1379 <<
" not_contains string axioms can be violated" << eom;
1381 if(use_counter_example)
1383 std::vector<exprt> lemmas;
1385 for(
const auto &v : violated)
1387 const exprt &val=v.second;
1398 lemmas.push_back(counter);
1401 for(
const auto &v : violated_not_contains)
1403 const exprt &val=v.second;
1410 std::set<std::pair<exprt, exprt>> indices;
1411 indices.insert(std::pair<exprt, exprt>(comp_val, func_val));
1413 axiom, indices, generator)[0];
1414 lemmas.push_back(counter);
1416 return {
false, lemmas };
1419 return {
false, std::vector<exprt>() };
1429 std::map<exprt, int> elems;
1431 std::list<std::pair<exprt, bool> > to_process;
1432 to_process.emplace_back(f,
true);
1434 while(!to_process.empty())
1436 exprt cur=to_process.back().first;
1437 bool positive=to_process.back().second;
1438 to_process.pop_back();
1439 if(cur.
id()==ID_plus)
1441 for(
const auto &op : cur.
operands())
1442 to_process.emplace_back(op, positive);
1444 else if(cur.
id()==ID_minus)
1446 to_process.emplace_back(cur.
op1(), !positive);
1447 to_process.emplace_back(cur.
op0(), positive);
1449 else if(cur.
id()==ID_unary_minus)
1451 to_process.emplace_back(cur.
op0(), !positive);
1456 elems[cur]=elems[cur]+1;
1458 elems[cur]=elems[cur]-1;
1471 std::map<exprt, int> &m,
1483 for(
const auto &term : m)
1486 const exprt &t=term.first;
1487 int second=negated?(-term.second):term.second;
1488 if(t.
id()==ID_constant)
1518 for(
int i=1; i<second; i++)
1527 for(
int i=-1; i>second; i--)
1565 exprt positive, negative;
1575 auto it=elems.find(qvar);
1579 if(it->second==1 || it->second==-1)
1581 neg=(it->second==1);
1588 "a proper function must have exactly one " 1589 "occurrences after reduction, or it cancelled out, and it does not" 1591 stream <<
"in string_refinementt::compute_inverse_function:" 1592 <<
" warning: occurrences of qvar cancelled out " <<
messaget::eom;
1637 for(
const auto &axiom : axioms.
universal)
1650 const std::vector<exprt> ¤t_constraints)
1652 for(
const auto &axiom : current_constraints)
1664 if(array_expr.
id()==ID_if)
1671 if(array_expr.
type().
id() == ID_array)
1674 accu.push_back(array_expr);
1678 for(
const auto &operand : array_expr.
operands())
1696 const bool is_size_t =
numeric_cast<std::size_t>(i).has_value();
1697 if(i.
id()!=ID_constant || is_size_t)
1699 std::vector<exprt> sub_arrays;
1701 for(
const auto &sub : sub_arrays)
1702 if(index_set.
cumulative[sub].insert(i).second)
1703 index_set.
current[sub].insert(i);
1726 const exprt &upper_bound,
1731 if(s.
id() == ID_array)
1733 for(std::size_t j = 0; j < s.
operands().size(); ++j)
1737 if(
auto ite = expr_try_dynamic_cast<if_exprt>(s))
1763 const auto &s = index_expr.
array();
1765 it.next_sibling_or_parent();
1789 it.next_sibling_or_parent();
1808 const exprt &formula)
1810 std::list<exprt> to_process;
1811 to_process.push_back(formula);
1813 while(!to_process.empty())
1815 exprt cur=to_process.back();
1816 to_process.pop_back();
1825 if(s.
id() != ID_array)
1831 to_process.push_back(*it);
1843 static std::unordered_set<exprt, irep_hash>
1847 auto index_str_containing_qvar = [&](
const exprt &e) {
1848 if(
auto index_expr = expr_try_dynamic_cast<index_exprt>(e))
1850 const auto &arr = index_expr->
array();
1851 const auto str_it = std::find(arr.depth_begin(), arr.depth_end(), str);
1858 if(index_str_containing_qvar(e))
1884 str.
id() == ID_array || indexes.
size() <= 1,
1885 "non constant array should always be accessed at the same index");
1887 for(
const auto &index : indexes)
1889 const exprt univ_var_value =
1897 conjuncts.push_back(instance);
1929 const auto &index_set1=index_set.
cumulative.find(
s1.content());
1930 const auto ¤t_index_set0=index_set.
current.find(s0.
content());
1931 const auto ¤t_index_set1=index_set.
current.find(
s1.content());
1935 current_index_set0!=index_set.
current.end() &&
1936 current_index_set1!=index_set.
current.end())
1938 typedef std::pair<exprt, exprt> expr_pairt;
1939 std::set<expr_pairt> index_pairs;
1941 for(
const auto &ic0 : current_index_set0->second)
1942 for(
const auto &i1 : index_set1->second)
1943 index_pairs.insert(expr_pairt(ic0, i1));
1944 for(
const auto &ic1 : current_index_set1->second)
1945 for(
const auto &i0 : index_set0->second)
1946 index_pairs.insert(expr_pairt(i0, ic1));
1962 for(
auto &operand : expr.
operands())
1965 if(expr.
id() == ID_array_list)
1975 for(
size_t i=0; i<expr.
operands().size(); i+=2)
1979 const auto index_value =
numeric_cast<std::size_t>(index);
1981 (index_value && *index_value<string_max_length))
1999 const auto super_get = [
this](
const exprt &expr) {
2009 std::reference_wrapper<const exprt> current(index_expr->
array());
2010 while(current.get().id() == ID_if)
2015 current = std::cref(if_expr.
true_case());
2016 else if(cond.is_false())
2022 const auto index =
get(index_expr->
index());
2023 const exprt unknown =
2028 if(
const auto index_value = numeric_cast<std::size_t>(index))
2029 return sparse_array->at(*index_value);
2030 return sparse_array->to_if_expression(index);
2034 array.is_nil() || array.id() == ID_symbol,
2036 "apart from symbols, array valuations can be interpreted as " 2037 "sparse arrays, id: ") +
2048 const auto from_dependencies =
2050 return *from_dependencies;
2053 const auto arr_model_opt =
2055 return *arr_model_opt;
2060 if(
const auto n = numeric_cast<std::size_t>(length))
2087 satcheck_no_simplifiert sat_check;
2108 [&](
const exprt &expr)
2112 indices[index_expr->
array()].push_back(index_expr->
index());
2129 it->id() != ID_plus && it->id() != ID_minus &&
2130 it->id() != ID_unary_minus && *it != var)
2135 it.next_sibling_or_parent();
2156 if(it->id() == ID_index)
2157 it.next_sibling_or_parent();
2179 for(
const auto &pair : body_indices)
2182 const exprt rep=pair.second.back();
2183 for(
size_t j=0; j<pair.second.size()-1; j++)
2185 const exprt i=pair.second[j];
2190 stream <<
"Indices not equal: " <<
to_string(constraint)
2191 <<
", str: " <<
format(pair.first) << eom;
2199 stream <<
"f is not linear: " <<
to_string(constraint)
2200 <<
", str: " <<
format(pair.first) << eom;
2208 stream <<
"Universal variable outside of index:" <<
to_string(constraint)
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
The type of an expression.
static void display_index_set(messaget::mstreamt &stream, const index_set_pairt &index_set)
Write index set to the given stream, use for debugging.
array_exprt concretize(std::size_t size, const typet &index_type) const
Convert to an array representation, ignores elements at index >= size.
static exprt sum_over_map(std::map< exprt, int > &m, const typet &type, bool negated=false)
static optionalt< exprt > find_counter_example(const namespacet &ns, ui_message_handlert::uit ui, const exprt &axiom, const symbol_exprt &var)
Creates a solver with axiom as the only formula added and runs it.
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'), str, and k, the function should return k+1.
static exprt instantiate(messaget::mstreamt &stream, const string_constraintt &axiom, const exprt &str, const exprt &val)
Substitute qvar the universally quantified variable of axiom, by an index val, in axiom...
void add_constraints(string_constraint_generatort &generatort)
For all builtin call on which a test (or an unsupported buitin) result depends, add the corresponding...
const std::set< array_string_exprt > & get_created_strings() const
Set of strings that have been created by the generator.
A generic base class for relations, i.e., binary predicates.
const std::string & id2string(const irep_idt &d)
virtual exprt to_if_expression(const exprt &index) const
Creates an if_expr corresponding to the result of accessing the array at the given index...
std::vector< equal_exprt > equations
std::map< exprt, std::vector< exprt > > array_index_mapt
literalt convert(const exprt &expr) override
const exprt & univ_lower_bound() const
const std::vector< string_constraintt > & get_constraints() const
bool equality_propagation
exprt get_witness_of(const string_not_contains_constraintt &c, const exprt &univ_val) const
exprt simplify_expr(const exprt &src, const namespacet &ns)
void clean_cache()
Clean the cache used by eval
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
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.
Deprecated expression utility functions.
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...
const std::vector< exprt > & get_lemmas() const
Axioms are of three kinds: universally quantified string constraint, not contains string constraints ...
const irep_idt & get_identifier() const
bool replace_expr(exprt &expr) const
Replace subexpressions of expr by a canonical element of the set they belong to.
string_refinementt constructor arguments
bool is_char_pointer_type(const typet &type)
For now, any unsigned bitvector type is considered a character.
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
std::map< exprt, std::set< exprt > > current
const componentst & components() const
symbol_exprt fresh_univ_index(const irep_idt &prefix, const typet &type)
generate an index symbol to be used as an universaly quantified variable
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.
exprt get_length(const array_string_exprt &s) const
Associate an actual finite length to infinite arrays.
The trinary if-then-else operator.
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)
exprt to_if_expression(const exprt &index) const override
Creates an if_expr corresponding to the result of accessing the array at the given index...
const std::vector< string_not_contains_constraintt > & get_not_contains_constraints() const
depth_iteratort depth_begin()
exprt univ_within_bounds() const
static union_find_replacet generate_symbol_resolution_from_equations(const std::vector< equal_exprt > &equations, const namespacet &ns, messaget::mstreamt &stream)
Add association for each char pointer in the equation.
Magic numbers used throughout the codebase.
A constant literal expression.
static bool validate(const string_refinementt::infot &info)
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.
static mstreamt & eom(mstreamt &m)
void clear_constraints()
Clear all constraints and lemmas.
#define INVARIANT(CONDITION, REASON)
void l_set_to_true(literalt a)
exprt substitute_array_lists(exprt expr, size_t string_max_length)
Replace array-lists by 'with' expressions.
const std::vector< symbol_exprt > & get_boolean_symbols() const
Boolean symbols for the results of some string functions.
Extract member of struct or union.
void operator()(const exprt &expr) override
string_dependenciest dependencies
string_refinementt(const infot &)
#define CHARACTER_FOR_UNKNOWN
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.
bool can_cast_expr< function_application_exprt >(const exprt &base)
exprt conjunction(const exprt::operandst &op)
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 ...
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.
const exprt & exists_lower_bound() const
const irep_idt & id() const
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
exprt make_union(const exprt &a, const exprt &b)
Keeps a map of symbols to expressions, such as none of the mapped values exist as a key...
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 visit(class expr_visitort &visitor)
void debug_model(const string_constraint_generatort &generator, messaget::mstreamt &stream, const namespacet &ns, const std::size_t max_string_length, const std::function< exprt(const exprt &)> &super_get, const std::vector< symbol_exprt > &boolean_symbols, const std::vector< symbol_exprt > &index_symbols)
Display part of the current model by mapping the variables created by the solver to constant expressi...
An expression denoting infinity.
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 string_constraint_generatort &generator)
Instantiates a quantified formula representing not_contains by substituting the quantifiers and gener...
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...
Constraints to encode non containement of strings.
static exprt get_char_array_and_concretize(const std::function< exprt(const exprt &)> &super_get, const namespacet &ns, const std::size_t max_string_length, 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...
int solver(std::istream &in)
std::map< exprt, std::set< exprt > > cumulative
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...
Represents arrays by the indexes up to which the value remains the same.
exprt simplify_sum(const exprt &f)
static bool is_valid_string_constraint(messaget::mstreamt &stream, const namespacet &ns, const string_constraintt &constraint)
Checks the data invariant for string_constraintt.
nonstd::optional< T > optionalt
void add(const std::size_t i, const exprt &expr)
Record the fact that equation i contains expression expr
union_find_replacet symbol_resolve
Represents arrays of the form array_of(x) with {i:=a} with {j:=b} ... by a default value x and a list...
const std::size_t MAX_CONCRETE_STRING_SIZE
static bool is_valid_string_constraint(messaget::mstreamt &stream, const namespacet &ns, const string_constraintt &constraint)
#define PRECONDITION(CONDITION)
#define forall_operands(it, expr)
std::vector< exprt > instantiate_not_contains(const string_not_contains_constraintt &axiom, const std::set< std::pair< exprt, exprt >> &index_pairs, const string_constraint_generatort &generator)
bool has_char_pointer_subtype(const typet &type, const namespacet &ns)
std::size_t max_string_length
array constructor from single element
bitvector_typet index_type()
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
const exprt & premise() const
decision_proceduret::resultt dec_solve() override
The unary minus expression.
static void debug_check_axioms_step(messaget::mstreamt &stream, const namespacet &ns, 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...
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
decision_proceduret::resultt dec_solve() override
Main decision procedure of the solver.
static bool is_linear_arithmetic_expr(const exprt &expr, const symbol_exprt &var)
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 bool find_qvar(const exprt &index, const symbol_exprt &qvar)
look for the symbol and return true if it is found
string_constraint_generatort generator
const std::unordered_map< exprt, array_string_exprt, irep_hash > & get_arrays_of_pointers() const
std::vector< exprt > operandst
static std::vector< exprt > generate_instantiations(messaget::mstreamt &stream, const namespacet &ns, const string_constraint_generatort &generator, const index_set_pairt &index_set, const string_axiomst &axioms)
Instantiation of all constraints.
void output_equations(std::ostream &output, const std::vector< equal_exprt > &equations, const namespacet &ns)
Output a vector of equations to the given stream, used for debugging.
String support via creating string constraints and progressively instantiating the universal constrai...
std::vector< string_constraintt > universal
bool has_char_array_subexpr(const exprt &expr, const namespacet &ns)
static optionalt< exprt > get_array(const std::function< exprt(const exprt &)> &super_get, const namespacet &ns, const std::size_t max_string_length, messaget::mstreamt &stream, const array_string_exprt &arr)
Get a model of an array and put it in a certain form.
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...
static void initial_index_set(index_set_pairt &index_set, const namespacet &ns, const string_constraintt &axiom)
const equal_exprt & to_equal_expr(const exprt &expr)
Cast a generic exprt to an equal_exprt.
exprt get(const exprt &expr) const override
Similar interface to union-find for expressions, with a function for replacing sub-expressions by the...
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, std::size_t max_string_length, bool use_counter_example, ui_message_handlert::uit ui, const union_find_replacet &symbol_resolve)
Check axioms takes the model given by the underlying solver and answers whether it satisfies the stri...
std::vector< exprt > find_expressions(const std::size_t i)
Maps equation to expressions contained in them and conversely expressions to equations that contain t...
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 std::string string_of_array(const array_exprt &arr)
convert the content of a string to a more readable representation.
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
const exprt & exists_upper_bound() const
Base class for all expressions.
static std::vector< exprt > extract_strings(const exprt &expr)
optionalt< exprt > make_array_pointer_association(const function_application_exprt &expr)
Associate array to pointer, and array to length.
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...
std::set< exprt > seen_instances
Operator to update elements in structs and arrays.
std::string to_string(const string_constraintt &expr)
Used for debug printing.
static std::map< exprt, int > map_representation_of_sum(const exprt &f)
#define string_refinement_invariantt(reason)
Universally quantified string constraint
const exprt & univ_upper_bound() const
static optionalt< interval_sparse_arrayt > of_expr(const exprt &expr, const exprt &extra_value)
If the expression is an array_exprt or a with_exprt uses the appropriate constructor, otherwise returns empty optional.
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.
Expression to hold a symbol (variable)
depth_iteratort depth_end()
exprt get(const exprt &expr) const override
Evaluates the given expression in the valuation found by string_refinementt::dec_solve.
std::string utf16_constant_array_to_java(const array_exprt &arr, std::size_t length)
Construct a string from a constant array.
const typet & subtype() const
#define DATA_INVARIANT(CONDITION, REASON)
void set_to(const exprt &expr, bool value) override
std::map< string_not_contains_constraintt, symbol_exprt > witness
const array_string_exprt & s0() const
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 is_char_array_type(const typet &type, const namespacet &ns)
Distinguish char array from other types.
std::vector< std::size_t > find_equations(const exprt &expr)
const std::vector< symbol_exprt > & get_index_symbols() const
Symbols used in existential quantifications.
std::vector< exprt > current_constraints
static array_index_mapt gather_indices(const exprt &expr)
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
bitvector_typet char_type()
array constructor from list of elements
void replace_symbols_in_equations(const union_find_replacet &symbol_resolve, std::vector< equal_exprt > &equations)
index_set_pairt index_sets
std::vector< string_not_contains_constraintt > not_contains
std::vector< std::pair< exprt, exprt > > to_vector() const
array_string_exprt & to_array_string_expr(exprt &expr)
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.
static exprt compute_inverse_function(messaget::mstreamt &stream, const exprt &qvar, const exprt &val, const exprt &f)
bool simplify(exprt &expr, const namespacet &ns)
symbol_generatort fresh_symbol
void output_dot(std::ostream &stream) const
void add_lemma(const exprt &lemma, bool simplify_lemma=true)
Add the given lemma to the solver.
const array_string_exprt & s1() const
find_qvar_visitort(const exprt &qvar)