Introspective pushdown analysis of higher-order programs

DOI10.1145/2364527.2364576MaRDI QIDQ5168912zbMATH OpenOpenAlexFDO

Authors Christopher Earl, Ilya Sergey, Matthew Might, David van Horn

Publication date 21 July 2014

Published in Proceedings of the 17th ACM SIGPLAN international conference on Functional programming (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1207.1813, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.360.2409

zbMATH Keywords

abstract garbage collectionabstract interpretationabstract machinescfa2higher-order languagesprogram analysispushdown analysispushdown systems

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Abstract: In the static analysis of functional programs, pushdown flow analysis and abstract garbage collection skirt just inside the boundaries of soundness and decidability. Alone, each method reduces analysis times and boosts precision by orders of magnitude. This work illuminates and conquers the theoretical challenges that stand in the way of combining the power of these techniques. The challenge in marrying these techniques is not subtle: computing the reachable control states of a pushdown system relies on limiting access during transition to the top of the stack; abstract garbage collection, on the other hand, needs full access to the entire stack to compute a root set, just as concrete collection does. emph{Introspective} pushdown systems resolve this conflict. Introspective pushdown systems provide enough access to the stack to allow abstract garbage collection, but they remain restricted enough to compute control-state reachability, thereby enabling the sound and precise product of pushdown analysis and abstract garbage collection. Experiments reveal synergistic interplay between the techniques, and the fusion demonstrates "better-than-both-worlds" precision.

Recommendations

• Pushdown flow analysis with abstract garbage collection
• Pushdown control-flow analysis for free
• Pushdown flow analysis of first-class control
• Systematic abstraction of abstract machines
• Exploiting reachability and cardinality in higher-order flow analysis

Cited in

(9)

• Analyzing pushdown systems with stack manipulation
• Pushdown flow analysis with abstract garbage collection
• Exploiting reachability and cardinality in higher-order flow analysis
• The Higher-Order Aggregate Update Problem
• Abstract allocation as a unified approach to polyvariance in control-flow analyses
• Liberate abstract garbage collection from the stack by decomposing the heap
• A posteriori environment analysis with Pushdown Delta CFA
• Improved functional flow and reachability analyses using indexed linear tree grammars
• Program Analysis Using Weighted Pushdown Systems

This page was built for publication: Introspective pushdown analysis of higher-order programs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5168912)