Webs and Flow-Directed Well-Typedness Preserving Program Transformations
Benjamin Quiring, David Van Horn, John H. Reppy, Olin Shivers
Abstract
We define webs to be the collections of producers and consumers ( e.g ., functions and calls) in a program that are constrained: in higher-order languages, multiple functions can flow to the same call, all of which must agree on an interface (e.g., calling convention). We argue that webs are fundamentally the unit of transformation : a change to one member requires changes across the entire web. We introduce a web-centric intermediate language that exposes webs as annotations, and describe web-based (that is, flow-directed) transformations guided by these annotations. As they affect all members of a web, these transformations are interprocedural, operating over entire modules. Through the lens of webs we reframe and generalize a collection of transformations from the literature, including dead-parameter elimination, uncurrying, and defunctionalization, as well as describe novel transformations. We contrast this approach with rewriting strategies that rely on inlining and cascading rewrites. Webs are an over-approximation of the semantic function-call relationship produced by control-flow analyses (CFA). This information is inherently independent from the transformations; more precise analyses permit more transformations. A limitation of precise analyses is that the transformations may not maintain well-typedness, as the type system is a less-precise static analysis. Our solution is a simple and lightweight typed-based analysis that causes the flow-directed transformations to preserve well-typedness, making flow-directed, type-preserving transformations easily accessible in many compilers. This analysis builds on unification, distinguishing types that look the same from types that have to be the same. Our experiments show that while our analysis is theoretically less precise, in practice its precision is similar to CFAs.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext a2f0a614-677c-40c7-a0e6-4a58dfecdc7fBuilds on3
- Demanded abstract interpretationBenno Stein, Bor-Yuh Evan Chang, Manu SridharanPLDI 2021 · 19 citations
- Generating Well-Typed Terms That Are Not "Useless"Justin Frank, Benjamin Quiring, Leonidas LampropoulosPOPL 2024 · 9 citations
- Better Defunctionalization through Lambda Set SpecializationWilliam Brandon, Benjamin Driscoll, Frank Dai, Wilson Berkow et al.PLDI 2023 · 7 citations
Related papers
- Improving Indirect-Call Analysis in LLVM with Type and Data-Flow Co-AnalysisDinghao Liu, Shouling Ji, Kangjie Lu, Qinming HeUSENIX Security 2024 · 13 citations
- Exact Recursive Probabilistic ProgrammingDavid Chiang, Colin McDonald, Chung-chieh ShanOOPSLA 2023 · 12 citations
- Defunctionalization with Dependent TypesYulong Huang, Jeremy YallopPLDI 2023 · 4 citations
- Graph IRs for Impure Higher-Order Languages: Making Aggressive Optimizations Affordable with Precise Effect DependenciesOliver Bracevac, Guannan Wei, Songlin Jia, Supun Abeysinghe et al.OOPSLA 2023 · 14 citations
- Unimocg: Modular Call-Graph Algorithms for Consistent Handling of Language FeaturesDominik Helm, Tobias Roth, Sven Keidel, Michael Reif et al.ISSTA 2024
