  Static analysis tools typically address the problem of excessive false
positives by requiring programmers to explicitly annotate their code. However,
when faced with incomplete annotations, many analysis tools are either too
conservative, yielding false positives, or too optimistic, resulting in unsound
analysis results. In order to flexibly and soundly deal with
partially-annotated programs, we propose to build upon and adapt the gradual
typing approach to abstract-interpretation-based program analyses.
Specifically, we focus on null-pointer analysis and demonstrate that a gradual
null-pointer analysis hits a sweet spot, by gracefully applying static analysis
where possible and relying on dynamic checks where necessary for soundness. In
addition to formalizing a gradual null-pointer analysis for a core imperative
language, we build a prototype using the Infer static analysis framework, and
present preliminary evidence that the gradual null-pointer analysis reduces
false positives compared to two existing null-pointer checkers for Infer.
Further, we discuss ways in which the gradualization approach used to derive
the gradual analysis from its static counterpart can be extended to support
more domains. This work thus provides a basis for future analysis tools that
can smoothly navigate the tradeoff between human effort and run-time overhead
to reduce the number of reported false positives.
