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