CBMC
Loading...
Searching...
No Matches
accelerate.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Loop Acceleration
4
5Author: 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
18
19#include "path.h"
20#include "trace_automaton.h"
21#include "subsumed.h"
22#include "acceleration_utils.h"
23
25
27{
28public:
46
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
56protected:
58
60 goto_programt::targett &loop_header,
64
67 goto_programt::targett &loop_header,
69 patht &prefix,
73
75
77 goto_programt::targett &loop_header,
82 goto_programt::targett &loop_header,
84 path_acceleratort &accelerator,
86
87 void set_dirty_vars(path_acceleratort &accelerator);
88 void add_dirty_checks();
89 bool is_underapproximate(path_acceleratort &accelerator);
90
92 goto_programt::targett loop_header,
95
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,
104
105 symbolt make_symbol(std::string name, typet type);
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)
Loop Acceleration.
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
void add_dirty_checks()
void insert_accelerator(goto_programt::targett &loop_header, goto_programt::targett &back_jump, path_acceleratort &accelerator, subsumed_patht &subsumed_path)
void insert_automaton(trace_automatont &automaton)
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)
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)
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()
bool contains_nested_loops(goto_programt::targett &loop_header)
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)
void make_overflow_loc(goto_programt::targett loop_header, goto_programt::targett &loop_end, goto_programt::targett &overflow_loc)
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()
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)
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)
static const int accelerate_limit
Definition accelerate.h:54
goto_programt::targett find_back_jump(goto_programt::targett loop_header)
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)
int accelerate_loop(goto_programt::targett &loop_header)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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.
instructionst::iterator targett
std::list< targett > targetst
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Expression to hold a symbol (variable)
Definition std_expr.h:131
The symbol table.
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.
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