Skip to content

Commit 1abc75e

Browse files
committed
Dependence graph: ensure grapht representation is consistent with domain
Previously the grapht representation was incrementally populated at the same time as the domain representation was computed, but at least one case (control dependencies crossing function callsites) was missing, leading to inconsistency, and doing it this way invites future similar mistakes. Instead, this commit switches to generating the grapht representation in one go after the AI fixedpoint has been computed.
1 parent e03b0cb commit 1abc75e

File tree

2 files changed

+21
-13
lines changed

2 files changed

+21
-13
lines changed

src/analyses/dependence_graph.cpp

Lines changed: 10 additions & 13 deletions
Original file line numberDiff line numberDiff line change
@@ -120,10 +120,6 @@ void dep_graph_domaint::control_dependencies(
120120

121121
it=next;
122122
}
123-
124-
// add edges to the graph
125-
for(const auto &c_dep : control_deps)
126-
dep_graph.add_dep(dep_edget::kindt::CTRL, c_dep, to);
127123
}
128124

129125
static bool may_be_def_use_pair(
@@ -185,15 +181,6 @@ void dep_graph_domaint::data_dependencies(
185181

186182
dep_graph.reaching_definitions()[to].clear_cache(it->first);
187183
}
188-
189-
// add edges to the graph
190-
for(const auto &d_dep : data_deps)
191-
{
192-
// *it might be handled in a future call call to visit only,
193-
// depending on the sequence of successors; make sure it exists
194-
dep_graph.get_state(d_dep);
195-
dep_graph.add_dep(dep_edget::kindt::DATA, d_dep, to);
196-
}
197184
}
198185

199186
void dep_graph_domaint::transform(
@@ -326,3 +313,13 @@ void dependence_grapht::add_dep(
326313
nodes[n_from].out[n_to].add(kind);
327314
nodes[n_to].in[n_from].add(kind);
328315
}
316+
317+
void dep_graph_domaint::populate_dep_graph(
318+
dependence_grapht &dep_graph, goto_programt::const_targett this_loc) const
319+
{
320+
for(const auto &c_dep : control_deps)
321+
dep_graph.add_dep(dep_edget::kindt::CTRL, c_dep, this_loc);
322+
323+
for(const auto &d_dep : data_deps)
324+
dep_graph.add_dep(dep_edget::kindt::DATA, d_dep, this_loc);
325+
}

src/analyses/dependence_graph.h

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -154,6 +154,9 @@ class dep_graph_domaint:public ai_domain_baset
154154
return node_id;
155155
}
156156

157+
void populate_dep_graph(
158+
dependence_grapht &, goto_programt::const_targett) const;
159+
157160
private:
158161
tvt has_values;
159162
node_indext node_id;
@@ -207,6 +210,14 @@ class dependence_grapht:
207210
}
208211
}
209212

213+
void finalize()
214+
{
215+
for(const auto &location_state : state_map)
216+
{
217+
location_state.second.populate_dep_graph(*this, location_state.first);
218+
}
219+
}
220+
210221
void add_dep(
211222
dep_edget::kindt kind,
212223
goto_programt::const_targett from,

0 commit comments

Comments
 (0)