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, loop_counter, 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  return false;
454 
455 #if 0
457 
458  program.append(body);
459  program.add_instruction(ASSERT)->guard=equal_exprt(target, not_exprt(target));
460 
461  try
462  {
463  if(program.check_sat(false))
464  {
465 #ifdef DEBUG
466  std::cout << "Fitting constant, eval'd to: "
467  << expr2c(program.eval(target), ns) << '\n';
468 #endif
469  constant_exprt val=to_constant_expr(program.eval(target));
470  mp_integer mp=binary2integer(val.get_value().c_str(), true);
471  monomialt mon;
472  monomialt::termt term;
473 
474  term.var=from_integer(1, target.type());
475  term.exp=1;
476  mon.terms.push_back(term);
477  mon.coeff=mp.to_long();
478 
479  poly.monomials.push_back(mon);
480 
481  return true;
482  }
483  }
484  catch(const std::string &s)
485  {
486  std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
487  }
488  catch(const char *s)
489  {
490  std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
491  }
492 
493  return false;
494 #endif
495 }
496 
498  scratch_programt &program,
499  std::map<exprt, int> &values,
500  std::set<std::pair<expr_listt, exprt> > &coefficients,
501  int num_unwindings,
502  goto_programt::instructionst &loop_body,
503  exprt &target,
504  overflow_instrumentert &overflow)
505 {
506  // First figure out what the appropriate type for this expression is.
507  typet expr_type=nil_typet();
508 
509  for(std::map<exprt, int>::iterator it=values.begin();
510  it!=values.end();
511  ++it)
512  {
513  typet this_type=it->first.type();
514  if(this_type.id()==ID_pointer)
515  {
516 #ifdef DEBUG
517  std::cout << "Overriding pointer type\n";
518 #endif
519  this_type=size_type();
520  }
521 
522  if(expr_type==nil_typet())
523  {
524  expr_type=this_type;
525  }
526  else
527  {
528  expr_type=join_types(expr_type, this_type);
529  }
530  }
531 
532  assert(to_bitvector_type(expr_type).get_width()>0);
533 
534 
535  // Now set the initial values of the all the variables...
536  for(std::map<exprt, int>::iterator it=values.begin();
537  it!=values.end();
538  ++it)
539  {
540  program.assign(it->first, from_integer(it->second, expr_type));
541  }
542 
543  // Now unwind the loop as many times as we need to.
544  for(int i=0; i < num_unwindings; i++)
545  {
546  program.append(loop_body);
547  }
548 
549  // Now build the polynomial for this point and assert it fits.
550  exprt rhs=nil_exprt();
551 
552  for(std::set<std::pair<expr_listt, exprt> >::iterator it=coefficients.begin();
553  it!=coefficients.end();
554  ++it)
555  {
556  int concrete_value=1;
557 
558  for(expr_listt::const_iterator e_it=it->first.begin();
559  e_it!=it->first.end();
560  ++e_it)
561  {
562  exprt e=*e_it;
563 
564  if(e==loop_counter)
565  {
566  concrete_value *= num_unwindings;
567  }
568  else
569  {
570  std::map<exprt, int>::iterator v_it=values.find(e);
571 
572  if(v_it!=values.end())
573  {
574  concrete_value *= v_it->second;
575  }
576  }
577  }
578 
579  // OK, concrete_value now contains the value of all the relevant variables
580  // multiplied together. Create the term concrete_value*coefficient and add
581  // it into the polynomial.
582  typecast_exprt cast(it->second, expr_type);
583  const mult_exprt term(from_integer(concrete_value, expr_type), cast);
584 
585  if(rhs.is_nil())
586  {
587  rhs=term;
588  }
589  else
590  {
591  rhs=plus_exprt(rhs, term);
592  }
593  }
594 
595  exprt overflow_expr;
596  overflow.overflow_expr(rhs, overflow_expr);
597 
598  program.add_instruction(ASSUME)->guard=not_exprt(overflow_expr);
599 
600  rhs=typecast_exprt(rhs, target.type());
601 
602  // We now have the RHS of the polynomial. Assert that this is equal to the
603  // actual value of the variable we're fitting.
604  const equal_exprt polynomial_holds(target, rhs);
605 
606  // Finally, assert that the polynomial equals the variable we're fitting.
607  goto_programt::targett assumption=program.add_instruction(ASSUME);
608  assumption->guard=polynomial_holds;
609 }
610 
612  goto_programt::instructionst &orig_body,
613  exprt &target,
615  expr_sett &cone)
616 {
617  utils.gather_rvalues(target, cone);
618 
619  for(goto_programt::instructionst::reverse_iterator r_it=orig_body.rbegin();
620  r_it!=orig_body.rend();
621  ++r_it)
622  {
623  if(r_it->is_assign())
624  {
625  // XXX -- this doesn't work if the assignment is not to a symbol, e.g.
626  // A[i]=0;
627  // or
628  // *p=x;
629  code_assignt assignment=to_code_assign(r_it->code);
630  expr_sett lhs_syms;
631 
632  utils.gather_rvalues(assignment.lhs(), lhs_syms);
633 
634  for(expr_sett::iterator s_it=lhs_syms.begin();
635  s_it!=lhs_syms.end();
636  ++s_it)
637  {
638  if(cone.find(*s_it)!=cone.end())
639  {
640  // We're assigning to something in the cone of influence -- expand the
641  // cone.
642  body.push_front(*r_it);
643  cone.erase(assignment.lhs());
644  utils.gather_rvalues(assignment.rhs(), cone);
645  break;
646  }
647  }
648  }
649  }
650 }
651 
653  std::map<exprt, polynomialt> polynomials,
655 {
656  // Checking that our polynomial is inductive with respect to the loop body is
657  // equivalent to checking safety of the following program:
658  //
659  // assume (target1==polynomial1);
660  // assume (target2==polynomial2)
661  // ...
662  // loop_body;
663  // loop_counter++;
664  // assert (target1==polynomial1);
665  // assert (target2==polynomial2);
666  // ...
668  std::vector<exprt> polynomials_hold;
669  substitutiont substitution;
670 
671  stash_polynomials(program, polynomials, substitution, body);
672 
673  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
674  it!=polynomials.end();
675  ++it)
676  {
677  const equal_exprt holds(it->first, it->second.to_expr());
678  program.add_instruction(ASSUME)->guard=holds;
679 
680  polynomials_hold.push_back(holds);
681  }
682 
683  program.append(body);
684 
685  codet inc_loop_counter=
686  code_assignt(
687  loop_counter,
689  program.add_instruction(ASSIGN)->code=inc_loop_counter;
690 
691  for(std::vector<exprt>::iterator it=polynomials_hold.begin();
692  it!=polynomials_hold.end();
693  ++it)
694  {
695  program.add_instruction(ASSERT)->guard=*it;
696  }
697 
698 #ifdef DEBUG
699  std::cout << "Checking following program for inductiveness:\n";
700  program.output(ns, "", std::cout);
701 #endif
702 
703  try
704  {
705  if(program.check_sat())
706  {
707  // We found a counterexample to inductiveness... :-(
708  #ifdef DEBUG
709  std::cout << "Not inductive!\n";
710  #endif
711  return false;
712  }
713  else
714  {
715  return true;
716  }
717  }
718  catch(const std::string &s)
719  {
720  std::cout << "Error in inductiveness SAT check: " << s << '\n';
721  return false;
722  }
723  catch(const char *s)
724  {
725  std::cout << "Error in inductiveness SAT check: " << s << '\n';
726  return false;
727  }
728 }
729 
731  scratch_programt &program,
732  std::map<exprt, polynomialt> &polynomials,
733  substitutiont &substitution,
735 {
736  expr_sett modified;
737  utils.find_modified(body, modified);
738  stash_variables(program, modified, substitution);
739 
740  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
741  it!=polynomials.end();
742  ++it)
743  {
744  it->second.substitute(substitution);
745  }
746 }
747 
749  scratch_programt &program,
750  expr_sett modified,
751  substitutiont &substitution)
752 {
753  find_symbols_sett vars;
754 
755  for(expr_sett::iterator it=modified.begin();
756  it!=modified.end();
757  ++it)
758  {
759  find_symbols(*it, vars);
760  }
761 
762  irep_idt loop_counter_name=to_symbol_expr(loop_counter).get_identifier();
763  vars.erase(loop_counter_name);
764 
765  for(find_symbols_sett::iterator it=vars.begin();
766  it!=vars.end();
767  ++it)
768  {
769  symbolt orig=*symbol_table.lookup(*it);
770  symbolt stashed_sym=utils.fresh_symbol("polynomial::stash", orig.type);
771  substitution[orig.symbol_expr()]=stashed_sym.symbol_expr();
772  program.assign(stashed_sym.symbol_expr(), orig.symbol_expr());
773  }
774 }
775 
776 /*
777  * Finds a precondition which guarantees that all the assumptions and assertions
778  * along this path hold.
779  *
780  * This is not the weakest precondition, since we make underapproximations due
781  * to aliasing.
782  */
783 
785 {
786  exprt ret=false_exprt();
787 
788  for(patht::reverse_iterator r_it=path.rbegin();
789  r_it!=path.rend();
790  ++r_it)
791  {
792  goto_programt::const_targett t=r_it->loc;
793 
794  if(t->is_assign())
795  {
796  // XXX Need to check for aliasing...
797  const code_assignt &assignment=to_code_assign(t->code);
798  const exprt &lhs=assignment.lhs();
799  const exprt &rhs=assignment.rhs();
800 
801  if(lhs.id()==ID_symbol)
802  {
803  replace_expr(lhs, rhs, ret);
804  }
805  else if(lhs.id()==ID_index ||
806  lhs.id()==ID_dereference)
807  {
808  continue;
809  }
810  else
811  {
812  throw "couldn't take WP of " + expr2c(lhs, ns) + "=" + expr2c(rhs, ns);
813  }
814  }
815  else if(t->is_assume() || t->is_assert())
816  {
817  ret=implies_exprt(t->guard, ret);
818  }
819  else
820  {
821  // Ignore.
822  }
823 
824  if(!r_it->guard.is_true() && !r_it->guard.is_nil())
825  {
826  // The guard isn't constant true, so we need to accumulate that too.
827  ret=implies_exprt(r_it->guard, ret);
828  }
829  }
830 
831  simplify(ret, ns);
832 
833  return ret;
834 }
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:3228
semantic type conversion
Definition: std_expr.h:2111
BigInt mp_integer
Definition: mp_arith.h:22
bool is_nil() const
Definition: irep.h:172
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:1159
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:4422
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:240
const irep_idt & id() const
Definition: irep.h:259
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
exprt & lhs()
Definition: std_code.h:209
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:4508
symbolt fresh_symbol(std::string base, typet type)
exprt & rhs()
Definition: std_code.h:214
exprt eval(const exprt &e)
Fixed-width bit-vector with two&#39;s complement interpretation.
Definition: std_types.h:1271
Symbolic Execution.
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:1340
A forall expression.
Definition: std_expr.h:4858
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)
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
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:4463
The boolean constant false.
Definition: std_expr.h:4497
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
const source_locationt & source_location() const
Definition: expr.h:125
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:3950
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:196
std::vector< monomialt > monomials
Definition: polynomial.h:46
bool simplify(exprt &expr, const namespacet &ns)