CBMC
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 message_handlert &message_handler);
212
213 void operator()();
214
215protected:
218
223
225
228
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,
257
259 const irep_idt &function_id,
263 bool del);
265 const irep_idt &function_id,
269 bool del);
270
272 const irep_idt &function_id,
274 const goto_functionst &goto_functions,
275 const namespacet &ns) const;
277 const irep_idt &function_id,
280 const namespacet &o_ns,
283 const namespacet &n_ns) const;
284
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,
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
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
334 old_fit==old_goto_functions.function_map.end() ?
335 empty :
336 old_fit->second.body;
338 new_fit==new_goto_functions.function_map.end() ?
339 empty :
340 new_fit->second.body;
341
343 function_id,
346 diff,
347 old_change_impact[function_id],
348 new_change_impact[function_id]);
349}
350
352 const irep_idt &function_id,
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");
372 ++o_it;
373 INVARIANT(n_it == d.first, "start of hunk");
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 {
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 }
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 {
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 }
417 ++n_it;
418 break;
419 }
420 }
421}
422
424 const irep_idt &function_id,
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
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,
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
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();
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,
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
610
611 output_instruction(prefix, goto_program, ns, target);
612 }
613}
614
616 const irep_idt &function_id,
619 const namespacet &o_ns,
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
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 {
666 prefix=' ';
668 prefix='d';
670 prefix='c';
671 else
673
674 ++o_target;
675 }
676 else if(mod_flags&DELETED)
678 else if(mod_flags&NEW)
679 prefix='+';
680 else if(mod_flags&NEW_DATA_DEP)
681 {
682 prefix='D';
683
687 "expected kind of flag");
688 ++o_target;
689 }
690 else if(mod_flags&NEW_CTRL_DEP)
691 {
692 prefix='C';
693
697 "expected kind of flag");
698 ++o_target;
699 }
700 else
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
720 else if(old_mod_flags&DELETED)
721 prefix='-';
722 else if(old_mod_flags&NEW)
725 prefix='d';
727 prefix='c';
728 else
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{
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{
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
virtual void output(const namespacet &ns, const irep_idt &function_id, const goto_programt &goto_program, std::ostream &out) const
Output the abstract states for a single function.
Definition ai.cpp:39
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:562
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
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
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
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, message_handlert &message_handler)
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
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)
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
#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
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
Definition invariant.h:423
Unified diff (using LCSS) of goto functions.
dstringt irep_idt