Program analysis using mixed term and set constraints

Abstract. There is a tension in program analysis between precision and eciency. In constraint-based program analysis, at one extreme methods based on unication of equality constraints over terms are very fast but often imprecise. At the other extreme, methods based on the resolution of inclusion constraints over set expressions are quite precise, but are often inecient in practice. We describe a parameterized framework for constraint-based program analyses that allows the analysis designer to embed terms and set expressions within each other. Constraints over these mixed expressions are partially between equality and inclusion, which enables an entire spectrum of program analyses with varying degrees of precision and eciency to be expressed. We also show that there are interesting analyses that take advantage of this mixture. In particular, we report on the design and implementation of an uncaught exception analysis for core ML. Our results show that the analysis approaches the eciency of algorithm W.