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