|
Static Value-Flow Analysis
|
#include <MHP.h>
Classes | |
| struct | NodeThreadSummary |
Public Types | |
| enum class | StateRepresentation { MaterializedContexts , QuerySummaries } |
| typedef Set< const FunObjVar * > | FunSet |
| typedef FIFOWorkList< CxtThreadStmt > | CxtThreadStmtWorkList |
| typedef Set< CxtThreadStmt > | CxtThreadStmtSet |
| typedef Map< CxtThreadStmt, NodeBS > | ThreadStmtToThreadInterleav |
| typedef Map< const ICFGNode *, CxtThreadStmtSet > | InstToThreadStmtSetMap |
| typedef Map< const ICFGNode *, NodeThreadSummary > | InstToThreadSummaryMap |
| typedef SVFLoopAndDomInfo::LoopBBs | LoopBBs |
| typedef Set< CxtStmt > | LockSpan |
| typedef std::pair< const FunObjVar *, const FunObjVar * > | FuncPair |
| typedef Map< FuncPair, bool > | FuncPairToBool |
Static Public Member Functions | |
| template<class ICFGGraph , class CGGraph > | |
| static std::unique_ptr< MHP > | create (TCT *t, ICFGGraph icfg, CGGraph cg, StateRepresentation representation=StateRepresentation::MaterializedContexts) |
| Construct MHP and initialize its graph-dependent ForkJoinAnalysis. | |
Public Attributes | |
| u32_t | numOfTotalQueries |
| Total number of queries. | |
| u32_t | numOfMHPQueries |
| Number of queries are answered as may-happen-in-parallel. | |
| double | interleavingTime |
| double | interleavingQueriesTime |
Protected Types | |
| typedef Map< const SVFBasicBlock *, std::vector< CxtStmt > > | BBToSymJoinsMap |
| typedef Map< CxtStmt, Set< const SVFBasicBlock * > > | SymJoinToLoopMap |
Protected Attributes | |
| ThreadCallGraph * | tcg |
| TCG. | |
| TCT * | tct |
| TCT. | |
| ForkJoinAnalysis * | fja |
| ForJoin Analysis. | |
| CxtThreadStmtWorkList | cxtStmtList |
| CxtThreadStmt worklist. | |
| ThreadStmtToThreadInterleav | threadStmtToThreadInterLeav |
| BBToSymJoinsMap | bbToSymJoins |
| Map a statement to its thread interleavings. | |
| SymJoinToLoopMap | symJoinLoop |
| symmetric in-loop join -> its loop's blocks | |
| InstToThreadStmtSetMap | instToTSMap |
| Map an instruction to its ThreadStmtSet. | |
| InstToThreadSummaryMap | instToThreadSummary |
| Exact per-node/per-tid query compression. | |
| Map< const ICFGNode *, const ICFGNode * > | querySummaryOwner |
| Non-candidate node -> entry summary. | |
| StateRepresentation | stateRepresentation |
| FuncPairToBool | nonCandidateFuncMHPRelMap |
This class serves as a base may-happen in parallel analysis for multithreaded program Given a statement under an abstract thread, it tells which abstract threads may be alive at the same time (May-happen-in-parallel).
|
protected |
|
protected |
|
virtual |
Destructor.
Destructor
|
explicitprotected |
Construction is paired with ForkJoinAnalysis initialization by create().
| representation | Keep per-context copies for clients that enumerate raw states (the pre-analysis detector and slicer). Main-phase clients issue only MHP queries and can use the exact projected query summary instead. |
Constructor
|
inlineprotected |
|
inlineprotected |
|
inlineprotected |
| template void MHP::analyze< const SlicedICFGView *, const SlicedThreadCallGraphView * > | ( | ICFGGraph | icfg, |
| CGGraph | cg | ||
| ) |
Start analysis here. One implementation for the whole program and a slice: the compute is templated on the two graphs it traverses – the ICFG (ICFG* whole / const SlicedICFGView* sliced) and the CallGraph (CallGraph* whole / const SlicedThreadCallGraphView* sliced) – and calls their GenericGraphTraits specialisations directly (no wrapper layer).
Start analysis here
Definition at line 115 of file MHP.cpp.
Analyze thread interleaving.
Analyze thread interleaving
handle non-candidate function
handle candidate function
update non-candidate functions' interleaving
Definition at line 129 of file MHP.cpp.
Build the exact, context-compressed representation used by repeated MHP queries after the context-sensitive fixed point has converged.
Compress the converged context-sensitive states for repeated MHP queries. Contexts are retained in the propagation maps; this is a query-only index and therefore cannot change the fixed point.
Definition at line 201 of file MHP.cpp.
|
protected |
Index the SCEV-symmetric in-loop joins by their loop blocks.
Definition at line 60 of file MHP.cpp.
|
static |
Construct MHP and initialize its graph-dependent ForkJoinAnalysis.
Definition at line 646 of file MHP.h.
|
protected |
Flow along edge cts.stmt -> dst: an edge leaving a symmetric join loop drops the joined tids (edge kill; the destination's state is never subtracted from).
Definition at line 77 of file MHP.cpp.
Definition at line 866 of file MHP.cpp.
|
protected |
Return thread id(s) which are directly or indirectly joined at this join site.
Return thread id(s) which are directly or indirectly joined at this join site
Definition at line 729 of file MHP.cpp.
|
inline |
Get interleaving thread for statement inst.
|
protected |
|
inline |
|
inline |
|
inline |
Get/has ThreadStmt.
Definition at line 142 of file MHP.h.
| const MHP::NodeThreadSummary * MHP::getThreadSummary | ( | const ICFGNode * | inst | ) | const |
Representation-independent per-thread summary used by MHP clients. Available after analyze() in both materialized and summary-only modes.
Definition at line 257 of file MHP.cpp.
|
protected |
Handle call.
Handle call instruction in the current thread scope (excluding any fork site)
Propagate to the return site of the call instruction, only if the callee is a non-candidate function, while for candidate function, return site should be handled after the callee is handled.
Definition at line 438 of file MHP.cpp.
|
protected |
|
protected |
Handle intra.
Handling intraprocedural statements (successive statements on the CFG )
Definition at line 585 of file MHP.cpp.
|
protected |
Handle join.
Handle join
for the join site in a loop loop which does not join the current thread we process the loop exit
Definition at line 374 of file MHP.cpp.
|
protected |
Handle non-candidate function.
Handle call instruction in the current thread scope (excluding any fork site)
Definition at line 316 of file MHP.cpp.
|
protected |
Handle return.
Handle return instruction in the current thread scope (excluding any join site)
Definition at line 507 of file MHP.cpp.
|
inline |
|
protected |
Whether the function is connected from main function in thread call graph.
Definition at line 759 of file MHP.cpp.
|
inlineprotected |
If lhs is a suffix of rhs, including equal.
Definition at line 278 of file MHP.h.
Whether thread t1 happens before t2 based on ForkJoin Analysis.
Whether two thread t1 happens-fore t2
Whether a join site must join a thread t.
A join site must join t if (1) t is not a multiforked thread (2) the join site of t is not in recursion
Definition at line 719 of file MHP.cpp.
Thread curTid can be fully joined by parentTid recursively.
Whether curTid can be fully joined by parentTid recursively
Definition at line 684 of file MHP.cpp.
Whether it is a fork site.
Definition at line 297 of file MHP.h.
Whether it is a join site.
Definition at line 303 of file MHP.h.
|
inlineprotected |
Match context.
Definition at line 273 of file MHP.h.
Interface to query whether two instructions may happen-in-parallel.
Definition at line 854 of file MHP.cpp.
Definition at line 832 of file MHP.cpp.
Answer MHP queries For a pair of ThreadStmts (t1,s1) = <l1> (t2,s2) = <l2> They may happen in parallel if (1) t1 == t2 and t1 inloop/incycle (2) t1!=t2 and t1 \in l2 and t2 \in l1
TODO: Any instruction in dead function is assumed no MHP with others.
Definition at line 794 of file MHP.cpp.
|
inlineprotected |
| void MHP::printInterleaving | ( | ) |
Print interleaving results.
Print interleaving results
|
inlineprotected |
Context helper functions.
Push calling context
handle calling context for candidate functions only
Definition at line 265 of file MHP.h.
|
inlineprotected |
WorkList helper functions.
|
inlineprotected |
Update Ancestor and sibling threads.
Update interleavings of ancestor threads according to TCT
Definition at line 610 of file MHP.cpp.
Update non-candidate functions' interleaving. Copy interleaving threads of the entry inst to other insts.
Update non-candidate functions' interleaving
Definition at line 275 of file MHP.cpp.
Update interleavings of sibling threads according to TCT
Exclude sibling thread that never happen in parallel based on ForkJoinAnalysis
The interleaving of a thread t is not unnecessary to be updated if (1) t HB Sibling and t fully joins curTid recursively or (2) Sibling HB t
Definition at line 654 of file MHP.cpp.
|
protected |
|
protected |
CxtThreadStmt worklist.
|
protected |
|
protected |
|
protected |
|
protected |
| u32_t SVF::MHP::numOfMHPQueries |
|
protected |
|
protected |
|
protected |
|
protected |