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.h>
21 #include <util/json_expr.h>
22 
23 #include "goto_rw.h"
24 
26  const dep_graph_domaint &src,
29 {
30  // An abstract state at location `to` may be non-bottom even if
31  // `merge(..., `to`) has not been called so far. This is due to the special
32  // handling of function entry edges (see transform()).
33  bool changed = is_bottom() || has_changed;
34 
35  // For computing the data dependencies, we would not need a fixpoint
36  // computation. The data dependencies at a location are computed from the
37  // result of the reaching definitions analysis at that location
38  // (in data_dependencies()). Thus, we only need to set the data dependencies
39  // part of an abstract state at a certain location once.
40  if(changed && data_deps.empty())
41  {
42  data_deps = src.data_deps;
44  }
45 
47  changed |=
49 
50  has_changed = false;
51 
52  return changed;
53 }
54 
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=from->function;
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
100  cfg_post_dominatorst::cfgt::entry_mapt::const_iterator e =
101  pd.cfg.entry_map.find(control_dep_candidate);
102 
103  INVARIANT(
104  e != pd.cfg.entry_map.end(), "cfg must have an entry for every location");
105 
107  pd.cfg[e->second];
108 
109  // successors of M
110  for(const auto &edge : m.out)
111  {
113  pd.cfg[edge.first];
114 
115  if(m_s.dominators.find(to)!=m_s.dominators.end())
116  post_dom_one=true;
117  else
118  post_dom_all=false;
119  }
120 
121  if(post_dom_all || !post_dom_one)
122  {
123  control_deps.erase(control_dep_candidate);
124  }
125  else
126  {
127  control_deps.insert(control_dep_candidate);
128  }
129  }
130 }
131 
133  const mp_integer &w_start,
134  const mp_integer &w_end,
135  const mp_integer &r_start,
136  const mp_integer &r_end)
137 {
138  assert(w_start>=0);
139  assert(r_start>=0);
140 
141  if((w_end!=-1 && w_end <= r_start) || // we < rs
142  (r_end!=-1 && w_start >= r_end)) // re < we
143  return false;
144  else if(w_start >= r_start) // rs <= ws < we,re
145  return true;
146  else if(w_end==-1 ||
147  (r_end!=-1 && w_end > r_start)) // ws <= rs < we,re
148  return true;
149  else
150  return false;
151 }
152 
156  dependence_grapht &dep_graph,
157  const namespacet &ns)
158 {
159  // data dependencies using def-use pairs
160  data_deps.clear();
161 
162  // TODO use (future) reaching-definitions-dereferencing rw_set
163  value_setst &value_sets=
164  dep_graph.reaching_definitions().get_value_sets();
165  rw_range_set_value_sett rw_set(ns, value_sets);
166  goto_rw(to, rw_set);
167 
169  {
170  const range_domaint &r_ranges=rw_set.get_ranges(it);
171  const rd_range_domaint::ranges_at_loct &w_ranges=
172  dep_graph.reaching_definitions()[to].get(it->first);
173 
174  for(const auto &w_range : w_ranges)
175  {
176  bool found=false;
177  for(const auto &wr : w_range.second)
178  for(const auto &r_range : r_ranges)
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  dep_graph.reaching_definitions()[to].clear_cache(it->first);
190  }
191 }
192 
194  const irep_idt &function_from,
196  const irep_idt &function_to,
198  ai_baset &ai,
199  const namespacet &ns)
200 {
201  dependence_grapht *dep_graph=dynamic_cast<dependence_grapht*>(&ai);
202  assert(dep_graph!=nullptr);
203 
204  // propagate control dependencies across function calls
205  if(from->is_function_call())
206  {
207  if(function_from == function_to)
208  {
209  control_dependencies(from, to, *dep_graph);
210  }
211  else
212  {
213  // edge to function entry point
214  const goto_programt::const_targett next = std::next(from);
215 
217  dynamic_cast<dep_graph_domaint*>(&(dep_graph->get_state(next)));
218  assert(s!=nullptr);
219 
220  if(s->is_bottom())
221  {
222  s->has_values = tvt::unknown();
223  s->has_changed = true;
224  }
225 
229 
230  control_deps.clear();
231  control_dep_candidates.clear();
232  }
233  }
234  else
235  control_dependencies(from, to, *dep_graph);
236 
237  data_dependencies(from, to, *dep_graph, ns);
238 }
239 
241  std::ostream &out,
242  const ai_baset &,
243  const namespacet &) const
244 {
245  if(!control_deps.empty())
246  {
247  out << "Control dependencies: ";
248  for(depst::const_iterator
249  it=control_deps.begin();
250  it!=control_deps.end();
251  ++it)
252  {
253  if(it!=control_deps.begin())
254  out << ",";
255  out << (*it)->location_number;
256  }
257  out << '\n';
258  }
259 
260  if(!data_deps.empty())
261  {
262  out << "Data dependencies: ";
263  for(depst::const_iterator
264  it=data_deps.begin();
265  it!=data_deps.end();
266  ++it)
267  {
268  if(it!=data_deps.begin())
269  out << ",";
270  out << (*it)->location_number;
271  }
272  out << '\n';
273  }
274 }
275 
280  const ai_baset &,
281  const namespacet &) const
282 {
283  json_arrayt graph;
284 
285  for(const auto &cd : control_deps)
286  {
287  json_objectt &link=graph.push_back().make_object();
288  link["locationNumber"]=
289  json_numbert(std::to_string(cd->location_number));
290  link["sourceLocation"]=json(cd->source_location);
291  link["type"]=json_stringt("control");
292  }
293 
294  for(const auto &dd : data_deps)
295  {
296  json_objectt &link=graph.push_back().make_object();
297  link["locationNumber"]=
298  json_numbert(std::to_string(dd->location_number));
299  link["sourceLocation"]=json(dd->source_location);
300  json_stringt(dd->source_location.as_string());
301  link["type"]=json_stringt("data");
302  }
303 
304  return std::move(graph);
305 }
306 
308  dep_edget::kindt kind,
311 {
312  const node_indext n_from = (*this)[from].get_node_id();
313  assert(n_from<size());
314  const node_indext n_to = (*this)[to].get_node_id();
315  assert(n_to<size());
316 
317  // add_edge is redundant as the subsequent operations also insert
318  // entries into the edge maps (implicitly)
319  // add_edge(n_from, n_to);
320  nodes[n_from].out[n_to].add(kind);
321  nodes[n_to].in[n_from].add(kind);
322 }
323 
325  dependence_grapht &dep_graph, goto_programt::const_targett this_loc) const
326 {
327  for(const auto &c_dep : control_deps)
328  dep_graph.add_dep(dep_edget::kindt::CTRL, c_dep, this_loc);
329 
330  for(const auto &d_dep : data_deps)
331  dep_graph.add_dep(dep_edget::kindt::DATA, d_dep, this_loc);
332 }
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final override
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...
BigInt mp_integer
Definition: mp_arith.h:22
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
entry_mapt entry_map
Definition: cfg.h:106
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: json.h:23
static tvt unknown()
Definition: threeval.h:33
bool util_inplace_set_union(std::set< T, Compare, Alloc > &target, const std::set< T, Compare, Alloc > &source)
Compute union of two sets.
const reaching_definitions_analysist & reaching_definitions() const
void add_dep(dep_edget::kindt kind, goto_programt::const_targett from, goto_programt::const_targett to)
jsont & push_back(const jsont &json)
Definition: json.h:163
void control_dependencies(goto_programt::const_targett from, goto_programt::const_targett to, dependence_grapht &dep_graph)
Expressions in JSON.
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
void goto_rw(goto_programt::const_targett target, const code_assignt &assign, rw_range_sett &rw_set)
Definition: goto_rw.cpp:722
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
value_setst & get_value_sets() const
void populate_dep_graph(dependence_grapht &, goto_programt::const_targett) const
std::size_t size() const
Definition: graph.h:212
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
#define forall_rw_range_set_r_objects(it, rw_set)
Definition: goto_rw.h:24
void data_dependencies(goto_programt::const_targett from, goto_programt::const_targett to, dependence_grapht &dep_graph, const namespacet &ns)
const V & get(const std::size_t value_index) const
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)
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)
bool is_bottom() const final override
const range_domaint & get_ranges(objectst::const_iterator it) const
Definition: goto_rw.h:135
json_objectt & make_object()
Definition: json.h:290
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.
std::map< locationt, rangest > ranges_at_loct
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:87