224 expr, value_set, language_mode, ns);
257 !instruction.
targets.empty(),
"goto should have at least one target");
261 instruction.
targets.size() == 1,
"no support for non-deterministic gotos");
285 << state.
source.
pc->source_location() <<
" by assume("
291 <<
"no unwinding assertion will be generated for self-loop at "
341 instruction.
targets.size() > 0,
342 "Instruction is an unconditional goto with no target: " +
343 instruction.
code().pretty());
383 "Tried to explore the other path of a branch, but the next "
384 "instruction along that path is not the same as the instruction "
385 "that we saved at the branch point. Saved instruction is " +
387 "\nwe were intending "
391 "instruction we think we saw on a previous path exploration is " +
402 log.
debug() <<
"Resuming from next instruction '"
421 log.
debug() <<
"Saving next instruction '"
424 log.
debug() <<
"Saving jump target '"
425 <<
jump_target.state.saved_target->source_location() <<
"'"
505 mstream <<
"Assignment to " << new_lhs.get_identifier()
506 <<
" [" << pointer_offset_bits(new_lhs.type(), ns).value_or(0) <<
" bits]"
599 return predecessor->location_number > instruction.location_number;
666 return std::move(state.
guard);
674 return std::move(state.
guard);
686 "atomic sections differ across branches",
687 state.
source.
pc->source_location());
741 const bool do_simplify,
842 log.conditional_output(
844 mstream <<
"Assignment to " << new_lhs.get_identifier() <<
" ["
845 << pointer_offset_bits(new_lhs.type(), ns).value_or(0) <<
" bits]"
864 goto_state.get_level2().current_names.empty() &&
865 dest_state.get_level2().current_names.empty())
873 goto_state.get_level2().current_names.get_delta_view(
899 dest_state.get_level2().current_names.get_delta_view(
930 const std::string loop_number = std::to_string(state.
source.
pc->loop_number);
937 const std::string property_id =
939 ".unwind." + loop_number;
943 "unwinding assertion loop " + loop_number,
bool is_failed_symbol(const exprt &expr)
Return true if, and only if, expr is the result of failed dereferencing.
static exprt guard(const exprt::operandst &guards, exprt cond)
virtual void clear()
Reset the abstract state.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
A constant literal expression.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
Base class for all expressions.
The Boolean constant false.
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? If not we can take shortcuts such as not entering function calls,...
unsigned atomic_section_id
Threads.
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
Central data structure: state.
goto_programt::const_targett saved_target
call_stackt & call_stack()
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...
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.
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.
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.
path_storaget & path_storage
Symbolic execution paths to be resumed later.
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)
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...
const irep_idt & id() const
Class that provides messages with a built-in verbosity 'level'.
mstreamt & statistics() const
mstreamt & warning() 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...
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().
incremental_dirtyt dirty
Local variables are considered 'dirty' if they've had an address taken and therefore may be referred ...
virtual void push(const patht &)=0
Add a path to resume to the storage.
std::vector< delta_view_itemt > delta_viewt
Delta view of the key-value pairs in two maps.
Expression providing an SSA-renamed symbol of expressions.
Expression to hold a symbol (variable)
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 goto_instruction(const exprt &guard, const renamedt< exprt, L2 > &cond, const sourcet &source)
Record a goto instruction.
virtual void location(const exprt &guard, const sourcet &source)
Record a location.
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.
static exprt conditional_cast(const exprt &expr, const typet &type)
Return value for build_reference_to; see that method for documentation.
static valuet build_reference_to(const exprt &what, const exprt &pointer, const namespacet &ns)
static bool should_ignore_value(const exprt &what, bool exclude_null_derefs, const irep_idt &language_mode)
Determine whether possible alias what should be ignored when replacing a pointer by its referees.
State type in value_set_domaint, used in value-set analysis and goto-symex.
std::vector< exprt > get_value_set(exprt expr, const namespacet &ns) const
Gets values pointed to by expr, including following dereference operators (i.e.
bool make_union(object_mapt &dest, const object_mapt &src) const
Merges two RHS expression sets.
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
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...
renamedt< exprt, L2 > try_evaluate_pointer_comparisons(renamedt< exprt, L2 > condition, const value_sett &value_set, const irep_idt &language_mode, const namespacet &ns)
Try to evaluate pointer comparisons where they can be trivially determined using the value-set.
GOTO Symex constant propagation.
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.
API to expression classes for Pointers.
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
void selectively_mutate(renamedt< exprt, level > &renamed, typename renamedt< exprt, level >::mutator_functiont get_mutated_expr)
This permits replacing subexpressions of the renamed value, so long as each replacement is consistent...
bool simplify(exprt &expr, const namespacet &ns)
exprt simplify_expr(exprt src, 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 binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
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.
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 unsigned goto_count, const unsigned dest_count)
Helper function for phi_function which merges the names of an identifier for two different states.
static std::optional< renamedt< exprt, L2 > > try_evaluate_pointer_comparison(const irep_idt &operation, const symbol_exprt &symbol_expr, const exprt &other_operand, const value_sett &value_set, const irep_idt language_mode, const namespacet &ns)
Try to evaluate a simple pointer comparison.
renamedt< exprt, L2 > try_evaluate_pointer_comparisons(renamedt< exprt, L2 > condition, const value_sett &value_set, const irep_idt &language_mode, const namespacet &ns)
Try to evaluate pointer comparisons where they can be trivially determined using the value-set.
static guardt merge_state_guards(goto_statet &goto_state, goto_symex_statet &state)