cprover
disjunctive_polynomial_acceleration.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Loop Acceleration
4 
5 Author: Matt Lewis
6 
7 \*******************************************************************/
8 
11 
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>
26 
27 #include <goto-symex/goto_symex.h>
29 
30 #include <analyses/goto_check.h>
31 
32 #include <ansi-c/expr2c.h>
33 
34 #include <util/symbol_table.h>
35 #include <util/options.h>
36 #include <util/std_expr.h>
37 #include <util/std_code.h>
38 #include <util/find_symbols.h>
39 #include <util/simplify_expr.h>
40 #include <util/replace_expr.h>
41 #include <util/arith_tools.h>
42 
43 #include "polynomial_accelerator.h"
44 #include "accelerator.h"
45 #include "util.h"
46 #include "cone_of_influence.h"
47 #include "overflow_instrumenter.h"
48 
50  path_acceleratort &accelerator)
51 {
52  std::map<exprt, polynomialt> polynomials;
54 
55  accelerator.clear();
56 
57 #ifdef DEBUG
58  std::cout << "Polynomial accelerating program:\n";
59 
60  for(goto_programt::instructionst::iterator
61  it=goto_program.instructions.begin();
62  it!=goto_program.instructions.end();
63  ++it)
64  {
65  if(loop.contains(it))
66  {
67  goto_program.output_instruction(ns, "scratch", std::cout, *it);
68  }
69  }
70 
71  std::cout << "Modified:\n";
72 
73  for(expr_sett::iterator it=modified.begin();
74  it!=modified.end();
75  ++it)
76  {
77  std::cout << expr2c(*it, ns) << '\n';
78  }
79 #endif
80 
81  if(loop_counter.is_nil())
82  {
83  symbolt loop_sym=
84  utils.fresh_symbol("polynomial::loop_counter", unsigned_poly_type());
85  loop_counter=loop_sym.symbol_expr();
86  }
87 
88  patht &path=accelerator.path;
89  path.clear();
90 
91  if(!find_path(path))
92  {
93  // No more paths!
94  return false;
95  }
96 
97 #if 0
98  for(expr_sett::iterator it=modified.begin();
99  it!=modified.end();
100  ++it)
101  {
102  polynomialt poly;
103  exprt target=*it;
104 
105  if(it->type().id()==ID_bool)
106  {
107  // Hack: don't try to accelerate booleans.
108  continue;
109  }
110 
111  if(target.id()==ID_index ||
112  target.id()==ID_dereference)
113  {
114  // We'll handle this later.
115  continue;
116  }
117 
118  if(fit_polynomial(target, poly, path))
119  {
120  std::map<exprt, polynomialt> this_poly;
121  this_poly[target]=poly;
122 
123  if(utils.check_inductive(this_poly, path))
124  {
125 #ifdef DEBUG
126  std::cout << "Fitted a polynomial for " << expr2c(target, ns)
127  << '\n';
128 #endif
129  polynomials[target]=poly;
130  accelerator.changed_vars.insert(target);
131  break;
132  }
133  }
134  }
135 
136  if(polynomials.empty())
137  {
138  return false;
139  }
140 #endif
141 
142  // Fit polynomials for the other variables.
143  expr_sett dirty;
144  utils.find_modified(accelerator.path, dirty);
145  polynomial_acceleratort path_acceleration(
148 
149  for(patht::iterator it=accelerator.path.begin();
150  it!=accelerator.path.end();
151  ++it)
152  {
153  if(it->loc->is_assign() || it->loc->is_decl())
154  {
155  assigns.push_back(*(it->loc));
156  }
157  }
158 
159  for(expr_sett::iterator it=dirty.begin();
160  it!=dirty.end();
161  ++it)
162  {
163 #ifdef DEBUG
164  std::cout << "Trying to accelerate " << expr2c(*it, ns) << '\n';
165 #endif
166 
167  if(it->type().id()==ID_bool)
168  {
169  // Hack: don't try to accelerate booleans.
170  accelerator.dirty_vars.insert(*it);
171 #ifdef DEBUG
172  std::cout << "Ignoring boolean\n";
173 #endif
174  continue;
175  }
176 
177  if(it->id()==ID_index ||
178  it->id()==ID_dereference)
179  {
180 #ifdef DEBUG
181  std::cout << "Ignoring array reference\n";
182 #endif
183  continue;
184  }
185 
186  if(accelerator.changed_vars.find(*it)!=accelerator.changed_vars.end())
187  {
188  // We've accelerated variable this already.
189 #ifdef DEBUG
190  std::cout << "We've accelerated it already\n";
191 #endif
192  continue;
193  }
194 
195  // Hack: ignore variables that depend on array values..
196  exprt array_rhs;
197 
198  if(depends_on_array(*it, array_rhs))
199  {
200 #ifdef DEBUG
201  std::cout << "Ignoring because it depends on an array\n";
202 #endif
203  continue;
204  }
205 
206 
207  polynomialt poly;
208  exprt target(*it);
209 
210  if(path_acceleration.fit_polynomial(assigns, target, poly))
211  {
212  std::map<exprt, polynomialt> this_poly;
213  this_poly[target]=poly;
214 
215  if(utils.check_inductive(this_poly, accelerator.path, guard_manager))
216  {
217  polynomials[target]=poly;
218  accelerator.changed_vars.insert(target);
219  continue;
220  }
221  }
222 
223 #ifdef DEBUG
224  std::cout << "Failed to accelerate " << expr2c(*it, ns) << '\n';
225 #endif
226 
227  // We weren't able to accelerate this target...
228  accelerator.dirty_vars.insert(target);
229  }
230 
231 
232  #if 0
233  if(!utils.check_inductive(polynomials, assigns))
234  {
235  // They're not inductive :-(
236  return false;
237  }
238  #endif
239 
240  substitutiont stashed;
241  utils.stash_polynomials(program, polynomials, stashed, path);
242 
243  exprt guard;
244  bool path_is_monotone;
245 
246  try
247  {
248  path_is_monotone =
249  utils.do_assumptions(polynomials, path, guard, guard_manager);
250  }
251  catch(const std::string &s)
252  {
253  // Couldn't do WP.
254  std::cout << "Assumptions error: " << s << '\n';
255  return false;
256  }
257 
258  exprt pre_guard(guard);
259 
260  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
261  it!=polynomials.end();
262  ++it)
263  {
264  replace_expr(it->first, it->second.to_expr(), guard);
265  }
266 
267  if(path_is_monotone)
268  {
269  // OK cool -- the path is monotone, so we can just assume the condition for
270  // the last iteration.
271  replace_expr(
272  loop_counter,
274  guard);
275  }
276  else
277  {
278  // The path is not monotone, so we need to introduce a quantifier to ensure
279  // that the condition held for all 0 <= k < n.
280  symbolt k_sym=utils.fresh_symbol("polynomial::k", unsigned_poly_type());
281  const symbol_exprt k = k_sym.symbol_expr();
282 
283  const and_exprt k_bound(
284  binary_relation_exprt(from_integer(0, k.type()), ID_le, k),
286  replace_expr(loop_counter, k, guard);
287 
288  simplify(guard, ns);
289 
290  implies_exprt implies(k_bound, guard);
291 
292  guard = forall_exprt(k, implies);
293  }
294 
295  // All our conditions are met -- we can finally build the accelerator!
296  // It is of the form:
297  //
298  // loop_counter=*;
299  // target1=polynomial1;
300  // target2=polynomial2;
301  // ...
302  // assume(guard);
303  // assume(no overflows in previous code);
304 
305  program.add(goto_programt::make_assumption(pre_guard));
306  program.assign(
307  loop_counter,
309 
310  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
311  it!=polynomials.end();
312  ++it)
313  {
314  program.assign(it->first, it->second.to_expr());
315  accelerator.changed_vars.insert(it->first);
316  }
317 
318  // Add in any array assignments we can do now.
319  if(!utils.do_arrays(assigns, polynomials, stashed, program))
320  {
321  // We couldn't model some of the array assignments with polynomials...
322  // Unfortunately that means we just have to bail out.
323  return false;
324  }
325 
326  program.add(goto_programt::make_assumption(guard));
327  program.fix_types();
328 
329  if(path_is_monotone)
330  {
331  utils.ensure_no_overflows(program);
332  }
333 
334  accelerator.pure_accelerator.instructions.swap(program.instructions);
335 
336  return true;
337 }
338 
340 {
342 
343  program.append(fixed);
344  program.append(fixed);
345 
346  // Let's make sure that we get a path we have not seen before.
347  for(std::list<distinguish_valuest>::iterator it=accelerated_paths.begin();
348  it!=accelerated_paths.end();
349  ++it)
350  {
351  exprt new_path=false_exprt();
352 
353  for(distinguish_valuest::iterator jt=it->begin();
354  jt!=it->end();
355  ++jt)
356  {
357  exprt distinguisher=jt->first;
358  bool taken=jt->second;
359 
360  if(taken)
361  {
362  not_exprt negated(distinguisher);
363  distinguisher.swap(negated);
364  }
365 
366  or_exprt disjunct(new_path, distinguisher);
367  new_path.swap(disjunct);
368  }
369 
370  program.assume(new_path);
371  }
372 
374 
375  try
376  {
377  if(program.check_sat(guard_manager))
378  {
379 #ifdef DEBUG
380  std::cout << "Found a path\n";
381 #endif
382  build_path(program, path);
383  record_path(program);
384 
385  return true;
386  }
387  }
388  catch(const std::string &s)
389  {
390  std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
391  }
392  catch(const char *s)
393  {
394  std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
395  }
396 
397  return false;
398 }
399 
401  exprt &var,
402  polynomialt &polynomial,
403  patht &path)
404 {
405  // These are the variables that var depends on with respect to the body.
406  std::vector<expr_listt> parameters;
407  std::set<std::pair<expr_listt, exprt> > coefficients;
408  expr_listt exprs;
410  expr_sett influence;
411 
412  cone_of_influence(var, influence);
413 
414 #ifdef DEBUG
415  std::cout << "Fitting a polynomial for " << expr2c(var, ns)
416  << ", which depends on:\n";
417 
418  for(expr_sett::iterator it=influence.begin();
419  it!=influence.end();
420  ++it)
421  {
422  std::cout << expr2c(*it, ns) << '\n';
423  }
424 #endif
425 
426  for(expr_sett::iterator it=influence.begin();
427  it!=influence.end();
428  ++it)
429  {
430  if(it->id()==ID_index ||
431  it->id()==ID_dereference)
432  {
433  // Hack: don't accelerate anything that depends on an array
434  // yet...
435  return false;
436  }
437 
438  exprs.clear();
439 
440  exprs.push_back(*it);
441  parameters.push_back(exprs);
442 
443  exprs.push_back(loop_counter);
444  parameters.push_back(exprs);
445  }
446 
447  // N
448  exprs.clear();
449  exprs.push_back(loop_counter);
450  parameters.push_back(exprs);
451 
452  // N^2
453  exprs.push_back(loop_counter);
454  parameters.push_back(exprs);
455 
456  // Constant
457  exprs.clear();
458  parameters.push_back(exprs);
459 
460  for(std::vector<expr_listt>::iterator it=parameters.begin();
461  it!=parameters.end();
462  ++it)
463  {
464  symbolt coeff=utils.fresh_symbol("polynomial::coeff", signed_poly_type());
465  coefficients.insert(make_pair(*it, coeff.symbol_expr()));
466 
467  // XXX HACK HACK HACK
468  // I'm just constraining these coefficients to prevent overflows
469  // messing things up later... Should really do this properly
470  // somehow.
471  program.assume(
473  from_integer(-(1 << 10), signed_poly_type()),
474  ID_lt,
475  coeff.symbol_expr()));
476  program.assume(
478  coeff.symbol_expr(),
479  ID_lt,
480  from_integer(1 << 10, signed_poly_type())));
481  }
482 
483  // Build a set of values for all the parameters that allow us to fit a
484  // unique polynomial.
485 
486  std::map<exprt, exprt> ivals1;
487  std::map<exprt, exprt> ivals2;
488  std::map<exprt, exprt> ivals3;
489 
490  for(expr_sett::iterator it=influence.begin();
491  it!=influence.end();
492  ++it)
493  {
494  symbolt ival1=utils.fresh_symbol("polynomial::init",
495  it->type());
496  symbolt ival2=utils.fresh_symbol("polynomial::init",
497  it->type());
498  symbolt ival3=utils.fresh_symbol("polynomial::init",
499  it->type());
500 
501  program.assume(binary_relation_exprt(ival1.symbol_expr(), "<",
502  ival2.symbol_expr()));
503  program.assume(binary_relation_exprt(ival2.symbol_expr(), "<",
504  ival3.symbol_expr()));
505 
506 #if 0
507  if(it->type()==signedbv_typet())
508  {
509  program.assume(binary_relation_exprt(ival1.symbol_expr(), ">",
510  from_integer(-100, it->type())));
511  }
512  program.assume(binary_relation_exprt(ival1.symbol_expr(), "<",
513  from_integer(100, it->type())));
514 
515  if(it->type()==signedbv_typet())
516  {
517  program.assume(binary_relation_exprt(ival2.symbol_expr(), ">",
518  from_integer(-100, it->type())));
519  }
520  program.assume(binary_relation_exprt(ival2.symbol_expr(), "<",
521  from_integer(100, it->type())));
522 
523  if(it->type()==signedbv_typet())
524  {
525  program.assume(binary_relation_exprt(ival3.symbol_expr(), ">",
526  from_integer(-100, it->type())));
527  }
528  program.assume(binary_relation_exprt(ival3.symbol_expr(), "<",
529  from_integer(100, it->type())));
530 #endif
531 
532  ivals1[*it]=ival1.symbol_expr();
533  ivals2[*it]=ival2.symbol_expr();
534  ivals3[*it]=ival3.symbol_expr();
535 
536  // ivals1[*it]=from_integer(1, it->type());
537  }
538 
539  std::map<exprt, exprt> values;
540 
541  for(expr_sett::iterator it=influence.begin();
542  it!=influence.end();
543  ++it)
544  {
545  values[*it]=ivals1[*it];
546  }
547 
548  // Start building the program. Begin by decl'ing each of the
549  // master distinguishers.
550  for(std::list<symbol_exprt>::iterator it = distinguishers.begin();
551  it != distinguishers.end();
552  ++it)
553  {
554  program.add(goto_programt::make_decl(*it));
555  }
556 
557  // Now assume our polynomial fits at each of our sample points.
558  assert_for_values(program, values, coefficients, 1, fixed, var);
559 
560  for(int n=0; n <= 1; n++)
561  {
562  for(expr_sett::iterator it=influence.begin();
563  it!=influence.end();
564  ++it)
565  {
566  values[*it]=ivals2[*it];
567  assert_for_values(program, values, coefficients, n, fixed, var);
568 
569  values[*it]=ivals3[*it];
570  assert_for_values(program, values, coefficients, n, fixed, var);
571 
572  values[*it]=ivals1[*it];
573  }
574  }
575 
576  for(expr_sett::iterator it=influence.begin();
577  it!=influence.end();
578  ++it)
579  {
580  values[*it]=ivals3[*it];
581  }
582 
583  assert_for_values(program, values, coefficients, 0, fixed, var);
584  assert_for_values(program, values, coefficients, 1, fixed, var);
585  assert_for_values(program, values, coefficients, 2, fixed, var);
586 
587  // Let's make sure that we get a path we have not seen before.
588  for(std::list<distinguish_valuest>::iterator it=accelerated_paths.begin();
589  it!=accelerated_paths.end();
590  ++it)
591  {
592  exprt new_path=false_exprt();
593 
594  for(distinguish_valuest::iterator jt=it->begin();
595  jt!=it->end();
596  ++jt)
597  {
598  exprt distinguisher=jt->first;
599  bool taken=jt->second;
600 
601  if(taken)
602  {
603  not_exprt negated(distinguisher);
604  distinguisher.swap(negated);
605  }
606 
607  or_exprt disjunct(new_path, distinguisher);
608  new_path.swap(disjunct);
609  }
610 
611  program.assume(new_path);
612  }
613 
614  utils.ensure_no_overflows(program);
615 
616  // Now do an ASSERT(false) to grab a counterexample
618 
619  // If the path is satisfiable, we've fitted a polynomial. Extract the
620  // relevant coefficients and return the expression.
621  try
622  {
623  if(program.check_sat(guard_manager))
624  {
625 #ifdef DEBUG
626  std::cout << "Found a polynomial\n";
627 #endif
628 
629  utils.extract_polynomial(program, coefficients, polynomial);
630  build_path(program, path);
631  record_path(program);
632 
633  return true;
634  }
635  }
636  catch(const std::string &s)
637  {
638  std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
639  }
640  catch(const char *s)
641  {
642  std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
643  }
644 
645  return false;
646 }
647 
649  scratch_programt &program,
650  std::map<exprt, exprt> &values,
651  std::set<std::pair<expr_listt, exprt> > &coefficients,
652  int num_unwindings,
653  goto_programt &loop_body,
654  exprt &target)
655 {
656  // First figure out what the appropriate type for this expression is.
657  optionalt<typet> expr_type;
658 
659  for(std::map<exprt, exprt>::iterator it=values.begin();
660  it!=values.end();
661  ++it)
662  {
663  if(!expr_type.has_value())
664  {
665  expr_type=it->first.type();
666  }
667  else
668  {
669  expr_type = join_types(*expr_type, it->first.type());
670  }
671  }
672 
673  // Now set the initial values of the all the variables...
674  for(std::map<exprt, exprt>::iterator it=values.begin();
675  it!=values.end();
676  ++it)
677  {
678  program.assign(it->first, it->second);
679  }
680 
681  // Now unwind the loop as many times as we need to.
682  for(int i=0; i<num_unwindings; i++)
683  {
684  program.append(loop_body);
685  }
686 
687  // Now build the polynomial for this point and assert it fits.
688  exprt rhs=nil_exprt();
689 
690  for(std::set<std::pair<expr_listt, exprt> >::iterator it=coefficients.begin();
691  it!=coefficients.end();
692  ++it)
693  {
694  exprt concrete_value = from_integer(1, *expr_type);
695 
696  for(expr_listt::const_iterator e_it=it->first.begin();
697  e_it!=it->first.end();
698  ++e_it)
699  {
700  exprt e=*e_it;
701 
702  if(e==loop_counter)
703  {
704  mult_exprt mult(
705  from_integer(num_unwindings, *expr_type), concrete_value);
706  mult.swap(concrete_value);
707  }
708  else
709  {
710  std::map<exprt, exprt>::iterator v_it=values.find(e);
711 
712  PRECONDITION(v_it!=values.end());
713 
714  mult_exprt mult(concrete_value, v_it->second);
715  mult.swap(concrete_value);
716  }
717  }
718 
719  // OK, concrete_value now contains the value of all the relevant variables
720  // multiplied together. Create the term concrete_value*coefficient and add
721  // it into the polynomial.
722  typecast_exprt cast(it->second, *expr_type);
723  const mult_exprt term(concrete_value, cast);
724 
725  if(rhs.is_nil())
726  {
727  rhs=term;
728  }
729  else
730  {
731  rhs=plus_exprt(rhs, term);
732  }
733  }
734 
735  rhs=typecast_exprt(rhs, target.type());
736 
737  // We now have the RHS of the polynomial. Assert that this is equal to the
738  // actual value of the variable we're fitting.
739  const equal_exprt polynomial_holds(target, rhs);
740 
741  // Finally, assert that the polynomial equals the variable we're fitting.
742  program.add(goto_programt::make_assumption(polynomial_holds));
743 }
744 
746  const exprt &target,
747  expr_sett &cone)
748 {
750  influence.cone_of_influence(target, cone);
751 }
752 
754 {
755  for(const auto &loop_instruction : loop)
756  {
757  const auto succs = goto_program.get_successors(loop_instruction);
758 
759  if(succs.size() > 1)
760  {
761  // This location has multiple successors -- each successor is a
762  // distinguishing point.
763  for(const auto &jt : succs)
764  {
765  symbolt distinguisher_sym =
766  utils.fresh_symbol("polynomial::distinguisher", bool_typet());
767  symbol_exprt distinguisher=distinguisher_sym.symbol_expr();
768 
769  distinguishing_points[jt]=distinguisher;
770  distinguishers.push_back(distinguisher);
771  }
772  }
773  }
774 }
775 
777  scratch_programt &scratch_program, patht &path)
778 {
780 
781  do
782  {
784 
785  const auto succs=goto_program.get_successors(t);
786 
787  INVARIANT(succs.size() > 0,
788  "we should have a looping path, so we should never hit a location "
789  "with no successors.");
790 
791  if(succs.size()==1)
792  {
793  // Only one successor -- accumulate it and move on.
794  path.push_back(path_nodet(t));
795  t=succs.front();
796  continue;
797  }
798 
799  // We have multiple successors. Examine the distinguisher variables
800  // to see which branch was taken.
801  bool found_branch=false;
802 
803  for(const auto &succ : succs)
804  {
805  exprt &distinguisher=distinguishing_points[succ];
806  bool taken=scratch_program.eval(distinguisher).is_true();
807 
808  if(taken)
809  {
810  if(!found_branch ||
811  (succ->location_number < next->location_number))
812  {
813  next=succ;
814  }
815 
816  found_branch=true;
817  }
818  }
819 
820  PRECONDITION(found_branch);
821 
822  exprt cond=nil_exprt();
823 
824  if(t->is_goto())
825  {
826  // If this was a conditional branch (it probably was), figure out
827  // if we hit the "taken" or "not taken" branch & accumulate the
828  // appropriate guard.
829  cond = not_exprt(t->get_condition());
830 
831  for(goto_programt::targetst::iterator it=t->targets.begin();
832  it!=t->targets.end();
833  ++it)
834  {
835  if(next==*it)
836  {
837  cond = t->get_condition();
838  break;
839  }
840  }
841  }
842 
843  path.push_back(path_nodet(t, cond));
844 
845  t=next;
846  } while(t != loop_header && loop.contains(t));
847 }
848 
849 /*
850  * Take the body of the loop we are accelerating and produce a fixed-path
851  * version of that body, suitable for use in the fixed-path acceleration we
852  * will be doing later.
853  */
855 {
857  std::map<exprt, exprt> shadow_distinguishers;
858 
860 
862  {
863  if(it->is_assert())
864  {
865  it->type=ASSUME;
866  }
867  }
868 
869  // We're only interested in paths that loop back to the loop header.
870  // As such, any path that jumps outside of the loop or jumps backwards
871  // to a location other than the loop header (i.e. a nested loop) is not
872  // one we're interested in, and we'll redirect it to this assume(false).
875 
876  // Make a sentinel instruction to mark the end of the loop body.
877  // We'll use this as the new target for any back-jumps to the loop
878  // header.
880 
881  // A pointer to the start of the fixed-path body. We'll be using this to
882  // iterate over the fixed-path body, but for now it's just a pointer to the
883  // first instruction.
885 
886  // Create shadow distinguisher variables. These guys identify the path that
887  // is taken through the fixed-path body.
888  for(std::list<symbol_exprt>::iterator it = distinguishers.begin();
889  it != distinguishers.end();
890  ++it)
891  {
892  exprt &distinguisher=*it;
893  symbolt shadow_sym=utils.fresh_symbol("polynomial::shadow_distinguisher",
894  bool_typet());
895  exprt shadow=shadow_sym.symbol_expr();
896  shadow_distinguishers[distinguisher]=shadow;
897 
899  fixedt,
901  }
902 
903  // We're going to iterate over the 2 programs in lockstep, which allows
904  // us to figure out which distinguishing point we've hit & instrument
905  // the relevant distinguisher variables.
907  t!=goto_program.instructions.end();
908  ++t, ++fixedt)
909  {
910  distinguish_mapt::iterator d=distinguishing_points.find(t);
911 
912  if(!loop.contains(t))
913  {
914  // This instruction isn't part of the loop... Just remove it.
915  fixedt->turn_into_skip();
916  continue;
917  }
918 
919  if(d!=distinguishing_points.end())
920  {
921  // We've hit a distinguishing point. Set the relevant shadow
922  // distinguisher to true.
923  exprt &distinguisher=d->second;
924  exprt &shadow=shadow_distinguishers[distinguisher];
925 
927  fixedt,
929 
930  assign->swap(*fixedt);
931  fixedt=assign;
932  }
933 
934  if(t->is_goto())
935  {
936  PRECONDITION(fixedt->is_goto());
937  // If this is a forwards jump, it's either jumping inside the loop
938  // (in which case we leave it alone), or it jumps outside the loop.
939  // If it jumps out of the loop, it's on a path we don't care about
940  // so we kill it.
941  //
942  // Otherwise, it's a backwards jump. If it jumps back to the loop
943  // header we're happy & redirect it to our end-of-body sentinel.
944  // If it jumps somewhere else, it's part of a nested loop and we
945  // kill it.
946  for(const auto &target : t->targets)
947  {
948  if(target->location_number > t->location_number)
949  {
950  // A forward jump...
951  if(loop.contains(target))
952  {
953  // Case 1: a forward jump within the loop. Do nothing.
954  continue;
955  }
956  else
957  {
958  // Case 2: a forward jump out of the loop. Kill.
959  fixedt->targets.clear();
960  fixedt->targets.push_back(kill);
961  }
962  }
963  else
964  {
965  // A backwards jump...
966  if(target==loop_header)
967  {
968  // Case 3: a backwards jump to the loop header. Redirect
969  // to sentinel.
970  fixedt->targets.clear();
971  fixedt->targets.push_back(end);
972  }
973  else
974  {
975  // Case 4: a nested loop. Kill.
976  fixedt->targets.clear();
977  fixedt->targets.push_back(kill);
978  }
979  }
980  }
981  }
982  }
983 
984  // OK, now let's assume that the path we took through the fixed-path
985  // body is the same as the master path. We do this by assuming that
986  // each of the shadow-distinguisher variables is equal to its corresponding
987  // master-distinguisher.
988  for(const auto &expr : distinguishers)
989  {
990  const exprt &shadow=shadow_distinguishers[expr];
991 
993  end, goto_programt::make_assumption(equal_exprt(expr, shadow)));
994  }
995 
996  // Finally, let's remove all the skips we introduced and fix the
997  // jump targets.
998  fixed.update();
1000 }
1001 
1003  scratch_programt &program)
1004 {
1005  distinguish_valuest path_val;
1006 
1007  for(std::list<symbol_exprt>::iterator it = distinguishers.begin();
1008  it != distinguishers.end();
1009  ++it)
1010  {
1011  path_val[*it]=program.eval(*it).is_true();
1012  }
1013 
1014  accelerated_paths.push_back(path_val);
1015 }
1016 
1018  const exprt &e,
1019  exprt &array)
1020 {
1021  expr_sett influence;
1022 
1023  cone_of_influence(e, influence);
1024 
1025  for(expr_sett::iterator it=influence.begin();
1026  it!=influence.end();
1027  ++it)
1028  {
1029  if(it->id()==ID_index ||
1030  it->id()==ID_dereference)
1031  {
1032  array=*it;
1033  return true;
1034  }
1035  }
1036 
1037  return false;
1038 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1201
symex_target_equation.h
Generate Equation using Symbolic Execution.
overflow_instrumenter.h
Loop Acceleration.
path_acceleratort::changed_vars
std::set< exprt > changed_vars
Definition: accelerator.h:65
polynomialt
Definition: polynomial.h:42
disjunctive_polynomial_accelerationt::utils
acceleration_utilst utils
Definition: disjunctive_polynomial_acceleration.h:101
disjunctive_polynomial_accelerationt::build_path
void build_path(scratch_programt &scratch_program, patht &path)
Definition: disjunctive_polynomial_acceleration.cpp:776
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
disjunctive_polynomial_accelerationt::distinguish_valuest
std::map< exprt, bool > distinguish_valuest
Definition: disjunctive_polynomial_acceleration.h:99
forall_exprt
A forall expression.
Definition: mathematical_expr.h:341
polynomial_acceleratort::fit_polynomial
bool fit_polynomial(goto_programt::instructionst &loop_body, exprt &target, polynomialt &polynomial)
Definition: polynomial_accelerator.cpp:434
acceleration_utilst::fresh_symbol
symbolt fresh_symbol(std::string base, typet type)
Definition: acceleration_utils.cpp:1261
disjunctive_polynomial_accelerationt::goto_functions
goto_functionst & goto_functions
Definition: disjunctive_polynomial_acceleration.h:92
expr_listt
std::list< exprt > expr_listt
Definition: acceleration_utils.h:34
goto_programt::instructionst
std::list< instructiont > instructionst
Definition: goto_program.h:577
disjunctive_polynomial_accelerationt::find_path
bool find_path(patht &path)
Definition: disjunctive_polynomial_acceleration.cpp:339
remove_skip
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:85
goto_programt::update
void update()
Update all indices.
Definition: goto_program.cpp:541
goto_programt::copy_from
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
Definition: goto_program.cpp:626
disjunctive_polynomial_accelerationt::goto_program
goto_programt & goto_program
Definition: disjunctive_polynomial_acceleration.h:93
cone_of_influencet::cone_of_influence
void cone_of_influence(const expr_sett &targets, expr_sett &cone)
Definition: cone_of_influence.cpp:18
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
disjunctive_polynomial_accelerationt::find_distinguishing_points
void find_distinguishing_points()
Definition: disjunctive_polynomial_acceleration.cpp:753
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
disjunctive_polynomial_accelerationt::message_handler
message_handlert & message_handler
Definition: disjunctive_polynomial_acceleration.h:70
disjunctive_polynomial_accelerationt::assert_for_values
void assert_for_values(scratch_programt &program, std::map< exprt, exprt > &values, std::set< std::pair< expr_listt, exprt > > &coefficients, int num_unwindings, goto_programt &loop_body, exprt &target)
Definition: disjunctive_polynomial_acceleration.cpp:648
exprt
Base class for all expressions.
Definition: expr.h:53
path_nodet
Definition: path.h:24
options.h
Options.
bool_typet
The Boolean type.
Definition: std_types.h:37
goto_programt::get_successors
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
Definition: goto_program.h:1084
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:92
acceleration_utilst::check_inductive
bool check_inductive(std::map< exprt, polynomialt > polynomials, patht &path, guard_managert &guard_manager)
Definition: acceleration_utils.cpp:113
path_acceleratort::dirty_vars
std::set< exprt > dirty_vars
Definition: accelerator.h:66
symbol_exprt
Expression to hold a symbol (variable)
Definition: std_expr.h:82
goto_programt::make_decl
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:920
equal_exprt
Equality.
Definition: std_expr.h:1190
scratch_programt::append
void append(goto_programt::instructionst &instructions)
Definition: scratch_program.cpp:82
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
acceleration_utilst::find_modified
void find_modified(const patht &path, expr_sett &modified)
Definition: acceleration_utils.cpp:86
path_acceleratort::clear
void clear()
Definition: accelerator.h:53
cone_of_influencet
Definition: cone_of_influence.h:28
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
goto_programt::insert_before
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:639
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
disjunctive_polynomial_accelerationt::loop_header
goto_programt::targett loop_header
Definition: disjunctive_polynomial_acceleration.h:96
or_exprt
Boolean OR.
Definition: std_expr.h:2245
disjunctive_polynomial_accelerationt::loop_counter
exprt loop_counter
Definition: disjunctive_polynomial_acceleration.h:102
scratch_programt
Definition: scratch_program.h:37
goto_programt::output_instruction
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
Definition: goto_program.cpp:41
goto_programt::make_skip
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:851
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
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:464
scratch_programt::eval
exprt eval(const exprt &e)
Definition: scratch_program.cpp:77
nil_exprt
The NIL expression.
Definition: std_expr.h:3973
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: std_types.h:1265
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
disjunctive_polynomial_accelerationt::modified
expr_sett modified
Definition: disjunctive_polynomial_acceleration.h:105
path_acceleratort::path
patht path
Definition: accelerator.h:62
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2693
disjunctive_polynomial_accelerationt::symbol_table
symbol_tablet & symbol_table
Definition: disjunctive_polynomial_acceleration.h:90
path_acceleratort
Definition: accelerator.h:27
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:986
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
irept::swap
void swap(irept &irep)
Definition: irep.h:463
path_acceleratort::pure_accelerator
goto_programt pure_accelerator
Definition: accelerator.h:63
irept::is_nil
bool is_nil() const
Definition: irep.h:398
irept::id
const irep_idt & id() const
Definition: irep.h:418
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
disjunctive_polynomial_accelerationt::accelerate
bool accelerate(path_acceleratort &accelerator)
Definition: disjunctive_polynomial_acceleration.cpp:49
goto_check.h
Program Transformation.
disjunctive_polynomial_accelerationt::loop
natural_loops_mutablet::natural_loopt & loop
Definition: disjunctive_polynomial_acceleration.h:95
std_code.h
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
disjunctive_polynomial_accelerationt::distinguishing_points
distinguish_mapt distinguishing_points
Definition: disjunctive_polynomial_acceleration.h:103
disjunctive_polynomial_accelerationt::guard_manager
guard_managert & guard_manager
Definition: disjunctive_polynomial_acceleration.h:94
minus_exprt
Binary minus.
Definition: std_expr.h:940
goto_program.h
Concrete Goto Program.
disjunctive_polynomial_accelerationt::ns
namespacet ns
Definition: disjunctive_polynomial_acceleration.h:91
join_types
typet join_types(const typet &t1, const typet &t2)
Return the smallest type that both t1 and t2 can be cast to without losing information.
Definition: util.cpp:70
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
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
disjunctive_polynomial_accelerationt::build_fixed
void build_fixed()
Definition: disjunctive_polynomial_acceleration.cpp:854
disjunctive_polynomial_accelerationt::depends_on_array
bool depends_on_array(const exprt &e, exprt &array)
Definition: disjunctive_polynomial_acceleration.cpp:1017
patht
std::list< path_nodet > patht
Definition: path.h:45
accelerator.h
Loop Acceleration.
disjunctive_polynomial_accelerationt::fixed
goto_programt fixed
Definition: disjunctive_polynomial_acceleration.h:106
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
ASSUME
@ ASSUME
Definition: goto_program.h:35
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
cone_of_influence.h
Loop Acceleration.
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:725
polynomial_acceleratort
Definition: polynomial_accelerator.h:32
disjunctive_polynomial_accelerationt::fit_polynomial
bool fit_polynomial(exprt &target, polynomialt &polynomial, patht &path)
Definition: disjunctive_polynomial_acceleration.cpp:400
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
disjunctive_polynomial_accelerationt::record_path
void record_path(scratch_programt &scratch_program)
Definition: disjunctive_polynomial_acceleration.cpp:1002
goto_programt::insert_after
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:655
disjunctive_polynomial_accelerationt::distinguishers
std::list< symbol_exprt > distinguishers
Definition: disjunctive_polynomial_acceleration.h:104
implies_exprt
Boolean implication.
Definition: std_expr.h:2200
disjunctive_polynomial_acceleration.h
Loop Acceleration.
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
disjunctive_polynomial_accelerationt::accelerated_paths
std::list< distinguish_valuest > accelerated_paths
Definition: disjunctive_polynomial_acceleration.h:107
symbol_table.h
Author: Diffblue Ltd.
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
remove_skip.h
Program Transformation.
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:295
true_exprt
The Boolean constant true.
Definition: std_expr.h:3955
std_expr.h
API to expression classes.
scratch_programt::assign
targett assign(const exprt &lhs, const exprt &rhs)
Definition: scratch_program.cpp:90
util.h
Loop Acceleration.
disjunctive_polynomial_accelerationt::cone_of_influence
void cone_of_influence(const exprt &target, expr_sett &cone)
Definition: disjunctive_polynomial_acceleration.cpp:745
polynomial_accelerator.h
Loop Acceleration.
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
wp.h
Weakest Preconditions.
validation_modet::INVARIANT
@ INVARIANT
loop_templatet::contains
virtual bool contains(const T instruction) const
Returns true if instruction is in this loop.
Definition: loop_analysis.h:40
not_exprt
Boolean negation.
Definition: std_expr.h:2843