CBMC
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(id),
74  has_changed(false),
76  {
77  }
78 
79  bool merge(const dep_graph_domaint &src, trace_ptrt from, trace_ptrt to);
80 
81  void transform(
82  const irep_idt &function_from,
83  trace_ptrt trace_from,
84  const irep_idt &function_to,
85  trace_ptrt trace_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  PRECONDITION(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::
179  set<goto_programt::const_targett, goto_programt::target_less_than>
181 
182  // Set of locations with control instructions on which the instruction at this
183  // location has a control dependency on
185 
186  // Set of locations with control instructions from which there is a path in
187  // the CFG to the current location (with the locations being in the same
188  // function). The set control_deps is a subset of this set.
190 
191  // Set of locations with instructions on which the instruction at this
192  // location has a data dependency on
194 
196 
197  friend const depst &
199  friend const depst &
201 
203  const irep_idt &function_id,
206  dependence_grapht &dep_graph);
207 
208  void data_dependencies(
210  const irep_idt &function_to,
212  dependence_grapht &dep_graph,
213  const namespacet &ns);
214 };
215 
217 
219  public ait<dep_graph_domaint>,
220  public grapht<dep_nodet>
221 {
222 public:
225 
226  typedef std::map<irep_idt, cfg_post_dominatorst> post_dominators_mapt;
227 
229 
230  void initialize(const goto_functionst &goto_functions)
231  {
232  ait<dep_graph_domaint>::initialize(goto_functions);
233  rd(goto_functions, ns);
234 
235  for(const auto &entry : goto_functions.function_map)
236  {
237  const goto_programt &goto_program = entry.second.body;
238  if(!goto_program.empty())
239  {
240  end_function_map.emplace(
241  entry.first, std::prev(goto_program.instructions.end()));
242  }
243  }
244  }
245 
246  void initialize(const irep_idt &function, const goto_programt &goto_program)
247  {
248  ait<dep_graph_domaint>::initialize(function, goto_program);
249 
250  // The dependency graph requires that all nodes are explicitly created
251  forall_goto_program_instructions(i_it, goto_program)
252  get_state(i_it).make_bottom();
253 
254  if(!goto_program.empty())
255  {
256  cfg_post_dominatorst &pd = post_dominators[function];
257  pd(goto_program);
258 
259  end_function_map.emplace(
260  function, std::prev(goto_program.instructions.end()));
261  }
262  }
263 
264  void finalize()
265  {
266  for(const auto &location_state :
267  static_cast<location_sensitive_storaget &>(*storage).internal())
268  {
269  std::static_pointer_cast<dep_graph_domaint>(location_state.second)
270  ->populate_dep_graph(*this, location_state.first);
271  }
272  }
273 
274  void add_dep(
275  dep_edget::kindt kind,
278 
280  {
281  return post_dominators;
282  }
283 
285  {
286  return rd;
287  }
288 
289 protected:
292  const namespacet &ns;
293 
296  std::map<irep_idt, goto_programt::const_targett> end_function_map;
297 };
298 
299 #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:117
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:194
The interface offered by a domain, allows code to manipulate domains without knowing their exact type...
Definition: ai_domain.h:54
virtual void make_bottom()=0
no states
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:73
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition: ai.h:562
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
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...
bool is_top() const final override
friend const depst & dependence_graph_test_get_control_deps(const dep_graph_domaint &)
dep_graph_domaint(node_indext id, message_handlert &message_handler)
void control_dependencies(const irep_idt &function_id, goto_programt::const_targett from, goto_programt::const_targett to, dependence_grapht &dep_graph)
std::set< goto_programt::const_targett, goto_programt::target_less_than > depst
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...
friend const depst & dependence_graph_test_get_data_deps(const dep_graph_domaint &)
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 directly (see make_entry) and domains may refuse to implem...
void make_entry() final override
Make this domain a reasonable entry-point state For most domains top is sufficient.
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
message_handlert & message_handler
grapht< dep_nodet >::node_indext node_indext
void add_dep(dep_edget::kindt kind, goto_programt::const_targett from, goto_programt::const_targett to)
dependence_grapht(const namespacet &_ns, message_handlert &)
friend dep_graph_domain_factoryt
const reaching_definitions_analysist & reaching_definitions() const
const post_dominators_mapt & cfg_post_dominators() 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.
std::map< irep_idt, goto_programt::const_targett > end_function_map
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:38
A collection of goto functions.
function_mapt function_map
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:622
instructionst::const_iterator const_targett
Definition: goto_program.h:615
bool empty() const
Is the program empty?
Definition: goto_program.h:799
This class represents a node in a directed graph.
Definition: graph.h:35
A generic directed graph with a parametric node type.
Definition: graph.h:167
Definition: json.h:27
The most conventional storage; one domain per location.
Definition: ai_storage.h:154
state_mapt & internal(void)
Definition: ai_storage.h:169
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
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:534
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
graph_nodet< dep_edget >::edget edget
graph_nodet< dep_edget >::edgest edgest
goto_programt::const_targett PC