research-article

Building and using pluggable type-checkers

Authors:

Todd W. SchillerAuthors Info & Claims

ICSE '11: Proceedings of the 33rd International Conference on Software Engineering

Pages 681 - 690

https://doi.org/10.1145/1985793.1985889

Published: 21 May 2011 Publication History

Get Access

Abstract

This paper describes practical experience building and using pluggable type-checkers. A pluggable type-checker refines (strengthens) the built-in type system of a programming language. This permits programmers to detect and prevent, at compile time, defects that would otherwise have been manifested as run-time errors. The prevented defects may be generally applicable to all programs, such as null pointer dereferences. Or, an application-specific pluggable type system may be designed for a single application.

We built a series of pluggable type checkers using the Checker Framework, and evaluated them on 2 million lines of code, finding hundreds of bugs in the process. We also observed 28 first-year computer science students use a checker to eliminate null pointer errors in their course projects.

Along with describing the checkers and characterizing the bugs we found, we report the insights we had throughout the process. Overall, we found that the type checkers were easy to write, easy for novices to productively use, and effective in finding real bugs and verifying program properties, even for widely tested and used open source projects.

References

[1]

J. R. Allen. Anatomy of LISP. McGraw-Hill, New York, 1978.

Digital Library

Google Scholar

[2]

C. Andreae, J. Noble, S. Markstrum, and T. Millstein. A framework for implementing pluggable type systems. In OOPSLA, pages 57--74, Oct. 2006.

Digital Library

Google Scholar

[3]

P. Chalin, P. James, and F. Rioux. Reducing the use of nullable types through non-null by default and monotonic non-null. IET Software, 2(6):515--531, Dec. 2008.

Crossref

Google Scholar

[4]

Checker Framework website. http://types.cs.washington.edu/checker-framework/.

Google Scholar

[5]

ECMA Technical Group TG49-TG4 (Eiffel) of ECMA Technical Committee 49 (Programming Languages), editor. Standard ECMA-367 and ISO/IEC 25436:2006, Eiffel Analysis, Design and Programming Language. ECMA International and International Standards Organization, Geneva, June 2006.

Google Scholar

[6]

T. Ekman and G. Hedin. The JastAdd extensible Java compiler. In OOPSLA, pages 1--18, Oct. 2007.

Digital Library

Google Scholar

[7]

T. Ekman and G. Hedin. Pluggable checking and inferencing of non-null types for Java. J. Object Tech., 6(9):455--475, Oct. 2007.

Crossref

Google Scholar

[8]

M. D. Ernst. Building and using pluggable type systems with the Checker Framework. In ECOOP, July 2008. Tool demo.

Google Scholar

[9]

M. D. Ernst. Type Annotations specification (JSR 308). http://types.cs.washington.edu/jsr308/, Sep. 12, 2008.

Google Scholar

[10]

M. D. Ernst, J. Cockrell, W. G. Griswold, and D. Notkin. Dynamically discovering likely program invariants to support program evolution. In ICSE, pages 213--224, May 1999.

Digital Library

Google Scholar

[11]

M. D. Ernst, J. H. Perkins, P. J. Guo, S. McCamant, C. Pacheco, M. S. Tschantz, and C. Xiao. The Daikon system for dynamic detection of likely invariants. Sci. Comput. Programming, 69(1-3):35--45, Dec. 2007.

Digital Library

Google Scholar

[12]

A. P. Ershov. On programming of arithmetic operations. CACM, 1(8):3--6, Aug. 1958.

Digital Library

Google Scholar

[13]

J.-C. Filliâtre and S. Conchon. Type-safe modular hash-consing. In ML, pages 12--19, Sep. 2006.

Digital Library

Google Scholar

[14]

J. S. Foster, M. Fähndrich, and A. Aiken. A theory of type qualifiers. In PLDI, pages 192--203, June 1999.

Digital Library

Google Scholar

[15]

J. S. Foster, T. Terauchi, and A. Aiken. Flow-sensitive type qualifiers. In PLDI, pages 1--12, June 2002.

Digital Library

Google Scholar

[16]

J. Gosling, B. Joy, G. Steele, and G. Bracha. The Java Language Specification. Addison Wesley, Boston, MA, third edition, 2005.

Digital Library

Google Scholar

[17]

E. Goto. Monocopy and associative algorithms in an extended Lisp. Technical Report 74-03, Information Science Laboratory, University of Tokyo, Tokyo, Japan, May 1974.

Google Scholar

[18]

D. Greenfieldboyce and J. S. Foster. Type qualifier inference for Java. In OOPSLA, pages 321--336, Oct. 2007.

Digital Library

Google Scholar

[19]

D. Hovemeyer, J. Spacco, and W. Pugh. Evaluating and tuning a static analysis to find null pointer bugs. In PASTE, pages 13--19, Sep. 2005.

Digital Library

Google Scholar

[20]

T. Lindholm and F. Yellin. The Java Virtual Machine Specification. Addison-Wesley, Reading, MA, USA, 2nd edition, 1999.

Digital Library

Google Scholar

[21]

D. Marinov and R. O'Callahan. Object equality profiling. In OOPSLA, pages 313--325, Nov. 2003.

Digital Library

Google Scholar

[22]

S. Markstrum, D. Marino, M. Esquivel, T. Millstein, C. Andreae, and J. Noble. JavaCOP: Declarative pluggable types for Java. ACM TOPLAS, 32(2):1--37, Jan. 2010.

Digital Library

Google Scholar

[23]

B. Meyer, A. Kogtenkov, and E. Stapf. Avoid a void: The eradication of null dereferencing. In Reflections on the Work of C. A. R. Hoare, chapter 9, pages 189--211. Springer, London, 2010.

Crossref

Google Scholar

[24]

N. Nystrom, M. R. Clarkson, and A. C. Myers. Polyglot: An extensible compiler framework for Java. In CC, pages 138--152, Apr. 2003.

Digital Library

Google Scholar

[25]

M. M. Papi, M. Ali, T. L. Correa Jr., J. H. Perkins, and M. D. Ernst. Practical pluggable types for Java. In ISSTA, pages 201--212, July 2008.

Digital Library

Google Scholar

[26]

M. Vaziri, F. Tip, S. Fink, and J. Dolby. Declarative object identity using relation types. In ECOOP, pages 54--78, Aug. 2007.

Digital Library

Google Scholar

[27]

O. Zendra and D. Colnet. Towards safer aliasing with the Eiffel language. In IWAOOS, pages 153--154, June 1999.

Digital Library

Google Scholar

Cited By

View all

Lee MBak JMoon SJhi YOh HFilkov VRay BZhou M(2024)Effective Unit Test Generation for Java Null Pointer ExceptionsProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695484(1044-1056)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695484
Lee EZhao YLhoták OYou JSatheeskumar KBrachthäuser J(2024)Qualifying System F<:: Some Terms and Conditions May ApplyProceedings of the ACM on Programming Languages10.1145/36498328:OOPSLA1(583-612)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649832
Xie DChen BHuang KWang YPan LChen ZPeng X(2024)Enhancing Field Tracking and Interprocedural Analysis to Find More Null Pointer Exceptions2024 IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER)10.1109/SANER60148.2024.00093(849-859)Online publication date: 12-Mar-2024
https://doi.org/10.1109/SANER60148.2024.00093
Show More Cited By

Index Terms

Building and using pluggable type-checkers
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language features
        Data types and structures
      2. Language types
        Object oriented languages
2. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program reasoning

Recommendations

Practical pluggable types for java
ISSTA '08: Proceedings of the 2008 international symposium on Software testing and analysis

This paper introduces the Checker Framework, which supports adding pluggable type systems to the Java language in a backward-compatible way. A type system designer defines type qualifiers and their semantics, and a compiler plug-in enforces the ...
Compile-time type-checking for custom type qualifiers in Java
OOPSLA '07: Companion to the 22nd ACM SIGPLAN conference on Object-oriented programming systems and applications companion

We have created a system that enables programmers to add custom type qualifiers to the Java language in a backward-compatible way. The system allows programmers to write type qualifiers in their programs and to create compiler plug-ins that enforce the ...
Compile-time type-checking for custom type qualifiers in Java
OOPSLA '07: Companion to the 22nd ACM SIGPLAN conference on Object-oriented programming systems and applications companion

We have created a system that enables programmers to add custom type qualifiers to the Java language in a backward-compatible way. The system allows programmers to write type qualifiers in their programs and to create compiler plug-ins that enforce the ...

Reviews

Reviewer: Andrew Brooks

The Checker Framework tool supports the processing of custom-built annotations for Java at compile time. This paper reports on a case study using the tool to build five checkers. The ease of building, the ease of use, and the effectiveness of each checker are discussed at length. An informal report is provided on classroom use of the Nullness checker. Figure 1 presents the case study statistics. Four of the five checkers were small in size, but the Nullness checker comprised over 4,000 lines of code. The number of annotations written for each program in the case study was typically over 100. Defects capable of causing runtime failure were found in more than half of the programs. Other kinds of errors, such as incorrect documentation, were found in most programs. The false positive rate was over 50 percent for eight of the 11 programs studied. In the classroom study, all students found at least one null pointer defect. The majority of students, however, only used the two annotations they had been taught (@NonNull and @Nullable). The authors conclude that the five checkers were easy to build and use. Since time was not used as a measure, particularly the time needed to identify and suppress false positives, these claims could be disputed. However, readers will be impressed by the detection of over 40 defects in well-tested and well-used programs. These checkers found defects for Google Collections that had been missed by the FindBugs static analysis tool. This paper is strongly recommended to the software engineering community. Online Computing Reviews Service

Access critical reviews of Computing literature here

Become a reviewer for Computing Reviews.

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

ICSE '11: Proceedings of the 33rd International Conference on Software Engineering

May 2011

1258 pages

ISBN:9781450304450

DOI:10.1145/1985793

General Chair:
Richard N. Taylor
UC Irvine, USA
,
Program Chairs:
Harald Gall
University of Zurich, Switzerland
,
Nenad Medvidović
University of Southern California, USA

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 21 May 2011

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

ICSE11

Sponsor:

SIGSOFT

ICSE11: International Conference on Software Engineering

May 21 - 28, 2011

HI, Waikiki, Honolulu, USA

Acceptance Rates

Overall Acceptance Rate 276 of 1,856 submissions, 15%

Upcoming Conference

ICSE 2025

2025 IEEE/ACM 46th International Conference on Software Engineering

April 26 - May 3, 2025

Ottawa , ON , Canada

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

87
Total Citations
View Citations
443
Total Downloads

Downloads (Last 12 months)31
Downloads (Last 6 weeks)2

Reflects downloads up to 13 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

View all

Lee MBak JMoon SJhi YOh HFilkov VRay BZhou M(2024)Effective Unit Test Generation for Java Null Pointer ExceptionsProceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering10.1145/3691620.3695484(1044-1056)Online publication date: 27-Oct-2024
https://dl.acm.org/doi/10.1145/3691620.3695484
Lee EZhao YLhoták OYou JSatheeskumar KBrachthäuser J(2024)Qualifying System F<:: Some Terms and Conditions May ApplyProceedings of the ACM on Programming Languages10.1145/36498328:OOPSLA1(583-612)Online publication date: 29-Apr-2024
https://dl.acm.org/doi/10.1145/3649832
Xie DChen BHuang KWang YPan LChen ZPeng X(2024)Enhancing Field Tracking and Interprocedural Analysis to Find More Null Pointer Exceptions2024 IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER)10.1109/SANER60148.2024.00093(849-859)Online publication date: 12-Mar-2024
https://doi.org/10.1109/SANER60148.2024.00093
Jha PDietl W(2024)OppropBERL: A GNN and BERT-Style Reinforcement Learning-Based Type Inference2024 IEEE International Conference on Software Analysis, Evolution and Reengineering (SANER)10.1109/SANER60148.2024.00021(131-136)Online publication date: 12-Mar-2024
https://doi.org/10.1109/SANER60148.2024.00021
Shankar NKim MSanchez HRueß HBeyene TBouchekir RBhatt DVaradarajan SMurugesan ARen HHong-Wong ISiu KVaranasi SErnst M(2024)Continuous Safety & Security Evidence Generation, Curation and Assurance Case Construction Using the Evidential Tool Bus2024 AIAA DATC/IEEE 43rd Digital Avionics Systems Conference (DASC)10.1109/DASC62030.2024.10749275(1-10)Online publication date: 29-Sep-2024
https://doi.org/10.1109/DASC62030.2024.10749275
Guerra EGomes EFerreira JWiese ILima PGerosa MMeirelles P(2024)How do annotations affect Java code readability?Empirical Software Engineering10.1007/s10664-024-10460-w29:3Online publication date: 3-May-2024
https://doi.org/10.1007/s10664-024-10460-w
Giallorenzo SMontesi FPeressotti MRademacher FSachweh SWizenty P(2024)A Toolchain for Checking Domain- and Model-Driven Properties of Jolie MicroservicesService-Oriented Computing10.1007/978-981-96-0808-9_13(161-175)Online publication date: 7-Dec-2024
https://doi.org/10.1007/978-981-96-0808-9_13
Karimipour NPham JClapp LSridharan MChandra SBlincoe KTonella P(2023)Practical Inference of Nullability TypesProceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3611643.3616326(1395-1406)Online publication date: 30-Nov-2023
https://dl.acm.org/doi/10.1145/3611643.3616326
Feldman KKellogg MChaparro OChandra SBlincoe KTonella P(2023)On the Relationship between Code Verifiability and UnderstandabilityProceedings of the 31st ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering10.1145/3611643.3616242(211-223)Online publication date: 30-Nov-2023
https://dl.acm.org/doi/10.1145/3611643.3616242
Shajii ARamirez GSmajlović HRay JBerger BAmarasinghe SNumanagić IVerbrugge CLhoták OShen X(2023)Codon: A Compiler for High-Performance Pythonic Applications and DSLsProceedings of the 32nd ACM SIGPLAN International Conference on Compiler Construction10.1145/3578360.3580275(191-202)Online publication date: 17-Feb-2023
https://dl.acm.org/doi/10.1145/3578360.3580275
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Cited By

Index Terms

Recommendations

Practical pluggable types for java

Compile-time type-checking for custom type qualifiers in Java

Compile-time type-checking for custom type qualifiers in Java

Reviews

Access critical reviews of Computing literature here