34 unsigned atomic_section_id,
52 unsigned atomic_section_id,
97 unsigned atomic_section_id,
102 SSA_step.
guard=guard;
113 unsigned atomic_section_id,
118 SSA_step.
guard=guard;
129 const exprt &ssa_full_lhs,
130 const exprt &original_full_lhs,
131 const exprt &ssa_rhs,
140 SSA_step.
guard=guard;
167 SSA_step.
guard=guard;
198 SSA_step.
guard=guard;
207 const irep_idt &function_identifier,
208 const std::vector<exprt> &ssa_function_arguments,
215 SSA_step.
guard = guard;
233 SSA_step.
guard = guard;
245 const std::list<exprt> &args)
250 SSA_step.
guard=guard;
254 SSA_step.
io_id=output_id;
264 const std::list<exprt> &args)
269 SSA_step.
guard=guard;
273 SSA_step.
io_id=output_id;
284 const std::list<exprt> &args)
289 SSA_step.
guard=guard;
293 SSA_step.
io_id=input_id;
306 SSA_step.
guard=guard;
317 const std::string &msg,
323 SSA_step.
guard=guard;
340 SSA_step.
guard=guard;
350 const std::string &msg,
394 if(step.is_assignment() && !step.ignore)
397 decision_procedure.
debug(),
399 step.output(mstream);
413 if(step.is_decl() && !step.ignore)
419 prop_conv.
convert(step.cond_expr);
425 "Error converting decls for step", step));
443 step.output(mstream);
449 step.guard_literal = prop_conv.
convert(step.guard);
455 "Error converting guard for step", step));
475 step.output(mstream);
481 step.cond_literal = prop_conv.
convert(step.cond_expr);
487 "Error converting assumptions for step", step));
508 step.output(mstream);
514 step.cond_literal = prop_conv.
convert(step.cond_expr);
520 "Error converting goto instructions for step", step));
532 if(step.is_constraint())
537 decision_procedure.
debug(),
539 step.output(mstream);
551 "Error converting constraints for step", step));
566 if(number_of_assertions==0)
569 if(number_of_assertions==1)
579 else if(step.is_assume())
589 disjuncts.reserve(number_of_assertions);
600 step.output(mstream);
611 step.cond_literal = prop_conv.
convert(implication);
617 "Error converting assertions for step", step));
623 else if(step.is_assume())
642 std::size_t argument_count=0;
647 step.converted_function_arguments.reserve(step.ssa_function_arguments.size());
649 for(
const auto &arg : step.ssa_function_arguments)
651 if(arg.is_constant() ||
652 arg.id()==ID_string_constant)
653 step.converted_function_arguments.push_back(arg);
662 dec_proc.
set_to(eq,
true);
663 step.converted_function_arguments.push_back(symbol);
672 std::size_t io_count=0;
677 for(
const auto &arg : step.io_args)
679 if(arg.is_constant() ||
680 arg.id()==ID_string_constant)
681 step.converted_io_args.push_back(arg);
685 symbol.
type()=arg.type();
691 dec_proc.
set_to(eq,
true);
692 step.converted_io_args.push_back(symbol);
709 for(
auto &step : SSA_step.
io_args)
724 step.output(ns, out);
725 out <<
"--------------\n";
731 std::ostream &out)
const 737 if(
source.
pc->source_location.is_not_nil())
738 out <<
" " <<
source.
pc->source_location <<
'\n';
752 out <<
"LOCATION" <<
'\n';
break;
754 out <<
"INPUT" <<
'\n';
break;
756 out <<
"OUTPUT" <<
'\n';
break;
759 out <<
"DECL" <<
'\n';
764 out <<
"ASSIGNMENT (";
774 out <<
"VISIBLE_ACTUAL_PARAMETER";
777 out <<
"HIDDEN_ACTUAL_PARAMETER";
794 out <<
"DEAD\n";
break;
796 out <<
"FUNCTION_CALL\n";
break;
798 out <<
"FUNCTION_RETURN\n";
break;
800 out <<
"CONSTRAINT\n";
break;
802 out <<
"SHARED READ\n";
break;
804 out <<
"SHARED WRITE\n";
break;
806 out <<
"ATOMIC_BEGIN\n";
break;
808 out <<
"AUTOMIC_END\n";
break;
810 out <<
"SPAWN\n";
break;
812 out <<
"MEMORY_BARRIER\n";
break;
836 out <<
"Thread " << source.thread_nr;
838 if(source.pc->source_location.is_not_nil())
839 out <<
" " << source.pc->source_location <<
'\n';
847 out <<
"ASSERT " <<
format(cond_expr) <<
'\n';
850 out <<
"ASSUME " <<
format(cond_expr) <<
'\n';
853 out <<
"LOCATION" <<
'\n';
856 out <<
"INPUT" <<
'\n';
859 out <<
"OUTPUT" <<
'\n';
863 out <<
"DECL" <<
'\n';
864 out <<
format(ssa_lhs) <<
'\n';
868 out <<
"ASSIGNMENT (";
869 switch(assignment_type)
878 out <<
"VISIBLE_ACTUAL_PARAMETER";
881 out <<
"HIDDEN_ACTUAL_PARAMETER";
901 out <<
"FUNCTION_CALL\n";
904 out <<
"FUNCTION_RETURN\n";
907 out <<
"CONSTRAINT\n";
910 out <<
"SHARED READ\n";
913 out <<
"SHARED WRITE\n";
916 out <<
"ATOMIC_BEGIN\n";
919 out <<
"AUTOMIC_END\n";
925 out <<
"MEMORY_BARRIER\n";
928 out <<
"IF " <<
format(cond_expr) <<
" GOTO\n";
935 if(is_assert() || is_assume() || is_assignment() || is_constraint())
936 out <<
format(cond_expr) <<
'\n';
938 if(is_assert() || is_constraint())
941 if(is_shared_read() || is_shared_write())
942 out <<
format(ssa_lhs) <<
'\n';
944 out <<
"Guard: " <<
format(guard) <<
'\n';
973 "Type inequality in SSA assignment\nlhs-type: " +
974 ssa_lhs.get_original_expr().type().id_string() +
975 "\nrhs-type: " + ssa_rhs.type().id_string());
979 for(
const auto &expr : io_args)
983 for(
const auto &expr : ssa_function_arguments)
990 called_function.empty() || !ns.
lookup(called_function, symbol),
991 "unknown function identifier " +
id2string(called_function));
virtual void spawn(const exprt &guard, const sourcet &source)
Record spawning a new thread.
virtual void memory_barrier(const exprt &guard, const sourcet &source)
Record creating a memory barrier.
const std::string & id2string(const irep_idt &d)
Generate Equation using Symbolic Execution.
goto_programt::const_targett pc
void convert(prop_convt &prop_conv)
Interface method to initiate the conversion into a decision procedure format.
unsigned atomic_section_id
std::string comment(const rw_set_baset::entryt &entry, bool write)
void convert_assumptions(prop_convt &prop_conv)
Converts assumptions: convert the expression the assumption represents.
bool base_type_eq(const typet &type1, const typet &type2, const namespacet &ns)
Check types for equality across all levels of hierarchy.
bool is_shared_read() const
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
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.
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
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
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.
typet & type()
Return the type of the expression.
assignment_typet assignment_type
virtual void atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record a beginning of an atomic section.
std::string unwrap_exception(const std::exception &e, int level)
Given a potentially nested exception, produce a string with all of nested exceptions information...
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...
The Boolean constant true.
virtual void constraint(const exprt &cond, const std::string &msg, const sourcet &source)
Record a global constraint: there is no guard limiting its scope.
Exceptions that can be raised during the equation conversion phase.
void util_throw_with_nested(T &&t)
void convert_constraints(decision_proceduret &decision_procedure) const
Converts constraints: set the represented condition to True.
Identifies source in the context of symbolic execution.
void validate_full_expr(const exprt &expr, const namespacet &ns, const validation_modet vm)
Check that the given expression is well-formed (full check, including checks of all subexpressions an...
virtual void decl(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source, assignment_typet assignment_type)
Declare a fresh variable.
Exceptions that can be raised in bv_conversion.
API to expression classes.
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 literalt convert(const exprt &expr)=0
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 set_to(const exprt &expr, bool value)=0
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
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
std::vector< exprt > operandst
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)
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.
void set_to_false(const exprt &expr)
Single SSA step in the equation.
void convert_decls(prop_convt &prop_conv) const
Converts declarations: these are effectively ignored by the decision procedure.
Base class for all expressions.
void set_to_true(const exprt &expr)
const exprt & get_original_expr() const
void conditional_output(mstreamt &mstream, const std::function< void(mstreamt &)> &output_generator) const
Generate output to message_stream using output_generator if the configured verbosity is at least as h...
#define UNREACHABLE
This should be used to mark dead code.
virtual void location(const exprt &guard, const sourcet &source)
Record a location.
std::size_t count_assertions() const
void set_identifier(const irep_idt &identifier)
#define DATA_CHECK(vm, condition, message)
This macro takes a condition which denotes a well-formedness criterion on goto programs, expressions, instructions, etc.
Expression to hold a symbol (variable)
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.
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.
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
void convert_io(decision_proceduret &decision_procedure)
Converts I/O: for each argument build an equality between its symbol and the argument itself...