SVF::SemiSparseAbstractInterpretation Class Reference

#include <SparseAbstractInterpretation.h>

Inheritance diagram for SVF::SemiSparseAbstractInterpretation:

Public Member Functions
	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.
virtual void	storeValue (const ValVar *pointer, const AbstractValue &val, const ICFGNode *node)
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
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 ()
virtual bool	mergeStatesFromPredecessors (const ICFGNode *node)
bool	isBranchEdgeFeasible (const IntraCFGEdge *edge, AbstractState &as)
void	collectBranchRefinement (const IntraCFGEdge *edge, AbstractState &as)
virtual void	recordBranchRefinement (NodeID objId, const IntervalValue &narrowed, AbstractState &as, const ICFGNode *loadIcfg, const ICFGNode *succ)
bool	shouldApplyNarrowing (const FunObjVar *fun)
	Check if narrowing should be applied: always for regular loops, mode-dependent for recursion.

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::SemiSparse.

ValVars live at their SVFG-style def-sites: reads pull from there, writes go there, state merges replace only the ObjVar map and skip the ValVar map, and the cycle helpers gather/scatter cycle ValVars around each widening iteration.

Definition at line 43 of file SparseAbstractInterpretation.h.

Constructor & Destructor Documentation

SemiSparseAbstractInterpretation()

SVF::SemiSparseAbstractInterpretation::SemiSparseAbstractInterpretation ( )

inline

Definition at line 46 of file SparseAbstractInterpretation.h.

    {
        preAnalysis->initCycleValVars();
    }

~SemiSparseAbstractInterpretation()

SVF::SemiSparseAbstractInterpretation::~SemiSparseAbstractInterpretation ( )

overridedefault

Member Function Documentation

getAbsValue() [1/4]

const AbstractValue & AbstractInterpretation::getAbsValue ( const ObjVar *  var, const ICFGNode *  node  )

protectedvirtual

Reimplemented from SVF::AbstractInterpretation.

Definition at line 143 of file AbstractStateManager.cpp.

{
    AbstractState& as = getAbsState(node);
    u32_t addr = AbstractState::getVirtualMemAddress(var->getId());
    return as.load(addr);
}

getAbsValue() [2/4]

const AbstractValue & AbstractInterpretation::getAbsValue ( const SVFVar *  var, const ICFGNode *  node  )

protectedvirtual

Reimplemented from SVF::AbstractInterpretation.

Definition at line 144 of file AbstractStateManager.cpp.

{
    if (const ObjVar* objVar = SVFUtil::dyn_cast<ObjVar>(var))
        return getAbsValue(objVar, node);
    if (const ValVar* valVar = SVFUtil::dyn_cast<ValVar>(var))
        return getAbsValue(valVar, node);
    assert(false && "Unknown SVFVar kind");
    abort();
}

getAbsValue() [3/4]

const AbstractValue & AbstractInterpretation::getAbsValue ( const ValVar *  var, const ICFGNode *  node  )

protectedvirtual

Read a top-level variable's abstract value. Dense base does a direct trace lookup; sparse subclasses override with their own resolution chain (def-site walk, call-result fallback, etc.). All three overloads are virtual so full-sparse can route ObjVar reads through the SVFG.

Dense base: direct trace lookup, with a top sentinel for genuinely missing entries (e.g. function parameters like argc, never written before first read). Sparse subclasses override with a def-site resolution chain.

The "in map" check is a raw map.count — NOT inVarToValTable / inVarToAddrsTable, which gate on isInterval / isAddr. SVF canonically represents uninit and null-pointer shapes as (interval=bottom ∧ addrs=∅); those predicates would falsely report such an entry as "not present", and the top fallback below would then clobber the very signal NullptrDerefDetector::isUninit keys off.

Reimplemented from SVF::AbstractInterpretation.

Definition at line 142 of file AbstractStateManager.cpp.

{
    u32_t id = var->getId();
    AbstractState& as = abstractTrace[node];
    if (as.getVarToVal().count(id))
        return as[id];
    as[id] = IntervalValue::top();
    return as[id];
}

getAbsValue() [4/4]

const AbstractValue & SemiSparseAbstractInterpretation::getAbsValue ( const ValVar *  var, const ICFGNode *  node  )

overrideprotectedvirtual

Read a top-level variable's abstract value. Dense base does a direct trace lookup; sparse subclasses override with their own resolution chain (def-site walk, call-result fallback, etc.). All three overloads are virtual so full-sparse can route ObjVar reads through the SVFG.

Dense base: direct trace lookup, with a top sentinel for genuinely missing entries (e.g. function parameters like argc, never written before first read). Sparse subclasses override with a def-site resolution chain.

The "in map" check is a raw map.count — NOT inVarToValTable / inVarToAddrsTable, which gate on isInterval / isAddr. SVF canonically represents uninit and null-pointer shapes as (interval=bottom ∧ addrs=∅); those predicates would falsely report such an entry as "not present", and the top fallback below would then clobber the very signal NullptrDerefDetector::isUninit keys off.

Reimplemented from SVF::AbstractInterpretation.

Definition at line 719 of file SparseAbstractInterpretation.cpp.

{
    // Read from the var's def-site (where updateAbsValue wrote it).
    return AbstractInterpretation::getAbsValue(var, getICFGNode(var));
}

getFullCycleHeadState()

AbstractState SemiSparseAbstractInterpretation::getFullCycleHeadState ( const ICFGCycleWTO *  cycle )

overrideprotectedvirtual

Build a full cycle-head AbstractState. Dense default: trace[cycle_head] as-is. Semi-sparse subclass: also pull cycle ValVars from def-sites.

Reimplemented from SVF::AbstractInterpretation.

Definition at line 591 of file SparseAbstractInterpretation.cpp.

{
    // Start from the dense snapshot (ObjVars + any ValVars that happen to
    // be cached at cycle_head's trace entry).
    AbstractState snap = AbstractInterpretation::getFullCycleHeadState(cycle);
 
    const Set<const ValVar*>& valVars = preAnalysis->getCycleValVars(cycle);
    if (valVars.empty())
        return snap;  // no cycle ValVars known: nothing to pull
 
    // Drop stale ValVar entries and pull each cycle ValVar from its
    // def-site.  ValVars without a genuine stored value are skipped to
    // avoid getAbsValue's top-fallback contaminating body def-sites on
    // the subsequent widen/narrow scatter.
    snap.clearValVars();
    for (const ValVar* v : valVars)
    {
        const ICFGNode* defSite = v->getICFGNode();
        if (!defSite || !hasAbsValue(v, defSite))
            continue;
        snap[v->getId()] = getAbsValue(v, defSite);
    }
    return snap;
}

getICFGNode()

const ICFGNode * SemiSparseAbstractInterpretation::getICFGNode ( const ValVar *  var ) const

protected

Definition at line 687 of file SparseAbstractInterpretation.cpp.

{
    // const ValVars are all defined in global node
    if (!var->getICFGNode())
    {
        return svfir->getICFG()->getGlobalICFGNode();
    }
    // for return value of callsite, use the ret-site as def-site
    else if (SVFUtil::isa<CallICFGNode>(var->getICFGNode()) &&
             SVFUtil::isa<RetValPN>(var))
    {
        return SVFUtil::dyn_cast<CallICFGNode>(var->getICFGNode())
               ->getRetICFGNode();
    }
    // for other ValVars, use their def-site as the node to query abstract
    // value.
    else
    {
        return var->getICFGNode();
    }
}

hasAbsValue() [1/4]

bool AbstractInterpretation::hasAbsValue ( const ObjVar *  var, const ICFGNode *  node  ) const

protectedvirtual

Reimplemented from SVF::AbstractInterpretation.

Definition at line 148 of file AbstractStateManager.cpp.

{
    auto it = abstractTrace.find(node);
    if (it == abstractTrace.end())
        return false;
    return it->second.getLocToVal().count(var->getId()) != 0;
}

hasAbsValue() [2/4]

bool AbstractInterpretation::hasAbsValue ( const SVFVar *  var, const ICFGNode *  node  ) const

protectedvirtual

Reimplemented from SVF::AbstractInterpretation.

Definition at line 149 of file AbstractStateManager.cpp.

{
    if (const ObjVar* objVar = SVFUtil::dyn_cast<ObjVar>(var))
        return hasAbsValue(objVar, node);
    if (const ValVar* valVar = SVFUtil::dyn_cast<ValVar>(var))
        return hasAbsValue(valVar, node);
    return false;
}

hasAbsValue() [3/4]

bool AbstractInterpretation::hasAbsValue ( const ValVar *  var, const ICFGNode *  node  ) const

protectedvirtual

Side-effect-free existence check.

Dense base: direct existence check at node. Mirrors the simplified getAbsValue lookup — uses raw map.contains rather than inVar*Table predicates, which would falsely report neutral (interval=bottom ∧ addrs=∅) entries as "not present".

Reimplemented from SVF::AbstractInterpretation.

Definition at line 147 of file AbstractStateManager.cpp.

{
    auto it = abstractTrace.find(node);
    if (it == abstractTrace.end())
        return false;
    return it->second.getVarToVal().count(var->getId()) != 0;
}

hasAbsValue() [4/4]

bool SemiSparseAbstractInterpretation::hasAbsValue ( const ValVar *  var, const ICFGNode *  node  ) const

overrideprotectedvirtual

Side-effect-free existence check.

Dense base: direct existence check at node. Mirrors the simplified getAbsValue lookup — uses raw map.contains rather than inVar*Table predicates, which would falsely report neutral (interval=bottom ∧ addrs=∅) entries as "not present".

Reimplemented from SVF::AbstractInterpretation.

Definition at line 726 of file SparseAbstractInterpretation.cpp.

{
    return AbstractInterpretation::hasAbsValue(var, getICFGNode(var));
}

joinStates()

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

overrideprotectedvirtual

Join src into dst with sparsity-aware semantics. Dense merges everything; semi-sparse skips ValVars.

Reimplemented from SVF::AbstractInterpretation.

Definition at line 667 of file SparseAbstractInterpretation.cpp.

{
    // ValVars live at def-sites in semi-sparse mode; they don't flow
    // through state merges.  Iterate src's ObjVar (_addrToAbsVal) entries
    // directly and join into dst, leaving dst's ValVar map untouched.
    // _freedAddrs (used by the null-deref detector) also rides along
    // ICFG edges — there is no SVFG-level encoding of free events.
    for (const auto& [id, val] : src.getLocToVal())
    {
        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);
}

narrowCycleState()

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

overrideprotectedvirtual

Narrow prev with cur; write the narrowed state back. Returns true when narrowing is disabled or the narrowed state equals prev. Semi-sparse subclass scatters the narrowed ValVars on non-fixpoint.

Reimplemented from SVF::AbstractInterpretation.

Definition at line 635 of file SparseAbstractInterpretation.cpp.

{
    // Delegate to base.  It returns true on the two non-scatter cases
    // (narrowing disabled, or narrow fixpoint); we preserve the original
    // "skip scatter at fixpoint" semantics by bailing early here.
    bool fixpoint = AbstractInterpretation::narrowCycleState(prev, cur, cycle);
    if (fixpoint)
        return true;
 
    // Non-fixpoint: base wrote the narrowed state to trace.  Scatter the
    // narrowed ValVars back to def-sites.
    const ICFGNode* cycle_head = cycle->head()->getICFGNode();
    const AbstractState& next = abstractTrace[cycle_head];
    for (const auto& [id, val] : next.getVarToVal())
        updateAbsValue(svfir->getSVFVar(id), val, cycle_head);
    return false;
}

updateAbsState()

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

overrideprotectedvirtual

Replace the state at node. Sparse subclasses replace only the ObjVar map (ValVars live at def-sites).

Reimplemented from SVF::AbstractInterpretation.

Definition at line 659 of file SparseAbstractInterpretation.cpp.

{
    // Only replace ObjVar state.  ValVars live at their def-sites and
    // must not be overwritten when the predecessor's state is merged in.
    abstractTrace[node].updateAddrStateOnly(state);
}

updateAbsValue() [1/4]

void AbstractInterpretation::updateAbsValue ( const ObjVar *  var, const AbstractValue &  val, const ICFGNode *  node  )

protectedvirtual

Reimplemented from SVF::AbstractInterpretation.

Definition at line 154 of file AbstractStateManager.cpp.

{
    AbstractState& as = getAbsState(node);
    u32_t addr = AbstractState::getVirtualMemAddress(var->getId());
    as.store(addr, val);
}

updateAbsValue() [2/4]

void AbstractInterpretation::updateAbsValue ( const SVFVar *  var, const AbstractValue &  val, const ICFGNode *  node  )

protectedvirtual

Reimplemented from SVF::AbstractInterpretation.

Definition at line 155 of file AbstractStateManager.cpp.

{
    if (const ObjVar* objVar = SVFUtil::dyn_cast<ObjVar>(var))
        updateAbsValue(objVar, val, node);
    else if (const ValVar* valVar = SVFUtil::dyn_cast<ValVar>(var))
        updateAbsValue(valVar, val, node);
    else
        assert(false && "Unknown SVFVar kind");
}

updateAbsValue() [3/4]

void AbstractInterpretation::updateAbsValue ( const ValVar *  var, const AbstractValue &  val, const ICFGNode *  node  )

protectedvirtual

Write a variable's abstract value. Sparse subclasses re-route ValVar writes to the def-site.

Reimplemented from SVF::AbstractInterpretation.

Definition at line 153 of file AbstractStateManager.cpp.

{
    abstractTrace[node][var->getId()] = val;
}

updateAbsValue() [4/4]

void SemiSparseAbstractInterpretation::updateAbsValue ( const ValVar *  var, const AbstractValue &  val, const ICFGNode *  node  )

overrideprotectedvirtual

Write a variable's abstract value. Sparse subclasses re-route ValVar writes to the def-site.

Reimplemented from SVF::AbstractInterpretation.

Definition at line 710 of file SparseAbstractInterpretation.cpp.

{
    // Write to the var's def-site so getAbsValue stays consistent.
    const ICFGNode* defNode = var->getICFGNode();
    abstractTrace[defNode ? defNode : node][var->getId()] = val;
}

widenCycleState()

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

overrideprotectedvirtual

Widen prev with cur; write the widened state to trace[cycle_head]. Returns true when next == prev (fixpoint). Semi-sparse subclass additionally scatters ValVars to their def-sites.

Reimplemented from SVF::AbstractInterpretation.

Definition at line 617 of file SparseAbstractInterpretation.cpp.

{
    // Base widens, writes trace[cycle_head], and returns fixpoint bool.
    bool fixpoint = AbstractInterpretation::widenCycleState(prev, cur, cycle);
 
    // Scatter the widened ValVars back to their def-sites so body nodes
    // observe the widened values on the next iteration.  Matches the
    // pre-refactor semantics: scatter unconditionally, including at
    // widening fixpoint (see the narrowing-starts-with-stale-body issue
    // fixed by always writing widened state back).
    const ICFGNode* cycle_head = cycle->head()->getICFGNode();
    const AbstractState& next = abstractTrace[cycle_head];
    for (const auto& [id, val] : next.getVarToVal())
        updateAbsValue(svfir->getSVFVar(id), val, cycle_head);
    return fixpoint;
}

---

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