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