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  {
75  }
76 
77  bool merge(
78  const dep_graph_domaint &src,
81 
82  void transform(
85  ai_baset &ai,
86  const namespacet &ns) final;
87 
88  void output(
89  std::ostream &out,
90  const ai_baset &ai,
91  const namespacet &ns) const final;
92 
93  jsont output_json(
94  const ai_baset &ai,
95  const namespacet &ns) const override;
96 
97  void make_top() final override
98  {
99  assert(node_id!=std::numeric_limits<node_indext>::max());
100 
101  has_values=tvt(true);
102  control_deps.clear();
103  data_deps.clear();
104  }
105 
106  void make_bottom() final
107  {
108  assert(node_id!=std::numeric_limits<node_indext>::max());
109 
110  has_values=tvt(false);
111  control_deps.clear();
112  data_deps.clear();
113  }
114 
115  void make_entry() final
116  {
117  make_top();
118  }
119 
120  void set_node_id(node_indext id)
121  {
122  node_id=id;
123  }
124 
125  node_indext get_node_id() const
126  {
127  assert(node_id!=std::numeric_limits<node_indext>::max());
128  return node_id;
129  }
130 
131 private:
133  node_indext node_id;
134 
135  typedef std::set<goto_programt::const_targett> depst;
136  depst control_deps, data_deps;
137 
138  void control_dependencies(
141  dependence_grapht &dep_graph);
142 
143  void data_dependencies(
146  dependence_grapht &dep_graph,
147  const namespacet &ns);
148 };
149 
151  public ait<dep_graph_domaint>,
152  public grapht<dep_nodet>
153 {
154 public:
157 
158  typedef std::map<irep_idt, cfg_post_dominatorst> post_dominators_mapt;
159 
160  explicit dependence_grapht(const namespacet &_ns):
161  ns(_ns),
162  rd(ns)
163  {
164  }
165 
166  void initialize(const goto_functionst &goto_functions)
167  {
168  ait<dep_graph_domaint>::initialize(goto_functions);
169  rd(goto_functions, ns);
170  }
171 
172  void initialize(const goto_programt &goto_program)
173  {
175 
176  if(!goto_program.empty())
177  {
178  const irep_idt id=goto_programt::get_function_id(goto_program);
179  cfg_post_dominatorst &pd=post_dominators[id];
180  pd(goto_program);
181  }
182  }
183 
184  void add_dep(
188 
189  const post_dominators_mapt &cfg_post_dominators() const
190  {
191  return post_dominators;
192  }
193 
195  {
196  return rd;
197  }
198 
200  {
201  std::pair<state_mapt::iterator, bool> entry=
202  state_map.insert(std::make_pair(l, dep_graph_domaint()));
203 
204  if(entry.second)
205  {
206  const node_indext node_id=add_node();
207  entry.first->second.set_node_id(node_id);
208  nodes[node_id].PC=l;
209  }
210 
211  return entry.first->second;
212  }
213 
214 protected:
215  const namespacet &ns;
216 
217  post_dominators_mapt post_dominators;
219 };
220 
221 #endif // CPROVER_ANALYSES_DEPENDENCE_GRAPH_H
A generic directed graph with a parametric node type.
Definition: graph.h:132
std::set< goto_programt::const_targett > depst
void make_bottom() final
Definition: json.h:21
Definition: ai.h:342
post_dominators_mapt post_dominators
static const irep_idt get_function_id(const_targett l)
bool empty() const
Is the program empty?
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)
grapht< dep_nodet >::node_indext node_indext
instructionst::const_iterator const_targett
void make_entry() final
void set_node_id(node_indext id)
void make_top() final override
Definition: threeval.h:19
std::map< irep_idt, cfg_post_dominatorst > post_dominators_mapt
const namespacet & ns
static graphmlt::node_indext add_node(const std::string &name, name_mapt &name_to_node, graphmlt &graph)
Definition: graphml.cpp:26
TO_BE_DOCUMENTED.
Definition: namespace.h:62
const post_dominators_mapt & cfg_post_dominators() const
nodet::node_indext node_indext
Definition: graph.h:139
goto_programt::const_targett PC
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis...
A Template Class for Graphs.
graph_nodet< dep_edget >::edget edget
Abstract Interpretation.
dependence_grapht(const namespacet &_ns)
Definition: ai.h:108
graph_nodet< dep_edget >::edgest edgest
virtual void initialize(const goto_programt &)
Definition: ai.cpp:269
node_indext get_node_id() const
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:33