CBMC
accelerate.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Loop Acceleration
4 
5 Author: Matt Lewis
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATE_H
13 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATE_H
14 
15 #include <util/namespace.h>
16 
17 #include <analyses/natural_loops.h>
18 
19 #include "path.h"
20 #include "trace_automaton.h"
21 #include "subsumed.h"
22 #include "acceleration_utils.h"
23 
24 class path_acceleratort;
25 
27 {
28 public:
30  goto_programt &_program,
31  goto_modelt &_goto_model,
33  bool _use_z3,
36  program(_program),
37  goto_functions(_goto_model.goto_functions),
38  symbol_table(_goto_model.symbol_table),
40  ns(_goto_model.symbol_table),
42  use_z3(_use_z3)
43  {
45  }
46 
47  int accelerate_loop(goto_programt::targett &loop_header);
48  int accelerate_loops();
49 
50  bool accelerate_path(patht &path, path_acceleratort &accelerator);
51 
52  void restrict_traces();
53 
54  static const int accelerate_limit = -1;
55 
56 protected:
58 
59  void find_paths(
60  goto_programt::targett &loop_header,
61  pathst &loop_paths,
62  pathst &exit_paths,
63  goto_programt::targett &back_jump);
64 
67  goto_programt::targett &loop_header,
69  patht &prefix,
70  pathst &loop_paths,
71  pathst &exit_paths,
72  goto_programt::targett &back_jump);
73 
75 
77  goto_programt::targett &loop_header,
78  goto_programt::targett &back_jump,
79  goto_programt &looping_path,
80  patht &inserted_path);
81  void insert_accelerator(
82  goto_programt::targett &loop_header,
83  goto_programt::targett &back_jump,
84  path_acceleratort &accelerator,
85  subsumed_patht &subsumed_path);
86 
87  void set_dirty_vars(path_acceleratort &accelerator);
88  void add_dirty_checks();
89  bool is_underapproximate(path_acceleratort &accelerator);
90 
91  void make_overflow_loc(
92  goto_programt::targett loop_header,
93  goto_programt::targett &loop_end,
94  goto_programt::targett &overflow_loc);
95 
96  void insert_automaton(trace_automatont &automaton);
98  trace_automatont::sym_mapt::iterator p,
99  trace_automatont::sym_mapt::iterator end,
100  state_sett &accept_states,
101  symbol_exprt state,
102  symbol_exprt next_state,
103  scratch_programt &state_machine);
104 
105  symbolt make_symbol(std::string name, typet type);
107  void decl(symbol_exprt &sym, goto_programt::targett t, exprt init);
108 
110 
119 
120  typedef std::map<
126 
128 
129  bool use_z3;
130 };
131 
133  goto_modelt &,
134  message_handlert &message_handler,
135  bool use_z3,
136  guard_managert &guard_manager);
137 
138 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATE_H
void accelerate_functions(goto_modelt &, message_handlert &message_handler, bool use_z3, guard_managert &guard_manager)
Definition: accelerate.cpp:635
Loop Acceleration.
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
void add_dirty_checks()
Definition: accelerate.cpp:348
void insert_accelerator(goto_programt::targett &loop_header, goto_programt::targett &back_jump, path_acceleratort &accelerator, subsumed_patht &subsumed_path)
Definition: accelerate.cpp:177
void insert_automaton(trace_automatont &automaton)
Definition: accelerate.cpp:467
acceleration_utilst utils
Definition: accelerate.h:118
goto_programt & program
Definition: accelerate.h:111
bool accelerate_path(patht &path, path_acceleratort &accelerator)
symbolt make_symbol(std::string name, typet type)
Definition: accelerate.cpp:436
void extend_path(goto_programt::targett &t, goto_programt::targett &loop_header, natural_loops_mutablet::natural_loopt &loop, patht &prefix, pathst &loop_paths, pathst &exit_paths, goto_programt::targett &back_jump)
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:448
symbol_tablet & symbol_table
Definition: accelerate.h:113
expr_mapt dirty_vars_map
Definition: accelerate.h:127
subsumed_pathst subsumed
Definition: accelerate.h:117
int accelerate_loops()
Definition: accelerate.cpp:606
bool contains_nested_loops(goto_programt::targett &loop_header)
Definition: accelerate.cpp:58
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:509
void make_overflow_loc(goto_programt::targett loop_header, goto_programt::targett &loop_end, goto_programt::targett &overflow_loc)
Definition: accelerate.cpp:234
acceleratet(goto_programt &_program, goto_modelt &_goto_model, message_handlert &message_handler, bool _use_z3, guard_managert &guard_manager)
Definition: accelerate.h:29
void restrict_traces()
Definition: accelerate.cpp:277
overflow_mapt overflow_locs
Definition: accelerate.h:125
namespacet ns
Definition: accelerate.h:115
std::map< goto_programt::targett, goto_programt::targetst, goto_programt::target_less_than > overflow_mapt
Definition: accelerate.h:124
void set_dirty_vars(path_acceleratort &accelerator)
Definition: accelerate.cpp:317
void find_paths(goto_programt::targett &loop_header, pathst &loop_paths, pathst &exit_paths, goto_programt::targett &back_jump)
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:37
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:203
int accelerate_loop(goto_programt::targett &loop_header)
Definition: accelerate.cpp:84
Base class for all expressions.
Definition: expr.h:56
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst::iterator targett
Definition: goto_program.h:614
std::list< targett > targetst
Definition: goto_program.h:616
A loop, specified as a set of instructions.
Definition: loop_analysis.h:24
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
Expression to hold a symbol (variable)
Definition: std_expr.h:131
The symbol table.
Definition: symbol_table.h:14
Symbol table entry.
Definition: symbol.h:28
The type of an expression, extends irept.
Definition: type.h:29
Compute natural loops in a goto_function.
Loop Acceleration.
std::list< patht > pathst
Definition: path.h:45
std::list< path_nodet > patht
Definition: path.h:44
A total order over targett and const_targett.
Definition: goto_program.h:392
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:20
Loop Acceleration.
std::list< subsumed_patht > subsumed_pathst
Definition: subsumed.h:33
Loop Acceleration.
std::set< statet > state_sett