Static Value-Flow Analysis
|
AbstractInterpretation is same as Abstract Execution. More...
#include <AbstractInterpretation.h>
Public Types | |
enum | HandleRecur { TOP , WIDEN_ONLY , WIDEN_NARROW } |
typedef SCCDetection< CallGraph * > | CallGraphSCC |
Public Member Functions | |
AbstractInterpretation () | |
Constructor. | |
virtual void | runOnModule (ICFG *icfg) |
virtual | ~AbstractInterpretation () |
Destructor. | |
void | analyse () |
Program entry. | |
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 |
AEStat * | stat |
std::vector< const CallICFGNode * > | callSiteStack |
Map< const FunObjVar *, const ICFGWTO * > | funcToWTO |
Set< std::pair< const CallICFGNode *, NodeID > > | nonRecursiveCallSites |
Set< const FunObjVar * > | recursiveFuns |
Map< std::string, std::function< void(const CallICFGNode *)> > | func_map |
Map< const ICFGNode *, AbstractState > | abstractTrace |
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 104 of file AbstractInterpretation.h.
Definition at line 112 of file AbstractInterpretation.h.
Enumerator | |
---|---|
TOP | |
WIDEN_ONLY | |
WIDEN_NARROW |
Definition at line 129 of file AbstractInterpretation.h.
AbstractInterpretation::AbstractInterpretation | ( | ) |
|
virtual |
Destructor.
Definition at line 68 of file AbstractInterpretation.cpp.
|
inline |
Definition at line 153 of file AbstractInterpretation.h.
void AbstractInterpretation::analyse | ( | ) |
Program entry.
Definition at line 148 of file AbstractInterpretation.cpp.
|
private |
Definition at line 1106 of file AbstractInterpretation.cpp.
|
private |
Definition at line 1066 of file AbstractInterpretation.cpp.
|
privatevirtual |
Definition at line 699 of file AbstractInterpretation.cpp.
|
privatevirtual |
Definition at line 640 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 166 of file AbstractInterpretation.h.
|
inlinestatic |
Definition at line 147 of file AbstractInterpretation.h.
|
inlineprivate |
Definition at line 309 of file AbstractInterpretation.h.
handle call node in ICFGNode
node | ICFGNode which has a single CallICFGNode |
Definition at line 608 of file AbstractInterpretation.cpp.
|
privatevirtual |
handle wto cycle (loop)
handle wto cycle (loop)
cycle | WTOCycle which has weak topo order of basic blocks and nested cycles |
Definition at line 775 of file AbstractInterpretation.cpp.
|
privatevirtual |
Global ICFGNode is handled at the entry of the program,.
handle global node
Definition at line 163 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 556 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 862 of file AbstractInterpretation.cpp.
|
private |
Definition at line 590 of file AbstractInterpretation.cpp.
|
private |
Handle two types of WTO components (singleton and cycle)
Definition at line 582 of file AbstractInterpretation.cpp.
Definition at line 304 of file AbstractInterpretation.h.
|
privatevirtual |
Definition at line 740 of file AbstractInterpretation.cpp.
|
private |
Compute IWTO for each function partition entry.
Compute WTO for each function partition entry.
This function first identifies function partition entries (pair: <entry, function set>), and then compute the IWTO for each pair. It does this by detecting call graph's strongly connected components (SCC). Each SCC forms a function partition, and any function that is invoked from outside its SCC is identified as an entry of the function partition.
Definition at line 84 of file AbstractInterpretation.cpp.
|
private |
Check if execution state exist at the branch edge
intraEdge | the edge from CmpStmt to the next node |
Definition at line 528 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 258 of file AbstractInterpretation.cpp.
|
privatevirtual |
Definition at line 691 of file AbstractInterpretation.cpp.
|
privatevirtual |
Definition at line 635 of file AbstractInterpretation.cpp.
|
privatevirtual |
Definition at line 734 of file AbstractInterpretation.cpp.
|
privatevirtual |
Definition at line 656 of file AbstractInterpretation.cpp.
|
privatevirtual |
Definition at line 684 of file AbstractInterpretation.cpp.
Definition at line 651 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 484 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 178 of file AbstractInterpretation.cpp.
|
privatevirtual |
Definition at line 665 of file AbstractInterpretation.cpp.
|
virtual |
collect checkpoint
Definition at line 43 of file AbstractInterpretation.cpp.
|
privatevirtual |
Check if this callnode is recursive call and skip it.
callnode | CallICFGNode which calls a recursive function |
Definition at line 923 of file AbstractInterpretation.cpp.
Definition at line 1212 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 1222 of file AbstractInterpretation.cpp.
Definition at line 1284 of file AbstractInterpretation.cpp.
Definition at line 1515 of file AbstractInterpretation.cpp.
Definition at line 1122 of file AbstractInterpretation.cpp.
Definition at line 1499 of file AbstractInterpretation.cpp.
Definition at line 1156 of file AbstractInterpretation.cpp.
Definition at line 1203 of file AbstractInterpretation.cpp.
|
private |
Definition at line 1138 of file AbstractInterpretation.cpp.
Definition at line 1507 of file AbstractInterpretation.cpp.
Definition at line 107 of file AbstractInterpretation.h.
Definition at line 106 of file AbstractInterpretation.h.
|
friend |
Definition at line 108 of file AbstractInterpretation.h.
|
friend |
Definition at line 109 of file AbstractInterpretation.h.
|
private |
Definition at line 329 of file AbstractInterpretation.h.
Execution State, used to store the Interval Value of every SVF variable.
Definition at line 293 of file AbstractInterpretation.h.
|
private |
Definition at line 298 of file AbstractInterpretation.h.
Set<const CallICFGNode*> SVF::AbstractInterpretation::checkpoints |
Definition at line 158 of file AbstractInterpretation.h.
|
private |
Definition at line 332 of file AbstractInterpretation.h.
|
private |
Definition at line 327 of file AbstractInterpretation.h.
Definition at line 299 of file AbstractInterpretation.h.
|
private |
Definition at line 295 of file AbstractInterpretation.h.
|
private |
Definition at line 330 of file AbstractInterpretation.h.
|
private |
Definition at line 300 of file AbstractInterpretation.h.
Definition at line 301 of file AbstractInterpretation.h.
|
private |
Definition at line 296 of file AbstractInterpretation.h.
|
private |
protected data members, also used in subclasses
Definition at line 291 of file AbstractInterpretation.h.
|
private |
Definition at line 333 of file AbstractInterpretation.h.