Go to the documentation of this file.
35 unsigned atomic_section_id,
51 unsigned atomic_section_id,
90 unsigned atomic_section_id,
104 unsigned atomic_section_id,
109 SSA_step.
guard=guard;
118 const exprt &ssa_full_lhs,
119 const exprt &original_full_lhs,
120 const exprt &ssa_rhs,
140 const exprt &initializer,
149 SSA_step.
guard=guard;
178 SSA_step.
guard=guard;
193 SSA_step.
guard = guard;
195 for(
const auto &arg : function_arguments)
211 SSA_step.
guard = guard;
227 SSA_step.
guard=guard;
228 for(
const auto &arg : args)
229 SSA_step.
io_args.emplace_back(arg.get());
230 SSA_step.
io_id=output_id;
240 const std::list<exprt> &args)
245 SSA_step.
guard=guard;
247 SSA_step.
io_id=output_id;
258 const std::list<exprt> &args)
263 SSA_step.
guard=guard;
265 SSA_step.
io_id=input_id;
278 SSA_step.
guard=guard;
287 const std::string &msg,
293 SSA_step.
guard=guard;
308 SSA_step.
guard=guard;
316 const std::string &msg,
356 std::size_t step_index = 0;
359 if(step.is_assignment() && !step.ignore && !step.converted)
362 step.output(mstream);
363 mstream << messaget::eom;
367 step.converted =
true;
378 std::size_t step_index = 0;
381 if(step.is_decl() && !step.ignore && !step.converted)
385 decision_procedure.
handle(step.cond_expr);
386 step.converted =
true;
397 std::size_t step_index = 0;
405 step.output(mstream);
406 mstream << messaget::eom;
409 step.guard_handle = decision_procedure.
handle(step.guard);
420 std::size_t step_index = 0;
431 step.output(mstream);
432 mstream << messaget::eom;
435 step.cond_handle = decision_procedure.
handle(step.cond_expr);
448 std::size_t step_index = 0;
459 step.output(mstream);
460 mstream << messaget::eom;
463 step.cond_handle = decision_procedure.
handle(step.cond_expr);
475 std::size_t step_index = 0;
478 if(step.is_constraint() && !step.ignore && !step.converted)
481 step.output(mstream);
482 mstream << messaget::eom;
486 step.converted =
true;
497 bool optimized_for_single_assertions)
504 if(number_of_assertions==0)
507 if(number_of_assertions == 1 && optimized_for_single_assertions)
509 std::size_t step_index = 0;
513 if(step.is_assert() && step.converted)
516 if(step.is_assert() && !step.ignore && !step.converted)
518 step.converted =
true;
526 else if(step.is_assume())
542 disjuncts.reserve(number_of_assertions);
546 std::vector<goto_programt::const_targett> involved_steps;
551 if(step.is_assert() && step.converted)
554 if(step.is_assert() && !step.ignore && !step.converted)
556 step.converted =
true;
559 step.output(mstream);
560 mstream << messaget::eom;
568 step.cond_handle = decision_procedure.
handle(implication);
573 involved_steps.push_back(step.source.pc);
577 disjuncts.push_back(
not_exprt(step.cond_handle));
579 else if(step.is_assume())
584 assumption.copy_to_operands(step.cond_handle);
591 involved_steps.push_back(step.source.pc);
596 const auto assertion_disjunction =
disjunction(disjuncts);
598 decision_procedure.
set_to_true(assertion_disjunction);
610 std::size_t step_index = 0;
616 step.converted_function_arguments.reserve(step.ssa_function_arguments.size());
618 for(
const auto &arg : step.ssa_function_arguments)
620 if(arg.is_constant() ||
621 arg.id()==ID_string_constant)
622 step.converted_function_arguments.push_back(arg);
631 decision_procedure.
set_to(eq,
true);
632 conjuncts.push_back(eq);
633 step.converted_function_arguments.push_back(symbol);
640 step_index,
conjunction(conjuncts), step.source.pc);
649 std::size_t step_index = 0;
655 for(
const auto &arg : step.io_args)
657 if(arg.is_constant() ||
658 arg.id()==ID_string_constant)
659 step.converted_io_args.push_back(arg);
669 decision_procedure.
set_to(eq,
true);
670 conjuncts.push_back(eq);
671 step.converted_io_args.push_back(symbol);
678 step_index,
conjunction(conjuncts), step.source.pc);
699 for(
auto &step : SSA_step.
io_args)
713 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
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.