34 const exprt &original_guard,
35 const exprt &new_guard,
84 const exprt &other_operand,
90 expr_try_dynamic_cast<constant_exprt>(other_operand);
94 (!constant_expr || constant_expr->
get_value() != ID_NULL))
100 expr_try_dynamic_cast<ssa_exprt>(symbol_expr);
104 const std::vector<exprt> value_set_elements =
107 bool constant_found =
false;
109 for(
const auto &value_set_element : value_set_elements)
112 value_set_element.id() == ID_unknown ||
113 value_set_element.id() == ID_invalid ||
125 value_set_element,
false, language_mode))
132 value_set_element, symbol_expr, ns);
144 constant_found =
true;
160 return operation == ID_equal ? make_renamed<L2>(
false_exprt{})
163 else if(value_set_elements.size() == 1)
167 return operation == ID_equal ? make_renamed<L2>(
true_exprt{})
189 const exprt &expr = renamed_expr.
get();
191 if(expr.
id() != ID_equal && expr.
id() != ID_notequal)
202 expr_try_dynamic_cast<symbol_exprt>(lhs);
211 expr.
id(), *symbol_expr_lhs, rhs, value_set, language_mode, ns);
224 expr, value_set, language_mode, ns);
243 new_guard = renamed_guard.
get();
257 !instruction.
targets.empty(),
"goto should have at least one target");
261 instruction.
targets.size() == 1,
"no support for non-deterministic gotos");
278 goto_target->is_goto() && new_guard.
is_true())))
332 instruction.
targets.size() > 0,
333 "Instruction is an unconditional goto with no target: " +
344 new_state_pc=goto_target;
350 while(state_pc!=goto_target && !state_pc->is_target())
353 if(state_pc==goto_target)
363 state_pc=goto_target;
374 "Tried to explore the other path of a branch, but the next "
375 "instruction along that path is not the same as the instruction "
376 "that we saved at the branch point. Saved instruction is " +
378 "\nwe were intending "
380 new_state_pc->get_code().pretty() +
382 "instruction we think we saw on a previous path exploration is " +
383 state_pc->get_code().pretty());
385 new_state_pc = state_pc;
393 log.
debug() <<
"Resuming from next instruction '"
412 log.
debug() <<
"Saving next instruction '"
415 log.
debug() <<
"Saving jump target '"
440 goto_state_list.emplace_back(state.
source, std::move(state));
449 goto_state_list.emplace_back(state.
source, state);
458 auto &taken_state = backward ? state : goto_state_list.back().second;
459 auto ¬_taken_state = backward ? goto_state_list.back().second : state;
474 new_guard.
id() == ID_symbol ||
475 (new_guard.
id() == ID_not &&
478 guard_expr=new_guard;
489 state.
assignment(std::move(new_lhs), new_rhs,
ns,
true,
false).get();
496 mstream <<
"Assignment to " << new_lhs.get_identifier()
497 <<
" [" << pointer_offset_bits(new_lhs.type(), ns).value_or(0) <<
" bits]"
503 new_lhs, new_lhs, guard_symbol_expr,
520 goto_statet &new_state = goto_state_list.back().second;
557 auto queue_unreachable_state_at_target = [&]() {
563 goto_state_list.emplace_back(state.
source, std::move(new_state));
576 queue_unreachable_state_at_target();
586 bool maybe_loop_head = std::any_of(
590 return predecessor->location_number > instruction.location_number;
600 queue_unreachable_state_at_target();
627 for(
auto list_it = state_list.rbegin(); list_it != state_list.rend();
630 merge_goto(list_it->first, std::move(list_it->second), state);
657 return std::move(state.
guard);
661 return std::move(goto_state.
guard);
665 return std::move(state.
guard);
677 "atomic sections differ across branches",
686 if(goto_state.reachable)
692 static_cast<goto_statet &
>(state) = std::move(goto_state);
703 state.
depth = std::min(state.
depth, goto_state.depth);
708 state.
guard = std::move(new_guard);
732 const bool do_simplify,
736 const unsigned goto_count,
737 const unsigned dest_count)
745 if(goto_count == dest_count)
751 (!dest_state.
reachable && goto_count == 0) ||
752 (!goto_state.
reachable && dest_count == 0))
781 exprt goto_state_rhs = ssa, dest_state_rhs = ssa;
784 const auto p_it = goto_state.
propagation.find(l1_identifier);
787 goto_state_rhs = *p_it;
793 const auto p_it = dest_state.
propagation.find(l1_identifier);
796 dest_state_rhs = *p_it;
810 rhs = goto_state_rhs;
812 rhs = dest_state_rhs;
813 else if(goto_count == 0)
814 rhs = dest_state_rhs;
815 else if(dest_count == 0)
816 rhs = goto_state_rhs;
826 dest_state.
assignment(ssa, rhs, ns,
true,
true).get();
831 mstream <<
"Assignment to " << new_lhs.get_identifier() <<
" ["
832 << pointer_offset_bits(new_lhs.type(), ns).value_or(0) <<
" bits]"
857 diff_guard -= dest_state.
guard;
863 for(
const auto &delta_item : delta_view)
865 const ssa_exprt &ssa = delta_item.m.first;
866 unsigned goto_count = delta_item.m.second;
867 unsigned dest_count = !delta_item.is_in_both_maps()
869 : delta_item.get_other_map_value().second;
889 for(
const auto &delta_item : delta_view)
891 if(delta_item.is_in_both_maps())
894 const ssa_exprt &ssa = delta_item.m.first;
895 unsigned goto_count = 0;
896 unsigned dest_count = delta_item.m.second;
917 const unsigned loop_number=state.
source.
pc->loop_number;
bool is_failed_symbol(const exprt &expr)
Return true if, and only if, expr is the result of failed dereferencing.
A constant literal expression.
const irep_idt & get_value() const
dstringt has one field, an unsigned integer no which is an index into a static table of strings.
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.
typet & type()
Return the type of the expression.
The Boolean constant false.
bool is_divisible(const ssa_exprt &expr) const
Determine whether expr would translate to an atomic SSA expression (returns false) or a composite obj...
This class represents an instruction in the GOTO intermediate representation.
std::set< targett > incoming_edges
targetst targets
The list of successor instructions.
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
const codet & get_code() const
Get the code represented by this instruction.
bool is_backwards_goto() const
Returns true if the instruction is a backwards branch.
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,...
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
const symex_level2t & get_level2() const
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
Central data structure: state.
goto_programt::const_targett saved_target
std::stack< bool > record_events
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...
static irep_idt guard_identifier()
call_stackt & call_stack()
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)
guard_managert & guard_manager
NODISCARD renamedt< ssa_exprt, level > rename_ssa(ssa_exprt ssa, const namespacet &ns)
Version of rename which is specialized for SSA exprt.
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.
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.
irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use,...
virtual void vcc(const exprt &, const std::string &msg, statet &)
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.
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 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...
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
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
source_locationt source_location
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().
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.
Wrapper for expressions or types which have been renamed up to a given level.
const underlyingt & get() const
void simplify(const namespacet &ns)
std::vector< delta_view_itemt > delta_viewt
Delta view of the key-value pairs in two maps.
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 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...
GOTO Symex constant propagation.
nonstd::optional< T > optionalt
Storage of symbolic execution paths to resume.
API to expression classes for Pointers.
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
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)
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.
const binary_exprt & to_binary_expr(const exprt &expr)
Cast an exprt to a binary_exprt.
bool can_cast_expr< symbol_exprt >(const exprt &base)
std::string to_string(const string_not_contains_constraintt &expr)
Used for debug printing.
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_state_map
Information saved at a conditional goto to resume execution.
bool unwinding_assertions
bool constant_propagation
bool self_loops_to_assumptions
bool doing_path_exploration
symex_renaming_levelt current_names
Identifies source in the context of symbolic execution.
goto_programt::const_targett pc
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 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 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.
static guardt merge_state_guards(goto_statet &goto_state, goto_symex_statet &state)