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