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)
39  program(_program),
40  goto_functions(_goto_model.goto_functions),
41  symbol_table(_goto_model.symbol_table),
42  ns(_goto_model.symbol_table),
44  use_z3(_use_z3)
45  {
47  }
48 
49  int accelerate_loop(goto_programt::targett &loop_header);
50  int accelerate_loops();
51 
52  bool accelerate_path(patht &path, path_acceleratort &accelerator);
53 
54  void restrict_traces();
55 
56  static const int accelerate_limit = -1;
57 
58 protected:
60 
61  void find_paths(
62  goto_programt::targett &loop_header,
63  pathst &loop_paths,
64  pathst &exit_paths,
65  goto_programt::targett &back_jump);
66 
67  void extend_path(
69  goto_programt::targett &loop_header,
71  patht &prefix,
72  pathst &loop_paths,
73  pathst &exit_paths,
74  goto_programt::targett &back_jump);
75 
77 
79  goto_programt::targett &loop_header,
80  goto_programt::targett &back_jump,
81  goto_programt &looping_path,
82  patht &inserted_path);
83  void insert_accelerator(
84  goto_programt::targett &loop_header,
85  goto_programt::targett &back_jump,
86  path_acceleratort &accelerator,
88 
89  void set_dirty_vars(path_acceleratort &accelerator);
90  void add_dirty_checks();
91  bool is_underapproximate(path_acceleratort &accelerator);
92 
93  void make_overflow_loc(
94  goto_programt::targett loop_header,
95  goto_programt::targett &loop_end,
96  goto_programt::targett &overflow_loc);
97 
98  void insert_automaton(trace_automatont &automaton);
100  trace_automatont::sym_mapt::iterator p,
101  trace_automatont::sym_mapt::iterator end,
102  state_sett &accept_states,
103  symbol_exprt state,
104  symbol_exprt next_state,
105  scratch_programt &state_machine);
106 
107  symbolt make_symbol(std::string name, typet type);
109  void decl(symbol_exprt &sym, goto_programt::targett t, exprt init);
110 
112 
120 
121  typedef std::map<goto_programt::targett, goto_programt::targetst>
124 
126 
127  bool use_z3;
128 };
129 
131  goto_modelt &,
133  bool use_z3);
134 
135 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATE_H
expr_mapt dirty_vars_map
Definition: accelerate.h:125
The type of an expression.
Definition: type.h:22
void insert_automaton(trace_automatont &automaton)
Definition: accelerate.cpp:480
acceleratet(goto_programt &_program, goto_modelt &_goto_model, message_handlert &message_handler, bool _use_z3)
Definition: accelerate.h:33
void make_overflow_loc(goto_programt::targett loop_header, goto_programt::targett &loop_end, goto_programt::targett &overflow_loc)
Definition: accelerate.cpp:232
natural_loops_mutablet natural_loops
Definition: accelerate.h:117
static const int accelerate_limit
Definition: accelerate.h:56
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:114
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.
message_handlert & message_handler
Definition: accelerate.h:59
int accelerate_loop(goto_programt::targett &loop_header)
Definition: accelerate.cpp:89
void set_dirty_vars(path_acceleratort &accelerator)
Definition: accelerate.cpp:321
Symbol table entry.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
subsumed_pathst subsumed
Definition: accelerate.h:118
symbol_tablet & symbol_table
Definition: accelerate.h:115
Loop Acceleration.
void add_dirty_checks()
Definition: accelerate.cpp:352
instructionst::iterator targett
Definition: goto_program.h:397
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:113
std::list< path_nodet > patht
Definition: path.h:45
The symbol table.
Definition: symbol_table.h:19
TO_BE_DOCUMENTED.
Definition: namespace.h:74
bool is_underapproximate(path_acceleratort &accelerator)
Definition: accelerate.cpp:418
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:444
goto_programt::targett find_back_jump(goto_programt::targett loop_header)
Definition: accelerate.cpp:34
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
std::map< goto_programt::targett, goto_programt::targetst > overflow_mapt
Definition: accelerate.h:122
Loop Acceleration.
void decl(symbol_exprt &sym, goto_programt::targett t)
Definition: accelerate.cpp:458
void accelerate_functions(goto_modelt &, message_handlert &message_handler, bool use_z3)
Definition: accelerate.cpp:647
Loop Acceleration.
bool accelerate_path(patht &path, path_acceleratort &accelerator)
Loop Acceleration.
Base class for all expressions.
Definition: expr.h:42
overflow_mapt overflow_locs
Definition: accelerate.h:123
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:521
Expression to hold a symbol (variable)
Definition: std_expr.h:90
void restrict_traces()
Definition: accelerate.cpp:281
Compute natural loops in a goto_function.
goto_programt coverage_criteriont message_handlert & message_handler
Definition: cover.cpp:66
int accelerate_loops()
Definition: accelerate.cpp:618
acceleration_utilst utils
Definition: accelerate.h:119
namespacet ns
Definition: accelerate.h:116
std::unordered_map< exprt, exprt, irep_hash > expr_mapt