Inheriting the interface of symex_targett this class represents the SSA form of the input program as a list of SSA_stept. More...

#include <symex_target_equation.h>

Inheritance diagram for symex_target_equationt:

Collaboration diagram for symex_target_equationt:

Public Types
typedef std::list< SSA_stept >	SSA_stepst

Public Types inherited from symex_targett
enum class	assignment_typet { STATE , HIDDEN , VISIBLE_ACTUAL_PARAMETER , HIDDEN_ACTUAL_PARAMETER , PHI , GUARD }

Public Member Functions
	symex_target_equationt (message_handlert &message_handler)

virtual	~symex_target_equationt ()=default

virtual void	shared_read (const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source)
	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)
	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)
	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)
	Declare a fresh variable. More...

virtual void	dead (const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source)
	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)
	Record a function call. More...

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

virtual void	location (const exprt &guard, const sourcet &source)
	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)
	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)
	Record formatted output. More...

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

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

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

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

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

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

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

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

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

void	convert (decision_proceduret &decision_procedure)
	Interface method to initiate the conversion into a decision procedure format. More...

void	convert_without_assertions (decision_proceduret &decision_procedure)
	Interface method to initiate the conversion into a decision procedure format. More...

void	convert_assignments (decision_proceduret &decision_procedure)
	Converts assignments: set the equality lhs==rhs to True. More...

void	convert_decls (decision_proceduret &decision_procedure)
	Converts declarations: these are effectively ignored by the decision procedure. More...

void	convert_assumptions (decision_proceduret &decision_procedure)
	Converts assumptions: convert the expression the assumption represents. More...

void	convert_assertions (decision_proceduret &decision_procedure, bool optimized_for_single_assertions=true)
	Converts assertions: build a disjunction of negated assertions. More...

void	convert_constraints (decision_proceduret &decision_procedure)
	Converts constraints: set the represented condition to True. More...

void	convert_goto_instructions (decision_proceduret &decision_procedure)
	Converts goto instructions: convert the expression representing the condition of this goto. More...

void	convert_guards (decision_proceduret &decision_procedure)
	Converts guards: convert the expression the guard represents. More...

void	convert_function_calls (decision_proceduret &decision_procedure)
	Converts function calls: for each argument build an equality between its symbol and the argument itself. More...

void	convert_io (decision_proceduret &decision_procedure)
	Converts I/O: for each argument build an equality between its symbol and the argument itself. More...

exprt	make_expression () const

std::size_t	count_assertions () const

std::size_t	count_ignored_SSA_steps () const

SSA_stepst::iterator	get_SSA_step (std::size_t s)

void	output (std::ostream &out) const

void	clear ()

bool	has_threads () const

void	validate (const namespacet &ns, const validation_modet vm) const

Public Member Functions inherited from symex_targett
	symex_targett ()

virtual	~symex_targett ()

Public Attributes
SSA_stepst	SSA_steps

Protected Member Functions
void	merge_ireps (SSA_stept &SSA_step)
	Merging causes identical ireps to be shared. More...

Protected Attributes
messaget	log

merge_irept	merge_irep

std::size_t	io_count = 0

std::size_t	argument_count = 0

Detailed Description

Inheriting the interface of symex_targett this class represents the SSA form of the input program as a list of SSA_stept.

It further extends the base class by providing a conversion interface for decision procedures.

Definition at line 33 of file symex_target_equation.h.

Member Typedef Documentation

◆ SSA_stepst

typedef std::list<SSA_stept> symex_target_equationt::SSA_stepst

Definition at line 250 of file symex_target_equation.h.

Constructor & Destructor Documentation

◆ symex_target_equationt()

symex_target_equationt::symex_target_equationt ( message_handlert & message_handler )

inlineexplicit

Definition at line 36 of file symex_target_equation.h.

◆ ~symex_target_equationt()

virtual symex_target_equationt::~symex_target_equationt ( )

virtualdefault

Member Function Documentation

◆ assertion()

void symex_target_equationt::assertion	(	const exprt &	guard,
		const exprt &	cond,
		const irep_idt &	property_id,
		const std::string &	msg,
		const sourcet &	source
	)

virtual

Record an assertion.

Parameters

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

Implements symex_targett.

Definition at line 282 of file symex_target_equation.cpp.

◆ assignment()

void symex_target_equationt::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
	)

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)

Implements symex_targett.

Definition at line 113 of file symex_target_equation.cpp.

◆ assumption()

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

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

Implements symex_targett.

Definition at line 268 of file symex_target_equation.cpp.

◆ atomic_begin()

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

virtual

Record a beginning of an atomic section.

start 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

Implements symex_targett.

Definition at line 86 of file symex_target_equation.cpp.

◆ atomic_end()

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

virtual

Record ending an atomic section.

end 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

Implements symex_targett.

Definition at line 100 of file symex_target_equation.cpp.

◆ clear()

void symex_target_equationt::clear ( void )

inline

Definition at line 266 of file symex_target_equation.h.

◆ constraint()

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

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

Implements symex_targett.

Definition at line 314 of file symex_target_equation.cpp.

◆ convert()

void symex_target_equationt::convert ( decision_proceduret & decision_procedure )

Interface method to initiate the conversion into a decision procedure format.

The method iterates over the equation, i.e. over the SSA steps and converts each type of step separately.

Parameters

decision_procedure A handle to a decision procedure interface

Definition at line 347 of file symex_target_equation.cpp.

◆ convert_assertions()

void symex_target_equationt::convert_assertions	(	decision_proceduret &	decision_procedure,
		bool	optimized_for_single_assertions = `true`
	)

Converts assertions: build a disjunction of negated assertions.

Parameters

decision_procedure	A handle to a decision procedure interface
optimized_for_single_assertions	Use an optimized encoding for single assertions (unsound for incremental conversions)

Definition at line 507 of file symex_target_equation.cpp.

◆ convert_assignments()

void symex_target_equationt::convert_assignments ( decision_proceduret & decision_procedure )

Converts assignments: set the equality lhs==rhs to True.

Parameters

decision_procedure A handle to a decision procedure interface

Definition at line 361 of file symex_target_equation.cpp.

◆ convert_assumptions()

void symex_target_equationt::convert_assumptions ( decision_proceduret & decision_procedure )

Converts assumptions: convert the expression the assumption represents.

Parameters

decision_procedure A handle to a decision procedure interface

Definition at line 429 of file symex_target_equation.cpp.

◆ convert_constraints()

void symex_target_equationt::convert_constraints ( decision_proceduret & decision_procedure )

Converts constraints: set the represented condition to True.

Parameters

decision_procedure A handle to a decision procedure interface

Definition at line 484 of file symex_target_equation.cpp.

◆ convert_decls()

void symex_target_equationt::convert_decls ( decision_proceduret & decision_procedure )

Converts declarations: these are effectively ignored by the decision procedure.

Parameters

decision_procedure A handle to a decision procedure interface

Definition at line 383 of file symex_target_equation.cpp.

◆ convert_function_calls()

void symex_target_equationt::convert_function_calls ( decision_proceduret & decision_procedure )

Converts function calls: for each argument build an equality between its symbol and the argument itself.

Parameters

decision_procedure A handle to a decision procedure interface

Definition at line 619 of file symex_target_equation.cpp.

◆ convert_goto_instructions()

void symex_target_equationt::convert_goto_instructions ( decision_proceduret & decision_procedure )

Converts goto instructions: convert the expression representing the condition of this goto.

Parameters

decision_procedure A handle to a decision procedure interface

Definition at line 457 of file symex_target_equation.cpp.

◆ convert_guards()

void symex_target_equationt::convert_guards ( decision_proceduret & decision_procedure )

Converts guards: convert the expression the guard represents.

Parameters

decision_procedure A handle to a decision procedure interface

Definition at line 404 of file symex_target_equation.cpp.

◆ convert_io()

void symex_target_equationt::convert_io ( decision_proceduret & decision_procedure )

Converts I/O: for each argument build an equality between its symbol and the argument itself.

Parameters

decision_procedure A handle to a decision procedure interface

Definition at line 659 of file symex_target_equation.cpp.

◆ convert_without_assertions()

void symex_target_equationt::convert_without_assertions ( decision_proceduret & decision_procedure )

Interface method to initiate the conversion into a decision procedure format.

The method iterates over the equation, i.e. over the SSA steps and converts each type of step separately, except assertions. This enables the caller to handle assertion conversion differently, e.g. for incremental solving.

Parameters

decision_procedure A handle to a particular decision procedure interface

Definition at line 330 of file symex_target_equation.cpp.

◆ count_assertions()

std::size_t symex_target_equationt::count_assertions ( ) const

inline

Definition at line 234 of file symex_target_equation.h.

◆ count_ignored_SSA_steps()

std::size_t symex_target_equationt::count_ignored_SSA_steps ( ) const

inline

Definition at line 242 of file symex_target_equation.h.

◆ dead()

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

virtual

Remove a variable from the scope.

declare a fresh variable

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

Implements symex_targett.

Definition at line 161 of file symex_target_equation.cpp.

◆ decl()

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

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)

Implements symex_targett.

Definition at line 135 of file symex_target_equation.cpp.

◆ function_call()

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

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

Implements symex_targett.

Definition at line 181 of file symex_target_equation.cpp.

◆ function_return()

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

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

Implements symex_targett.

Definition at line 200 of file symex_target_equation.cpp.

◆ get_SSA_step()

SSA_stepst::iterator symex_target_equationt::get_SSA_step ( std::size_t s )

inline

Definition at line 253 of file symex_target_equation.h.

◆ goto_instruction()

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

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

Implements symex_targett.

Definition at line 300 of file symex_target_equation.cpp.

◆ has_threads()

bool symex_target_equationt::has_threads ( ) const

inline

Definition at line 271 of file symex_target_equation.h.

◆ input()

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

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

Implements symex_targett.

Definition at line 252 of file symex_target_equation.cpp.

◆ location()

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

virtual

Record a location.

Parameters

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

Implements symex_targett.

Definition at line 169 of file symex_target_equation.cpp.

◆ make_expression()

exprt symex_target_equationt::make_expression ( ) const

◆ memory_barrier()

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

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

Implements symex_targett.

Definition at line 74 of file symex_target_equation.cpp.

◆ merge_ireps()

void symex_target_equationt::merge_ireps ( SSA_stept & SSA_step )

protected

Merging causes identical ireps to be shared.

This is only enabled if the definition SHARING is defined.

Parameters

SSA_step The step you want to have shared values.

Definition at line 700 of file symex_target_equation.cpp.

◆ output() [1/2]

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

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

Implements symex_targett.

Definition at line 216 of file symex_target_equation.cpp.

◆ output() [2/2]

void symex_target_equationt::output ( std::ostream & out ) const

Definition at line 720 of file symex_target_equation.cpp.

◆ output_fmt()

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

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

Implements symex_targett.

Definition at line 233 of file symex_target_equation.cpp.

◆ shared_read()

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

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

Implements symex_targett.

Definition at line 30 of file symex_target_equation.cpp.

◆ shared_write()

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

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

Implements symex_targett.

Definition at line 46 of file symex_target_equation.cpp.

◆ spawn()

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

virtual

Record spawning a new thread.

spawn 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

Implements symex_targett.

Definition at line 63 of file symex_target_equation.cpp.

◆ validate()

void symex_target_equationt::validate	(	const namespacet &	ns,
		const validation_modet	vm
	)		const

inline

Definition at line 279 of file symex_target_equation.h.

Member Data Documentation

◆ argument_count

std::size_t symex_target_equationt::argument_count = 0

protected

Definition at line 296 of file symex_target_equation.h.

◆ io_count

std::size_t symex_target_equationt::io_count = 0

protected

Definition at line 293 of file symex_target_equation.h.

◆ log

messaget symex_target_equationt::log

protected

Definition at line 286 of file symex_target_equation.h.

◆ merge_irep

merge_irept symex_target_equationt::merge_irep

protected

Definition at line 289 of file symex_target_equation.h.

◆ SSA_steps

SSA_stepst symex_target_equationt::SSA_steps

Definition at line 251 of file symex_target_equation.h.

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

/home/runner/work/cbmc/cbmc/src/goto-symex/symex_target_equation.h
/home/runner/work/cbmc/cbmc/src/goto-symex/symex_target_equation.cpp

Public Types

Public Member Functions

Public Attributes

Protected Member Functions

Protected Attributes

Detailed Description

Member Typedef Documentation

◆ SSA_stepst

Constructor & Destructor Documentation

◆ symex_target_equationt()

◆ ~symex_target_equationt()

Member Function Documentation

◆ assertion()

◆ assignment()

◆ assumption()

◆ atomic_begin()

◆ atomic_end()

◆ clear()

◆ constraint()

◆ convert()

◆ convert_assertions()

◆ convert_assignments()

◆ convert_assumptions()

◆ convert_constraints()

◆ convert_decls()

◆ convert_function_calls()

◆ convert_goto_instructions()

◆ convert_guards()

◆ convert_io()

◆ convert_without_assertions()

◆ count_assertions()

◆ count_ignored_SSA_steps()

◆ dead()

◆ decl()

◆ function_call()

◆ function_return()

◆ get_SSA_step()

◆ goto_instruction()

◆ has_threads()

◆ input()

◆ location()

◆ make_expression()

◆ memory_barrier()

◆ merge_ireps()

◆ output() [1/2]

◆ output() [2/2]

◆ output_fmt()

◆ shared_read()

◆ shared_write()

◆ spawn()

◆ validate()

Member Data Documentation

◆ argument_count

◆ io_count

◆ log

◆ merge_irep

◆ SSA_steps