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 
212  void operator()();
213 
214 protected:
217 
222 
224 
227 
229  {
230  SAME=0,
231  NEW=1<<0,
232  DELETED=1<<1,
237  };
238 
239  typedef std::map<goto_programt::const_targett, unsigned>
241  typedef std::map<irep_idt, goto_program_change_impactt>
243 
245 
246  void change_impact(const irep_idt &function_id);
247 
248  void change_impact(
249  const irep_idt &function_id,
250  const goto_programt &old_goto_program,
251  const goto_programt &new_goto_program,
253  goto_program_change_impactt &old_impact,
254  goto_program_change_impactt &new_impact);
255 
256  void propogate_dep_back(
257  const irep_idt &function_id,
258  const dependence_grapht::nodet &d_node,
259  const dependence_grapht &dep_graph,
261  bool del);
263  const irep_idt &function_id,
264  const dependence_grapht::nodet &d_node,
265  const dependence_grapht &dep_graph,
267  bool del);
268 
270  const irep_idt &function_id,
271  const goto_program_change_impactt &c_i,
272  const goto_functionst &goto_functions,
273  const namespacet &ns) const;
275  const irep_idt &function_id,
276  const goto_program_change_impactt &o_c_i,
277  const goto_functionst &o_goto_functions,
278  const namespacet &o_ns,
279  const goto_program_change_impactt &n_c_i,
280  const goto_functionst &n_goto_functions,
281  const namespacet &n_ns) const;
282 
283  void output_instruction(
284  char prefix,
285  const goto_programt &goto_program,
286  const namespacet &ns,
287  goto_programt::const_targett &target) const;
288 };
289 
291  const goto_modelt &model_old,
292  const goto_modelt &model_new,
293  impact_modet _impact_mode,
294  bool _compact_output):
295  impact_mode(_impact_mode),
296  compact_output(_compact_output),
297  old_goto_functions(model_old.goto_functions),
298  ns_old(model_old.symbol_table),
299  new_goto_functions(model_new.goto_functions),
300  ns_new(model_new.symbol_table),
301  unified_diff(model_old, model_new),
302  old_dep_graph(ns_old),
303  new_dep_graph(ns_new)
304 {
305  // syntactic difference?
306  if(!unified_diff())
307  return;
308 
309  // compute program dependence graph of old code
311 
312  // compute program dependence graph of new code
314 }
315 
316 void change_impactt::change_impact(const irep_idt &function_id)
317 {
319 
320  if(diff.empty())
321  return;
322 
323  goto_functionst::function_mapt::const_iterator old_fit =
324  old_goto_functions.function_map.find(function_id);
325  goto_functionst::function_mapt::const_iterator new_fit =
326  new_goto_functions.function_map.find(function_id);
327 
328  goto_programt empty;
329 
330  const goto_programt &old_goto_program=
331  old_fit==old_goto_functions.function_map.end() ?
332  empty :
333  old_fit->second.body;
334  const goto_programt &new_goto_program=
335  new_fit==new_goto_functions.function_map.end() ?
336  empty :
337  new_fit->second.body;
338 
340  function_id,
341  old_goto_program,
342  new_goto_program,
343  diff,
344  old_change_impact[function_id],
345  new_change_impact[function_id]);
346 }
347 
349  const irep_idt &function_id,
350  const goto_programt &old_goto_program,
351  const goto_programt &new_goto_program,
353  goto_program_change_impactt &old_impact,
354  goto_program_change_impactt &new_impact)
355 {
357  old_goto_program.instructions.begin();
359  new_goto_program.instructions.begin();
360 
361  for(const auto &d : diff)
362  {
363  switch(d.second)
364  {
366  assert(o_it!=old_goto_program.instructions.end());
367  assert(n_it!=new_goto_program.instructions.end());
368  old_impact[o_it]|=SAME;
369  ++o_it;
370  assert(n_it==d.first);
371  new_impact[n_it]|=SAME;
372  ++n_it;
373  break;
375  assert(o_it!=old_goto_program.instructions.end());
376  assert(o_it==d.first);
377  {
378  const dependence_grapht::nodet &d_node=
379  old_dep_graph[old_dep_graph[o_it].get_node_id()];
380 
384  function_id, d_node, old_dep_graph, old_change_impact, true);
388  function_id, d_node, old_dep_graph, old_change_impact, true);
389  }
390  old_impact[o_it]|=DELETED;
391  ++o_it;
392  break;
394  assert(n_it!=new_goto_program.instructions.end());
395  assert(n_it==d.first);
396  {
397  const dependence_grapht::nodet &d_node=
398  new_dep_graph[new_dep_graph[n_it].get_node_id()];
399 
402  {
404  function_id, d_node, new_dep_graph, new_change_impact, false);
405  }
408  {
410  function_id, d_node, new_dep_graph, new_change_impact, false);
411  }
412  }
413  new_impact[n_it]|=NEW;
414  ++n_it;
415  break;
416  }
417  }
418 }
419 
421  const irep_idt &function_id,
422  const dependence_grapht::nodet &d_node,
423  const dependence_grapht &dep_graph,
425  bool del)
426 {
427  for(dependence_grapht::edgest::const_iterator it = d_node.out.begin();
428  it != d_node.out.end(); ++it)
429  {
430  goto_programt::const_targett src = dep_graph[it->first].PC;
431 
432  mod_flagt data_flag = del ? DEL_DATA_DEP : NEW_DATA_DEP;
433  mod_flagt ctrl_flag = del ? DEL_CTRL_DEP : NEW_CTRL_DEP;
434 
435  if(
436  (change_impact[function_id][src] & data_flag) ||
437  (change_impact[function_id][src] & ctrl_flag))
438  continue;
439  if(it->second.get() == dep_edget::kindt::DATA
440  || it->second.get() == dep_edget::kindt::BOTH)
441  change_impact[function_id][src] |= data_flag;
442  else
443  change_impact[function_id][src] |= ctrl_flag;
445  function_id,
446  dep_graph[dep_graph[src].get_node_id()],
447  dep_graph,
449  del);
450  }
451 }
452 
454  const irep_idt &function_id,
455  const dependence_grapht::nodet &d_node,
456  const dependence_grapht &dep_graph,
458  bool del)
459 {
460  for(dependence_grapht::edgest::const_iterator it = d_node.in.begin();
461  it != d_node.in.end(); ++it)
462  {
463  goto_programt::const_targett src = dep_graph[it->first].PC;
464 
465  mod_flagt data_flag = del ? DEL_DATA_DEP : NEW_DATA_DEP;
466  mod_flagt ctrl_flag = del ? DEL_CTRL_DEP : NEW_CTRL_DEP;
467 
468  if(
469  (change_impact[function_id][src] & data_flag) ||
470  (change_impact[function_id][src] & ctrl_flag))
471  {
472  continue;
473  }
474  if(it->second.get() == dep_edget::kindt::DATA
475  || it->second.get() == dep_edget::kindt::BOTH)
476  change_impact[function_id][src] |= data_flag;
477  else
478  change_impact[function_id][src] |= ctrl_flag;
479 
481  function_id,
482  dep_graph[dep_graph[src].get_node_id()],
483  dep_graph,
485  del);
486  }
487 }
488 
490 {
491  // sorted iteration over intersection(old functions, new functions)
492  typedef std::map<irep_idt,
493  goto_functionst::function_mapt::const_iterator>
494  function_mapt;
495 
496  function_mapt old_funcs, new_funcs;
497 
498  for(auto it = old_goto_functions.function_map.begin();
499  it != old_goto_functions.function_map.end();
500  ++it)
501  {
502  old_funcs.insert(std::make_pair(it->first, it));
503  }
504  for(auto it = new_goto_functions.function_map.begin();
505  it != new_goto_functions.function_map.end();
506  ++it)
507  {
508  new_funcs.insert(std::make_pair(it->first, it));
509  }
510 
511  function_mapt::const_iterator ito=old_funcs.begin();
512  for(function_mapt::const_iterator itn=new_funcs.begin();
513  itn!=new_funcs.end();
514  ++itn)
515  {
516  while(ito!=old_funcs.end() && ito->first<itn->first)
517  ++ito;
518 
519  if(ito!=old_funcs.end() && itn->first==ito->first)
520  {
521  change_impact(itn->first);
522 
523  ++ito;
524  }
525  }
526 
527  goto_functions_change_impactt::const_iterator oc_it=
528  old_change_impact.begin();
529  for(goto_functions_change_impactt::const_iterator
530  nc_it=new_change_impact.begin();
531  nc_it!=new_change_impact.end();
532  ++nc_it)
533  {
534  for( ;
535  oc_it!=old_change_impact.end() && oc_it->first<nc_it->first;
536  ++oc_it)
538  oc_it->first,
539  oc_it->second,
541  ns_old);
542 
543  if(oc_it==old_change_impact.end() || nc_it->first<oc_it->first)
545  nc_it->first,
546  nc_it->second,
548  ns_new);
549  else
550  {
551  assert(oc_it->first==nc_it->first);
552 
554  nc_it->first,
555  oc_it->second,
557  ns_old,
558  nc_it->second,
560  ns_new);
561 
562  ++oc_it;
563  }
564  }
565 }
566 
568  const irep_idt &function_id,
569  const goto_program_change_impactt &c_i,
570  const goto_functionst &goto_functions,
571  const namespacet &ns) const
572 {
573  goto_functionst::function_mapt::const_iterator f_it =
574  goto_functions.function_map.find(function_id);
575  assert(f_it!=goto_functions.function_map.end());
576  const goto_programt &goto_program=f_it->second.body;
577 
578  if(!compact_output)
579  std::cout << "/** " << function_id << " **/\n";
580 
581  forall_goto_program_instructions(target, goto_program)
582  {
583  goto_program_change_impactt::const_iterator c_entry=
584  c_i.find(target);
585  const unsigned mod_flags =
586  c_entry == c_i.end() ? static_cast<unsigned>(SAME) : c_entry->second;
587 
588  char prefix = ' ';
589  // syntactic changes are preferred over data/control-dependence
590  // modifications
591  if(mod_flags==SAME)
592  prefix=' ';
593  else if(mod_flags&DELETED)
594  prefix='-';
595  else if(mod_flags&NEW)
596  prefix='+';
597  else if(mod_flags&NEW_DATA_DEP)
598  prefix='D';
599  else if(mod_flags&NEW_CTRL_DEP)
600  prefix='C';
601  else if(mod_flags&DEL_DATA_DEP)
602  prefix='d';
603  else if(mod_flags&DEL_CTRL_DEP)
604  prefix='c';
605  else
606  UNREACHABLE;
607 
608  output_instruction(prefix, goto_program, ns, target);
609  }
610 }
611 
613  const irep_idt &function_id,
614  const goto_program_change_impactt &o_c_i,
615  const goto_functionst &o_goto_functions,
616  const namespacet &o_ns,
617  const goto_program_change_impactt &n_c_i,
618  const goto_functionst &n_goto_functions,
619  const namespacet &n_ns) const
620 {
621  goto_functionst::function_mapt::const_iterator o_f_it =
622  o_goto_functions.function_map.find(function_id);
623  assert(o_f_it!=o_goto_functions.function_map.end());
624  const goto_programt &old_goto_program=o_f_it->second.body;
625 
626  goto_functionst::function_mapt::const_iterator f_it =
627  n_goto_functions.function_map.find(function_id);
628  assert(f_it!=n_goto_functions.function_map.end());
629  const goto_programt &goto_program=f_it->second.body;
630 
631  if(!compact_output)
632  std::cout << "/** " << function_id << " **/\n";
633 
635  old_goto_program.instructions.begin();
636  forall_goto_program_instructions(target, goto_program)
637  {
638  goto_program_change_impactt::const_iterator o_c_entry=
639  o_c_i.find(o_target);
640  const unsigned old_mod_flags = o_c_entry == o_c_i.end()
641  ? static_cast<unsigned>(SAME)
642  : o_c_entry->second;
643 
644  if(old_mod_flags&DELETED)
645  {
646  output_instruction('-', goto_program, o_ns, o_target);
647  ++o_target;
648  --target;
649  continue;
650  }
651 
652  goto_program_change_impactt::const_iterator c_entry=
653  n_c_i.find(target);
654  const unsigned mod_flags =
655  c_entry == n_c_i.end() ? static_cast<unsigned>(SAME) : c_entry->second;
656 
657  char prefix = ' ';
658  // syntactic changes are preferred over data/control-dependence
659  // modifications
660  if(mod_flags==SAME)
661  {
662  if(old_mod_flags==SAME)
663  prefix=' ';
664  else if(old_mod_flags&DEL_DATA_DEP)
665  prefix='d';
666  else if(old_mod_flags&DEL_CTRL_DEP)
667  prefix='c';
668  else
669  UNREACHABLE;
670 
671  ++o_target;
672  }
673  else if(mod_flags&DELETED)
674  UNREACHABLE;
675  else if(mod_flags&NEW)
676  prefix='+';
677  else if(mod_flags&NEW_DATA_DEP)
678  {
679  prefix='D';
680 
681  assert(old_mod_flags==SAME ||
682  old_mod_flags&DEL_DATA_DEP ||
683  old_mod_flags&DEL_CTRL_DEP);
684  ++o_target;
685  }
686  else if(mod_flags&NEW_CTRL_DEP)
687  {
688  prefix='C';
689 
690  assert(old_mod_flags==SAME ||
691  old_mod_flags&DEL_DATA_DEP ||
692  old_mod_flags&DEL_CTRL_DEP);
693  ++o_target;
694  }
695  else
696  UNREACHABLE;
697 
698  output_instruction(prefix, goto_program, n_ns, target);
699  }
700  for( ;
701  o_target!=old_goto_program.instructions.end();
702  ++o_target)
703  {
704  goto_program_change_impactt::const_iterator o_c_entry=
705  o_c_i.find(o_target);
706  const unsigned old_mod_flags = o_c_entry == o_c_i.end()
707  ? static_cast<unsigned>(SAME)
708  : o_c_entry->second;
709 
710  char prefix = ' ';
711  // syntactic changes are preferred over data/control-dependence
712  // modifications
713  if(old_mod_flags==SAME)
714  UNREACHABLE;
715  else if(old_mod_flags&DELETED)
716  prefix='-';
717  else if(old_mod_flags&NEW)
718  UNREACHABLE;
719  else if(old_mod_flags&DEL_DATA_DEP)
720  prefix='d';
721  else if(old_mod_flags&DEL_CTRL_DEP)
722  prefix='c';
723  else
724  UNREACHABLE;
725 
726  output_instruction(prefix, goto_program, o_ns, o_target);
727  }
728 }
729 
731  char prefix,
732  const goto_programt &goto_program,
733  const namespacet &ns,
734  goto_programt::const_targett &target) const
735 {
736  if(compact_output)
737  {
738  if(prefix == ' ')
739  return;
740  const irep_idt &file = target->source_location().get_file();
741  const irep_idt &line = target->source_location().get_line();
742  if(!file.empty() && !line.empty())
743  std::cout << prefix << " " << id2string(file)
744  << " " << id2string(line) << '\n';
745  }
746  else
747  {
748  std::cout << prefix;
749  target->output(std::cout);
750  }
751 }
752 
754  const goto_modelt &model_old,
755  const goto_modelt &model_new,
756  impact_modet impact_mode,
757  bool compact_output)
758 {
759  change_impactt c(model_old, model_new, impact_mode, compact_output);
760  c();
761 }
Forall_goto_program_instructions
#define Forall_goto_program_instructions(it, program)
Definition: goto_program.h:1234
UNREACHABLE
#define UNREACHABLE
This should be used to mark dead code.
Definition: invariant.h:503
dstringt
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition: dstring.h:36
impact_modet
impact_modet
Definition: change_impact.h:18
grapht::size
std::size_t size() const
Definition: graph.h:212
change_impactt::operator()
void operator()()
Definition: change_impact.cpp:489
change_impactt::goto_program_change_impactt
std::map< goto_programt::const_targett, unsigned > goto_program_change_impactt
Definition: change_impact.cpp:240
dependence_grapht
Definition: dependence_graph.h:211
impact_modet::BACKWARD
@ BACKWARD
change_impactt::old_change_impact
goto_functions_change_impactt old_change_impact
Definition: change_impact.cpp:244
slicing_criteriont
Definition: full_slicer.h:35
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:87
change_impactt::new_goto_functions
const goto_functionst & new_goto_functions
Definition: change_impact.cpp:220
change_impactt::propogate_dep_forward
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)
Definition: change_impact.cpp:420
dependence_grapht::cfg_post_dominators
const post_dominators_mapt & cfg_post_dominators() const
Definition: dependence_graph.h:272
goto_model.h
change_impact
void change_impact(const goto_modelt &model_old, const goto_modelt &model_new, impact_modet impact_mode, bool compact_output)
Definition: change_impact.cpp:753
unified_difft::differencet::SAME
@ SAME
goto_modelt
Definition: goto_model.h:25
change_impactt::ns_old
const namespacet ns_old
Definition: change_impact.cpp:219
change_impactt::NEW_DATA_DEP
@ NEW_DATA_DEP
Definition: change_impact.cpp:233
irep_idt
dstringt irep_idt
Definition: irep.h:37
to_string
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Definition: string_constraint.cpp:58
impact_modet::BOTH
@ BOTH
change_impactt::old_goto_functions
const goto_functionst & old_goto_functions
Definition: change_impact.cpp:218
goto_functionst::function_map
function_mapt function_map
Definition: goto_functions.h:29
change_impactt::unified_diff
unified_difft unified_diff
Definition: change_impact.cpp:223
cfg_baset::entries
const entry_mapt & entries() const
Get a map from program points to their corresponding node indices.
Definition: cfg.h:259
change_impactt::change_impact
void change_impact(const irep_idt &function_id)
Definition: change_impact.cpp:316
unified_difft
Definition: unified_diff.h:29
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
change_impactt::output_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
Definition: change_impact.cpp:567
change_impactt::mod_flagt
mod_flagt
Definition: change_impact.cpp:228
namespacet
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition: namespace.h:90
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:21
unified_diff.h
change_impactt::propogate_dep_back
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)
Definition: change_impact.cpp:453
graph_nodet::in
edgest in
Definition: graph.h:42
change_impactt::goto_functions_change_impactt
std::map< irep_idt, goto_program_change_impactt > goto_functions_change_impactt
Definition: change_impact.cpp:242
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
id2string
const std::string & id2string(const irep_idt &d)
Definition: irep.h:47
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
change_impactt::NEW
@ NEW
Definition: change_impact.cpp:231
change_impactt::change_impactt
change_impactt(const goto_modelt &model_old, const goto_modelt &model_new, impact_modet impact_mode, bool compact_output)
Definition: change_impact.cpp:290
change_impactt::new_dep_graph
dependence_grapht new_dep_graph
Definition: change_impact.cpp:226
change_impactt::ns_new
const namespacet ns_new
Definition: change_impact.cpp:221
change_impactt::NEW_CTRL_DEP
@ NEW_CTRL_DEP
Definition: change_impact.cpp:235
change_impactt::SAME
@ SAME
Definition: change_impact.cpp:230
change_impactt::old_dep_graph
dependence_grapht old_dep_graph
Definition: change_impact.cpp:225
dstringt::empty
bool empty() const
Definition: dstring.h:88
unified_difft::differencet::DELETED
@ DELETED
impact_modet::FORWARD
@ FORWARD
change_impactt::new_change_impact
goto_functions_change_impactt new_change_impact
Definition: change_impact.cpp:244
full_slicert::add_decl_dead
void add_decl_dead(const cfgt::nodet &node, queuet &queue, decl_deadt &decl_dead)
Definition: full_slicer.cpp:55
dep_edget::kindt::BOTH
@ BOTH
change_impactt::impact_mode
impact_modet impact_mode
Definition: change_impact.cpp:215
full_slicert::operator()
void operator()(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
Definition: full_slicer.cpp:255
full_slicert::add_jumps
void add_jumps(queuet &queue, jumpst &jumps, const dependence_grapht::post_dominators_mapt &post_dominators)
Definition: full_slicer.cpp:86
change_impactt::DEL_CTRL_DEP
@ DEL_CTRL_DEP
Definition: change_impact.cpp:236
cfg_baset< cfg_nodet >
goto_programt::instructions
instructionst instructions
The list of instructions in the goto program.
Definition: goto_program.h:592
dep_edget::kindt::DATA
@ DATA
goto_functionst
A collection of goto functions.
Definition: goto_functions.h:24
cfg_baset< cfg_nodet >::nodet
base_grapht::nodet nodet
Definition: cfg.h:92
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:191
unified_difft::differencet::NEW
@ NEW
change_impactt::DELETED
@ DELETED
Definition: change_impact.cpp:232
change_impactt
Definition: change_impact.cpp:203
goto_programt
A generic container class for the GOTO intermediate representation of one function.
Definition: goto_program.h:72
change_impact.h
unified_difft::get_diff
goto_program_difft get_diff(const irep_idt &function) const
Definition: unified_diff.cpp:31
change_impactt::compact_output
bool compact_output
Definition: change_impact.cpp:216
goto_programt::const_targett
instructionst::const_iterator const_targett
Definition: goto_program.h:587
full_slicert::jumpst
std::list< cfgt::entryt > jumpst
Definition: full_slicer_class.h:65
change_impactt::output_instruction
void output_instruction(char prefix, const goto_programt &goto_program, const namespacet &ns, goto_programt::const_targett &target) const
Definition: change_impact.cpp:730
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:37
implicit
static bool implicit(goto_programt::const_targett target)
Definition: full_slicer.cpp:235
dep_nodet
Definition: dependence_graph.h:58
dstringt::begin
std::string::const_iterator begin() const
Definition: dstring.h:192
change_impactt::DEL_DATA_DEP
@ DEL_DATA_DEP
Definition: change_impact.cpp:234
unified_difft::goto_program_difft
std::list< std::pair< goto_programt::const_targett, differencet > > goto_program_difft
Definition: unified_diff.h:46
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:1229
dependence_graph.h
grapht< dep_nodet >::nodet
dep_nodet nodet
Definition: graph.h:169