cprover
cfg_dominators.h
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Compute dominators for CFG of goto_function
4 
5 Author: Georg Weissenbacher, georg@weissenbacher.name
6 
7 \*******************************************************************/
8 
11 
12 #ifndef CPROVER_ANALYSES_CFG_DOMINATORS_H
13 #define CPROVER_ANALYSES_CFG_DOMINATORS_H
14 
15 #include <set>
16 #include <list>
17 #include <map>
18 #include <iosfwd>
19 #include <cassert>
20 
23 #include <goto-programs/cfg.h>
24 
36 template <class P, class T, bool post_dom>
38 {
39 public:
40  typedef std::set<T> target_sett;
41 
42  struct nodet
43  {
45  };
46 
49 
50  void operator()(P &program);
51 
54  const typename cfgt::nodet &get_node(const T &program_point) const
55  {
56  return cfg.get_node(program_point);
57  }
58 
61  typename cfgt::nodet &get_node(const T &program_point)
62  {
63  return cfg.get_node(program_point);
64  }
65 
67  typename cfgt::entryt get_node_index(const T &program_point) const
68  {
69  return cfg.get_node_index(program_point);
70  }
71 
77  bool dominates(T lhs, const nodet &rhs_node) const
78  {
79  return rhs_node.dominators.count(lhs);
80  }
81 
84  bool dominates(T lhs, T rhs) const
85  {
86  return dominates(lhs, get_node(rhs));
87  }
88 
92  bool program_point_reachable(const nodet &program_point_node) const
93  {
94  // Dominator analysis walks from the entry point, so a side-effect is to
95  // identify unreachable program points (those which don't dominate even
96  // themselves).
97  return !program_point_node.dominators.empty();
98  }
99 
103  bool program_point_reachable(T program_point) const
104  {
105  // Dominator analysis walks from the entry point, so a side-effect is to
106  // identify unreachable program points (those which don't dominate even
107  // themselves).
108  return program_point_reachable(get_node(program_point));
109  }
110 
112 
113  void output(std::ostream &) const;
114 
115 protected:
116  void initialise(P &program);
117  void fixedpoint(P &program);
118 };
119 
121 template <class P, class T, bool post_dom>
122 std::ostream &operator << (
123  std::ostream &out,
124  const cfg_dominators_templatet<P, T, post_dom> &cfg_dominators)
125 {
126  cfg_dominators.output(out);
127  return out;
128 }
129 
131 template <class P, class T, bool post_dom>
133 {
134  initialise(program);
135  fixedpoint(program);
136 }
137 
139 template <class P, class T, bool post_dom>
141 {
142  cfg(program);
143 }
144 
146 template <class P, class T, bool post_dom>
148 {
149  std::list<T> worklist;
150 
151  if(cfgt::nodes_empty(program))
152  return;
153 
154  if(post_dom)
155  entry_node = cfgt::get_last_node(program);
156  else
157  entry_node = cfgt::get_first_node(program);
158  typename cfgt::nodet &n = cfg.get_node(entry_node);
159  n.dominators.insert(entry_node);
160 
161  for(typename cfgt::edgest::const_iterator
162  s_it=(post_dom?n.in:n.out).begin();
163  s_it!=(post_dom?n.in:n.out).end();
164  ++s_it)
165  worklist.push_back(cfg[s_it->first].PC);
166 
167  while(!worklist.empty())
168  {
169  // get node from worklist
170  T current=worklist.front();
171  worklist.pop_front();
172 
173  bool changed=false;
174  typename cfgt::nodet &node = cfg.get_node(current);
175  if(node.dominators.empty())
176  {
177  for(const auto &edge : (post_dom ? node.out : node.in))
178  if(!cfg[edge.first].dominators.empty())
179  {
180  node.dominators=cfg[edge.first].dominators;
181  node.dominators.insert(current);
182  changed=true;
183  }
184  }
185 
186  // compute intersection of predecessors
187  for(const auto &edge : (post_dom ? node.out : node.in))
188  {
189  const target_sett &other=cfg[edge.first].dominators;
190  if(other.empty())
191  continue;
192 
193  typename target_sett::const_iterator n_it=node.dominators.begin();
194  typename target_sett::const_iterator o_it=other.begin();
195 
196  // in-place intersection. not safe to use set_intersect
197  while(n_it!=node.dominators.end() && o_it!=other.end())
198  {
199  if(*n_it==current)
200  ++n_it;
201  else if(*n_it<*o_it)
202  {
203  changed=true;
204  node.dominators.erase(n_it++);
205  }
206  else if(*o_it<*n_it)
207  ++o_it;
208  else
209  {
210  ++n_it;
211  ++o_it;
212  }
213  }
214 
215  while(n_it!=node.dominators.end())
216  {
217  if(*n_it==current)
218  ++n_it;
219  else
220  {
221  changed=true;
222  node.dominators.erase(n_it++);
223  }
224  }
225  }
226 
227  if(changed) // fixed point for node reached?
228  {
229  for(const auto &edge : (post_dom ? node.in : node.out))
230  {
231  worklist.push_back(cfg[edge.first].PC);
232  }
233  }
234  }
235 }
236 
240 template <class T>
241 void dominators_pretty_print_node(const T &node, std::ostream &out)
242 {
243  out << node;
244 }
245 
247  const goto_programt::targett& target,
248  std::ostream& out)
249 {
250  out << target->code.pretty();
251 }
252 
254 template <class P, class T, bool post_dom>
256 {
257  for(const auto &node : cfg.entries())
258  {
259  auto n=node.first;
260 
262  if(post_dom)
263  out << " post-dominated by ";
264  else
265  out << " dominated by ";
266  bool first=true;
267  for(const auto &d : cfg[node.second].dominators)
268  {
269  if(!first)
270  out << ", ";
271  first=false;
273  }
274  out << "\n";
275  }
276 }
277 
281 
285 
286 template<>
288  const goto_programt::const_targett &node,
289  std::ostream &out)
290 {
291  out << node->location_number;
292 }
293 
294 #endif // CPROVER_ANALYSES_CFG_DOMINATORS_H
cfg.h
Control Flow Graph.
cfg_dominators_templatet::program_point_reachable
bool program_point_reachable(const nodet &program_point_node) const
Returns true if the program point for program_point_node is reachable from the entry point.
Definition: cfg_dominators.h:92
cfg_baset< nodet, const goto_programt, goto_programt::const_targett >::entryt
base_grapht::node_indext entryt
Definition: cfg.h:91
operator<<
std::ostream & operator<<(std::ostream &out, const cfg_dominators_templatet< P, T, post_dom > &cfg_dominators)
Print the result of the dominator computation.
Definition: cfg_dominators.h:122
cfg_dominators_templatet::cfgt
procedure_local_cfg_baset< nodet, P, T > cfgt
Definition: cfg_dominators.h:47
cfg_dominators_templatet::get_node_index
cfgt::entryt get_node_index(const T &program_point) const
Get the graph node index for program_point.
Definition: cfg_dominators.h:67
graph_nodet::in
edgest in
Definition: graph.h:43
cfg_baset::get_node
nodet & get_node(const goto_programt::const_targett &program_point)
Get the CFG graph node relating to program_point.
Definition: cfg.h:245
cfg_dominators_templatet::target_sett
std::set< T > target_sett
Definition: cfg_dominators.h:40
graph_nodet::out
edgest out
Definition: graph.h:43
cfg_baset::get_node_index
entryt get_node_index(const goto_programt::const_targett &program_point) const
Get the graph node index for program_point.
Definition: cfg.h:239
cfg_dominators_templatet::dominates
bool dominates(T lhs, T rhs) const
Returns true if program point lhs dominates rhs.
Definition: cfg_dominators.h:84
cfg_dominators_templatet::nodet::dominators
target_sett dominators
Definition: cfg_dominators.h:44
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
cfg_dominators_templatet::initialise
void initialise(P &program)
Initialises the elements of the fixed point analysis.
Definition: cfg_dominators.h:140
cfg_dominators_templatet::dominates
bool dominates(T lhs, const nodet &rhs_node) const
Returns true if the program point corresponding to rhs_node is dominated by program point lhs.
Definition: cfg_dominators.h:77
cfg_dominators_templatet::operator()
void operator()(P &program)
Compute dominators.
Definition: cfg_dominators.h:132
goto_program.h
Concrete Goto Program.
cfg_dominators_templatet::program_point_reachable
bool program_point_reachable(T program_point) const
Returns true if the program point for program_point_node is reachable from the entry point.
Definition: cfg_dominators.h:103
dominators_pretty_print_node
void dominators_pretty_print_node(const T &node, std::ostream &out)
Pretty-print a single node in the dominator tree.
Definition: cfg_dominators.h:241
cfg_dominators_templatet::get_node
cfgt::nodet & get_node(const T &program_point)
Get the graph node (which gives dominators, predecessors and successors) for program_point.
Definition: cfg_dominators.h:61
cfg_dominatorst
cfg_dominators_templatet< const goto_programt, goto_programt::const_targett, false > cfg_dominatorst
Definition: cfg_dominators.h:280
procedure_local_cfg_baset< nodet, P, T >
cfg_post_dominatorst
cfg_dominators_templatet< const goto_programt, goto_programt::const_targett, true > cfg_post_dominatorst
Definition: cfg_dominators.h:284
goto_functions.h
Goto Programs with Functions.
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
cfg_base_nodet
Definition: cfg.h:28
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:580
cfg_dominators_templatet::nodet
Definition: cfg_dominators.h:43
cfg_dominators_templatet::entry_node
T entry_node
Definition: cfg_dominators.h:111
cfg_dominators_templatet::output
void output(std::ostream &) const
Print the result of the dominator computation.
Definition: cfg_dominators.h:255
cfg_dominators_templatet::fixedpoint
void fixedpoint(P &program)
Computes the MOP for the dominator analysis.
Definition: cfg_dominators.h:147
cfg_dominators_templatet::cfg
cfgt cfg
Definition: cfg_dominators.h:48
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:579
cfg_dominators_templatet
Dominator graph.
Definition: cfg_dominators.h:38