Gradual Program Analysis for Null Pointers

Authors Sam Estep, Jenna Wise, Jonathan Aldrich, Éric Tanter, Johannes Bader, Joshua Sunshine

Thumbnail PDF


  • Filesize: 0.83 MB
  • 25 pages

Document Identifiers

Author Details

Sam Estep
  • Carnegie Mellon University, Pittsburgh, PA, USA
Jenna Wise
  • Carnegie Mellon University, Pittsburgh, PA, USA
Jonathan Aldrich
  • Carnegie Mellon University, Pittsburgh, PA, USA
Éric Tanter
  • Computer Science Department (DCC), University of Chile, Santiago, Chile
Johannes Bader
  • Jane Street, New York, NY, USA
Joshua Sunshine
  • Carnegie Mellon University, Pittsburgh, PA, USA

Cite AsGet BibTex

Sam Estep, Jenna Wise, Jonathan Aldrich, Éric Tanter, Johannes Bader, and Joshua Sunshine. Gradual Program Analysis for Null Pointers. In 35th European Conference on Object-Oriented Programming (ECOOP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 194, pp. 3:1-3:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)


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.

Subject Classification

ACM Subject Classification
  • Software and its engineering → General programming languages
  • Software and its engineering → Software verification
  • gradual typing
  • gradual verification
  • dataflow analysis


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Nathaniel Ayewah and William Pugh. The google findbugs fixit. In Proceedings of the 19th international symposium on Software testing and analysis, pages 241-252, 2010. Google Scholar
  2. Johannes Bader, Jonathan Aldrich, and Éric Tanter. Gradual program verification. In International Conference on Verification, Model Checking, and Abstract Interpretation, pages 25-46. Springer, 2018. Google Scholar
  3. Subarno Banerjee, Lazaro Clapp, and Manu Sridharan. Nullaway: Practical type-based null safety for java. arXiv preprint arXiv:1907.02127, 2019. Google Scholar
  4. Mike Barnett, Manuel Fahndrich, Francesco Logozzo, and Diego Garbervetsky. Annotations for (more) precise points-to analysis. In IWACO 2007, January 2007. URL:
  5. Dan Brotherston, Werner Dietl, and Ondřej Lhoták. Granullar: Gradual nullable types for java. In Proceedings of the 26th International Conference on Compiler Construction, CC 2017, pages 87-97, New York, NY, USA, 2017. ACM. URL:
  6. Patrice Chalin and Perry R James. Non-null references by default in java: Alleviating the nullity annotation burden. In European Conference on Object-Oriented Programming, pages 227-247. Springer, 2007. Google Scholar
  7. Jong-Deok Choi, Keunwoo Lee, Alexey Loginov, Robert O’Callahan, Vivek Sarkar, and Manu Sridharan. Efficient and precise datarace detection for multithreaded object-oriented programs. In Proceedings of the ACM SIGPLAN 2002 Conference on Programming Language Design and Implementation, PLDI ’02, page 258–269, New York, NY, USA, 2002. Association for Computing Machinery. URL:
  8. Patrick Cousot and Radhia Cousot. Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpoints. In Conference Record of the 4th ACM Symposium on Principles of Programming Languages (POPL 77), pages 238-252, Los Angeles, CA, USA, January 1977. ACM. Google Scholar
  9. Brian A Davey and Hilary A Priestley. Introduction to lattices and order. Cambridge university press, 2002. Google Scholar
  10. Sam Estep, Jenna Wise, Jonathan Aldrich, Éric Tanter, Johannes Bader, and Joshua Sunshine. Gradual program analysis for null pointers, 2021. URL:
  11. Facebook. Infer: A tool to detect bugs in java and c/c++/objective-c code before it ships., 2019. Accessed: 2019-10-28.
  12. Facebook. Eradicate., 2020. Accessed: 2021-1-10.
  13. Robert Bruce Findler and Matthias Felleisen. Contracts for higher-order functions. In Proceedings of the 7th ACM SIGPLAN Conference on Functional Programming (ICFP 2002), pages 48-59, Pittsburgh, PA, USA, 2002. ACM. Google Scholar
  14. Ronald Garcia, Alison M. Clark, and Éric Tanter. Abstracting gradual typing. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '16, pages 429-442, New York, NY, USA, 2016. ACM. URL:
  15. Brittany Johnson, Yoonki Song, Emerson Murphy-Hill, and Robert Bowdidge. Why don't software developers use static analysis tools to find bugs? In Proceedings of the 2013 International Conference on Software Engineering, pages 672-681. IEEE Press, 2013. Google Scholar
  16. Gary A Kildall. A unified approach to global program optimization. In Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, pages 194-206. ACM, 1973. Google Scholar
  17. Kenneth Knowles and Cormac Flanagan. Hybrid type checking. ACM Transactions on Programming Languages and Systems (TOPLAS), 32(2):1-34, 2010. Google Scholar
  18. Bertrand Meyer. Eiffel: The Language. Prentice Hall, 1992. Google Scholar
  19. Abel Nieto, Marianna Rapoport, Gregor Richards, and Ondřej Lhoták. Blame for null. In European Conference on Object-Oriented Programming, 2020. Google Scholar
  20. Peter W O'Hearn. Incorrectness logic. Proceedings of the ACM on Programming Languages, 4(POPL):1-32, 2019. Google Scholar
  21. Matthew M Papi, Mahmood Ali, Telmo Luis Correa Jr, Jeff H Perkins, and Michael D Ernst. Practical pluggable types for java. In Proceedings of the 2008 international symposium on Software testing and analysis, pages 201-212, 2008. Google Scholar
  22. Jeremy G Siek and Walid Taha. Gradual typing for functional languages. In Scheme and Functional Programming Workshop, volume 6, pages 81-92, 2006. Google Scholar
  23. Jeremy G Siek, Michael M Vitousek, Matteo Cimini, and John Tang Boyland. Refined criteria for gradual typing. In LIPIcs-Leibniz International Proceedings in Informatics, volume 32. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2015. Google Scholar
  24. Jenna Wise, Johannes Bader, Cameron Wong, Jonathan Aldrich, Éric Tanter, and Joshua Sunshine. Gradual verification of recursive heap data structures. Proceedings of the ACM on Programming Languages, 4(OOPSLA):1-28, 2020. Google Scholar
  25. Dana N Xu. Hybrid contract checking via symbolic simplification. In Proceedings of the ACM SIGPLAN 2012 workshop on Partial evaluation and program manipulation, pages 107-116, 2012. Google Scholar
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail