31 const exprt &original_guard,
32 const exprt &new_guard,
81 new_guard = renamed_guard.
get();
95 !instruction.
targets.empty(),
"goto should have at least one target");
99 instruction.
targets.size() == 1,
"no support for non-deterministic gotos");
116 goto_target->is_goto() && new_guard.
is_true())))
122 log.statistics() <<
"replacing self-loop at "
123 << state.
source.
pc->source_location() <<
" by assume("
129 <<
"no unwinding assertion will be generated for self-loop at "
179 instruction.
targets.size() > 0,
180 "Instruction is an unconditional goto with no target: " +
191 new_state_pc=goto_target;
197 while(state_pc!=goto_target && !state_pc->is_target())
200 if(state_pc==goto_target)
210 state_pc=goto_target;
221 "Tried to explore the other path of a branch, but the next "
222 "instruction along that path is not the same as the instruction "
223 "that we saved at the branch point. Saved instruction is " +
225 "\nwe were intending "
227 new_state_pc->code().pretty() +
229 "instruction we think we saw on a previous path exploration is " +
230 state_pc->code().pretty());
232 new_state_pc = state_pc;
235 log.debug() <<
"Resuming from jump target '" << state_pc->source_location()
240 log.debug() <<
"Resuming from next instruction '"
241 << state_pc->source_location() <<
"'" <<
log.eom;
259 log.debug() <<
"Saving next instruction '"
262 log.debug() <<
"Saving jump target '"
265 path_storage.push(next_instruction);
266 path_storage.push(jump_target);
287 goto_state_list.emplace_back(state.
source, std::move(state));
296 goto_state_list.emplace_back(state.
source, state);
305 auto &taken_state = backward ? state : goto_state_list.back().second;
306 auto ¬_taken_state = backward ? goto_state_list.back().second : state;
321 new_guard.
id() == ID_symbol ||
322 (new_guard.
id() == ID_not &&
325 guard_expr=new_guard;
336 state.
assignment(std::move(new_lhs), new_rhs,
ns,
true,
false).get();
340 log.conditional_output(
343 mstream <<
"Assignment to " << new_lhs.get_identifier()
344 <<
" [" << pointer_offset_bits(new_lhs.type(), ns).value_or(0) <<
" bits]"
350 new_lhs, new_lhs, guard_symbol_expr,
367 goto_statet &new_state = goto_state_list.back().second;
404 auto queue_unreachable_state_at_target = [&]() {
410 goto_state_list.emplace_back(state.
source, std::move(new_state));
423 queue_unreachable_state_at_target();
433 bool maybe_loop_head = std::any_of(
437 return predecessor->location_number > instruction.location_number;
447 queue_unreachable_state_at_target();
474 for(
auto list_it = state_list.rbegin(); list_it != state_list.rend();
477 merge_goto(list_it->first, std::move(list_it->second), state);
504 return std::move(state.
guard);
508 return std::move(goto_state.
guard);
512 return std::move(state.
guard);
524 "atomic sections differ across branches",
525 state.
source.
pc->source_location());
533 if(goto_state.reachable)
539 static_cast<goto_statet &
>(state) = std::move(goto_state);
550 state.
depth = std::min(state.
depth, goto_state.depth);
555 state.
guard = std::move(new_guard);
579 const bool do_simplify,
583 const std::size_t goto_count,
584 const std::size_t dest_count)
592 if(goto_count == dest_count)
598 (!dest_state.
reachable && goto_count == 0) ||
599 (!goto_state.
reachable && dest_count == 0))
627 level_0 != std::to_string(dest_state.
source.
thread_nr) && dest_count != 0)
632 exprt goto_state_rhs = ssa, dest_state_rhs = ssa;
635 const auto p_it = goto_state.
propagation.find(l1_identifier);
638 goto_state_rhs = *p_it;
644 const auto p_it = dest_state.
propagation.find(l1_identifier);
647 dest_state_rhs = *p_it;
661 rhs = goto_state_rhs;
663 rhs = dest_state_rhs;
664 else if(goto_count == 0)
665 rhs = dest_state_rhs;
666 else if(dest_count == 0)
667 rhs = goto_state_rhs;
681 dest_state.
assignment(ssa, rhs, ns,
true,
true).get();
686 mstream <<
"Assignment to " << new_lhs.get_identifier() <<
" ["
687 << pointer_offset_bits(new_lhs.type(), ns).value_or(0) <<
" bits]"
712 diff_guard -= dest_state.
guard;
718 for(
const auto &delta_item : delta_view)
720 const ssa_exprt &ssa = delta_item.m.first;
721 std::size_t goto_count = delta_item.m.second;
722 std::size_t dest_count = !delta_item.is_in_both_maps()
724 : delta_item.get_other_map_value().second;
744 for(
const auto &delta_item : delta_view)
746 if(delta_item.is_in_both_maps())
749 const ssa_exprt &ssa = delta_item.m.first;
750 std::size_t goto_count = 0;
751 std::size_t dest_count = delta_item.m.second;
772 const std::string loop_number = std::to_string(state.
source.
pc->loop_number);
779 const std::string property_id =
781 ".unwind." + loop_number;
785 "unwinding assertion loop " + loop_number,
static exprt guard(const exprt::operandst &guards, exprt cond)
Base class for all expressions.
bool is_true() const
Return whether the expression is a constant representing true.
bool is_false() const
Return whether the expression is a constant representing false.
The Boolean constant false.
bool is_divisible(const ssa_exprt &expr, bool disjoined_fields_only) const
Determine whether expr would translate to an atomic SSA expression (returns false) or a composite obj...
Stack frames – these are used for function calls and for exceptions.
std::list< std::pair< symex_targett::sourcet, goto_statet > > goto_state_listt
std::unordered_map< irep_idt, loop_infot > loop_iterations
std::map< goto_programt::const_targett, goto_state_listt, goto_programt::target_less_than > goto_state_map
This class represents an instruction in the GOTO intermediate representation.
const goto_instruction_codet & code() const
Get the code represented by this instruction.
targetst targets
The list of successor instructions.
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
std::set< targett, target_less_than > incoming_edges
const exprt & condition() const
Get the condition of gotos, assume, assert.
const_targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
static irep_idt loop_id(const irep_idt &function_id, const instructiont &instruction)
Human-readable loop name.
instructionst::const_iterator const_targett
Container for data that varies per program point, e.g.
unsigned depth
Distance from entry.
bool reachable
Is this code reachable?
void apply_condition(const exprt &condition, const goto_symex_statet &previous_state, const namespacet &ns)
Given a condition that must hold on this path, propagate as much knowledge as possible.
unsigned atomic_section_id
Threads.
sharing_mapt< irep_idt, exprt > propagation
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
const symex_level2t & get_level2() const
Central data structure: state.
goto_programt::const_targett saved_target
call_stackt & call_stack()
std::stack< bool > record_events
static irep_idt guard_identifier()
renamedt< ssa_exprt, L2 > assignment(ssa_exprt lhs, const exprt &rhs, const namespacet &ns, bool rhs_is_simplified, bool record_value, bool allow_pointer_unsoundness=false)
guard_managert & guard_manager
renamedt< exprt, level > rename(exprt expr, const namespacet &ns)
Rewrites symbol expressions in exprt, applying a suffix to each symbol reflecting its most recent ver...
field_sensitivityt field_sensitivity
symex_targett::sourcet source
bool has_saved_jump_target
This state is saved, with the PC pointing to the target of a GOTO.
renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)
Version of rename which is specialized for SSA exprt.
std::vector< threadt > threads
bool has_saved_next_instruction
This state is saved, with the PC pointing to the next instruction of a GOTO.
virtual bool should_stop_unwind(const symex_targett::sourcet &source, const call_stackt &context, unsigned unwind)
Determine whether to unwind a loop.
void try_filter_value_sets(goto_symex_statet &state, exprt condition, const value_sett &original_value_set, value_sett *jump_taken_value_set, value_sett *jump_not_taken_value_set, const namespacet &ns)
Try to filter value sets based on whether possible values of a pointer-typed symbol make the conditio...
void apply_goto_condition(goto_symex_statet ¤t_state, goto_statet &jump_taken_state, goto_statet &jump_not_taken_state, const exprt &original_guard, const exprt &new_guard, const namespacet &ns)
Propagate constants and points-to information implied by a GOTO condition.
virtual bool check_break(const irep_idt &loop_id, unsigned unwind)
Defines condition for interrupting symbolic execution for a specific loop.
void symex_unreachable_goto(statet &state)
Symbolically execute a GOTO instruction in the context of unreachable code.
goto_symex_statet statet
A type abbreviation for goto_symex_statet.
irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use,...
virtual void symex_goto(statet &state)
Symbolically execute a GOTO instruction.
void phi_function(const goto_statet &goto_state, statet &dest_state)
Merge the SSA assignments from goto_state into dest_state.
symex_target_equationt & target
The equation that this execution is building up.
guard_managert & guard_manager
Used to create guards.
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
virtual void loop_bound_exceeded(statet &state, const exprt &guard)
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
virtual void vcc(const exprt &cond, const irep_idt &property_id, const std::string &msg, statet &state)
Symbolically execute a verification condition (assertion).
virtual void merge_goto(const symex_targett::sourcet &source, goto_statet &&goto_state, statet &state)
Merge a single branch, the symbolic state of which is held in goto_state, into the current overall sy...
virtual void do_simplify(exprt &expr, const value_sett &value_set)
messaget log
The messaget to write log messages to.
const symex_configt symex_config
The configuration to use for this symbolic execution.
bool should_pause_symex
Set when states are pushed onto the workqueue If this flag is set at the end of a symbolic execution ...
void symex_assume_l2(statet &, const exprt &cond)
void merge_gotos(statet &state)
Merge all branches joining at the current program point.
void add(const exprt &expr)
bool disjunction_may_simplify(const guard_exprt &other_guard)
Returns true if operator|= with other_guard may result in a simpler expression.
The trinary if-then-else operator.
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
Wrapper for dirtyt that permits incremental population, ensuring each function is analysed exactly on...
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
const irep_idt & id() const
Class that provides messages with a built-in verbosity 'level'.
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...
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
bool lookup(const irep_idt &name, const symbolt *&symbol) const override
See documentation for namespace_baset::lookup().
Wrapper for expressions or types which have been renamed up to a given level.
void simplify(simplify_exprt &simplifier)
const underlyingt & get() const
std::vector< delta_view_itemt > delta_viewt
bool empty() const
Check if map is empty.
void get_delta_view(const sharing_mapt &other, delta_viewt &delta_view, const bool only_common=true) const
Get a delta view of the elements in the map.
Expression providing an SSA-renamed symbol of expressions.
void set_level_2(std::size_t i)
const irep_idt get_level_0() const
const exprt & get_original_expr() const
irep_idt get_object_name() const
Expression to hold a symbol (variable)
const irep_idt & get_identifier() const
irep_idt name
The unique identifier.
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
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.
The Boolean constant true.
bool make_union(object_mapt &dest, const object_mapt &src) const
Merges two RHS expression sets.
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
Deprecated expression utility functions.
void symex_transition(goto_symext::statet &state)
Transition to the next instruction, which increments the internal program counter and initializes the...
const std::string & id2string(const irep_idt &d)
std::string from_expr(const namespacet &ns, const irep_idt &identifier, const exprt &expr)
Storage of symbolic execution paths to resume.
bool simplify(exprt &expr, const namespacet &ns)
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
#define PRECONDITION(CONDITION)
#define INVARIANT(CONDITION, REASON)
This macro uses the wrapper function 'invariant_violated_string'.
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
API to expression classes.
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
Information saved at a conditional goto to resume execution.
symex_renaming_levelt current_names
Identifies source in the context of symbolic execution.
goto_programt::const_targett pc
static void merge_names(const goto_statet &goto_state, goto_symext::statet &dest_state, const namespacet &ns, const guardt &diff_guard, messaget &log, const bool do_simplify, symex_target_equationt &target, const incremental_dirtyt &dirty, const ssa_exprt &ssa, const std::size_t goto_count, const std::size_t dest_count)
Helper function for phi_function which merges the names of an identifier for two different states.
static guardt merge_state_guards(goto_statet &goto_state, goto_symex_statet &state)