Taming and Dissecting Recursions through Interprocedural Weak Topological Ordering
Abstract interpretation provides a foundational framework for approximating program semantics by interpreting code through abstract domains using monotonic functions over ordered sets along a program’s control flow graph (CFG). To facilitate fixpoint computation in abstract interpretation, weak topological ordering (WTO) is an effective strategy for handling loops, as it identifies strategic control points in the CFG where widening and narrowing operations should be applied. However, existing abstract interpreters still face challenges when extending WTO computation in the presence of recursive programs. Computing a precise whole-program WTO requires full context-sensitive analysis which is unscalable for large programs, while context-insensitive analysis introduces spurious cycles that compromise precision. Current approaches either ignore recursion (resulting in unsoundness) or rely on conservative approximations, sacrificing precision by adopting the greatest elements of abstract domains and applying widening at function boundaries without subsequent narrowing refinements. These can lead to undesired results for downstream tasks, such as bug detection.
To address the above limitations, we present RecTopo a new technique to boost the efficiency of precise abstract interpretation in the presence of recursive programs through interprocedural weak topological ordering (IWTO). Rather than pursuing an expensive whole-program WTO analysis, RecTopo employs an on-demand approach that strategically decomposes programs at recursion boundaries and constructs targeted IWTOs for each recursive component. RecTopo dissects and analyzes (nested) recursions through interleaved widening and narrowing operations. This approach enables precise control over interpretation ordering within recursive structures while eliminating spurious recursions through systematic correlation of control flow and call graphs.
We implemented RecTopo and evaluated its effectiveness using an assertion-based checking client focused on buffer overflow detection, comparing it against three popular open-source abstract interpreters (IKOS, Clam, CSA). The experiments on 8312 programs from the NIST dataset demonstrate that, on average, RecTopo is 31.99% more precise and achieves a 17.49% higher recall rate compared to three other tools. Moreover, RecTopo exhibits an average precision improvement of 46.51% and a higher recall rate of 32.98% compared to our baselines across ten large open-source projects. Further ablation studies reveal that IWTO reduces spurious widening operations compared to whole-program WTO, resulting in a 12.83% reduction in analysis time.
Mon 30 JunDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
11:00 - 12:45 | Formal Methods, Logics, and Static Analysis FrameworksTechnical Papers at Auditorium M003 Chair(s): Marco Carbone IT University of Copenhagen | ||
11:00 21mTalk | Compositional Static Value Analysis for Higher-Order Numerical Programs Technical Papers Milla Valnet Sorbonne Université, Raphaël Monat Inria and University of Lille, Antoine Miné Sorbonne Université | ||
11:21 21mTalk | Lightweight Diagramming for Formal Methods: A Grounded Language Design Technical Papers Siddhartha Prasad Brown University, Ben Greenman University of Utah, Tim Nelson Brown University, Shriram Krishnamurthi Brown University | ||
11:42 21mTalk | Taming and Dissecting Recursions through Interprocedural Weak Topological Ordering Technical Papers Jiawei Yang , Xiao Cheng Macquarie University, Bor-Yuh Evan Chang University of Colorado Boulder & Amazon, Xiapu Luo Hong Kong Polytechnic University, Yulei Sui University of New South Wales | ||
12:03 21mTalk | The Algebra of Patterns Technical Papers | ||
12:24 21mTalk | A theory of (linear-time) timed monitors Technical Papers Mouloud Amara IRIF, Université Paris Cité, Giovanni Bernardi IRIF, Université Paris Cité, Mohammed Aristide Foughali Université Paris Cité / IRIF, Adrian Francalanza University of Malta | ||