Efficient Abstract Interpretation via Selective Widening
Abstract interpretation provides a systematic framework for static analysis, where widening operators are crucial for ensuring termination when analyzing programs over infinite-height lattices. Current abstract interpreters apply widening operations and fixpoint detection uniformly across all variables at the identified widening point (e.g., control-flow loop headers), leading to costly computations. Through our empirical study, we observe that infinite ascending chains typically originate from only a subset of variables involved in value-flow cycles, providing opportunities for selective widening and targeted fixpoint detection. This paper introduces an efficient approach to optimize abstract interpretation over non-relational domains through selective widening guided by value-flow analysis. We develop a modular and condensed value-flow graph (MVFG) that enables precise identification of variables requiring widening by detecting value-flow cycles across procedure boundaries. Our MVFG design incorporates efficient shortcut edges that summarize interprocedural value flows, achieving the precision of context-sensitive analysis but with linear complexity. By aligning value-flow cycles with the weak topological ordering (WTO) of the control-flow graph, we identify the minimal set of variables requiring widening operations, applying widening exclusively to variables that participate in value-flow back edges. Our evaluation on large-scale open-source projects shows that our selective widening approach reduces analysis time by up to 41.2% while maintaining identical precision. The method significantly reduces the number of widened variables by up to 99.5%, with greater benefits observed in larger codebases.
Sat 18 OctDisplayed time zone: Perth change
16:00 - 17:30 | AbstractionOOPSLA at Orchid East Chair(s): Steve Blackburn Google and Australian National University | ||
16:00 15mTalk | Abstract Interpretation of Temporal Safety Effects of Higher Order Programs OOPSLA Mihai Nicola Stevens Institute of Technology, Chaitanya Agarwal New York University, Eric Koskinen Stevens Institute of Technology, Thomas Wies New York University | ||
16:15 15mTalk | A Hoare Logic For Symmetry Properties OOPSLA | ||
16:30 15mTalk | Efficient Abstract Interpretation via Selective Widening OOPSLA | ||
16:45 15mTalk | Encode the $\forall\exists$ Relational Hoare Logic into Standard Hoare Logic OOPSLA Shushu Wu Shanghai Jiao Tong University, Xiwei Wu Shanghai Jiao Tong University, Qinxiang Cao Shanghai Jiao Tong University | ||
17:00 15mTalk | Structural Abstraction and Refinement for Probabilistic Programs OOPSLA Guanyan Li University of Oxford, Juanen Li Beijing Normal University, Zhilei Han Tsinghua University, Peixin Wang East China Normal University, Hongfei Fu Shanghai Jiao Tong University, Fei He Tsinghua University | ||
17:15 15mTalk | Work Packets: A New Abstraction for GC Software Engineering, Optimization, and Innovation OOPSLA Wenyu Zhao Australian National University, Stephen M. Blackburn Google; Australian National University, Kathryn S McKinley Google | ||