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(
84  const irep_idt &function_from,
86  const irep_idt &function_to,
88  ai_baset &ai,
89  const namespacet &ns) final override;
90 
91  void output(
92  std::ostream &out,
93  const ai_baset &ai,
94  const namespacet &ns) const final override;
95 
97  const ai_baset &ai,
98  const namespacet &ns) const override;
99 
100  void make_top() final override
101  {
102  DATA_INVARIANT(node_id!=std::numeric_limits<node_indext>::max(),
103  "node_id must not be valid");
104 
105  has_values=tvt(true);
106  control_deps.clear();
107  control_dep_candidates.clear();
108  data_deps.clear();
109  }
110 
111  void make_bottom() final override
112  {
113  DATA_INVARIANT(node_id!=std::numeric_limits<node_indext>::max(),
114  "node_id must be valid");
115 
116  has_values=tvt(false);
117  control_deps.clear();
118  control_dep_candidates.clear();
119  data_deps.clear();
120 
121  has_changed = false;
122  }
123 
124  void make_entry() final override
125  {
127  node_id != std::numeric_limits<node_indext>::max(),
128  "node_id must not be valid");
129 
131  control_deps.clear();
132  control_dep_candidates.clear();
133  data_deps.clear();
134 
135  has_changed = false;
136  }
137 
138  bool is_top() const final override
139  {
140  DATA_INVARIANT(node_id!=std::numeric_limits<node_indext>::max(),
141  "node_id must be valid");
142 
144  !has_values.is_true() ||
145  (control_deps.empty() && control_dep_candidates.empty() &&
146  data_deps.empty()),
147  "If the domain is top, it must have no dependencies");
148 
149  return has_values.is_true();
150  }
151 
152  bool is_bottom() const final override
153  {
154  DATA_INVARIANT(node_id!=std::numeric_limits<node_indext>::max(),
155  "node_id must be valid");
156 
158  !has_values.is_false() ||
159  (control_deps.empty() && control_dep_candidates.empty() &&
160  data_deps.empty()),
161  "If the domain is bottom, it must have no dependencies");
162 
163  return has_values.is_false();
164  }
165 
167  {
168  node_id=id;
169  }
170 
172  {
173  assert(node_id!=std::numeric_limits<node_indext>::max());
174  return node_id;
175  }
176 
177  void populate_dep_graph(
179 
180 private:
184 
185  typedef std::set<goto_programt::const_targett> depst;
186 
187  // Set of locations with control instructions on which the instruction at this
188  // location has a control dependency on
190 
191  // Set of locations with control instructions from which there is a path in
192  // the CFG to the current location (with the locations being in the same
193  // function). The set control_deps is a subset of this set.
195 
196  // Set of locations with instructions on which the instruction at this
197  // location has a data dependency on
199 
200  friend const depst &
202  friend const depst &
204 
208  dependence_grapht &dep_graph);
209 
210  void data_dependencies(
213  dependence_grapht &dep_graph,
214  const namespacet &ns);
215 };
216 
218  public ait<dep_graph_domaint>,
219  public grapht<dep_nodet>
220 {
221 public:
224 
225  typedef std::map<irep_idt, cfg_post_dominatorst> post_dominators_mapt;
226 
227  explicit dependence_grapht(const namespacet &_ns):
228  ns(_ns),
229  rd(ns)
230  {
231  }
232 
233  void initialize(const goto_functionst &goto_functions)
234  {
235  ait<dep_graph_domaint>::initialize(goto_functions);
236  rd(goto_functions, ns);
237  }
238 
239  void initialize(const goto_programt &goto_program)
240  {
242 
243  if(!goto_program.empty())
244  {
245  const irep_idt id=goto_programt::get_function_id(goto_program);
247  pd(goto_program);
248  }
249  }
250 
251  void finalize()
252  {
253  for(const auto &location_state : state_map)
254  {
255  location_state.second.populate_dep_graph(*this, location_state.first);
256  }
257  }
258 
259  void add_dep(
260  dep_edget::kindt kind,
263 
265  {
266  return post_dominators;
267  }
268 
270  {
271  return rd;
272  }
273 
275  {
276  std::pair<state_mapt::iterator, bool> entry=
277  state_map.insert(std::make_pair(l, dep_graph_domaint()));
278 
279  if(entry.second)
280  {
281  const node_indext node_id=add_node();
282  entry.first->second.set_node_id(node_id);
283  nodes[node_id].PC=l;
284  }
285 
286  return entry.first->second;
287  }
288 
289 protected:
290  const namespacet &ns;
291 
294 };
295 
296 #endif // CPROVER_ANALYSES_DEPENDENCE_GRAPH_H
bool is_false() const
Definition: threeval.h:26
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:167
void transform(const irep_idt &function_from, goto_programt::const_targett from, const irep_idt &function_to, 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...
std::set< goto_programt::const_targett > depst
Definition: json.h:23
Definition: ai.h:365
static tvt unknown()
Definition: threeval.h:33
post_dominators_mapt post_dominators
kindt get() const
void initialize(const goto_programt &goto_program)
Initialize all the abstract states for a single function.
reaching_definitions_analysist rd
const reaching_definitions_analysist & reaching_definitions() const
void initialize(const goto_functionst &goto_functions)
Initialize all the abstract states for a whole program.
void add_dep(dep_edget::kindt kind, goto_programt::const_targett from, goto_programt::const_targett to)
virtual void initialize(const goto_programt &goto_program)
Initialize all the abstract states for a single function.
Definition: ai.cpp:202
void make_entry() final override
Make this domain 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'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:415
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:93
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
A collection of goto functions.
nodet::node_indext node_indext
Definition: graph.h:174
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:35
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:72
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:180
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:626
static const irep_idt get_function_id(const_targett l)
Get the id of the function that contains the instruction pointed-to by the given instruction iterator...
Definition: goto_program.h:440
state_mapt state_map
Definition: ai.h:416
node_indext get_node_id() const
bool is_bottom() const final override
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:485
Compute dominators for CFG of goto_function.
virtual statet & get_state(goto_programt::const_targett l)
Get the state for the given location, creating it in a default way if it doesn't exist.
void add(kindt _kind)
This class represents a node in a directed graph.
Definition: graph.h:35
void finalize()
Override this to add a cleanup or post-processing step after fixedpoint has run.
friend const depst & dependence_graph_test_get_data_deps(const dep_graph_domaint &)