BANE: A Library for Scalable Constraint-Based Program Analysis

Program analysis is an important aspect of modern program development. Compilers use program analysis to prove the correctness of optimizing program transformations. Static error detection tools use program analysis to alert the programmer to the presence of potential errors. This dissertation focuses on the expressiveness and implementation of constraint-based program analyses, i.e., analyses that are expressed as solutions to a system of constraints. We show that structuring the implementation of program analyses around a library of generic constraint solvers promotes reuse, gives control over precision-efficiency tradeoffs, and enables optimizations that yield orders of magnitude speedups over standard implementations. The first part of the dissertation develops the formalism of mixed constraints which provides a combination of several constraint formalisms with distinct precision-efficiency tradeoffs. We provide a semantics for constraints and constraint resolution algorithms. The second part of the dissertation describes an implementation of mixed constraints and a number of novel techniques to support the practical resolution of large constraint systems. We give empirical results supporting the claims of scalability, reuse, and choice of precision-efficiency tradeoffs provided by the mixed constraint framework.