27 cfg_nodet():node_required(false)
32 #ifdef DEBUG_FULL_SLICERT 33 std::set<unsigned> required_by;
40 typedef std::vector<cfgt::entryt> dep_node_to_cfgt;
41 typedef std::stack<cfgt::entryt> queuet;
43 inline void add_to_queue(
45 const cfgt::entryt &entry,
48 #ifdef DEBUG_FULL_SLICERT 49 cfg[entry].required_by.insert(reason->location_number);
69 for(cfgt::entry_mapt::iterator
70 e_it=cfg.entry_map.begin();
71 e_it!=cfg.entry_map.end();
74 if(criterion(e_it->first))
75 add_to_queue(queue, e_it->second, e_it->first);
77 add_to_queue(queue, e_it->second, e_it->first);
78 else if((e_it->first->is_goto() && e_it->first->guard.is_true()) ||
79 e_it->first->is_throw())
80 jumps.push_back(e_it->second);
81 else if(e_it->first->is_decl())
86 else if(e_it->first->is_dead())
95 dep_graph(goto_functions, ns);
98 fixedpoint(goto_functions, queue, jumps, decl_dead, dep_graph);
104 if(f_it->second.body_available())
108 const cfgt::entryt &e=cfg.entry_map[i_it];
109 if(!i_it->is_end_function() &&
110 !cfg[e].node_required)
112 #ifdef DEBUG_FULL_SLICERT 115 std::string c=
"ins:"+std::to_string(i_it->location_number);
117 for(std::set<unsigned>::const_iterator
118 req_it=cfg[e].required_by.begin();
119 req_it!=cfg[e].required_by.end();
122 if(req_it!=cfg[e].required_by.begin())
124 c+=std::to_string(*req_it);
126 i_it->source_location.set_column(c);
127 i_it->source_location.set_comment(c);
143 decl_deadt &decl_dead,
146 std::vector<cfgt::entryt> dep_node_to_cfg;
147 dep_node_to_cfg.reserve(dep_graph.
size());
148 for(
unsigned i=0; i<dep_graph.
size(); ++i)
150 cfgt::entry_mapt::const_iterator entry=
151 cfg.entry_map.find(dep_graph[i].PC);
152 assert(entry!=cfg.entry_map.end());
154 dep_node_to_cfg.push_back(entry->second);
158 while(!queue.empty())
160 while(!queue.empty())
162 cfgt::entryt e=queue.top();
163 cfgt::nodet &node=cfg[e];
167 if(node.node_required)
171 node.node_required=
true;
174 add_dependencies(node, queue, dep_graph, dep_node_to_cfg);
177 add_function_calls(node, queue, goto_functions);
180 add_decl_dead(node, queue, decl_dead);
190 const cfgt::nodet &node,
193 const dep_node_to_cfgt &dep_node_to_cfg)
196 dep_graph[dep_graph[node.PC].get_node_id()];
198 for(dependence_grapht::edgest::const_iterator
199 it=d_node.
in.begin();
202 add_to_queue(queue, dep_node_to_cfg[it->first], node.PC);
213 bool compact_output);
242 typedef std::map<goto_programt::const_targett, unsigned>
244 typedef std::map<irep_idt, goto_program_change_impactt>
258 void propogate_dep_back(
263 void propogate_dep_forward(
269 void output_change_impact(
274 void output_change_impact(
283 void output_instruction(
char prefix,
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)
324 goto_functionst::function_mapt::const_iterator old_fit=
326 goto_functionst::function_mapt::const_iterator new_fit=
334 old_fit->second.body;
338 new_fit->second.body;
360 for(
const auto &d : diff)
367 old_impact[o_it]|=
SAME;
369 assert(n_it==d.first);
370 new_impact[n_it]|=
SAME;
375 assert(o_it==d.first);
400 assert(n_it==d.first);
420 new_impact[n_it]|=
NEW;
434 for(dependence_grapht::edgest::const_iterator it = d_node.out.begin();
435 it != d_node.out.end(); ++it)
442 if((change_impact[src->function][src] &data_flag)
443 || (change_impact[src->function][src] &ctrl_flag))
447 change_impact[src->function][src] |= data_flag;
449 change_impact[src->function][src] |= ctrl_flag;
461 for(dependence_grapht::edgest::const_iterator it = d_node.in.begin();
462 it != d_node.in.end(); ++it)
469 if((change_impact[src->function][src] &data_flag)
470 || (change_impact[src->function][src] &ctrl_flag))
476 change_impact[src->function][src] |= data_flag;
478 change_impact[src->function][src] |= ctrl_flag;
489 goto_functionst::function_mapt::const_iterator>
492 function_mapt old_funcs, new_funcs;
495 old_funcs.insert(std::make_pair(it->first, it));
497 new_funcs.insert(std::make_pair(it->first, it));
499 function_mapt::const_iterator ito=old_funcs.begin();
500 for(function_mapt::const_iterator itn=new_funcs.begin();
501 itn!=new_funcs.end();
504 while(ito!=old_funcs.end() && ito->first<itn->first)
507 if(ito!=old_funcs.end() && itn->first==ito->first)
515 goto_functions_change_impactt::const_iterator oc_it=
517 for(goto_functions_change_impactt::const_iterator
539 assert(oc_it->first==nc_it->first);
561 goto_functionst::function_mapt::const_iterator f_it=
567 std::cout <<
"/** " <<
function <<
" **/\n";
571 goto_program_change_impactt::const_iterator c_entry=
573 const unsigned mod_flags=
574 c_entry==c_i.end() ?
SAME : c_entry->second;
583 else if(mod_flags&
NEW)
609 goto_functionst::function_mapt::const_iterator o_f_it=
614 goto_functionst::function_mapt::const_iterator f_it=
620 std::cout <<
"/** " <<
function <<
" **/\n";
623 old_goto_program.instructions.begin();
626 goto_program_change_impactt::const_iterator o_c_entry=
627 o_c_i.find(o_target);
628 const unsigned old_mod_flags=
629 o_c_entry==o_c_i.end() ?
SAME : o_c_entry->second;
639 goto_program_change_impactt::const_iterator c_entry=
641 const unsigned mod_flags=
642 c_entry==n_c_i.end() ?
SAME : c_entry->second;
649 if(old_mod_flags==
SAME)
660 else if(mod_flags&DELETED)
662 else if(mod_flags&
NEW)
668 assert(old_mod_flags==
SAME ||
677 assert(old_mod_flags==
SAME ||
688 o_target!=old_goto_program.instructions.end();
691 goto_program_change_impactt::const_iterator o_c_entry=
692 o_c_i.find(o_target);
693 const unsigned old_mod_flags=
694 o_c_entry==o_c_i.end() ?
SAME : o_c_entry->second;
699 if(old_mod_flags==
SAME)
703 else if(old_mod_flags&
NEW)
726 const irep_idt &
file=target->source_location.get_file();
727 const irep_idt &line=target->source_location.get_line();
729 std::cout << prefix <<
" " <<
id2string(file)
745 change_impactt c(model_old, model_new, impact_mode, compact_output);
const code_declt & to_code_decl(const codet &code)
void add_dependencies(const cfgt::nodet &node, queuet &queue, const dependence_grapht &dep_graph, const dep_node_to_cfgt &dep_node_to_cfg)
const std::string & id2string(const irep_idt &d)
void output_change_impact(const irep_idt &function, const goto_program_change_impactt &c_i, const goto_functionst &goto_functions, const namespacet &ns) const
const code_deadt & to_code_dead(const codet &code)
Field-Sensitive Program Dependence Analysis, Litvak et al., FSE 2010.
instructionst instructions
The list of instructions in the goto program.
const irep_idt & get_identifier() const
Data and control-dependencies of syntactic diff.
static bool implicit(goto_programt::const_targett target)
void change_impact(const irep_idt &function)
std::map< goto_programt::const_targett, unsigned > goto_program_change_impactt
void propogate_dep_back(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
instructionst::const_iterator const_targett
dependence_grapht old_dep_graph
void propogate_dep_forward(const dependence_grapht::nodet &d_node, const dependence_grapht &dep_graph, goto_functions_change_impactt &change_impact, bool del)
void fixedpoint(goto_functionst &goto_functions, queuet &queue, jumpst &jumps, decl_deadt &decl_dead, const dependence_grapht &dep_graph)
const post_dominators_mapt & cfg_post_dominators() const
change_impactt(const goto_modelt &model_old, const goto_modelt &model_new, impact_modet impact_mode, bool compact_output)
const goto_functionst & old_goto_functions
function_mapt function_map
goto_functions_change_impactt new_change_impact
Unified diff (using LCSS) of goto functions.
A specialization of goto_program_templatet over goto programs in which instructions have codet type...
void remove_skip(goto_programt &goto_program)
remove unnecessary skip statements
void output_instruction(char prefix, const goto_programt &goto_program, const namespacet &ns, const irep_idt &function, goto_programt::const_targett &target) const
dependence_grapht new_dep_graph
Base class for all expressions.
const symbol_exprt & to_symbol_expr(const exprt &expr)
Cast a generic exprt to a symbol_exprt.
#define Forall_goto_functions(it, functions)
#define Forall_goto_program_instructions(it, program)
std::map< irep_idt, goto_program_change_impactt > goto_functions_change_impactt
std::list< std::pair< goto_programt::const_targett, differencet > > goto_program_difft
void get_diff(const irep_idt &function, goto_program_difft &dest) const
void operator()(goto_functionst &goto_functions, const namespacet &ns, slicing_criteriont &criterion)
#define forall_goto_functions(it, functions)
std::ostream & output_instruction(const class namespacet &ns, const irep_idt &identifier, std::ostream &out, instructionst::const_iterator it) const
See below.
#define forall_goto_program_instructions(it, program)
void change_impact(const goto_modelt &model_old, const goto_modelt &model_new, impact_modet impact_mode, bool compact_output)
unified_difft unified_diff
goto_functions_change_impactt old_change_impact