cprover
|
#include <symex_target_equation.h>
Classes | |
class | SSA_stept |
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 | |
symex_target_equationt (const namespacet &_ns) | |
virtual | ~symex_target_equationt () |
virtual void | shared_read (const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source) |
read from a shared variable More... | |
virtual void | shared_write (const exprt &guard, const ssa_exprt &ssa_object, unsigned atomic_section_id, const sourcet &source) |
write to a sharedvariable 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 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) |
declare a fresh variable More... | |
virtual void | function_call (const exprt &guard, const irep_idt &identifier, const sourcet &source) |
just record a location More... | |
virtual void | function_return (const exprt &guard, const irep_idt &identifier, const sourcet &source) |
just record a location More... | |
virtual void | location (const exprt &guard, const sourcet &source) |
just record a location More... | |
virtual void | output (const exprt &guard, const sourcet &source, const irep_idt &fmt, const std::list< exprt > &args) |
just record 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) |
just record formatted output More... | |
virtual void | input (const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args) |
just record 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 constraint More... | |
virtual void | spawn (const exprt &guard, const sourcet &source) |
spawn a new thread More... | |
virtual void | memory_barrier (const exprt &guard, const sourcet &source) |
virtual void | atomic_begin (const exprt &guard, unsigned atomic_section_id, const sourcet &source) |
start an atomic section More... | |
virtual void | atomic_end (const exprt &guard, unsigned atomic_section_id, const sourcet &source) |
end an atomic section More... | |
void | convert (prop_convt &prop_conv) |
void | convert_assignments (decision_proceduret &decision_procedure) const |
converts assignments More... | |
void | convert_decls (prop_convt &prop_conv) const |
converts declarations More... | |
void | convert_assumptions (prop_convt &prop_conv) |
converts assumptions More... | |
void | convert_assertions (prop_convt &prop_conv) |
converts assertions More... | |
void | convert_constraints (decision_proceduret &decision_procedure) const |
converts constraints More... | |
void | convert_goto_instructions (prop_convt &prop_conv) |
converts goto instructions More... | |
void | convert_guards (prop_convt &prop_conv) |
converts guards More... | |
void | convert_io (decision_proceduret &decision_procedure) |
converts I/O More... | |
exprt | make_expression () const |
unsigned | count_assertions () const |
unsigned | count_ignored_SSA_steps () const |
SSA_stepst::iterator | get_SSA_step (unsigned s) |
void | output (std::ostream &out) const |
void | clear () |
bool | has_threads () const |
![]() | |
symex_targett () | |
virtual | ~symex_targett () |
Public Attributes | |
SSA_stepst | SSA_steps |
Protected Member Functions | |
void | merge_ireps (SSA_stept &SSA_step) |
Protected Attributes | |
const namespacet & | ns |
merge_irept | merge_irep |
Definition at line 31 of file symex_target_equation.h.
typedef std::list<SSA_stept> symex_target_equationt::SSA_stepst |
Definition at line 285 of file symex_target_equation.h.
|
explicit |
Definition at line 25 of file symex_target_equation.cpp.
|
virtual |
Definition at line 30 of file symex_target_equation.cpp.
|
virtual |
record an assertion
Implements symex_targett.
Definition at line 325 of file symex_target_equation.cpp.
References goto_trace_stept::ASSERT, symex_target_equationt::SSA_stept::comment, symex_target_equationt::SSA_stept::cond_expr, symex_target_equationt::SSA_stept::guard, merge_ireps(), symex_target_equationt::SSA_stept::source, SSA_steps, and symex_target_equationt::SSA_stept::type.
|
virtual |
write to a variable
Implements symex_targett.
Definition at line 132 of file symex_target_equation.cpp.
References goto_trace_stept::ASSIGNMENT, symex_target_equationt::SSA_stept::assignment_type, symex_target_equationt::SSA_stept::cond_expr, symex_target_equationt::SSA_stept::guard, symex_target_equationt::SSA_stept::hidden, irept::is_not_nil(), merge_ireps(), symex_target_equationt::SSA_stept::original_full_lhs, symex_target_equationt::SSA_stept::source, symex_target_equationt::SSA_stept::ssa_full_lhs, symex_target_equationt::SSA_stept::ssa_lhs, symex_target_equationt::SSA_stept::ssa_rhs, SSA_steps, symex_targett::STATE, symex_target_equationt::SSA_stept::type, and symex_targett::VISIBLE_ACTUAL_PARAMETER.
|
virtual |
record an assumption
Implements symex_targett.
Definition at line 308 of file symex_target_equation.cpp.
References goto_trace_stept::ASSUME, symex_target_equationt::SSA_stept::cond_expr, symex_target_equationt::SSA_stept::guard, merge_ireps(), symex_target_equationt::SSA_stept::source, SSA_steps, and symex_target_equationt::SSA_stept::type.
Referenced by convert_assertions().
|
virtual |
start an atomic section
Implements symex_targett.
Definition at line 100 of file symex_target_equation.cpp.
References goto_trace_stept::ATOMIC_BEGIN, symex_target_equationt::SSA_stept::atomic_section_id, symex_target_equationt::SSA_stept::guard, merge_ireps(), symex_target_equationt::SSA_stept::source, SSA_steps, and symex_target_equationt::SSA_stept::type.
|
virtual |
end an atomic section
Implements symex_targett.
Definition at line 116 of file symex_target_equation.cpp.
References goto_trace_stept::ATOMIC_END, symex_target_equationt::SSA_stept::atomic_section_id, symex_target_equationt::SSA_stept::guard, merge_ireps(), symex_target_equationt::SSA_stept::source, SSA_steps, and symex_target_equationt::SSA_stept::type.
|
inline |
Definition at line 301 of file symex_target_equation.h.
|
virtual |
record a constraint
Implements symex_targett.
Definition at line 361 of file symex_target_equation.cpp.
References symex_target_equationt::SSA_stept::comment, symex_target_equationt::SSA_stept::cond_expr, goto_trace_stept::CONSTRAINT, symex_target_equationt::SSA_stept::guard, merge_ireps(), symex_target_equationt::SSA_stept::source, SSA_steps, and symex_target_equationt::SSA_stept::type.
Referenced by partial_order_concurrencyt::add_constraint().
void symex_target_equationt::convert | ( | prop_convt & | prop_conv | ) |
Definition at line 379 of file symex_target_equation.cpp.
References convert_assertions(), convert_assignments(), convert_assumptions(), convert_constraints(), convert_decls(), convert_goto_instructions(), convert_guards(), and convert_io().
Referenced by scratch_programt::check_sat(), and bmct::do_conversion().
void symex_target_equationt::convert_assertions | ( | prop_convt & | prop_conv | ) |
converts assertions
Definition at line 489 of file symex_target_equation.cpp.
References assumption(), const_literal(), prop_convt::convert(), exprt::copy_to_operands(), count_assertions(), disjunction(), irept::id(), decision_proceduret::set_to_false(), decision_proceduret::set_to_true(), and SSA_steps.
Referenced by convert().
void symex_target_equationt::convert_assignments | ( | decision_proceduret & | decision_procedure | ) | const |
converts assignments
Definition at line 395 of file symex_target_equation.cpp.
References decision_proceduret::set_to_true(), and SSA_steps.
Referenced by convert().
void symex_target_equationt::convert_assumptions | ( | prop_convt & | prop_conv | ) |
converts assumptions
Definition at line 437 of file symex_target_equation.cpp.
References const_literal(), prop_convt::convert(), and SSA_steps.
Referenced by convert().
void symex_target_equationt::convert_constraints | ( | decision_proceduret & | decision_procedure | ) | const |
converts constraints
Definition at line 472 of file symex_target_equation.cpp.
References decision_proceduret::set_to_true(), and SSA_steps.
Referenced by convert().
void symex_target_equationt::convert_decls | ( | prop_convt & | prop_conv | ) | const |
converts declarations
Definition at line 407 of file symex_target_equation.cpp.
References prop_convt::convert(), and SSA_steps.
Referenced by convert().
void symex_target_equationt::convert_goto_instructions | ( | prop_convt & | prop_conv | ) |
converts goto instructions
Definition at line 454 of file symex_target_equation.cpp.
References const_literal(), prop_convt::convert(), and SSA_steps.
Referenced by convert().
void symex_target_equationt::convert_guards | ( | prop_convt & | prop_conv | ) |
converts guards
Definition at line 423 of file symex_target_equation.cpp.
References const_literal(), prop_convt::convert(), and SSA_steps.
Referenced by convert().
void symex_target_equationt::convert_io | ( | decision_proceduret & | dec_proc | ) |
converts I/O
Definition at line 557 of file symex_target_equation.cpp.
References merge_irep, symbol_exprt::set_identifier(), decision_proceduret::set_to(), SSA_steps, and exprt::type().
Referenced by convert().
|
inline |
Definition at line 263 of file symex_target_equation.h.
References SSA_steps.
Referenced by scratch_programt::check_sat(), and convert_assertions().
|
inline |
Definition at line 274 of file symex_target_equation.h.
References SSA_steps.
Referenced by bmct::run().
|
virtual |
declare a fresh variable
Implements symex_targett.
Definition at line 190 of file symex_target_equation.cpp.
|
virtual |
declare a fresh variable
Implements symex_targett.
Definition at line 163 of file symex_target_equation.cpp.
References symex_target_equationt::SSA_stept::cond_expr, goto_trace_stept::DECL, ssa_exprt::get_original_expr(), symex_target_equationt::SSA_stept::guard, symex_target_equationt::SSA_stept::hidden, irept::is_not_nil(), merge_ireps(), symex_target_equationt::SSA_stept::original_full_lhs, symex_target_equationt::SSA_stept::source, symex_target_equationt::SSA_stept::ssa_full_lhs, symex_target_equationt::SSA_stept::ssa_lhs, SSA_steps, symex_targett::STATE, and symex_target_equationt::SSA_stept::type.
|
virtual |
just record a location
Implements symex_targett.
Definition at line 214 of file symex_target_equation.cpp.
References goto_trace_stept::FUNCTION_CALL, symex_target_equationt::SSA_stept::guard, symex_target_equationt::SSA_stept::identifier, merge_ireps(), symex_target_equationt::SSA_stept::source, SSA_steps, and symex_target_equationt::SSA_stept::type.
|
virtual |
just record a location
Implements symex_targett.
Definition at line 231 of file symex_target_equation.cpp.
References goto_trace_stept::FUNCTION_RETURN, symex_target_equationt::SSA_stept::guard, symex_target_equationt::SSA_stept::identifier, merge_ireps(), symex_target_equationt::SSA_stept::source, SSA_steps, and symex_target_equationt::SSA_stept::type.
|
inline |
Definition at line 288 of file symex_target_equation.h.
References symex_target_equationt::SSA_stept::output().
|
virtual |
record a goto instruction
Implements symex_targett.
Definition at line 344 of file symex_target_equation.cpp.
References symex_target_equationt::SSA_stept::cond_expr, goto_trace_stept::GOTO, symex_target_equationt::SSA_stept::guard, merge_ireps(), symex_target_equationt::SSA_stept::source, SSA_steps, and symex_target_equationt::SSA_stept::type.
|
inline |
Definition at line 306 of file symex_target_equation.h.
Referenced by bmct::run(), bmct::show_vcc_json(), and bmct::show_vcc_plain().
|
virtual |
just record input
Implements symex_targett.
Definition at line 289 of file symex_target_equation.cpp.
References symex_target_equationt::SSA_stept::guard, goto_trace_stept::INPUT, symex_target_equationt::SSA_stept::io_args, symex_target_equationt::SSA_stept::io_id, merge_ireps(), symex_target_equationt::SSA_stept::source, SSA_steps, and symex_target_equationt::SSA_stept::type.
just record a location
Implements symex_targett.
Definition at line 199 of file symex_target_equation.cpp.
References symex_target_equationt::SSA_stept::guard, goto_trace_stept::LOCATION, merge_ireps(), symex_target_equationt::SSA_stept::source, SSA_steps, and symex_target_equationt::SSA_stept::type.
exprt symex_target_equationt::make_expression | ( | ) | const |
Implements symex_targett.
Definition at line 86 of file symex_target_equation.cpp.
References symex_target_equationt::SSA_stept::guard, goto_trace_stept::MEMORY_BARRIER, merge_ireps(), symex_target_equationt::SSA_stept::source, SSA_steps, and symex_target_equationt::SSA_stept::type.
|
protected |
Definition at line 587 of file symex_target_equation.cpp.
References symex_target_equationt::SSA_stept::cond_expr, symex_target_equationt::SSA_stept::guard, symex_target_equationt::SSA_stept::io_args, merge_irep, symex_target_equationt::SSA_stept::original_full_lhs, symex_target_equationt::SSA_stept::ssa_full_lhs, symex_target_equationt::SSA_stept::ssa_lhs, and symex_target_equationt::SSA_stept::ssa_rhs.
Referenced by assertion(), assignment(), assumption(), atomic_begin(), atomic_end(), constraint(), decl(), function_call(), function_return(), goto_instruction(), input(), location(), memory_barrier(), output(), output_fmt(), shared_read(), shared_write(), and spawn().
|
virtual |
just record output
Implements symex_targett.
Definition at line 248 of file symex_target_equation.cpp.
References symex_target_equationt::SSA_stept::guard, symex_target_equationt::SSA_stept::io_args, symex_target_equationt::SSA_stept::io_id, merge_ireps(), goto_trace_stept::OUTPUT, symex_target_equationt::SSA_stept::source, SSA_steps, and symex_target_equationt::SSA_stept::type.
Referenced by operator<<().
void symex_target_equationt::output | ( | std::ostream & | out | ) | const |
Definition at line 604 of file symex_target_equation.cpp.
|
virtual |
just record formatted output
Implements symex_targett.
Definition at line 267 of file symex_target_equation.cpp.
References symex_target_equationt::SSA_stept::format_string, symex_target_equationt::SSA_stept::formatted, symex_target_equationt::SSA_stept::guard, symex_target_equationt::SSA_stept::io_args, symex_target_equationt::SSA_stept::io_id, merge_ireps(), goto_trace_stept::OUTPUT, symex_target_equationt::SSA_stept::source, SSA_steps, and symex_target_equationt::SSA_stept::type.
|
virtual |
read from a shared variable
Implements symex_targett.
Definition at line 35 of file symex_target_equation.cpp.
References symex_target_equationt::SSA_stept::atomic_section_id, symex_target_equationt::SSA_stept::guard, merge_ireps(), goto_trace_stept::SHARED_READ, symex_target_equationt::SSA_stept::source, symex_target_equationt::SSA_stept::ssa_lhs, SSA_steps, and symex_target_equationt::SSA_stept::type.
|
virtual |
write to a sharedvariable
Implements symex_targett.
Definition at line 54 of file symex_target_equation.cpp.
References symex_target_equationt::SSA_stept::atomic_section_id, symex_target_equationt::SSA_stept::guard, merge_ireps(), goto_trace_stept::SHARED_WRITE, symex_target_equationt::SSA_stept::source, symex_target_equationt::SSA_stept::ssa_lhs, SSA_steps, and symex_target_equationt::SSA_stept::type.
spawn a new thread
Implements symex_targett.
Definition at line 73 of file symex_target_equation.cpp.
References symex_target_equationt::SSA_stept::guard, merge_ireps(), symex_target_equationt::SSA_stept::source, goto_trace_stept::SPAWN, SSA_steps, and symex_target_equationt::SSA_stept::type.
|
protected |
Definition at line 321 of file symex_target_equation.h.
Referenced by convert_io(), and merge_ireps().
|
protected |
Definition at line 318 of file symex_target_equation.h.
Referenced by operator<<(), output(), and symex_target_equationt::SSA_stept::SSA_stept().
SSA_stepst symex_target_equationt::SSA_steps |
Definition at line 286 of file symex_target_equation.h.
Referenced by partial_order_concurrencyt::add_init_writes(), assertion(), symex_slice_by_tracet::assign_merges(), assignment(), assumption(), atomic_begin(), atomic_end(), partial_order_concurrencyt::build_event_lists(), build_goto_trace(), memory_model_sct::build_per_thread_map(), fault_localizationt::collect_guards(), symex_slicet::collect_open_variables(), symex_slice_by_tracet::compute_ts_back(), constraint(), convert_assertions(), convert_assignments(), convert_assumptions(), convert_constraints(), convert_decls(), convert_goto_instructions(), convert_guards(), convert_io(), count_assertions(), count_ignored_SSA_steps(), decl(), fault_localizationt::freeze_guards(), function_call(), function_return(), counterexample_beautificationt::get_failed_property(), fault_localizationt::get_failed_property(), counterexample_beautificationt::get_minimization_list(), goto_instruction(), input(), location(), memory_barrier(), counterexample_beautificationt::operator()(), graphml_witnesst::operator()(), bmc_all_propertiest::operator()(), bmc_covert::operator()(), output(), output_fmt(), postcondition(), precondition(), memory_model_sct::program_order(), bmct::run(), fault_localizationt::run(), bmc_covert::satisfying_assignment(), shared_read(), shared_write(), bmct::show_program(), bmct::show_vcc_json(), bmct::show_vcc_plain(), simple_slice(), symex_slicet::slice(), symex_slice_by_tracet::slice_by_trace(), symex_slice_by_tracet::slice_SSA_steps(), spawn(), and memory_model_sct::thread_spawn().