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/json.h>
20 #include <util/json_expr.h>
21 
22 #include "goto_rw.h"
23 
25  const dep_graph_domaint &src,
28 {
29  bool changed=has_values.is_false();
31 
32  depst::iterator it=control_deps.begin();
33  for(const auto &c_dep : src.control_deps)
34  {
35  while(it!=control_deps.end() && *it<c_dep)
36  ++it;
37  if(it==control_deps.end() || c_dep<*it)
38  {
39  control_deps.insert(it, c_dep);
40  changed=true;
41  }
42  else if(it!=control_deps.end())
43  ++it;
44  }
45 
46  it=data_deps.begin();
47  for(const auto &d_dep : src.data_deps)
48  {
49  while(it!=data_deps.end() && *it<d_dep)
50  ++it;
51  if(it==data_deps.end() || d_dep<*it)
52  {
53  data_deps.insert(it, d_dep);
54  changed=true;
55  }
56  else if(it!=data_deps.end())
57  ++it;
58  }
59 
60  return changed;
61 }
62 
66  dependence_grapht &dep_graph)
67 {
68  // Better Slicing of Programs with Jumps and Switches
69  // Kumar and Horwitz, FASE'02:
70  // Node N is control dependent on node M iff N postdominates one
71  // but not all of M's CFG successors.
72  //
73  // candidates for M are from and all existing control-depended on
74  // nodes; from is added if it is a goto or assume instruction
75  if(from->is_goto() ||
76  from->is_assume())
77  control_deps.insert(from);
78 
80  const cfg_post_dominatorst &pd=dep_graph.cfg_post_dominators().at(id);
81 
82  // check all candidates for M
83  for(depst::iterator
84  it=control_deps.begin();
85  it!=control_deps.end();
86  ) // no ++it
87  {
88  depst::iterator next=it;
89  ++next;
90 
91  // check all CFG successors
92  // special case: assumptions also introduce a control dependency
93  bool post_dom_all=!(*it)->is_assume();
94  bool post_dom_one=false;
95 
96  // we could hard-code assume and goto handling here to improve
97  // performance
98  cfg_post_dominatorst::cfgt::entry_mapt::const_iterator e=
99  pd.cfg.entry_map.find(*it);
100 
101  assert(e!=pd.cfg.entry_map.end());
102 
104  pd.cfg[e->second];
105 
106  for(const auto &edge : m.out)
107  {
109  pd.cfg[edge.first];
110 
111  if(m_s.dominators.find(to)!=m_s.dominators.end())
112  post_dom_one=true;
113  else
114  post_dom_all=false;
115  }
116 
117  if(post_dom_all ||
118  !post_dom_one)
119  control_deps.erase(it);
120 
121  it=next;
122  }
123 
124  // add edges to the graph
125  for(const auto &c_dep : control_deps)
126  dep_graph.add_dep(dep_edget::kindt::CTRL, c_dep, to);
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 
153  dependence_grapht &dep_graph,
154  const namespacet &ns)
155 {
156  // data dependencies using def-use pairs
157  data_deps.clear();
158 
159  // TODO use (future) reaching-definitions-dereferencing rw_set
160  value_setst &value_sets=
161  dep_graph.reaching_definitions().get_value_sets();
162  rw_range_set_value_sett rw_set(ns, value_sets);
163  goto_rw(to, rw_set);
164 
166  {
167  const range_domaint &r_ranges=rw_set.get_ranges(it);
168  const rd_range_domaint::ranges_at_loct &w_ranges=
169  dep_graph.reaching_definitions()[to].get(it->first);
170 
171  for(const auto &w_range : w_ranges)
172  {
173  bool found=false;
174  for(const auto &wr : w_range.second)
175  for(const auto &r_range : r_ranges)
176  if(!found &&
177  may_be_def_use_pair(wr.first, wr.second,
178  r_range.first, r_range.second))
179  {
180  // found a def-use pair
181  data_deps.insert(w_range.first);
182  found=true;
183  }
184  }
185 
186  dep_graph.reaching_definitions()[to].clear_cache(it->first);
187  }
188 
189  // add edges to the graph
190  for(const auto &d_dep : data_deps)
191  {
192  // *it might be handled in a future call call to visit only,
193  // depending on the sequence of successors; make sure it exists
194  dep_graph.get_state(d_dep);
195  dep_graph.add_dep(dep_edget::kindt::DATA, d_dep, to);
196  }
197 }
198 
202  ai_baset &ai,
203  const namespacet &ns)
204 {
205  dependence_grapht *dep_graph=dynamic_cast<dependence_grapht*>(&ai);
206  assert(dep_graph!=nullptr);
207 
208  // propagate control dependencies across function calls
209  if(from->is_function_call())
210  {
212  ++next;
213 
214  if(next==to)
215  {
216  control_dependencies(from, to, *dep_graph);
217  }
218  else
219  {
220  // edge to function entry point
221 
223  dynamic_cast<dep_graph_domaint*>(&(dep_graph->get_state(next)));
224  assert(s!=nullptr);
225 
226  depst::iterator it=s->control_deps.begin();
227  for(const auto &c_dep : control_deps)
228  {
229  while(it!=s->control_deps.end() && *it<c_dep)
230  ++it;
231  if(it==s->control_deps.end() || c_dep<*it)
232  s->control_deps.insert(it, c_dep);
233  else if(it!=s->control_deps.end())
234  ++it;
235  }
236 
237  control_deps.clear();
238  }
239  }
240  else
241  control_dependencies(from, to, *dep_graph);
242 
243  data_dependencies(from, to, *dep_graph, ns);
244 }
245 
247  std::ostream &out,
248  const ai_baset &ai,
249  const namespacet &ns) const
250 {
251  if(!control_deps.empty())
252  {
253  out << "Control dependencies: ";
254  for(depst::const_iterator
255  it=control_deps.begin();
256  it!=control_deps.end();
257  ++it)
258  {
259  if(it!=control_deps.begin())
260  out << ",";
261  out << (*it)->location_number;
262  }
263  out << '\n';
264  }
265 
266  if(!data_deps.empty())
267  {
268  out << "Data dependencies: ";
269  for(depst::const_iterator
270  it=data_deps.begin();
271  it!=data_deps.end();
272  ++it)
273  {
274  if(it!=data_deps.begin())
275  out << ",";
276  out << (*it)->location_number;
277  }
278  out << '\n';
279  }
280 }
281 
286  const ai_baset &ai,
287  const namespacet &ns) const
288 {
289  json_arrayt graph;
290 
291  for(const auto &cd : control_deps)
292  {
293  json_objectt &link=graph.push_back().make_object();
294  link["locationNumber"]=
295  json_numbert(std::to_string(cd->location_number));
296  link["sourceLocation"]=json(cd->source_location);
297  link["type"]=json_stringt("control");
298  }
299 
300  for(const auto &dd : data_deps)
301  {
302  json_objectt &link=graph.push_back().make_object();
303  link["locationNumber"]=
304  json_numbert(std::to_string(dd->location_number));
305  link["sourceLocation"]=json(dd->source_location);
306  json_stringt(dd->source_location.as_string());
307  link["type"]=json_stringt("data");
308  }
309 
310  return graph;
311 }
312 
314  dep_edget::kindt kind,
317 {
318  const node_indext n_from=state_map[from].get_node_id();
319  assert(n_from<size());
320  const node_indext n_to=state_map[to].get_node_id();
321  assert(n_to<size());
322 
323  // add_edge is redundant as the subsequent operations also insert
324  // entries into the edge maps (implicitly)
325  // add_edge(n_from, n_to);
326  nodes[n_from].out[n_to].add(kind);
327  nodes[n_to].in[n_from].add(kind);
328 }
bool is_false() const
Definition: threeval.h:26
BigInt mp_integer
Definition: mp_arith.h:19
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
entry_mapt entry_map
Definition: cfg.h:87
Definition: json.h:21
static tvt unknown()
Definition: threeval.h:33
static const irep_idt get_function_id(const_targett l)
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:157
instructionst::const_iterator const_targett
void control_dependencies(goto_programt::const_targett from, goto_programt::const_targett to, dependence_grapht &dep_graph)
Expressions in JSON.
TO_BE_DOCUMENTED.
Definition: namespace.h:62
void goto_rw(goto_programt::const_targett target, const code_assignt &assign, rw_range_sett &rw_set)
Definition: goto_rw.cpp:678
jsont output_json(const ai_baset &ai, const namespacet &ns) const override
Outputs the current value of the domain.
void transform(goto_programt::const_targett from, goto_programt::const_targett to, ai_baset &ai, const namespacet &ns) final
const post_dominators_mapt & cfg_post_dominators() const
value_setst & get_value_sets() const
std::size_t size() const
Definition: graph.h:177
nodet::node_indext node_indext
Definition: graph.h:139
#define forall_rw_range_set_r_objects(it, rw_set)
Definition: goto_rw.h:23
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)
Definition: ai.h:108
bool merge(const dep_graph_domaint &src, goto_programt::const_targett from, goto_programt::const_targett to)
state_mapt state_map
Definition: ai.h:378
const range_domaint & get_ranges(objectst::const_iterator it) const
Definition: goto_rw.h:109
json_objectt & make_object()
Definition: json.h:234
virtual statet & get_state(goto_programt::const_targett l)
std::map< locationt, rangest > ranges_at_loct
void output(std::ostream &out, const ai_baset &ai, const namespacet &ns) const final
json_objectt json(const source_locationt &location)
Definition: json_expr.cpp:23