#include <shared_buffers.h>

Collaboration diagram for shared_bufferst:

Classes
class	cfg_visitort

class	varst

Public Types
typedef std::map< irep_idt, varst >	var_mapt

Public Member Functions
	shared_bufferst (symbol_table_baset &_symbol_table, unsigned _nb_threads, messaget &_message)

void	set_cav11 (memory_modelt model)

const varst &	operator() (const irep_idt &object)
	instruments the variable

void	add_initialization_code (goto_functionst &goto_functions)

void	delay_read (goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &read_object, const irep_idt &write_object)
	delays a read (POWER)

void	flush_read (goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &write_object)
	flushes read (POWER)

void	write (goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &object, goto_programt::instructiont &original_instruction, const unsigned current_thread)
	instruments write

void	det_flush (goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &object, const unsigned current_thread)
	flush buffers (instruments fence)

void	nondet_flush (const irep_idt &function_id, goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &object, const unsigned current_thread, const bool tso_pso_rmo)
	instruments read

void	assignment (goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &id_lhs, const exprt &rhs)
	add an assignment in the goto-program

void	assignment (goto_programt &goto_program, goto_programt::targett &t, const source_locationt &source_location, const irep_idt &id_lhs, const irep_idt &id_rhs)

bool	track (const irep_idt &id) const

irep_idt	choice (const irep_idt &function_id, const std::string &suffix)

bool	is_buffered (const namespacet &, const symbol_exprt &, bool is_write)

bool	is_buffered_in_general (const symbol_exprt &, bool is_write)

void	weak_memory (value_setst &value_sets, symbol_table_baset &symbol_table, goto_programt &goto_program, memory_modelt model, goto_functionst &goto_functions)

void	affected_by_delay (value_setst &value_sets, goto_functionst &goto_functions)
	analysis over the goto-program which computes in affected_by_delay_set the variables (non necessarily shared themselves) whose value could be changed as effect of a read delay

Public Attributes
var_mapt	var_map

std::set< irep_idt >	cycles

std::multimap< irep_idt, source_locationt >	cycles_loc

std::multimap< irep_idt, source_locationt >	cycles_r_loc

std::set< irep_idt >	affected_by_delay_set

Protected Member Functions
std::string	unique ()
	returns a unique id (for fresh variables)

irep_idt	add (const symbolt &object, const std::string &suffix, const typet &type, bool added_as_instrumentation)
	add a new var for instrumenting the input var

irep_idt	add (const symbolt &object, const std::string &suffix, const typet &type)

irep_idt	add_fresh_var (const symbolt &object, const std::string &suffix, const typet &type)

void	add_initialization (goto_programt &goto_program)

Protected Attributes
class symbol_table_baset &	symbol_table

unsigned	nb_threads

std::set< irep_idt >	instrumentations

unsigned	uniq

bool	cav11

messaget &	message

Detailed Description

Definition at line 28 of file shared_buffers.h.

Member Typedef Documentation

◆ var_mapt

typedef std::map<irep_idt, varst> shared_bufferst::var_mapt

Definition at line 78 of file shared_buffers.h.

Constructor & Destructor Documentation

◆ shared_bufferst()

shared_bufferst::shared_bufferst	(	symbol_table_baset &	_symbol_table,
		unsigned	_nb_threads,
		messaget &	_message
	)

inline

Definition at line 31 of file shared_buffers.h.

Member Function Documentation

◆ add() [1/2]

irep_idt shared_bufferst::add	(	const symbolt &	object,
		const std::string &	suffix,
		const typet &	type
	)

inlineprotected

Definition at line 255 of file shared_buffers.h.

◆ add() [2/2]

irep_idt shared_bufferst::add	(	const symbolt &	object,
		const std::string &	suffix,
		const typet &	type,
		bool	instrument
	)

protected

add a new var for instrumenting the input var

parameters: var, suffix, type of the var, added as an instrumentation

Returns: identifier of the new var

Definition at line 72 of file shared_buffers.cpp.

◆ add_fresh_var()

irep_idt shared_bufferst::add_fresh_var	(	const symbolt &	object,
		const std::string &	suffix,
		const typet &	type
	)

inlineprotected

Definition at line 261 of file shared_buffers.h.

◆ add_initialization()

void shared_bufferst::add_initialization ( goto_programt & goto_program )

protected

Definition at line 96 of file shared_buffers.cpp.

◆ add_initialization_code()

void shared_bufferst::add_initialization_code ( goto_functionst & goto_functions )

Definition at line 125 of file shared_buffers.cpp.

◆ affected_by_delay()

void shared_bufferst::affected_by_delay	(	value_setst &	value_sets,
		goto_functionst &	goto_functions
	)

analysis over the goto-program which computes in affected_by_delay_set the variables (non necessarily shared themselves) whose value could be changed as effect of a read delay

Definition at line 1006 of file shared_buffers.cpp.

◆ assignment() [1/2]

void shared_bufferst::assignment	(	goto_programt &	goto_program,
		goto_programt::targett &	t,
		const source_locationt &	source_location,
		const irep_idt &	id_lhs,
		const exprt &	rhs
	)

add an assignment in the goto-program

Definition at line 140 of file shared_buffers.cpp.

◆ assignment() [2/2]

void shared_bufferst::assignment	(	goto_programt &	goto_program,
		goto_programt::targett &	t,
		const source_locationt &	source_location,
		const irep_idt &	id_lhs,
		const irep_idt &	id_rhs
	)

inline

Definition at line 137 of file shared_buffers.h.

◆ choice()

irep_idt shared_bufferst::choice	(	const irep_idt &	function_id,
		const std::string &	suffix
	)

inline

Definition at line 162 of file shared_buffers.h.

◆ delay_read()

void shared_bufferst::delay_read	(	goto_programt &	goto_program,
		goto_programt::targett &	t,
		const source_locationt &	source_location,
		const irep_idt &	read_object,
		const irep_idt &	write_object
	)

delays a read (POWER)

Definition at line 176 of file shared_buffers.cpp.

◆ det_flush()

void shared_bufferst::det_flush	(	goto_programt &	goto_program,
		goto_programt::targett &	t,
		const source_locationt &	source_location,
		const irep_idt &	object,
		const unsigned	current_thread
	)

flush buffers (instruments fence)

Definition at line 327 of file shared_buffers.cpp.

◆ flush_read()

void shared_bufferst::flush_read	(	goto_programt &	goto_program,
		goto_programt::targett &	t,
		const source_locationt &	source_location,
		const irep_idt &	write_object
	)

flushes read (POWER)

Definition at line 225 of file shared_buffers.cpp.

◆ is_buffered()

bool shared_bufferst::is_buffered	(	const namespacet &	ns,
		const symbol_exprt &	symbol_expr,
		bool	is_write
	)

Definition at line 932 of file shared_buffers.cpp.

◆ is_buffered_in_general()

bool shared_bufferst::is_buffered_in_general	(	const symbol_exprt &	symbol_expr,
		bool	is_write
	)

Definition at line 964 of file shared_buffers.cpp.

◆ nondet_flush()

void shared_bufferst::nondet_flush	(	const irep_idt &	function_id,
		goto_programt &	goto_program,
		goto_programt::targett &	t,
		const source_locationt &	source_location,
		const irep_idt &	object,
		const unsigned	current_thread,
		const bool	tso_pso_rmo
	)

instruments read

Definition at line 433 of file shared_buffers.cpp.

◆ operator()()

const shared_bufferst::varst & shared_bufferst::operator() ( const irep_idt & object )

instruments the variable

Definition at line 31 of file shared_buffers.cpp.

◆ set_cav11()

void shared_bufferst::set_cav11 ( memory_modelt model )

inline

Definition at line 43 of file shared_buffers.h.

◆ track()

bool shared_bufferst::track ( const irep_idt & id ) const

inline

Definition at line 149 of file shared_buffers.h.

◆ unique()

std::string shared_bufferst::unique ( void )

protected

returns a unique id (for fresh variables)

Definition at line 24 of file shared_buffers.cpp.

◆ weak_memory()

void shared_bufferst::weak_memory	(	value_setst &	value_sets,
		symbol_table_baset &	symbol_table,
		goto_programt &	goto_program,
		memory_modelt	model,
		goto_functionst &	goto_functions
	)

◆ write()

void shared_bufferst::write	(	goto_programt &	goto_program,
		goto_programt::targett &	t,
		const source_locationt &	source_location,
		const irep_idt &	object,
		goto_programt::instructiont &	original_instruction,
		const unsigned	current_thread
	)

instruments write

Definition at line 265 of file shared_buffers.cpp.

Member Data Documentation

◆ affected_by_delay_set

std::set<irep_idt> shared_bufferst::affected_by_delay_set

Definition at line 235 of file shared_buffers.h.

◆ cav11

bool shared_bufferst::cav11

protected

Definition at line 243 of file shared_buffers.h.

◆ cycles

std::set<irep_idt> shared_bufferst::cycles

Definition at line 83 of file shared_buffers.h.

◆ cycles_loc

std::multimap<irep_idt, source_locationt> shared_bufferst::cycles_loc

Definition at line 85 of file shared_buffers.h.

◆ cycles_r_loc

std::multimap<irep_idt, source_locationt> shared_bufferst::cycles_r_loc

Definition at line 87 of file shared_buffers.h.

◆ instrumentations

std::set<irep_idt> shared_bufferst::instrumentations

protected

Definition at line 231 of file shared_buffers.h.

◆ message

messaget& shared_bufferst::message

protected

Definition at line 246 of file shared_buffers.h.

◆ nb_threads

unsigned shared_bufferst::nb_threads

protected

Definition at line 228 of file shared_buffers.h.

◆ symbol_table

class symbol_table_baset& shared_bufferst::symbol_table

protected

Definition at line 225 of file shared_buffers.h.

◆ uniq

unsigned shared_bufferst::uniq

protected

Definition at line 239 of file shared_buffers.h.

◆ var_map

var_mapt shared_bufferst::var_map

Definition at line 79 of file shared_buffers.h.

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

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

Classes

Public Types

Public Member Functions

Public Attributes

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ var_mapt

Constructor & Destructor Documentation

◆ shared_bufferst()

Member Function Documentation

◆ add() [1/2]

◆ add() [2/2]

◆ add_fresh_var()

◆ add_initialization()

◆ add_initialization_code()

◆ affected_by_delay()

◆ assignment() [1/2]

◆ assignment() [2/2]

◆ choice()

◆ delay_read()

◆ det_flush()

◆ flush_read()

◆ is_buffered()

◆ is_buffered_in_general()

◆ nondet_flush()

◆ operator()()

◆ set_cav11()

◆ track()

◆ unique()

◆ weak_memory()

◆ write()

Member Data Documentation

◆ affected_by_delay_set

◆ cav11

◆ cycles

◆ cycles_loc

◆ cycles_r_loc

◆ instrumentations

◆ message

◆ nb_threads

◆ symbol_table

◆ uniq

◆ var_map