License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.ECOOP.2021.3
URN: urn:nbn:de:0030-drops-140469
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14046/
Estep, Sam ;
Wise, Jenna ;
Aldrich, Jonathan ;
Tanter, Éric ;
Bader, Johannes ;
Sunshine, Joshua
Gradual Program Analysis for Null Pointers
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.
BibTeX - Entry
@InProceedings{estep_et_al:LIPIcs.ECOOP.2021.3,
author = {Estep, Sam and Wise, Jenna and Aldrich, Jonathan and Tanter, \'{E}ric and Bader, Johannes and Sunshine, Joshua},
title = {{Gradual Program Analysis for Null Pointers}},
booktitle = {35th European Conference on Object-Oriented Programming (ECOOP 2021)},
pages = {3:1--3:25},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-190-0},
ISSN = {1868-8969},
year = {2021},
volume = {194},
editor = {M{\o}ller, Anders and Sridharan, Manu},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/14046},
URN = {urn:nbn:de:0030-drops-140469},
doi = {10.4230/LIPIcs.ECOOP.2021.3},
annote = {Keywords: gradual typing, gradual verification, dataflow analysis}
}
