cprover
polynomial_accelerator.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Loop Acceleration
4 
5 Author: Matt Lewis
6 
7 \*******************************************************************/
8 
11 
12 #include "polynomial_accelerator.h"
13 
14 #include <iostream>
15 #include <map>
16 #include <set>
17 #include <string>
18 #include <sstream>
19 
21 #include <goto-programs/wp.h>
22 
23 #include <goto-symex/goto_symex.h>
25 
26 #include <analyses/goto_check.h>
27 
28 #include <ansi-c/expr2c.h>
29 
30 #include <util/c_types.h>
31 #include <util/symbol_table.h>
32 #include <util/options.h>
33 #include <util/std_expr.h>
34 #include <util/std_code.h>
35 #include <util/find_symbols.h>
36 #include <util/simplify_expr.h>
37 #include <util/replace_expr.h>
38 #include <util/arith_tools.h>
39 
40 #include "accelerator.h"
41 #include "util.h"
42 #include "cone_of_influence.h"
43 #include "overflow_instrumenter.h"
44 
46  patht &loop,
47  path_acceleratort &accelerator)
48 {
50  accelerator.clear();
51 
52  for(patht::iterator it=loop.begin();
53  it!=loop.end();
54  ++it)
55  {
56  body.push_back(*(it->loc));
57  }
58 
59  expr_sett targets;
60  std::map<exprt, polynomialt> polynomials;
63 
64  utils.find_modified(body, targets);
65 
66 #ifdef DEBUG
67  std::cout << "Polynomial accelerating program:\n";
68 
69  for(goto_programt::instructionst::iterator it=body.begin();
70  it!=body.end();
71  ++it)
72  {
73  program.output_instruction(ns, "scratch", std::cout, *it);
74  }
75 
76  std::cout << "Modified:\n";
77 
78  for(expr_sett::iterator it=targets.begin();
79  it!=targets.end();
80  ++it)
81  {
82  std::cout << expr2c(*it, ns) << '\n';
83  }
84 #endif
85 
86  for(goto_programt::instructionst::iterator it=body.begin();
87  it!=body.end();
88  ++it)
89  {
90  if(it->is_assign() || it->is_decl())
91  {
92  assigns.push_back(*it);
93  }
94  }
95 
96  if(loop_counter.is_nil())
97  {
98  symbolt loop_sym=utils.fresh_symbol("polynomial::loop_counter",
100  loop_counter=loop_sym.symbol_expr();
101  }
102 
103  for(expr_sett::iterator it=targets.begin();
104  it!=targets.end();
105  ++it)
106  {
107  polynomialt poly;
108  exprt target=*it;
109  expr_sett influence;
110  goto_programt::instructionst sliced_assigns;
111 
112  if(target.type()==bool_typet())
113  {
114  // Hack: don't accelerate booleans.
115  continue;
116  }
117 
118  cone_of_influence(assigns, target, sliced_assigns, influence);
119 
120  if(influence.find(target)==influence.end())
121  {
122 #ifdef DEBUG
123  std::cout << "Found nonrecursive expression: "
124  << expr2c(target, ns) << '\n';
125 #endif
126 
127  nonrecursive.insert(target);
128  continue;
129  }
130 
131  if(target.id()==ID_index ||
132  target.id()==ID_dereference)
133  {
134  // We can't accelerate a recursive indirect access...
135  accelerator.dirty_vars.insert(target);
136  continue;
137  }
138 
139  if(fit_polynomial_sliced(sliced_assigns, target, influence, poly))
140  {
141  std::map<exprt, polynomialt> this_poly;
142  this_poly[target]=poly;
143 
144  if(check_inductive(this_poly, assigns))
145  {
146  polynomials.insert(std::make_pair(target, poly));
147  }
148  }
149  else
150  {
151 #ifdef DEBUG
152  std::cout << "Failed to fit a polynomial for "
153  << expr2c(target, ns) << '\n';
154 #endif
155  accelerator.dirty_vars.insert(*it);
156  }
157  }
158 
159 #if 0
160  if(polynomials.empty())
161  {
162  // return false;
163  }
164 
165  if (!utils.check_inductive(polynomials, assigns)) {
166  // They're not inductive :-(
167  return false;
168  }
169 #endif
170 
171  substitutiont stashed;
172  stash_polynomials(program, polynomials, stashed, body);
173 
174  exprt guard;
175  exprt guard_last;
176 
177  bool path_is_monotone;
178 
179  try
180  {
181  path_is_monotone=utils.do_assumptions(polynomials, loop, guard);
182  }
183  catch(const std::string &s)
184  {
185  // Couldn't do WP.
186  std::cout << "Assumptions error: " << s << '\n';
187  return false;
188  }
189 
190  guard_last=guard;
191 
192  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
193  it!=polynomials.end();
194  ++it)
195  {
196  replace_expr(it->first, it->second.to_expr(), guard_last);
197  }
198 
199  if(path_is_monotone)
200  {
201  // OK cool -- the path is monotone, so we can just assume the condition for
202  // the first and last iterations.
203  replace_expr(
204  loop_counter,
206  guard_last);
207  // simplify(guard_last, ns);
208  }
209  else
210  {
211  // The path is not monotone, so we need to introduce a quantifier to ensure
212  // that the condition held for all 0 <= k < n.
213  symbolt k_sym=utils.fresh_symbol("polynomial::k", unsigned_poly_type());
214  const symbol_exprt k = k_sym.symbol_expr();
215 
216  const and_exprt k_bound(
217  binary_relation_exprt(from_integer(0, k.type()), ID_le, k),
219  replace_expr(loop_counter, k, guard_last);
220 
221  implies_exprt implies(k_bound, guard_last);
222  // simplify(implies, ns);
223 
224  guard_last = forall_exprt(k, implies);
225  }
226 
227  // All our conditions are met -- we can finally build the accelerator!
228  // It is of the form:
229  //
230  // assume(guard);
231  // loop_counter=*;
232  // target1=polynomial1;
233  // target2=polynomial2;
234  // ...
235  // assume(guard);
236  // assume(no overflows in previous code);
237 
238  program.add_instruction(ASSUME)->guard=guard;
239 
241 
242  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
243  it!=polynomials.end();
244  ++it)
245  {
246  program.assign(it->first, it->second.to_expr());
247  }
248 
249  // Add in any array assignments we can do now.
251  assigns, polynomials, loop_counter, stashed, nonrecursive, program))
252  {
253  // We couldn't model some of the array assignments with polynomials...
254  // Unfortunately that means we just have to bail out.
255 #ifdef DEBUG
256  std::cout << "Failed to accelerate a nonrecursive expression\n";
257 #endif
258  return false;
259  }
260 
261  program.add_instruction(ASSUME)->guard=guard_last;
262  program.fix_types();
263 
264  if(path_is_monotone)
265  {
266  utils.ensure_no_overflows(program);
267  }
268 
269  accelerator.pure_accelerator.instructions.swap(program.instructions);
270 
271  return true;
272 }
273 
276  exprt &var,
277  expr_sett &influence,
278  polynomialt &polynomial)
279 {
280  // These are the variables that var depends on with respect to the body.
281  std::vector<expr_listt> parameters;
282  std::set<std::pair<expr_listt, exprt> > coefficients;
283  expr_listt exprs;
285  exprt overflow_var =
286  utils.fresh_symbol("polynomial::overflow", bool_typet()).symbol_expr();
287  overflow_instrumentert overflow(program, overflow_var, symbol_table);
288 
289 #ifdef DEBUG
290  std::cout << "Fitting a polynomial for " << expr2c(var, ns)
291  << ", which depends on:\n";
292 
293  for(expr_sett::iterator it=influence.begin();
294  it!=influence.end();
295  ++it)
296  {
297  std::cout << expr2c(*it, ns) << '\n';
298  }
299 #endif
300 
301  for(expr_sett::iterator it=influence.begin();
302  it!=influence.end();
303  ++it)
304  {
305  if(it->id()==ID_index ||
306  it->id()==ID_dereference)
307  {
308  // Hack: don't accelerate variables that depend on arrays...
309  return false;
310  }
311 
312  exprs.clear();
313 
314  exprs.push_back(*it);
315  parameters.push_back(exprs);
316 
317  exprs.push_back(loop_counter);
318  parameters.push_back(exprs);
319  }
320 
321  // N
322  exprs.clear();
323  exprs.push_back(loop_counter);
324  parameters.push_back(exprs);
325 
326  // N^2
327  exprs.push_back(loop_counter);
328  // parameters.push_back(exprs);
329 
330  // Constant
331  exprs.clear();
332  parameters.push_back(exprs);
333 
334  if(!is_bitvector(var.type()))
335  {
336  // We don't really know how to accelerate non-bitvectors anyway...
337  return false;
338  }
339 
340  std::size_t width=to_bitvector_type(var.type()).get_width();
341  assert(width>0);
342 
343  for(std::vector<expr_listt>::iterator it=parameters.begin();
344  it!=parameters.end();
345  ++it)
346  {
347  symbolt coeff=utils.fresh_symbol("polynomial::coeff",
348  signedbv_typet(width));
349  coefficients.insert(std::make_pair(*it, coeff.symbol_expr()));
350  }
351 
352  // Build a set of values for all the parameters that allow us to fit a
353  // unique polynomial.
354 
355  // XXX
356  // This isn't ok -- we're assuming 0, 1 and 2 are valid values for the
357  // variables involved, but this might make the path condition UNSAT. Should
358  // really be solving the path constraints a few times to get valid probe
359  // values...
360 
361  std::map<exprt, int> values;
362 
363  for(expr_sett::iterator it=influence.begin();
364  it!=influence.end();
365  ++it)
366  {
367  values[*it]=0;
368  }
369 
370 #ifdef DEBUG
371  std::cout << "Fitting polynomial over " << values.size()
372  << " variables\n";
373 #endif
374 
375  for(int n=0; n<=2; n++)
376  {
377  for(expr_sett::iterator it=influence.begin();
378  it!=influence.end();
379  ++it)
380  {
381  values[*it]=1;
382  assert_for_values(program, values, coefficients, n, body, var, overflow);
383  values[*it]=0;
384  }
385  }
386 
387  // Now just need to assert the case where all values are 0 and all are 2.
388  assert_for_values(program, values, coefficients, 0, body, var, overflow);
389  assert_for_values(program, values, coefficients, 2, body, var, overflow);
390 
391  for(expr_sett::iterator it=influence.begin();
392  it!=influence.end();
393  ++it)
394  {
395  values[*it]=2;
396  }
397 
398  assert_for_values(program, values, coefficients, 2, body, var, overflow);
399 
400 #ifdef DEBUG
401  std::cout << "Fitting polynomial with program:\n";
402  program.output(ns, "", std::cout);
403 #endif
404 
405  // Now do an ASSERT(false) to grab a counterexample
406  goto_programt::targett assertion=program.add_instruction(ASSERT);
407  assertion->guard=false_exprt();
408 
409 
410  // If the path is satisfiable, we've fitted a polynomial. Extract the
411  // relevant coefficients and return the expression.
412  try
413  {
414  if(program.check_sat())
415  {
416  utils.extract_polynomial(program, coefficients, polynomial);
417  return true;
418  }
419  }
420  catch(const std::string &s)
421  {
422  std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
423  }
424  catch(const char *s)
425  {
426  std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
427  }
428 
429  return false;
430 }
431 
434  exprt &target,
435  polynomialt &polynomial)
436 {
438  expr_sett influence;
439 
440  cone_of_influence(body, target, sliced, influence);
441 
442  return fit_polynomial_sliced(sliced, target, influence, polynomial);
443 }
444 
447  exprt &target,
448  polynomialt &poly)
449 {
450  return false;
451 
452 #if 0
454 
455  program.append(body);
456  program.add_instruction(ASSERT)->guard=equal_exprt(target, not_exprt(target));
457 
458  try
459  {
460  if(program.check_sat(false))
461  {
462 #ifdef DEBUG
463  std::cout << "Fitting constant, eval'd to: "
464  << expr2c(program.eval(target), ns) << '\n';
465 #endif
466  constant_exprt val=to_constant_expr(program.eval(target));
467  mp_integer mp=binary2integer(val.get_value().c_str(), true);
468  monomialt mon;
469  monomialt::termt term;
470 
471  term.var=from_integer(1, target.type());
472  term.exp=1;
473  mon.terms.push_back(term);
474  mon.coeff=mp.to_long();
475 
476  poly.monomials.push_back(mon);
477 
478  return true;
479  }
480  }
481  catch(const std::string &s)
482  {
483  std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
484  }
485  catch(const char *s)
486  {
487  std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
488  }
489 
490  return false;
491 #endif
492 }
493 
495  scratch_programt &program,
496  std::map<exprt, int> &values,
497  std::set<std::pair<expr_listt, exprt> > &coefficients,
498  int num_unwindings,
499  goto_programt::instructionst &loop_body,
500  exprt &target,
501  overflow_instrumentert &overflow)
502 {
503  // First figure out what the appropriate type for this expression is.
504  typet expr_type=nil_typet();
505 
506  for(std::map<exprt, int>::iterator it=values.begin();
507  it!=values.end();
508  ++it)
509  {
510  typet this_type=it->first.type();
511  if(this_type.id()==ID_pointer)
512  {
513 #ifdef DEBUG
514  std::cout << "Overriding pointer type\n";
515 #endif
516  this_type=size_type();
517  }
518 
519  if(expr_type==nil_typet())
520  {
521  expr_type=this_type;
522  }
523  else
524  {
525  expr_type=join_types(expr_type, this_type);
526  }
527  }
528 
529  assert(to_bitvector_type(expr_type).get_width()>0);
530 
531 
532  // Now set the initial values of the all the variables...
533  for(std::map<exprt, int>::iterator it=values.begin();
534  it!=values.end();
535  ++it)
536  {
537  program.assign(it->first, from_integer(it->second, expr_type));
538  }
539 
540  // Now unwind the loop as many times as we need to.
541  for(int i=0; i < num_unwindings; i++)
542  {
543  program.append(loop_body);
544  }
545 
546  // Now build the polynomial for this point and assert it fits.
547  exprt rhs=nil_exprt();
548 
549  for(std::set<std::pair<expr_listt, exprt> >::iterator it=coefficients.begin();
550  it!=coefficients.end();
551  ++it)
552  {
553  int concrete_value=1;
554 
555  for(expr_listt::const_iterator e_it=it->first.begin();
556  e_it!=it->first.end();
557  ++e_it)
558  {
559  exprt e=*e_it;
560 
561  if(e==loop_counter)
562  {
563  concrete_value *= num_unwindings;
564  }
565  else
566  {
567  std::map<exprt, int>::iterator v_it=values.find(e);
568 
569  if(v_it!=values.end())
570  {
571  concrete_value *= v_it->second;
572  }
573  }
574  }
575 
576  // OK, concrete_value now contains the value of all the relevant variables
577  // multiplied together. Create the term concrete_value*coefficient and add
578  // it into the polynomial.
579  typecast_exprt cast(it->second, expr_type);
580  const mult_exprt term(from_integer(concrete_value, expr_type), cast);
581 
582  if(rhs.is_nil())
583  {
584  rhs=term;
585  }
586  else
587  {
588  rhs=plus_exprt(rhs, term);
589  }
590  }
591 
592  exprt overflow_expr;
593  overflow.overflow_expr(rhs, overflow_expr);
594 
595  program.add_instruction(ASSUME)->guard=not_exprt(overflow_expr);
596 
597  rhs=typecast_exprt(rhs, target.type());
598 
599  // We now have the RHS of the polynomial. Assert that this is equal to the
600  // actual value of the variable we're fitting.
601  const equal_exprt polynomial_holds(target, rhs);
602 
603  // Finally, assert that the polynomial equals the variable we're fitting.
604  goto_programt::targett assumption=program.add_instruction(ASSUME);
605  assumption->guard=polynomial_holds;
606 }
607 
609  goto_programt::instructionst &orig_body,
610  exprt &target,
612  expr_sett &cone)
613 {
614  utils.gather_rvalues(target, cone);
615 
616  for(goto_programt::instructionst::reverse_iterator r_it=orig_body.rbegin();
617  r_it!=orig_body.rend();
618  ++r_it)
619  {
620  if(r_it->is_assign())
621  {
622  // XXX -- this doesn't work if the assignment is not to a symbol, e.g.
623  // A[i]=0;
624  // or
625  // *p=x;
626  code_assignt assignment=to_code_assign(r_it->code);
627  expr_sett lhs_syms;
628 
629  utils.gather_rvalues(assignment.lhs(), lhs_syms);
630 
631  for(expr_sett::iterator s_it=lhs_syms.begin();
632  s_it!=lhs_syms.end();
633  ++s_it)
634  {
635  if(cone.find(*s_it)!=cone.end())
636  {
637  // We're assigning to something in the cone of influence -- expand the
638  // cone.
639  body.push_front(*r_it);
640  cone.erase(assignment.lhs());
641  utils.gather_rvalues(assignment.rhs(), cone);
642  break;
643  }
644  }
645  }
646  }
647 }
648 
650  std::map<exprt, polynomialt> polynomials,
652 {
653  // Checking that our polynomial is inductive with respect to the loop body is
654  // equivalent to checking safety of the following program:
655  //
656  // assume (target1==polynomial1);
657  // assume (target2==polynomial2)
658  // ...
659  // loop_body;
660  // loop_counter++;
661  // assert (target1==polynomial1);
662  // assert (target2==polynomial2);
663  // ...
665  std::vector<exprt> polynomials_hold;
666  substitutiont substitution;
667 
668  stash_polynomials(program, polynomials, substitution, body);
669 
670  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
671  it!=polynomials.end();
672  ++it)
673  {
674  const equal_exprt holds(it->first, it->second.to_expr());
675  program.add_instruction(ASSUME)->guard=holds;
676 
677  polynomials_hold.push_back(holds);
678  }
679 
680  program.append(body);
681 
682  codet inc_loop_counter=
683  code_assignt(
684  loop_counter,
686  program.add_instruction(ASSIGN)->code=inc_loop_counter;
687 
688  for(std::vector<exprt>::iterator it=polynomials_hold.begin();
689  it!=polynomials_hold.end();
690  ++it)
691  {
692  program.add_instruction(ASSERT)->guard=*it;
693  }
694 
695 #ifdef DEBUG
696  std::cout << "Checking following program for inductiveness:\n";
697  program.output(ns, "", std::cout);
698 #endif
699 
700  try
701  {
702  if(program.check_sat())
703  {
704  // We found a counterexample to inductiveness... :-(
705  #ifdef DEBUG
706  std::cout << "Not inductive!\n";
707  #endif
708  return false;
709  }
710  else
711  {
712  return true;
713  }
714  }
715  catch(const std::string &s)
716  {
717  std::cout << "Error in inductiveness SAT check: " << s << '\n';
718  return false;
719  }
720  catch(const char *s)
721  {
722  std::cout << "Error in inductiveness SAT check: " << s << '\n';
723  return false;
724  }
725 }
726 
728  scratch_programt &program,
729  std::map<exprt, polynomialt> &polynomials,
730  substitutiont &substitution,
732 {
733  expr_sett modified;
734  utils.find_modified(body, modified);
735  stash_variables(program, modified, substitution);
736 
737  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
738  it!=polynomials.end();
739  ++it)
740  {
741  it->second.substitute(substitution);
742  }
743 }
744 
746  scratch_programt &program,
747  expr_sett modified,
748  substitutiont &substitution)
749 {
750  find_symbols_sett vars;
751 
752  for(expr_sett::iterator it=modified.begin();
753  it!=modified.end();
754  ++it)
755  {
756  find_symbols(*it, vars);
757  }
758 
759  irep_idt loop_counter_name=to_symbol_expr(loop_counter).get_identifier();
760  vars.erase(loop_counter_name);
761 
762  for(find_symbols_sett::iterator it=vars.begin();
763  it!=vars.end();
764  ++it)
765  {
766  symbolt orig=*symbol_table.lookup(*it);
767  symbolt stashed_sym=utils.fresh_symbol("polynomial::stash", orig.type);
768  substitution[orig.symbol_expr()]=stashed_sym.symbol_expr();
769  program.assign(stashed_sym.symbol_expr(), orig.symbol_expr());
770  }
771 }
772 
773 /*
774  * Finds a precondition which guarantees that all the assumptions and assertions
775  * along this path hold.
776  *
777  * This is not the weakest precondition, since we make underapproximations due
778  * to aliasing.
779  */
780 
782 {
783  exprt ret=false_exprt();
784 
785  for(patht::reverse_iterator r_it=path.rbegin();
786  r_it!=path.rend();
787  ++r_it)
788  {
789  goto_programt::const_targett t=r_it->loc;
790 
791  if(t->is_assign())
792  {
793  // XXX Need to check for aliasing...
794  const code_assignt &assignment=to_code_assign(t->code);
795  const exprt &lhs=assignment.lhs();
796  const exprt &rhs=assignment.rhs();
797 
798  if(lhs.id()==ID_symbol)
799  {
800  replace_expr(lhs, rhs, ret);
801  }
802  else if(lhs.id()==ID_index ||
803  lhs.id()==ID_dereference)
804  {
805  continue;
806  }
807  else
808  {
809  throw "couldn't take WP of " + expr2c(lhs, ns) + "=" + expr2c(rhs, ns);
810  }
811  }
812  else if(t->is_assume() || t->is_assert())
813  {
814  ret=implies_exprt(t->guard, ret);
815  }
816  else
817  {
818  // Ignore.
819  }
820 
821  if(!r_it->guard.is_true() && !r_it->guard.is_nil())
822  {
823  // The guard isn't constant true, so we need to accumulate that too.
824  ret=implies_exprt(r_it->guard, ret);
825  }
826  }
827 
828  simplify(ret, ns);
829 
830  return ret;
831 }
std::list< exprt > expr_listt
bool is_bitvector(const typet &t)
Convenience function – is the type a bitvector of some kind?
Definition: util.cpp:33
The type of an expression.
Definition: type.h:22
Boolean negation.
Definition: std_expr.h:3230
semantic type conversion
Definition: std_expr.h:2111
BigInt mp_integer
Definition: mp_arith.h:22
bool is_nil() const
Definition: irep.h:102
A generic base class for relations, i.e., binary predicates.
Definition: std_expr.h:752
Generate Equation using Symbolic Execution.
targett assign(const exprt &lhs, const exprt &rhs)
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a generic typet to a bitvector_typet.
Definition: std_types.h:1150
std::ostream & output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
Output goto program to given stream.
const irep_idt & get_identifier() const
Definition: std_expr.h:128
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:120
typet & type()
Definition: expr.h:56
unsignedbv_typet size_type()
Definition: c_types.cpp:58
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
A constant literal expression.
Definition: std_expr.h:4424
void assert_for_values(scratch_programt &program, std::map< exprt, int > &values, std::set< std::pair< expr_listt, exprt >> &coefficients, int num_unwindings, goto_programt::instructionst &loop_body, exprt &target, overflow_instrumentert &overflow)
boolean implication
Definition: std_expr.h:2339
equality
Definition: std_expr.h:1354
std::list< instructiont > instructionst
Definition: goto_program.h:395
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:239
const irep_idt & id() const
Definition: irep.h:189
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
exprt & lhs()
Definition: std_code.h:208
class symbol_exprt symbol_expr() const
produces a symbol_exprt for a symbol
Definition: symbol.cpp:111
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
The NIL expression.
Definition: std_expr.h:4510
symbolt fresh_symbol(std::string base, typet type)
exprt & rhs()
Definition: std_code.h:213
exprt eval(const exprt &e)
Fixed-width bit-vector with two&#39;s complement interpretation.
Definition: std_types.h:1262
Symbolic Execution.
virtual bool accelerate(patht &loop, path_acceleratort &accelerator)
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
instructionst::const_iterator const_targett
Definition: goto_program.h:398
bool do_nonrecursive(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, exprt &loop_counter, substitutiont &substitution, expr_sett &nonrecursive, scratch_programt &program)
bool check_inductive(std::map< exprt, polynomialt > polynomials, goto_programt::instructionst &body)
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:1301
A forall expression.
Definition: std_expr.h:4860
The plus expression.
Definition: std_expr.h:893
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
Program Transformation.
message_handlert & message_handler
Loop Acceleration.
void extract_polynomial(scratch_programt &program, std::set< std::pair< expr_listt, exprt > > &coefficients, polynomialt &polynomial)
void overflow_expr(const exprt &expr, expr_sett &cases)
void stash_polynomials(scratch_programt &program, std::map< exprt, polynomialt > &polynomials, std::map< exprt, exprt > &stashed, goto_programt::instructionst &body)
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
const constant_exprt & to_constant_expr(const exprt &expr)
Cast a generic exprt to a constant_exprt.
Definition: std_expr.h:4465
The boolean constant false.
Definition: std_expr.h:4499
void gather_rvalues(const exprt &expr, expr_sett &rvalues)
binary multiplication
Definition: std_expr.h:1017
bool fit_polynomial(goto_programt::instructionst &loop_body, exprt &target, polynomialt &polynomial)
bool do_assumptions(std::map< exprt, polynomialt > polynomials, patht &body, exprt &guard)
typet type
Type of symbol.
Definition: symbol.h:34
Loop Acceleration.
void cone_of_influence(goto_programt::instructionst &orig_body, exprt &target, goto_programt::instructionst &body, expr_sett &influence)
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
unsigned int exp
Definition: polynomial.h:26
std::map< exprt, exprt > substitutiont
Definition: polynomial.h:39
goto_programt pure_accelerator
Definition: accelerator.h:63
bool fit_const(goto_programt::instructionst &loop_body, exprt &target, polynomialt &polynomial)
The NIL type.
Definition: std_types.h:44
std::string expr2c(const exprt &expr, const namespacet &ns)
Definition: expr2c.cpp:3967
binary minus
Definition: std_expr.h:959
void stash_variables(scratch_programt &program, expr_sett modified, substitutiont &substitution)
Expression to hold a symbol (variable)
Definition: std_expr.h:90
Options.
A statement in a programming language.
Definition: std_code.h:21
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:20
Loop Acceleration.
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
void find_symbols(const exprt &src, find_symbols_sett &dest)
Concrete Goto Program.
bool fit_polynomial_sliced(goto_programt::instructionst &sliced_body, exprt &target, expr_sett &influence, polynomialt &polynomial)
Assignment.
Definition: std_code.h:195
std::vector< monomialt > monomials
Definition: polynomial.h:46
bool simplify(exprt &expr, const namespacet &ns)