Skip to content

Commit 20874ec

Browse files
Make variable-sensitivity dependence graph produce control dependencies
Previously the variable sensitivity domain dependence graph only produced data dependency information. This patch copies out the control dependency code from the original dependency graph code and patches those into the variable sensitivity dependence graph code. Note, this does *not* change the algorithm used to calculate the control dependencies, it just means we can calculate both control dependencies (using the original algorithm) and the data dependencies using the new variable sensitivity based algorithm in a single pass of the tools.
1 parent 1036d4c commit 20874ec

File tree

3 files changed

+462
-11
lines changed

3 files changed

+462
-11
lines changed

src/analyses/variable-sensitivity/variable_sensitivity_dependence_graph.cpp

Lines changed: 290 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,7 @@
2222
* \param ns the namespace to use
2323
* \param deps the destination in which to accumlate data dependencies
2424
*/
25-
void variable_sensitivity_dependence_grapht::eval_data_deps(
25+
void variable_sensitivity_dependence_domaint::eval_data_deps(
2626
const exprt &expr, const namespacet &ns, data_depst &deps) const
2727
{
2828
const auto res=
@@ -58,14 +58,64 @@ void variable_sensitivity_dependence_grapht::eval_data_deps(
5858
* \param ai the abstract interpreter
5959
* \param ns the namespace
6060
*/
61-
void variable_sensitivity_dependence_grapht::transform(
61+
void variable_sensitivity_dependence_domaint::transform(
6262
locationt from,
6363
locationt to,
6464
ai_baset &ai,
6565
const namespacet &ns)
6666
{
6767
variable_sensitivity_domaint::transform(from, to, ai, ns);
6868

69+
variable_sensitivity_dependence_grapht *dep_graph=
70+
dynamic_cast<variable_sensitivity_dependence_grapht*>(&ai);
71+
assert(dep_graph!=nullptr);
72+
73+
// propagate control dependencies across function calls
74+
if(from->is_function_call())
75+
{
76+
if(from->function == to->function)
77+
{
78+
control_dependencies(from, to, *dep_graph);
79+
}
80+
else
81+
{
82+
// edge to function entry point
83+
const goto_programt::const_targett next = std::next(from);
84+
85+
variable_sensitivity_dependence_domaint *s=
86+
dynamic_cast<variable_sensitivity_dependence_domaint*>
87+
(&(dep_graph->get_state(next)));
88+
assert(s!=nullptr);
89+
90+
if(s->has_values.is_false())
91+
{
92+
s->has_values=tvt::unknown();
93+
s->has_changed=true;
94+
}
95+
96+
// modify abstract state of return location
97+
if(s->merge_control_dependencies(
98+
control_deps,
99+
control_dep_candidates))
100+
s->has_changed=true;
101+
102+
control_deps.clear();
103+
control_dep_candidates.clear();
104+
}
105+
}
106+
else
107+
control_dependencies(from, to, *dep_graph);
108+
109+
// Find all the data dependencies in the the 'to' expression
110+
data_dependencies(from, to, *dep_graph, ns);
111+
}
112+
113+
void variable_sensitivity_dependence_domaint::data_dependencies(
114+
goto_programt::const_targett from,
115+
goto_programt::const_targett to,
116+
variable_sensitivity_dependence_grapht &dep_graph,
117+
const namespacet &ns)
118+
{
69119
// Find all the data dependencies in the the 'to' expression
70120
domain_data_deps.clear();
71121
if(to->is_assign())
@@ -76,6 +126,165 @@ void variable_sensitivity_dependence_grapht::transform(
76126
}
77127
}
78128

129+
void variable_sensitivity_dependence_domaint::control_dependencies(
130+
goto_programt::const_targett from,
131+
goto_programt::const_targett to,
132+
variable_sensitivity_dependence_grapht &dep_graph)
133+
{
134+
// Better Slicing of Programs with Jumps and Switches
135+
// Kumar and Horwitz, FASE'02:
136+
// "Node N is control dependent on node M iff N postdominates, in
137+
// the CFG, one but not all of M's CFG successors."
138+
//
139+
// The "successor" above refers to an immediate successor of M.
140+
141+
// Candidates for M for "to" are "from" and all existing control
142+
// dependencies on nodes. "from" is added if it is a goto or assume
143+
// instruction
144+
145+
// Add new candidates
146+
147+
if(from->is_goto() || from->is_assume())
148+
control_dep_candidates.insert(from);
149+
else if(from->is_end_function())
150+
{
151+
control_dep_candidates.clear();
152+
return;
153+
}
154+
155+
if(control_dep_candidates.empty())
156+
return;
157+
158+
// Compute postdominators if needed
159+
160+
const goto_functionst &goto_functions=dep_graph.goto_functions;
161+
162+
const irep_idt id=goto_programt::get_function_id(from);
163+
cfg_post_dominatorst &pd_tmp=dep_graph.cfg_post_dominators()[id];
164+
165+
goto_functionst::function_mapt::const_iterator f_it=
166+
goto_functions.function_map.find(id);
167+
168+
if(f_it==goto_functions.function_map.end())
169+
return;
170+
171+
const goto_programt &goto_program=f_it->second.body;
172+
173+
if(pd_tmp.cfg.size()==0) // have we computed the dominators already?
174+
{
175+
pd_tmp(goto_program);
176+
}
177+
178+
const cfg_post_dominatorst &pd=pd_tmp;
179+
180+
// Check all candidates
181+
182+
for(const auto &cd : control_dep_candidates)
183+
{
184+
// check all CFG successors of M
185+
// special case: assumptions also introduce a control dependency
186+
bool post_dom_all=!cd->is_assume();
187+
bool post_dom_one=false;
188+
189+
// we could hard-code assume and goto handling here to improve
190+
// performance
191+
cfg_post_dominatorst::cfgt::entry_mapt::const_iterator e=
192+
pd.cfg.entry_map.find(cd);
193+
194+
assert(e!=pd.cfg.entry_map.end());
195+
196+
const cfg_post_dominatorst::cfgt::nodet &m=
197+
pd.cfg[e->second];
198+
199+
// successors of M
200+
for(const auto &edge : m.out)
201+
{
202+
const cfg_post_dominatorst::cfgt::nodet &m_s=
203+
pd.cfg[edge.first];
204+
205+
if(m_s.dominators.find(to)!=m_s.dominators.end())
206+
post_dom_one=true;
207+
else
208+
post_dom_all=false;
209+
}
210+
211+
if(post_dom_all || !post_dom_one)
212+
{
213+
control_deps.erase(cd);
214+
}
215+
else
216+
{
217+
tvt branch=tvt::unknown();
218+
219+
if(cd->is_goto() && !cd->is_backwards_goto())
220+
{
221+
goto_programt::const_targett t=cd->get_target();
222+
branch=to->location_number>=t->location_number?tvt(false):tvt(true);
223+
}
224+
225+
control_deps.insert(std::make_pair(cd, branch));
226+
}
227+
}
228+
229+
// add edges to the graph
230+
for(const auto &c_dep : control_deps)
231+
dep_graph.add_dep(vs_dep_edget::kindt::CTRL, c_dep.first, to);
232+
}
233+
234+
bool variable_sensitivity_dependence_domaint::merge_control_dependencies(
235+
const control_depst &other_control_deps,
236+
const control_dep_candidatest &other_control_dep_candidates)
237+
{
238+
bool changed=false;
239+
240+
// Merge control dependencies
241+
242+
control_depst::iterator it=control_deps.begin();
243+
244+
for(const auto &c_dep : other_control_deps)
245+
{
246+
// find position to insert
247+
while(it!=control_deps.end() && it->first<c_dep.first)
248+
++it;
249+
250+
if(it==control_deps.end() || c_dep.first<it->first)
251+
{
252+
// hint points at position that will follow the new element
253+
control_deps.insert(it, c_dep);
254+
changed=true;
255+
}
256+
else
257+
{
258+
assert(it!=control_deps.end());
259+
assert(!(it->first<c_dep.first));
260+
assert(!(c_dep.first<it->first));
261+
262+
tvt &branch1=it->second;
263+
const tvt &branch2=c_dep.second;
264+
265+
if(branch1!=branch2 && !branch1.is_unknown())
266+
{
267+
branch1=tvt::unknown();
268+
changed=true;
269+
}
270+
271+
++it;
272+
}
273+
}
274+
275+
// Merge control dependency candidates
276+
277+
size_t n=control_dep_candidates.size();
278+
279+
control_dep_candidates.insert(
280+
other_control_dep_candidates.begin(),
281+
other_control_dep_candidates.end());
282+
283+
changed|=n!=control_dep_candidates.size();
284+
285+
return changed;
286+
}
287+
79288
/**
80289
* Computes the join between "this" and "b"
81290
*
@@ -84,18 +293,21 @@ void variable_sensitivity_dependence_grapht::transform(
84293
* \param to the current location
85294
* \return true if something has changed in the merge
86295
*/
87-
bool variable_sensitivity_dependence_grapht::merge(
296+
bool variable_sensitivity_dependence_domaint::merge(
88297
const variable_sensitivity_domaint &b,
89298
locationt from,
90299
locationt to)
91300
{
92301
bool changed = false;
93302

94303
changed = variable_sensitivity_domaint::merge(b, from, to);
304+
changed |= has_values.is_false() || has_changed;
95305

96-
const auto cast_b =
97-
dynamic_cast<const variable_sensitivity_dependence_grapht&>(b);
306+
// Handle data dependencies
307+
const auto& cast_b =
308+
dynamic_cast<const variable_sensitivity_dependence_domaint&>(b);
98309

310+
// Merge data dependencies
99311
for (auto bdep : cast_b.domain_data_deps)
100312
{
101313
for(exprt bexpr : bdep.second)
@@ -105,6 +317,13 @@ bool variable_sensitivity_dependence_grapht::merge(
105317
}
106318
}
107319

320+
changed |= merge_control_dependencies(
321+
cast_b.control_deps,
322+
cast_b.control_dep_candidates);
323+
324+
has_changed=false;
325+
has_values=tvt::unknown();
326+
108327
return changed;
109328
}
110329

@@ -119,7 +338,7 @@ bool variable_sensitivity_dependence_grapht::merge(
119338
* between here and this will be retained.
120339
* \param ns: The global namespace
121340
*/
122-
void variable_sensitivity_dependence_grapht::merge_three_way_function_return(
341+
void variable_sensitivity_dependence_domaint::merge_three_way_function_return(
123342
const ai_domain_baset &function_call,
124343
const ai_domain_baset &function_start,
125344
const ai_domain_baset &function_end,
@@ -144,11 +363,30 @@ void variable_sensitivity_dependence_grapht::merge_three_way_function_return(
144363
* \param ai the abstract domain
145364
* \param ns the namespace
146365
*/
147-
void variable_sensitivity_dependence_grapht::output(
366+
void variable_sensitivity_dependence_domaint::output(
148367
std::ostream &out,
149368
const ai_baset &ai,
150369
const namespacet &ns) const
151370
{
371+
if(!control_deps.empty())
372+
{
373+
out << "Control dependencies: ";
374+
for(control_depst::const_iterator
375+
it=control_deps.begin();
376+
it!=control_deps.end();
377+
++it)
378+
{
379+
if(it!=control_deps.begin())
380+
out << ",";
381+
382+
const goto_programt::const_targett cd=it->first;
383+
const tvt branch=it->second;
384+
385+
out << cd->location_number << " [" << branch << "]";
386+
}
387+
out << "\n";
388+
}
389+
152390
if(!domain_data_deps.empty())
153391
{
154392
out << "Data dependencies: ";
@@ -185,12 +423,26 @@ void variable_sensitivity_dependence_grapht::output(
185423
*
186424
* \return the domain, formatted as a JSON object.
187425
*/
188-
jsont variable_sensitivity_dependence_grapht::output_json(
426+
jsont variable_sensitivity_dependence_domaint::output_json(
189427
const ai_baset &ai,
190428
const namespacet &ns) const
191429
{
192430
json_arrayt graph;
193431

432+
for(const auto &cd : control_deps)
433+
{
434+
const goto_programt::const_targett target=cd.first;
435+
const tvt branch=cd.second;
436+
437+
json_objectt &link=graph.push_back().make_object();
438+
439+
link["locationNumber"]=
440+
json_numbert(std::to_string(target->location_number));
441+
link["sourceLocation"]=json(target->source_location);
442+
link["type"]=json_stringt("control");
443+
link["branch"]=json_stringt(branch.to_string());
444+
}
445+
194446
for(const auto &dep : domain_data_deps)
195447
{
196448
json_objectt &link=graph.push_back().make_object();
@@ -213,3 +465,33 @@ jsont variable_sensitivity_dependence_grapht::output_json(
213465

214466
return graph;
215467
}
468+
469+
void variable_sensitivity_dependence_domaint::populate_dep_graph(
470+
variable_sensitivity_dependence_grapht &dep_graph,
471+
goto_programt::const_targett this_loc) const
472+
{
473+
for(const auto &c_dep : control_deps)
474+
dep_graph.add_dep(vs_dep_edget::kindt::CTRL, c_dep.first, this_loc);
475+
476+
for(const auto &d_dep : domain_data_deps)
477+
dep_graph.add_dep(vs_dep_edget::kindt::DATA, d_dep.first, this_loc);
478+
}
479+
480+
void variable_sensitivity_dependence_grapht::add_dep(
481+
vs_dep_edget::kindt kind,
482+
goto_programt::const_targett from,
483+
goto_programt::const_targett to)
484+
{
485+
const node_indext n_from=state_map[from].get_node_id();
486+
assert(n_from<size());
487+
const node_indext n_to=state_map[to].get_node_id();
488+
assert(n_to<size());
489+
490+
// add_edge is redundant as the subsequent operations also insert
491+
// entries into the edge maps (implicitly)
492+
493+
// add_edge(n_from, n_to);
494+
495+
nodes[n_from].out[n_to].add(kind);
496+
nodes[n_to].in[n_from].add(kind);
497+
}

0 commit comments

Comments
 (0)