#include <symex_bmc.h>
+ Inheritance diagram for symex_bmct:
+ Collaboration diagram for symex_bmct:
Loop unwind handlers take the call stack, loop number, the unwind count so far, and an out-parameter specifying an advisory maximum, which they may set.
Recursion unwind handlers take the function ID, the unwind count so far, and an out-parameter specifying an advisory maximum, which they may set.
The type of delegate functions that retrieve a
goto_functiont for a particular function identifier.
Add a callback function that will be called to determine whether to unwind loops.
Add a callback function that will be called to determine whether to unwind recursion.
Construct a
goto_symext to execute a particular program.
A virtual destructor allowing derived classes to be cleaned up correctly.
Symbolically execute the entire program starting from entry point.
Puts the initial state of the entry point function into the path storage.
Performs symbolic execution using a state and equation that have already been used to symbolically execute part of the program.
Symbolically execute the entire program starting from entry point.
Defines condition for interrupting symbolic execution for a specific loop.
Set when states are pushed onto the workqueue If this flag is set at the end of a symbolic execution run, it means that symbolic execution has been paused because we encountered a GOTO instruction while doing path exploration, and thus pushed the successor states of the GOTO onto path_storage.
If this flag is set to true then assertions will be temporarily ignored by the symbolic executions.
Number of VCCs generated during the run of this
goto_symext object.
Protected Member Functions
show progress
Merge a single branch, the symbolic state of which is held in goto_state, into the current overall symbolic state.
Determine whether to unwind a loop.
- Protected Member Functions inherited from
goto_symext Initialize the symbolic execution and the given state with the beginning of the entry point function.
Invokes symex_step and verifies whether additional threads can be executed.
Executes the instruction
state.source.pc Case-switches over the type of the instruction being executed and calls another function appropriate to the instruction type, for example
symex_function_call if the current instruction is a function call,
symex_goto if the current instruction is a goto, etc.
Prints the route of symex as it walks through the code.
Clean up an expression.
Given an expression, find the root object and the offset into it.
Replace all dereference operations within expr with explicit references to the objects they may refer to.
If
expr is a
dereference_exprt, replace it with explicit references to the objects it may point to.
Transforms an lvalue expression by replacing any dereference operations it contains with explicit references to the objects they may point to (using
goto_symext::dereference_rec), and translates
byte_extract, member and
index operations into integer offsets from a root symbol (if any).
Symbolically execute a GOTO instruction.
Symbolically execute a GOTO instruction in the context of unreachable code.
Symbolically execute a SET_RETURN_VALUE instruction.
Symbolically execute a START_THREAD instruction.
Symbolically execute an ATOMIC_BEGIN instruction.
Symbolically execute an ATOMIC_END instruction.
Symbolically execute a DECL instruction.
Symbolically execute a DECL instruction for the given symbol or simulate such an execution for a synthetic symbol.
Symbolically execute a DEAD instruction.
Kill a symbol, as if it had been the subject of a DEAD instruction.
Symbolically execute an OTHER instruction.
Propagate constants and points-to information implied by a GOTO condition.
Try to filter value sets based on whether possible values of a pointer-typed symbol make the condition true or false.
Symbolically execute a verification condition (assertion).
Symbolically execute an ASSUME instruction or simulate such an execution for a synthetic assumption.
Merge all branches joining at the current program point.
Merge the SSA assignments from goto_state into dest_state.
Symbolically execute a FUNCTION_CALL instruction.
Preserves locality of parameters of a given function by applying L1 renaming to them.
Symbolically execute a END_FUNCTION instruction.
Symbolic execution of a call to a function call.
Symbolic execution of a function call by inlining.
Iterates over arguments and assigns them to the parameters, which are symbols whose name and type are deduced from the type of goto_function.
Symbolically execute a THROW instruction.
Symbolically execute a CATCH instruction.
Symbolically execute an ASSIGN instruction or simulate such an execution for a synthetic assignment.
Attempt to constant propagate side effects of the assignment (if any)
Create an empty string constant.
Attempt to constant propagate string concatenation.
Attempt to constant propagate getting a substring of a string.
Attempt to constant propagate converting an integer to a string.
Attempt to constant propagate deleting a character from a string.
Attempt to constant propagate deleting a substring from a string.
Attempt to constant propagate setting the length of a string.
Attempt to constant propagate setting the char at the given index.
Attempt to constant propagate trim operations.
Attempt to constant propagate case changes, both upper and lower.
Attempt to constant proagate character replacement.
Assign constant string length and string data given by a char array to given ssa variables.
Installs a new symbol in the symbol table to represent the given character array, and assigns the character array to the symbol.
Generate array to pointer association primitive.
Execute a single let expression, which should not have any nested let expressions (use
lift_lets instead if there might be).
Symbolically execute an assignment instruction that has an allocate on the right hand side.
Symbolically execute an OTHER instruction that does a CPP delete
Handles side effects of type 'new' for C++ and 'new array' for C++ and Java language modes.
Symbolically execute an OTHER instruction that does a CPP printf
Symbolically execute an OTHER instruction that does a CPP input.
Symbolically execute an OTHER instruction that does a CPP output.
Callbacks that may provide an unwind/do-not-unwind decision for a loop.
Callbacks that may provide an unwind/do-not-unwind decision for a recursive call.
The configuration to use for this symbolic execution.
language_mode: ID_java, ID_C or another language identifier if we know the source language in use,
irep_idt() otherwise.
The symbol table associated with the goto-program being executed.
Initialized just before symbolic execution begins, to point to both
outer_symbol_table and the symbol table owned by the
goto_symex_statet object used during symbolic execution.
Used to create guards.
The equation that this execution is building up.
A monotonically increasing index for each encountered ATOMIC_BEGIN instruction.
Variables that should be killed at the end of the current symex_step invocation.
The messaget to write log messages to.
Symbolic execution paths to be resumed later.
Shadow memory instrumentation API.
Additional Inherited Members
- Static Public Member Functions inherited from
goto_symext Return a function to get/load a goto function from the given goto model Create a default delegate to retrieve function bodies from a
goto_functionst.
- Static Protected Member Functions inherited from
goto_symext
Detailed Description
Member Typedef Documentation
◆ loop_unwind_handlert
Loop unwind handlers take the call stack, loop number, the unwind count so far, and an out-parameter specifying an advisory maximum, which they may set.
If set the advisory maximum is set it is only used to print useful information for the user (e.g. "unwinding iteration N, max M"), and is not enforced. They return true to halt unwinding, false to authorise unwinding, or Unknown to indicate they have no opinion.
Definition at line 46 of file symex_bmc.h.
◆ recursion_unwind_handlert
Recursion unwind handlers take the function ID, the unwind count so far, and an out-parameter specifying an advisory maximum, which they may set.
If set the advisory maximum is set it is only used to print useful information for the user (e.g. "unwinding iteration N, max M"), and is not enforced. They return true to halt unwinding, false to authorise unwinding, or Unknown to indicate they have no opinion.
Definition at line 55 of file symex_bmc.h.
Constructor & Destructor Documentation
◆ symex_bmct()
Member Function Documentation
◆ add_loop_unwind_handler()
Add a callback function that will be called to determine whether to unwind loops.
The first function added will get the first chance to answer, and the first authoratitive (true or false) answer is final.
- Parameters
-
handler new callback
Definition at line 61 of file symex_bmc.h.
◆ add_recursion_unwind_handler()
Add a callback function that will be called to determine whether to unwind recursion.
The first function added will get the first chance to answer, and the first authoratitive (true or false) answer is final.
- Parameters
-
handler new callback
Definition at line 70 of file symex_bmc.h.
◆ get_unwind_recursion()
)
overrideprotectedvirtual
◆ merge_goto()
)
overrideprotectedvirtual
Merge a single branch, the symbolic state of which is held in goto_state, into the current overall symbolic state.
goto_state is no longer expected to be valid afterwards.
- Parameters
-
source source associated with the incoming goto_state
goto_state A state to be merged into this location
state Symbolic execution state to be updated
Reimplemented from goto_symext.
Definition at line 107 of file symex_bmc.cpp.
◆ output_coverage_report()
◆ should_stop_unwind()
)
overrideprotectedvirtual
Determine whether to unwind a loop.
- Parameters
-
source
context
unwind
- Returns
- true indicates abort, with false we continue
Reimplemented from goto_symext.
Definition at line 127 of file symex_bmc.cpp.
◆ symex_step()
)
overrideprotectedvirtual
Member Data Documentation
◆ last_source_location
◆ loop_unwind_handlers
Callbacks that may provide an unwind/do-not-unwind decision for a loop.
Definition at line 88 of file symex_bmc.h.
◆ record_coverage
◆ recursion_unwind_handlers
Callbacks that may provide an unwind/do-not-unwind decision for a recursive call.
Definition at line 92 of file symex_bmc.h.
◆ symex_coverage
◆ unwindset
The documentation for this class was generated from the following files:
