Newly-Single and Loving It: Improving Higher-Order Must-Alias Analysis with Heap Fragments
Theories of higher-order must-alias analysis, often under the guise of environment analysis, provide deep behavioral insight. But these theories—in particular those that are most insightful otherwise—can reason about recursion only in limited cases. This weakness is not inherent to the theories but to the frameworks in which they're defined: machine models which thread the heap through evaluation. Since these frameworks allocate each abstract resource in the heap, the constituent theories of environment analysis conflate co-live resources identified in the abstract, such as recursively-created bindings. We present heap fragments as a general technique to allow these theories to reason about recursion in a general and robust way. We instantiate abstract counting in a heap-fragment framework and compare its performance to a precursor entire-heap framework. We also sketch an approach to realizing binding invariants, a more powerful environment analysis, in the heap-fragment framework.