Abstract

Control-Flow Analysis (CFA) is a static technique for understanding the execution of higher-order programs without running the code. CFA aids in identifying bugs, assisting program comprehension, and exposing optimization opportunities. Constructing a CFA typically begins with an idealized evaluator--such as an abstract machine or interpreter--and proceeds by approximating components of evaluation to ensure that: (a) the analysis is sound (representing all possible behaviors), and (b) the analysis is guaranteed to terminate (finitely representable). These constraints necessitate a loss of precision, providing an approximation of the values that flow to program locations rather than exact execution traces. This imprecision causes the analysis to reveal what may happen relative to the chosen abstraction, rather than what must happen in any concrete execution. To extract more detailed information, a more precise abstraction or methodology must be used. A common approach for increasing precision is context-sensitivity, which considers program evaluation under different contexts derived from a finite representation of the evaluation history. Dominant forms include object-allocation or type sensitivity for object-oriented languages and call-site sensitivity for functional languages. In this dissertation, I extend a specific form of call-site sensitivity (based on the last-m stack frames) pioneered by m-CFA to two non-standard language semantics. The first is a demand-driven lambda calculus employing a kind of lazy evaluation, enabling targeting the analysis to specific code regions. The second is a new big-step formalism for effect handlers, a modern form of first-class control. Both semantics required novel adaptations of the m-CFA approach to address their unique challenges. I implemented these analyses in a Scheme-like language for verification and subsequently integrated them into the Koka compiler. The results demonstrate how my novel context-sensitive approaches are able to obtain more precise information in the demand-driven setting, and precisely reason about complex patterns induced by first-class control in the novel formalism for effect handlers. Additionally, the results show that the proposed context-sensitive approaches are more scalable than existing approaches: compared to full-program analysis for the former, and to other direct-style full-program analysis approaches for the latter.

Degree

PhD

College and Department

Computational, Mathematical, and Physical Sciences; Computer Science

Rights

https://lib.byu.edu/about/copyright/