Cited By
View all- Schwarz MSaan SSeidl HErhard JVojdani V(2023)Clustered Relational Thread-Modular Abstract Interpretation with Local TracesProgramming Languages and Systems10.1007/978-3-031-30044-8_2(28-58)Online publication date: 22-Apr-2023
Trace-based control-flow analysis
Pages 482 - 496
Abstract
We define a small-step semantics for the untyped λ-calculus, that traces the β-reductions that occur during evaluation. By abstracting the computation traces, we reconstruct k-CFA using abstract interpretation, and justify constraint-based k-CFA in a semantic way. The abstract interpretation of the trace semantics also paves the way for introducing widening operators in CFA that go beyond existing analyses, that are all based on exploring a finite state space. We define ∇CFA, a widening-based analysis that limits the cycles in call stacks, and can achieve better precision than k-CFA at a similar cost.
References
[1]
Baudouin L Charlier and Pascal Van Hentenryck. 1992. A Universal Top-Down Fixpoint Algorithm. USA. ftp://ftp.cs.brown.edu/pub/techreports/92/cs92-25.pdf
[2]
Patrick Cousot. 1997. Constructive Design of a Hierarchy of Semantics of a Transition System by Abstract Interpretation (Extended Abstract). Electronic Notes in Theoretical Computer Science, 6, 1-2 (1997), apr, 77–102. https://doi.org/10.1016/s1571-0661(05)80168-9
[3]
Patrick Cousot and Radhia Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In Proceedings of the 4superscript th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL ’77). Association for Computing Machinery, New York, NY, USA. 238–252. isbn:9781450373500 https://doi.org/10.1145/512950.512973
[4]
David Darais, Nicholas Labich, Phuc C. Nguyen, and David Van Horn. 2017. Abstracting definitional interpreters (functional pearl). Proc. ACM Program. Lang., 1, ICFP (2017), 12:1–12:25. https://doi.org/10.1145/3110256
[5]
Paulo Emílio de Vilhena, François Pottier, and Jacques-Henri Jourdan. 2020. Spy game: verifying a local generic solver in Iris. Proc. ACM Program. Lang., 4, POPL (2020), 33:1–33:28. https://doi.org/10.1145/3371101
[6]
Christopher Earl, Matthew Might, and David Van Horn. 2010. Pushdown Control-Flow Analysis of Higher-Order Programs. Workshop on Scheme and Functional Programming, abs/1007.4268 (2010), arxiv:1007.4268
[7]
Christopher Earl, Ilya Sergey, Matthew Might, and David Van Horn. 2012. Introspective pushdown analysis of higher-order programs. In ACM SIGPLAN International Conference on Functional Programming, ICFP’12, Copenhagen, Denmark, September 9-15, 2012, Peter Thiemann and Robby Bruce Findler (Eds.). ACM, 177–188. https://doi.org/10.1145/2364527.2364576
[8]
Leandro Facchinetti, Zachary Palmer, and Scott F. Smith. 2019. Higher-order Demand-driven Program Analysis. ACM Trans. Program. Lang. Syst., 41, 3 (2019), 14:1–14:53. https://doi.org/10.1145/3310340
[9]
Kimball Germane and Michael D. Adams. 2020. Liberate Abstract Garbage Collection from the Stack by Decomposing the Heap. In Programming Languages and Systems - 29th European Symposium on Programming, ESOP 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Peter Müller (Ed.) (Lecture Notes in Computer Science, Vol. 12075). Springer, 197–223. https://doi.org/10.1007/978-3-030-44914-8_8
[10]
Thomas Gilray, Michael D. Adams, and Matthew Might. 2016. Allocation characterizes polyvariance: a unified methodology for polyvariant control-flow analysis. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016, Jacques Garrigue, Gabriele Keller, and Eijiro Sumii (Eds.). ACM, 407–420. https://doi.org/10.1145/2951913.2951936
[11]
Thomas Gilray, Steven Lyde, Michael D. Adams, Matthew Might, and David Van Horn. 2016. Pushdown control-flow analysis for free. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, Rastislav Bodík and Rupak Majumdar (Eds.). ACM, 691–704. https://doi.org/10.1145/2837614.2837631
[12]
Maria Handjieva and Stanislav Tzolovski. 1998. Refining Static Analyses by Trace-Based Partitioning Using Control Flow. In Static Analysis, 5th International Symposium, SAS ’98, Pisa, Italy, September 14-16, 1998, Proceedings, Giorgio Levi (Ed.) (Lecture Notes in Computer Science, Vol. 1503). Springer, 200–214. https://doi.org/10.1007/3-540-49727-7_12
[13]
Nevin Heintze. 1994. Set-Based Analysis of ML Programs. ACM SIGPLAN Lisp Pointers, VII, 3 (1994), July, 306–317. https://doi.org/10.1145/182590.182495
[14]
Nevin Heintze and David McAllester. 1997. On the Complexity of Set-Based Analysis. In Proceedings of the Second ACM SIGPLAN International Conference on Functional Programming (ICFP ’ 97). Association for Computing Machinery, New York, NY, USA. 150–163. isbn:0897919181 https://doi.org/10.1145/258948.258963
[15]
David Van Horn and Matthew Might. 2010. Abstracting Abstract Machines. In Proceedings of the 15superscript th ACM SIGPLAN international conference on Functional programming - ICFP ' 10. ACM Press. https://doi.org/10.1145/1863543.1863553
[16]
Suresh Jagannathan and Stephen Weeks. 1995. A Unified Treatment of Flow Analysis in Higher-order Languages. In Proceedings of the 22superscript nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL ' 95. ACM Press. https://doi.org/10.1145/199448.199536
[17]
Suresh Jagannathan and Andrew K. Wright. 1996. Flow-Directed Inlining. In Proceedings of the ACM SIGPLAN’96 Conference on Programming Language Design and Implementation (PLDI), Philadephia, Pennsylvania, USA, May 21-24, 1996, Charles N. Fischer (Ed.). ACM, 193–205. https://doi.org/10.1145/231379.231417
[18]
J. Ian Johnson, Nicholas Labich, Matthew Might, and David Van Horn. 2013. Optimizing abstract abstract machines. In Proceedings of the 18th ACM SIGPLAN international conference on Functional programming - ICFP ' 13. ACM Press. https://doi.org/10.1145/2500365.2500604
[19]
Neil D. Jones. 1981. Flow analysis of lambda expressions. In Automata, Languages and Programming, S. Even and O. Kariv (Eds.). Springer Berlin Heidelberg, 114–128. https://doi.org/10.1007/3-540-10843-2_10
[20]
Neil D. Jones and Alan Mycroft. 1986. Data Flow Analysis of Applicative Programs Using Minimal Function Graphs. In Proceedings of the 13superscript th ACM SIGACT-SIGPLAN symposium on Principles of programming languages - POPL ' 86. ACM Press. https://doi.org/10.1145/512644.512672
[21]
Neil D. Jones and Mads Rosendahl. 1997. Higher-Order Minimal Function Graphs. Journal of Functional and Logic Programming, 1997, 2 (1997), Feb., issn:1080-5230 http://danae.uni-muenster.de/lehre/kuchen/JFLP/articles/ 1997/A97-02/A97-02.html
[22]
Donald E Knuth. 1991. Textbook examples of recursion. Artificial Intelligence and Mathematical Theory of Computation. Papers in Honor of John McCarthy, 207–229. arxiv:cs/9301113
[23]
Xavier Leroy, Damien Doligez, Jacques Garrigue, Didier Rémy, and Jérôme Vouillon. 2017. The Objective Caml System, Documentation and User’s Manual – Release 4.06. http://caml.inria.fr/pub/docs/manual-ocaml-4.06/
[24]
Laurent Mauborgne and Xavier Rival. 2005. Trace Partitioning in Abstract Interpretation Based Static Analyzers. 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, Shmuel Sagiv (Ed.) (Lecture Notes in Computer Science, Vol. 3444). Springer, 5–20. https://doi.org/10.1007/978-3-540-31987-0_2
[25]
Jan Midtgaard. 2012. Control-Flow Analysis of Functional Programs. Comput. Surveys, 44, 3 (2012), June, 1–33. https://doi.org/10.1145/2187671.2187672
[26]
Jan Midtgaard and Thomas P. Jensen. 2008. A Calculational Approach to Control-Flow Analysis by Abstract Interpretation. In Static Analysis, 15th International Symposium, SAS 2008, María Alpuente and Germán Vidal (Eds.). Springer LNCS vol. 5079, 347–362. https://doi.org/10.1007/978-3-540-69166-2_23
[27]
Jan Midtgaard and Thomas P. Jensen. 2009. Control-Flow Analysis of Function Calls and Returns by Abstract Interpretation. In Proceedings of the 14superscript th ACM SIGPLAN international conference on Functional programming - ICFP ' 09. ACM Press. https://doi.org/10.1145/1596550.1596592
[28]
Matthew Might and Olin Shivers. 2006. Improving Flow Analyses via ΓCFA: Abstract Garbage Collection and Counting. In Proceedings of the Eleventh ACM SIGPLAN International Conference on Functional Programming (ICFP ’06). Association for Computing Machinery, New York, NY, USA. 13–25. isbn:1595933093 https://doi.org/10.1145/1159803.1159807
[29]
Matthew Might, Yannis Smaragdakis, and David Van Horn. 2010. Resolving and exploiting the k-CFA paradox: illuminating functional vs. object-oriented program analysis. In Proceedings of the 2010 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2010, Toronto, Ontario, Canada, June 5-10, 2010, Benjamin G. Zorn and Alexander Aiken (Eds.). ACM, 305–315. https://doi.org/10.1145/1806596.1806631
[30]
Benoît Montagu and Thomas P. Jensen. 2020. Stable Relations and Abstract Interpretation of Higher-order Programs. Proc. ACM Program. Lang., 4, ICFP (2020), 119:1–119:30. https://doi.org/10.1145/3409001
[31]
Flemming Nielson and Hanne Riis Nielson. 1997. Infinitary Control Flow Analysis. In Proceedings of the 24superscript th ACM SIGPLAN-SIGACT symposium on Principles of programming languages - POPL ' 97. ACM Press. https://doi.org/10.1145/263699.263745
[32]
Flemming Nielson and Hanne Riis Nielson. 2006. Types from Control Flow Analysis. In Program Analysis and Compilation, Theory and Practice, Essays Dedicated to Reinhard Wilhelm on the Occasion of His 60th Birthday, Thomas W. Reps, Mooly Sagiv, and Jörg Bauer (Eds.) (Lecture Notes in Computer Science, Vol. 4444). Springer, 293–310. https://doi.org/10.1007/978-3-540-71322-7_14
[33]
Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. 1999. Principles of Program Analysis. Springer Berlin Heidelberg. https://doi.org/10.1007/978-3-662-03811-6
[34]
Jens Palsberg. 1995. Closure analysis in constraint form. ACM Transactions on Programming Languages and Systems, 17, 1 (1995), jan, 47–62. https://doi.org/10.1145/200994.201001
[35]
Benjamin C. Pierce. 2002. Types and Programming Languages. MIT Press, Cambridge, Mass. isbn:978-0-262-16209-8
[36]
Xavier Rival and Laurent Mauborgne. 2007. The trace partitioning abstract domain. ACM Trans. Program. Lang. Syst., 29, 5 (2007), 26. https://doi.org/10.1145/1275497.1275501
[37]
Xavier Rival and Kwangkeun Yi. 2020. Introduction to static analysis: an abstract interpretation perspective. The MIT Press, Cambridge, Massachusetts. isbn:9780262043410
[38]
Helmut Seidl and Ralf Vogler. 2018. Three Improvements to the Top-Down Solver. In Proceedings of the 20th International Symposium on Principles and Practice of Declarative Programming, PPDP 2018, Frankfurt am Main, Germany, September 03-05, 2018, David Sabel and Peter Thiemann (Eds.). ACM, 21:1–21:14. https://doi.org/10.1145/3236950.3236967
[39]
Peter Sestoft. 1989. Replacing function parameters by global variables. In Proceedings of the fourth international conference on Functional programming languages and computer architecture - FPCA ' 89. ACM Press, 39–53. https://doi.org/10.1145/99370.99374
[40]
Micha Sharir and Amir Pnueli. 1981. Two Approaches to Interprocedural Data Flow Analysis. In Program Flow Analysis: Theory and Applications, S.S. Muchnick and N.D. Jones (Eds.). Prentice-Hall, Inc., Englewood Cliffs, New Jersey, 189–233.
[41]
Olin Shivers. 1988. Control-Flow Analysis in Scheme. In Proceedings of the ACM SIGPLAN 1988 conference on Programming Language design and Implementation - PLDI ' 88, Richard L. Wexelblat (Ed.). ACM, 164–174. https://doi.org/10.1145/53990.54007
[42]
Olin Shivers. 1991. The Semantics of Scheme Control-Flow Analysis. In Proceedings of the 1991 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation (PEPM ’ 91). Association for Computing Machinery, New York, NY, USA. 190–198. isbn:0897914333 https://doi.org/10.1145/115865.115884
[43]
David Van Horn and Harry G. Mairson. 2008. Deciding kCFA is Complete for EXPTIME. In Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming (ICFP ’08). Association for Computing Machinery, New York, NY, USA. 275–282. isbn:9781595939197 https://doi.org/10.1145/1411204.1411243
[44]
Dimitrios Vardoulakis and Olin Shivers. 2010. CFA2: A Context-Free Approach to Control-Flow Analysis. In Proc. of 19th European Symposium on Programming, ESOP 2010. Springer LNCS vol. 6012, 570–589. https://doi.org/10.1007/978-3-642-11957-6_30
[45]
Dimitrios Vardoulakis and Olin Shivers. 2011. Pushdown flow analysis of first-class control. In Proceeding of the 16th ACM SIGPLAN international conference on Functional Programming, ICFP 2011, Tokyo, Japan, September 19-21, 2011, Manuel M. T. Chakravarty, Zhenjiang Hu, and Olivier Danvy (Eds.). ACM, 69–80. https://doi.org/10.1145/2034773.2034785
[46]
Andrew K. Wright and Suresh Jagannathan. 1998. Polymorphic Splitting: An Effective Polyvariant Flow Analysis. ACM Trans. Program. Lang. Syst., 20, 1 (1998), 166–207. https://doi.org/10.1145/271510.271523
Index Terms
- Trace-based control-flow analysis
Recommendations
Control-flow analysis of function calls and returns by abstract interpretation
ICFP '09We derive a control-flow analysis that approximates the interprocedural control-flow of both function calls and returns in the presence of first-class functions and tail-call optimization. In addition to an abstract environment, our analysis computes ...
Pushdown control-flow analysis for free
POPL '16Traditional control-flow analysis (CFA) for higher-order languages introduces spurious connections between callers and callees, and different invocations of a function may pollute each other's return flows. Recently, three distinct approaches have been ...
Pushdown control-flow analysis for free
POPL '16: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming LanguagesTraditional control-flow analysis (CFA) for higher-order languages introduces spurious connections between callers and callees, and different invocations of a function may pollute each other's return flows. Recently, three distinct approaches have been ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
June 2021
1341 pages
Copyright © 2021 ACM.
Publication rights licensed to ACM. ACM acknowledges that this contribution was authored or co-authored by an employee, contractor or affiliate of a national government. As such, the Government retains a nonexclusive, royalty-free right to publish or reproduce this article, or to allow others to do so, for Government purposes only.
Sponsors
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 18 June 2021
Check for updates
Badges
Author Tags
Qualifiers
- Research-article
Conference
PLDI '21
Sponsor:
PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation
June 20 - 25, 2021
Virtual, Canada
Acceptance Rates
Overall Acceptance Rate 406 of 2,067 submissions, 20%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations1Total Citations
- 371Total Downloads
- Downloads (Last 12 months)61
- Downloads (Last 6 weeks)12
Reflects downloads up to 21 Dec 2024
Other Metrics
Citations
Cited By
View all- Schwarz MSaan SSeidl HErhard JVojdani V(2023)Clustered Relational Thread-Modular Abstract Interpretation with Local TracesProgramming Languages and Systems10.1007/978-3-031-30044-8_2(28-58)Online publication date: 22-Apr-2023
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in