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