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;
305  program.assign(
306  loop_counter,
308 
309  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
310  it!=polynomials.end();
311  ++it)
312  {
313  program.assign(it->first, it->second.to_expr());
314  accelerator.changed_vars.insert(it->first);
315  }
316 
317  // Add in any array assignments we can do now.
318  if(!utils.do_arrays(assigns, polynomials, loop_counter, stashed, program))
319  {
320  // We couldn't model some of the array assignments with polynomials...
321  // Unfortunately that means we just have to bail out.
322  return false;
323  }
324 
325  program.add_instruction(ASSUME)->guard=guard;
326  program.fix_types();
327 
328  if(path_is_monotone)
329  {
330  utils.ensure_no_overflows(program);
331  }
332 
333  accelerator.pure_accelerator.instructions.swap(program.instructions);
334 
335  return true;
336 }
337 
339 {
341 
342  program.append(fixed);
343  program.append(fixed);
344 
345  // Let's make sure that we get a path we have not seen before.
346  for(std::list<distinguish_valuest>::iterator it=accelerated_paths.begin();
347  it!=accelerated_paths.end();
348  ++it)
349  {
350  exprt new_path=false_exprt();
351 
352  for(distinguish_valuest::iterator jt=it->begin();
353  jt!=it->end();
354  ++jt)
355  {
356  exprt distinguisher=jt->first;
357  bool taken=jt->second;
358 
359  if(taken)
360  {
361  not_exprt negated(distinguisher);
362  distinguisher.swap(negated);
363  }
364 
365  or_exprt disjunct(new_path, distinguisher);
366  new_path.swap(disjunct);
367  }
368 
369  program.assume(new_path);
370  }
371 
372  program.add_instruction(ASSERT)->guard=false_exprt();
373 
374  try
375  {
376  if(program.check_sat())
377  {
378 #ifdef DEBUG
379  std::cout << "Found a path\n";
380 #endif
381  build_path(program, path);
382  record_path(program);
383 
384  return true;
385  }
386  }
387  catch(const std::string &s)
388  {
389  std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
390  }
391  catch(const char *s)
392  {
393  std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
394  }
395 
396  return false;
397 }
398 
400  exprt &var,
401  polynomialt &polynomial,
402  patht &path)
403 {
404  // These are the variables that var depends on with respect to the body.
405  std::vector<expr_listt> parameters;
406  std::set<std::pair<expr_listt, exprt> > coefficients;
407  expr_listt exprs;
409  expr_sett influence;
410 
411  cone_of_influence(var, influence);
412 
413 #ifdef DEBUG
414  std::cout << "Fitting a polynomial for " << expr2c(var, ns)
415  << ", which depends on:\n";
416 
417  for(expr_sett::iterator it=influence.begin();
418  it!=influence.end();
419  ++it)
420  {
421  std::cout << expr2c(*it, ns) << '\n';
422  }
423 #endif
424 
425  for(expr_sett::iterator it=influence.begin();
426  it!=influence.end();
427  ++it)
428  {
429  if(it->id()==ID_index ||
430  it->id()==ID_dereference)
431  {
432  // Hack: don't accelerate anything that depends on an array
433  // yet...
434  return false;
435  }
436 
437  exprs.clear();
438 
439  exprs.push_back(*it);
440  parameters.push_back(exprs);
441 
442  exprs.push_back(loop_counter);
443  parameters.push_back(exprs);
444  }
445 
446  // N
447  exprs.clear();
448  exprs.push_back(loop_counter);
449  parameters.push_back(exprs);
450 
451  // N^2
452  exprs.push_back(loop_counter);
453  parameters.push_back(exprs);
454 
455  // Constant
456  exprs.clear();
457  parameters.push_back(exprs);
458 
459  for(std::vector<expr_listt>::iterator it=parameters.begin();
460  it!=parameters.end();
461  ++it)
462  {
463  symbolt coeff=utils.fresh_symbol("polynomial::coeff", signed_poly_type());
464  coefficients.insert(make_pair(*it, coeff.symbol_expr()));
465 
466  // XXX HACK HACK HACK
467  // I'm just constraining these coefficients to prevent overflows
468  // messing things up later... Should really do this properly
469  // somehow.
470  program.assume(
472  from_integer(-(1 << 10), signed_poly_type()),
473  ID_lt,
474  coeff.symbol_expr()));
475  program.assume(
477  coeff.symbol_expr(),
478  ID_lt,
479  from_integer(1 << 10, signed_poly_type())));
480  }
481 
482  // Build a set of values for all the parameters that allow us to fit a
483  // unique polynomial.
484 
485  std::map<exprt, exprt> ivals1;
486  std::map<exprt, exprt> ivals2;
487  std::map<exprt, exprt> ivals3;
488 
489  for(expr_sett::iterator it=influence.begin();
490  it!=influence.end();
491  ++it)
492  {
493  symbolt ival1=utils.fresh_symbol("polynomial::init",
494  it->type());
495  symbolt ival2=utils.fresh_symbol("polynomial::init",
496  it->type());
497  symbolt ival3=utils.fresh_symbol("polynomial::init",
498  it->type());
499 
500  program.assume(binary_relation_exprt(ival1.symbol_expr(), "<",
501  ival2.symbol_expr()));
502  program.assume(binary_relation_exprt(ival2.symbol_expr(), "<",
503  ival3.symbol_expr()));
504 
505 #if 0
506  if(it->type()==signedbv_typet())
507  {
508  program.assume(binary_relation_exprt(ival1.symbol_expr(), ">",
509  from_integer(-100, it->type())));
510  }
511  program.assume(binary_relation_exprt(ival1.symbol_expr(), "<",
512  from_integer(100, it->type())));
513 
514  if(it->type()==signedbv_typet())
515  {
516  program.assume(binary_relation_exprt(ival2.symbol_expr(), ">",
517  from_integer(-100, it->type())));
518  }
519  program.assume(binary_relation_exprt(ival2.symbol_expr(), "<",
520  from_integer(100, it->type())));
521 
522  if(it->type()==signedbv_typet())
523  {
524  program.assume(binary_relation_exprt(ival3.symbol_expr(), ">",
525  from_integer(-100, it->type())));
526  }
527  program.assume(binary_relation_exprt(ival3.symbol_expr(), "<",
528  from_integer(100, it->type())));
529 #endif
530 
531  ivals1[*it]=ival1.symbol_expr();
532  ivals2[*it]=ival2.symbol_expr();
533  ivals3[*it]=ival3.symbol_expr();
534 
535  // ivals1[*it]=from_integer(1, it->type());
536  }
537 
538  std::map<exprt, exprt> values;
539 
540  for(expr_sett::iterator it=influence.begin();
541  it!=influence.end();
542  ++it)
543  {
544  values[*it]=ivals1[*it];
545  }
546 
547  // Start building the program. Begin by decl'ing each of the
548  // master distinguishers.
549  for(std::list<exprt>::iterator it=distinguishers.begin();
550  it!=distinguishers.end();
551  ++it)
552  {
553  program.add_instruction(DECL)->code=code_declt(*it);
554  }
555 
556  // Now assume our polynomial fits at each of our sample points.
557  assert_for_values(program, values, coefficients, 1, fixed, var);
558 
559  for(int n=0; n <= 1; n++)
560  {
561  for(expr_sett::iterator it=influence.begin();
562  it!=influence.end();
563  ++it)
564  {
565  values[*it]=ivals2[*it];
566  assert_for_values(program, values, coefficients, n, fixed, var);
567 
568  values[*it]=ivals3[*it];
569  assert_for_values(program, values, coefficients, n, fixed, var);
570 
571  values[*it]=ivals1[*it];
572  }
573  }
574 
575  for(expr_sett::iterator it=influence.begin();
576  it!=influence.end();
577  ++it)
578  {
579  values[*it]=ivals3[*it];
580  }
581 
582  assert_for_values(program, values, coefficients, 0, fixed, var);
583  assert_for_values(program, values, coefficients, 1, fixed, var);
584  assert_for_values(program, values, coefficients, 2, fixed, var);
585 
586  // Let's make sure that we get a path we have not seen before.
587  for(std::list<distinguish_valuest>::iterator it=accelerated_paths.begin();
588  it!=accelerated_paths.end();
589  ++it)
590  {
591  exprt new_path=false_exprt();
592 
593  for(distinguish_valuest::iterator jt=it->begin();
594  jt!=it->end();
595  ++jt)
596  {
597  exprt distinguisher=jt->first;
598  bool taken=jt->second;
599 
600  if(taken)
601  {
602  not_exprt negated(distinguisher);
603  distinguisher.swap(negated);
604  }
605 
606  or_exprt disjunct(new_path, distinguisher);
607  new_path.swap(disjunct);
608  }
609 
610  program.assume(new_path);
611  }
612 
613  utils.ensure_no_overflows(program);
614 
615  // Now do an ASSERT(false) to grab a counterexample
616  program.add_instruction(ASSERT)->guard=false_exprt();
617 
618  // If the path is satisfiable, we've fitted a polynomial. Extract the
619  // relevant coefficients and return the expression.
620  try
621  {
622  if(program.check_sat())
623  {
624 #ifdef DEBUG
625  std::cout << "Found a polynomial\n";
626 #endif
627 
628  utils.extract_polynomial(program, coefficients, polynomial);
629  build_path(program, path);
630  record_path(program);
631 
632  return true;
633  }
634  }
635  catch(const std::string &s)
636  {
637  std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
638  }
639  catch(const char *s)
640  {
641  std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
642  }
643 
644  return false;
645 }
646 
648  scratch_programt &program,
649  std::map<exprt, exprt> &values,
650  std::set<std::pair<expr_listt, exprt> > &coefficients,
651  int num_unwindings,
652  goto_programt &loop_body,
653  exprt &target)
654 {
655  // First figure out what the appropriate type for this expression is.
656  typet expr_type=nil_typet();
657 
658  for(std::map<exprt, exprt>::iterator it=values.begin();
659  it!=values.end();
660  ++it)
661  {
662  if(expr_type==nil_typet())
663  {
664  expr_type=it->first.type();
665  }
666  else
667  {
668  expr_type=join_types(expr_type, it->first.type());
669  }
670  }
671 
672  // Now set the initial values of the all the variables...
673  for(std::map<exprt, exprt>::iterator it=values.begin();
674  it!=values.end();
675  ++it)
676  {
677  program.assign(it->first, it->second);
678  }
679 
680  // Now unwind the loop as many times as we need to.
681  for(int i=0; i<num_unwindings; i++)
682  {
683  program.append(loop_body);
684  }
685 
686  // Now build the polynomial for this point and assert it fits.
687  exprt rhs=nil_exprt();
688 
689  for(std::set<std::pair<expr_listt, exprt> >::iterator it=coefficients.begin();
690  it!=coefficients.end();
691  ++it)
692  {
693  exprt concrete_value=from_integer(1, expr_type);
694 
695  for(expr_listt::const_iterator e_it=it->first.begin();
696  e_it!=it->first.end();
697  ++e_it)
698  {
699  exprt e=*e_it;
700 
701  if(e==loop_counter)
702  {
703  mult_exprt mult(
704  from_integer(num_unwindings, expr_type), concrete_value);
705  mult.swap(concrete_value);
706  }
707  else
708  {
709  std::map<exprt, exprt>::iterator v_it=values.find(e);
710 
711  PRECONDITION(v_it!=values.end());
712 
713  mult_exprt mult(concrete_value, v_it->second);
714  mult.swap(concrete_value);
715  }
716  }
717 
718  // OK, concrete_value now contains the value of all the relevant variables
719  // multiplied together. Create the term concrete_value*coefficient and add
720  // it into the polynomial.
721  typecast_exprt cast(it->second, expr_type);
722  const mult_exprt term(concrete_value, cast);
723 
724  if(rhs.is_nil())
725  {
726  rhs=term;
727  }
728  else
729  {
730  rhs=plus_exprt(rhs, term);
731  }
732  }
733 
734  rhs=typecast_exprt(rhs, target.type());
735 
736  // We now have the RHS of the polynomial. Assert that this is equal to the
737  // actual value of the variable we're fitting.
738  const equal_exprt polynomial_holds(target, rhs);
739 
740  // Finally, assert that the polynomial equals the variable we're fitting.
741  goto_programt::targett assumption=program.add_instruction(ASSUME);
742  assumption->guard=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(natural_loops_mutablet::natural_loopt::iterator it=loop.begin();
756  it!=loop.end();
757  ++it)
758  {
759  const auto succs=goto_program.get_successors(*it);
760 
761  if(succs.size() > 1)
762  {
763  // This location has multiple successors -- each successor is a
764  // distinguishing point.
765  for(const auto &jt : succs)
766  {
767  symbolt distinguisher_sym =
768  utils.fresh_symbol("polynomial::distinguisher", bool_typet());
769  symbol_exprt distinguisher=distinguisher_sym.symbol_expr();
770 
771  distinguishing_points[jt]=distinguisher;
772  distinguishers.push_back(distinguisher);
773  }
774  }
775  }
776 }
777 
779  scratch_programt &scratch_program, patht &path)
780 {
782 
783  do
784  {
786 
787  const auto succs=goto_program.get_successors(t);
788 
789  INVARIANT(succs.size() > 0,
790  "we should have a looping path, so we should never hit a location "
791  "with no successors.");
792 
793  if(succs.size()==1)
794  {
795  // Only one successor -- accumulate it and move on.
796  path.push_back(path_nodet(t));
797  t=succs.front();
798  continue;
799  }
800 
801  // We have multiple successors. Examine the distinguisher variables
802  // to see which branch was taken.
803  bool found_branch=false;
804 
805  for(const auto &succ : succs)
806  {
807  exprt &distinguisher=distinguishing_points[succ];
808  bool taken=scratch_program.eval(distinguisher).is_true();
809 
810  if(taken)
811  {
812  if(!found_branch ||
813  (succ->location_number < next->location_number))
814  {
815  next=succ;
816  }
817 
818  found_branch=true;
819  }
820  }
821 
822  PRECONDITION(found_branch);
823 
824  exprt cond=nil_exprt();
825 
826  if(t->is_goto())
827  {
828  // If this was a conditional branch (it probably was), figure out
829  // if we hit the "taken" or "not taken" branch & accumulate the
830  // appropriate guard.
831  cond=not_exprt(t->guard);
832 
833  for(goto_programt::targetst::iterator it=t->targets.begin();
834  it!=t->targets.end();
835  ++it)
836  {
837  if(next==*it)
838  {
839  cond=t->guard;
840  break;
841  }
842  }
843  }
844 
845  path.push_back(path_nodet(t, cond));
846 
847  t=next;
848  }
849  while(t!=loop_header && (loop.find(t)!=loop.end()));
850 }
851 
852 /*
853  * Take the body of the loop we are accelerating and produce a fixed-path
854  * version of that body, suitable for use in the fixed-path acceleration we
855  * will be doing later.
856  */
858 {
860  std::map<exprt, exprt> shadow_distinguishers;
861 
863 
865  {
866  if(it->is_assert())
867  {
868  it->type=ASSUME;
869  }
870  }
871 
872  // We're only interested in paths that loop back to the loop header.
873  // As such, any path that jumps outside of the loop or jumps backwards
874  // to a location other than the loop header (i.e. a nested loop) is not
875  // one we're interested in, and we'll redirect it to this assume(false).
877  kill->guard=false_exprt();
878 
879  // Make a sentinel instruction to mark the end of the loop body.
880  // We'll use this as the new target for any back-jumps to the loop
881  // header.
883 
884  // A pointer to the start of the fixed-path body. We'll be using this to
885  // iterate over the fixed-path body, but for now it's just a pointer to the
886  // first instruction.
888 
889  // Create shadow distinguisher variables. These guys identify the path that
890  // is taken through the fixed-path body.
891  for(std::list<exprt>::iterator it=distinguishers.begin();
892  it!=distinguishers.end();
893  ++it)
894  {
895  exprt &distinguisher=*it;
896  symbolt shadow_sym=utils.fresh_symbol("polynomial::shadow_distinguisher",
897  bool_typet());
898  exprt shadow=shadow_sym.symbol_expr();
899  shadow_distinguishers[distinguisher]=shadow;
900 
902  assign->make_assignment();
903  assign->code=code_assignt(shadow, false_exprt());
904  }
905 
906  // We're going to iterate over the 2 programs in lockstep, which allows
907  // us to figure out which distinguishing point we've hit & instrument
908  // the relevant distinguisher variables.
910  t!=goto_program.instructions.end();
911  ++t, ++fixedt)
912  {
913  distinguish_mapt::iterator d=distinguishing_points.find(t);
914 
915  if(loop.find(t)==loop.end())
916  {
917  // This instruction isn't part of the loop... Just remove it.
918  fixedt->make_skip();
919  continue;
920  }
921 
922  if(d!=distinguishing_points.end())
923  {
924  // We've hit a distinguishing point. Set the relevant shadow
925  // distinguisher to true.
926  exprt &distinguisher=d->second;
927  exprt &shadow=shadow_distinguishers[distinguisher];
928 
930  assign->make_assignment();
931  assign->code=code_assignt(shadow, true_exprt());
932 
933  assign->swap(*fixedt);
934  fixedt=assign;
935  }
936 
937  if(t->is_goto())
938  {
939  PRECONDITION(fixedt->is_goto());
940  // If this is a forwards jump, it's either jumping inside the loop
941  // (in which case we leave it alone), or it jumps outside the loop.
942  // If it jumps out of the loop, it's on a path we don't care about
943  // so we kill it.
944  //
945  // Otherwise, it's a backwards jump. If it jumps back to the loop
946  // header we're happy & redirect it to our end-of-body sentinel.
947  // If it jumps somewhere else, it's part of a nested loop and we
948  // kill it.
949  for(const auto &target : t->targets)
950  {
951  if(target->location_number > t->location_number)
952  {
953  // A forward jump...
954  if(loop.find(target)!=loop.end())
955  {
956  // Case 1: a forward jump within the loop. Do nothing.
957  continue;
958  }
959  else
960  {
961  // Case 2: a forward jump out of the loop. Kill.
962  fixedt->targets.clear();
963  fixedt->targets.push_back(kill);
964  }
965  }
966  else
967  {
968  // A backwards jump...
969  if(target==loop_header)
970  {
971  // Case 3: a backwards jump to the loop header. Redirect
972  // to sentinel.
973  fixedt->targets.clear();
974  fixedt->targets.push_back(end);
975  }
976  else
977  {
978  // Case 4: a nested loop. Kill.
979  fixedt->targets.clear();
980  fixedt->targets.push_back(kill);
981  }
982  }
983  }
984  }
985  }
986 
987  // OK, now let's assume that the path we took through the fixed-path
988  // body is the same as the master path. We do this by assuming that
989  // each of the shadow-distinguisher variables is equal to its corresponding
990  // master-distinguisher.
991  for(const auto &expr : distinguishers)
992  {
993  const exprt &shadow=shadow_distinguishers[expr];
994 
995  fixed.insert_after(end)->make_assumption(equal_exprt(expr, shadow));
996  }
997 
998  // Finally, let's remove all the skips we introduced and fix the
999  // jump targets.
1000  fixed.update();
1001  remove_skip(fixed);
1002 }
1003 
1005  scratch_programt &program)
1006 {
1007  distinguish_valuest path_val;
1008 
1009  for(std::list<exprt>::iterator it=distinguishers.begin();
1010  it!=distinguishers.end();
1011  ++it)
1012  {
1013  path_val[*it]=program.eval(*it).is_true();
1014  }
1015 
1016  accelerated_paths.push_back(path_val);
1017 }
1018 
1020  const exprt &e,
1021  exprt &array)
1022 {
1023  expr_sett influence;
1024 
1025  cone_of_influence(e, influence);
1026 
1027  for(expr_sett::iterator it=influence.begin();
1028  it!=influence.end();
1029  ++it)
1030  {
1031  if(it->id()==ID_index ||
1032  it->id()==ID_dereference)
1033  {
1034  array=*it;
1035  return true;
1036  }
1037  }
1038 
1039  return false;
1040 }
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:3228
semantic type conversion
Definition: std_expr.h:2111
bool is_nil() const
Definition: irep.h:172
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:204
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:259
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
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:4486
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:254
targett assume(const exprt &guard)
The NIL expression.
Definition: std_expr.h:4508
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:1271
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:242
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:1340
A forall expression.
Definition: std_expr.h:4858
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:4497
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:3950
bool fit_polynomial(exprt &target, polynomialt &polynomial, patht &path)
void swap(irept &irep)
Definition: irep.h:303
#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:196
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)