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 
25 template <class P, class T, bool post_dom>
27 {
28 public:
29  typedef std::set<T> target_sett;
30 
31  struct nodet
32  {
34  };
35 
38 
39  void operator()(P &program);
40 
42 
43  void output(std::ostream &) const;
44 
45 protected:
46  void initialise(P &program);
47  void fixedpoint(P &program);
48 };
49 
51 template <class P, class T, bool post_dom>
52 std::ostream &operator << (
53  std::ostream &out,
54  const cfg_dominators_templatet<P, T, post_dom> &cfg_dominators)
55 {
56  cfg_dominators.output(out);
57  return out;
58 }
59 
61 template <class P, class T, bool post_dom>
63 {
64  initialise(program);
65  fixedpoint(program);
66 }
67 
69 template <class P, class T, bool post_dom>
71 {
72  cfg(program);
73 }
74 
76 template <class P, class T, bool post_dom>
78 {
79  std::list<T> worklist;
80 
81  if(cfg.nodes_empty(program))
82  return;
83 
84  if(post_dom)
85  entry_node=cfg.get_last_node(program);
86  else
87  entry_node=cfg.get_first_node(program);
88  typename cfgt::nodet &n=cfg[cfg.entry_map[entry_node]];
89  n.dominators.insert(entry_node);
90 
91  for(typename cfgt::edgest::const_iterator
92  s_it=(post_dom?n.in:n.out).begin();
93  s_it!=(post_dom?n.in:n.out).end();
94  ++s_it)
95  worklist.push_back(cfg[s_it->first].PC);
96 
97  while(!worklist.empty())
98  {
99  // get node from worklist
100  T current=worklist.front();
101  worklist.pop_front();
102 
103  bool changed=false;
104  typename cfgt::nodet &node=cfg[cfg.entry_map[current]];
105  if(node.dominators.empty())
106  {
107  for(const auto &edge : (post_dom ? node.out : node.in))
108  if(!cfg[edge.first].dominators.empty())
109  {
110  node.dominators=cfg[edge.first].dominators;
111  node.dominators.insert(current);
112  changed=true;
113  }
114  }
115 
116  // compute intersection of predecessors
117  for(const auto &edge : (post_dom ? node.out : node.in))
118  {
119  const target_sett &other=cfg[edge.first].dominators;
120  if(other.empty())
121  continue;
122 
123  typename target_sett::const_iterator n_it=node.dominators.begin();
124  typename target_sett::const_iterator o_it=other.begin();
125 
126  // in-place intersection. not safe to use set_intersect
127  while(n_it!=node.dominators.end() && o_it!=other.end())
128  {
129  if(*n_it==current)
130  ++n_it;
131  else if(*n_it<*o_it)
132  {
133  changed=true;
134  node.dominators.erase(n_it++);
135  }
136  else if(*o_it<*n_it)
137  ++o_it;
138  else
139  {
140  ++n_it;
141  ++o_it;
142  }
143  }
144 
145  while(n_it!=node.dominators.end())
146  {
147  if(*n_it==current)
148  ++n_it;
149  else
150  {
151  changed=true;
152  node.dominators.erase(n_it++);
153  }
154  }
155  }
156 
157  if(changed) // fixed point for node reached?
158  {
159  for(const auto &edge : (post_dom ? node.in : node.out))
160  {
161  worklist.push_back(cfg[edge.first].PC);
162  }
163  }
164  }
165 }
166 
170 template <class T>
171 void dominators_pretty_print_node(const T &node, std::ostream &out)
172 {
173  out << node;
174 }
175 
177  const goto_programt::targett& target,
178  std::ostream& out)
179 {
180  out << target->code.pretty();
181 }
182 
184 template <class P, class T, bool post_dom>
186 {
187  for(const auto &node : cfg.entry_map)
188  {
189  auto n=node.first;
190 
192  if(post_dom)
193  out << " post-dominated by ";
194  else
195  out << " dominated by ";
196  bool first=true;
197  for(const auto &d : cfg[node.second].dominators)
198  {
199  if(!first)
200  out << ", ";
201  first=false;
203  }
204  out << "\n";
205  }
206 }
207 
211 
215 
216 template<>
218  const goto_programt::const_targett &node,
219  std::ostream &out)
220 {
221  out << node->location_number;
222 }
223 
224 #endif // CPROVER_ANALYSES_CFG_DOMINATORS_H
cfg.h
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:52
cfg_dominators_templatet::cfgt
procedure_local_cfg_baset< nodet, P, T > cfgt
Definition: cfg_dominators.h:36
graph_nodet::in
edgest in
Definition: graph.h:43
cfg_dominators_templatet::target_sett
std::set< T > target_sett
Definition: cfg_dominators.h:29
graph_nodet::out
edgest out
Definition: graph.h:43
cfg_dominators_templatet::nodet::dominators
target_sett dominators
Definition: cfg_dominators.h:33
cfg_dominators_templatet::initialise
void initialise(P &program)
Initialises the elements of the fixed point analysis.
Definition: cfg_dominators.h:70
cfg_dominators_templatet::operator()
void operator()(P &program)
Compute dominators.
Definition: cfg_dominators.h:62
goto_program.h
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:171
cfg_dominatorst
cfg_dominators_templatet< const goto_programt, goto_programt::const_targett, false > cfg_dominatorst
Definition: cfg_dominators.h:210
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:214
goto_functions.h
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
cfg_base_nodet
Definition: cfg.h:26
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:415
cfg_dominators_templatet::nodet
Definition: cfg_dominators.h:31
cfg_dominators_templatet::entry_node
T entry_node
Definition: cfg_dominators.h:41
cfg_dominators_templatet::output
void output(std::ostream &) const
Print the result of the dominator computation.
Definition: cfg_dominators.h:185
cfg_dominators_templatet::fixedpoint
void fixedpoint(P &program)
Computes the MOP for the dominator analysis.
Definition: cfg_dominators.h:77
cfg_dominators_templatet::cfg
cfgt cfg
Definition: cfg_dominators.h:37
goto_programt::targett
instructionst::iterator targett
Definition: goto_program.h:414
cfg_dominators_templatet
Definition: cfg_dominators.h:26