cprover
symex_targett Class Referenceabstract

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 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_identifier, const std::vector< exprt > &ssa_function_arguments, const sourcet &source, bool hidden)=0
 Record a function call. More...
 
virtual void function_return (const exprt &guard, 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< exprt > &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 exprt &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 23 of file symex_target.h.

Member Enumeration Documentation

◆ assignment_typet

Enumerator
STATE 
HIDDEN 
VISIBLE_ACTUAL_PARAMETER 
HIDDEN_ACTUAL_PARAMETER 
PHI 
GUARD 

Definition at line 64 of file symex_target.h.

Constructor & Destructor Documentation

◆ symex_targett()

symex_targett::symex_targett ( )
inline

Definition at line 26 of file symex_target.h.

◆ ~symex_targett()

virtual symex_targett::~symex_targett ( )
inlinevirtual

Definition at line 30 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
guardPrecondition for reaching this assertion
condCondition this assertion represents
msgThe message associated with this assertion
sourcePointer 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
guardPrecondition for this read event
ssa_lhsVariable to be written to, must be a symbol (and not nil)
ssa_full_lhsFull left-hand side with symex level annotations
original_full_lhsFull left-hand side without symex level annotations
ssa_rhsRight-hand side of the assignment
sourcePointer to location in the input GOTO program of this assignment
assignment_typeTo 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
guardPrecondition for reaching this assumption
condCondition this assumption represents
sourcePointer 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
guardPrecondition for reaching this atomic section
atomic_section_idIdentifier for this atomic section
sourcePointer 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
guardPrecondition for reaching the end of this atomic section
atomic_section_idIdentifier for this atomic section
sourcePointer 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
condCondition represented by this constraint
msgThe message associated with this constraint
sourcePointer 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
guardPrecondition for removal of this variable
ssa_lhsVariable to be removed, must be symbol
sourcePointer 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 sourcet source,
assignment_typet  assignment_type 
)
pure virtual

Declare a fresh variable.

The cond_expr is lhs==lhs.

Parameters
guardPrecondition for a declaration of this variable
ssa_lhsVariable to be declared, must be symbol (and not nil)
sourcePointer to location in the input GOTO program of this declaration
assignment_typeTo 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_identifier,
const std::vector< exprt > &  ssa_function_arguments,
const sourcet source,
bool  hidden 
)
pure virtual

Record a function call.

Parameters
guardPrecondition for calling a function
function_identifierName of the function
ssa_function_argumentsVector of arguments in SSA form
sourceTo location in the input GOTO program of this
hiddenShould 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 sourcet source,
bool  hidden 
)
pure virtual

Record return from a function.

Parameters
guardPrecondition for returning from a function
sourcePointer to location in the input GOTO program of this
hiddenShould 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 exprt cond,
const sourcet source 
)
pure virtual

Record a goto instruction.

Parameters
guardPrecondition for reaching this goto instruction
condCondition under which this goto should be taken
sourcePointer 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
guardPrecondition for reading from the input
sourcePointer to location in the input GOTO program of this input
input_idName of the input
argsA 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
guardPrecondition for reaching this location
sourcePointer 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
guardPrecondition for reaching this barrier
sourcePointer 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< exprt > &  args 
)
pure virtual

Record an output.

Parameters
guardPrecondition for writing to the output
sourcePointer to location in the input GOTO program of this output
output_idName of the output
argsA 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
guardPrecondition for writing to the output
sourcePointer to location in the input GOTO program of this output
output_idName of the output
fmtFormatting string
argsA 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
guardPrecondition for this read event
ssa_objectVariable to be read from
atomic_section_idID of the atomic section in which this read takes place (if any)
sourcePointer 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
guardPrecondition for this write event
ssa_objectVariable to be written to
atomic_section_idID of the atomic section in which this write takes place (if any)
sourcePointer 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
guardPrecondition for reaching spawning a new thread
sourcePointer 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: