cprover
symex_target_equationt Class Reference

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:

Classes

class  SSA_stept
 Single SSA step in the equation. More...
 

Public Types

typedef std::list< SSA_steptSSA_stepst
 
- Public Types inherited from symex_targett
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

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 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_identifier, const std::vector< exprt > &ssa_function_arguments, const sourcet &source, bool hidden)
 Record a function call. More...
 
virtual void function_return (const exprt &guard, 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< exprt > &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 std::string &msg, const sourcet &source)
 Record an assertion. More...
 
virtual void goto_instruction (const exprt &guard, const exprt &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 (prop_convt &prop_conv)
 Interface method to initiate the conversion into a decision procedure format. More...
 
void convert_assignments (decision_proceduret &decision_procedure) const
 Converts assignments: set the equality lhs==rhs to True. More...
 
void convert_decls (prop_convt &prop_conv) const
 Converts declarations: these are effectively ignored by the decision procedure. More...
 
void convert_assumptions (prop_convt &prop_conv)
 Converts assumptions: convert the expression the assumption represents. More...
 
void convert_assertions (prop_convt &prop_conv)
 Converts assertions: build a disjunction of negated assertions. More...
 
void convert_constraints (decision_proceduret &decision_procedure) const
 Converts constraints: set the represented condition to True. More...
 
void convert_goto_instructions (prop_convt &prop_conv)
 Converts goto instructions: convert the expression representing the condition of this goto. More...
 
void convert_guards (prop_convt &prop_conv)
 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 namespacet &ns) 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)
 

Protected Attributes

merge_irept merge_irep
 

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 35 of file symex_target_equation.h.

Member Typedef Documentation

◆ SSA_stepst

Definition at line 371 of file symex_target_equation.h.

Constructor & Destructor Documentation

◆ ~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 std::string &  msg,
const sourcet source 
)
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

Implements symex_targett.

Definition at line 314 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
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)

Implements symex_targett.

Definition at line 126 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
guardPrecondition for reaching this assumption
condCondition this assumption represents
sourcePointer to location in the input GOTO program of this assumption

Implements symex_targett.

Definition at line 298 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
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

Implements symex_targett.

Definition at line 95 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
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

Implements symex_targett.

Definition at line 111 of file symex_target_equation.cpp.

◆ clear()

void symex_target_equationt::clear ( void  )
inline

Definition at line 387 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
condCondition represented by this constraint
msgThe message associated with this constraint
sourcePointer to location in the input GOTO program of this constraint

Implements symex_targett.

Definition at line 348 of file symex_target_equation.cpp.

◆ convert()

void symex_target_equationt::convert ( prop_convt prop_conv)

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
prop_convA handle to a particular decision procedure interface

Definition at line 366 of file symex_target_equation.cpp.

◆ convert_assertions()

void symex_target_equationt::convert_assertions ( prop_convt prop_conv)

Converts assertions: build a disjunction of negated assertions.

Parameters
prop_convA handle to a particular decision procedure interface

Definition at line 558 of file symex_target_equation.cpp.

◆ convert_assignments()

void symex_target_equationt::convert_assignments ( decision_proceduret decision_procedure) const

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

Parameters
decision_procedureA handle to a particular decision procedure interface

Definition at line 389 of file symex_target_equation.cpp.

◆ convert_assumptions()

void symex_target_equationt::convert_assumptions ( prop_convt prop_conv)

Converts assumptions: convert the expression the assumption represents.

Parameters
prop_convA handle to a particular decision procedure interface

Definition at line 461 of file symex_target_equation.cpp.

◆ convert_constraints()

void symex_target_equationt::convert_constraints ( decision_proceduret decision_procedure) const

Converts constraints: set the represented condition to True.

Parameters
decision_procedureA handle to a particular decision procedure interface

Definition at line 527 of file symex_target_equation.cpp.

◆ convert_decls()

void symex_target_equationt::convert_decls ( prop_convt prop_conv) const

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

Parameters
prop_convA handle to a particular decision procedure interface

Definition at line 408 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_procedureA handle to a particular decision procedure interface

Definition at line 639 of file symex_target_equation.cpp.

◆ convert_goto_instructions()

void symex_target_equationt::convert_goto_instructions ( prop_convt prop_conv)

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

Parameters
prop_convA handle to a particular decision procedure interface

Definition at line 494 of file symex_target_equation.cpp.

◆ convert_guards()

void symex_target_equationt::convert_guards ( prop_convt prop_conv)

Converts guards: convert the expression the guard represents.

Parameters
prop_convA handle to a particular decision procedure interface

Definition at line 431 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_procedureA handle to a particular decision procedure interface

Definition at line 669 of file symex_target_equation.cpp.

◆ count_assertions()

std::size_t symex_target_equationt::count_assertions ( ) const
inline

Definition at line 349 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 360 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
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

Implements symex_targett.

Definition at line 183 of file symex_target_equation.cpp.

◆ decl()

void symex_target_equationt::decl ( const exprt guard,
const ssa_exprt ssa_lhs,
const sourcet source,
assignment_typet  assignment_type 
)
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)

Implements symex_targett.

Definition at line 156 of file symex_target_equation.cpp.

◆ function_call()

void symex_target_equationt::function_call ( const exprt guard,
const irep_idt function_identifier,
const std::vector< exprt > &  ssa_function_arguments,
const sourcet source,
bool  hidden 
)
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

Implements symex_targett.

Definition at line 205 of file symex_target_equation.cpp.

◆ function_return()

void symex_target_equationt::function_return ( const exprt guard,
const sourcet source,
bool  hidden 
)
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

Implements symex_targett.

Definition at line 225 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 374 of file symex_target_equation.h.

◆ goto_instruction()

void symex_target_equationt::goto_instruction ( const exprt guard,
const exprt cond,
const sourcet source 
)
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

Implements symex_targett.

Definition at line 332 of file symex_target_equation.cpp.

◆ has_threads()

bool symex_target_equationt::has_threads ( ) const
inline

Definition at line 392 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
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

Implements symex_targett.

Definition at line 280 of file symex_target_equation.cpp.

◆ location()

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

Record a location.

Parameters
guardPrecondition for reaching this location
sourcePointer to location in the input GOTO program to be recorded

Implements symex_targett.

Definition at line 191 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
guardPrecondition for reaching this barrier
sourcePointer to location in the input GOTO program where a new barrier is created

Implements symex_targett.

Definition at line 81 of file symex_target_equation.cpp.

◆ merge_ireps()

void symex_target_equationt::merge_ireps ( SSA_stept SSA_step)
protected

Definition at line 698 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< exprt > &  args 
)
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

Implements symex_targett.

Definition at line 241 of file symex_target_equation.cpp.

◆ output() [2/2]

void symex_target_equationt::output ( std::ostream &  out,
const namespacet ns 
) const

Definition at line 718 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
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

Implements symex_targett.

Definition at line 259 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
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

Implements symex_targett.

Definition at line 31 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
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

Implements symex_targett.

Definition at line 49 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
guardPrecondition for reaching spawning a new thread
sourcePointer to location in the input GOTO program where a new thread is to be spawned

Implements symex_targett.

Definition at line 68 of file symex_target_equation.cpp.

◆ validate()

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

Definition at line 403 of file symex_target_equation.h.

Member Data Documentation

◆ merge_irep

merge_irept symex_target_equationt::merge_irep
protected

Definition at line 411 of file symex_target_equation.h.

◆ SSA_steps

SSA_stepst symex_target_equationt::SSA_steps

Definition at line 372 of file symex_target_equation.h.


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