33 unsigned atomic_section_id,
49 unsigned atomic_section_id,
88 unsigned atomic_section_id,
102 unsigned atomic_section_id,
116 const exprt &ssa_full_lhs,
117 const exprt &original_full_lhs,
118 const exprt &ssa_rhs,
138 const exprt &initializer,
193 for(
const auto &arg : function_arguments)
226 for(
const auto &arg : args)
227 SSA_step.
io_args.emplace_back(arg.get());
228 SSA_step.
io_id=output_id;
238 const std::list<exprt> &args)
245 SSA_step.
io_id=output_id;
256 const std::list<exprt> &args)
263 SSA_step.
io_id=input_id;
286 const std::string &msg,
316 const std::string &msg,
349 const auto convert_SSA_start = std::chrono::steady_clock::now();
354 const auto convert_SSA_stop = std::chrono::steady_clock::now();
355 std::chrono::duration<double> convert_SSA_runtime =
356 std::chrono::duration<double>(convert_SSA_stop - convert_SSA_start);
357 log.
statistics() <<
"Runtime Convert SSA: " << convert_SSA_runtime.count()
364 std::size_t step_index = 0;
367 if(step.is_assignment() && !step.ignore && !step.converted)
370 step.output(mstream);
371 mstream << messaget::eom;
375 step.converted =
true;
386 std::size_t step_index = 0;
389 if(step.is_decl() && !step.ignore && !step.converted)
393 decision_procedure.
handle(step.cond_expr);
394 decision_procedure.
handle(
395 equal_exprt{step.ssa_full_lhs, step.ssa_full_lhs});
396 step.converted =
true;
407 std::size_t step_index = 0;
415 step.output(mstream);
416 mstream << messaget::eom;
419 step.guard_handle = decision_procedure.
handle(step.guard);
422 hardness.
register_ssa(step_index, step.guard, step.source.pc);
432 std::size_t step_index = 0;
443 step.output(mstream);
444 mstream << messaget::eom;
447 step.cond_handle = decision_procedure.
handle(step.cond_expr);
460 std::size_t step_index = 0;
471 step.output(mstream);
472 mstream << messaget::eom;
475 step.cond_handle = decision_procedure.
handle(step.cond_expr);
487 std::size_t step_index = 0;
490 if(step.is_constraint() && !step.ignore && !step.converted)
493 step.output(mstream);
494 mstream << messaget::eom;
498 step.converted =
true;
509 bool optimized_for_single_assertions)
516 if(number_of_assertions==0)
519 if(number_of_assertions == 1 && optimized_for_single_assertions)
521 std::size_t step_index = 0;
525 if(step.is_assert() && step.converted)
528 if(step.is_assert() && !step.ignore && !step.converted)
530 step.converted =
true;
538 else if(step.is_assume())
554 disjuncts.reserve(number_of_assertions);
558 std::vector<goto_programt::const_targett> involved_steps;
563 if(step.is_assert() && step.converted)
566 if(step.is_assert() && !step.ignore && !step.converted)
568 step.converted =
true;
571 step.output(mstream);
572 mstream << messaget::eom;
585 involved_steps.push_back(step.source.pc);
589 disjuncts.push_back(
not_exprt(step.cond_handle));
591 else if(step.is_assume())
596 assumption.copy_to_operands(step.cond_handle);
603 involved_steps.push_back(step.source.pc);
608 const auto assertion_disjunction =
disjunction(disjuncts);
610 decision_procedure.
set_to_true(assertion_disjunction);
622 std::size_t step_index = 0;
628 step.converted_function_arguments.reserve(step.ssa_function_arguments.size());
630 for(
const auto &arg : step.ssa_function_arguments)
632 if(arg.is_constant() ||
633 arg.id()==ID_string_constant)
634 step.converted_function_arguments.push_back(arg);
643 decision_procedure.
set_to(eq,
true);
644 conjuncts.push_back(eq);
645 step.converted_function_arguments.push_back(symbol);
652 step_index,
conjunction(conjuncts), step.source.pc);
661 std::size_t step_index = 0;
667 for(
const auto &arg : step.io_args)
669 if(arg.is_constant() ||
670 arg.id()==ID_string_constant)
671 step.converted_io_args.push_back(arg);
681 decision_procedure.
set_to(eq,
true);
682 conjuncts.push_back(eq);
683 step.converted_io_args.push_back(symbol);
690 step_index,
conjunction(conjuncts), step.source.pc);
711 for(
auto &step : SSA_step.
io_args)
725 out <<
"--------------\n";
static exprt guard(const exprt::operandst &guards, exprt cond)
Single SSA step in the equation.
std::vector< exprt > ssa_function_arguments
unsigned atomic_section_id
symex_targett::sourcet source
std::list< exprt > io_args
An interface for a decision procedure for satisfiability problems.
void set_to_false(const exprt &)
For a Boolean expression expr, add the constraint 'not expr'.
virtual exprt handle(const exprt &)=0
Generate a handle, which is an expression that has the same value as the argument in any model that i...
void set_to_true(const exprt &)
For a Boolean expression expr, add the constraint 'expr'.
virtual void set_to(const exprt &, bool value)=0
For a Boolean expression expr, add the constraint 'expr' if value is true, otherwise add 'not expr'.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
std::vector< exprt > operandst
The Boolean constant false.
mstreamt & statistics() 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...
Wrapper for expressions or types which have been renamed up to a given level.
const underlyingt & get() const
Expression providing an SSA-renamed symbol of expressions.
const exprt & get_original_expr() const
Expression to hold a symbol (variable)
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.
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
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.
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.
virtual void atomic_begin(const exprt &guard, unsigned atomic_section_id, const sourcet &source)
Record a beginning of an atomic section.
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.
void convert(decision_proceduret &decision_procedure)
Interface method to initiate the conversion into a decision procedure format.
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 Boolean constant true.
static exprt implication(exprt lhs, exprt rhs)
static void with_solver_hardness(decision_proceduret &maybe_hardness_collector, std::function< void(solver_hardnesst &hardness)> handler)
#define UNREACHABLE
This should be used to mark dead code.
#define PRECONDITION(CONDITION)
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
exprt disjunction(const exprt::operandst &op)
1) generates a disjunction for two or more operands 2) for one operand, returns the operand 3) return...
API to expression classes.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
A structure that facilitates collecting the complexity statistics from a decision procedure.
void register_ssa(std::size_t ssa_index, const exprt &ssa_expression, goto_programt::const_targett pc)
Called from the symtex_target_equationt::convert_*, this function associates an SSA step to all the s...
void register_assertion_ssas(const exprt &ssa_expression, const std::vector< goto_programt::const_targett > &pcs)
Called from the symtex_target_equationt::convert_assertions, this function associates the disjunction...
void register_ssa_size(std::size_t size)
Identifies source in the context of symbolic execution.
goto_programt::const_targett pc
static std::function< void(solver_hardnesst &)> hardness_register_ssa(std::size_t step_index, const SSA_stept &step)
Generate Equation using Symbolic Execution.