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 
153  const irep_idt id=j.PC->function;
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=(*d_it)->function;
188  INVARIANT(id==id2,
189  "goto/jump expected to be within a single function");
190 
191  cfg_post_dominatorst::cfgt::entry_mapt::const_iterator e2=
192  pd.cfg.entry_map.find(*d_it);
193 
194  assert(e2!=pd.cfg.entry_map.end());
195 
197  pd.cfg[e2->second];
198 
199  if(n2.dominators.size()>post_dom_size)
200  {
201  nearest=*d_it;
202  post_dom_size=n2.dominators.size();
203  }
204  }
205  }
206  if(nearest!=lex_succ)
207  {
208  add_to_queue(queue, *it, nearest);
209  jumps.erase(it);
210  }
211  }
212 
213  it=next;
214  }
215 }
216 
218  goto_functionst &goto_functions,
219  queuet &queue,
220  jumpst &jumps,
221  decl_deadt &decl_dead,
222  const dependence_grapht &dep_graph)
223 {
224  std::vector<cfgt::entryt> dep_node_to_cfg;
225  dep_node_to_cfg.reserve(dep_graph.size());
226  for(dependence_grapht::node_indext i=0; i<dep_graph.size(); ++i)
227  {
228  cfgt::entry_mapt::const_iterator entry=
229  cfg.entry_map.find(dep_graph[i].PC);
230  assert(entry!=cfg.entry_map.end());
231 
232  dep_node_to_cfg.push_back(entry->second);
233  }
234 
235  // process queue until empty
236  while(!queue.empty())
237  {
238  while(!queue.empty())
239  {
240  cfgt::entryt e=queue.top();
241  cfgt::nodet &node=cfg[e];
242  queue.pop();
243 
244  // already done by some earlier iteration?
245  if(node.node_required)
246  continue;
247 
248  // node is required
249  node.node_required=true;
250 
251  // add data and control dependencies of node
252  add_dependencies(node, queue, dep_graph, dep_node_to_cfg);
253 
254  // retain all calls of the containing function
255  add_function_calls(node, queue, goto_functions);
256 
257  // find all the symbols it uses to add declarations
258  add_decl_dead(node, queue, decl_dead);
259  }
260 
261  // add any required jumps
262  add_jumps(queue, jumps, dep_graph.cfg_post_dominators());
263  }
264 }
265 
267 {
268  // some variables are used during symbolic execution only
269 
270  const irep_idt &statement=target->code.get_statement();
271  if(statement==ID_array_copy)
272  return true;
273 
274  if(!target->is_assign())
275  return false;
276 
277  const code_assignt &a=to_code_assign(target->code);
278  if(a.lhs().id()!=ID_symbol)
279  return false;
280 
281  const symbol_exprt &s=to_symbol_expr(a.lhs());
282 
283  return s.get_identifier()==CPROVER_PREFIX "rounding_mode";
284 }
285 
287  goto_functionst &goto_functions,
288  const namespacet &ns,
290 {
291  // build the CFG data structure
292  cfg(goto_functions);
293 
294  // fill queue with according to slicing criterion
295  queuet queue;
296  // gather all unconditional jumps as they may need to be included
297  jumpst jumps;
298  // declarations or dead instructions may be necessary as well
299  decl_deadt decl_dead;
300 
301  for(cfgt::entry_mapt::iterator
302  e_it=cfg.entry_map.begin();
303  e_it!=cfg.entry_map.end();
304  e_it++)
305  {
306  if(criterion(e_it->first))
307  add_to_queue(queue, e_it->second, e_it->first);
308  else if(implicit(e_it->first))
309  add_to_queue(queue, e_it->second, e_it->first);
310  else if((e_it->first->is_goto() && e_it->first->guard.is_true()) ||
311  e_it->first->is_throw())
312  jumps.push_back(e_it->second);
313  else if(e_it->first->is_decl())
314  {
315  const exprt &s=to_code_decl(e_it->first->code).symbol();
316  decl_dead[to_symbol_expr(s).get_identifier()].push(e_it->second);
317  }
318  else if(e_it->first->is_dead())
319  {
320  const exprt &s=to_code_dead(e_it->first->code).symbol();
321  decl_dead[to_symbol_expr(s).get_identifier()].push(e_it->second);
322  }
323  }
324 
325  // compute program dependence graph (and post-dominators)
326  dependence_grapht dep_graph(ns);
327  dep_graph(goto_functions, ns);
328 
329  // compute the fixedpoint
330  fixedpoint(goto_functions, queue, jumps, decl_dead, dep_graph);
331 
332  // now replace those instructions that are not needed
333  // by skips
334 
335  Forall_goto_functions(f_it, goto_functions)
336  if(f_it->second.body_available())
337  {
338  Forall_goto_program_instructions(i_it, f_it->second.body)
339  {
340  const cfgt::entryt &e=cfg.entry_map[i_it];
341  if(!i_it->is_end_function() && // always retained
342  !cfg[e].node_required)
343  i_it->make_skip();
344 #ifdef DEBUG_FULL_SLICERT
345  else
346  {
347  std::string c="ins:"+std::to_string(i_it->location_number);
348  c+=" req by:";
349  for(std::set<unsigned>::const_iterator
350  req_it=cfg[e].required_by.begin();
351  req_it!=cfg[e].required_by.end();
352  ++req_it)
353  {
354  if(req_it!=cfg[e].required_by.begin())
355  c+=",";
356  c+=std::to_string(*req_it);
357  }
358  i_it->source_location.set_column(c); // for show-goto-functions
359  i_it->source_location.set_comment(c); // for dump-c
360  }
361 #endif
362  }
363  }
364 
365  // remove the skips
366  remove_skip(goto_functions);
367 }
368 
370  goto_functionst &goto_functions,
371  const namespacet &ns,
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 
385 void full_slicer(goto_modelt &goto_model)
386 {
388  const namespacet ns(goto_model.symbol_table);
389  full_slicert()(goto_model.goto_functions, ns, a);
390 }
391 
393  goto_functionst &goto_functions,
394  const namespacet &ns,
395  const std::list<std::string> &properties)
396 {
397  properties_criteriont p(properties);
398  full_slicert()(goto_functions, ns, p);
399 }
400 
402  goto_modelt &goto_model,
403  const std::list<std::string> &properties)
404 {
405  const namespacet ns(goto_model.symbol_table);
406  property_slicer(goto_model.goto_functions, ns, properties);
407 }
408 
410 {
411 }
const code_declt & to_code_decl(const codet &code)
Definition: std_code.h:289
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:341
entry_mapt entry_map
Definition: cfg.h:106
exprt & symbol()
Definition: std_code.h:266
virtual ~slicing_criteriont()
const irep_idt & get_identifier() const
Definition: std_expr.h:128
std::unordered_map< irep_idt, queuet > decl_deadt
static bool implicit(goto_programt::const_targett target)
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:29
std::size_t entryt
Definition: cfg.h:65
#define INVARIANT(CONDITION, REASON)
Definition: invariant.h:205
edgest in
Definition: graph.h:42
const code_assignt & to_code_assign(const codet &code)
Definition: std_code.h:239
const irep_idt & id() const
Definition: irep.h:189
exprt & lhs()
Definition: std_code.h:208
std::stack< cfgt::entryt > queuet
cfg_base_nodet< cfg_nodet, goto_programt::const_targett > nodet
Definition: graph.h:136
std::map< irep_idt, cfg_post_dominatorst > post_dominators_mapt
instructionst::const_iterator const_targett
Definition: goto_program.h:398
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:74
std::list< cfgt::entryt > jumpst
const post_dominators_mapt & cfg_post_dominators() const
std::size_t size() const
Definition: graph.h:178
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
Definition: std_expr.h:210
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:140
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:318
void add_to_queue(queuet &queue, const cfgt::entryt &entry, goto_programt::const_targett reason)
Base class for all expressions.
Definition: expr.h:42
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:86
std::string to_string(const string_constraintt &expr)
Used for debug printing.
#define Forall_goto_functions(it, functions)
goto_programt coverage_criteriont criterion
Definition: cover.cpp:63
Slicing.
const edgest & in(node_indext n) const
Definition: graph.h:188
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:740
Expression to hold a symbol (variable)
Definition: std_expr.h:90
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:20
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)
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:32
Assignment.
Definition: std_code.h:195