CBMC
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 
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  CHECK_RETURN(f_it != goto_functions.function_map.end());
44 
45  CHECK_RETURN(!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(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 exprt &a_lhs = target->assign_lhs();
246  if(a_lhs.id() != ID_symbol)
247  return false;
248 
249  const symbol_exprt &s = to_symbol_expr(a_lhs);
250 
252 }
253 
255  goto_functionst &goto_functions,
256  const namespacet &ns,
257  const slicing_criteriont &criterion,
258  message_handlert &message_handler)
259 {
260  // build the CFG data structure
261  cfg(goto_functions);
262  for(const auto &gf_entry : goto_functions.function_map)
263  {
264  forall_goto_program_instructions(i_it, gf_entry.second.body)
265  cfg.get_node(i_it).function_id = gf_entry.first;
266  }
267 
268  // fill queue with according to slicing criterion
269  queuet queue;
270  // gather all unconditional jumps as they may need to be included
271  jumpst jumps;
272  // declarations or dead instructions may be necessary as well
273  decl_deadt decl_dead;
274 
275  for(const auto &instruction_and_index : cfg.entries())
276  {
277  const auto &instruction = instruction_and_index.first;
278  const auto instruction_node_index = instruction_and_index.second;
279  if(criterion(cfg[instruction_node_index].function_id, instruction))
280  add_to_queue(queue, instruction_node_index, instruction);
281  else if(implicit(instruction))
282  add_to_queue(queue, instruction_node_index, instruction);
283  else if(
284  (instruction->is_goto() && instruction->condition().is_true()) ||
285  instruction->is_throw())
286  jumps.push_back(instruction_node_index);
287  else if(instruction->is_decl())
288  {
289  const auto &s = instruction->decl_symbol();
290  decl_dead[s.get_identifier()].push(instruction_node_index);
291  }
292  else if(instruction->is_dead())
293  {
294  const auto &s = instruction->dead_symbol();
295  decl_dead[s.get_identifier()].push(instruction_node_index);
296  }
297  }
298 
299  // compute program dependence graph (and post-dominators)
300  dependence_grapht dep_graph(ns, message_handler);
301  dep_graph(goto_functions, ns);
302 
303  // compute the fixedpoint
304  fixedpoint(goto_functions, queue, jumps, decl_dead, dep_graph);
305 
306  // now replace those instructions that are not needed
307  // by skips
308 
309  for(auto &gf_entry : goto_functions.function_map)
310  {
311  if(gf_entry.second.body_available())
312  {
313  Forall_goto_program_instructions(i_it, gf_entry.second.body)
314  {
315  const auto &cfg_node = cfg.get_node(i_it);
316  if(
317  !i_it->is_end_function() && // always retained
318  !cfg_node.node_required)
319  {
320  i_it->turn_into_skip();
321  }
322 #ifdef DEBUG_FULL_SLICERT
323  else
324  {
325  std::string c="ins:"+std::to_string(i_it->location_number);
326  c+=" req by:";
327  for(std::set<unsigned>::const_iterator req_it =
328  cfg_node.required_by.begin();
329  req_it != cfg_node.required_by.end();
330  ++req_it)
331  {
332  if(req_it != cfg_node.required_by.begin())
333  c+=",";
334  c+=std::to_string(*req_it);
335  }
336  i_it->source_location.set_column(c); // for show-goto-functions
337  i_it->source_location.set_comment(c); // for dump-c
338  }
339 #endif
340  }
341  }
342  }
343 
344  // remove the skips
345  remove_skip(goto_functions);
346 }
347 
349  goto_functionst &goto_functions,
350  const namespacet &ns,
351  const slicing_criteriont &criterion,
352  message_handlert &message_handler)
353 {
354  full_slicert()(goto_functions, ns, criterion, message_handler);
355 }
356 
358  goto_functionst &goto_functions,
359  const namespacet &ns,
360  message_handlert &message_handler)
361 {
363  full_slicert()(goto_functions, ns, a, message_handler);
364 }
365 
366 void full_slicer(goto_modelt &goto_model, message_handlert &message_handler)
367 {
369  const namespacet ns(goto_model.symbol_table);
370  full_slicert()(goto_model.goto_functions, ns, a, message_handler);
371 }
372 
374  goto_functionst &goto_functions,
375  const namespacet &ns,
376  const std::list<std::string> &properties,
377  message_handlert &message_handler)
378 {
379  properties_criteriont p(properties);
380  full_slicert()(goto_functions, ns, p, message_handler);
381 }
382 
384  goto_modelt &goto_model,
385  const std::list<std::string> &properties,
386  message_handlert &message_handler)
387 {
388  const namespacet ns(goto_model.symbol_table);
389  property_slicer(goto_model.goto_functions, ns, properties, message_handler);
390 }
391 
393 {
394 }
irep_idt rounding_mode_identifier()
Return the identifier of the program symbol used to store the current rounding mode.
Symbolic Execution.
base_grapht::node_indext entryt
Definition: cfg.h:91
const entry_mapt & entries() const
Get a map from program points to their corresponding node indices.
Definition: cfg.h:259
base_grapht::nodet nodet
Definition: cfg.h:92
entryt get_node_index(const goto_programt::const_targett &program_point) const
Get the graph node index for program_point.
Definition: cfg.h:239
nodet & get_node(const goto_programt::const_targett &program_point)
Get the CFG graph node relating to program_point.
Definition: cfg.h:245
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.
const cfgt::nodet & get_node(const T &program_point) const
Get the graph node (which gives dominators, predecessors and successors) for program_point.
const post_dominators_mapt & cfg_post_dominators() const
std::map< irep_idt, cfg_post_dominatorst > post_dominators_mapt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
Base class for all expressions.
Definition: expr.h:56
void add_function_calls(const cfgt::nodet &node, queuet &queue, const goto_functionst &goto_functions)
Definition: full_slicer.cpp:36
std::list< cfgt::entryt > jumpst
void add_to_queue(queuet &queue, const cfgt::entryt &entry, goto_programt::const_targett reason)
std::unordered_map< irep_idt, queuet > decl_deadt
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
void fixedpoint(goto_functionst &goto_functions, queuet &queue, jumpst &jumps, decl_deadt &decl_dead, const dependence_grapht &dep_graph)
void add_decl_dead(const cfgt::nodet &node, queuet &queue, decl_deadt &decl_dead)
Definition: full_slicer.cpp:54
void operator()(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion, message_handlert &message_handler)
std::stack< cfgt::entryt > queuet
std::vector< cfgt::entryt > dep_node_to_cfgt
void add_jumps(queuet &queue, jumpst &jumps, const dependence_grapht::post_dominators_mapt &post_dominators)
Definition: full_slicer.cpp:85
A collection of goto functions.
function_mapt function_map
symbol_tablet symbol_table
Symbol table.
Definition: goto_model.h:31
goto_functionst goto_functions
GOTO functions.
Definition: goto_model.h:34
instructionst::const_iterator const_targett
Definition: goto_program.h:615
edgest in
Definition: graph.h:42
nodet::node_indext node_indext
Definition: graph.h:173
std::size_t size() const
Definition: graph.h:212
const irep_idt & id() const
Definition: irep.h:384
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
virtual ~slicing_criteriont()
Expression to hold a symbol (variable)
Definition: std_expr.h:131
const irep_idt & get_identifier() const
Definition: std_expr.h:160
static bool find_symbols(symbol_kindt, const typet &, std::function< bool(const symbol_exprt &)>, std::unordered_set< irep_idt > &bindings)
std::unordered_set< irep_idt > find_symbols_sett
Definition: find_symbols.h:20
static bool implicit(goto_programt::const_targett target)
void property_slicer(goto_functionst &goto_functions, const namespacet &ns, const std::list< std::string > &properties, message_handlert &message_handler)
void full_slicer(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion, message_handlert &message_handler)
Goto Program Slicing.
#define forall_goto_program_instructions(it, program)
#define Forall_goto_program_instructions(it, program)
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:87
Program Transformation.
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Definition: std_expr.h:272
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.