Go to the documentation of this file.
37 unsigned atomic_section_id,
53 unsigned atomic_section_id,
92 unsigned atomic_section_id,
106 unsigned atomic_section_id,
111 SSA_step.
guard=guard;
120 const exprt &ssa_full_lhs,
121 const exprt &original_full_lhs,
122 const exprt &ssa_rhs,
142 const exprt &initializer,
151 SSA_step.
guard=guard;
180 SSA_step.
guard=guard;
195 SSA_step.
guard = guard;
197 for(
const auto &arg : function_arguments)
213 SSA_step.
guard = guard;
229 SSA_step.
guard=guard;
230 for(
const auto &arg : args)
231 SSA_step.
io_args.emplace_back(arg.get());
232 SSA_step.
io_id=output_id;
242 const std::list<exprt> &args)
247 SSA_step.
guard=guard;
249 SSA_step.
io_id=output_id;
260 const std::list<exprt> &args)
265 SSA_step.
guard=guard;
267 SSA_step.
io_id=input_id;
280 SSA_step.
guard=guard;
289 const std::string &msg,
295 SSA_step.
guard=guard;
310 SSA_step.
guard=guard;
318 const std::string &msg,
351 const auto convert_SSA_start = std::chrono::steady_clock::now();
356 const auto convert_SSA_stop = std::chrono::steady_clock::now();
357 std::chrono::duration<double> convert_SSA_runtime =
358 std::chrono::duration<double>(convert_SSA_stop - convert_SSA_start);
359 log.
status() <<
"Runtime Convert SSA: " << convert_SSA_runtime.count() <<
"s"
366 std::size_t step_index = 0;
369 if(step.is_assignment() && !step.ignore && !step.converted)
372 step.output(mstream);
373 mstream << messaget::eom;
377 step.converted =
true;
388 std::size_t step_index = 0;
391 if(step.is_decl() && !step.ignore && !step.converted)
395 decision_procedure.
handle(step.cond_expr);
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);
430 std::size_t step_index = 0;
441 step.output(mstream);
442 mstream << messaget::eom;
445 step.cond_handle = decision_procedure.
handle(step.cond_expr);
458 std::size_t step_index = 0;
469 step.output(mstream);
470 mstream << messaget::eom;
473 step.cond_handle = decision_procedure.
handle(step.cond_expr);
485 std::size_t step_index = 0;
488 if(step.is_constraint() && !step.ignore && !step.converted)
491 step.output(mstream);
492 mstream << messaget::eom;
496 step.converted =
true;
507 bool optimized_for_single_assertions)
514 if(number_of_assertions==0)
517 if(number_of_assertions == 1 && optimized_for_single_assertions)
519 std::size_t step_index = 0;
523 if(step.is_assert() && step.converted)
526 if(step.is_assert() && !step.ignore && !step.converted)
528 step.converted =
true;
536 else if(step.is_assume())
552 disjuncts.reserve(number_of_assertions);
556 std::vector<goto_programt::const_targett> involved_steps;
561 if(step.is_assert() && step.converted)
564 if(step.is_assert() && !step.ignore && !step.converted)
566 step.converted =
true;
569 step.output(mstream);
570 mstream << messaget::eom;
578 step.cond_handle = decision_procedure.
handle(implication);
583 involved_steps.push_back(step.source.pc);
587 disjuncts.push_back(
not_exprt(step.cond_handle));
589 else if(step.is_assume())
594 assumption.copy_to_operands(step.cond_handle);
601 involved_steps.push_back(step.source.pc);
606 const auto assertion_disjunction =
disjunction(disjuncts);
608 decision_procedure.
set_to_true(assertion_disjunction);
620 std::size_t step_index = 0;
626 step.converted_function_arguments.reserve(step.ssa_function_arguments.size());
628 for(
const auto &arg : step.ssa_function_arguments)
630 if(arg.is_constant() ||
631 arg.id()==ID_string_constant)
632 step.converted_function_arguments.push_back(arg);
641 decision_procedure.
set_to(eq,
true);
642 conjuncts.push_back(eq);
643 step.converted_function_arguments.push_back(symbol);
650 step_index,
conjunction(conjuncts), step.source.pc);
659 std::size_t step_index = 0;
665 for(
const auto &arg : step.io_args)
667 if(arg.is_constant() ||
668 arg.id()==ID_string_constant)
669 step.converted_io_args.push_back(arg);
679 decision_procedure.
set_to(eq,
true);
680 conjuncts.push_back(eq);
681 step.converted_io_args.push_back(symbol);
688 step_index,
conjunction(conjuncts), step.source.pc);
709 for(
auto &step : SSA_step.
io_args)
723 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.
Generate Equation using Symbolic Execution.
void register_ssa_size(std::size_t size)
exprt conjunction(const exprt::operandst &op)
1) generates a conjunction for two or more operands 2) for one operand, returns the operand 3) return...
Capability to collect the statistics of the complexity of individual solver queries.
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.
goto_programt::const_targett pc
mstreamt & status() const
std::function< void(solver_hardnesst &)> handlert
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.
symex_targett::sourcet source
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
Decision Procedure Interface.
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.
static hardness_collectort::handlert hardness_register_ssa(std::size_t step_index, const SSA_stept &step)
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...
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...
virtual void spawn(const exprt &guard, const sourcet &source)
Record spawning a new thread.
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 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.
A structure that facilitates collecting the complexity statistics from a decision procedure.
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.
API to expression classes.
void with_solver_hardness(T &maybe_hardness_collector, hardness_collectort::handlert handler)
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.