12 #ifndef CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_H
13 #define CPROVER_GOTO_SYMEX_SYMEX_TARGET_EQUATION_H
37 :
log(message_handler)
47 unsigned atomic_section_id,
54 unsigned atomic_section_id,
61 const exprt &ssa_full_lhs,
62 const exprt &original_full_lhs,
71 const exprt &initializer,
114 const std::list<exprt> &args);
121 const std::list<exprt> &args);
134 const std::string &msg,
146 const std::string &msg,
162 unsigned atomic_section_id,
168 unsigned atomic_section_id,
207 bool optimized_for_single_assertions =
true);
236 return narrow_cast<std::size_t>(std::count_if(
238 return step.is_assert() && !step.ignore && !step.converted;
244 return narrow_cast<std::size_t>(std::count_if(
255 SSA_stepst::iterator it=
SSA_steps.begin();
264 void output(std::ostream &out)
const;
275 return step.source.thread_nr != 0;
282 step.validate(ns, vm);
300 const symex_target_equationt::SSA_stepst::const_iterator a,
301 const symex_target_equationt::SSA_stepst::const_iterator b)
static exprt guard(const exprt::operandst &guards, exprt cond)
Single SSA step in the equation.
An interface for a decision procedure for satisfiability problems.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
Class that provides messages with a built-in verbosity 'level'.
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
Wrapper for expressions or types which have been renamed up to a given level.
Expression providing an SSA-renamed symbol of expressions.
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
virtual void constraint(const exprt &cond, const std::string &msg, const sourcet &source)
Record a global constraint: there is no guard limiting its scope.
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...
virtual void assertion(const exprt &guard, const exprt &cond, const irep_idt &property_id, const std::string &msg, const sourcet &source)
Record an assertion.
virtual void input(const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)
Record an input.
exprt make_expression() const
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< renamedt< exprt, L2 >> &args)
Record an output.
std::size_t count_assertions() const
SSA_stepst::iterator get_SSA_step(std::size_t s)
void convert_decls(decision_proceduret &decision_procedure)
Converts declarations: these are effectively ignored by the decision procedure.
std::size_t argument_count
void convert_assumptions(decision_proceduret &decision_procedure)
Converts assumptions: convert the expression the assumption represents.
std::size_t count_ignored_SSA_steps() const
void convert_without_assertions(decision_proceduret &decision_procedure)
Interface method to initiate the conversion into a decision procedure format.
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)
Record an assumption.
void validate(const namespacet &ns, const validation_modet vm) const
virtual void atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record a beginning of an atomic section.
std::list< SSA_stept > SSA_stepst
virtual void spawn(const exprt &guard, const sourcet &source)
Record spawning a new thread.
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...
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.
virtual void function_return(const exprt &guard, const irep_idt &function_id, const sourcet &source, bool hidden)
Record return from a function.
virtual void atomic_end(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record ending an atomic section.
void convert_assignments(decision_proceduret &decision_procedure)
Converts assignments: set the equality lhs==rhs to True.
void merge_ireps(SSA_stept &SSA_step)
Merging causes identical ireps to be shared.
void convert_guards(decision_proceduret &decision_procedure)
Converts guards: convert the expression the guard represents.
virtual void goto_instruction(const exprt &guard, const renamedt< exprt, L2 > &cond, const sourcet &source)
Record a goto instruction.
symex_target_equationt(message_handlert &message_handler)
void convert(decision_proceduret &decision_procedure)
Interface method to initiate the conversion into a decision procedure format.
virtual ~symex_target_equationt()=default
virtual void dead(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source)
Remove a variable from the scope.
virtual void location(const exprt &guard, const sourcet &source)
Record a location.
void convert_io(decision_proceduret &decision_procedure)
Converts I/O: for each argument build an equality between its symbol and the argument itself.
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.
void convert_function_calls(decision_proceduret &decision_procedure)
Converts function calls: for each argument build an equality between its symbol and the argument itse...
void convert_constraints(decision_proceduret &decision_procedure)
Converts constraints: set the represented condition to True.
void convert_goto_instructions(decision_proceduret &decision_procedure)
Converts goto instructions: convert the expression representing the condition of this goto.
virtual void memory_barrier(const exprt &guard, const sourcet &source)
Record creating a memory barrier.
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.
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.
void convert_assertions(decision_proceduret &decision_procedure, bool optimized_for_single_assertions=true)
Converts assertions: build a disjunction of negated assertions.
The interface of the target container for symbolic execution to record its symbolic steps into.
#define PRECONDITION(CONDITION)
Identifies source in the context of symbolic execution.
Generate Equation using Symbolic Execution.
bool operator<(const symex_target_equationt::SSA_stepst::const_iterator a, const symex_target_equationt::SSA_stepst::const_iterator b)