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, 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<symbol_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<symbol_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<symbol_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 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:809
symex_target_equation.h
overflow_instrumenter.h
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:438
path_acceleratort::changed_vars
std::set< exprt > changed_vars
Definition: accelerator.h:65
polynomialt
Definition: polynomial.h:41
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:778
arith_tools.h
disjunctive_polynomial_accelerationt::distinguish_valuest
std::map< exprt, bool > distinguish_valuest
Definition: disjunctive_polynomial_acceleration.h:96
forall_exprt
A forall expression.
Definition: std_expr.h:4777
polynomial_acceleratort::fit_polynomial
bool fit_polynomial(goto_programt::instructionst &loop_body, exprt &target, polynomialt &polynomial)
Definition: polynomial_accelerator.cpp:435
typet
The type of an expression, extends irept.
Definition: type.h:27
acceleration_utilst::fresh_symbol
symbolt fresh_symbol(std::string base, typet type)
Definition: acceleration_utils.cpp:1271
disjunctive_polynomial_accelerationt::goto_functions
goto_functionst & goto_functions
Definition: disjunctive_polynomial_acceleration.h:90
expr_listt
std::list< exprt > expr_listt
Definition: acceleration_utils.h:34
goto_programt::instructionst
std::list< instructiont > instructionst
Definition: goto_program.h:412
disjunctive_polynomial_accelerationt::find_path
bool find_path(patht &path)
Definition: disjunctive_polynomial_acceleration.cpp:338
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
nil_typet
The NIL type, i.e., an invalid type, no value.
Definition: std_types.h:39
goto_programt::update
void update()
Update all indices.
Definition: goto_program.cpp:506
goto_programt::copy_from
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
Definition: goto_program.cpp:591
disjunctive_polynomial_accelerationt::goto_program
goto_programt & goto_program
Definition: disjunctive_polynomial_acceleration.h:91
code_declt
A codet representing the declaration of a local variable.
Definition: std_code.h:352
cone_of_influencet::cone_of_influence
void cone_of_influence(const expr_sett &targets, expr_sett &cone)
Definition: cone_of_influence.cpp:18
and_exprt
Boolean AND.
Definition: std_expr.h:2409
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
disjunctive_polynomial_accelerationt::find_distinguishing_points
void find_distinguishing_points()
Definition: disjunctive_polynomial_acceleration.cpp:753
acceleration_utilst::do_arrays
bool do_arrays(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, substitutiont &substitution, scratch_programt &program)
Definition: acceleration_utils.cpp:556
disjunctive_polynomial_accelerationt::message_handler
message_handlert & message_handler
Definition: disjunctive_polynomial_acceleration.h:68
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:647
exprt
Base class for all expressions.
Definition: expr.h:54
path_nodet
Definition: path.h:23
options.h
bool_typet
The Boolean type.
Definition: std_types.h:28
goto_programt::get_successors
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
Definition: goto_program.h:715
exprt::is_true
bool is_true() const
Return whether the expression is a constant representing true.
Definition: expr.cpp:90
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:143
equal_exprt
Equality.
Definition: std_expr.h:1484
scratch_programt::append
void append(goto_programt::instructionst &instructions)
Definition: scratch_program.cpp:72
unsigned_poly_type
unsignedbv_typet unsigned_poly_type()
Definition: util.cpp:25
acceleration_utilst::find_modified
void find_modified(const patht &path, expr_sett &modified)
Definition: acceleration_utils.cpp:86
path_acceleratort::clear
void clear()
Definition: accelerator.h:53
cone_of_influencet
Definition: cone_of_influence.h:27
goto_programt::add_instruction
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:541
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:194
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
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:510
acceleration_utilst::extract_polynomial
void extract_polynomial(scratch_programt &program, std::set< std::pair< expr_listt, exprt > > &coefficients, polynomialt &polynomial)
Definition: acceleration_utils.cpp:1222
find_symbols.h
disjunctive_polynomial_accelerationt::loop_header
goto_programt::targett loop_header
Definition: disjunctive_polynomial_acceleration.h:93
or_exprt
Boolean OR.
Definition: std_expr.h:2531
disjunctive_polynomial_accelerationt::loop_counter
exprt loop_counter
Definition: disjunctive_polynomial_acceleration.h:99
scratch_programt
Definition: scratch_program.h:36
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:37
signed_poly_type
signedbv_typet signed_poly_type()
Definition: util.cpp:20
expr2c.h
expr2c
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:3955
scratch_programt::fix_types
void fix_types()
Definition: scratch_program.cpp:124
scratch_programt::eval
exprt eval(const exprt &e)
Definition: scratch_program.cpp:63
nil_exprt
The NIL expression.
Definition: std_expr.h:4461
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: std_types.h:1278
goto_symex.h
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:121
scratch_programt::check_sat
bool check_sat(bool do_slice)
Definition: scratch_program.cpp:25
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:2320
disjunctive_polynomial_accelerationt::symbol_table
symbol_tablet & symbol_table
Definition: disjunctive_polynomial_acceleration.h:88
path_acceleratort
Definition: accelerator.h:26
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:1159
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:479
irept::swap
void swap(irept &irep)
Definition: irep.h:303
scratch_programt::assume
targett assume(const exprt &guard)
Definition: scratch_program.cpp:91
path_acceleratort::pure_accelerator
goto_programt pure_accelerator
Definition: accelerator.h:63
irept::is_nil
bool is_nil() const
Definition: irep.h:172
irept::id
const irep_idt & id() const
Definition: irep.h:259
false_exprt
The Boolean constant false.
Definition: std_expr.h:4452
disjunctive_polynomial_accelerationt::accelerate
bool accelerate(path_acceleratort &accelerator)
Definition: disjunctive_polynomial_acceleration.cpp:49
goto_check.h
disjunctive_polynomial_accelerationt::loop
natural_loops_mutablet::natural_loopt & loop
Definition: disjunctive_polynomial_acceleration.h:92
SKIP
Definition: goto_program.h:38
std_code.h
disjunctive_polynomial_accelerationt::distinguishing_points
distinguish_mapt distinguishing_points
Definition: disjunctive_polynomial_acceleration.h:100
minus_exprt
Binary minus.
Definition: std_expr.h:1106
goto_program.h
disjunctive_polynomial_accelerationt::ns
namespacet ns
Definition: disjunctive_polynomial_acceleration.h:89
join_types
typet join_types(const typet &t1, const typet &t2)
Return the smallest type that both t1 and t2 can be cast to without losing information.
Definition: util.cpp:70
source_locationt
Definition: source_location.h:20
simplify_expr.h
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1633
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:420
disjunctive_polynomial_accelerationt::build_fixed
void build_fixed()
Definition: disjunctive_polynomial_acceleration.cpp:857
disjunctive_polynomial_accelerationt::depends_on_array
bool depends_on_array(const exprt &e, exprt &array)
Definition: disjunctive_polynomial_acceleration.cpp:1019
DECL
Definition: goto_program.h:47
acceleration_utilst::check_inductive
bool check_inductive(std::map< exprt, polynomialt > polynomials, patht &path)
Definition: acceleration_utils.cpp:114
patht
std::list< path_nodet > patht
Definition: path.h:45
accelerator.h
disjunctive_polynomial_accelerationt::fixed
goto_programt fixed
Definition: disjunctive_polynomial_acceleration.h:103
symbolt
Symbol table entry.
Definition: symbol.h:27
replace_expr
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
Definition: replace_expr.cpp:12
ASSUME
Definition: goto_program.h:35
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:123
cone_of_influence.h
binary_relation_exprt
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:878
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:399
goto_functions.h
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
disjunctive_polynomial_accelerationt::record_path
void record_path(scratch_programt &scratch_program)
Definition: disjunctive_polynomial_acceleration.cpp:1004
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:518
disjunctive_polynomial_accelerationt::distinguishers
std::list< symbol_exprt > distinguishers
Definition: disjunctive_polynomial_acceleration.h:101
implies_exprt
Boolean implication.
Definition: std_expr.h:2485
disjunctive_polynomial_acceleration.h
replace_expr.h
disjunctive_polynomial_accelerationt::accelerated_paths
std::list< distinguish_valuest > accelerated_paths
Definition: disjunctive_polynomial_acceleration.h:104
symbol_table.h
Author: Diffblue Ltd.
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2277
remove_skip.h
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:256
true_exprt
The Boolean constant true.
Definition: std_expr.h:4443
ASSERT
Definition: goto_program.h:36
std_expr.h
scratch_programt::assign
targett assign(const exprt &lhs, const exprt &rhs)
Definition: scratch_program.cpp:80
util.h
acceleration_utilst::do_assumptions
bool do_assumptions(std::map< exprt, polynomialt > polynomials, patht &body, exprt &guard)
Definition: acceleration_utils.cpp:357
disjunctive_polynomial_accelerationt::cone_of_influence
void cone_of_influence(const exprt &target, expr_sett &cone)
Definition: disjunctive_polynomial_acceleration.cpp:745
polynomial_accelerator.h
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:414
wp.h
validation_modet::INVARIANT
not_exprt
Boolean negation.
Definition: std_expr.h:3308