SPLASH: U: Gradual Program Analysis

Annotations are a common and useful way to make static analysis tools more usable, but there is no standard way to analyze programs that have only partial annotations. We give a formal framework that transforms arbitrary static analyses assuming complete annotations into gradual analyses accepting partial annotations. Our approach is based on gradual typing, and thus combines static and dynamic analysis to give soundness guarantees via runtime checks. We satisfy a preestablished property called the gradual guarantee, ensuring that our system reacts predictably as the programmer adds annotations one-by-one. We implement a speci c instance of our general framework as a static null-pointer checker in Facebook Infer, and nd in a preliminary empirical investigation that our framework gives fewer statically-reported false positives than Infer’s existing checkers.