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 
18 #include <analyses/natural_loops.h>
19 
21 
22 #include "path.h"
23 #include "accelerator.h"
24 #include "trace_automaton.h"
25 #include "subsumed.h"
26 #include "scratch_program.h"
27 #include "acceleration_utils.h"
28 
30 {
31  public:
33  goto_functionst &_goto_functions,
34  symbol_tablet &_symbol_table,
35  bool _use_z3) :
36  program(_program),
37  goto_functions(_goto_functions),
38  symbol_table(_symbol_table),
41  use_z3(_use_z3)
42  {
44  }
45 
46  int accelerate_loop(goto_programt::targett &loop_header);
47  int accelerate_loops();
48 
49  bool accelerate_path(patht &path, path_acceleratort &accelerator);
50 
51  void restrict_traces();
52 
53  static const int accelerate_limit = -1;
54 
55  protected:
56  void find_paths(goto_programt::targett &loop_header,
57  pathst &loop_paths,
58  pathst &exit_paths,
59  goto_programt::targett &back_jump);
60 
62  goto_programt::targett &loop_header,
64  patht &prefix,
65  pathst &loop_paths,
66  pathst &exit_paths,
67  goto_programt::targett &back_jump);
68 
70 
72  goto_programt::targett &back_jump,
73  goto_programt &looping_path,
74  patht &inserted_path);
76  goto_programt::targett &back_jump,
77  path_acceleratort &accelerator,
79 
80  void set_dirty_vars(path_acceleratort &accelerator);
81  void add_dirty_checks();
82  bool is_underapproximate(path_acceleratort &accelerator);
83 
85  goto_programt::targett &loop_end,
86  goto_programt::targett &overflow_loc);
87 
88  void insert_automaton(trace_automatont &automaton);
89  void build_state_machine(trace_automatont::sym_mapt::iterator p,
90  trace_automatont::sym_mapt::iterator end,
91  state_sett &accept_states,
92  symbol_exprt state,
93  symbol_exprt next_state,
94  scratch_programt &state_machine);
95 
96  symbolt make_symbol(std::string name, typet type);
98  void decl(symbol_exprt &sym, goto_programt::targett t, exprt init);
99 
101 
109 
110  typedef std::map<goto_programt::targett, goto_programt::targetst>
113 
115 
116  bool use_z3;
117 };
118 
120  goto_functionst &functions,
121  symbol_tablet &ns,
122  bool use_z3);
123 
124 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATE_H
expr_mapt dirty_vars_map
Definition: accelerate.h:114
The type of an expression.
Definition: type.h:20
void insert_automaton(trace_automatont &automaton)
Definition: accelerate.cpp:484
void make_overflow_loc(goto_programt::targett loop_header, goto_programt::targett &loop_end, goto_programt::targett &overflow_loc)
Definition: accelerate.cpp:236
natural_loops_mutablet natural_loops
Definition: accelerate.h:106
static const int accelerate_limit
Definition: accelerate.h:53
void insert_looping_path(goto_programt::targett &loop_header, goto_programt::targett &back_jump, goto_programt &looping_path, patht &inserted_path)
Definition: accelerate.cpp:205
goto_functionst & goto_functions
Definition: accelerate.h:103
Loop Acceleration.
bool contains_nested_loops(goto_programt::targett &loop_header)
Definition: accelerate.cpp:59
std::list< subsumed_patht > subsumed_pathst
Definition: subsumed.h:33
Goto Programs with Functions.
void accelerate_functions(goto_functionst &functions, symbol_tablet &ns, bool use_z3)
Definition: accelerate.cpp:652
int accelerate_loop(goto_programt::targett &loop_header)
Definition: accelerate.cpp:89
void set_dirty_vars(path_acceleratort &accelerator)
Definition: accelerate.cpp:325
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:33
subsumed_pathst subsumed
Definition: accelerate.h:107
symbol_tablet & symbol_table
Definition: accelerate.h:104
Loop Acceleration.
void add_dirty_checks()
Definition: accelerate.cpp:356
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)
goto_programt & program
Definition: accelerate.h:102
std::list< path_nodet > patht
Definition: path.h:45
The symbol table.
Definition: symbol_table.h:52
TO_BE_DOCUMENTED.
Definition: namespace.h:62
bool is_underapproximate(path_acceleratort &accelerator)
Definition: accelerate.cpp:422
Loop Acceleration.
std::list< patht > pathst
Definition: path.h:46
void insert_accelerator(goto_programt::targett &loop_header, goto_programt::targett &back_jump, path_acceleratort &accelerator, subsumed_patht &subsumed)
Definition: accelerate.cpp:182
void find_paths(goto_programt::targett &loop_header, pathst &loop_paths, pathst &exit_paths, goto_programt::targett &back_jump)
std::set< statet > state_sett
symbolt make_symbol(std::string name, typet type)
Definition: accelerate.cpp:448
goto_programt::targett find_back_jump(goto_programt::targett loop_header)
Definition: accelerate.cpp:34
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
std::map< goto_programt::targett, goto_programt::targetst > overflow_mapt
Definition: accelerate.h:111
Loop Acceleration.
void decl(symbol_exprt &sym, goto_programt::targett t)
Definition: accelerate.cpp:462
acceleratet(goto_programt &_program, goto_functionst &_goto_functions, symbol_tablet &_symbol_table, bool _use_z3)
Definition: accelerate.h:32
Loop Acceleration.
bool accelerate_path(patht &path, path_acceleratort &accelerator)
Loop Acceleration.
Base class for all expressions.
Definition: expr.h:46
overflow_mapt overflow_locs
Definition: accelerate.h:112
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:525
Expression to hold a symbol (variable)
Definition: std_expr.h:82
void restrict_traces()
Definition: accelerate.cpp:285
Compute natural loops in a goto_function.
int accelerate_loops()
Definition: accelerate.cpp:622
acceleration_utilst utils
Definition: accelerate.h:108
namespacet ns
Definition: accelerate.h:105
std::unordered_map< exprt, exprt, irep_hash > expr_mapt