cprover
Loading...
Searching...
No Matches
change_impact.cpp
Go to the documentation of this file.
1/*******************************************************************\
2
3Module: Data and control-dependencies of syntactic diff
4
5Author: Michael Tautschnig
6
7Date: 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,
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
66 // declarations or dead instructions may be necessary as well
68
69 for(const auto &entry : cfg.entries())
70 {
71 const auto &instruction = instruction_and_index.first;
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())
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)
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 {
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,
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 {
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
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,
190 const dep_node_to_cfgt &dep_node_to_cfg)
191{
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{
205public:
207 const goto_modelt &model_old,
208 const goto_modelt &model_new,
210 bool compact_output);
211
212 void operator()();
213
214protected:
217
222
224
227
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,
255
257 const irep_idt &function_id,
261 bool del);
263 const irep_idt &function_id,
267 bool del);
268
270 const irep_idt &function_id,
272 const goto_functionst &goto_functions,
273 const namespacet &ns) const;
275 const irep_idt &function_id,
278 const namespacet &o_ns,
281 const namespacet &n_ns) const;
282
284 char prefix,
285 const goto_programt &goto_program,
286 const namespacet &ns,
287 const irep_idt &function_id,
288 goto_programt::const_targett &target) const;
289};
290
292 const goto_modelt &model_old,
293 const goto_modelt &model_new,
295 bool _compact_output):
296 impact_mode(_impact_mode),
297 compact_output(_compact_output),
298 old_goto_functions(model_old.goto_functions),
299 ns_old(model_old.symbol_table),
300 new_goto_functions(model_new.goto_functions),
301 ns_new(model_new.symbol_table),
302 unified_diff(model_old, model_new),
303 old_dep_graph(ns_old),
304 new_dep_graph(ns_new)
305{
306 // syntactic difference?
307 if(!unified_diff())
308 return;
309
310 // compute program dependence graph of old code
312
313 // compute program dependence graph of new code
315}
316
318{
320
321 if(diff.empty())
322 return;
323
324 goto_functionst::function_mapt::const_iterator old_fit =
325 old_goto_functions.function_map.find(function_id);
326 goto_functionst::function_mapt::const_iterator new_fit =
327 new_goto_functions.function_map.find(function_id);
328
329 goto_programt empty;
330
333 empty :
334 old_fit->second.body;
337 empty :
338 new_fit->second.body;
339
341 function_id,
344 diff,
345 old_change_impact[function_id],
346 new_change_impact[function_id]);
347}
348
350 const irep_idt &function_id,
356{
358 old_goto_program.instructions.begin();
360 new_goto_program.instructions.begin();
361
362 for(const auto &d : diff)
363 {
364 switch(d.second)
365 {
367 assert(o_it!=old_goto_program.instructions.end());
368 assert(n_it!=new_goto_program.instructions.end());
370 ++o_it;
371 assert(n_it==d.first);
373 ++n_it;
374 break;
376 assert(o_it!=old_goto_program.instructions.end());
377 assert(o_it==d.first);
378 {
380 old_dep_graph[old_dep_graph[o_it].get_node_id()];
381
385 function_id, d_node, old_dep_graph, old_change_impact, true);
389 function_id, d_node, old_dep_graph, old_change_impact, true);
390 }
392 ++o_it;
393 break;
395 assert(n_it!=new_goto_program.instructions.end());
396 assert(n_it==d.first);
397 {
399 new_dep_graph[new_dep_graph[n_it].get_node_id()];
400
403 {
405 function_id, d_node, new_dep_graph, new_change_impact, false);
406 }
409 {
411 function_id, d_node, new_dep_graph, new_change_impact, false);
412 }
413 }
415 ++n_it;
416 break;
417 }
418 }
419}
420
422 const irep_idt &function_id,
426 bool del)
427{
428 for(dependence_grapht::edgest::const_iterator it = d_node.out.begin();
429 it != d_node.out.end(); ++it)
430 {
431 goto_programt::const_targett src = dep_graph[it->first].PC;
432
435
436 if(
437 (change_impact[function_id][src] & data_flag) ||
438 (change_impact[function_id][src] & ctrl_flag))
439 continue;
440 if(it->second.get() == dep_edget::kindt::DATA
441 || it->second.get() == dep_edget::kindt::BOTH)
442 change_impact[function_id][src] |= data_flag;
443 else
444 change_impact[function_id][src] |= ctrl_flag;
446 function_id,
447 dep_graph[dep_graph[src].get_node_id()],
448 dep_graph,
450 del);
451 }
452}
453
455 const irep_idt &function_id,
459 bool del)
460{
461 for(dependence_grapht::edgest::const_iterator it = d_node.in.begin();
462 it != d_node.in.end(); ++it)
463 {
464 goto_programt::const_targett src = dep_graph[it->first].PC;
465
468
469 if(
470 (change_impact[function_id][src] & data_flag) ||
471 (change_impact[function_id][src] & ctrl_flag))
472 {
473 continue;
474 }
475 if(it->second.get() == dep_edget::kindt::DATA
476 || it->second.get() == dep_edget::kindt::BOTH)
477 change_impact[function_id][src] |= data_flag;
478 else
479 change_impact[function_id][src] |= ctrl_flag;
480
482 function_id,
483 dep_graph[dep_graph[src].get_node_id()],
484 dep_graph,
486 del);
487 }
488}
489
491{
492 // sorted iteration over intersection(old functions, new functions)
493 typedef std::map<irep_idt,
494 goto_functionst::function_mapt::const_iterator>
495 function_mapt;
496
497 function_mapt old_funcs, new_funcs;
498
499 for(auto it = old_goto_functions.function_map.begin();
501 ++it)
502 {
503 old_funcs.insert(std::make_pair(it->first, it));
504 }
505 for(auto it = new_goto_functions.function_map.begin();
507 ++it)
508 {
509 new_funcs.insert(std::make_pair(it->first, it));
510 }
511
512 function_mapt::const_iterator ito=old_funcs.begin();
513 for(function_mapt::const_iterator itn=new_funcs.begin();
514 itn!=new_funcs.end();
515 ++itn)
516 {
517 while(ito!=old_funcs.end() && ito->first<itn->first)
518 ++ito;
519
520 if(ito!=old_funcs.end() && itn->first==ito->first)
521 {
522 change_impact(itn->first);
523
524 ++ito;
525 }
526 }
527
528 goto_functions_change_impactt::const_iterator oc_it=
529 old_change_impact.begin();
530 for(goto_functions_change_impactt::const_iterator
531 nc_it=new_change_impact.begin();
533 ++nc_it)
534 {
535 for( ;
536 oc_it!=old_change_impact.end() && oc_it->first<nc_it->first;
537 ++oc_it)
539 oc_it->first,
540 oc_it->second,
542 ns_old);
543
544 if(oc_it==old_change_impact.end() || nc_it->first<oc_it->first)
546 nc_it->first,
547 nc_it->second,
549 ns_new);
550 else
551 {
552 assert(oc_it->first==nc_it->first);
553
555 nc_it->first,
556 oc_it->second,
558 ns_old,
559 nc_it->second,
561 ns_new);
562
563 ++oc_it;
564 }
565 }
566}
567
569 const irep_idt &function_id,
571 const goto_functionst &goto_functions,
572 const namespacet &ns) const
573{
574 goto_functionst::function_mapt::const_iterator f_it =
575 goto_functions.function_map.find(function_id);
576 assert(f_it!=goto_functions.function_map.end());
577 const goto_programt &goto_program=f_it->second.body;
578
579 if(!compact_output)
580 std::cout << "/** " << function_id << " **/\n";
581
582 forall_goto_program_instructions(target, goto_program)
583 {
584 goto_program_change_impactt::const_iterator c_entry=
585 c_i.find(target);
586 const unsigned mod_flags =
587 c_entry == c_i.end() ? static_cast<unsigned>(SAME) : c_entry->second;
588
589 char prefix = ' ';
590 // syntactic changes are preferred over data/control-dependence
591 // modifications
592 if(mod_flags==SAME)
593 prefix=' ';
594 else if(mod_flags&DELETED)
595 prefix='-';
596 else if(mod_flags&NEW)
597 prefix='+';
598 else if(mod_flags&NEW_DATA_DEP)
599 prefix='D';
600 else if(mod_flags&NEW_CTRL_DEP)
601 prefix='C';
602 else if(mod_flags&DEL_DATA_DEP)
603 prefix='d';
604 else if(mod_flags&DEL_CTRL_DEP)
605 prefix='c';
606 else
608
609 output_instruction(prefix, goto_program, ns, function_id, target);
610 }
611}
612
614 const irep_idt &function_id,
617 const namespacet &o_ns,
620 const namespacet &n_ns) const
621{
622 goto_functionst::function_mapt::const_iterator o_f_it =
623 o_goto_functions.function_map.find(function_id);
624 assert(o_f_it!=o_goto_functions.function_map.end());
625 const goto_programt &old_goto_program=o_f_it->second.body;
626
627 goto_functionst::function_mapt::const_iterator f_it =
628 n_goto_functions.function_map.find(function_id);
629 assert(f_it!=n_goto_functions.function_map.end());
630 const goto_programt &goto_program=f_it->second.body;
631
632 if(!compact_output)
633 std::cout << "/** " << function_id << " **/\n";
634
636 old_goto_program.instructions.begin();
637 forall_goto_program_instructions(target, goto_program)
638 {
639 goto_program_change_impactt::const_iterator o_c_entry=
640 o_c_i.find(o_target);
641 const unsigned old_mod_flags = o_c_entry == o_c_i.end()
642 ? static_cast<unsigned>(SAME)
643 : o_c_entry->second;
644
646 {
647 output_instruction('-', goto_program, o_ns, function_id, o_target);
648 ++o_target;
649 --target;
650 continue;
651 }
652
653 goto_program_change_impactt::const_iterator c_entry=
654 n_c_i.find(target);
655 const unsigned mod_flags =
656 c_entry == n_c_i.end() ? static_cast<unsigned>(SAME) : c_entry->second;
657
658 char prefix = ' ';
659 // syntactic changes are preferred over data/control-dependence
660 // modifications
661 if(mod_flags==SAME)
662 {
664 prefix=' ';
666 prefix='d';
668 prefix='c';
669 else
671
672 ++o_target;
673 }
674 else if(mod_flags&DELETED)
676 else if(mod_flags&NEW)
677 prefix='+';
678 else if(mod_flags&NEW_DATA_DEP)
679 {
680 prefix='D';
681
685 ++o_target;
686 }
687 else if(mod_flags&NEW_CTRL_DEP)
688 {
689 prefix='C';
690
694 ++o_target;
695 }
696 else
698
699 output_instruction(prefix, goto_program, n_ns, function_id, target);
700 }
701 for( ;
702 o_target!=old_goto_program.instructions.end();
703 ++o_target)
704 {
705 goto_program_change_impactt::const_iterator o_c_entry=
706 o_c_i.find(o_target);
707 const unsigned old_mod_flags = o_c_entry == o_c_i.end()
708 ? static_cast<unsigned>(SAME)
709 : o_c_entry->second;
710
711 char prefix = ' ';
712 // syntactic changes are preferred over data/control-dependence
713 // modifications
716 else if(old_mod_flags&DELETED)
717 prefix='-';
718 else if(old_mod_flags&NEW)
721 prefix='d';
723 prefix='c';
724 else
726
727 output_instruction(prefix, goto_program, o_ns, function_id, o_target);
728 }
729}
730
732 char prefix,
733 const goto_programt &goto_program,
734 const namespacet &ns,
735 const irep_idt &function_id,
736 goto_programt::const_targett &target) const
737{
739 {
740 if(prefix == ' ')
741 return;
742 const irep_idt &file = target->source_location().get_file();
743 const irep_idt &line = target->source_location().get_line();
744 if(!file.empty() && !line.empty())
745 std::cout << prefix << " " << id2string(file)
746 << " " << id2string(line) << '\n';
747 }
748 else
749 {
750 std::cout << prefix;
751 goto_program.output_instruction(ns, function_id, std::cout, *target);
752 }
753}
754
756 const goto_modelt &model_old,
757 const goto_modelt &model_new,
758 impact_modet impact_mode,
759 bool compact_output)
760{
761 change_impactt c(model_old, model_new, impact_mode, compact_output);
762 c();
763}
void change_impact(const goto_modelt &model_old, const goto_modelt &model_new, impact_modet impact_mode, bool compact_output)
Data and control-dependencies of syntactic diff.
impact_modet
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:564
base_grapht::node_indext entryt
Definition cfg.h:91
base_grapht::nodet nodet
Definition cfg.h:92
nodet & get_node(const goto_programt::const_targett &program_point)
Get the CFG graph node relating to program_point.
Definition cfg.h:245
entryt get_node_index(const goto_programt::const_targett &program_point) const
Get the graph node index for program_point.
Definition cfg.h:239
goto_functions_change_impactt old_change_impact
void output_instruction(char prefix, const goto_programt &goto_program, const namespacet &ns, const irep_idt &function_id, goto_programt::const_targett &target) const
unified_difft unified_diff
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)
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< goto_programt::const_targett, unsigned > goto_program_change_impactt
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
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Definition dstring.h:37
bool empty() const
Definition dstring.h:88
void add_function_calls(const cfgt::nodet &node, queuet &queue, const goto_functionst &goto_functions)
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)
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)
void operator()(goto_functionst &goto_functions, const namespacet &ns, const slicing_criteriont &criterion)
std::stack< cfgt::entryt > queuet
void add_jumps(queuet &queue, jumpst &jumps, const dependence_grapht::post_dominators_mapt &post_dominators)
A collection of goto functions.
function_mapt function_map
A generic container class for the GOTO intermediate representation of one function.
instructionst::const_iterator const_targett
std::ostream & output_instruction(const namespacet &ns, const irep_idt &identifier, std::ostream &out, const instructionst::value_type &instruction) const
Output a single instruction.
dep_nodet nodet
Definition graph.h:169
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Definition namespace.h:91
std::list< std::pair< goto_programt::const_targett, differencet > > goto_program_difft
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)
dstringt irep_idt
Definition irep.h:37
const std::string & id2string(const irep_idt &d)
Definition irep.h:47
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
#define UNREACHABLE
This should be used to mark dead code.
Definition invariant.h:503
Definition kdev_t.h:19
Unified diff (using LCSS) of goto functions.