cprover
instrumentert::cfg_visitort Class Reference

#include <goto2graph.h>

Collaboration diagram for instrumentert::cfg_visitort:
[legend]

Public Types

typedef std::multimap< irep_idt, event_idtid2nodet
 
typedef std::pair< irep_idt, event_idtid2node_pairt
 
typedef std::pair< event_idt, event_idtnodet
 
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_targettupdated
 
incoming_post out_pos
 
unsigned thread
 
data_dpt data_dp
 
std::set< event_idtunknown_read_nodes
 
std::set< event_idtunknown_write_nodes
 
std::set< irep_idtfunctions_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

namespacetns
 
instrumentertinstrumenter
 
event_graphtegraph
 
std::vector< std::set< event_idt > > & egraph_SCCs
 
wmm_graphtegraph_alt
 
unsigned current_thread
 
unsigned coming_from
 

Detailed Description

Definition at line 90 of file goto2graph.h.

Member Typedef Documentation

§ id2node_pairt

Definition at line 165 of file goto2graph.h.

§ id2nodet

Definition at line 164 of file goto2graph.h.

§ incoming_post

Definition at line 176 of file goto2graph.h.

§ nodet

Definition at line 174 of file goto2graph.h.

Constructor & Destructor Documentation

§ ~cfg_visitort()

virtual instrumentert::cfg_visitort::~cfg_visitort ( )
inlinevirtual

Definition at line 157 of file goto2graph.h.

§ cfg_visitort()

instrumentert::cfg_visitort::cfg_visitort ( namespacet _ns,
instrumentert _instrumenter 
)
inline

Definition at line 210 of file goto2graph.h.

Member Function Documentation

§ contains_shared_array()

§ enter_function()

void instrumentert::cfg_visitort::enter_function ( const irep_idt function)
inline

Definition at line 225 of file goto2graph.h.

Referenced by visit_cfg().

§ leave_function()

void instrumentert::cfg_visitort::leave_function ( const irep_idt function)
inline

Definition at line 232 of file goto2graph.h.

Referenced by visit_cfg().

§ local()

bool instrumentert::cfg_visitort::local ( const irep_idt i)
inline

Definition at line 86 of file goto2graph.cpp.

Referenced by visit_cfg().

§ visit_cfg()

void instrumentert::cfg_visitort::visit_cfg ( value_setst value_sets,
memory_modelt  model,
bool  no_dependencies,
loop_strategyt  duplicate_body,
const irep_idt function 
)
inline

§ visit_cfg_asm_fence()

void instrumentert::cfg_visitort::visit_cfg_asm_fence ( goto_programt::instructionst::iterator  i_it)
protected

§ visit_cfg_assign()

§ visit_cfg_backedge()

void instrumentert::cfg_visitort::visit_cfg_backedge ( goto_programt::const_targett  targ,
goto_programt::const_targett  i_it 
)
inlineprotected

§ visit_cfg_body()

void instrumentert::cfg_visitort::visit_cfg_body ( goto_programt::const_targett  i_it,
loop_strategyt  replicate_body,
value_setst value_sets 
)
inlineprotected

strategy: fwd/bwd alternation

Definition at line 454 of file goto2graph.cpp.

References all_loops, arrays_only, and no_loop.

§ visit_cfg_duplicate()

§ visit_cfg_fence()

void instrumentert::cfg_visitort::visit_cfg_fence ( goto_programt::instructionst::iterator  i_it)
protected

§ visit_cfg_function()

void instrumentert::cfg_visitort::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 
)
virtual

TODO: move the visitor outside, and inherit.

Parameters
value_setsvalue_sets and options
functionfunction to analyse
initial_vertexincoming edges
ending_vertexoutcoming 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().

§ visit_cfg_function_call()

void instrumentert::cfg_visitort::visit_cfg_function_call ( value_setst value_sets,
goto_programt::instructionst::iterator  i_it,
memory_modelt  model,
bool  no_dependenciess,
loop_strategyt  duplicate_body 
)
protected

§ visit_cfg_goto()

void instrumentert::cfg_visitort::visit_cfg_goto ( goto_programt::instructionst::iterator  i_it,
loop_strategyt  replicate_body,
value_setst value_sets 
)
protected

Definition at line 629 of file goto2graph.cpp.

References messaget::eom().

§ visit_cfg_lwfence()

void instrumentert::cfg_visitort::visit_cfg_lwfence ( goto_programt::instructionst::iterator  i_it)
protected

§ visit_cfg_propagate()

void instrumentert::cfg_visitort::visit_cfg_propagate ( goto_programt::instructionst::iterator  i_it)
inlineprotected

Definition at line 291 of file goto2graph.cpp.

§ visit_cfg_reference_function()

void instrumentert::cfg_visitort::visit_cfg_reference_function ( irep_idt  id_function)
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.

§ visit_cfg_skip()

void instrumentert::cfg_visitort::visit_cfg_skip ( goto_programt::instructionst::iterator  i_it)
protected

Definition at line 1149 of file goto2graph.cpp.

§ visit_cfg_thread()

void instrumentert::cfg_visitort::visit_cfg_thread ( ) const
protected

Definition at line 303 of file goto2graph.cpp.

Member Data Documentation

§ coming_from

unsigned instrumentert::cfg_visitort::coming_from
protected

Definition at line 103 of file goto2graph.h.

§ current_thread

unsigned instrumentert::cfg_visitort::current_thread
protected

Definition at line 102 of file goto2graph.h.

§ data_dp

data_dpt instrumentert::cfg_visitort::data_dp

Definition at line 201 of file goto2graph.h.

§ egraph

event_grapht& instrumentert::cfg_visitort::egraph
protected

Definition at line 97 of file goto2graph.h.

§ egraph_alt

wmm_grapht& instrumentert::cfg_visitort::egraph_alt
protected

Definition at line 99 of file goto2graph.h.

§ egraph_SCCs

std::vector<std::set<event_idt> >& instrumentert::cfg_visitort::egraph_SCCs
protected

Definition at line 98 of file goto2graph.h.

§ fr_rf_counter

unsigned instrumentert::cfg_visitort::fr_rf_counter

Definition at line 171 of file goto2graph.h.

Referenced by instrumentert::goto2graph_cfg().

§ functions_met

std::set<irep_idt> instrumentert::cfg_visitort::functions_met

Definition at line 208 of file goto2graph.h.

§ in_pos

incoming_post instrumentert::cfg_visitort::in_pos

Definition at line 178 of file goto2graph.h.

§ instrumenter

instrumentert& instrumentert::cfg_visitort::instrumenter
protected

Definition at line 94 of file goto2graph.h.

§ map_reads

id2nodet instrumentert::cfg_visitort::map_reads

Definition at line 166 of file goto2graph.h.

§ map_writes

id2nodet instrumentert::cfg_visitort::map_writes

Definition at line 166 of file goto2graph.h.

§ max_thread

unsigned instrumentert::cfg_visitort::max_thread

Definition at line 161 of file goto2graph.h.

Referenced by instrumentert::goto2graph_cfg().

§ ns

namespacet& instrumentert::cfg_visitort::ns
protected

Definition at line 93 of file goto2graph.h.

§ out_pos

incoming_post instrumentert::cfg_visitort::out_pos

Definition at line 182 of file goto2graph.h.

§ read_counter

unsigned instrumentert::cfg_visitort::read_counter

Definition at line 169 of file goto2graph.h.

Referenced by instrumentert::goto2graph_cfg().

§ thread

unsigned instrumentert::cfg_visitort::thread

Definition at line 198 of file goto2graph.h.

§ unknown_read_nodes

std::set<event_idt> instrumentert::cfg_visitort::unknown_read_nodes

Definition at line 204 of file goto2graph.h.

§ unknown_write_nodes

std::set<event_idt> instrumentert::cfg_visitort::unknown_write_nodes

Definition at line 205 of file goto2graph.h.

§ updated

std::set<goto_programt::const_targett> instrumentert::cfg_visitort::updated

Definition at line 179 of file goto2graph.h.

§ write_counter

unsigned instrumentert::cfg_visitort::write_counter

Definition at line 168 of file goto2graph.h.

Referenced by instrumentert::goto2graph_cfg().

§ ws_counter

unsigned instrumentert::cfg_visitort::ws_counter

Definition at line 170 of file goto2graph.h.

Referenced by instrumentert::goto2graph_cfg().


The documentation for this class was generated from the following files: