#include <goto2graph.h>

Inheritance diagram for instrumentert:

Collaboration diagram for instrumentert:

Classes
class	cfg_visitort

Public Types
typedef std::map< irep_idt, std::pair< std::set< event_idt >, std::set< event_idt > > >	map_function_nodest

Public Member Functions
void	print_map_function_graph () const

	instrumentert (goto_modelt &_goto_model, messaget &_message)

unsigned	goto2graph_cfg (value_setst &value_sets, memory_modelt model, bool no_dependencies, loop_strategyt duplicate_body)
	goes through CFG and build a static abstract event graph overapproximating the read/write relations for any executions More...

void	collect_cycles (memory_modelt model)

void	collect_cycles_by_SCCs (memory_modelt model)
	Note: can be distributed (#define DISTRIBUTED) More...

void	cfg_cycles_filter ()

void	set_parameters_collection (unsigned _max_var=0, unsigned _max_po_trans=0, bool _ignore_arrays=false)

void	instrument_with_strategy (instrumentation_strategyt strategy)

void	instrument_my_events (const std::set< event_idt > &events)

void	set_rendering_options (bool aligned, bool file, bool function)

void	print_outputs (memory_modelt model, bool hide_internals)

Static Public Member Functions
static std::set< event_idt >	extract_my_events ()

Public Attributes
namespacet	ns

messaget &	message

event_grapht	egraph

std::vector< std::set< event_idt > >	egraph_SCCs

std::set< event_grapht::critical_cyclet >	set_of_cycles

std::vector< std::set< event_grapht::critical_cyclet > >	set_of_cycles_per_SCC

unsigned	num_sccs

map_function_nodest	map_function_graph

std::set< irep_idt >	var_to_instr

std::multimap< irep_idt, source_locationt >	id2loc

std::multimap< irep_idt, source_locationt >	id2cycloc

Protected Types
typedef std::set< event_grapht::critical_cyclet >	set_of_cyclest

typedef std::set< goto_programt::instructiont::targett >	target_sett

Protected Member Functions
bool	local (const irep_idt &id)
	is local variable? More...

void	add_instr_to_interleaving (goto_programt::instructionst::iterator it, goto_programt &interleaving)

bool	is_cfg_spurious (const event_grapht::critical_cyclet &cyc)

unsigned	cost (const event_grapht::critical_cyclet::delayt &e)
	cost function More...

void	instrument_all_inserter (const set_of_cyclest &set)

void	instrument_one_event_per_cycle_inserter (const set_of_cyclest &set)

void	instrument_one_read_per_cycle_inserter (const set_of_cyclest &set)

void	instrument_one_write_per_cycle_inserter (const set_of_cyclest &set)

void	instrument_minimum_interference_inserter (const set_of_cyclest &set)

void	instrument_my_events_inserter (const set_of_cyclest &set, const std::set< event_idt > &events)

void	print_outputs_local (const std::set< event_grapht::critical_cyclet > &set, std::ofstream &dot, std::ofstream &ref, std::ofstream &output, std::ofstream &all, std::ofstream &table, memory_modelt model, bool hide_internals)

Protected Attributes
goto_functionst &	goto_functions

std::map< event_idt, event_idt >	map_vertex_gnode

wmm_grapht	egraph_alt

unsigned	unique_id

bool	render_po_aligned

bool	render_by_file

bool	render_by_function

Detailed Description

Definition at line 29 of file goto2graph.h.

Member Typedef Documentation

◆ map_function_nodest

typedef std::map<irep_idt, std::pair<std::set<event_idt>, std::set<event_idt> > > instrumentert::map_function_nodest

Definition at line 324 of file goto2graph.h.

◆ set_of_cyclest

typedef std::set<event_grapht::critical_cyclet> instrumentert::set_of_cyclest

protected

Definition at line 60 of file goto2graph.h.

◆ target_sett

typedef std::set<goto_programt::instructiont::targett> instrumentert::target_sett

protected

Definition at line 84 of file goto2graph.h.

Constructor & Destructor Documentation

◆ instrumentert()

instrumentert::instrumentert	(	goto_modelt &	_goto_model,
		messaget &	_message
	)

inline

Definition at line 357 of file goto2graph.h.

Member Function Documentation

◆ add_instr_to_interleaving()

void instrumentert::add_instr_to_interleaving	(	goto_programt::instructionst::iterator	it,
		goto_programt &	interleaving
	)

inlineprotected

Definition at line 1226 of file goto2graph.cpp.

◆ cfg_cycles_filter()

void instrumentert::cfg_cycles_filter ( )

Definition at line 1400 of file goto2graph.cpp.

◆ collect_cycles()

void instrumentert::collect_cycles ( memory_modelt model )

inline

Definition at line 381 of file goto2graph.h.

◆ collect_cycles_by_SCCs()

void instrumentert::collect_cycles_by_SCCs ( memory_modelt model )

Note: can be distributed (#define DISTRIBUTED)

Definition at line 1608 of file goto2graph.cpp.

◆ cost()

unsigned instrumentert::cost ( const event_grapht::critical_cyclet::delayt & e )

inlineprotected

cost function

Definition at line 177 of file instrumenter_strategies.cpp.

◆ extract_my_events()

std::set< event_idt > instrumentert::extract_my_events ( )

static

Definition at line 404 of file instrumenter_strategies.cpp.

◆ goto2graph_cfg()

unsigned instrumentert::goto2graph_cfg	(	value_setst &	value_sets,
		memory_modelt	model,
		bool	no_dependencies,
		loop_strategyt	duplicate_body
	)

goes through CFG and build a static abstract event graph overapproximating the read/write relations for any executions

Definition at line 88 of file goto2graph.cpp.

◆ instrument_all_inserter()

void instrumentert::instrument_all_inserter ( const set_of_cyclest & set )

inlineprotected

Definition at line 82 of file instrumenter_strategies.cpp.

◆ instrument_minimum_interference_inserter()

void instrumentert::instrument_minimum_interference_inserter ( const set_of_cyclest & set )

inlineprotected

Definition at line 192 of file instrumenter_strategies.cpp.

◆ instrument_my_events()

void instrumentert::instrument_my_events ( const std::set< event_idt > & events )

Definition at line 386 of file instrumenter_strategies.cpp.

◆ instrument_my_events_inserter()

void instrumentert::instrument_my_events_inserter	(	const set_of_cyclest &	set,
		const std::set< event_idt > &	events
	)

inlineprotected

Definition at line 354 of file instrumenter_strategies.cpp.

◆ instrument_one_event_per_cycle_inserter()

void instrumentert::instrument_one_event_per_cycle_inserter ( const set_of_cyclest & set )

inlineprotected

Definition at line 111 of file instrumenter_strategies.cpp.

◆ instrument_one_read_per_cycle_inserter()

void instrumentert::instrument_one_read_per_cycle_inserter ( const set_of_cyclest & set )

inlineprotected

Definition at line 162 of file instrumenter_strategies.cpp.

◆ instrument_one_write_per_cycle_inserter()

void instrumentert::instrument_one_write_per_cycle_inserter ( const set_of_cyclest & set )

inlineprotected

Definition at line 169 of file instrumenter_strategies.cpp.

◆ instrument_with_strategy()

void instrumentert::instrument_with_strategy ( instrumentation_strategyt strategy )

Definition at line 23 of file instrumenter_strategies.cpp.

◆ is_cfg_spurious()

bool instrumentert::is_cfg_spurious ( const event_grapht::critical_cyclet & cyc )

protected

Definition at line 1253 of file goto2graph.cpp.

◆ local()

bool instrumentert::local ( const irep_idt & id )

inlineprotected

is local variable?

Definition at line 33 of file goto2graph.cpp.

◆ print_map_function_graph()

void instrumentert::print_map_function_graph ( ) const

inline

Definition at line 327 of file goto2graph.h.

◆ print_outputs()

void instrumentert::print_outputs	(	memory_modelt	model,
		bool	hide_internals
	)

Definition at line 1553 of file goto2graph.cpp.

◆ print_outputs_local()

void instrumentert::print_outputs_local	(	const std::set< event_grapht::critical_cyclet > &	set,
		std::ofstream &	dot,
		std::ofstream &	ref,
		std::ofstream &	output,
		std::ofstream &	all,
		std::ofstream &	table,
		memory_modelt	model,
		bool	hide_internals
	)

inlineprotected

Definition at line 1447 of file goto2graph.cpp.

◆ set_parameters_collection()

void instrumentert::set_parameters_collection	(	unsigned	_max_var = `0`,
		unsigned	_max_po_trans = `0`,
		bool	_ignore_arrays = `false`
	)

inline

Definition at line 394 of file goto2graph.h.

◆ set_rendering_options()

void instrumentert::set_rendering_options	(	bool	aligned,
		bool	file,
		bool	function
	)

inline

Definition at line 414 of file goto2graph.h.

Member Data Documentation

◆ egraph

event_grapht instrumentert::egraph

Definition at line 309 of file goto2graph.h.

◆ egraph_alt

wmm_grapht instrumentert::egraph_alt

protected

Definition at line 40 of file goto2graph.h.

◆ egraph_SCCs

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

Definition at line 312 of file goto2graph.h.

◆ goto_functions

goto_functionst& instrumentert::goto_functions

protected

Definition at line 36 of file goto2graph.h.

◆ id2cycloc

std::multimap<irep_idt, source_locationt> instrumentert::id2cycloc

Definition at line 355 of file goto2graph.h.

◆ id2loc

std::multimap<irep_idt, source_locationt> instrumentert::id2loc

Definition at line 354 of file goto2graph.h.

◆ map_function_graph

map_function_nodest instrumentert::map_function_graph

Definition at line 325 of file goto2graph.h.

◆ map_vertex_gnode

std::map<event_idt, event_idt> instrumentert::map_vertex_gnode

protected

Definition at line 39 of file goto2graph.h.

◆ message

messaget& instrumentert::message

Definition at line 306 of file goto2graph.h.

◆ ns

namespacet instrumentert::ns

Definition at line 33 of file goto2graph.h.

◆ num_sccs

unsigned instrumentert::num_sccs

Definition at line 319 of file goto2graph.h.

◆ render_by_file

bool instrumentert::render_by_file

protected

Definition at line 46 of file goto2graph.h.

◆ render_by_function

bool instrumentert::render_by_function

protected

Definition at line 47 of file goto2graph.h.

◆ render_po_aligned

bool instrumentert::render_po_aligned

protected

Definition at line 45 of file goto2graph.h.

◆ set_of_cycles

std::set<event_grapht::critical_cyclet> instrumentert::set_of_cycles

Definition at line 315 of file goto2graph.h.

◆ set_of_cycles_per_SCC

std::vector<std::set<event_grapht::critical_cyclet> > instrumentert::set_of_cycles_per_SCC

Definition at line 318 of file goto2graph.h.

◆ unique_id

unsigned instrumentert::unique_id

protected

Definition at line 42 of file goto2graph.h.

◆ var_to_instr

std::set<irep_idt> instrumentert::var_to_instr

Definition at line 353 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
/home/runner/work/cbmc/cbmc/src/goto-instrument/wmm/instrumenter_strategies.cpp

Classes

Public Types

Public Member Functions

Static Public Member Functions

Public Attributes

Protected Types

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ map_function_nodest

◆ set_of_cyclest

◆ target_sett

Constructor & Destructor Documentation

◆ instrumentert()

Member Function Documentation

◆ add_instr_to_interleaving()

◆ cfg_cycles_filter()

◆ collect_cycles()

◆ collect_cycles_by_SCCs()

◆ cost()

◆ extract_my_events()

◆ goto2graph_cfg()

◆ instrument_all_inserter()

◆ instrument_minimum_interference_inserter()

◆ instrument_my_events()

◆ instrument_my_events_inserter()

◆ instrument_one_event_per_cycle_inserter()

◆ instrument_one_read_per_cycle_inserter()

◆ instrument_one_write_per_cycle_inserter()

◆ instrument_with_strategy()

◆ is_cfg_spurious()

◆ local()

◆ print_map_function_graph()

◆ print_outputs()

◆ print_outputs_local()

◆ set_parameters_collection()

◆ set_rendering_options()

Member Data Documentation

◆ egraph

◆ egraph_alt

◆ egraph_SCCs

◆ goto_functions

◆ id2cycloc

◆ id2loc

◆ map_function_graph

◆ map_vertex_gnode

◆ message

◆ ns

◆ num_sccs

◆ render_by_file

◆ render_by_function

◆ render_po_aligned

◆ set_of_cycles

◆ set_of_cycles_per_SCC

◆ unique_id

◆ var_to_instr