SVF::FullSparseAbstractInterpretation Class Reference

#include <SparseAbstractInterpretation.h>

Inheritance diagram for SVF::FullSparseAbstractInterpretation:

Public Member Functions
	FullSparseAbstractInterpretation ()
	~FullSparseAbstractInterpretation () 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.
const Set< const ICFGNode * >	getUseSitesOfValVar (const ValVar *var) const
const ICFGNode *	getDefSiteOfValVar (const ValVar *var) const
const Set< const ICFGNode * >	getDefSiteOfObjVar (const ObjVar *obj, const ICFGNode *node) const
const Set< const ICFGNode * >	getUseSitesOfObjVar (const ObjVar *obj, const ICFGNode *node) const
const AbstractValue &	getAbsValue (const ValVar *var, const ICFGNode *node) override
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)
bool	hasAbsValue (const ValVar *var, const ICFGNode *node) const override
	Side-effect-free existence check.
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
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)
std::deque< 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)
AbstractValue	loadValue (const ValVar *pointer, const ICFGNode *node)
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
void	buildSVFG ()
	Build the SVFG on top of the semi-sparse precompute.
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	shouldApplyNarrowing (const FunObjVar *fun)
	Check if narrowing should be applied: always for regular loops, mode-dependent for recursion.

Protected Attributes
SVFG *	svfg {nullptr}
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

Additional Inherited Members
Public Types inherited from SVF::AbstractInterpretation
enum	AESparsity { Dense , SemiSparse , Sparse }
enum	HandleRecur { TOP , WIDEN_ONLY , WIDEN_NARROW }
Static Public Member Functions inherited from SVF::AbstractInterpretation
static AbstractInterpretation &	getAEInstance ()

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. ValVar reads currently assert(false) until the SVFG-backed resolution lands (see doc/plan-full-sparse.md); cycle helpers are inherited from the semi-sparse parent and will also need extension for ObjVars.

Definition at line 83 of file SparseAbstractInterpretation.h.

Constructor & Destructor Documentation

FullSparseAbstractInterpretation()

SVF::FullSparseAbstractInterpretation::FullSparseAbstractInterpretation ( )

inline

Definition at line 86 of file SparseAbstractInterpretation.h.

    {
        buildSVFG();
    }

~FullSparseAbstractInterpretation()

FullSparseAbstractInterpretation::~FullSparseAbstractInterpretation ( )

override

Definition at line 42 of file SparseAbstractInterpretation.cpp.

{
    delete svfg;
}

Member Function Documentation

buildSVFG()

void FullSparseAbstractInterpretation::buildSVFG ( )

protected

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

Definition at line 47 of file SparseAbstractInterpretation.cpp.

{
    SVFGBuilder memSSA(true);
    svfg = memSSA.buildFullSVFG(preAnalysis->getPointerAnalysis());
}

getAbsValue() [1/5]

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

virtual

Reimplemented from SVF::AbstractInterpretation.

Definition at line 60 of file AbstractStateManager.cpp.

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

getAbsValue() [2/5]

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

virtual

Reimplemented from SVF::AbstractInterpretation.

Definition at line 60 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/5]

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

virtual

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 60 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/5]

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

overridevirtual

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 63 of file SparseAbstractInterpretation.cpp.

{
    assert(false && "FullSparseAbstractInterpretation::getAbsValue not implemented");
    abort();
}

getAbsValue() [5/5]

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

overridevirtual

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 59 of file AbstractStateManager.cpp.

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

getDefSiteOfObjVar()

const Set< const ICFGNode * > FullSparseAbstractInterpretation::getDefSiteOfObjVar	(	const ObjVar *	obj,
		const ICFGNode *	node
	)		const

Given an ObjVar and its def-site ICFGNode, find all use-site ICFGNodes by following outgoing IndirectSVFGEdges whose pts contains the ObjVar

Definition at line 96 of file SparseAbstractInterpretation.cpp.

{
    assert(svfg && "SVFG is not built for full-sparse AE");
    Set<const ICFGNode*> defSites;
    for(auto* vNode : node->getVFGNodes())
    {
        for(const SVFGNode* svfgNode : svfg->getDefSiteOfObjVar(obj, vNode))
        {
            defSites.insert(svfgNode->getICFGNode());
        }
    }
    return defSites;
}

getDefSiteOfValVar()

const ICFGNode * FullSparseAbstractInterpretation::getDefSiteOfValVar

(

const ValVar *

var

)

const

Definition at line 89 of file SparseAbstractInterpretation.cpp.

{
    assert(svfg && "SVFG is not built for full-sparse AE");
    return svfg->getDefSiteOfValVar(var)->getICFGNode();
}

getUseSitesOfObjVar()

const Set< const ICFGNode * > FullSparseAbstractInterpretation::getUseSitesOfObjVar	(	const ObjVar *	obj,
		const ICFGNode *	node
	)		const

Given an ObjVar and its def-site ICFGNode, find all use-site ICFGNodes by following outgoing IndirectSVFGEdges whose pts contains the ObjVar

Definition at line 111 of file SparseAbstractInterpretation.cpp.

{
    assert(svfg && "SVFG is not built for full-sparse AE");
    Set<const ICFGNode*> useSites;
    for(auto* vNode : node->getVFGNodes())
    {
        for(const SVFGNode* svfgNode : svfg->getUseSitesOfObjVar(obj, vNode))
        {
            useSites.insert(svfgNode->getICFGNode());
        }
    }
    return useSites;
}

getUseSitesOfValVar()

const Set< const ICFGNode * > FullSparseAbstractInterpretation::getUseSitesOfValVar

(

const ValVar *

var

)

const

Definition at line 77 of file SparseAbstractInterpretation.cpp.

{
    assert(svfg && "SVFG is not built for full-sparse AE");
    Set<const ICFGNode*> useSites;
    for(const SVFGNode* svfgNode : svfg->getUseSitesOfValVar(var))
    {
        useSites.insert(svfgNode->getICFGNode());
    }
    return useSites;
}

hasAbsValue() [1/5]

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

virtual

Reimplemented from SVF::AbstractInterpretation.

Definition at line 63 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/5]

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

virtual

Reimplemented from SVF::AbstractInterpretation.

Definition at line 63 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/5]

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

virtual

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 63 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/5]

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

overridevirtual

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 70 of file SparseAbstractInterpretation.cpp.

{
    assert(false && "FullSparseAbstractInterpretation::hasAbsValue not implemented");
    abort();
}

hasAbsValue() [5/5]

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

overridevirtual

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 62 of file AbstractStateManager.cpp.

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

Member Data Documentation

svfg

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

protected

Definition at line 114 of file SparseAbstractInterpretation.h.

{nullptr};

---

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