22
22
* \param ns the namespace to use
23
23
* \param deps the destination in which to accumlate data dependencies
24
24
*/
25
- void variable_sensitivity_dependence_grapht ::eval_data_deps (
25
+ void variable_sensitivity_dependence_domaint ::eval_data_deps (
26
26
const exprt &expr, const namespacet &ns, data_depst &deps) const
27
27
{
28
28
const auto res=
@@ -58,14 +58,64 @@ void variable_sensitivity_dependence_grapht::eval_data_deps(
58
58
* \param ai the abstract interpreter
59
59
* \param ns the namespace
60
60
*/
61
- void variable_sensitivity_dependence_grapht ::transform (
61
+ void variable_sensitivity_dependence_domaint ::transform (
62
62
locationt from,
63
63
locationt to,
64
64
ai_baset &ai,
65
65
const namespacet &ns)
66
66
{
67
67
variable_sensitivity_domaint::transform (from, to, ai, ns);
68
68
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
+ {
69
119
// Find all the data dependencies in the the 'to' expression
70
120
domain_data_deps.clear ();
71
121
if (to->is_assign ())
@@ -76,6 +126,165 @@ void variable_sensitivity_dependence_grapht::transform(
76
126
}
77
127
}
78
128
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
+
79
288
/* *
80
289
* Computes the join between "this" and "b"
81
290
*
@@ -84,18 +293,21 @@ void variable_sensitivity_dependence_grapht::transform(
84
293
* \param to the current location
85
294
* \return true if something has changed in the merge
86
295
*/
87
- bool variable_sensitivity_dependence_grapht ::merge (
296
+ bool variable_sensitivity_dependence_domaint ::merge (
88
297
const variable_sensitivity_domaint &b,
89
298
locationt from,
90
299
locationt to)
91
300
{
92
301
bool changed = false ;
93
302
94
303
changed = variable_sensitivity_domaint::merge (b, from, to);
304
+ changed |= has_values.is_false () || has_changed;
95
305
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);
98
309
310
+ // Merge data dependencies
99
311
for (auto bdep : cast_b.domain_data_deps )
100
312
{
101
313
for (exprt bexpr : bdep.second )
@@ -105,6 +317,13 @@ bool variable_sensitivity_dependence_grapht::merge(
105
317
}
106
318
}
107
319
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
+
108
327
return changed;
109
328
}
110
329
@@ -119,7 +338,7 @@ bool variable_sensitivity_dependence_grapht::merge(
119
338
* between here and this will be retained.
120
339
* \param ns: The global namespace
121
340
*/
122
- void variable_sensitivity_dependence_grapht ::merge_three_way_function_return (
341
+ void variable_sensitivity_dependence_domaint ::merge_three_way_function_return (
123
342
const ai_domain_baset &function_call,
124
343
const ai_domain_baset &function_start,
125
344
const ai_domain_baset &function_end,
@@ -144,11 +363,30 @@ void variable_sensitivity_dependence_grapht::merge_three_way_function_return(
144
363
* \param ai the abstract domain
145
364
* \param ns the namespace
146
365
*/
147
- void variable_sensitivity_dependence_grapht ::output (
366
+ void variable_sensitivity_dependence_domaint ::output (
148
367
std::ostream &out,
149
368
const ai_baset &ai,
150
369
const namespacet &ns) const
151
370
{
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
+
152
390
if (!domain_data_deps.empty ())
153
391
{
154
392
out << " Data dependencies: " ;
@@ -185,12 +423,26 @@ void variable_sensitivity_dependence_grapht::output(
185
423
*
186
424
* \return the domain, formatted as a JSON object.
187
425
*/
188
- jsont variable_sensitivity_dependence_grapht ::output_json (
426
+ jsont variable_sensitivity_dependence_domaint ::output_json (
189
427
const ai_baset &ai,
190
428
const namespacet &ns) const
191
429
{
192
430
json_arrayt graph;
193
431
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
+
194
446
for (const auto &dep : domain_data_deps)
195
447
{
196
448
json_objectt &link =graph.push_back ().make_object ();
@@ -213,3 +465,33 @@ jsont variable_sensitivity_dependence_grapht::output_json(
213
465
214
466
return graph;
215
467
}
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