31 const exprt &original_guard,
32 const exprt &new_guard,
81 const exprt &other_operand,
87 expr_try_dynamic_cast<constant_exprt>(other_operand);
91 other_without_typecast.
id() != ID_address_of &&
92 (!constant_expr || constant_expr->
get_value() != ID_NULL))
98 expr_try_dynamic_cast<ssa_exprt>(symbol_expr);
102 const std::vector<exprt> value_set_elements =
105 bool constant_found =
false;
107 for(
const auto &value_set_element : value_set_elements)
110 value_set_element.id() == ID_unknown ||
111 value_set_element.id() == ID_invalid ||
123 value_set_element,
false, language_mode))
130 value_set_element, symbol_expr, ns);
134 constant_found =
true;
145 return operation == ID_equal ? make_renamed<L2>(
false_exprt{})
148 else if(value_set_elements.size() == 1)
152 return operation == ID_equal ? make_renamed<L2>(
true_exprt{})
174 const exprt &expr = renamed_expr.
get();
176 if(expr.
id() != ID_equal && expr.
id() != ID_notequal)
187 expr_try_dynamic_cast<symbol_exprt>(lhs);
196 expr.
id(), *symbol_expr_lhs, rhs, value_set, language_mode, ns);
209 expr, value_set, language_mode, ns);
228 new_guard = renamed_guard.
get();
242 !instruction.
targets.empty(),
"goto should have at least one target");
246 instruction.
targets.size() == 1,
"no support for non-deterministic gotos");
263 goto_target->is_goto() && new_guard.
is_true())))
317 instruction.
targets.size() > 0,
318 "Instruction is an unconditional goto with no target: " +
329 new_state_pc=goto_target;
335 while(state_pc!=goto_target && !state_pc->is_target())
338 if(state_pc==goto_target)
348 state_pc=goto_target;
359 "Tried to explore the other path of a branch, but the next "
360 "instruction along that path is not the same as the instruction "
361 "that we saved at the branch point. Saved instruction is " +
363 "\nwe were intending "
365 new_state_pc->code.pretty() +
367 "instruction we think we saw on a previous path exploration is " +
368 state_pc->code.pretty());
370 new_state_pc = state_pc;
378 log.
debug() <<
"Resuming from next instruction '"
397 log.
debug() <<
"Saving next instruction '"
400 log.
debug() <<
"Saving jump target '"
425 goto_state_list.emplace_back(state.
source, std::move(state));
434 goto_state_list.emplace_back(state.
source, state);
443 auto &taken_state = backward ? state : goto_state_list.back().second;
444 auto ¬_taken_state = backward ? goto_state_list.back().second : state;
459 new_guard.
id() == ID_symbol ||
460 (new_guard.
id() == ID_not &&
463 guard_expr=new_guard;
474 state.
assignment(std::move(new_lhs), new_rhs,
ns,
true,
false).get();
481 mstream <<
"Assignment to " << new_lhs.get_identifier()
482 <<
" [" << pointer_offset_bits(new_lhs.type(), ns).value_or(0) <<
" bits]"
488 new_lhs, new_lhs, guard_symbol_expr,
505 goto_statet &new_state = goto_state_list.back().second;
542 auto queue_unreachable_state_at_target = [&]() {
548 goto_state_list.emplace_back(state.
source, std::move(new_state));
561 queue_unreachable_state_at_target();
571 bool maybe_loop_head = std::any_of(
575 return predecessor->location_number > instruction.location_number;
585 queue_unreachable_state_at_target();
612 for(
auto list_it = state_list.rbegin(); list_it != state_list.rend();
615 merge_goto(list_it->first, std::move(list_it->second), state);
642 return std::move(state.
guard);
646 return std::move(goto_state.
guard);
650 return std::move(state.
guard);
662 "atomic sections differ across branches",
671 if(goto_state.reachable)
677 static_cast<goto_statet &
>(state) = std::move(goto_state);
688 state.
depth = std::min(state.
depth, goto_state.depth);
693 state.
guard = std::move(new_guard);
717 const bool do_simplify,
721 const unsigned goto_count,
722 const unsigned dest_count)
730 if(goto_count == dest_count)
736 (!dest_state.
reachable && goto_count == 0) ||
737 (!goto_state.
reachable && dest_count == 0))
766 exprt goto_state_rhs = ssa, dest_state_rhs = ssa;
769 const auto p_it = goto_state.
propagation.find(l1_identifier);
772 goto_state_rhs = *p_it;
778 const auto p_it = dest_state.
propagation.find(l1_identifier);
781 dest_state_rhs = *p_it;
795 rhs = goto_state_rhs;
797 rhs = dest_state_rhs;
798 else if(goto_count == 0)
799 rhs = dest_state_rhs;
800 else if(dest_count == 0)
801 rhs = goto_state_rhs;
811 dest_state.
assignment(ssa, rhs, ns,
true,
true).get();
816 mstream <<
"Assignment to " << new_lhs.get_identifier() <<
" ["
817 << pointer_offset_bits(new_lhs.type(), ns).value_or(0) <<
" bits]"
842 diff_guard -= dest_state.
guard;
848 for(
const auto &delta_item : delta_view)
850 const ssa_exprt &ssa = delta_item.m.first;
851 unsigned goto_count = delta_item.m.second;
852 unsigned dest_count = !delta_item.is_in_both_maps()
854 : delta_item.get_other_map_value().second;
874 for(
const auto &delta_item : delta_view)
876 if(delta_item.is_in_both_maps())
879 const ssa_exprt &ssa = delta_item.m.first;
880 unsigned goto_count = 0;
881 unsigned dest_count = delta_item.m.second;
902 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.
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.
codet code
Do not read or modify directly – use get_X() instead.
std::set< targett > incoming_edges
targetst targets
The list of successor instructions.
const exprt & get_condition() const
Get the condition of gotos, assume, assert.
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.
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 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...
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.
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
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)
#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)
bool can_cast_type< pointer_typet >(const typet &type)
Check whether a reference to a typet is a pointer_typet.
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)