Document Open Access Logo

Taming and Dissecting Recursions Through Interprocedural Weak Topological Ordering

Authors Jiawei Yang , Xiao Cheng , Bor-Yuh Evan Chang , Xiapu Luo , Yulei Sui

PDF

File

Thumbnail PDF
PDF
LIPIcs.ECOOP.2025.34.pdf
  • Filesize: 6.34 MB
  • 31 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Program analysis
Keywords
  • Abstract interpretation
  • recursion
  • weak topological ordering

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Abstract

Abstract interpretation provides a foundational framework for approximating program semantics by interpreting code through abstract domains using semantic 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 not scalable 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.

Cite As Get BibTex

Jiawei Yang, Xiao Cheng, Bor-Yuh Evan Chang, Xiapu Luo, and Yulei Sui. Taming and Dissecting Recursions Through Interprocedural Weak Topological Ordering. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 34:1-34:31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.ECOOP.2025.34

Author Details

Jiawei Yang
  • The Hong Kong Polytechnic University, Hong Kong
Xiao Cheng
  • University of New South Wales, Sydney, Australia
Bor-Yuh Evan Chang
  • University of Colorado Boulder, Boulder, CO, USA
  • Amazon, Boulder, CO, USA
Xiapu Luo
  • The Hong Kong Polytechnic University, Hong Kong
Yulei Sui
  • University of New South Wales, Sydney, Australia

Funding

This research is supported by Australian Research Council Grants DP250101396 and FT220100391.

Supplementary Materials

References

  1. Darknet: Open source neural networks in CDarknet: Open source neural networks in C. https://github.com/pjreddie/darknet, 2023.
  2. MP4v2: A C/C++ library to create, modify and read MP4 filesMP4v2: A C/C++ library to create, modify and read MP4 files. https://github.com/enzo1982/mp4v2/, 2023.
  3. RIOT: The friendly OS for IoTRIOT: The friendly OS for IoT. https://github.com/RIOT-OS/RIOT, 2023.
  4. YAJL: A fast streaming JSON parsing library in CYAJL: A fast streaming JSON parsing library in C. https://github.com/lloyd/yajl, 2023.
  5. Tmux: Tmux source code. https://github.com/tmux/tmux, 2023.
  6. A buffer overflow patch in libplist. https://github.com/libimobiledevice/libplist/commit/4765d9a60ca4248a8f89289271ac69cbffcc29bc, 2024.
  7. 8cc: C compiler8cc: C compiler. https://github.com/rui314/8cc, 2024.
  8. libplist: A small portable C library to handle Apple Property List files in binary, XML, JSON, or OpenStep format.libplist: A small portable C library to handle Apple Property List files in binary, XML, JSON, or OpenStep format. https://github.com/libimobiledevice/libplist, 2024.
  9. Teeworlds: A retro multiplayer shooter. https://teeworlds.com/, 2024.
  10. Gianluca Amato and Francesca Scozzari. Localizing widening and narrowing. In International Static Analysis Symposium, pages 25-42. Springer, 2013. URL: https://doi.org/10.1007/978-3-642-38856-9_4.
  11. Gianluca Amato, Francesca Scozzari, Helmut Seidl, Kalmer Apinis, and Vesal Vojdani. Efficiently intertwining widening and narrowing. Science of Computer Programming, 120:1-24, 2016. URL: https://doi.org/10.1016/j.scico.2015.12.005.
  12. George Balatsouras and Yannis Smaragdakis. Structure-sensitive points-to analysis for C and C++Structure-sensitive points-to analysis for C and C++. In SAS '16, 2016. URL: https://doi.org/10.1007/978-3-662-53413-7_5.
  13. François Bourdoncle. Efficient chaotic iteration strategies with widenings. In Formal Methods in Programming and Their Applications: International Conference Academgorodok, Novosibirsk, Russia June 28-July 2, 1993 Proceedings, pages 128-141. Springer, 2005. URL: https://doi.org/10.1007/BFb0039704.
  14. Katharina Brandl, Sebastian Erdweg, Sven Keidel, and Nils Hansen. Modular abstract definitional interpreters for webassembly. In 37th European Conference on Object-Oriented Programming (ECOOP 2023), pages 5-1. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2023. Google Scholar
  15. Guillaume Brat, Jorge A Navas, Nija Shi, and Arnaud Venet. IKOS: A framework for static analysis based on abstract interpretationIKOS: A framework for static analysis based on abstract interpretation. In Software Engineering and Formal Methods: 12th International Conference, SEFM 2014, Grenoble, France, September 1-5, 2014. Proceedings 12, pages 271-277. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-10431-7_20.
  16. Cristian Cadar, Daniel Dunbar, and Dawson Engler. KLEE: Unassisted and automatic generation of high-coverage tests for complex systems programsKLEE: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, OSDI'08, pages 209-224. USENIX Association, 2008. URL: http://www.usenix.org/events/osdi08/tech/full_papers/cadar/cadar.pdf.
  17. Liqian Chen, Antoine Miné, Ji Wang, and Patrick Cousot. Interval polyhedra: An abstract domain to infer interval linear relationships. In International Static Analysis Symposium, pages 309-325. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03237-0_21.
  18. Xiao Cheng, Jiawei Wang, and Yulei Sui. Precise sparse abstract execution via cross-domain interaction. In 46th International Conference on Software Engineering, ICSE '24. ACM/IEEE, 2024. URL: https://doi.org/10.1145/3597503.3639220.
  19. Clam. Clam: LLVM front-end for CrabClam: LLVM front-end for Crab, 2024. URL: https://github.com/seahorn/clam.
  20. Patrick Cousot. Asynchronous iterative methods for solving a fixpoint system of monotone equations. Technical report, Research Report IMAG-RR-88, Université Scientifique et Médicale de Grenoble, 1977. Google Scholar
  21. Patrick Cousot. Méthodes itératives de construction et d'approximation de points fixes d'opérateurs monotones sur un treillis, analyse sémantique des programmes. PhD thesis, Institut National Polytechnique de Grenoble-INPG; Université Joseph-Fourier …, 1978. URL: https://tel.archives-ouvertes.fr/tel-00288657.
  22. Patrick Cousot. Semantic foundations of program analysis. In Program flow analysis: theory and applications, pages 303-342. Prentice Hall, 1981. Google Scholar
  23. Patrick Cousot. Abstracting induction by extrapolation and interpolation. In Deepak D'Souza, Akash Lal, and Kim Guldstrand Larsen, editors, Verification, Model Checking, and Abstract Interpretation, pages 19-42, Berlin, Heidelberg, 2015. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-662-46081-8_2.
  24. Patrick Cousot and Radhia Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pages 238-252, 1977. URL: https://doi.org/10.1145/512950.512973.
  25. Patrick Cousot and Radhia Cousot. Abstract interpretation frameworks. Journal of logic and computation, 2(4):511-547, 1992. URL: https://doi.org/10.1093/logcom/2.4.511.
  26. Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, David Monniaux, and Xavier Rival. The Astrée analyzerThe Astrée analyzer. In Programming Languages and Systems: 14th European Symposium on Programming, ESOP 2005, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2005, Edinburgh, UK, April 4-8, 2005. Proceedings 14, pages 21-30. Springer, 2005. URL: https://doi.org/10.1007/978-3-540-31987-0_3.
  27. Patrick Cousot, Roberto Giacobazzi, and Francesco Ranzato. A²I: Abstract² InterpretationA²I: Abstract² Interpretation. Proc. ACM Program. Lang., 3(POPL), January 2019. URL: https://doi.org/10.1145/3290355.
  28. CWE-121: Stack-based buffer overflowCWE-121: Stack-based buffer overflow. https://cwe.mitre.org/data/definitions/121.html, 2024.
  29. CWE-122: Heap-based buffer overflowCWE-122: Heap-based buffer overflow. https://cwe.mitre.org/data/definitions/122.html, 2024.
  30. CWE-126: buffer over-readCWE-126: buffer over-read. https://cwe.mitre.org/data/definitions/126.html, 2024.
  31. Manuvir Das, Sorin Lerner, and Mark Seigle. ESP: Path-sensitive program verification in polynomial timeESP: Path-sensitive program verification in polynomial time. In Proceedings of the 2002 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), Berlin, Germany, June 17-19, 2002, PLDI '02, pages 57-68, New York, NY, USA, 2002. Association for Computing Machinery. URL: https://doi.org/10.1145/512529.512538.
  32. Matt Elder. Bourdoncle components, 2010. Google Scholar
  33. Denis Gopan and Thomas Reps. Lookahead widening. In Thomas Ball and Robert B. Jones, editors, Computer Aided Verification, pages 452-466, Berlin, Heidelberg, 2006. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/11817963_41.
  34. Arie Gurfinkel and Jorge A. Navas. Abstract interpretation of LLVM with a region-based memory modelAbstract interpretation of LLVM with a region-based memory model. In Software Verification: 13th International Conference, VSTTE 2021, New Haven, CT, USA, October 18–19, 2021, and 14th International Workshop, NSV 2021, Los Angeles, CA, USA, July 18–19, 2021, Revised Selected Papers, pages 122-144, Berlin, Heidelberg, 2021. Springer-Verlag. URL: https://doi.org/10.1007/978-3-030-95561-8_8.
  35. Nicolas Halbwachs and Julien Henry. When the decreasing sequence fails. In Antoine Miné and David Schmidt, editors, Static Analysis, pages 198-213, Berlin, Heidelberg, 2012. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/978-3-642-33125-1_15.
  36. Ben Hardekopf and Calvin Lin. Flow-sensitive pointer analysis for millions of lines of code. In International Symposium on Code Generation and Optimization (CGO 2011), pages 289-298. IEEE, 2011. URL: https://doi.org/10.1109/CGO.2011.5764696.
  37. Daniel Kästner, Stephan Wilhelm, Stefana Nenova, Patrick Cousot, Radhia Cousot, Jérôme Feret, Laurent Mauborgne, Antoine Miné, Xavier Rival, et al. Astrée: Proving the absence of runtime errors. Proc. of Embedded Real Time Software and Systems (ERTS2 2010), 9, 2010. Google Scholar
  38. Sven Keidel, Sebastian Erdweg, and Tobias Hombücher. Combinator-based fixpoint algorithms for big-step abstract interpreters. Proceedings of the ACM on Programming Languages, 7(ICFP):955-981, 2023. URL: https://doi.org/10.1145/3607863.
  39. Sol Kim, Kihong Heo, Hakjoo Oh, and Kwangkeun Yi. Widening with thresholds via binary search. Software: Practice and Experience, 46(10):1317-1328, 2016. URL: https://doi.org/10.1002/spe.2381.
  40. Sung Kook Kim, Arnaud J. Venet, and Aditya V. Thakur. Deterministic parallel fixpoint computation. Proc. ACM Program. Lang., 4(POPL), December 2019. URL: https://doi.org/10.1145/3371082.
  41. Chris Lattner and Vikram Adve. LLVM: A compilation framework for lifelong program analysis & transformationLLVM: A compilation framework for lifelong program analysis & transformation. In International symposium on code generation and optimization, 2004. CGO 2004., pages 75-86. IEEE, 2004. URL: https://doi.org/10.1109/CGO.2004.1281665.
  42. Jacob Laurel, Rem Yang, Gagandeep Singh, and Sasa Misailovic. A dual number abstraction for static analysis of Clarke JacobiansA dual number abstraction for static analysis of Clarke Jacobians. Proc. ACM Program. Lang., 6(POPL), January 2022. URL: https://doi.org/10.1145/3498718.
  43. Zohar Manna. Mathematical theory of computation. Dover Publications, Inc., 2003. Google Scholar
  44. David Monniaux. The parallel implementation of the Astrée static analyzerThe parallel implementation of the Astrée static analyzer. In Kwangkeun Yi, editor, Programming Languages and Systems, pages 86-96, Berlin, Heidelberg, 2005. Springer Berlin Heidelberg. URL: https://doi.org/10.1007/11575467_7.
  45. Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solverZ3: An efficient SMT solver. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 337-340. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-78800-3_24.
  46. NIST datasetsNIST datasets. https://samate.nist.gov/SARD/test-suites/116, 2023.
  47. Hakjoo Oh, Kihong Heo, Wonchan Lee, Woosuk Lee, and Kwangkeun Yi. Design and implementation of sparse global analyses for C-like languages. In Proceedings of the 33rd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '12, pages 229-238, New York, NY, USA, 2012. Association for Computing Machinery. URL: https://doi.org/10.1145/2254064.2254092.
  48. Hakjoo Oh, Kihong Heo, Wonchan Lee, Woosuk Lee, and Kwangkeun Yi. The Sparrow static analyzer, 2012. URL: https://opam.ocaml.org/packages/sparrow/.
  49. Hakjoo Oh and Kwangkeun Yi. An algorithmic mitigation of large spurious interprocedural cycles in static analysis. Software: Practice and Experience, 40(8):585-603, 2010. URL: https://doi.org/10.1002/spe.969.
  50. Komal Pathade and Uday P. Khedker. Computing partially path-sensitive MFP solutions in data flow analysesComputing partially path-sensitive MFP solutions in data flow analyses. In Proceedings of the 27th International Conference on Compiler Construction, CC 2018, pages 37-47, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3178372.3179497.
  51. Komal Pathade and Uday P. Khedker. Path sensitive MFP solutions in presence of intersecting infeasible control flow path segmentsPath sensitive MFP solutions in presence of intersecting infeasible control flow path segments. In Proceedings of the 28th International Conference on Compiler Construction, CC 2019, pages 159-169, New York, NY, USA, 2019. Association for Computing Machinery. URL: https://doi.org/10.1145/3302516.3307349.
  52. D.J. Pearce, P.H.J. Kelly, and C. Hankin. Efficient field-sensitive pointer analysis of CEfficient field-sensitive pointer analysis of C. ACM TOPLAS, 30(1):4-es, 2007. URL: https://doi.org/10.1145/1290520.1290524.
  53. Property list. https://en.wikipedia.org/wiki/Property_list, 2024.
  54. Xavier Rival and Bor-Yuh Evan Chang. Calling context abstraction with shapes. SIGPLAN Not., 46(1):173-186, January 2011. URL: https://doi.org/10.1145/1925844.1926406.
  55. Qingkai Shi, Xiao Xiao, Rongxin Wu, Jinguo Zhou, Gang Fan, and Charles Zhang. Pinpoint: Fast and precise sparse value flow analysis for million lines of code. In Proceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 693-706, 2018. URL: https://doi.org/10.1145/3192366.3192418.
  56. Qingkai Shi, Peisen Yao, Rongxin Wu, and Charles Zhang. Path-sensitive sparse analysis without path conditions. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, PLDI 2021, pages 930-943, New York, NY, USA, 2021. Association for Computing Machinery. URL: https://doi.org/10.1145/3453483.3454086.
  57. Johannes Späth, Karim Ali, and Eric Bodden. Context-, flow-, and field-sensitive data-flow analysis using synchronized pushdown systems. Proceedings of the ACM on Programming Languages, 3(POPL):1-29, 2019. URL: https://doi.org/10.1145/3290361.
  58. Benno Stein, Bor-Yuh Evan Chang, and Manu Sridharan. Interactive abstract interpretation with demanded summarization. ACM Transactions on Programming Languages and Systems, 46(1):1-40, 2024. URL: https://doi.org/10.1145/3648441.
  59. Yulei Sui, Ding Ye, and Jingling Xue. Static memory leak detection using full-sparse value-flow analysis. In Proceedings of the 2012 International Symposium on Software Testing and Analysis, ISSTA '12, pages 254-264. ACM, 2012. URL: https://doi.org/10.1145/2338965.2336784.
  60. Yulei Sui, Ding Ye, and Jingling Xue. Detecting memory leaks statically with full-sparse value-flow analysis. IEEE Trans. Software Eng (TSE '14)., 40(2):107-122, 2014. URL: https://doi.org/10.1109/TSE.2014.2302311.
  61. Robert Tarjan. Depth-first search and linear graph algorithms. SIAM journal on computing, 1(2):146-160, 1972. URL: https://doi.org/10.1137/0201010.
  62. Alfred Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5(2):285-309, 1955. Google Scholar
  63. Oskar Haarklou Veileborg, Georgian-Vlad Saioc, and Anders Møller. Detecting blocking errors in go programs using localized abstract interpretation. In Proceedings of the 37th IEEE/ACM International Conference on Automated Software Engineering, ASE '22, New York, NY, USA, 2023. Association for Computing Machinery. URL: https://doi.org/10.1145/3551349.3561154.
  64. Arnaud Venet and Guillaume Brat. Precise and efficient static array bound checking for large embedded C programsPrecise and efficient static array bound checking for large embedded C programs. In Proceedings of the ACM SIGPLAN 2004 Conference on Programming Language Design and Implementation, PLDI '04, pages 231-242, New York, NY, USA, 2004. Association for Computing Machinery. URL: https://doi.org/10.1145/996841.996869.
  65. Cathrin Weiss, Cindy Rubio-González, and Ben Liblit. Database-backed program analysis for scalable error propagation. In 2015 IEEE/ACM 37th IEEE International Conference on Software Engineering, volume 1, pages 586-597, 2015. URL: https://doi.org/10.1109/ICSE.2015.75.
  66. Peisen Yao, Qingkai Shi, Heqing Huang, and Charles Zhang. Program analysis via efficient symbolic abstraction. Proc. ACM Program. Lang., 5(OOPSLA), October 2021. URL: https://doi.org/10.1145/3485495.
  67. Zhiqiang Zuo, John Thorpe, Yifei Wang, Qiuhong Pan, Shenming Lu, Kai Wang, Guoqing Harry Xu, Linzhang Wang, and Xuandong Li. Grapple: A graph system for static finite-state property checking of large-scale systems code. In Proceedings of the Fourteenth EuroSys Conference 2019, Dresden, Germany, March 25-28, 2019, EuroSys '19. ACM, 2019. URL: https://doi.org/10.1145/3302424.3303972.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2025 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact