Thomas Gilray
Abstract
Traditional 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 published that provide perfect call-stack precision in a computable manner: CFA2, PDCFA, and AAC. Unfortunately, implementing CFA2 and PDCFA requires significant engineering effort. Furthermore, all three are computationally expensive. For a monovariant analysis, CFA2 is in O(2^n), PDCFA is in O(n^6), and AAC is in O(n^8). In this paper, we describe a new technique that builds on these but is both straightforward to implement and computationally inexpensive. The crucial insight is an unusual state-dependent allocation strategy for the addresses of continuations. Our technique imposes only a constant-factor overhead on the underlying analysis and costs only O(n^3) in the monovariant case. We present the intuitions behind this development, benchmarks demonstrating its efficacy, and a proof of the precision of this analysis.
- P. Cousot and R. Cousot. Static determination of dynamic properties of programs. In Proceedings of the Second International Symposium on Programming, pages 106–130. Paris, France, 1976.Google Scholar
- P. Cousot and R. Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Proceedings of the 4th ACM SIGACTSIGPLAN Symposium on Principles of Programming Languages, POPL ’77, pages 238–252, New York, NY, USA, Jan. 1977. ACM. doi: 10.1145/512950.512973. Google ScholarDigital Library
- P. Cousot and R. Cousot. Systematic design of program analysis frameworks. In Proceedings of the 6th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, POPL ’79, pages 269–282, New York, NY, USA, Jan. 1979. ACM. doi: 10.1145/567752.567778. Google ScholarDigital Library
- C. Earl, M. Might, and D. Van Horn. Pushdown control-flow analysis of higher-order programs: Precise, polyvariant and polynomial-time. In Scheme Workshop, August 2010.Google Scholar
- C. Earl, I. Sergey, M. Might, and D. Van Horn. Introspective pushdown analysis of higher-order programs. In Proceedings of the 17th ACM SIGPLAN International Conference on Functional Programming, ICFP ’12, pages 177–188, New York, NY, USA, Sept. 2012. Google ScholarDigital Library
- ACM. ISBN 978-1-4503-1054-3. doi: 10.1145/2364527.2364576.Google Scholar
- C. Flanagan, A. Sabry, B. F. Duba, and M. Felleisen. The essence of compiling with continuations. In Proceedings of the ACM SIGPLAN 1993 Conference on Programming Language Design and Implementation, PLDI ’93, pages 237–247, New York, NY, USA, Aug. 1993. Google ScholarDigital Library
- ACM. ISBN 0-89791-598-4. doi: 10.1145/155090.155113.Google Scholar
- J. I. Johnson. AAC complexity analysis discussion. Unpublished correspondence, June 2015.Google Scholar
- J. I. Johnson and D. Van Horn. Abstracting abstract control. In Proceedings of the 10th ACM Symposium on Dynamic Languages, DLS ’14, pages 11–22, New York, NY, USA, Oct. 2014. ACM. ISBN 978-1-4503-3211-8. doi: 10.1145/2661088.2661098. Google ScholarDigital Library
- J. I. Johnson, N. Labich, M. Might, and D. Van Horn. Optimizing abstract abstract machines. In Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, ICFP ’13, pages 443–454, New York, NY, USA, Sept. 2013. ACM. ISBN 978- 1-4503-2326-0. doi: 10.1145/2500365.2500604. Google ScholarDigital Library
- J. Midtgaard. Control-flow analysis of functional programs. ACM Computing Surveys (CSUR), 44(3):10:1–10:33, June 2012. Google ScholarDigital Library
- ISSN 0360-0300. doi: 10.1145/2187671.2187672.Google Scholar
- M. Might. Environment Analysis of Higher-Order Languages. PhD thesis, Georgia Institute of Technology, Atlanta, GA, 2007. Google ScholarDigital Library
- M. Might. Abstract interpreters for free. In R. Cousot and M. Martel, editors, Proceedings of the Static Analysis Symposium, volume 6337 of Lecture Notes in Computer Science, pages 407–421. Springer Berlin Heidelberg, 2010. ISBN 978-3-642-15768-4. doi: 10.1007/978-3- 642-15769-1_25. Google ScholarDigital Library
- M. Might, Y. Smaragdakis, and D. Van Horn. Resolving and exploiting the k-CFA paradox: illuminating functional vs. object-oriented program analysis. In Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’10, pages 305–315, New York, NY, USA, June 2010. ACM. ISBN 978-1- 4503-0019-3. doi: 10.1145/1806596.1806631. Google ScholarDigital Library
- A. Tarski. A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5(2):285–309, 1955.Google ScholarCross Ref
- D. Van Horn and M. Might. Abstracting abstract machines. In Proceedings of the 15th ACM SIGPLAN International Conference on Functional Programming, ICFP ’10, pages 51–62, New York, NY, USA, Sept. 2010. ACM. ISBN 978-1-60558-794-3. doi: 10.1145/1863543.1863553. Google ScholarDigital Library
- D. Vardoulakis and O. Shivers. CFA2: A context-free approach to control-flow analysis. In A. D. Gordon, editor, Proceedings of the European Symposium on Programming, volume 6012 of Lecture Notes in Computer Science, pages 570–589. Springer Berlin Heidelberg, 2010. ISBN 978-3-642-11956-9. doi: 10.1007/978-3-642-11957- 6_30. Google ScholarDigital Library
Index Terms
- Pushdown control-flow analysis for free
Recommendations
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 ...
Allocation characterizes polyvariance: a unified methodology for polyvariant control-flow analysis
ICFP '16The polyvariance of a static analysis is the degree to which it structurally differentiates approximations of program values. Polyvariant techniques come in a number of different flavors that represent alternative heuristics for managing the trade-off ...
Allocation characterizes polyvariance: a unified methodology for polyvariant control-flow analysis
ICFP 2016: Proceedings of the 21st ACM SIGPLAN International Conference on Functional ProgrammingThe polyvariance of a static analysis is the degree to which it structurally differentiates approximations of program values. Polyvariant techniques come in a number of different flavors that represent alternative heuristics for managing the trade-off ...
Comments