cprover
full_slicer.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Slicing
4 
5 Author: Daniel Kroening, kroening@kroening.com
6 
7 \*******************************************************************/
8 
11 
12 #include "full_slicer.h"
13 #include "full_slicer_class.h"
14 
15 #include <util/find_symbols.h>
16 #include <util/cprover_prefix.h>
17 #ifdef DEBUG_FULL_SLICERT
18 #endif
19 
21 
23  const cfgt::nodet &node,
24  queuet &queue,
25  const dependence_grapht &dep_graph,
26  const dep_node_to_cfgt &dep_node_to_cfg)
27 {
28  const dependence_grapht::nodet &d_node=
29  dep_graph[dep_graph[node.PC].get_node_id()];
30 
31  for(dependence_grapht::edgest::const_iterator
32  it=d_node.in.begin();
33  it!=d_node.in.end();
34  ++it)
35  add_to_queue(queue, dep_node_to_cfg[it->first], node.PC);
36 }
37 
39  const cfgt::nodet &node,
40  queuet &queue,
41  const goto_functionst &goto_functions)
42 {
43  goto_functionst::function_mapt::const_iterator f_it=
44  goto_functions.function_map.find(node.PC->function);
45  assert(f_it!=goto_functions.function_map.end());
46 
47  assert(!f_it->second.body.instructions.empty());
48  goto_programt::const_targett begin_function=
49  f_it->second.body.instructions.begin();
50 
51  cfgt::entry_mapt::const_iterator entry=
52  cfg.entry_map.find(begin_function);
53  assert(entry!=cfg.entry_map.end());
54 
55  for(cfgt::edgest::const_iterator
56  it=cfg[entry->second].in.begin();
57  it!=cfg[entry->second].in.end();
58  ++it)
59  add_to_queue(queue, it->first, node.PC);
60 }
61 
63  const cfgt::nodet &node,
64  queuet &queue,
65  decl_deadt &decl_dead)
66 {
67  if(decl_dead.empty())
68  return;
69 
70  find_symbols_sett syms;
71  find_symbols(node.PC->code, syms);
72  find_symbols(node.PC->guard, syms);
73 
74  for(find_symbols_sett::const_iterator
75  it=syms.begin();
76  it!=syms.end();
77  ++it)
78  {
79  decl_deadt::iterator entry=decl_dead.find(*it);
80  if(entry==decl_dead.end())
81  continue;
82 
83  while(!entry->second.empty())
84  {
85  add_to_queue(queue, entry->second.top(), node.PC);
86  entry->second.pop();
87  }
88 
89  decl_dead.erase(entry);
90  }
91 }
92 
94  queuet &queue,
95  jumpst &jumps,
96  const dependence_grapht::post_dominators_mapt &post_dominators)
97 {
98  // Based on:
99  // On slicing programs with jump statements
100  // Hiralal Agrawal, PLDI'94
101  // Figure 7:
102  // Slice = the slice obtained using the conventional slicing algorithm;
103  // do {
104  // Traverse the postdominator tree using the preorder traversal,
105  // and for each jump statement, J, encountered that is
106  // (i) not in Slice and
107  // (ii) whose nearest postdominator in Slice is different from
108  // the nearest lexical successor in Slice) do {
109  // Add J to Slice;
110  // Add the transitive closure of the dependences of J to Slice;
111  // }
112  // } until no new jump statements may be added to Slice;
113  // For each goto statement, Goto L, in Slice, if the statement
114  // labeled L is not in Slice then associate the label L with its
115  // nearest postdominator in Slice;
116  // return (Slice);
117 
118  for(jumpst::iterator
119  it=jumps.begin();
120  it!=jumps.end();
121  ) // no ++it
122  {
123  jumpst::iterator next=it;
124  ++next;
125 
126  const cfgt::nodet &j=cfg[*it];
127 
128  // is j in the slice already?
129  if(j.node_required)
130  {
131  jumps.erase(it);
132  it=next;
133  continue;
134  }
135 
136  // check nearest lexical successor in slice
137  goto_programt::const_targett lex_succ=j.PC;
138  for( ; !lex_succ->is_end_function(); ++lex_succ)
139  {
140  cfgt::entry_mapt::const_iterator entry=
141  cfg.entry_map.find(lex_succ);
142  assert(entry!=cfg.entry_map.end());
143 
144  if(cfg[entry->second].node_required)
145  break;
146  }
147  if(lex_succ->is_end_function())
148  {
149  it=next;
150  continue;
151  }
152 
154  const cfg_post_dominatorst &pd=post_dominators.at(id);
155 
156  cfg_post_dominatorst::cfgt::entry_mapt::const_iterator e=
157  pd.cfg.entry_map.find(j.PC);
158 
159  assert(e!=pd.cfg.entry_map.end());
160 
162  pd.cfg[e->second];
163 
164  // find the nearest post-dominator in slice
165  if(n.dominators.find(lex_succ)==n.dominators.end())
166  {
167  add_to_queue(queue, *it, lex_succ);
168  jumps.erase(it);
169  }
170  else
171  {
172  // check whether the nearest post-dominator is different from
173  // lex_succ
174  goto_programt::const_targett nearest=lex_succ;
175  std::size_t post_dom_size=0;
176  for(cfg_dominatorst::target_sett::const_iterator
177  d_it=n.dominators.begin();
178  d_it!=n.dominators.end();
179  ++d_it)
180  {
181  cfgt::entry_mapt::const_iterator entry=
182  cfg.entry_map.find(*d_it);
183  assert(entry!=cfg.entry_map.end());
184 
185  if(cfg[entry->second].node_required)
186  {
187  const irep_idt id2=goto_programt::get_function_id(*d_it);
188  assert(id==id2);
189 
190  cfg_post_dominatorst::cfgt::entry_mapt::const_iterator e2=
191  pd.cfg.entry_map.find(*d_it);
192 
193  assert(e2!=pd.cfg.entry_map.end());
194 
196  pd.cfg[e2->second];
197 
198  if(n2.dominators.size()>post_dom_size)
199  {
200  nearest=*d_it;
201  post_dom_size=n2.dominators.size();
202  }
203  }
204  }
205  if(nearest!=lex_succ)
206  {
207  add_to_queue(queue, *it, nearest);
208  jumps.erase(it);
209  }
210  }
211 
212  it=next;
213  }
214 }
215 
217  goto_functionst &goto_functions,
218  queuet &queue,
219  jumpst &jumps,
220  decl_deadt &decl_dead,
221  const dependence_grapht &dep_graph)
222 {
223  std::vector<cfgt::entryt> dep_node_to_cfg;
224  dep_node_to_cfg.reserve(dep_graph.size());
225  for(dependence_grapht::node_indext i=0; i<dep_graph.size(); ++i)
226  {
227  cfgt::entry_mapt::const_iterator entry=
228  cfg.entry_map.find(dep_graph[i].PC);
229  assert(entry!=cfg.entry_map.end());
230 
231  dep_node_to_cfg.push_back(entry->second);
232  }
233 
234  // process queue until empty
235  while(!queue.empty())
236  {
237  while(!queue.empty())
238  {
239  cfgt::entryt e=queue.top();
240  cfgt::nodet &node=cfg[e];
241  queue.pop();
242 
243  // already done by some earlier iteration?
244  if(node.node_required)
245  continue;
246 
247  // node is required
248  node.node_required=true;
249 
250  // add data and control dependencies of node
251  add_dependencies(node, queue, dep_graph, dep_node_to_cfg);
252 
253  // retain all calls of the containing function
254  add_function_calls(node, queue, goto_functions);
255 
256  // find all the symbols it uses to add declarations
257  add_decl_dead(node, queue, decl_dead);
258  }
259 
260  // add any required jumps
261  add_jumps(queue, jumps, dep_graph.cfg_post_dominators());
262  }
263 }
264 
266 {
267  // some variables are used during symbolic execution only
268 
269  const irep_idt &statement=target->code.get_statement();
270  if(statement==ID_array_copy)
271  return true;
272 
273  if(!target->is_assign())
274  return false;
275 
276  const code_assignt &a=to_code_assign(target->code);
277  if(a.lhs().id()!=ID_symbol)
278  return false;
279 
280  const symbol_exprt &s=to_symbol_expr(a.lhs());
281 
282  return s.get_identifier()==CPROVER_PREFIX "rounding_mode";
283 }
284 
286  goto_functionst &goto_functions,
287  const namespacet &ns,
288  slicing_criteriont &criterion)
289 {
290  // build the CFG data structure
291  cfg(goto_functions);
292 
293  // fill queue with according to slicing criterion
294  queuet queue;
295  // gather all unconditional jumps as they may need to be included
296  jumpst jumps;
297  // declarations or dead instructions may be necessary as well
298  decl_deadt decl_dead;
299 
300  for(cfgt::entry_mapt::iterator
301  e_it=cfg.entry_map.begin();
302  e_it!=cfg.entry_map.end();
303  e_it++)
304  {
305  if(criterion(e_it->first))
306  add_to_queue(queue, e_it->second, e_it->first);
307  else if(implicit(e_it->first))
308  add_to_queue(queue, e_it->second, e_it->first);
309  else if((e_it->first->is_goto() && e_it->first->guard.is_true()) ||
310  e_it->first->is_throw())
311  jumps.push_back(e_it->second);
312  else if(e_it->first->is_decl())
313  {
314  const exprt &s=to_code_decl(e_it->first->code).symbol();
315  decl_dead[to_symbol_expr(s).get_identifier()].push(e_it->second);
316  }
317  else if(e_it->first->is_dead())
318  {
319  const exprt &s=to_code_dead(e_it->first->code).symbol();
320  decl_dead[to_symbol_expr(s).get_identifier()].push(e_it->second);
321  }
322  }
323 
324  // compute program dependence graph (and post-dominators)
325  dependence_grapht dep_graph(ns);
326  dep_graph(goto_functions, ns);
327 
328  // compute the fixedpoint
329  fixedpoint(goto_functions, queue, jumps, decl_dead, dep_graph);
330 
331  // now replace those instructions that are not needed
332  // by skips
333 
334  Forall_goto_functions(f_it, goto_functions)
335  if(f_it->second.body_available())
336  {
337  Forall_goto_program_instructions(i_it, f_it->second.body)
338  {
339  const cfgt::entryt &e=cfg.entry_map[i_it];
340  if(!i_it->is_end_function() && // always retained
341  !cfg[e].node_required)
342  i_it->make_skip();
343 #ifdef DEBUG_FULL_SLICERT
344  else
345  {
346  std::string c="ins:"+std::to_string(i_it->location_number);
347  c+=" req by:";
348  for(std::set<unsigned>::const_iterator
349  req_it=cfg[e].required_by.begin();
350  req_it!=cfg[e].required_by.end();
351  ++req_it)
352  {
353  if(req_it!=cfg[e].required_by.begin())
354  c+=",";
355  c+=std::to_string(*req_it);
356  }
357  i_it->source_location.set_column(c); // for show-goto-functions
358  i_it->source_location.set_comment(c); // for dump-c
359  }
360 #endif
361  }
362  }
363 
364  // remove the skips
365  remove_skip(goto_functions);
366  goto_functions.update();
367 }
368 
370  goto_functionst &goto_functions,
371  const namespacet &ns,
372  slicing_criteriont &criterion)
373 {
374  full_slicert()(goto_functions, ns, criterion);
375 }
376 
378  goto_functionst &goto_functions,
379  const namespacet &ns)
380 {
382  full_slicert()(goto_functions, ns, a);
383 }
384 
386  goto_functionst &goto_functions,
387  const namespacet &ns,
388  const std::list<std::string> &properties)
389 {
390  properties_criteriont p(properties);
391  full_slicert()(goto_functions, ns, p);
392 }
393 
395 {
396 }
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:218
void add_dependencies(const cfgt::nodet &node, queuet &queue, const dependence_grapht &dep_graph, const dep_node_to_cfgt &dep_node_to_cfg)
Definition: full_slicer.cpp:22
#define CPROVER_PREFIX
const code_deadt & to_code_dead(const codet &code)
Definition: std_code.h:260
entry_mapt entry_map
Definition: cfg.h:87
exprt & symbol()
Definition: std_code.h:205
virtual ~slicing_criteriont()
const irep_idt & get_identifier() const
Definition: std_expr.h:120
static const irep_idt get_function_id(const_targett l)
static bool implicit(goto_programt::const_targett target)
std::size_t entryt
Definition: cfg.h:65
edgest in
Definition: graph.h:41
std::unordered_set< irep_idt, irep_id_hash > find_symbols_sett
Definition: find_symbols.h:20
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:178
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:157
instructionst::const_iterator const_targett
std::stack< cfgt::entryt > queuet
cfg_base_nodet< cfg_nodet, goto_programt::const_targett > nodet
Definition: graph.h:135
std::map< irep_idt, cfg_post_dominatorst > post_dominators_mapt
void fixedpoint(goto_functionst &goto_functions, queuet &queue, jumpst &jumps, decl_deadt &decl_dead, const dependence_grapht &dep_graph)
TO_BE_DOCUMENTED.
Definition: namespace.h:62
std::list< cfgt::entryt > jumpst
const post_dominators_mapt & cfg_post_dominators() const
std::size_t size() const
Definition: graph.h:177
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, slicing_criteriont &criterion)
void add_decl_dead(const cfgt::nodet &node, queuet &queue, decl_deadt &decl_dead)
Definition: full_slicer.cpp:62
nodet::node_indext node_indext
Definition: graph.h:139
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties)
void add_function_calls(const cfgt::nodet &node, queuet &queue, const goto_functionst &goto_functions)
Definition: full_slicer.cpp:38
exprt & symbol()
Definition: std_code.h:247
std::unordered_map< irep_idt, queuet, irep_id_hash > decl_deadt
void add_to_queue(queuet &queue, const cfgt::entryt &entry, goto_programt::const_targett reason)
void remove_skip(goto_programt &goto_program)
remove unnecessary skip statements
Definition: remove_skip.cpp:71
Base class for all expressions.
Definition: expr.h:46
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:202
#define Forall_goto_functions(it, functions)
Slicing.
const edgest & in(node_indext n) const
Definition: graph.h:187
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:73
Expression to hold a symbol (variable)
Definition: std_expr.h:82
Goto Program Slicing.
Program Transformation.
void operator()(goto_functionst &goto_functions, const namespacet &ns, slicing_criteriont &criterion)
void add_jumps(queuet &queue, jumpst &jumps, const dependence_grapht::post_dominators_mapt &post_dominators)
Definition: full_slicer.cpp:93
std::vector< cfgt::entryt > dep_node_to_cfgt
void find_symbols(const exprt &src, find_symbols_sett &dest)
Assignment.
Definition: std_code.h:144