|
Static Value-Flow Analysis
|
AbstractInterpretation is same as Abstract Execution. More...
#include <AbstractInterpretation.h>
Public Types | |
| enum | HandleRecur { TOP , WIDEN_ONLY , WIDEN_NARROW } |
Public Member Functions | |
| AbstractInterpretation () | |
| Constructor. | |
| virtual void | runOnModule (ICFG *icfg) |
| virtual | ~AbstractInterpretation () |
| Destructor. | |
| void | analyse () |
| Program entry. | |
| void | analyzeFromAllProgEntries () |
| Analyze all entry points (functions without callers) | |
| std::deque< const FunObjVar * > | collectProgEntryFuns () |
| Get all entry point functions (functions without callers) | |
| void | addDetector (std::unique_ptr< AEDetector > detector) |
| AbstractState & | getAbsStateFromTrace (const ICFGNode *node) |
| Retrieves the abstract state from the trace for a given ICFG node. | |
Static Public Member Functions | |
| static AbstractInterpretation & | getAEInstance () |
Public Attributes | |
| Set< const CallICFGNode * > | checkpoints |
Private Attributes | |
| SVFIR * | svfir |
| protected data members, also used in subclasses | |
| AEAPI * | api {nullptr} |
| Execution State, used to store the Interval Value of every SVF variable. | |
| ICFG * | icfg |
| CallGraph * | callGraph |
| AEStat * | stat |
| PreAnalysis * | preAnalysis {nullptr} |
| Map< std::string, std::function< void(const CallICFGNode *)> > | func_map |
| Map< const ICFGNode *, AbstractState > | abstractTrace |
| Set< const ICFGNode * > | allAnalyzedNodes |
| std::string | moduleName |
| std::vector< std::unique_ptr< AEDetector > > | detectors |
| AbsExtAPI * | utils |
| Map< s32_t, s32_t > | _reverse_predicate |
| Map< s32_t, s32_t > | _switch_lhsrhs_predicate |
Friends | |
| class | AEStat |
| class | AEAPI |
| class | BufOverflowDetector |
| class | NullptrDerefDetector |
AbstractInterpretation is same as Abstract Execution.
Definition at line 107 of file AbstractInterpretation.h.
| Enumerator | |
|---|---|
| TOP | |
| WIDEN_ONLY | |
| WIDEN_NARROW | |
Definition at line 130 of file AbstractInterpretation.h.
| AbstractInterpretation::AbstractInterpretation | ( | ) |
|
virtual |
Destructor.
Definition at line 75 of file AbstractInterpretation.cpp.
|
inline |
Definition at line 161 of file AbstractInterpretation.h.
| void AbstractInterpretation::analyse | ( | ) |
Program entry.
Program entry - analyze from all entry points (multi-entry analysis is the default)
Definition at line 117 of file AbstractInterpretation.cpp.
| void AbstractInterpretation::analyzeFromAllProgEntries | ( | ) |
Analyze all entry points (functions without callers)
Analyze all entry points (functions without callers) - for whole-program analysis. Abstract state is shared across entry points so that functions analyzed from earlier entries are not re-analyzed from scratch.
Definition at line 126 of file AbstractInterpretation.cpp.
|
private |
Definition at line 1346 of file AbstractInterpretation.cpp.
|
private |
Definition at line 1306 of file AbstractInterpretation.cpp.
Get all entry point functions (functions without callers)
Collect entry point functions for analysis. Entry points are functions without callers (no incoming edges in CallGraph). Uses a deque to allow efficient insertion at front for prioritizing main()
Definition at line 84 of file AbstractInterpretation.cpp.
|
inline |
Retrieves the abstract state from the trace for a given ICFG node.
| node | Pointer to the ICFG node. |
| Assertion | if no trace exists for the node. |
Definition at line 174 of file AbstractInterpretation.h.
|
inlinestatic |
Definition at line 155 of file AbstractInterpretation.h.
|
private |
Get callee function: directly for direct calls, via pointer analysis for indirect calls.
Definition at line 821 of file AbstractInterpretation.cpp.
|
private |
Get the next nodes of a node within the same function
| node | The node to get successors for |
Get the next nodes of a node within the same function For CallICFGNode, includes shortcut to RetICFGNode
Definition at line 649 of file AbstractInterpretation.cpp.
|
private |
Get the next nodes outside a cycle
| cycle | The cycle to get exit successors for |
Get the next nodes outside a cycle Inner cycles are skipped since their next nodes cannot be outside the outer cycle
Definition at line 674 of file AbstractInterpretation.cpp.
|
inlineprivate |
Definition at line 333 of file AbstractInterpretation.h.
handle call node in ICFGNode
| node | ICFGNode which has a single CallICFGNode |
Definition at line 754 of file AbstractInterpretation.cpp.
|
privatevirtual |
Definition at line 777 of file AbstractInterpretation.cpp.
|
privatevirtual |
Handle direct or indirect call: get callee(s), process function body, set return state.
For direct calls, the callee is known statically. For indirect calls, the previous implementation resolved callees from the abstract state's address domain, which only picked the first address and missed other targets. Since the abstract state's address domain is not an over-approximation for function pointers (it may be uninitialized or incomplete), we now use Andersen's pointer analysis results from the pre-computed call graph, which soundly resolves all possible indirect call targets.
Definition at line 900 of file AbstractInterpretation.cpp.
|
private |
Handle a function using worklist algorithm
| funEntry | The entry node of the function to handle |
Handle a function using worklist algorithm guided by WTO order. All top-level WTO components are pushed into the worklist upfront, so the traversal order is exactly the WTO order — each node is visited once, and cycles are handled as whole components.
Definition at line 729 of file AbstractInterpretation.cpp.
|
privatevirtual |
Global ICFGNode is handled at the entry of the program,.
handle global node Initializes the abstract state for the global ICFG node and processes all global statements. This includes setting up the null pointer and black hole pointer (blkPtr). BlkPtr is initialized to point to the BlackHole object, representing an unknown memory location that cannot be statically resolved.
Definition at line 150 of file AbstractInterpretation.cpp.
Handle an ICFG node by merging states and processing statements
| node | The ICFG node to handle |
Handle an ICFG node by merging states from predecessors and processing statements Returns true if the abstract state has changed, false if fixpoint reached or infeasible
Definition at line 577 of file AbstractInterpretation.cpp.
|
privatevirtual |
handle wto cycle (loop)
| cycle | WTOCycle which has weak topo order of basic blocks and nested cycles |
Handle WTO cycle (loop or recursive function) using widening/narrowing iteration.
Widening is applied at the cycle head to ensure termination of the analysis. The cycle head's abstract state is iteratively updated until a fixpoint is reached.
== What is being widened == The abstract state at the cycle head node, which includes:
i starting at 0 and incrementing each iteration== Regular loops (non-recursive functions) == All modes (TOP/WIDEN_ONLY/WIDEN_NARROW) behave the same for regular loops:
== Recursive function cycles == Behavior depends on Options::HandleRecur():
Definition at line 977 of file AbstractInterpretation.cpp.
|
privatevirtual |
Handle recursive call in TOP mode: set all stores and return value to TOP.
Definition at line 793 of file AbstractInterpretation.cpp.
|
privatevirtual |
handle instructions in svf basic blocks
handle instructions in ICFGSingletonWTO
| block | basic block that has one instruction or a series of instructions |
Definition at line 550 of file AbstractInterpretation.cpp.
handle SVF Statement like CmpStmt, CallStmt, GepStmt, LoadStmt, StoreStmt, etc.
| stmt | SVFStatement which is a value flow of instruction |
Definition at line 1056 of file AbstractInterpretation.cpp.
Definition at line 328 of file AbstractInterpretation.h.
|
private |
Check if execution state exist at the branch edge
| intraEdge | the edge from CmpStmt to the next node |
Definition at line 522 of file AbstractInterpretation.cpp.
|
private |
Check if this cmpStmt and succ are satisfiable to the execution state.
| cmpStmt | CmpStmt is a conditional branch statement |
| succ | the value of cmpStmt (True or False) |
Definition at line 252 of file AbstractInterpretation.cpp.
|
privatevirtual |
Definition at line 772 of file AbstractInterpretation.cpp.
|
privatevirtual |
Check if caller and callee are in the same CallGraph SCC (i.e. a recursive callsite)
Definition at line 813 of file AbstractInterpretation.cpp.
Check if a function is recursive (part of a call graph SCC)
Definition at line 787 of file AbstractInterpretation.cpp.
|
private |
Check if this SwitchInst and succ are satisfiable to the execution state.
| var | var in switch inst |
| succ | the case value of switch inst |
Definition at line 478 of file AbstractInterpretation.cpp.
Check if execution state exist by merging states of predecessor nodes
| icfgNode | The icfg node to analyse |
get execution state by merging states of predecessor blocks Scenario 1: preblock --—(intraEdge)-—> block, join the preES of inEdges Scenario 2: preblock --—(callEdge)-—> block
Definition at line 181 of file AbstractInterpretation.cpp.
|
virtual |
collect checkpoint
Definition at line 44 of file AbstractInterpretation.cpp.
|
privatevirtual |
Set all store values in a recursive function to TOP (used in TOP mode)
Definition at line 1118 of file AbstractInterpretation.cpp.
Check if narrowing should be applied: always for regular loops, mode-dependent for recursion.
Definition at line 869 of file AbstractInterpretation.cpp.
|
private |
Skip recursive callsites (within SCC); entry calls from outside SCC are not skipped.
Definition at line 851 of file AbstractInterpretation.cpp.
Definition at line 1452 of file AbstractInterpretation.cpp.
|
private |
Find the comparison predicates in "class BinaryOPStmt:OpCode" under SVF/svf/include/SVFIR/SVFStatements.h You are only required to handle integer predicates, including Add, FAdd, Sub, FSub, Mul, FMul, SDiv, FDiv, UDiv, SRem, FRem, URem, Xor, And, Or, AShr, Shl, LShr
Definition at line 1462 of file AbstractInterpretation.cpp.
Definition at line 1524 of file AbstractInterpretation.cpp.
Definition at line 1769 of file AbstractInterpretation.cpp.
Definition at line 1362 of file AbstractInterpretation.cpp.
Definition at line 1753 of file AbstractInterpretation.cpp.
Definition at line 1396 of file AbstractInterpretation.cpp.
Definition at line 1443 of file AbstractInterpretation.cpp.
|
private |
Definition at line 1378 of file AbstractInterpretation.cpp.
Definition at line 1761 of file AbstractInterpretation.cpp.
Definition at line 110 of file AbstractInterpretation.h.
Definition at line 109 of file AbstractInterpretation.h.
|
friend |
Definition at line 111 of file AbstractInterpretation.h.
|
friend |
Definition at line 112 of file AbstractInterpretation.h.
|
private |
Definition at line 353 of file AbstractInterpretation.h.
Definition at line 354 of file AbstractInterpretation.h.
Execution State, used to store the Interval Value of every SVF variable.
Definition at line 319 of file AbstractInterpretation.h.
|
private |
Definition at line 322 of file AbstractInterpretation.h.
| Set<const CallICFGNode*> SVF::AbstractInterpretation::checkpoints |
Definition at line 166 of file AbstractInterpretation.h.
|
private |
Definition at line 357 of file AbstractInterpretation.h.
|
private |
Definition at line 351 of file AbstractInterpretation.h.
|
private |
Definition at line 321 of file AbstractInterpretation.h.
|
private |
Definition at line 355 of file AbstractInterpretation.h.
|
private |
Definition at line 325 of file AbstractInterpretation.h.
|
private |
Definition at line 323 of file AbstractInterpretation.h.
|
private |
protected data members, also used in subclasses
Definition at line 317 of file AbstractInterpretation.h.
|
private |
Definition at line 358 of file AbstractInterpretation.h.