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