|
ROSE 0.11.145.147
|
Path searching functor.
This is the base class for user-defined functors called when searching for feasible paths.
Definition at line 178 of file FeasiblePath.h.
#include <Rose/BinaryAnalysis/FeasiblePath.h>
Public Types | |
| enum | Action { BREAK , CONTINUE } |
| Enumerator | |
|---|---|
| BREAK | Do not continue along this path. |
| CONTINUE | Continue along this path. |
Definition at line 180 of file FeasiblePath.h.
|
inlinevirtual |
Definition at line 185 of file FeasiblePath.h.
|
virtual |
Function invoked whenever a complete path is found.
The analyzer is a reference to the analyzer that's invoking this callback.
The path enumerates the CFG vertices and edges that compose the path.
The cpu represents the machine state at the start of the final vertex of the path. Modifications to the state have undefined behavior; the state may be re-used by the analysis when testing subsequent paths.
The solver contains the assertions that are satisfied to prove that this path is feasible. The solver contains multiple levels: an initial level that's probably empty (trivially satisfiable), followed by an additional level pushed for each edge of the path.
The return value from this callback determines whether the analysis will search for additional paths. A return value of Action::CONTINUE means the model checker will try other paths, and a return value of Action::BREAK means no more paths will be tested.
|
virtual |
Function invoked whenever a null pointer dereference is detected.
The following parameters are passed to this callback:
The analyzer is the state of the analysis at the time that the null dereference is detected. Additional information such as the partitioner is available through this object.
The path is the execution path from a starting vertex to the vertex in which the null dereference occurs. Each vertex of the path is a basic block or function summary. All but the last vertex will have a corresponding symbolic state of the model checker as it existed at the end of processing the vertex. These states should not be modified by this callback.
The insn is the instruction during which the null dereference occurred and may be a null pointer in some situations. For instance, the instruction will be null if the dereference occurs when popping the return address from the stack for a function that was called but whose implementation is not present (such as when the inter-procedural depth was too great, the function is a non-linked import, etc.)
The cpu is the model checker's state immediately prior to the null dereference. This callback must not modify the state.
The solver is the optional SMT solver used to conclude that the execution path is feasible and that a null dereference occurs. This callback can query the SMT solver to obtain information about the evidence of satisfiability. This callback may use the solver for additional work either in its current transaction or by pushing additional transactions; this callback should not pop the current transaction.
The ioMode indicates whether the null address was read or written.
The addr is the address that was accessed. Depending on the model checker's settings, this is either a constant or a symbolic expression. In the latter case, the solver will have evidence that the expression can be zero.
The return value indicates whether the model checker should continue along the same path (Action::CONTINUE) or backtrack (Action::BREAK). If this callback requests backtracking then the model checker may continue evaluating the current path vertex but will not call any more more path processing functions until the backtrack occurs.
|
virtual |
Function invoked every time a memory reference occurs.
The following parameters are passed to this callback:
The analyzer is the state of the analysis at the time that the memory I/O is detected. Additional information such as the partitioner is available through this object.
The path is the execution path from a starting vertex to the vertex in which the memory I/O occurs. Each vertex of the path is a basic block or function summary. All but the last vertex will have a corresponding symbolic state of the model checker as it existed at the end of processing the vertex. These states should not be modified by this callback.
The insn is the instruction during which the memoryIo occurred and may be a null pointer in some situations. For instance, the instruction will be null if the I/O occurs when popping the return address from the stack for a function that was called but whose implementation is not present (such as when the inter-procedural depth was too great, the function is a non-linked import, etc.)
The cpu is the model checker's state immediately prior to the memory I/O. This callback must not modify the state.
The solver is the optional SMT solver used to conclude that the execution path is feasible. This callback can query the SMT solver to obtain information about the evidence of satisfiability. This callback may use the solver for additional work either in its current transaction or by pushing additional transactions; this callback should not pop the current transaction.
The ioMode indicates whether the memory address was read or written.
The addr is the address that was accessed.
The value is the value read or written.
The insn is the instruction during which the null dereference occurred and may be a null pointer in some situations. For instance, the instruction will be null if the dereference occurs when popping the return address from the stack for a function that was called but whose implementation is not present (such as when the inter-procedural depth was too great, the function is a non-linked import, etc.).
The return value indicates whether the model checker should continue along the same path (Action::CONTINUE) or backtrack (Action::BREAK). If this callback requests backtracking then the model checker may continue evaluating the current path vertex but will not call any more more path processing functions until the backtrack occurs.
1.9.8