Draft Full sparse (should talk about functions)

[bjjwwang]

PR Description — Full-Sparse AE for SVF

TL;DR

Add a third sparsity mode to SVF's abstract execution. Replace dense's "copy entire _addrToAbsVal at every ICFG node" with three SSA-anchored transfers + two AE-side overlays. Memory drops 98% versus Dense; 332/352 tests pass; Dense and Semi-Sparse remain at 352/352.

---

Why Full-Sparse

Dense AE's mergeStatesFromPredecessors does two unrelated jobs at once:

1. Propagating store-produced values along ICFG edges (the legitimate dataflow job).
2. Materialising reaching values at every non-store SSA anchor as a side-effect of bulk state copy — phi nodes, function entries, call returns. This second job is what makes Dense's reader "just work": trace[useNode]._addrToAbsVal[obj] is always populated, regardless of whether the reaching def is a store, a phi, a function entry, or a call return.

Full-Sparse decouples the two. Values live at MSSA def-anchors only; reads route through getDefSiteOfObjVar. Memory cost falls from O(ICFG nodes × all ObjVars) to O(real def-anchors only).

But once we kick out the bulk copy, three things Dense had implicitly stop working. The PR is essentially "rebuild those three things sparingly":

1. Non-store SSA anchors (MSSAPHI / FormalIN / ActualOUT) need to be filled by someone, since merge no longer materialises them. → Three transfer helpers (Section 1).
2. Branch refinement (cmp-induced narrowing) and GEP-precision refinements were carried by merge's bulk copy. → Two AE-side overlays (Section 2 + the pathRefinedAt table for branches).
3. Cycle widening relied on trace[cycleHead] having every variable's current value because merge put them there. → ValVar pull-and-scatter at cycle heads + ObjVar via re-firing transfers (Section 3).

---

1. Why three new transfer helpers?

void runMSSAPHITransferAt(const ICFGNode* N);
void runFormalINTransferAt(const ICFGNode* N);
void runActualOUTTransferAt(const ICFGNode* N);

The invariant they establish

For every ICFG node N that getDefSiteOfObjVar may return, and every ObjVar o it anchors at N, there is exactly one filler that writes trace[N]._addrToAbsVal[o] during N's WTO visit, before any downstream reader observes it.

MSSA produces exactly five kinds of ObjVar def-anchors:

Anchor SVFG node | ICFG host | Filler -- | -- | -- StoreVFGNode | store stmt | existing updateStateOnStore MSSAPHISVFGNode | block entry / cycle head | runMSSAPHITransferAt FormalINSVFGNode | FunEntryICFGNode | runFormalINTransferAt ActualOUTSVFGNode (normal callee) | RetICFGNode | runActualOUTTransferAt ActualOUTSVFGNode (ExtAPI callee) | CallICFGNode | existing AbsExtAPI handler

ES_Loc_TOTAL (ObjVar storage) drops 98.2% versus Dense. ES_Var_TOTAL (ValVar storage) drops 97.7%.

Dense and Semi-Sparse remain unchanged at 352/352 — none of the new mechanisms fire in those modes.

---

Out of scope (the 20 remaining failures)

• 4 × recursive_afterrec: ActualOUT chain through self-recursive SCCs needs more iteration; tractable follow-up.
• 6 × detector FP/FN under branch refinement: pathRefinedAt overlay needs to extend to ValVar pointers (if (cond) p = NULL; UNSAFE_LOAD(p);).
• 5 × ExtAPI / scanf / switch / memcpy edge cases: middling effort.
• 1 × BASIC_array_int_0: Phase D's flow-insensitive trade-off (won't fix without losing the simplicity).
• 4 × very complex CFG (goto + nested loops + while-true exit): borderline cases.

None indicate a soundness regression.

---

Files changed

• svf/include/AE/Svfexe/AbstractStateManager.h: public API for the three transfers, pathRefinedAt, gepOverlay.
• svf/lib/AE/Svfexe/AbstractStateManager.cpp: transfer implementations, sparsity-aware reader, gepOverlay write/read paths.
• svf/lib/AE/Svfexe/AbstractInterpretation.cpp: driver hooks for the three transfers, modified mergeStatesFromPredecessors, modified isCmpBranchFeasible signature.
• svf/lib/AE/Core/AbstractState.cpp: sparsity gate in joinWith.
• svf/lib/AE/Svfexe/SparseAbstractInterpretation.cpp: cycle ValVar pull-and-scatter.
• svf/lib/AE/Svfexe/PreAnalysis.cpp: initCycleValVars for the bottom-up cycle ValVar set.
• svf/lib/AE/Svfexe/AbsExtAPI.cpp: ObjVar reads in ExtAPI handlers go through the sparsity-aware reader.

No SVFG / VFG / ICFG / MSSA / Andersen header or behavioural changes.

PR Description — Full-Sparse AE for SVF TL;DR Add a third sparsity mode to SVF's abstract execution. Replace dense's "copy entire _addrToAbsVal at every ICFG node" with three SSA-anchored transfers + two AE-side overlays. Memory drops 98% versus Dense; 332/352 tests pass; Dense and Semi-Sparse remain at 352/352.

Why Full-Sparse
Dense AE's mergeStatesFromPredecessors does two unrelated jobs at once:

Propagating store-produced values along ICFG edges (the legitimate dataflow job).
Materialising reaching values at every non-store SSA anchor as a side-effect of bulk state copy — phi nodes, function entries, call returns. This second job is what makes Dense's reader "just work": trace[useNode]._addrToAbsVal[obj] is always populated, regardless of whether the reaching def is a store, a phi, a function entry, or a call return.
Full-Sparse decouples the two. Values live at MSSA def-anchors only; reads route through getDefSiteOfObjVar. Memory cost falls from O(ICFG nodes × all ObjVars) to O(real def-anchors only).

But once we kick out the bulk copy, three things Dense had implicitly stop working. The PR is essentially "rebuild those three things sparingly":

Non-store SSA anchors (MSSAPHI / FormalIN / ActualOUT) need to be filled by someone, since merge no longer materialises them. → Three transfer helpers (Section 1).
Branch refinement (cmp-induced narrowing) and GEP-precision refinements were carried by merge's bulk copy. → Two AE-side overlays (Section 2 + the pathRefinedAt table for branches).
Cycle widening relied on trace[cycleHead] having every variable's current value because merge put them there. → ValVar pull-and-scatter at cycle heads + ObjVar via re-firing transfers (Section 3).

1. Why three new transfer helpers?

void runMSSAPHITransferAt(const ICFGNode* N);
void runFormalINTransferAt(const ICFGNode* N);
void runActualOUTTransferAt(const ICFGNode* N);
The invariant they establish
For every ICFG node N that getDefSiteOfObjVar may return, and every ObjVar o it anchors at N, there is exactly one filler that writes trace[N]._addrToAbsVal[o] during N's WTO visit, before any downstream reader observes it.

MSSA produces exactly five kinds of ObjVar def-anchors:

Anchor SVFG node ICFG host Filler
StoreVFGNode store stmt existing updateStateOnStore
MSSAPHISVFGNode block entry / cycle head runMSSAPHITransferAt
FormalINSVFGNode FunEntryICFGNode runFormalINTransferAt
ActualOUTSVFGNode (normal callee) RetICFGNode runActualOUTTransferAt
ActualOUTSVFGNode (ExtAPI callee) CallICFGNode existing AbsExtAPI handler
Without these three helpers, four out of five anchor kinds would be empty when the reader tries to read from them — and the entire sparse design collapses into "everything reads top".

What they share — one pattern, three flavours

runXxxTransferAt(N):
for each Xxx-kind VFG node D at N:
for each obj in D.MR.getPointsTo():
meet = ⊥
for each upstream CHI U of D (via SVFG indirect edges):
if trace[U.ICFGNode][obj] exists:
meet ⊔= trace[U.ICFGNode][obj]
commitTransferValue(trace[N], obj, meet) # fill-empty-only
The only thing that varies is how upstream CHIs are reached — and that boils down to one SVFG quirk: MU (use-annotation) nodes don't hold values, only CHI (def-annotation) nodes do. If an edge leads to a MU, walk one more indirect-edge hop.

Transfer Direct upstream MU intermediary? Hops
MSSAPHI indirect in-edges → operand CHIs no 1
FormalIN CallIndSVFGEdge → ActualIN (CallMU) → upstream CHI yes 2 (then fall back to globalICFGNode if no caller reached)
ActualOUT RetIndSVFGEdge → FormalOUT (RetMU) → callee CHI yes 2 (skip entirely if callee is ExtAPI)
Critical detail: commitTransferValue is fill-empty-only
The transfer only writes to slots merge left empty. If merge already wrote a value (which it can, when isCmpBranchFeasible narrowed the pred state in Dense/Phase-A), the transfer defers. Without this, transfer's un-refined upstream values would clobber merge's branch-refined precision and break four assert tests in early prototyping.

In the final design (Phase B+ where merge skips ObjVar copy entirely), the slot is always empty when the transfer runs and the transfer becomes the primary filler — but the fill-empty-only semantics stay as a safety property.

getPathRefinedAt

Map<const ICFGNode*, Map<NodeID, AbstractValue>>& getPathRefinedAt();
This is the public accessor for the branch refinement overlay — a separate concern from the three transfers but tied into the same reader. The overlay stores per-ObjVar narrowings that come from if (p < 5) style cmp branches, which MSSA does not model (cmp is not a def in SSA). It is populated by the modified mergeStatesFromPredecessors (folding each feasible edge's narrowingDelta from isCmpBranchFeasible) and consumed by getAbstractValue(ObjVar, useNode) via meet at read time.

Why we need to expose it: cycle handling (SparseAbstractInterpretation::widenCycleState) and external diagnostics need to inspect / preserve the overlay across iterations.

2. Why gepOverlay?

Map<NodeID, AbstractValue> gepOverlay;
The disconnect
AE precise-refines GEP fields at runtime via getGepObjAddrs(base, [low, high]):

int a[10];
a[3] = 7; // AE writes obj-id 42 (= GepObjVar(base=37, offset=3))
v = a[3]; // AE reads obj-id 42
But MSSA / Andersen are static — they only see the base obj arr (id 37) for these stores, not the field-precise GepObjVar id 42. Concretely:

getDefSiteOfObjVar(42, useNode) returns null because no SVFG indirect edge has 42 in its PointsTo set.
The globalICFGNode fallback for non-globally-initialised arrays returns nothing.
So a GepObjVar read in pure sparse mode would always return ⊤. Every array test would fail.

What we tried first and discarded
ICFG reverse BFS fallback: walk back from useNode via ICFG in-edges until we find a node whose trace holds obj 42. Worked correctly (324/352) but was an O(N) graph walk inside a function that should be O(1), with stale-cache issues across WTO iterations.
Route via base's MSSA def-site: call getDefSiteOfObjVar(baseObj, useNode), then read trace[defNode][gepId]. Triggered SVFG's hard assert(defSite == nullptr && "unique indirect definition"), because complex ICFG nodes (call sites, init nodes) host multiple VFG nodes referencing the base — multiple matches violate the API's unique-def invariant.
Selectively merge only GepObjVar ids: in joinWith, copy only ids whose SVFVar is a GepObjVar. Memory exploded to 2.24M Loc entries because struct field GepObjVars propagated densely to every node in their containing function.
The shipped solution
A flow-insensitive global map keyed by GepObjVar's NodeID (which uniquely encodes (base, offset) via SVFIR's canonical getGepObjVar). Single map, lives in AbstractStateManager.

storeValue(p, val, n):
... # existing trace + Andersen mirror writes
for o in pts(p):
if o is GepObjVar:
gepOverlay[o.id].join_with(val) # fold to the global map

getAbstractValue(ObjVar* var, ICFGNode* node):
... step 1-3 (local, MSSA, globalICFGNode) ...
if !base && var is GepObjVar: # step 4
if gepOverlay.has(var.id):
base = gepOverlay[var.id]
Why this works
Reader O(1): single Map::find, no graph walk.
No SVFG modification: doesn't touch the asserting API.
Unaffected by sparse merge gating: gepOverlay is a separate global structure, propagation isn't merge's job.
Cross-procedural for free: every GepObjVar write across all functions folds into the same map; reads anywhere find them.
Trade-off: flow-insensitive
GepObjVar values use join_with only — never strong-update. So:

a[3]=7; a[3]=11; assert(a[3]==11) reads [7, 11] (joined), not 11. One test regresses (BASIC_array_int_0).
a[3]=7; a[5]=11; assert(a[3]==7) still reads 7 (different keys). Works fine.
for (i...) a[i] = 0; a[k] = 99; assert(a[k]==99) reads [0, 99]. Loses precision in this pattern.
In our 352-test suite, net effect is +8 tests passing versus BFS — flow-insensitivity costs 1 test but the BFS version had its own staleness bugs in cycles that cost more.

Why GepObjVar can get away without widening
A standard concern with flow-insensitive join-only structures is termination. For interval domains it isn't a problem: the lattice has finite height (bounded by [-INF, INF]), and join_with only ever climbs the lattice. So gepOverlay naturally terminates without needing an explicit widen operator. Precision is sacrificed; soundness and termination are not.

3. How Full-Sparse handles cycles
   Cycles are the place where everything sparse-related compounds. The challenge: WTO widening compares prev and cur snapshots at the cycle head, and Dense relies on those snapshots having every value via merge's bulk copy. Sparse's prev/cur snapshots come from trace[cycleHead], which doesn't store ValVars at all in sparse mode.

We solve ValVar and ObjVar with two different mechanisms.

3.1 ValVar — pull-and-scatter
In sparse, ValVars only live at their def-sites (var->getICFGNode()). They are never written to trace[cycleHead] by merge. So we must explicitly transport them in and out of the cycle head's snapshot.

Pre-analysis collects the cycle's ValVar set (PreAnalysis::initCycleValVars):

Map<const ICFGCycleWTO*, Set<const ValVar*>> cycleToValVars;
Bottom-up over the WTO: each cycle's ValVar set = LHS ValVars of every stmt in its singleton members + nested sub-cycles' sets + (if head is a FunEntryICFGNode) formal parameters. Computed once before AE runs; reused on every iteration.

Entering the cycle iteration (SparseAbstractInterpretation::getFullCycleHeadState):

AbstractState snap = base::getFullCycleHeadState(cycle); // ObjVars come from trace
snap.clearValVars();
for (const ValVar* v : preAnalysis->getCycleValVars(cycle)):
if (v->getICFGNode() && hasAbsValue(v, v->getICFGNode())):
snap[v->getId()] = getAbsValue(v, v->getICFGNode()) // pull from def-site
Exiting the cycle iteration (widenCycleState / narrowCycleState):

base::widenCycleState(prev, cur, cycle) // writes widened state to trace[cycleHead]
for (id, val) in trace[cycleHead].getVarToVal():
updateAbsValue(svfir->getSVFVar(id), val, cycleHead) // scatter back to def-site
Note that updateAbsValue in sparse mode internally routes the write to the var's def-site (not literally cycleHead) — that's how the next iteration's body reads pick up the widened value.

3.2 ObjVar — no scatter, just re-fire runMSSAPHITransferAt
ObjVars do live in trace[cycleHead]._addrToAbsVal in sparse mode, populated each iteration by runMSSAPHITransferAt(cycleHead) (which joins from operand def-sites = entry def + back-edge def per latch). This means:

The widen-set for ObjVars is implicit — it's exactly MR.getPointsTo() of the MSSAPHIs at cycle head, computed dynamically each iteration. No pre-collection needed.
No scatter needed — values stay in trace[cycleHead]. The next iteration's body reads route via getDefSiteOfObjVar(o, useNode), which (for objs whose defs reach via the cycle's MSSAPHI) returns cycleHead, and the read finds the widened value there.
Per-iteration timeline:

iter k:
prev = getFullCycleHeadState(cycle) # ObjVars: copy of trace[cycleHead] from iter k-1
# ValVars: pulled from def-sites

mergeStatesFromPredecessors(cycleHead) # sparse: clears _addrToAbsVal
runMSSAPHITransferAt(cycleHead) # re-fills _addrToAbsVal:
# for each obj in MR.PointsTo():
# join over operand def-sites
handleICFGNode body # body stmts may write to other nodes

cur = getFullCycleHeadState(cycle) # ObjVars: trace[cycleHead] just refilled
# ValVars: pulled again

next = prev.widening(cur) # widens both _varToAbsVal and _addrToAbsVal
trace[cycleHead] = next

scatter ValVars from trace[cycleHead] back to their def-sites

ObjVars stay in trace[cycleHead] for iter k+1

3.3 Recursion
WTO treats recursion SCCs as cycles, so the same machinery applies. One subtlety: runActualOUTTransferAt at a recursive call's RetICFGNode walks RetIndSVFGEdge → FormalOUT → IndirectSVFGEdge to find callee CHIs, which may include the same call's ActualOUT (a self-loop). First iteration finds the slot empty (just cleared by merge); WTO iterates the SCC and the slot fills in subsequent rounds. fill-empty-only ensures the recursion's skipRecursionWithTop mode (when enabled) writes ⊤ to exactly the slot the reader will consult, and the transfer doesn't subsequently overwrite that ⊤.

3.4 GepObjVar in cycles
gepOverlay participates in cycles trivially: every iteration's stores fold their values into the same global map via join_with. The lattice is bounded so termination is automatic. There is no widening on gepOverlay and none is needed — the worst case is intervals saturating to [-INF, INF], which terminates the WTO loop.

3.5 The widening monotonicity bug worth noting
An earlier draft of pathRefinedAt's cross-iteration commit used meet. Under widening, this trapped overlay entries at iteration 1's tightest narrowing, while the base def-anchor value widened around them. Reads computed meet(widened_base, stale_tight_overlay) = stale_tight_overlay, and the cycle never converged.

Fix: cross-iteration commit uses join. The per-iteration tightening still happens because isCmpBranchFeasible recomputes narrowingDelta each round and the per-pred snapshot folds delta via meet — that part is correct. Only the cross-iteration step needed to climb the lattice with the base value, not against it. Single-line change in mergeStatesFromPredecessors recovered 50/115 failing tests at the time.

Empirical results (289-file benchmark)
Mode ES_Loc_TOTAL ES_Var_TOTAL Tests
Dense 2,320,904 4,200,835 352/352
Semi-Sparse 2,320,832 106,608 352/352
Full-Sparse 42,323 98,622 332/352
ES_Loc_TOTAL (ObjVar storage) drops 98.2% versus Dense. ES_Var_TOTAL (ValVar storage) drops 97.7%.

Dense and Semi-Sparse remain unchanged at 352/352 — none of the new mechanisms fire in those modes.

Out of scope (the 20 remaining failures)
4 × recursive_afterrec: ActualOUT chain through self-recursive SCCs needs more iteration; tractable follow-up.
6 × detector FP/FN under branch refinement: pathRefinedAt overlay needs to extend to ValVar pointers (if (cond) p = NULL; UNSAFE_LOAD(p);).
5 × ExtAPI / scanf / switch / memcpy edge cases: middling effort.
1 × BASIC_array_int_0: Phase D's flow-insensitive trade-off (won't fix without losing the simplicity).
4 × very complex CFG (goto + nested loops + while-true exit): borderline cases.
None indicate a soundness regression.

Files changed
svf/include/AE/Svfexe/AbstractStateManager.h: public API for the three transfers, pathRefinedAt, gepOverlay.
svf/lib/AE/Svfexe/AbstractStateManager.cpp: transfer implementations, sparsity-aware reader, gepOverlay write/read paths.
svf/lib/AE/Svfexe/AbstractInterpretation.cpp: driver hooks for the three transfers, modified mergeStatesFromPredecessors, modified isCmpBranchFeasible signature.
svf/lib/AE/Core/AbstractState.cpp: sparsity gate in joinWith.
svf/lib/AE/Svfexe/SparseAbstractInterpretation.cpp: cycle ValVar pull-and-scatter.
svf/lib/AE/Svfexe/PreAnalysis.cpp: initCycleValVars for the bottom-up cycle ValVar set.
svf/lib/AE/Svfexe/AbsExtAPI.cpp: ObjVar reads in ExtAPI handlers go through the sparsity-aware reader.
No SVFG / VFG / ICFG / MSSA / Andersen header or behavioural changes.