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