cprover
Loading...
Searching...
No Matches
accelerate.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Loop Acceleration
4
5Author: Matt Lewis
6
7\*******************************************************************/
8
11
12#include "accelerate.h"
13
15
17
18#include <util/arith_tools.h>
19#include <util/find_symbols.h>
20#include <util/std_code.h>
21#include <util/std_expr.h>
22
23#include <iostream>
24#include <list>
25
26#include "accelerator.h"
29#include "path.h"
30#include "scratch_program.h"
31#include "util.h"
32
34 goto_programt::targett loop_header)
35{
37 natural_loops.loop_map.at(loop_header);
38 goto_programt::targett back_jump=loop_header;
39
40 for(const auto &t : loop)
41 {
42 if(
43 t->is_goto() && t->get_condition().is_true() && t->targets.size() == 1 &&
44 t->targets.front() == loop_header &&
45 t->location_number > back_jump->location_number)
46 {
47 back_jump=t;
48 }
49 }
50
51 return back_jump;
52}
53
55{
57 natural_loops.loop_map.at(loop_header);
58
59 for(const auto &t : loop)
60 {
61 if(t->is_backwards_goto())
62 {
63 if(t->targets.size()!=1 ||
64 t->get_target()!=loop_header)
65 {
66 return true;
67 }
68 }
69
70 // Header of some other loop?
71 if(t != loop_header && natural_loops.is_loop_header(t))
72 {
73 return true;
74 }
75 }
76
77 return false;
78}
79
81{
82 pathst loop_paths, exit_paths;
83 goto_programt::targett back_jump=find_back_jump(loop_header);
84 int num_accelerated=0;
85 std::list<path_acceleratort> accelerators;
87 natural_loops.loop_map.at(loop_header);
88
89 if(contains_nested_loops(loop_header))
90 {
91 // For now, only accelerate innermost loops.
92#ifdef DEBUG
93 std::cout << "Not accelerating an outer loop\n";
94#endif
95 return 0;
96 }
97
98 goto_programt::targett overflow_loc;
99 make_overflow_loc(loop_header, back_jump, overflow_loc);
100 program.update();
101
102#if 1
107 program,
108 loop,
109 loop_header,
112#else
114 acceleration(symbol_table, goto_functions, program, loop, loop_header);
115#endif
116
117 path_acceleratort accelerator;
118
119 while(acceleration.accelerate(accelerator) &&
120 (accelerate_limit < 0 ||
121 num_accelerated < accelerate_limit))
122 {
123 // set_dirty_vars(accelerator);
124
125 if(is_underapproximate(accelerator))
126 {
127 // We have some underapproximated variables -- just punt for now.
128#ifdef DEBUG
129 std::cout << "Not inserting accelerator because of underapproximation\n";
130#endif
131
132 continue;
133 }
134
135 accelerators.push_back(accelerator);
136 num_accelerated++;
137
138#ifdef DEBUG
139 std::cout << "Accelerated path:\n";
140 output_path(accelerator.path, program, ns, std::cout);
141
142 std::cout << "Accelerator has "
143 << accelerator.pure_accelerator.instructions.size()
144 << " instructions\n";
145#endif
146 }
147
149 program.insert_before_swap(loop_header, skip);
150
151 goto_programt::targett new_inst=loop_header;
152 ++new_inst;
153
154 loop.insert_instruction(new_inst);
155
156 std::cout << "Overflow loc is " << overflow_loc->location_number << '\n';
157 std::cout << "Back jump is " << back_jump->location_number << '\n';
158
159 for(std::list<path_acceleratort>::iterator it=accelerators.begin();
160 it!=accelerators.end();
161 ++it)
162 {
163 subsumed_patht inserted(it->path);
164
165 insert_accelerator(loop_header, back_jump, *it, inserted);
166 subsumed.push_back(inserted);
167 num_accelerated++;
168 }
169
170 return num_accelerated;
171}
172
174 goto_programt::targett &loop_header,
175 goto_programt::targett &back_jump,
176 path_acceleratort &accelerator,
177 subsumed_patht &subsumed_path)
178{
180 loop_header,
181 back_jump,
182 accelerator.pure_accelerator,
183 subsumed_path.accelerator);
184
185 if(!accelerator.overflow_path.instructions.empty())
186 {
188 loop_header, back_jump, accelerator.overflow_path, subsumed_path.residue);
189 }
190}
191
192/*
193 * Insert a looping path (usually an accelerator) into a goto-program,
194 * beginning at loop_header and jumping back to loop_header via back_jump.
195 * Stores the locations at which the looping path was added in inserted_path.
196 *
197 * THIS DESTROYS looping_path!!
198 */
200 goto_programt::targett &loop_header,
201 goto_programt::targett &back_jump,
202 goto_programt &looping_path,
203 patht &inserted_path)
204{
205 goto_programt::targett loop_body=loop_header;
206 ++loop_body;
207
209 loop_body,
211 loop_body,
213 loop_body->source_location()));
214
215 program.destructive_insert(loop_body, looping_path);
216
217 jump = program.insert_before(
218 loop_body, goto_programt::make_goto(back_jump, true_exprt()));
219
220 for(goto_programt::targett t=loop_header;
221 t!=loop_body;
222 ++t)
223 {
224 inserted_path.push_back(path_nodet(t));
225 }
226
227 inserted_path.push_back(path_nodet(back_jump));
228}
229
231 goto_programt::targett loop_header,
232 goto_programt::targett &loop_end,
233 goto_programt::targett &overflow_loc)
234{
235 symbolt overflow_sym=utils.fresh_symbol("accelerate::overflow", bool_typet());
236 const exprt &overflow_var=overflow_sym.symbol_expr();
238 natural_loops.loop_map.at(loop_header);
239 overflow_instrumentert instrumenter(program, overflow_var, symbol_table);
240
241 for(const auto &loop_instruction : loop)
242 {
243 overflow_locs[loop_instruction] = goto_programt::targetst();
244 goto_programt::targetst &added = overflow_locs[loop_instruction];
245
246 instrumenter.add_overflow_checks(loop_instruction, added);
247 for(const auto &new_instruction : added)
248 loop.insert_instruction(new_instruction);
249 }
250
252 loop_header,
254 t->swap(*loop_header);
255 loop.insert_instruction(t);
256 overflow_locs[loop_header].push_back(t);
257
258 overflow_loc = program.insert_after(loop_end, goto_programt::make_skip());
259 overflow_loc->swap(*loop_end);
260 loop.insert_instruction(overflow_loc);
261
263 loop_end, goto_programt::make_goto(overflow_loc, not_exprt(overflow_var)));
264 t2->swap(*loop_end);
265 overflow_locs[overflow_loc].push_back(t2);
266 loop.insert_instruction(t2);
267
268 goto_programt::targett tmp=overflow_loc;
269 overflow_loc=loop_end;
270 loop_end=tmp;
271}
272
274{
275 trace_automatont automaton(program);
276
277 for(subsumed_pathst::iterator it=subsumed.begin();
278 it!=subsumed.end();
279 ++it)
280 {
281 if(!it->subsumed.empty())
282 {
283#ifdef DEBUG
285 std::cout << "Restricting path:\n";
286 output_path(it->subsumed, program, ns, std::cout);
287#endif
288
289 automaton.add_path(it->subsumed);
290 }
291
292 patht double_accelerator;
293 patht::iterator jt=double_accelerator.begin();
294 double_accelerator.insert(
295 jt, it->accelerator.begin(), it->accelerator.end());
296 double_accelerator.insert(
297 jt, it->accelerator.begin(), it->accelerator.end());
298
299#ifdef DEBUG
301 std::cout << "Restricting path:\n";
302 output_path(double_accelerator, program, ns, std::cout);
303#endif
304 automaton.add_path(double_accelerator);
305 }
306
307 std::cout << "Building trace automaton...\n";
308
309 automaton.build();
310 insert_automaton(automaton);
311}
312
314{
315 for(std::set<exprt>::iterator it=accelerator.dirty_vars.begin();
316 it!=accelerator.dirty_vars.end();
317 ++it)
318 {
319 expr_mapt::iterator jt=dirty_vars_map.find(*it);
320 exprt dirty_var;
321
322 if(jt==dirty_vars_map.end())
323 {
325 symbolt new_sym=utils.fresh_symbol("accelerate::dirty", bool_typet());
326 dirty_var=new_sym.symbol_expr();
327 dirty_vars_map[*it]=dirty_var;
328 }
329 else
330 {
331 dirty_var=jt->second;
332 }
333
334#ifdef DEBUG
335 std::cout << "Setting dirty flag " << expr2c(dirty_var, ns)
336 << " for " << expr2c(*it, ns) << '\n';
337#endif
338
339 accelerator.pure_accelerator.add(
341 }
342}
343
345{
346 for(expr_mapt::iterator it=dirty_vars_map.begin();
347 it!=dirty_vars_map.end();
348 ++it)
349 {
353 }
354
356
358 it!=program.instructions.end();
359 it=next)
360 {
361 next=it;
362 ++next;
363
364 // If this is an assign to a tracked variable, clear the dirty flag.
365 // Note: this order of insertions means that we assume each of the read
366 // variables is clean _before_ clearing any dirty flags.
367 if(it->is_assign())
368 {
369 const exprt &lhs = it->assign_lhs();
370 expr_mapt::iterator dirty_var=dirty_vars_map.find(lhs);
371
372 if(dirty_var!=dirty_vars_map.end())
373 {
375 code_assignt(dirty_var->second, false_exprt()));
376 program.insert_before_swap(it, clear_flag);
377 }
378 }
379
380 // Find which symbols are read, i.e. those appearing in a guard or on
381 // the right hand side of an assignment. Assume each is not dirty.
383
384 if(it->has_condition())
385 find_symbols_or_nexts(it->get_condition(), read);
386
387 if(it->is_assign())
388 {
389 find_symbols_or_nexts(it->assign_rhs(), read);
390 }
391
392 for(find_symbols_sett::iterator jt=read.begin();
393 jt!=read.end();
394 ++jt)
395 {
396 const exprt &var=ns.lookup(*jt).symbol_expr();
397 expr_mapt::iterator dirty_var=dirty_vars_map.find(var);
398
399 if(dirty_var==dirty_vars_map.end())
400 {
401 continue;
402 }
403
405 goto_programt::make_assumption(not_exprt(dirty_var->second));
406 program.insert_before_swap(it, not_dirty);
407 }
408 }
409}
410
412{
413 for(std::set<exprt>::iterator it=accelerator.dirty_vars.begin();
414 it!=accelerator.dirty_vars.end();
415 ++it)
416 {
417 if(it->id()==ID_symbol && it->type() == bool_typet())
418 {
419 const irep_idt &id=to_symbol_expr(*it).get_identifier();
420 const symbolt &sym = symbol_table.lookup_ref(id);
421
422 if(sym.module=="scratch")
423 {
424 continue;
425 }
426 }
427
428#ifdef DEBUG
429 std::cout << "Underapproximate variable: " << expr2c(*it, ns) << '\n';
430#endif
431 return true;
432 }
433
434 return false;
435}
436
438{
439 symbolt ret;
440 ret.module="accelerate";
441 ret.name=name;
442 ret.base_name=name;
443 ret.pretty_name=name;
444 ret.type=type;
445
446 symbol_table.add(ret);
447
448 return ret;
449}
450
452{
453#if 0
455 code_declt code(sym);
456
457 decl->make_decl();
458 decl->code=code;
459#endif
460}
461
463{
464 decl(sym, t);
465
468}
469
471{
472 symbolt state_sym=make_symbol("trace_automaton::state",
474 symbolt next_state_sym=make_symbol("trace_automaton::next_state",
476 symbol_exprt state=state_sym.symbol_expr();
477 symbol_exprt next_state=next_state_sym.symbol_expr();
478
479 trace_automatont::sym_mapt transitions;
480 state_sett accept_states;
481
482 automaton.get_transitions(transitions);
483 automaton.accept_states(accept_states);
484
485 std::cout
486 << "Inserting trace automaton with "
487 << automaton.num_states() << " states, "
488 << accept_states.size() << " accepting states and "
489 << transitions.size() << " transitions\n";
490
491 // Declare the variables we'll use to encode the state machine.
493 decl(state, t, from_integer(automaton.init_state(), state.type()));
494 decl(next_state, t);
495
496 // Now for each program location that appears as a symbol in the
497 // trace automaton, add the appropriate code to drive the state
498 // machine.
499 for(const auto &sym : automaton.alphabet)
500 {
501 scratch_programt state_machine{
503 trace_automatont::sym_range_pairt p=transitions.equal_range(sym);
504
505 build_state_machine(p.first, p.second, accept_states, state, next_state,
506 state_machine);
507
508 program.insert_before_swap(sym, state_machine);
509 }
510}
511
513 trace_automatont::sym_mapt::iterator begin,
514 trace_automatont::sym_mapt::iterator end,
515 state_sett &accept_states,
516 symbol_exprt state,
517 symbol_exprt next_state,
518 scratch_programt &state_machine)
519{
520 std::map<unsigned int, unsigned int> successor_counts;
521 unsigned int max_count=0;
522 unsigned int likely_next=0;
523
524 // Optimisation: find the most common successor state and initialise
525 // next_state to that value. This reduces the size of the state machine
526 // driver substantially.
527 for(trace_automatont::sym_mapt::iterator p=begin; p!=end; ++p)
528 {
529 trace_automatont::state_pairt state_pair=p->second;
530 unsigned int to=state_pair.second;
531 unsigned int count=0;
532
533 if(successor_counts.find(to)==successor_counts.end())
534 {
535 count=1;
536 }
537 else
538 {
539 count=successor_counts[to] + 1;
540 }
541
542 successor_counts[to]=count;
543
544 if(count > max_count)
545 {
546 max_count=count;
547 likely_next=to;
548 }
549 }
550
551 // Optimisation: if there is only one possible successor state, just
552 // jump straight to it instead of driving the whole machine.
553 if(successor_counts.size()==1)
554 {
555 if(accept_states.find(likely_next)!=accept_states.end())
556 {
557 // It's an accept state. Just assume(false).
558 state_machine.assume(false_exprt());
559 }
560 else
561 {
562 state_machine.assign(state,
563 from_integer(likely_next, next_state.type()));
564 }
565
566 return;
567 }
568
569 state_machine.assign(next_state,
570 from_integer(likely_next, next_state.type()));
571
572 for(trace_automatont::sym_mapt::iterator p=begin; p!=end; ++p)
573 {
574 trace_automatont::state_pairt state_pair=p->second;
575 unsigned int from=state_pair.first;
576 unsigned int to=state_pair.second;
577
578 if(to==likely_next)
579 {
580 continue;
581 }
582
583 // We're encoding the transition
584 //
585 // from -loc-> to
586 //
587 // which we encode by inserting:
588 //
589 // next_state=(state==from) ? to : next_state;
590 //
591 // just before loc.
592 equal_exprt guard(state, from_integer(from, state.type()));
593 if_exprt rhs(guard, from_integer(to, next_state.type()), next_state);
594 state_machine.assign(next_state, rhs);
595 }
596
597 // Update the state and assume(false) if we've hit an accept state.
598 state_machine.assign(state, next_state);
599
600 for(state_sett::iterator it=accept_states.begin();
601 it!=accept_states.end();
602 ++it)
603 {
604 state_machine.assume(
605 not_exprt(equal_exprt(state, from_integer(*it, state.type()))));
606 }
607}
608
610{
611 int num_accelerated=0;
612
613 for(natural_loops_mutablet::loop_mapt::iterator it =
614 natural_loops.loop_map.begin();
615 it!=natural_loops.loop_map.end();
616 ++it)
617 {
618 goto_programt::targett t=it->first;
619 num_accelerated += accelerate_loop(t);
620 }
621
622 program.update();
623
624 if(num_accelerated > 0)
625 {
626 std::cout << "Engaging crush mode...\n";
627
629 // add_dirty_checks();
630 program.update();
631
632 std::cout << "Crush mode engaged.\n";
633 }
634
635 return num_accelerated;
636}
637
639 goto_modelt &goto_model,
640 message_handlert &message_handler,
641 bool use_z3,
642 guard_managert &guard_manager)
643{
644 for(auto &gf_entry : goto_model.goto_functions.function_map)
645 {
646 std::cout << "Accelerating function " << gf_entry.first << '\n';
647 acceleratet accelerate(
648 gf_entry.second.body, goto_model, message_handler, use_z3, guard_manager);
649
650 int num_accelerated=accelerate.accelerate_loops();
651
652 if(num_accelerated > 0)
653 {
654 std::cout << "Added " << num_accelerated
655 << " accelerator(s)\n";
656 }
657 }
658}
void accelerate_functions(goto_modelt &goto_model, message_handlert &message_handler, bool use_z3, guard_managert &guard_manager)
Definition: accelerate.cpp:638
Loop Acceleration.
Loop Acceleration.
constant_exprt from_integer(const mp_integer &int_value, const typet &type)
Definition: arith_tools.cpp:99
void add_dirty_checks()
Definition: accelerate.cpp:344
void insert_accelerator(goto_programt::targett &loop_header, goto_programt::targett &back_jump, path_acceleratort &accelerator, subsumed_patht &subsumed_path)
Definition: accelerate.cpp:173
void insert_automaton(trace_automatont &automaton)
Definition: accelerate.cpp:470
acceleration_utilst utils
Definition: accelerate.h:118
goto_programt & program
Definition: accelerate.h:111
symbolt make_symbol(std::string name, typet type)
Definition: accelerate.cpp:437
natural_loops_mutablet natural_loops
Definition: accelerate.h:116
message_handlert & message_handler
Definition: accelerate.h:57
void decl(symbol_exprt &sym, goto_programt::targett t)
Definition: accelerate.cpp:451
symbol_tablet & symbol_table
Definition: accelerate.h:113
expr_mapt dirty_vars_map
Definition: accelerate.h:124
subsumed_pathst subsumed
Definition: accelerate.h:117
int accelerate_loops()
Definition: accelerate.cpp:609
bool contains_nested_loops(goto_programt::targett &loop_header)
Definition: accelerate.cpp:54
void build_state_machine(trace_automatont::sym_mapt::iterator p, trace_automatont::sym_mapt::iterator end, state_sett &accept_states, symbol_exprt state, symbol_exprt next_state, scratch_programt &state_machine)
Definition: accelerate.cpp:512
void make_overflow_loc(goto_programt::targett loop_header, goto_programt::targett &loop_end, goto_programt::targett &overflow_loc)
Definition: accelerate.cpp:230
void restrict_traces()
Definition: accelerate.cpp:273
overflow_mapt overflow_locs
Definition: accelerate.h:122
namespacet ns
Definition: accelerate.h:115
void set_dirty_vars(path_acceleratort &accelerator)
Definition: accelerate.cpp:313
goto_functionst & goto_functions
Definition: accelerate.h:112
bool is_underapproximate(path_acceleratort &accelerator)
Definition: accelerate.cpp:411
static const int accelerate_limit
Definition: accelerate.h:54
goto_programt::targett find_back_jump(goto_programt::targett loop_header)
Definition: accelerate.cpp:33
guard_managert & guard_manager
Definition: accelerate.h:114
void insert_looping_path(goto_programt::targett &loop_header, goto_programt::targett &back_jump, goto_programt &looping_path, patht &inserted_path)
Definition: accelerate.cpp:199
int accelerate_loop(goto_programt::targett &loop_header)
Definition: accelerate.cpp:80
symbolt fresh_symbol(std::string base, typet type)
The Boolean type.
Definition: std_types.h:36
A codet representing an assignment in the program.
A codet representing the declaration of a local variable.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
bool accelerate(path_acceleratort &accelerator)
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
function_mapt function_map
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:33
This class represents an instruction in the GOTO intermediate representation.
Definition: goto_program.h:180
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
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
void update()
Update all indices.
void insert_before_swap(targett target)
Insertion that preserves jumps to "target".
Definition: goto_program.h:619
void destructive_insert(const_targett target, goto_programt &p)
Inserts the given program p before target.
Definition: goto_program.h:706
instructionst::iterator targett
Definition: goto_program.h:592
static instructiont make_assignment(const code_assignt &_code, const source_locationt &l=source_locationt::nil())
Create an assignment instruction.
static instructiont make_skip(const source_locationt &l=source_locationt::nil())
Definition: goto_program.h:880
targett insert_after(const_targett target)
Insertion after the instruction pointed-to by the given instruction iterator target.
Definition: goto_program.h:684
targett add(instructiont &&instruction)
Adds a given instruction at the end.
Definition: goto_program.h:715
static instructiont make_goto(targett _target, 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.
Definition: goto_program.h:668
std::list< targett > targetst
Definition: goto_program.h:594
The trinary if-then-else operator.
Definition: std_expr.h:2226
bool is_loop_header(const T instruction) const
Returns true if instruction is the header of any loop.
Definition: loop_analysis.h:93
loop_mapt loop_map
Definition: loop_analysis.h:88
A loop, specified as a set of instructions.
Definition: loop_analysis.h:24
bool insert_instruction(const T instruction)
Adds instruction to this loop.
Definition: loop_analysis.h:74
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Definition: namespace.cpp:138
Boolean negation.
Definition: std_expr.h:2181
goto_programt overflow_path
Definition: accelerator.h:64
std::set< exprt > dirty_vars
Definition: accelerator.h:66
goto_programt pure_accelerator
Definition: accelerator.h:63
targett assume(const exprt &guard)
targett assign(const exprt &lhs, const exprt &rhs)
A side_effect_exprt that returns a non-deterministically chosen value.
Definition: std_code.h:1520
patht residue
Definition: subsumed.h:30
patht accelerator
Definition: subsumed.h:29
Expression to hold a symbol (variable)
Definition: std_expr.h:80
const irep_idt & get_identifier() const
Definition: std_expr.h:109
bool add(const symbolt &symbol)
Add a new symbol to the symbol table.
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
irep_idt base_name
Base (non-scoped) name.
Definition: symbol.h:46
irep_idt module
Name of module the symbol belongs to.
Definition: symbol.h:43
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
irep_idt name
The unique identifier.
Definition: symbol.h:40
irep_idt pretty_name
Language-specific display name.
Definition: symbol.h:52
void get_transitions(sym_mapt &transitions)
void accept_states(state_sett &states)
std::multimap< goto_programt::targett, state_pairt > sym_mapt
std::pair< sym_mapt::iterator, sym_mapt::iterator > sym_range_pairt
std::pair< statet, statet > state_pairt
unsigned num_states()
void add_path(patht &path)
The Boolean constant true.
Definition: std_expr.h:2856
The type of an expression, extends irept.
Definition: type.h:29
const source_locationt & source_location() const
Definition: type.h:74
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
Goto Programs with Functions.
@ SKIP
Definition: goto_program.h:38
Compute natural loops in a goto_function.
Loop Acceleration.
void output_path(const patht &path, const goto_programt &program, const namespacet &ns, std::ostream &str)
Definition: path.cpp:16
Loop Acceleration.
std::list< patht > pathst
Definition: path.h:45
std::list< path_nodet > patht
Definition: path.h:44
Loop Acceleration.
API to expression classes.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:189
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:20
std::set< statet > state_sett
unsignedbv_typet unsigned_poly_type()
Definition: util.cpp:25
Loop Acceleration.