cprover
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
19#include <util/symbol_table.h>
20
22
23#include <analyses/guard.h>
25
26#include "polynomial.h"
27#include "path.h"
28#include "cone_of_influence.h"
29
32
33typedef std::unordered_map<exprt, exprt, irep_hash> expr_mapt;
34typedef std::list<exprt> expr_listt;
35
37{
38protected:
40
41public:
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 scratch_programt &program,
69 std::set<std::pair<expr_listt, exprt>> &coefficients,
70 polynomialt &polynomial);
71
72 bool check_inductive(
73 std::map<exprt, polynomialt> polynomials,
74 patht &path,
75 guard_managert &guard_manager);
77 expr_sett modified,
78 substitutiont &substitution);
80 std::map<exprt, polynomialt> &polynomials,
81 std::map<exprt, exprt> &stashed,
82 patht &path);
83
85 void abstract_arrays(exprt &expr, expr_mapt &abstractions);
86 void push_nondet(exprt &expr);
87
88 bool do_assumptions(
89 std::map<exprt, polynomialt> polynomials,
90 patht &body,
91 exprt &guard,
92 guard_managert &guard_manager);
93
94 typedef std::pair<exprt, exprt> expr_pairt;
95 typedef std::vector<expr_pairt> expr_pairst;
96
98 {
102 };
103
104 typedef std::vector<polynomial_array_assignmentt>
106
108 std::map<exprt, polynomialt> &polynomials,
109 substitutiont &substitution,
110 scratch_programt &program);
113 expr_sett &arrays_written);
115 expr_pairst &array_assignments,
116 std::map<exprt, polynomialt> &polynomials,
117 polynomial_array_assignmentst &array_polynomials,
118 polynomialst &nondet_indices);
119 bool expr2poly(
120 exprt &expr,
121 std::map<exprt, polynomialt> &polynomials,
122 polynomialt &poly);
123
124 bool do_nonrecursive(
126 std::map<exprt, polynomialt> &polynomials,
127 substitutiont &substitution,
128 expr_sett &nonrecursive,
129 scratch_programt &program);
130 bool assign_array(
131 const index_exprt &lhs,
132 const exprt &rhs,
133 scratch_programt &program);
134
135 void gather_array_accesses(const exprt &expr, expr_sett &arrays);
136
137 void gather_rvalues(const exprt &expr, expr_sett &rvalues);
138
140
141 void find_modified(const patht &path, expr_sett &modified);
142 void find_modified(
143 const goto_programt &program,
144 expr_sett &modified);
145 void find_modified(
146 const goto_programt::instructionst &instructions,
147 expr_sett &modified);
148 void find_modified(
150 expr_sett &modified);
151 void find_modified(
153 expr_sett &modified);
154
155 symbolt fresh_symbol(std::string base, typet type);
156
162};
163
164#endif // CPROVER_GOTO_INSTRUMENT_ACCELERATE_ACCELERATION_UTILS_H
std::unordered_map< exprt, exprt, irep_hash > expr_mapt
std::list< exprt > expr_listt
acceleration_utilst(symbol_tablet &_symbol_table, message_handlert &message_handler, const goto_functionst &_goto_functions, exprt &_loop_counter)
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)
symbolt fresh_symbol(std::string base, typet type)
void abstract_arrays(exprt &expr, expr_mapt &abstractions)
acceleration_utilst(symbol_tablet &_symbol_table, message_handlert &message_handler, const goto_functionst &_goto_functions)
std::vector< expr_pairt > expr_pairst
bool do_assumptions(std::map< exprt, polynomialt > polynomials, patht &body, exprt &guard, guard_managert &guard_manager)
symbol_tablet & symbol_table
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)
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)
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:73
instructionst::const_iterator const_targett
Definition: goto_program.h:593
std::list< instructiont > instructionst
Definition: goto_program.h:590
Array index operator.
Definition: std_expr.h:1328
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:2874
The symbol table.
Definition: symbol_table.h:14
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
Author: Diffblue Ltd.