cprover
acceleration_utils.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Loop Acceleration
4 
5 Author: Matt Lewis
6 
7 \*******************************************************************/
8 
11 
12 #include "acceleration_utils.h"
13 
14 #include <iostream>
15 #include <map>
16 #include <set>
17 #include <string>
18 #include <sstream>
19 #include <algorithm>
20 #include <ctime>
21 
23 #include <goto-programs/wp.h>
25 
26 #include <goto-symex/goto_symex.h>
28 
29 #include <analyses/goto_check.h>
30 
31 #include <ansi-c/expr2c.h>
32 
33 #include <util/symbol_table.h>
34 #include <util/options.h>
35 #include <util/std_expr.h>
36 #include <util/std_code.h>
37 #include <util/find_symbols.h>
38 #include <util/simplify_expr.h>
39 #include <util/replace_expr.h>
40 #include <util/arith_tools.h>
41 
42 #include "accelerator.h"
43 #include "util.h"
44 #include "cone_of_influence.h"
45 #include "overflow_instrumenter.h"
46 
48  const exprt &expr,
49  expr_sett &rvalues)
50 {
51  if(expr.id()==ID_symbol ||
52  expr.id()==ID_index ||
53  expr.id()==ID_member ||
54  expr.id()==ID_dereference)
55  {
56  rvalues.insert(expr);
57  }
58  else
59  {
60  forall_operands(it, expr)
61  {
62  gather_rvalues(*it, rvalues);
63  }
64  }
65 }
66 
68  const goto_programt &body,
69  expr_sett &modified)
70 {
72  find_modified(it, modified);
73 }
74 
76  const goto_programt::instructionst &instructions,
77  expr_sett &modified)
78 {
79  for(goto_programt::instructionst::const_iterator
80  it=instructions.begin();
81  it!=instructions.end();
82  ++it)
83  find_modified(it, modified);
84 }
85 
87  const patht &path,
88  expr_sett &modified)
89 {
90  for(const auto &step : path)
91  find_modified(step.loc, modified);
92 }
93 
96  expr_sett &modified)
97 {
98  for(const auto &step : loop)
99  find_modified(step, modified);
100 }
101 
104  expr_sett &modified)
105 {
106  if(t->is_assign())
107  {
108  code_assignt assignment=to_code_assign(t->code);
109  modified.insert(assignment.lhs());
110  }
111 }
112 
114  std::map<exprt, polynomialt> polynomials,
115  patht &path,
116  guard_managert &guard_manager)
117 {
118  // Checking that our polynomial is inductive with respect to the loop body is
119  // equivalent to checking safety of the following program:
120  //
121  // assume (target1==polynomial1);
122  // assume (target2==polynomial2)
123  // ...
124  // loop_body;
125  // loop_counter++;
126  // assert (target1==polynomial1);
127  // assert (target2==polynomial2);
128  // ...
129  scratch_programt program(symbol_table, message_handler, guard_manager);
130  std::vector<exprt> polynomials_hold;
131  substitutiont substitution;
132 
133  stash_polynomials(program, polynomials, substitution, path);
134 
135  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
136  it!=polynomials.end();
137  ++it)
138  {
139  const equal_exprt holds(it->first, it->second.to_expr());
140  program.add(goto_programt::make_assumption(holds));
141 
142  polynomials_hold.push_back(holds);
143  }
144 
145  program.append_path(path);
146 
147  auto inc_loop_counter = code_assignt(
148  loop_counter,
150 
151  program.add(goto_programt::make_assignment(inc_loop_counter));
152 
153  ensure_no_overflows(program);
154 
155  for(const auto &p : polynomials_hold)
157 
158 #ifdef DEBUG
159  std::cout << "Checking following program for inductiveness:\n";
160  program.output(ns, irep_idt(), std::cout);
161 #endif
162 
163  try
164  {
165  if(program.check_sat(guard_manager))
166  {
167  // We found a counterexample to inductiveness... :-(
168  #ifdef DEBUG
169  std::cout << "Not inductive!\n";
170  #endif
171  return false;
172  }
173  else
174  {
175  return true;
176  }
177  }
178  catch(const std::string &s)
179  {
180  std::cout << "Error in inductiveness SAT check: " << s << '\n';
181  return false;
182  }
183  catch (const char *s)
184  {
185  std::cout << "Error in inductiveness SAT check: " << s << '\n';
186  return false;
187  }
188 }
189 
191  scratch_programt &program,
192  std::map<exprt, polynomialt> &polynomials,
193  substitutiont &substitution,
194  patht &path)
195 {
196  expr_sett modified;
197 
198  find_modified(path, modified);
199  stash_variables(program, modified, substitution);
200 
201  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
202  it!=polynomials.end();
203  ++it)
204  {
205  it->second.substitute(substitution);
206  }
207 }
208 
210  scratch_programt &program,
211  expr_sett modified,
212  substitutiont &substitution)
213 {
214  find_symbols_sett vars =
215  find_symbols_or_nexts(modified.begin(), modified.end());
216  const irep_idt &loop_counter_name =
218  vars.erase(loop_counter_name);
219 
220  for(const irep_idt &symbol : vars)
221  {
222  const symbolt &orig = symbol_table.lookup_ref(symbol);
223  symbolt stashed_sym=fresh_symbol("polynomial::stash", orig.type);
224  substitution[orig.symbol_expr()]=stashed_sym.symbol_expr();
225  program.assign(stashed_sym.symbol_expr(), orig.symbol_expr());
226  }
227 }
228 
229 /*
230  * Finds a precondition which guarantees that all the assumptions and assertions
231  * along this path hold.
232  *
233  * This is not the weakest precondition, since we make underapproximations due
234  * to aliasing.
235  */
236 
238 {
239  exprt ret=false_exprt();
240 
241  for(patht::reverse_iterator r_it=path.rbegin();
242  r_it!=path.rend();
243  ++r_it)
244  {
245  goto_programt::const_targett t=r_it->loc;
246 
247  if(t->is_assign())
248  {
249  // XXX Need to check for aliasing...
250  const code_assignt &assignment=to_code_assign(t->code);
251  const exprt &lhs=assignment.lhs();
252  const exprt &rhs=assignment.rhs();
253 
254  if(lhs.id()==ID_symbol ||
255  lhs.id()==ID_index ||
256  lhs.id()==ID_dereference)
257  {
258  replace_expr(lhs, rhs, ret);
259  }
260  else
261  {
262  throw "couldn't take WP of " + expr2c(lhs, ns) + "=" + expr2c(rhs, ns);
263  }
264  }
265  else if(t->is_assume() || t->is_assert())
266  {
267  ret = implies_exprt(t->get_condition(), ret);
268  }
269  else
270  {
271  // Ignore.
272  }
273 
274  if(!r_it->guard.is_true() && !r_it->guard.is_nil())
275  {
276  // The guard isn't constant true, so we need to accumulate that too.
277  ret=implies_exprt(r_it->guard, ret);
278  }
279  }
280 
281  // Hack: replace array accesses with nondet.
282  expr_mapt array_abstractions;
283  // abstract_arrays(ret, array_abstractions);
284 
285  simplify(ret, ns);
286 
287  return ret;
288 }
289 
291  exprt &expr,
292  expr_mapt &abstractions)
293 {
294  if(expr.id()==ID_index ||
295  expr.id()==ID_dereference)
296  {
297  expr_mapt::iterator it=abstractions.find(expr);
298 
299  if(it==abstractions.end())
300  {
301  symbolt sym=fresh_symbol("accelerate::array_abstraction", expr.type());
302  abstractions[expr]=sym.symbol_expr();
303  expr=sym.symbol_expr();
304  }
305  else
306  {
307  expr=it->second;
308  }
309  }
310  else
311  {
312  Forall_operands(it, expr)
313  {
314  abstract_arrays(*it, abstractions);
315  }
316  }
317 }
318 
320 {
321  Forall_operands(it, expr)
322  {
323  push_nondet(*it);
324  }
325 
326  if(expr.id() == ID_not && to_not_expr(expr).op().id() == ID_nondet)
327  {
328  expr = side_effect_expr_nondett(expr.type(), expr.source_location());
329  }
330  else if(expr.id()==ID_equal ||
331  expr.id()==ID_lt ||
332  expr.id()==ID_gt ||
333  expr.id()==ID_le ||
334  expr.id()==ID_ge)
335  {
336  const auto &rel_expr = to_binary_relation_expr(expr);
337  if(rel_expr.lhs().id() == ID_nondet || rel_expr.rhs().id() == ID_nondet)
338  {
339  expr = side_effect_expr_nondett(expr.type(), expr.source_location());
340  }
341  }
342 }
343 
345  std::map<exprt, polynomialt> polynomials,
346  patht &path,
347  exprt &guard,
348  guard_managert &guard_manager)
349 {
350  // We want to check that if an assumption fails, the next iteration can't be
351  // feasible again. To do this we check the following program for safety:
352  //
353  // loop_counter=1;
354  // assume(target1==polynomial1);
355  // assume(target2==polynomial2);
356  // ...
357  // assume(precondition);
358  //
359  // loop_counter=*;
360  // target1=polynomial1);
361  // target2=polynomial2);
362  // ...
363  // assume(!precondition);
364  //
365  // loop_counter++;
366  //
367  // target1=polynomial1;
368  // target2=polynomial2;
369  // ...
370  //
371  // assume(no overflows in above program)
372  // assert(!precondition);
373 
374  exprt condition=precondition(path);
375  scratch_programt program(symbol_table, message_handler, guard_manager);
376 
377  substitutiont substitution;
378  stash_polynomials(program, polynomials, substitution, path);
379 
380  std::vector<exprt> polynomials_hold;
381 
382  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
383  it!=polynomials.end();
384  ++it)
385  {
386  exprt lhs=it->first;
387  exprt rhs=it->second.to_expr();
388 
389  polynomials_hold.push_back(equal_exprt(lhs, rhs));
390  }
391 
393 
394  for(std::vector<exprt>::iterator it=polynomials_hold.begin();
395  it!=polynomials_hold.end();
396  ++it)
397  {
398  program.assume(*it);
399  }
400 
401  program.assume(not_exprt(condition));
402 
403  program.assign(
404  loop_counter,
406 
407  for(std::map<exprt, polynomialt>::iterator p_it=polynomials.begin();
408  p_it!=polynomials.end();
409  ++p_it)
410  {
411  program.assign(p_it->first, p_it->second.to_expr());
412  }
413 
414  program.assume(condition);
415  program.assign(
416  loop_counter,
418 
419  for(std::map<exprt, polynomialt>::iterator p_it=polynomials.begin();
420  p_it!=polynomials.end();
421  ++p_it)
422  {
423  program.assign(p_it->first, p_it->second.to_expr());
424  }
425 
426  ensure_no_overflows(program);
427 
428  program.add(goto_programt::make_assertion(condition));
429 
430  guard=not_exprt(condition);
431  simplify(guard, ns);
432 
433 #ifdef DEBUG
434  std::cout << "Checking following program for monotonicity:\n";
435  program.output(ns, irep_idt(), std::cout);
436 #endif
437 
438  try
439  {
440  if(program.check_sat(guard_manager))
441  {
442  #ifdef DEBUG
443  std::cout << "Path is not monotone\n";
444  #endif
445 
446  return false;
447  }
448  }
449  catch(const std::string &s)
450  {
451  std::cout << "Error in monotonicity SAT check: " << s << '\n';
452  return false;
453  }
454  catch(const char *s)
455  {
456  std::cout << "Error in monotonicity SAT check: " << s << '\n';
457  return false;
458  }
459 
460 #ifdef DEBUG
461  std::cout << "Path is monotone\n";
462 #endif
463 
464  return true;
465 }
466 
468 {
469  symbolt overflow_sym=fresh_symbol("polynomial::overflow", bool_typet());
470  const exprt &overflow_var=overflow_sym.symbol_expr();
471  overflow_instrumentert instrumenter(program, overflow_var, symbol_table);
472 
473  optionst checker_options;
474 
475  checker_options.set_option("signed-overflow-check", true);
476  checker_options.set_option("unsigned-overflow-check", true);
477  checker_options.set_option("assert-to-assume", true);
478  checker_options.set_option("assumptions", true);
479  checker_options.set_option("simplify", true);
480 
481 
482 #ifdef DEBUG
483  time_t now=time(0);
484  std::cout << "Adding overflow checks at " << now << "...\n";
485 #endif
486 
487  instrumenter.add_overflow_checks();
488  program.add(goto_programt::make_assumption(not_exprt(overflow_var)));
489 
490  // goto_functionst::goto_functiont fn;
491  // fn.body.instructions.swap(program.instructions);
492  // goto_check(ns, checker_options, fn);
493  // fn.body.instructions.swap(program.instructions);
494 
495 #ifdef DEBUG
496  now=time(0);
497  std::cout << "Done at " << now << ".\n";
498 #endif
499 }
500 
502  goto_programt::instructionst &loop_body,
503  expr_sett &arrays_written)
504 {
505  expr_pairst assignments;
506 
507  for(goto_programt::instructionst::reverse_iterator r_it=loop_body.rbegin();
508  r_it!=loop_body.rend();
509  ++r_it)
510  {
511  if(r_it->is_assign())
512  {
513  // Is this an array assignment?
514  code_assignt assignment=to_code_assign(r_it->code);
515 
516  if(assignment.lhs().id()==ID_index)
517  {
518  // This is an array assignment -- accumulate it in our list.
519  assignments.push_back(
520  std::make_pair(assignment.lhs(), assignment.rhs()));
521 
522  // Also add this array to the set of arrays written to.
523  index_exprt index_expr=to_index_expr(assignment.lhs());
524  arrays_written.insert(index_expr.array());
525  }
526  else
527  {
528  // This is a regular assignment. Do weakest precondition on all our
529  // array expressions with respect to this assignment.
530  for(expr_pairst::iterator a_it=assignments.begin();
531  a_it!=assignments.end();
532  ++a_it)
533  {
534  replace_expr(assignment.lhs(), assignment.rhs(), a_it->first);
535  replace_expr(assignment.lhs(), assignment.rhs(), a_it->second);
536  }
537  }
538  }
539  }
540 
541  return assignments;
542 }
543 
545  goto_programt::instructionst &loop_body,
546  std::map<exprt, polynomialt> &polynomials,
547  substitutiont &substitution,
548  scratch_programt &program)
549 {
550 #ifdef DEBUG
551  std::cout << "Doing arrays...\n";
552 #endif
553 
554  expr_sett arrays_written;
555  expr_pairst array_assignments;
556 
557  array_assignments=gather_array_assignments(loop_body, arrays_written);
558 
559 #ifdef DEBUG
560  std::cout << "Found " << array_assignments.size()
561  << " array assignments\n";
562 #endif
563 
564  if(array_assignments.empty())
565  {
566  // The loop doesn't write to any arrays. We're done!
567  return true;
568  }
569 
570  polynomial_array_assignmentst poly_assignments;
571  polynomialst nondet_indices;
572 
574  array_assignments, polynomials, poly_assignments, nondet_indices))
575  {
576  // We weren't able to model some array assignment. That means we need to
577  // bail out altogether :-(
578 #ifdef DEBUG
579  std::cout << "Couldn't model an array assignment :-(\n";
580 #endif
581  return false;
582  }
583 
584  // First make all written-to arrays nondeterministic.
585  for(expr_sett::iterator it=arrays_written.begin();
586  it!=arrays_written.end();
587  ++it)
588  {
589  program.assign(
590  *it, side_effect_expr_nondett(it->type(), source_locationt()));
591  }
592 
593  // Now add in all the effects of this loop on the arrays.
594  exprt::operandst array_operands;
595 
596  for(polynomial_array_assignmentst::iterator it=poly_assignments.begin();
597  it!=poly_assignments.end();
598  ++it)
599  {
600  polynomialt stashed_index=it->index;
601  polynomialt stashed_value=it->value;
602 
603  stashed_index.substitute(substitution);
604  stashed_value.substitute(substitution);
605 
606  array_operands.push_back(equal_exprt(
607  index_exprt(it->array, stashed_index.to_expr()),
608  stashed_value.to_expr()));
609  }
610 
611  exprt arrays_expr=conjunction(array_operands);
612 
613  symbolt k_sym=fresh_symbol("polynomial::k", unsigned_poly_type());
614  const symbol_exprt k = k_sym.symbol_expr();
615 
616  const and_exprt k_bound(
617  binary_relation_exprt(from_integer(0, k.type()), ID_le, k),
619  replace_expr(loop_counter, k, arrays_expr);
620 
621  implies_exprt implies(k_bound, arrays_expr);
622 
623  const forall_exprt forall(k, implies);
624  program.assume(forall);
625 
626  // Now have to encode that the array doesn't change at indices we didn't
627  // touch.
628  for(expr_sett::iterator a_it=arrays_written.begin();
629  a_it!=arrays_written.end();
630  ++a_it)
631  {
632  exprt array=*a_it;
633  exprt old_array=substitution[array];
634  std::vector<polynomialt> indices;
635  bool nonlinear_index=false;
636 
637  for(polynomial_array_assignmentst::iterator it=poly_assignments.begin();
638  it!=poly_assignments.end();
639  ++it)
640  {
641  if(it->array==array)
642  {
643  polynomialt index=it->index;
644  index.substitute(substitution);
645  indices.push_back(index);
646 
647  if(index.max_degree(loop_counter) > 1 ||
648  (index.coeff(loop_counter)!=1 && index.coeff(loop_counter)!=-1))
649  {
650 #ifdef DEBUG
651  std::cout << expr2c(index.to_expr(), ns) << " is nonlinear\n";
652 #endif
653  nonlinear_index=true;
654  }
655  }
656  }
657 
658  exprt idx_never_touched=nil_exprt();
659  symbolt idx_sym=fresh_symbol("polynomial::idx", signed_poly_type());
660  const symbol_exprt idx = idx_sym.symbol_expr();
661 
662  // Optimization: if all the assignments to a particular array A are of the
663  // form:
664  // A[loop_counter + e]=f
665  // where e does not contain loop_counter, we don't need quantifier
666  // alternation to encode the non-changedness. We can get away
667  // with the expression:
668  // forall k; k < e || k > loop_counter+e => A[k]=old_A[k]
669 
670  if(!nonlinear_index)
671  {
672  polynomialt pos_eliminator, neg_eliminator;
673 
674  neg_eliminator.from_expr(loop_counter);
675  pos_eliminator=neg_eliminator;
676  pos_eliminator.mult(-1);
677 
678  exprt::operandst unchanged_operands;
679 
680  for(std::vector<polynomialt>::iterator it=indices.begin();
681  it!=indices.end();
682  ++it)
683  {
684  polynomialt index=*it;
685  exprt max_idx, min_idx;
686 
687  if(index.coeff(loop_counter)==1)
688  {
689  max_idx=
690  minus_exprt(
691  index.to_expr(),
692  from_integer(1, index.to_expr().type()));
693  index.add(pos_eliminator);
694  min_idx=index.to_expr();
695  }
696  else if(index.coeff(loop_counter)==-1)
697  {
698  min_idx=
699  plus_exprt(
700  index.to_expr(),
701  from_integer(1, index.to_expr().type()));
702  index.add(neg_eliminator);
703  max_idx=index.to_expr();
704  }
705  else
706  {
707  assert(!"ITSALLGONEWRONG");
708  }
709 
710  or_exprt unchanged_by_this_one(
711  binary_relation_exprt(idx, ID_lt, min_idx),
712  binary_relation_exprt(idx, ID_gt, max_idx));
713  unchanged_operands.push_back(unchanged_by_this_one);
714  }
715 
716  idx_never_touched=conjunction(unchanged_operands);
717  }
718  else
719  {
720  // The vector `indices' now contains all of the indices written
721  // to for the current array, each with the free variable
722  // loop_counter. Now let's build an expression saying that the
723  // fresh variable idx is none of these indices.
724  exprt::operandst idx_touched_operands;
725 
726  for(std::vector<polynomialt>::iterator it=indices.begin();
727  it!=indices.end();
728  ++it)
729  {
730  idx_touched_operands.push_back(
731  not_exprt(equal_exprt(idx, it->to_expr())));
732  }
733 
734  exprt idx_not_touched=conjunction(idx_touched_operands);
735 
736  // OK, we have an expression saying idx is not touched by the
737  // loop_counter'th iteration. Let's quantify that to say that
738  // idx is not touched at all.
739  symbolt l_sym=fresh_symbol("polynomial::l", signed_poly_type());
740  exprt l=l_sym.symbol_expr();
741 
742  replace_expr(loop_counter, l, idx_not_touched);
743 
744  // 0 < l <= loop_counter => idx_not_touched
745  and_exprt l_bound(
746  binary_relation_exprt(from_integer(0, l.type()), ID_lt, l),
748  implies_exprt idx_not_touched_bound(l_bound, idx_not_touched);
749 
750  idx_never_touched=exprt(ID_forall);
751  idx_never_touched.type()=bool_typet();
752  idx_never_touched.copy_to_operands(l);
753  idx_never_touched.copy_to_operands(idx_not_touched_bound);
754  }
755 
756  // We now have an expression saying idx is never touched. It is the
757  // following:
758  // forall l . 0 < l <= loop_counter => idx!=index_1 && ... && idx!=index_N
759  //
760  // Now let's build an expression saying that such an idx doesn't get
761  // updated by this loop, i.e.
762  // idx_never_touched => A[idx]==A_old[idx]
763  equal_exprt value_unchanged(
764  index_exprt(array, idx), index_exprt(old_array, idx));
765  implies_exprt idx_unchanged(idx_never_touched, value_unchanged);
766 
767  // Cool. Finally, we want to quantify over idx to say that every idx that
768  // is never touched has its value unchanged. So our expression is:
769  // forall idx . idx_never_touched => A[idx]==A_old[idx]
770  const forall_exprt array_unchanged(idx, idx_unchanged);
771 
772  // And we're done!
773  program.assume(array_unchanged);
774  }
775 
776  return true;
777 }
778 
780  expr_pairst &array_assignments,
781  std::map<exprt, polynomialt> &polynomials,
782  polynomial_array_assignmentst &array_polynomials,
783  polynomialst &nondet_indices)
784 {
785  for(expr_pairst::iterator it=array_assignments.begin();
786  it!=array_assignments.end();
787  ++it)
788  {
789  polynomial_array_assignmentt poly_assignment;
790  index_exprt index_expr=to_index_expr(it->first);
791 
792  poly_assignment.array=index_expr.array();
793 
794  if(!expr2poly(index_expr.index(), polynomials, poly_assignment.index))
795  {
796  // Couldn't convert the index -- bail out.
797 #ifdef DEBUG
798  std::cout << "Couldn't convert index: "
799  << expr2c(index_expr.index(), ns) << '\n';
800 #endif
801  return false;
802  }
803 
804 #ifdef DEBUG
805  std::cout << "Converted index to: "
806  << expr2c(poly_assignment.index.to_expr(), ns)
807  << '\n';
808 #endif
809 
810  if(it->second.id()==ID_nondet)
811  {
812  nondet_indices.push_back(poly_assignment.index);
813  }
814  else if(!expr2poly(it->second, polynomials, poly_assignment.value))
815  {
816  // Couldn't conver the RHS -- bail out.
817 #ifdef DEBUG
818  std::cout << "Couldn't convert RHS: " << expr2c(it->second, ns)
819  << '\n';
820 #endif
821  return false;
822  }
823  else
824  {
825 #ifdef DEBUG
826  std::cout << "Converted RHS to: "
827  << expr2c(poly_assignment.value.to_expr(), ns)
828  << '\n';
829 #endif
830 
831  array_polynomials.push_back(poly_assignment);
832  }
833  }
834 
835  return true;
836 }
837 
839  exprt &expr,
840  std::map<exprt, polynomialt> &polynomials,
841  polynomialt &poly)
842 {
843  exprt subbed_expr=expr;
844 
845  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
846  it!=polynomials.end();
847  ++it)
848  {
849  replace_expr(it->first, it->second.to_expr(), subbed_expr);
850  }
851 
852 #ifdef DEBUG
853  std::cout << "expr2poly(" << expr2c(subbed_expr, ns) << ")\n";
854 #endif
855 
856  try
857  {
858  poly.from_expr(subbed_expr);
859  }
860  catch(...)
861  {
862  return false;
863  }
864 
865  return true;
866 }
867 
870  std::map<exprt, polynomialt> &polynomials,
871  substitutiont &substitution,
872  expr_sett &nonrecursive,
873  scratch_programt &program)
874 {
875  // We have some variables that are defined non-recursively -- that
876  // is to say, their value at the end of a loop iteration does not
877  // depend on their value at the previous iteration. We can solve
878  // for these variables by just forward simulating the path and
879  // taking the expressions we get at the end.
880  replace_mapt state;
881  std::unordered_set<index_exprt, irep_hash> array_writes;
882  expr_sett arrays_written;
883  expr_sett arrays_read;
884 
885  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
886  it!=polynomials.end();
887  ++it)
888  {
889  const exprt &var=it->first;
890  polynomialt poly=it->second;
891  poly.substitute(substitution);
892  exprt e=poly.to_expr();
893 
894 #if 0
895  replace_expr(
896  loop_counter,
898  e);
899 #endif
900 
901  state[var]=e;
902  }
903 
904  for(expr_sett::iterator it=nonrecursive.begin();
905  it!=nonrecursive.end();
906  ++it)
907  {
908  exprt e=*it;
909  state[e]=e;
910  }
911 
912  for(goto_programt::instructionst::iterator it=body.begin();
913  it!=body.end();
914  ++it)
915  {
916  if(it->is_assign())
917  {
918  exprt lhs = it->get_assign().lhs();
919  exprt rhs = it->get_assign().rhs();
920 
921  if(lhs.id()==ID_dereference)
922  {
923  // Not handling pointer dereferences yet...
924 #ifdef DEBUG
925  std::cout << "Bailing out on write-through-pointer\n";
926 #endif
927  return false;
928  }
929 
930  if(lhs.id()==ID_index)
931  {
932  auto &lhs_index_expr = to_index_expr(lhs);
933  replace_expr(state, lhs_index_expr.index());
934  array_writes.insert(lhs_index_expr);
935 
936  if(arrays_written.find(lhs_index_expr.array()) != arrays_written.end())
937  {
938  // We've written to this array before -- be conservative and bail
939  // out now.
940 #ifdef DEBUG
941  std::cout << "Bailing out on array written to twice in loop: "
942  << expr2c(lhs_index_expr.array(), ns) << '\n';
943 #endif
944  return false;
945  }
946 
947  arrays_written.insert(lhs_index_expr.array());
948  }
949 
950  replace_expr(state, rhs);
951  state[lhs]=rhs;
952 
953  gather_array_accesses(rhs, arrays_read);
954  }
955  }
956 
957  // Be conservative: if we read and write from the same array, bail out.
958  for(expr_sett::iterator it=arrays_written.begin();
959  it!=arrays_written.end();
960  ++it)
961  {
962  if(arrays_read.find(*it)!=arrays_read.end())
963  {
964 #ifdef DEBUG
965  std::cout << "Bailing out on array read and written on same path\n";
966 #endif
967  return false;
968  }
969  }
970 
971  for(expr_sett::iterator it=nonrecursive.begin();
972  it!=nonrecursive.end();
973  ++it)
974  {
975  if(it->id()==ID_symbol)
976  {
977  exprt &val=state[*it];
978  program.assign(*it, val);
979 
980 #ifdef DEBUG
981  std::cout << "Fitted nonrecursive: " << expr2c(*it, ns) << "=" <<
982  expr2c(val, ns) << '\n';
983 #endif
984  }
985  }
986 
987  for(const auto &write : array_writes)
988  {
989  const auto &lhs = write;
990  const auto &rhs = state[write];
991 
992  if(!assign_array(lhs, rhs, program))
993  {
994 #ifdef DEBUG
995  std::cout << "Failed to assign a nonrecursive array: " <<
996  expr2c(lhs, ns) << "=" << expr2c(rhs, ns) << '\n';
997 #endif
998  return false;
999  }
1000  }
1001 
1002  return true;
1003 }
1004 
1006  const index_exprt &lhs,
1007  const exprt &rhs,
1008  scratch_programt &program)
1009 {
1010 #ifdef DEBUG
1011  std::cout << "Modelling array assignment " << expr2c(lhs, ns) << "=" <<
1012  expr2c(rhs, ns) << '\n';
1013 #endif
1014 
1015  if(lhs.id()==ID_dereference)
1016  {
1017  // Don't handle writes through pointers for now...
1018 #ifdef DEBUG
1019  std::cout << "Bailing out on write-through-pointer\n";
1020 #endif
1021  return false;
1022  }
1023 
1024  // We handle N iterations of the array write:
1025  //
1026  // A[i]=e
1027  //
1028  // by the following sequence:
1029  //
1030  // A'=nondet()
1031  // assume(forall 0 <= k < N . A'[i(k/loop_counter)]=e(k/loop_counter));
1032  // assume(forall j . notwritten(j) ==> A'[j]=A[j]);
1033  // A=A'
1034 
1035  const exprt &arr=lhs.op0();
1036  exprt idx=lhs.op1();
1037  const exprt &fresh_array =
1038  fresh_symbol("polynomial::array", arr.type()).symbol_expr();
1039 
1040  // First make the fresh nondet array.
1041  program.assign(
1042  fresh_array, side_effect_expr_nondett(arr.type(), lhs.source_location()));
1043 
1044  // Then assume that the fresh array has the appropriate values at the indices
1045  // the loop updated.
1046  equal_exprt changed(lhs, rhs);
1047  replace_expr(arr, fresh_array, changed);
1048 
1049  symbolt k_sym=fresh_symbol("polynomial::k", unsigned_poly_type());
1050  const symbol_exprt k = k_sym.symbol_expr();
1051 
1052  const and_exprt k_bound(
1053  binary_relation_exprt(from_integer(0, k.type()), ID_le, k),
1054  binary_relation_exprt(k, ID_lt, loop_counter));
1055  replace_expr(loop_counter, k, changed);
1056 
1057  implies_exprt implies(k_bound, changed);
1058 
1059  forall_exprt forall(k, implies);
1060  program.assume(forall);
1061 
1062  // Now let's ensure that the array did not change at the indices we
1063  // didn't touch.
1064 #ifdef DEBUG
1065  std::cout << "Trying to polynomialize " << expr2c(idx, ns) << '\n';
1066 #endif
1067 
1068  polynomialt poly;
1069 
1070  try
1071  {
1072  if(idx.id()==ID_pointer_offset)
1073  {
1074  poly.from_expr(to_unary_expr(idx).op());
1075  }
1076  else
1077  {
1078  poly.from_expr(idx);
1079  }
1080  }
1081  catch(...)
1082  {
1083  // idx is probably nonlinear... bail out.
1084 #ifdef DEBUG
1085  std::cout << "Failed to polynomialize\n";
1086 #endif
1087  return false;
1088  }
1089 
1090  if(poly.max_degree(loop_counter) > 1)
1091  {
1092  // The index expression is nonlinear, e.g. it's something like:
1093  //
1094  // A[x*loop_counter]=0;
1095  //
1096  // where x changes inside the loop. Modelling this requires quantifier
1097  // alternation, and that's too expensive. Bail out.
1098 #ifdef DEBUG
1099  std::cout << "Bailing out on nonlinear index: "
1100  << expr2c(idx, ns) << '\n';
1101 #endif
1102  return false;
1103  }
1104 
1105  int stride=poly.coeff(loop_counter);
1106  exprt not_touched;
1107  exprt lower_bound=idx;
1108  exprt upper_bound=idx;
1109 
1110  if(stride > 0)
1111  {
1112  replace_expr(
1113  loop_counter, from_integer(0, loop_counter.type()), lower_bound);
1114  lower_bound = simplify_expr(std::move(lower_bound), ns);
1115  }
1116  else
1117  {
1118  replace_expr(
1119  loop_counter, from_integer(0, loop_counter.type()), upper_bound);
1120  upper_bound = simplify_expr(std::move(upper_bound), ns);
1121  }
1122 
1123  if(stride==0)
1124  {
1125  // The index we write to doesn't depend on the loop counter....
1126  // We could optimise for this, but I suspect it's not going to
1127  // happen to much so just bail out.
1128 #ifdef DEBUG
1129  std::cout << "Bailing out on write to constant array index: " <<
1130  expr2c(idx, ns) << '\n';
1131 #endif
1132  return false;
1133  }
1134  else if(stride == 1 || stride == -1)
1135  {
1136  // This is the simplest case -- we have an assignment like:
1137  //
1138  // A[c + loop_counter]=e;
1139  //
1140  // where c doesn't change in the loop. The expression to say it doesn't
1141  // change at unexpected places is:
1142  //
1143  // forall k . (k < c || k >= loop_counter + c) ==> A'[k]==A[k]
1144 
1145  not_touched = or_exprt(
1146  binary_relation_exprt(k, ID_lt, lower_bound),
1147  binary_relation_exprt(k, ID_ge, upper_bound));
1148  }
1149  else
1150  {
1151  // A more complex case -- our assignment is:
1152  //
1153  // A[c + s*loop_counter]=e;
1154  //
1155  // where c and s are constants. Now our condition for an index i
1156  // to be unchanged is:
1157  //
1158  // i < c || i >= (c + s*loop_counter) || (i - c) % s!=0
1159 
1160  const minus_exprt step(k, lower_bound);
1161 
1162  not_touched = or_exprt(
1163  or_exprt(
1164  binary_relation_exprt(k, ID_lt, lower_bound),
1165  binary_relation_exprt(k, ID_ge, lower_bound)),
1167  mod_exprt(step, from_integer(stride, step.type())),
1168  from_integer(0, step.type())));
1169  }
1170 
1171  // OK now do the assumption.
1172  exprt fresh_lhs=lhs;
1173  exprt old_lhs=lhs;
1174 
1175  replace_expr(arr, fresh_array, fresh_lhs);
1176  replace_expr(loop_counter, k, fresh_lhs);
1177 
1178  replace_expr(loop_counter, k, old_lhs);
1179 
1180  equal_exprt idx_unchanged(fresh_lhs, old_lhs);
1181 
1182  implies=implies_exprt(not_touched, idx_unchanged);
1183  forall.where() = implies;
1184 
1185  program.assume(forall);
1186 
1187  // Finally, assign the array to the fresh one we've just build.
1188  program.assign(arr, fresh_array);
1189 
1190  return true;
1191 }
1192 
1194  const exprt &e,
1195  expr_sett &arrays)
1196 {
1197  if(e.id() == ID_index)
1198  {
1199  arrays.insert(to_index_expr(e).array());
1200  }
1201  else if(e.id() == ID_dereference)
1202  {
1203  arrays.insert(to_dereference_expr(e).pointer());
1204  }
1205 
1206  forall_operands(it, e)
1207  {
1208  gather_array_accesses(*it, arrays);
1209  }
1210 }
1211 
1213  scratch_programt &program,
1214  std::set<std::pair<expr_listt, exprt> > &coefficients,
1215  polynomialt &polynomial)
1216 {
1217  for(std::set<std::pair<expr_listt, exprt> >::iterator it=coefficients.begin();
1218  it!=coefficients.end();
1219  ++it)
1220  {
1221  monomialt monomial;
1222  expr_listt terms=it->first;
1223  exprt coefficient=it->second;
1224  constant_exprt concrete_term=to_constant_expr(program.eval(coefficient));
1225  std::map<exprt, int> degrees;
1226 
1227  mp_integer mp=binary2integer(concrete_term.get_value().c_str(), true);
1228  monomial.coeff = numeric_cast_v<int>(mp);
1229 
1230  if(monomial.coeff==0)
1231  {
1232  continue;
1233  }
1234 
1235  for(const auto &term : terms)
1236  {
1237  if(degrees.find(term)!=degrees.end())
1238  {
1239  degrees[term]++;
1240  }
1241  else
1242  {
1243  degrees[term]=1;
1244  }
1245  }
1246 
1247  for(std::map<exprt, int>::iterator it=degrees.begin();
1248  it!=degrees.end();
1249  ++it)
1250  {
1251  monomialt::termt term;
1252  term.var=it->first;
1253  term.exp=it->second;
1254  monomial.terms.push_back(term);
1255  }
1256 
1257  polynomial.monomials.push_back(monomial);
1258  }
1259 }
1260 
1262 {
1263  static int num_symbols=0;
1264 
1265  std::string name=base + "_" + std::to_string(num_symbols++);
1266  symbolt ret;
1267  ret.module="scratch";
1268  ret.name=name;
1269  ret.base_name=name;
1270  ret.pretty_name=name;
1271  ret.type=type;
1272 
1273  symbol_table.add(ret);
1274 
1275  return ret;
1276 }
acceleration_utilst::symbol_table
symbol_tablet & symbol_table
Definition: acceleration_utils.h:157
exprt::copy_to_operands
void copy_to_operands(const exprt &expr)
Copy the given argument to the end of exprt's operands.
Definition: expr.h:150
polynomialt::from_expr
void from_expr(const exprt &expr)
Definition: polynomial.cpp:101
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symex_target_equation.h
Generate Equation using Symbolic Execution.
overflow_instrumenter.h
Loop Acceleration.
dstringt::c_str
const char * c_str() const
Definition: dstring.h:99
to_unary_expr
const unary_exprt & to_unary_expr(const exprt &expr)
Cast an exprt to a unary_exprt.
Definition: std_expr.h:316
polynomialt::add
void add(polynomialt &other)
Definition: polynomial.cpp:179
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
polynomialt
Definition: polynomial.h:42
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
Forall_operands
#define Forall_operands(it, expr)
Definition: expr.h:24
arith_tools.h
acceleration_utilst::do_assumptions
bool do_assumptions(std::map< exprt, polynomialt > polynomials, patht &body, exprt &guard, guard_managert &guard_manager)
Definition: acceleration_utils.cpp:344
acceleration_utilst::expr_pairst
std::vector< expr_pairt > expr_pairst
Definition: acceleration_utils.h:95
forall_exprt
A forall expression.
Definition: mathematical_expr.h:341
optionst
Definition: options.h:23
typet
The type of an expression, extends irept.
Definition: type.h:29
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
acceleration_utilst::fresh_symbol
symbolt fresh_symbol(std::string base, typet type)
Definition: acceleration_utils.cpp:1261
acceleration_utilst::push_nondet
void push_nondet(exprt &expr)
Definition: acceleration_utils.cpp:319
find_symbols_or_nexts
void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest)
Add to the set dest the sub-expressions of src with id ID_symbol or ID_next_symbol.
Definition: find_symbols.cpp:18
to_index_expr
const index_exprt & to_index_expr(const exprt &expr)
Cast an exprt to an index_exprt.
Definition: std_expr.h:1347
expr_listt
std::list< exprt > expr_listt
Definition: acceleration_utils.h:34
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
goto_programt::instructionst
std::list< instructiont > instructionst
Definition: goto_program.h:577
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
acceleration_utils.h
Loop Acceleration.
monomialt::termt::exp
unsigned int exp
Definition: polynomial.h:26
acceleration_utilst::assign_array
bool assign_array(const index_exprt &lhs, const exprt &rhs, scratch_programt &program)
Definition: acceleration_utils.cpp:1005
acceleration_utilst::message_handler
message_handlert & message_handler
Definition: acceleration_utils.h:39
and_exprt
Boolean AND.
Definition: std_expr.h:2137
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:686
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:881
acceleration_utilst::do_arrays
bool do_arrays(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, substitutiont &substitution, scratch_programt &program)
Definition: acceleration_utils.cpp:544
exprt
Base class for all expressions.
Definition: expr.h:53
symbolt::base_name
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
options.h
Options.
optionst::set_option
void set_option(const std::string &option, const bool value)
Definition: options.cpp:28
irep_idt
dstringt irep_idt
Definition: irep.h:32
bool_typet
The Boolean type.
Definition: std_types.h:37
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:55
acceleration_utilst::check_inductive
bool check_inductive(std::map< exprt, polynomialt > polynomials, patht &path, guard_managert &guard_manager)
Definition: acceleration_utils.cpp:113
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
polynomialt::monomials
std::vector< monomialt > monomials
Definition: polynomial.h:46
equal_exprt
Equality.
Definition: std_expr.h:1190
goto_programt::make_assignment
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:1024
unsigned_poly_type
unsignedbv_typet unsigned_poly_type()
Definition: util.cpp:25
notequal_exprt
Disequality.
Definition: std_expr.h:1248
acceleration_utilst::find_modified
void find_modified(const patht &path, expr_sett &modified)
Definition: acceleration_utils.cpp:86
symbolt::pretty_name
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
guard_expr_managert
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:23
acceleration_utilst::stash_polynomials
void stash_polynomials(scratch_programt &program, std::map< exprt, polynomialt > &polynomials, std::map< exprt, exprt > &stashed, patht &path)
Definition: acceleration_utils.cpp:190
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
polynomialt::coeff
int coeff(const exprt &expr)
Definition: polynomial.cpp:427
polynomialt::max_degree
int max_degree(const exprt &var)
Definition: polynomial.cpp:409
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:893
find_symbols.h
or_exprt
Boolean OR.
Definition: std_expr.h:2245
acceleration_utilst::expr2poly
bool expr2poly(exprt &expr, std::map< exprt, polynomialt > &polynomials, polynomialt &poly)
Definition: acceleration_utils.cpp:838
scratch_programt
Definition: scratch_program.h:37
goto_programt::output
std::ostream & output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
Output goto program to given stream.
Definition: goto_program.cpp:549
monomialt::coeff
int coeff
Definition: polynomial.h:31
monomialt
Definition: polynomial.h:21
forall_operands
#define forall_operands(it, expr)
Definition: expr.h:18
signed_poly_type
signedbv_typet signed_poly_type()
Definition: util.cpp:20
expr2c.h
expr2c
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:3878
polynomialt::mult
void mult(int scalar)
Definition: polynomial.cpp:253
scratch_programt::eval
exprt eval(const exprt &e)
Definition: scratch_program.cpp:77
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
nil_exprt
The NIL expression.
Definition: std_expr.h:3973
goto_symex.h
Symbolic Execution.
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
acceleration_utilst::precondition
exprt precondition(patht &path)
Definition: acceleration_utils.cpp:237
monomialt::termt::var
exprt var
Definition: polynomial.h:25
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
index_exprt::index
exprt & index()
Definition: std_expr.h:1319
expr_sett
std::unordered_set< exprt, irep_hash > expr_sett
Definition: cone_of_influence.h:21
acceleration_utilst::ensure_no_overflows
void ensure_no_overflows(scratch_programt &program)
Definition: acceleration_utils.cpp:467
acceleration_utilst::extract_polynomial
void extract_polynomial(scratch_programt &program, std::set< std::pair< expr_listt, exprt >> &coefficients, polynomialt &polynomial)
Definition: acceleration_utils.cpp:1212
index_exprt::array
exprt & array()
Definition: std_expr.h:1309
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
scratch_programt::assume
targett assume(const exprt &guard)
Definition: scratch_program.cpp:97
irept::id
const irep_idt & id() const
Definition: irep.h:418
acceleration_utilst::polynomial_array_assignmentst
std::vector< polynomial_array_assignmentt > polynomial_array_assignmentst
Definition: acceleration_utils.h:105
exprt::operandst
std::vector< exprt > operandst
Definition: expr.h:55
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
goto_check.h
Program Transformation.
overflow_instrumentert
Definition: overflow_instrumenter.h:26
std_code.h
acceleration_utilst::abstract_arrays
void abstract_arrays(exprt &expr, expr_mapt &abstractions)
Definition: acceleration_utils.cpp:290
minus_exprt
Binary minus.
Definition: std_expr.h:940
scratch_programt::append_path
void append_path(patht &path)
Definition: scratch_program.cpp:153
acceleration_utilst::array_assignments2polys
bool array_assignments2polys(expr_pairst &array_assignments, std::map< exprt, polynomialt > &polynomials, polynomial_array_assignmentst &array_polynomials, polynomialst &nondet_indices)
Definition: acceleration_utils.cpp:779
goto_program.h
Concrete Goto Program.
natural_loops_templatet< goto_programt, goto_programt::targett >::natural_loopt
parentt::loopt natural_loopt
Definition: natural_loops.h:52
source_locationt
Definition: source_location.h:20
simplify_expr.h
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1945
substitutiont
std::map< exprt, exprt > substitutiont
Definition: polynomial.h:39
acceleration_utilst::polynomial_array_assignmentt::index
polynomialt index
Definition: acceleration_utils.h:100
monomialt::termt
Definition: polynomial.h:24
symbol_table_baset::add
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
Definition: symbol_table_base.cpp:18
to_dereference_expr
const dereference_exprt & to_dereference_expr(const exprt &expr)
Cast an exprt to a dereference_exprt.
Definition: std_expr.h:2944
acceleration_utilst::gather_array_assignments
expr_pairst gather_array_assignments(goto_programt::instructionst &loop_body, expr_sett &arrays_written)
Definition: acceleration_utils.cpp:501
binding_exprt::where
exprt & where()
Definition: std_expr.h:4152
find_symbols_sett
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:22
polynomialt::to_expr
exprt to_expr()
Definition: polynomial.cpp:23
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
patht
std::list< path_nodet > patht
Definition: path.h:45
accelerator.h
Loop Acceleration.
to_not_expr
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Definition: std_expr.h:2868
polynomialt::substitute
void substitute(substitutiont &substitution)
Definition: polynomial.cpp:161
symbolt
Symbol table entry.
Definition: symbol.h:28
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
acceleration_utilst::polynomial_array_assignmentt::array
exprt array
Definition: acceleration_utils.h:99
replace_mapt
std::unordered_map< exprt, exprt, irep_hash > replace_mapt
Definition: replace_expr.h:22
binary2integer
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:120
cone_of_influence.h
Loop Acceleration.
acceleration_utilst::gather_array_accesses
void gather_array_accesses(const exprt &expr, expr_sett &arrays)
Definition: acceleration_utils.cpp:1193
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:725
polynomialst
std::vector< polynomialt > polynomialst
Definition: polynomial.h:63
acceleration_utilst::polynomial_array_assignmentt
Definition: acceleration_utils.h:98
goto_functions.h
Goto Programs with Functions.
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
acceleration_utilst::loop_counter
exprt & loop_counter
Definition: acceleration_utils.h:160
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
acceleration_utilst::polynomial_array_assignmentt::value
polynomialt value
Definition: acceleration_utils.h:101
implies_exprt
Boolean implication.
Definition: std_expr.h:2200
acceleration_utilst::stash_variables
void stash_variables(scratch_programt &program, expr_sett modified, substitutiont &substitution)
Definition: acceleration_utils.cpp:209
goto_programt::make_assumption
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:905
replace_expr.h
index_exprt
Array index operator.
Definition: std_expr.h:1293
scratch_programt::check_sat
bool check_sat(bool do_slice, guard_managert &guard_manager)
Definition: scratch_program.cpp:26
symbol_table.h
Author: Diffblue Ltd.
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
symbolt::module
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
binary_exprt::op1
exprt & op1()
Definition: expr.h:105
expr_mapt
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
Definition: acceleration_utils.h:33
std_expr.h
API to expression classes.
scratch_programt::assign
targett assign(const exprt &lhs, const exprt &rhs)
Definition: scratch_program.cpp:90
acceleration_utilst::gather_rvalues
void gather_rvalues(const exprt &expr, expr_sett &rvalues)
Definition: acceleration_utils.cpp:47
util.h
Loop Acceleration.
to_binary_relation_expr
const binary_relation_exprt & to_binary_relation_expr(const exprt &expr)
Cast an exprt to a binary_relation_exprt.
Definition: std_expr.h:774
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:3914
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
symbolt::name
irep_idt name
The unique identifier.
Definition: symbol.h:40
overflow_instrumentert::add_overflow_checks
void add_overflow_checks()
Definition: overflow_instrumenter.cpp:30
acceleration_utilst::ns
namespacet ns
Definition: acceleration_utils.h:158
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1196
wp.h
Weakest Preconditions.
binary_exprt::op0
exprt & op0()
Definition: expr.h:102
monomialt::terms
std::vector< termt > terms
Definition: polynomial.h:30
mod_exprt
Modulo.
Definition: std_expr.h:1100
not_exprt
Boolean negation.
Definition: std_expr.h:2843
acceleration_utilst::do_nonrecursive
bool do_nonrecursive(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, substitutiont &substitution, expr_sett &nonrecursive, scratch_programt &program)
Definition: acceleration_utils.cpp:868
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3939