cprover
|
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>
Classes | |
class | SSA_stept |
Single SSA step in the equation. More... | |
Public Types | |
typedef std::list< SSA_stept > | SSA_stepst |
![]() | |
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 |
![]() | |
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 |
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.
typedef std::list<SSA_stept> symex_target_equationt::SSA_stepst |
Definition at line 368 of file symex_target_equation.h.
|
virtualdefault |
|
virtual |
Record an assertion.
guard | Precondition for reaching this assertion |
cond | Condition this assertion represents |
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 314 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 126 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 298 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 95 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 111 of file symex_target_equation.cpp.
|
inline |
Definition at line 384 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 348 of file symex_target_equation.cpp.
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.
prop_conv | A handle to a particular decision procedure interface |
Definition at line 366 of file symex_target_equation.cpp.
void symex_target_equationt::convert_assertions | ( | prop_convt & | prop_conv | ) |
Converts assertions: build a disjunction of negated assertions.
prop_conv | A handle to a particular decision procedure interface |
Definition at line 558 of file symex_target_equation.cpp.
void symex_target_equationt::convert_assignments | ( | decision_proceduret & | decision_procedure | ) | const |
Converts assignments: set the equality lhs==rhs to True.
decision_procedure | A handle to a particular decision procedure interface |
Definition at line 389 of file symex_target_equation.cpp.
void symex_target_equationt::convert_assumptions | ( | prop_convt & | prop_conv | ) |
Converts assumptions: convert the expression the assumption represents.
prop_conv | A handle to a particular decision procedure interface |
Definition at line 461 of file symex_target_equation.cpp.
void symex_target_equationt::convert_constraints | ( | decision_proceduret & | decision_procedure | ) | const |
Converts constraints: set the represented condition to True.
decision_procedure | A handle to a particular decision procedure interface |
Definition at line 527 of file symex_target_equation.cpp.
void symex_target_equationt::convert_decls | ( | prop_convt & | prop_conv | ) | const |
Converts declarations: these are effectively ignored by the decision procedure.
prop_conv | A handle to a particular decision procedure interface |
Definition at line 408 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 particular decision procedure interface |
Definition at line 639 of file symex_target_equation.cpp.
void symex_target_equationt::convert_goto_instructions | ( | prop_convt & | prop_conv | ) |
Converts goto instructions: convert the expression representing the condition of this goto.
prop_conv | A handle to a particular decision procedure interface |
Definition at line 494 of file symex_target_equation.cpp.
void symex_target_equationt::convert_guards | ( | prop_convt & | prop_conv | ) |
Converts guards: convert the expression the guard represents.
prop_conv | A handle to a particular decision procedure interface |
Definition at line 431 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 particular decision procedure interface |
Definition at line 669 of file symex_target_equation.cpp.
|
inline |
Definition at line 346 of file symex_target_equation.h.
|
inline |
Definition at line 357 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 183 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) |
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 156 of file symex_target_equation.cpp.
|
virtual |
Record a function call.
guard | Precondition for calling a function |
function_identifier | 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 205 of file symex_target_equation.cpp.
|
virtual |
Record return from a function.
guard | Precondition for returning from a function |
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 225 of file symex_target_equation.cpp.
|
inline |
Definition at line 371 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 332 of file symex_target_equation.cpp.
|
inline |
Definition at line 389 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 280 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 191 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 81 of file symex_target_equation.cpp.
|
protected |
Definition at line 698 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 241 of file symex_target_equation.cpp.
void symex_target_equationt::output | ( | std::ostream & | out, |
const namespacet & | ns | ||
) | const |
Definition at line 718 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 259 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 31 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 49 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 68 of file symex_target_equation.cpp.
|
inline |
Definition at line 400 of file symex_target_equation.h.
|
protected |
Definition at line 408 of file symex_target_equation.h.
SSA_stepst symex_target_equationt::SSA_steps |
Definition at line 369 of file symex_target_equation.h.