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 <map>
16 #include <set>
17 
18 #include <util/symbol_table.h>
19 
22 
23 #include <analyses/natural_loops.h>
24 
25 #include "scratch_program.h"
26 #include "polynomial.h"
27 #include "path.h"
28 #include "accelerator.h"
29 #include "cone_of_influence.h"
30 
31 typedef std::unordered_map<exprt, exprt, irep_hash> expr_mapt;
32 
34 {
35  public:
37  const goto_functionst &_goto_functions,
38  exprt &_loop_counter) :
39  symbol_table(_symbol_table),
41  goto_functions(_goto_functions),
42  loop_counter(_loop_counter)
43  {
44  }
45 
47  const goto_functionst &_goto_functions) :
48  symbol_table(_symbol_table),
50  goto_functions(_goto_functions),
52  {
53  }
54 
56  std::set<std::pair<expr_listt, exprt> > &coefficients,
57  polynomialt &polynomial);
58 
59  bool check_inductive(std::map<exprt, polynomialt> polynomials,
60  patht &path);
61  void stash_variables(scratch_programt &program,
62  expr_sett modified,
63  substitutiont &substitution);
64  void stash_polynomials(scratch_programt &program,
65  std::map<exprt, polynomialt> &polynomials,
66  std::map<exprt, exprt> &stashed,
67  patht &path);
68 
69  exprt precondition(patht &path);
70  void abstract_arrays(exprt &expr, expr_mapt &abstractions);
71  void push_nondet(exprt &expr);
72 
73  bool do_assumptions(std::map<exprt, polynomialt> polynomials,
74  patht &body,
75  exprt &guard);
76 
77  typedef std::pair<exprt, exprt> expr_pairt;
78  typedef std::vector<expr_pairt> expr_pairst;
79 
81  {
85  };
86 
87  typedef std::vector<polynomial_array_assignmentt>
89 
91  std::map<exprt, polynomialt> &polynomials,
93  substitutiont &substitution,
94  scratch_programt &program);
97  expr_sett &arrays_written);
99  expr_pairst &array_assignments,
100  std::map<exprt, polynomialt> &polynomials,
101  polynomial_array_assignmentst &array_polynomials,
102  polynomialst &nondet_indices);
103  bool expr2poly(
104  exprt &expr,
105  std::map<exprt, polynomialt> &polynomials,
106  polynomialt &poly);
107 
108  bool do_nonrecursive(
109  goto_programt::instructionst &loop_body,
110  std::map<exprt, polynomialt> &polynomials,
112  substitutiont &substitution,
113  expr_sett &nonrecursive,
114  scratch_programt &program);
115  bool assign_array(
116  const exprt &lhs,
117  const exprt &rhs,
118  const exprt &loop_counter,
119  scratch_programt &program);
120 
121  void gather_array_accesses(const exprt &expr, expr_sett &arrays);
122 
123  void gather_rvalues(const exprt &expr, expr_sett &rvalues);
124 
125  void ensure_no_overflows(scratch_programt &program);
126 
127  void find_modified(const patht &path, expr_sett &modified);
128  void find_modified(
129  const goto_programt &program,
130  expr_sett &modified);
131  void find_modified(
132  const goto_programt::instructionst &instructions,
133  expr_sett &modified);
134  void find_modified(
136  expr_sett &modified);
137  void find_modified(
139  expr_sett &modified);
140 
141  symbolt fresh_symbol(std::string base, typet type);
142 
148 
149  static int num_symbols;
150 };
151 
152 #endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATION_UTILS_H
The type of an expression.
Definition: type.h:20
acceleration_utilst(symbol_tablet &_symbol_table, const goto_functionst &_goto_functions)
std::pair< exprt, exprt > expr_pairt
exprt precondition(patht &path)
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:33
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)
instructionst::const_iterator const_targett
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:3764
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:52
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:62
void find_modified(const patht &path, expr_sett &modified)
Loop Acceleration.
void gather_array_accesses(const exprt &expr, expr_sett &arrays)
acceleration_utilst(symbol_tablet &_symbol_table, const goto_functionst &_goto_functions, exprt &_loop_counter)
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)
Symbol table.
bool expr2poly(exprt &expr, std::map< exprt, polynomialt > &polynomials, polynomialt &poly)
void gather_rvalues(const exprt &expr, expr_sett &rvalues)
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
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:46
std::map< exprt, exprt > substitutiont
Definition: polynomial.h:39
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)