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 
240  program.assign(
241  loop_counter,
244 
245  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
246  it!=polynomials.end();
247  ++it)
248  {
249  program.assign(it->first, it->second.to_expr());
250  }
251 
252  // Add in any array assignments we can do now.
254  assigns, polynomials, stashed, nonrecursive, program))
255  {
256  // We couldn't model some of the array assignments with polynomials...
257  // Unfortunately that means we just have to bail out.
258 #ifdef DEBUG
259  std::cout << "Failed to accelerate a nonrecursive expression\n";
260 #endif
261  return false;
262  }
263 
264  program.add_instruction(ASSUME)->guard=guard_last;
265  program.fix_types();
266 
267  if(path_is_monotone)
268  {
269  utils.ensure_no_overflows(program);
270  }
271 
272  accelerator.pure_accelerator.instructions.swap(program.instructions);
273 
274  return true;
275 }
276 
279  exprt &var,
280  expr_sett &influence,
281  polynomialt &polynomial)
282 {
283  // These are the variables that var depends on with respect to the body.
284  std::vector<expr_listt> parameters;
285  std::set<std::pair<expr_listt, exprt> > coefficients;
286  expr_listt exprs;
288  exprt overflow_var =
289  utils.fresh_symbol("polynomial::overflow", bool_typet()).symbol_expr();
290  overflow_instrumentert overflow(program, overflow_var, symbol_table);
291 
292 #ifdef DEBUG
293  std::cout << "Fitting a polynomial for " << expr2c(var, ns)
294  << ", which depends on:\n";
295 
296  for(expr_sett::iterator it=influence.begin();
297  it!=influence.end();
298  ++it)
299  {
300  std::cout << expr2c(*it, ns) << '\n';
301  }
302 #endif
303 
304  for(expr_sett::iterator it=influence.begin();
305  it!=influence.end();
306  ++it)
307  {
308  if(it->id()==ID_index ||
309  it->id()==ID_dereference)
310  {
311  // Hack: don't accelerate variables that depend on arrays...
312  return false;
313  }
314 
315  exprs.clear();
316 
317  exprs.push_back(*it);
318  parameters.push_back(exprs);
319 
320  exprs.push_back(loop_counter);
321  parameters.push_back(exprs);
322  }
323 
324  // N
325  exprs.clear();
326  exprs.push_back(loop_counter);
327  parameters.push_back(exprs);
328 
329  // N^2
330  exprs.push_back(loop_counter);
331  // parameters.push_back(exprs);
332 
333  // Constant
334  exprs.clear();
335  parameters.push_back(exprs);
336 
337  if(!is_bitvector(var.type()))
338  {
339  // We don't really know how to accelerate non-bitvectors anyway...
340  return false;
341  }
342 
343  std::size_t width=to_bitvector_type(var.type()).get_width();
344  assert(width>0);
345 
346  for(std::vector<expr_listt>::iterator it=parameters.begin();
347  it!=parameters.end();
348  ++it)
349  {
350  symbolt coeff=utils.fresh_symbol("polynomial::coeff",
351  signedbv_typet(width));
352  coefficients.insert(std::make_pair(*it, coeff.symbol_expr()));
353  }
354 
355  // Build a set of values for all the parameters that allow us to fit a
356  // unique polynomial.
357 
358  // XXX
359  // This isn't ok -- we're assuming 0, 1 and 2 are valid values for the
360  // variables involved, but this might make the path condition UNSAT. Should
361  // really be solving the path constraints a few times to get valid probe
362  // values...
363 
364  std::map<exprt, int> values;
365 
366  for(expr_sett::iterator it=influence.begin();
367  it!=influence.end();
368  ++it)
369  {
370  values[*it]=0;
371  }
372 
373 #ifdef DEBUG
374  std::cout << "Fitting polynomial over " << values.size()
375  << " variables\n";
376 #endif
377 
378  for(int n=0; n<=2; n++)
379  {
380  for(expr_sett::iterator it=influence.begin();
381  it!=influence.end();
382  ++it)
383  {
384  values[*it]=1;
385  assert_for_values(program, values, coefficients, n, body, var, overflow);
386  values[*it]=0;
387  }
388  }
389 
390  // Now just need to assert the case where all values are 0 and all are 2.
391  assert_for_values(program, values, coefficients, 0, body, var, overflow);
392  assert_for_values(program, values, coefficients, 2, body, var, overflow);
393 
394  for(expr_sett::iterator it=influence.begin();
395  it!=influence.end();
396  ++it)
397  {
398  values[*it]=2;
399  }
400 
401  assert_for_values(program, values, coefficients, 2, body, var, overflow);
402 
403 #ifdef DEBUG
404  std::cout << "Fitting polynomial with program:\n";
405  program.output(ns, "", std::cout);
406 #endif
407 
408  // Now do an ASSERT(false) to grab a counterexample
409  goto_programt::targett assertion=program.add_instruction(ASSERT);
410  assertion->guard=false_exprt();
411 
412 
413  // If the path is satisfiable, we've fitted a polynomial. Extract the
414  // relevant coefficients and return the expression.
415  try
416  {
417  if(program.check_sat())
418  {
419  utils.extract_polynomial(program, coefficients, polynomial);
420  return true;
421  }
422  }
423  catch(const std::string &s)
424  {
425  std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
426  }
427  catch(const char *s)
428  {
429  std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
430  }
431 
432  return false;
433 }
434 
437  exprt &target,
438  polynomialt &polynomial)
439 {
441  expr_sett influence;
442 
443  cone_of_influence(body, target, sliced, influence);
444 
445  return fit_polynomial_sliced(sliced, target, influence, polynomial);
446 }
447 
450  exprt &target,
451  polynomialt &poly)
452 {
453  // unused parameters
454  (void)body;
455  (void)target;
456  (void)poly;
457  return false;
458 
459 #if 0
461 
462  program.append(body);
463  program.add_instruction(ASSERT)->guard=equal_exprt(target, not_exprt(target));
464 
465  try
466  {
467  if(program.check_sat(false))
468  {
469 #ifdef DEBUG
470  std::cout << "Fitting constant, eval'd to: "
471  << expr2c(program.eval(target), ns) << '\n';
472 #endif
473  constant_exprt val=to_constant_expr(program.eval(target));
474  mp_integer mp=binary2integer(val.get_value().c_str(), true);
475  monomialt mon;
476  monomialt::termt term;
477 
478  term.var=from_integer(1, target.type());
479  term.exp=1;
480  mon.terms.push_back(term);
481  mon.coeff=mp.to_long();
482 
483  poly.monomials.push_back(mon);
484 
485  return true;
486  }
487  }
488  catch(const std::string &s)
489  {
490  std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
491  }
492  catch(const char *s)
493  {
494  std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
495  }
496 
497  return false;
498 #endif
499 }
500 
502  scratch_programt &program,
503  std::map<exprt, int> &values,
504  std::set<std::pair<expr_listt, exprt> > &coefficients,
505  int num_unwindings,
506  goto_programt::instructionst &loop_body,
507  exprt &target,
508  overflow_instrumentert &overflow)
509 {
510  // First figure out what the appropriate type for this expression is.
511  typet expr_type=nil_typet();
512 
513  for(std::map<exprt, int>::iterator it=values.begin();
514  it!=values.end();
515  ++it)
516  {
517  typet this_type=it->first.type();
518  if(this_type.id()==ID_pointer)
519  {
520 #ifdef DEBUG
521  std::cout << "Overriding pointer type\n";
522 #endif
523  this_type=size_type();
524  }
525 
526  if(expr_type==nil_typet())
527  {
528  expr_type=this_type;
529  }
530  else
531  {
532  expr_type=join_types(expr_type, this_type);
533  }
534  }
535 
536  assert(to_bitvector_type(expr_type).get_width()>0);
537 
538 
539  // Now set the initial values of the all the variables...
540  for(std::map<exprt, int>::iterator it=values.begin();
541  it!=values.end();
542  ++it)
543  {
544  program.assign(it->first, from_integer(it->second, expr_type));
545  }
546 
547  // Now unwind the loop as many times as we need to.
548  for(int i=0; i < num_unwindings; i++)
549  {
550  program.append(loop_body);
551  }
552 
553  // Now build the polynomial for this point and assert it fits.
554  exprt rhs=nil_exprt();
555 
556  for(std::set<std::pair<expr_listt, exprt> >::iterator it=coefficients.begin();
557  it!=coefficients.end();
558  ++it)
559  {
560  int concrete_value=1;
561 
562  for(expr_listt::const_iterator e_it=it->first.begin();
563  e_it!=it->first.end();
564  ++e_it)
565  {
566  exprt e=*e_it;
567 
568  if(e==loop_counter)
569  {
570  concrete_value *= num_unwindings;
571  }
572  else
573  {
574  std::map<exprt, int>::iterator v_it=values.find(e);
575 
576  if(v_it!=values.end())
577  {
578  concrete_value *= v_it->second;
579  }
580  }
581  }
582 
583  // OK, concrete_value now contains the value of all the relevant variables
584  // multiplied together. Create the term concrete_value*coefficient and add
585  // it into the polynomial.
586  typecast_exprt cast(it->second, expr_type);
587  const mult_exprt term(from_integer(concrete_value, expr_type), cast);
588 
589  if(rhs.is_nil())
590  {
591  rhs=term;
592  }
593  else
594  {
595  rhs=plus_exprt(rhs, term);
596  }
597  }
598 
599  exprt overflow_expr;
600  overflow.overflow_expr(rhs, overflow_expr);
601 
602  program.add_instruction(ASSUME)->guard=not_exprt(overflow_expr);
603 
604  rhs=typecast_exprt(rhs, target.type());
605 
606  // We now have the RHS of the polynomial. Assert that this is equal to the
607  // actual value of the variable we're fitting.
608  const equal_exprt polynomial_holds(target, rhs);
609 
610  // Finally, assert that the polynomial equals the variable we're fitting.
611  goto_programt::targett assumption=program.add_instruction(ASSUME);
612  assumption->guard=polynomial_holds;
613 }
614 
616  goto_programt::instructionst &orig_body,
617  exprt &target,
619  expr_sett &cone)
620 {
621  utils.gather_rvalues(target, cone);
622 
623  for(goto_programt::instructionst::reverse_iterator r_it=orig_body.rbegin();
624  r_it!=orig_body.rend();
625  ++r_it)
626  {
627  if(r_it->is_assign())
628  {
629  // XXX -- this doesn't work if the assignment is not to a symbol, e.g.
630  // A[i]=0;
631  // or
632  // *p=x;
633  code_assignt assignment=to_code_assign(r_it->code);
634  expr_sett lhs_syms;
635 
636  utils.gather_rvalues(assignment.lhs(), lhs_syms);
637 
638  for(expr_sett::iterator s_it=lhs_syms.begin();
639  s_it!=lhs_syms.end();
640  ++s_it)
641  {
642  if(cone.find(*s_it)!=cone.end())
643  {
644  // We're assigning to something in the cone of influence -- expand the
645  // cone.
646  body.push_front(*r_it);
647  cone.erase(assignment.lhs());
648  utils.gather_rvalues(assignment.rhs(), cone);
649  break;
650  }
651  }
652  }
653  }
654 }
655 
657  std::map<exprt, polynomialt> polynomials,
659 {
660  // Checking that our polynomial is inductive with respect to the loop body is
661  // equivalent to checking safety of the following program:
662  //
663  // assume (target1==polynomial1);
664  // assume (target2==polynomial2)
665  // ...
666  // loop_body;
667  // loop_counter++;
668  // assert (target1==polynomial1);
669  // assert (target2==polynomial2);
670  // ...
672  std::vector<exprt> polynomials_hold;
673  substitutiont substitution;
674 
675  stash_polynomials(program, polynomials, substitution, body);
676 
677  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
678  it!=polynomials.end();
679  ++it)
680  {
681  const equal_exprt holds(it->first, it->second.to_expr());
682  program.add_instruction(ASSUME)->guard=holds;
683 
684  polynomials_hold.push_back(holds);
685  }
686 
687  program.append(body);
688 
689  codet inc_loop_counter=
690  code_assignt(
691  loop_counter,
693  program.add_instruction(ASSIGN)->code=inc_loop_counter;
694 
695  for(std::vector<exprt>::iterator it=polynomials_hold.begin();
696  it!=polynomials_hold.end();
697  ++it)
698  {
699  program.add_instruction(ASSERT)->guard=*it;
700  }
701 
702 #ifdef DEBUG
703  std::cout << "Checking following program for inductiveness:\n";
704  program.output(ns, "", std::cout);
705 #endif
706 
707  try
708  {
709  if(program.check_sat())
710  {
711  // We found a counterexample to inductiveness... :-(
712  #ifdef DEBUG
713  std::cout << "Not inductive!\n";
714  #endif
715  return false;
716  }
717  else
718  {
719  return true;
720  }
721  }
722  catch(const std::string &s)
723  {
724  std::cout << "Error in inductiveness SAT check: " << s << '\n';
725  return false;
726  }
727  catch(const char *s)
728  {
729  std::cout << "Error in inductiveness SAT check: " << s << '\n';
730  return false;
731  }
732 }
733 
735  scratch_programt &program,
736  std::map<exprt, polynomialt> &polynomials,
737  substitutiont &substitution,
739 {
740  expr_sett modified;
741  utils.find_modified(body, modified);
742  stash_variables(program, modified, substitution);
743 
744  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
745  it!=polynomials.end();
746  ++it)
747  {
748  it->second.substitute(substitution);
749  }
750 }
751 
753  scratch_programt &program,
754  expr_sett modified,
755  substitutiont &substitution)
756 {
757  find_symbols_sett vars;
758 
759  for(expr_sett::iterator it=modified.begin();
760  it!=modified.end();
761  ++it)
762  {
763  find_symbols(*it, vars);
764  }
765 
766  irep_idt loop_counter_name=to_symbol_expr(loop_counter).get_identifier();
767  vars.erase(loop_counter_name);
768 
769  for(find_symbols_sett::iterator it=vars.begin();
770  it!=vars.end();
771  ++it)
772  {
773  symbolt orig=*symbol_table.lookup(*it);
774  symbolt stashed_sym=utils.fresh_symbol("polynomial::stash", orig.type);
775  substitution[orig.symbol_expr()]=stashed_sym.symbol_expr();
776  program.assign(stashed_sym.symbol_expr(), orig.symbol_expr());
777  }
778 }
779 
780 /*
781  * Finds a precondition which guarantees that all the assumptions and assertions
782  * along this path hold.
783  *
784  * This is not the weakest precondition, since we make underapproximations due
785  * to aliasing.
786  */
787 
789 {
790  exprt ret=false_exprt();
791 
792  for(patht::reverse_iterator r_it=path.rbegin();
793  r_it!=path.rend();
794  ++r_it)
795  {
796  goto_programt::const_targett t=r_it->loc;
797 
798  if(t->is_assign())
799  {
800  // XXX Need to check for aliasing...
801  const code_assignt &assignment=to_code_assign(t->code);
802  const exprt &lhs=assignment.lhs();
803  const exprt &rhs=assignment.rhs();
804 
805  if(lhs.id()==ID_symbol)
806  {
807  replace_expr(lhs, rhs, ret);
808  }
809  else if(lhs.id()==ID_index ||
810  lhs.id()==ID_dereference)
811  {
812  continue;
813  }
814  else
815  {
816  throw "couldn't take WP of " + expr2c(lhs, ns) + "=" + expr2c(rhs, ns);
817  }
818  }
819  else if(t->is_assume() || t->is_assert())
820  {
821  ret=implies_exprt(t->guard, ret);
822  }
823  else
824  {
825  // Ignore.
826  }
827 
828  if(!r_it->guard.is_true() && !r_it->guard.is_nil())
829  {
830  // The guard isn't constant true, so we need to accumulate that too.
831  ret=implies_exprt(r_it->guard, ret);
832  }
833  }
834 
835  simplify(ret, ns);
836 
837  return ret;
838 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
symex_target_equation.h
overflow_instrumenter.h
polynomialt
Definition: polynomial.h:41
polynomial_acceleratort::message_handler
message_handlert & message_handler
Definition: polynomial_accelerator.h:69
arith_tools.h
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
polynomial_acceleratort::cone_of_influence
void cone_of_influence(goto_programt::instructionst &orig_body, exprt &target, goto_programt::instructionst &body, expr_sett &influence)
Definition: polynomial_accelerator.cpp:615
typet
The type of an expression, extends irept.
Definition: type.h:27
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:274
polynomial_acceleratort::fit_polynomial_sliced
bool fit_polynomial_sliced(goto_programt::instructionst &sliced_body, exprt &target, expr_sett &influence, polynomialt &polynomial)
Definition: polynomial_accelerator.cpp:277
acceleration_utilst::fresh_symbol
symbolt fresh_symbol(std::string base, typet type)
Definition: acceleration_utils.cpp:1271
expr_listt
std::list< exprt > expr_listt
Definition: acceleration_utils.h:34
symbolt::type
typet type
Type of symbol.
Definition: symbol.h:31
polynomial_acceleratort::fit_const
bool fit_const(goto_programt::instructionst &loop_body, exprt &target, polynomialt &polynomial)
Definition: polynomial_accelerator.cpp:448
is_bitvector
bool is_bitvector(const typet &t)
Convenience function – is the type a bitvector of some kind?
Definition: util.cpp:33
goto_programt::instructionst
std::list< instructiont > instructionst
Definition: goto_program.h:412
mp_integer
BigInt mp_integer
Definition: mp_arith.h:22
nil_typet
The NIL type, i.e., an invalid type, no value.
Definition: std_types.h:39
monomialt::termt::exp
unsigned int exp
Definition: polynomial.h:26
polynomial_acceleratort::stash_polynomials
void stash_polynomials(scratch_programt &program, std::map< exprt, polynomialt > &polynomials, std::map< exprt, exprt > &stashed, goto_programt::instructionst &body)
Definition: polynomial_accelerator.cpp:734
and_exprt
Boolean AND.
Definition: std_expr.h:2409
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:1042
exprt
Base class for all expressions.
Definition: expr.h:54
polynomial_acceleratort::symbol_table
symbol_tablet & symbol_table
Definition: polynomial_accelerator.h:153
options.h
bool_typet
The Boolean type.
Definition: std_types.h:28
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
polynomial_acceleratort::accelerate
bool accelerate(patht &loop, path_acceleratort &accelerator)
Definition: polynomial_accelerator.cpp:45
polynomialt::monomials
std::vector< monomialt > monomials
Definition: polynomial.h:46
equal_exprt
Equality.
Definition: std_expr.h:1484
polynomial_acceleratort::precondition
exprt precondition(patht &path)
Definition: polynomial_accelerator.cpp:788
polynomial_acceleratort::ns
const namespacet ns
Definition: polynomial_accelerator.h:154
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
goto_programt::add_instruction
targett add_instruction()
Adds an instruction at the end.
Definition: goto_program.h:541
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:68
find_symbols
void find_symbols(const exprt &src, find_symbols_sett &dest)
Definition: find_symbols.cpp:16
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
polynomial_acceleratort::stash_variables
void stash_variables(scratch_programt &program, expr_sett modified, substitutiont &substitution)
Definition: polynomial_accelerator.cpp:752
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
goto_programt::output
std::ostream & output(const namespacet &ns, const irep_idt &identifier, std::ostream &out) const
Output goto program to given stream.
Definition: goto_program.cpp:514
monomialt
Definition: polynomial.h: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
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:176
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
polynomial_acceleratort::check_inductive
bool check_inductive(std::map< exprt, polynomialt > polynomials, goto_programt::instructionst &body)
Definition: polynomial_accelerator.cpp:656
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:269
scratch_programt::check_sat
bool check_sat(bool do_slice)
Definition: scratch_program.cpp:25
monomialt::termt::var
exprt var
Definition: polynomial.h:25
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2320
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
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:251
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
goto_check.h
overflow_instrumentert
Definition: overflow_instrumenter.h:25
std_code.h
minus_exprt
Binary minus.
Definition: std_expr.h:1106
goto_program.h
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
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
monomialt::termt
Definition: polynomial.h:23
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:420
ASSIGN
Definition: goto_program.h:46
find_symbols_sett
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:20
acceleration_utilst::check_inductive
bool check_inductive(std::map< exprt, polynomialt > polynomials, patht &path)
Definition: acceleration_utils.cpp:114
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:334
patht
std::list< path_nodet > patht
Definition: path.h:45
accelerator.h
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
binary2integer
const mp_integer binary2integer(const std::string &n, bool is_signed)
convert binary string representation to mp_integer
Definition: mp_arith.cpp:120
cone_of_influence.h
binary_relation_exprt
A base class for relations, i.e., binary predicates.
Definition: std_expr.h:878
polynomial_acceleratort::loop_counter
exprt loop_counter
Definition: polynomial_accelerator.h:158
symbol_table_baset::lookup
const symbolt * lookup(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:86
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:415
polynomial_acceleratort::assert_for_values
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)
Definition: polynomial_accelerator.cpp:501
implies_exprt
Boolean implication.
Definition: std_expr.h:2485
replace_expr.h
polynomial_acceleratort::nonrecursive
expr_sett nonrecursive
Definition: polynomial_accelerator.h:160
symbol_table.h
Author: Diffblue Ltd.
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2277
size_type
unsignedbv_typet size_type()
Definition: c_types.cpp:58
code_assignt
A codet representing an assignment in the program.
Definition: std_code.h:256
constant_exprt
A constant literal expression.
Definition: std_expr.h:4384
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
acceleration_utilst::gather_rvalues
void gather_rvalues(const exprt &expr, expr_sett &rvalues)
Definition: acceleration_utils.cpp:47
util.h
overflow_instrumentert::overflow_expr
void overflow_expr(const exprt &expr, expr_sett &cases)
Definition: overflow_instrumenter.cpp:94
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:228
c_types.h
acceleration_utilst::do_assumptions
bool do_assumptions(std::map< exprt, polynomialt > polynomials, patht &body, exprt &guard)
Definition: acceleration_utils.cpp:357
polynomial_acceleratort::utils
acceleration_utilst utils
Definition: polynomial_accelerator.h:156
polynomial_accelerator.h
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:414
wp.h
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1158
codet
Data structure for representing an arbitrary statement in a program.
Definition: std_code.h:34
not_exprt
Boolean negation.
Definition: std_expr.h:3308
acceleration_utilst::do_nonrecursive
bool do_nonrecursive(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, substitutiont &substitution, expr_sett &nonrecursive, scratch_programt &program)
Definition: acceleration_utils.cpp:880
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:4423