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