Gradual Program Analysis for Null Pointers
Fri 16 Jul 2021 02:00 - 02:20 at ECOOP 1 - Program Analysis / Runtimes (time band 2) Chair(s): Werner Dietl
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.
slides (ECOOP21 slides.pdf) | 597KiB |
Thu 15 JulDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
19:00 - 20:00 | Program Analysis (time band 1)ECOOP Technical Papers at ECOOP 1 Chair(s): Uday P. Khedker Indian Institute of Technology (IIT) Bombay | ||
19:00 20mTalk | Lossless, Persisted Summarization of Static Callgraph, Points-To and Data-Flow AnalysisDistinguished Paper ECOOP Technical Papers Philipp Dominik Schubert Heinz Nixdorf Institut, Paderborn University, Ben Hermann Technical University Dortmund, Eric Bodden University of Paderborn; Fraunhofer IEM Link to publication DOI Pre-print Media Attached | ||
19:20 20mTalk | Lifted Static Analysis of Dynamic Program Families by Abstract Interpretation ECOOP Technical Papers DOI | ||
19:40 20mTalk | Gradual Program Analysis for Null Pointers ECOOP Technical Papers Sam Estep Carnegie Mellon University, Jenna DiVincenzo (Wise) Carnegie Mellon University, Jonathan Aldrich Carnegie Mellon University, Éric Tanter University of Chile, Johannes Bader Jane Street, Joshua Sunshine Carnegie Mellon University DOI Pre-print Media Attached File Attached |
Fri 16 JulDisplayed time zone: Brussels, Copenhagen, Madrid, Paris change
02:00 - 03:20 | Program Analysis / Runtimes (time band 2)ECOOP Technical Papers at ECOOP 1 Chair(s): Werner Dietl University of Waterloo | ||
02:00 20mTalk | Gradual Program Analysis for Null Pointers ECOOP Technical Papers Sam Estep Carnegie Mellon University, Jenna DiVincenzo (Wise) Carnegie Mellon University, Jonathan Aldrich Carnegie Mellon University, Éric Tanter University of Chile, Johannes Bader Jane Street, Joshua Sunshine Carnegie Mellon University DOI Pre-print Media Attached File Attached | ||
02:20 20mTalk | Best-Effort Lazy Evaluation for Python Software Built On APIs ECOOP Technical Papers DOI | ||
02:40 20mTalk | Lifted Static Analysis of Dynamic Program Families by Abstract Interpretation ECOOP Technical Papers DOI | ||
03:00 20mTalk | Accelerating Object-Sensitive Pointer Analysis by Exploiting Object Containment and Reachability ECOOP Technical Papers Dongjie He University of New South Wales, Jingbo Lu UNSW Sydney, Yaoqing Gao Huawei Canada, Jingling Xue UNSW DOI Pre-print |