#include <goto2graph.h>

Collaboration diagram for instrumentert::cfg_visitort:

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 >, goto_programt::target_less_than >	incoming_post

Public Member Functions
virtual	~cfg_visitort ()

	cfg_visitort (namespacet &_ns, instrumentert &_instrumenter)

void	enter_function (const irep_idt &function_id)

void	leave_function (const irep_idt &function_id)

void	visit_cfg (value_setst &value_sets, memory_modelt model, bool no_dependencies, loop_strategyt duplicate_body, const irep_idt &function_id)

virtual void	visit_cfg_function (value_setst &value_sets, memory_modelt model, bool no_dependencies, loop_strategyt duplicate_body, const irep_idt &function_id, 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, goto_programt::target_less_than >	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 (const irep_idt &function_id, 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 (const irep_idt &function_id, const goto_programt &goto_program, 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 (const goto_programt &goto_program, goto_programt::const_targett targ, goto_programt::const_targett i_it)

void	visit_cfg_assign (value_setst &value_sets, const irep_idt &function_id, goto_programt::instructionst::iterator &i_it, bool no_dependencies)

void	visit_cfg_fence (goto_programt::instructionst::iterator i_it, const irep_idt &function_id)

void	visit_cfg_skip (goto_programt::instructionst::iterator i_it)

void	visit_cfg_lwfence (goto_programt::instructionst::iterator i_it, const irep_idt &function_id)

void	visit_cfg_asm_fence (goto_programt::instructionst::iterator i_it, const irep_idt &function_id)

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 (const irep_idt &function_id, const goto_programt &goto_program, 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

Detailed Description

Definition at line 86 of file goto2graph.h.

Member Typedef Documentation

◆ id2node_pairt

typedef std::pair<irep_idt, event_idt> instrumentert::cfg_visitort::id2node_pairt

Definition at line 181 of file goto2graph.h.

◆ id2nodet

typedef std::multimap<irep_idt, event_idt> instrumentert::cfg_visitort::id2nodet

Definition at line 180 of file goto2graph.h.

◆ incoming_post

typedef std::map< goto_programt::const_targett, std::set<nodet>, goto_programt::target_less_than> instrumentert::cfg_visitort::incoming_post

Definition at line 195 of file goto2graph.h.

◆ nodet

typedef std::pair<event_idt, event_idt> instrumentert::cfg_visitort::nodet

Definition at line 190 of file goto2graph.h.

Constructor & Destructor Documentation

◆ ~cfg_visitort()

virtual instrumentert::cfg_visitort::~cfg_visitort ( )

inlinevirtual

Definition at line 173 of file goto2graph.h.

◆ cfg_visitort()

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

inline

Definition at line 230 of file goto2graph.h.

Member Function Documentation

◆ contains_shared_array()

bool instrumentert::cfg_visitort::contains_shared_array	(	const irep_idt &	function_id,
		goto_programt::const_targett	targ,
		goto_programt::const_targett	i_it,
		value_setst &	value_sets
	)		const

protected

Definition at line 408 of file goto2graph.cpp.

◆ enter_function()

void instrumentert::cfg_visitort::enter_function ( const irep_idt & function_id )

inline

Definition at line 245 of file goto2graph.h.

◆ leave_function()

void instrumentert::cfg_visitort::leave_function ( const irep_idt & function_id )

inline

Definition at line 252 of file goto2graph.h.

◆ local()

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

inline

Definition at line 81 of file goto2graph.cpp.

◆ 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_id
	)

inline

Definition at line 257 of file goto2graph.h.

◆ visit_cfg_asm_fence()

void instrumentert::cfg_visitort::visit_cfg_asm_fence	(	goto_programt::instructionst::iterator	i_it,
		const irep_idt &	function_id
	)

protected

Definition at line 788 of file goto2graph.cpp.

◆ visit_cfg_assign()

void instrumentert::cfg_visitort::visit_cfg_assign	(	value_setst &	value_sets,
		const irep_idt &	function_id,
		goto_programt::instructionst::iterator &	i_it,
		bool	no_dependencies
	)

protected

Definition at line 841 of file goto2graph.cpp.

◆ visit_cfg_backedge()

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

inlineprotected

strategy: fwd/bwd alternation

Definition at line 583 of file goto2graph.cpp.

◆ visit_cfg_body()

void instrumentert::cfg_visitort::visit_cfg_body	(	const irep_idt &	function_id,
		const goto_programt &	goto_program,
		goto_programt::const_targett	i_it,
		loop_strategyt	replicate_body,
		value_setst &	value_sets
	)

inlineprotected

strategy: fwd/bwd alternation

Definition at line 464 of file goto2graph.cpp.

◆ visit_cfg_duplicate()

void instrumentert::cfg_visitort::visit_cfg_duplicate	(	const goto_programt &	goto_program,
		goto_programt::const_targett	targ,
		goto_programt::const_targett	i_it
	)

inlineprotected

Definition at line 517 of file goto2graph.cpp.

◆ visit_cfg_fence()

void instrumentert::cfg_visitort::visit_cfg_fence	(	goto_programt::instructionst::iterator	i_it,
		const irep_idt &	function_id
	)

protected

Definition at line 1178 of file goto2graph.cpp.

◆ 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_id,
		std::set< nodet > &	ending_vertex
	)

virtual

TODO: move the visitor outside, and inherit.

Parameters

value_sets	Value_sets and options
model	Memory model
no_dependencies	Option to disable dependency analysis
duplicate_body	Control which loop body segments should be duplicated
function_id	Function to analyse
ending_vertex	Outcoming edges

Definition at line 148 of file goto2graph.cpp.

◆ 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

Definition at line 687 of file goto2graph.cpp.

◆ visit_cfg_goto()

void instrumentert::cfg_visitort::visit_cfg_goto	(	const irep_idt &	function_id,
		const goto_programt &	goto_program,
		goto_programt::instructionst::iterator	i_it,
		loop_strategyt	replicate_body,
		value_setst &	value_sets
	)

protected

Definition at line 649 of file goto2graph.cpp.

◆ visit_cfg_lwfence()

void instrumentert::cfg_visitort::visit_cfg_lwfence	(	goto_programt::instructionst::iterator	i_it,
		const irep_idt &	function_id
	)

protected

Definition at line 749 of file goto2graph.cpp.

◆ visit_cfg_propagate()

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

inlineprotected

Definition at line 294 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 316 of file goto2graph.cpp.

◆ visit_cfg_skip()

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

protected

Definition at line 1220 of file goto2graph.cpp.

◆ visit_cfg_thread()

void instrumentert::cfg_visitort::visit_cfg_thread ( ) const

protected

Definition at line 306 of file goto2graph.cpp.

Member Data Documentation

◆ coming_from

unsigned instrumentert::cfg_visitort::coming_from

protected

Definition at line 99 of file goto2graph.h.

◆ current_thread

unsigned instrumentert::cfg_visitort::current_thread

protected

Definition at line 98 of file goto2graph.h.

◆ data_dp

data_dpt instrumentert::cfg_visitort::data_dp

Definition at line 221 of file goto2graph.h.

◆ egraph

event_grapht& instrumentert::cfg_visitort::egraph

protected

Definition at line 93 of file goto2graph.h.

◆ egraph_alt

wmm_grapht& instrumentert::cfg_visitort::egraph_alt

protected

Definition at line 95 of file goto2graph.h.

◆ egraph_SCCs

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

protected

Definition at line 94 of file goto2graph.h.

◆ fr_rf_counter

unsigned instrumentert::cfg_visitort::fr_rf_counter

Definition at line 187 of file goto2graph.h.

◆ functions_met

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

Definition at line 228 of file goto2graph.h.

◆ in_pos

incoming_post instrumentert::cfg_visitort::in_pos

Definition at line 197 of file goto2graph.h.

◆ instrumenter

instrumentert& instrumentert::cfg_visitort::instrumenter

protected

Definition at line 90 of file goto2graph.h.

◆ map_reads

id2nodet instrumentert::cfg_visitort::map_reads

Definition at line 182 of file goto2graph.h.

◆ map_writes

id2nodet instrumentert::cfg_visitort::map_writes

Definition at line 182 of file goto2graph.h.

◆ max_thread

unsigned instrumentert::cfg_visitort::max_thread

Definition at line 177 of file goto2graph.h.

◆ ns

namespacet& instrumentert::cfg_visitort::ns

protected

Definition at line 89 of file goto2graph.h.

◆ out_pos

incoming_post instrumentert::cfg_visitort::out_pos

Definition at line 202 of file goto2graph.h.

◆ read_counter

unsigned instrumentert::cfg_visitort::read_counter

Definition at line 185 of file goto2graph.h.

◆ thread

unsigned instrumentert::cfg_visitort::thread

Definition at line 218 of file goto2graph.h.

◆ unknown_read_nodes

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

Definition at line 224 of file goto2graph.h.

◆ unknown_write_nodes

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

Definition at line 225 of file goto2graph.h.

◆ updated

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

Definition at line 199 of file goto2graph.h.

◆ write_counter

unsigned instrumentert::cfg_visitort::write_counter

Definition at line 184 of file goto2graph.h.

◆ ws_counter

unsigned instrumentert::cfg_visitort::ws_counter

Definition at line 186 of file goto2graph.h.

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

/home/runner/work/cbmc/cbmc/src/goto-instrument/wmm/goto2graph.h
/home/runner/work/cbmc/cbmc/src/goto-instrument/wmm/goto2graph.cpp

Public Types

Public Member Functions

Public Attributes

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ id2node_pairt

◆ id2nodet

◆ incoming_post

◆ nodet

Constructor & Destructor Documentation

◆ ~cfg_visitort()

◆ cfg_visitort()

Member Function Documentation

◆ contains_shared_array()

◆ enter_function()

◆ leave_function()

◆ local()

◆ visit_cfg()

◆ visit_cfg_asm_fence()

◆ visit_cfg_assign()

◆ visit_cfg_backedge()

◆ visit_cfg_body()

◆ visit_cfg_duplicate()

◆ visit_cfg_fence()

◆ visit_cfg_function()

◆ visit_cfg_function_call()

◆ visit_cfg_goto()

◆ visit_cfg_lwfence()

◆ visit_cfg_propagate()

◆ visit_cfg_reference_function()

◆ visit_cfg_skip()

◆ visit_cfg_thread()

Member Data Documentation

◆ coming_from

◆ current_thread

◆ data_dp

◆ egraph

◆ egraph_alt

◆ egraph_SCCs

◆ fr_rf_counter

◆ functions_met

◆ in_pos

◆ instrumenter

◆ map_reads

◆ map_writes

◆ max_thread

◆ ns

◆ out_pos

◆ read_counter

◆ thread

◆ unknown_read_nodes

◆ unknown_write_nodes

◆ updated

◆ write_counter

◆ ws_counter