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