The interface of the target container for symbolic execution to record its symbolic steps into. More...

#include <symex_target.h>

Inheritance diagram for symex_targett:

Classes
struct	sourcet
	Identifies source in the context of symbolic execution. More...

Public Types
enum	assignment_typet { assignment_typet::STATE, assignment_typet::HIDDEN, assignment_typet::VISIBLE_ACTUAL_PARAMETER, assignment_typet::HIDDEN_ACTUAL_PARAMETER, assignment_typet::PHI, assignment_typet::GUARD }

Public Member Functions
	symex_targett ()

virtual	~symex_targett ()

virtual void	shared_read (const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)=0
	Read from a shared variable `ssa_object` (which is both the left- and the right–hand side of assignment): we effectively assign the value stored in `ssa_object` by another thread to `ssa_object` in the memory scope of this thread. More...

virtual void	shared_write (const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)=0
	Write to a shared variable `ssa_object:` we effectively assign a value from this thread to be visible by other threads. More...

virtual void	assignment (const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &ssa_full_lhs, const exprt &original_full_lhs, const exprt &ssa_rhs, const sourcet &source, assignment_typet assignment_type)=0
	Write to a local variable. More...

virtual void	decl (const exprt &guard, const ssa_exprt &ssa_lhs, const exprt &initializer, const sourcet &source, assignment_typet assignment_type)=0
	Declare a fresh variable. More...

virtual void	dead (const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source)=0
	Remove a variable from the scope. More...

virtual void	function_call (const exprt &guard, const irep_idt &function_id, const std::vector< renamedt< exprt, L2 >> &ssa_function_arguments, const sourcet &source, bool hidden)=0
	Record a function call. More...

virtual void	function_return (const exprt &guard, const irep_idt &function_id, const sourcet &source, bool hidden)=0
	Record return from a function. More...

virtual void	location (const exprt &guard, const sourcet &source)=0
	Record a location. More...

virtual void	output (const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< renamedt< exprt, L2 >> &args)=0
	Record an output. More...

virtual void	output_fmt (const exprt &guard, const sourcet &source, const irep_idt &output_id, const irep_idt &fmt, const std::list< exprt > &args)=0
	Record formatted output. More...

virtual void	input (const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)=0
	Record an input. More...

virtual void	assumption (const exprt &guard, const exprt &cond, const sourcet &source)=0
	Record an assumption. More...

virtual void	assertion (const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)=0
	Record an assertion. More...

virtual void	goto_instruction (const exprt &guard, const renamedt< exprt, L2 > &cond, const sourcet &source)=0
	Record a goto instruction. More...

virtual void	constraint (const exprt &cond, const std::string &msg, const sourcet &source)=0
	Record a global constraint: there is no guard limiting its scope. More...

virtual void	spawn (const exprt &guard, const sourcet &source)=0
	Record spawning a new thread. More...

virtual void	memory_barrier (const exprt &guard, const sourcet &source)=0
	Record creating a memory barrier. More...

virtual void	atomic_begin (const exprt &guard, unsigned atomic_section_id, const sourcet &source)=0
	Record a beginning of an atomic section. More...

virtual void	atomic_end (const exprt &guard, unsigned atomic_section_id, const sourcet &source)=0
	Record ending an atomic section. More...

Detailed Description

The interface of the target container for symbolic execution to record its symbolic steps into.

Presently, symex_target_equationt is the only implementation of this interface.

Definition at line 24 of file symex_target.h.

Member Enumeration Documentation

◆ assignment_typet

enum symex_targett::assignment_typet

strong

Enumerator
STATE
HIDDEN
VISIBLE_ACTUAL_PARAMETER
HIDDEN_ACTUAL_PARAMETER
PHI
GUARD

Definition at line 68 of file symex_target.h.

Constructor & Destructor Documentation

◆ symex_targett()

symex_targett::symex_targett ( )

inline

Definition at line 27 of file symex_target.h.

◆ ~symex_targett()

virtual symex_targett::~symex_targett ( )

inlinevirtual

Definition at line 31 of file symex_target.h.

Member Function Documentation

◆ assertion()

virtual void symex_targett::assertion	(	const exprt &	guard,
		const exprt &	cond,
		const std::string &	msg,
		const sourcet &	source
	)

pure virtual

Record an assertion.

Parameters

guard	Precondition for reaching this assertion
cond	Condition this assertion represents
msg	The message associated with this assertion
source	Pointer to location in the input GOTO program of this assertion

Implemented in symex_target_equationt.

◆ assignment()

virtual void symex_targett::assignment	(	const exprt &	guard,
		const ssa_exprt &	ssa_lhs,
		const exprt &	ssa_full_lhs,
		const exprt &	original_full_lhs,
		const exprt &	ssa_rhs,
		const sourcet &	source,
		assignment_typet	assignment_type
	)

pure virtual

Write to a local variable.

The cond_expr is lhs==rhs.

Parameters

guard	Precondition for this read event
ssa_lhs	Variable to be written to, must be a symbol (and not nil)
ssa_full_lhs	Full left-hand side with symex level annotations
original_full_lhs	Full left-hand side without symex level annotations
ssa_rhs	Right-hand side of the assignment
source	Pointer to location in the input GOTO program of this assignment
assignment_type	To distinguish between different types of assignments (some may be hidden for the further analysis)

Implemented in symex_target_equationt.

◆ assumption()

virtual void symex_targett::assumption	(	const exprt &	guard,
		const exprt &	cond,
		const sourcet &	source
	)

pure virtual

Record an assumption.

Parameters

guard	Precondition for reaching this assumption
cond	Condition this assumption represents
source	Pointer to location in the input GOTO program of this assumption

Implemented in symex_target_equationt.

◆ atomic_begin()

virtual void symex_targett::atomic_begin	(	const exprt &	guard,
		unsigned	atomic_section_id,
		const sourcet &	source
	)

pure virtual

Record a beginning of an atomic section.

Parameters

guard	Precondition for reaching this atomic section
atomic_section_id	Identifier for this atomic section
source	Pointer to location in the input GOTO program where an atomic section begins

Implemented in symex_target_equationt.

◆ atomic_end()

virtual void symex_targett::atomic_end	(	const exprt &	guard,
		unsigned	atomic_section_id,
		const sourcet &	source
	)

pure virtual

Record ending an atomic section.

Parameters

guard	Precondition for reaching the end of this atomic section
atomic_section_id	Identifier for this atomic section
source	Pointer to location in the input GOTO program where an atomic section ends

Implemented in symex_target_equationt.

◆ constraint()

virtual void symex_targett::constraint	(	const exprt &	cond,
		const std::string &	msg,
		const sourcet &	source
	)

pure virtual

Record a global constraint: there is no guard limiting its scope.

Parameters

cond	Condition represented by this constraint
msg	The message associated with this constraint
source	Pointer to location in the input GOTO program of this constraint

Implemented in symex_target_equationt.

◆ dead()

virtual void symex_targett::dead	(	const exprt &	guard,
		const ssa_exprt &	ssa_lhs,
		const sourcet &	source
	)

pure virtual

Remove a variable from the scope.

Parameters

guard	Precondition for removal of this variable
ssa_lhs	Variable to be removed, must be symbol
source	Pointer to location in the input GOTO program of this removal

Implemented in symex_target_equationt.

◆ decl()

virtual void symex_targett::decl	(	const exprt &	guard,
		const ssa_exprt &	ssa_lhs,
		const exprt &	initializer,
		const sourcet &	source,
		assignment_typet	assignment_type
	)

pure virtual

Declare a fresh variable.

The cond_expr is lhs==lhs.

Parameters

guard	Precondition for a declaration of this variable
ssa_lhs	Variable to be declared, must be symbol (and not nil)
initializer	Initial value
source	Pointer to location in the input GOTO program of this declaration
assignment_type	To distinguish between different types of assignments (some may be hidden for the further analysis)

Implemented in symex_target_equationt.

◆ function_call()

virtual void symex_targett::function_call	(	const exprt &	guard,
		const irep_idt &	function_id,
		const std::vector< renamedt< exprt, L2 >> &	ssa_function_arguments,
		const sourcet &	source,
		bool	hidden
	)

pure virtual

Record a function call.

Parameters

guard	Precondition for calling a function
function_id	Name of the function
ssa_function_arguments	Vector of arguments in SSA form
source	To location in the input GOTO program of this
hidden	Should this step be recorded as hidden? function call

Implemented in symex_target_equationt.

◆ function_return()

virtual void symex_targett::function_return	(	const exprt &	guard,
		const irep_idt &	function_id,
		const sourcet &	source,
		bool	hidden
	)

pure virtual

Record return from a function.

Parameters

guard	Precondition for returning from a function
function_id	Name of the function from which we return
source	Pointer to location in the input GOTO program of this
hidden	Should this step be recorded as hidden? function return

Implemented in symex_target_equationt.

◆ goto_instruction()

virtual void symex_targett::goto_instruction	(	const exprt &	guard,
		const renamedt< exprt, L2 > &	cond,
		const sourcet &	source
	)

pure virtual

Record a goto instruction.

Parameters

guard	Precondition for reaching this goto instruction
cond	Condition under which this goto should be taken
source	Pointer to location in the input GOTO program of this goto instruction

Implemented in symex_target_equationt.

◆ input()

virtual void symex_targett::input	(	const exprt &	guard,
		const sourcet &	source,
		const irep_idt &	input_id,
		const std::list< exprt > &	args
	)

pure virtual

Record an input.

Parameters

guard	Precondition for reading from the input
source	Pointer to location in the input GOTO program of this input
input_id	Name of the input
args	A list of IO arguments

Implemented in symex_target_equationt.

◆ location()

virtual void symex_targett::location	(	const exprt &	guard,
		const sourcet &	source
	)

pure virtual

Record a location.

Parameters

guard	Precondition for reaching this location
source	Pointer to location in the input GOTO program to be recorded

Implemented in symex_target_equationt.

◆ memory_barrier()

virtual void symex_targett::memory_barrier	(	const exprt &	guard,
		const sourcet &	source
	)

pure virtual

Record creating a memory barrier.

Parameters

guard	Precondition for reaching this barrier
source	Pointer to location in the input GOTO program where a new barrier is created

Implemented in symex_target_equationt.

◆ output()

virtual void symex_targett::output	(	const exprt &	guard,
		const sourcet &	source,
		const irep_idt &	output_id,
		const std::list< renamedt< exprt, L2 >> &	args
	)

pure virtual

Record an output.

Parameters

guard	Precondition for writing to the output
source	Pointer to location in the input GOTO program of this output
output_id	Name of the output
args	A list of IO arguments

Implemented in symex_target_equationt.

◆ output_fmt()

virtual void symex_targett::output_fmt	(	const exprt &	guard,
		const sourcet &	source,
		const irep_idt &	output_id,
		const irep_idt &	fmt,
		const std::list< exprt > &	args
	)

pure virtual

Record formatted output.

Parameters

guard	Precondition for writing to the output
source	Pointer to location in the input GOTO program of this output
output_id	Name of the output
fmt	Formatting string
args	A list of IO arguments

Implemented in symex_target_equationt.

◆ shared_read()

virtual void symex_targett::shared_read	(	const exprt &	guard,
		const ssa_exprt &	ssa_object,
		unsigned	atomic_section_id,
		const sourcet &	source
	)

pure virtual

Read from a shared variable ssa_object (which is both the left- and the right–hand side of assignment): we effectively assign the value stored in ssa_object by another thread to ssa_object in the memory scope of this thread.

Parameters

guard	Precondition for this read event
ssa_object	Variable to be read from
atomic_section_id	ID of the atomic section in which this read takes place (if any)
source	Pointer to location in the input GOTO program of this read

Implemented in symex_target_equationt.

◆ shared_write()

virtual void symex_targett::shared_write	(	const exprt &	guard,
		const ssa_exprt &	ssa_object,
		unsigned	atomic_section_id,
		const sourcet &	source
	)

pure virtual

Write to a shared variable ssa_object: we effectively assign a value from this thread to be visible by other threads.

Parameters

guard	Precondition for this write event
ssa_object	Variable to be written to
atomic_section_id	ID of the atomic section in which this write takes place (if any)
source	Pointer to location in the input GOTO program of this write

Implemented in symex_target_equationt.

◆ spawn()

virtual void symex_targett::spawn	(	const exprt &	guard,
		const sourcet &	source
	)

pure virtual

Record spawning a new thread.

Parameters

guard	Precondition for reaching spawning a new thread
source	Pointer to location in the input GOTO program where a new thread is to be spawned

Implemented in symex_target_equationt.

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

/home/runner/work/cbmc-documentation/cbmc-documentation/src/goto-symex/symex_target.h

Classes

Public Types

Public Member Functions

Detailed Description

Member Enumeration Documentation

◆ assignment_typet

Constructor & Destructor Documentation

◆ symex_targett()

◆ ~symex_targett()

Member Function Documentation

◆ assertion()

◆ assignment()

◆ assumption()

◆ atomic_begin()

◆ atomic_end()

◆ constraint()

◆ dead()

◆ decl()

◆ function_call()

◆ function_return()

◆ goto_instruction()

◆ input()

◆ location()

◆ memory_barrier()

◆ output()

◆ output_fmt()

◆ shared_read()

◆ shared_write()

◆ spawn()