Gradual Program Analysis for Null Pointers

TL;DR

This paper introduces a gradual null-pointer analysis that combines static and dynamic checks to reduce false positives in program analysis, balancing soundness and programmer effort.

Contribution

It adapts gradual typing to abstract interpretation, formalizes a new gradual null-pointer analysis, and demonstrates its effectiveness within the Infer framework.

Findings

Reduces false positives compared to existing null-pointer checkers.

Balances static analysis and dynamic checks for soundness.

Provides a formal foundation for gradual analysis in various domains.

Abstract

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.