cprover
Loading...
Searching...
No Matches
string_refinement.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: String support via creating string constraints and progressively
4 instantiating the universal constraints as needed.
5 The procedure is described in the PASS paper at HVC'13:
6 "PASS: String Solving with Parameterized Array and Interval Automaton"
7 by Guodong Li and Indradeep Ghosh.
8
9Author: Alberto Griggio, alberto.griggio@gmail.com
10
11\*******************************************************************/
12
19
20#include "string_refinement.h"
21
23#include <stack>
24#include <unordered_set>
25
26#include <util/expr_iterator.h>
27#include <util/expr_util.h>
28#include <util/format_type.h>
29#include <util/magic.h>
30#include <util/range.h>
31#include <util/simplify_expr.h>
32
35#include "string_dependencies.h"
37
39 messaget::mstreamt &stream,
40 const namespacet &ns,
41 const string_constraintt &constraint);
42
44 const namespacet &ns,
45 const exprt &axiom,
46 const symbol_exprt &var,
47 message_handlert &message_handler);
48
65static std::pair<bool, std::vector<exprt>> check_axioms(
66 const string_axiomst &axioms,
68 const std::function<exprt(const exprt &)> &get,
69 messaget::mstreamt &stream,
70 const namespacet &ns,
71 bool use_counter_example,
72 const union_find_replacet &symbol_resolve,
73 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
74 &not_contain_witnesses);
75
76static void initial_index_set(
77 index_set_pairt &index_set,
78 const namespacet &ns,
79 const string_constraintt &axiom);
80
81static void initial_index_set(
82 index_set_pairt &index_set,
83 const namespacet &ns,
85
86static void initial_index_set(
87 index_set_pairt &index_set,
88 const namespacet &ns,
89 const string_axiomst &axioms);
90
91exprt simplify_sum(const exprt &f);
92
93static void update_index_set(
94 index_set_pairt &index_set,
95 const namespacet &ns,
96 const std::vector<exprt> &current_constraints);
97
98static void update_index_set(
99 index_set_pairt &index_set,
100 const namespacet &ns,
101 const exprt &formula);
102
103static std::vector<exprt> instantiate(
105 const index_set_pairt &index_set,
106 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
107 &witnesses);
108
110 const std::function<exprt(const exprt &)> &super_get,
111 const namespacet &ns,
112 messaget::mstreamt &stream,
113 const array_string_exprt &arr,
114 const array_poolt &array_pool);
115
117 const index_exprt &index_expr,
118 symbol_generatort &symbol_generator,
119 const bool left_propagate);
120
128template <typename T>
129static std::vector<T>
130fill_in_map_as_vector(const std::map<std::size_t, T> &index_value)
131{
132 std::vector<T> result;
133 if(!index_value.empty())
134 {
135 result.resize(index_value.rbegin()->first + 1);
136 for(auto it = index_value.rbegin(); it != index_value.rend(); ++it)
137 {
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++)
144 result[j] = value;
145 }
146 }
147 return result;
148}
149
150static bool validate(const string_refinementt::infot &info)
151{
152 PRECONDITION(info.ns);
153 PRECONDITION(info.prop);
154 return true;
155}
156
158 : supert(info),
159 config_(info),
160 loop_bound_(info.refinement_bound),
161 generator(*info.ns, *info.message_handler)
162{
163}
164
169
171static void
173{
174 std::size_t count = 0;
175 std::size_t count_current = 0;
176 for(const auto &i : index_set.cumulative)
177 {
178 const exprt &s = i.first;
179 stream << "IS(" << format(s) << ")=={" << messaget::eom;
180
181 for(const auto &j : i.second)
182 {
183 const auto it = index_set.current.find(i.first);
184 if(
185 it != index_set.current.end() && it->second.find(j) != it->second.end())
186 {
187 count_current++;
188 stream << "**";
189 }
190 stream << " " << format(j) << ";" << messaget::eom;
191 count++;
192 }
193 stream << "}" << messaget::eom;
194 }
195 stream << count << " elements in index set (" << count_current
196 << " newly added)" << messaget::eom;
197}
198
220static std::vector<exprt> generate_instantiations(
221 const index_set_pairt &index_set,
222 const string_axiomst &axioms,
223 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
224 &not_contain_witnesses)
225{
226 std::vector<exprt> lemmas;
227 for(const auto &i : index_set.current)
228 {
229 for(const auto &univ_axiom : axioms.universal)
230 {
231 for(const auto &j : i.second)
232 lemmas.push_back(instantiate(univ_axiom, i.first, j));
233 }
234 }
235 for(const auto &nc_axiom : axioms.not_contains)
236 {
237 for(const auto &instance :
238 instantiate(nc_axiom, index_set, not_contain_witnesses))
239 lemmas.push_back(instance);
240 }
241 return lemmas;
242}
243
249 exprt &expr)
250{
251 if(const auto equal_expr = expr_try_dynamic_cast<equal_exprt>(expr))
252 {
253 if(
255 as_const(equal_expr->rhs())))
256 {
257 const auto new_equation =
258 generator.make_array_pointer_association(equal_expr->lhs(), *fun_app);
259 if(new_equation)
260 {
261 expr =
262 equal_exprt{from_integer(true, new_equation->type()), *new_equation};
263 }
264 }
265 }
266}
267
272static exprt
273replace_expr_copy(const union_find_replacet &symbol_resolve, exprt expr)
274{
275 symbol_resolve.replace_expr(expr);
276 return expr;
277}
278
283void string_refinementt::set_to(const exprt &expr, bool value)
284{
285 PRECONDITION(expr.is_boolean());
287 if(!value)
288 equations.push_back(not_exprt{expr});
289 else
290 equations.push_back(expr);
291}
292
301 union_find_replacet &symbol_solver,
302 const std::vector<exprt> &equations,
303 const namespacet &ns,
304 messaget::mstreamt &stream)
305{
306 const std::string log_message =
307 "WARNING string_refinement.cpp generate_symbol_resolution_from_equations:";
308 auto equalities = make_range(equations).filter(
309 [&](const exprt &e) { return can_cast_expr<equal_exprt>(e); });
310 for(const exprt &e : equalities)
311 {
312 const equal_exprt &eq = to_equal_expr(e);
313 const exprt &lhs = to_equal_expr(eq).lhs();
314 const exprt &rhs = to_equal_expr(eq).rhs();
315 if(lhs.id() != ID_symbol)
316 {
317 stream << log_message << "non symbol lhs: " << format(lhs)
318 << " with rhs: " << format(rhs) << messaget::eom;
319 continue;
320 }
321
322 if(lhs.type() != rhs.type())
323 {
324 stream << log_message << "non equal types lhs: " << format(lhs)
325 << "\n####################### rhs: " << format(rhs)
326 << messaget::eom;
327 continue;
328 }
329
330 if(is_char_pointer_type(rhs.type()))
331 {
332 symbol_solver.make_union(lhs, simplify_expr(rhs, ns));
333 }
334 else if(rhs.id() == ID_function_application)
335 {
336 // function applications can be ignored because they will be replaced
337 // in the convert_function_application step of dec_solve
338 }
339 else if(
340 lhs.type().id() != ID_pointer && has_char_pointer_subtype(lhs.type(), ns))
341 {
342 if(rhs.type().id() == ID_struct || rhs.type().id() == ID_struct_tag)
343 {
344 const struct_typet &struct_type = to_struct_type(ns.follow(rhs.type()));
345 for(const auto &comp : struct_type.components())
346 {
347 if(is_char_pointer_type(comp.type()))
348 {
349 const member_exprt lhs_data(lhs, comp.get_name(), comp.type());
350 const exprt rhs_data = simplify_expr(
351 member_exprt(rhs, comp.get_name(), comp.type()), ns);
352 symbol_solver.make_union(lhs_data, rhs_data);
353 }
354 }
355 }
356 else
357 {
358 stream << log_message << "non struct with char pointer subexpr "
359 << format(rhs) << "\n * of type " << format(rhs.type())
360 << messaget::eom;
361 }
362 }
363 }
364}
365
372static std::vector<exprt>
374{
375 std::vector<exprt> result;
376 if(lhs.type() == string_typet())
377 result.push_back(lhs);
378 else if(lhs.type().id() == ID_struct || lhs.type().id() == ID_struct_tag)
379 {
380 const struct_typet &struct_type = to_struct_type(ns.follow(lhs.type()));
381 for(const auto &comp : struct_type.components())
382 {
383 const std::vector<exprt> strings_in_comp = extract_strings_from_lhs(
384 member_exprt(lhs, comp.get_name(), comp.type()), ns);
385 result.insert(
386 result.end(), strings_in_comp.begin(), strings_in_comp.end());
387 }
388 }
389 return result;
390}
391
397static std::vector<exprt>
398extract_strings(const exprt &expr, const namespacet &ns)
399{
400 std::vector<exprt> result;
401 for(auto it = expr.depth_begin(); it != expr.depth_end();)
402 {
403 if(it->type() == string_typet() && it->id() != ID_if)
404 {
405 result.push_back(*it);
406 it.next_sibling_or_parent();
407 }
408 else if(it->id() == ID_symbol)
409 {
410 for(const exprt &e : extract_strings_from_lhs(*it, ns))
411 result.push_back(e);
412 it.next_sibling_or_parent();
413 }
414 else
415 ++it;
416 }
417 return result;
418}
419
427 const equal_exprt &eq,
428 union_find_replacet &symbol_resolve,
429 const namespacet &ns)
430{
431 if(eq.rhs().type() == string_typet())
432 {
433 symbol_resolve.make_union(eq.lhs(), simplify_expr(eq.rhs(), ns));
434 }
435 else if(has_subtype(eq.lhs().type(), ID_string, ns))
436 {
437 if(
438 eq.rhs().type().id() == ID_struct ||
439 eq.rhs().type().id() == ID_struct_tag)
440 {
441 const struct_typet &struct_type =
442 to_struct_type(ns.follow(eq.rhs().type()));
443 for(const auto &comp : struct_type.components())
444 {
445 const member_exprt lhs_data(eq.lhs(), comp.get_name(), comp.type());
446 const exprt rhs_data = simplify_expr(
447 member_exprt(eq.rhs(), comp.get_name(), comp.type()), ns);
449 equal_exprt(lhs_data, rhs_data), symbol_resolve, ns);
450 }
451 }
452 }
453}
454
463 const std::vector<equal_exprt> &equations,
464 const namespacet &ns,
465 messaget::mstreamt &stream)
466{
467 const std::string log_message =
468 "WARNING string_refinement.cpp "
469 "string_identifiers_resolution_from_equations:";
470
471 equation_symbol_mappingt equation_map;
472
473 // Indexes of equations that need to be added to the result
474 std::unordered_set<size_t> required_equations;
475 std::stack<size_t> equations_to_treat;
476
477 for(std::size_t i = 0; i < equations.size(); ++i)
478 {
479 const equal_exprt &eq = equations[i];
480 if(eq.rhs().id() == ID_function_application)
481 {
482 if(required_equations.insert(i).second)
483 equations_to_treat.push(i);
484
485 std::vector<exprt> rhs_strings = extract_strings(eq.rhs(), ns);
486 for(const auto &expr : rhs_strings)
487 equation_map.add(i, expr);
488 }
489 else if(
490 eq.lhs().type().id() != ID_pointer &&
491 has_subtype(eq.lhs().type(), ID_string, ns))
492 {
493 std::vector<exprt> lhs_strings = extract_strings_from_lhs(eq.lhs(), ns);
494
495 for(const auto &expr : lhs_strings)
496 equation_map.add(i, expr);
497
498 if(lhs_strings.empty())
499 {
500 stream << log_message << "non struct with string subtype "
501 << format(eq.lhs()) << "\n * of type "
502 << format(eq.lhs().type()) << messaget::eom;
503 }
504
505 for(const exprt &expr : extract_strings(eq.rhs(), ns))
506 equation_map.add(i, expr);
507 }
508 }
509
510 // transitively add all equations which depend on the equations to treat
511 while(!equations_to_treat.empty())
512 {
513 const std::size_t i = equations_to_treat.top();
514 equations_to_treat.pop();
515 for(const exprt &string : equation_map.find_expressions(i))
516 {
517 for(const std::size_t j : equation_map.find_equations(string))
518 {
519 if(required_equations.insert(j).second)
520 equations_to_treat.push(j);
521 }
522 }
523 }
524
525 union_find_replacet result;
526 for(const std::size_t i : required_equations)
527 add_string_equation_to_symbol_resolution(equations[i], result, ns);
528
529 return result;
530}
531
532#ifdef DEBUG
534static void
535output_equations(std::ostream &output, const std::vector<exprt> &equations)
536{
537 for(std::size_t i = 0; i < equations.size(); ++i)
538 output << " [" << i << "] " << format(equations[i]) << std::endl;
539}
540#endif
541
552// NOLINTNEXTLINE
555// NOLINTNEXTLINE
560// NOLINTNEXTLINE
607{
608#ifdef DEBUG
609 log.debug() << "dec_solve: Initial set of equations" << messaget::eom;
610 output_equations(log.debug(), equations);
611#endif
612
613 log.debug() << "dec_solve: Build symbol solver from equations"
614 << messaget::eom;
615 // symbol_resolve is used by get and is kept between calls to dec_solve,
616 // that's why we use a class member here
619#ifdef DEBUG
620 log.debug() << "symbol resolve:" << messaget::eom;
621 for(const auto &pair : symbol_resolve.to_vector())
622 log.debug() << format(pair.first) << " --> " << format(pair.second)
623 << messaget::eom;
624#endif
625
626 const union_find_replacet string_id_symbol_resolve =
628 [&] {
629 std::vector<equal_exprt> equalities;
630 for(const auto &eq : equations)
631 {
632 if(auto equal_expr = expr_try_dynamic_cast<equal_exprt>(eq))
633 equalities.push_back(*equal_expr);
634 }
635 return equalities;
636 }(),
637 ns,
638 log.debug());
639#ifdef DEBUG
640 log.debug() << "symbol resolve string:" << messaget::eom;
641 for(const auto &pair : string_id_symbol_resolve.to_vector())
642 {
643 log.debug() << format(pair.first) << " --> " << format(pair.second)
644 << messaget::eom;
645 }
646#endif
647
648 log.debug() << "dec_solve: Replacing string ids and simplifying arguments"
649 " in function applications"
650 << messaget::eom;
651 for(exprt &expr : equations)
652 {
653 auto it = expr.depth_begin();
654 while(it != expr.depth_end())
655 {
657 {
658 // Simplification is required because the array pool may not realize
659 // that an expression like
660 // `(unsignedbv[16]*)((signedbv[8]*)&constarray[0] + 0)` is the
661 // same pointer as `&constarray[0]
662 simplify(it.mutate(), ns);
663 string_id_symbol_resolve.replace_expr(it.mutate());
664 it.next_sibling_or_parent();
665 }
666 else
667 ++it;
668 }
669 }
670
671 // Constraints start clear at each `dec_solve` call.
672 string_constraintst constraints;
673 for(auto &expr : equations)
675
676#ifdef DEBUG
677 output_equations(log.debug(), equations);
678#endif
679
680 log.debug() << "dec_solve: compute dependency graph and remove function "
681 << "applications captured by the dependencies:" << messaget::eom;
682 std::vector<exprt> local_equations;
683 for(const exprt &eq : equations)
684 {
685 // Ensures that arrays that are equal, are associated to the same nodes
686 // in the graph.
687 const exprt eq_with_char_array_replaced_with_representative_elements =
689 const optionalt<exprt> new_equation = add_node(
691 eq_with_char_array_replaced_with_representative_elements,
694 if(new_equation)
695 local_equations.push_back(*new_equation);
696 else
697 local_equations.push_back(eq);
698 }
699 equations.clear();
700
701#ifdef DEBUG
703#endif
704
705 log.debug() << "dec_solve: add constraints" << messaget::eom;
706 merge(
707 constraints,
709
710#ifdef DEBUG
711 output_equations(log.debug(), equations);
712#endif
713
714#ifdef DEBUG
715 log.debug() << "dec_solve: arrays_of_pointers:" << messaget::eom;
717 {
718 log.debug() << " * " << format(pair.first) << "\t--> "
719 << format(pair.second) << " : " << format(pair.second.type())
720 << messaget::eom;
721 }
722#endif
723
724 for(const auto &eq : local_equations)
725 {
726#ifdef DEBUG
727 log.debug() << "dec_solve: set_to " << format(eq) << messaget::eom;
728#endif
729 supert::set_to(eq, true);
730 }
731
732 std::transform(
733 constraints.universal.begin(),
734 constraints.universal.end(),
735 std::back_inserter(axioms.universal),
736 [&](string_constraintt constraint) {
737 constraint.replace_expr(symbol_resolve);
738 DATA_INVARIANT(
739 is_valid_string_constraint(log.error(), ns, constraint),
740 string_refinement_invariantt(
741 "string constraints satisfy their invariant"));
742 return constraint;
743 });
744
745 std::transform(
746 constraints.not_contains.begin(),
747 constraints.not_contains.end(),
748 std::back_inserter(axioms.not_contains),
750 replace(symbol_resolve, axiom);
751 return axiom;
752 });
753
754 // Used to store information about witnesses for not_contains constraints
755 std::unordered_map<string_not_contains_constraintt, symbol_exprt>
756 not_contain_witnesses;
757 for(const auto &nc_axiom : axioms.not_contains)
758 {
759 const auto &witness_type = [&] {
760 const auto &rtype = to_array_type(nc_axiom.s0.type());
761 const typet &index_type = rtype.size().type();
763 }();
764 not_contain_witnesses.emplace(
765 nc_axiom, generator.fresh_symbol("not_contains_witness", witness_type));
766 }
767
768 for(const exprt &lemma : constraints.existential)
769 {
771 }
772
773 // All generated strings should have non-negative length
774 for(const auto &pair : generator.array_pool.created_strings())
775 {
776 exprt length = generator.array_pool.get_or_create_length(pair.first);
777 add_lemma(
778 binary_relation_exprt{length, ID_ge, from_integer(0, length.type())});
779 }
780
781 // Initial try without index set
782 const auto get = [this](const exprt &expr) { return this->get(expr); };
784 const decision_proceduret::resultt initial_result = supert::dec_solve();
785 if(initial_result == resultt::D_SATISFIABLE)
786 {
787 bool satisfied;
788 std::vector<exprt> counter_examples;
789 std::tie(satisfied, counter_examples) = check_axioms(
790 axioms,
791 generator,
792 get,
793 log.debug(),
794 ns,
797 not_contain_witnesses);
798 if(satisfied)
799 {
800 log.debug() << "check_SAT: the model is correct" << messaget::eom;
802 }
803 log.debug() << "check_SAT: got SAT but the model is not correct"
804 << messaget::eom;
805 }
806 else
807 {
808 log.debug() << "check_SAT: got UNSAT or ERROR" << messaget::eom;
809 return initial_result;
810 }
811
814 current_constraints.clear();
815 const auto initial_instances =
816 generate_instantiations(index_sets, axioms, not_contain_witnesses);
817 for(const auto &instance : initial_instances)
818 {
820 }
821
822 while((loop_bound_--) > 0)
823 {
825 const decision_proceduret::resultt refined_result = supert::dec_solve();
826
827 if(refined_result == resultt::D_SATISFIABLE)
828 {
829 bool satisfied;
830 std::vector<exprt> counter_examples;
831 std::tie(satisfied, counter_examples) = check_axioms(
832 axioms,
833 generator,
834 get,
835 log.debug(),
836 ns,
839 not_contain_witnesses);
840 if(satisfied)
841 {
842 log.debug() << "check_SAT: the model is correct" << messaget::eom;
844 }
845
846 log.debug()
847 << "check_SAT: got SAT but the model is not correct, refining..."
848 << messaget::eom;
849
850 // Since the model is not correct although we got SAT, we need to refine
851 // the property we are checking by adding more indices to the index set,
852 // and instantiating universal formulas with this indices.
853 // We will then relaunch the solver with these added lemmas.
854 index_sets.current.clear();
856
858
859 if(index_sets.current.empty())
860 {
861 if(axioms.not_contains.empty())
862 {
863 log.error() << "dec_solve: current index set is empty, "
864 << "this should not happen" << messaget::eom;
865 return resultt::D_ERROR;
866 }
867 else
868 {
869 log.debug() << "dec_solve: current index set is empty, "
870 << "adding counter examples" << messaget::eom;
871 for(const auto &counter : counter_examples)
872 add_lemma(counter);
873 }
874 }
875 current_constraints.clear();
876 const auto instances =
877 generate_instantiations(index_sets, axioms, not_contain_witnesses);
878 for(const auto &instance : instances)
879 add_lemma(
881 }
882 else
883 {
884 log.debug() << "check_SAT: default return "
885 << static_cast<int>(refined_result) << messaget::eom;
886 return refined_result;
887 }
888 }
889 log.debug() << "string_refinementt::dec_solve reached the maximum number"
890 << "of steps allowed" << messaget::eom;
891 return resultt::D_ERROR;
892}
898 const exprt &lemma,
899 const bool simplify_lemma)
900{
901 if(!seen_instances.insert(lemma).second)
902 return;
903
904 current_constraints.push_back(lemma);
905
906 exprt simple_lemma = lemma;
907 if(simplify_lemma)
908 {
909 simplify(simple_lemma, ns);
910 }
911
912 if(simple_lemma.is_true())
913 {
914#if 0
915 log.debug() << "string_refinementt::add_lemma : tautology" << messaget::eom;
916#endif
917 return;
918 }
919
920 symbol_resolve.replace_expr(simple_lemma);
921
922 // Replace empty arrays with array_of expression because the solver cannot
923 // handle empty arrays.
924 for(auto it = simple_lemma.depth_begin(); it != simple_lemma.depth_end();)
925 {
926 if(it->id() == ID_array && it->operands().empty())
927 {
928 it.mutate() = array_of_exprt(
931 to_array_type(it->type()));
932 it.next_sibling_or_parent();
933 }
934 else
935 ++it;
936 }
937
938 log.debug() << "adding lemma " << format(simple_lemma) << messaget::eom;
939
940 prop.l_set_to_true(convert(simple_lemma));
941}
942
958 const std::function<exprt(const exprt &)> &super_get,
959 const namespacet &ns,
960 messaget::mstreamt &stream,
961 const array_string_exprt &arr,
962 const array_poolt &array_pool)
963{
964 const auto &size_from_pool = array_pool.get_length_if_exists(arr);
965 exprt size_val;
966 if(size_from_pool.has_value())
967 {
968 const exprt size = size_from_pool.value();
969 size_val = simplify_expr(super_get(size), ns);
970 if(!size_val.is_constant())
971 {
972 stream << "(sr::get_valid_array_size) string of unknown size: "
973 << format(size_val) << messaget::eom;
974 return {};
975 }
976 }
977 else if(to_array_type(arr.type()).size().is_constant())
978 size_val = simplify_expr(to_array_type(arr.type()).size(), ns);
979 else
980 return {};
981
982 auto n_opt = numeric_cast<std::size_t>(size_val);
983 if(!n_opt)
984 {
985 stream << "(sr::get_valid_array_size) size is not valid" << messaget::eom;
986 return {};
987 }
988
989 return size_val;
990}
991
1002 const std::function<exprt(const exprt &)> &super_get,
1003 const namespacet &ns,
1004 messaget::mstreamt &stream,
1005 const array_string_exprt &arr,
1006 const array_poolt &array_pool)
1007{
1008 const auto size =
1009 get_valid_array_size(super_get, ns, stream, arr, array_pool);
1010 if(!size.has_value())
1011 {
1012 return {};
1013 }
1014
1015 const size_t n = numeric_cast<std::size_t>(size.value()).value();
1016
1018 {
1019 stream << "(sr::get_valid_array_size) long string (size "
1020 << " = " << n << ") " << format(arr) << messaget::eom;
1021 stream << "(sr::get_valid_array_size) consider reducing "
1022 "max-nondet-string-length so "
1023 "that no string exceeds "
1025 << " in length and "
1026 "make sure all functions returning strings are loaded"
1027 << messaget::eom;
1028 stream << "(sr::get_valid_array_size) this can also happen on invalid "
1029 "object access"
1030 << messaget::eom;
1031 return nil_exprt();
1032 }
1033
1034 const exprt arr_val = simplify_expr(super_get(arr), ns);
1036 const typet &index_type = size.value().type();
1037
1038 if(
1039 const auto &array = interval_sparse_arrayt::of_expr(
1041 return array->concretize(n, index_type);
1042 return {};
1043}
1044
1049static std::string string_of_array(const array_exprt &arr)
1050{
1051 if(arr.type().id() != ID_array)
1052 return std::string("");
1053
1054 exprt size_expr = to_array_type(arr.type()).size();
1055 auto n = numeric_cast_v<std::size_t>(to_constant_expr(size_expr));
1056 return utf16_constant_array_to_java(arr, n);
1057}
1058
1068 const std::function<exprt(const exprt &)> &super_get,
1069 const namespacet &ns,
1070 messaget::mstreamt &stream,
1071 const array_string_exprt &arr,
1072 array_poolt &array_pool)
1073{
1074 stream << "- " << format(arr) << ":\n";
1075 stream << std::string(4, ' ') << "- type: " << format(arr.type())
1076 << messaget::eom;
1077 const auto arr_model_opt = get_array(super_get, ns, stream, arr, array_pool);
1078 if(arr_model_opt)
1079 {
1080 stream << std::string(4, ' ') << "- char_array: " << format(*arr_model_opt)
1081 << '\n';
1082 stream << std::string(4, ' ')
1083 << "- type : " << format(arr_model_opt->type()) << messaget::eom;
1084 const exprt simple = simplify_expr(*arr_model_opt, ns);
1085 stream << std::string(4, ' ')
1086 << "- simplified_char_array: " << format(simple) << messaget::eom;
1087 if(
1088 const auto concretized_array = get_array(
1089 super_get, ns, stream, to_array_string_expr(simple), array_pool))
1090 {
1091 stream << std::string(4, ' ')
1092 << "- concretized_char_array: " << format(*concretized_array)
1093 << messaget::eom;
1094
1095 if(
1096 const auto array_expr =
1097 expr_try_dynamic_cast<array_exprt>(*concretized_array))
1098 {
1099 stream << std::string(4, ' ') << "- as_string: \""
1100 << string_of_array(*array_expr) << "\"\n";
1101 }
1102 else
1103 stream << std::string(2, ' ') << "- warning: not an array"
1104 << messaget::eom;
1105 return *concretized_array;
1106 }
1107 return simple;
1108 }
1109 stream << std::string(4, ' ') << "- incomplete model" << messaget::eom;
1110 return arr;
1111}
1112
1116 const string_constraint_generatort &generator,
1117 messaget::mstreamt &stream,
1118 const namespacet &ns,
1119 const std::function<exprt(const exprt &)> &super_get,
1120 const std::vector<symbol_exprt> &symbols,
1121 array_poolt &array_pool)
1122{
1123 stream << "debug_model:" << '\n';
1124 for(const auto &pointer_array : generator.array_pool.get_arrays_of_pointers())
1125 {
1126 const auto arr = pointer_array.second;
1127 const exprt model =
1128 get_char_array_and_concretize(super_get, ns, stream, arr, array_pool);
1129
1130 stream << "- " << format(arr) << ":\n"
1131 << " - pointer: " << format(pointer_array.first) << "\n"
1132 << " - model: " << format(model) << messaget::eom;
1133 }
1134
1135 for(const auto &symbol : symbols)
1136 {
1137 stream << " - " << symbol.get_identifier() << ": "
1138 << format(super_get(symbol)) << '\n';
1139 }
1140 stream << messaget::eom;
1141}
1142
1156 const with_exprt &expr,
1157 const exprt &index,
1158 const bool left_propagate)
1159{
1160 return left_propagate ? interval_sparse_arrayt(expr).to_if_expression(index)
1161 : sparse_arrayt::to_if_expression(expr, index);
1162}
1163
1171 const array_exprt &array_expr,
1172 const exprt &index,
1173 symbol_generatort &symbol_generator)
1174{
1175 const typet &char_type = array_expr.type().element_type();
1176 const exprt default_val = symbol_generator("out_of_bound_access", char_type);
1177 const interval_sparse_arrayt sparse_array(array_expr, default_val);
1178 return sparse_array.to_if_expression(index);
1179}
1180
1182 const if_exprt &if_expr,
1183 const exprt &index,
1184 symbol_generatort &symbol_generator,
1185 const bool left_propagate)
1186{
1187 exprt true_index = index_exprt(if_expr.true_case(), index);
1188 exprt false_index = index_exprt(if_expr.false_case(), index);
1189
1190 // Substitute recursively in branches of conditional expressions
1191 optionalt<exprt> substituted_true_case =
1192 substitute_array_access(true_index, symbol_generator, left_propagate);
1193 optionalt<exprt> substituted_false_case =
1194 substitute_array_access(false_index, symbol_generator, left_propagate);
1195
1196 return if_exprt(
1197 if_expr.cond(),
1198 substituted_true_case ? *substituted_true_case : true_index,
1199 substituted_false_case ? *substituted_false_case : false_index);
1200}
1201
1203 const index_exprt &index_expr,
1204 symbol_generatort &symbol_generator,
1205 const bool left_propagate)
1206{
1207 const exprt &array = index_expr.array();
1208 if(auto array_of = expr_try_dynamic_cast<array_of_exprt>(array))
1209 return array_of->op();
1210 if(auto array_with = expr_try_dynamic_cast<with_exprt>(array))
1212 *array_with, index_expr.index(), left_propagate);
1213 if(auto array_expr = expr_try_dynamic_cast<array_exprt>(array))
1215 *array_expr, index_expr.index(), symbol_generator);
1216 if(auto if_expr = expr_try_dynamic_cast<if_exprt>(array))
1218 *if_expr, index_expr.index(), symbol_generator, left_propagate);
1219
1220 INVARIANT(
1221 array.is_nil() || array.id() == ID_symbol || array.id() == ID_nondet_symbol,
1222 std::string(
1223 "in case the array is unknown, it should be a symbol or nil, id: ") +
1224 id2string(array.id()));
1225 return {};
1226}
1227
1232 exprt &expr,
1233 symbol_generatort &symbol_generator,
1234 const bool left_propagate)
1235{
1236 // Recurse down structure and modify on the way.
1237 for(auto it = expr.depth_begin(), itend = expr.depth_end(); it != itend; ++it)
1238 {
1239 if(const auto index_expr = expr_try_dynamic_cast<index_exprt>(*it))
1240 {
1241 optionalt<exprt> result =
1242 substitute_array_access(*index_expr, symbol_generator, left_propagate);
1243
1244 // Only perform a write when we have something changed.
1245 if(result)
1246 it.mutate() = *result;
1247 }
1248 }
1249}
1250
1271 exprt expr,
1272 symbol_generatort &symbol_generator,
1273 const bool left_propagate)
1274{
1275 substitute_array_access_in_place(expr, symbol_generator, left_propagate);
1276 return expr;
1277}
1278
1290 const string_not_contains_constraintt &constraint,
1291 const symbol_exprt &univ_var,
1292 const std::function<exprt(const exprt &)> &get)
1293{
1294 // If the for all is vacuously true, the negation is false.
1295 const auto lbe = numeric_cast_v<mp_integer>(
1296 to_constant_expr(get(constraint.exists_lower_bound)));
1297 const auto ube = numeric_cast_v<mp_integer>(
1298 to_constant_expr(get(constraint.exists_upper_bound)));
1299 const auto univ_bounds = and_exprt(
1300 binary_relation_exprt(get(constraint.univ_lower_bound), ID_le, univ_var),
1301 binary_relation_exprt(get(constraint.univ_upper_bound), ID_gt, univ_var));
1302
1303 // The negated existential becomes an universal, and this is the unrolling of
1304 // that universal quantifier.
1305 // Ff the upper bound is smaller than the lower bound (specifically, it might
1306 // actually be negative as it is initially unconstrained) then there is
1307 // nothing to do (and the reserve call would fail).
1308 if(ube < lbe)
1309 return and_exprt(univ_bounds, get(constraint.premise));
1310
1311 std::vector<exprt> conjuncts;
1312 conjuncts.reserve(numeric_cast_v<std::size_t>(ube - lbe));
1313 for(mp_integer i = lbe; i < ube; ++i)
1314 {
1315 const constant_exprt i_expr = from_integer(i, univ_var.type());
1316 const exprt s0_char =
1317 get(index_exprt(constraint.s0, plus_exprt(univ_var, i_expr)));
1318 const exprt s1_char = get(index_exprt(constraint.s1, i_expr));
1319 conjuncts.push_back(equal_exprt(s0_char, s1_char));
1320 }
1321 const exprt equal_strings = conjunction(conjuncts);
1322 return and_exprt(univ_bounds, get(constraint.premise), equal_strings);
1323}
1324
1329template <typename T>
1331 messaget::mstreamt &stream,
1332 const T &axiom,
1333 const T &axiom_in_model,
1334 const exprt &negaxiom,
1335 const exprt &with_concretized_arrays)
1336{
1337 stream << std::string(4, ' ') << "- axiom:\n" << std::string(6, ' ');
1338 stream << to_string(axiom);
1339 stream << '\n'
1340 << std::string(4, ' ') << "- axiom_in_model:\n"
1341 << std::string(6, ' ');
1342 stream << to_string(axiom_in_model) << '\n'
1343 << std::string(4, ' ') << "- negated_axiom:\n"
1344 << std::string(6, ' ') << format(negaxiom) << '\n';
1345 stream << std::string(4, ' ') << "- negated_axiom_with_concretized_arrays:\n"
1346 << std::string(6, ' ') << format(with_concretized_arrays) << '\n';
1347}
1348
1350static std::pair<bool, std::vector<exprt>> check_axioms(
1351 const string_axiomst &axioms,
1353 const std::function<exprt(const exprt &)> &get,
1354 messaget::mstreamt &stream,
1355 const namespacet &ns,
1356 bool use_counter_example,
1357 const union_find_replacet &symbol_resolve,
1358 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
1359 &not_contain_witnesses)
1360{
1361 stream << "string_refinementt::check_axioms:" << messaget::eom;
1362
1363 stream << "symbol_resolve:" << messaget::eom;
1364 auto pairs = symbol_resolve.to_vector();
1365 for(const auto &pair : pairs)
1366 stream << " - " << format(pair.first) << " --> " << format(pair.second)
1367 << messaget::eom;
1368
1369#ifdef DEBUG
1371 generator,
1372 stream,
1373 ns,
1374 get,
1375 generator.fresh_symbol.created_symbols,
1376 generator.array_pool);
1377#endif
1378
1379 // Maps from indexes of violated universal axiom to a witness of violation
1380 std::map<size_t, exprt> violated;
1381
1382 stream << "string_refinement::check_axioms: " << axioms.universal.size()
1383 << " universal axioms:" << messaget::eom;
1384 for(size_t i = 0; i < axioms.universal.size(); i++)
1385 {
1386 const string_constraintt &axiom = axioms.universal[i];
1387 const string_constraintt axiom_in_model(
1388 axiom.univ_var,
1389 get(axiom.lower_bound),
1390 get(axiom.upper_bound),
1391 get(axiom.body),
1392 stream.message.get_message_handler());
1393
1394 exprt negaxiom = axiom_in_model.negation();
1395 negaxiom = simplify_expr(negaxiom, ns);
1396
1397 stream << std::string(2, ' ') << i << ".\n";
1398 const exprt with_concretized_arrays =
1399 substitute_array_access(negaxiom, generator.fresh_symbol, true);
1401 stream, axiom, axiom_in_model, negaxiom, with_concretized_arrays);
1402
1403 if(
1404 const auto &witness = find_counter_example(
1405 ns,
1406 with_concretized_arrays,
1407 axiom.univ_var,
1408 stream.message.get_message_handler()))
1409 {
1410 stream << std::string(4, ' ')
1411 << "- violated_for: " << format(axiom.univ_var) << "="
1412 << format(*witness) << messaget::eom;
1413 violated[i] = *witness;
1414 }
1415 else
1416 stream << std::string(4, ' ') << "- correct" << messaget::eom;
1417 }
1418
1419 // Maps from indexes of violated not_contains axiom to a witness of violation
1420 std::map<std::size_t, exprt> violated_not_contains;
1421
1422 stream << "there are " << axioms.not_contains.size() << " not_contains axioms"
1423 << messaget::eom;
1424 for(std::size_t i = 0; i < axioms.not_contains.size(); i++)
1425 {
1426 const string_not_contains_constraintt &nc_axiom = axioms.not_contains[i];
1427 const symbol_exprt univ_var = generator.fresh_symbol(
1428 "not_contains_univ_var", nc_axiom.s0.length_type());
1429 const exprt negated_axiom = negation_of_not_contains_constraint(
1430 nc_axiom, univ_var, [&](const exprt &expr) {
1431 return simplify_expr(get(expr), ns);
1432 });
1433
1434 stream << std::string(2, ' ') << i << ".\n";
1436 stream, nc_axiom, nc_axiom, negated_axiom, negated_axiom);
1437
1438 if(
1439 const auto witness = find_counter_example(
1440 ns, negated_axiom, univ_var, stream.message.get_message_handler()))
1441 {
1442 stream << std::string(4, ' ')
1443 << "- violated_for: " << univ_var.get_identifier() << "="
1444 << format(*witness) << messaget::eom;
1445 violated_not_contains[i] = *witness;
1446 }
1447 }
1448
1449 if(violated.empty() && violated_not_contains.empty())
1450 {
1451 stream << "no violated property" << messaget::eom;
1452 return {true, std::vector<exprt>()};
1453 }
1454 else
1455 {
1456 stream << violated.size() << " universal string axioms can be violated"
1457 << messaget::eom;
1458 stream << violated_not_contains.size()
1459 << " not_contains string axioms can be violated" << messaget::eom;
1460
1461 if(use_counter_example)
1462 {
1463 std::vector<exprt> lemmas;
1464
1465 for(const auto &v : violated)
1466 {
1467 const exprt &val = v.second;
1468 const string_constraintt &axiom = axioms.universal[v.first];
1469
1470 exprt instance(axiom.body);
1471 replace_expr(axiom.univ_var, val, instance);
1472 // We are not sure the index set contains only positive numbers
1473 and_exprt bounds(
1474 axiom.univ_within_bounds(),
1475 binary_relation_exprt(from_integer(0, val.type()), ID_le, val));
1476 replace_expr(axiom.univ_var, val, bounds);
1477 const implies_exprt counter(bounds, instance);
1478 lemmas.push_back(counter);
1479 }
1480
1481 for(const auto &v : violated_not_contains)
1482 {
1483 const exprt &val = v.second;
1484 const string_not_contains_constraintt &axiom =
1485 axioms.not_contains[v.first];
1486
1487 const exprt func_val =
1488 index_exprt(not_contain_witnesses.at(axiom), val);
1489 const exprt comp_val = simplify_sum(plus_exprt(val, func_val));
1490
1491 std::set<std::pair<exprt, exprt>> indices;
1492 indices.insert(std::pair<exprt, exprt>(comp_val, func_val));
1493 const exprt counter =
1494 ::instantiate_not_contains(axiom, indices, not_contain_witnesses)[0];
1495 lemmas.push_back(counter);
1496 }
1497 return {false, lemmas};
1498 }
1499 }
1500 return {false, std::vector<exprt>()};
1501}
1502
1506{
1507 return linear_functiont{f}.to_expr();
1508}
1509
1516 index_set_pairt &index_set,
1517 const namespacet &ns,
1518 const string_axiomst &axioms)
1519{
1520 for(const auto &axiom : axioms.universal)
1521 initial_index_set(index_set, ns, axiom);
1522 for(const auto &axiom : axioms.not_contains)
1523 initial_index_set(index_set, ns, axiom);
1524}
1525
1531 index_set_pairt &index_set,
1532 const namespacet &ns,
1533 const std::vector<exprt> &current_constraints)
1534{
1535 for(const auto &axiom : current_constraints)
1536 update_index_set(index_set, ns, axiom);
1537}
1538
1545static void get_sub_arrays(const exprt &array_expr, std::vector<exprt> &accu)
1546{
1547 if(array_expr.id() == ID_if)
1548 {
1549 get_sub_arrays(to_if_expr(array_expr).true_case(), accu);
1550 get_sub_arrays(to_if_expr(array_expr).false_case(), accu);
1551 }
1552 else
1553 {
1554 if(array_expr.type().id() == ID_array)
1555 {
1556 // TODO: check_that it does not contain any sub_array
1557 accu.push_back(array_expr);
1558 }
1559 else
1560 {
1561 for(const auto &operand : array_expr.operands())
1562 get_sub_arrays(operand, accu);
1563 }
1564 }
1565}
1566
1573 index_set_pairt &index_set,
1574 const namespacet &ns,
1575 const exprt &s,
1576 exprt i)
1577{
1578 simplify(i, ns);
1579 const bool is_size_t = numeric_cast<std::size_t>(i).has_value();
1580 if(!i.is_constant() || is_size_t)
1581 {
1582 std::vector<exprt> sub_arrays;
1583 get_sub_arrays(s, sub_arrays);
1584 for(const auto &sub : sub_arrays)
1585 if(index_set.cumulative[sub].insert(i).second)
1586 index_set.current[sub].insert(i);
1587 }
1588}
1589
1606 index_set_pairt &index_set,
1607 const namespacet &ns,
1608 const exprt &qvar,
1609 const exprt &upper_bound,
1610 const exprt &s,
1611 const exprt &i)
1612{
1614 s.id() == ID_symbol || s.id() == ID_nondet_symbol || s.id() == ID_array ||
1615 s.id() == ID_if);
1616 if(s.id() == ID_array)
1617 {
1618 for(std::size_t j = 0; j < s.operands().size(); ++j)
1619 add_to_index_set(index_set, ns, s, from_integer(j, i.type()));
1620 return;
1621 }
1622 if(auto ite = expr_try_dynamic_cast<if_exprt>(s))
1623 {
1624 initial_index_set(index_set, ns, qvar, upper_bound, ite->true_case(), i);
1625 initial_index_set(index_set, ns, qvar, upper_bound, ite->false_case(), i);
1626 return;
1627 }
1628 const minus_exprt u_minus_1(upper_bound, from_integer(1, upper_bound.type()));
1629 exprt i_copy = i;
1630 replace_expr(qvar, u_minus_1, i_copy);
1631 add_to_index_set(index_set, ns, s, i_copy);
1632}
1633
1635 index_set_pairt &index_set,
1636 const namespacet &ns,
1637 const string_constraintt &axiom)
1638{
1639 const symbol_exprt &qvar = axiom.univ_var;
1640 const auto &bound = axiom.upper_bound;
1641 auto it = axiom.body.depth_begin();
1642 const auto end = axiom.body.depth_end();
1643 while(it != end)
1644 {
1645 if(it->id() == ID_index && is_char_type(it->type()))
1646 {
1647 const auto &index_expr = to_index_expr(*it);
1648 const auto &s = index_expr.array();
1649 initial_index_set(index_set, ns, qvar, bound, s, index_expr.index());
1650 it.next_sibling_or_parent();
1651 }
1652 else
1653 ++it;
1654 }
1655}
1656
1658 index_set_pairt &index_set,
1659 const namespacet &ns,
1661{
1662 auto it = axiom.premise.depth_begin();
1663 const auto end = axiom.premise.depth_end();
1664 while(it != end)
1665 {
1666 if(it->id() == ID_index && is_char_type(it->type()))
1667 {
1668 const exprt &s = to_index_expr(*it).array();
1669 const exprt &i = to_index_expr(*it).index();
1670
1671 // cur is of the form s[i] and no quantified variable appears in i
1672 add_to_index_set(index_set, ns, s, i);
1673
1674 it.next_sibling_or_parent();
1675 }
1676 else
1677 ++it;
1678 }
1679
1680 const minus_exprt kminus1(
1682 add_to_index_set(index_set, ns, axiom.s1.content(), kminus1);
1683}
1684
1690 index_set_pairt &index_set,
1691 const namespacet &ns,
1692 const exprt &formula)
1693{
1694 std::list<exprt> to_process;
1695 to_process.push_back(formula);
1696
1697 while(!to_process.empty())
1698 {
1699 exprt cur = to_process.back();
1700 to_process.pop_back();
1701 if(cur.id() == ID_index && is_char_type(cur.type()))
1702 {
1703 const exprt &s = to_index_expr(cur).array();
1704 const exprt &i = to_index_expr(cur).index();
1706 s.type().id() == ID_array,
1707 string_refinement_invariantt("index expressions must index on arrays"));
1708 exprt simplified = simplify_sum(i);
1709 if(s.id() != ID_array) // do not update index set of constant arrays
1710 add_to_index_set(index_set, ns, s, simplified);
1711 }
1712 else
1713 {
1714 for(const auto &op : as_const(cur).operands())
1715 to_process.push_back(op);
1716 }
1717 }
1718}
1719
1738static std::vector<exprt> instantiate(
1740 const index_set_pairt &index_set,
1741 const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
1742 &witnesses)
1743{
1744 const array_string_exprt &s0 = axiom.s0;
1745 const array_string_exprt &s1 = axiom.s1;
1746
1747 const auto &index_set0 = index_set.cumulative.find(s0.content());
1748 const auto &index_set1 = index_set.cumulative.find(s1.content());
1749 const auto &current_index_set0 = index_set.current.find(s0.content());
1750 const auto &current_index_set1 = index_set.current.find(s1.content());
1751
1752 if(
1753 index_set0 != index_set.cumulative.end() &&
1754 index_set1 != index_set.cumulative.end() &&
1755 current_index_set0 != index_set.current.end() &&
1756 current_index_set1 != index_set.current.end())
1757 {
1758 typedef std::pair<exprt, exprt> expr_pairt;
1759 std::set<expr_pairt> index_pairs;
1760
1761 for(const auto &ic0 : current_index_set0->second)
1762 for(const auto &i1 : index_set1->second)
1763 index_pairs.insert(expr_pairt(ic0, i1));
1764 for(const auto &ic1 : current_index_set1->second)
1765 for(const auto &i0 : index_set0->second)
1766 index_pairs.insert(expr_pairt(i0, ic1));
1767
1768 return ::instantiate_not_contains(axiom, index_pairs, witnesses);
1769 }
1770 return {};
1771}
1772
1780exprt substitute_array_lists(exprt expr, size_t string_max_length)
1781{
1782 for(auto &operand : expr.operands())
1783 operand = substitute_array_lists(operand, string_max_length);
1784
1785 if(expr.id() == ID_array_list)
1786 {
1788 expr.operands().size() >= 2,
1789 string_refinement_invariantt("array-lists must have at least two "
1790 "operands"));
1791 const typet &char_type = expr.operands()[1].type();
1793 exprt ret_expr = array_of_exprt(from_integer(0, char_type), arr_type);
1794
1795 for(size_t i = 0; i < expr.operands().size(); i += 2)
1796 {
1797 const exprt &index = expr.operands()[i];
1798 const exprt &value = expr.operands()[i + 1];
1799 const auto index_value = numeric_cast<std::size_t>(index);
1800 if(
1801 !index.is_constant() ||
1802 (index_value && *index_value < string_max_length))
1803 ret_expr = with_exprt(ret_expr, index, value);
1804 }
1805 return ret_expr;
1806 }
1807
1808 return expr;
1809}
1810
1819{
1820 const auto super_get = [this](const exprt &expr) {
1821 return supert::get(expr);
1822 };
1823 exprt ecopy(expr);
1824 (void)symbol_resolve.replace_expr(ecopy);
1825
1826 // Special treatment for index expressions
1827 const auto &index_expr = expr_try_dynamic_cast<index_exprt>(ecopy);
1828 if(index_expr && is_char_type(index_expr->type()))
1829 {
1830 std::reference_wrapper<const exprt> current(index_expr->array());
1831 while(current.get().id() == ID_if)
1832 {
1833 const auto &if_expr = expr_dynamic_cast<if_exprt>(current.get());
1834 const exprt cond = get(if_expr.cond());
1835 if(cond.is_true())
1836 current = std::cref(if_expr.true_case());
1837 else if(cond.is_false())
1838 current = std::cref(if_expr.false_case());
1839 else
1841 }
1842 const auto array = supert::get(current.get());
1843 const auto index = get(index_expr->index());
1844
1845 // If the underlying solver does not know about the existence of an array,
1846 // it can return nil, which cannot be used in the expression returned here.
1847 if(array.is_nil())
1848 return index_exprt(current, index);
1849
1850 const exprt unknown =
1851 from_integer(CHARACTER_FOR_UNKNOWN, index_expr->type());
1852 if(
1853 const auto sparse_array = interval_sparse_arrayt::of_expr(array, unknown))
1854 {
1855 if(const auto index_value = numeric_cast<std::size_t>(index))
1856 return sparse_array->at(*index_value);
1857 return sparse_array->to_if_expression(index);
1858 }
1859
1860 INVARIANT(array.id() == ID_symbol || array.id() == ID_nondet_symbol,
1861 "Apart from symbols, array valuations can be interpreted as "
1862 "sparse arrays. Array model : " + array.pretty());
1863 return index_exprt(array, index);
1864 }
1865
1866 if(is_char_array_type(ecopy.type(), ns))
1867 {
1869
1870 if(
1871 const auto from_dependencies =
1872 dependencies.eval(arr, [&](const exprt &expr) { return get(expr); }))
1873 return *from_dependencies;
1874
1875 if(
1876 const auto arr_model_opt =
1877 get_array(super_get, ns, log.debug(), arr, generator.array_pool))
1878 return *arr_model_opt;
1879
1880 if(
1881 const auto &length_from_pool =
1883 {
1884 const exprt length = super_get(length_from_pool.value());
1885
1886 if(const auto n = numeric_cast<std::size_t>(length))
1887 {
1888 const interval_sparse_arrayt sparse_array(from_integer(
1890 return sparse_array.concretize(*n, length.type());
1891 }
1892 }
1893 return arr;
1894 }
1895 return supert::get(ecopy);
1896}
1897
1908 const namespacet &ns,
1909 const exprt &axiom,
1910 const symbol_exprt &var,
1911 message_handlert &message_handler)
1912{
1913 satcheck_no_simplifiert sat_check(message_handler);
1914 bv_pointerst solver(ns, sat_check, message_handler);
1915 solver << axiom;
1916
1918 return solver.get(var);
1919 else
1920 return {};
1921}
1922
1924typedef std::map<exprt, std::vector<exprt>> array_index_mapt;
1925
1928{
1929 array_index_mapt indices;
1930 // clang-format off
1931 std::for_each(
1932 expr.depth_begin(),
1933 expr.depth_end(),
1934 [&](const exprt &expr)
1935 {
1936 const auto index_expr = expr_try_dynamic_cast<const index_exprt>(expr);
1937 if(index_expr)
1938 indices[index_expr->array()].push_back(index_expr->index());
1939 });
1940 // clang-format on
1941 return indices;
1942}
1943
1949static bool
1951{
1952 for(auto it = expr.depth_begin(); it != expr.depth_end();)
1953 {
1954 if(
1955 it->id() != ID_plus && it->id() != ID_minus &&
1956 it->id() != ID_unary_minus && *it != var)
1957 {
1958 if(std::find(it->depth_begin(), it->depth_end(), var) != it->depth_end())
1959 return false;
1960 else
1961 it.next_sibling_or_parent();
1962 }
1963 else
1964 ++it;
1965 }
1966 return true;
1967}
1968
1977{
1978 for(auto it = constr.body.depth_begin(); it != constr.body.depth_end();)
1979 {
1980 if(*it == constr.univ_var)
1981 return false;
1982 if(it->id() == ID_index)
1983 it.next_sibling_or_parent();
1984 else
1985 ++it;
1986 }
1987 return true;
1988}
1989
1997 messaget::mstreamt &stream,
1998 const namespacet &ns,
1999 const string_constraintt &constraint)
2000{
2001 const array_index_mapt body_indices = gather_indices(constraint.body);
2002 // Must validate for each string. Note that we have an invariant that the
2003 // second value in the pair is non-empty.
2004 for(const auto &pair : body_indices)
2005 {
2006 // Condition 1: All indices of the same string must be the of the same form
2007 const exprt rep = pair.second.back();
2008 for(size_t j = 0; j < pair.second.size() - 1; j++)
2009 {
2010 const exprt i = pair.second[j];
2011 const equal_exprt equals(rep, i);
2012 const exprt result = simplify_expr(equals, ns);
2013 if(result.is_false())
2014 {
2015 stream << "Indices not equal: " << to_string(constraint)
2016 << ", str: " << format(pair.first) << messaget::eom;
2017 return false;
2018 }
2019 }
2020
2021 // Condition 2: f must be linear in the quantified variable
2022 if(!is_linear_arithmetic_expr(rep, constraint.univ_var))
2023 {
2024 stream << "f is not linear: " << to_string(constraint)
2025 << ", str: " << format(pair.first) << messaget::eom;
2026 return false;
2027 }
2028
2029 // Condition 3: the quantified variable can only occur in indices in the
2030 // body
2031 if(!universal_only_in_index(constraint))
2032 {
2033 stream << "Universal variable outside of index:" << to_string(constraint)
2034 << messaget::eom;
2035 return false;
2036 }
2037 }
2038
2039 return true;
2040}
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
optionalt< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
Target numeric_cast_v(const mp_integer &arg)
Convert an mp_integer to integral type Target An invariant will fail if the conversion is not possibl...
const T & as_const(T &value)
Return a reference to the same object but ensures the type is const.
Definition as_const.h:14
static bool convert(const irep_idt &identifier, const std::ostringstream &s, symbol_table_baset &symbol_table, message_handlert &message_handler)
int8_t s1
bitvector_typet index_type()
Definition c_types.cpp:22
bitvector_typet char_type()
Definition c_types.cpp:111
Boolean AND.
Definition std_expr.h:2071
Array constructor from list of elements.
Definition std_expr.h:1563
const array_typet & type() const
Definition std_expr.h:1570
Array constructor from single element.
Definition std_expr.h:1498
Correspondance between arrays and pointers string representations.
Definition array_pool.h:42
exprt get_or_create_length(const array_string_exprt &s)
Get the length of an array_string_exprt from the array_pool.
const std::unordered_map< exprt, array_string_exprt, irep_hash > & get_arrays_of_pointers() const
Definition array_pool.h:50
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...
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.
const typet & length_type() const
Definition string_expr.h:70
Arrays with given size.
Definition std_types.h:763
const exprt & size() const
Definition std_types.h:796
const typet & element_type() const
The type of the elements of the array.
Definition std_types.h:783
const namespacet & ns
Definition arrays.h:56
messaget log
Definition arrays.h:57
exprt & lhs()
Definition std_expr.h:613
exprt & rhs()
Definition std_expr.h:623
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition std_expr.h:707
decision_proceduret::resultt dec_solve() override
Run the decision procedure to solve the problem.
A constant literal expression.
Definition std_expr.h:2942
resultt
Result of running the decision procedure.
virtual exprt get(const exprt &expr) const =0
Return expr with variables replaced by values from satisfying assignment if available.
virtual void set_to(const exprt &expr, bool value)=0
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
Equality.
Definition std_expr.h:1306
Maps equation to expressions contained in them and conversely expressions to equations that contain t...
void add(const std::size_t i, const exprt &expr)
Record the fact that equation i contains expression expr
std::vector< std::size_t > find_equations(const exprt &expr)
std::vector< exprt > find_expressions(const std::size_t i)
Base class for all expressions.
Definition expr.h:56
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:27
depth_iteratort depth_end()
Definition expr.cpp:249
bool is_boolean() const
Return whether the expression represents a Boolean.
Definition expr.h:216
depth_iteratort depth_begin()
Definition expr.cpp:247
bool is_false() const
Return whether the expression is a constant representing false.
Definition expr.cpp:34
bool is_constant() const
Return whether the expression is a constant.
Definition expr.h:204
typet & type()
Return the type of the expression.
Definition expr.h:84
operandst & operands()
Definition expr.h:94
The trinary if-then-else operator.
Definition std_expr.h:2323
exprt & cond()
Definition std_expr.h:2340
exprt & false_case()
Definition std_expr.h:2360
exprt & true_case()
Definition std_expr.h:2350
Boolean implication.
Definition std_expr.h:2134
Array index operator.
Definition std_expr.h:1410
exprt & index()
Definition std_expr.h:1450
exprt & array()
Definition std_expr.h:1440
An expression denoting infinity.
Definition std_expr.h:3042
Represents arrays by the indexes up to which the value remains the same.
exprt to_if_expression(const exprt &index) 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,...
array_exprt concretize(std::size_t size, const typet &index_type) const
Convert to an array representation, ignores elements at index >= size.
const irep_idt & get(const irep_idt &name) const
Definition irep.cpp:44
const irep_idt & id() const
Definition irep.h:396
bool is_nil() const
Definition irep.h:376
Canonical representation of linear function, for instance, expression $x + x - y + 5 - 3$ would given...
Extract member of struct or union.
Definition std_expr.h:2794
messaget & message
Definition message.h:246
mstreamt & error() const
Definition message.h:399
mstreamt & debug() const
Definition message.h:429
message_handlert & get_message_handler()
Definition message.h:184
static eomt eom
Definition message.h:297
Binary minus.
Definition std_expr.h:1006
const typet & follow(const typet &) const
Resolve type symbol to the type it points to.
Definition namespace.cpp:49
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
The NIL expression.
Definition std_expr.h:3026
Boolean negation.
Definition std_expr.h:2278
The plus expression Associativity is not specified.
Definition std_expr.h:947
void l_set_to_true(literalt a)
Definition prop.h:52
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.
optionalt< exprt > make_array_pointer_association(const exprt &return_code, const function_application_exprt &expr)
Associate array to pointer, and array to length.
static bool is_valid_string_constraint(messaget::mstreamt &stream, const namespacet &ns, const string_constraintt &constraint)
Checks the data invariant for string_constraintt.
exprt univ_within_bounds() const
static array_index_mapt gather_indices(const exprt &expr)
static bool universal_only_in_index(const string_constraintt &constr)
The universally quantified variable is only allowed to occur in index expressions in the body of a st...
static bool is_linear_arithmetic_expr(const exprt &expr, const symbol_exprt &var)
std::map< exprt, std::vector< exprt > > array_index_mapt
void output_dot(std::ostream &stream) const
void clean_cache()
Clean the cache used by eval
NODISCARD string_constraintst add_constraints(string_constraint_generatort &generatort, message_handlert &message_handler)
For all builtin call on which a test (or an unsupported buitin) result depends, add the corresponding...
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...
string_constraint_generatort generator
union_find_replacet symbol_resolve
std::vector< exprt > equations
string_refinementt(const infot &)
decision_proceduret::resultt dec_solve() override
Main decision procedure of the solver.
std::set< exprt > seen_instances
void set_to(const exprt &expr, bool value) override
Record the constraints to ensure that the expression is true when the boolean is true and false other...
string_dependenciest dependencies
index_set_pairt index_sets
exprt get(const exprt &expr) const override
Evaluates the given expression in the valuation found by string_refinementt::dec_solve.
std::vector< exprt > current_constraints
void add_lemma(const exprt &lemma, bool simplify_lemma=true)
Add the given lemma to the solver.
String type.
Definition std_types.h:913
Structure type, corresponds to C style structs.
Definition std_types.h:231
const componentst & components() const
Definition std_types.h:147
Expression to hold a symbol (variable)
Definition std_expr.h:113
const irep_idt & get_identifier() const
Definition std_expr.h:142
Generation of fresh symbols of a given type.
Definition array_pool.h:22
The type of an expression, extends irept.
Definition type.h:29
Similar interface to union-find for expressions, with a function for replacing sub-expressions by the...
std::vector< std::pair< exprt, exprt > > to_vector() const
exprt make_union(const exprt &a, const exprt &b)
Merge the set containing a and the set containing b.
bool replace_expr(exprt &expr) const
Replace subexpressions of expr by the representative element of the set they belong to.
Operator to update elements in structs and arrays.
Definition std_expr.h:2424
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.
Definition expr_cast.h:81
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.
Definition expr_cast.h:207
Forward depth-first search iterators These iterators' copy operations are expensive,...
bool has_subtype(const typet &type, const std::function< bool(const typet &)> &pred, const namespacet &ns)
returns true if any of the contained types satisfies pred
Deprecated expression utility functions.
static format_containert< T > format(const T &o)
Definition format.h:37
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
Magic numbers used throughout the codebase.
const std::size_t MAX_CONCRETE_STRING_SIZE
Definition magic.h:14
bool can_cast_expr< function_application_exprt >(const exprt &base)
nonstd::optional< T > optionalt
Definition optional.h:35
Ranges: pair of begin and end iterators, which can be initialized from containers,...
ranget< iteratort > make_range(iteratort begin, iteratort end)
Definition range.h:524
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, const namespacet &ns)
BigInt mp_integer
Definition smt_terms.h:18
void solver(std::vector< framet > &frames, const std::unordered_set< symbol_exprt, irep_hash > &address_taken, const solver_optionst &solver_options, const namespacet &ns, std::vector< propertyt > &properties, std::size_t property_index)
Definition solver.cpp:44
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:534
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Definition std_expr.cpp:63
bool can_cast_expr< equal_exprt >(const exprt &base)
Definition std_expr.h:1331
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition std_expr.h:1478
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition std_expr.h:2403
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition std_expr.h:2992
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition std_expr.h:1347
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition std_types.h:308
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition std_types.h:844
#define CHARACTER_FOR_UNKNOWN
Module: String solver Author: Diffblue Ltd.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
void merge(string_constraintst &result, string_constraintst other)
Merge two sets of constraints by appending to the first one.
Defines related function for string constraints.
std::vector< exprt > instantiate_not_contains(const string_not_contains_constraintt &axiom, const std::set< std::pair< exprt, exprt > > &index_pairs, const std::unordered_map< string_not_contains_constraintt, symbol_exprt > &witnesses)
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...
Keeps track of dependencies between strings.
array_string_exprt & to_array_string_expr(exprt &expr)
Definition string_expr.h:96
static void initial_index_set(index_set_pairt &index_set, const namespacet &ns, const string_constraintt &axiom)
static bool is_valid_string_constraint(messaget::mstreamt &stream, const namespacet &ns, const string_constraintt &constraint)
static std::string string_of_array(const array_exprt &arr)
convert the content of a string to a more readable representation.
static void update_index_set(index_set_pairt &index_set, const namespacet &ns, const std::vector< exprt > &current_constraints)
Add to the index set all the indices that appear in the formulas.
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 std::vector< exprt > extract_strings_from_lhs(const exprt &lhs, const namespacet &ns)
This is meant to be used on the lhs of an equation with string subtype.
exprt substitute_array_lists(exprt expr, size_t string_max_length)
Replace array-lists by 'with' expressions.
static std::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 > &not_contain_witnesses)
Check axioms takes the model given by the underlying solver and answers whether it satisfies the stri...
static void add_equations_for_symbol_resolution(union_find_replacet &symbol_solver, const std::vector< exprt > &equations, const namespacet &ns, messaget::mstreamt &stream)
Add association for each char pointer in the equation.
static void make_char_array_pointer_associations(string_constraint_generatort &generator, exprt &expr)
If expr is an equation whose right-hand-side is a associate_array_to_pointer call,...
static void add_string_equation_to_symbol_resolution(const equal_exprt &eq, union_find_replacet &symbol_resolve, const namespacet &ns)
Given an equation on strings, mark these strings as belonging to the same set in the symbol_resolve s...
static bool validate(const string_refinementt::infot &info)
static void add_to_index_set(index_set_pairt &index_set, const namespacet &ns, const exprt &s, exprt i)
Add i to the index set all the indices that appear in the formula.
exprt simplify_sum(const exprt &f)
static 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.
union_find_replacet string_identifiers_resolution_from_equations(const std::vector< equal_exprt > &equations, const namespacet &ns, messaget::mstreamt &stream)
Symbol resolution for expressions of type string typet.
static void display_index_set(messaget::mstreamt &stream, const index_set_pairt &index_set)
Write index set to the given stream, use for debugging.
static std::vector< T > fill_in_map_as_vector(const std::map< std::size_t, T > &index_value)
Convert index-value map to a vector of values.
static exprt negation_of_not_contains_constraint(const string_not_contains_constraintt &constraint, const symbol_exprt &univ_var, const std::function< exprt(const exprt &)> &get)
Negates the constraint to be fed to a solver.
static 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.
static exprt replace_expr_copy(const union_find_replacet &symbol_resolve, exprt expr)
Substitute sub-expressions in equation by representative elements of symbol_resolve whenever possible...
static void substitute_array_access_in_place(exprt &expr, symbol_generatort &symbol_generator, const bool left_propagate)
Auxiliary function for substitute_array_access Performs the same operation but modifies the argument ...
static void get_sub_arrays(const exprt &array_expr, std::vector< exprt > &accu)
An expression representing an array of characters can be in the form of an if expression for instance...
void debug_model(const string_constraint_generatort &generator, messaget::mstreamt &stream, const namespacet &ns, const std::function< exprt(const exprt &)> &super_get, const std::vector< symbol_exprt > &symbols, array_poolt &array_pool)
Display part of the current model by mapping the variables created by the solver to constant expressi...
static std::vector< exprt > instantiate(const string_not_contains_constraintt &axiom, const index_set_pairt &index_set, const std::unordered_map< string_not_contains_constraintt, symbol_exprt > &witnesses)
Instantiates a quantified formula representing not_contains by substituting the quantifiers and gener...
static optionalt< exprt > substitute_array_access(const index_exprt &index_expr, symbol_generatort &symbol_generator, const bool left_propagate)
static void debug_check_axioms_step(messaget::mstreamt &stream, const T &axiom, const T &axiom_in_model, const exprt &negaxiom, const exprt &with_concretized_arrays)
Debugging function which outputs the different steps an axiom goes through to be checked in check axi...
static exprt get_char_array_and_concretize(const std::function< exprt(const exprt &)> &super_get, const namespacet &ns, messaget::mstreamt &stream, const array_string_exprt &arr, array_poolt &array_pool)
Debugging function which finds the valuation of the given array in super_get and concretize unknown c...
static std::vector< exprt > generate_instantiations(const index_set_pairt &index_set, const string_axiomst &axioms, const std::unordered_map< string_not_contains_constraintt, symbol_exprt > &not_contain_witnesses)
Instantiation of all constraints.
String support via creating string constraints and progressively instantiating the universal constrai...
exprt substitute_array_access(exprt expr, symbol_generatort &symbol_generator, const bool left_propagate)
Create an equivalent expression where array accesses and 'with' expressions are replaced by 'if' expr...
union_find_replacet string_identifiers_resolution_from_equations(const std::vector< equal_exprt > &equations, const namespacet &ns, messaget::mstreamt &stream)
Symbol resolution for expressions of type string typet.
#define string_refinement_invariantt(reason)
std::string utf16_constant_array_to_java(const array_exprt &arr, std::size_t length)
Construct a string from a constant array.
bool is_char_type(const typet &type)
For now, any unsigned bitvector type of width smaller or equal to 16 is considered a character.
bool has_char_pointer_subtype(const typet &type, const namespacet &ns)
bool is_char_array_type(const typet &type, const namespacet &ns)
Distinguish char array from other types.
bool is_char_pointer_type(const typet &type)
For now, any unsigned bitvector type is considered a character.
const namespacet * ns
std::map< exprt, std::set< exprt > > current
std::map< exprt, std::set< exprt > > cumulative
std::vector< string_constraintt > universal
std::vector< string_not_contains_constraintt > not_contains
Collection of constraints of different types: existential formulas, universal formulas,...
std::vector< string_not_contains_constraintt > not_contains
std::vector< exprt > existential
std::vector< string_constraintt > universal
Constraints to encode non containement of strings.
string_refinementt constructor arguments