cprover
disjunctive_polynomial_acceleration.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_DISJUNCTIVE_POLYNOMIAL_ACCELERATION_H
13 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_DISJUNCTIVE_POLYNOMIAL_ACCELERATION_H
14 
15 #include <map>
16 #include <set>
17 
18 #include <util/symbol_table.h>
19 #include <util/message.h>
20 
23 
24 #include <analyses/natural_loops.h>
25 
26 #include "scratch_program.h"
27 #include "polynomial.h"
28 #include "path.h"
29 #include "accelerator.h"
30 #include "cone_of_influence.h"
31 #include "acceleration_utils.h"
32 
34 {
35 public:
38  symbol_tablet &_symbol_table,
39  goto_functionst &_goto_functions,
40  goto_programt &_goto_program,
42  goto_programt::targett _loop_header,
45  symbol_table(_symbol_table),
47  goto_functions(_goto_functions),
48  goto_program(_goto_program),
50  loop(_loop),
51  loop_header(_loop_header),
53  {
56  build_fixed();
58  }
59 
60  bool accelerate(path_acceleratort &accelerator);
61 
62  bool fit_polynomial(
63  exprt &target,
64  polynomialt &polynomial,
65  patht &path);
66 
67  bool find_path(patht &path);
68 
69 protected:
71 
72  void assert_for_values(
73  scratch_programt &program,
74  std::map<exprt, exprt> &values,
75  std::set<std::pair<expr_listt, exprt> > &coefficients,
76  int num_unwindings,
77  goto_programt &loop_body,
78  exprt &target);
79  void cone_of_influence(const exprt &target, expr_sett &cone);
80 
82 
83  void build_path(scratch_programt &scratch_program, patht &path);
84  void build_fixed();
85 
86  void record_path(scratch_programt &scratch_program);
87 
88  bool depends_on_array(const exprt &e, exprt &array);
89 
97 
98  typedef std::map<goto_programt::targett, exprt> distinguish_mapt;
99  typedef std::map<exprt, bool> distinguish_valuest;
100 
104  std::list<symbol_exprt> distinguishers;
107  std::list<distinguish_valuest> accelerated_paths;
108 };
109 
110 // NOLINTNEXTLINE(whitespace/line_length)
111 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_DISJUNCTIVE_POLYNOMIAL_ACCELERATION_H
path.h
Loop Acceleration.
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
polynomialt
Definition: polynomial.h:42
disjunctive_polynomial_accelerationt::utils
acceleration_utilst utils
Definition: disjunctive_polynomial_acceleration.h:101
disjunctive_polynomial_accelerationt::build_path
void build_path(scratch_programt &scratch_program, patht &path)
Definition: disjunctive_polynomial_acceleration.cpp:776
acceleration_utilst
Definition: acceleration_utils.h:37
disjunctive_polynomial_accelerationt::distinguish_mapt
std::map< goto_programt::targett, exprt > distinguish_mapt
Definition: disjunctive_polynomial_acceleration.h:98
disjunctive_polynomial_accelerationt::distinguish_valuest
std::map< exprt, bool > distinguish_valuest
Definition: disjunctive_polynomial_acceleration.h:99
disjunctive_polynomial_accelerationt::goto_functions
goto_functionst & goto_functions
Definition: disjunctive_polynomial_acceleration.h:92
disjunctive_polynomial_accelerationt::find_path
bool find_path(patht &path)
Definition: disjunctive_polynomial_acceleration.cpp:339
polynomial.h
Loop Acceleration.
acceleration_utils.h
Loop Acceleration.
disjunctive_polynomial_accelerationt::goto_program
goto_programt & goto_program
Definition: disjunctive_polynomial_acceleration.h:93
disjunctive_polynomial_accelerationt::find_distinguishing_points
void find_distinguishing_points()
Definition: disjunctive_polynomial_acceleration.cpp:753
disjunctive_polynomial_accelerationt::message_handler
message_handlert & message_handler
Definition: disjunctive_polynomial_acceleration.h:70
disjunctive_polynomial_accelerationt::assert_for_values
void assert_for_values(scratch_programt &program, std::map< exprt, exprt > &values, std::set< std::pair< expr_listt, exprt > > &coefficients, int num_unwindings, goto_programt &loop_body, exprt &target)
Definition: disjunctive_polynomial_acceleration.cpp:648
exprt
Base class for all expressions.
Definition: expr.h:53
scratch_program.h
Loop Acceleration.
disjunctive_polynomial_accelerationt::disjunctive_polynomial_accelerationt
disjunctive_polynomial_accelerationt(message_handlert &message_handler, symbol_tablet &_symbol_table, goto_functionst &_goto_functions, goto_programt &_goto_program, natural_loops_mutablet::natural_loopt &_loop, goto_programt::targett _loop_header, guard_managert &guard_manager)
Definition: disjunctive_polynomial_acceleration.h:36
acceleration_utilst::find_modified
void find_modified(const patht &path, expr_sett &modified)
Definition: acceleration_utils.cpp:86
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
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
disjunctive_polynomial_accelerationt::loop_header
goto_programt::targett loop_header
Definition: disjunctive_polynomial_acceleration.h:96
disjunctive_polynomial_accelerationt::loop_counter
exprt loop_counter
Definition: disjunctive_polynomial_acceleration.h:102
scratch_programt
Definition: scratch_program.h:37
nil_exprt
The NIL expression.
Definition: std_expr.h:3973
disjunctive_polynomial_accelerationt::modified
expr_sett modified
Definition: disjunctive_polynomial_acceleration.h:105
loop_templatet
A loop, specified as a set of instructions.
Definition: loop_analysis.h:24
disjunctive_polynomial_accelerationt::symbol_table
symbol_tablet & symbol_table
Definition: disjunctive_polynomial_acceleration.h:90
path_acceleratort
Definition: accelerator.h:27
expr_sett
std::unordered_set< exprt, irep_hash > expr_sett
Definition: cone_of_influence.h:21
message_handlert
Definition: message.h:28
disjunctive_polynomial_accelerationt::accelerate
bool accelerate(path_acceleratort &accelerator)
Definition: disjunctive_polynomial_acceleration.cpp:49
disjunctive_polynomial_accelerationt::loop
natural_loops_mutablet::natural_loopt & loop
Definition: disjunctive_polynomial_acceleration.h:95
disjunctive_polynomial_accelerationt::distinguishing_points
distinguish_mapt distinguishing_points
Definition: disjunctive_polynomial_acceleration.h:103
disjunctive_polynomial_accelerationt::guard_manager
guard_managert & guard_manager
Definition: disjunctive_polynomial_acceleration.h:94
disjunctive_polynomial_accelerationt
Definition: disjunctive_polynomial_acceleration.h:34
goto_program.h
Concrete Goto Program.
disjunctive_polynomial_accelerationt::ns
namespacet ns
Definition: disjunctive_polynomial_acceleration.h:91
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
disjunctive_polynomial_accelerationt::build_fixed
void build_fixed()
Definition: disjunctive_polynomial_acceleration.cpp:854
disjunctive_polynomial_accelerationt::depends_on_array
bool depends_on_array(const exprt &e, exprt &array)
Definition: disjunctive_polynomial_acceleration.cpp:1017
patht
std::list< path_nodet > patht
Definition: path.h:45
accelerator.h
Loop Acceleration.
disjunctive_polynomial_accelerationt::fixed
goto_programt fixed
Definition: disjunctive_polynomial_acceleration.h:106
natural_loops.h
Compute natural loops in a goto_function.
cone_of_influence.h
Loop Acceleration.
disjunctive_polynomial_accelerationt::fit_polynomial
bool fit_polynomial(exprt &target, polynomialt &polynomial, patht &path)
Definition: disjunctive_polynomial_acceleration.cpp:400
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
disjunctive_polynomial_accelerationt::record_path
void record_path(scratch_programt &scratch_program)
Definition: disjunctive_polynomial_acceleration.cpp:1002
disjunctive_polynomial_accelerationt::distinguishers
std::list< symbol_exprt > distinguishers
Definition: disjunctive_polynomial_acceleration.h:104
disjunctive_polynomial_accelerationt::accelerated_paths
std::list< distinguish_valuest > accelerated_paths
Definition: disjunctive_polynomial_acceleration.h:107
symbol_table.h
Author: Diffblue Ltd.
message.h
disjunctive_polynomial_accelerationt::cone_of_influence
void cone_of_influence(const exprt &target, expr_sett &cone)
Definition: disjunctive_polynomial_acceleration.cpp:745
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579