cprover
acceleration_utils.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_ACCELERATION_UTILS_H
13 #define CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATION_UTILS_H
14 
15 #include <list>
16 #include <map>
17 #include <set>
18 
19 #include <util/symbol_table.h>
20 #include <util/message.h>
21 
24 
25 #include <analyses/natural_loops.h>
26 
27 #include "scratch_program.h"
28 #include "polynomial.h"
29 #include "path.h"
30 #include "accelerator.h"
31 #include "cone_of_influence.h"
32 
33 typedef std::unordered_map<exprt, exprt, irep_hash> expr_mapt;
34 typedef std::list<exprt> expr_listt;
35 
37 {
38 protected:
40 
41 public:
43  symbol_tablet &_symbol_table,
45  const goto_functionst &_goto_functions,
46  exprt &_loop_counter)
48  symbol_table(_symbol_table),
50  goto_functions(_goto_functions),
51  loop_counter(_loop_counter)
52  {
53  }
54 
56  symbol_tablet &_symbol_table,
58  const goto_functionst &_goto_functions)
60  symbol_table(_symbol_table),
62  goto_functions(_goto_functions),
64  {
65  }
66 
68  std::set<std::pair<expr_listt, exprt> > &coefficients,
69  polynomialt &polynomial);
70 
71  bool check_inductive(std::map<exprt, polynomialt> polynomials,
72  patht &path);
73  void stash_variables(scratch_programt &program,
74  expr_sett modified,
75  substitutiont &substitution);
76  void stash_polynomials(scratch_programt &program,
77  std::map<exprt, polynomialt> &polynomials,
78  std::map<exprt, exprt> &stashed,
79  patht &path);
80 
81  exprt precondition(patht &path);
82  void abstract_arrays(exprt &expr, expr_mapt &abstractions);
83  void push_nondet(exprt &expr);
84 
85  bool do_assumptions(std::map<exprt, polynomialt> polynomials,
86  patht &body,
87  exprt &guard);
88 
89  typedef std::pair<exprt, exprt> expr_pairt;
90  typedef std::vector<expr_pairt> expr_pairst;
91 
93  {
97  };
98 
99  typedef std::vector<polynomial_array_assignmentt>
101 
102  bool do_arrays(goto_programt::instructionst &loop_body,
103  std::map<exprt, polynomialt> &polynomials,
104  substitutiont &substitution,
105  scratch_programt &program);
107  goto_programt::instructionst &loop_body,
108  expr_sett &arrays_written);
110  expr_pairst &array_assignments,
111  std::map<exprt, polynomialt> &polynomials,
112  polynomial_array_assignmentst &array_polynomials,
113  polynomialst &nondet_indices);
114  bool expr2poly(
115  exprt &expr,
116  std::map<exprt, polynomialt> &polynomials,
117  polynomialt &poly);
118 
119  bool do_nonrecursive(
120  goto_programt::instructionst &loop_body,
121  std::map<exprt, polynomialt> &polynomials,
122  substitutiont &substitution,
123  expr_sett &nonrecursive,
124  scratch_programt &program);
125  bool assign_array(
126  const exprt &lhs,
127  const exprt &rhs,
128  scratch_programt &program);
129 
130  void gather_array_accesses(const exprt &expr, expr_sett &arrays);
131 
132  void gather_rvalues(const exprt &expr, expr_sett &rvalues);
133 
134  void ensure_no_overflows(scratch_programt &program);
135 
136  void find_modified(const patht &path, expr_sett &modified);
137  void find_modified(
138  const goto_programt &program,
139  expr_sett &modified);
140  void find_modified(
141  const goto_programt::instructionst &instructions,
142  expr_sett &modified);
143  void find_modified(
145  expr_sett &modified);
146  void find_modified(
148  expr_sett &modified);
149 
150  symbolt fresh_symbol(std::string base, typet type);
151 
157 };
158 
159 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATION_UTILS_H
std::list< exprt > expr_listt
The type of an expression, extends irept.
Definition: type.h:27
std::pair< exprt, exprt > expr_pairt
exprt precondition(patht &path)
acceleration_utilst(symbol_tablet &_symbol_table, message_handlert &message_handler, const goto_functionst &_goto_functions)
Goto Programs with Functions.
std::vector< polynomialt > polynomialst
Definition: polynomial.h:63
Symbol table entry.
Definition: symbol.h:27
acceleration_utilst(symbol_tablet &_symbol_table, message_handlert &message_handler, const goto_functionst &_goto_functions, exprt &_loop_counter)
std::vector< polynomial_array_assignmentt > polynomial_array_assignmentst
Loop Acceleration.
bool assign_array(const exprt &lhs, const exprt &rhs, scratch_programt &program)
std::list< instructiont > instructionst
Definition: goto_program.h:412
bool array_assignments2polys(expr_pairst &array_assignments, std::map< exprt, polynomialt > &polynomials, polynomial_array_assignmentst &array_polynomials, polynomialst &nondet_indices)
void ensure_no_overflows(scratch_programt &program)
std::vector< expr_pairt > expr_pairst
std::unordered_set< exprt, irep_hash > expr_sett
The NIL expression.
Definition: std_expr.h:4461
symbolt fresh_symbol(std::string base, typet type)
void stash_variables(scratch_programt &program, expr_sett modified, substitutiont &substitution)
void abstract_arrays(exprt &expr, expr_mapt &abstractions)
bool do_arrays(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, substitutiont &substitution, scratch_programt &program)
std::list< path_nodet > patht
Definition: path.h:45
The symbol table.
Definition: symbol_table.h:19
instructionst::const_iterator const_targett
Definition: goto_program.h:415
const goto_functionst & goto_functions
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
void find_modified(const patht &path, expr_sett &modified)
Loop Acceleration.
void gather_array_accesses(const exprt &expr, expr_sett &arrays)
A collection of goto functions.
void extract_polynomial(scratch_programt &program, std::set< std::pair< expr_listt, exprt > > &coefficients, polynomialt &polynomial)
bool check_inductive(std::map< exprt, polynomialt > polynomials, patht &path)
Author: Diffblue Ltd.
bool expr2poly(exprt &expr, std::map< exprt, polynomialt > &polynomials, polynomialt &poly)
void gather_rvalues(const exprt &expr, expr_sett &rvalues)
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
bool do_assumptions(std::map< exprt, polynomialt > polynomials, patht &body, exprt &guard)
Loop Acceleration.
Loop Acceleration.
Loop Acceleration.
Base class for all expressions.
Definition: expr.h:54
std::map< exprt, exprt > substitutiont
Definition: polynomial.h:39
message_handlert & message_handler
bool do_nonrecursive(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, substitutiont &substitution, expr_sett &nonrecursive, scratch_programt &program)
void push_nondet(exprt &expr)
symbol_tablet & symbol_table
Compute natural loops in a goto_function.
Concrete Goto Program.
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
expr_pairst gather_array_assignments(goto_programt::instructionst &loop_body, expr_sett &arrays_written)
void stash_polynomials(scratch_programt &program, std::map< exprt, polynomialt > &polynomials, std::map< exprt, exprt > &stashed, patht &path)