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);
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);
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())
82 const auto &s=instruction->decl_symbol();
83 decl_dead[s.get_identifier()].push(instruction_node_index);
85 else if(instruction->is_dead())
87 const auto &s=instruction->dead_symbol();
88 decl_dead[s.get_identifier()].push(instruction_node_index);
94 dep_graph(goto_functions, ns);
97 fixedpoint(goto_functions, queue, jumps, decl_dead, dep_graph);
104 if(gf_entry.second.body_available())
109 if(!i_it->is_end_function() &&
112 #ifdef DEBUG_FULL_SLICERT
117 for(std::set<unsigned>::const_iterator
118 req_it=node.required_by.begin();
119 req_it!=node.required_by.end();
122 if(req_it!=node.required_by.begin())
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());
149 for(
unsigned i=0; i<dep_graph.
size(); ++i)
155 while(!queue.empty())
157 while(!queue.empty())
164 if(node.node_required)
168 node.node_required=
true;
187 const cfgt::nodet &node,
190 const dep_node_to_cfgt &dep_node_to_cfg)
193 dep_graph[dep_graph[node.PC].get_node_id()];
195 for(dependence_grapht::edgest::const_iterator
196 it=d_node.
in.begin();
199 add_to_queue(queue, dep_node_to_cfg[it->first], node.PC);
241 map<goto_programt::const_targett, unsigned, goto_programt::target_less_than>
243 typedef std::map<irep_idt, goto_program_change_impactt>
296 bool _compact_output,
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)
326 goto_functionst::function_mapt::const_iterator old_fit =
328 goto_functionst::function_mapt::const_iterator new_fit =
336 old_fit->second.body;
340 new_fit->second.body;
364 for(
const auto &d : diff)
371 old_impact[o_it]|=
SAME;
373 INVARIANT(n_it == d.first,
"start of hunk");
374 new_impact[n_it]|=
SAME;
379 INVARIANT(o_it == d.first,
"start of hunk");
398 INVARIANT(n_it == d.first,
"start of hunk");
416 new_impact[n_it]|=
NEW;
430 for(dependence_grapht::edgest::const_iterator it = d_node.out.begin();
431 it != d_node.out.end(); ++it)
449 dep_graph[dep_graph[src].get_node_id()],
463 for(dependence_grapht::edgest::const_iterator it = d_node.in.begin();
464 it != d_node.in.end(); ++it)
485 dep_graph[dep_graph[src].get_node_id()],
496 goto_functionst::function_mapt::const_iterator>
499 function_mapt old_funcs, new_funcs;
505 old_funcs.insert(std::make_pair(it->first, it));
511 new_funcs.insert(std::make_pair(it->first, it));
514 function_mapt::const_iterator ito=old_funcs.
begin();
515 for(function_mapt::const_iterator itn=new_funcs.begin();
516 itn!=new_funcs.end();
519 while(ito!=old_funcs.end() && ito->first<itn->first)
522 if(ito!=old_funcs.end() && itn->first==ito->first)
530 goto_functions_change_impactt::const_iterator oc_it=
532 for(goto_functions_change_impactt::const_iterator
554 INVARIANT(oc_it->first == nc_it->first,
"same instruction");
576 goto_functionst::function_mapt::const_iterator f_it =
582 std::cout <<
"/** " << function_id <<
" **/\n";
586 goto_program_change_impactt::const_iterator c_entry=
588 const unsigned mod_flags =
589 c_entry == c_i.end() ?
static_cast<unsigned>(
SAME) : c_entry->second;
598 else if(mod_flags&
NEW)
624 goto_functionst::function_mapt::const_iterator o_f_it =
629 goto_functionst::function_mapt::const_iterator f_it =
635 std::cout <<
"/** " << function_id <<
" **/\n";
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)
655 goto_program_change_impactt::const_iterator c_entry=
657 const unsigned mod_flags =
658 c_entry == n_c_i.end() ?
static_cast<unsigned>(
SAME) : c_entry->second;
665 if(old_mod_flags==
SAME)
678 else if(mod_flags&
NEW)
687 "expected kind of flag");
697 "expected kind of flag");
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)
718 if(old_mod_flags==
SAME)
722 else if(old_mod_flags&
NEW)
745 const irep_idt &file = target->source_location().get_file();
746 const irep_idt &line = target->source_location().get_line();
748 std::cout << prefix <<
" " <<
id2string(file)
754 target->output(std::cout);
766 model_old, model_new, impact_mode, compact_output, message_handler);
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.
base_grapht::node_indext entryt
const entry_mapt & entries() const
Get a map from program points to their corresponding node indices.
entryt get_node_index(const goto_programt::const_targett &program_point) const
Get the graph node index for program_point.
nodet & get_node(const goto_programt::const_targett &program_point)
Get the CFG graph node relating to program_point.
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
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 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.
std::string::const_iterator begin() const
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 instructions
The list of instructions in the goto program.
instructionst::const_iterator const_targett
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
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)
#define forall_goto_program_instructions(it, program)
#define Forall_goto_program_instructions(it, program)
const std::string & id2string(const irep_idt &d)
void remove_skip(goto_programt &goto_program, goto_programt::targett begin, goto_programt::targett end)
remove unnecessary skip statements
#define CHECK_RETURN(CONDITION)
#define UNREACHABLE
This should be used to mark dead code.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Unified diff (using LCSS) of goto functions.