Skip to content

Commit c99d3bf

Browse files
smowtonpeterschrammel
authored andcommitted
Generalise dominators template (#422)
This previously assumed some internal specifics of goto_programt. This generalises it to allow the CFG graph to specify how to retrieve the start and end nodes or detect an empty program, and moves the details particular to goto_programt into its particular specialisation. This allows us to use the generic dominators implementation on other control-flow graph representations.
1 parent b6ced64 commit c99d3bf

File tree

2 files changed

+42
-12
lines changed

2 files changed

+42
-12
lines changed

src/analyses/cfg_dominators.h

+39-12
Original file line numberDiff line numberDiff line change
@@ -124,13 +124,13 @@ void cfg_dominators_templatet<P, T, post_dom>::fixedpoint(P &program)
124124
{
125125
std::list<T> worklist;
126126

127-
if(program.instructions.empty())
127+
if(cfg.nodes_empty(program))
128128
return;
129129

130130
if(post_dom)
131-
entry_node = --program.instructions.end();
131+
entry_node=cfg.get_last_node(program);
132132
else
133-
entry_node = program.instructions.begin();
133+
entry_node=cfg.get_first_node(program);
134134
typename cfgt::nodet &n=cfg[cfg.entry_map[entry_node]];
135135
n.dominators.insert(entry_node);
136136

@@ -200,6 +200,25 @@ void cfg_dominators_templatet<P, T, post_dom>::fixedpoint(P &program)
200200

201201
/*******************************************************************\
202202
203+
Function: dominators_pretty_print_node
204+
205+
Inputs: `node` to print and stream `out` to pretty-print it to
206+
207+
Outputs:
208+
209+
Purpose: Pretty-print a single node in the dominator tree.
210+
Supply a specialisation if operator<< is not sufficient.
211+
212+
\*******************************************************************/
213+
214+
template <class T>
215+
void dominators_pretty_print_node(const T &node, std::ostream &out)
216+
{
217+
out << node;
218+
}
219+
220+
/*******************************************************************\
221+
203222
Function: cfg_dominators_templatet::output
204223
205224
Inputs:
@@ -215,20 +234,20 @@ void cfg_dominators_templatet<P, T, post_dom>::output(std::ostream &out) const
215234
{
216235
for(const auto &node : cfg.entry_map)
217236
{
218-
unsigned n=node.first->location_number;
237+
T n=node.first;
219238

239+
dominators_pretty_print_node(n, out);
220240
if(post_dom)
221-
out << n << " post-dominated by ";
241+
out << " post-dominated by ";
222242
else
223-
out << n << " dominated by ";
224-
for(typename target_sett::const_iterator
225-
d_it=node.second.dominators.begin();
226-
d_it!=node.second.dominators.end();
227-
) // no d_it++
243+
out << " dominated by ";
244+
bool first=true;
245+
for(const auto &d : cfg[node.second].dominators)
228246
{
229-
out << (*d_it)->location_number;
230-
if (++d_it!=node.second.dominators.end())
247+
if(!first)
231248
out << ", ";
249+
first=false;
250+
dominators_pretty_print_node(d, out);
232251
}
233252
out << "\n";
234253
}
@@ -240,4 +259,12 @@ typedef cfg_dominators_templatet<const goto_programt, goto_programt::const_targe
240259
typedef cfg_dominators_templatet<const goto_programt, goto_programt::const_targett, true>
241260
cfg_post_dominatorst;
242261

262+
template<>
263+
inline void dominators_pretty_print_node(
264+
const goto_programt::const_targett& node,
265+
std::ostream& out)
266+
{
267+
out << node->location_number;
268+
}
269+
243270
#endif // CPROVER_ANALYSES_CFG_DOMINATORS_H

src/goto-programs/cfg.h

+3
Original file line numberDiff line numberDiff line change
@@ -131,6 +131,9 @@ class cfg_baset:public graph< cfg_base_nodet<T,I> >
131131
compute_edges(goto_functions, goto_program);
132132
}
133133

134+
I get_first_node(P &program) const { return program.instructions.begin(); }
135+
I get_last_node(P &program) const { return --program.instructions.end(); }
136+
bool nodes_empty(P &program) const { return program.instructions.empty(); }
134137
};
135138

136139
/*******************************************************************\

0 commit comments

Comments
 (0)