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 =
182  utils.do_assumptions(polynomials, loop, guard, guard_manager);
183  }
184  catch(const std::string &s)
185  {
186  // Couldn't do WP.
187  std::cout << "Assumptions error: " << s << '\n';
188  return false;
189  }
190 
191  guard_last=guard;
192 
193  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
194  it!=polynomials.end();
195  ++it)
196  {
197  replace_expr(it->first, it->second.to_expr(), guard_last);
198  }
199 
200  if(path_is_monotone)
201  {
202  // OK cool -- the path is monotone, so we can just assume the condition for
203  // the first and last iterations.
204  replace_expr(
205  loop_counter,
207  guard_last);
208  // simplify(guard_last, ns);
209  }
210  else
211  {
212  // The path is not monotone, so we need to introduce a quantifier to ensure
213  // that the condition held for all 0 <= k < n.
214  symbolt k_sym=utils.fresh_symbol("polynomial::k", unsigned_poly_type());
215  const symbol_exprt k = k_sym.symbol_expr();
216 
217  const and_exprt k_bound(
218  binary_relation_exprt(from_integer(0, k.type()), ID_le, k),
220  replace_expr(loop_counter, k, guard_last);
221 
222  implies_exprt implies(k_bound, guard_last);
223  // simplify(implies, ns);
224 
225  guard_last = forall_exprt(k, implies);
226  }
227 
228  // All our conditions are met -- we can finally build the accelerator!
229  // It is of the form:
230  //
231  // assume(guard);
232  // loop_counter=*;
233  // target1=polynomial1;
234  // target2=polynomial2;
235  // ...
236  // assume(guard);
237  // assume(no overflows in previous code);
238 
239  program.add(goto_programt::make_assumption(guard));
240 
241  program.assign(
242  loop_counter,
245 
246  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
247  it!=polynomials.end();
248  ++it)
249  {
250  program.assign(it->first, it->second.to_expr());
251  }
252 
253  // Add in any array assignments we can do now.
255  assigns, polynomials, stashed, nonrecursive, program))
256  {
257  // We couldn't model some of the array assignments with polynomials...
258  // Unfortunately that means we just have to bail out.
259 #ifdef DEBUG
260  std::cout << "Failed to accelerate a nonrecursive expression\n";
261 #endif
262  return false;
263  }
264 
265  program.add(goto_programt::make_assumption(guard_last));
266  program.fix_types();
267 
268  if(path_is_monotone)
269  {
270  utils.ensure_no_overflows(program);
271  }
272 
273  accelerator.pure_accelerator.instructions.swap(program.instructions);
274 
275  return true;
276 }
277 
280  exprt &var,
281  expr_sett &influence,
282  polynomialt &polynomial)
283 {
284  // These are the variables that var depends on with respect to the body.
285  std::vector<expr_listt> parameters;
286  std::set<std::pair<expr_listt, exprt> > coefficients;
287  expr_listt exprs;
289  exprt overflow_var =
290  utils.fresh_symbol("polynomial::overflow", bool_typet()).symbol_expr();
291  overflow_instrumentert overflow(program, overflow_var, symbol_table);
292 
293 #ifdef DEBUG
294  std::cout << "Fitting a polynomial for " << expr2c(var, ns)
295  << ", which depends on:\n";
296 
297  for(expr_sett::iterator it=influence.begin();
298  it!=influence.end();
299  ++it)
300  {
301  std::cout << expr2c(*it, ns) << '\n';
302  }
303 #endif
304 
305  for(expr_sett::iterator it=influence.begin();
306  it!=influence.end();
307  ++it)
308  {
309  if(it->id()==ID_index ||
310  it->id()==ID_dereference)
311  {
312  // Hack: don't accelerate variables that depend on arrays...
313  return false;
314  }
315 
316  exprs.clear();
317 
318  exprs.push_back(*it);
319  parameters.push_back(exprs);
320 
321  exprs.push_back(loop_counter);
322  parameters.push_back(exprs);
323  }
324 
325  // N
326  exprs.clear();
327  exprs.push_back(loop_counter);
328  parameters.push_back(exprs);
329 
330  // N^2
331  exprs.push_back(loop_counter);
332  // parameters.push_back(exprs);
333 
334  // Constant
335  exprs.clear();
336  parameters.push_back(exprs);
337 
338  if(!is_bitvector(var.type()))
339  {
340  // We don't really know how to accelerate non-bitvectors anyway...
341  return false;
342  }
343 
344  std::size_t width=to_bitvector_type(var.type()).get_width();
345  assert(width>0);
346 
347  for(std::vector<expr_listt>::iterator it=parameters.begin();
348  it!=parameters.end();
349  ++it)
350  {
351  symbolt coeff=utils.fresh_symbol("polynomial::coeff",
352  signedbv_typet(width));
353  coefficients.insert(std::make_pair(*it, coeff.symbol_expr()));
354  }
355 
356  // Build a set of values for all the parameters that allow us to fit a
357  // unique polynomial.
358 
359  // XXX
360  // This isn't ok -- we're assuming 0, 1 and 2 are valid values for the
361  // variables involved, but this might make the path condition UNSAT. Should
362  // really be solving the path constraints a few times to get valid probe
363  // values...
364 
365  std::map<exprt, int> values;
366 
367  for(expr_sett::iterator it=influence.begin();
368  it!=influence.end();
369  ++it)
370  {
371  values[*it]=0;
372  }
373 
374 #ifdef DEBUG
375  std::cout << "Fitting polynomial over " << values.size()
376  << " variables\n";
377 #endif
378 
379  for(int n=0; n<=2; n++)
380  {
381  for(expr_sett::iterator it=influence.begin();
382  it!=influence.end();
383  ++it)
384  {
385  values[*it]=1;
386  assert_for_values(program, values, coefficients, n, body, var, overflow);
387  values[*it]=0;
388  }
389  }
390 
391  // Now just need to assert the case where all values are 0 and all are 2.
392  assert_for_values(program, values, coefficients, 0, body, var, overflow);
393  assert_for_values(program, values, coefficients, 2, body, var, overflow);
394 
395  for(expr_sett::iterator it=influence.begin();
396  it!=influence.end();
397  ++it)
398  {
399  values[*it]=2;
400  }
401 
402  assert_for_values(program, values, coefficients, 2, body, var, overflow);
403 
404 #ifdef DEBUG
405  std::cout << "Fitting polynomial with program:\n";
406  program.output(ns, irep_idt(), std::cout);
407 #endif
408 
409  // Now do an ASSERT(false) to grab a counterexample
411 
412  // If the path is satisfiable, we've fitted a polynomial. Extract the
413  // relevant coefficients and return the expression.
414  try
415  {
416  if(program.check_sat(guard_manager))
417  {
418  utils.extract_polynomial(program, coefficients, polynomial);
419  return true;
420  }
421  }
422  catch(const std::string &s)
423  {
424  std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
425  }
426  catch(const char *s)
427  {
428  std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
429  }
430 
431  return false;
432 }
433 
436  exprt &target,
437  polynomialt &polynomial)
438 {
440  expr_sett influence;
441 
442  cone_of_influence(body, target, sliced, influence);
443 
444  return fit_polynomial_sliced(sliced, target, influence, polynomial);
445 }
446 
449  exprt &target,
450  polynomialt &poly)
451 {
452  // unused parameters
453  (void)body;
454  (void)target;
455  (void)poly;
456  return false;
457 
458 #if 0
460 
461  program.append(body);
462  program.add_instruction(ASSERT)->guard=equal_exprt(target, not_exprt(target));
463 
464  try
465  {
466  if(program.check_sat(false))
467  {
468 #ifdef DEBUG
469  std::cout << "Fitting constant, eval'd to: "
470  << expr2c(program.eval(target), ns) << '\n';
471 #endif
472  constant_exprt val=to_constant_expr(program.eval(target));
473  mp_integer mp=binary2integer(val.get_value().c_str(), true);
474  monomialt mon;
475  monomialt::termt term;
476 
477  term.var=from_integer(1, target.type());
478  term.exp=1;
479  mon.terms.push_back(term);
480  mon.coeff=mp.to_long();
481 
482  poly.monomials.push_back(mon);
483 
484  return true;
485  }
486  }
487  catch(const std::string &s)
488  {
489  std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
490  }
491  catch(const char *s)
492  {
493  std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
494  }
495 
496  return false;
497 #endif
498 }
499 
501  scratch_programt &program,
502  std::map<exprt, int> &values,
503  std::set<std::pair<expr_listt, exprt> > &coefficients,
504  int num_unwindings,
505  goto_programt::instructionst &loop_body,
506  exprt &target,
507  overflow_instrumentert &overflow)
508 {
509  // First figure out what the appropriate type for this expression is.
510  optionalt<typet> expr_type;
511 
512  for(std::map<exprt, int>::iterator it=values.begin();
513  it!=values.end();
514  ++it)
515  {
516  typet this_type=it->first.type();
517  if(this_type.id()==ID_pointer)
518  {
519 #ifdef DEBUG
520  std::cout << "Overriding pointer type\n";
521 #endif
522  this_type=size_type();
523  }
524 
525  if(!expr_type.has_value())
526  {
527  expr_type=this_type;
528  }
529  else
530  {
531  expr_type = join_types(*expr_type, this_type);
532  }
533  }
534 
535  INVARIANT(
536  to_bitvector_type(*expr_type).get_width() > 0,
537  "joined types must be non-empty bitvector types");
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(goto_programt::make_assumption(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  program.add(goto_programt::make_assumption(polynomial_holds));
612 }
613 
615  goto_programt::instructionst &orig_body,
616  exprt &target,
618  expr_sett &cone)
619 {
620  utils.gather_rvalues(target, cone);
621 
622  for(goto_programt::instructionst::reverse_iterator r_it=orig_body.rbegin();
623  r_it!=orig_body.rend();
624  ++r_it)
625  {
626  if(r_it->is_assign())
627  {
628  // XXX -- this doesn't work if the assignment is not to a symbol, e.g.
629  // A[i]=0;
630  // or
631  // *p=x;
632  code_assignt assignment=to_code_assign(r_it->code);
633  expr_sett lhs_syms;
634 
635  utils.gather_rvalues(assignment.lhs(), lhs_syms);
636 
637  for(expr_sett::iterator s_it=lhs_syms.begin();
638  s_it!=lhs_syms.end();
639  ++s_it)
640  {
641  if(cone.find(*s_it)!=cone.end())
642  {
643  // We're assigning to something in the cone of influence -- expand the
644  // cone.
645  body.push_front(*r_it);
646  cone.erase(assignment.lhs());
647  utils.gather_rvalues(assignment.rhs(), cone);
648  break;
649  }
650  }
651  }
652  }
653 }
654 
656  std::map<exprt, polynomialt> polynomials,
658 {
659  // Checking that our polynomial is inductive with respect to the loop body is
660  // equivalent to checking safety of the following program:
661  //
662  // assume (target1==polynomial1);
663  // assume (target2==polynomial2)
664  // ...
665  // loop_body;
666  // loop_counter++;
667  // assert (target1==polynomial1);
668  // assert (target2==polynomial2);
669  // ...
671  std::vector<exprt> polynomials_hold;
672  substitutiont substitution;
673 
674  stash_polynomials(program, polynomials, substitution, body);
675 
676  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
677  it!=polynomials.end();
678  ++it)
679  {
680  const equal_exprt holds(it->first, it->second.to_expr());
681  program.add(goto_programt::make_assumption(holds));
682 
683  polynomials_hold.push_back(holds);
684  }
685 
686  program.append(body);
687 
688  auto inc_loop_counter = code_assignt(
689  loop_counter,
691  program.add(goto_programt::make_assignment(inc_loop_counter));
692 
693  for(std::vector<exprt>::iterator it=polynomials_hold.begin();
694  it!=polynomials_hold.end();
695  ++it)
696  {
697  program.add(goto_programt::make_assertion(*it));
698  }
699 
700 #ifdef DEBUG
701  std::cout << "Checking following program for inductiveness:\n";
702  program.output(ns, irep_idt(), std::cout);
703 #endif
704 
705  try
706  {
707  if(program.check_sat(guard_manager))
708  {
709  // We found a counterexample to inductiveness... :-(
710  #ifdef DEBUG
711  std::cout << "Not inductive!\n";
712  #endif
713  return false;
714  }
715  else
716  {
717  return true;
718  }
719  }
720  catch(const std::string &s)
721  {
722  std::cout << "Error in inductiveness SAT check: " << s << '\n';
723  return false;
724  }
725  catch(const char *s)
726  {
727  std::cout << "Error in inductiveness SAT check: " << s << '\n';
728  return false;
729  }
730 }
731 
733  scratch_programt &program,
734  std::map<exprt, polynomialt> &polynomials,
735  substitutiont &substitution,
737 {
738  expr_sett modified;
739  utils.find_modified(body, modified);
740  stash_variables(program, modified, substitution);
741 
742  for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
743  it!=polynomials.end();
744  ++it)
745  {
746  it->second.substitute(substitution);
747  }
748 }
749 
751  scratch_programt &program,
752  expr_sett modified,
753  substitutiont &substitution)
754 {
755  find_symbols_sett vars =
756  find_symbols_or_nexts(modified.begin(), modified.end());
757  irep_idt loop_counter_name=to_symbol_expr(loop_counter).get_identifier();
758  vars.erase(loop_counter_name);
759 
760  for(const irep_idt &id : vars)
761  {
762  const symbolt &orig = symbol_table.lookup_ref(id);
763  symbolt stashed_sym=utils.fresh_symbol("polynomial::stash", orig.type);
764  substitution[orig.symbol_expr()]=stashed_sym.symbol_expr();
765  program.assign(stashed_sym.symbol_expr(), orig.symbol_expr());
766  }
767 }
768 
769 /*
770  * Finds a precondition which guarantees that all the assumptions and assertions
771  * along this path hold.
772  *
773  * This is not the weakest precondition, since we make underapproximations due
774  * to aliasing.
775  */
776 
778 {
779  exprt ret=false_exprt();
780 
781  for(patht::reverse_iterator r_it=path.rbegin();
782  r_it!=path.rend();
783  ++r_it)
784  {
785  goto_programt::const_targett t=r_it->loc;
786 
787  if(t->is_assign())
788  {
789  // XXX Need to check for aliasing...
790  const code_assignt &assignment=to_code_assign(t->code);
791  const exprt &lhs=assignment.lhs();
792  const exprt &rhs=assignment.rhs();
793 
794  if(lhs.id()==ID_symbol)
795  {
796  replace_expr(lhs, rhs, ret);
797  }
798  else if(lhs.id()==ID_index ||
799  lhs.id()==ID_dereference)
800  {
801  continue;
802  }
803  else
804  {
805  throw "couldn't take WP of " + expr2c(lhs, ns) + "=" + expr2c(rhs, ns);
806  }
807  }
808  else if(t->is_assume() || t->is_assert())
809  {
810  ret = implies_exprt(t->get_condition(), ret);
811  }
812  else
813  {
814  // Ignore.
815  }
816 
817  if(!r_it->guard.is_true() && !r_it->guard.is_nil())
818  {
819  // The guard isn't constant true, so we need to accumulate that too.
820  ret=implies_exprt(r_it->guard, ret);
821  }
822  }
823 
824  simplify(ret, ns);
825 
826  return ret;
827 }
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
symex_target_equation.h
Generate Equation using Symbolic Execution.
overflow_instrumenter.h
Loop Acceleration.
dstringt::c_str
const char * c_str() const
Definition: dstring.h:99
symbol_table_baset::lookup_ref
const symbolt & lookup_ref(const irep_idt &name) const
Find a symbol in the symbol table for read-only access.
Definition: symbol_table_base.h:104
polynomialt
Definition: polynomial.h:42
polynomial_acceleratort::message_handler
message_handlert & message_handler
Definition: polynomial_accelerator.h:73
arith_tools.h
acceleration_utilst::do_assumptions
bool do_assumptions(std::map< exprt, polynomialt > polynomials, patht &body, exprt &guard, guard_managert &guard_manager)
Definition: acceleration_utils.cpp:344
forall_exprt
A forall expression.
Definition: mathematical_expr.h:341
polynomial_acceleratort::fit_polynomial
bool fit_polynomial(goto_programt::instructionst &loop_body, exprt &target, polynomialt &polynomial)
Definition: polynomial_accelerator.cpp:434
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:614
typet
The type of an expression, extends irept.
Definition: type.h:29
code_assignt::rhs
exprt & rhs()
Definition: std_code.h:317
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:278
acceleration_utilst::fresh_symbol
symbolt fresh_symbol(std::string base, typet type)
Definition: acceleration_utils.cpp:1261
find_symbols_or_nexts
void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest)
Add to the set dest the sub-expressions of src with id ID_symbol or ID_next_symbol.
Definition: find_symbols.cpp:18
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:447
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:577
mp_integer
BigInt mp_integer
Definition: mp_arith.h:19
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:732
and_exprt
Boolean AND.
Definition: std_expr.h:2137
goto_programt::add
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:686
plus_exprt
The plus expression Associativity is not specified.
Definition: std_expr.h:881
exprt
Base class for all expressions.
Definition: expr.h:53
polynomial_acceleratort::symbol_table
symbol_tablet & symbol_table
Definition: polynomial_accelerator.h:157
options.h
Options.
irep_idt
dstringt irep_idt
Definition: irep.h:32
bool_typet
The Boolean type.
Definition: std_types.h:37
acceleration_utilst::check_inductive
bool check_inductive(std::map< exprt, polynomialt > polynomials, patht &path, guard_managert &guard_manager)
Definition: acceleration_utils.cpp:113
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:82
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:1190
polynomial_acceleratort::precondition
exprt precondition(patht &path)
Definition: polynomial_accelerator.cpp:777
polynomial_acceleratort::ns
const namespacet ns
Definition: polynomial_accelerator.h:158
scratch_programt::append
void append(goto_programt::instructionst &instructions)
Definition: scratch_program.cpp:82
goto_programt::make_assignment
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
Definition: goto_program.h:1024
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:694
exprt::type
typet & type()
Return the type of the expression.
Definition: expr.h:81
goto_programt::make_assertion
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:893
find_symbols.h
polynomial_acceleratort::stash_variables
void stash_variables(scratch_programt &program, expr_sett modified, substitutiont &substitution)
Definition: polynomial_accelerator.cpp:750
scratch_programt
Definition: scratch_program.h:37
monomialt::coeff
int coeff
Definition: polynomial.h:31
monomialt
Definition: polynomial.h:21
expr2c.h
expr2c
std::string expr2c(const exprt &expr, const namespacet &ns, const expr2c_configurationt &configuration)
Definition: expr2c.cpp:3878
scratch_programt::eval
exprt eval(const exprt &e)
Definition: scratch_program.cpp:77
symbol_exprt::get_identifier
const irep_idt & get_identifier() const
Definition: std_expr.h:111
nil_exprt
The NIL expression.
Definition: std_expr.h:3973
signedbv_typet
Fixed-width bit-vector with two's complement interpretation.
Definition: std_types.h:1265
goto_symex.h
Symbolic Execution.
symbolt::symbol_expr
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition: symbol.cpp:122
polynomial_acceleratort::check_inductive
bool check_inductive(std::map< exprt, polynomialt > polynomials, goto_programt::instructionst &body)
Definition: polynomial_accelerator.cpp:655
code_assignt::lhs
exprt & lhs()
Definition: std_code.h:312
monomialt::termt::var
exprt var
Definition: polynomial.h:25
simplify
bool simplify(exprt &expr, const namespacet &ns)
Definition: simplify_expr.cpp:2693
path_acceleratort
Definition: accelerator.h:27
mult_exprt
Binary multiplication Associativity is not specified.
Definition: std_expr.h:986
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:467
acceleration_utilst::extract_polynomial
void extract_polynomial(scratch_programt &program, std::set< std::pair< expr_listt, exprt >> &coefficients, polynomialt &polynomial)
Definition: acceleration_utils.cpp:1212
to_symbol_expr
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:177
path_acceleratort::pure_accelerator
goto_programt pure_accelerator
Definition: accelerator.h:63
irept::is_nil
bool is_nil() const
Definition: irep.h:398
irept::id
const irep_idt & id() const
Definition: irep.h:418
false_exprt
The Boolean constant false.
Definition: std_expr.h:3964
goto_check.h
Program Transformation.
overflow_instrumentert
Definition: overflow_instrumenter.h:26
std_code.h
optionalt
nonstd::optional< T > optionalt
Definition: optional.h:35
minus_exprt
Binary minus.
Definition: std_expr.h:940
goto_program.h
Concrete Goto Program.
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
bitvector_typet::get_width
std::size_t get_width() const
Definition: std_types.h:1041
side_effect_expr_nondett
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1945
substitutiont
std::map< exprt, exprt > substitutiont
Definition: polynomial.h:39
monomialt::termt
Definition: polynomial.h:24
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:585
find_symbols_sett
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:22
to_code_assign
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:383
patht
std::list< path_nodet > patht
Definition: path.h:45
accelerator.h
Loop Acceleration.
symbolt
Symbol table entry.
Definition: symbol.h:28
replace_expr
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
Definition: replace_expr.cpp:12
from_integer
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
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
Loop Acceleration.
binary_relation_exprt
A base class for relations, i.e., binary predicates whose two operands have the same type.
Definition: std_expr.h:725
polynomial_acceleratort::loop_counter
exprt loop_counter
Definition: polynomial_accelerator.h:163
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
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:500
implies_exprt
Boolean implication.
Definition: std_expr.h:2200
goto_programt::make_assumption
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:905
replace_expr.h
polynomial_acceleratort::nonrecursive
expr_sett nonrecursive
Definition: polynomial_accelerator.h:165
scratch_programt::check_sat
bool check_sat(bool do_slice, guard_managert &guard_manager)
Definition: scratch_program.cpp:26
symbol_table.h
Author: Diffblue Ltd.
typecast_exprt
Semantic type conversion.
Definition: std_expr.h:2013
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:295
constant_exprt
A constant literal expression.
Definition: std_expr.h:3906
ASSERT
@ ASSERT
Definition: goto_program.h:36
std_expr.h
API to expression classes.
scratch_programt::assign
targett assign(const exprt &lhs, const exprt &rhs)
Definition: scratch_program.cpp:90
acceleration_utilst::gather_rvalues
void gather_rvalues(const exprt &expr, expr_sett &rvalues)
Definition: acceleration_utils.cpp:47
util.h
Loop Acceleration.
overflow_instrumentert::overflow_expr
void overflow_expr(const exprt &expr, expr_sett &cases)
Definition: overflow_instrumenter.cpp:94
constant_exprt::get_value
const irep_idt & get_value() const
Definition: std_expr.h:3914
exprt::source_location
const source_locationt & source_location() const
Definition: expr.h:254
c_types.h
polynomial_acceleratort::utils
acceleration_utilst utils
Definition: polynomial_accelerator.h:161
polynomial_accelerator.h
Loop Acceleration.
polynomial_acceleratort::guard_manager
guard_managert & guard_manager
Definition: polynomial_accelerator.h:160
wp.h
Weakest Preconditions.
monomialt::terms
std::vector< termt > terms
Definition: polynomial.h:30
validation_modet::INVARIANT
@ INVARIANT
to_bitvector_type
const bitvector_typet & to_bitvector_type(const typet &type)
Cast a typet to a bitvector_typet.
Definition: std_types.h:1089
not_exprt
Boolean negation.
Definition: std_expr.h:2843
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:868
to_constant_expr
const constant_exprt & to_constant_expr(const exprt &expr)
Cast an exprt to a constant_exprt.
Definition: std_expr.h:3939