cprover
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 #include <util/expr.h>
17 #include <util/message.h>
18 
19 #include <analyses/natural_loops.h>
20 
22 
23 #include "path.h"
24 #include "accelerator.h"
25 #include "trace_automaton.h"
26 #include "subsumed.h"
27 #include "scratch_program.h"
28 #include "acceleration_utils.h"
29 
31 {
32 public:
34  goto_programt &_program,
35  goto_modelt &_goto_model,
37  bool _use_z3,
40  program(_program),
41  goto_functions(_goto_model.goto_functions),
42  symbol_table(_goto_model.symbol_table),
44  ns(_goto_model.symbol_table),
46  use_z3(_use_z3)
47  {
49  }
50 
51  int accelerate_loop(goto_programt::targett &loop_header);
52  int accelerate_loops();
53 
54  bool accelerate_path(patht &path, path_acceleratort &accelerator);
55 
56  void restrict_traces();
57 
58  static const int accelerate_limit = -1;
59 
60 protected:
62 
63  void find_paths(
64  goto_programt::targett &loop_header,
65  pathst &loop_paths,
66  pathst &exit_paths,
67  goto_programt::targett &back_jump);
68 
71  goto_programt::targett &loop_header,
73  patht &prefix,
74  pathst &loop_paths,
75  pathst &exit_paths,
76  goto_programt::targett &back_jump);
77 
79 
81  goto_programt::targett &loop_header,
82  goto_programt::targett &back_jump,
83  goto_programt &looping_path,
84  patht &inserted_path);
85  void insert_accelerator(
86  goto_programt::targett &loop_header,
87  goto_programt::targett &back_jump,
88  path_acceleratort &accelerator,
89  subsumed_patht &subsumed_path);
90 
91  void set_dirty_vars(path_acceleratort &accelerator);
92  void add_dirty_checks();
93  bool is_underapproximate(path_acceleratort &accelerator);
94 
95  void make_overflow_loc(
96  goto_programt::targett loop_header,
97  goto_programt::targett &loop_end,
98  goto_programt::targett &overflow_loc);
99 
100  void insert_automaton(trace_automatont &automaton);
101  void build_state_machine(
102  trace_automatont::sym_mapt::iterator p,
103  trace_automatont::sym_mapt::iterator end,
104  state_sett &accept_states,
105  symbol_exprt state,
106  symbol_exprt next_state,
107  scratch_programt &state_machine);
108 
109  symbolt make_symbol(std::string name, typet type);
111  void decl(symbol_exprt &sym, goto_programt::targett t, exprt init);
112 
114 
123 
124  typedef std::map<goto_programt::targett, goto_programt::targetst>
127 
129 
130  bool use_z3;
131 };
132 
134  goto_modelt &,
135  message_handlert &message_handler,
136  bool use_z3,
137  guard_managert &guard_manager);
138 
139 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATE_H
subsumed.h
Loop Acceleration.
acceleratet::restrict_traces
void restrict_traces()
Definition: accelerate.cpp:274
subsumed_patht
Definition: subsumed.h:20
path.h
Loop Acceleration.
acceleratet::accelerate_limit
static const int accelerate_limit
Definition: accelerate.h:58
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
acceleratet::utils
acceleration_utilst utils
Definition: accelerate.h:122
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
acceleration_utilst
Definition: acceleration_utils.h:37
accelerate_functions
void accelerate_functions(goto_modelt &, message_handlert &message_handler, bool use_z3, guard_managert &guard_manager)
Definition: accelerate.cpp:639
acceleratet::guard_manager
guard_managert & guard_manager
Definition: accelerate.h:118
typet
The type of an expression, extends irept.
Definition: type.h:29
pathst
std::list< patht > pathst
Definition: path.h:46
acceleratet::symbol_table
symbol_tablet & symbol_table
Definition: accelerate.h:117
acceleratet
Definition: accelerate.h:31
trace_automaton.h
Loop Acceleration.
acceleration_utils.h
Loop Acceleration.
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
scratch_program.h
Loop Acceleration.
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
namespace.h
subsumed_pathst
std::list< subsumed_patht > subsumed_pathst
Definition: subsumed.h:33
acceleratet::subsumed
subsumed_pathst subsumed
Definition: accelerate.h:121
acceleratet::is_underapproximate
bool is_underapproximate(path_acceleratort &accelerator)
Definition: accelerate.cpp:412
expr.h
acceleratet::accelerate_loop
int accelerate_loop(goto_programt::targett &loop_header)
Definition: accelerate.cpp:81
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
acceleratet::extend_path
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)
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
trace_automatont
Definition: trace_automaton.h:89
scratch_programt
Definition: scratch_program.h:37
acceleratet::acceleratet
acceleratet(goto_programt &_program, goto_modelt &_goto_model, message_handlert &message_handler, bool _use_z3, guard_managert &guard_manager)
Definition: accelerate.h:33
acceleratet::overflow_mapt
std::map< goto_programt::targett, goto_programt::targetst > overflow_mapt
Definition: accelerate.h:125
acceleratet::find_paths
void find_paths(goto_programt::targett &loop_header, pathst &loop_paths, pathst &exit_paths, goto_programt::targett &back_jump)
acceleratet::add_dirty_checks
void add_dirty_checks()
Definition: accelerate.cpp:345
loop_templatet
A loop, specified as a set of instructions.
Definition: loop_analysis.h:24
path_acceleratort
Definition: accelerator.h:27
acceleratet::accelerate_path
bool accelerate_path(patht &path, path_acceleratort &accelerator)
message_handlert
Definition: message.h:28
acceleratet::program
goto_programt & program
Definition: accelerate.h:115
natural_loops_templatet< goto_programt, goto_programt::targett >
acceleratet::use_z3
bool use_z3
Definition: accelerate.h:130
acceleratet::make_symbol
symbolt make_symbol(std::string name, typet type)
Definition: accelerate.cpp:438
acceleratet::overflow_locs
overflow_mapt overflow_locs
Definition: accelerate.h:126
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
acceleratet::accelerate_loops
int accelerate_loops()
Definition: accelerate.cpp:610
patht
std::list< path_nodet > patht
Definition: path.h:45
accelerator.h
Loop Acceleration.
symbolt
Symbol table entry.
Definition: symbol.h:28
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
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
acceleratet::ns
namespacet ns
Definition: accelerate.h:119
acceleratet::insert_automaton
void insert_automaton(trace_automatont &automaton)
Definition: accelerate.cpp:471
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
message.h
expr_mapt
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
Definition: acceleration_utils.h:33
acceleratet::natural_loops
natural_loops_mutablet natural_loops
Definition: accelerate.h:120
acceleratet::goto_functions
goto_functionst & goto_functions
Definition: accelerate.h:116
acceleratet::dirty_vars_map
expr_mapt dirty_vars_map
Definition: accelerate.h:128
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
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