Go to the documentation of this file.
31 const exprt &original_guard,
32 const exprt &new_guard,
78 const exprt &other_operand,
84 expr_try_dynamic_cast<constant_exprt>(other_operand);
88 other_without_typecast.
id() != ID_address_of &&
89 (!constant_expr || constant_expr->
get_value() != ID_NULL))
95 expr_try_dynamic_cast<ssa_exprt>(symbol_expr);
99 const std::vector<exprt> value_set_elements =
102 bool constant_found =
false;
104 for(
const auto &value_set_element : value_set_elements)
107 value_set_element.id() == ID_unknown ||
108 value_set_element.id() == ID_invalid ||
120 value_set_element,
false, language_mode))
127 value_set_element, symbol_expr, ns);
131 constant_found =
true;
142 return operation == ID_equal ? make_renamed<L2>(
false_exprt{})
145 else if(value_set_elements.size() == 1)
149 return operation == ID_equal ? make_renamed<L2>(
true_exprt{})
171 const exprt &expr = renamed_expr.
get();
173 if(expr.
id() != ID_equal && expr.
id() != ID_notequal)
184 expr_try_dynamic_cast<symbol_exprt>(lhs);
193 expr.
id(), *symbol_expr_lhs, rhs, value_set, language_mode, ns);
206 expr, value_set, language_mode, ns);
225 new_guard = renamed_guard.
get();
239 !instruction.
targets.empty(),
"goto should have at least one target");
243 instruction.
targets.size() == 1,
"no support for non-deterministic gotos");
260 goto_target->is_goto() && new_guard.
is_true())))
314 instruction.
targets.size() > 0,
315 "Instruction is an unconditional goto with no target: " +
326 new_state_pc=goto_target;
332 while(state_pc!=goto_target && !state_pc->is_target())
335 if(state_pc==goto_target)
345 state_pc=goto_target;
356 "Tried to explore the other path of a branch, but the next "
357 "instruction along that path is not the same as the instruction "
358 "that we saved at the branch point. Saved instruction is " +
360 "\nwe were intending "
362 new_state_pc->code.pretty() +
364 "instruction we think we saw on a previous path exploration is " +
365 state_pc->code.pretty());
367 new_state_pc = state_pc;
375 log.
debug() <<
"Resuming from next instruction '"
394 log.
debug() <<
"Saving next instruction '"
397 log.
debug() <<
"Saving jump target '"
422 goto_state_list.emplace_back(state.
source, std::move(state));
431 goto_state_list.emplace_back(state.
source, state);
440 auto &taken_state = backward ? state : goto_state_list.back().second;
441 auto ¬_taken_state = backward ? goto_state_list.back().second : state;
456 new_guard.
id() == ID_symbol ||
457 (new_guard.
id() == ID_not &&
460 guard_expr=new_guard;
471 state.
assignment(std::move(new_lhs), new_rhs,
ns,
true,
false).get();
478 mstream <<
"Assignment to " << new_lhs.get_identifier()
479 <<
" [" << pointer_offset_bits(new_lhs.type(), ns).value_or(0) <<
" bits]"
485 new_lhs, new_lhs, guard_symbol_expr,
502 goto_statet &new_state = goto_state_list.back().second;
539 auto queue_unreachable_state_at_target = [&]() {
545 goto_state_list.emplace_back(state.
source, std::move(new_state));
558 queue_unreachable_state_at_target();
568 bool maybe_loop_head = std::any_of(
572 return predecessor->location_number > instruction.location_number;
582 queue_unreachable_state_at_target();
609 for(
auto list_it = state_list.rbegin(); list_it != state_list.rend();
612 merge_goto(list_it->first, std::move(list_it->second), state);
639 return std::move(state.
guard);
643 return std::move(goto_state.
guard);
647 return std::move(state.
guard);
659 "atomic sections differ across branches",
668 if(goto_state.reachable)
674 static_cast<goto_statet &
>(state) = std::move(goto_state);
685 state.
depth = std::min(state.
depth, goto_state.depth);
690 state.
guard = std::move(new_guard);
714 const bool do_simplify,
718 const unsigned goto_count,
719 const unsigned dest_count)
727 if(goto_count == dest_count)
733 (!dest_state.
reachable && goto_count == 0) ||
734 (!goto_state.
reachable && dest_count == 0))
763 exprt goto_state_rhs = ssa, dest_state_rhs = ssa;
766 const auto p_it = goto_state.
propagation.find(l1_identifier);
769 goto_state_rhs = *p_it;
775 const auto p_it = dest_state.
propagation.find(l1_identifier);
778 dest_state_rhs = *p_it;
792 rhs = goto_state_rhs;
794 rhs = dest_state_rhs;
795 else if(goto_count == 0)
796 rhs = dest_state_rhs;
797 else if(dest_count == 0)
798 rhs = goto_state_rhs;
808 dest_state.
assignment(ssa, rhs, ns,
true,
true).get();
813 mstream <<
"Assignment to " << new_lhs.get_identifier() <<
" ["
814 << pointer_offset_bits(new_lhs.type(), ns).value_or(0) <<
" bits]"
839 diff_guard -= dest_state.
guard;
845 for(
const auto &delta_item : delta_view)
847 const ssa_exprt &ssa = delta_item.m.first;
848 unsigned goto_count = delta_item.m.second;
849 unsigned dest_count = !delta_item.is_in_both_maps()
851 : delta_item.get_other_map_value().second;
871 for(
const auto &delta_item : delta_view)
873 if(delta_item.is_in_both_maps())
876 const ssa_exprt &ssa = delta_item.m.first;
877 unsigned goto_count = 0;
878 unsigned dest_count = delta_item.m.second;
899 const unsigned loop_number=state.
source.
pc->loop_number;
Class that provides messages with a built-in verbosity 'level'.
std::vector< delta_view_itemt > delta_viewt
Delta view of the key-value pairs in two maps.
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
bool can_cast_expr< symbol_exprt >(const exprt &base)
void get_value_set(exprt expr, value_setst::valuest &dest, const namespacet &ns) const
Gets values pointed to by expr, including following dereference operators (i.e.
void symex_assume_l2(statet &, const exprt &cond)
bool self_loops_to_assumptions
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.
Return value for build_reference_to; see that method for documentation.
const exprt & skip_typecast(const exprt &expr)
find the expression nested inside typecasts, if any
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.
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.
void symex_unreachable_goto(statet &state)
Symbolically execute a GOTO instruction in the context of unreachable code.
NODISCARD 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)
const irep_idt get_level_0() const
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...
static irep_idt guard_identifier()
bool reachable
Is this code reachable? If not we can take shortcuts such as not entering function calls,...
std::string pretty(unsigned indent=0, unsigned max_indent=0) const
goto_programt::const_targett pc
symex_target_equationt & target
The equation that this execution is building up.
bool has_saved_jump_target
This state is saved, with the PC pointing to the target of a GOTO.
path_storaget & path_storage
Symbolic execution paths to be resumed later.
Central data structure: state.
The trinary if-then-else operator.
void simplify(const namespacet &ns)
guard_managert & guard_manager
guard_managert & guard_manager
Used to create guards.
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.
Base class for all expressions.
void merge_gotos(statet &state)
Merge all branches joining at the current program point.
irep_idt get_object_name() const
symex_targett::sourcet source
NODISCARD renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)
Version of rename which is specialized for SSA exprt.
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
targetst targets
The list of successor instructions.
bool is_true() const
Return whether the expression is a constant representing true.
Expression to hold a symbol (variable)
const exprt & get_original_expr() const
const underlyingt & get() const
GOTO Symex constant propagation.
virtual bool should_stop_unwind(const symex_targett::sourcet &source, const call_stackt &context, unsigned unwind)
Determine whether to unwind a loop.
bool make_union(object_mapt &dest, const object_mapt &src) const
Merges two RHS expression sets.
bool is_false() const
Return whether the expression is a constant representing false.
Thrown when a goto program that's being processed is in an invalid format, for example passing the wr...
sharing_mapt< irep_idt, exprt > propagation
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
bool is_failed_symbol(const exprt &expr)
Return true if, and only if, expr is the result of failed dereferencing.
static irep_idt loop_id(const irep_idt &function_id, const instructiont &instruction)
Human-readable loop name.
messaget log
The messaget to write log messages to.
virtual void location(const exprt &guard, const sourcet &source)
Record a location.
Expression providing an SSA-renamed symbol of expressions.
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().
std::vector< threadt > threads
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...
call_stackt & call_stack()
bool has_saved_next_instruction
This state is saved, with the PC pointing to the next instruction of a GOTO.
#define DATA_INVARIANT(CONDITION, REASON)
This condition should be used to document that assumptions that are made on goto_functions,...
const ssa_exprt & to_ssa_expr(const exprt &expr)
Cast a generic exprt to an ssa_exprt.
virtual void symex_goto(statet &state)
Symbolically execute a GOTO instruction.
virtual void push(const patht &)=0
Add a path to resume to the storage.
unsigned depth
Distance from entry.
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...
codet code
Do not read or modify directly – use get_X() instead.
source_locationt source_location
void add(const exprt &expr)
#define PRECONDITION(CONDITION)
const irep_idt & get_identifier() const
bool doing_path_exploration
exprt boolean_negate(const exprt &src)
negate a Boolean expression, possibly removing a not_exprt, and swapping false and true
bool unwinding_assertions
std::unordered_map< irep_idt, loop_infot > loop_iterations
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
static optionalt< 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.
void phi_function(const goto_statet &goto_state, statet &dest_state)
Merge the SSA assignments from goto_state into dest_state.
const object_descriptor_exprt & to_object_descriptor_expr(const exprt &expr)
Cast an exprt to an object_descriptor_exprt.
bool empty() const
Check if map is empty.
bool simplify(exprt &expr, const namespacet &ns)
bool disjunction_may_simplify(const guard_exprt &other_guard)
Returns true if operator|= with other_guard may result in a simpler expression.
incremental_dirtyt dirty
Local variables are considered 'dirty' if they've had an address taken and therefore may be referred ...
const irep_idt & id() const
The Boolean constant false.
Stack frames – these are used for function calls and for exceptions.
nonstd::optional< T > optionalt
Information saved at a conditional goto to resume execution.
Container for data that varies per program point, e.g.
void symex_transition(goto_symext::statet &state)
Transition to the next instruction, which increments the internal program counter and initializes the...
field_sensitivityt field_sensitivity
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
std::list< std::pair< symex_targett::sourcet, goto_statet > > goto_state_listt
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
namespacet ns
Initialized just before symbolic execution begins, to point to both outer_symbol_table and the symbol...
Deprecated expression utility functions.
virtual void goto_instruction(const exprt &guard, const renamedt< exprt, L2 > &cond, const sourcet &source)
Record a goto instruction.
virtual bool check_break(const irep_idt &loop_id, unsigned unwind)
Defines condition for interrupting symbolic execution for a specific loop.
void set_level_2(std::size_t i)
symex_renaming_levelt current_names
irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use,...
bool is_divisible(const ssa_exprt &expr) const
Determine whether expr would translate to an atomic SSA expression (returns false) or a composite obj...
std::set< targett > incoming_edges
const not_exprt & to_not_expr(const exprt &expr)
Cast an exprt to an not_exprt.
unsigned atomic_section_id
Threads.
const symex_level2t & get_level2() const
virtual void vcc(const exprt &, const std::string &msg, statet &)
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...
const symex_configt symex_config
The configuration to use for this symbolic execution.
static valuet build_reference_to(const exprt &what, const exprt &pointer, const namespacet &ns)
std::stack< bool > record_events
instructionst::const_iterator const_targett
virtual void loop_bound_exceeded(statet &state, const exprt &guard)
NODISCARD 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...
goto_programt::const_targett saved_target
Identifies source in the context of symbolic execution.
std::map< goto_programt::const_targett, goto_state_listt > goto_state_map
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.
Wrapper for dirtyt that permits incremental population, ensuring each function is analysed exactly on...
The Boolean constant true.
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
A constant literal expression.
static guardt merge_state_guards(goto_statet &goto_state, goto_symex_statet &state)
This class represents an instruction in the GOTO intermediate representation.
API to expression classes.
const irep_idt & get_value() const
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
irep_idt name
The unique identifier.
targett get_target() const
Returns the first (and only) successor for the usual case of a single target.
Wrapper for expressions or types which have been renamed up to a given level.
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.
bool should_pause_symex
Set when states are pushed onto the workqueue If this flag is set at the end of a symbolic execution ...
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.