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,
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.
status() <<
"Runtime Convert SSA: " << convert_SSA_runtime.count() <<
"s"
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 step.converted =
true;
405 std::size_t step_index = 0;
413 step.output(mstream);
414 mstream << messaget::eom;
417 step.guard_handle = decision_procedure.
handle(step.guard);
428 std::size_t step_index = 0;
439 step.output(mstream);
440 mstream << messaget::eom;
443 step.cond_handle = decision_procedure.
handle(step.cond_expr);
456 std::size_t step_index = 0;
467 step.output(mstream);
468 mstream << messaget::eom;
471 step.cond_handle = decision_procedure.
handle(step.cond_expr);
483 std::size_t step_index = 0;
486 if(step.is_constraint() && !step.ignore && !step.converted)
489 step.output(mstream);
490 mstream << messaget::eom;
494 step.converted =
true;
505 bool optimized_for_single_assertions)
512 if(number_of_assertions==0)
515 if(number_of_assertions == 1 && optimized_for_single_assertions)
517 std::size_t step_index = 0;
521 if(step.is_assert() && step.converted)
524 if(step.is_assert() && !step.ignore && !step.converted)
526 step.converted =
true;
534 else if(step.is_assume())
550 disjuncts.reserve(number_of_assertions);
554 std::vector<goto_programt::const_targett> involved_steps;
559 if(step.is_assert() && step.converted)
562 if(step.is_assert() && !step.ignore && !step.converted)
564 step.converted =
true;
567 step.output(mstream);
568 mstream << messaget::eom;
576 step.cond_handle = decision_procedure.
handle(implication);
581 involved_steps.push_back(step.source.pc);
585 disjuncts.push_back(
not_exprt(step.cond_handle));
587 else if(step.is_assume())
592 assumption.copy_to_operands(step.cond_handle);
599 involved_steps.push_back(step.source.pc);
604 const auto assertion_disjunction =
disjunction(disjuncts);
606 decision_procedure.
set_to_true(assertion_disjunction);
618 std::size_t step_index = 0;
624 step.converted_function_arguments.reserve(step.ssa_function_arguments.size());
626 for(
const auto &arg : step.ssa_function_arguments)
628 if(arg.is_constant() ||
629 arg.id()==ID_string_constant)
630 step.converted_function_arguments.push_back(arg);
639 decision_procedure.
set_to(eq,
true);
640 conjuncts.push_back(eq);
641 step.converted_function_arguments.push_back(symbol);
648 step_index,
conjunction(conjuncts), step.source.pc);
657 std::size_t step_index = 0;
663 for(
const auto &arg : step.io_args)
665 if(arg.is_constant() ||
666 arg.id()==ID_string_constant)
667 step.converted_io_args.push_back(arg);
677 decision_procedure.
set_to(eq,
true);
678 conjuncts.push_back(eq);
679 step.converted_io_args.push_back(symbol);
686 step_index,
conjunction(conjuncts), step.source.pc);
707 for(
auto &step : SSA_step.
io_args)
721 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.