CBMC
change_impact.cpp
Go to the documentation of this file.
1 /*******************************************************************\
2 
3 Module: Data and control-dependencies of syntactic diff
4 
5 Author: Michael Tautschnig
6 
7 Date: April 2016
8 
9 \*******************************************************************/
10 
13 
14 #include "change_impact.h"
15 
16 #include <iostream>
17 
19 
21 
22 #include "unified_diff.h"
23 
24 #if 0
25  struct cfg_nodet
26  {
27  cfg_nodet():node_required(false)
28  {
29  }
30 
31  bool node_required;
32 #ifdef DEBUG_FULL_SLICERT
33  std::set<unsigned> required_by;
34 #endif
35  };
36 
37  typedef cfg_baset<cfg_nodet> cfgt;
38  cfgt cfg;
39 
40  typedef std::vector<cfgt::entryt> dep_node_to_cfgt;
41  typedef std::stack<cfgt::entryt> queuet;
42 
43  inline void add_to_queue(
44  queuet &queue,
45  const cfgt::entryt &entry,
47  {
48 #ifdef DEBUG_FULL_SLICERT
49  cfg[entry].required_by.insert(reason->location_number);
50 #endif
51  queue.push(entry);
52  }
53 
55  goto_functionst &goto_functions,
56  const namespacet &ns,
57  slicing_criteriont &criterion)
58 {
59  // build the CFG data structure
60  cfg(goto_functions);
61 
62  // fill queue with according to slicing criterion
63  queuet queue;
64  // gather all unconditional jumps as they may need to be included
65  jumpst jumps;
66  // declarations or dead instructions may be necessary as well
67  decl_deadt decl_dead;
68 
69  for(const auto &entry : cfg.entries())
70  {
71  const auto &instruction = instruction_and_index.first;
72  const auto instruction_node_index = instruction_and_index.second;
73  if(criterion(instruction))
74  add_to_queue(queue, instruction_node_index, instruction);
75  else if(implicit(instruction))
76  add_to_queue(queue, instruction_node_index, instruction);
77  else if((instruction->is_goto() && instruction->guard.is_true()) ||
78  instruction->is_throw())
79  jumps.push_back(instruction_node_index);
80  else if(instruction->is_decl())
81  {
82  const auto &s=instruction->decl_symbol();
83  decl_dead[s.get_identifier()].push(instruction_node_index);
84  }
85  else if(instruction->is_dead())
86  {
87  const auto &s=instruction->dead_symbol();
88  decl_dead[s.get_identifier()].push(instruction_node_index);
89  }
90  }
91 
92  // compute program dependence graph (and post-dominators)
93  dependence_grapht dep_graph(ns);
94  dep_graph(goto_functions, ns);
95 
96  // compute the fixedpoint
97  fixedpoint(goto_functions, queue, jumps, decl_dead, dep_graph);
98 
99  // now replace those instructions that are not needed
100  // by skips
101 
102  for(auto &gf_entry : goto_functions.function_map)
103  {
104  if(gf_entry.second.body_available())
105  {
106  Forall_goto_program_instructions(i_it, gf_entry.second.body)
107  {
108  const auto &node = cfg.get_node(i_it);
109  if(!i_it->is_end_function() && // always retained
110  !node.node_required)
111  i_it->make_skip();
112 #ifdef DEBUG_FULL_SLICERT
113  else
114  {
115  std::string c="ins:"+std::to_string(i_it->location_number);
116  c+=" req by:";
117  for(std::set<unsigned>::const_iterator
118  req_it=node.required_by.begin();
119  req_it!=node.required_by.end();
120  ++req_it)
121  {
122  if(req_it!=node.required_by.begin())
123  c+=",";
124  c+=std::to_string(*req_it);
125  }
126  i_it->source_location.set_column(c); // for show-goto-functions
127  i_it->source_location.set_comment(c); // for dump-c
128  }
129 #endif
130  }
131  }
132  }
133 
134  // remove the skips
135  remove_skip(goto_functions);
136 }
137 
138 
140  goto_functionst &goto_functions,
141  queuet &queue,
142  jumpst &jumps,
143  decl_deadt &decl_dead,
144  const dependence_grapht &dep_graph)
145 {
146  std::vector<cfgt::entryt> dep_node_to_cfg;
147  dep_node_to_cfg.reserve(dep_graph.size());
148 
149  for(unsigned i=0; i<dep_graph.size(); ++i)
150  {
151  dep_node_to_cfg.push_back(cfg.get_node_index(dep_graph[i].PC));
152  }
153 
154  // process queue until empty
155  while(!queue.empty())
156  {
157  while(!queue.empty())
158  {
159  cfgt::entryt e=queue.top();
160  cfgt::nodet &node=cfg[e];
161  queue.pop();
162 
163  // already done by some earlier iteration?
164  if(node.node_required)
165  continue;
166 
167  // node is required
168  node.node_required=true;
169 
170  // add data and control dependencies of node
171  add_dependencies(node, queue, dep_graph, dep_node_to_cfg);
172 
173  // retain all calls of the containing function
174  add_function_calls(node, queue, goto_functions);
175 
176  // find all the symbols it uses to add declarations
177  add_decl_dead(node, queue, decl_dead);
178  }
179 
180  // add any required jumps
181  add_jumps(queue, jumps, dep_graph.cfg_post_dominators());
182  }
183 }
184 
185 
187  const cfgt::nodet &node,
188  queuet &queue,
189  const dependence_grapht &dep_graph,
190  const dep_node_to_cfgt &dep_node_to_cfg)
191 {
192  const dependence_grapht::nodet &d_node=
193  dep_graph[dep_graph[node.PC].get_node_id()];
194 
195  for(dependence_grapht::edgest::const_iterator
196  it=d_node.in.begin();
197  it!=d_node.in.end();
198  ++it)
199  add_to_queue(queue, dep_node_to_cfg[it->first], node.PC);
200 }
201 #endif
202 
204 {
205 public:
207  const goto_modelt &model_old,
208  const goto_modelt &model_new,
210  bool compact_output,
211  message_handlert &message_handler);
212 
213  void operator()();
214 
215 protected:
218 
223 
225 
228 
230  {
231  SAME=0,
232  NEW=1<<0,
233  DELETED=1<<1,
237  DEL_CTRL_DEP=1<<5
238  };
239 
240  typedef std::
241  map<goto_programt::const_targett, unsigned, goto_programt::target_less_than>
243  typedef std::map<irep_idt, goto_program_change_impactt>
245 
247 
248  void change_impact(const irep_idt &function_id);
249 
250  void change_impact(
251  const irep_idt &function_id,
252  const goto_programt &old_goto_program,
253  const goto_programt &new_goto_program,
255  goto_program_change_impactt &old_impact,
256  goto_program_change_impactt &new_impact);
257 
258  void propogate_dep_back(
259  const irep_idt &function_id,
260  const dependence_grapht::nodet &d_node,
261  const dependence_grapht &dep_graph,
263  bool del);
265  const irep_idt &function_id,
266  const dependence_grapht::nodet &d_node,
267  const dependence_grapht &dep_graph,
269  bool del);
270 
272  const irep_idt &function_id,
273  const goto_program_change_impactt &c_i,
274  const goto_functionst &goto_functions,
275  const namespacet &ns) const;
277  const irep_idt &function_id,
278  const goto_program_change_impactt &o_c_i,
279  const goto_functionst &o_goto_functions,
280  const namespacet &o_ns,
281  const goto_program_change_impactt &n_c_i,
282  const goto_functionst &n_goto_functions,
283  const namespacet &n_ns) const;
284 
285  void output_instruction(
286  char prefix,
287  const goto_programt &goto_program,
288  const namespacet &ns,
289  goto_programt::const_targett &target) const;
290 };
291 
293  const goto_modelt &model_old,
294  const goto_modelt &model_new,
295  impact_modet _impact_mode,
296  bool _compact_output,
297  message_handlert &message_handler)
298  : impact_mode(_impact_mode),
299  compact_output(_compact_output),
300  old_goto_functions(model_old.goto_functions),
301  ns_old(model_old.symbol_table),
302  new_goto_functions(model_new.goto_functions),
303  ns_new(model_new.symbol_table),
304  unified_diff(model_old, model_new),
305  old_dep_graph(ns_old, message_handler),
306  new_dep_graph(ns_new, message_handler)
307 {
308  // syntactic difference?
309  if(!unified_diff())
310  return;
311 
312  // compute program dependence graph of old code
314 
315  // compute program dependence graph of new code
317 }
318 
319 void change_impactt::change_impact(const irep_idt &function_id)
320 {
322 
323  if(diff.empty())
324  return;
325 
326  goto_functionst::function_mapt::const_iterator old_fit =
327  old_goto_functions.function_map.find(function_id);
328  goto_functionst::function_mapt::const_iterator new_fit =
329  new_goto_functions.function_map.find(function_id);
330 
331  goto_programt empty;
332 
333  const goto_programt &old_goto_program=
334  old_fit==old_goto_functions.function_map.end() ?
335  empty :
336  old_fit->second.body;
337  const goto_programt &new_goto_program=
338  new_fit==new_goto_functions.function_map.end() ?
339  empty :
340  new_fit->second.body;
341 
343  function_id,
344  old_goto_program,
345  new_goto_program,
346  diff,
347  old_change_impact[function_id],
348  new_change_impact[function_id]);
349 }
350 
352  const irep_idt &function_id,
353  const goto_programt &old_goto_program,
354  const goto_programt &new_goto_program,
356  goto_program_change_impactt &old_impact,
357  goto_program_change_impactt &new_impact)
358 {
360  old_goto_program.instructions.begin();
362  new_goto_program.instructions.begin();
363 
364  for(const auto &d : diff)
365  {
366  switch(d.second)
367  {
369  INVARIANT(o_it != old_goto_program.instructions.end(), "within range");
370  INVARIANT(n_it != new_goto_program.instructions.end(), "within range");
371  old_impact[o_it]|=SAME;
372  ++o_it;
373  INVARIANT(n_it == d.first, "start of hunk");
374  new_impact[n_it]|=SAME;
375  ++n_it;
376  break;
378  INVARIANT(o_it != old_goto_program.instructions.end(), "within range");
379  INVARIANT(o_it == d.first, "start of hunk");
380  {
381  const dependence_grapht::nodet &d_node=
382  old_dep_graph[old_dep_graph[o_it].get_node_id()];
383 
387  function_id, d_node, old_dep_graph, old_change_impact, true);
391  function_id, d_node, old_dep_graph, old_change_impact, true);
392  }
393  old_impact[o_it]|=DELETED;
394  ++o_it;
395  break;
397  INVARIANT(n_it != new_goto_program.instructions.end(), "within range");
398  INVARIANT(n_it == d.first, "start of hunk");
399  {
400  const dependence_grapht::nodet &d_node=
401  new_dep_graph[new_dep_graph[n_it].get_node_id()];
402 
405  {
407  function_id, d_node, new_dep_graph, new_change_impact, false);
408  }
411  {
413  function_id, d_node, new_dep_graph, new_change_impact, false);
414  }
415  }
416  new_impact[n_it]|=NEW;
417  ++n_it;
418  break;
419  }
420  }
421 }
422 
424  const irep_idt &function_id,
425  const dependence_grapht::nodet &d_node,
426  const dependence_grapht &dep_graph,
428  bool del)
429 {
430  for(dependence_grapht::edgest::const_iterator it = d_node.out.begin();
431  it != d_node.out.end(); ++it)
432  {
433  goto_programt::const_targett src = dep_graph[it->first].PC;
434 
435  mod_flagt data_flag = del ? DEL_DATA_DEP : NEW_DATA_DEP;
436  mod_flagt ctrl_flag = del ? DEL_CTRL_DEP : NEW_CTRL_DEP;
437 
438  if(
439  (change_impact[function_id][src] & data_flag) ||
440  (change_impact[function_id][src] & ctrl_flag))
441  continue;
442  if(it->second.get() == dep_edget::kindt::DATA
443  || it->second.get() == dep_edget::kindt::BOTH)
444  change_impact[function_id][src] |= data_flag;
445  else
446  change_impact[function_id][src] |= ctrl_flag;
448  function_id,
449  dep_graph[dep_graph[src].get_node_id()],
450  dep_graph,
452  del);
453  }
454 }
455 
457  const irep_idt &function_id,
458  const dependence_grapht::nodet &d_node,
459  const dependence_grapht &dep_graph,
461  bool del)
462 {
463  for(dependence_grapht::edgest::const_iterator it = d_node.in.begin();
464  it != d_node.in.end(); ++it)
465  {
466  goto_programt::const_targett src = dep_graph[it->first].PC;
467 
468  mod_flagt data_flag = del ? DEL_DATA_DEP : NEW_DATA_DEP;
469  mod_flagt ctrl_flag = del ? DEL_CTRL_DEP : NEW_CTRL_DEP;
470 
471  if(
472  (change_impact[function_id][src] & data_flag) ||
473  (change_impact[function_id][src] & ctrl_flag))
474  {
475  continue;
476  }
477  if(it->second.get() == dep_edget::kindt::DATA
478  || it->second.get() == dep_edget::kindt::BOTH)
479  change_impact[function_id][src] |= data_flag;
480  else
481  change_impact[function_id][src] |= ctrl_flag;
482 
484  function_id,
485  dep_graph[dep_graph[src].get_node_id()],
486  dep_graph,
488  del);
489  }
490 }
491 
493 {
494  // sorted iteration over intersection(old functions, new functions)
495  typedef std::map<irep_idt,
496  goto_functionst::function_mapt::const_iterator>
497  function_mapt;
498 
499  function_mapt old_funcs, new_funcs;
500 
501  for(auto it = old_goto_functions.function_map.begin();
502  it != old_goto_functions.function_map.end();
503  ++it)
504  {
505  old_funcs.insert(std::make_pair(it->first, it));
506  }
507  for(auto it = new_goto_functions.function_map.begin();
508  it != new_goto_functions.function_map.end();
509  ++it)
510  {
511  new_funcs.insert(std::make_pair(it->first, it));
512  }
513 
514  function_mapt::const_iterator ito=old_funcs.begin();
515  for(function_mapt::const_iterator itn=new_funcs.begin();
516  itn!=new_funcs.end();
517  ++itn)
518  {
519  while(ito!=old_funcs.end() && ito->first<itn->first)
520  ++ito;
521 
522  if(ito!=old_funcs.end() && itn->first==ito->first)
523  {
524  change_impact(itn->first);
525 
526  ++ito;
527  }
528  }
529 
530  goto_functions_change_impactt::const_iterator oc_it=
531  old_change_impact.begin();
532  for(goto_functions_change_impactt::const_iterator
533  nc_it=new_change_impact.begin();
534  nc_it!=new_change_impact.end();
535  ++nc_it)
536  {
537  for( ;
538  oc_it!=old_change_impact.end() && oc_it->first<nc_it->first;
539  ++oc_it)
541  oc_it->first,
542  oc_it->second,
544  ns_old);
545 
546  if(oc_it==old_change_impact.end() || nc_it->first<oc_it->first)
548  nc_it->first,
549  nc_it->second,
551  ns_new);
552  else
553  {
554  INVARIANT(oc_it->first == nc_it->first, "same instruction");
555 
557  nc_it->first,
558  oc_it->second,
560  ns_old,
561  nc_it->second,
563  ns_new);
564 
565  ++oc_it;
566  }
567  }
568 }
569 
571  const irep_idt &function_id,
572  const goto_program_change_impactt &c_i,
573  const goto_functionst &goto_functions,
574  const namespacet &ns) const
575 {
576  goto_functionst::function_mapt::const_iterator f_it =
577  goto_functions.function_map.find(function_id);
578  CHECK_RETURN(f_it != goto_functions.function_map.end());
579  const goto_programt &goto_program=f_it->second.body;
580 
581  if(!compact_output)
582  std::cout << "/** " << function_id << " **/\n";
583 
584  forall_goto_program_instructions(target, goto_program)
585  {
586  goto_program_change_impactt::const_iterator c_entry=
587  c_i.find(target);
588  const unsigned mod_flags =
589  c_entry == c_i.end() ? static_cast<unsigned>(SAME) : c_entry->second;
590 
591  char prefix = ' ';
592  // syntactic changes are preferred over data/control-dependence
593  // modifications
594  if(mod_flags==SAME)
595  prefix=' ';
596  else if(mod_flags&DELETED)
597  prefix='-';
598  else if(mod_flags&NEW)
599  prefix='+';
600  else if(mod_flags&NEW_DATA_DEP)
601  prefix='D';
602  else if(mod_flags&NEW_CTRL_DEP)
603  prefix='C';
604  else if(mod_flags&DEL_DATA_DEP)
605  prefix='d';
606  else if(mod_flags&DEL_CTRL_DEP)
607  prefix='c';
608  else
609  UNREACHABLE;
610 
611  output_instruction(prefix, goto_program, ns, target);
612  }
613 }
614 
616  const irep_idt &function_id,
617  const goto_program_change_impactt &o_c_i,
618  const goto_functionst &o_goto_functions,
619  const namespacet &o_ns,
620  const goto_program_change_impactt &n_c_i,
621  const goto_functionst &n_goto_functions,
622  const namespacet &n_ns) const
623 {
624  goto_functionst::function_mapt::const_iterator o_f_it =
625  o_goto_functions.function_map.find(function_id);
626  CHECK_RETURN(o_f_it != o_goto_functions.function_map.end());
627  const goto_programt &old_goto_program=o_f_it->second.body;
628 
629  goto_functionst::function_mapt::const_iterator f_it =
630  n_goto_functions.function_map.find(function_id);
631  CHECK_RETURN(f_it != n_goto_functions.function_map.end());
632  const goto_programt &goto_program=f_it->second.body;
633 
634  if(!compact_output)
635  std::cout << "/** " << function_id << " **/\n";
636 
638  old_goto_program.instructions.begin();
639  forall_goto_program_instructions(target, goto_program)
640  {
641  goto_program_change_impactt::const_iterator o_c_entry=
642  o_c_i.find(o_target);
643  const unsigned old_mod_flags = o_c_entry == o_c_i.end()
644  ? static_cast<unsigned>(SAME)
645  : o_c_entry->second;
646 
647  if(old_mod_flags&DELETED)
648  {
649  output_instruction('-', goto_program, o_ns, o_target);
650  ++o_target;
651  --target;
652  continue;
653  }
654 
655  goto_program_change_impactt::const_iterator c_entry=
656  n_c_i.find(target);
657  const unsigned mod_flags =
658  c_entry == n_c_i.end() ? static_cast<unsigned>(SAME) : c_entry->second;
659 
660  char prefix = ' ';
661  // syntactic changes are preferred over data/control-dependence
662  // modifications
663  if(mod_flags==SAME)
664  {
665  if(old_mod_flags==SAME)
666  prefix=' ';
667  else if(old_mod_flags&DEL_DATA_DEP)
668  prefix='d';
669  else if(old_mod_flags&DEL_CTRL_DEP)
670  prefix='c';
671  else
672  UNREACHABLE;
673 
674  ++o_target;
675  }
676  else if(mod_flags&DELETED)
677  UNREACHABLE;
678  else if(mod_flags&NEW)
679  prefix='+';
680  else if(mod_flags&NEW_DATA_DEP)
681  {
682  prefix='D';
683 
685  old_mod_flags == SAME || old_mod_flags & DEL_DATA_DEP ||
686  old_mod_flags & DEL_CTRL_DEP,
687  "expected kind of flag");
688  ++o_target;
689  }
690  else if(mod_flags&NEW_CTRL_DEP)
691  {
692  prefix='C';
693 
695  old_mod_flags == SAME || old_mod_flags & DEL_DATA_DEP ||
696  old_mod_flags & DEL_CTRL_DEP,
697  "expected kind of flag");
698  ++o_target;
699  }
700  else
701  UNREACHABLE;
702 
703  output_instruction(prefix, goto_program, n_ns, target);
704  }
705  for( ;
706  o_target!=old_goto_program.instructions.end();
707  ++o_target)
708  {
709  goto_program_change_impactt::const_iterator o_c_entry=
710  o_c_i.find(o_target);
711  const unsigned old_mod_flags = o_c_entry == o_c_i.end()
712  ? static_cast<unsigned>(SAME)
713  : o_c_entry->second;
714 
715  char prefix = ' ';
716  // syntactic changes are preferred over data/control-dependence
717  // modifications
718  if(old_mod_flags==SAME)
719  UNREACHABLE;
720  else if(old_mod_flags&DELETED)
721  prefix='-';
722  else if(old_mod_flags&NEW)
723  UNREACHABLE;
724  else if(old_mod_flags&DEL_DATA_DEP)
725  prefix='d';
726  else if(old_mod_flags&DEL_CTRL_DEP)
727  prefix='c';
728  else
729  UNREACHABLE;
730 
731  output_instruction(prefix, goto_program, o_ns, o_target);
732  }
733 }
734 
736  char prefix,
737  const goto_programt &goto_program,
738  const namespacet &ns,
739  goto_programt::const_targett &target) const
740 {
741  if(compact_output)
742  {
743  if(prefix == ' ')
744  return;
745  const irep_idt &file = target->source_location().get_file();
746  const irep_idt &line = target->source_location().get_line();
747  if(!file.empty() && !line.empty())
748  std::cout << prefix << " " << id2string(file)
749  << " " << id2string(line) << '\n';
750  }
751  else
752  {
753  std::cout << prefix;
754  target->output(std::cout);
755  }
756 }
757 
759  const goto_modelt &model_old,
760  const goto_modelt &model_new,
761  impact_modet impact_mode,
762  bool compact_output,
763  message_handlert &message_handler)
764 {
765  change_impactt c(
766  model_old, model_new, impact_mode, compact_output, message_handler);
767  c();
768 }
void change_impact(const goto_modelt &model_old, const goto_modelt &model_new, impact_modet impact_mode, bool compact_output, message_handlert &message_handler)
Data and control-dependencies of syntactic diff.
impact_modet
Definition: change_impact.h:19
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
goto_functions_change_impactt old_change_impact
unified_difft unified_diff
std::map< goto_programt::const_targett, unsigned, goto_programt::target_less_than > goto_program_change_impactt
void change_impact(const irep_idt &function_id)
change_impactt(const goto_modelt &model_old, const goto_modelt &model_new, impact_modet impact_mode, bool compact_output, message_handlert &message_handler)
void output_instruction(char prefix, const goto_programt &goto_program, const namespacet &ns, goto_programt::const_targett &target) const
dependence_grapht new_dep_graph
void propogate_dep_back(const irep_idt &function_id, const dependence_grapht::nodet &d_node, const dependence_grapht &dep_graph, goto_functions_change_impactt &change_impact, bool del)
std::map< irep_idt, goto_program_change_impactt > goto_functions_change_impactt
const goto_functionst & old_goto_functions
const namespacet ns_old
goto_functions_change_impactt new_change_impact
void output_change_impact(const irep_idt &function_id, const goto_program_change_impactt &c_i, const goto_functionst &goto_functions, const namespacet &ns) const
dependence_grapht old_dep_graph
void propogate_dep_forward(const irep_idt &function_id, const dependence_grapht::nodet &d_node, const dependence_grapht &dep_graph, goto_functions_change_impactt &change_impact, bool del)
const goto_functionst & new_goto_functions
const namespacet ns_new
impact_modet impact_mode
const post_dominators_mapt & cfg_post_dominators() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:38
bool empty() const
Definition: dstring.h:89
std::string::const_iterator begin() const
Definition: dstring.h:193
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
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
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:73
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:622
instructionst::const_iterator const_targett
Definition: goto_program.h:615
edgest in
Definition: graph.h:42
dep_nodet nodet
Definition: graph.h:169
std::size_t size() const
Definition: graph.h:212
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:94
std::list< std::pair< goto_programt::const_targett, differencet > > goto_program_difft
Definition: unified_diff.h:46
goto_program_difft get_diff(const irep_idt &function) const
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
static bool implicit(goto_programt::const_targett target)
Symbol Table + CFG.
#define forall_goto_program_instructions(it, program)
#define Forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
Definition: irep.h:44
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
Definition: remove_skip.cpp:87
#define CHECK_RETURN(CONDITION)
Definition: invariant.h:495
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:525
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
Definition: invariant.h:534
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Unified diff (using LCSS) of goto functions.
dstringt irep_idt