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,
41  const exprt &axiom,
42  const symbol_exprt &var);
43 
60 static std::pair<bool, std::vector<exprt>> check_axioms(
61  const string_axiomst &axioms,
63  const std::function<exprt(const exprt &)> &get,
64  messaget::mstreamt &stream,
65  const namespacet &ns,
66  std::size_t max_string_length,
67  bool use_counter_example,
69  const union_find_replacet &symbol_resolve);
70 
71 static void initial_index_set(
72  index_set_pairt &index_set,
73  const namespacet &ns,
74  const string_constraintt &axiom);
75 
76 static void initial_index_set(
77  index_set_pairt &index_set,
78  const namespacet &ns,
79  const string_not_contains_constraintt &axiom);
80 
81 static void initial_index_set(
82  index_set_pairt &index_set,
83  const namespacet &ns,
84  const string_axiomst &axioms);
85 
86 exprt simplify_sum(const exprt &f);
87 
88 static void update_index_set(
89  index_set_pairt &index_set,
90  const namespacet &ns,
91  const std::vector<exprt> &current_constraints);
92 
93 static void update_index_set(
94  index_set_pairt &index_set,
95  const namespacet &ns,
96  const exprt &formula);
97 
108 static exprt instantiate(
109  messaget::mstreamt &stream,
110  const string_constraintt &axiom,
111  const exprt &str,
112  const exprt &val);
113 
114 static std::vector<exprt> instantiate(
115  const string_not_contains_constraintt &axiom,
116  const index_set_pairt &index_set,
117  const string_constraint_generatort &generator);
118 
120  const std::function<exprt(const exprt &)> &super_get,
121  const namespacet &ns,
122  const std::size_t max_string_length,
123  messaget::mstreamt &stream,
124  const array_string_exprt &arr);
125 
127  const index_exprt &index_expr,
128  const std::function<symbol_exprt(const irep_idt &, const typet &)>
129  &symbol_generator,
130  const bool left_propagate);
131 
139 template <typename T>
140 static std::vector<T> fill_in_map_as_vector(
141  const std::map<std::size_t, T> &index_value)
142 {
143  std::vector<T> result;
144  if(!index_value.empty())
145  {
146  result.resize(index_value.rbegin()->first+1);
147  for(auto it=index_value.rbegin(); it!=index_value.rend(); ++it)
148  {
149  const std::size_t index=it->first;
150  const T &value = it->second;
151  const auto next=std::next(it);
152  const std::size_t leftmost_index_to_pad=
153  next!=index_value.rend()
154  ? next->first+1
155  : 0;
156  for(std::size_t j=leftmost_index_to_pad; j<=index; j++)
157  result[j]=value;
158  }
159  }
160  return result;
161 }
162 
163 static bool validate(const string_refinementt::infot &info)
164 {
165  PRECONDITION(info.ns);
166  PRECONDITION(info.prop);
167  return true;
168 }
169 
171  : supert(info),
172  config_(info),
173  loop_bound_(info.refinement_bound),
174  max_string_length(info.max_string_length),
175  generator(*info.ns)
176 {
177 }
178 
180  string_refinementt(info, validate(info)) { }
181 
183 static void display_index_set(
184  messaget::mstreamt &stream,
185  const index_set_pairt &index_set)
186 {
187  const auto eom=messaget::eom;
188  std::size_t count=0;
189  std::size_t count_current=0;
190  for(const auto &i : index_set.cumulative)
191  {
192  const exprt &s=i.first;
193  stream << "IS(" << format(s) << ")=={" << eom;
194 
195  for(const auto &j : i.second)
196  {
197  const auto it=index_set.current.find(i.first);
198  if(it!=index_set.current.end() && it->second.find(j)!=it->second.end())
199  {
200  count_current++;
201  stream << "**";
202  }
203  stream << " " << format(j) << ";" << eom;
204  count++;
205  }
206  stream << "}" << eom;
207  }
208  stream << count << " elements in index set (" << count_current
209  << " newly added)" << eom;
210 }
211 
225 // NOLINTNEXTLINE
233 static std::vector<exprt> generate_instantiations(
234  messaget::mstreamt &stream,
235  const namespacet &ns,
236  const string_constraint_generatort &generator,
237  const index_set_pairt &index_set,
238  const string_axiomst &axioms)
239 {
240  std::vector<exprt> lemmas;
241  for(const auto &i : index_set.current)
242  {
243  for(const auto &univ_axiom : axioms.universal)
244  {
245  for(const auto &j : i.second)
246  lemmas.push_back(instantiate(stream, univ_axiom, i.first, j));
247  }
248  }
249  for(const auto &nc_axiom : axioms.not_contains)
250  {
251  for(const auto &instance :
252  instantiate(nc_axiom, index_set, generator))
253  lemmas.push_back(instance);
254  }
255  return lemmas;
256 }
257 
261  string_constraint_generatort &generator,
262  std::vector<equal_exprt> &equations)
263 {
264  for(equal_exprt &eq : equations)
265  {
266  if(
267  const auto fun_app =
268  expr_try_dynamic_cast<function_application_exprt>(eq.rhs()))
269  {
270  if(const auto result = generator.make_array_pointer_association(*fun_app))
271  eq.rhs() = *result;
272  }
273  }
274 }
275 
277  const union_find_replacet &symbol_resolve,
278  std::vector<equal_exprt> &equations)
279 {
280  for(equal_exprt &eq : equations)
281  symbol_resolve.replace_expr(eq);
282 }
283 
288 void string_refinementt::set_to(const exprt &expr, bool value)
289 {
290  PRECONDITION(expr.type().id()==ID_bool);
292 
293  if(expr.id() == ID_equal && value)
294  {
295  const equal_exprt &eq_expr = to_equal_expr(expr);
296  equations.push_back(eq_expr);
297  }
298  else
299  {
300  INVARIANT(
301  !has_char_array_subexpr(expr, ns), "char array only appear in equations");
302  supert::set_to(expr, value);
303  }
304 }
305 
313  const std::vector<equal_exprt> &equations,
314  const namespacet &ns,
315  messaget::mstreamt &stream)
316 {
317  const auto eom = messaget::eom;
318  const std::string log_message =
319  "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  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  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  return solver;
373 }
374 
380 static std::vector<exprt> extract_strings_from_lhs(const exprt &lhs)
381 {
382  std::vector<exprt> result;
383  if(lhs.type() == string_typet())
384  result.push_back(lhs);
385  else if(lhs.type().id() == ID_struct)
386  {
387  const struct_typet &struct_type = to_struct_type(lhs.type());
388  for(const auto &comp : struct_type.components())
389  {
390  const std::vector<exprt> strings_in_comp = extract_strings_from_lhs(
391  member_exprt(lhs, comp.get_name(), comp.type()));
392  result.insert(
393  result.end(), strings_in_comp.begin(), strings_in_comp.end());
394  }
395  }
396  return result;
397 }
398 
403 static std::vector<exprt> extract_strings(const exprt &expr)
404 {
405  std::vector<exprt> result;
406  for(auto it = expr.depth_begin(); it != expr.depth_end();)
407  {
408  if(it->type() == string_typet() && it->id() != ID_if)
409  {
410  result.push_back(*it);
411  it.next_sibling_or_parent();
412  }
413  else if(it->id() == ID_symbol)
414  {
415  for(const exprt &e : extract_strings_from_lhs(*it))
416  result.push_back(e);
417  it.next_sibling_or_parent();
418  }
419  else
420  ++it;
421  }
422  return result;
423 }
424 
432  const equal_exprt &eq,
433  union_find_replacet &symbol_resolve,
434  const namespacet &ns)
435 {
436  if(eq.rhs().type() == string_typet())
437  {
438  symbol_resolve.make_union(eq.lhs(), eq.rhs());
439  }
440  else if(has_subtype(eq.lhs().type(), ID_string, ns))
441  {
442  if(eq.rhs().type().id() == ID_struct)
443  {
444  const struct_typet &struct_type = to_struct_type(eq.rhs().type());
445  for(const auto &comp : struct_type.components())
446  {
447  const member_exprt lhs_data(eq.lhs(), comp.get_name(), comp.type());
448  const exprt rhs_data = simplify_expr(
449  member_exprt(eq.rhs(), comp.get_name(), comp.type()), ns);
451  equal_exprt(lhs_data, rhs_data), symbol_resolve, ns);
452  }
453  }
454  }
455 }
456 
465  std::vector<equal_exprt> &equations,
466  const namespacet &ns,
467  messaget::mstreamt &stream)
468 {
469  const auto eom = messaget::eom;
470  const std::string log_message =
471  "WARNING string_refinement.cpp "
472  "string_identifiers_resolution_from_equations:";
473 
474  equation_symbol_mappingt equation_map;
475 
476  // Indexes of equations that need to be added to the result
477  std::unordered_set<size_t> required_equations;
478  std::stack<size_t> equations_to_treat;
479 
480  for(std::size_t i = 0; i < equations.size(); ++i)
481  {
482  const equal_exprt &eq = equations[i];
483  if(eq.rhs().id() == ID_function_application)
484  {
485  if(required_equations.insert(i).second)
486  equations_to_treat.push(i);
487 
488  std::vector<exprt> rhs_strings = extract_strings(eq.rhs());
489  for(const auto &expr : rhs_strings)
490  equation_map.add(i, expr);
491  }
492  else if(
493  eq.lhs().type().id() != ID_pointer &&
494  has_subtype(eq.lhs().type(), ID_string, ns))
495  {
496  std::vector<exprt> lhs_strings = extract_strings_from_lhs(eq.lhs());
497 
498  for(const auto &expr : lhs_strings)
499  equation_map.add(i, expr);
500 
501  if(lhs_strings.empty())
502  {
503  stream << log_message << "non struct with string subtype "
504  << format(eq.lhs()) << "\n * of type "
505  << format(eq.lhs().type()) << eom;
506  }
507 
508  for(const exprt &expr : extract_strings(eq.rhs()))
509  equation_map.add(i, expr);
510  }
511  }
512 
513  // transitively add all equations which depend on the equations to treat
514  while(!equations_to_treat.empty())
515  {
516  const std::size_t i = equations_to_treat.top();
517  equations_to_treat.pop();
518  for(const exprt &string : equation_map.find_expressions(i))
519  {
520  for(const std::size_t j : equation_map.find_equations(string))
521  {
522  if(required_equations.insert(j).second)
523  equations_to_treat.push(j);
524  }
525  }
526  }
527 
528  union_find_replacet result;
529  for(const std::size_t i : required_equations)
530  add_string_equation_to_symbol_resolution(equations[i], result, ns);
531 
532  return result;
533 }
534 
537  std::ostream &output,
538  const std::vector<equal_exprt> &equations,
539  const namespacet &ns)
540 {
541  for(std::size_t i = 0; i < equations.size(); ++i)
542  output << " [" << i << "] " << format(equations[i].lhs())
543  << " == " << format(equations[i].rhs()) << std::endl;
544 }
545 
556 // NOLINTNEXTLINE
559 // NOLINTNEXTLINE
564 // NOLINTNEXTLINE
611 {
612 #ifdef DEBUG
613  debug() << "dec_solve: Initial set of equations" << eom;
615 #endif
616 
617  debug() << "dec_solve: Build symbol solver from equations" << eom;
618  // This is used by get, 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 char pointer symbols" << eom;
639 
640  debug() << "dec_solve: Replacing string ids in function applications" << eom;
641  for(equal_exprt &eq : equations)
642  {
644  string_id_symbol_resolve.replace_expr(eq.rhs());
645  }
646 
647  // Generator is also used by get, so we have to use it as a class member
648  // but we make sure it is cleared at each `dec_solve` call.
651 
652 #ifdef DEBUG
654 #endif
655 
656  debug() << "dec_solve: compute dependency graph and remove function "
657  << "applications captured by the dependencies:" << eom;
658  std::vector<exprt> local_equations;
659  for(const equal_exprt &eq : equations)
660  {
662  local_equations.push_back(eq);
663  }
664  equations.clear();
665 
666 #ifdef DEBUG
668 #endif
669 
670  debug() << "dec_solve: add constraints" << eom;
672 
673 #ifdef DEBUG
675 #endif
676 
677 #ifdef DEBUG
678  debug() << "dec_solve: arrays_of_pointers:" << eom;
679  for(auto pair : generator.array_pool.get_arrays_of_pointers())
680  {
681  debug() << " * " << format(pair.first) << "\t--> " << format(pair.second)
682  << " : " << format(pair.second.type()) << eom;
683  }
684 #endif
685 
686  for(const auto &eq : local_equations)
687  {
688 #ifdef DEBUG
689  debug() << "dec_solve: set_to " << format(eq) << eom;
690 #endif
691  supert::set_to(eq, true);
692  }
693 
694  const auto constraints = generator.get_constraints();
695  std::transform(
696  constraints.begin(),
697  constraints.end(),
698  std::back_inserter(axioms.universal),
699  [&](string_constraintt constraint) {
700  constraint.replace_expr(symbol_resolve);
702  is_valid_string_constraint(error(), ns, constraint),
704  "string constraints satisfy their invariant"));
705  return constraint;
706  });
707 
708  const auto not_contains_constraints =
710  std::transform(
711  not_contains_constraints.begin(),
712  not_contains_constraints.end(),
713  std::back_inserter(axioms.not_contains),
716  return axiom;
717  });
718 
719  for(const auto &nc_axiom : axioms.not_contains)
720  {
721  const auto &witness_type = [&] {
722  const auto &rtype = to_array_type(nc_axiom.s0().type());
723  const typet &index_type = rtype.size().type();
725  }();
726  generator.witness[nc_axiom] =
727  generator.fresh_symbol("not_contains_witness", witness_type);
728  }
729 
730  for(const exprt &lemma : generator.get_lemmas())
731  add_lemma(lemma);
732 
733  // Initial try without index set
734  const auto get = [this](const exprt &expr) { return this->get(expr); };
737  if(res==resultt::D_SATISFIABLE)
738  {
739  bool satisfied;
740  std::vector<exprt> counter_examples;
741  std::tie(satisfied, counter_examples) = check_axioms(
742  axioms,
743  generator,
744  get,
745  debug(),
746  ns,
749  supert::config_.ui,
751  if(satisfied)
752  {
753  debug() << "check_SAT: the model is correct" << eom;
754  return resultt::D_SATISFIABLE;
755  }
756  debug() << "check_SAT: got SAT but the model is not correct" << eom;
757  }
758  else
759  {
760  debug() << "check_SAT: got UNSAT or ERROR" << eom;
761  return res;
762  }
763 
766  current_constraints.clear();
767  for(const auto &instance :
769  debug(),
770  ns,
771  generator,
772  index_sets,
773  axioms))
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  supert::config_.ui,
795  if(satisfied)
796  {
797  debug() << "check_SAT: the model is correct" << eom;
798  return resultt::D_SATISFIABLE;
799  }
800 
801  debug() << "check_SAT: got SAT but the model is not correct, refining..."
802  << eom;
803 
804  // Since the model is not correct although we got SAT, we need to refine
805  // the property we are checking by adding more indices to the index set,
806  // and instantiating universal formulas with this indices.
807  // We will then relaunch the solver with these added lemmas.
808  index_sets.current.clear();
810 
812 
813  if(index_sets.current.empty())
814  {
815  if(axioms.not_contains.empty())
816  {
817  error() << "dec_solve: current index set is empty, "
818  << "this should not happen" << eom;
819  return resultt::D_ERROR;
820  }
821  else
822  {
823  debug() << "dec_solve: current index set is empty, "
824  << "adding counter examples" << eom;
825  for(const auto &counter : counter_examples)
826  add_lemma(counter);
827  }
828  }
829  current_constraints.clear();
830  for(const auto &instance :
832  debug(),
833  ns,
834  generator,
835  index_sets,
836  axioms))
837  add_lemma(instance);
838  }
839  else
840  {
841  debug() << "check_SAT: default return " << static_cast<int>(res) << eom;
842  return res;
843  }
844  }
845  debug() << "string_refinementt::dec_solve reached the maximum number"
846  << "of steps allowed" << eom;
847  return resultt::D_ERROR;
848 }
849 
855  const exprt &lemma,
856  const bool simplify_lemma)
857 {
858  if(!seen_instances.insert(lemma).second)
859  return;
860 
861  current_constraints.push_back(lemma);
862 
863  exprt simple_lemma=lemma;
864  if(simplify_lemma)
865  simplify(simple_lemma, ns);
866 
867  if(simple_lemma.is_true())
868  {
869 #if 0
870  debug() << "string_refinementt::add_lemma : tautology" << eom;
871 #endif
872  return;
873  }
874 
875  symbol_resolve.replace_expr(simple_lemma);
876 
877  // Replace empty arrays with array_of expression because the solver cannot
878  // handle empty arrays.
879  for(auto it = simple_lemma.depth_begin(); it != simple_lemma.depth_end();)
880  {
881  if(it->id() == ID_array && it->operands().empty())
882  {
883  it.mutate() = array_of_exprt(
884  from_integer(CHARACTER_FOR_UNKNOWN, it->type().subtype()),
885  to_array_type(it->type()));
886  it.next_sibling_or_parent();
887  }
888  else
889  ++it;
890  }
891 
892  debug() << "adding lemma " << format(simple_lemma) << eom;
893 
894  prop.l_set_to_true(convert(simple_lemma));
895 }
896 
907  const std::function<exprt(const exprt &)> &super_get,
908  const namespacet &ns,
909  const std::size_t max_string_length,
910  messaget::mstreamt &stream,
911  const array_string_exprt &arr)
912 {
913  const auto eom = messaget::eom;
914  const exprt &size = arr.length();
915  exprt arr_val = simplify_expr(super_get(arr), ns);
916  exprt size_val=super_get(size);
917  size_val=simplify_expr(size_val, ns);
918  const typet char_type = arr.type().subtype();
919  const typet &index_type=size.type();
920  const array_typet empty_ret_type(char_type, from_integer(0, index_type));
921  const array_of_exprt empty_ret(from_integer(0, char_type), empty_ret_type);
922 
923  if(size_val.id()!=ID_constant)
924  {
925  stream << "(sr::get_array) string of unknown size: " << format(size_val)
926  << eom;
927  return {};
928  }
929 
930  auto n_opt = numeric_cast<std::size_t>(size_val);
931  if(!n_opt)
932  {
933  stream << "(sr::get_array) size is not valid" << eom;
934  return {};
935  }
936  std::size_t n = *n_opt;
937 
939  {
940  stream << "(sr::get_array) long string (size " << format(arr.length())
941  << " = " << n << ") " << format(arr) << eom;
942  stream << "(sr::get_array) consider reducing string-max-input-length so "
943  "that no string exceeds "
945  << " in length and "
946  "make sure all functions returning strings are loaded"
947  << eom;
948  stream << "(sr::get_array) this can also happen on invalid object access"
949  << eom;
950  return nil_exprt();
951  }
952 
953  if(
954  const auto &array = interval_sparse_arrayt::of_expr(
956  return array->concretize(n, index_type);
957  return {};
958 }
959 
964 static std::string string_of_array(const array_exprt &arr)
965 {
966  if(arr.type().id()!=ID_array)
967  return std::string("");
968 
969  exprt size_expr=to_array_type(arr.type()).size();
970  auto n = numeric_cast_v<std::size_t>(size_expr);
971  return utf16_constant_array_to_java(arr, n);
972 }
973 
983  const std::function<exprt(const exprt &)> &super_get,
984  const namespacet &ns,
985  const std::size_t max_string_length,
986  messaget::mstreamt &stream,
987  const array_string_exprt &arr)
988 {
989  const auto &eom = messaget::eom;
990  static const std::string indent(" ");
991  stream << "- " << format(arr) << ":\n";
992  stream << indent << indent << "- type: " << format(arr.type()) << eom;
993  const auto arr_model_opt =
994  get_array(super_get, ns, max_string_length, stream, arr);
995  if(arr_model_opt)
996  {
997  stream << indent << indent << "- char_array: " << format(*arr_model_opt)
998  << '\n';
999  stream << indent << indent << "- type : " << format(arr_model_opt->type())
1000  << eom;
1001  const exprt simple = simplify_expr(*arr_model_opt, ns);
1002  stream << indent << indent << "- simplified_char_array: " << format(simple)
1003  << eom;
1004  if(
1005  const auto concretized_array = get_array(
1006  super_get, ns, max_string_length, stream, to_array_string_expr(simple)))
1007  {
1008  stream << indent << indent
1009  << "- concretized_char_array: " << format(*concretized_array)
1010  << eom;
1011 
1012  if(
1013  const auto array_expr =
1014  expr_try_dynamic_cast<array_exprt>(*concretized_array))
1015  {
1016  stream << indent << indent << "- as_string: \""
1017  << string_of_array(*array_expr) << "\"\n";
1018  }
1019  else
1020  stream << indent << "- warning: not an array" << eom;
1021  return *concretized_array;
1022  }
1023  return simple;
1024  }
1025  stream << indent << indent << "- incomplete model" << eom;
1026  return arr;
1027 }
1028 
1032  const string_constraint_generatort &generator,
1033  messaget::mstreamt &stream,
1034  const namespacet &ns,
1035  const std::size_t max_string_length,
1036  const std::function<exprt(const exprt &)> &super_get,
1037  const std::vector<symbol_exprt> &boolean_symbols,
1038  const std::vector<symbol_exprt> &index_symbols)
1039 {
1040  static const std::string indent(" ");
1041 
1042  stream << "debug_model:" << '\n';
1043  for(const auto &pointer_array : generator.array_pool.get_arrays_of_pointers())
1044  {
1045  const auto arr = pointer_array.second;
1046  const exprt model = get_char_array_and_concretize(
1047  super_get, ns, max_string_length, stream, arr);
1048 
1049  stream << "- " << format(arr) << ":\n"
1050  << indent << "- pointer: " << format(pointer_array.first) << "\n"
1051  << indent << "- model: " << format(model) << messaget::eom;
1052  }
1053 
1054  for(const auto &symbol : boolean_symbols)
1055  {
1056  stream << " - " << symbol.get_identifier() << ": "
1057  << format(super_get(symbol)) << '\n';
1058  }
1059 
1060  for(const auto &symbol : index_symbols)
1061  {
1062  stream << " - " << symbol.get_identifier() << ": "
1063  << format(super_get(symbol)) << '\n';
1064  }
1065  stream << messaget::eom;
1066 }
1067 
1081  const with_exprt &expr,
1082  const exprt &index,
1083  const bool left_propagate)
1084 {
1085  return left_propagate ? interval_sparse_arrayt(expr).to_if_expression(index)
1086  : sparse_arrayt(expr).to_if_expression(index);
1087 }
1088 
1096  const array_exprt &array_expr,
1097  const exprt &index,
1098  const std::function<symbol_exprt(const irep_idt &, const typet &)>
1099  &symbol_generator)
1100 {
1101  const typet &char_type = array_expr.type().subtype();
1102  const exprt default_val = symbol_generator("out_of_bound_access", char_type);
1103  const interval_sparse_arrayt sparse_array(array_expr, default_val);
1104  return sparse_array.to_if_expression(index);
1105 }
1106 
1108  const if_exprt &if_expr,
1109  const exprt &index,
1110  const std::function<symbol_exprt(const irep_idt &, const typet &)>
1111  &symbol_generator,
1112  const bool left_propagate)
1113 {
1114  // Substitute recursively in branches of conditional expressions
1115  const exprt true_case = substitute_array_access(
1116  index_exprt(if_expr.true_case(), index), symbol_generator, left_propagate);
1117  const exprt false_case = substitute_array_access(
1118  index_exprt(if_expr.false_case(), index), symbol_generator, left_propagate);
1119 
1120  return if_exprt(if_expr.cond(), true_case, false_case);
1121 }
1122 
1124  const index_exprt &index_expr,
1125  const std::function<symbol_exprt(const irep_idt &, const typet &)>
1126  &symbol_generator,
1127  const bool left_propagate)
1128 {
1129  const exprt &array = index_expr.array();
1130  if(auto array_of = expr_try_dynamic_cast<array_of_exprt>(array))
1131  return array_of->op();
1132  if(auto array_with = expr_try_dynamic_cast<with_exprt>(array))
1133  return substitute_array_access(
1134  *array_with, index_expr.index(), left_propagate);
1135  if(auto array_expr = expr_try_dynamic_cast<array_exprt>(array))
1136  return substitute_array_access(
1137  *array_expr, index_expr.index(), symbol_generator);
1138  if(auto if_expr = expr_try_dynamic_cast<if_exprt>(array))
1139  return substitute_array_access(
1140  *if_expr, index_expr.index(), symbol_generator, left_propagate);
1141 
1142  INVARIANT(
1143  array.is_nil() || array.id() == ID_symbol,
1144  std::string(
1145  "in case the array is unknown, it should be a symbol or nil, id: ")
1146  + id2string(array.id()));
1147  return index_expr;
1148 }
1149 
1154  exprt &expr,
1155  const std::function<symbol_exprt(const irep_idt &, const typet &)>
1156  &symbol_generator,
1157  const bool left_propagate)
1158 {
1159  if(const auto index_expr = expr_try_dynamic_cast<index_exprt>(expr))
1160  {
1161  expr =
1162  substitute_array_access(*index_expr, symbol_generator, left_propagate);
1163  }
1164 
1165  for(auto &op : expr.operands())
1166  substitute_array_access_in_place(op, symbol_generator, left_propagate);
1167 }
1168 
1190  exprt expr,
1191  const std::function<symbol_exprt(const irep_idt &, const typet &)>
1192  &symbol_generator,
1193  const bool left_propagate)
1194 {
1195  substitute_array_access_in_place(expr, symbol_generator, left_propagate);
1196  return expr;
1197 }
1198 
1210  const string_not_contains_constraintt &constraint,
1211  const symbol_exprt &univ_var,
1212  const std::function<exprt(const exprt &)> &get)
1213 {
1214  // If the for all is vacuously true, the negation is false.
1215  const auto lbe =
1216  numeric_cast_v<mp_integer>(get(constraint.exists_lower_bound()));
1217  const auto ube =
1218  numeric_cast_v<mp_integer>(get(constraint.exists_upper_bound()));
1219  const auto univ_bounds = and_exprt(
1220  binary_relation_exprt(get(constraint.univ_lower_bound()), ID_le, univ_var),
1221  binary_relation_exprt(get(constraint.univ_upper_bound()), ID_gt, univ_var));
1222 
1223  // The negated existential becomes an universal, and this is the unrolling of
1224  // that universal quantifier.
1225  std::vector<exprt> conjuncts;
1226  conjuncts.reserve(numeric_cast_v<std::size_t>(ube - lbe));
1227  for(mp_integer i=lbe; i<ube; ++i)
1228  {
1229  const constant_exprt i_expr = from_integer(i, univ_var.type());
1230  const exprt s0_char =
1231  get(index_exprt(constraint.s0(), plus_exprt(univ_var, i_expr)));
1232  const exprt s1_char = get(index_exprt(constraint.s1(), i_expr));
1233  conjuncts.push_back(equal_exprt(s0_char, s1_char));
1234  }
1235  const exprt equal_strings = conjunction(conjuncts);
1236  return and_exprt(univ_bounds, get(constraint.premise()), equal_strings);
1237 }
1238 
1243 template <typename T>
1245  messaget::mstreamt &stream,
1246  const namespacet &ns,
1247  const T &axiom,
1248  const T &axiom_in_model,
1249  const exprt &negaxiom,
1250  const exprt &with_concretized_arrays)
1251 {
1252  static const std::string indent = " ";
1253  static const std::string indent2 = " ";
1254  stream << indent2 << "- axiom:\n" << indent2 << indent;
1255  stream << to_string(axiom);
1256  stream << '\n' << indent2 << "- axiom_in_model:\n" << indent2 << indent;
1257  stream << to_string(axiom_in_model) << '\n'
1258  << indent2 << "- negated_axiom:\n"
1259  << indent2 << indent << format(negaxiom) << '\n';
1260  stream << indent2 << "- negated_axiom_with_concretized_arrays:\n"
1261  << indent2 << indent << format(with_concretized_arrays) << '\n';
1262 }
1263 
1266 static std::pair<bool, std::vector<exprt>> check_axioms(
1267  const string_axiomst &axioms,
1268  string_constraint_generatort &generator,
1269  const std::function<exprt(const exprt &)> &get,
1270  messaget::mstreamt &stream,
1271  const namespacet &ns,
1272  std::size_t max_string_length,
1273  bool use_counter_example,
1275  const union_find_replacet &symbol_resolve)
1276 {
1277  const auto eom=messaget::eom;
1278  static const std::string indent = " ";
1279  static const std::string indent2 = " ";
1280  // clang-format off
1281  const auto gen_symbol = [&](const irep_idt &id, const typet &type)
1282  {
1283  return generator.fresh_symbol(id, type);
1284  };
1285  // clang-format on
1286 
1287  stream << "string_refinementt::check_axioms:" << eom;
1288 
1289  stream << "symbol_resolve:" << eom;
1290  auto pairs = symbol_resolve.to_vector();
1291  for(const auto &pair : pairs)
1292  stream << " - " << format(pair.first) << " --> " << format(pair.second)
1293  << eom;
1294 
1295 #ifdef DEBUG
1296  debug_model(
1297  generator,
1298  stream,
1299  ns,
1300  max_string_length,
1301  get,
1302  generator.get_boolean_symbols(),
1303  generator.get_index_symbols());
1304 #endif
1305 
1306  // Maps from indexes of violated universal axiom to a witness of violation
1307  std::map<size_t, exprt> violated;
1308 
1309  stream << "string_refinement::check_axioms: " << axioms.universal.size()
1310  << " universal axioms:" << eom;
1311  for(size_t i=0; i<axioms.universal.size(); i++)
1312  {
1313  const string_constraintt &axiom=axioms.universal[i];
1314  const string_constraintt axiom_in_model(
1315  axiom.univ_var,
1316  get(axiom.lower_bound),
1317  get(axiom.upper_bound),
1318  get(axiom.body));
1319 
1320  exprt negaxiom = axiom_in_model.negation();
1321  negaxiom = simplify_expr(negaxiom, ns);
1322 
1323  stream << indent << i << ".\n";
1324  const exprt with_concretized_arrays =
1325  substitute_array_access(negaxiom, gen_symbol, true);
1327  stream, ns, axiom, axiom_in_model, negaxiom, with_concretized_arrays);
1328 
1329  if(
1330  const auto &witness =
1331  find_counter_example(ns, ui, with_concretized_arrays, axiom.univ_var))
1332  {
1333  stream << indent2 << "- violated_for: " << format(axiom.univ_var) << "="
1334  << format(*witness) << eom;
1335  violated[i]=*witness;
1336  }
1337  else
1338  stream << indent2 << "- correct" << eom;
1339  }
1340 
1341  // Maps from indexes of violated not_contains axiom to a witness of violation
1342  std::map<std::size_t, exprt> violated_not_contains;
1343 
1344  stream << "there are " << axioms.not_contains.size()
1345  << " not_contains axioms" << eom;
1346  for(std::size_t i = 0; i < axioms.not_contains.size(); i++)
1347  {
1348  const string_not_contains_constraintt &nc_axiom=axioms.not_contains[i];
1349  const symbol_exprt univ_var = generator.fresh_univ_index(
1350  "not_contains_univ_var", nc_axiom.s0().length().type());
1351  const exprt negated_axiom = negation_of_not_contains_constraint(
1352  nc_axiom, univ_var, [&](const exprt &expr) {
1353  return simplify_expr(get(expr), ns); });
1354 
1355  stream << indent << i << ".\n";
1357  stream, ns, nc_axiom, nc_axiom, negated_axiom, negated_axiom);
1358 
1359  if(
1360  const auto witness =
1361  find_counter_example(ns, ui, negated_axiom, univ_var))
1362  {
1363  stream << indent2 << "- violated_for: " << univ_var.get_identifier()
1364  << "=" << format(*witness) << eom;
1365  violated_not_contains[i]=*witness;
1366  }
1367  }
1368 
1369  if(violated.empty() && violated_not_contains.empty())
1370  {
1371  stream << "no violated property" << eom;
1372  return { true, std::vector<exprt>() };
1373  }
1374  else
1375  {
1376  stream << violated.size()
1377  << " universal string axioms can be violated" << eom;
1378  stream << violated_not_contains.size()
1379  << " not_contains string axioms can be violated" << eom;
1380 
1381  if(use_counter_example)
1382  {
1383  std::vector<exprt> lemmas;
1384 
1385  for(const auto &v : violated)
1386  {
1387  const exprt &val=v.second;
1388  const string_constraintt &axiom=axioms.universal[v.first];
1389 
1390  exprt instance(axiom.body);
1391  replace_expr(axiom.univ_var, val, instance);
1392  // We are not sure the index set contains only positive numbers
1393  and_exprt bounds(
1394  axiom.univ_within_bounds(),
1395  binary_relation_exprt(from_integer(0, val.type()), ID_le, val));
1396  replace_expr(axiom.univ_var, val, bounds);
1397  const implies_exprt counter(bounds, instance);
1398  lemmas.push_back(counter);
1399  }
1400 
1401  for(const auto &v : violated_not_contains)
1402  {
1403  const exprt &val=v.second;
1404  const string_not_contains_constraintt &axiom=
1405  axioms.not_contains[v.first];
1406 
1407  const exprt func_val=generator.get_witness_of(axiom, val);
1408  const exprt comp_val=simplify_sum(plus_exprt(val, func_val));
1409 
1410  std::set<std::pair<exprt, exprt>> indices;
1411  indices.insert(std::pair<exprt, exprt>(comp_val, func_val));
1412  const exprt counter=::instantiate_not_contains(
1413  axiom, indices, generator)[0];
1414  lemmas.push_back(counter);
1415  }
1416  return { false, lemmas };
1417  }
1418  }
1419  return { false, std::vector<exprt>() };
1420 }
1421 
1426 static std::map<exprt, int> map_representation_of_sum(const exprt &f)
1427 {
1428  // number of time the leaf should be added (can be negative)
1429  std::map<exprt, int> elems;
1430 
1431  std::list<std::pair<exprt, bool> > to_process;
1432  to_process.emplace_back(f, true);
1433 
1434  while(!to_process.empty())
1435  {
1436  exprt cur=to_process.back().first;
1437  bool positive=to_process.back().second;
1438  to_process.pop_back();
1439  if(cur.id()==ID_plus)
1440  {
1441  for(const auto &op : cur.operands())
1442  to_process.emplace_back(op, positive);
1443  }
1444  else if(cur.id()==ID_minus)
1445  {
1446  to_process.emplace_back(cur.op1(), !positive);
1447  to_process.emplace_back(cur.op0(), positive);
1448  }
1449  else if(cur.id()==ID_unary_minus)
1450  {
1451  to_process.emplace_back(cur.op0(), !positive);
1452  }
1453  else
1454  {
1455  if(positive)
1456  elems[cur]=elems[cur]+1;
1457  else
1458  elems[cur]=elems[cur]-1;
1459  }
1460  }
1461  return elems;
1462 }
1463 
1471  std::map<exprt, int> &m,
1472  const typet &type,
1473  bool negated=false)
1474 {
1475  exprt sum=nil_exprt();
1476  mp_integer constants=0;
1477  typet index_type;
1478  if(m.empty())
1479  return from_integer(0, type);
1480  else
1481  index_type=m.begin()->first.type();
1482 
1483  for(const auto &term : m)
1484  {
1485  // We should group constants together...
1486  const exprt &t=term.first;
1487  int second=negated?(-term.second):term.second;
1488  if(t.id()==ID_constant)
1489  {
1490  std::string value(to_constant_expr(t).get_value().c_str());
1491  constants+=binary2integer(value, true)*second;
1492  }
1493  else
1494  {
1495  switch(second)
1496  {
1497  case -1:
1498  if(sum.is_nil())
1499  sum=unary_minus_exprt(t);
1500  else
1501  sum=minus_exprt(sum, t);
1502  break;
1503 
1504  case 1:
1505  if(sum.is_nil())
1506  sum=t;
1507  else
1508  sum=plus_exprt(sum, t);
1509  break;
1510 
1511  default:
1512  if(second>1)
1513  {
1514  if(sum.is_nil())
1515  sum=t;
1516  else
1517  plus_exprt(sum, t);
1518  for(int i=1; i<second; i++)
1519  sum=plus_exprt(sum, t);
1520  }
1521  else if(second<-1)
1522  {
1523  if(sum.is_nil())
1524  sum=unary_minus_exprt(t);
1525  else
1526  sum=minus_exprt(sum, t);
1527  for(int i=-1; i>second; i--)
1528  sum=minus_exprt(sum, t);
1529  }
1530  }
1531  }
1532  }
1533 
1534  exprt index_const=from_integer(constants, index_type);
1535  if(sum.is_not_nil())
1536  return plus_exprt(sum, index_const);
1537  else
1538  return index_const;
1539 }
1540 
1544 {
1545  std::map<exprt, int> map=map_representation_of_sum(f);
1546  return sum_over_map(map, f.type());
1547 }
1548 
1560  messaget::mstreamt &stream,
1561  const exprt &qvar,
1562  const exprt &val,
1563  const exprt &f)
1564 {
1565  exprt positive, negative;
1566  // number of time the element should be added (can be negative)
1567  // qvar has to be equal to val - f(0) if it appears positively in f
1568  // (i.e. if f(qvar)=f(0) + qvar) and f(0) - val if it appears negatively
1569  // in f. So we start by computing val - f(0).
1570  std::map<exprt, int> elems=map_representation_of_sum(minus_exprt(val, f));
1571 
1572  // true if qvar appears negatively in f (positively in elems):
1573  bool neg=false;
1574 
1575  auto it=elems.find(qvar);
1576  INVARIANT(
1577  it!=elems.end(),
1578  string_refinement_invariantt("a function must have an occurrence of qvar"));
1579  if(it->second==1 || it->second==-1)
1580  {
1581  neg=(it->second==1);
1582  }
1583  else
1584  {
1585  INVARIANT(
1586  it->second == 0,
1588  "a proper function must have exactly one "
1589  "occurrences after reduction, or it cancelled out, and it does not"
1590  " have one"));
1591  stream << "in string_refinementt::compute_inverse_function:"
1592  << " warning: occurrences of qvar cancelled out " << messaget::eom;
1593  }
1594 
1595  elems.erase(it);
1596  return sum_over_map(elems, f.type(), neg);
1597 }
1598 
1600 {
1601 private:
1602  const exprt &qvar_;
1603 
1604 public:
1605  bool found;
1606 
1607  explicit find_qvar_visitort(const exprt &qvar): qvar_(qvar), found(false) {}
1608 
1609  void operator()(const exprt &expr) override
1610  {
1611  if(expr==qvar_)
1612  found=true;
1613  }
1614 };
1615 
1620 static bool find_qvar(const exprt &index, const symbol_exprt &qvar)
1621 {
1622  find_qvar_visitort v2(qvar);
1623  index.visit(v2);
1624  return v2.found;
1625 }
1626 
1632 static void initial_index_set(
1633  index_set_pairt &index_set,
1634  const namespacet &ns,
1635  const string_axiomst &axioms)
1636 {
1637  for(const auto &axiom : axioms.universal)
1638  initial_index_set(index_set, ns, axiom);
1639  for(const auto &axiom : axioms.not_contains)
1640  initial_index_set(index_set, ns, axiom);
1641 }
1642 
1647 static void update_index_set(
1648  index_set_pairt &index_set,
1649  const namespacet &ns,
1650  const std::vector<exprt> &current_constraints)
1651 {
1652  for(const auto &axiom : current_constraints)
1653  update_index_set(index_set, ns, axiom);
1654 }
1655 
1662 static void get_sub_arrays(const exprt &array_expr, std::vector<exprt> &accu)
1663 {
1664  if(array_expr.id()==ID_if)
1665  {
1666  get_sub_arrays(to_if_expr(array_expr).true_case(), accu);
1667  get_sub_arrays(to_if_expr(array_expr).false_case(), accu);
1668  }
1669  else
1670  {
1671  if(array_expr.type().id() == ID_array)
1672  {
1673  // TODO: check_that it does not contain any sub_array
1674  accu.push_back(array_expr);
1675  }
1676  else
1677  {
1678  for(const auto &operand : array_expr.operands())
1679  get_sub_arrays(operand, accu);
1680  }
1681  }
1682 }
1683 
1689 static void add_to_index_set(
1690  index_set_pairt &index_set,
1691  const namespacet &ns,
1692  const exprt &s,
1693  exprt i)
1694 {
1695  simplify(i, ns);
1696  const bool is_size_t = numeric_cast<std::size_t>(i).has_value();
1697  if(i.id()!=ID_constant || is_size_t)
1698  {
1699  std::vector<exprt> sub_arrays;
1700  get_sub_arrays(s, sub_arrays);
1701  for(const auto &sub : sub_arrays)
1702  if(index_set.cumulative[sub].insert(i).second)
1703  index_set.current[sub].insert(i);
1704  }
1705 }
1706 
1722 static void initial_index_set(
1723  index_set_pairt &index_set,
1724  const namespacet &ns,
1725  const exprt &qvar,
1726  const exprt &upper_bound,
1727  const exprt &s,
1728  const exprt &i)
1729 {
1730  PRECONDITION(s.id() == ID_symbol || s.id() == ID_array || s.id() == ID_if);
1731  if(s.id() == ID_array)
1732  {
1733  for(std::size_t j = 0; j < s.operands().size(); ++j)
1734  add_to_index_set(index_set, ns, s, from_integer(j, i.type()));
1735  return;
1736  }
1737  if(auto ite = expr_try_dynamic_cast<if_exprt>(s))
1738  {
1739  initial_index_set(index_set, ns, qvar, upper_bound, ite->true_case(), i);
1740  initial_index_set(index_set, ns, qvar, upper_bound, ite->false_case(), i);
1741  return;
1742  }
1743  const minus_exprt u_minus_1(upper_bound, from_integer(1, upper_bound.type()));
1744  exprt i_copy = i;
1745  replace_expr(qvar, u_minus_1, i_copy);
1746  add_to_index_set(index_set, ns, s, i_copy);
1747 }
1748 
1749 static void initial_index_set(
1750  index_set_pairt &index_set,
1751  const namespacet &ns,
1752  const string_constraintt &axiom)
1753 {
1754  const symbol_exprt &qvar = axiom.univ_var;
1755  const auto &bound = axiom.upper_bound;
1756  auto it = axiom.body.depth_begin();
1757  const auto end = axiom.body.depth_end();
1758  while(it != end)
1759  {
1760  if(it->id() == ID_index && is_char_type(it->type()))
1761  {
1762  const auto &index_expr = to_index_expr(*it);
1763  const auto &s = index_expr.array();
1764  initial_index_set(index_set, ns, qvar, bound, s, index_expr.index());
1765  it.next_sibling_or_parent();
1766  }
1767  else
1768  ++it;
1769  }
1770 }
1771 
1772 static void initial_index_set(
1773  index_set_pairt &index_set,
1774  const namespacet &ns,
1775  const string_not_contains_constraintt &axiom)
1776 {
1777  auto it=axiom.premise().depth_begin();
1778  const auto end=axiom.premise().depth_end();
1779  while(it!=end)
1780  {
1781  if(it->id() == ID_index && is_char_type(it->type()))
1782  {
1783  const exprt &s=it->op0();
1784  const exprt &i=it->op1();
1785 
1786  // cur is of the form s[i] and no quantified variable appears in i
1787  add_to_index_set(index_set, ns, s, i);
1788 
1789  it.next_sibling_or_parent();
1790  }
1791  else
1792  ++it;
1793  }
1794 
1795  const minus_exprt kminus1(
1796  axiom.exists_upper_bound(),
1797  from_integer(1, axiom.exists_upper_bound().type()));
1798  add_to_index_set(index_set, ns, axiom.s1().content(), kminus1);
1799 }
1800 
1805 static void update_index_set(
1806  index_set_pairt &index_set,
1807  const namespacet &ns,
1808  const exprt &formula)
1809 {
1810  std::list<exprt> to_process;
1811  to_process.push_back(formula);
1812 
1813  while(!to_process.empty())
1814  {
1815  exprt cur=to_process.back();
1816  to_process.pop_back();
1817  if(cur.id() == ID_index && is_char_type(cur.type()))
1818  {
1819  const exprt &s=cur.op0();
1820  const exprt &i=cur.op1();
1822  s.type().id()==ID_array,
1823  string_refinement_invariantt("index expressions must index on arrays"));
1824  exprt simplified=simplify_sum(i);
1825  if(s.id() != ID_array) // do not update index set of constant arrays
1826  add_to_index_set(index_set, ns, s, simplified);
1827  }
1828  else
1829  {
1830  forall_operands(it, cur)
1831  to_process.push_back(*it);
1832  }
1833  }
1834 }
1835 
1843 static std::unordered_set<exprt, irep_hash>
1844 find_indexes(const exprt &expr, const exprt &str, const symbol_exprt &qvar)
1845 {
1846  decltype(find_indexes(expr, str, qvar)) result;
1847  auto index_str_containing_qvar = [&](const exprt &e) {
1848  if(auto index_expr = expr_try_dynamic_cast<index_exprt>(e))
1849  {
1850  const auto &arr = index_expr->array();
1851  const auto str_it = std::find(arr.depth_begin(), arr.depth_end(), str);
1852  return str_it != arr.depth_end() && find_qvar(index_expr->index(), qvar);
1853  }
1854  return false;
1855  };
1856 
1857  std::for_each(expr.depth_begin(), expr.depth_end(), [&](const exprt &e) {
1858  if(index_str_containing_qvar(e))
1859  result.insert(to_index_expr(e).index());
1860  });
1861  return result;
1862 }
1863 
1877  messaget::mstreamt &stream,
1878  const string_constraintt &axiom,
1879  const exprt &str,
1880  const exprt &val)
1881 {
1882  const auto indexes = find_indexes(axiom.body, str, axiom.univ_var);
1883  INVARIANT(
1884  str.id() == ID_array || indexes.size() <= 1,
1885  "non constant array should always be accessed at the same index");
1886  exprt::operandst conjuncts;
1887  for(const auto &index : indexes)
1888  {
1889  const exprt univ_var_value =
1890  compute_inverse_function(stream, axiom.univ_var, val, index);
1891  implies_exprt instance(
1892  and_exprt(
1893  binary_relation_exprt(axiom.univ_var, ID_ge, axiom.lower_bound),
1894  binary_relation_exprt(axiom.univ_var, ID_lt, axiom.upper_bound)),
1895  axiom.body);
1896  replace_expr(axiom.univ_var, univ_var_value, instance);
1897  conjuncts.push_back(instance);
1898  }
1899  return conjunction(conjuncts);
1900 }
1901 
1920 static std::vector<exprt> instantiate(
1921  const string_not_contains_constraintt &axiom,
1922  const index_set_pairt &index_set,
1923  const string_constraint_generatort &generator)
1924 {
1925  const array_string_exprt &s0 = axiom.s0();
1926  const array_string_exprt &s1 = axiom.s1();
1927 
1928  const auto &index_set0=index_set.cumulative.find(s0.content());
1929  const auto &index_set1=index_set.cumulative.find(s1.content());
1930  const auto &current_index_set0=index_set.current.find(s0.content());
1931  const auto &current_index_set1=index_set.current.find(s1.content());
1932 
1933  if(index_set0!=index_set.cumulative.end() &&
1934  index_set1!=index_set.cumulative.end() &&
1935  current_index_set0!=index_set.current.end() &&
1936  current_index_set1!=index_set.current.end())
1937  {
1938  typedef std::pair<exprt, exprt> expr_pairt;
1939  std::set<expr_pairt> index_pairs;
1940 
1941  for(const auto &ic0 : current_index_set0->second)
1942  for(const auto &i1 : index_set1->second)
1943  index_pairs.insert(expr_pairt(ic0, i1));
1944  for(const auto &ic1 : current_index_set1->second)
1945  for(const auto &i0 : index_set0->second)
1946  index_pairs.insert(expr_pairt(i0, ic1));
1947 
1948  return ::instantiate_not_contains(axiom, index_pairs, generator);
1949  }
1950  return { };
1951 }
1952 
1960 exprt substitute_array_lists(exprt expr, size_t string_max_length)
1961 {
1962  for(auto &operand : expr.operands())
1963  operand = substitute_array_lists(operand, string_max_length);
1964 
1965  if(expr.id() == ID_array_list)
1966  {
1968  expr.operands().size()>=2,
1969  string_refinement_invariantt("array-lists must have at least two "
1970  "operands"));
1971  const typet &char_type = expr.operands()[1].type();
1973  exprt ret_expr=array_of_exprt(from_integer(0, char_type), arr_type);
1974 
1975  for(size_t i=0; i<expr.operands().size(); i+=2)
1976  {
1977  const exprt &index=expr.operands()[i];
1978  const exprt &value=expr.operands()[i+1];
1979  const auto index_value = numeric_cast<std::size_t>(index);
1980  if(!index.is_constant() ||
1981  (index_value && *index_value<string_max_length))
1982  ret_expr=with_exprt(ret_expr, index, value);
1983  }
1984  return ret_expr;
1985  }
1986 
1987  return expr;
1988 }
1989 
1998 {
1999  const auto super_get = [this](const exprt &expr) {
2000  return supert::get(expr);
2001  };
2002  exprt ecopy(expr);
2003  (void)symbol_resolve.replace_expr(ecopy);
2004 
2005  // Special treatment for index expressions
2006  const auto &index_expr = expr_try_dynamic_cast<index_exprt>(ecopy);
2007  if(index_expr && is_char_type(index_expr->type()))
2008  {
2009  std::reference_wrapper<const exprt> current(index_expr->array());
2010  while(current.get().id() == ID_if)
2011  {
2012  const auto &if_expr = expr_dynamic_cast<if_exprt>(current.get());
2013  const exprt cond = get(if_expr.cond());
2014  if(cond.is_true())
2015  current = std::cref(if_expr.true_case());
2016  else if(cond.is_false())
2017  current = std::cref(if_expr.false_case());
2018  else
2019  UNREACHABLE;
2020  }
2021  const auto array = supert::get(current.get());
2022  const auto index = get(index_expr->index());
2023  const exprt unknown =
2024  from_integer(CHARACTER_FOR_UNKNOWN, index_expr->type());
2025  if(
2026  const auto sparse_array = interval_sparse_arrayt::of_expr(array, unknown))
2027  {
2028  if(const auto index_value = numeric_cast<std::size_t>(index))
2029  return sparse_array->at(*index_value);
2030  return sparse_array->to_if_expression(index);
2031  }
2032 
2033  INVARIANT(
2034  array.is_nil() || array.id() == ID_symbol,
2035  std::string(
2036  "apart from symbols, array valuations can be interpreted as "
2037  "sparse arrays, id: ") +
2038  id2string(array.id()));
2039  return index_exprt(array, index);
2040  }
2041 
2042  if(is_char_array_type(ecopy.type(), ns))
2043  {
2045  arr.length() = generator.array_pool.get_length(arr);
2046 
2047  if(
2048  const auto from_dependencies =
2049  dependencies.eval(arr, [&](const exprt &expr) { return get(expr); }))
2050  return *from_dependencies;
2051 
2052  if(
2053  const auto arr_model_opt =
2054  get_array(super_get, ns, max_string_length, debug(), arr))
2055  return *arr_model_opt;
2056 
2057  if(generator.get_created_strings().count(arr))
2058  {
2059  const exprt length = super_get(arr.length());
2060  if(const auto n = numeric_cast<std::size_t>(length))
2061  {
2062  const interval_sparse_arrayt sparse_array(
2064  return sparse_array.concretize(*n, length.type());
2065  }
2066  }
2067  return arr;
2068  }
2069  return supert::get(ecopy);
2070 }
2071 
2082  const namespacet &ns,
2083  const ui_message_handlert::uit ui,
2084  const exprt &axiom,
2085  const symbol_exprt &var)
2086 {
2087  satcheck_no_simplifiert sat_check;
2088  boolbvt solver(ns, sat_check);
2089  solver << axiom;
2090 
2092  return solver.get(var);
2093  else
2094  return { };
2095 }
2096 
2098 typedef std::map<exprt, std::vector<exprt>> array_index_mapt;
2099 
2102 {
2103  array_index_mapt indices;
2104  // clang-format off
2105  std::for_each(
2106  expr.depth_begin(),
2107  expr.depth_end(),
2108  [&](const exprt &expr)
2109  {
2110  const auto index_expr = expr_try_dynamic_cast<const index_exprt>(expr);
2111  if(index_expr)
2112  indices[index_expr->array()].push_back(index_expr->index());
2113  });
2114  // clang-format on
2115  return indices;
2116 }
2117 
2123 static bool
2125 {
2126  for(auto it = expr.depth_begin(); it != expr.depth_end();)
2127  {
2128  if(
2129  it->id() != ID_plus && it->id() != ID_minus &&
2130  it->id() != ID_unary_minus && *it != var)
2131  {
2132  if(find_qvar(*it, var))
2133  return false;
2134  else
2135  it.next_sibling_or_parent();
2136  }
2137  else
2138  ++it;
2139  }
2140  return true;
2141 }
2142 
2151 {
2152  for(auto it = constr.body.depth_begin(); it != constr.body.depth_end();)
2153  {
2154  if(*it == constr.univ_var)
2155  return false;
2156  if(it->id() == ID_index)
2157  it.next_sibling_or_parent();
2158  else
2159  ++it;
2160  }
2161  return true;
2162 }
2163 
2171  messaget::mstreamt &stream,
2172  const namespacet &ns,
2173  const string_constraintt &constraint)
2174 {
2175  const auto eom=messaget::eom;
2176  const array_index_mapt body_indices = gather_indices(constraint.body);
2177  // Must validate for each string. Note that we have an invariant that the
2178  // second value in the pair is non-empty.
2179  for(const auto &pair : body_indices)
2180  {
2181  // Condition 1: All indices of the same string must be the of the same form
2182  const exprt rep=pair.second.back();
2183  for(size_t j=0; j<pair.second.size()-1; j++)
2184  {
2185  const exprt i=pair.second[j];
2186  const equal_exprt equals(rep, i);
2187  const exprt result=simplify_expr(equals, ns);
2188  if(result.is_false())
2189  {
2190  stream << "Indices not equal: " << to_string(constraint)
2191  << ", str: " << format(pair.first) << eom;
2192  return false;
2193  }
2194  }
2195 
2196  // Condition 2: f must be linear in the quantified variable
2197  if(!is_linear_arithmetic_expr(rep, constraint.univ_var))
2198  {
2199  stream << "f is not linear: " << to_string(constraint)
2200  << ", str: " << format(pair.first) << eom;
2201  return false;
2202  }
2203 
2204  // Condition 3: the quantified variable can only occur in indices in the
2205  // body
2206  if(!universal_only_in_index(constraint))
2207  {
2208  stream << "Universal variable outside of index:" << to_string(constraint)
2209  << eom;
2210  return false;
2211  }
2212  }
2213 
2214  return true;
2215 }
const if_exprt & to_if_expr(const exprt &expr)
Cast a generic exprt to an if_exprt.
Definition: std_expr.h:3426
The type of an expression.
Definition: type.h:22
const namespacet * ns
Definition: bv_refinement.h:37
static void display_index_set(messaget::mstreamt &stream, const index_set_pairt &index_set)
Write index set to the given stream, use for debugging.
array_exprt concretize(std::size_t size, const typet &index_type) const
Convert to an array representation, ignores elements at index >= size.
static exprt sum_over_map(std::map< exprt, int > &m, const typet &type, bool negated=false)
exprt & true_case()
Definition: std_expr.h:3395
static optionalt< exprt > find_counter_example(const namespacet &ns, ui_message_handlert::uit ui, const exprt &axiom, const symbol_exprt &var)
Creates a solver with axiom as the only formula added and runs it.
static std::unordered_set< exprt, irep_hash > find_indexes(const exprt &expr, const exprt &str, const symbol_exprt &qvar)
Find indexes of str used in expr that contains qvar, for instance with arguments (str[k+1]==&#39;a&#39;), str, and k, the function should return k+1.
BigInt mp_integer
Definition: mp_arith.h:22
static exprt instantiate(messaget::mstreamt &stream, const string_constraintt &axiom, const exprt &str, const exprt &val)
Substitute qvar the universally quantified variable of axiom, by an index val, in axiom...
void add_constraints(string_constraint_generatort &generatort)
For all builtin call on which a test (or an unsupported buitin) result depends, add the corresponding...
const std::set< array_string_exprt > & get_created_strings() const
Set of strings that have been created by the generator.
bool is_nil() const
Definition: irep.h:102
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
const std::string & id2string(const irep_idt &d)
Definition: irep.h:43
bool is_not_nil() const
Definition: irep.h:103
virtual exprt to_if_expression(const exprt &index) const
Creates an if_expr corresponding to the result of accessing the array at the given index...
std::vector< equal_exprt > equations
std::map< exprt, std::vector< exprt > > array_index_mapt
literalt convert(const exprt &expr) override
Definition: prop_conv.cpp:162
const exprt & univ_lower_bound() const
const std::vector< string_constraintt > & get_constraints() const
bool equality_propagation
Definition: prop_conv.h:112
exprt get_witness_of(const string_not_contains_constraintt &c, const exprt &univ_val) const
exprt & op0()
Definition: expr.h:72
exprt simplify_expr(const exprt &src, const namespacet &ns)
void clean_cache()
Clean the cache used by eval
bool has_subtype(const typet &type, const std::function< bool(const typet &)> &pred, const namespacet &ns)
returns true if any of the contained types satisfies pred
Definition: expr_util.cpp:139
union_find_replacet string_identifiers_resolution_from_equations(std::vector< equal_exprt > &equations, const namespacet &ns, messaget::mstreamt &stream)
Symbol resolution for expressions of type string typet.
Deprecated expression utility functions.
bool add_node(string_dependenciest &dependencies, const equal_exprt &equation, array_poolt &array_pool)
When right hand side of equation is a builtin_function add a "string_builtin_function" node to the gr...
const std::vector< exprt > & get_lemmas() const
Axioms are of three kinds: universally quantified string constraint, not contains string constraints ...
const irep_idt & get_identifier() const
Definition: std_expr.h:128
bool is_false() const
Definition: expr.cpp:131
bool replace_expr(exprt &expr) const
Replace subexpressions of expr by a canonical element of the set they belong to.
string_refinementt constructor arguments
bool is_char_pointer_type(const typet &type)
For now, any unsigned bitvector type is considered a character.
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:120
std::map< exprt, std::set< exprt > > current
const componentst & components() const
Definition: std_types.h:245
symbol_exprt fresh_univ_index(const irep_idt &prefix, const typet &type)
generate an index symbol to be used as an universaly quantified variable
static void update_index_set(index_set_pairt &index_set, const namespacet &ns, const std::vector< exprt > &current_constraints)
Add to the index set all the indices that appear in the formulas.
exprt get_length(const array_string_exprt &s) const
Associate an actual finite length to infinite arrays.
The trinary if-then-else operator.
Definition: std_expr.h:3361
exprt & cond()
Definition: std_expr.h:3385
bool is_true() const
Definition: expr.cpp:124
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)
typet & type()
Definition: expr.h:56
exprt to_if_expression(const exprt &index) const override
Creates an if_expr corresponding to the result of accessing the array at the given index...
const std::vector< string_not_contains_constraintt > & get_not_contains_constraints() const
depth_iteratort depth_begin()
Definition: expr.cpp:299
exprt univ_within_bounds() const
static union_find_replacet generate_symbol_resolution_from_equations(const std::vector< equal_exprt > &equations, const namespacet &ns, messaget::mstreamt &stream)
Add association for each char pointer in the equation.
Magic numbers used throughout the codebase.
A constant literal expression.
Definition: std_expr.h:4424
static bool validate(const string_refinementt::infot &info)
auto expr_dynamic_cast(TExpr &base) -> typename detail::expr_dynamic_cast_return_typet< T, TExpr >::type
Cast a reference to a generic exprt to a specific derived class.
Definition: expr_cast.h:165
static mstreamt & eom(mstreamt &m)
Definition: message.h:272
Structure type.
Definition: std_types.h:297
boolean implication
Definition: std_expr.h:2339
void clear_constraints()
Clear all constraints and lemmas.
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
void l_set_to_true(literalt a)
Definition: prop.h:49
exprt substitute_array_lists(exprt expr, size_t string_max_length)
Replace array-lists by &#39;with&#39; expressions.
Definition: boolbv.h:31
const std::vector< symbol_exprt > & get_boolean_symbols() const
Boolean symbols for the results of some string functions.
Extract member of struct or union.
Definition: std_expr.h:3871
void operator()(const exprt &expr) override
TO_BE_DOCUMENTED.
Definition: std_types.h:1569
string_dependenciest dependencies
equality
Definition: std_expr.h:1354
string_refinementt(const infot &)
#define CHARACTER_FOR_UNKNOWN
static void add_to_index_set(index_set_pairt &index_set, const namespacet &ns, const exprt &s, exprt i)
Add i to the index set all the indices that appear in the formula.
bool can_cast_expr< function_application_exprt >(const exprt &base)
Definition: std_expr.h:4608
exprt conjunction(const exprt::operandst &op)
Definition: std_expr.cpp:48
static void substitute_array_access_in_place(exprt &expr, const std::function< symbol_exprt(const irep_idt &, const typet &)> &symbol_generator, const bool left_propagate)
Auxiliary function for substitute_array_access Performs the same operation but modifies the argument ...
static std::vector< T > fill_in_map_as_vector(const std::map< std::size_t, T > &index_value)
Convert index-value map to a vector of values.
const exprt & exists_lower_bound() const
const irep_idt & id() const
Definition: irep.h:189
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
exprt make_union(const exprt &a, const exprt &b)
Keeps a map of symbols to expressions, such as none of the mapped values exist as a key...
static void get_sub_arrays(const exprt &array_expr, std::vector< exprt > &accu)
An expression representing an array of characters can be in the form of an if expression for instance...
void visit(class expr_visitort &visitor)
Definition: expr.cpp:263
void debug_model(const string_constraint_generatort &generator, messaget::mstreamt &stream, const namespacet &ns, const std::size_t max_string_length, const std::function< exprt(const exprt &)> &super_get, const std::vector< symbol_exprt > &boolean_symbols, const std::vector< symbol_exprt > &index_symbols)
Display part of the current model by mapping the variables created by the solver to constant expressi...
An expression denoting infinity.
Definition: std_expr.h:4694
Defines related function for string constraints.
std::vector< exprt > instantiate_not_contains(const string_not_contains_constraintt &axiom, const std::set< std::pair< exprt, exprt >> &index_pairs, const string_constraint_generatort &generator)
Instantiates a quantified formula representing not_contains by substituting the quantifiers and gener...
optionalt< exprt > eval(const array_string_exprt &s, const std::function< exprt(const exprt &)> &get_value) const
Attempt to evaluate the given string from the dependencies and valuation of strings on which it depen...
Constraints to encode non containement of strings.
static exprt get_char_array_and_concretize(const std::function< exprt(const exprt &)> &super_get, const namespacet &ns, const std::size_t max_string_length, messaget::mstreamt &stream, const array_string_exprt &arr)
Debugging function which finds the valuation of the given array in super_get and concretize unknown c...
The NIL expression.
Definition: std_expr.h:4510
int solver(std::istream &in)
std::map< exprt, std::set< exprt > > cumulative
static bool universal_only_in_index(const string_constraintt &constr)
The universally quantified variable is only allowed to occur in index expressions in the body of a st...
Represents arrays by the indexes up to which the value remains the same.
exprt simplify_sum(const exprt &f)
static bool is_valid_string_constraint(messaget::mstreamt &stream, const namespacet &ns, const string_constraintt &constraint)
Checks the data invariant for string_constraintt.
nonstd::optional< T > optionalt
Definition: optional.h:35
boolean AND
Definition: std_expr.h:2255
void add(const std::size_t i, const exprt &expr)
Record the fact that equation i contains expression expr
optionalt< Target > numeric_cast(const exprt &arg)
Converts an expression to any integral type.
Definition: arith_tools.h:122
exprt & op1()
Definition: expr.h:75
union_find_replacet symbol_resolve
mstreamt & error() const
Definition: message.h:302
Represents arrays of the form array_of(x) with {i:=a} with {j:=b} ... by a default value x and a list...
const std::size_t MAX_CONCRETE_STRING_SIZE
Definition: magic.h:14
TO_BE_DOCUMENTED.
Definition: namespace.h:74
static bool is_valid_string_constraint(messaget::mstreamt &stream, const namespacet &ns, const string_constraintt &constraint)
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
#define forall_operands(it, expr)
Definition: expr.h:17
The plus expression.
Definition: std_expr.h:893
const namespacet & ns
std::vector< exprt > instantiate_not_contains(const string_not_contains_constraintt &axiom, const std::set< std::pair< exprt, exprt >> &index_pairs, const string_constraint_generatort &generator)
bool has_char_pointer_subtype(const typet &type, const namespacet &ns)
std::size_t max_string_length
array constructor from single element
Definition: std_expr.h:1550
size_t size() const
Definition: dstring.h:77
bitvector_typet index_type()
Definition: c_types.cpp:16
const struct_typet & to_struct_type(const typet &type)
Cast a generic typet to a struct_typet.
Definition: std_types.h:318
decision_proceduret::resultt dec_solve() override
The unary minus expression.
Definition: std_expr.h:444
static void debug_check_axioms_step(messaget::mstreamt &stream, const namespacet &ns, const T &axiom, const T &axiom_in_model, const exprt &negaxiom, const exprt &with_concretized_arrays)
Debugging function which outputs the different steps an axiom goes through to be checked in check axi...
exprt & false_case()
Definition: std_expr.h:3405
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:4465
decision_proceduret::resultt dec_solve() override
Main decision procedure of the solver.
static bool is_linear_arithmetic_expr(const exprt &expr, const symbol_exprt &var)
bool is_constant() const
Definition: expr.cpp:119
static exprt negation_of_not_contains_constraint(const string_not_contains_constraintt &constraint, const symbol_exprt &univ_var, const std::function< exprt(const exprt &)> &get)
Negates the constraint to be fed to a solver.
static bool find_qvar(const exprt &index, const symbol_exprt &qvar)
look for the symbol and return true if it is found
string_constraint_generatort generator
const std::unordered_map< exprt, array_string_exprt, irep_hash > & get_arrays_of_pointers() const
std::vector< exprt > operandst
Definition: expr.h:45
static std::vector< exprt > generate_instantiations(messaget::mstreamt &stream, const namespacet &ns, const string_constraint_generatort &generator, const index_set_pairt &index_set, const string_axiomst &axioms)
Instantiation of all constraints.
void output_equations(std::ostream &output, const std::vector< equal_exprt > &equations, const namespacet &ns)
Output a vector of equations to the given stream, used for debugging.
String support via creating string constraints and progressively instantiating the universal constrai...
std::vector< string_constraintt > universal
bool has_char_array_subexpr(const exprt &expr, const namespacet &ns)
static optionalt< exprt > get_array(const std::function< exprt(const exprt &)> &super_get, const namespacet &ns, const std::size_t max_string_length, messaget::mstreamt &stream, const array_string_exprt &arr)
Get a model of an array and put it in a certain form.
static void make_char_array_pointer_associations(string_constraint_generatort &generator, std::vector< equal_exprt > &equations)
Fill the array_pointer correspondence and replace the right hand sides of the corresponding equations...
static void initial_index_set(index_set_pairt &index_set, const namespacet &ns, const string_constraintt &axiom)
const equal_exprt & to_equal_expr(const exprt &expr)
Cast a generic exprt to an equal_exprt.
Definition: std_expr.h:1377
exprt get(const exprt &expr) const override
Definition: boolbv_get.cpp:21
Similar interface to union-find for expressions, with a function for replacing sub-expressions by the...
static std::pair< bool, std::vector< exprt > > check_axioms(const string_axiomst &axioms, string_constraint_generatort &generator, const std::function< exprt(const exprt &)> &get, messaget::mstreamt &stream, const namespacet &ns, std::size_t max_string_length, bool use_counter_example, ui_message_handlert::uit ui, const union_find_replacet &symbol_resolve)
Check axioms takes the model given by the underlying solver and answers whether it satisfies the stri...
std::vector< exprt > find_expressions(const std::size_t i)
exprt & index()
Definition: std_expr.h:1496
Maps equation to expressions contained in them and conversely expressions to equations that contain t...
const configt config_
static void add_string_equation_to_symbol_resolution(const equal_exprt &eq, union_find_replacet &symbol_resolve, const namespacet &ns)
Given an equation on strings, mark these strings as belonging to the same set in the symbol_resolve s...
static std::string string_of_array(const array_exprt &arr)
convert the content of a string to a more readable representation.
const array_typet & to_array_type(const typet &type)
Cast a generic typet to an array_typet.
Definition: std_types.h:1045
const exprt & exists_upper_bound() const
Base class for all expressions.
Definition: expr.h:42
static std::vector< exprt > extract_strings(const exprt &expr)
optionalt< exprt > make_array_pointer_association(const function_application_exprt &expr)
Associate array to pointer, and array to length.
void set_to(const exprt &expr, bool value) override
Record the constraints to ensure that the expression is true when the boolean is true and false other...
std::set< exprt > seen_instances
Operator to update elements in structs and arrays.
Definition: std_expr.h:3461
std::string to_string(const string_constraintt &expr)
Used for debug printing.
#define UNREACHABLE
Definition: invariant.h:250
literalt neg(literalt a)
Definition: literal.h:192
static std::map< exprt, int > map_representation_of_sum(const exprt &f)
#define string_refinement_invariantt(reason)
Universally quantified string constraint
string_axiomst axioms
const exprt & univ_upper_bound() const
arrays with given size
Definition: std_types.h:1004
binary minus
Definition: std_expr.h:959
static optionalt< interval_sparse_arrayt > of_expr(const exprt &expr, const exprt &extra_value)
If the expression is an array_exprt or a with_exprt uses the appropriate constructor, otherwise returns empty optional.
static std::vector< exprt > extract_strings_from_lhs(const exprt &lhs)
This is meant to be used on the lhs of an equation with string subtype.
Expression to hold a symbol (variable)
Definition: std_expr.h:90
depth_iteratort depth_end()
Definition: expr.cpp:301
int8_t s1
Definition: bytecode_info.h:59
mstreamt & debug() const
Definition: message.h:332
exprt get(const exprt &expr) const override
Evaluates the given expression in the valuation found by string_refinementt::dec_solve.
std::string utf16_constant_array_to_java(const array_exprt &arr, std::size_t length)
Construct a string from a constant array.
const typet & subtype() const
Definition: type.h:33
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:257
void set_to(const exprt &expr, bool value) override
Definition: boolbv.cpp:601
std::map< string_not_contains_constraintt, symbol_exprt > witness
const array_string_exprt & s0() const
bool is_char_type(const typet &type)
For now, any unsigned bitvector type of width smaller or equal to 16 is considered a character...
bool is_char_array_type(const typet &type, const namespacet &ns)
Distinguish char array from other types.
operandst & operands()
Definition: expr.h:66
std::vector< std::size_t > find_equations(const exprt &expr)
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
const std::vector< symbol_exprt > & get_index_symbols() const
Symbols used in existential quantifications.
exprt negation() const
std::vector< exprt > current_constraints
static array_index_mapt gather_indices(const exprt &expr)
exprt & array()
Definition: std_expr.h:1486
const index_exprt & to_index_expr(const exprt &expr)
Cast a generic exprt to an index_exprt.
Definition: std_expr.h:1517
bitvector_typet char_type()
Definition: c_types.cpp:114
array constructor from list of elements
Definition: std_expr.h:1617
void replace_symbols_in_equations(const union_find_replacet &symbol_resolve, std::vector< equal_exprt > &equations)
index_set_pairt index_sets
std::vector< string_not_contains_constraintt > not_contains
std::vector< std::pair< exprt, exprt > > to_vector() const
array_string_exprt & to_array_string_expr(exprt &expr)
Definition: string_expr.h:162
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:91
static exprt compute_inverse_function(messaget::mstreamt &stream, const exprt &qvar, const exprt &val, const exprt &f)
bool simplify(exprt &expr, const namespacet &ns)
void output_dot(std::ostream &stream) const
void add_lemma(const exprt &lemma, bool simplify_lemma=true)
Add the given lemma to the solver.
array index operator
Definition: std_expr.h:1462
static format_containert< T > format(const T &o)
Definition: format.h:35
const array_string_exprt & s1() const
find_qvar_visitort(const exprt &qvar)