Understanding program behaviors requires reasoning about control flow. Functional programs complicate this reasoning since call targets are computed in general. Control-flow analysis (CFA) can effectively reason about control flow (and much more) but is costly. Demand-driven CFA is less expensive but less versatile, and it is difficult to make it do what classical CFA does. This is unfortunate because many fundamental optimizations rely on control flow reasoning. In this paper, we present Demand-on-Demand Control-Flow Analysis (DoDCFA), a hybrid exhaustive--demand-driven CFA that recovers some of the versatility/applicability of classical CFA while improving on the speed of Demand CFA. The result is an analysis that can inexpensively and effectively analyze control flow and environment behavior sufficient to justify inlining.

Effect handlers enable powerful control flow patterns by capturing and resuming continuations, but no control flow analysis exists for programs using them. Applying existing approaches for other delimited control operators would either lose precision through CPS translation or be computationally intractable. We present HMCFA, the first practical control flow analysis for effect handlers based on big-step semantics. Our key technical contributions are: (1) a big-step semantics for effect handlers that allocates denotables and continuations in an explicit store to avoid unbounded syntactic growth, enabling systematic abstraction in the style of Abstracting Definitional Interpreters (ADI); we prove this semantics equivalent to Bauer and Pretnar's substitution-based big-step semantics. (2) A two-component timestamp that tracks both the current call context and the context in which each handler was installed, so that when an operation is dispatched to a handler, its analysis reflects the invocation context that installed it. We prove our concrete semantics equivalent to Bauer and Pretnar's and establish soundness of our abstraction via address freshness. An evaluation on Koka benchmarks shows that our address space has good precision even without context sensitivity, but that our timestamp can close most of the remaining gap in precision while still being tractable on our benchmark suite. An evaluation on Koka benchmarks shows that our address space has good precision even without context sensitivity, but that our timestamp can close most of the remaining gap in precision while still being tractable on our benchmark suite.

Abstract By decoupling and decomposing control flows, demand control-flow analysis (CFA) resolves only the flow segments determined necessary to produce a specified control-flow fact. It therefore presents a more flexible interface and pricing model than typical CFA, making many useful applications practical. At present, the only realization of demand CFA is the context-insensitive Demand 0CFA. Typical mechanisms for adding context sensitivity are not compatible with the demand setting because the analyzer is dispatched at arbitrary program points in indeterminate contexts. We overcome this challenge by identifying a context suitable for a demand analysis and designing a representation thereof that allows it to model incomplete knowledge of the context. On top of this design, we construct Demand m-CFA, a context-sensitive demand CFA hierarchy. With the attractive pricing model of demand analysis and the precision offered by context sensitivity, we show that Demand m-CFA can replace its exhaustive counterpart in compiler backends and integrate into interactive tools such as language servers.

Over the last 15 years, several popular systematic abstraction frameworks have emerged—frameworks that allow a static analysis to be derived by systematically transforming a concrete semantics. These frameworks guarantee computability of the resulting artifact by the application of an a priori abstraction which induces a particular finitization in the execution space. While effective, this abstraction occurs without regard for program structure, subjecting each program point to the same fixed degree of context sensitivity. In this paper, we present CGADI, an enhancement to systematic abstraction frameworks based on definitional interpreters which defers abstraction until a parameterized safety property signals that it should be applied. We then examine this enhanced framework instantiated with two such safety properties: a simple reentrancy property which detects non-recursive portions of program execution, and a size change property which detects evaluation paths destined to converge by virtue of appropriately decreasing values along them. The result is that CGADI can operate in the fully-precise concrete space for portions of execution without forfeiting computability. Our evaluation demonstrates that CGADI is able to produce a higher number of precise results than a corresponding CFA at relatively low cost and that, with no special treatment, CGADI can handle many programming patterns targeted by specific analysis techniques.

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.

Abstract Abstract garbage collection and the use of pushdown systems each enhance the precision of control-flow analysis (CFA). However, their respective needs conflict: abstract garbage collection requires the stack but pushdown systems obscure it. Though several existing techniques address this conflict, none take full advantage of the underlying interplay. In this paper, we dissolve this conflict with a technique which exploits the precision of pushdown systems to decompose the heap across the continuation.This technique liberates abstract garbage collection from the stack, increasing its effectiveness and the compositionality of its host analysis. We generalize our approach to apply compositional treatment to abstract timestamps which induces the context abstraction of m-CFA, an abstraction more precise than k-CFA’s for many common programming patterns.

Flow-driven higher-order inlining is blocked by free variables, yet current theories of environment analysis cannot reliably cope with multiply-bound variables. One of these, ΔCFA, is a promising theory based on stack change but is undermined by its finite-state model of the stack. We present Pushdown ΔCFA which takes a ΔCFA-approach to pushdown models of control flow and can cope with multiply-bound variables, even in the face of recursion.

Abstract Okasaki introduced the canonical formulation of functional red-black trees when he gave a concise, elegant method of persistent element insertion. Persistent element deletion, on the other hand, has not enjoyed the same treatment. For this reason, many functional implementations simply omit persistent deletion. Those that include deletion typically take one of two approaches. The more-common approach is a superficial translation of the standard imperative algorithm. The resulting algorithm has functional airs but remains clumsy and verbose, characteristic of its imperative heritage. (Indeed, even the term insertion is a holdover from imperative origins, but is now established in functional contexts. Accordingly, we use the term deletion which has the same connotation.) The less-common approach leverages the features of advanced type systems, which obscures the essence of the algorithm. Nevertheless, foreign-language implementors reference such implementations and, apparently unable to tease apart the algorithm and its type specification, transliterate the entirety unnecessarily. Our goal is to provide for persistent deletion what Okasaki did for insertion: a succinct, comprehensible method that will liberate implementors. We conceptually simplify deletion by temporarily introducing a “double-black” color into Okasaki's tree type. This third color, with its natural interpretation, significantly simplifies the preservation of invariants during deletion.