SVF::MTASVFGBuilder Class Reference

#include <MTASVFGBuilder.h>

Inheritance diagram for SVF::MTASVFGBuilder:

Public Types
typedef Set< const StmtSVFGNode * >	SVFGNodeSet
typedef NodeBS	SVFGNodeIDSet
typedef std::pair< const StmtSVFGNode *, const StmtSVFGNode * >	ThreadVFEdge
Public Types inherited from SVF::SVFGBuilder
typedef PointerAnalysis::CallSiteSet	CallSiteSet
typedef PointerAnalysis::CallEdgeMap	CallEdgeMap
typedef PointerAnalysis::FunctionSet	FunctionSet
typedef SVFG::SVFGEdgeSetTy	SVFGEdgeSet

Public Member Functions
	MTASVFGBuilder (MHP *m, LockAnalysis *la)
	Constructor: driven by the interleaving (MHP) and lock analyses.
	~MTASVFGBuilder () override=default
void	configureForMainSolve (const SlicedICFGView *slice)
const std::map< ThreadVFEdge, std::set< const ICFGNode * > > &	getThreadVFQueryMap () const
Public Member Functions inherited from SVF::SVFGBuilder
	SVFGBuilder (bool _SVFGWithIndCall=Options::SVFGWithIndirectCall(), bool _SVFGWithPostOpts=Options::OPTSVFG())
	Constructor.
virtual	~SVFGBuilder ()=default
	Destructor.
SVFG *	buildPTROnlySVFG (BVDataPTAImpl *pta)
SVFG *	buildFullSVFG (BVDataPTAImpl *pta)
SVFG *	getSVFG () const
	Get SVFG instance.
void	markValidVFEdge (SVFGEdgeSet &edges)
	Mark feasible VF edge by removing it from set vfEdgesAtIndCallSite.
bool	isSpuriousVFEdgeAtIndCallSite (const SVFGEdge *edge)
	Return true if this is an VF Edge pre-connected by Andersen's analysis.
virtual std::unique_ptr< MemSSA >	buildMSSA (BVDataPTAImpl *pta, bool ptrOnlyMSSA)
	Build Memory SSA.

Static Public Attributes
static u32_t	numOfNewSVFGEdges = 0
	Number of thread-aware (interference) SVFG edges added.

Protected Member Functions
void	buildSVFG () override
	Rewrite the SVFG build hook: build the stock SVFG, then add MHP edges.
std::unique_ptr< MRGenerator >	createMRGenerator (BVDataPTAImpl *pta, bool ptrOnlyMSSA) override
Protected Member Functions inherited from SVF::SVFGBuilder
SVFG *	build (BVDataPTAImpl *pta, VFG::VFGK kind)
	Create a DDA SVFG. By default actualOut and FormalIN are removed, unless withAOFI is set true.
virtual void	releaseMemory ()
	Release global SVFG.

Private Member Functions
void	collectLoadStoreSVFGNodes ()
void	connectThreadJoinEdges ()
void	addJoinRetEdge (const FormalOUTSVFGNode *formalOut, const ActualOUTSVFGNode *actualOut, CallSiteID csId)
void	connectMHPEdges (PointerAnalysis *pta)
	Connect inter-thread (interference) value-flow edges for MHP pairs.
void	handleStoreLoad (const StmtSVFGNode *n1, const StmtSVFGNode *n2, PointerAnalysis *pta)
void	handleStoreStore (const StmtSVFGNode *n1, const StmtSVFGNode *n2, PointerAnalysis *pta)
void	recordThreadVFSource (const StmtSVFGNode *s, const StmtSVFGNode *sp, bool commonLock)
SVFGEdge *	addTDEdge (NodeID srcId, NodeID dstId, const PointsTo &pts)
	Add a thread-MHP indirect value-flow edge srcId -> dstId carrying pts.
SVFGNodeIDSet	getPrevNodes (const StmtSVFGNode *n)
	Lock-span head/tail tests (non-interference lock-pair pruning).
SVFGNodeIDSet	getSuccNodes (const StmtSVFGNode *n)
bool	isHeadOfSpan (const StmtSVFGNode *n)
bool	isTailOfSpan (const StmtSVFGNode *n)

Private Attributes
const SlicedICFGView *	icfgSlice = nullptr
	Main-solve configuration (see configureForMainSolve); defaults suit VFG_pre.
bool	recordThreadVF = true
	false = skip [THREAD-VF] recording
SVFGNodeSet	stnodeSet
	all store SVFG nodes
SVFGNodeSet	ldnodeSet
	all load SVFG nodes
std::map< ThreadVFEdge, std::set< const ICFGNode * > >	threadVFQueryMap
	[THREAD-VF] per-edge query map (see getThreadVFQueryMap).
MHP *	mhp
LockAnalysis *	lockana
Map< const StmtSVFGNode *, SVFGNodeIDSet >	prevset
Map< const StmtSVFGNode *, SVFGNodeIDSet >	succset
Map< const StmtSVFGNode *, bool >	headmap
Map< const StmtSVFGNode *, bool >	tailmap

Additional Inherited Members
Protected Attributes inherited from SVF::SVFGBuilder
SVFGEdgeSet	vfEdgesAtIndCallSite
	SVFG Edges connected at indirect call/ret sites.
std::unique_ptr< SVFG >	svfg
bool	SVFGWithIndCall
	SVFG with precomputed indirect call edges.
bool	SVFGWithPostOpts
	Build optimised version of SVFG.

Detailed Description

Definition at line 56 of file MTASVFGBuilder.h.

Member Typedef Documentation

SVFGNodeIDSet

typedef NodeBS SVF::MTASVFGBuilder::SVFGNodeIDSet

Definition at line 60 of file MTASVFGBuilder.h.

SVFGNodeSet

typedef Set<const StmtSVFGNode*> SVF::MTASVFGBuilder::SVFGNodeSet

Definition at line 59 of file MTASVFGBuilder.h.

ThreadVFEdge

typedef std::pair<const StmtSVFGNode*, const StmtSVFGNode*> SVF::MTASVFGBuilder::ThreadVFEdge

A candidate thread-aware value-flow edge s –o--> s' (src store, dst load/store), keyed by its endpoint SVFG nodes.

Definition at line 84 of file MTASVFGBuilder.h.

Constructor & Destructor Documentation

MTASVFGBuilder()

SVF::MTASVFGBuilder::MTASVFGBuilder ( MHP *  m, LockAnalysis *  la  )

inline

Constructor: driven by the interleaving (MHP) and lock analyses.

Definition at line 63 of file MTASVFGBuilder.h.

: SVFGBuilder(), mhp(m), lockana(la) {}

~MTASVFGBuilder()

SVF::MTASVFGBuilder::~MTASVFGBuilder ( )

overridedefault

Member Function Documentation

addJoinRetEdge()

void MTASVFGBuilder::addJoinRetEdge ( const FormalOUTSVFGNode *  formalOut, const ActualOUTSVFGNode *  actualOut, CallSiteID  csId  )

private

Add a FormalOUT -> ActualOUT inter-procedural indirect ret edge for a join, mirroring SVFG::addInterIndirectVFRetEdge using the public SVFG API (points-to intersection + dedup via hasInterVFGEdge + addSVFGEdge).

Mirror of SVFG::addInterIndirectVFRetEdge over the public SVFG API, so the join edges can be added from the builder without modifying core SVFG.

Definition at line 137 of file MTASVFGBuilder.cpp.

{
    NodeBS cpts = formalOut->getPointsTo();
    const NodeBS& dpts = actualOut->getPointsTo();
    if (!cpts.intersects(dpts))
        return;
    cpts &= dpts;
 
    SVFGNode* src = svfg->getSVFGNode(formalOut->getId());
    SVFGNode* dst = svfg->getSVFGNode(actualOut->getId());
    if (SVFGEdge* edge = svfg->hasInterVFGEdge(src, dst, SVFGEdge::RetIndVF, csId))
    {
        SVFUtil::cast<RetIndSVFGEdge>(edge)->addPointsTo(cpts);
    }
    else
    {
        RetIndSVFGEdge* retEdge = new RetIndSVFGEdge(src, dst, csId);
        retEdge->addPointsTo(cpts);
        svfg->addSVFGEdge(retEdge);
    }
}

addTDEdge()

SVFGEdge * MTASVFGBuilder::addTDEdge ( NodeID  srcId, NodeID  dstId, const PointsTo &  pts  )

private

Add a thread-MHP indirect value-flow edge srcId -> dstId carrying pts.

Add (or merge into) a thread-MHP indirect value-flow edge src -> dst.

Definition at line 226 of file MTASVFGBuilder.cpp.

{
    SVFGNode* srcNode = svfg->getSVFGNode(srcId);
    SVFGNode* dstNode = svfg->getSVFGNode(dstId);
 
    if (SVFGEdge* edge = svfg->hasThreadVFGEdge(srcNode, dstNode, SVFGEdge::TheadMHPIndirectVF))
    {
        assert(SVFUtil::isa<IndirectSVFGEdge>(edge) && "should be an indirect value-flow edge!");
        return (SVFUtil::cast<IndirectSVFGEdge>(edge)->addPointsTo(pts.toNodeBS()) ? edge : nullptr);
    }
    else
    {
        numOfNewSVFGEdges++;
        ThreadMHPIndSVFGEdge* indirectEdge = new ThreadMHPIndSVFGEdge(srcNode, dstNode);
        indirectEdge->addPointsTo(pts.toNodeBS());
        return (svfg->addSVFGEdge(indirectEdge) ? indirectEdge : nullptr);
    }
}

buildSVFG()

void MTASVFGBuilder::buildSVFG ( )

overrideprotectedvirtual

Rewrite the SVFG build hook: build the stock SVFG, then add MHP edges.

Build the stock (thread-oblivious) SVFG, add the FSAM join-related def-use edges (relocated out of core SVFG.cpp), then add thread-aware MHP edges.

Reimplemented from SVF::SVFGBuilder.

Definition at line 126 of file MTASVFGBuilder.cpp.

{
    svfg->buildSVFG();
    connectThreadJoinEdges();
    connectMHPEdges(svfg->getMSSA()->getPTA());
}

collectLoadStoreSVFGNodes()

void MTASVFGBuilder::collectLoadStoreSVFGNodes ( )

private

Collect the store/load SVFG nodes to pair for interference edges (all of them, or – when a slice is set – only the kept ones).

Collect all store/load SVFG nodes.

Definition at line 200 of file MTASVFGBuilder.cpp.

{
    for (SVFG::const_iterator it = svfg->begin(), eit = svfg->end(); it != eit; ++it)
    {
        const SVFGNode* snode = it->second;
        const bool isLoad = SVFUtil::isa<LoadSVFGNode>(snode);
        if (!isLoad && !SVFUtil::isa<StoreSVFGNode>(snode))
            continue;
        const StmtSVFGNode* node = SVFUtil::cast<StmtSVFGNode>(snode);
        const ICFGNode* icfg = node->getICFGNode();
        if (icfg == nullptr)
            continue;
        // Main-solve slice restriction: an interference edge touching a sliced-out
        // node is inert in the gated FSAM solve, so skip building it here.
        if (icfgSlice != nullptr && !icfgSlice->isKeptNode(icfg))
            continue;
        if (isLoad)
            ldnodeSet.insert(node);
        else
            stnodeSet.insert(node);
    }
}

configureForMainSolve()

void SVF::MTASVFGBuilder::configureForMainSolve ( const SlicedICFGView *  slice )

inline

Configure the builder for the main (post-slicing) FSAM solve rather than the pre-analysis VFG_pre:

• slice != null restricts the interference-edge construction to kept store/load nodes (a sliced-out endpoint's edge is inert in the gated solve, so it need not be built);
• the [THREAD-VF] query map is skipped, as only VFG_pre slicing reads it. The pre-analysis build leaves this unset (whole program, query map built).

Definition at line 76 of file MTASVFGBuilder.h.

    {
        icfgSlice = slice;
        recordThreadVF = false;
    }

connectMHPEdges()

void MTASVFGBuilder::connectMHPEdges ( PointerAnalysis *  pta )

private

Connect inter-thread (interference) value-flow edges for MHP pairs.

For every MHP store/load and store/store pair, add the thread-aware (interference) value-flow edges.

Definition at line 490 of file MTASVFGBuilder.cpp.

{
    collectLoadStoreSVFGNodes();
 
    // Inverted access index (object -> access-node bitset): unioning the
    // bitsets per store visits each may-alias pair exactly once, no dedup tables.
    Map<NodeID, SVFGNodeIDSet> objToStoreIds;
    Map<NodeID, SVFGNodeIDSet> objToLoadIds;
    for (const StmtSVFGNode* store : stnodeSet)
        for (NodeID obj : pta->getPts(store->getDstNodeID()))
            objToStoreIds[obj].set(store->getId());
    for (const StmtSVFGNode* load : ldnodeSet)
        for (NodeID obj : pta->getPts(load->getSrcNodeID()))
            objToLoadIds[obj].set(load->getId());
 
    for (const StmtSVFGNode* store : stnodeSet)
    {
        SVFGNodeIDSet candLoads, candStores;
        for (NodeID obj : pta->getPts(store->getDstNodeID()))
        {
            candStores |= objToStoreIds[obj];
            Map<NodeID, SVFGNodeIDSet>::const_iterator lIt = objToLoadIds.find(obj);
            if (lIt != objToLoadIds.end())
                candLoads |= lIt->second;
        }
 
        for (NodeID loadId : candLoads)
            handleStoreLoad(store, SVFUtil::cast<StmtSVFGNode>(svfg->getSVFGNode(loadId)), pta);
 
        // Visit each unordered store pair once: only partners with a larger id.
        const NodeID storeId = store->getId();
        for (NodeID otherId : candStores)
        {
            if (otherId <= storeId)
                continue;
            handleStoreStore(store, SVFUtil::cast<StmtSVFGNode>(svfg->getSVFGNode(otherId)), pta);
        }
    }
}

connectThreadJoinEdges()

void MTASVFGBuilder::connectThreadJoinEdges ( )

private

FSAM join-related thread-oblivious value flow (the "return" half of treating a join as a call without a forward): connect each start routine's exit defs (FormalOUT) to the ActualOUT at every site that joins it (FormalOUT -> ActualOUT ret edge). Done here as a post-pass over the stock SVFG, so core SVFG.cpp stays unmodified.

FSAM join-related def-use (the "return" half of treating a join as a call without a forward): for every FormalOUT (a start routine's exit def), connect it to the ActualOUT at each site that joins that routine. Relocated here from core SVFG::connectIndirectSVFGEdges so the stock SVFG stays unmodified.

Definition at line 166 of file MTASVFGBuilder.cpp.

{
    ThreadCallGraph* tcg =
        SVFUtil::dyn_cast<ThreadCallGraph>(svfg->getMSSA()->getPTA()->getCallGraph());
    if (tcg == nullptr)
        return;
 
    MemSSA* mssa = svfg->getMSSA();
    for (SVFG::const_iterator it = svfg->begin(), eit = svfg->end(); it != eit; ++it)
    {
        const FormalOUTSVFGNode* formalOut = SVFUtil::dyn_cast<FormalOUTSVFGNode>(it->second);
        if (formalOut == nullptr)
            continue;
 
        ThreadCallGraph::InstSet joinsites;
        tcg->getJoinSites(tcg->getCallGraphNode(formalOut->getFun()), joinsites);
        for (const CallICFGNode* cs : joinsites)
        {
            if (!mssa->hasCHI(cs))
                continue;
            SVFG::ActualOUTSVFGNodeSet& actualOuts = svfg->getActualOUTSVFGNodes(cs);
            for (NodeID aoId : actualOuts)
            {
                const ActualOUTSVFGNode* actualOut =
                    SVFUtil::cast<ActualOUTSVFGNode>(svfg->getSVFGNode(aoId));
                addJoinRetEdge(formalOut, actualOut, svfg->getCallSiteID(cs, formalOut->getFun()));
            }
        }
    }
}

createMRGenerator()

std::unique_ptr< MRGenerator > MTASVFGBuilder::createMRGenerator ( BVDataPTAImpl *  pta, bool  ptrOnlyMSSA  )

overrideprotectedvirtual

Inject a thread-aware MRGenerator so the MemSSA mod-ref carries the FSAM fork/join side effects (relocated here from core MemRegion).

Reimplemented from SVF::SVFGBuilder.

Definition at line 106 of file MTASVFGBuilder.cpp.

{
    switch (Options::MemPar())
    {
    case MemSSA::MemPartition::Distinct:
        return std::make_unique<ThreadMRG<DistinctMRG>>(pta, ptrOnlyMSSA);
    case MemSSA::MemPartition::IntraDisjoint:
        return std::make_unique<ThreadMRG<IntraDisjointMRG>>(pta, ptrOnlyMSSA);
    case MemSSA::MemPartition::InterDisjoint:
        return std::make_unique<ThreadMRG<InterDisjointMRG>>(pta, ptrOnlyMSSA);
    default:
        assert(false && "unrecognised memory partition strategy");
        return nullptr;
    }
}

getPrevNodes()

MTASVFGBuilder::SVFGNodeIDSet MTASVFGBuilder::getPrevNodes ( const StmtSVFGNode *  n )

private

Lock-span head/tail tests (non-interference lock-pair pruning).

Backward reachable store SVFG nodes via indirect value flow (lock-span head test).

Definition at line 248 of file MTASVFGBuilder.cpp.

{
    if (prevset.find(n) != prevset.end())
        return prevset[n];
 
    SVFGNodeIDSet prev;
    Set<const SVFGNode*> worklist;
    Set<const SVFGNode*> visited;
 
    for (SVFGEdge::SVFGEdgeSetTy::iterator iter = n->InEdgeBegin(); iter != n->InEdgeEnd(); ++iter)
    {
        SVFGEdge* edge = *iter;
        if (edge->isIndirectVFGEdge())
            worklist.insert(edge->getSrcNode());
    }
 
    while (!worklist.empty())
    {
        const SVFGNode* node = *worklist.begin();
        worklist.erase(worklist.begin());
        visited.insert(node);
        if (SVFUtil::isa<StoreSVFGNode>(node))
            prev.set(node->getId());
        else
        {
            for (SVFGEdge::SVFGEdgeSetTy::iterator iter = node->InEdgeBegin(); iter != node->InEdgeEnd(); ++iter)
            {
                SVFGEdge* edge = *iter;
                if (edge->isIndirectVFGEdge() && visited.find(edge->getSrcNode()) == visited.end())
                    worklist.insert(edge->getSrcNode());
            }
        }
    }
    prevset[n] = prev;
    return prev;
}

getSuccNodes()

MTASVFGBuilder::SVFGNodeIDSet MTASVFGBuilder::getSuccNodes ( const StmtSVFGNode *  n )

private

Forward reachable store/load SVFG nodes via indirect value flow (lock-span tail test).

Definition at line 288 of file MTASVFGBuilder.cpp.

{
    if (succset.find(n) != succset.end())
        return succset[n];
 
    SVFGNodeIDSet succ;
    Set<const SVFGNode*> worklist;
    Set<const SVFGNode*> visited;
 
    for (SVFGEdge::SVFGEdgeSetTy::iterator iter = n->OutEdgeBegin(); iter != n->OutEdgeEnd(); ++iter)
    {
        SVFGEdge* edge = *iter;
        if (edge->isIndirectVFGEdge())
            worklist.insert(edge->getDstNode());
    }
 
    while (!worklist.empty())
    {
        const SVFGNode* node = *worklist.begin();
        worklist.erase(worklist.begin());
        visited.insert(node);
        if (SVFUtil::isa<StoreSVFGNode, LoadSVFGNode>(node))
            succ.set(node->getId());
        else
        {
            for (SVFGEdge::SVFGEdgeSetTy::iterator iter = node->OutEdgeBegin(); iter != node->OutEdgeEnd(); ++iter)
            {
                SVFGEdge* edge = *iter;
                if (edge->isIndirectVFGEdge() && visited.find(edge->getDstNode()) == visited.end())
                    worklist.insert(edge->getDstNode());
            }
        }
    }
    succset[n] = succ;
    return succ;
}

getThreadVFQueryMap()

const std::map< ThreadVFEdge, std::set< const ICFGNode * > > & SVF::MTASVFGBuilder::getThreadVFQueryMap ( ) const

inline

[THREAD-VF] per-edge query map (MSli §4.2, Fig. 6 rule [THREAD-VF]).

While building VFG_pre we record, for every candidate thread-aware value-flow edge (s,s') the construction evaluates, its Query(s –o--> s') set: the endpoints {s,s'} plus — under a common lock — the in-span witnesses Succ_spl(s) / Pred_spl'(s') that decide TL/HD membership, i.e. whether the edge survives the non-interference test (Def. 2). The query is kept per edge (not pre-unioned) so ILA slicing can restrict the sources to the edges that survive the FSPTA slice — ThreadVF(VFG'_pre) — rather than every candidate pair. Feeding the retained edges' queries into ILA slicing makes the sliced MHP/lock reproduce the same value-flow decisions the main phase makes, while keeping the slice minimal.

The value stores only the additional lock-span witnesses; the endpoint ICFG nodes are implicit in the key and consumers must add them back.

Definition at line 101 of file MTASVFGBuilder.h.

    {
        return threadVFQueryMap;
    }

handleStoreLoad()

void MTASVFGBuilder::handleStoreLoad ( const StmtSVFGNode *  n1, const StmtSVFGNode *  n2, PointerAnalysis *  pta  )

private

Store -> Load interference: add a thread-aware def-use edge if the store may happen in parallel with and may alias the load, unless excluded by a common lock (then only when the store is a span tail and the load a span head).

Definition at line 415 of file MTASVFGBuilder.cpp.

{
    const ICFGNode* i1 = n1->getICFGNode();
    const ICFGNode* i2 = n2->getICFGNode();
 
    if (!mhp->mayHappenInParallel(i1, i2))
        return;
 
    // No alias() re-check: the bucketed candidate generator only pairs accesses
    // whose raw points-to sets share an object, so the intersection below is
    // non-empty by construction and alias() could never answer NoAlias here.
    PointsTo pts = pta->getPts(n1->getDstNodeID());
    pts &= pta->getPts(n2->getSrcNodeID());
 
    // [THREAD-VF] source extraction runs for every candidate pair (both the
    // pairs that survive and the ones the lock test prunes), so the sliced ILA
    // can re-derive whether the edge holds.
    bool commonLock = lockana->isProtectedByCommonLock(i1, i2);
    if (recordThreadVF)
        recordThreadVFSource(n1, n2, commonLock);
 
    if (commonLock)
    {
        if (isTailOfSpan(n1) && isHeadOfSpan(n2))
            addTDEdge(n1->getId(), n2->getId(), pts);
    }
    else
    {
        addTDEdge(n1->getId(), n2->getId(), pts);
    }
}

handleStoreStore()

void MTASVFGBuilder::handleStoreStore ( const StmtSVFGNode *  n1, const StmtSVFGNode *  n2, PointerAnalysis *  pta  )

private

Store -> Store interference (symmetric): add thread-aware def-use edges in both directions, with the same lock-span pruning as store/load.

Definition at line 451 of file MTASVFGBuilder.cpp.

{
    const ICFGNode* i1 = n1->getICFGNode();
    const ICFGNode* i2 = n2->getICFGNode();
 
    if (!mhp->mayHappenInParallel(i1, i2))
        return;
 
    // No alias() re-check: see handleStoreLoad -- bucketing already guarantees a
    // shared raw object.
    PointsTo pts = pta->getPts(n1->getDstNodeID());
    pts &= pta->getPts(n2->getDstNodeID());
 
    // Both directions are candidate thread-aware edges; extract sources for each.
    bool commonLock = lockana->isProtectedByCommonLock(i1, i2);
    if (recordThreadVF)
    {
        recordThreadVFSource(n1, n2, commonLock);
        recordThreadVFSource(n2, n1, commonLock);
    }
 
    if (commonLock)
    {
        if (isTailOfSpan(n1) && isHeadOfSpan(n2))
            addTDEdge(n1->getId(), n2->getId(), pts);
        if (isTailOfSpan(n2) && isHeadOfSpan(n1))
            addTDEdge(n2->getId(), n1->getId(), pts);
    }
    else
    {
        addTDEdge(n1->getId(), n2->getId(), pts);
        addTDEdge(n2->getId(), n1->getId(), pts);
    }
}

isHeadOfSpan()

bool MTASVFGBuilder::isHeadOfSpan ( const StmtSVFGNode *  n )

private

Whether, for all lock spans n belongs to, n is the first write (span head).

Definition at line 328 of file MTASVFGBuilder.cpp.

{
    if (headmap.find(n) != headmap.end())
        return headmap[n];
 
    SVFGNodeIDSet prev = getPrevNodes(n);
    for (NodeID id : prev)
    {
        const StmtSVFGNode* prevNode = SVFUtil::dyn_cast<StmtSVFGNode>(svfg->getSVFGNode(id));
        if (prevNode && lockana->isInSameSpan(prevNode->getICFGNode(), n->getICFGNode()))
        {
            headmap[n] = false;
            return false;
        }
    }
    headmap[n] = true;
    return true;
}

isTailOfSpan()

bool MTASVFGBuilder::isTailOfSpan ( const StmtSVFGNode *  n )

private

Whether, for all lock spans n belongs to, n is the last write (span tail).

Definition at line 350 of file MTASVFGBuilder.cpp.

{
    assert(SVFUtil::isa<StoreSVFGNode>(n) && "tail test only for store nodes");
 
    if (tailmap.find(n) != tailmap.end())
        return tailmap[n];
 
    SVFGNodeIDSet succ = getSuccNodes(n);
    for (NodeID id : succ)
    {
        const SVFGNode* sn = svfg->getSVFGNode(id);
        if (SVFUtil::isa<LoadSVFGNode>(sn))
            continue;
        const StmtSVFGNode* succNode = SVFUtil::dyn_cast<StmtSVFGNode>(sn);
        if (succNode && lockana->isInSameSpan(succNode->getICFGNode(), n->getICFGNode()))
        {
            tailmap[n] = false;
            return false;
        }
    }
    tailmap[n] = true;
    return true;
}

recordThreadVFSource()

void MTASVFGBuilder::recordThreadVFSource ( const StmtSVFGNode *  s, const StmtSVFGNode *  sp, bool  commonLock  )

private

Record the [THREAD-VF] slicing sources for one candidate pair s –o--> s' (s = src store, sp = dst load/store). Adds the endpoints, and — when the pair is protected by a common lock — the in-span successor/predecessor witnesses needed to re-decide the non-interference (tail/head) test.

Record the per-edge [THREAD-VF] query for one candidate pair s –o--> sp (see getThreadVFQueryMap for the rule): the endpoints, plus – under a common lock – the in-span Succ_spl(s) / Pred_spl'(sp) witnesses. Enumerated fully (the tail/head boolean tests short-circuit; source extraction must not).

Definition at line 380 of file MTASVFGBuilder.cpp.

{
    // Per-edge Query set. The endpoints are NOT duplicated into the value --
    // they are recoverable from the map key -- so the value holds only the
    // additional in-span witnesses below (empty for the common lock-free case).
    std::set<const ICFGNode*>& query = threadVFQueryMap[ {s, sp}];
 
    if (!commonLock)
        return;
 
    // Succ_spl(s) = { x in s's span | x is a store, s --o--> x } (tail witnesses).
    for (NodeID id : getSuccNodes(s))
    {
        const SVFGNode* sn = svfg->getSVFGNode(id);
        if (!SVFUtil::isa<StoreSVFGNode>(sn))
            continue;
        const StmtSVFGNode* succNode = SVFUtil::cast<StmtSVFGNode>(sn);
        if (lockana->isInSameSpan(succNode->getICFGNode(), s->getICFGNode()))
            query.insert(succNode->getICFGNode());
    }
 
    // Pred_spl'(sp) = { x in sp's span | x --o--> sp } (head witnesses).
    for (NodeID id : getPrevNodes(sp))
    {
        const StmtSVFGNode* prevNode = SVFUtil::dyn_cast<StmtSVFGNode>(svfg->getSVFGNode(id));
        if (prevNode && lockana->isInSameSpan(prevNode->getICFGNode(), sp->getICFGNode()))
            query.insert(prevNode->getICFGNode());
    }
}

Member Data Documentation

headmap

Map<const StmtSVFGNode*, bool> SVF::MTASVFGBuilder::headmap

private

Definition at line 170 of file MTASVFGBuilder.h.

icfgSlice

const SlicedICFGView* SVF::MTASVFGBuilder::icfgSlice = nullptr

private

Main-solve configuration (see configureForMainSolve); defaults suit VFG_pre.

null = whole program

Definition at line 116 of file MTASVFGBuilder.h.

ldnodeSet

SVFGNodeSet SVF::MTASVFGBuilder::ldnodeSet

private

all load SVFG nodes

Definition at line 160 of file MTASVFGBuilder.h.

lockana

LockAnalysis* SVF::MTASVFGBuilder::lockana

private

Definition at line 166 of file MTASVFGBuilder.h.

mhp

MHP* SVF::MTASVFGBuilder::mhp

private

Definition at line 165 of file MTASVFGBuilder.h.

numOfNewSVFGEdges

u32_t MTASVFGBuilder::numOfNewSVFGEdges = 0

static

Number of thread-aware (interference) SVFG edges added.

Definition at line 67 of file MTASVFGBuilder.h.

prevset

Map<const StmtSVFGNode*, SVFGNodeIDSet> SVF::MTASVFGBuilder::prevset

private

Definition at line 168 of file MTASVFGBuilder.h.

recordThreadVF

bool SVF::MTASVFGBuilder::recordThreadVF = true

private

false = skip [THREAD-VF] recording

Definition at line 117 of file MTASVFGBuilder.h.

stnodeSet

SVFGNodeSet SVF::MTASVFGBuilder::stnodeSet

private

all store SVFG nodes

Definition at line 159 of file MTASVFGBuilder.h.

succset

Map<const StmtSVFGNode*, SVFGNodeIDSet> SVF::MTASVFGBuilder::succset

private

Definition at line 169 of file MTASVFGBuilder.h.

tailmap

Map<const StmtSVFGNode*, bool> SVF::MTASVFGBuilder::tailmap

private

Definition at line 171 of file MTASVFGBuilder.h.

threadVFQueryMap

std::map<ThreadVFEdge, std::set<const ICFGNode*> > SVF::MTASVFGBuilder::threadVFQueryMap

private

[THREAD-VF] per-edge query map (see getThreadVFQueryMap).

Definition at line 163 of file MTASVFGBuilder.h.

---

The documentation for this class was generated from the following files:

• /home/runner/work/SVF/SVF/svf/include/MTA/MTASVFGBuilder.h
• /home/runner/work/SVF/SVF/svf/lib/MTA/MTASVFGBuilder.cpp