Go to the documentation of this file.
26 unsigned atomic_section_id,
42 unsigned atomic_section_id,
81 unsigned atomic_section_id,
95 unsigned atomic_section_id,
100 SSA_step.
guard=guard;
109 const exprt &ssa_full_lhs,
110 const exprt &original_full_lhs,
111 const exprt &ssa_rhs,
131 const exprt &initializer,
140 SSA_step.
guard=guard;
169 SSA_step.
guard=guard;
184 SSA_step.
guard = guard;
186 for(
const auto &arg : function_arguments)
202 SSA_step.
guard = guard;
218 SSA_step.
guard=guard;
219 for(
const auto &arg : args)
220 SSA_step.
io_args.emplace_back(arg.get());
221 SSA_step.
io_id=output_id;
231 const std::list<exprt> &args)
236 SSA_step.
guard=guard;
238 SSA_step.
io_id=output_id;
249 const std::list<exprt> &args)
254 SSA_step.
guard=guard;
256 SSA_step.
io_id=input_id;
269 SSA_step.
guard=guard;
278 const std::string &msg,
284 SSA_step.
guard=guard;
299 SSA_step.
guard=guard;
307 const std::string &msg,
345 if(step.is_assignment() && !step.ignore && !step.converted)
348 step.output(mstream);
349 mstream << messaget::eom;
353 step.converted =
true;
363 if(step.is_decl() && !step.ignore && !step.converted)
367 decision_procedure.
handle(step.cond_expr);
368 step.converted =
true;
383 step.output(mstream);
384 mstream << messaget::eom;
387 step.guard_handle = decision_procedure.
handle(step.guard);
405 step.output(mstream);
406 mstream << messaget::eom;
409 step.cond_handle = decision_procedure.
handle(step.cond_expr);
428 step.output(mstream);
429 mstream << messaget::eom;
432 step.cond_handle = decision_procedure.
handle(step.cond_expr);
443 if(step.is_constraint() && !step.ignore && !step.converted)
446 step.output(mstream);
447 mstream << messaget::eom;
451 step.converted =
true;
458 bool optimized_for_single_assertions)
465 if(number_of_assertions==0)
468 if(number_of_assertions == 1 && optimized_for_single_assertions)
473 if(step.is_assert() && step.converted)
476 if(step.is_assert() && !step.ignore && !step.converted)
478 step.converted =
true;
483 else if(step.is_assume())
493 disjuncts.reserve(number_of_assertions);
500 if(step.is_assert() && step.converted)
503 if(step.is_assert() && !step.ignore && !step.converted)
505 step.converted =
true;
508 step.output(mstream);
509 mstream << messaget::eom;
517 step.cond_handle = decision_procedure.
handle(implication);
520 disjuncts.push_back(
not_exprt(step.cond_handle));
522 else if(step.is_assume())
527 assumption.copy_to_operands(step.cond_handle);
543 step.converted_function_arguments.reserve(step.ssa_function_arguments.size());
545 for(
const auto &arg : step.ssa_function_arguments)
547 if(arg.is_constant() ||
548 arg.id()==ID_string_constant)
549 step.converted_function_arguments.push_back(arg);
558 dec_proc.
set_to(eq,
true);
559 step.converted_function_arguments.push_back(symbol);
571 for(
const auto &arg : step.io_args)
573 if(arg.is_constant() ||
574 arg.id()==ID_string_constant)
575 step.converted_io_args.push_back(arg);
585 dec_proc.
set_to(eq,
true);
586 step.converted_io_args.push_back(symbol);
606 for(
auto &step : SSA_step.
io_args)
620 out <<
"--------------\n";
#define UNREACHABLE
This should be used to mark dead code.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)
Record an assumption.
virtual void function_return(const exprt &guard, const irep_idt &function_id, const sourcet &source, bool hidden)
Record return from a function.
virtual void memory_barrier(const exprt &guard, const sourcet &source)
Record creating a memory barrier.
unsigned atomic_section_id
Single SSA step in the equation.
void convert_goto_instructions(decision_proceduret &decision_procedure)
Converts goto instructions: convert the expression representing the condition of this goto.
Base class for all expressions.
void set_to_true(const exprt &expr)
For a Boolean expression expr, add the constraint 'expr'.
std::size_t argument_count
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
Expression to hold a symbol (variable)
void convert_decls(decision_proceduret &decision_procedure)
Converts declarations: these are effectively ignored by the decision procedure.
const exprt & get_original_expr() const
const underlyingt & get() const
std::vector< exprt > ssa_function_arguments
void set_to_false(const exprt &expr)
For a Boolean expression expr, add the constraint 'not expr'.
std::list< exprt > io_args
virtual void location(const exprt &guard, const sourcet &source)
Record a location.
void convert_assignments(decision_proceduret &decision_procedure)
Converts assignments: set the equality lhs==rhs to True.
Expression providing an SSA-renamed symbol of expressions.
virtual void set_to(const exprt &expr, bool value)=0
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
virtual void atomic_end(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record ending an atomic section.
std::size_t count_assertions() const
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
#define PRECONDITION(CONDITION)
virtual void dead(const exprt &guard, const ssa_exprt &ssa_lhs, const sourcet &source)
Remove a variable from the scope.
void convert_io(decision_proceduret &decision_procedure)
Converts I/O: for each argument build an equality between its symbol and the argument itself.
std::vector< exprt > operandst
The Boolean constant false.
void convert_constraints(decision_proceduret &decision_procedure)
Converts constraints: set the represented condition to True.
virtual exprt handle(const exprt &expr)=0
Generate a handle, which is an expression that has the same value as the argument in any model that i...
virtual void spawn(const exprt &guard, const sourcet &source)
Record spawning a new thread.
void convert_guards(decision_proceduret &decision_procedure)
Converts guards: convert the expression the guard represents.
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...
void merge_ireps(SSA_stept &SSA_step)
Merging causes identical ireps to be shared.
virtual void atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record a beginning of an atomic section.
void convert_assertions(decision_proceduret &decision_procedure, bool optimized_for_single_assertions=true)
Converts assertions: build a disjunction of negated assertions.
virtual void assertion(const exprt &guard, const exprt &cond, const std::string &msg, const sourcet &source)
Record an assertion.
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 goto_instruction(const exprt &guard, const renamedt< exprt, L2 > &cond, const sourcet &source)
Record a goto instruction.
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.
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 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...
void convert(decision_proceduret &decision_procedure)
Interface method to initiate the conversion into a decision procedure format.
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...
void convert_without_assertions(decision_proceduret &decision_procedure)
Interface method to initiate the conversion into a decision procedure format.
virtual void constraint(const exprt &cond, const std::string &msg, const sourcet &source)
Record a global constraint: there is no guard limiting its scope.
Identifies source in the context of symbolic execution.
void convert_assumptions(decision_proceduret &decision_procedure)
Converts assumptions: convert the expression the assumption represents.
The Boolean constant true.
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.
Wrapper for expressions or types which have been renamed up to a given level.
virtual void input(const exprt &guard, const sourcet &source, const irep_idt &input_id, const std::list< exprt > &args)
Record an input.
virtual void output(const exprt &guard, const sourcet &source, const irep_idt &output_id, const std::list< renamedt< exprt, L2 >> &args)
Record an output.
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.