cprover
polynomial_accelerator.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_POLYNOMIAL_ACCELERATOR_H
13 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_POLYNOMIAL_ACCELERATOR_H
14 
15 #include <map>
16 #include <set>
17 
18 #include <util/symbol_table.h>
19 
22 
23 #include "scratch_program.h"
24 #include "polynomial.h"
25 #include "path.h"
26 #include "accelerator.h"
27 #include "acceleration_utils.h"
28 #include "cone_of_influence.h"
29 #include "overflow_instrumenter.h"
30 
32 {
33 public:
36  const symbol_tablet &_symbol_table,
37  const goto_functionst &_goto_functions,
40  symbol_table(const_cast<symbol_tablet &>(_symbol_table)),
42  goto_functions(_goto_functions),
45  {
47  }
48 
51  const symbol_tablet &_symbol_table,
52  const goto_functionst &_goto_functions,
53  exprt &_loop_counter,
56  symbol_table(const_cast<symbol_tablet &>(_symbol_table)),
58  goto_functions(_goto_functions),
61  loop_counter(_loop_counter)
62  {
63  }
64 
65  bool accelerate(patht &loop, path_acceleratort &accelerator);
66 
67  bool fit_polynomial(
69  exprt &target,
70  polynomialt &polynomial);
71 
72 protected:
74 
76  goto_programt::instructionst &sliced_body,
77  exprt &target,
78  expr_sett &influence,
79  polynomialt &polynomial);
80 
81  void assert_for_values(
82  scratch_programt &program,
83  std::map<exprt, int> &values,
84  std::set<std::pair<expr_listt, exprt>> &coefficients,
85  int num_unwindings,
87  exprt &target,
88  overflow_instrumentert &overflow);
90  scratch_programt &program,
91  std::set<std::pair<expr_listt, exprt>> &coefficients,
92  polynomialt &polynomial);
93  void cone_of_influence(
95  exprt &target,
97  expr_sett &influence);
98 
99  bool fit_const(
100  goto_programt::instructionst &loop_body,
101  exprt &target,
102  polynomialt &polynomial);
103 
104  bool check_inductive(
105  std::map<exprt, polynomialt> polynomials,
107  void stash_variables(
108  scratch_programt &program,
109  expr_sett modified,
110  substitutiont &substitution);
111  void stash_polynomials(
112  scratch_programt &program,
113  std::map<exprt, polynomialt> &polynomials,
114  std::map<exprt, exprt> &stashed,
116 
117  exprt precondition(patht &path);
118 
120  std::map<exprt, polynomialt> polynomials,
121  patht &body,
122  exprt &guard);
123 
124  typedef std::pair<exprt, exprt> expr_pairt;
125  typedef std::vector<expr_pairt> expr_pairst;
126 
128  {
133 
134  typedef std::vector<polynomial_array_assignmentt>
136 
137  bool do_arrays(
138  goto_programt::instructionst &loop_body,
139  std::map<exprt, polynomialt> &polynomials,
140  substitutiont &substitution,
141  scratch_programt &program);
143  goto_programt::instructionst &loop_body,
144  expr_sett &arrays_written);
146  expr_pairst &array_assignments,
147  std::map<exprt, polynomialt> &polynomials,
148  polynomial_array_assignmentst &array_polynomials,
149  polynomialst &nondet_indices);
150  bool expr2poly(
151  exprt &expr,
152  std::map<exprt, polynomialt> &polynomials,
153  polynomialt &poly);
154 
156 
158  const namespacet ns;
162 
164 
166 };
167 
169 
170 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_POLYNOMIAL_ACCELERATOR_H
path.h
Loop Acceleration.
overflow_instrumenter.h
Loop Acceleration.
symbol_tablet
The symbol table.
Definition: symbol_table.h:20
polynomial_acceleratort::extract_polynomial
void extract_polynomial(scratch_programt &program, std::set< std::pair< expr_listt, exprt >> &coefficients, polynomialt &polynomial)
polynomialt
Definition: polynomial.h:42
acceleration_utilst
Definition: acceleration_utils.h:37
polynomial_acceleratort::message_handler
message_handlert & message_handler
Definition: polynomial_accelerator.h:73
polynomial_acceleratort::fit_polynomial
bool fit_polynomial(goto_programt::instructionst &loop_body, exprt &target, polynomialt &polynomial)
Definition: polynomial_accelerator.cpp:434
polynomial_acceleratort::cone_of_influence
void cone_of_influence(goto_programt::instructionst &orig_body, exprt &target, goto_programt::instructionst &body, expr_sett &influence)
Definition: polynomial_accelerator.cpp:614
polynomial_acceleratort::fit_polynomial_sliced
bool fit_polynomial_sliced(goto_programt::instructionst &sliced_body, exprt &target, expr_sett &influence, polynomialt &polynomial)
Definition: polynomial_accelerator.cpp:278
polynomial_acceleratort::do_arrays
bool do_arrays(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, substitutiont &substitution, scratch_programt &program)
polynomial_acceleratort::expr_pairst
std::vector< expr_pairt > expr_pairst
Definition: polynomial_accelerator.h:125
polynomial_acceleratort::fit_const
bool fit_const(goto_programt::instructionst &loop_body, exprt &target, polynomialt &polynomial)
Definition: polynomial_accelerator.cpp:447
goto_programt::instructionst
std::list< instructiont > instructionst
Definition: goto_program.h:577
polynomial.h
Loop Acceleration.
acceleration_utils.h
Loop Acceleration.
polynomial_acceleratort::stash_polynomials
void stash_polynomials(scratch_programt &program, std::map< exprt, polynomialt > &polynomials, std::map< exprt, exprt > &stashed, goto_programt::instructionst &body)
Definition: polynomial_accelerator.cpp:732
exprt
Base class for all expressions.
Definition: expr.h:53
polynomial_acceleratort::do_assumptions
bool do_assumptions(std::map< exprt, polynomialt > polynomials, patht &body, exprt &guard)
polynomial_acceleratort::symbol_table
symbol_tablet & symbol_table
Definition: polynomial_accelerator.h:157
scratch_program.h
Loop Acceleration.
polynomial_acceleratort::array_assignments2polys
bool array_assignments2polys(expr_pairst &array_assignments, std::map< exprt, polynomialt > &polynomials, polynomial_array_assignmentst &array_polynomials, polynomialst &nondet_indices)
polynomial_acceleratort::gather_array_assignments
expr_pairst gather_array_assignments(goto_programt::instructionst &loop_body, expr_sett &arrays_written)
polynomial_acceleratort::accelerate
bool accelerate(patht &loop, path_acceleratort &accelerator)
Definition: polynomial_accelerator.cpp:45
polynomial_acceleratort::precondition
exprt precondition(patht &path)
Definition: polynomial_accelerator.cpp:777
polynomial_acceleratort::ns
const namespacet ns
Definition: polynomial_accelerator.h:158
polynomial_acceleratort::ensure_no_overflows
void ensure_no_overflows(goto_programt &program)
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
polynomial_acceleratort::stash_variables
void stash_variables(scratch_programt &program, expr_sett modified, substitutiont &substitution)
Definition: polynomial_accelerator.cpp:750
scratch_programt
Definition: scratch_program.h:37
polynomial_acceleratort::polynomial_acceleratort
polynomial_acceleratort(message_handlert &message_handler, const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions, guard_managert &guard_manager)
Definition: polynomial_accelerator.h:34
nil_exprt
The NIL expression.
Definition: std_expr.h:3973
polynomial_acceleratort::check_inductive
bool check_inductive(std::map< exprt, polynomialt > polynomials, goto_programt::instructionst &body)
Definition: polynomial_accelerator.cpp:655
polynomial_acceleratort::polynomial_array_assignment::index
polynomialt index
Definition: polynomial_accelerator.h:130
polynomial_acceleratort::polynomial_array_assignment::value
polynomialt value
Definition: polynomial_accelerator.h:131
path_acceleratort
Definition: accelerator.h:27
expr_sett
std::unordered_set< exprt, irep_hash > expr_sett
Definition: cone_of_influence.h:21
polynomial_acceleratort::goto_functions
const goto_functionst & goto_functions
Definition: polynomial_accelerator.h:159
message_handlert
Definition: message.h:28
polynomial_acceleratort::polynomial_acceleratort
polynomial_acceleratort(message_handlert &message_handler, const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions, exprt &_loop_counter, guard_managert &guard_manager)
Definition: polynomial_accelerator.h:49
overflow_instrumentert
Definition: overflow_instrumenter.h:26
goto_program.h
Concrete Goto Program.
substitutiont
std::map< exprt, exprt > substitutiont
Definition: polynomial.h:39
polynomial_acceleratort::polynomial_array_assignment::array
exprt array
Definition: polynomial_accelerator.h:129
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
patht
std::list< path_nodet > patht
Definition: path.h:45
accelerator.h
Loop Acceleration.
cone_of_influence.h
Loop Acceleration.
polynomialst
std::vector< polynomialt > polynomialst
Definition: polynomial.h:63
polynomial_acceleratort
Definition: polynomial_accelerator.h:32
polynomial_acceleratort::polynomial_array_assignment
Definition: polynomial_accelerator.h:128
goto_functions.h
Goto Programs with Functions.
polynomial_acceleratort::expr_pairt
std::pair< exprt, exprt > expr_pairt
Definition: polynomial_accelerator.h:124
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
polynomial_acceleratort::polynomial_array_assignmentst
std::vector< polynomial_array_assignmentt > polynomial_array_assignmentst
Definition: polynomial_accelerator.h:135
polynomial_acceleratort::loop_counter
exprt loop_counter
Definition: polynomial_accelerator.h:163
polynomial_acceleratort::assert_for_values
void assert_for_values(scratch_programt &program, std::map< exprt, int > &values, std::set< std::pair< expr_listt, exprt >> &coefficients, int num_unwindings, goto_programt::instructionst &loop_body, exprt &target, overflow_instrumentert &overflow)
Definition: polynomial_accelerator.cpp:500
find_modified
expr_sett find_modified(goto_programt::instructionst &body)
polynomial_acceleratort::nonrecursive
expr_sett nonrecursive
Definition: polynomial_accelerator.h:165
symbol_table.h
Author: Diffblue Ltd.
polynomial_acceleratort::polynomial_array_assignmentt
struct polynomial_acceleratort::polynomial_array_assignment polynomial_array_assignmentt
polynomial_acceleratort::expr2poly
bool expr2poly(exprt &expr, std::map< exprt, polynomialt > &polynomials, polynomialt &poly)
polynomial_acceleratort::utils
acceleration_utilst utils
Definition: polynomial_accelerator.h:161
polynomial_acceleratort::guard_manager
guard_managert & guard_manager
Definition: polynomial_accelerator.h:160