CBMC
All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Modules Pages
cfg_dominators.h
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Compute dominators for CFG of goto_function
4
5Author: 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
22#include <goto-programs/cfg.h>
23
35template <class P, class T, bool post_dom>
37{
38public:
39 typedef std::set<T, typename P::target_less_than> target_sett;
40
41 struct nodet
42 {
44 };
45
48
49 void operator()(P &program);
50
53 const typename cfgt::nodet &get_node(const T &program_point) const
54 {
56 }
57
61 {
63 }
64
66 typename cfgt::entryt get_node_index(const T &program_point) const
67 {
69 }
70
76 bool dominates(T lhs, const nodet &rhs_node) const
77 {
78 return rhs_node.dominators.count(lhs);
79 }
80
83 bool dominates(T lhs, T rhs) const
84 {
85 return dominates(lhs, get_node(rhs));
86 }
87
92 {
93 // Dominator analysis walks from the entry point, so a side-effect is to
94 // identify unreachable program points (those which don't dominate even
95 // themselves).
96 return !program_point_node.dominators.empty();
97 }
98
103 {
104 // Dominator analysis walks from the entry point, so a side-effect is to
105 // identify unreachable program points (those which don't dominate even
106 // themselves).
108 }
109
111
112 void output(std::ostream &) const;
113
114protected:
115 void initialise(P &program);
116 void fixedpoint(P &program);
117};
118
120template <class P, class T, bool post_dom>
121std::ostream &operator << (
122 std::ostream &out,
123 const cfg_dominators_templatet<P, T, post_dom> &cfg_dominators)
124{
125 cfg_dominators.output(out);
126 return out;
127}
128
130template <class P, class T, bool post_dom>
132{
133 initialise(program);
134 fixedpoint(program);
135}
136
138template <class P, class T, bool post_dom>
140{
141 cfg(program);
142}
143
145template <class P, class T, bool post_dom>
147{
148 std::list<T> worklist;
149
150 if(cfgt::nodes_empty(program))
151 return;
152
153 if(post_dom)
154 entry_node = cfgt::get_last_node(program);
155 else
156 entry_node = cfgt::get_first_node(program);
157 typename cfgt::nodet &n = cfg.get_node(entry_node);
158 n.dominators.insert(entry_node);
159
160 for(typename cfgt::edgest::const_iterator
161 s_it=(post_dom?n.in:n.out).begin();
162 s_it!=(post_dom?n.in:n.out).end();
163 ++s_it)
164 worklist.push_back(cfg[s_it->first].PC);
165
166 // A program may have multiple "exit" nodes when self loops or assume(false)
167 // instructions are present.
168 if(post_dom)
169 {
170 for(auto &cfg_entry : cfg.entry_map)
171 {
172 if(cfg[cfg_entry.second].PC == entry_node)
173 continue;
174
175 typename cfgt::nodet &n_it = cfg[cfg_entry.second];
176 if(
177 n_it.out.empty() ||
178 (n_it.out.size() == 1 && n_it.out.begin()->first == cfg_entry.second))
179 {
180 n_it.dominators.insert(cfg[cfg_entry.second].PC);
181 for(const auto &predecessor : n_it.in)
182 worklist.push_back(cfg[predecessor.first].PC);
183 }
184 }
185 }
186
187 while(!worklist.empty())
188 {
189 // get node from worklist
190 T current=worklist.front();
191 worklist.pop_front();
192
193 bool changed=false;
194 typename cfgt::nodet &node = cfg.get_node(current);
195 if(node.dominators.empty())
196 {
197 for(const auto &edge : (post_dom ? node.out : node.in))
198 if(!cfg[edge.first].dominators.empty())
199 {
200 node.dominators=cfg[edge.first].dominators;
201 node.dominators.insert(current);
202 changed=true;
203 }
204 }
205
206 // compute intersection of predecessors
207 for(const auto &edge : (post_dom ? node.out : node.in))
208 {
209 const target_sett &other=cfg[edge.first].dominators;
210 if(other.empty())
211 continue;
212
213 typename target_sett::const_iterator n_it=node.dominators.begin();
214 typename target_sett::const_iterator o_it=other.begin();
215
216 // in-place intersection. not safe to use set_intersect
217 while(n_it!=node.dominators.end() && o_it!=other.end())
218 {
219 if(*n_it==current)
220 ++n_it;
221 else if(typename P::target_less_than()(*n_it, *o_it))
222 {
223 changed=true;
224 node.dominators.erase(n_it++);
225 }
226 else if(typename P::target_less_than()(*o_it, *n_it))
227 ++o_it;
228 else
229 {
230 ++n_it;
231 ++o_it;
232 }
233 }
234
235 while(n_it!=node.dominators.end())
236 {
237 if(*n_it==current)
238 ++n_it;
239 else
240 {
241 changed=true;
242 node.dominators.erase(n_it++);
243 }
244 }
245 }
246
247 if(changed) // fixed point for node reached?
248 {
249 for(const auto &edge : (post_dom ? node.in : node.out))
250 {
251 worklist.push_back(cfg[edge.first].PC);
252 }
253 }
254 }
255}
256
261template <class T>
262void dominators_pretty_print_node(const T &node, std::ostream &out)
263{
264 out << node;
265}
266
268 const goto_programt::targett& target,
269 std::ostream& out)
270{
271 out << target->code().pretty();
272}
273
275template <class P, class T, bool post_dom>
277{
278 for(const auto &node : cfg.entries())
279 {
280 auto n=node.first;
281
283 if(post_dom)
284 out << " post-dominated by ";
285 else
286 out << " dominated by ";
287 bool first=true;
288 for(const auto &d : cfg[node.second].dominators)
289 {
290 if(!first)
291 out << ", ";
292 first=false;
294 }
295 out << "\n";
296 }
297}
298
302
306
307template<>
310 std::ostream &out)
311{
312 out << node->location_number;
313}
314
315#endif // CPROVER_ANALYSES_CFG_DOMINATORS_H
Control Flow Graph.
cfg_dominators_templatet< const goto_programt, goto_programt::const_targett, false > cfg_dominatorst
std::ostream & operator<<(std::ostream &out, const cfg_dominators_templatet< P, T, post_dom > &cfg_dominators)
Print the result of the dominator computation.
void dominators_pretty_print_node(const T &node, std::ostream &out)
Pretty-print a single node in the dominator tree.
cfg_dominators_templatet< const goto_programt, goto_programt::const_targett, true > cfg_post_dominatorst
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
Definition ai.cpp:39
virtual bool fixedpoint(trace_ptrt starting_trace, const irep_idt &function_id, const goto_programt &goto_program, const goto_functionst &goto_functions, const namespacet &ns)
Run the fixedpoint algorithm until it reaches a fixed point.
Definition ai.cpp:229
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
ait()
Definition ai.h:565
base_grapht::node_indext entryt
Definition cfg.h:91
nodet & get_node(const goto_programt::const_targett &program_point)
Get the CFG graph node relating to program_point.
Definition cfg.h:245
entryt get_node_index(const goto_programt::const_targett &program_point) const
Get the graph node index for program_point.
Definition cfg.h:239
bool dominates(T lhs, T rhs) const
Returns true if program point lhs dominates rhs.
const cfgt::nodet & get_node(const T &program_point) const
Get the graph node (which gives dominators, predecessors and successors) for program_point.
procedure_local_cfg_baset< nodet, P, T > cfgt
cfgt::nodet & get_node(const T &program_point)
Get the graph node (which gives dominators, predecessors and successors) for program_point.
void output(std::ostream &) const
Print the result of the dominator computation.
void operator()(P &program)
Compute dominators.
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.
void fixedpoint(P &program)
Computes the MOP for the dominator analysis.
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.
std::set< T, typename P::target_less_than > target_sett
bool program_point_reachable(T program_point) const
Returns true if the program point for program_point_node is reachable from the entry point.
void initialise(P &program)
Initialises the elements of the fixed point analysis.
cfgt::entryt get_node_index(const T &program_point) const
Get the graph node index for program_point.
A generic container class for the GOTO intermediate representation of one function.
instructionst::iterator targett
instructionst::const_iterator const_targett
Goto Programs with Functions.
Concrete Goto Program.