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  {
33  target_sett dominators;
34  };
35 
37  cfgt cfg;
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
I get_last_node(P &program) const
Definition: cfg.h:155
void initialise(P &program)
Initialises the elements of the fixed point analysis.
void fixedpoint(P &program)
Computes the MOP for the dominator analysis.
Control Flow Graph.
std::ostream & operator<<(std::ostream &out, const cfg_dominators_templatet< P, T, post_dom > &cfg_dominators)
Print the result of the dominator computation.
entry_mapt entry_map
Definition: cfg.h:87
Goto Programs with Functions.
void dominators_pretty_print_node(const T &node, std::ostream &out)
Pretty-print a single node in the dominator tree.
bool nodes_empty(P &program) const
Definition: cfg.h:156
edgest in
Definition: graph.h:41
edgest out
Definition: graph.h:41
instructionst::const_iterator const_targett
bool empty() const
Definition: graph.h:182
void output(std::ostream &) const
Print the result of the dominator computation.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
Definition: goto_program.h:24
cfg_dominators_templatet< const goto_programt, goto_programt::const_targett, true > cfg_post_dominatorst
void operator()(P &program)
Compute dominators.
I get_first_node(P &program) const
Definition: cfg.h:154
Concrete Goto Program.
procedure_local_cfg_baset< nodet, P, T > cfgt
cfg_dominators_templatet< const goto_programt, goto_programt::const_targett, false > cfg_dominatorst