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,
105  substitutiont &substitution,
106  scratch_programt &program);
108  goto_programt::instructionst &loop_body,
109  expr_sett &arrays_written);
111  expr_pairst &array_assignments,
112  std::map<exprt, polynomialt> &polynomials,
113  polynomial_array_assignmentst &array_polynomials,
114  polynomialst &nondet_indices);
115  bool expr2poly(
116  exprt &expr,
117  std::map<exprt, polynomialt> &polynomials,
118  polynomialt &poly);
119 
120  bool do_nonrecursive(
121  goto_programt::instructionst &loop_body,
122  std::map<exprt, polynomialt> &polynomials,
124  substitutiont &substitution,
125  expr_sett &nonrecursive,
126  scratch_programt &program);
127  bool assign_array(
128  const exprt &lhs,
129  const exprt &rhs,
130  const exprt &loop_counter,
131  scratch_programt &program);
132 
133  void gather_array_accesses(const exprt &expr, expr_sett &arrays);
134 
135  void gather_rvalues(const exprt &expr, expr_sett &rvalues);
136 
137  void ensure_no_overflows(scratch_programt &program);
138 
139  void find_modified(const patht &path, expr_sett &modified);
140  void find_modified(
141  const goto_programt &program,
142  expr_sett &modified);
143  void find_modified(
144  const goto_programt::instructionst &instructions,
145  expr_sett &modified);
146  void find_modified(
148  expr_sett &modified);
149  void find_modified(
151  expr_sett &modified);
152 
153  symbolt fresh_symbol(std::string base, typet type);
154 
160 
161  static int num_symbols;
162 };
163 
164 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATION_UTILS_H
std::list< exprt > expr_listt
The type of an expression.
Definition: type.h:22
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.This is a symbol in the symbol table, stored in an object of type symbol_tablet...
Definition: symbol.h:30
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 do_arrays(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, exprt &loop_counter, substitutiont &substitution, scratch_programt &program)
std::list< instructiont > instructionst
Definition: goto_program.h:395
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:4508
symbolt fresh_symbol(std::string base, typet type)
bool assign_array(const exprt &lhs, const exprt &rhs, const exprt &loop_counter, scratch_programt &program)
void stash_variables(scratch_programt &program, expr_sett modified, substitutiont &substitution)
void abstract_arrays(exprt &expr, expr_mapt &abstractions)
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:398
bool do_nonrecursive(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, exprt &loop_counter, substitutiont &substitution, expr_sett &nonrecursive, scratch_programt &program)
const goto_functionst & goto_functions
TO_BE_DOCUMENTED.
Definition: namespace.h:74
void find_modified(const patht &path, expr_sett &modified)
Loop Acceleration.
void gather_array_accesses(const exprt &expr, expr_sett &arrays)
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:70
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:42
std::map< exprt, exprt > substitutiont
Definition: polynomial.h:39
message_handlert & message_handler
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)