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