CBMC
|
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>
Public Types | |
typedef std::list< SSA_stept > | SSA_stepst |
![]() | |
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 |
![]() | |
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 |
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.
typedef std::list<SSA_stept> symex_target_equationt::SSA_stepst |
Definition at line 250 of file symex_target_equation.h.
|
inlineexplicit |
Definition at line 36 of file symex_target_equation.h.
|
virtualdefault |
|
virtual |
Record an assertion.
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.
|
virtual |
Write to a local variable.
The cond_expr
is lhs==rhs.
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.
|
virtual |
Record an assumption.
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.
|
virtual |
Record a beginning of an atomic section.
start an atomic section
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.
|
virtual |
Record ending an atomic section.
end an atomic section
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.
|
inline |
Definition at line 266 of file symex_target_equation.h.
|
virtual |
Record a global constraint: there is no guard limiting its scope.
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.
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.
decision_procedure | A handle to a decision procedure interface |
Definition at line 347 of file symex_target_equation.cpp.
void symex_target_equationt::convert_assertions | ( | decision_proceduret & | decision_procedure, |
bool | optimized_for_single_assertions = true |
||
) |
Converts assertions: build a disjunction of negated assertions.
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.
void symex_target_equationt::convert_assignments | ( | decision_proceduret & | decision_procedure | ) |
Converts assignments: set the equality lhs==rhs to True.
decision_procedure | A handle to a decision procedure interface |
Definition at line 361 of file symex_target_equation.cpp.
void symex_target_equationt::convert_assumptions | ( | decision_proceduret & | decision_procedure | ) |
Converts assumptions: convert the expression the assumption represents.
decision_procedure | A handle to a decision procedure interface |
Definition at line 429 of file symex_target_equation.cpp.
void symex_target_equationt::convert_constraints | ( | decision_proceduret & | decision_procedure | ) |
Converts constraints: set the represented condition to True.
decision_procedure | A handle to a decision procedure interface |
Definition at line 484 of file symex_target_equation.cpp.
void symex_target_equationt::convert_decls | ( | decision_proceduret & | decision_procedure | ) |
Converts declarations: these are effectively ignored by the decision procedure.
decision_procedure | A handle to a decision procedure interface |
Definition at line 383 of file symex_target_equation.cpp.
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.
decision_procedure | A handle to a decision procedure interface |
Definition at line 619 of file symex_target_equation.cpp.
void symex_target_equationt::convert_goto_instructions | ( | decision_proceduret & | decision_procedure | ) |
Converts goto instructions: convert the expression representing the condition of this goto.
decision_procedure | A handle to a decision procedure interface |
Definition at line 457 of file symex_target_equation.cpp.
void symex_target_equationt::convert_guards | ( | decision_proceduret & | decision_procedure | ) |
Converts guards: convert the expression the guard represents.
decision_procedure | A handle to a decision procedure interface |
Definition at line 404 of file symex_target_equation.cpp.
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.
decision_procedure | A handle to a decision procedure interface |
Definition at line 659 of file symex_target_equation.cpp.
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.
decision_procedure | A handle to a particular decision procedure interface |
Definition at line 330 of file symex_target_equation.cpp.
|
inline |
Definition at line 234 of file symex_target_equation.h.
|
inline |
Definition at line 242 of file symex_target_equation.h.
|
virtual |
Remove a variable from the scope.
declare a fresh variable
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.
|
virtual |
Declare a fresh variable.
The cond_expr
is lhs==lhs.
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.
|
virtual |
Record a function call.
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.
|
virtual |
Record return from a function.
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.
|
inline |
Definition at line 253 of file symex_target_equation.h.
|
virtual |
Record a goto instruction.
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.
|
inline |
Definition at line 271 of file symex_target_equation.h.
|
virtual |
Record an input.
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.
Record a location.
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.
exprt symex_target_equationt::make_expression | ( | ) | const |
Record creating a memory barrier.
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.
|
protected |
Merging causes identical ireps to be shared.
This is only enabled if the definition SHARING is defined.
SSA_step | The step you want to have shared values. |
Definition at line 700 of file symex_target_equation.cpp.
|
virtual |
Record an output.
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.
void symex_target_equationt::output | ( | std::ostream & | out | ) | const |
Definition at line 720 of file symex_target_equation.cpp.
|
virtual |
Record formatted output.
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.
|
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.
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.
|
virtual |
Write to a shared variable ssa_object:
we effectively assign a value from this thread to be visible by other threads.
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.
Record spawning a new thread.
spawn a new thread
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.
|
inline |
Definition at line 279 of file symex_target_equation.h.
|
protected |
Definition at line 296 of file symex_target_equation.h.
|
protected |
Definition at line 293 of file symex_target_equation.h.
|
protected |
Definition at line 286 of file symex_target_equation.h.
|
protected |
Definition at line 289 of file symex_target_equation.h.
SSA_stepst symex_target_equationt::SSA_steps |
Definition at line 251 of file symex_target_equation.h.