You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Add sparse abstract interpretation with def-use driven state propagation
Introduces sparse mode (-sparse flag) for Abstract Interpretation that
propagates only needed variable states at each ICFG node, instead of
copying full abstract states from predecessors.
Key components:
- SparseDefUse: maps address-taken ObjVars to their StoreStmt def sites
- getValVars/getObjVars/getSVFVars: collect variables needed at each node
- getAbstractValue(ValVar/ObjVar/SVFVar): fetch values from SSA def sites
- getAbstractState(vector<ValVar*/ObjVar*/SVFVar*>): build sparse states
- sparseStatePropagate: orchestrates sparse fetch before node handling
- Widen set: PreAnalysis computes variables defined in each loop body,
ensuring all loop-modified variables participate in widening/narrowing
- Fix IntervalValue operator<< signed overflow (1<<31 in 32-bit int)
Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>
0 commit comments