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