cprover
Loading...
Searching...
No Matches
dependence_graph.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Field-Sensitive Program Dependence Analysis, Litvak et al.,
4 FSE 2010
5
6Author: Michael Tautschnig
7
8Date: August 2013
9
10\*******************************************************************/
11
14
15#ifndef CPROVER_ANALYSES_DEPENDENCE_GRAPH_H
16#define CPROVER_ANALYSES_DEPENDENCE_GRAPH_H
17
18#include <util/graph.h>
19#include <util/threeval.h>
20
21#include "ai.h"
22#include "cfg_dominators.h"
24
26
28{
29public:
30 enum class kindt { NONE, CTRL, DATA, BOTH };
31
32 void add(kindt _kind)
33 {
34 switch(kind)
35 {
36 case kindt::NONE:
37 kind=_kind;
38 break;
39 case kindt::DATA:
40 case kindt::CTRL:
41 if(kind!=_kind)
43 break;
44 case kindt::BOTH:
45 break;
46 }
47 }
48
49 kindt get() const
50 {
51 return kind;
52 }
53
54protected:
56};
57
58struct dep_nodet:public graph_nodet<dep_edget>
59{
62
64};
65
67{
68public:
70
72 : has_values(false), node_id(id), has_changed(false)
73 {
74 }
75
76 bool merge(const dep_graph_domaint &src, trace_ptrt from, trace_ptrt to);
77
78 void transform(
79 const irep_idt &function_from,
80 trace_ptrt trace_from,
81 const irep_idt &function_to,
82 trace_ptrt trace_to,
83 ai_baset &ai,
84 const namespacet &ns) final override;
85
86 void output(
87 std::ostream &out,
88 const ai_baset &ai,
89 const namespacet &ns) const final override;
90
92 const ai_baset &ai,
93 const namespacet &ns) const override;
94
95 void make_top() final override
96 {
97 DATA_INVARIANT(node_id!=std::numeric_limits<node_indext>::max(),
98 "node_id must not be valid");
99
100 has_values=tvt(true);
101 control_deps.clear();
103 data_deps.clear();
104 }
105
106 void make_bottom() final override
107 {
108 DATA_INVARIANT(node_id!=std::numeric_limits<node_indext>::max(),
109 "node_id must be valid");
110
111 has_values=tvt(false);
112 control_deps.clear();
114 data_deps.clear();
115
116 has_changed = false;
117 }
118
119 void make_entry() final override
120 {
122 node_id != std::numeric_limits<node_indext>::max(),
123 "node_id must not be valid");
124
126 control_deps.clear();
128 data_deps.clear();
129
130 has_changed = false;
131 }
132
133 bool is_top() const final override
134 {
135 DATA_INVARIANT(node_id!=std::numeric_limits<node_indext>::max(),
136 "node_id must be valid");
137
139 !has_values.is_true() ||
140 (control_deps.empty() && control_dep_candidates.empty() &&
141 data_deps.empty()),
142 "If the domain is top, it must have no dependencies");
143
144 return has_values.is_true();
145 }
146
147 bool is_bottom() const final override
148 {
149 DATA_INVARIANT(node_id!=std::numeric_limits<node_indext>::max(),
150 "node_id must be valid");
151
153 !has_values.is_false() ||
154 (control_deps.empty() && control_dep_candidates.empty() &&
155 data_deps.empty()),
156 "If the domain is bottom, it must have no dependencies");
157
158 return has_values.is_false();
159 }
160
162 {
163 assert(node_id!=std::numeric_limits<node_indext>::max());
164 return node_id;
165 }
166
169
170private:
174
175 typedef std::set<goto_programt::const_targett> depst;
176
177 // Set of locations with control instructions on which the instruction at this
178 // location has a control dependency on
180
181 // Set of locations with control instructions from which there is a path in
182 // the CFG to the current location (with the locations being in the same
183 // function). The set control_deps is a subset of this set.
185
186 // Set of locations with instructions on which the instruction at this
187 // location has a data dependency on
189
190 friend const depst &
192 friend const depst &
194
196 const irep_idt &function_id,
199 dependence_grapht &dep_graph);
200
203 const irep_idt &function_to,
205 dependence_grapht &dep_graph,
206 const namespacet &ns);
207};
208
210
212 public ait<dep_graph_domaint>,
213 public grapht<dep_nodet>
214{
215public:
216 using ait<dep_graph_domaint>::operator[];
217 using grapht<dep_nodet>::operator[];
218
219 typedef std::map<irep_idt, cfg_post_dominatorst> post_dominators_mapt;
220
221 explicit dependence_grapht(const namespacet &_ns);
222
223 void initialize(const goto_functionst &goto_functions)
224 {
226 rd(goto_functions, ns);
227 }
228
229 void initialize(const irep_idt &function, const goto_programt &goto_program)
230 {
231 ait<dep_graph_domaint>::initialize(function, goto_program);
232
233 // The dependency graph requires that all nodes are explicitly created
234 forall_goto_program_instructions(i_it, goto_program)
235 get_state(i_it).make_bottom();
236
237 if(!goto_program.empty())
238 {
240 pd(goto_program);
241 }
242 }
243
244 void finalize()
245 {
246 for(const auto &location_state :
247 static_cast<location_sensitive_storaget &>(*storage).internal())
248 {
249 std::static_pointer_cast<dep_graph_domaint>(location_state.second)
250 ->populate_dep_graph(*this, location_state.first);
251 }
252 }
253
254 void add_dep(
255 dep_edget::kindt kind,
258
260 {
261 return post_dominators;
262 }
263
265 {
266 return rd;
267 }
268
269protected:
273
276};
277
278#endif // CPROVER_ANALYSES_DEPENDENCE_GRAPH_H
Abstract Interpretation.
Compute dominators for CFG of goto_function.
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition ai.h:119
virtual void initialize(const irep_idt &function_id, const goto_programt &goto_program)
Initialize all the abstract states for a single function.
Definition ai.cpp:189
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition ai_domain.h:55
virtual void make_bottom()=0
no states
ai_history_baset::trace_ptrt trace_ptrt
Definition ai_domain.h:74
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
virtual statet & get_state(locationt l)
Definition ai.h:613
kindt get() const
void add(kindt _kind)
This ensures that all domains are constructed with the node ID that links them to the graph part of t...
friend const depst & dependence_graph_test_get_control_deps(const dep_graph_domaint &)
bool is_top() const final override
friend const depst & dependence_graph_test_get_data_deps(const dep_graph_domaint &)
void control_dependencies(const irep_idt &function_id, goto_programt::const_targett from, goto_programt::const_targett to, dependence_grapht &dep_graph)
node_indext get_node_id() const
bool merge(const dep_graph_domaint &src, trace_ptrt from, trace_ptrt to)
bool is_bottom() const final override
void make_bottom() final override
no states
void populate_dep_graph(dependence_grapht &, goto_programt::const_targett) const
jsont output_json(const ai_baset &ai, const namespacet &ns) const override
Outputs the current value of the domain.
void transform(const irep_idt &function_from, trace_ptrt trace_from, const irep_idt &function_to, trace_ptrt trace_to, ai_baset &ai, const namespacet &ns) final override
how function calls are treated: a) there is an edge from each call site to the function head b) there...
dep_graph_domaint(node_indext id)
void data_dependencies(goto_programt::const_targett from, const irep_idt &function_to, goto_programt::const_targett to, dependence_grapht &dep_graph, const namespacet &ns)
void make_top() final override
all states – the analysis doesn't use this, and domains may refuse to implement it.
std::set< goto_programt::const_targett > depst
void make_entry() final override
Make this domain a reasonable entry-point state.
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
grapht< dep_nodet >::node_indext node_indext
void add_dep(dep_edget::kindt kind, goto_programt::const_targett from, goto_programt::const_targett to)
const post_dominators_mapt & cfg_post_dominators() const
const reaching_definitions_analysist & reaching_definitions() const
reaching_definitions_analysist rd
std::map< irep_idt, cfg_post_dominatorst > post_dominators_mapt
void initialize(const goto_functionst &goto_functions)
Initialize all the abstract states for a whole program.
void finalize()
Override this to add a cleanup or post-processing step after fixedpoint has run.
void initialize(const irep_idt &function, const goto_programt &goto_program)
Initialize all the abstract states for a single function.
post_dominators_mapt post_dominators
const namespacet & ns
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
A collection of goto functions.
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
bool empty() const
Is the program empty?
This class represents a node in a directed graph.
Definition graph.h:35
std::map< node_indext, edget > edgest
Definition graph.h:40
A generic directed graph with a parametric node type.
Definition graph.h:167
nodet::node_indext node_indext
Definition graph.h:173
Definition json.h:27
The most conventional storage; one domain per location.
Definition ai_storage.h:153
state_mapt & internal(void)
Definition ai_storage.h:168
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
Definition threeval.h:20
bool is_false() const
Definition threeval.h:26
bool is_true() const
Definition threeval.h:25
static tvt unknown()
Definition threeval.h:33
#define forall_goto_program_instructions(it, program)
A Template Class for Graphs.
Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis,...
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition invariant.h:510
graph_nodet< dep_edget >::edget edget
graph_nodet< dep_edget >::edgest edgest
goto_programt::const_targett PC