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