CBMC
dependence_graph.cpp
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 #include "dependence_graph.h"
16 
17 #include <util/container_utils.h>
18 #include <util/json_irep.h>
19 
20 #include "goto_rw.h"
21 
23  const dep_graph_domaint &src,
24  trace_ptrt,
25  trace_ptrt)
26 {
27  // An abstract state at location `to` may be non-bottom even if
28  // `merge(..., `to`) has not been called so far. This is due to the special
29  // handling of function entry edges (see transform()).
30  bool changed = is_bottom() || has_changed;
31 
32  // For computing the data dependencies, we would not need a fixpoint
33  // computation. The data dependencies at a location are computed from the
34  // result of the reaching definitions analysis at that location
35  // (in data_dependencies()). Thus, we only need to set the data dependencies
36  // part of an abstract state at a certain location once.
37  if(changed && data_deps.empty())
38  {
39  data_deps = src.data_deps;
41  }
42 
44  changed |=
46 
47  has_changed = false;
48 
49  return changed;
50 }
51 
53  const irep_idt &function_id,
56  dependence_grapht &dep_graph)
57 {
58  // Better Slicing of Programs with Jumps and Switches
59  // Kumar and Horwitz, FASE'02:
60  // "Node N is control dependent on node M iff N postdominates, in
61  // the CFG, one but not all of M's CFG successors."
62  //
63  // The "successor" above refers to an immediate successor of M.
64  //
65  // When computing the control dependencies of a node N (i.e., "to"
66  // being N), candidates for M are all control statements (gotos or
67  // assumes) from which there is a path in the CFG to N.
68 
69  // Add new candidates
70 
71  if(from->is_goto() || from->is_assume())
72  control_dep_candidates.insert(from);
73  else if(from->is_end_function())
74  {
75  control_dep_candidates.clear();
76  return;
77  }
78 
79  if(control_dep_candidates.empty())
80  return;
81 
82  // Get postdominators
83 
84  const irep_idt id = function_id;
85  const cfg_post_dominatorst &pd=dep_graph.cfg_post_dominators().at(id);
86 
87  // Check all candidates
88 
89  for(const auto &control_dep_candidate : control_dep_candidates)
90  {
91  // check all CFG successors of M
92  // special case: assumptions also introduce a control dependency
93  bool post_dom_all = !control_dep_candidate->is_assume();
94  bool post_dom_one=false;
95 
96  // we could hard-code assume and goto handling here to improve
97  // performance
99  pd.get_node(control_dep_candidate);
100 
101  // successors of M
102  for(const auto &edge : m.out)
103  {
104  // Could use pd.dominates(to, control_dep_candidate) but this would impose
105  // another dominator node lookup per call to this function, which is too
106  // expensive.
108  pd.cfg[edge.first];
109 
110  if(m_s.dominators.find(to)!=m_s.dominators.end())
111  post_dom_one=true;
112  else
113  post_dom_all=false;
114  }
115 
116  if(post_dom_all || !post_dom_one)
117  {
118  control_deps.erase(control_dep_candidate);
119  }
120  else
121  {
122  control_deps.insert(control_dep_candidate);
123  }
124  }
125 }
126 
128  const range_spect &w_start,
129  const range_spect &w_end,
130  const range_spect &r_start,
131  const range_spect &r_end)
132 {
133  PRECONDITION(w_start >= range_spect{0});
134  PRECONDITION(r_start >= range_spect{0});
135 
136  if(
137  (!w_end.is_unknown() && w_end <= r_start) || // we < rs
138  (!r_end.is_unknown() && w_start >= r_end)) // re < we
139  {
140  return false;
141  }
142  else if(w_start >= r_start) // rs <= ws < we,re
143  return true;
144  else if(
145  w_end.is_unknown() ||
146  (!r_end.is_unknown() && w_end > r_start)) // ws <= rs < we,re
147  {
148  return true;
149  }
150  else
151  return false;
152 }
153 
156  const irep_idt &function_to,
158  dependence_grapht &dep_graph,
159  const namespacet &ns)
160 {
161  // data dependencies using def-use pairs
162  data_deps.clear();
163 
164  // TODO use (future) reaching-definitions-dereferencing rw_set
165  value_setst &value_sets=
166  dep_graph.reaching_definitions().get_value_sets();
167  rw_range_set_value_sett rw_set(ns, value_sets);
168  goto_rw(function_to, to, rw_set);
169 
170  for(const auto &read_object_entry : rw_set.get_r_set())
171  {
172  const range_domaint &r_ranges = rw_set.get_ranges(read_object_entry.second);
173  const rd_range_domaint::ranges_at_loct &w_ranges =
174  dep_graph.reaching_definitions()[to].get(read_object_entry.first);
175 
176  for(const auto &w_range : w_ranges)
177  {
178  bool found=false;
179  for(const auto &wr : w_range.second)
180  {
181  for(const auto &r_range : r_ranges)
182  {
183  if(!found &&
184  may_be_def_use_pair(wr.first, wr.second,
185  r_range.first, r_range.second))
186  {
187  // found a def-use pair
188  data_deps.insert(w_range.first);
189  found=true;
190  }
191  }
192  }
193  }
194 
195  dep_graph.reaching_definitions()[to].clear_cache(read_object_entry.first);
196  }
197 
198  if(to->is_set_return_value())
199  {
200  auto entry = dep_graph.end_function_map.find(function_to);
201  CHECK_RETURN(entry != dep_graph.end_function_map.end());
202 
203  goto_programt::const_targett end_function = entry->second;
204 
205  dep_graph_domaint *s =
206  dynamic_cast<dep_graph_domaint *>(&(dep_graph.get_state(end_function)));
207  CHECK_RETURN(s != nullptr);
208 
209  if(s->is_bottom())
210  s->has_values = tvt::unknown();
211 
212  if(s->data_deps.insert(to).second)
213  s->has_changed = true;
214  }
215 }
216 
218  const irep_idt &function_from,
219  trace_ptrt trace_from,
220  const irep_idt &function_to,
221  trace_ptrt trace_to,
222  ai_baset &ai,
223  const namespacet &ns)
224 {
225  locationt from{trace_from->current_location()};
226  locationt to{trace_to->current_location()};
227 
228  dependence_grapht *dep_graph=dynamic_cast<dependence_grapht*>(&ai);
229  assert(dep_graph!=nullptr);
230 
231  // We do not propagate control dependencies on function calls, i.e., only the
232  // entry point of a function should have a control dependency on the call
233  depst filtered_control_deps;
234  std::copy_if(
235  control_deps.begin(),
236  control_deps.end(),
237  std::inserter(filtered_control_deps, filtered_control_deps.end()),
238  [](goto_programt::const_targett dep) { return !dep->is_function_call(); });
239  control_deps = std::move(filtered_control_deps);
240 
241  // propagate control dependencies across function calls
242  if(from->is_function_call() && function_from != function_to)
243  {
244  // edge to function entry point
245  const goto_programt::const_targett next = std::next(from);
246 
247  dep_graph_domaint *s =
248  dynamic_cast<dep_graph_domaint *>(&(dep_graph->get_state(next)));
249  CHECK_RETURN(s != nullptr);
250 
251  if(s->is_bottom())
252  {
253  s->has_values = tvt::unknown();
254  s->has_changed = true;
255  }
256 
258  s->has_changed |=
260 
261  control_deps.clear();
262  control_deps.insert(from);
263 
264  control_dep_candidates.clear();
265  }
266  else
267  control_dependencies(function_from, from, to, *dep_graph);
268 
269  data_dependencies(from, function_to, to, *dep_graph, ns);
270 }
271 
273  std::ostream &out,
274  const ai_baset &,
275  const namespacet &) const
276 {
277  if(!control_deps.empty())
278  {
279  out << "Control dependencies: ";
280  for(depst::const_iterator
281  it=control_deps.begin();
282  it!=control_deps.end();
283  ++it)
284  {
285  if(it!=control_deps.begin())
286  out << ",";
287  out << (*it)->location_number;
288  }
289  out << '\n';
290  }
291 
292  if(!data_deps.empty())
293  {
294  out << "Data dependencies: ";
295  for(depst::const_iterator
296  it=data_deps.begin();
297  it!=data_deps.end();
298  ++it)
299  {
300  if(it!=data_deps.begin())
301  out << ",";
302  out << (*it)->location_number;
303  }
304  out << '\n';
305  }
306 }
307 
312  const ai_baset &,
313  const namespacet &) const
314 {
315  json_arrayt graph;
316 
317  for(const auto &cd : control_deps)
318  {
319  json_objectt link{
320  {"locationNumber", json_numbert(std::to_string(cd->location_number))},
321  {"sourceLocation", json(cd->source_location())},
322  {"type", json_stringt("control")}};
323  graph.push_back(std::move(link));
324  }
325 
326  for(const auto &dd : data_deps)
327  {
328  json_objectt link{
329  {"locationNumber", json_numbert(std::to_string(dd->location_number))},
330  {"sourceLocation", json(dd->source_location())},
331  {"type", json_stringt("data")}};
332  graph.push_back(std::move(link));
333  }
334 
335  return std::move(graph);
336 }
337 
341 class dep_graph_domain_factoryt : public ai_domain_factoryt<dep_graph_domaint>
342 {
343 public:
345  {
346  }
347 
348  std::unique_ptr<statet> make(locationt l) const override
349  {
350  auto node_id = dg.add_node();
351  dg.nodes[node_id].PC = l;
352  auto p = util_make_unique<dep_graph_domaint>(node_id);
353  CHECK_RETURN(p->is_bottom());
354 
355  return std::unique_ptr<statet>(p.release());
356  }
357 
358 private:
360 };
361 
364  ns(_ns),
365  rd(ns)
366 {
367 }
368 
370  dep_edget::kindt kind,
373 {
374  const node_indext n_from = (*this)[from].get_node_id();
375  assert(n_from<size());
376  const node_indext n_to = (*this)[to].get_node_id();
377  assert(n_to<size());
378 
379  // add_edge is redundant as the subsequent operations also insert
380  // entries into the edge maps (implicitly)
381  // add_edge(n_from, n_to);
382  nodes[n_from].out[n_to].add(kind);
383  nodes[n_to].in[n_from].add(kind);
384 }
385 
387  dependence_grapht &dep_graph, goto_programt::const_targett this_loc) const
388 {
389  for(const auto &c_dep : control_deps)
390  dep_graph.add_dep(dep_edget::kindt::CTRL, c_dep, this_loc);
391 
392  for(const auto &d_dep : data_deps)
393  dep_graph.add_dep(dep_edget::kindt::DATA, d_dep, this_loc);
394 }
dependence_grapht::reaching_definitions
const reaching_definitions_analysist & reaching_definitions() const
Definition: dependence_graph.h:277
dependence_grapht::end_function_map
std::map< irep_idt, goto_programt::const_targett > end_function_map
Definition: dependence_graph.h:289
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
rw_range_sett::get_r_set
const objectst & get_r_set() const
Definition: goto_rw.h:220
json_numbert
Definition: json.h:290
grapht< dep_nodet >::size
std::size_t size() const
Definition: graph.h:212
dep_graph_domaint::data_deps
depst data_deps
Definition: dependence_graph.h:188
dep_graph_domaint::transform
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...
Definition: dependence_graph.cpp:217
may_be_def_use_pair
static bool may_be_def_use_pair(const range_spect &w_start, const range_spect &w_end, const range_spect &r_start, const range_spect &r_end)
Definition: dependence_graph.cpp:127
dep_graph_domaint::has_changed
bool has_changed
Definition: dependence_graph.h:173
dependence_grapht
Definition: dependence_graph.h:211
range_spect::is_unknown
bool is_unknown() const
Definition: goto_rw.h:74
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:369
dependence_grapht::dependence_grapht
dependence_grapht(const namespacet &_ns)
Definition: dependence_graph.cpp:362
CHECK_RETURN
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
reaching_definitions_analysist::get_value_sets
value_setst & get_value_sets() const
Definition: reaching_definitions.h:366
rw_range_sett::get_ranges
const range_domaint & get_ranges(const std::unique_ptr< range_domain_baset > &ranges) const
Definition: goto_rw.h:231
dependence_grapht::cfg_post_dominators
const post_dominators_mapt & cfg_post_dominators() const
Definition: dependence_graph.h:272
range_spect
Data type to describe upper and lower bounds of the range of bits that a read or write access may aff...
Definition: goto_rw.h:60
grapht::add_node
node_indext add_node(arguments &&... values)
Definition: graph.h:180
ait
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition: ai.h:563
rd_range_domaint::ranges_at_loct
std::map< locationt, rangest > ranges_at_loct
Definition: reaching_definitions.h:252
dep_graph_domaint::is_bottom
bool is_bottom() const final override
Definition: dependence_graph.h:147
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:58
rw_range_set_value_sett
Definition: goto_rw.h:368
jsont
Definition: json.h:26
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:341
json_irep.h
dep_graph_domaint::output
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
Definition: dependence_graph.cpp:272
ai_domain_baset::trace_ptrt
ai_history_baset::trace_ptrt trace_ptrt
Definition: ai_domain.h:74
goto_rw.h
json_arrayt
Definition: json.h:164
grapht< dep_nodet >::node_indext
nodet::node_indext node_indext
Definition: graph.h:173
json_objectt
Definition: json.h:299
dep_graph_domaint::has_values
tvt has_values
Definition: dependence_graph.h:171
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:90
util_make_unique
std::unique_ptr< T > util_make_unique(Ts &&... ts)
Definition: make_unique.h:19
dep_graph_domain_factoryt::dep_graph_domain_factoryt
dep_graph_domain_factoryt(dependence_grapht &_dg)
Definition: dependence_graph.cpp:344
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:52
dep_graph_domain_factoryt::make
std::unique_ptr< statet > make(locationt l) const override
Definition: dependence_graph.cpp:348
PRECONDITION
#define PRECONDITION(CONDITION)
Definition: invariant.h:463
util_inplace_set_union
bool util_inplace_set_union(std::set< T, Compare, Alloc > &target, const std::set< T, Compare, Alloc > &source)
Compute union of two sets.
Definition: container_utils.h:28
json
static void json(json_objectT &result, const irep_idt &property_id, const property_infot &property_info)
Definition: properties.cpp:120
dep_edget::kindt
kindt
Definition: dependence_graph.h:30
cfg_dominators_templatet::nodet::dominators
target_sett dominators
Definition: cfg_dominators.h:43
dep_graph_domain_factoryt::dg
dependence_grapht & dg
Definition: dependence_graph.cpp:359
cfg_dominators_templatet::get_node
const cfgt::nodet & get_node(const T &program_point) const
Get the graph node (which gives dominators, predecessors and successors) for program_point.
Definition: cfg_dominators.h:53
grapht::nodes
nodest nodes
Definition: graph.h:176
tvt::unknown
static tvt unknown()
Definition: threeval.h:33
dep_graph_domaint::depst
std::set< goto_programt::const_targett > depst
Definition: dependence_graph.h:175
dep_graph_domaint::control_dep_candidates
depst control_dep_candidates
Definition: dependence_graph.h:184
dep_graph_domaint::control_deps
depst control_deps
Definition: dependence_graph.h:179
dep_edget::kindt::DATA
@ DATA
ai_domain_baset::locationt
goto_programt::const_targett locationt
Definition: ai_domain.h:73
ai_domain_factoryt
Definition: ai_domain.h:196
dep_graph_domaint::merge
bool merge(const dep_graph_domaint &src, trace_ptrt from, trace_ptrt to)
Definition: dependence_graph.cpp:22
value_setst
Definition: value_sets.h:21
dep_edget::kindt::CTRL
@ CTRL
container_utils.h
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:154
ai_baset
This is the basic interface of the abstract interpreter with default implementations of the core func...
Definition: ai.h:118
ai_domain_factory_baset::locationt
ai_domain_baset::locationt locationt
Definition: ai_domain.h:171
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:587
goto_rw
static void goto_rw(const irep_idt &function, goto_programt::const_targett target, const exprt &lhs, const exprt &function_expr, const exprt::operandst &arguments, rw_range_sett &rw_set)
Definition: goto_rw.cpp:843
dep_graph_domaint::populate_dep_graph
void populate_dep_graph(dependence_grapht &, goto_programt::const_targett) const
Definition: dependence_graph.cpp:386
cfg_dominators_templatet::nodet
Definition: cfg_dominators.h:41
ait::get_state
virtual statet & get_state(locationt l)
Definition: ai.h:613
sparse_bitvector_analysist::get
const V & get(const std::size_t value_index) const
Definition: reaching_definitions.h:45
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:311
cfg_dominators_templatet::cfg
cfgt cfg
Definition: cfg_dominators.h:47
dep_graph_domaint
Definition: dependence_graph.h:66
json_arrayt::push_back
jsont & push_back(const jsont &json)
Definition: json.h:212
dependence_graph.h
cfg_dominators_templatet
Dominator graph.
Definition: cfg_dominators.h:36
json_stringt
Definition: json.h:269
range_domaint
Definition: goto_rw.h:174