32 : max_depth(options.get_unsigned_int_option(
"depth")),
33 doing_path_exploration(options.is_set(
"paths")),
34 allow_pointer_unsoundness(
35 options.get_bool_option(
"allow-pointer-unsoundness")),
36 constant_propagation(options.get_bool_option(
"propagation")),
37 self_loops_to_assumptions(
38 options.get_bool_option(
"self-loops-to-assumptions")),
39 simplify_opt(options.get_bool_option(
"simplify")),
40 unwinding_assertions(options.get_bool_option(
"unwinding-assertions")),
41 partial_loops(options.get_bool_option(
"partial-loops")),
42 havoc_undefined_functions(
43 options.get_bool_option(
"havoc-undefined-functions")),
44 run_validation_checks(options.get_bool_option(
"validate-ssa-equation")),
45 show_symex_steps(options.get_bool_option(
"show-goto-symex-steps")),
46 show_points_to_sets(options.get_bool_option(
"show-points-to-sets")),
47 max_field_sensitivity_array_size(
48 options.is_set(
"no-array-field-sensitivity")
50 : options.is_set(
"max-field-sensitivity-array-size")
51 ? options.get_unsigned_int_option(
52 "max-field-sensitivity-array-size")
54 complexity_limits_active(
55 options.get_signed_int_option(
"symex-complexity-limit") > 0),
56 cache_dereferences{options.get_bool_option(
"symex-cache-dereferences")}
65 std::vector<framet::active_loop_infot> &active_loops)
67 while(!active_loops.empty())
69 if(!active_loops.back().loop.contains(
to))
70 active_loops.pop_back();
79 bool is_backwards_goto)
97 i_e->is_backwards_goto() &&
i_e->get_target() ==
to &&
98 (!is_backwards_goto ||
99 state.
source.
pc->location_number >
i_e->location_number))
125 state.
source.
pc->is_backwards_goto() &&
126 state.
source.
pc->location_number <
to->location_number)
184 const exprt &condition,
186 const std::string &msg,
256 const bool is_assert = state.
source.
pc->is_assert();
303 statet &state,
const get_goto_functiont &get_goto_function)
319 std::cout <<
"********* Now executing thread " << t <<
'\n';
328 const get_goto_functiont &get_goto_function)
383 const get_goto_functiont &get_goto_function,
401 const get_goto_functiont &get_goto_function)
410 catch(
const std::out_of_range &)
425 [storage](
const irep_idt &
id) { return storage->get_unique_l2_index(id); });
431 std::prev(start_function->body.instructions.end());
432 state->call_stack().top().end_of_function =
limit;
433 state->call_stack().top().calling_location.pc =
434 state->call_stack().top().end_of_function;
435 state->call_stack().top().hidden_function = start_function->is_hidden();
437 state->symex_target = &
target;
439 state->run_validation_checks =
symex_config.run_validation_checks;
456 state->call_stack().top().loops_info =
468 const get_goto_functiont &get_goto_function,
473 state->shadow_memory.fields = fields;
479 const get_goto_functiont &get_goto_function,
485 state->shadow_memory.fields = fields;
497 return [&goto_model](
507 <<
" location number: " << source.
pc->location_number;
522 (state.
source.
pc->code().is_nil() &&
528 if(state.
source.
pc->code().is_not_nil())
531 std::size_t size = 0;
539 log.
status() <<
"[Guard size: " << size <<
"] "
543 state.
source.
pc->source_location().is_not_nil() &&
544 !state.
source.
pc->source_location().get_java_bytecode_index().empty())
547 <<
" bytecode index: "
548 << state.
source.
pc->source_location().get_java_bytecode_index();
560 if(!call_stack.empty())
575 if(!call_stack.empty())
579 for(
auto &frame : call_stack)
595 const get_goto_functiont &get_goto_function,
605 const get_goto_functiont &get_goto_function,
625 switch(instruction.
type())
770 if(return_value && *symbol_expr != *return_value)
774 return_value = *symbol_expr;
791 condition = state.
rename<
L1>(std::move(condition),
ns).get();
824 const bool exclude_null_derefs =
false;
Abstract interface to eager or lazy GOTO models.
virtual const goto_functionst::goto_functiont & get_goto_function(const irep_idt &id)=0
Get a GOTO function by name, or throw if no such function exists.
Replace symbols with constants while maintaining syntactically valid expressions.
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
complexity_violationt check_complexity(goto_symex_statet &state)
Checks the passed-in state to see if its become too complex for us to deal with, and if so set its gu...
void run_transformations(complexity_violationt complexity_violation, goto_symex_statet ¤t_state)
Runs a suite of transformations on the state and symex executable, performing whatever transformation...
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.
const_depth_iteratort depth_cend() const
bool is_false() const
Return whether the expression is a constant representing false.
typet & type()
Return the type of the expression.
const_depth_iteratort depth_cbegin() const
The Boolean constant false.
Stack frames – these are used for function calls and for exceptions.
std::vector< active_loop_infot > active_loops
std::unordered_map< irep_idt, loop_infot > loop_iterations
goto_programt::const_targett end_of_function
std::shared_ptr< lexical_loopst > loops_info
::goto_functiont goto_functiont
static irep_idt entry_point()
Get the identifier of the entry point to a goto model.
This class represents an instruction in the GOTO intermediate representation.
const exprt & return_value() const
Get the return value of a SET_RETURN_VALUE instruction.
const exprt & assign_lhs() const
Get the lhs of the assignment for ASSIGN.
const exprt & assign_rhs() const
Get the rhs of the assignment for ASSIGN.
std::set< targett, target_less_than > incoming_edges
const exprt & condition() const
Get the condition of gotos, assume, assert.
const source_locationt & source_location() const
goto_program_instruction_typet type() const
What kind of instruction?
static irep_idt loop_id(const irep_idt &function_id, const instructiont &instruction)
Human-readable loop name.
instructionst::const_iterator const_targett
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.
value_sett value_set
Uses level 1 names, and is used to do dereferencing.
Central data structure: state.
call_stackt & call_stack()
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...
std::stack< bool > record_events
symbol_tablet symbol_table
contains symbols that are minted during symbolic execution, such as dynamically created objects etc.
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.
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...
virtual NODISCARD symbol_tablet symex_with_state(statet &state, const get_goto_functiont &get_goto_functions)
Symbolically execute the entire program starting from entry point.
void rewrite_quantifiers(exprt &, statet &)
virtual void symex_assume(statet &state, const exprt &cond)
Symbolically execute an ASSUME instruction or simulate such an execution for a synthetic assumption.
void symex_threaded_step(statet &state, const get_goto_functiont &get_goto_function)
Invokes symex_step and verifies whether additional threads can be executed.
void symex_unreachable_goto(statet &state)
Symbolically execute a GOTO instruction in the context of unreachable code.
complexity_limitert complexity_module
virtual void symex_atomic_begin(statet &state)
Symbolically execute an ATOMIC_BEGIN instruction.
const symbol_table_baset & outer_symbol_table
The symbol table associated with the goto-program being executed.
irep_idt language_mode
language_mode: ID_java, ID_C or another language identifier if we know the source language in use,...
void symex_set_return_value(statet &state, const exprt &return_value)
Symbolically execute a SET_RETURN_VALUE instruction.
bool ignore_assertions
If this flag is set to true then assertions will be temporarily ignored by the symbolic executions.
static get_goto_functiont get_goto_function(abstract_goto_modelt &goto_model)
Return a function to get/load a goto function from the given goto model Create a default delegate to ...
virtual void symex_step(const get_goto_functiont &get_goto_function, statet &state)
Called for each step in the symbolic execution This calls print_symex_step to print symex's current i...
virtual void symex_goto(statet &state)
Symbolically execute a GOTO instruction.
virtual void symex_decl(statet &state)
Symbolically execute a DECL instruction.
void symex_catch(statet &state)
Symbolically execute a CATCH instruction.
path_storaget & path_storage
Symbolic execution paths to be resumed later.
std::unique_ptr< statet > initialize_entry_point_state(const get_goto_functiont &get_goto_function)
Initialize the symbolic execution and the given state with the beginning of the entry point function.
symex_target_equationt & target
The equation that this execution is building up.
std::function< const goto_functionst::goto_functiont &(const irep_idt &) get_goto_functiont)
The type of delegate functions that retrieve a goto_functiont for a particular function identifier.
guard_managert & guard_manager
Used to create guards.
virtual NODISCARD symbol_tablet resume_symex_from_saved_state(const get_goto_functiont &get_goto_function, const statet &saved_state, symex_target_equationt *saved_equation)
Performs symbolic execution using a state and equation that have already been used to symbolically ex...
void symex_assert(const goto_programt::instructiont &, statet &)
virtual void symex_dead(statet &state)
Symbolically execute a DEAD instruction.
std::size_t path_segment_vccs
Number of VCCs generated during the run of this goto_symext object.
virtual void symex_start_thread(statet &state)
Symbolically execute a START_THREAD instruction.
virtual NODISCARD symbol_tablet symex_from_entry_point_of(const get_goto_functiont &get_goto_function, const shadow_memory_field_definitionst &fields)
Symbolically execute the entire program starting from entry point.
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).
void kill_instruction_local_symbols(statet &state)
Kills any variables in instruction_local_symbols (these are currently always let-bound variables defi...
virtual void symex_end_of_function(statet &)
Symbolically execute a END_FUNCTION instruction.
exprt clean_expr(exprt expr, statet &state, bool write)
Clean up an expression.
void symex_assign(statet &state, const exprt &lhs, const exprt &rhs)
Symbolically execute an ASSIGN instruction or simulate such an execution for a synthetic assignment.
void print_symex_step(statet &state)
Prints the route of symex as it walks through the code.
void symex_throw(statet &state)
Symbolically execute a THROW instruction.
virtual void do_simplify(exprt &expr)
virtual void symex_other(statet &state)
Symbolically execute an OTHER instruction.
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.
messaget::mstreamt & print_callstack_entry(const symex_targett::sourcet &target)
std::vector< symbol_exprt > instruction_local_symbols
Variables that should be killed at the end of the current symex_step invocation.
virtual void symex_atomic_end(statet &state)
Symbolically execute an ATOMIC_END instruction.
virtual void symex_function_call(const get_goto_functiont &get_goto_function, statet &state, const goto_programt::instructiont &instruction)
Symbolically execute a FUNCTION_CALL instruction.
void execute_next_instruction(const get_goto_functiont &get_goto_function, statet &state)
Executes the instruction state.source.pc Case-switches over the type of the instruction being execute...
virtual void initialize_path_storage_from_entry_point_of(const get_goto_functiont &get_goto_function, symbol_table_baset &new_symbol_table, const shadow_memory_field_definitionst &fields)
Puts the initial state of the entry point function into the path storage.
void add(const exprt &expr)
exprt guard_expr(exprt expr) const
Return guard => dest or a simplified variant thereof if either guard or dest are trivial.
void populate_dirty_for_function(const irep_idt &id, const goto_functionst::goto_functiont &function)
Analyse the given function with dirtyt if it hasn't been seen before.
const irep_idt & id() const
A very simple, cheap analysis to determine when dereference operations are trivially guarded by a che...
mstreamt & status() const
A namespacet is essentially one or two symbol tables bound together, to allow for symbol lookups in t...
const symbol_table_baset & get_symbol_table() const
Return first symbol table registered with the namespace.
incremental_dirtyt dirty
Local variables are considered 'dirty' if they've had an address taken and therefore may be referred ...
std::shared_ptr< lexical_loopst > get_loop_analysis(const irep_idt &function_id)
std::unordered_map< irep_idt, local_safe_pointerst > safe_pointers
Map function identifiers to local_safe_pointerst instances.
virtual void push(const patht &)=0
Add a path to resume to the storage.
void add_function_loops(const irep_idt &identifier, const goto_programt &body)
Generates a loop analysis for the instructions in goto_programt and keys it against function ID.
The pointer type These are both 'bitvector_typet' (they have a width) and 'type_with_subtypet' (they ...
The shadow memory field definitions.
Expression to hold a symbol (variable)
The symbol table base class interface.
Inheriting the interface of symex_targett this class represents the SSA form of the input program as ...
virtual void assertion(const exprt &guard, const exprt &cond, const irep_idt &property_id, const std::string &msg, const sourcet &source)
Record an assertion.
virtual void assumption(const exprt &guard, const exprt &cond, const sourcet &source)
Record an assumption.
virtual void location(const exprt &guard, const sourcet &source)
Record a location.
void insert(const symbol_exprt &old_expr, const exprt &new_expr)
Thrown when we encounter an instruction, parameters to an instruction etc.
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.
complexity_violationt
What sort of symex-complexity violation has taken place.
Forward depth-first search iterators These iterators' copy operations are expensive,...
bool has_subexpr(const exprt &expr, const std::function< bool(const exprt &)> &pred)
returns true if the expression has a subexpression that satisfies pred
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)
constexpr std::size_t DEFAULT_MAX_FIELD_SENSITIVITY_ARRAY_SIZE
Limit the size of arrays for which field_sensitivity gets applied.
API to expression classes for 'mathematical' expressions.
const quantifier_exprt & to_quantifier_expr(const exprt &expr)
Cast an exprt to a quantifier_exprt.
Storage of symbolic execution paths to resume.
const pointer_typet & to_pointer_type(const typet &type)
Cast a typet to a pointer_typet.
#define CHECK_RETURN(CONDITION)
#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 symbol_exprt & to_symbol_expr(const exprt &expr)
Cast an exprt to a symbol_exprt.
Information saved at a conditional goto to resume execution.
symex_configt(const optionst &options)
Construct a symex_configt using options specified in an optionst.
Identifies source in the context of symbolic execution.
goto_programt::const_targett pc
void symex_transition(goto_symext::statet &state, goto_programt::const_targett to, bool is_backwards_goto)
static optionalt< symbol_exprt > find_unique_pointer_typed_symbol(const exprt &expr)
Check if an expression only contains one unique symbol (possibly repeated multiple times)
static void switch_to_thread(goto_symex_statet &state, const unsigned int thread_nb)
static void pop_exited_loops(const goto_programt::const_targett &to, std::vector< framet::active_loop_infot > &active_loops)
If 'to' is not an instruction in our currently top-most active loop, pop and re-check until we find a...