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.find(it)!=loop.end())
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))
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=utils.do_assumptions(polynomials, path, guard);
249  }
250  catch(const std::string &s)
251  {
252  // Couldn't do WP.
253  std::cout << "Assumptions error: " << s << '\n';
254  return false;
255  }
256 
257  exprt pre_guard(guard);
258 
259  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
260  it!=polynomials.end();
261  ++it)
262  {
263  replace_expr(it->first, it->second.to_expr(), guard);
264  }
265 
266  if(path_is_monotone)
267  {
268  // OK cool -- the path is monotone, so we can just assume the condition for
269  // the last iteration.
270  replace_expr(
271  loop_counter,
273  guard);
274  }
275  else
276  {
277  // The path is not monotone, so we need to introduce a quantifier to ensure
278  // that the condition held for all 0 <= k < n.
279  symbolt k_sym=utils.fresh_symbol("polynomial::k", unsigned_poly_type());
280  const symbol_exprt k = k_sym.symbol_expr();
281 
282  const and_exprt k_bound(
283  binary_relation_exprt(from_integer(0, k.type()), ID_le, k),
285  replace_expr(loop_counter, k, guard);
286 
287  simplify(guard, ns);
288 
289  implies_exprt implies(k_bound, guard);
290 
291  guard = forall_exprt(k, implies);
292  }
293 
294  // All our conditions are met -- we can finally build the accelerator!
295  // It is of the form:
296  //
297  // loop_counter=*;
298  // target1=polynomial1;
299  // target2=polynomial2;
300  // ...
301  // assume(guard);
302  // assume(no overflows in previous code);
303 
304  program.add_instruction(ASSUME)->guard=pre_guard;
306 
307  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
308  it!=polynomials.end();
309  ++it)
310  {
311  program.assign(it->first, it->second.to_expr());
312  accelerator.changed_vars.insert(it->first);
313  }
314 
315  // Add in any array assignments we can do now.
316  if(!utils.do_arrays(assigns, polynomials, loop_counter, stashed, program))
317  {
318  // We couldn't model some of the array assignments with polynomials...
319  // Unfortunately that means we just have to bail out.
320  return false;
321  }
322 
323  program.add_instruction(ASSUME)->guard=guard;
324  program.fix_types();
325 
326  if(path_is_monotone)
327  {
328  utils.ensure_no_overflows(program);
329  }
330 
331  accelerator.pure_accelerator.instructions.swap(program.instructions);
332 
333  return true;
334 }
335 
337 {
339 
340  program.append(fixed);
341  program.append(fixed);
342 
343  // Let's make sure that we get a path we have not seen before.
344  for(std::list<distinguish_valuest>::iterator it=accelerated_paths.begin();
345  it!=accelerated_paths.end();
346  ++it)
347  {
348  exprt new_path=false_exprt();
349 
350  for(distinguish_valuest::iterator jt=it->begin();
351  jt!=it->end();
352  ++jt)
353  {
354  exprt distinguisher=jt->first;
355  bool taken=jt->second;
356 
357  if(taken)
358  {
359  not_exprt negated(distinguisher);
360  distinguisher.swap(negated);
361  }
362 
363  or_exprt disjunct(new_path, distinguisher);
364  new_path.swap(disjunct);
365  }
366 
367  program.assume(new_path);
368  }
369 
370  program.add_instruction(ASSERT)->guard=false_exprt();
371 
372  try
373  {
374  if(program.check_sat())
375  {
376 #ifdef DEBUG
377  std::cout << "Found a path\n";
378 #endif
379  build_path(program, path);
380  record_path(program);
381 
382  return true;
383  }
384  }
385  catch(const std::string &s)
386  {
387  std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
388  }
389  catch(const char *s)
390  {
391  std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
392  }
393 
394  return false;
395 }
396 
398  exprt &var,
399  polynomialt &polynomial,
400  patht &path)
401 {
402  // These are the variables that var depends on with respect to the body.
403  std::vector<expr_listt> parameters;
404  std::set<std::pair<expr_listt, exprt> > coefficients;
405  expr_listt exprs;
407  expr_sett influence;
408 
409  cone_of_influence(var, influence);
410 
411 #ifdef DEBUG
412  std::cout << "Fitting a polynomial for " << expr2c(var, ns)
413  << ", which depends on:\n";
414 
415  for(expr_sett::iterator it=influence.begin();
416  it!=influence.end();
417  ++it)
418  {
419  std::cout << expr2c(*it, ns) << '\n';
420  }
421 #endif
422 
423  for(expr_sett::iterator it=influence.begin();
424  it!=influence.end();
425  ++it)
426  {
427  if(it->id()==ID_index ||
428  it->id()==ID_dereference)
429  {
430  // Hack: don't accelerate anything that depends on an array
431  // yet...
432  return false;
433  }
434 
435  exprs.clear();
436 
437  exprs.push_back(*it);
438  parameters.push_back(exprs);
439 
440  exprs.push_back(loop_counter);
441  parameters.push_back(exprs);
442  }
443 
444  // N
445  exprs.clear();
446  exprs.push_back(loop_counter);
447  parameters.push_back(exprs);
448 
449  // N^2
450  exprs.push_back(loop_counter);
451  parameters.push_back(exprs);
452 
453  // Constant
454  exprs.clear();
455  parameters.push_back(exprs);
456 
457  for(std::vector<expr_listt>::iterator it=parameters.begin();
458  it!=parameters.end();
459  ++it)
460  {
461  symbolt coeff=utils.fresh_symbol("polynomial::coeff", signed_poly_type());
462  coefficients.insert(make_pair(*it, coeff.symbol_expr()));
463 
464  // XXX HACK HACK HACK
465  // I'm just constraining these coefficients to prevent overflows
466  // messing things up later... Should really do this properly
467  // somehow.
468  program.assume(
470  from_integer(-(1 << 10), signed_poly_type()),
471  ID_lt,
472  coeff.symbol_expr()));
473  program.assume(
475  coeff.symbol_expr(),
476  ID_lt,
477  from_integer(1 << 10, signed_poly_type())));
478  }
479 
480  // Build a set of values for all the parameters that allow us to fit a
481  // unique polynomial.
482 
483  std::map<exprt, exprt> ivals1;
484  std::map<exprt, exprt> ivals2;
485  std::map<exprt, exprt> ivals3;
486 
487  for(expr_sett::iterator it=influence.begin();
488  it!=influence.end();
489  ++it)
490  {
491  symbolt ival1=utils.fresh_symbol("polynomial::init",
492  it->type());
493  symbolt ival2=utils.fresh_symbol("polynomial::init",
494  it->type());
495  symbolt ival3=utils.fresh_symbol("polynomial::init",
496  it->type());
497 
498  program.assume(binary_relation_exprt(ival1.symbol_expr(), "<",
499  ival2.symbol_expr()));
500  program.assume(binary_relation_exprt(ival2.symbol_expr(), "<",
501  ival3.symbol_expr()));
502 
503 #if 0
504  if(it->type()==signedbv_typet())
505  {
506  program.assume(binary_relation_exprt(ival1.symbol_expr(), ">",
507  from_integer(-100, it->type())));
508  }
509  program.assume(binary_relation_exprt(ival1.symbol_expr(), "<",
510  from_integer(100, it->type())));
511 
512  if(it->type()==signedbv_typet())
513  {
514  program.assume(binary_relation_exprt(ival2.symbol_expr(), ">",
515  from_integer(-100, it->type())));
516  }
517  program.assume(binary_relation_exprt(ival2.symbol_expr(), "<",
518  from_integer(100, it->type())));
519 
520  if(it->type()==signedbv_typet())
521  {
522  program.assume(binary_relation_exprt(ival3.symbol_expr(), ">",
523  from_integer(-100, it->type())));
524  }
525  program.assume(binary_relation_exprt(ival3.symbol_expr(), "<",
526  from_integer(100, it->type())));
527 #endif
528 
529  ivals1[*it]=ival1.symbol_expr();
530  ivals2[*it]=ival2.symbol_expr();
531  ivals3[*it]=ival3.symbol_expr();
532 
533  // ivals1[*it]=from_integer(1, it->type());
534  }
535 
536  std::map<exprt, exprt> values;
537 
538  for(expr_sett::iterator it=influence.begin();
539  it!=influence.end();
540  ++it)
541  {
542  values[*it]=ivals1[*it];
543  }
544 
545  // Start building the program. Begin by decl'ing each of the
546  // master distinguishers.
547  for(std::list<exprt>::iterator it=distinguishers.begin();
548  it!=distinguishers.end();
549  ++it)
550  {
551  program.add_instruction(DECL)->code=code_declt(*it);
552  }
553 
554  // Now assume our polynomial fits at each of our sample points.
555  assert_for_values(program, values, coefficients, 1, fixed, var);
556 
557  for(int n=0; n <= 1; n++)
558  {
559  for(expr_sett::iterator it=influence.begin();
560  it!=influence.end();
561  ++it)
562  {
563  values[*it]=ivals2[*it];
564  assert_for_values(program, values, coefficients, n, fixed, var);
565 
566  values[*it]=ivals3[*it];
567  assert_for_values(program, values, coefficients, n, fixed, var);
568 
569  values[*it]=ivals1[*it];
570  }
571  }
572 
573  for(expr_sett::iterator it=influence.begin();
574  it!=influence.end();
575  ++it)
576  {
577  values[*it]=ivals3[*it];
578  }
579 
580  assert_for_values(program, values, coefficients, 0, fixed, var);
581  assert_for_values(program, values, coefficients, 1, fixed, var);
582  assert_for_values(program, values, coefficients, 2, fixed, var);
583 
584  // Let's make sure that we get a path we have not seen before.
585  for(std::list<distinguish_valuest>::iterator it=accelerated_paths.begin();
586  it!=accelerated_paths.end();
587  ++it)
588  {
589  exprt new_path=false_exprt();
590 
591  for(distinguish_valuest::iterator jt=it->begin();
592  jt!=it->end();
593  ++jt)
594  {
595  exprt distinguisher=jt->first;
596  bool taken=jt->second;
597 
598  if(taken)
599  {
600  not_exprt negated(distinguisher);
601  distinguisher.swap(negated);
602  }
603 
604  or_exprt disjunct(new_path, distinguisher);
605  new_path.swap(disjunct);
606  }
607 
608  program.assume(new_path);
609  }
610 
611  utils.ensure_no_overflows(program);
612 
613  // Now do an ASSERT(false) to grab a counterexample
614  program.add_instruction(ASSERT)->guard=false_exprt();
615 
616  // If the path is satisfiable, we've fitted a polynomial. Extract the
617  // relevant coefficients and return the expression.
618  try
619  {
620  if(program.check_sat())
621  {
622 #ifdef DEBUG
623  std::cout << "Found a polynomial\n";
624 #endif
625 
626  utils.extract_polynomial(program, coefficients, polynomial);
627  build_path(program, path);
628  record_path(program);
629 
630  return true;
631  }
632  }
633  catch(const std::string &s)
634  {
635  std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
636  }
637  catch(const char *s)
638  {
639  std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
640  }
641 
642  return false;
643 }
644 
646  scratch_programt &program,
647  std::map<exprt, exprt> &values,
648  std::set<std::pair<expr_listt, exprt> > &coefficients,
649  int num_unwindings,
650  goto_programt &loop_body,
651  exprt &target)
652 {
653  // First figure out what the appropriate type for this expression is.
654  typet expr_type=nil_typet();
655 
656  for(std::map<exprt, exprt>::iterator it=values.begin();
657  it!=values.end();
658  ++it)
659  {
660  if(expr_type==nil_typet())
661  {
662  expr_type=it->first.type();
663  }
664  else
665  {
666  expr_type=join_types(expr_type, it->first.type());
667  }
668  }
669 
670  // Now set the initial values of the all the variables...
671  for(std::map<exprt, exprt>::iterator it=values.begin();
672  it!=values.end();
673  ++it)
674  {
675  program.assign(it->first, it->second);
676  }
677 
678  // Now unwind the loop as many times as we need to.
679  for(int i=0; i<num_unwindings; i++)
680  {
681  program.append(loop_body);
682  }
683 
684  // Now build the polynomial for this point and assert it fits.
685  exprt rhs=nil_exprt();
686 
687  for(std::set<std::pair<expr_listt, exprt> >::iterator it=coefficients.begin();
688  it!=coefficients.end();
689  ++it)
690  {
691  exprt concrete_value=from_integer(1, expr_type);
692 
693  for(expr_listt::const_iterator e_it=it->first.begin();
694  e_it!=it->first.end();
695  ++e_it)
696  {
697  exprt e=*e_it;
698 
699  if(e==loop_counter)
700  {
701  mult_exprt mult(
702  from_integer(num_unwindings, expr_type), concrete_value);
703  mult.swap(concrete_value);
704  }
705  else
706  {
707  std::map<exprt, exprt>::iterator v_it=values.find(e);
708 
709  PRECONDITION(v_it!=values.end());
710 
711  mult_exprt mult(concrete_value, v_it->second);
712  mult.swap(concrete_value);
713  }
714  }
715 
716  // OK, concrete_value now contains the value of all the relevant variables
717  // multiplied together. Create the term concrete_value*coefficient and add
718  // it into the polynomial.
719  typecast_exprt cast(it->second, expr_type);
720  const mult_exprt term(concrete_value, cast);
721 
722  if(rhs.is_nil())
723  {
724  rhs=term;
725  }
726  else
727  {
728  rhs=plus_exprt(rhs, term);
729  }
730  }
731 
732  rhs=typecast_exprt(rhs, target.type());
733 
734  // We now have the RHS of the polynomial. Assert that this is equal to the
735  // actual value of the variable we're fitting.
736  const equal_exprt polynomial_holds(target, rhs);
737 
738  // Finally, assert that the polynomial equals the variable we're fitting.
739  goto_programt::targett assumption=program.add_instruction(ASSUME);
740  assumption->guard=polynomial_holds;
741 }
742 
744  const exprt &target,
745  expr_sett &cone)
746 {
748  influence.cone_of_influence(target, cone);
749 }
750 
752 {
753  for(natural_loops_mutablet::natural_loopt::iterator it=loop.begin();
754  it!=loop.end();
755  ++it)
756  {
757  const auto succs=goto_program.get_successors(*it);
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->guard);
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->guard;
838  break;
839  }
840  }
841  }
842 
843  path.push_back(path_nodet(t, cond));
844 
845  t=next;
846  }
847  while(t!=loop_header && (loop.find(t)!=loop.end()));
848 }
849 
850 /*
851  * Take the body of the loop we are accelerating and produce a fixed-path
852  * version of that body, suitable for use in the fixed-path acceleration we
853  * will be doing later.
854  */
856 {
858  std::map<exprt, exprt> shadow_distinguishers;
859 
861 
863  {
864  if(it->is_assert())
865  {
866  it->type=ASSUME;
867  }
868  }
869 
870  // We're only interested in paths that loop back to the loop header.
871  // As such, any path that jumps outside of the loop or jumps backwards
872  // to a location other than the loop header (i.e. a nested loop) is not
873  // one we're interested in, and we'll redirect it to this assume(false).
875  kill->guard=false_exprt();
876 
877  // Make a sentinel instruction to mark the end of the loop body.
878  // We'll use this as the new target for any back-jumps to the loop
879  // header.
881 
882  // A pointer to the start of the fixed-path body. We'll be using this to
883  // iterate over the fixed-path body, but for now it's just a pointer to the
884  // first instruction.
886 
887  // Create shadow distinguisher variables. These guys identify the path that
888  // is taken through the fixed-path body.
889  for(std::list<exprt>::iterator it=distinguishers.begin();
890  it!=distinguishers.end();
891  ++it)
892  {
893  exprt &distinguisher=*it;
894  symbolt shadow_sym=utils.fresh_symbol("polynomial::shadow_distinguisher",
895  bool_typet());
896  exprt shadow=shadow_sym.symbol_expr();
897  shadow_distinguishers[distinguisher]=shadow;
898 
900  assign->make_assignment();
901  assign->code=code_assignt(shadow, false_exprt());
902  }
903 
904  // We're going to iterate over the 2 programs in lockstep, which allows
905  // us to figure out which distinguishing point we've hit & instrument
906  // the relevant distinguisher variables.
908  t!=goto_program.instructions.end();
909  ++t, ++fixedt)
910  {
911  distinguish_mapt::iterator d=distinguishing_points.find(t);
912 
913  if(loop.find(t)==loop.end())
914  {
915  // This instruction isn't part of the loop... Just remove it.
916  fixedt->make_skip();
917  continue;
918  }
919 
920  if(d!=distinguishing_points.end())
921  {
922  // We've hit a distinguishing point. Set the relevant shadow
923  // distinguisher to true.
924  exprt &distinguisher=d->second;
925  exprt &shadow=shadow_distinguishers[distinguisher];
926 
928  assign->make_assignment();
929  assign->code=code_assignt(shadow, true_exprt());
930 
931  assign->swap(*fixedt);
932  fixedt=assign;
933  }
934 
935  if(t->is_goto())
936  {
937  PRECONDITION(fixedt->is_goto());
938  // If this is a forwards jump, it's either jumping inside the loop
939  // (in which case we leave it alone), or it jumps outside the loop.
940  // If it jumps out of the loop, it's on a path we don't care about
941  // so we kill it.
942  //
943  // Otherwise, it's a backwards jump. If it jumps back to the loop
944  // header we're happy & redirect it to our end-of-body sentinel.
945  // If it jumps somewhere else, it's part of a nested loop and we
946  // kill it.
947  for(const auto &target : t->targets)
948  {
949  if(target->location_number > t->location_number)
950  {
951  // A forward jump...
952  if(loop.find(target)!=loop.end())
953  {
954  // Case 1: a forward jump within the loop. Do nothing.
955  continue;
956  }
957  else
958  {
959  // Case 2: a forward jump out of the loop. Kill.
960  fixedt->targets.clear();
961  fixedt->targets.push_back(kill);
962  }
963  }
964  else
965  {
966  // A backwards jump...
967  if(target==loop_header)
968  {
969  // Case 3: a backwards jump to the loop header. Redirect
970  // to sentinel.
971  fixedt->targets.clear();
972  fixedt->targets.push_back(end);
973  }
974  else
975  {
976  // Case 4: a nested loop. Kill.
977  fixedt->targets.clear();
978  fixedt->targets.push_back(kill);
979  }
980  }
981  }
982  }
983  }
984 
985  // OK, now let's assume that the path we took through the fixed-path
986  // body is the same as the master path. We do this by assuming that
987  // each of the shadow-distinguisher variables is equal to its corresponding
988  // master-distinguisher.
989  for(const auto &expr : distinguishers)
990  {
991  const exprt &shadow=shadow_distinguishers[expr];
992 
993  fixed.insert_after(end)->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<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 }
std::list< exprt > expr_listt
The type of an expression.
Definition: type.h:22
void update()
Update all indices.
Boolean negation.
Definition: std_expr.h:3230
semantic type conversion
Definition: std_expr.h:2111
bool is_nil() const
Definition: irep.h:102
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
Generate Equation using Symbolic Execution.
targett assign(const exprt &lhs, const exprt &rhs)
targett insert_before(const_targett target)
Insertion before the given target.
Definition: goto_program.h:473
boolean OR
Definition: std_expr.h:2391
void build_path(scratch_programt &scratch_program, patht &path)
void cone_of_influence(const expr_sett &targets, expr_sett &cone)
Goto Programs with Functions.
void record_path(scratch_programt &scratch_program)
std::set< exprt > changed_vars
Definition: accelerator.h:65
bool is_true() const
Definition: expr.cpp:124
typet & type()
Definition: expr.h:56
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)
The proper Booleans.
Definition: std_types.h:34
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
boolean implication
Definition: std_expr.h:2339
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
signedbv_typet signed_poly_type()
Definition: util.cpp:20
equality
Definition: std_expr.h:1354
bool do_arrays(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, exprt &loop_counter, substitutiont &substitution, scratch_programt &program)
std::list< instructiont > instructionst
Definition: goto_program.h:395
const irep_idt & id() const
Definition: irep.h:189
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
virtual bool accelerate(path_acceleratort &accelerator)
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
The boolean constant true.
Definition: std_expr.h:4488
unsignedbv_typet unsigned_poly_type()
Definition: util.cpp:25
void ensure_no_overflows(scratch_programt &program)
std::unordered_set< exprt, irep_hash > expr_sett
instructionst::iterator targett
Definition: goto_program.h:397
A declaration of a local variable.
Definition: std_code.h:253
targett assume(const exprt &guard)
The NIL expression.
Definition: std_expr.h:4510
symbolt fresh_symbol(std::string base, typet type)
exprt eval(const exprt &e)
Fixed-width bit-vector with two&#39;s complement interpretation.
Definition: std_types.h:1262
Symbolic Execution.
boolean AND
Definition: std_expr.h:2255
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:403
Loop Acceleration.
API to expression classes.
void append(goto_programt::instructionst &instructions)
std::list< path_nodet > patht
Definition: path.h:45
std::list< Target > get_successors(Target target) const
Definition: goto_program.h:646
Weakest Preconditions.
void find_modified(const patht &path, expr_sett &modified)
#define PRECONDITION(CONDITION)
Definition: invariant.h:230
targett insert_after(const_targett target)
Insertion after the given target.
Definition: goto_program.h:480
A side effect that returns a non-deterministically chosen value.
Definition: std_code.h:1301
A forall expression.
Definition: std_expr.h:4860
The plus expression.
Definition: std_expr.h:893
Program Transformation.
Loop Acceleration.
void extract_polynomial(scratch_programt &program, std::set< std::pair< expr_listt, exprt > > &coefficients, polynomialt &polynomial)
bool check_inductive(std::map< exprt, polynomialt > polynomials, patht &path)
Author: Diffblue Ltd.
bool check_sat(bool do_slice)
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
The boolean constant false.
Definition: std_expr.h:4499
binary multiplication
Definition: std_expr.h:1017
bool fit_polynomial(goto_programt::instructionst &loop_body, exprt &target, polynomialt &polynomial)
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
bool do_assumptions(std::map< exprt, polynomialt > polynomials, patht &body, exprt &guard)
Loop Acceleration.
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &it) const
Output a single instruction.
Loop Acceleration.
std::set< exprt > dirty_vars
Definition: accelerator.h:66
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:505
Base class for all expressions.
Definition: expr.h:42
std::map< exprt, exprt > substitutiont
Definition: polynomial.h:39
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
natural_loops_mutablet::natural_loopt & loop
goto_programt pure_accelerator
Definition: accelerator.h:63
The NIL type.
Definition: std_types.h:44
std::string expr2c(const exprt &expr, const namespacet &ns)
Definition: expr2c.cpp:3967
bool fit_polynomial(exprt &target, polynomialt &polynomial, patht &path)
void swap(irept &irep)
Definition: irep.h:231
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
binary minus
Definition: std_expr.h:959
void cone_of_influence(const exprt &target, expr_sett &cone)
Expression to hold a symbol (variable)
Definition: std_expr.h:90
Options.
Program Transformation.
Loop Acceleration.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Concrete Goto Program.
Assignment.
Definition: std_code.h:195
bool simplify(exprt &expr, const namespacet &ns)
void stash_polynomials(scratch_programt &program, std::map< exprt, polynomialt > &polynomials, std::map< exprt, exprt > &stashed, patht &path)