12 #ifndef CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_H 13 #define CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_H 44 unsigned atomic_section_id,
51 unsigned atomic_section_id,
58 const exprt &ssa_full_lhs,
59 const exprt &original_full_lhs,
81 const std::vector<exprt> &ssa_function_arguments,
99 const std::list<exprt> &args);
107 const std::list<exprt> &args);
114 const std::list<exprt> &args);
126 const std::string &msg,
138 const std::string &msg,
154 unsigned atomic_section_id,
160 unsigned atomic_section_id,
339 std::ostream &out) const;
349 for(SSA_stepst::const_iterator
360 for(SSA_stepst::const_iterator
373 SSA_stepst::iterator it=
SSA_steps.begin();
391 for(SSA_stepst::const_iterator it=
SSA_steps.begin();
394 if(it->source.thread_nr!=0)
403 step.validate(ns, vm);
413 const symex_target_equationt::SSA_stepst::const_iterator a,
414 const symex_target_equationt::SSA_stepst::const_iterator b)
419 #endif // CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_H const irept & get_nil_irep()
The type of an expression, extends irept.
virtual void spawn(const exprt &guard, const sourcet &source)
Record spawning a new thread.
SSA_stepst::iterator get_SSA_step(std::size_t s)
virtual void memory_barrier(const exprt &guard, const sourcet &source)
Record creating a memory barrier.
void convert(prop_convt &prop_conv)
Interface method to initiate the conversion into a decision procedure format.
unsigned atomic_section_id
bool is_atomic_end() const
bool is_function_return() const
exprt make_expression() const
void convert_assumptions(prop_convt &prop_conv)
Converts assumptions: convert the expression the assumption represents.
bool is_shared_read() const
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.
Generate Equation using Symbolic Execution.
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)
Record an assumption.
virtual void input(const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)
Record an input.
virtual void goto_instruction(const exprt &guard, const exprt &cond, const sourcet &source)
Record a goto instruction.
bool is_constraint() const
bool is_function_call() const
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
virtual void function_return(const exprt &guard, const sourcet &source, bool hidden)
Record return from a function.
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< exprt > &args)
Record an output.
assignment_typet assignment_type
std::list< exprt > converted_io_args
virtual void atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record a beginning of an atomic section.
void validate(const namespacet &ns, const validation_modet vm) const
bool is_atomic_begin() const
virtual void atomic_end(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record ending an atomic section.
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 b...
bool is_shared_write() const
void convert_function_calls(decision_proceduret &decision_procedure)
Converts function calls: for each argument build an equality between its symbol and the argument itse...
virtual void constraint(const exprt &cond, const std::string &msg, const sourcet &source)
Record a global constraint: there is no guard limiting its scope.
void convert_constraints(decision_proceduret &decision_procedure) const
Converts constraints: set the represented condition to True.
Identifies source in the context of symbolic execution.
virtual void decl(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source, assignment_typet assignment_type)
Declare a fresh variable.
The interface of the target container for symbolic execution to record its symbolic steps into...
virtual ~symex_target_equationt()=default
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
#define PRECONDITION(CONDITION)
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.
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.
dstringt has one field, an unsigned integer no which is an index into a static table of strings...
bool is_assignment() const
std::list< exprt > io_args
void convert_goto_instructions(prop_convt &prop_conv)
Converts goto instructions: convert the expression representing the condition of this goto...
literalt const_literal(bool value)
bool is_memory_barrier() const
void convert_assignments(decision_proceduret &decision_procedure) const
Converts assignments: set the equality lhs==rhs to True.
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 assignme...
virtual void assertion(const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)
Record an assertion.
void convert_assertions(prop_convt &prop_conv)
Converts assertions: build a disjunction of negated assertions.
Single SSA step in the equation.
std::list< SSA_stept > SSA_stepst
void convert_decls(prop_convt &prop_conv) const
Converts declarations: these are effectively ignored by the decision procedure.
Base class for all expressions.
bool operator<(const symex_target_equationt::SSA_stepst::const_iterator a, const symex_target_equationt::SSA_stepst::const_iterator b)
virtual void location(const exprt &guard, const sourcet &source)
Record a location.
std::size_t count_assertions() const
std::size_t count_ignored_SSA_steps() const
std::vector< exprt > ssa_function_arguments
void output(const namespacet &ns, std::ostream &out) const
void validate(const namespacet &ns, const validation_modet vm) const
Check that the SSA step is well-formed.
virtual void dead(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source)
Remove a variable from the scope.
std::vector< exprt > converted_function_arguments
void merge_ireps(SSA_stept &SSA_step)
goto_trace_stept::typet type
Expression providing an SSA-renamed symbol of expressions.
void convert_guards(prop_convt &prop_conv)
Converts guards: convert the expression the guard represents.
void convert_io(decision_proceduret &decision_procedure)
Converts I/O: for each argument build an equality between its symbol and the argument itself...