#include <MTASlicer.h>

Inheritance diagram for SVF::MultiStageSlicer:

Public Member Functions
	MultiStageSlicer (SVFIR svfir, AndersenBase pta, MHP mhp, LockAnalysis lockAnalysis, SVFG *svfg=nullptr)
OrderedSet< const ICFGNode * >	runILASlicing (const OrderedSet< const SVFStmt * > &vulnerableStatements, const OrderedSet< const ICFGNode * > &threadVFSources={})
ValueFlowSlice	runPTASlicing (const OrderedSet< const SVFStmt * > &vulnerableStatements, SVFG *refinedMainVFG)
void	computePreCandidateSlice (const OrderedSet< const SVFStmt * > &vulnerableStatements)
const ValueFlowSlice &	getPreCandidateSlice () const
	Return the pre-candidate slice after computePreCandidateSlice().
Public Member Functions inherited from SVF::MTASlicerBase
	MTASlicerBase (SVFIR svfir, AndersenBase pta, MHP mhp, LockAnalysis lockAnalysis, SVFG *svfg=nullptr)

Private Attributes
ValueFlowSlice	preCandidateSlice
bool	preCandidateComputed = false

Additional Inherited Members
Protected Member Functions inherited from SVF::MTASlicerBase
OrderedSet< const VFGNode * >	computeDataDependenceSVFGNodes (const OrderedSet< const SVFStmt * > &seeds, SVFG *svfg)
OrderedSet< const ICFGNode * >	svfgNodesToICFGNodes (const OrderedSet< const VFGNode * > &nodes, const OrderedSet< const SVFStmt * > &seeds)
	Project the retained VFG nodes (plus the seeds) onto their ICFG nodes.
OrderedSet< const CallICFGNode * >	getDependentThreadCreate (const ICFGNode *node)
OrderedSet< const TCTNode * >	getTCTNodeSetFromNode (const ICFGNode *node)
OrderedSet< const ICFGNode * >	getLockSet (const ICFGNode *node)
OrderedSet< const CallICFGNode * >	collectPthreadStatements (const OrderedSet< const ICFGNode * > &sourceNodes)
OrderedSet< const CallICFGNode * >	collectMutexStatements (const OrderedSet< const ICFGNode * > &sourceNodes)
std::pair< OrderedSet< const CallICFGNode * >, OrderedSet< const CallICFGNode * > >	collectCommonThreadStatements (const OrderedSet< const ICFGNode * > &sourceNodes)
void	addSynchronizationDependencies (const OrderedSet< const CallICFGNode * > &pthreadCallNodes, const OrderedSet< const CallICFGNode * > &mutexCallNodes, OrderedSet< const ICFGNode * > &retainedNodes)
OrderedSet< const ICFGNode * >	expandCallDependence (const OrderedSet< const ICFGNode * > &nodes)
Static Protected Member Functions inherited from SVF::MTASlicerBase
static void	enqueueSVFGNode (const SVFGNode node, OrderedSet< const SVFGNode > &visited, std::deque< const SVFGNode * > &worklist)
Protected Attributes inherited from SVF::MTASlicerBase
SVFIR *	svfir
AndersenBase *	pta
MHP *	mhp
LockAnalysis *	lockAnalysis
CallGraph *	callGraph
SVFG *	svfg
	thread-aware VFG_pre (PTA/Single slicers; null for MTA)

Detailed Description

MultiStageSlicer - the multi-stage (differential) slicer of MSli. The pre-candidate closure scopes ILA queries and the Main-TVF overlay; the final closure is recomputed over that refined main graph. Stage 1 (ILA): runILASlicing – synchronization slicing + function expansion, feeding the sliced MHP/lock. Stage 2 (FSPTA): runPTASlicing – backward data-dependence slice feeding the sliced flow-sensitive solve. Contrast: SingleSlicer below folds everything into ONE unified slice.

Definition at line 201 of file MTASlicer.h.

Constructor & Destructor Documentation

◆ MultiStageSlicer()

SVF::MultiStageSlicer::MultiStageSlicer	(	SVFIR *	svfir,
		AndersenBase *	pta,
		MHP *	mhp,
		LockAnalysis *	lockAnalysis,
		SVFG *	svfg = nullptr )

Definition at line 793 of file MTASlicer.cpp.

    : MTASlicerBase(svfir, pta, mhp, lockAnalysis, svfg)
{
}

Member Function Documentation

◆ computePreCandidateSlice()

void SVF::MultiStageSlicer::computePreCandidateSlice ( const OrderedSet< const SVFStmt * > & vulnerableStatements )

Compute the pre-candidate slice used to restrict [THREAD-VF] sources and scope construction of the refined main overlay.

Definition at line 858 of file MTASlicer.cpp.

{
    preCandidateSlice = ValueFlowSlice{};
    preCandidateSlice.svfgNodes =
        computeDataDependenceSVFGNodes(vulnerableStatements, svfg);
    preCandidateSlice.icfgNodes =
        svfgNodesToICFGNodes(preCandidateSlice.svfgNodes, vulnerableStatements);
    preCandidateComputed = true;
}

◆ getPreCandidateSlice()

const ValueFlowSlice & SVF::MultiStageSlicer::getPreCandidateSlice ( ) const

Return the pre-candidate slice after computePreCandidateSlice().

Definition at line 869 of file MTASlicer.cpp.

{
    assert(preCandidateComputed && "pre-candidate slice has not been computed");
    return preCandidateSlice;
}

◆ runILASlicing()

OrderedSet< const ICFGNode * > SVF::MultiStageSlicer::runILASlicing	(	const OrderedSet< const SVFStmt * > &	vulnerableStatements,
		const OrderedSet< const ICFGNode * > &	threadVFSources = {} )

Stage 1: the ILA slice (synchronization + function expansion for the IRView).

Parameters

vulnerableStatements	Set of vulnerable statements to start slicing from (the [INIT] rule: pre-analysis race statements).
threadVFSources	Extra ILA slicing sources from the [THREAD-VF] rule (MSli 4.2): statements whose MHP/lock-span results are queried during the main-phase thread-aware value-flow construction (endpoints and in-span non-interference witnesses collected while building VFG_pre).

Returns: Set of ICFG nodes in the slice (including call/ret and entry/exit nodes)

Definition at line 800 of file MTASlicer.cpp.

{
 
    // Step 1: Form the complete ILA source set first. MSli section 4.2 defines
    // V_ILA as [INIT] union [THREAD-VF], then closes every source over its
    // synchronization dependences. Keep this set at ICFG granularity: some
    // THREAD-VF call/marker nodes have no attached SVF statement.
    OrderedSet<const ICFGNode*> ilaSourceNodes = threadVFSources;
    for (const SVFStmt* stmt : vulnerableStatements)
        ilaSourceNodes.insert(stmt->getICFGNode());
 
    // Step 2: synchronization-dependence closure of the complete source set.
    auto commonStmts = collectCommonThreadStatements(ilaSourceNodes);
    const OrderedSet<const CallICFGNode*>& pthreadCallNodes = commonStmts.first;
    const OrderedSet<const CallICFGNode*>& mutexCallNodes = commonStmts.second;
 
    // Form V_ILA_sync before function expansion: all [INIT] and [THREAD-VF]
    // sources plus the synchronization primitives on which they depend.
    OrderedSet<const ICFGNode*> initialSliceResult;
    addSynchronizationDependencies(
        pthreadCallNodes, mutexCallNodes, initialSliceResult);
    for (const SVFStmt* stmt : vulnerableStatements)
    {
        initialSliceResult.insert(stmt->getICFGNode());
    }
    initialSliceResult.insert(threadVFSources.begin(), threadVFSources.end());
 
    // Step 3: Expand keptNodes to include call/ret nodes and function entry/exit
    // nodes (call dependence).
    OrderedSet<const ICFGNode*> finalSlice = expandCallDependence(initialSliceResult);
 
    // Slicing invariant: no relevant synchronization primitive may be contracted
    // into a bridge edge. Return nodes are retained because the sliced ICFG
    // represents external synchronization calls as paired call/return nodes.
    for (const CallICFGNode* callNode : pthreadCallNodes)
    {
        assert(finalSlice.count(callNode) && finalSlice.count(callNode->getRetICFGNode()) &&
               "ILA slice dropped a fork/join synchronization dependence");
        (void)callNode;
    }
    for (const CallICFGNode* callNode : mutexCallNodes)
    {
        assert(finalSlice.count(callNode) && finalSlice.count(callNode->getRetICFGNode()) &&
               "ILA slice dropped a lock/unlock synchronization dependence");
        (void)callNode;
    }
    return finalSlice;
}

◆ runPTASlicing()

ValueFlowSlice SVF::MultiStageSlicer::runPTASlicing	(	const OrderedSet< const SVFStmt * > &	vulnerableStatements,
		SVFG *	refinedMainVFG )

Stage 2: the FSPTA slice (backward data dependence over the refined main value-flow graph; node set only, no function expansion).

Definition at line 876 of file MTASlicer.cpp.

{
    ValueFlowSlice result;
    result.svfgNodes =
        computeDataDependenceSVFGNodes(vulnerableStatements, refinedMainVFG);
    result.icfgNodes =
        svfgNodesToICFGNodes(result.svfgNodes, vulnerableStatements);
    return result;
}

Member Data Documentation

◆ preCandidateComputed

bool SVF::MultiStageSlicer::preCandidateComputed = false

private

Definition at line 239 of file MTASlicer.h.

◆ preCandidateSlice

ValueFlowSlice SVF::MultiStageSlicer::preCandidateSlice