|
| | schedule_execution_statet (const goto_functionst &goto_functions, const namespacet &ns, reachability_treet *art, std::shared_ptr< symex_targett > _target, contextt &context, optionst &options, unsigned int *ptotal_claims, unsigned int *premaining_claims, unsigned int *psimplified_claims, unsigned int *ptruncations) |
| | schedule_execution_statet (const schedule_execution_statet &ref)=default |
| std::shared_ptr< execution_statet > | clone () const override |
| | Duplicate this execution state.
|
| | ~schedule_execution_statet () override |
| void | claim (const expr2tc &expr, const std::string &msg) override |
| | Symbolically assert something.
|
| void | note_bounded_loop_truncation () override |
| | Under –no-unwinding-assertions a truncated loop is cut with an assumption, which drives the state guard false and so is indistinguishable at the scheduler from a genuinely infeasible path.
|
| | execution_statet (const goto_functionst &goto_functions, const namespacet &ns, reachability_treet *art, std::shared_ptr< symex_targett > _target, contextt &context, std::shared_ptr< ex_state_level2t > l2init, optionst &options) |
| | Default constructor.
|
| | execution_statet (const execution_statet &ex) |
| | Default copy constructor.
|
| execution_statet & | operator= (const execution_statet &ex)=delete |
| | Public assignment is deleted: a standalone a = b would not be correct here (it would leave the base goto_symext slice, threads_state, cur_state, and state_level2 as a's old objects).
|
| virtual | ~execution_statet ()=default |
| | Default destructor.
|
| void | increment_context_switch () |
| | Increase number of context switches this ex_state has taken.
|
| int | get_context_switch () const |
| | Get the number of context switches performed by this ex_state.
|
| unsigned int | get_active_state_number () const |
| | Fetch the thread ID of the current active thread.
|
| void | set_thread_start_data (unsigned int tid, const expr2tc &argdata) |
| | Set internal thread startup data.
|
| const expr2tc & | get_thread_start_data (unsigned int tid) const |
| | Fetch internal thread startup data.
|
| void | symex_step (reachability_treet &art) override |
| | Make one symbolic execution step.
|
| void | symex_end_function (reachability_treet &art, const goto_programt::instructiont &instruction) |
| void | symex_assign (const expr2tc &code, const bool hidden, const guard2tc &guard) override |
| | Symbolically assign a value.
|
| void | symex_goto (const expr2tc &old_guard) override |
| | Perform a jump across GOTO code.
|
| void | assume (const expr2tc &assumption) override |
| | Assume some expression is true.
|
| void | defer_assumption (const expr2tc &assumption) override |
| | As assume(), the deferred assumption reads its condition now.
|
| void | symex_printf (const expr2tc &lhs, expr2tc &code) override |
| | Implemented by goto_symext::symex_printf.
|
| unsigned int & | get_dynamic_counter () override |
| | Fetch reference to count of dynamic objects in this state.
|
| unsigned int & | get_nondet_counter () override |
| | Like get_dynamic_counter, but with nondet symbols.
|
| expr2tc | get_guard_identifier () |
| | Fetch name of current execution guard.
|
| goto_symex_statet & | get_active_state () |
| | Get reference to current thread state.
|
| const goto_symex_statet & | get_active_state () const |
| unsigned int | get_active_atomic_number () const |
| | Get atomic number count for current thread state.
|
| void | increment_active_atomic_number () |
| | Increase current threads atomic number count.
|
| void | decrement_active_atomic_number () |
| | Decrease current threads atomic number count.
|
| void | switch_to_thread (unsigned int i) |
| | Perform a context switch to thread ID i.
|
| bool | is_cur_state_guard_false (const expr2tc &guard) |
| | Determines if current state guard is false.
|
| void | execute_guard () |
| | Generates execution guard that's true if this interleaving can be reached.
|
| bool | check_if_ileaves_blocked () |
| | Test to see if interleavings are blocked by the current state.
|
| bool | all_threads_terminal () const |
| | True iff every thread in this schedule has reached a terminal state, i.e.
|
| unsigned int | add_thread (const goto_programt *prog) |
| | Create a new thread.
|
| void | end_thread () |
| | Record a thread as ended.
|
| void | update_after_switch_point () |
| | Perform any necessary steps after a context switch point.
|
| void | preserve_last_paths (const transition_resultt &transition) |
| void | cull_all_paths () |
| void | restore_last_paths () |
| void | record_parked_path (goto_programt::const_targett target, statet::merge_state_listt::iterator parked) override |
| | Hook called when a step parks a merge_statet snapshot for a deferred merge — a GOTO forking off its sibling arm, or a RETURN parking the continuation at end_of_function.
|
| void | analyze_assign (const expr2tc &assign) |
| | Analyze the contents of an assignment for threading.
|
| void | analyze_read (const expr2tc &expr) |
| | Analyze the contents of a read for threading.
|
| void | get_expr_globals (const namespacet &ns, const expr2tc &expr, std::set< expr2tc > &global_list, access_kindt kind, bool under_deref=false) |
| | Get list of globals accessed by expr.
|
| expr2tc | resolve_pointer_target (const namespacet &ns, const expr2tc &ptr, bool &to_global, bool through_deref) |
| | Resolve one pointer level: the object ptr's value set names, or nil.
|
| void | record_aggregate_held_target (const namespacet &ns, const expr2tc &expr, std::set< expr2tc > &global_list, access_kindt kind) |
| | Record what a dereference reaches when the pointer it goes through is not a bare symbol (R29).
|
| void | record_access_key (const expr2tc &key, std::set< expr2tc > &global_list, access_kindt kind) |
| | Record key as an object accessed by this transition, for MPOR.
|
| bool | check_mpor_dependency (unsigned int j, unsigned int l) const |
| | Check for scheduling dependencies.
|
| transition_footprintt | last_transition_footprint (unsigned int tid) const |
| | Footprint of the transition thread tid most recently completed.
|
| bool | check_mpor_dependency (unsigned int j, const transition_footprintt &fp) const |
| | As check_mpor_dependency, but against a footprint captured earlier rather than against a thread's current one.
|
| void | calculate_mpor_constraints () |
| | Calculate MPOR schedulable threads.
|
| bool | is_transition_blocked_by_mpor () const |
| | Read-only accessor for mpor_says_no.
|
| const std::vector< std::vector< int > > & | get_dependency_chain () const |
| | Read-only accessor for the MPOR dependency chain, for the A6.4 harness.
|
| const std::vector< unsigned int > & | get_thread_last_transition () const |
| | Read-only accessor for the chain's run order, for the A6.4 harness.
|
| void | force_cswitch () |
| | Accessor method for cswitch_forced.
|
| bool | has_cswitch_point_occured () const |
| | Has a context switch point occurred.
|
| bool | can_execution_continue () const |
| | Can execution continue in this thread?
|
| std::size_t | generate_hash () const |
| | Generate hash of entire execution state.
|
| std::size_t | update_hash_for_assignment (const expr2tc &rhs) |
| | Generate hash of an expression.
|
| void | print_stack_traces (unsigned int indent=0) const |
| | Print stack trace of each thread to stdout.
|
| void | switch_to_monitor () |
| | Switch to registered monitor thread.
|
| void | switch_away_from_monitor () |
| | Switch away from registered monitor thread.
|
| void | kill_monitor_thread () |
| | Makr registered monitor thread as ended.
|
| void | analyze_args (const expr2tc &expr) override |
| | Analyze the shared varables in a function call, this is because an argumemt may be renamed to constant bool in symex_function_call_code(), while we need to get the information for context switch.
|
| | goto_symext (const namespacet &_ns, contextt &_new_context, const goto_functionst &goto_functions, std::shared_ptr< symex_targett > _target, optionst &opts) |
| | Default constructor.
|
| | goto_symext (const goto_symext &sym) |
| goto_symext & | operator= (const goto_symext &sym) |
| expr2tc | guard_identifier () |
| | Return identifier for goto guards.
|
| bool | chase_copies (expr2tc &expr) const |
| | Rewrite an expression onto the canonical basis of its copy chains: every L2 symbol with an entry in copy_definitions is replaced by the value it was assigned.
|
| tvt::tv_enumt | path_guard_decides (const expr2tc &new_guard, bool already_false, bool already_true) |
| | Whether the accumulated path guard already decides a branch condition: TV_TRUE when a conjunct matches it, TV_FALSE when one matches its negation, TV_UNKNOWN otherwise.
|
| void | record_guard_definition (const expr2tc &guard_expr, const expr2tc &rhs) |
| | Remember a guard generation's defining condition for path_guard_decides.
|
| expr2tc | rewrite_conjunct (const expr2tc &conjunct) |
| | A path-guard conjunct rewritten onto the canonical basis path_guard_decides compares on.
|
| conjunct_indext | prefix_index (const guard2tc &guard) |
| | The conjunct index of guard, which must not be true.
|
| void | record_copy_definition (const expr2tc &renamed_lhs, const expr2tc &rhs) |
| | Record a copy chain for chase_copies after an unconditional assignment, when the rhs is a stable value: a (possibly typecast) L2 symbol, or a pure bitvector computation over such leaves.
|
| goto_symext::symex_resultt | get_symex_result () |
| | Create a symex result for this run.
|
| void | add_memory_leak_checks () |
| | Perform accounting checks / assertions at end of a program run.
|
| void | release_symex_caches () |
| | Free what only symex reads, once a formula is built: the guard prefix index grows with every branching goto and would otherwise live through solving.
|
|
| enum class | access_kindt { READ
, WRITE
} |
| | Kind of memory access, used by get_expr_globals to decide whether a read-only global can be filtered out of cswitch-triggering sets. More...
|
| typedef goto_symex_statet::merge_statet | merge_statet |
| typedef goto_symex_statet | statet |
| using | conjunct_indext = persistent_map<expr2tc, size_t, irep2_hash> |
| | Rewritten conjunct -> position of the first conjunct rewriting to it.
|
| static void | reset_dynamic_counter () |
| | Zero the dynamic-object counter.
|
| static std::string | assertion_message (const namespacet &ns, const goto_programt::instructiont &i) |
| | The message of the claim an ASSERT instruction raises for itself, as opposed to a check symex raises while evaluating its guard.
|
| static constexpr const char * | guard_execution_name |
| | Name of the top-level execution guard symbol.
|
| static unsigned | dynamic_counter = 0 |
| | Number of dynamic objects in this state.
|
| static unsigned int | node_count = 0 |
| void | copy_derived_from (const execution_statet &ex) |
| | Copy execution_statet's own scheduling fields from ex.
|
| virtual void | do_simplify (expr2tc &expr) |
| | Perform simplification on an expression.
|
| expr2tc | branch_decision_guard (const expr2tc &guard) const |
| | The guard a branch decision is read from.
|
| void | dereference (expr2tc &expr, dereferencet::modet mode, bool block_assertions=false) |
| | Dereference an expression.
|
| void | symex_return (const expr2tc &code) |
| | Perform interpretation of RETURN instruction.
|
| void | symex_witness_function_return (expr2tc ret_val, const irep_idt &call_line) |
| bool | symex_witness_function_enter (const irep_idt &call_line) |
| void | symex_witness_branching (const expr2tc &old_guard, const expr2tc &new_guard, bool forward, bool &new_guard_true, bool &new_guard_false, const goto_programt::instructiont &instruction) |
| void | symex_witness_assert (expr2tc &new_expr, const std::string &msg) |
| void | symex_other (const expr2tc &code) |
| | Interpret an OTHER instruction.
|
| void | symex_decl (const expr2tc &code) |
| | Interpret an DECL instruction.
|
| void | symex_dead (const expr2tc &code) |
| | Interpret an DEAD instruction.
|
| bool | stack_checks_enabled () const |
| | True when either stack limit is on.
|
| void | check_stack_size (const expr2tc &expr, const std::string &subject="") |
| | Account expr's storage against the current frame and claim that neither –stack-limit nor –total-stack-limit is exceeded.
|
| void | symex_assume () |
| | Interpret an ASSUME instruction.
|
| void | symex_assert () |
| | Interpret an ASSERT instruction.
|
| bool | check_incremental (const expr2tc &expr, const std::string &msg) |
| | Perform incremental SMT solving for assert and assume statements.
|
| void | record_property_verdict (const std::string &msg, property_verdictt verdict, const std::string ¬e="") |
| | Record a verdict for the claim being symbolically executed.
|
| virtual void | assertion (const expr2tc &assertion, const std::string &msg) |
| | Perform an assertion.
|
| void | propagate_assume_equality (const expr2tc &the_assumption) |
| | Lift var == const from an assume into the level2 constant propagator so subsequent renames of var substitute the constant directly.
|
| void | flush_deferred_assumptions () |
| | Before a claim that needs them, emit every deferred assumption into the target equation.
|
| void | merge_gotos () |
| | Merge converging states into current state.
|
| void | merge_value_sets (const statet::merge_statet &merge_state) |
| | Merge pointer tracking value sets in a phi function.
|
| void | merge_locality (const statet::merge_statet &merge_state) |
| void | snapshot_interval_domain (statet::merge_statet &merge_state) |
| | Record the online interval domain in a path being parked, so merge_interval_domain can join it back in (#8047).
|
| void | assume_loop_continues (const goto_programt::instructiont &instruction, const expr2tc &guard, bool forward, bool always_jumps) |
| | Narrow the online interval domain by the condition under which a loop GOTO's continuing path proceeds; nothing when the GOTO always jumps, since that path is dead.
|
| void | merge_interval_domain (const statet::merge_statet &merge_state) |
| | Join a parked path's interval domain into the shared one; a path parked without a snapshot sends the domain to top.
|
| void | phi_function (const statet::merge_statet &merge_state) |
| | Join a previous jump's merge snapshot into the active thread state.
|
| bool | get_unwind (const symex_targett::sourcet &source, const BigInt &unwind) |
| | Test whether unwinding bound has been exceeded.
|
| void | loop_bound_exceeded (const expr2tc &guard) |
| | Encode unwinding assertions and assumption.
|
| void | pop_frame () |
| | Pop a stack frame.
|
| bool | is_python_gc_object (const symbolt *base) const |
| | Whether base is a user-defined Python class instance that follows garbage-collected lifetime semantics (issue #4773).
|
| bool | make_return_assignment (expr2tc &assign, const expr2tc &code_return) |
| | Create assignment for return statement.
|
| void | symex_function_call (const expr2tc &call) |
| | Perform function call.
|
| void | symex_end_of_function () |
| | End a functions interpretation.
|
| virtual void | symex_function_call_deref (const expr2tc &call) |
| | Handle an indirect function call, to a pointer.
|
| virtual void | symex_function_call_code (const expr2tc &call) |
| | Handle a call to a statically-known function: checks recursion bounds, sets up the new frame, assigns arguments, and jumps to the body.
|
| bool | symex_uninterpreted_function (const code_function_call2t &call, const irep_idt &identifier) |
| | Model a call to a "__ESBMC_uninterpreted_*" or "__CPROVER_uninterpreted_*" function as a genuine uninterpreted function: assign the return an uninterpreted_func2t application of the (mangled) callee to its renamed arguments.
|
| bool | get_unwind_recursion (const irep_idt &identifier, BigInt unwind) |
| | Discover whether recursion bound has been exceeded.
|
| expr2tc | argument_value (const type2tc &arg_type, const expr2tc &rhs, const irep_idt &identifier) |
| | Convert an actual argument to its parameter's type, claiming the call undefined when the two are incompatible.
|
| unsigned int | argument_assignments (const irep_idt &function_identifier, const code_type2t &function_type, const std::vector< expr2tc > &arguments) |
| | Join up function arguments.
|
| bool | run_next_function_ptr_target (bool first) |
| | Setup next function in a chain of func ptr calls.
|
| void | run_intrinsic (const code_function_call2t &call, reachability_treet &art, const std::string &symname) |
| | Run an intrinsic, something prefixed with __ESBMC.
|
| bool | run_builtin (const code_function_call2t &call, const std::string &symname) |
| | Run a builtin, something prefixed with __builtin.
|
| void | symex_bounded_math (const code_function_call2t &call, const std::string &function) |
| | _builtin_bounded<function>(x, exact): the bounded result of a transcendental function, from util/arith/transcendental.h.
|
| void | intrinsic_yield (reachability_treet &arg) |
| | Perform yield; forces a context switch point.
|
| void | intrinsic_switch_to (const code_function_call2t &c, reachability_treet &art) |
| | Perform switch_to; switches control to explicit thread ID.
|
| void | intrinsic_switch_from (reachability_treet &arg) |
| | Yield, always switching away from this thread.
|
| void | intrinsic_get_thread_id (const code_function_call2t &call, reachability_treet &art) |
| | Perform get_thread_id; return the current thread identifier.
|
| void | intrinsic_set_thread_data (const code_function_call2t &call, reachability_treet &art) |
| | Perform set_thread_state; store thread startup information.
|
| void | intrinsic_get_thread_data (const code_function_call2t &call, reachability_treet &art) |
| | Perform get_thread_data; get thread startup information.
|
| void | intrinsic_spawn_thread (const code_function_call2t &call, reachability_treet &art) |
| | Perform spawn_thread; Generates a new thread at a named function.
|
| void | intrinsic_terminate_thread (reachability_treet &art) |
| | Perform terminate_thread; Record thread as terminated.
|
| void | intrinsic_havoc_object (const code_function_call2t &call) |
| | Perform havoc_object; assign nondet to every object the argument may point to, whole and of any size.
|
| void | intrinsic_init_thread_local (reachability_treet &art) |
| | Perform init_thread_local; seeds each __thread-qualified global to its static initializer in the active thread's renaming scope.
|
| void | intrinsic_really_atomic_begin (reachability_treet &art) |
| | Really atomic start/end - atomic blocks that just disable ileaves.
|
| void | intrinsic_really_atomic_end (reachability_treet &art) |
| | Really atomic start/end - atomic blocks that just disable ileaves.
|
| void | intrinsic_switch_to_monitor (reachability_treet &art) |
| | Context switch to the monitor thread.
|
| void | intrinsic_switch_from_monitor (reachability_treet &art) |
| | Context switch from the monitor thread.
|
| void | intrinsic_register_monitor (const code_function_call2t &call, reachability_treet &art) |
| | Register which thread is the monitor thread.
|
| void | intrinsic_kill_monitor (reachability_treet &art) |
| | Terminate the monitor thread.
|
| void | intrinsic_memset (reachability_treet &art, const code_function_call2t &func_call) |
| | Intrinsic call for C memset function call.
|
| void | intrinsic_memcpy (reachability_treet &art, const code_function_call2t &func_call) |
| | Intrinsic call for C memcpy function call.
|
| void | intrinsic_memchr (reachability_treet &art, const code_function_call2t &func_call) |
| | Intrinsic call for C memchr function call.
|
| void | intrinsic_memcmp (reachability_treet &art, const code_function_call2t &func_call) |
| | Models __ESBMC_memcmp(s1, s2, n): for a constant n with both pointers resolving to concrete primitive objects, build the lexicographic comparison result as a single nested-ite expression over the n byte reads (no loop, no unwinding) and assign it to the call's return.
|
| bool | memcpy_symbolic_length (const expr2tc &dst_arg, const expr2tc &src_arg, const expr2tc &n_arg) |
| | Models a memcpy/memmove whose length is not a constant, the case intrinsic_memcpy_impl otherwise defers to the C byte loop (which then unwinds –unwind times per call).
|
| void | memcpy_finish (const code_function_call2t &func_call, const expr2tc &dst_arg, const expr2tc &src_arg, const expr2tc &n_arg) |
| | The NULL checks and return-value assignment shared by both of intrinsic_memcpy_impl's paths.
|
| void | claim_valid_operand (const expr2tc &ptr, const expr2tc &n, const std::string &func) |
| | An INTERNAL dereference drops an unknown or invalid target without a claim, so the memory builtins claim it themselves when ptr's value set holds one and n is nonzero.
|
| void | claim_not_code (const expr2tc &guard) |
| | Claim that a memory builtin's operand, on the path guard selects, is not a code object; nothing under –no-pointer-check.
|
| bool | memcmp_resolve_operand (const expr2tc &ptr, unsigned long number_of_bytes, expr2tc &object, uint64_t &offset, uint64_t &avail_bytes, bool rename_object=true) |
| | Helper for intrinsic_memcmp: resolve ptr to a single concrete primitive object with a constant offset, validating that an number_of_bytes read stays in bounds.
|
| void | claim_nonnull_operand (const expr2tc &ptr, const expr2tc &n, const std::string &func) |
| | Claims ptr is not NULL unless n is zero.
|
| void | intrinsic_memmove (reachability_treet &art, const code_function_call2t &func_call) |
| | Models __ESBMC_memmove.
|
| void | intrinsic_memcpy_impl (reachability_treet &art, const code_function_call2t &func_call, const std::string &bump_name) |
| | Shared core for intrinsic_memcpy / intrinsic_memmove; bump_name is the C fallback (__memcpy_impl / __memmove_impl) used when the byte-exact optimisation cannot apply.
|
| void | bump_call (const code_function_call2t &func_call, const std::string &symname) |
| void | intrinsic_get_object_size (const code_function_call2t &func_call, reachability_treet &art) |
| | Returns the size of the object.
|
| void | intrinsic_builtin_object_size (const code_function_call2t &func_call, reachability_treet &art) |
| | Implements GCC's __builtin_object_size intrinsic for object size determination.
|
| void | replace_races_check (expr2tc &expr) |
| void | simplify_python_builtins (expr2tc &expr) |
| void | reject_untyped_isinstance (const expr2tc &value) |
| void | volatile_check (expr2tc &expr) |
| void | finalize_realloc_result (const expr2tc &lhs, const expr2tc &result, const expr2tc &new_array, const guard2tc &guard, const expr2tc &realloc_size, const expr2tc &alloc_fail) |
| | Finalize the result of a realloc operation.
|
| void | update_pointer_validity (const expr2tc &old_ptr, const expr2tc &alloc_fail, const guard2tc &guard) |
| | Update pointer validity information after realloc.
|
| expr2tc | model_allocation_failure (const expr2tc &result, const expr2tc &old_ptr, const guard2tc &guard, const expr2tc &over_cap, expr2tc &alloc_fail) |
| | Model allocation failure behavior for realloc.
|
| void | bound_dynamic_object_size (const code_assign2t &code) |
| | Bound at PTRDIFF_MAX the object size an assignment records, reporting a constant request that exceeds it rather than assuming it away.
|
| expr2tc | create_result_pointer (const expr2tc &new_array, const type2tc &lhs_type) |
| | Create result pointer from newly allocated array.
|
| expr2tc | calculate_old_element_count (const expr2tc &old_base_array, const type2tc &elem_type, bool old_is_array) |
| | Calculate the number of elements in the old memory object.
|
| expr2tc | calculate_element_count (const expr2tc &size_bytes, const expr2tc &elem_size) |
| | Calculate number of elements from byte size.
|
| type2tc | determine_fallback_element_type (const sideeffect2t &code, const expr2tc &lhs) |
| | Determine fallback element type for realloc.
|
| void | analyze_old_object (const expr2tc &old_obj, type2tc &elem_type, expr2tc &old_base_array, bool &old_is_array) |
| | Analyze an object a reallocated pointer may point to.
|
| void | copy_old_objects (const std::list< dereference_callbackt::internal_item > &old_objects, const expr2tc &new_array, const expr2tc &new_elem_count, const type2tc &elem_type, const guard2tc &guard) |
| | Copy each object a reallocated pointer may point to into the new allocation, guarded by the pointer pointing to it.
|
| bool | handle_realloc_zero_size (const expr2tc &lhs, const sideeffect2t &code, const guard2tc &guard, const expr2tc &realloc_size) |
| | Handle realloc with zero size parameter.
|
| void | copy_single_element (const expr2tc &old_base_array, const expr2tc &new_array, const expr2tc &idx, const type2tc &elem_type, const type2tc &new_elem_type, bool old_is_array, const guard2tc &guard) |
| | Copy a single element between old and new arrays.
|
| void | copy_memory_content (const expr2tc &old_base_array, const expr2tc &new_array, const expr2tc &old_elem_count, const expr2tc &new_elem_count, const type2tc &elem_type, bool old_is_array, const guard2tc &guard) |
| | Copy memory content from old to new allocation.
|
| expr2tc | create_dynamic_memory_symbol (const type2tc &elem_type, const expr2tc &size_expr, const std::string &name_prefix) |
| | Create a new dynamic memory symbol.
|
| bool | terminate_handler () |
| | Call terminate function handler when needed.
|
| bool | unexpected_handler () |
| | Call unexpected function handler when needed.
|
| void | replace_dynamic_allocation (expr2tc &expr) |
| | Replace ireps regarding dynamic allocations with code.
|
| std::vector< expr2tc > | value_set_objects (const expr2tc &ptr, bool &complete) |
| | The objects the value set says ptr may address.
|
| expr2tc | named_object (const expr2tc &base) const |
| | base if it is a named object, nil otherwise.
|
| bool | resolve_by_value_set (expr2tc &expr, const expr2tc &ptr, const std::function< expr2tc(const expr2tc &)> &resolve) |
| | A pointer reaching a check through a parameter or a local variable is a plain symbol, so the syntactic address_of tests below find no name and the check falls back on __ESBMC_alloc and DYNAMIC_SIZE.
|
| bool | resolve_valid_object_by_value_set (expr2tc &expr, const expr2tc &obj_ref) |
| | Decide VALID_OBJECT from the object the value set names, if it names one.
|
| bool | resolve_dynamic_size_by_value_set (expr2tc &expr) |
| | Size a heap object by its allocation, and an object with automatic or static storage by its type.
|
| void | replace_valid_object (expr2tc &expr) |
| | Decide VALID_OBJECT / DEALLOCATED_OBJ against the object the pointer names.
|
| void | replace_dynamic_size (expr2tc &expr) |
| | Size the object DYNAMIC_SIZE names, falling back to the heap-only table.
|
| void | default_replace_dynamic_allocation (expr2tc &expr) |
| bool | is_valid_object (const symbolt &symbol) |
| | Decide if symbol is valid or not.
|
| void | handle_sideeffect (const expr2tc &lhs, const sideeffect2t &effect, const guard2tc &guard) |
| | Handle side effects in the symbolic execution.
|
| bool | handle_conditional (const expr2tc &lhs, const if2t &if_effect, const guard2tc &guard) |
| | Handle conditional expressions (if2t) in the symbolic execution.
|
| expr2tc | materialise_old_snapshot (const expr2tc &value, const guard2tc &guard) |
| | Give a value storage of its own, for __ESBMC_old.
|
| void | symex_assign_rec (const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc full_rhs, guard2tc &guard, const bool hidden) |
| | Recursively perform symex assign.
|
| void | symex_assign_symbol (const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden) |
| | Perform assignment to a symbol.
|
| void | symex_assign_structure (const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden) |
| | Perform assignment to a structure.
|
| void | symex_assign_array_structure (const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden) |
| | Perform assignment to an array literal.
|
| void | symex_assign_union (const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden) |
| | Perform assignment to a union.
|
| void | symex_assign_extract (const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden) |
| | Perform assignment to an extract irep.
|
| void | symex_assign_typecast (const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden) |
| | Perform assignment to a typecast irep.
|
| void | symex_assign_array (const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden) |
| | Perform assignment to an array.
|
| void | symex_assign_member (const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden) |
| | Perform assignment to a struct.
|
| void | symex_assign_if (const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden) |
| | Perform assignment to an "if".
|
| void | symex_assign_byte_extract (const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden) |
| | Perform assignment to a byte extract.
|
| void | symex_assign_concat (const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden) |
| | Assign through a 'concat' operation.
|
| void | symex_assign_bitfield (const expr2tc &lhs, const expr2tc &full_lhs, expr2tc &rhs, expr2tc &full_rhs, guard2tc &guard, const bool hidden) |
| | This method is used when we need to assign a value to a struct bitfield which is obtained via applying a bit-mask and bit-shifting.
|
| expr2tc | symex_malloc (const expr2tc &lhs, const sideeffect2t &code, const guard2tc &guard) |
| | Symbolic implementation of malloc.
|
| void | symex_realloc (const expr2tc &lhs, const sideeffect2t &code, const guard2tc &guard) |
| | Implementation of realloc.
|
| expr2tc | symex_alloca (const expr2tc &lhs, const sideeffect2t &code, const guard2tc &guard) |
| | Symbolic implementation of alloca.
|
| expr2tc | symex_mem (const bool is_malloc, const expr2tc &lhs, const sideeffect2t &code, const guard2tc &guard) |
| | Wrapper around for alloca and malloc.
|
| void | offer_malloc_zero_null (const expr2tc &size, expr2tc &rhs, guard2tc &alloc_guard) |
| | Offer both outcomes C17 7.22.3p1 permits for a zero-sized malloc, under –malloc-zero-is-null.
|
| expr2tc | symex_mem_inf (const expr2tc &lhs, const type2tc &base_type, const guard2tc &guard) |
| | Wrapper around for infinite array allocation.
|
| void | track_new_pointer (const expr2tc &ptr_obj, const type2tc &new_type, const guard2tc &guard, const expr2tc &size=expr2tc()) |
| | Pointer modelling update function.
|
| void | record_frame_alloca (const expr2tc &lhs, const expr2tc &object, bool is_malloc) |
| | Records an alloca'd object on the current frame, to die when it returns.
|
| void | symex_free (const expr2tc &expr) |
| | Symbolic implementation of free.
|
| void | invalidate_object (const expr2tc &ptr) |
| | Clear the valid bit of the object ptr points to, with no free checks.
|
| void | symex_cpp_delete (const expr2tc &code) |
| | Symbolic implementation of c++'s delete.
|
| void | symex_cpp_new (const expr2tc &lhs, const sideeffect2t &code, const guard2tc &guard) |
| | Symbolic implementation of c++'s new.
|
| expr2tc | symex_sprintf_store (const code_printf2t &call) |
| | Store an unrenamed sprintf or snprintf call's output in its destination buffer, when the format bounds that output's length.
|
| expr2tc | sprintf_output (const code_printf2t &call, size_t fmt_idx, const type2tc &char_type, std::vector< expr2tc > &chars) |
| | The output of an unrenamed sprintf or snprintf call: its characters before the NUL in chars, and its length, nil when unknown.
|
| expr2tc | printf_output_length (const code_printf2t &call, size_t fmt_idx, size_t &max_len) |
| | The length of an unrenamed printf-family call's output whose constant format holds only text and d, i, u or s conversions without flags, width or precision, with its largest value in max_len; nil for any other format.
|
| expr2tc | string_length (const expr2tc &ptr, size_t &max_len) |
| | The characters a s conversion prints for the unrenamed char pointer ptr, adding its largest value to max_len; nil unless ptr resolves to one byte array at a constant offset.
|
| expr2tc | printf_return_length (const expr2tc &lhs, const code_printf2t &call, size_t fmt_idx) |
| | Store an unrenamed sprintf-family call's output and return the length that call returns: the stored length, or for printf, fprintf and dprintf with a used result, printf_output_length.
|
| void | assume_printf_length (const expr2tc &retval, const expr2tc &len) |
| | Assume a printf-family call's return value equals the length of its output, when both are known.
|
| void | assume_printf_range (const expr2tc &retval, const BigInt &lo, const BigInt &hi, bool may_fail) |
| | Assume a printf-family call's return value lies in [lo, hi], or is -1 when may_fail.
|
| void | symex_asprintf_buffer (const expr2tc &strp, const expr2tc &retval) |
| | Point an asprintf/vasprintf call's strp at a fresh heap buffer of retval + 1 bytes, allocated only when retval is non-negative.
|
| bool | format_printf_output (const code_printf2t &call, size_t fmt_idx, printf_formattert &formatter, bool &constant_args) |
| | Run formatter over an unrenamed printf-family call; false when the format is not a constant.
|
| bool | recover_va_list_args (const code_printf2t &call, size_t fmt_idx, std::list< expr2tc > &out) |
| | Recover the variadic arguments hidden behind a va_list operand of a v*printf-family call (vprintf/vfprintf/vsprintf/vsnprintf/vasprintf).
|
| void | symex_input (const code_function_call2t &expr) |
| | Symbolic implementation of scanf and fscanf.
|
| void | symex_va_arg (const expr2tc &lhs, const sideeffect2t &code, const guard2tc &guard) |
| | Symbolic implementation of va_arg.
|
| std::optional< renaming::level2t::name_record > | va_list_l1_record (const expr2tc &va_list_expr) const |
| | Resolve a va_list expression to the l1 identity record of the local variable backing it; nullopt when it cannot be pinned down to one.
|
| std::vector< renaming::level2t::name_record > | va_list_pointee_records (const expr2tc &va_list_expr) const |
| | The l1 identity records of the local va_lists a pointer-valued expression may point to.
|
| bool | va_list_is_started (const expr2tc &va_list_expr) const |
| | Whether the va_list denoted by this expression is known (or assumed) to have been initialised by va_start/va_copy.
|
| void | va_list_mark_started (const expr2tc &va_list_expr, bool started, const expr2tc &cursor) |
| | Record the started-by-va_start state of the va_list denoted by this expression, and the va_arg index it reads next, if known (nil if not).
|
| void | va_list_start (const expr2tc &va_list_expr) |
| | va_start: the va_list reads this frame's first variadic argument next.
|
| expr2tc | va_list_cursor_symbol (const renaming::level2t::name_record &rec) |
| | The l1 symbol holding the va_arg index a local va_list reads next.
|
| expr2tc | va_list_cursor (const expr2tc &va_list_expr) |
| | The cursor symbol of a started local va_list; nil when its cursor is not known, and the frame's cursor applies.
|
| std::vector< renaming::level2t::name_record > | va_list_owner_records (const expr2tc &va_list_expr) const |
| | The records va_list_frame looks for: a va_copy destination's are those of the va_list it was copied from.
|
| void | va_list_copy (const expr2tc &dst, const expr2tc &src) |
| | va_copy: start dst as src is, reading where src reads next.
|
| goto_symex_statet::framet & | va_list_frame (const expr2tc &va_list_expr) |
| | The frame whose variadic arguments a va_list reads: the activation that declared it, which is a caller's when the va_list was passed down.
|
| void | replace_nondet (expr2tc &expr) |
| | Replace nondet func calls with nondeterminism.
|
| bool | is_assume_false (const expr2tc &assumption) |
| | Incrementally check the assumption.
|
| void | assume_uf_congruence (const irep_idt &identifier, const irep_idt &name, const std::vector< expr2tc > &arguments, const expr2tc &result, const type2tc &ret_type) |
| | Assume equal arguments imply an equal result against every earlier application of identifier, and record this one.
|
| void | key_intrinsic_pointer_reads (const code_function_call2t &call, const irep_idt &id) |
| | Key the reads the memcpy/memmove/memcmp/memchr intrinsics perform, which symex carries out internally rather than through a dereference (#7826).
|
| int | CS_number |
| | Number of context switches performed by this ex_state.
|
| std::vector< std::set< expr2tc > > | thread_last_reads |
| | For each thread, a set of symbols that were read by the thread in the last transition (run).
|
| std::vector< std::set< expr2tc > > | thread_last_writes |
| | For each thread, a set of symbols that were written by the thread in the last transition (run).
|
| std::vector< std::vector< int > > | dependency_chain |
| | Dependancy chain for POR calculations.
|
| std::vector< unsigned int > | thread_last_transition |
| | Run-order ordinal of each thread's last completed transition; 0 for a thread that has not run.
|
| unsigned int | transition_ordinal |
| | Ordinal issued to the next completed transition.
|
| bool | mpor_says_no |
| | MPOR scheduling outcome.
|
| bool | cswitch_forced |
| | Indicates a mandatory context switch should occur.
|
| bool | symex_trace |
| | Are we tracing / printing symex instructions?
|
| bool | smt_during_symex |
| | Are we encoding SMT during exploration?
|
| bool | smt_thread_guard |
| | Are we evaluating the thread guard in the SMT solver during context switching?
|
| bool | no_propagation |
| | Was constant propagation disabled with –no-propagation?
|
| optionst & | options |
| | Options we're working with.
|
| irep_idt | guard_identifier_s |
| | Symbol prefix for guards.
|
| persistent_map< irep_idt, expr2tc, irep_id_hash > | guard_definitions |
| | Defining condition of each L2 guard symbol generation, i.e.
|
| persistent_map< irep_idt, expr2tc, irep_id_hash > | copy_definitions |
| | Copy chains between L2 symbol generations: lhs generation -> the stable value it was unconditionally assigned — a (possibly typecast) L2 symbol, or a pure bitvector computation over such leaves (the operand-split idiom).
|
| persistent_map< expr2tc, conjunct_indext, irep2_hash > | guard_prefix_index |
| | prefix_index's result per and-chain node of a path guard.
|
| std::vector< deferred_assumptiont > | deferred_assumptions |
| | Assumptions defer_assumption() holds back, in program order.
|
| bool | claim_skips_deferred = false |
| | Set while claim() handles a Python assert's own condition, which needs no deferred assumption.
|
| std::unordered_map< irep_idt, expr2tc > | dynamic_object_sizes |
| | The renamed byte size each heap object was allocated with, by symbol.
|
| unsigned | first_loop |
| | Loop numbers.
|
| unsigned | total_claims |
| | Number of assertions executed.
|
| unsigned | remaining_claims |
| | Number of assertions remaining to be discharged.
|
| unsigned | simplified_claims |
| | Number of assertions that were trivially verified.
|
| unsigned | bounded_loop_truncations = 0 |
| | Loops cut off at the unwinding bound with no unwinding assertion to flag it, i.e.
|
| reachability_treet * | art1 |
| | Reachability tree we're working with.
|
| std::map< unsigned, BigInt > | unwind_set |
| | Unwind bounds, loop number -> max unwinds.
|
| std::map< std::pair< std::string, unsigned >, BigInt > | unwind_func_set |
| | Unwind bounds by function name and per-function loop index (0-indexed), (function name, loop index) -> max unwinds.
|
| std::map< unsigned, std::pair< std::string, unsigned > > | loop_id_to_func_index |
| | Mapping global loop ID -> (function name, per-function loop index).
|
| BigInt | max_unwind |
| | Global maximum number of unwinds.
|
| std::optional< interval_domaint > | interval_domain_state |
| | Online interval domain: guard pruning is on by default (disable with –no-interval-symex-guard); assertion pruning via –interval-symex-assert discharges claims proven TRUE.
|
| const namespacet & | ns |
| | Namespace we're working in.
|
| contextt & | new_context |
| | Context we're working with.
|
| const goto_functionst & | goto_functions |
| | GOTO functions that we're operating over.
|
| std::shared_ptr< symex_targett > | target |
| | Target listening to the execution trace.
|
| goto_symex_statet * | cur_state |
| | Target thread we're currently operating upon.
|
| irep_idt | valid_ptr_arr_name |
| | Symbol names for modelling arrays.
|
| irep_idt | alloc_size_arr_name |
| irep_idt | dyn_info_arr_name |
| std::list< allocated_obj > | dynamic_memory |
| | List of all allocated objects.
|
| std::map< irep_idt, std::vector< std::pair< std::vector< expr2tc >, expr2tc > > > | uf_applications |
| | Per-callee history of uninterpreted-function applications the SMT backend cannot encode natively, keyed on the mangled callee name.
|
| std::unordered_map< renaming::level2t::name_record, bool, renaming::level2t::name_rec_hash > | va_started |
| | Level-1 identities (base name, activation, thread) of va_list objects initialised by va_start, or by va_copy from a started source, and whether each has a cursor symbol of its own.
|
| std::unordered_map< renaming::level2t::name_record, renaming::level2t::name_record, renaming::level2t::name_rec_hash > | va_copied_from |
| | For each va_copy destination, the local va_list whose frame's variadic arguments it reads, so a copy made in a callee reads the caller's.
|
| bool | no_return_value_opt |
| | Disable return value optimization.
|
| unsigned long | stack_limit |
| | Limit size, in bits, for a single stack frame.
|
| unsigned long | total_stack_limit |
| | Limit size, in bits, for every live stack frame taken together.
|
| unsigned long | depth_limit |
| | Depth limit, as given by the –depth option.
|
| unsigned long | break_insn |
| | Instruction number we are to break at – that is, trap, to the debugger.
|
| bool | memory_leak_check |
| | Flag as to whether we're performing memory leak checks.
|
| bool | no_reachable_memleak |
| | Flag as to whether we're pruning the objects from the memory leak check that are still reachable via global pointers.
|
| bool | no_assertions |
| | Flag as to whether we're checking user assertions.
|
| bool | no_simplify |
| | Flag as to whether we're not simplifying exprs.
|
| bool | no_unwinding_assertions |
| | Flag as to whether we're inserting unwinding assertions.
|
| bool | partial_loops |
| | Flag as to whether we're not enabling partial loops.
|
| bool | k_induction |
| | Flag as to whether we're doing a k-induction.
|
| bool | base_case |
| | Flag as to whether we're doing a k-induction base case.
|
| bool | forward_condition |
| | Flag as to whether we're doing a k-induction forward condition.
|
| bool | inductive_step |
| | Flag as to whether we're doing a k-induction inductive step.
|
| bool | validate_witness |
| | Cached from –validate-violation-witness; checked on every branch/intrinsic.
|
| std::list< dereference_callbackt::internal_item > | internal_deref_items |
| | Set of dereference state records; this field is used as a mailbox between the dereference code and the caller, who will inspect the contents after a call to dereference (in INTERNAL mode) completes.
|
| static constexpr size_t | max_copy_definition_nodes = 64 |
| | Cap on one recorded copy definition's flattened node count: canonicalization doubles nested arithmetic chains per link, and an oversized definition costs more to match than it prunes.
|
1.15.0