cprover
string_refinement.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: 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 
9 Author: Alberto Griggio, alberto.griggio@gmail.com
10 
11 \*******************************************************************/
12 
19 
21 
22 #include <iomanip>
23 #include <numeric>
24 #include <stack>
25 #include <util/expr_iterator.h>
26 #include <util/expr_util.h>
27 #include <util/simplify_expr.h>
28 #include <solvers/sat/satcheck.h>
30 #include <unordered_set>
31 #include <util/magic.h>
32 
33 static bool is_valid_string_constraint(
34  messaget::mstreamt &stream,
35  const namespacet &ns,
36  const string_constraintt &constraint);
37 
39  const namespacet &ns,
40  const exprt &axiom,
41  const symbol_exprt &var);
42 
59 static std::pair<bool, std::vector<exprt>> check_axioms(
60  const string_axiomst &axioms,
62  const std::function<exprt(const exprt &)> &get,
63  messaget::mstreamt &stream,
64  const namespacet &ns,
65  bool use_counter_example,
66  const union_find_replacet &symbol_resolve,
67  const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
68  &not_contain_witnesses);
69 
70 static void initial_index_set(
71  index_set_pairt &index_set,
72  const namespacet &ns,
73  const string_constraintt &axiom);
74 
75 static void initial_index_set(
76  index_set_pairt &index_set,
77  const namespacet &ns,
78  const string_not_contains_constraintt &axiom);
79 
80 static void initial_index_set(
81  index_set_pairt &index_set,
82  const namespacet &ns,
83  const string_axiomst &axioms);
84 
85 exprt simplify_sum(const exprt &f);
86 
87 static void update_index_set(
88  index_set_pairt &index_set,
89  const namespacet &ns,
90  const std::vector<exprt> &current_constraints);
91 
92 static void update_index_set(
93  index_set_pairt &index_set,
94  const namespacet &ns,
95  const exprt &formula);
96 
106 static exprt instantiate(
107  const string_constraintt &axiom,
108  const exprt &str,
109  const exprt &val);
110 
111 static std::vector<exprt> instantiate(
112  const string_not_contains_constraintt &axiom,
113  const index_set_pairt &index_set,
114  const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
115  &witnesses);
116 
118  const std::function<exprt(const exprt &)> &super_get,
119  const namespacet &ns,
120  messaget::mstreamt &stream,
121  const array_string_exprt &arr);
122 
124  const index_exprt &index_expr,
125  const std::function<symbol_exprt(const irep_idt &, const typet &)>
126  &symbol_generator,
127  const bool left_propagate);
128 
136 template <typename T>
137 static std::vector<T> fill_in_map_as_vector(
138  const std::map<std::size_t, T> &index_value)
139 {
140  std::vector<T> result;
141  if(!index_value.empty())
142  {
143  result.resize(index_value.rbegin()->first+1);
144  for(auto it=index_value.rbegin(); it!=index_value.rend(); ++it)
145  {
146  const std::size_t index=it->first;
147  const T &value = it->second;
148  const auto next=std::next(it);
149  const std::size_t leftmost_index_to_pad=
150  next!=index_value.rend()
151  ? next->first+1
152  : 0;
153  for(std::size_t j=leftmost_index_to_pad; j<=index; j++)
154  result[j]=value;
155  }
156  }
157  return result;
158 }
159 
160 static bool validate(const string_refinementt::infot &info)
161 {
162  PRECONDITION(info.ns);
163  PRECONDITION(info.prop);
164  return true;
165 }
166 
168  : supert(info),
169  config_(info),
170  loop_bound_(info.refinement_bound),
171  generator(*info.ns)
172 {
173 }
174 
176  string_refinementt(info, validate(info)) { }
177 
179 static void display_index_set(
180  messaget::mstreamt &stream,
181  const index_set_pairt &index_set)
182 {
183  const auto eom=messaget::eom;
184  std::size_t count=0;
185  std::size_t count_current=0;
186  for(const auto &i : index_set.cumulative)
187  {
188  const exprt &s=i.first;
189  stream << "IS(" << format(s) << ")=={" << eom;
190 
191  for(const auto &j : i.second)
192  {
193  const auto it=index_set.current.find(i.first);
194  if(it!=index_set.current.end() && it->second.find(j)!=it->second.end())
195  {
196  count_current++;
197  stream << "**";
198  }
199  stream << " " << format(j) << ";" << eom;
200  count++;
201  }
202  stream << "}" << eom;
203  }
204  stream << count << " elements in index set (" << count_current
205  << " newly added)" << eom;
206 }
207 
220 // NOLINTNEXTLINE(whitespace/line_length)
226 // NOLINTNEXTLINE(whitespace/line_length)
229 static std::vector<exprt> generate_instantiations(
230  const index_set_pairt &index_set,
231  const string_axiomst &axioms,
232  const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
233  &not_contain_witnesses)
234 {
235  std::vector<exprt> lemmas;
236  for(const auto &i : index_set.current)
237  {
238  for(const auto &univ_axiom : axioms.universal)
239  {
240  for(const auto &j : i.second)
241  lemmas.push_back(instantiate(univ_axiom, i.first, j));
242  }
243  }
244  for(const auto &nc_axiom : axioms.not_contains)
245  {
246  for(const auto &instance :
247  instantiate(nc_axiom, index_set, not_contain_witnesses))
248  lemmas.push_back(instance);
249  }
250  return lemmas;
251 }
252 
256  string_constraint_generatort &generator,
257  std::vector<equal_exprt> &equations)
258 {
259  for(equal_exprt &eq : equations)
260  {
261  if(
262  const auto fun_app =
263  expr_try_dynamic_cast<function_application_exprt>(eq.rhs()))
264  {
265  if(const auto result = generator.make_array_pointer_association(*fun_app))
266  eq.rhs() = *result;
267  }
268  }
269 }
270 
275 static exprt
276 replace_expr_copy(const union_find_replacet &symbol_resolve, exprt expr)
277 {
278  symbol_resolve.replace_expr(expr);
279  return expr;
280 }
281 
286 void string_refinementt::set_to(const exprt &expr, bool value)
287 {
288  PRECONDITION(expr.type().id()==ID_bool);
290 
291  if(expr.id() == ID_equal && value)
292  {
293  const equal_exprt &eq_expr = to_equal_expr(expr);
294  equations.push_back(eq_expr);
295  }
296  else
297  {
298  INVARIANT(
299  !has_char_array_subexpr(expr, ns), "char array only appear in equations");
300  supert::set_to(expr, value);
301  }
302 }
303 
313  union_find_replacet &symbol_solver,
314  const std::vector<equal_exprt> &equations,
315  const namespacet &ns,
316  messaget::mstreamt &stream)
317 {
318  const auto eom = messaget::eom;
319  const std::string log_message =
320  "WARNING string_refinement.cpp generate_symbol_resolution_from_equations:";
321  for(const equal_exprt &eq : equations)
322  {
323  const exprt &lhs = eq.lhs();
324  const exprt &rhs = eq.rhs();
325  if(lhs.id()!=ID_symbol)
326  {
327  stream << log_message << "non symbol lhs: " << format(lhs)
328  << " with rhs: " << format(rhs) << eom;
329  continue;
330  }
331 
332  if(lhs.type()!=rhs.type())
333  {
334  stream << log_message << "non equal types lhs: " << format(lhs)
335  << "\n####################### rhs: " << format(rhs) << eom;
336  continue;
337  }
338 
339  if(is_char_pointer_type(rhs.type()))
340  {
341  symbol_solver.make_union(lhs, rhs);
342  }
343  else if(rhs.id() == ID_function_application)
344  {
345  // function applications can be ignored because they will be replaced
346  // in the convert_function_application step of dec_solve
347  }
348  else if(
349  lhs.type().id() != ID_pointer && has_char_pointer_subtype(lhs.type(), ns))
350  {
351  if(rhs.type().id() == ID_struct)
352  {
353  const struct_typet &struct_type = to_struct_type(rhs.type());
354  for(const auto &comp : struct_type.components())
355  {
356  if(is_char_pointer_type(comp.type()))
357  {
358  const member_exprt lhs_data(lhs, comp.get_name(), comp.type());
359  const exprt rhs_data = simplify_expr(
360  member_exprt(rhs, comp.get_name(), comp.type()), ns);
361  symbol_solver.make_union(lhs_data, rhs_data);
362  }
363  }
364  }
365  else
366  {
367  stream << log_message << "non struct with char pointer subexpr "
368  << format(rhs) << "\n * of type " << format(rhs.type()) << eom;
369  }
370  }
371  }
372 }
373 
379 static std::vector<exprt> extract_strings_from_lhs(const exprt &lhs)
380 {
381  std::vector<exprt> result;
382  if(lhs.type() == string_typet())
383  result.push_back(lhs);
384  else if(lhs.type().id() == ID_struct)
385  {
386  const struct_typet &struct_type = to_struct_type(lhs.type());
387  for(const auto &comp : struct_type.components())
388  {
389  const std::vector<exprt> strings_in_comp = extract_strings_from_lhs(
390  member_exprt(lhs, comp.get_name(), comp.type()));
391  result.insert(
392  result.end(), strings_in_comp.begin(), strings_in_comp.end());
393  }
394  }
395  return result;
396 }
397 
402 static std::vector<exprt> extract_strings(const exprt &expr)
403 {
404  std::vector<exprt> result;
405  for(auto it = expr.depth_begin(); it != expr.depth_end();)
406  {
407  if(it->type() == string_typet() && it->id() != ID_if)
408  {
409  result.push_back(*it);
410  it.next_sibling_or_parent();
411  }
412  else if(it->id() == ID_symbol)
413  {
414  for(const exprt &e : extract_strings_from_lhs(*it))
415  result.push_back(e);
416  it.next_sibling_or_parent();
417  }
418  else
419  ++it;
420  }
421  return result;
422 }
423 
431  const equal_exprt &eq,
432  union_find_replacet &symbol_resolve,
433  const namespacet &ns)
434 {
435  if(eq.rhs().type() == string_typet())
436  {
437  symbol_resolve.make_union(eq.lhs(), eq.rhs());
438  }
439  else if(has_subtype(eq.lhs().type(), ID_string, ns))
440  {
441  if(eq.rhs().type().id() == ID_struct)
442  {
443  const struct_typet &struct_type = to_struct_type(eq.rhs().type());
444  for(const auto &comp : struct_type.components())
445  {
446  const member_exprt lhs_data(eq.lhs(), comp.get_name(), comp.type());
447  const exprt rhs_data = simplify_expr(
448  member_exprt(eq.rhs(), comp.get_name(), comp.type()), ns);
450  equal_exprt(lhs_data, rhs_data), symbol_resolve, ns);
451  }
452  }
453  }
454 }
455 
464  std::vector<equal_exprt> &equations,
465  const namespacet &ns,
466  messaget::mstreamt &stream)
467 {
468  const auto eom = messaget::eom;
469  const std::string log_message =
470  "WARNING string_refinement.cpp "
471  "string_identifiers_resolution_from_equations:";
472 
473  equation_symbol_mappingt equation_map;
474 
475  // Indexes of equations that need to be added to the result
476  std::unordered_set<size_t> required_equations;
477  std::stack<size_t> equations_to_treat;
478 
479  for(std::size_t i = 0; i < equations.size(); ++i)
480  {
481  const equal_exprt &eq = equations[i];
482  if(eq.rhs().id() == ID_function_application)
483  {
484  if(required_equations.insert(i).second)
485  equations_to_treat.push(i);
486 
487  std::vector<exprt> rhs_strings = extract_strings(eq.rhs());
488  for(const auto &expr : rhs_strings)
489  equation_map.add(i, expr);
490  }
491  else if(
492  eq.lhs().type().id() != ID_pointer &&
493  has_subtype(eq.lhs().type(), ID_string, ns))
494  {
495  std::vector<exprt> lhs_strings = extract_strings_from_lhs(eq.lhs());
496 
497  for(const auto &expr : lhs_strings)
498  equation_map.add(i, expr);
499 
500  if(lhs_strings.empty())
501  {
502  stream << log_message << "non struct with string subtype "
503  << format(eq.lhs()) << "\n * of type "
504  << format(eq.lhs().type()) << eom;
505  }
506 
507  for(const exprt &expr : extract_strings(eq.rhs()))
508  equation_map.add(i, expr);
509  }
510  }
511 
512  // transitively add all equations which depend on the equations to treat
513  while(!equations_to_treat.empty())
514  {
515  const std::size_t i = equations_to_treat.top();
516  equations_to_treat.pop();
517  for(const exprt &string : equation_map.find_expressions(i))
518  {
519  for(const std::size_t j : equation_map.find_equations(string))
520  {
521  if(required_equations.insert(j).second)
522  equations_to_treat.push(j);
523  }
524  }
525  }
526 
527  union_find_replacet result;
528  for(const std::size_t i : required_equations)
529  add_string_equation_to_symbol_resolution(equations[i], result, ns);
530 
531  return result;
532 }
533 
534 #ifdef DEBUG
535 static void output_equations(
537  std::ostream &output,
538  const std::vector<equal_exprt> &equations)
539 {
540  for(std::size_t i = 0; i < equations.size(); ++i)
541  output << " [" << i << "] " << format(equations[i].lhs())
542  << " == " << format(equations[i].rhs()) << std::endl;
543 }
544 #endif
545 
556 // NOLINTNEXTLINE
559 // NOLINTNEXTLINE
564 // NOLINTNEXTLINE
611 {
612 #ifdef DEBUG
613  debug() << "dec_solve: Initial set of equations" << eom;
614  output_equations(debug(), equations);
615 #endif
616 
617  debug() << "dec_solve: Build symbol solver from equations" << eom;
618  // symbol_resolve is used by get and is kept between calls to dec_solve,
619  // that's why we use a class member here
621 #ifdef DEBUG
622  debug() << "symbol resolve:" << eom;
623  for(const auto &pair : symbol_resolve.to_vector())
624  debug() << format(pair.first) << " --> " << format(pair.second) << eom;
625 #endif
626 
627  const union_find_replacet string_id_symbol_resolve =
629 #ifdef DEBUG
630  debug() << "symbol resolve string:" << eom;
631  for(const auto &pair : string_id_symbol_resolve.to_vector())
632  {
633  debug() << format(pair.first) << " --> " << format(pair.second) << eom;
634  }
635 #endif
636 
637  debug() << "dec_solve: Replacing string ids in function applications" << eom;
638  for(equal_exprt &eq : equations)
639  {
641  string_id_symbol_resolve.replace_expr(eq.rhs());
642  }
643 
644  // Generator is also used by get, so we have to use it as a class member
645  // but we make sure it is cleared at each `dec_solve` call.
648 
649 #ifdef DEBUG
650  output_equations(debug(), equations);
651 #endif
652 
653  debug() << "dec_solve: compute dependency graph and remove function "
654  << "applications captured by the dependencies:" << eom;
655  std::vector<equal_exprt> local_equations;
656  for(const equal_exprt &eq : equations)
657  {
658  // Ensures that arrays that are equal, are associated to the same nodes
659  // in the graph.
660  const equal_exprt eq_with_char_array_replaced_with_representative_elements =
662  const bool node_added = add_node(
663  dependencies,
664  eq_with_char_array_replaced_with_representative_elements,
666  if(!node_added)
667  local_equations.push_back(eq);
668  }
669  equations.clear();
670 
671 #ifdef DEBUG
673 #endif
674 
675  debug() << "dec_solve: add constraints" << eom;
677 
678 #ifdef DEBUG
679  output_equations(debug(), equations);
680 #endif
681 
682 #ifdef DEBUG
683  debug() << "dec_solve: arrays_of_pointers:" << eom;
684  for(auto pair : generator.array_pool.get_arrays_of_pointers())
685  {
686  debug() << " * " << format(pair.first) << "\t--> " << format(pair.second)
687  << " : " << format(pair.second.type()) << eom;
688  }
689 #endif
690 
691  for(const auto &eq : local_equations)
692  {
693 #ifdef DEBUG
694  debug() << "dec_solve: set_to " << format(eq) << eom;
695 #endif
696  supert::set_to(eq, true);
697  }
698 
699  std::transform(
702  std::back_inserter(axioms.universal),
703  [&](string_constraintt constraint) {
704  constraint.replace_expr(symbol_resolve);
706  is_valid_string_constraint(error(), ns, constraint),
708  "string constraints satisfy their invariant"));
709  return constraint;
710  });
711 
712  std::transform(
715  std::back_inserter(axioms.not_contains),
717  replace(symbol_resolve, axiom);
718  return axiom;
719  });
720 
721  // Used to store information about witnesses for not_contains constraints
722  std::unordered_map<string_not_contains_constraintt, symbol_exprt>
723  not_contain_witnesses;
724  for(const auto &nc_axiom : axioms.not_contains)
725  {
726  const auto &witness_type = [&] {
727  const auto &rtype = to_array_type(nc_axiom.s0.type());
728  const typet &index_type = rtype.size().type();
730  }();
731  not_contain_witnesses[nc_axiom] =
732  generator.fresh_symbol("not_contains_witness", witness_type);
733  }
734 
735  for(const exprt &lemma : generator.constraints.existential)
736  add_lemma(lemma);
737 
738  // Initial try without index set
739  const auto get = [this](const exprt &expr) { return this->get(expr); };
742  if(res==resultt::D_SATISFIABLE)
743  {
744  bool satisfied;
745  std::vector<exprt> counter_examples;
746  std::tie(satisfied, counter_examples) = check_axioms(
747  axioms,
748  generator,
749  get,
750  debug(),
751  ns,
754  not_contain_witnesses);
755  if(satisfied)
756  {
757  debug() << "check_SAT: the model is correct" << eom;
758  return resultt::D_SATISFIABLE;
759  }
760  debug() << "check_SAT: got SAT but the model is not correct" << eom;
761  }
762  else
763  {
764  debug() << "check_SAT: got UNSAT or ERROR" << eom;
765  return res;
766  }
767 
770  current_constraints.clear();
771  const auto instances =
772  generate_instantiations(index_sets, axioms, not_contain_witnesses);
773  for(const auto &instance : instances)
774  add_lemma(instance);
775 
776  while((loop_bound_--)>0)
777  {
780 
781  if(res==resultt::D_SATISFIABLE)
782  {
783  bool satisfied;
784  std::vector<exprt> counter_examples;
785  std::tie(satisfied, counter_examples) = check_axioms(
786  axioms,
787  generator,
788  get,
789  debug(),
790  ns,
793  not_contain_witnesses);
794  if(satisfied)
795  {
796  debug() << "check_SAT: the model is correct" << eom;
797  return resultt::D_SATISFIABLE;
798  }
799 
800  debug() << "check_SAT: got SAT but the model is not correct, refining..."
801  << eom;
802 
803  // Since the model is not correct although we got SAT, we need to refine
804  // the property we are checking by adding more indices to the index set,
805  // and instantiating universal formulas with this indices.
806  // We will then relaunch the solver with these added lemmas.
807  index_sets.current.clear();
809 
811 
812  if(index_sets.current.empty())
813  {
814  if(axioms.not_contains.empty())
815  {
816  error() << "dec_solve: current index set is empty, "
817  << "this should not happen" << eom;
818  return resultt::D_ERROR;
819  }
820  else
821  {
822  debug() << "dec_solve: current index set is empty, "
823  << "adding counter examples" << eom;
824  for(const auto &counter : counter_examples)
825  add_lemma(counter);
826  }
827  }
828  current_constraints.clear();
829  const auto instances =
830  generate_instantiations(index_sets, axioms, not_contain_witnesses);
831  for(const auto &instance : instances)
832  add_lemma(instance);
833  }
834  else
835  {
836  debug() << "check_SAT: default return " << static_cast<int>(res) << eom;
837  return res;
838  }
839  }
840  debug() << "string_refinementt::dec_solve reached the maximum number"
841  << "of steps allowed" << eom;
842  return resultt::D_ERROR;
843 }
844 
850  const exprt &lemma,
851  const bool simplify_lemma)
852 {
853  if(!seen_instances.insert(lemma).second)
854  return;
855 
856  current_constraints.push_back(lemma);
857 
858  exprt simple_lemma=lemma;
859  if(simplify_lemma)
860  simplify(simple_lemma, ns);
861 
862  if(simple_lemma.is_true())
863  {
864 #if 0
865  debug() << "string_refinementt::add_lemma : tautology" << eom;
866 #endif
867  return;
868  }
869 
870  symbol_resolve.replace_expr(simple_lemma);
871 
872  // Replace empty arrays with array_of expression because the solver cannot
873  // handle empty arrays.
874  for(auto it = simple_lemma.depth_begin(); it != simple_lemma.depth_end();)
875  {
876  if(it->id() == ID_array && it->operands().empty())
877  {
878  it.mutate() = array_of_exprt(
879  from_integer(CHARACTER_FOR_UNKNOWN, it->type().subtype()),
880  to_array_type(it->type()));
881  it.next_sibling_or_parent();
882  }
883  else
884  ++it;
885  }
886 
887  debug() << "adding lemma " << format(simple_lemma) << eom;
888 
889  prop.l_set_to_true(convert(simple_lemma));
890 }
891 
901  const std::function<exprt(const exprt &)> &super_get,
902  const namespacet &ns,
903  messaget::mstreamt &stream,
904  const array_string_exprt &arr)
905 {
906  const auto eom = messaget::eom;
907  const exprt &size = arr.length();
908  exprt arr_val = simplify_expr(super_get(arr), ns);
909  exprt size_val=super_get(size);
910  size_val=simplify_expr(size_val, ns);
911  const typet char_type = arr.type().subtype();
912  const typet &index_type=size.type();
913  const array_typet empty_ret_type(char_type, from_integer(0, index_type));
914  const array_of_exprt empty_ret(from_integer(0, char_type), empty_ret_type);
915 
916  if(size_val.id()!=ID_constant)
917  {
918  stream << "(sr::get_array) string of unknown size: " << format(size_val)
919  << eom;
920  return {};
921  }
922 
923  auto n_opt = numeric_cast<std::size_t>(size_val);
924  if(!n_opt)
925  {
926  stream << "(sr::get_array) size is not valid" << eom;
927  return {};
928  }
929  std::size_t n = *n_opt;
930 
932  {
933  stream << "(sr::get_array) long string (size " << format(arr.length())
934  << " = " << n << ") " << format(arr) << eom;
935  stream << "(sr::get_array) consider reducing max-nondet-string-length so "
936  "that no string exceeds "
938  << " in length and "
939  "make sure all functions returning strings are loaded"
940  << eom;
941  stream << "(sr::get_array) this can also happen on invalid object access"
942  << eom;
943  return nil_exprt();
944  }
945 
946  if(
947  const auto &array = interval_sparse_arrayt::of_expr(
949  return array->concretize(n, index_type);
950  return {};
951 }
952 
957 static std::string string_of_array(const array_exprt &arr)
958 {
959  if(arr.type().id()!=ID_array)
960  return std::string("");
961 
962  exprt size_expr=to_array_type(arr.type()).size();
963  auto n = numeric_cast_v<std::size_t>(size_expr);
964  return utf16_constant_array_to_java(arr, n);
965 }
966 
975  const std::function<exprt(const exprt &)> &super_get,
976  const namespacet &ns,
977  messaget::mstreamt &stream,
978  const array_string_exprt &arr)
979 {
980  const auto &eom = messaget::eom;
981  stream << "- " << format(arr) << ":\n";
982  stream << std::string(4, ' ') << "- type: " << format(arr.type()) << eom;
983  const auto arr_model_opt =
984  get_array(super_get, ns, stream, arr);
985  if(arr_model_opt)
986  {
987  stream << std::string(4, ' ') << "- char_array: " << format(*arr_model_opt)
988  << '\n';
989  stream << std::string(4, ' ') << "- type : " << format(arr_model_opt->type())
990  << eom;
991  const exprt simple = simplify_expr(*arr_model_opt, ns);
992  stream << std::string(4, ' ') << "- simplified_char_array: " << format(simple)
993  << eom;
994  if(
995  const auto concretized_array = get_array(
996  super_get, ns, stream, to_array_string_expr(simple)))
997  {
998  stream << std::string(4, ' ')
999  << "- concretized_char_array: " << format(*concretized_array)
1000  << eom;
1001 
1002  if(
1003  const auto array_expr =
1004  expr_try_dynamic_cast<array_exprt>(*concretized_array))
1005  {
1006  stream << std::string(4, ' ') << "- as_string: \""
1007  << string_of_array(*array_expr) << "\"\n";
1008  }
1009  else
1010  stream << std::string(2, ' ') << "- warning: not an array" << eom;
1011  return *concretized_array;
1012  }
1013  return simple;
1014  }
1015  stream << std::string(4, ' ') << "- incomplete model" << eom;
1016  return arr;
1017 }
1018 
1022  const string_constraint_generatort &generator,
1023  messaget::mstreamt &stream,
1024  const namespacet &ns,
1025  const std::function<exprt(const exprt &)> &super_get,
1026  const std::vector<symbol_exprt> &symbols)
1027 {
1028  stream << "debug_model:" << '\n';
1029  for(const auto &pointer_array : generator.array_pool.get_arrays_of_pointers())
1030  {
1031  const auto arr = pointer_array.second;
1032  const exprt model = get_char_array_and_concretize(
1033  super_get, ns, stream, arr);
1034 
1035  stream << "- " << format(arr) << ":\n"
1036  << " - pointer: " << format(pointer_array.first) << "\n"
1037  << " - model: " << format(model) << messaget::eom;
1038  }
1039 
1040  for(const auto &symbol : symbols)
1041  {
1042  stream << " - " << symbol.get_identifier() << ": "
1043  << format(super_get(symbol)) << '\n';
1044  }
1045  stream << messaget::eom;
1046 }
1047 
1061  const with_exprt &expr,
1062  const exprt &index,
1063  const bool left_propagate)
1064 {
1065  return left_propagate ? interval_sparse_arrayt(expr).to_if_expression(index)
1066  : sparse_arrayt::to_if_expression(expr, index);
1067 }
1068 
1076  const array_exprt &array_expr,
1077  const exprt &index,
1078  const std::function<symbol_exprt(const irep_idt &, const typet &)>
1079  &symbol_generator)
1080 {
1081  const typet &char_type = array_expr.type().subtype();
1082  const exprt default_val = symbol_generator("out_of_bound_access", char_type);
1083  const interval_sparse_arrayt sparse_array(array_expr, default_val);
1084  return sparse_array.to_if_expression(index);
1085 }
1086 
1088  const if_exprt &if_expr,
1089  const exprt &index,
1090  const std::function<symbol_exprt(const irep_idt &, const typet &)>
1091  &symbol_generator,
1092  const bool left_propagate)
1093 {
1094  // Substitute recursively in branches of conditional expressions
1095  const exprt true_case = substitute_array_access(
1096  index_exprt(if_expr.true_case(), index), symbol_generator, left_propagate);
1097  const exprt false_case = substitute_array_access(
1098  index_exprt(if_expr.false_case(), index), symbol_generator, left_propagate);
1099 
1100  return if_exprt(if_expr.cond(), true_case, false_case);
1101 }
1102 
1104  const index_exprt &index_expr,
1105  const std::function<symbol_exprt(const irep_idt &, const typet &)>
1106  &symbol_generator,
1107  const bool left_propagate)
1108 {
1109  const exprt &array = index_expr.array();
1110  if(auto array_of = expr_try_dynamic_cast<array_of_exprt>(array))
1111  return array_of->op();
1112  if(auto array_with = expr_try_dynamic_cast<with_exprt>(array))
1113  return substitute_array_access(
1114  *array_with, index_expr.index(), left_propagate);
1115  if(auto array_expr = expr_try_dynamic_cast<array_exprt>(array))
1116  return substitute_array_access(
1117  *array_expr, index_expr.index(), symbol_generator);
1118  if(auto if_expr = expr_try_dynamic_cast<if_exprt>(array))
1119  return substitute_array_access(
1120  *if_expr, index_expr.index(), symbol_generator, left_propagate);
1121 
1122  INVARIANT(
1123  array.is_nil() || array.id() == ID_symbol,
1124  std::string(
1125  "in case the array is unknown, it should be a symbol or nil, id: ")
1126  + id2string(array.id()));
1127  return index_expr;
1128 }
1129 
1134  exprt &expr,
1135  const std::function<symbol_exprt(const irep_idt &, const typet &)>
1136  &symbol_generator,
1137  const bool left_propagate)
1138 {
1139  if(const auto index_expr = expr_try_dynamic_cast<index_exprt>(expr))
1140  {
1141  expr =
1142  substitute_array_access(*index_expr, symbol_generator, left_propagate);
1143  }
1144 
1145  for(auto &op : expr.operands())
1146  substitute_array_access_in_place(op, symbol_generator, left_propagate);
1147 }
1148 
1170  exprt expr,
1171  const std::function<symbol_exprt(const irep_idt &, const typet &)>
1172  &symbol_generator,
1173  const bool left_propagate)
1174 {
1175  substitute_array_access_in_place(expr, symbol_generator, left_propagate);
1176  return expr;
1177 }
1178 
1190  const string_not_contains_constraintt &constraint,
1191  const symbol_exprt &univ_var,
1192  const std::function<exprt(const exprt &)> &get)
1193 {
1194  // If the for all is vacuously true, the negation is false.
1195  const auto lbe =
1196  numeric_cast_v<mp_integer>(get(constraint.exists_lower_bound));
1197  const auto ube =
1198  numeric_cast_v<mp_integer>(get(constraint.exists_upper_bound));
1199  const auto univ_bounds = and_exprt(
1200  binary_relation_exprt(get(constraint.univ_lower_bound), ID_le, univ_var),
1201  binary_relation_exprt(get(constraint.univ_upper_bound), ID_gt, univ_var));
1202 
1203  // The negated existential becomes an universal, and this is the unrolling of
1204  // that universal quantifier.
1205  std::vector<exprt> conjuncts;
1206  conjuncts.reserve(numeric_cast_v<std::size_t>(ube - lbe));
1207  for(mp_integer i=lbe; i<ube; ++i)
1208  {
1209  const constant_exprt i_expr = from_integer(i, univ_var.type());
1210  const exprt s0_char =
1211  get(index_exprt(constraint.s0, plus_exprt(univ_var, i_expr)));
1212  const exprt s1_char = get(index_exprt(constraint.s1, i_expr));
1213  conjuncts.push_back(equal_exprt(s0_char, s1_char));
1214  }
1215  const exprt equal_strings = conjunction(conjuncts);
1216  return and_exprt(univ_bounds, get(constraint.premise), equal_strings);
1217 }
1218 
1223 template <typename T>
1225  messaget::mstreamt &stream,
1226  const T &axiom,
1227  const T &axiom_in_model,
1228  const exprt &negaxiom,
1229  const exprt &with_concretized_arrays)
1230 {
1231  stream << std::string(4, ' ') << "- axiom:\n" << std::string(6, ' ');
1232  stream << to_string(axiom);
1233  stream << '\n' << std::string(4, ' ') << "- axiom_in_model:\n"
1234  << std::string(6, ' ');
1235  stream << to_string(axiom_in_model) << '\n'
1236  << std::string(4, ' ') << "- negated_axiom:\n"
1237  << std::string(6, ' ') << format(negaxiom) << '\n';
1238  stream << std::string(4, ' ') << "- negated_axiom_with_concretized_arrays:\n"
1239  << std::string(6, ' ') << format(with_concretized_arrays) << '\n';
1240 }
1241 
1243 static std::pair<bool, std::vector<exprt>> check_axioms(
1244  const string_axiomst &axioms,
1245  string_constraint_generatort &generator,
1246  const std::function<exprt(const exprt &)> &get,
1247  messaget::mstreamt &stream,
1248  const namespacet &ns,
1249  bool use_counter_example,
1250  const union_find_replacet &symbol_resolve,
1251  const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
1252  &not_contain_witnesses)
1253 {
1254  const auto eom=messaget::eom;
1255  // clang-format off
1256  const auto gen_symbol = [&](const irep_idt &id, const typet &type)
1257  {
1258  return generator.fresh_symbol(id, type);
1259  };
1260  // clang-format on
1261 
1262  stream << "string_refinementt::check_axioms:" << eom;
1263 
1264  stream << "symbol_resolve:" << eom;
1265  auto pairs = symbol_resolve.to_vector();
1266  for(const auto &pair : pairs)
1267  stream << " - " << format(pair.first) << " --> " << format(pair.second)
1268  << eom;
1269 
1270 #ifdef DEBUG
1271  debug_model(
1272  generator, stream, ns, get, generator.fresh_symbol.created_symbols);
1273 #endif
1274 
1275  // Maps from indexes of violated universal axiom to a witness of violation
1276  std::map<size_t, exprt> violated;
1277 
1278  stream << "string_refinement::check_axioms: " << axioms.universal.size()
1279  << " universal axioms:" << eom;
1280  for(size_t i=0; i<axioms.universal.size(); i++)
1281  {
1282  const string_constraintt &axiom=axioms.universal[i];
1283  const string_constraintt axiom_in_model(
1284  axiom.univ_var,
1285  get(axiom.lower_bound),
1286  get(axiom.upper_bound),
1287  get(axiom.body));
1288 
1289  exprt negaxiom = axiom_in_model.negation();
1290  negaxiom = simplify_expr(negaxiom, ns);
1291 
1292  stream << std::string(2, ' ') << i << ".\n";
1293  const exprt with_concretized_arrays =
1294  substitute_array_access(negaxiom, gen_symbol, true);
1296  stream, axiom, axiom_in_model, negaxiom, with_concretized_arrays);
1297 
1298  if(
1299  const auto &witness =
1300  find_counter_example(ns, with_concretized_arrays, axiom.univ_var))
1301  {
1302  stream << std::string(4, ' ') << "- violated_for: "
1303  << format(axiom.univ_var) << "=" << format(*witness) << eom;
1304  violated[i]=*witness;
1305  }
1306  else
1307  stream << std::string(4, ' ') << "- correct" << eom;
1308  }
1309 
1310  // Maps from indexes of violated not_contains axiom to a witness of violation
1311  std::map<std::size_t, exprt> violated_not_contains;
1312 
1313  stream << "there are " << axioms.not_contains.size()
1314  << " not_contains axioms" << eom;
1315  for(std::size_t i = 0; i < axioms.not_contains.size(); i++)
1316  {
1317  const string_not_contains_constraintt &nc_axiom=axioms.not_contains[i];
1318  const symbol_exprt univ_var = generator.fresh_symbol(
1319  "not_contains_univ_var", nc_axiom.s0.length().type());
1320  const exprt negated_axiom = negation_of_not_contains_constraint(
1321  nc_axiom, univ_var, [&](const exprt &expr) {
1322  return simplify_expr(get(expr), ns); });
1323 
1324  stream << std::string(2, ' ') << i << ".\n";
1326  stream, nc_axiom, nc_axiom, negated_axiom, negated_axiom);
1327 
1328  if(
1329  const auto witness =
1330  find_counter_example(ns, negated_axiom, univ_var))
1331  {
1332  stream << std::string(4, ' ') << "- violated_for: "
1333  << univ_var.get_identifier() << "=" << format(*witness) << eom;
1334  violated_not_contains[i]=*witness;
1335  }
1336  }
1337 
1338  if(violated.empty() && violated_not_contains.empty())
1339  {
1340  stream << "no violated property" << eom;
1341  return { true, std::vector<exprt>() };
1342  }
1343  else
1344  {
1345  stream << violated.size()
1346  << " universal string axioms can be violated" << eom;
1347  stream << violated_not_contains.size()
1348  << " not_contains string axioms can be violated" << eom;
1349 
1350  if(use_counter_example)
1351  {
1352  std::vector<exprt> lemmas;
1353 
1354  for(const auto &v : violated)
1355  {
1356  const exprt &val=v.second;
1357  const string_constraintt &axiom=axioms.universal[v.first];
1358 
1359  exprt instance(axiom.body);
1360  replace_expr(axiom.univ_var, val, instance);
1361  // We are not sure the index set contains only positive numbers
1362  and_exprt bounds(
1363  axiom.univ_within_bounds(),
1364  binary_relation_exprt(from_integer(0, val.type()), ID_le, val));
1365  replace_expr(axiom.univ_var, val, bounds);
1366  const implies_exprt counter(bounds, instance);
1367  lemmas.push_back(counter);
1368  }
1369 
1370  for(const auto &v : violated_not_contains)
1371  {
1372  const exprt &val=v.second;
1373  const string_not_contains_constraintt &axiom=
1374  axioms.not_contains[v.first];
1375 
1376  const exprt func_val =
1377  index_exprt(not_contain_witnesses.at(axiom), val);
1378  const exprt comp_val=simplify_sum(plus_exprt(val, func_val));
1379 
1380  std::set<std::pair<exprt, exprt>> indices;
1381  indices.insert(std::pair<exprt, exprt>(comp_val, func_val));
1382  const exprt counter =
1383  ::instantiate_not_contains(axiom, indices, not_contain_witnesses)[0];
1384  lemmas.push_back(counter);
1385  }
1386  return { false, lemmas };
1387  }
1388  }
1389  return { false, std::vector<exprt>() };
1390 }
1391 
1396 static std::map<exprt, int> map_representation_of_sum(const exprt &f)
1397 {
1398  // number of time the leaf should be added (can be negative)
1399  std::map<exprt, int> elems;
1400 
1401  std::list<std::pair<exprt, bool> > to_process;
1402  to_process.emplace_back(f, true);
1403 
1404  while(!to_process.empty())
1405  {
1406  exprt cur=to_process.back().first;
1407  bool positive=to_process.back().second;
1408  to_process.pop_back();
1409  if(cur.id()==ID_plus)
1410  {
1411  for(const auto &op : cur.operands())
1412  to_process.emplace_back(op, positive);
1413  }
1414  else if(cur.id()==ID_minus)
1415  {
1416  to_process.emplace_back(cur.op1(), !positive);
1417  to_process.emplace_back(cur.op0(), positive);
1418  }
1419  else if(cur.id()==ID_unary_minus)
1420  {
1421  to_process.emplace_back(cur.op0(), !positive);
1422  }
1423  else
1424  {
1425  if(positive)
1426  elems[cur]=elems[cur]+1;
1427  else
1428  elems[cur]=elems[cur]-1;
1429  }
1430  }
1431  return elems;
1432 }
1433 
1441  std::map<exprt, int> &m,
1442  const typet &type,
1443  bool negated=false)
1444 {
1445  exprt sum=nil_exprt();
1446  mp_integer constants=0;
1447  typet index_type;
1448  if(m.empty())
1449  return from_integer(0, type);
1450  else
1451  index_type=m.begin()->first.type();
1452 
1453  for(const auto &term : m)
1454  {
1455  // We should group constants together...
1456  const exprt &t=term.first;
1457  int second=negated?(-term.second):term.second;
1458  if(t.id()==ID_constant)
1459  {
1460  const auto int_value = numeric_cast_v<mp_integer>(to_constant_expr(t));
1461  constants += int_value * second;
1462  }
1463  else
1464  {
1465  switch(second)
1466  {
1467  case -1:
1468  if(sum.is_nil())
1469  sum=unary_minus_exprt(t);
1470  else
1471  sum=minus_exprt(sum, t);
1472  break;
1473 
1474  case 1:
1475  if(sum.is_nil())
1476  sum=t;
1477  else
1478  sum=plus_exprt(sum, t);
1479  break;
1480 
1481  default:
1482  if(second>1)
1483  {
1484  if(sum.is_nil())
1485  sum=t;
1486  else
1487  plus_exprt(sum, t);
1488  for(int i=1; i<second; i++)
1489  sum=plus_exprt(sum, t);
1490  }
1491  else if(second<-1)
1492  {
1493  if(sum.is_nil())
1494  sum=unary_minus_exprt(t);
1495  else
1496  sum=minus_exprt(sum, t);
1497  for(int i=-1; i>second; i--)
1498  sum=minus_exprt(sum, t);
1499  }
1500  }
1501  }
1502  }
1503 
1504  exprt index_const=from_integer(constants, index_type);
1505  if(sum.is_not_nil())
1506  return plus_exprt(sum, index_const);
1507  else
1508  return index_const;
1509 }
1510 
1514 {
1515  std::map<exprt, int> map=map_representation_of_sum(f);
1516  return sum_over_map(map, f.type());
1517 }
1518 
1529  const exprt &qvar,
1530  const exprt &val,
1531  const exprt &f)
1532 {
1533  exprt positive, negative;
1534  // number of time the element should be added (can be negative)
1535  // qvar has to be equal to val - f(0) if it appears positively in f
1536  // (i.e. if f(qvar)=f(0) + qvar) and f(0) - val if it appears negatively
1537  // in f. So we start by computing val - f(0).
1538  std::map<exprt, int> elems=map_representation_of_sum(minus_exprt(val, f));
1539 
1540  // true if qvar appears negatively in f (positively in elems):
1541  bool neg=false;
1542 
1543  auto it=elems.find(qvar);
1544  INVARIANT(
1545  it!=elems.end(),
1546  string_refinement_invariantt("a function must have an occurrence of qvar"));
1547  if(it->second==1 || it->second==-1)
1548  {
1549  neg=(it->second==1);
1550  }
1551  else
1552  {
1553  INVARIANT(
1554  it->second == 0,
1556  "a proper function must have exactly one "
1557  "occurrences after reduction, or it cancelled out, and it does not"
1558  " have one"));
1559  }
1560 
1561  elems.erase(it);
1562  return sum_over_map(elems, f.type(), neg);
1563 }
1564 
1566 {
1567 private:
1568  const exprt &qvar_;
1569 
1570 public:
1571  bool found;
1572 
1573  explicit find_qvar_visitort(const exprt &qvar): qvar_(qvar), found(false) {}
1574 
1575  void operator()(const exprt &expr) override
1576  {
1577  if(expr==qvar_)
1578  found=true;
1579  }
1580 };
1581 
1586 static bool find_qvar(const exprt &index, const symbol_exprt &qvar)
1587 {
1588  find_qvar_visitort v2(qvar);
1589  index.visit(v2);
1590  return v2.found;
1591 }
1592 
1598 static void initial_index_set(
1599  index_set_pairt &index_set,
1600  const namespacet &ns,
1601  const string_axiomst &axioms)
1602 {
1603  for(const auto &axiom : axioms.universal)
1604  initial_index_set(index_set, ns, axiom);
1605  for(const auto &axiom : axioms.not_contains)
1606  initial_index_set(index_set, ns, axiom);
1607 }
1608 
1613 static void update_index_set(
1614  index_set_pairt &index_set,
1615  const namespacet &ns,
1616  const std::vector<exprt> &current_constraints)
1617 {
1618  for(const auto &axiom : current_constraints)
1619  update_index_set(index_set, ns, axiom);
1620 }
1621 
1628 static void get_sub_arrays(const exprt &array_expr, std::vector<exprt> &accu)
1629 {
1630  if(array_expr.id()==ID_if)
1631  {
1632  get_sub_arrays(to_if_expr(array_expr).true_case(), accu);
1633  get_sub_arrays(to_if_expr(array_expr).false_case(), accu);
1634  }
1635  else
1636  {
1637  if(array_expr.type().id() == ID_array)
1638  {
1639  // TODO: check_that it does not contain any sub_array
1640  accu.push_back(array_expr);
1641  }
1642  else
1643  {
1644  for(const auto &operand : array_expr.operands())
1645  get_sub_arrays(operand, accu);
1646  }
1647  }
1648 }
1649 
1655 static void add_to_index_set(
1656  index_set_pairt &index_set,
1657  const namespacet &ns,
1658  const exprt &s,
1659  exprt i)
1660 {
1661  simplify(i, ns);
1662  const bool is_size_t = numeric_cast<std::size_t>(i).has_value();
1663  if(i.id()!=ID_constant || is_size_t)
1664  {
1665  std::vector<exprt> sub_arrays;
1666  get_sub_arrays(s, sub_arrays);
1667  for(const auto &sub : sub_arrays)
1668  if(index_set.cumulative[sub].insert(i).second)
1669  index_set.current[sub].insert(i);
1670  }
1671 }
1672 
1688 static void initial_index_set(
1689  index_set_pairt &index_set,
1690  const namespacet &ns,
1691  const exprt &qvar,
1692  const exprt &upper_bound,
1693  const exprt &s,
1694  const exprt &i)
1695 {
1696  PRECONDITION(s.id() == ID_symbol || s.id() == ID_array || s.id() == ID_if);
1697  if(s.id() == ID_array)
1698  {
1699  for(std::size_t j = 0; j < s.operands().size(); ++j)
1700  add_to_index_set(index_set, ns, s, from_integer(j, i.type()));
1701  return;
1702  }
1703  if(auto ite = expr_try_dynamic_cast<if_exprt>(s))
1704  {
1705  initial_index_set(index_set, ns, qvar, upper_bound, ite->true_case(), i);
1706  initial_index_set(index_set, ns, qvar, upper_bound, ite->false_case(), i);
1707  return;
1708  }
1709  const minus_exprt u_minus_1(upper_bound, from_integer(1, upper_bound.type()));
1710  exprt i_copy = i;
1711  replace_expr(qvar, u_minus_1, i_copy);
1712  add_to_index_set(index_set, ns, s, i_copy);
1713 }
1714 
1715 static void initial_index_set(
1716  index_set_pairt &index_set,
1717  const namespacet &ns,
1718  const string_constraintt &axiom)
1719 {
1720  const symbol_exprt &qvar = axiom.univ_var;
1721  const auto &bound = axiom.upper_bound;
1722  auto it = axiom.body.depth_begin();
1723  const auto end = axiom.body.depth_end();
1724  while(it != end)
1725  {
1726  if(it->id() == ID_index && is_char_type(it->type()))
1727  {
1728  const auto &index_expr = to_index_expr(*it);
1729  const auto &s = index_expr.array();
1730  initial_index_set(index_set, ns, qvar, bound, s, index_expr.index());
1731  it.next_sibling_or_parent();
1732  }
1733  else
1734  ++it;
1735  }
1736 }
1737 
1738 static void initial_index_set(
1739  index_set_pairt &index_set,
1740  const namespacet &ns,
1741  const string_not_contains_constraintt &axiom)
1742 {
1743  auto it = axiom.premise.depth_begin();
1744  const auto end = axiom.premise.depth_end();
1745  while(it!=end)
1746  {
1747  if(it->id() == ID_index && is_char_type(it->type()))
1748  {
1749  const exprt &s=it->op0();
1750  const exprt &i=it->op1();
1751 
1752  // cur is of the form s[i] and no quantified variable appears in i
1753  add_to_index_set(index_set, ns, s, i);
1754 
1755  it.next_sibling_or_parent();
1756  }
1757  else
1758  ++it;
1759  }
1760 
1761  const minus_exprt kminus1(
1763  add_to_index_set(index_set, ns, axiom.s1.content(), kminus1);
1764 }
1765 
1770 static void update_index_set(
1771  index_set_pairt &index_set,
1772  const namespacet &ns,
1773  const exprt &formula)
1774 {
1775  std::list<exprt> to_process;
1776  to_process.push_back(formula);
1777 
1778  while(!to_process.empty())
1779  {
1780  exprt cur=to_process.back();
1781  to_process.pop_back();
1782  if(cur.id() == ID_index && is_char_type(cur.type()))
1783  {
1784  const exprt &s=cur.op0();
1785  const exprt &i=cur.op1();
1787  s.type().id()==ID_array,
1788  string_refinement_invariantt("index expressions must index on arrays"));
1789  exprt simplified=simplify_sum(i);
1790  if(s.id() != ID_array) // do not update index set of constant arrays
1791  add_to_index_set(index_set, ns, s, simplified);
1792  }
1793  else
1794  {
1795  forall_operands(it, cur)
1796  to_process.push_back(*it);
1797  }
1798  }
1799 }
1800 
1808 static std::unordered_set<exprt, irep_hash>
1809 find_indexes(const exprt &expr, const exprt &str, const symbol_exprt &qvar)
1810 {
1811  decltype(find_indexes(expr, str, qvar)) result;
1812  auto index_str_containing_qvar = [&](const exprt &e) {
1813  if(auto index_expr = expr_try_dynamic_cast<index_exprt>(e))
1814  {
1815  const auto &arr = index_expr->array();
1816  const auto str_it = std::find(arr.depth_begin(), arr.depth_end(), str);
1817  return str_it != arr.depth_end() && find_qvar(index_expr->index(), qvar);
1818  }
1819  return false;
1820  };
1821 
1822  std::for_each(expr.depth_begin(), expr.depth_end(), [&](const exprt &e) {
1823  if(index_str_containing_qvar(e))
1824  result.insert(to_index_expr(e).index());
1825  });
1826  return result;
1827 }
1828 
1845  const string_constraintt &axiom,
1846  const exprt &str,
1847  const exprt &val)
1848 {
1849  exprt::operandst conjuncts;
1850  for(const auto &index : find_indexes(axiom.body, str, axiom.univ_var))
1851  {
1852  const exprt univ_var_value =
1853  compute_inverse_function(axiom.univ_var, val, index);
1854  implies_exprt instance(
1855  and_exprt(
1856  binary_relation_exprt(axiom.univ_var, ID_ge, axiom.lower_bound),
1857  binary_relation_exprt(axiom.univ_var, ID_lt, axiom.upper_bound)),
1858  axiom.body);
1859  replace_expr(axiom.univ_var, univ_var_value, instance);
1860  conjuncts.push_back(instance);
1861  }
1862  return conjunction(conjuncts);
1863 }
1864 
1883 static std::vector<exprt> instantiate(
1884  const string_not_contains_constraintt &axiom,
1885  const index_set_pairt &index_set,
1886  const std::unordered_map<string_not_contains_constraintt, symbol_exprt>
1887  &witnesses)
1888 {
1889  const array_string_exprt &s0 = axiom.s0;
1890  const array_string_exprt &s1 = axiom.s1;
1891 
1892  const auto &index_set0=index_set.cumulative.find(s0.content());
1893  const auto &index_set1=index_set.cumulative.find(s1.content());
1894  const auto &current_index_set0=index_set.current.find(s0.content());
1895  const auto &current_index_set1=index_set.current.find(s1.content());
1896 
1897  if(index_set0!=index_set.cumulative.end() &&
1898  index_set1!=index_set.cumulative.end() &&
1899  current_index_set0!=index_set.current.end() &&
1900  current_index_set1!=index_set.current.end())
1901  {
1902  typedef std::pair<exprt, exprt> expr_pairt;
1903  std::set<expr_pairt> index_pairs;
1904 
1905  for(const auto &ic0 : current_index_set0->second)
1906  for(const auto &i1 : index_set1->second)
1907  index_pairs.insert(expr_pairt(ic0, i1));
1908  for(const auto &ic1 : current_index_set1->second)
1909  for(const auto &i0 : index_set0->second)
1910  index_pairs.insert(expr_pairt(i0, ic1));
1911 
1912  return ::instantiate_not_contains(axiom, index_pairs, witnesses);
1913  }
1914  return { };
1915 }
1916 
1924 exprt substitute_array_lists(exprt expr, size_t string_max_length)
1925 {
1926  for(auto &operand : expr.operands())
1927  operand = substitute_array_lists(operand, string_max_length);
1928 
1929  if(expr.id() == ID_array_list)
1930  {
1932  expr.operands().size()>=2,
1933  string_refinement_invariantt("array-lists must have at least two "
1934  "operands"));
1935  const typet &char_type = expr.operands()[1].type();
1937  exprt ret_expr=array_of_exprt(from_integer(0, char_type), arr_type);
1938 
1939  for(size_t i=0; i<expr.operands().size(); i+=2)
1940  {
1941  const exprt &index=expr.operands()[i];
1942  const exprt &value=expr.operands()[i+1];
1943  const auto index_value = numeric_cast<std::size_t>(index);
1944  if(!index.is_constant() ||
1945  (index_value && *index_value<string_max_length))
1946  ret_expr=with_exprt(ret_expr, index, value);
1947  }
1948  return ret_expr;
1949  }
1950 
1951  return expr;
1952 }
1953 
1962 {
1963  const auto super_get = [this](const exprt &expr) {
1964  return supert::get(expr);
1965  };
1966  exprt ecopy(expr);
1967  (void)symbol_resolve.replace_expr(ecopy);
1968 
1969  // Special treatment for index expressions
1970  const auto &index_expr = expr_try_dynamic_cast<index_exprt>(ecopy);
1971  if(index_expr && is_char_type(index_expr->type()))
1972  {
1973  std::reference_wrapper<const exprt> current(index_expr->array());
1974  while(current.get().id() == ID_if)
1975  {
1976  const auto &if_expr = expr_dynamic_cast<if_exprt>(current.get());
1977  const exprt cond = get(if_expr.cond());
1978  if(cond.is_true())
1979  current = std::cref(if_expr.true_case());
1980  else if(cond.is_false())
1981  current = std::cref(if_expr.false_case());
1982  else
1983  UNREACHABLE;
1984  }
1985  const auto array = supert::get(current.get());
1986  const auto index = get(index_expr->index());
1987  const exprt unknown =
1988  from_integer(CHARACTER_FOR_UNKNOWN, index_expr->type());
1989  if(
1990  const auto sparse_array = interval_sparse_arrayt::of_expr(array, unknown))
1991  {
1992  if(const auto index_value = numeric_cast<std::size_t>(index))
1993  return sparse_array->at(*index_value);
1994  return sparse_array->to_if_expression(index);
1995  }
1996 
1997  INVARIANT(
1998  array.is_nil() || array.id() == ID_symbol,
1999  std::string(
2000  "apart from symbols, array valuations can be interpreted as "
2001  "sparse arrays, id: ") +
2002  id2string(array.id()));
2003  return index_exprt(array, index);
2004  }
2005 
2006  if(is_char_array_type(ecopy.type(), ns))
2007  {
2009  arr.length() = generator.array_pool.get_length(arr);
2010 
2011  if(
2012  const auto from_dependencies =
2013  dependencies.eval(arr, [&](const exprt &expr) { return get(expr); }))
2014  return *from_dependencies;
2015 
2016  if(
2017  const auto arr_model_opt =
2018  get_array(super_get, ns, debug(), arr))
2019  return *arr_model_opt;
2020 
2021  if(generator.array_pool.created_strings().count(arr))
2022  {
2023  const exprt length = super_get(arr.length());
2024  if(const auto n = numeric_cast<std::size_t>(length))
2025  {
2026  const interval_sparse_arrayt sparse_array(
2028  return sparse_array.concretize(*n, length.type());
2029  }
2030  }
2031  return arr;
2032  }
2033  return supert::get(ecopy);
2034 }
2035 
2045  const namespacet &ns,
2046  const exprt &axiom,
2047  const symbol_exprt &var)
2048 {
2049  satcheck_no_simplifiert sat_check;
2050  boolbvt solver(ns, sat_check);
2051  solver << axiom;
2052 
2054  return solver.get(var);
2055  else
2056  return { };
2057 }
2058 
2060 typedef std::map<exprt, std::vector<exprt>> array_index_mapt;
2061 
2064 {
2065  array_index_mapt indices;
2066  // clang-format off
2067  std::for_each(
2068  expr.depth_begin(),
2069  expr.depth_end(),
2070  [&](const exprt &expr)
2071  {
2072  const auto index_expr = expr_try_dynamic_cast<const index_exprt>(expr);
2073  if(index_expr)
2074  indices[index_expr->array()].push_back(index_expr->index());
2075  });
2076  // clang-format on
2077  return indices;
2078 }
2079 
2085 static bool
2087 {
2088  for(auto it = expr.depth_begin(); it != expr.depth_end();)
2089  {
2090  if(
2091  it->id() != ID_plus && it->id() != ID_minus &&
2092  it->id() != ID_unary_minus && *it != var)
2093  {
2094  if(find_qvar(*it, var))
2095  return false;
2096  else
2097  it.next_sibling_or_parent();
2098  }
2099  else
2100  ++it;
2101  }
2102  return true;
2103 }
2104 
2113 {
2114  for(auto it = constr.body.depth_begin(); it != constr.body.depth_end();)
2115  {
2116  if(*it == constr.univ_var)
2117  return false;
2118  if(it->id() == ID_index)
2119  it.next_sibling_or_parent();
2120  else
2121  ++it;
2122  }
2123  return true;
2124 }
2125 
2133  messaget::mstreamt &stream,
2134  const namespacet &ns,
2135  const string_constraintt &constraint)
2136 {
2137  const auto eom=messaget::eom;
2138  const array_index_mapt body_indices = gather_indices(constraint.body);
2139  // Must validate for each string. Note that we have an invariant that the
2140  // second value in the pair is non-empty.
2141  for(const auto &pair : body_indices)
2142  {
2143  // Condition 1: All indices of the same string must be the of the same form
2144  const exprt rep=pair.second.back();
2145  for(size_t j=0; j<pair.second.size()-1; j++)
2146  {
2147  const exprt i=pair.second[j];
2148  const equal_exprt equals(rep, i);
2149  const exprt result=simplify_expr(equals, ns);
2150  if(result.is_false())
2151  {
2152  stream << "Indices not equal: " << to_string(constraint)
2153  << ", str: " << format(pair.first) << eom;
2154  return false;
2155  }
2156  }
2157 
2158  // Condition 2: f must be linear in the quantified variable
2159  if(!is_linear_arithmetic_expr(rep, constraint.univ_var))
2160  {
2161  stream << "f is not linear: " << to_string(constraint)
2162  << ", str: " << format(pair.first) << eom;
2163  return false;
2164  }
2165 
2166  // Condition 3: the quantified variable can only occur in indices in the
2167  // body
2168  if(!universal_only_in_index(constraint))
2169  {
2170  stream << "Universal variable outside of index:" << to_string(constraint)
2171  << eom;
2172  return false;
2173  }
2174  }
2175 
2176  return true;
2177 }
string_refinementt::loop_bound_
std::size_t loop_bound_
Definition: string_refinement.h:93
with_exprt
Operator to update elements in structs and arrays.
Definition: std_expr.h:3514
string_axiomst::universal
std::vector< string_constraintt > universal
Definition: string_refinement_util.h:61
struct_union_typet::components
const componentst & components() const
Definition: std_types.h:205
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
format
static format_containert< T > format(const T &o)
Definition: format.h:35
prop_conv_solvert::equality_propagation
bool equality_propagation
Definition: prop_conv.h:112
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
check_axioms
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...
Definition: string_refinement.cpp:1243
string_refinementt::generator
string_constraint_generatort generator
Definition: string_refinement.h:94
typet::subtype
const typet & subtype() const
Definition: type.h:38
array_poolt::get_arrays_of_pointers
const std::unordered_map< exprt, array_string_exprt, irep_hash > & get_arrays_of_pointers() const
Definition: string_constraint_generator.h:58
conjunction
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:50
union_find_replacet::to_vector
std::vector< std::pair< exprt, exprt > > to_vector() const
Definition: union_find_replace.cpp:46
fill_in_map_as_vector
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.
Definition: string_refinement.cpp:137
generate_instantiations
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.
Definition: string_refinement.cpp:229
to_struct_type
const struct_typet & to_struct_type(const typet &type)
Cast a typet to a struct_typet.
Definition: std_types.h:349
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
exprt::depth_begin
depth_iteratort depth_begin()
Definition: expr.cpp:282
instantiate_not_contains
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)
extract_strings
static std::vector< exprt > extract_strings(const exprt &expr)
Definition: string_refinement.cpp:402
string_not_contains_constraintt::univ_upper_bound
exprt univ_upper_bound
Definition: string_constraint.h:128
typet
The type of an expression, extends irept.
Definition: type.h:27
negation_of_not_contains_constraint
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.
Definition: string_refinement.cpp:1189
debug_check_axioms_step
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...
Definition: string_refinement.cpp:1224
display_index_set
static void display_index_set(messaget::mstreamt &stream, const index_set_pairt &index_set)
Write index set to the given stream, use for debugging.
Definition: string_refinement.cpp:179
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1648
to_if_expr
const if_exprt & to_if_expr(const exprt &expr)
Cast an exprt to an if_exprt.
Definition: std_expr.h:3482
array_poolt::get_length
exprt get_length(const array_string_exprt &s) const
Associate an actual finite length to infinite arrays.
Definition: string_constraint_generator_main.cpp:72
boolbvt::set_to
void set_to(const exprt &expr, bool value) override
Definition: boolbv.cpp:593
string_refinementt::current_constraints
std::vector< exprt > current_constraints
Definition: string_refinement.h:102
add_node
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...
Definition: string_refinement_util.cpp:373
string_constraintt
Definition: string_constraint.h:58
mp_integer
BigInt mp_integer
Definition: mp_arith.h:22
if_exprt
The trinary if-then-else operator.
Definition: std_expr.h:3427
is_char_type
bool is_char_type(const typet &type)
For now, any unsigned bitvector type of width smaller or equal to 16 is considered a character.
Definition: string_refinement_util.cpp:30
index_set_pairt
Definition: string_refinement_util.h:53
interval_sparse_arrayt
Represents arrays by the indexes up to which the value remains the same.
Definition: string_refinement_util.h:92
replace
void replace(const union_find_replacet &replace_map, string_not_contains_constraintt &constraint)
Definition: string_constraint.cpp:65
string_constraint_generatort::fresh_symbol
symbol_generatort fresh_symbol
Definition: string_constraint_generator.h:133
interval_sparse_arrayt::to_if_expression
exprt to_if_expression(const exprt &index) const
Definition: string_refinement_util.cpp:97
string_refinementt::equations
std::vector< equal_exprt > equations
Definition: string_refinement.h:110
union_find_replacet::replace_expr
bool replace_expr(exprt &expr) const
Replace subexpressions of expr by the representative element of the set they belong to.
Definition: union_find_replace.cpp:28
and_exprt
Boolean AND.
Definition: std_expr.h:2409
find_qvar_visitort::found
bool found
Definition: string_refinement.cpp:1571
s1
int8_t s1
Definition: bytecode_info.h:59
MAX_CONCRETE_STRING_SIZE
const std::size_t MAX_CONCRETE_STRING_SIZE
Definition: magic.h:14
binary_relation_exprt::rhs
exprt & rhs()
Definition: std_expr.h:931
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
exprt
Base class for all expressions.
Definition: expr.h:54
INVARIANT
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition: invariant.h:400
binary_relation_exprt::lhs
exprt & lhs()
Definition: std_expr.h:921
exprt::op0
exprt & op0()
Definition: expr.h:84
propt::l_set_to_true
void l_set_to_true(literalt a)
Definition: prop.h:49
array_string_exprt::content
exprt & content()
Definition: string_expr.h:80
string_constraint_generatort::make_array_pointer_association
optionalt< exprt > make_array_pointer_association(const function_application_exprt &expr)
Associate array to pointer, and array to length.
Definition: string_constraint_generator_main.cpp:352
interval_sparse_arrayt::of_expr
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,...
Definition: string_refinement_util.cpp:150
get_sub_arrays
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...
Definition: string_refinement.cpp:1628
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:53
messaget::eom
static eomt eom
Definition: message.h:284
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
string_refinementt::index_sets
index_set_pairt index_sets
Definition: string_refinement.h:107
string_not_contains_constraintt::exists_upper_bound
exprt exists_upper_bound
Definition: string_constraint.h:131
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:143
string_axiomst
Definition: string_refinement_util.h:59
simplify_expr
exprt simplify_expr(const exprt &src, const namespacet &ns)
Definition: simplify_expr.cpp:2325
index_type
bitvector_typet index_type()
Definition: c_types.cpp:16
equal_exprt
Equality.
Definition: std_expr.h:1484
magic.h
Magic numbers used throughout the codebase.
exprt::visit
void visit(class expr_visitort &visitor)
Definition: expr.cpp:246
string_constraintt::univ_var
symbol_exprt univ_var
Definition: string_constraint.h:63
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:478
string_constraint_generatort::array_pool
array_poolt array_pool
Definition: string_constraint_generator.h:135
string_not_contains_constraintt::premise
exprt premise
Definition: string_constraint.h:129
infinity_exprt
An expression denoting infinity.
Definition: std_expr.h:4625
if_exprt::false_case
exprt & false_case()
Definition: std_expr.h:3465
sparse_arrayt::to_if_expression
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.
Definition: string_refinement_util.cpp:76
string_constraint_generatort
Definition: string_constraint_generator.h:120
exprt::is_false
bool is_false() const
Return whether the expression is a constant representing false.
Definition: expr.cpp:99
initial_index_set
static void initial_index_set(index_set_pairt &index_set, const namespacet &ns, const string_constraintt &axiom)
Definition: string_refinement.cpp:1715
string_constraintt::upper_bound
exprt upper_bound
Definition: string_constraint.h:65
substitute_array_access
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)
Definition: string_refinement.cpp:1103
string_constraintt::array_index_mapt
std::map< exprt, std::vector< exprt > > array_index_mapt
Definition: string_refinement.cpp:2060
string_constraintt::body
exprt body
Definition: string_constraint.h:66
decision_proceduret::resultt::D_SATISFIABLE
find_indexes
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'),...
Definition: string_refinement.cpp:1809
string_constraintt::lower_bound
exprt lower_bound
Definition: string_constraint.h:64
instantiate
static exprt instantiate(const string_constraintt &axiom, const exprt &str, const exprt &val)
Substitute qvar the universally quantified variable of axiom, by an index val, in axiom,...
Definition: string_refinement.cpp:1844
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
get_array
static optionalt< exprt > get_array(const std::function< exprt(const exprt &)> &super_get, const namespacet &ns, messaget::mstreamt &stream, const array_string_exprt &arr)
Get a model of an array and put it in a certain form.
Definition: string_refinement.cpp:900
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
irept::is_not_nil
bool is_not_nil() const
Definition: irep.h:173
is_valid_string_constraint
static bool is_valid_string_constraint(messaget::mstreamt &stream, const namespacet &ns, const string_constraintt &constraint)
find_qvar
static bool find_qvar(const exprt &index, const symbol_exprt &qvar)
look for the symbol and return true if it is found
Definition: string_refinement.cpp:1586
validate
static bool validate(const string_refinementt::infot &info)
Definition: string_refinement.cpp:160
is_char_pointer_type
bool is_char_pointer_type(const typet &type)
For now, any unsigned bitvector type is considered a character.
Definition: string_refinement_util.cpp:44
bv_refinementt::dec_solve
decision_proceduret::resultt dec_solve() override
Definition: bv_refinement_loop.cpp:24
messaget::error
mstreamt & error() const
Definition: message.h:386
string_dependenciest::clean_cache
void clean_cache()
Clean the cache used by eval
Definition: string_refinement_util.cpp:366
CHARACTER_FOR_UNKNOWN
#define CHARACTER_FOR_UNKNOWN
Definition: string_builtin_function.h:16
string_identifiers_resolution_from_equations
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.
Definition: string_refinement.cpp:463
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
substitute_array_lists
exprt substitute_array_lists(exprt expr, size_t string_max_length)
Replace array-lists by 'with' expressions.
Definition: string_refinement.cpp:1924
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:20
string_of_array
static std::string string_of_array(const array_exprt &arr)
convert the content of a string to a more readable representation.
Definition: string_refinement.cpp:957
string_refinementt::get
exprt get(const exprt &expr) const override
Evaluates the given expression in the valuation found by string_refinementt::dec_solve.
Definition: string_refinement.cpp:1961
string_dependenciest::eval
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...
Definition: string_refinement_util.cpp:344
string_not_contains_constraintt::exists_lower_bound
exprt exists_lower_bound
Definition: string_constraint.h:130
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
has_subtype
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
Definition: expr_util.cpp:153
string_constraint_generatort::constraints
string_constraintst constraints
Definition: string_constraint_generator.h:137
string_dependenciest::output_dot
void output_dot(std::ostream &stream) const
Definition: string_refinement_util.cpp:480
nil_exprt
The NIL expression.
Definition: std_expr.h:4461
array_of_exprt
Array constructor from single element.
Definition: std_expr.h:1678
bv_refinementt::infot::prop
propt * prop
Definition: bv_refinement.h:36
string_constraintt::is_valid_string_constraint
static bool is_valid_string_constraint(messaget::mstreamt &stream, const namespacet &ns, const string_constraintt &constraint)
Checks the data invariant for string_constraintt.
Definition: string_refinement.cpp:2132
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2320
exprt::op1
exprt & op1()
Definition: expr.h:87
is_char_array_type
bool is_char_array_type(const typet &type, const namespacet &ns)
Distinguish char array from other types.
Definition: string_refinement_util.cpp:37
index_exprt::index
exprt & index()
Definition: std_expr.h:1631
make_char_array_pointer_associations
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...
Definition: string_refinement.cpp:255
const_expr_visitort
Definition: expr.h:328
decision_proceduret::ns
const namespacet & ns
Definition: decision_procedure.h:61
string_dependenciest::add_constraints
void add_constraints(string_constraint_generatort &generatort)
For all builtin call on which a test (or an unsupported buitin) result depends, add the corresponding...
Definition: string_refinement_util.cpp:505
unary_minus_exprt
The unary minus expression.
Definition: std_expr.h:469
index_exprt::array
exprt & array()
Definition: std_expr.h:1621
string_constraintst::clear
void clear()
Clear all constraints.
Definition: string_constraint_generator_main.cpp:217
decision_proceduret::resultt::D_ERROR
irept::is_nil
bool is_nil() const
Definition: irep.h:172
irept::id
const irep_idt & id() const
Definition: irep.h:259
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:57
string_refinementt::axioms
string_axiomst axioms
Definition: string_refinement.h:99
equation_symbol_mappingt::add
void add(const std::size_t i, const exprt &expr)
Record the fact that equation i contains expression expr
Definition: string_refinement_util.cpp:186
string_refinement.h
update_index_set
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.
Definition: string_refinement.cpp:1613
equation_symbol_mappingt
Maps equation to expressions contained in them and conversely expressions to equations that contain t...
Definition: string_refinement_util.h:140
add_to_index_set
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.
Definition: string_refinement.cpp:1655
debug_model
void debug_model(const string_constraint_generatort &generator, messaget::mstreamt &stream, const namespacet &ns, const std::function< exprt(const exprt &)> &super_get, const std::vector< symbol_exprt > &symbols)
Display part of the current model by mapping the variables created by the solver to constant expressi...
Definition: string_refinement.cpp:1021
to_array_string_expr
array_string_exprt & to_array_string_expr(exprt &expr)
Definition: string_expr.h:101
compute_inverse_function
static exprt compute_inverse_function(const exprt &qvar, const exprt &val, const exprt &f)
Definition: string_refinement.cpp:1528
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
bv_refinementt
Definition: bv_refinement.h:19
string_refinementt::symbol_resolve
union_find_replacet symbol_resolve
Definition: string_refinement.h:108
find_counter_example
static optionalt< exprt > find_counter_example(const namespacet &ns, const exprt &axiom, const symbol_exprt &var)
Creates a solver with axiom as the only formula added and runs it.
Definition: string_refinement.cpp:2044
prop_conv_solvert::convert
literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:157
decision_proceduret::resultt
resultt
Definition: decision_procedure.h:47
utf16_constant_array_to_java
std::string utf16_constant_array_to_java(const array_exprt &arr, std::size_t length)
Construct a string from a constant array.
Definition: string_constraint_generator_format.cpp:483
minus_exprt
Binary minus.
Definition: std_expr.h:1106
union_find_replacet::make_union
exprt make_union(const exprt &a, const exprt &b)
Merge the set containing a and the set containing b.
Definition: union_find_replace.cpp:15
string_constraintt::negation
exprt negation() const
Definition: string_constraint.h:100
string_refinementt::dec_solve
decision_proceduret::resultt dec_solve() override
Main decision procedure of the solver.
Definition: string_refinement.cpp:610
string_refinementt::dependencies
string_dependenciest dependencies
Definition: string_refinement.h:112
char_type
bitvector_typet char_type()
Definition: c_types.cpp:114
simplify_expr.h
string_not_contains_constraintt::univ_lower_bound
exprt univ_lower_bound
Definition: string_constraint.h:127
add_equations_for_symbol_resolution
static void add_equations_for_symbol_resolution(union_find_replacet &symbol_solver, const std::vector< equal_exprt > &equations, const namespacet &ns, messaget::mstreamt &stream)
Add association for each char pointer in the equation.
Definition: string_refinement.cpp:312
member_exprt
Extract member of struct or union.
Definition: std_expr.h:3890
expr_util.h
Deprecated expression utility functions.
satcheck.h
string_constraintt::univ_within_bounds
exprt univ_within_bounds() const
Definition: string_constraint.h:86
string_refinementt
Definition: string_refinement.h:62
interval_sparse_arrayt::concretize
array_exprt concretize(std::size_t size, const typet &index_type) const
Convert to an array representation, ignores elements at index >= size.
Definition: string_refinement_util.cpp:168
struct_typet
Structure type, corresponds to C style structs.
Definition: std_types.h:276
sum_over_map
static exprt sum_over_map(std::map< exprt, int > &m, const typet &type, bool negated=false)
Definition: string_refinement.cpp:1440
array_typet
Arrays with given size.
Definition: std_types.h:1000
expr_iterator.h
string_constraintt::universal_only_in_index
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...
Definition: string_refinement.cpp:2112
if_exprt::true_case
exprt & true_case()
Definition: std_expr.h:3455
replace_expr_copy
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...
Definition: string_refinement.cpp:276
substitute_array_access_in_place
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 ...
Definition: string_refinement.cpp:1133
find_qvar_visitort::operator()
void operator()(const exprt &expr) override
Definition: string_refinement.cpp:1575
union_find_replacet
Similar interface to union-find for expressions, with a function for replacing sub-expressions by the...
Definition: union_find_replace.h:16
replace_expr
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
Definition: replace_expr.cpp:12
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
string_refinementt::instantiate_not_contains
std::vector< exprt > instantiate_not_contains(const string_not_contains_constraintt &axiom, const std::set< std::pair< exprt, exprt >> &index_pairs, const std::unordered_map< string_not_contains_constraintt, symbol_exprt > &witnesses)
Instantiates a quantified formula representing not_contains by substituting the quantifiers and gener...
Definition: string_constraint_instantiation.cpp:21
string_refinement_invariantt
#define string_refinement_invariantt(reason)
Definition: string_refinement_invariant.h:12
solver
int solver(std::istream &in)
Definition: smt2_solver.cpp:360
has_char_pointer_subtype
bool has_char_pointer_subtype(const typet &type, const namespacet &ns)
Definition: string_refinement_util.cpp:49
exprt::is_constant
bool is_constant() const
Return whether the expression is a constant.
Definition: expr.cpp:83
if_exprt::cond
exprt & cond()
Definition: std_expr.h:3445
array_string_exprt::length
exprt & length()
Definition: string_expr.h:70
string_typet
String type.
Definition: std_types.h:1662
string_constraint_instantiation.h
binary_relation_exprt
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:878
simplify_sum
exprt simplify_sum(const exprt &f)
Definition: string_refinement.cpp:1513
to_array_type
const array_typet & to_array_type(const typet &type)
Cast a typet to an array_typet.
Definition: std_types.h:1048
to_equal_expr
const equal_exprt & to_equal_expr(const exprt &expr)
Cast an exprt to an equal_exprt.
Definition: std_expr.h:1519
get_char_array_and_concretize
static exprt get_char_array_and_concretize(const std::function< exprt(const exprt &)> &super_get, const namespacet &ns, messaget::mstreamt &stream, const array_string_exprt &arr)
Debugging function which finds the valuation of the given array in super_get and concretize unknown c...
Definition: string_refinement.cpp:974
string_not_contains_constraintt::s0
array_string_exprt s0
Definition: string_constraint.h:132
find_qvar_visitort::find_qvar_visitort
find_qvar_visitort(const exprt &qvar)
Definition: string_refinement.cpp:1573
boolbvt
Definition: boolbv.h:32
array_poolt::created_strings
const std::set< array_string_exprt > & created_strings() const
Definition: string_constraint_generator_main.cpp:160
index_set_pairt::current
std::map< exprt, std::set< exprt > > current
Definition: string_refinement_util.h:56
equation_symbol_mappingt::find_expressions
std::vector< exprt > find_expressions(const std::size_t i)
Definition: string_refinement_util.cpp:193
messaget::mstreamt
Definition: message.h:212
string_constraintst::not_contains
std::vector< string_not_contains_constraintt > not_contains
Definition: string_constraint_generator.h:112
implies_exprt
Boolean implication.
Definition: std_expr.h:2485
string_refinementt::add_lemma
void add_lemma(const exprt &lemma, bool simplify_lemma=true)
Add the given lemma to the solver.
Definition: string_refinement.cpp:849
string_not_contains_constraintt
Constraints to encode non containement of strings.
Definition: string_constraint.h:125
index_set_pairt::cumulative
std::map< exprt, std::set< exprt > > cumulative
Definition: string_refinement_util.h:55
string_constraintt::is_linear_arithmetic_expr
static bool is_linear_arithmetic_expr(const exprt &expr, const symbol_exprt &var)
Definition: string_refinement.cpp:2086
string_refinementt::infot
string_refinementt constructor arguments
Definition: string_refinement.h:72
exprt::operands
operandst & operands()
Definition: expr.h:78
messaget::debug
mstreamt & debug() const
Definition: message.h:416
string_refinementt::config_
const configt config_
Definition: string_refinement.h:92
string_constraintt::gather_indices
static array_index_mapt gather_indices(const exprt &expr)
Definition: string_refinement.cpp:2063
string_refinementt::set_to
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...
Definition: string_refinement.cpp:286
index_exprt
Array index operator.
Definition: std_expr.h:1595
string_not_contains_constraintt::s1
array_string_exprt s1
Definition: string_constraint.h:133
bv_refinementt::infot::ns
const namespacet * ns
Definition: bv_refinement.h:35
constant_exprt
A constant literal expression.
Definition: std_expr.h:4384
extract_strings_from_lhs
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.
Definition: string_refinement.cpp:379
exprt::depth_end
depth_iteratort depth_end()
Definition: expr.cpp:284
string_refinementt::configt::use_counter_example
bool use_counter_example
Definition: string_refinement.h:68
neg
literalt neg(literalt a)
Definition: literal.h:192
map_representation_of_sum
static std::map< exprt, int > map_representation_of_sum(const exprt &f)
Definition: string_refinement.cpp:1396
string_refinementt::string_refinementt
string_refinementt(const infot &)
Definition: string_refinement.cpp:175
has_char_array_subexpr
bool has_char_array_subexpr(const exprt &expr, const namespacet &ns)
Definition: string_refinement_util.cpp:54
equation_symbol_mappingt::find_equations
std::vector< std::size_t > find_equations(const exprt &expr)
Definition: string_refinement_util.cpp:199
array_exprt
Array constructor from list of elements.
Definition: std_expr.h:1739
add_string_equation_to_symbol_resolution
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...
Definition: string_refinement.cpp:430
string_axiomst::not_contains
std::vector< string_not_contains_constraintt > not_contains
Definition: string_refinement_util.h:62
array_string_exprt
Definition: string_expr.h:67
find_qvar_visitort::qvar_
const exprt & qvar_
Definition: string_refinement.cpp:1568
boolbvt::get
exprt get(const exprt &expr) const override
Definition: boolbv_get.cpp:21
can_cast_expr< function_application_exprt >
bool can_cast_expr< function_application_exprt >(const exprt &base)
Definition: std_expr.h:4544
string_refinementt::seen_instances
std::set< exprt > seen_instances
Definition: string_refinement.h:97
validation_modet::INVARIANT
prop_conv_solvert::prop
propt & prop
Definition: prop_conv.h:152
find_qvar_visitort
Definition: string_refinement.cpp:1565
string_constraintst::existential
std::vector< exprt > existential
Definition: string_constraint_generator.h:110
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:4423
string_constraintst::universal
std::vector< string_constraintt > universal
Definition: string_constraint_generator.h:111