Semi-Sparse Abstract Interpretation (#1803 rebased on #1804) - #1806

Open

bjjwwang wants to merge 27 commits into

SVF-tools:masterfrom

bjjwwang:semi-sparse2

Commits on Mar 23, 2026

feat: add semi-sparse abstract interpretation mode (-semi-sparse)
bjjwwang
committed
feat(semi-sparse): achieve 70.6% state size reduction via hybrid merge strategy
bjjwwang
committed
chore: remove semi-sparse.md from repo (keep locally)
bjjwwang
committed
refactor: replace orphanVarDefMap with CallICFGNode::getRetICFGNode()

bjjwwang
and
claude
committed
chore: remove state size instrumentation from runOnModule

bjjwwang
and
claude
committed

Commits on Mar 24, 2026

refactor: unify API signatures and decouple AEDetector/AbsExtAPI from AbstractState

bjjwwang
and
claude
committed
refactor: replace as[idx] with getAbstractValue/updateAbstractValue API

bjjwwang
and
claude
committed
refactor: eliminate remaining as[idx] in AbsExtAPI and AEDetector

bjjwwang
and
claude
committed
fix: correct getAbstractValue dispatch and dense/semi-sparse mode handling

bjjwwang
and
claude
committed
fix: restore defensive top initialization for uninitialized operands in Binary/Cmp

bjjwwang
and
claude
committed
fix: semi-sparse getAbstractValue should check current node's state first

bjjwwang
and
claude
committed

Commits on Mar 25, 2026

refactor: remove buildSparseState, lift GEP methods to AbstractInterpretation

bjjwwang
and
claude
committed
fix: resolve semi-sparse segfault in snprintf handler

bjjwwang
and
claude
committed

Commits on Mar 26, 2026

fix: getAbstractValue returns top for absent ValVars instead of bottom

bjjwwang
and
claude
committed
refactor: remove sparsity checks from updateStateOnPhi and mergeStatesFromPredecessors

bjjwwang
and
claude
committed
refactor: remove pullValVarIntoState, simplify pullBranchConditionVars

bjjwwang
and
claude
committed
docs: add detailed comments for AbstractInterpretation public API

bjjwwang
and
claude
committed
chore: remove compatible_dense_semisparse.md from repo

bjjwwang
and
claude
committed
refactor: move semi-sparse merge logic into joinWith, remove joinAddrOnly

bjjwwang
and
claude
committed

Commits on Mar 27, 2026

chore: remove stale joinAddrOnly comment from AbstractState.h

bjjwwang
and
claude
committed
refactor: remove pullBranchConditionVars and pullLoadChainPointerIntoState

bjjwwang
and
claude
committed

Commits on Mar 28, 2026

refactor: clean up AbstractState — remove functions that read ValVars

bjjwwang
and
claude
committed
refactor: extract AbstractStateManager from AbstractInterpretation

bjjwwang
and
claude
committed
refactor: AbsExtAPI and AEDetector use AbstractStateManager directly

bjjwwang
and
claude
committed
refactor: add loadValue/storeValue to AbstractStateManager

bjjwwang
and
claude
committed

Commits on Mar 30, 2026

refactor: remove redundant ICFGNode/AbstractState params; narrow SVFVar to ValVar

bjjwwang
and
claude
committed
fix getAccessOffset
bjjwwang
committed