cprover
dependence_graph.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Field-Sensitive Program Dependence Analysis, Litvak et al.,
4  FSE 2010
5 
6 Author: Michael Tautschnig
7 
8 Date: 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"
23 #include "reaching_definitions.h"
24 
25 class dependence_grapht;
26 
27 class dep_edget
28 {
29 public:
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 
54 protected:
56 };
57 
58 struct dep_nodet:public graph_nodet<dep_edget>
59 {
62 
64 };
65 
67 {
68 public:
70 
72  : has_values(false),
73  node_id(std::numeric_limits<node_indext>::max()),
74  has_changed(false)
75  {
76  }
77 
78  bool merge(
79  const dep_graph_domaint &src,
82 
83  void transform(
86  ai_baset &ai,
87  const namespacet &ns) final override;
88 
89  void output(
90  std::ostream &out,
91  const ai_baset &ai,
92  const namespacet &ns) const final override;
93 
95  const ai_baset &ai,
96  const namespacet &ns) const override;
97 
98  void make_top() final override
99  {
100  DATA_INVARIANT(node_id!=std::numeric_limits<node_indext>::max(),
101  "node_id must not be valid");
102 
103  has_values=tvt(true);
104  control_deps.clear();
105  control_dep_candidates.clear();
106  data_deps.clear();
107  }
108 
109  void make_bottom() final override
110  {
111  DATA_INVARIANT(node_id!=std::numeric_limits<node_indext>::max(),
112  "node_id must be valid");
113 
114  has_values=tvt(false);
115  control_deps.clear();
116  control_dep_candidates.clear();
117  data_deps.clear();
118 
119  has_changed = false;
120  }
121 
122  void make_entry() final override
123  {
125  node_id != std::numeric_limits<node_indext>::max(),
126  "node_id must not be valid");
127 
129  control_deps.clear();
130  control_dep_candidates.clear();
131  data_deps.clear();
132 
133  has_changed = false;
134  }
135 
136  bool is_top() const final override
137  {
138  DATA_INVARIANT(node_id!=std::numeric_limits<node_indext>::max(),
139  "node_id must be valid");
140 
142  !has_values.is_true() ||
143  (control_deps.empty() && control_dep_candidates.empty() &&
144  data_deps.empty()),
145  "If the domain is top, it must have no dependencies");
146 
147  return has_values.is_true();
148  }
149 
150  bool is_bottom() const final override
151  {
152  DATA_INVARIANT(node_id!=std::numeric_limits<node_indext>::max(),
153  "node_id must be valid");
154 
156  !has_values.is_false() ||
157  (control_deps.empty() && control_dep_candidates.empty() &&
158  data_deps.empty()),
159  "If the domain is bottom, it must have no dependencies");
160 
161  return has_values.is_false();
162  }
163 
165  {
166  node_id=id;
167  }
168 
170  {
171  assert(node_id!=std::numeric_limits<node_indext>::max());
172  return node_id;
173  }
174 
175  void populate_dep_graph(
177 
178 private:
182 
183  typedef std::set<goto_programt::const_targett> depst;
184 
185  // Set of locations with control instructions on which the instruction at this
186  // location has a control dependency on
188 
189  // Set of locations with control instructions from which there is a path in
190  // the CFG to the current location (with the locations being in the same
191  // function). The set control_deps is a subset of this set.
193 
194  // Set of locations with instructions on which the instruction at this
195  // location has a data dependency on
197 
198  friend const depst &
200  friend const depst &
202 
206  dependence_grapht &dep_graph);
207 
208  void data_dependencies(
211  dependence_grapht &dep_graph,
212  const namespacet &ns);
213 };
214 
216  public ait<dep_graph_domaint>,
217  public grapht<dep_nodet>
218 {
219 public:
222 
223  typedef std::map<irep_idt, cfg_post_dominatorst> post_dominators_mapt;
224 
225  explicit dependence_grapht(const namespacet &_ns):
226  ns(_ns),
227  rd(ns)
228  {
229  }
230 
231  void initialize(const goto_functionst &goto_functions)
232  {
233  ait<dep_graph_domaint>::initialize(goto_functions);
234  rd(goto_functions, ns);
235  }
236 
238  {
240 
241  if(!goto_program.empty())
242  {
245  pd(goto_program);
246  }
247  }
248 
249  void finalize()
250  {
251  for(const auto &location_state : state_map)
252  {
253  location_state.second.populate_dep_graph(*this, location_state.first);
254  }
255  }
256 
257  void add_dep(
258  dep_edget::kindt kind,
261 
263  {
264  return post_dominators;
265  }
266 
268  {
269  return rd;
270  }
271 
273  {
274  std::pair<state_mapt::iterator, bool> entry=
275  state_map.insert(std::make_pair(l, dep_graph_domaint()));
276 
277  if(entry.second)
278  {
279  const node_indext node_id=add_node();
280  entry.first->second.set_node_id(node_id);
281  nodes[node_id].PC=l;
282  }
283 
284  return entry.first->second;
285  }
286 
287 protected:
288  const namespacet &ns;
289 
292 };
293 
294 #endif // CPROVER_ANALYSES_DEPENDENCE_GRAPH_H
bool is_false() const
Definition: threeval.h:26
void transform(goto_programt::const_targett from, goto_programt::const_targett 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...
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
A generic directed graph with a parametric node type.
Definition: graph.h:133
std::set< goto_programt::const_targett > depst
Definition: json.h:23
Definition: ai.h:294
static tvt unknown()
Definition: threeval.h:33
post_dominators_mapt post_dominators
void initialize(const goto_programt &goto_program)
STL namespace.
reaching_definitions_analysist rd
const reaching_definitions_analysist & reaching_definitions() const
void initialize(const goto_functionst &goto_functions)
void add_dep(dep_edget::kindt kind, goto_programt::const_targett from, goto_programt::const_targett to)
void make_entry() final override
a reasonable entry-point state
grapht< dep_nodet >::node_indext node_indext
bool is_top() const final override
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:27
void set_node_id(node_indext id)
void make_top() final override
all states – the analysis doesn&#39;t use this, and domains may refuse to implement it.
void control_dependencies(goto_programt::const_targett from, goto_programt::const_targett to, dependence_grapht &dep_graph)
Definition: threeval.h:19
std::map< irep_idt, cfg_post_dominatorst > post_dominators_mapt
const namespacet & ns
instructionst::const_iterator const_targett
Definition: goto_program.h:398
TO_BE_DOCUMENTED.
Definition: namespace.h:74
jsont output_json(const ai_baset &ai, const namespacet &ns) const override
Outputs the current value of the domain.
const post_dominators_mapt & cfg_post_dominators() const
void populate_dep_graph(dependence_grapht &, goto_programt::const_targett) const
nodet::node_indext node_indext
Definition: graph.h:140
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
Definition: dstring.h:33
goto_programt::const_targett PC
bool is_true() const
Definition: threeval.h:25
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:70
Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis...
void data_dependencies(goto_programt::const_targett from, goto_programt::const_targett to, dependence_grapht &dep_graph, const namespacet &ns)
A Template Class for Graphs.
graph_nodet< dep_edget >::edget edget
friend const depst & dependence_graph_test_get_control_deps(const dep_graph_domaint &)
node_indext add_node()
Definition: graph.h:146
Abstract Interpretation.
dependence_grapht(const namespacet &_ns)
The basic interface of an abstract interpreter.
Definition: ai.h:32
bool merge(const dep_graph_domaint &src, goto_programt::const_targett from, goto_programt::const_targett to)
graph_nodet< dep_edget >::edgest edgest
void make_bottom() final override
no states
bool empty() const
Is the program empty?
Definition: goto_program.h:590
virtual void initialize(const goto_programt &)
Definition: ai.cpp:202
static const irep_idt get_function_id(const_targett l)
Definition: goto_program.h:418
state_mapt state_map
Definition: ai.h:345
goto_programt & goto_program
Definition: cover.cpp:63
node_indext get_node_id() const
bool is_bottom() const final override
#define DATA_INVARIANT(CONDITION, REASON)
Definition: invariant.h:278
Compute dominators for CFG of goto_function.
virtual statet & get_state(goto_programt::const_targett l)
void add(kindt _kind)
This class represents a node in a directed graph.
Definition: graph.h:34
friend const depst & dependence_graph_test_get_data_deps(const dep_graph_domaint &)