#include <SparseAbstractInterpretation.h>

Inheritance diagram for SVF::FullSparseAbstractInterpretation:

Public Member Functions
	FullSparseAbstractInterpretation ()

	~FullSparseAbstractInterpretation () override

Public Member Functions inherited from SVF::SemiSparseAbstractInterpretation
	SemiSparseAbstractInterpretation ()

	~SemiSparseAbstractInterpretation () override=default

Public Member Functions inherited from SVF::AbstractInterpretation
virtual void	runOnModule ()

virtual	~AbstractInterpretation ()
	Destructor.

void	analyse ()
	Program entry.

void	analyzeFromAllProgEntries ()
	Analyze all entry points (functions without callers)

FIFOWorkList< const FunObjVar * >	collectProgEntryFuns ()
	Get all entry point functions (functions without callers)

void	addDetector (std::unique_ptr< AEDetector > detector)

const SVFVar *	getSVFVar (NodeID varId) const
	Retrieve SVFVar given its ID; asserts if no such variable exists.

AbstractState &	getAbsState (const ICFGNode *node)

bool	hasAbsState (const ICFGNode *node)

void	getAbsState (const Set< const ValVar * > &vars, AbstractState &result, const ICFGNode *node)

void	getAbsState (const Set< const ObjVar * > &vars, AbstractState &result, const ICFGNode *node)

void	getAbsState (const Set< const SVFVar * > &vars, AbstractState &result, const ICFGNode *node)

IntervalValue	getGepElementIndex (const GepStmt *gep)

IntervalValue	getGepByteOffset (const GepStmt *gep)

AddressValue	getGepObjAddrs (const ValVar *pointer, IntervalValue offset)

virtual AbstractValue	loadValue (const ValVar pointer, const ICFGNode node)
	Virtual so full-sparse can layer the GepObj overlay on top.

const SVFType *	getPointeeElement (const ObjVar var, const ICFGNode node)

u32_t	getAllocaInstByteSize (const AddrStmt *addr)

Map< const ICFGNode *, AbstractState > &	getTrace ()

AbstractState &	operator[] (const ICFGNode *node)

Protected Member Functions
void	joinStates (AbstractState &dst, const AbstractState &src) override

void	storeValue (const ValVar pointer, const AbstractValue &val, const ICFGNode node) override

bool	mergeStatesFromPredecessors (const ICFGNode *node) override

void	recordBranchRefinement (NodeID objId, const IntervalValue &narrowed, AbstractState &as, const ICFGNode loadIcfg, const ICFGNode succ) override

Protected Member Functions inherited from SVF::SemiSparseAbstractInterpretation
AbstractState	getFullCycleHeadState (const ICFGCycleWTO *cycle) override

bool	widenCycleState (const AbstractState &prev, const AbstractState &cur, const ICFGCycleWTO *cycle) override

bool	narrowCycleState (const AbstractState &prev, const AbstractState &cur, const ICFGCycleWTO *cycle) override

const AbstractValue &	getAbsValue (const ValVar var, const ICFGNode node) override

bool	hasAbsValue (const ValVar var, const ICFGNode node) const override
	Side-effect-free existence check.

void	updateAbsValue (const ValVar var, const AbstractValue &val, const ICFGNode node) override

void	updateAbsState (const ICFGNode *node, const AbstractState &state) override

void	joinStates (AbstractState &dst, const AbstractState &src) override

const ICFGNode *	getICFGNode (const ValVar *var) const

virtual const AbstractValue &	getAbsValue (const ValVar var, const ICFGNode node)

virtual const AbstractValue &	getAbsValue (const ObjVar var, const ICFGNode node)

virtual const AbstractValue &	getAbsValue (const SVFVar var, const ICFGNode node)

virtual bool	hasAbsValue (const ValVar var, const ICFGNode node) const
	Side-effect-free existence check.

virtual bool	hasAbsValue (const ObjVar var, const ICFGNode node) const

virtual bool	hasAbsValue (const SVFVar var, const ICFGNode node) const

virtual void	updateAbsValue (const ValVar var, const AbstractValue &val, const ICFGNode node)

virtual void	updateAbsValue (const ObjVar var, const AbstractValue &val, const ICFGNode node)

virtual void	updateAbsValue (const SVFVar var, const AbstractValue &val, const ICFGNode node)

Protected Member Functions inherited from SVF::AbstractInterpretation
	AbstractInterpretation ()

bool	isBranchEdgeFeasible (const IntraCFGEdge *edge, AbstractState &as)

void	collectBranchRefinement (const IntraCFGEdge *edge, AbstractState &as)

bool	shouldApplyNarrowing (const FunObjVar *fun)
	Check if narrowing should be applied: always for regular loops, mode-dependent for recursion.

Private Member Functions
void	pullObjValueFlows (const ICFGNode *node)

bool	isIndirectSVFGEdgeFeasible (const IndirectSVFGEdge edge, const VFGNode dst)

bool	isICFGPathFeasible (const ICFGNode src, const ICFGNode dst)

bool	isIntraEdgeBranchFeasible (const IntraCFGEdge edge, const ICFGNode src)
	Return whether this intra edge is allowed by the current branch state.

void	propagateAndApplyRefinement (const ICFGNode *node)

void	buildSVFG ()
	Build the SVFG on top of the semi-sparse precompute.

Private Attributes
Map< const ICFGNode *, Map< NodeID, IntervalValue > >	refinementTrace

std::unique_ptr< SVFGBuilder >	svfgBuilder

SVFG *	svfg {nullptr}
	View pointer into svfgBuilder's graph; non-null after buildSVFG().

Additional Inherited Members
Public Types inherited from SVF::AbstractInterpretation
enum	AESparsity { Dense , SemiSparse , Sparse }

enum	HandleRecur { TOP , WIDEN_ONLY , WIDEN_NARROW }

enum	AEFunEntryMode { MAIN , NO_MAIN }

Static Public Member Functions inherited from SVF::AbstractInterpretation
static AbstractInterpretation &	getAEInstance ()

Protected Attributes inherited from SVF::AbstractInterpretation
SVFIR *	svfir {nullptr}
	Data and helpers reachable from SparseAbstractInterpretation.

AEWTO *	preAnalysis {nullptr}

Map< const ICFGNode *, AbstractState >	abstractTrace
	per-node trace; owned here

Detailed Description

Abstract Interpretation for Options::AESparsity::Sparse (full-sparse).

In full-sparse mode both ValVars and ObjVars live at their SVFG def-sites; reads query the SVFG for the reaching-def site, writes happen at def-sites. See doc/plan-full-sparse.md for the phase plan; Phase 1 routes ValVar and ObjVar reads through the SVFG.

Definition at line 85 of file SparseAbstractInterpretation.h.

Constructor & Destructor Documentation

◆ FullSparseAbstractInterpretation()

SVF::FullSparseAbstractInterpretation::FullSparseAbstractInterpretation ( )

inline

Definition at line 88 of file SparseAbstractInterpretation.h.

    {
        buildSVFG();
    }

◆ ~FullSparseAbstractInterpretation()

FullSparseAbstractInterpretation::~FullSparseAbstractInterpretation ( )

overridedefault

Member Function Documentation

◆ buildSVFG()

void FullSparseAbstractInterpretation::buildSVFG ( )

private

Build the SVFG on top of the semi-sparse precompute.

Definition at line 44 of file SparseAbstractInterpretation.cpp.

{
    svfgBuilder = std::make_unique<SVFGBuilder>(true);
    svfg = svfgBuilder->buildFullSVFG(preAnalysis->getPointerAnalysis());
}

◆ isICFGPathFeasible()

bool FullSparseAbstractInterpretation::isICFGPathFeasible	(	const ICFGNode *	src,
		const ICFGNode *	dst
	)

private

Return whether a branch-feasible ICFG path exists from src to dst. Conditional edges are checked with a pure branch-feasibility query, so path probing does not create branch-refinement side effects.

Definition at line 363 of file SparseAbstractInterpretation.cpp.

{
    bool feasible = true;
    if (!src || !dst)
    {
        feasible = true;
    }
    else if (src == dst)
    {
        feasible = true;
    }
    else
    {
        const FunObjVar* fun = src->getFun();
        if (!fun || fun != dst->getFun())
        {
            feasible = true;
        }
        else
        {
            feasible = false;
            std::deque<const ICFGNode*> worklist;
            Set<const ICFGNode*> visited;
            worklist.push_back(src);
            visited.insert(src);
 
            while (!worklist.empty() && !feasible)
            {
                const ICFGNode* cur = worklist.front();
                worklist.pop_front();
 
                // Treat a call as an intra-procedural summary edge for path
                // queries. Feasibility of the callee body is handled by the
                // normal analysis; here we only need caller-side reachability,
                // e.g. entry -> ret-site.
                if (const CallICFGNode* call =
                            SVFUtil::dyn_cast<CallICFGNode>(cur))
                {
                    const ICFGNode* succ = call->getRetICFGNode();
                    if (!succ || succ->getFun() != fun)
                    {
                        // Ignore missing or cross-function return summaries.
                    }
                    else if (succ == dst)
                    {
                        feasible = true;
                    }
                    else if (!visited.count(succ))
                    {
                        visited.insert(succ);
                        worklist.push_back(succ);
                    }
                    else
                    {
                        // Already visited.
                    }
                }
 
                for (const ICFGEdge* edge : cur->getOutEdges())
                {
                    const IntraCFGEdge* intraEdge =
                        SVFUtil::dyn_cast<IntraCFGEdge>(edge);
                    const ICFGNode* succ =
                        intraEdge ? intraEdge->getDstNode() : nullptr;
 
                    if (!intraEdge)
                    {
                        // Non-intra ICFG edges are not part of this path query.
                    }
                    else if (!succ || succ->getFun() != fun)
                    {
                        // Keep the query inside src's function.
                    }
                    else if (!isIntraEdgeBranchFeasible(intraEdge, cur))
                    {
                        // The conditional edge is unreachable in cur's state.
                    }
                    else if (succ == dst)
                    {
                        feasible = true;
                    }
                    else if (!visited.count(succ))
                    {
                        visited.insert(succ);
                        worklist.push_back(succ);
                    }
                    else
                    {
                        // Already visited.
                    }
                }
            }
        }
    }
 
    return feasible;
}

◆ isIndirectSVFGEdgeFeasible()

bool FullSparseAbstractInterpretation::isIndirectSVFGEdgeFeasible	(	const IndirectSVFGEdge *	edge,
		const VFGNode *	dst
	)

private

Return whether an indirect SVFG edge should be pulled into dst. Besides branch-feasible ICFG reachability, this rejects paths where another store to the same points-to object kills the edge's value.

Definition at line 253 of file SparseAbstractInterpretation.cpp.

{
    assert(edge && "Indirect SVFG edge must exist");
    assert(dst && "Indirect SVFG edge must have a destination node");
 
    const SVFGNode* src = SVFUtil::dyn_cast<SVFGNode>(edge->getSrcNode());
    assert(src && "Indirect SVFG edge must have an SVFG source node");
 
    const ICFGNode* srcICFG = src->getICFGNode();
    const ICFGNode* dstICFG = dst->getICFGNode();
    assert(srcICFG && "SVFG source node must have an ICFG node");
    assert(dstICFG && "SVFG destination node must have an ICFG node");
 
    const FunObjVar* fun = srcICFG->getFun();
    bool feasible = true;
    if (srcICFG == dstICFG)
    {
        feasible = true;
    }
    else if (!fun || fun != dstICFG->getFun())
    {
        feasible = true;
    }
    else
    {
        feasible = false;
        std::deque<const ICFGNode*> worklist;
        Set<const ICFGNode*> visited;
        worklist.push_back(srcICFG);
        visited.insert(srcICFG);
 
        while (!worklist.empty() && !feasible)
        {
            const ICFGNode* cur = worklist.front();
            worklist.pop_front();
 
            if (cur != srcICFG && hasRedefineToSameObj(cur, edge))
            {
                // This ICFG path redefines the same object before dst.
            }
            else
            {
                // Treat a call as an intra-procedural summary edge for path
                // queries. Feasibility of the callee body is handled by the
                // normal analysis; here we only need caller-side reachability,
                // e.g. entry -> ret-site.
                if (const CallICFGNode* call =
                            SVFUtil::dyn_cast<CallICFGNode>(cur))
                {
                    const ICFGNode* succ = call->getRetICFGNode();
                    if (!succ || succ->getFun() != fun)
                    {
                        // Ignore missing or cross-function return summaries.
                    }
                    else if (succ == dstICFG)
                    {
                        feasible = true;
                    }
                    else if (!visited.count(succ))
                    {
                        visited.insert(succ);
                        worklist.push_back(succ);
                    }
                    else
                    {
                        // Already visited.
                    }
                }
 
                for (const ICFGEdge* icfgEdge : cur->getOutEdges())
                {
                    const IntraCFGEdge* intraEdge =
                        SVFUtil::dyn_cast<IntraCFGEdge>(icfgEdge);
                    const ICFGNode* succ =
                        intraEdge ? intraEdge->getDstNode() : nullptr;
 
                    if (!intraEdge)
                    {
                        // Non-intra ICFG edges are not part of this path query.
                    }
                    else if (!succ || succ->getFun() != fun)
                    {
                        // Keep the query inside src's function.
                    }
                    else if (!isIntraEdgeBranchFeasible(intraEdge, cur))
                    {
                        // The conditional edge is unreachable in cur's state.
                    }
                    else if (succ == dstICFG)
                    {
                        feasible = true;
                    }
                    else if (!visited.count(succ))
                    {
                        visited.insert(succ);
                        worklist.push_back(succ);
                    }
                    else
                    {
                        // Already visited.
                    }
                }
            }
        }
    }
 
    return feasible;
}

◆ isIntraEdgeBranchFeasible()

bool FullSparseAbstractInterpretation::isIntraEdgeBranchFeasible	(	const IntraCFGEdge *	edge,
		const ICFGNode *	src
	)

private

Return whether this intra edge is allowed by the current branch state.

Definition at line 462 of file SparseAbstractInterpretation.cpp.

{
    bool feasible = true;
    if (!edge->getCondition())
    {
        feasible = true;
    }
    else if (!hasAbsState(src))
    {
        feasible = true;
    }
    else
    {
        AbstractState edgeState = getAbsState(src);
        feasible = isBranchEdgeFeasible(edge, edgeState);
    }
 
    return feasible;
}

◆ joinStates()

void FullSparseAbstractInterpretation::joinStates	(	AbstractState &	dst,
		const AbstractState &	src
	)

overrideprotectedvirtual

Full-sparse does not merge normal value-flow state along ICFG edges. The ICFG join carries only side-channel state that is not represented as MemorySSA def-use flow: GepObjVar field snapshots and _freedAddrs. Base/Dummy ObjVars are populated later by pullObjValueFlows from SVFG indirect in-edges; ValVars stay at their def-sites.

Reimplemented from SVF::AbstractInterpretation.

Definition at line 64 of file SparseAbstractInterpretation.cpp.

{
    // Propagate GepObjVar entries along ICFG edges.  Kill semantics
    // come from handleNode's as.store(addr, val) overwriting trace at
    // store sites (not from a JOIN here), so joinStates only forwards
    // the post-write snapshot.  This lets Gep fields scattered across
    // many store ICFG nodes converge at downstream use sites, and lets
    // extapi handlers (memcpy/memset/strlen) read upstream-written
    // values via plain as.load(srcAddr).  Base/Dummy are NOT propagated
    // here — they ride pullObjValueFlows Step 1 (SVFG indirect edges, with
    // MSSA chi/mu kill semantics).
    for (const auto& [id, val] : src.getLocToVal())
    {
        if (!SVFUtil::isa<GepObjVar>(svfir->getGNode(id)))
            continue;
        u32_t addr = AbstractState::getVirtualMemAddress(id);
        if (dst.getLocToVal().count(id))
            dst.load(addr).join_with(val);
        else
            dst.store(addr, val);
    }
    for (NodeID a : src.getFreedAddrs())
        dst.addToFreedAddrs(a);
}

◆ mergeStatesFromPredecessors()

bool FullSparseAbstractInterpretation::mergeStatesFromPredecessors ( const ICFGNode * node )

overrideprotectedvirtual

Thin wrapper: defer to base for ICFG-edge bookkeeping (predecessor iteration, branch feasibility, joinStates, updateAbsState, reachability return). For reachable nodes, additionally run pullObjValueFlows to populate trace[node] with obj values from SVFG def-sites.

Reimplemented from SVF::AbstractInterpretation.

Definition at line 112 of file SparseAbstractInterpretation.cpp.

{
    refinementTrace.erase(node);
 
    if (!AbstractInterpretation::mergeStatesFromPredecessors(node))
        return false;
 
    pullObjValueFlows(node);
 
    // Compose pred-inherited refinement on top of branch narrowings
    // just captured, then MEET into trace[node] so reads see narrowed.
    propagateAndApplyRefinement(node);
    return true;
}

◆ propagateAndApplyRefinement()

void FullSparseAbstractInterpretation::propagateAndApplyRefinement ( const ICFGNode * node )

private

Compose pred-inherited refinement into refinementTrace[node] (single-pred linear copy / multi-pred intersect-JOIN; any pred without refinement drops the inheritance), then MEET the final refinementTrace[node] into trace[node]._addrToAbsVal so the inherited base getAbsValue(ObjVar*, node) returns the narrowed value directly — no read-time override or cache. Called once per merge as the last step.

Definition at line 502 of file SparseAbstractInterpretation.cpp.

{
    // e.g.
    // if (x > 0) {
    //     use(x); // use 1
    //     use(x); // use 2
    // }
    // Step 1: compose pred-inherited refinement into refinementTrace[node].
    // At use2, we don't have conditional intra-edge, but we can inherit the
    // refinement from use1's conditional edge.  When multiple preds, JOIN the
    // inherited constraints.
    Map<NodeID, IntervalValue> inherited;
    bool inheritOk = true;
    bool first = true;
    for (auto& e : node->getInEdges())
    {
        const ICFGNode* pred = e->getSrcNode();
        if (hasAbsState(pred))
        {
            auto pit = refinementTrace.find(pred);
            if (pit == refinementTrace.end())
            {
                inheritOk = false;
                break;
            }
            else if (first)
            {
                inherited = pit->second;
                first = false;
            }
            else
            {
                for (auto it = inherited.begin(); it != inherited.end();)
                {
                    auto eit = pit->second.find(it->first);
                    if (eit == pit->second.end())
                    {
                        it = inherited.erase(it);
                    }
                    else
                    {
                        it->second.join_with(eit->second);
                        ++it;
                    }
                }
            }
        }
    }
    if (inheritOk && !first && !inherited.empty())
    {
        auto& nodeRef = refinementTrace[node];
        for (const auto& [id, val] : inherited)
        {
            auto rit = nodeRef.find(id);
            if (rit == nodeRef.end())
            {
                nodeRef[id] = val;
            }
            else
            {
                rit->second.meet_with(val);
            }
        }
    }
    // e.g.
    // if (x > 0) {
    //     use(x); // use 1
    //     use(x); // use 2
    // }
    // Step 2: at use1, recordBranchRefinement captures the predState's narrowed
    // constraint into refinementTrace[use1].  At use2, we find the inherited
    // refinement from use1 and MEET it into the base value so the use observes
    // the narrowed constraint.
    auto nit = refinementTrace.find(node);
    if (nit != refinementTrace.end())
    {
        AbstractState& trace = abstractTrace[node];
        for (const auto& [id, constraint] : nit->second)
        {
            if (trace.inAddrToValTable(id))
            {
                u32_t addr = AbstractState::getVirtualMemAddress(id);
                trace.load(addr).getInterval().meet_with(constraint);
            }
        }
    }
}

◆ pullObjValueFlows()

void FullSparseAbstractInterpretation::pullObjValueFlows ( const ICFGNode * node )

private

SVFG-pull helper: walk each VFG node's indirect SVFG in-edges and pull obj values from upstream def-site traces into trace[node]. Multiple sources (e.g. mphi operands) JOIN.

Definition at line 128 of file SparseAbstractInterpretation.cpp.

{
    NodeBS denseLocalObjs;
    for (const auto& item : abstractTrace[node].getLocToVal())
    {
        NodeID id = item.first;
        if (SVFUtil::isa<GepObjVar>(svfir->getGNode(id)))
            denseLocalObjs.set(id);
    }
    // e.g.
    //     store i32 7, i32* %p   ; def-site D for obj_p
    //     ...
    //     %v = load i32, i32* %p ; use-site U
    // Step 1: intra-node SVFG-pull.  For each VFG node hosted at U, walk
    // the indirect SVFG in-edges back to D; for every obj id labelling
    // the edge, JOIN the obj's value at D into U's trace.  GepObjVar
    // labels are pulled exactly.  BaseObjVar labels are expanded to every
    // sibling field via getAllFieldsObjVars because Andersen may label a
    // field-sensitive consumer with the field-insensitive base.
    //
    // Gep fields already present at this node came through the dense
    // ICFG propagation in joinStates.  Treat those as authoritative and
    // do not re-join older SVFG defs over them; otherwise a killed init
    // field can be reintroduced at the load site (e.g. a[9] initialized
    // to 9, overwritten to 10, then pulled back to [9,10]).
    // Reads/writes go through SemiSparse to bypass FullSparse's refinement
    // layer (these are def-site pulls, not real stores; refinement is
    // applied later in propagateAndApplyRefinement).
    for (const VFGNode* v : node->getVFGNodes())
    {
        for (auto eit = v->InEdgeBegin(); eit != v->InEdgeEnd(); ++eit)
        {
            const IndirectSVFGEdge* indEdge =
                SVFUtil::dyn_cast<IndirectSVFGEdge>(*eit);
            if (indEdge)
            {
                const SVFGNode* src =
                    SVFUtil::dyn_cast<SVFGNode>(indEdge->getSrcNode());
                assert(src && "SVFG incoming edge must have a source node");
                assert(v && "SVFG incoming edge must have a destination node");
 
                const ICFGNode* srcICFG = src->getICFGNode();
                const ICFGNode* dstICFG = v->getICFGNode();
                assert(srcICFG && "SVFG source node must have an ICFG node");
                assert(dstICFG &&
                       "SVFG destination node must have an ICFG node");
 
                if (!isIndirectSVFGEdgeFeasible(indEdge, v))
                    continue;
 
                if (srcICFG && hasAbsState(srcICFG))
                {
                    for (NodeID id : indEdge->getPointsTo())
                    {
                        SVFVar* gn = svfir->getGNode(id);
                        NodeBS idsToPull;
 
                        if (SVFUtil::isa<GepObjVar>(gn))
                        {
                            idsToPull.set(id);
                        }
                        else if (auto* base = SVFUtil::dyn_cast<BaseObjVar>(gn))
                        {
                            idsToPull = svfir->getAllFieldsObjVars(base);
                        }
                        else
                        {
                            idsToPull.set(id);
                        }
 
                        for (NodeID fid : idsToPull)
                        {
                            const ObjVar* obj =
                                SVFUtil::dyn_cast<ObjVar>(svfir->getGNode(fid));
                            // Dense Gep propagation has already carried the
                            // current value to this node.
                            if (denseLocalObjs.test(fid))
                            {
                                continue;
                            }
                            if (obj &&
                                    SemiSparseAbstractInterpretation::hasAbsValue(
                                        obj, srcICFG))
                            {
                                AbstractValue cur;
                                if (SemiSparseAbstractInterpretation::
                                        hasAbsValue(obj, node))
                                {
                                    cur = SemiSparseAbstractInterpretation::
                                          getAbsValue(obj, node);
                                }
                                cur.join_with(SemiSparseAbstractInterpretation::
                                              getAbsValue(obj, srcICFG));
                                SemiSparseAbstractInterpretation::
                                updateAbsValue(obj, cur, node);
                            }
                        }
                    }
                }
            }
        }
    }
 
    // Step 2 (boundary pull) intentionally removed: with GepObjVar dense
    // propagation in joinStates above, Gep field values arrive at use
    // sites along ICFG edges without needing the boundary pull.
}

◆ recordBranchRefinement()

void FullSparseAbstractInterpretation::recordBranchRefinement	(	NodeID	objId,
		const IntervalValue &	narrowed,
		AbstractState &	as,
		const ICFGNode *	loadIcfg,
		const ICFGNode *	succ
	)

overrideprotectedvirtual

Capture branch narrowings into refinementTrace[succ] instead of writing them into the local as: in FullSparse as would be discarded by joinStates (no-op for ObjVar), so we route the narrowing to refinementTrace and let propagateAndApplyRefinement bake it into trace at the end of mergeStatesFromPredecessors.

Reimplemented from SVF::AbstractInterpretation.

Definition at line 483 of file SparseAbstractInterpretation.cpp.

{
    if (narrowed.isBottom())
        return;
 
    auto& succRef = refinementTrace[succ];
    auto rit = succRef.find(objId);
    if (rit == succRef.end())
    {
        succRef[objId] = narrowed;
    }
    else
    {
        rit->second.join_with(narrowed);
    }
}

◆ storeValue()

void FullSparseAbstractInterpretation::storeValue	(	const ValVar *	pointer,
		const AbstractValue &	val,
		const ICFGNode *	node
	)

overrideprotectedvirtual

After a store overwrites an ObjVar, clear any branch refinement for that ObjVar at the store's node so stale branch constraints don't propagate past the redefinition.

Reimplemented from SVF::AbstractInterpretation.

Definition at line 90 of file SparseAbstractInterpretation.cpp.

{
    // Clear branch refinement for every ObjVar this store overwrites.
    // A store redefines the ObjVar; the pre-store branch constraint
    // (inherited into refinementTrace[node]) is immediately stale.
    // Without this, successors inherit the stale constraint and MEET
    // it onto the pulled post-store value, erasing the store's effect.
    const AbstractValue& ptrVal = getAbsValue(pointer, node);
    AbstractState& as = getAbsState(node);
    for (auto addr : ptrVal.getAddrs())
    {
        NodeID objId = as.getIDFromAddr(addr);
        auto rit = refinementTrace.find(node);
        if (rit != refinementTrace.end())
            rit->second.erase(objId);
    }
    // Delegate to base for the actual ObjVar update.
    SemiSparseAbstractInterpretation::storeValue(pointer, val, node);
}

Member Data Documentation

◆ refinementTrace

Map<const ICFGNode*, Map<NodeID, IntervalValue> > SVF::FullSparseAbstractInterpretation::refinementTrace

private

Path-refined obj values produced by branch narrowing. Each entry is the interval constraint (not effective value) so base trace can widen/narrow independently. Cached at branch successors by recordBranchRefinement; propagated and applied by propagateAndApplyRefinement at the end of mergeStatesFromPredecessors.

Definition at line 161 of file SparseAbstractInterpretation.h.

◆ svfg

SVFG* SVF::FullSparseAbstractInterpretation::svfg {nullptr}

private

View pointer into svfgBuilder's graph; non-null after buildSVFG().

Definition at line 171 of file SparseAbstractInterpretation.h.

171{nullptr};

◆ svfgBuilder

std::unique_ptr<SVFGBuilder> SVF::FullSparseAbstractInterpretation::svfgBuilder

private

Owns the SVFG (via SVFGBuilder's internal unique_ptr). Without this, SVFGBuilder would be a local in buildSVFG() and free the graph at scope exit, leaving svfg dangling.

Definition at line 169 of file SparseAbstractInterpretation.h.

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

/home/runner/work/SVF/SVF/svf/include/AE/Svfexe/SparseAbstractInterpretation.h
/home/runner/work/SVF/SVF/svf/lib/AE/Svfexe/SparseAbstractInterpretation.cpp

Public Member Functions

Protected Member Functions

Private Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ FullSparseAbstractInterpretation()

◆ ~FullSparseAbstractInterpretation()

Member Function Documentation

◆ buildSVFG()

◆ isICFGPathFeasible()

◆ isIndirectSVFGEdgeFeasible()

◆ isIntraEdgeBranchFeasible()

◆ joinStates()

◆ mergeStatesFromPredecessors()

◆ propagateAndApplyRefinement()

◆ pullObjValueFlows()

◆ recordBranchRefinement()

◆ storeValue()

Member Data Documentation

◆ refinementTrace

◆ svfg

◆ svfgBuilder