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), node_id(id), has_changed(false)
73  {
74  }
75 
76  bool merge(
77  const dep_graph_domaint &src,
80 
81  void transform(
82  const irep_idt &function_from,
84  const irep_idt &function_to,
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  assert(node_id!=std::numeric_limits<node_indext>::max());
167  return node_id;
168  }
169 
170  void populate_dep_graph(
172 
173 private:
177 
178  typedef std::set<goto_programt::const_targett> depst;
179 
180  // Set of locations with control instructions on which the instruction at this
181  // location has a control dependency on
183 
184  // Set of locations with control instructions from which there is a path in
185  // the CFG to the current location (with the locations being in the same
186  // function). The set control_deps is a subset of this set.
188 
189  // Set of locations with instructions on which the instruction at this
190  // location has a data dependency on
192 
193  friend const depst &
195  friend const depst &
197 
199  const irep_idt &function_id,
202  dependence_grapht &dep_graph);
203 
204  void data_dependencies(
206  const irep_idt &function_to,
208  dependence_grapht &dep_graph,
209  const namespacet &ns);
210 };
211 
213 
215  public ait<dep_graph_domaint>,
216  public grapht<dep_nodet>
217 {
218 public:
221 
222  typedef std::map<irep_idt, cfg_post_dominatorst> post_dominators_mapt;
223 
224  explicit dependence_grapht(const namespacet &_ns);
225 
226  void initialize(const goto_functionst &goto_functions)
227  {
228  ait<dep_graph_domaint>::initialize(goto_functions);
229  rd(goto_functions, ns);
230  }
231 
232  void initialize(const irep_idt &function, const goto_programt &goto_program)
233  {
234  ait<dep_graph_domaint>::initialize(function, goto_program);
235 
236  // The dependency graph requires that all nodes are explicitly created
237  forall_goto_program_instructions(i_it, goto_program)
238  get_state(i_it).make_bottom();
239 
240  if(!goto_program.empty())
241  {
242  cfg_post_dominatorst &pd = post_dominators[function];
243  pd(goto_program);
244  }
245  }
246 
247  void finalize()
248  {
249  for(const auto &location_state :
250  static_cast<location_sensitive_storaget &>(*storage).internal())
251  {
252  std::static_pointer_cast<dep_graph_domaint>(location_state.second)
253  ->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 
272 protected:
275  const namespacet &ns;
276 
279 };
280 
281 #endif // CPROVER_ANALYSES_DEPENDENCE_GRAPH_H
dependence_grapht::reaching_definitions
const reaching_definitions_analysist & reaching_definitions() const
Definition: dependence_graph.h:267
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:37
dep_graph_domaint::data_deps
depst data_deps
Definition: dependence_graph.h:191
dep_graph_domaint::node_indext
grapht< dep_nodet >::node_indext node_indext
Definition: dependence_graph.h:69
dependence_grapht::initialize
void initialize(const irep_idt &function, const goto_programt &goto_program)
Initialize all the abstract states for a single function.
Definition: dependence_graph.h:232
ai_domain_baset::make_bottom
virtual void make_bottom()=0
no states
dep_graph_domaint::has_changed
bool has_changed
Definition: dependence_graph.h:176
dependence_grapht
Definition: dependence_graph.h:217
dependence_grapht::add_dep
void add_dep(dep_edget::kindt kind, goto_programt::const_targett from, goto_programt::const_targett to)
Definition: dependence_graph.cpp:361
dependence_grapht::dep_graph_domain_factoryt
friend dep_graph_domain_factoryt
Definition: dependence_graph.h:273
dep_graph_domaint::node_id
node_indext node_id
Definition: dependence_graph.h:175
dependence_grapht::dependence_grapht
dependence_grapht(const namespacet &_ns)
Definition: dependence_graph.cpp:354
threeval.h
grapht
A generic directed graph with a parametric node type.
Definition: graph.h:168
dependence_grapht::cfg_post_dominators
const post_dominators_mapt & cfg_post_dominators() const
Definition: dependence_graph.h:262
location_sensitive_storaget::internal
state_mapt & internal(void)
Definition: ai_storage.h:164
dep_graph_domaint::make_top
void make_top() final override
all states – the analysis doesn't use this, and domains may refuse to implement it.
Definition: dependence_graph.h:98
goto_programt::empty
bool empty() const
Is the program empty?
Definition: goto_program.h:762
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition: ai.h:558
dep_graph_domaint::is_bottom
bool is_bottom() const final override
Definition: dependence_graph.h:150
dep_nodet::edget
graph_nodet< dep_edget >::edget edget
Definition: dependence_graph.h:60
dependence_grapht::finalize
void finalize()
Override this to add a cleanup or post-processing step after fixedpoint has run.
Definition: dependence_graph.h:247
dep_edget::kindt::NONE
@ NONE
jsont
Definition: json.h:27
dep_graph_domain_factoryt
This ensures that all domains are constructed with the node ID that links them to the graph part of t...
Definition: dependence_graph.cpp:334
dep_graph_domaint::output
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
Definition: dependence_graph.cpp:264
reaching_definitions_analysist
Definition: reaching_definitions.h:339
dep_graph_domaint::make_entry
void make_entry() final override
Make this domain a reasonable entry-point state.
Definition: dependence_graph.h:122
cfg_dominators.h
Compute dominators for CFG of goto_function.
dependence_grapht::dep_graph_domaint
friend dep_graph_domaint
Definition: dependence_graph.h:274
dependence_grapht::initialize
void initialize(const goto_functionst &goto_functions)
Initialize all the abstract states for a whole program.
Definition: dependence_graph.h:226
dep_graph_domaint::has_values
tvt has_values
Definition: dependence_graph.h:174
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:92
DATA_INVARIANT
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:511
dep_graph_domaint::transform
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
Definition: dependence_graph.cpp:195
dep_graph_domaint::control_dependencies
void control_dependencies(const irep_idt &function_id, goto_programt::const_targett from, goto_programt::const_targett to, dependence_grapht &dep_graph)
Definition: dependence_graph.cpp:54
dep_nodet::PC
goto_programt::const_targett PC
Definition: dependence_graph.h:63
dep_edget::add
void add(kindt _kind)
Definition: dependence_graph.h:32
dep_graph_domaint::make_bottom
void make_bottom() final override
no states
Definition: dependence_graph.h:109
dep_graph_domaint::dep_graph_domaint
dep_graph_domaint(node_indext id)
Definition: dependence_graph.h:71
dep_edget
Definition: dependence_graph.h:28
ait< dep_graph_domaint >::get_state
virtual statet & get_state(trace_ptrt p)
Get the state for the given history, creating it with the factory if it doesn't exist.
Definition: ai.h:515
dep_graph_domaint::get_node_id
node_indext get_node_id() const
Definition: dependence_graph.h:164
dependence_grapht::rd
reaching_definitions_analysist rd
Definition: dependence_graph.h:278
dep_edget::kindt
kindt
Definition: dependence_graph.h:30
dep_graph_domaint::dependence_graph_test_get_data_deps
friend const depst & dependence_graph_test_get_data_deps(const dep_graph_domaint &)
dep_edget::get
kindt get() const
Definition: dependence_graph.h:49
dependence_grapht::post_dominators_mapt
std::map< irep_idt, cfg_post_dominatorst > post_dominators_mapt
Definition: dependence_graph.h:222
dep_graph_domaint::dependence_graph_test_get_control_deps
friend const depst & dependence_graph_test_get_control_deps(const dep_graph_domaint &)
tvt::unknown
static tvt unknown()
Definition: threeval.h:33
dep_graph_domaint::depst
std::set< goto_programt::const_targett > depst
Definition: dependence_graph.h:178
reaching_definitions.h
Range-based reaching definitions analysis (following Field- Sensitive Program Dependence Analysis,...
dep_graph_domaint::control_dep_candidates
depst control_dep_candidates
Definition: dependence_graph.h:187
ai.h
Abstract Interpretation.
tvt::is_false
bool is_false() const
Definition: threeval.h:26
dep_edget::kindt::BOTH
@ BOTH
location_sensitive_storaget
The most conventional storage; one domain per location.
Definition: ai_storage.h:150
dep_graph_domaint::is_top
bool is_top() const final override
Definition: dependence_graph.h:136
tvt
Definition: threeval.h:20
dep_graph_domaint::control_deps
depst control_deps
Definition: dependence_graph.h:182
dependence_grapht::post_dominators
post_dominators_mapt post_dominators
Definition: dependence_graph.h:277
ai_baset::initialize
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:190
dep_edget::kindt::DATA
@ DATA
dep_edget::kind
kindt kind
Definition: dependence_graph.h:55
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:23
graph.h
A Template Class for Graphs.
dep_graph_domaint::merge
bool merge(const dep_graph_domaint &src, goto_programt::const_targett from, goto_programt::const_targett to)
Definition: dependence_graph.cpp:24
graph_nodet
This class represents a node in a directed graph.
Definition: graph.h:36
dep_edget::kindt::CTRL
@ CTRL
dep_graph_domaint::data_dependencies
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)
Definition: dependence_graph.cpp:150
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:119
dep_nodet::edgest
graph_nodet< dep_edget >::edgest edgest
Definition: dependence_graph.h:61
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
dep_graph_domaint::populate_dep_graph
void populate_dep_graph(dependence_grapht &, goto_programt::const_targett) const
Definition: dependence_graph.cpp:378
dep_nodet
Definition: dependence_graph.h:59
ai_domain_baset
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:58
dep_graph_domaint::output_json
jsont output_json(const ai_baset &ai, const namespacet &ns) const override
Outputs the current value of the domain.
Definition: dependence_graph.cpp:303
dep_graph_domaint
Definition: dependence_graph.h:67
dependence_grapht::ns
const namespacet & ns
Definition: dependence_graph.h:275
forall_goto_program_instructions
#define forall_goto_program_instructions(it, program)
Definition: goto_program.h:1196
tvt::is_true
bool is_true() const
Definition: threeval.h:25
cfg_dominators_templatet
Dominator graph.
Definition: cfg_dominators.h:38