CBMC
Public Member Functions | Public Attributes | List of all members
SSA_stept Class Reference

Single SSA step in the equation. More...

#include <ssa_step.h>

+ Inheritance diagram for SSA_stept:
+ Collaboration diagram for SSA_stept:

Public Member Functions

bool is_assert () const
 
bool is_assume () const
 
bool is_assignment () const
 
bool is_goto () const
 
bool is_constraint () const
 
bool is_location () const
 
bool is_output () const
 
bool is_decl () const
 
bool is_function_call () const
 
bool is_function_return () const
 
bool is_shared_read () const
 
bool is_shared_write () const
 
bool is_spawn () const
 
bool is_memory_barrier () const
 
bool is_atomic_begin () const
 
bool is_atomic_end () const
 
exprt get_ssa_expr () const
 
 SSA_stept (const symex_targett::sourcet &_source, goto_trace_stept::typet _type)
 
void output (std::ostream &out) const
 
void validate (const namespacet &ns, const validation_modet vm) const
 Check that the SSA step is well-formed. More...
 

Public Attributes

symex_targett::sourcet source
 
goto_trace_stept::typet type
 
bool hidden = false
 
exprt guard
 
exprt guard_handle
 
ssa_exprt ssa_lhs
 
exprt ssa_full_lhs
 
exprt original_full_lhs
 
exprt ssa_rhs
 
symex_targett::assignment_typet assignment_type
 
exprt cond_expr
 
exprt cond_handle
 
std::string comment
 
irep_idt property_id
 
irep_idt format_string
 
irep_idt io_id
 
bool formatted = false
 
std::list< exprt > io_args
 
std::list< exprt > converted_io_args
 
irep_idt called_function
 
std::vector< exprt > ssa_function_arguments
 
std::vector< exprt > converted_function_arguments
 
unsigned atomic_section_id = 0
 
bool ignore = false
 
bool converted = false
 

Detailed Description

Single SSA step in the equation.

Its type is defined as goto_trace_stept::typet. Every SSA step has a source to identify its origin in the input GOTO program and a guard expression which holds the path condition required to reach this step: they limit the scope of this step.

SSA steps that represent assignments and declarations also store the left- and right-hand sides of the assignment. The left-hand side ssa_lhs is required to be of type ssa_exprt: in SSA form, variables are only assigned once, see Static Single Assignment (SSA) Form. To achieve that, we annotate the original name with 3 types of levels, see ssa_exprt. The assignment step also represents the left-hand side in two other full forms: ssa_full_lhs and original_full_lhs, which store the original expressions from the input GOTO program before removing array indexes, pointers, etc. The ssa_full_lhs uses the level-annotated names.

Assumptions, assertions, goto steps, and constraints have cond_expr which represent the condition guarding this step, i.e. what must hold for this step to be taken. Both guard and cond_expr will later be translated into verification condition for the SAT/SMT solver (or some other decision procedure), to be referred by their respective handles. Constraints usually arise from external conditions, such as memory models or partial orders: they represent assumptions with global effect.

Function calls store called_function name as well as a vector of arguments ssa_function_arguments. The converted version of a variable will contain its version for the SAT/SMT conversion.

Definition at line 46 of file ssa_step.h.

Constructor & Destructor Documentation

◆ SSA_stept()

SSA_stept::SSA_stept ( const symex_targett::sourcet &  _source,
goto_trace_stept::typet  _type 
)
inline

Definition at line 177 of file ssa_step.h.

Member Function Documentation

◆ get_ssa_expr()

exprt SSA_stept::get_ssa_expr ( ) const
inline

Definition at line 151 of file ssa_step.h.

◆ is_assert()

bool SSA_stept::is_assert ( ) const
inline

Definition at line 52 of file ssa_step.h.

◆ is_assignment()

bool SSA_stept::is_assignment ( ) const
inline

Definition at line 62 of file ssa_step.h.

◆ is_assume()

bool SSA_stept::is_assume ( ) const
inline

Definition at line 57 of file ssa_step.h.

◆ is_atomic_begin()

bool SSA_stept::is_atomic_begin ( ) const
inline

Definition at line 122 of file ssa_step.h.

◆ is_atomic_end()

bool SSA_stept::is_atomic_end ( ) const
inline

Definition at line 127 of file ssa_step.h.

◆ is_constraint()

bool SSA_stept::is_constraint ( ) const
inline

Definition at line 72 of file ssa_step.h.

◆ is_decl()

bool SSA_stept::is_decl ( ) const
inline

Definition at line 87 of file ssa_step.h.

◆ is_function_call()

bool SSA_stept::is_function_call ( ) const
inline

Definition at line 92 of file ssa_step.h.

◆ is_function_return()

bool SSA_stept::is_function_return ( ) const
inline

Definition at line 97 of file ssa_step.h.

◆ is_goto()

bool SSA_stept::is_goto ( ) const
inline

Definition at line 67 of file ssa_step.h.

◆ is_location()

bool SSA_stept::is_location ( ) const
inline

Definition at line 77 of file ssa_step.h.

◆ is_memory_barrier()

bool SSA_stept::is_memory_barrier ( ) const
inline

Definition at line 117 of file ssa_step.h.

◆ is_output()

bool SSA_stept::is_output ( ) const
inline

Definition at line 82 of file ssa_step.h.

◆ is_shared_read()

bool SSA_stept::is_shared_read ( ) const
inline

Definition at line 102 of file ssa_step.h.

◆ is_shared_write()

bool SSA_stept::is_shared_write ( ) const
inline

Definition at line 107 of file ssa_step.h.

◆ is_spawn()

bool SSA_stept::is_spawn ( ) const
inline

Definition at line 112 of file ssa_step.h.

◆ output()

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

Definition at line 14 of file ssa_step.cpp.

◆ validate()

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

Check that the SSA step is well-formed.

Parameters
nsnamespace to lookup identifiers
vmvalidation mode to be used for reporting failures

Definition at line 129 of file ssa_step.cpp.

Member Data Documentation

◆ assignment_type

symex_targett::assignment_typet SSA_stept::assignment_type

Definition at line 142 of file ssa_step.h.

◆ atomic_section_id

unsigned SSA_stept::atomic_section_id = 0

Definition at line 169 of file ssa_step.h.

◆ called_function

irep_idt SSA_stept::called_function

Definition at line 163 of file ssa_step.h.

◆ comment

std::string SSA_stept::comment

Definition at line 147 of file ssa_step.h.

◆ cond_expr

exprt SSA_stept::cond_expr

Definition at line 145 of file ssa_step.h.

◆ cond_handle

exprt SSA_stept::cond_handle

Definition at line 146 of file ssa_step.h.

◆ converted

bool SSA_stept::converted = false

Definition at line 175 of file ssa_step.h.

◆ converted_function_arguments

std::vector<exprt> SSA_stept::converted_function_arguments

Definition at line 166 of file ssa_step.h.

◆ converted_io_args

std::list<exprt> SSA_stept::converted_io_args

Definition at line 160 of file ssa_step.h.

◆ format_string

irep_idt SSA_stept::format_string

Definition at line 157 of file ssa_step.h.

◆ formatted

bool SSA_stept::formatted = false

Definition at line 158 of file ssa_step.h.

◆ guard

exprt SSA_stept::guard

Definition at line 135 of file ssa_step.h.

◆ guard_handle

exprt SSA_stept::guard_handle

Definition at line 136 of file ssa_step.h.

◆ hidden

bool SSA_stept::hidden = false

Definition at line 133 of file ssa_step.h.

◆ ignore

bool SSA_stept::ignore = false

Definition at line 172 of file ssa_step.h.

◆ io_args

std::list<exprt> SSA_stept::io_args

Definition at line 159 of file ssa_step.h.

◆ io_id

irep_idt SSA_stept::io_id

Definition at line 157 of file ssa_step.h.

◆ original_full_lhs

exprt SSA_stept::original_full_lhs

Definition at line 140 of file ssa_step.h.

◆ property_id

irep_idt SSA_stept::property_id

Definition at line 149 of file ssa_step.h.

◆ source

symex_targett::sourcet SSA_stept::source

Definition at line 49 of file ssa_step.h.

◆ ssa_full_lhs

exprt SSA_stept::ssa_full_lhs

Definition at line 140 of file ssa_step.h.

◆ ssa_function_arguments

std::vector<exprt> SSA_stept::ssa_function_arguments

Definition at line 166 of file ssa_step.h.

◆ ssa_lhs

ssa_exprt SSA_stept::ssa_lhs

Definition at line 139 of file ssa_step.h.

◆ ssa_rhs

exprt SSA_stept::ssa_rhs

Definition at line 141 of file ssa_step.h.

◆ type

goto_trace_stept::typet SSA_stept::type

Definition at line 50 of file ssa_step.h.

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