cprover
|
#include <goto2graph.h>
Public Types | |
typedef std::multimap< irep_idt, event_idt > | id2nodet |
typedef std::pair< irep_idt, event_idt > | id2node_pairt |
typedef std::pair< event_idt, event_idt > | nodet |
typedef std::map< goto_programt::const_targett, std::set< nodet > > | incoming_post |
Public Member Functions | |
virtual | ~cfg_visitort () |
cfg_visitort (namespacet &_ns, instrumentert &_instrumenter) | |
void | enter_function (const irep_idt &function) |
void | leave_function (const irep_idt &function) |
void | visit_cfg (value_setst &value_sets, memory_modelt model, bool no_dependencies, loop_strategyt duplicate_body, const irep_idt &function) |
virtual void | visit_cfg_function (value_setst &value_sets, memory_modelt model, bool no_dependencies, loop_strategyt duplicate_body, const irep_idt &function, const std::set< nodet > &initial_vertex, std::set< nodet > &ending_vertex) |
TODO: move the visitor outside, and inherit. More... | |
bool | local (const irep_idt &i) |
Public Attributes | |
unsigned | max_thread |
id2nodet | map_reads |
id2nodet | map_writes |
unsigned | write_counter |
unsigned | read_counter |
unsigned | ws_counter |
unsigned | fr_rf_counter |
incoming_post | in_pos |
std::set< goto_programt::const_targett > | updated |
incoming_post | out_pos |
unsigned | thread |
data_dpt | data_dp |
std::set< event_idt > | unknown_read_nodes |
std::set< event_idt > | unknown_write_nodes |
std::set< irep_idt > | functions_met |
Protected Member Functions | |
bool | contains_shared_array (goto_programt::const_targett targ, goto_programt::const_targett i_it, value_setst &value_sets) const |
void | visit_cfg_thread () const |
void | visit_cfg_propagate (goto_programt::instructionst::iterator i_it) |
void | visit_cfg_body (goto_programt::const_targett i_it, loop_strategyt replicate_body, value_setst &value_sets) |
strategy: fwd/bwd alternation More... | |
void | visit_cfg_backedge (goto_programt::const_targett targ, goto_programt::const_targett i_it) |
strategy: fwd/bwd alternation More... | |
void | visit_cfg_duplicate (goto_programt::const_targett targ, goto_programt::const_targett i_it) |
void | visit_cfg_assign (value_setst &value_sets, namespacet &ns, goto_programt::instructionst::iterator &i_it, bool no_dependencies) |
void | visit_cfg_fence (goto_programt::instructionst::iterator i_it) |
void | visit_cfg_skip (goto_programt::instructionst::iterator i_it) |
void | visit_cfg_lwfence (goto_programt::instructionst::iterator i_it) |
void | visit_cfg_asm_fence (goto_programt::instructionst::iterator i_it) |
void | visit_cfg_function_call (value_setst &value_sets, goto_programt::instructionst::iterator i_it, memory_modelt model, bool no_dependenciess, loop_strategyt duplicate_body) |
void | visit_cfg_goto (goto_programt::instructionst::iterator i_it, loop_strategyt replicate_body, value_setst &value_sets) |
void | visit_cfg_reference_function (irep_idt id_function) |
references the first and last edges of the function More... | |
Protected Attributes | |
namespacet & | ns |
instrumentert & | instrumenter |
event_grapht & | egraph |
std::vector< std::set< event_idt > > & | egraph_SCCs |
wmm_grapht & | egraph_alt |
unsigned | current_thread |
unsigned | coming_from |
Definition at line 90 of file goto2graph.h.
typedef std::pair<irep_idt, event_idt> instrumentert::cfg_visitort::id2node_pairt |
Definition at line 165 of file goto2graph.h.
typedef std::multimap<irep_idt, event_idt> instrumentert::cfg_visitort::id2nodet |
Definition at line 164 of file goto2graph.h.
typedef std::map<goto_programt::const_targett, std::set<nodet> > instrumentert::cfg_visitort::incoming_post |
Definition at line 176 of file goto2graph.h.
typedef std::pair<event_idt, event_idt> instrumentert::cfg_visitort::nodet |
Definition at line 174 of file goto2graph.h.
|
inlinevirtual |
Definition at line 157 of file goto2graph.h.
|
inline |
Definition at line 210 of file goto2graph.h.
References coming_from, current_thread, fr_rf_counter, max_thread, read_counter, thread, write_counter, and ws_counter.
|
protected |
Definition at line 405 of file goto2graph.cpp.
References messaget::debug(), messaget::eom(), forall_rw_set_r_entries, forall_rw_set_w_entries, source_locationt::get_line(), id2string(), messaget::mstreamt::message, instrumentert::ns, rw_set_baset::r_entries, messaget::mstreamt::source_location, and rw_set_baset::w_entries.
|
inline |
|
inline |
|
inline |
Definition at line 86 of file goto2graph.cpp.
References instrumenter, and instrumentert::local().
|
inline |
Definition at line 237 of file goto2graph.h.
References enter_function(), messaget::eom(), instrumenter, leave_function(), instrumentert::message, visit_cfg_function(), and messaget::warning().
Referenced by instrumentert::goto2graph_cfg().
|
protected |
Definition at line 757 of file goto2graph.cpp.
References grapht< N >::add_edge(), grapht< N >::add_node(), event_grapht::add_node(), event_grapht::add_po_edge(), abstract_eventt::ASMfence, instrumentert::egraph, instrumentert::egraph_alt, and messaget::eom().
|
protected |
Definition at line 797 of file goto2graph.cpp.
References event_grapht::add_com_edge(), grapht< N >::add_edge(), grapht< N >::add_node(), event_grapht::add_node(), event_grapht::add_po_edge(), messaget::debug(), instrumentert::egraph, instrumentert::egraph_alt, messaget::eom(), forall_rw_set_r_entries, forall_rw_set_w_entries, id2string(), instrumentert::local(), event_grapht::message, instrumentert::ns, abstract_eventt::Read, abstract_eventt::thread, and abstract_eventt::Write.
|
inlineprotected |
strategy: fwd/bwd alternation
Definition at line 563 of file goto2graph.cpp.
References add_all_pos, grapht< N >::add_edge(), event_grapht::add_po_back_edge(), instrumentert::egraph, instrumentert::egraph_alt, and messaget::eom().
|
inlineprotected |
strategy: fwd/bwd alternation
Definition at line 454 of file goto2graph.cpp.
References all_loops, arrays_only, and no_loop.
|
inlineprotected |
Definition at line 499 of file goto2graph.cpp.
References alt_copy_segment(), goto_function_templatet< bodyT >::body, event_grapht::copy_segment(), messaget::debug(), instrumentert::egraph, instrumentert::egraph_alt, messaget::eom(), and messaget::mstreamt::message.
|
protected |
Definition at line 1114 of file goto2graph.cpp.
References grapht< N >::add_edge(), grapht< N >::add_node(), event_grapht::add_node(), event_grapht::add_po_edge(), instrumentert::egraph, instrumentert::egraph_alt, messaget::eom(), and abstract_eventt::Fence.
|
virtual |
TODO: move the visitor outside, and inherit.
value_sets | value_sets and options |
function | function to analyse |
initial_vertex | incoming edges |
ending_vertex | outcoming edges |
Definition at line 153 of file goto2graph.cpp.
References add_all_pos, CPROVER_PREFIX, instrumentert::egraph, messaget::eom(), Forall_goto_program_instructions, is_fence(), is_lwfence(), event_grapht::map_data_dp, instrumentert::ns, and TSO.
Referenced by visit_cfg().
|
protected |
Definition at line 658 of file goto2graph.cpp.
References messaget::eom(), code_function_callt::function(), symbol_exprt::get_identifier(), to_code_function_call(), and to_symbol_expr().
|
protected |
Definition at line 629 of file goto2graph.cpp.
References messaget::eom().
|
protected |
Definition at line 725 of file goto2graph.cpp.
References grapht< N >::add_edge(), grapht< N >::add_node(), event_grapht::add_node(), event_grapht::add_po_edge(), instrumentert::egraph, instrumentert::egraph_alt, messaget::eom(), and abstract_eventt::Lwfence.
|
inlineprotected |
Definition at line 291 of file goto2graph.cpp.
|
inlineprotected |
references the first and last edges of the function
Definition at line 313 of file goto2graph.cpp.
References add_all_pos, messaget::debug(), messaget::eom(), id_function, and messaget::mstreamt::message.
|
protected |
Definition at line 1149 of file goto2graph.cpp.
|
protected |
Definition at line 303 of file goto2graph.cpp.
|
protected |
Definition at line 103 of file goto2graph.h.
Referenced by cfg_visitort().
|
protected |
Definition at line 102 of file goto2graph.h.
Referenced by cfg_visitort().
data_dpt instrumentert::cfg_visitort::data_dp |
Definition at line 201 of file goto2graph.h.
|
protected |
Definition at line 97 of file goto2graph.h.
|
protected |
Definition at line 99 of file goto2graph.h.
|
protected |
Definition at line 98 of file goto2graph.h.
unsigned instrumentert::cfg_visitort::fr_rf_counter |
Definition at line 171 of file goto2graph.h.
Referenced by cfg_visitort(), and instrumentert::goto2graph_cfg().
std::set<irep_idt> instrumentert::cfg_visitort::functions_met |
Definition at line 208 of file goto2graph.h.
Referenced by enter_function(), and leave_function().
incoming_post instrumentert::cfg_visitort::in_pos |
Definition at line 178 of file goto2graph.h.
|
protected |
Definition at line 94 of file goto2graph.h.
Referenced by local(), and visit_cfg().
id2nodet instrumentert::cfg_visitort::map_reads |
Definition at line 166 of file goto2graph.h.
id2nodet instrumentert::cfg_visitort::map_writes |
Definition at line 166 of file goto2graph.h.
unsigned instrumentert::cfg_visitort::max_thread |
Definition at line 161 of file goto2graph.h.
Referenced by cfg_visitort(), and instrumentert::goto2graph_cfg().
|
protected |
Definition at line 93 of file goto2graph.h.
incoming_post instrumentert::cfg_visitort::out_pos |
Definition at line 182 of file goto2graph.h.
unsigned instrumentert::cfg_visitort::read_counter |
Definition at line 169 of file goto2graph.h.
Referenced by cfg_visitort(), and instrumentert::goto2graph_cfg().
unsigned instrumentert::cfg_visitort::thread |
Definition at line 198 of file goto2graph.h.
Referenced by cfg_visitort().
std::set<event_idt> instrumentert::cfg_visitort::unknown_read_nodes |
Definition at line 204 of file goto2graph.h.
std::set<event_idt> instrumentert::cfg_visitort::unknown_write_nodes |
Definition at line 205 of file goto2graph.h.
std::set<goto_programt::const_targett> instrumentert::cfg_visitort::updated |
Definition at line 179 of file goto2graph.h.
unsigned instrumentert::cfg_visitort::write_counter |
Definition at line 168 of file goto2graph.h.
Referenced by cfg_visitort(), and instrumentert::goto2graph_cfg().
unsigned instrumentert::cfg_visitort::ws_counter |
Definition at line 170 of file goto2graph.h.
Referenced by cfg_visitort(), and instrumentert::goto2graph_cfg().