CBMC
Loading...
Searching...
No Matches
acceleration_utils.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Loop Acceleration
4
5Author: 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
20
21#include <analyses/guard.h>
23
24#include "polynomial.h"
25#include "path.h"
26#include "cone_of_influence.h"
27
30
31typedef std::unordered_map<exprt, exprt, irep_hash> expr_mapt;
32typedef std::list<exprt> expr_listt;
33
35{
36protected:
38
39public:
52
64
66 scratch_programt &program,
67 std::set<std::pair<expr_listt, exprt>> &coefficients,
69
70 bool check_inductive(
71 std::map<exprt, polynomialt> polynomials,
72 patht &path,
73 guard_managert &guard_manager);
75 expr_sett modified,
78 std::map<exprt, polynomialt> &polynomials,
79 std::map<exprt, exprt> &stashed,
80 patht &path);
81
84 void push_nondet(exprt &expr);
85
86 bool do_assumptions(
87 std::map<exprt, polynomialt> polynomials,
88 patht &body,
89 exprt &guard,
90 guard_managert &guard_manager);
91
92 typedef std::pair<exprt, exprt> expr_pairt;
93 typedef std::vector<expr_pairt> expr_pairst;
94
101
102 typedef std::vector<polynomial_array_assignmentt>
104
106 std::map<exprt, polynomialt> &polynomials,
108 scratch_programt &program);
114 std::map<exprt, polynomialt> &polynomials,
117 bool expr2poly(
118 exprt &expr,
119 std::map<exprt, polynomialt> &polynomials,
121
122 bool do_nonrecursive(
124 std::map<exprt, polynomialt> &polynomials,
126 expr_sett &nonrecursive,
127 scratch_programt &program);
128 bool assign_array(
129 const index_exprt &lhs,
130 const exprt &rhs,
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
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
162#endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATION_UTILS_H
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
std::list< exprt > expr_listt
static exprt guard(const exprt::operandst &guards, exprt cond)
symbol_table_baset & symbol_table
void push_nondet(exprt &expr)
bool array_assignments2polys(expr_pairst &array_assignments, std::map< exprt, polynomialt > &polynomials, polynomial_array_assignmentst &array_polynomials, polynomialst &nondet_indices)
void find_modified(const patht &path, expr_sett &modified)
std::vector< polynomial_array_assignmentt > polynomial_array_assignmentst
std::pair< exprt, exprt > expr_pairt
const goto_functionst & goto_functions
bool do_nonrecursive(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, substitutiont &substitution, expr_sett &nonrecursive, scratch_programt &program)
bool do_arrays(goto_programt::instructionst &loop_body, std::map< exprt, polynomialt > &polynomials, substitutiont &substitution, scratch_programt &program)
void stash_polynomials(scratch_programt &program, std::map< exprt, polynomialt > &polynomials, std::map< exprt, exprt > &stashed, patht &path)
bool expr2poly(exprt &expr, std::map< exprt, polynomialt > &polynomials, polynomialt &poly)
message_handlert & message_handler
bool check_inductive(std::map< exprt, polynomialt > polynomials, patht &path, guard_managert &guard_manager)
bool assign_array(const index_exprt &lhs, const exprt &rhs, scratch_programt &program)
void gather_rvalues(const exprt &expr, expr_sett &rvalues)
acceleration_utilst(symbol_table_baset &_symbol_table, message_handlert &message_handler, const goto_functionst &_goto_functions, exprt &_loop_counter)
symbolt fresh_symbol(std::string base, typet type)
void abstract_arrays(exprt &expr, expr_mapt &abstractions)
std::vector< expr_pairt > expr_pairst
bool do_assumptions(std::map< exprt, polynomialt > polynomials, patht &body, exprt &guard, guard_managert &guard_manager)
void ensure_no_overflows(scratch_programt &program)
void extract_polynomial(scratch_programt &program, std::set< std::pair< expr_listt, exprt > > &coefficients, polynomialt &polynomial)
exprt precondition(patht &path)
void gather_array_accesses(const exprt &expr, expr_sett &arrays)
acceleration_utilst(symbol_table_baset &_symbol_table, message_handlert &message_handler, const goto_functionst &_goto_functions)
void stash_variables(scratch_programt &program, expr_sett modified, substitutiont &substitution)
expr_pairst gather_array_assignments(goto_programt::instructionst &loop_body, expr_sett &arrays_written)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
Base class for all expressions.
Definition expr.h:56
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
std::list< instructiont > instructionst
Array index operator.
Definition std_expr.h:1470
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:3208
The symbol table base class interface.
Symbol table entry.
Definition symbol.h:28
The type of an expression, extends irept.
Definition type.h:29
Loop Acceleration.
std::unordered_set< exprt, irep_hash > expr_sett
Concrete Goto Program.
Guard Data Structure.
Compute natural loops in a goto_function.
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
This is unused by this implementation of guards, but can be used by other implementations of the same...
Definition guard_expr.h:20