cprover
Loading...
Searching...
No Matches
disjunctive_polynomial_acceleration.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
21
22#include <util/std_code.h>
23#include <util/simplify_expr.h>
24#include <util/replace_expr.h>
25#include <util/arith_tools.h>
26
27#include "accelerator.h"
28#include "cone_of_influence.h"
30#include "scratch_program.h"
31#include "util.h"
32
34 path_acceleratort &accelerator)
35{
36 std::map<exprt, polynomialt> polynomials;
38
39 accelerator.clear();
40
41#ifdef DEBUG
42 std::cout << "Polynomial accelerating program:\n";
43
44 for(goto_programt::instructionst::iterator
45 it=goto_program.instructions.begin();
46 it!=goto_program.instructions.end();
47 ++it)
48 {
49 if(loop.contains(it))
50 {
51 goto_program.output_instruction(ns, "scratch", std::cout, *it);
52 }
53 }
54
55 std::cout << "Modified:\n";
56
57 for(expr_sett::iterator it=modified.begin();
58 it!=modified.end();
59 ++it)
60 {
61 std::cout << expr2c(*it, ns) << '\n';
62 }
63#endif
64
66 {
68 utils.fresh_symbol("polynomial::loop_counter", unsigned_poly_type());
69 loop_counter=loop_sym.symbol_expr();
70 }
71
72 patht &path=accelerator.path;
73 path.clear();
74
75 if(!find_path(path))
76 {
77 // No more paths!
78 return false;
79 }
80
81#if 0
82 for(expr_sett::iterator it=modified.begin();
83 it!=modified.end();
84 ++it)
85 {
87 exprt target=*it;
88
89 if(it->type().id()==ID_bool)
90 {
91 // Hack: don't try to accelerate booleans.
92 continue;
93 }
94
95 if(target.id()==ID_index ||
96 target.id()==ID_dereference)
97 {
98 // We'll handle this later.
99 continue;
100 }
101
102 if(fit_polynomial(target, poly, path))
103 {
104 std::map<exprt, polynomialt> this_poly;
105 this_poly[target]=poly;
106
108 {
109#ifdef DEBUG
110 std::cout << "Fitted a polynomial for " << expr2c(target, ns)
111 << '\n';
112#endif
113 polynomials[target]=poly;
114 accelerator.changed_vars.insert(target);
115 break;
116 }
117 }
118 }
119
120 if(polynomials.empty())
121 {
122 return false;
123 }
124#endif
125
126 // Fit polynomials for the other variables.
127 expr_sett dirty;
128 utils.find_modified(accelerator.path, dirty);
132
133 for(patht::iterator it=accelerator.path.begin();
134 it!=accelerator.path.end();
135 ++it)
136 {
137 if(it->loc->is_assign() || it->loc->is_decl())
138 {
139 assigns.push_back(*(it->loc));
140 }
141 }
142
143 for(expr_sett::iterator it=dirty.begin();
144 it!=dirty.end();
145 ++it)
146 {
147#ifdef DEBUG
148 std::cout << "Trying to accelerate " << expr2c(*it, ns) << '\n';
149#endif
150
151 if(it->type().id()==ID_bool)
152 {
153 // Hack: don't try to accelerate booleans.
154 accelerator.dirty_vars.insert(*it);
155#ifdef DEBUG
156 std::cout << "Ignoring boolean\n";
157#endif
158 continue;
159 }
160
161 if(it->id()==ID_index ||
162 it->id()==ID_dereference)
163 {
164#ifdef DEBUG
165 std::cout << "Ignoring array reference\n";
166#endif
167 continue;
168 }
169
170 if(accelerator.changed_vars.find(*it)!=accelerator.changed_vars.end())
171 {
172 // We've accelerated variable this already.
173#ifdef DEBUG
174 std::cout << "We've accelerated it already\n";
175#endif
176 continue;
177 }
178
179 // Hack: ignore variables that depend on array values..
181
183 {
184#ifdef DEBUG
185 std::cout << "Ignoring because it depends on an array\n";
186#endif
187 continue;
188 }
189
190
192 exprt target(*it);
193
194 if(path_acceleration.fit_polynomial(assigns, target, poly))
195 {
196 std::map<exprt, polynomialt> this_poly;
197 this_poly[target]=poly;
198
200 {
201 polynomials[target]=poly;
202 accelerator.changed_vars.insert(target);
203 continue;
204 }
205 }
206
207#ifdef DEBUG
208 std::cout << "Failed to accelerate " << expr2c(*it, ns) << '\n';
209#endif
210
211 // We weren't able to accelerate this target...
212 accelerator.dirty_vars.insert(target);
213 }
214
215
216 #if 0
217 if(!utils.check_inductive(polynomials, assigns))
218 {
219 // They're not inductive :-(
220 return false;
221 }
222 #endif
223
226
227 exprt guard;
228 bool path_is_monotone;
229
230 try
231 {
234 }
235 catch(const std::string &s)
236 {
237 // Couldn't do WP.
238 std::cout << "Assumptions error: " << s << '\n';
239 return false;
240 }
241
242 exprt pre_guard(guard);
243
244 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
245 it!=polynomials.end();
246 ++it)
247 {
248 replace_expr(it->first, it->second.to_expr(), guard);
249 }
250
252 {
253 // OK cool -- the path is monotone, so we can just assume the condition for
254 // the last iteration.
258 guard);
259 }
260 else
261 {
262 // The path is not monotone, so we need to introduce a quantifier to ensure
263 // that the condition held for all 0 <= k < n.
265 const symbol_exprt k = k_sym.symbol_expr();
266
267 const and_exprt k_bound(
270 replace_expr(loop_counter, k, guard);
271
272 simplify(guard, ns);
273
274 implies_exprt implies(k_bound, guard);
275
276 guard = forall_exprt(k, implies);
277 }
278
279 // All our conditions are met -- we can finally build the accelerator!
280 // It is of the form:
281 //
282 // loop_counter=*;
283 // target1=polynomial1;
284 // target2=polynomial2;
285 // ...
286 // assume(guard);
287 // assume(no overflows in previous code);
288
290 program.assign(
293
294 for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
295 it!=polynomials.end();
296 ++it)
297 {
298 program.assign(it->first, it->second.to_expr());
299 accelerator.changed_vars.insert(it->first);
300 }
301
302 // Add in any array assignments we can do now.
303 if(!utils.do_arrays(assigns, polynomials, stashed, program))
304 {
305 // We couldn't model some of the array assignments with polynomials...
306 // Unfortunately that means we just have to bail out.
307 return false;
308 }
309
310 program.add(goto_programt::make_assumption(guard));
311 program.fix_types();
312
314 {
315 utils.ensure_no_overflows(program);
316 }
317
318 accelerator.pure_accelerator.instructions.swap(program.instructions);
319
320 return true;
321}
322
324{
326
327 program.append(fixed);
328 program.append(fixed);
329
330 // Let's make sure that we get a path we have not seen before.
331 for(std::list<distinguish_valuest>::iterator it=accelerated_paths.begin();
332 it!=accelerated_paths.end();
333 ++it)
334 {
336
337 for(distinguish_valuest::iterator jt=it->begin();
338 jt!=it->end();
339 ++jt)
340 {
341 exprt distinguisher=jt->first;
342 bool taken=jt->second;
343
344 if(taken)
345 {
348 }
349
351 new_path.swap(disjunct);
352 }
353
354 program.assume(new_path);
355 }
356
358
359 try
360 {
361 if(program.check_sat(guard_manager))
362 {
363#ifdef DEBUG
364 std::cout << "Found a path\n";
365#endif
366 build_path(program, path);
367 record_path(program);
368
369 return true;
370 }
371 }
372 catch(const std::string &s)
373 {
374 std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
375 }
376 catch(const char *s)
377 {
378 std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
379 }
380
381 return false;
382}
383
385 exprt &var,
387 patht &path)
388{
389 // These are the variables that var depends on with respect to the body.
390 std::vector<expr_listt> parameters;
391 std::set<std::pair<expr_listt, exprt> > coefficients;
395
397
398#ifdef DEBUG
399 std::cout << "Fitting a polynomial for " << expr2c(var, ns)
400 << ", which depends on:\n";
401
402 for(expr_sett::iterator it=influence.begin();
403 it!=influence.end();
404 ++it)
405 {
406 std::cout << expr2c(*it, ns) << '\n';
407 }
408#endif
409
410 for(expr_sett::iterator it=influence.begin();
411 it!=influence.end();
412 ++it)
413 {
414 if(it->id()==ID_index ||
415 it->id()==ID_dereference)
416 {
417 // Hack: don't accelerate anything that depends on an array
418 // yet...
419 return false;
420 }
421
422 exprs.clear();
423
424 exprs.push_back(*it);
425 parameters.push_back(exprs);
426
427 exprs.push_back(loop_counter);
428 parameters.push_back(exprs);
429 }
430
431 // N
432 exprs.clear();
433 exprs.push_back(loop_counter);
434 parameters.push_back(exprs);
435
436 // N^2
437 exprs.push_back(loop_counter);
438 parameters.push_back(exprs);
439
440 // Constant
441 exprs.clear();
442 parameters.push_back(exprs);
443
444 for(std::vector<expr_listt>::iterator it=parameters.begin();
445 it!=parameters.end();
446 ++it)
447 {
448 symbolt coeff=utils.fresh_symbol("polynomial::coeff", signed_poly_type());
449 coefficients.insert(make_pair(*it, coeff.symbol_expr()));
450
451 // XXX HACK HACK HACK
452 // I'm just constraining these coefficients to prevent overflows
453 // messing things up later... Should really do this properly
454 // somehow.
455 program.assume(
457 from_integer(-(1 << 10), signed_poly_type()),
458 ID_lt,
459 coeff.symbol_expr()));
460 program.assume(
462 coeff.symbol_expr(),
463 ID_lt,
464 from_integer(1 << 10, signed_poly_type())));
465 }
466
467 // Build a set of values for all the parameters that allow us to fit a
468 // unique polynomial.
469
470 std::map<exprt, exprt> ivals1;
471 std::map<exprt, exprt> ivals2;
472 std::map<exprt, exprt> ivals3;
473
474 for(expr_sett::iterator it=influence.begin();
475 it!=influence.end();
476 ++it)
477 {
478 symbolt ival1=utils.fresh_symbol("polynomial::init",
479 it->type());
480 symbolt ival2=utils.fresh_symbol("polynomial::init",
481 it->type());
482 symbolt ival3=utils.fresh_symbol("polynomial::init",
483 it->type());
484
485 program.assume(binary_relation_exprt(ival1.symbol_expr(), "<",
486 ival2.symbol_expr()));
487 program.assume(binary_relation_exprt(ival2.symbol_expr(), "<",
488 ival3.symbol_expr()));
489
490#if 0
491 if(it->type()==signedbv_typet())
492 {
493 program.assume(binary_relation_exprt(ival1.symbol_expr(), ">",
494 from_integer(-100, it->type())));
495 }
496 program.assume(binary_relation_exprt(ival1.symbol_expr(), "<",
497 from_integer(100, it->type())));
498
499 if(it->type()==signedbv_typet())
500 {
501 program.assume(binary_relation_exprt(ival2.symbol_expr(), ">",
502 from_integer(-100, it->type())));
503 }
504 program.assume(binary_relation_exprt(ival2.symbol_expr(), "<",
505 from_integer(100, it->type())));
506
507 if(it->type()==signedbv_typet())
508 {
509 program.assume(binary_relation_exprt(ival3.symbol_expr(), ">",
510 from_integer(-100, it->type())));
511 }
512 program.assume(binary_relation_exprt(ival3.symbol_expr(), "<",
513 from_integer(100, it->type())));
514#endif
515
516 ivals1[*it]=ival1.symbol_expr();
517 ivals2[*it]=ival2.symbol_expr();
518 ivals3[*it]=ival3.symbol_expr();
519
520 // ivals1[*it]=from_integer(1, it->type());
521 }
522
523 std::map<exprt, exprt> values;
524
525 for(expr_sett::iterator it=influence.begin();
526 it!=influence.end();
527 ++it)
528 {
529 values[*it]=ivals1[*it];
530 }
531
532 // Start building the program. Begin by decl'ing each of the
533 // master distinguishers.
534 for(std::list<symbol_exprt>::iterator it = distinguishers.begin();
535 it != distinguishers.end();
536 ++it)
537 {
538 program.add(goto_programt::make_decl(*it));
539 }
540
541 // Now assume our polynomial fits at each of our sample points.
542 assert_for_values(program, values, coefficients, 1, fixed, var);
543
544 for(int n=0; n <= 1; n++)
545 {
546 for(expr_sett::iterator it=influence.begin();
547 it!=influence.end();
548 ++it)
549 {
550 values[*it]=ivals2[*it];
551 assert_for_values(program, values, coefficients, n, fixed, var);
552
553 values[*it]=ivals3[*it];
554 assert_for_values(program, values, coefficients, n, fixed, var);
555
556 values[*it]=ivals1[*it];
557 }
558 }
559
560 for(expr_sett::iterator it=influence.begin();
561 it!=influence.end();
562 ++it)
563 {
564 values[*it]=ivals3[*it];
565 }
566
567 assert_for_values(program, values, coefficients, 0, fixed, var);
568 assert_for_values(program, values, coefficients, 1, fixed, var);
569 assert_for_values(program, values, coefficients, 2, fixed, var);
570
571 // Let's make sure that we get a path we have not seen before.
572 for(std::list<distinguish_valuest>::iterator it=accelerated_paths.begin();
573 it!=accelerated_paths.end();
574 ++it)
575 {
577
578 for(distinguish_valuest::iterator jt=it->begin();
579 jt!=it->end();
580 ++jt)
581 {
582 exprt distinguisher=jt->first;
583 bool taken=jt->second;
584
585 if(taken)
586 {
589 }
590
592 new_path.swap(disjunct);
593 }
594
595 program.assume(new_path);
596 }
597
598 utils.ensure_no_overflows(program);
599
600 // Now do an ASSERT(false) to grab a counterexample
602
603 // If the path is satisfiable, we've fitted a polynomial. Extract the
604 // relevant coefficients and return the expression.
605 try
606 {
607 if(program.check_sat(guard_manager))
608 {
609#ifdef DEBUG
610 std::cout << "Found a polynomial\n";
611#endif
612
613 utils.extract_polynomial(program, coefficients, polynomial);
614 build_path(program, path);
615 record_path(program);
616
617 return true;
618 }
619 }
620 catch(const std::string &s)
621 {
622 std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
623 }
624 catch(const char *s)
625 {
626 std::cout << "Error in fitting polynomial SAT check: " << s << '\n';
627 }
628
629 return false;
630}
631
633 scratch_programt &program,
634 std::map<exprt, exprt> &values,
635 std::set<std::pair<expr_listt, exprt> > &coefficients,
636 int num_unwindings,
638 exprt &target)
639{
640 // First figure out what the appropriate type for this expression is.
642
643 for(std::map<exprt, exprt>::iterator it=values.begin();
644 it!=values.end();
645 ++it)
646 {
647 if(!expr_type.has_value())
648 {
649 expr_type=it->first.type();
650 }
651 else
652 {
653 expr_type = join_types(*expr_type, it->first.type());
654 }
655 }
656
657 // Now set the initial values of the all the variables...
658 for(std::map<exprt, exprt>::iterator it=values.begin();
659 it!=values.end();
660 ++it)
661 {
662 program.assign(it->first, it->second);
663 }
664
665 // Now unwind the loop as many times as we need to.
666 for(int i=0; i<num_unwindings; i++)
667 {
668 program.append(loop_body);
669 }
670
671 // Now build the polynomial for this point and assert it fits.
672 exprt rhs=nil_exprt();
673
674 for(std::set<std::pair<expr_listt, exprt> >::iterator it=coefficients.begin();
675 it!=coefficients.end();
676 ++it)
677 {
679
680 for(expr_listt::const_iterator e_it=it->first.begin();
681 e_it!=it->first.end();
682 ++e_it)
683 {
684 exprt e=*e_it;
685
686 if(e==loop_counter)
687 {
688 mult_exprt mult(
690 mult.swap(concrete_value);
691 }
692 else
693 {
694 std::map<exprt, exprt>::iterator v_it=values.find(e);
695
696 PRECONDITION(v_it!=values.end());
697
698 mult_exprt mult(concrete_value, v_it->second);
699 mult.swap(concrete_value);
700 }
701 }
702
703 // OK, concrete_value now contains the value of all the relevant variables
704 // multiplied together. Create the term concrete_value*coefficient and add
705 // it into the polynomial.
706 typecast_exprt cast(it->second, *expr_type);
707 const mult_exprt term(concrete_value, cast);
708
709 if(rhs.is_nil())
710 {
711 rhs=term;
712 }
713 else
714 {
715 rhs=plus_exprt(rhs, term);
716 }
717 }
718
719 rhs=typecast_exprt(rhs, target.type());
720
721 // We now have the RHS of the polynomial. Assert that this is equal to the
722 // actual value of the variable we're fitting.
723 const equal_exprt polynomial_holds(target, rhs);
724
725 // Finally, assert that the polynomial equals the variable we're fitting.
727}
728
730 const exprt &target,
732{
734 influence.cone_of_influence(target, cone);
735}
736
738{
739 for(const auto &loop_instruction : loop)
740 {
742
743 if(succs.size() > 1)
744 {
745 // This location has multiple successors -- each successor is a
746 // distinguishing point.
747 for(const auto &jt : succs)
748 {
750 utils.fresh_symbol("polynomial::distinguisher", bool_typet());
752
754 distinguishers.push_back(distinguisher);
755 }
756 }
757 }
758}
759
762{
764
765 do
766 {
768
769 const auto succs=goto_program.get_successors(t);
770
771 INVARIANT(succs.size() > 0,
772 "we should have a looping path, so we should never hit a location "
773 "with no successors.");
774
775 if(succs.size()==1)
776 {
777 // Only one successor -- accumulate it and move on.
778 path.push_back(path_nodet(t));
779 t=succs.front();
780 continue;
781 }
782
783 // We have multiple successors. Examine the distinguisher variables
784 // to see which branch was taken.
785 bool found_branch=false;
786
787 for(const auto &succ : succs)
788 {
790 bool taken=scratch_program.eval(distinguisher).is_true();
791
792 if(taken)
793 {
794 if(!found_branch ||
795 (succ->location_number < next->location_number))
796 {
797 next=succ;
798 }
799
800 found_branch=true;
801 }
802 }
803
805
806 exprt cond=nil_exprt();
807
808 if(t->is_goto())
809 {
810 // If this was a conditional branch (it probably was), figure out
811 // if we hit the "taken" or "not taken" branch & accumulate the
812 // appropriate guard.
813 cond = not_exprt(t->get_condition());
814
815 for(goto_programt::targetst::iterator it=t->targets.begin();
816 it!=t->targets.end();
817 ++it)
818 {
819 if(next==*it)
820 {
821 cond = t->get_condition();
822 break;
823 }
824 }
825 }
826
827 path.push_back(path_nodet(t, cond));
828
829 t=next;
830 } while(t != loop_header && loop.contains(t));
831}
832
833/*
834 * Take the body of the loop we are accelerating and produce a fixed-path
835 * version of that body, suitable for use in the fixed-path acceleration we
836 * will be doing later.
837 */
839{
841 std::map<exprt, exprt> shadow_distinguishers;
842
844
845 for(auto &instruction : fixed.instructions)
846 {
847 if(instruction.is_assert())
848 instruction.turn_into_assume();
849 }
850
851 // We're only interested in paths that loop back to the loop header.
852 // As such, any path that jumps outside of the loop or jumps backwards
853 // to a location other than the loop header (i.e. a nested loop) is not
854 // one we're interested in, and we'll redirect it to this assume(false).
857
858 // Make a sentinel instruction to mark the end of the loop body.
859 // We'll use this as the new target for any back-jumps to the loop
860 // header.
862
863 // A pointer to the start of the fixed-path body. We'll be using this to
864 // iterate over the fixed-path body, but for now it's just a pointer to the
865 // first instruction.
867
868 // Create shadow distinguisher variables. These guys identify the path that
869 // is taken through the fixed-path body.
870 for(std::list<symbol_exprt>::iterator it = distinguishers.begin();
871 it != distinguishers.end();
872 ++it)
873 {
874 exprt &distinguisher=*it;
875 symbolt shadow_sym=utils.fresh_symbol("polynomial::shadow_distinguisher",
876 bool_typet());
877 exprt shadow=shadow_sym.symbol_expr();
879
881 fixedt,
883 }
884
885 // We're going to iterate over the 2 programs in lockstep, which allows
886 // us to figure out which distinguishing point we've hit & instrument
887 // the relevant distinguisher variables.
889 t!=goto_program.instructions.end();
890 ++t, ++fixedt)
891 {
892 distinguish_mapt::iterator d=distinguishing_points.find(t);
893
894 if(!loop.contains(t))
895 {
896 // This instruction isn't part of the loop... Just remove it.
897 fixedt->turn_into_skip();
898 continue;
899 }
900
901 if(d!=distinguishing_points.end())
902 {
903 // We've hit a distinguishing point. Set the relevant shadow
904 // distinguisher to true.
905 exprt &distinguisher=d->second;
907
909 fixedt,
911
912 assign->swap(*fixedt);
913 fixedt=assign;
914 }
915
916 if(t->is_goto())
917 {
918 PRECONDITION(fixedt->is_goto());
919 // If this is a forwards jump, it's either jumping inside the loop
920 // (in which case we leave it alone), or it jumps outside the loop.
921 // If it jumps out of the loop, it's on a path we don't care about
922 // so we kill it.
923 //
924 // Otherwise, it's a backwards jump. If it jumps back to the loop
925 // header we're happy & redirect it to our end-of-body sentinel.
926 // If it jumps somewhere else, it's part of a nested loop and we
927 // kill it.
928 for(const auto &target : t->targets)
929 {
930 if(target->location_number > t->location_number)
931 {
932 // A forward jump...
933 if(loop.contains(target))
934 {
935 // Case 1: a forward jump within the loop. Do nothing.
936 continue;
937 }
938 else
939 {
940 // Case 2: a forward jump out of the loop. Kill.
941 fixedt->targets.clear();
942 fixedt->targets.push_back(kill);
943 }
944 }
945 else
946 {
947 // A backwards jump...
948 if(target==loop_header)
949 {
950 // Case 3: a backwards jump to the loop header. Redirect
951 // to sentinel.
952 fixedt->targets.clear();
953 fixedt->targets.push_back(end);
954 }
955 else
956 {
957 // Case 4: a nested loop. Kill.
958 fixedt->targets.clear();
959 fixedt->targets.push_back(kill);
960 }
961 }
962 }
963 }
964 }
965
966 // OK, now let's assume that the path we took through the fixed-path
967 // body is the same as the master path. We do this by assuming that
968 // each of the shadow-distinguisher variables is equal to its corresponding
969 // master-distinguisher.
970 for(const auto &expr : distinguishers)
971 {
973
976 }
977
978 // Finally, let's remove all the skips we introduced and fix the
979 // jump targets.
980 fixed.update();
982}
983
985 scratch_programt &program)
986{
988
989 for(std::list<symbol_exprt>::iterator it = distinguishers.begin();
990 it != distinguishers.end();
991 ++it)
992 {
993 path_val[*it]=program.eval(*it).is_true();
994 }
995
996 accelerated_paths.push_back(path_val);
997}
998
1000 const exprt &e,
1001 exprt &array)
1002{
1004
1006
1007 for(expr_sett::iterator it=influence.begin();
1008 it!=influence.end();
1009 ++it)
1010 {
1011 if(it->id()==ID_index ||
1012 it->id()==ID_dereference)
1013 {
1014 array=*it;
1015 return true;
1016 }
1017 }
1018
1019 return false;
1020}
std::list< exprt > expr_listt
Loop Acceleration.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
void find_modified(const patht &path, expr_sett &modified)
bool do_arrays(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, substitutiont &substitution, scratch_programt &program)
void stash_polynomials(scratch_programt &program, std::map< exprt, polynomialt > &polynomials, std::map< exprt, exprt > &stashed, patht &path)
bool check_inductive(std::map< exprt, polynomialt > polynomials, patht &path, guard_managert &guard_manager)
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)
virtual void clear()
Reset the abstract state.
Definition ai.h:267
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
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
The Boolean type.
Definition std_types.h:36
A codet representing an assignment in the program.
void assert_for_values(scratch_programt &program, std::map< exprt, exprt > &values, std::set< std::pair< expr_listt, exprt > > &coefficients, int num_unwindings, goto_programt &loop_body, exprt &target)
natural_loops_mutablet::natural_loopt & loop
void record_path(scratch_programt &scratch_program)
bool fit_polynomial(exprt &target, polynomialt &polynomial, patht &path)
void cone_of_influence(const exprt &target, expr_sett &cone)
void build_path(scratch_programt &scratch_program, patht &path)
Equality.
Definition std_expr.h:1225
Base class for all expressions.
Definition expr.h:54
bool is_true() const
Return whether the expression is a constant representing true.
Definition expr.cpp:33
typet & type()
Return the type of the expression.
Definition expr.h:82
The Boolean constant false.
Definition std_expr.h:2865
A forall expression.
A generic container class for the GOTO intermediate representation of one function.
static instructiont make_assumption(const exprt &g, const source_locationt &l=source_locationt::nil())
instructionst instructions
The list of instructions in the goto program.
void copy_from(const goto_programt &src)
Copy a full goto program, preserving targets.
void update()
Update all indices.
instructionst::iterator targett
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
std::list< instructiont > instructionst
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
std::list< Target > get_successors(Target target) const
Get control-flow successors of a given instruction.
targett add(instructiont &&instruction)
Adds a given instruction at the end.
static instructiont make_decl(const symbol_exprt &symbol, const source_locationt &l=source_locationt::nil())
static instructiont make_assertion(const exprt &g, const source_locationt &l=source_locationt::nil())
targett insert_before(const_targett target)
Insertion before the instruction pointed-to by the given instruction iterator target.
Boolean implication.
Definition std_expr.h:2037
void swap(irept &irep)
Definition irep.h:442
const irep_idt & id() const
Definition irep.h:396
bool is_nil() const
Definition irep.h:376
Binary minus.
Definition std_expr.h:973
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
Boolean OR.
Definition std_expr.h:2082
std::set< exprt > changed_vars
Definition accelerator.h:65
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
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
Symbol table entry.
Definition symbol.h:28
class symbol_exprt symbol_expr() const
Produces a symbol_exprt for a symbol.
Definition symbol.cpp:121
The Boolean constant true.
Definition std_expr.h:2856
Semantic type conversion.
Definition std_expr.h:1920
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
Concrete Goto Program.
std::list< path_nodet > patht
Definition path.h:44
std::map< exprt, exprt > substitutiont
Definition polynomial.h:39
Loop Acceleration.
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Program Transformation.
bool replace_expr(const exprt &what, const exprt &by, exprt &dest)
Loop Acceleration.
bool simplify(exprt &expr, const namespacet &ns)
#define PRECONDITION(CONDITION)
Definition invariant.h:463
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
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
signedbv_typet signed_poly_type()
Definition util.cpp:20
Loop Acceleration.