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:

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

 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 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 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_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)
 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 38 of file symex_target_equation.h.

Member Typedef Documentation

◆ SSA_stepst

Definition at line 240 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 41 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 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 284 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 110 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 270 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 83 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 97 of file symex_target_equation.cpp.

◆ clear()

void symex_target_equationt::clear ( void  )
inline

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

Definition at line 330 of file symex_target_equation.cpp.

◆ convert_assertions()

void symex_target_equationt::convert_assertions ( decision_proceduret decision_procedure)

Converts assertions: build a disjunction of negated assertions.

Parameters
decision_procedureA handle to a decision procedure interface

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

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

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

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

Definition at line 370 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 decision procedure interface

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

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

Definition at line 394 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 decision procedure interface

Definition at line 629 of file symex_target_equation.cpp.

◆ count_assertions()

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

Definition at line 224 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 232 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 163 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 138 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
guardPrecondition for calling a function
function_idName 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 183 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
guardPrecondition for returning from a function
function_idName of the function from which we return
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 202 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 243 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
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 300 of file symex_target_equation.cpp.

◆ has_threads()

bool symex_target_equationt::has_threads ( ) const
inline

Definition at line 261 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 254 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 171 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 71 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_stepThe step you want to have shared values.

Definition at line 659 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
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 218 of file symex_target_equation.cpp.

◆ output() [2/2]

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

Definition at line 679 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 235 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 27 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 43 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 60 of file symex_target_equation.cpp.

◆ validate()

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

Definition at line 269 of file symex_target_equation.h.

Member Data Documentation

◆ argument_count

std::size_t symex_target_equationt::argument_count = 0
protected

Definition at line 286 of file symex_target_equation.h.

◆ io_count

std::size_t symex_target_equationt::io_count = 0
protected

Definition at line 283 of file symex_target_equation.h.

◆ log

messaget symex_target_equationt::log
protected

Definition at line 276 of file symex_target_equation.h.

◆ merge_irep

merge_irept symex_target_equationt::merge_irep
protected

Definition at line 279 of file symex_target_equation.h.

◆ SSA_steps

SSA_stepst symex_target_equationt::SSA_steps

Definition at line 241 of file symex_target_equation.h.


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