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 
21 
22 #include "polynomial.h"
23 #include "path.h"
24 #include "acceleration_utils.h"
25 #include "cone_of_influence.h"
26 
27 class path_acceleratort;
29 
31 {
32 public:
35  const symbol_tablet &_symbol_table,
36  const goto_functionst &_goto_functions,
39  symbol_table(const_cast<symbol_tablet &>(_symbol_table)),
41  goto_functions(_goto_functions),
44  {
46  }
47 
50  const symbol_tablet &_symbol_table,
51  const goto_functionst &_goto_functions,
52  exprt &_loop_counter,
55  symbol_table(const_cast<symbol_tablet &>(_symbol_table)),
57  goto_functions(_goto_functions),
60  loop_counter(_loop_counter)
61  {
62  }
63 
64  bool accelerate(patht &loop, path_acceleratort &accelerator);
65 
66  bool fit_polynomial(
68  exprt &target,
69  polynomialt &polynomial);
70 
71 protected:
73 
75  goto_programt::instructionst &sliced_body,
76  exprt &target,
77  expr_sett &influence,
78  polynomialt &polynomial);
79 
80  void assert_for_values(
81  scratch_programt &program,
82  std::map<exprt, int> &values,
83  std::set<std::pair<expr_listt, exprt>> &coefficients,
84  int num_unwindings,
86  exprt &target,
87  overflow_instrumentert &overflow);
89  scratch_programt &program,
90  std::set<std::pair<expr_listt, exprt>> &coefficients,
91  polynomialt &polynomial);
92  void cone_of_influence(
94  exprt &target,
96  expr_sett &influence);
97 
98  bool fit_const(
100  exprt &target,
101  polynomialt &polynomial);
102 
103  bool check_inductive(
104  std::map<exprt, polynomialt> polynomials,
106  void stash_variables(
107  scratch_programt &program,
108  expr_sett modified,
109  substitutiont &substitution);
110  void stash_polynomials(
111  scratch_programt &program,
112  std::map<exprt, polynomialt> &polynomials,
113  std::map<exprt, exprt> &stashed,
115 
116  exprt precondition(patht &path);
117 
119  std::map<exprt, polynomialt> polynomials,
120  patht &body,
121  exprt &guard);
122 
123  typedef std::pair<exprt, exprt> expr_pairt;
124  typedef std::vector<expr_pairt> expr_pairst;
125 
127  {
132 
133  typedef std::vector<polynomial_array_assignmentt>
135 
136  bool do_arrays(
137  goto_programt::instructionst &loop_body,
138  std::map<exprt, polynomialt> &polynomials,
139  substitutiont &substitution,
140  scratch_programt &program);
142  goto_programt::instructionst &loop_body,
143  expr_sett &arrays_written);
145  expr_pairst &array_assignments,
146  std::map<exprt, polynomialt> &polynomials,
147  polynomial_array_assignmentst &array_polynomials,
148  polynomialst &nondet_indices);
149  bool expr2poly(
150  exprt &expr,
151  std::map<exprt, polynomialt> &polynomials,
152  polynomialt &poly);
153 
155 
157  const namespacet ns;
161 
163 
165 };
166 
168 
169 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_POLYNOMIAL_ACCELERATOR_H
Loop Acceleration.
Base class for all expressions.
Definition: expr.h:54
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:71
std::list< instructiont > instructionst
Definition: goto_program.h:644
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:91
The NIL expression.
Definition: std_expr.h:2820
bool expr2poly(exprt &expr, std::map< exprt, polynomialt > &polynomials, polynomialt &poly)
std::vector< expr_pairt > expr_pairst
std::vector< polynomial_array_assignmentt > polynomial_array_assignmentst
void stash_variables(scratch_programt &program, expr_sett modified, substitutiont &substitution)
polynomial_acceleratort(message_handlert &message_handler, const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions, exprt &_loop_counter, guard_managert &guard_manager)
void stash_polynomials(scratch_programt &program, std::map< exprt, polynomialt > &polynomials, std::map< exprt, exprt > &stashed, goto_programt::instructionst &body)
bool fit_polynomial_sliced(goto_programt::instructionst &sliced_body, exprt &target, expr_sett &influence, polynomialt &polynomial)
std::pair< exprt, exprt > expr_pairt
bool array_assignments2polys(expr_pairst &array_assignments, std::map< exprt, polynomialt > &polynomials, polynomial_array_assignmentst &array_polynomials, polynomialst &nondet_indices)
bool accelerate(patht &loop, path_acceleratort &accelerator)
bool check_inductive(std::map< exprt, polynomialt > polynomials, goto_programt::instructionst &body)
expr_pairst gather_array_assignments(goto_programt::instructionst &loop_body, expr_sett &arrays_written)
struct polynomial_acceleratort::polynomial_array_assignment polynomial_array_assignmentt
void extract_polynomial(scratch_programt &program, std::set< std::pair< expr_listt, exprt >> &coefficients, polynomialt &polynomial)
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)
bool fit_const(goto_programt::instructionst &loop_body, exprt &target, polynomialt &polynomial)
const goto_functionst & goto_functions
bool do_assumptions(std::map< exprt, polynomialt > polynomials, patht &body, exprt &guard)
bool do_arrays(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, substitutiont &substitution, scratch_programt &program)
polynomial_acceleratort(message_handlert &message_handler, const symbol_tablet &_symbol_table, const goto_functionst &_goto_functions, guard_managert &guard_manager)
void cone_of_influence(goto_programt::instructionst &orig_body, exprt &target, goto_programt::instructionst &body, expr_sett &influence)
bool fit_polynomial(goto_programt::instructionst &loop_body, exprt &target, polynomialt &polynomial)
void ensure_no_overflows(goto_programt &program)
message_handlert & message_handler
The symbol table.
Definition: symbol_table.h:14
Loop Acceleration.
std::unordered_set< exprt, irep_hash > expr_sett
Concrete Goto Program.
Loop Acceleration.
std::list< path_nodet > patht
Definition: path.h:44
Loop Acceleration.
std::vector< polynomialt > polynomialst
Definition: polynomial.h:63
std::map< exprt, exprt > substitutiont
Definition: polynomial.h:39
expr_sett find_modified(goto_programt::instructionst &body)
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition: guard_expr.h:20
Author: Diffblue Ltd.