Manual
User Manual:
Open the PDF directly: View PDF .
Page Count: 249
Download | ![]() |
Open PDF In Browser | View PDF |
The Checker Framework Manual: Custom pluggable types for Java https://checkerframework.org/ Version 2.5.1 (1 May 2018) For the impatient: Section 1.3 (page 13) describes how to install and use pluggable type-checkers. Contents 1 2 3 Introduction 1.1 How to read this manual . . . . . . . . . 1.2 How it works: Pluggable types . . . . . . 1.3 Installation . . . . . . . . . . . . . . . . 1.4 Example use: detecting a null pointer bug . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 13 13 13 13 Using a checker 2.1 Writing annotations . . . . . . . . . . . . . . . . . . . . . . . . 2.2 Running a checker . . . . . . . . . . . . . . . . . . . . . . . . 2.2.1 Using annotated libraries . . . . . . . . . . . . . . . . . 2.2.2 Distributing your annotated project . . . . . . . . . . . 2.2.3 Summary of command-line options . . . . . . . . . . . 2.2.4 Checker auto-discovery . . . . . . . . . . . . . . . . . . 2.2.5 Shorthand for built-in checkers . . . . . . . . . . . . . 2.3 What the checker guarantees . . . . . . . . . . . . . . . . . . . 2.4 Tips about writing annotations . . . . . . . . . . . . . . . . . . 2.4.1 Write annotations before you run a checker . . . . . . . 2.4.2 How to get started annotating legacy code . . . . . . . . 2.4.3 Annotations indicate normal behavior . . . . . . . . . . 2.4.4 Subclasses must respect superclass annotations . . . . . 2.4.5 Annotations on constructor invocations . . . . . . . . . 2.4.6 What to do if a checker issues a warning about your code . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 15 16 16 17 17 19 19 19 20 20 20 21 22 23 23 Nullness Checker 3.1 What the Nullness Checker checks . . . . . . . . . . . . . . . 3.2 Nullness annotations . . . . . . . . . . . . . . . . . . . . . . 3.2.1 Nullness qualifiers . . . . . . . . . . . . . . . . . . . 3.2.2 Nullness method annotations . . . . . . . . . . . . . . 3.2.3 Initialization qualifiers . . . . . . . . . . . . . . . . . 3.2.4 Map key qualifiers . . . . . . . . . . . . . . . . . . . 3.3 Writing nullness annotations . . . . . . . . . . . . . . . . . . 3.3.1 Implicit qualifiers . . . . . . . . . . . . . . . . . . . . 3.3.2 Default annotation . . . . . . . . . . . . . . . . . . . 3.3.3 Conditional nullness . . . . . . . . . . . . . . . . . . 3.3.4 Nullness and arrays . . . . . . . . . . . . . . . . . . . 3.3.5 Run-time checks for nullness . . . . . . . . . . . . . . 3.3.6 Additional details . . . . . . . . . . . . . . . . . . . . 3.3.7 Inference of @NonNull and @Nullable annotations . . 3.4 Suppressing nullness warnings . . . . . . . . . . . . . . . . . 3.4.1 Suppressing warnings with assertions and method calls . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 25 26 26 27 27 27 28 28 28 28 29 29 29 30 30 30 . . . . . . . . . . . . . . . . 2 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.5 . . . . . . . . . . . . . . . . . . . . . . 31 31 31 31 32 32 32 33 33 33 33 34 35 35 38 38 39 40 41 43 44 44 4 Map Key Checker 4.1 Map key annotations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.2 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4.3 Inference of @KeyFor annotations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 50 50 51 51 5 Optional Checker for possibly-present data 5.1 How to run the Optional Checker . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5.2 Optional annotations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 53 53 53 6 Interning Checker 6.1 Interning annotations . . . . . . . . . . . . . . . . . . . . . . 6.2 Annotating your code with @Interned . . . . . . . . . . . . . 6.2.1 Implicit qualifiers . . . . . . . . . . . . . . . . . . . . 6.2.2 InternedDistinct: values not equals() to any other value 6.3 What the Interning Checker checks . . . . . . . . . . . . . . . 6.3.1 Limitations of the Interning Checker . . . . . . . . . . 6.4 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6.5 Other interning annotations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 55 56 56 56 56 57 58 58 58 Lock Checker 7.1 What the Lock Checker guarantees . . . . . . . . . . . . . 7.2 Lock annotations . . . . . . . . . . . . . . . . . . . . . . 7.2.1 Type qualifiers . . . . . . . . . . . . . . . . . . . 7.2.2 Declaration annotations . . . . . . . . . . . . . . 7.3 Type-checking rules . . . . . . . . . . . . . . . . . . . . . 7.3.1 Polymorphic qualifiers . . . . . . . . . . . . . . . 7.3.2 Dereferences . . . . . . . . . . . . . . . . . . . . 7.3.3 Primitive types, boxed primitive types, and Strings 7.3.4 Overriding . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 59 59 59 59 61 61 61 62 62 62 3.6 3.7 3.8 3.9 7 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.5.1 Tiny examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.5.2 Example annotated source code . . . . . . . . . . . . . . . . . . . . . . . . Tips for getting started . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Nullness_Lite: An Unsound Option of the Nullness Checker for fewer false positives 3.7.1 Introduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.7.2 Who wants to use Nullness_Lite option? . . . . . . . . . . . . . . . . . . . . 3.7.3 How to use the Nullness_Lite? . . . . . . . . . . . . . . . . . . . . . . . . . 3.7.4 More information . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Other tools for nullness checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.8.1 Which tool is right for you? . . . . . . . . . . . . . . . . . . . . . . . . . . 3.8.2 Incompatibility note about FindBugs @Nullable . . . . . . . . . . . . . . . 3.8.3 Relationship to Optional. . . . . . . . . . . . . . . . . . . . . . . . . Initialization Checker . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.9.1 Initialization qualifiers . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.9.2 How an object becomes initialized . . . . . . . . . . . . . . . . . . . . . . . 3.9.3 Partial initialization . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.9.4 Method calls from the constructor . . . . . . . . . . . . . . . . . . . . . . . 3.9.5 Initialization of circular data structures . . . . . . . . . . . . . . . . . . . . 3.9.6 How to handle warnings . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3.9.7 More details about initialization checking . . . . . . . . . . . . . . . . . . . 3.9.8 Rawness Initialization Checker . . . . . . . . . . . . . . . . . . . . . . . . . 3 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7.4 7.5 7.6 7.7 8 7.3.5 Side effects . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7.4.1 Examples of @GuardedBy . . . . . . . . . . . . . . . . . . . . . . . . . . 7.4.2 @GuardedBy({“a”, “b”}) is not a subtype of @GuardedBy({“a”}) . . . . . 7.4.3 Examples of @Holding . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7.4.4 Examples of @EnsuresLockHeld and @EnsuresLockHeldIf . . . . . . . . 7.4.5 Example of @LockingFree, @ReleasesNoLocks, and @MayReleaseLocks 7.4.6 Polymorphism and method formal parameters with unknown guards . . . . More locking details . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7.5.1 Two types of locking: monitor locks and explicit locks . . . . . . . . . . . 7.5.2 Held locks and held expressions; aliasing . . . . . . . . . . . . . . . . . . 7.5.3 Run-time checks for locking . . . . . . . . . . . . . . . . . . . . . . . . . 7.5.4 Discussion of default qualifier . . . . . . . . . . . . . . . . . . . . . . . . 7.5.5 Discussion of @Holding . . . . . . . . . . . . . . . . . . . . . . . . . . . Other lock annotations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 7.6.1 Relationship to annotations in Java Concurrency in Practice . . . . . . . . Possible extensions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 62 63 64 64 65 65 66 67 67 67 67 68 68 69 69 69 Index Checker for sequence bounds (arrays and strings) 8.1 Index Checker structure and annotations . . . . . . . . . . 8.2 Lower bounds . . . . . . . . . . . . . . . . . . . . . . . . 8.3 Upper bounds . . . . . . . . . . . . . . . . . . . . . . . . 8.4 Sequence minimum lengths . . . . . . . . . . . . . . . . . 8.5 Sequences of the same length . . . . . . . . . . . . . . . . 8.6 Binary search indices . . . . . . . . . . . . . . . . . . . . 8.7 Substring indices . . . . . . . . . . . . . . . . . . . . . . 8.7.1 The need for the @SubstringIndexFor annotation 8.8 Inequalities . . . . . . . . . . . . . . . . . . . . . . . . . 8.9 Annotating fixed-size data structures . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 70 71 72 73 74 75 76 76 77 77 Fake Enum Checker for fake enumerations 9.1 Fake enum annotations . . . . . . . . . 9.2 What the Fenum Checker checks . . . . 9.3 Running the Fenum Checker . . . . . . 9.4 Suppressing warnings . . . . . . . . . . 9.5 Example . . . . . . . . . . . . . . . . . 9.6 The fake enumeration pattern . . . . . . 9.7 References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 79 79 80 80 81 81 82 82 10 Tainting Checker 10.1 Tainting annotations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10.2 Tips on writing @Untainted annotations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10.3 @Tainted and @Untainted can be used for many purposes . . . . . . . . . . . . . . . . . . . . . . . 83 83 83 84 11 Regex Checker for regular expression syntax 11.1 Regex annotations . . . . . . . . . . . . . . . . . . . . 11.2 Annotating your code with @Regex . . . . . . . . . . . 11.2.1 Implicit qualifiers . . . . . . . . . . . . . . . . 11.2.2 Capturing groups . . . . . . . . . . . . . . . . 11.2.3 Concatenation of partial regular expressions . . 11.2.4 Testing whether a string is a regular expression 11.2.5 Suppressing warnings . . . . . . . . . . . . . 85 85 85 85 86 86 87 87 9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 Format String Checker 12.1 Formatting terminology . . . . . . . . . 12.2 Format String Checker annotations . . . 12.2.1 Conversion Categories . . . . . 12.2.2 Subtyping rules for @Format . . 12.3 What the Format String Checker checks 12.3.1 Possible false alarms . . . . . . 12.3.2 Possible missed alarms . . . . . 12.4 Implicit qualifiers . . . . . . . . . . . . 12.5 @FormatMethod . . . . . . . . . . . . 12.6 Testing whether a format string is valid . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 88 88 88 89 91 91 92 92 93 93 93 13 Internationalization Format String Checker (I18n Format String Checker) 13.1 Internationalization Format String Checker annotations . . . . . . . . . . 13.2 Conversion categories . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13.3 Subtyping rules for @I18nFormat . . . . . . . . . . . . . . . . . . . . . 13.4 What the Internationalization Format String Checker checks . . . . . . . 13.5 Resource files . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13.6 Running the Internationalization Format Checker . . . . . . . . . . . . . 13.7 Testing whether a string has an i18n format type . . . . . . . . . . . . . . 13.8 Examples of using the Internationalization Format Checker . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 95 95 96 96 97 98 99 99 99 14 Property File Checker 14.1 General Property File Checker . . . . . . . . . . 14.2 Internationalization Checker (I18n Checker) . . . 14.2.1 Internationalization annotations . . . . . 14.2.2 Running the Internationalization Checker 14.3 Compiler Message Key Checker . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 101 101 102 102 102 102 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 Signature String Checker for string representations of types 104 15.1 Signature annotations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104 15.2 What the Signature Checker checks . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106 16 GUI Effect Checker 16.1 GUI effect annotations . . . . . . . . . . . . . . . . . . . . . . . . . . . 16.2 What the GUI Effect Checker checks . . . . . . . . . . . . . . . . . . . . 16.3 Running the GUI Effect Checker . . . . . . . . . . . . . . . . . . . . . . 16.4 Annotation defaults . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16.5 Polymorphic effects . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16.5.1 Defining an effect-polymorphic type . . . . . . . . . . . . . . . . 16.5.2 Using an effect-polymorphic type . . . . . . . . . . . . . . . . . 16.5.3 Subclassing a specific instantiation of an effect-polymorphic type 16.5.4 Subtyping with polymorphic effects . . . . . . . . . . . . . . . . 16.6 References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 107 108 108 108 108 109 109 109 109 110 111 17 Units Checker 17.1 Units annotations . . . . . . . 17.2 Extending the Units Checker . 17.3 What the Units Checker checks 17.4 Running the Units Checker . . 17.5 Suppressing warnings . . . . . 17.6 References . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 112 112 113 114 114 114 115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 Signedness Checker 18.1 Annotations . . . . . . . . . . . . . . . . . . . . 18.1.1 Default qualifiers . . . . . . . . . . . . . 18.2 Prohibited operations . . . . . . . . . . . . . . . 18.3 Rationale . . . . . . . . . . . . . . . . . . . . . 18.4 Utility routines for manipulating unsigned values . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 116 116 117 117 117 118 19 Constant Value Checker 19.1 Annotations . . . . . . . . . . . . . . . . . . . . . . . . . . 19.1.1 Type Annotations . . . . . . . . . . . . . . . . . . . 19.1.2 Compile-time execution of expressions . . . . . . . 19.1.3 @StaticallyExecutable methods and the classpath 19.2 Warnings . . . . . . . . . . . . . . . . . . . . . . . . . . . 19.3 Unsoundly ignoring overflow . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 119 119 119 121 121 121 122 20 Aliasing Checker 20.1 Aliasing annotations . . . . . . . . . . . . . . 20.2 Leaking contexts . . . . . . . . . . . . . . . . 20.3 Restrictions on where @Unique may be written 20.4 Aliasing type refinement . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 123 123 124 125 125 21 Reflection resolution 21.1 MethodVal and ClassVal Checkers . . . . 21.1.1 ClassVal Checker . . . . . . . . . 21.1.2 MethodVal Checker . . . . . . . 21.1.3 MethodVal and ClassVal inference 21.2 Reflection resolution example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 127 127 127 128 129 130 22 Subtyping Checker 22.1 Using the Subtyping Checker . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22.2 Subtyping Checker example . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22.3 Type aliases and typedefs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 132 132 133 135 23 Third-party checkers 23.1 Typestate checkers . . . . . . . . . . . . . . . . . . 23.1.1 Comparison to flow-sensitive type refinement 23.2 Units and dimensions checker . . . . . . . . . . . . 23.3 Thread locality checker . . . . . . . . . . . . . . . . 23.4 Safety-Critical Java checker . . . . . . . . . . . . . 23.5 Generic Universe Types checker . . . . . . . . . . . 23.6 EnerJ checker . . . . . . . . . . . . . . . . . . . . . 23.7 CheckLT taint checker . . . . . . . . . . . . . . . . 23.8 SPARTA information flow type-checker for Android 23.9 Immutability checkers: IGJ, OIGJ, and Javari . . . . 23.10Read Checker for CERT FIO08-J . . . . . . . . . . . 23.11SQL checker that supports multiple dialects . . . . . 23.12Glacier: Class immutability . . . . . . . . . . . . . . 137 137 137 138 138 138 138 138 138 138 139 139 139 139 . . . . . . . . . . . . . . . 6 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 Generics and polymorphism 24.1 Generics (parametric polymorphism or type polymorphism) . . . . 24.1.1 Raw types . . . . . . . . . . . . . . . . . . . . . . . . . . . 24.1.2 Restricting instantiation of a generic class . . . . . . . . . . 24.1.3 Type annotations on a use of a generic type variable . . . . 24.1.4 Annotations on wildcards . . . . . . . . . . . . . . . . . . 24.1.5 Examples of qualifiers on a type parameter . . . . . . . . . 24.1.6 Covariant type parameters . . . . . . . . . . . . . . . . . . 24.1.7 Method type argument inference and type qualifiers . . . . . 24.1.8 The Bottom type . . . . . . . . . . . . . . . . . . . . . . . 24.2 Qualifier polymorphism . . . . . . . . . . . . . . . . . . . . . . . . 24.2.1 Examples of using polymorphic qualifiers . . . . . . . . . . 24.2.2 Relationship to subtyping and generics . . . . . . . . . . . 24.2.3 The @PolyAll qualifier applies to every type system . . . . 24.2.4 Using multiple polymorphic qualifiers in a method signature 24.2.5 Using a single polymorphic qualifier in a method signature . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 140 140 140 140 142 142 143 143 144 144 144 145 145 146 146 147 25 Advanced type system features 25.1 Invariant array types . . . . . . . . . . . . . . . . . . . . . . . . . . . 25.2 Context-sensitive type inference for array constructors . . . . . . . . . 25.3 The effective qualifier on a type (defaults and inference) . . . . . . . . 25.3.1 Default qualifier for unannotated types . . . . . . . . . . . . . . 25.3.2 Defaulting rules and CLIMB-to-top . . . . . . . . . . . . . . . 25.3.3 Inherited defaults . . . . . . . . . . . . . . . . . . . . . . . . . 25.3.4 Inherited wildcard annotations . . . . . . . . . . . . . . . . . . 25.3.5 Default qualifiers for .class files (conservative library defaults) 25.4 Automatic type refinement (flow-sensitive type qualifier inference) . . . 25.4.1 Type refinement examples . . . . . . . . . . . . . . . . . . . . 25.4.2 Types that are not refined . . . . . . . . . . . . . . . . . . . . . 25.4.3 Run-time tests and type refinement . . . . . . . . . . . . . . . . 25.4.4 Fields and flow-sensitive analysis . . . . . . . . . . . . . . . . 25.4.5 Side effects, determinism, purity, and flow-sensitive analysis . . 25.4.6 Assertions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25.5 Writing Java expressions as annotation arguments . . . . . . . . . . . . 25.6 Field invariants . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25.7 Unused fields . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25.7.1 @Unused annotation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 149 149 149 150 151 152 153 153 154 154 155 156 156 157 158 160 160 161 162 162 26 Suppressing warnings 26.1 @SuppressWarnings annotation . . . . . . . . . . . . . . 26.1.1 @SuppressWarnings syntax . . . . . . . . . . . . 26.1.2 Where @SuppressWarnings can be written . . . . 26.1.3 Good practices when suppressing warnings . . . . 26.2 @AssumeAssertion string in an assert message . . . . . 26.2.1 Suppressing warnings and defensive programming 26.3 -AsuppressWarnings command-line option . . . . . . . 26.4 -AskipUses and -AonlyUses command-line options . . . 26.5 -AskipDefs and -AonlyDefs command-line options . . . 26.6 -Alint command-line option . . . . . . . . . . . . . . . . 26.7 Don’t run the processor . . . . . . . . . . . . . . . . . . . 26.8 Checker-specific mechanisms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 164 164 165 165 165 166 167 167 168 168 168 169 169 7 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 Handling legacy code 170 27.1 Checking partially-annotated programs: handling unannotated code . . . . . . . . . . . . . . . . . . 170 27.1.1 Declaration annotations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 170 28 Type inference 28.1 Local type inference during type-checking . . . . . . . . . . 28.2 Type inference to annotate a program . . . . . . . . . . . . . 28.2.1 Type inference tools . . . . . . . . . . . . . . . . . 28.3 Whole-program inference . . . . . . . . . . . . . . . . . . . 28.3.1 Whole-program inference ignores some code . . . . 28.3.2 Manually checking whole-program inference results 28.3.3 How whole-program inference works . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 172 172 172 173 173 174 174 175 29 Annotating libraries 29.1 Tips for annotating a library . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29.1.1 Don’t change the code . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29.1.2 Library annotations should reflect the specification, not the implementation . . . . . . 29.1.3 Report bugs upstream . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29.1.4 Fully annotate the library, or indicate which parts you did not . . . . . . . . . . . . . 29.1.5 Verify your annotations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29.2 Creating an annotated library . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29.3 Creating an annotated JDK . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29.4 Compiling partially-annotated libraries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29.4.1 The -AuseDefaultsForUncheckedCode=source,bytecode command-line argument 29.5 Using stub classes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29.5.1 Using a stub file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29.5.2 Stub file format . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29.5.3 Creating a stub file . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29.5.4 Troubleshooting stub libraries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29.6 Troubleshooting/debugging annotated libraries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 176 176 177 177 177 177 177 178 179 179 180 180 180 181 181 182 182 30 How to create a new checker 30.1 How checkers build on the Checker Framework . . . . . . . . . . . . . . . . . . . . . 30.2 The parts of a checker . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30.3 Compiling and using a custom checker . . . . . . . . . . . . . . . . . . . . . . . . . . 30.3.1 Tips for creating a checker . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30.4 Annotations: Type qualifiers and hierarchy . . . . . . . . . . . . . . . . . . . . . . . . 30.4.1 Defining the type qualifiers . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30.4.2 Declaratively defining the qualifier hierarchy . . . . . . . . . . . . . . . . . . 30.4.3 Procedurally defining the qualifier hierarchy . . . . . . . . . . . . . . . . . . . 30.4.4 Defining a default annotation . . . . . . . . . . . . . . . . . . . . . . . . . . . 30.4.5 Relevant Java types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30.4.6 Do not re-use type qualifiers . . . . . . . . . . . . . . . . . . . . . . . . . . . 30.4.7 Completeness of the type hierarchy . . . . . . . . . . . . . . . . . . . . . . . 30.4.8 Annotations whose argument is a Java expression (dependent type annotations) 30.5 The checker class: Compiler interface . . . . . . . . . . . . . . . . . . . . . . . . . . 30.5.1 Indicating supported annotations . . . . . . . . . . . . . . . . . . . . . . . . . 30.5.2 Bundling multiple checkers . . . . . . . . . . . . . . . . . . . . . . . . . . . 30.5.3 Providing command-line options . . . . . . . . . . . . . . . . . . . . . . . . . 30.6 Visitor: Type rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30.6.1 AST traversal . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30.6.2 Avoid hardcoding . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 184 185 185 186 186 187 188 189 189 190 190 190 190 191 192 192 193 193 194 195 195 8 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30.7 Type factory: Implicit annotations (type introduction rules) . . . . . . 30.7.1 Declaratively specifying implicit annotations . . . . . . . . . 30.7.2 Procedurally specifying implicit annotations . . . . . . . . . . 30.8 Dataflow: enhancing flow-sensitive type qualifier inference . . . . . . 30.8.1 Determine expressions to refine the types of . . . . . . . . . . 30.8.2 Create required class . . . . . . . . . . . . . . . . . . . . . . 30.8.3 Override methods that handle Nodes of interest . . . . . . . . 30.8.4 Implement the refinement . . . . . . . . . . . . . . . . . . . 30.8.5 Disabling flow-sensitive inference . . . . . . . . . . . . . . . 30.9 Annotated JDK . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30.10Testing framework . . . . . . . . . . . . . . . . . . . . . . . . . . . 30.11Debugging options . . . . . . . . . . . . . . . . . . . . . . . . . . . 30.11.1 Amount of detail in messages . . . . . . . . . . . . . . . . . 30.11.2 Stub and JDK libraries . . . . . . . . . . . . . . . . . . . . . 30.11.3 Progress tracing . . . . . . . . . . . . . . . . . . . . . . . . . 30.11.4 Saving the command-line arguments to a file . . . . . . . . . 30.11.5 Visualizing the dataflow graph . . . . . . . . . . . . . . . . . 30.11.6 Miscellaneous debugging options . . . . . . . . . . . . . . . 30.11.7 Examples . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30.11.8 Using an external debugger . . . . . . . . . . . . . . . . . . . 30.12Documenting the checker . . . . . . . . . . . . . . . . . . . . . . . . 30.13javac implementation survival guide . . . . . . . . . . . . . . . . . . 30.13.1 Checker access to compiler information . . . . . . . . . . . . 30.13.2 How a checker fits in the compiler as an annotation processor 30.14Integrating a checker with the Checker Framework . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 195 195 196 196 196 197 197 198 199 199 199 200 200 200 200 200 200 201 201 201 201 202 202 203 204 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 205 205 206 207 207 207 208 208 208 209 209 212 212 212 214 214 32 Frequently Asked Questions (FAQs) 32.1 Motivation for pluggable type-checking . . . . . . . . . . . . . . . . . . . . 32.1.1 I don’t make type errors, so would pluggable type-checking help me? 32.1.2 Should I use pluggable types (type qualifiers) or Java subtypes? . . . 32.2 Getting started . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32.2.1 How do I get started annotating an existing program? . . . . . . . . . 32.2.2 Which checker should I start with? . . . . . . . . . . . . . . . . . . . 32.2.3 How can I join the checker-framework-dev mailing list? . . . . . . . 32.3 Usability of pluggable type-checking . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 215 216 216 217 218 218 218 218 218 31 Integration with external tools 31.1 Android Studio 3.0 and the Android Gradle Plugin 3.0 . . . 31.2 Ant task . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31.2.1 Explanation . . . . . . . . . . . . . . . . . . . . . . 31.3 Eclipse . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31.3.1 Using an Ant task . . . . . . . . . . . . . . . . . . . 31.3.2 Troubleshooting Eclipse . . . . . . . . . . . . . . . 31.4 Gradle . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31.5 IntelliJ IDEA . . . . . . . . . . . . . . . . . . . . . . . . . 31.6 Javac compiler . . . . . . . . . . . . . . . . . . . . . . . . 31.7 Maven . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31.8 NetBeans . . . . . . . . . . . . . . . . . . . . . . . . . . . 31.8.1 Adding a checker via the Project Properties window 31.8.2 Adding a checker via an ant target . . . . . . . . . . 31.9 tIDE . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31.10Type inference tools . . . . . . . . . . . . . . . . . . . . . . 9 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32.3.1 32.3.2 32.3.3 32.3.4 32.3.5 Are type annotations easy to read and write? . . . . . . . . . . . . . . . . . . . . . . . . . . Will my code become cluttered with type annotations? . . . . . . . . . . . . . . . . . . . . . Will using the Checker Framework slow down my program? Will it slow down the compiler? How do I shorten the command line when invoking a checker? . . . . . . . . . . . . . . . . . Method pre-condition contracts, including formal parameter annotations, make no sense for public methods . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32.4 How to handle warnings and errors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32.4.1 What should I do if a checker issues a warning about my code? . . . . . . . . . . . . . . . . 32.4.2 What does a certain Checker Framework warning message mean? . . . . . . . . . . . . . . . 32.4.3 Can a pluggable type-checker guarantee that my code is correct? . . . . . . . . . . . . . . . . 32.4.4 What guarantee does the Checker Framework give for concurrent code? . . . . . . . . . . . . 32.4.5 How do I make compilation succeed even if a checker issues errors? . . . . . . . . . . . . . . 32.4.6 Why does the checker always say there are 100 errors or warnings? . . . . . . . . . . . . . . 32.4.7 Why does the Checker Framework report an error regarding a type I have not written in my program? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32.4.8 How can I do run-time monitoring of properties that were not statically checked? . . . . . . . 32.5 False positive warnings . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32.5.1 What is a “false positive” warning? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32.5.2 How can I improve the Checker Framework to eliminate a false positive warning? . . . . . . . 32.5.3 Why doesn’t the Checker Framework infer types for fields and method return types? . . . . . 32.5.4 Why doesn’t the Checker Framework track relationships between variables? . . . . . . . . . . 32.5.5 Why isn’t the Checker Framework path-sensitive? . . . . . . . . . . . . . . . . . . . . . . . 32.6 Syntax of type annotations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32.6.1 What is a “receiver”? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32.6.2 What is the meaning of an annotation after a type, such as @NonNull Object @Nullable? . 32.6.3 What is the meaning of array annotations such as @NonNull Object @Nullable []? . . . . 32.6.4 What is the meaning of varargs annotations such as @English String @NonEmpty ...? . . 32.6.5 What is the meaning of a type qualifier at a class declaration? . . . . . . . . . . . . . . . . . 32.6.6 Why shouldn’t a qualifier apply to both types and declarations? . . . . . . . . . . . . . . . . 32.6.7 How do I annotate a fully-qualified type name? . . . . . . . . . . . . . . . . . . . . . . . . . 32.6.8 What is the difference between type annotations and declaration annotations? . . . . . . . . . 32.7 Semantics of type annotations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32.7.1 How can I handle typestate, or phases of my program with different data properties? . . . . . 32.7.2 Why are explicit and implicit bounds defaulted differently? . . . . . . . . . . . . . . . . . . . 32.7.3 Why are type annotations declared with @Retention(RetentionPolicy.RUNTIME)? . . . . 32.8 Creating a new checker . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32.8.1 How do I create a new checker? . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32.8.2 What properties can and cannot be handled by type-checking? . . . . . . . . . . . . . . . . . 32.8.3 Why is there no declarative syntax for writing type rules? . . . . . . . . . . . . . . . . . . . . 32.9 Tool questions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32.9.1 How does pluggable type-checking work? . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32.9.2 What classpath is needed to use an annotated library? . . . . . . . . . . . . . . . . . . . . . . 32.9.3 Why do .class files contain more annotations than the source code? . . . . . . . . . . . . . 32.9.4 Is there a type-checker for managing checked and unchecked exceptions? . . . . . . . . . . . 32.10Relationship to other tools . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32.10.1 Why not just use a bug detector (like FindBugs)? . . . . . . . . . . . . . . . . . . . . . . . . 32.10.2 How does the Checker Framework compare with Eclipse’s null analysis? . . . . . . . . . . . 32.10.3 How does the Checker Framework compare with the JDK’s Optional type? . . . . . . . . . 32.10.4 How does pluggable type-checking compare with JML? . . . . . . . . . . . . . . . . . . . . 32.10.5 Is the Checker Framework an official part of Java? . . . . . . . . . . . . . . . . . . . . . . . 32.10.6 What is the relationship between the Checker Framework and JSR 305? . . . . . . . . . . . . 10 218 219 219 219 219 220 220 220 220 221 221 221 221 221 222 222 222 222 223 225 225 225 226 226 226 227 227 228 228 228 228 229 229 230 230 230 230 230 230 231 231 231 231 231 232 232 232 233 233 32.10.7 What is the relationship between the Checker Framework and JSR 308? . . . . . . . . . . . . 233 33 Troubleshooting, getting help, and contributing 33.1 Common problems and solutions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33.1.1 Unable to compile the Checker Framework . . . . . . . . . . . . . . . . . . . . . . . 33.1.2 Unable to run the checker, or checker crashes . . . . . . . . . . . . . . . . . . . . . . 33.1.3 Unexpected type-checking results . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33.1.4 Unexpected compilation output when running javac without a pluggable type-checker 33.2 How to report problems (bug reporting) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33.2.1 Problems with annotated libraries . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33.3 Building from source . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33.3.1 Install prerequisites . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33.3.2 Obtain the source . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33.3.3 Build the Checker Framework . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33.3.4 Build the Checker Framework Manual (this document) . . . . . . . . . . . . . . . . . 33.3.5 Configure Eclipse to edit the Checker Framework . . . . . . . . . . . . . . . . . . . . 33.3.6 Enable Travis continuous integration builds . . . . . . . . . . . . . . . . . . . . . . . 33.3.7 Code style . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33.4 Contributing fixes (creating a pull request) . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33.5 Publications . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33.6 Comparison to other tools . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33.7 Credits and changelog . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33.8 License . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 234 234 234 234 237 239 240 240 241 241 241 242 242 242 243 243 244 244 245 246 246 Chapter 1 Introduction The Checker Framework enhances Java’s type system to make it more powerful and useful. This lets software developers detect and prevent errors in their Java programs. A “checker” is a tool that warns you about certain errors or gives you a guarantee that those errors do not occur. The Checker Framework comes with checkers for specific types of errors: 1. 2. 3. 4. 5. 6. 7. 8. 9. 10. 11. Nullness Checker for null pointer errors (see Chapter 3, page 25) Initialization Checker to ensure all fields are set in the constructor (see Chapter 3.9, page 35) Map Key Checker to track which values are keys in a map (see Chapter 4, page 50) Optional Checker for errors in using the Optional type (see Chapter 5, page 53) Interning Checker for errors in equality testing and interning (see Chapter 6, page 55) Lock Checker for concurrency and lock errors (see Chapter 7, page 59) Index Checker for array accesses (see Chapter 8, page 70) Fake Enum Checker to allow type-safe fake enum patterns and type aliases or typedefs (see Chapter 9, page 79) Tainting Checker for trust and security errors (see Chapter 10, page 83) Regex Checker to prevent use of syntactically invalid regular expressions (see Chapter 11, page 85) Format String Checker to ensure that format strings have the right number and type of % directives (see Chapter 12, page 88) 12. Internationalization Format String Checker to ensure that i18n format strings have the right number and type of {} directives (see Chapter 13, page 95) 13. Property File Checker to ensure that valid keys are used for property files and resource bundles (see Chapter 14, page 101) 14. Internationalization Checker to ensure that code is properly internationalized (see Chapter 14.2, page 102) 15. Signature String Checker to ensure that the string representation of a type is properly used, for example in Class.forName (see Chapter 15, page 104) 16. GUI Effect Checker to ensure that non-GUI threads do not access the UI, which would crash the application (see Chapter 16, page 107) 17. Units Checker to ensure operations are performed on correct units of measurement (see Chapter 17, page 112) 18. Signedness Checker to ensure unsigned and signed values are not mixed (see Chapter 18, page 116) 19. Constant Value Checker to determine whether an expression’s value can be known at compile time (see Chapter 19, page 119) 20. Aliasing Checker to identify whether expressions have aliases (see Chapter 20, page 123) 21. Subtyping Checker for customized checking without writing any code (see Chapter 22, page 132) 22. Third-party checkers that are distributed separately from the Checker Framework (see Chapter 23, page 137) These checkers are easy to use and are invoked as arguments to javac. The Checker Framework also enables you to write new checkers of your own; see Chapters 22 and 30. 12 1.1 How to read this manual If you wish to get started using some particular type system from the list above, then the most effective way to read this manual is: • Read all of the introductory material (Chapters 1–2). • Read just one of the descriptions of a particular type system and its checker (Chapters 3–23). • Skim the advanced material that will enable you to make more effective use of a type system (Chapters 24–33), so that you will know what is available and can find it later. Skip Chapter 30 on creating a new checker. 1.2 How it works: Pluggable types The Checker Framework supports adding pluggable type systems to the Java language in a backward-compatible way. Java’s built-in type-checker finds and prevents many errors — but it doesn’t find and prevent enough errors. The Checker Framework lets you run an additional type-checker as a plug-in to the javac compiler. Your code stays completely backward-compatible: your code compiles with any Java compiler, it runs on any JVM, and your coworkers don’t have to use the enhanced type system if they don’t want to. You can check only part of your program. Type inference tools exist to help you annotate your code; see Chapter 28.2, page 172. A type system designer uses the Checker Framework to define type qualifiers and their semantics, and a compiler plug-in (a “checker”) enforces the semantics. Programmers can write the type qualifiers in their programs and use the plug-in to detect or prevent errors. The Checker Framework is useful both to programmers who wish to write error-free code, and to type system designers who wish to evaluate and deploy their type systems. This document uses the terms “checker”, “checker plugin”, “type-checking compiler plugin”, and “annotation processor” as synonyms. 1.3 Installation This section describes how to install the Checker Framework. (If you wish to try the Checker Framework without installing it, use the Checker Framework Live Demo webpage.) The Checker Framework release contains everything that you need, both to run checkers and to write your own checkers. As an alternative, you can build the latest development version from source (Section 33.3, page 241). Requirement: You must have JDK 8 installed. You can get the JDK from Oracle or elsewhere. The installation process is simple! It has two required steps and one optional step. 1. Download the Checker Framework distribution: https://checkerframework.org/checker-framework-2.5.1.zip 2. Unzip it to create a checker-framework directory. 3. Configure your IDE, build system, or command shell to include the Checker Framework on the classpath. Choose the appropriate section of Chapter 31. That’s all there is to it! Now you are ready to start using the checkers. We recommend that you work through the Checker Framework tutorial (https://checkerframework.org/ tutorial/), which walks you through how to use the Checker Framework on the command line. There is also a Nullness Checker tutorial (https://github.com/glts/safer-spring-petclinic/wiki) by David Bürgin. Section 1.4 walks you through a simple example. More detailed instructions for using a checker appear in Chapter 2. 1.4 Example use: detecting a null pointer bug This section gives a very simple example of running the Checker Framework. There is also a tutorial (https: //checkerframework.org/tutorial/) that gives more extensive instructions for using the Checker Framework on 13 the command line, and a Nullness Checker tutorial (https://github.com/glts/safer-spring-petclinic/wiki) by David Bürgin. 1. Let’s consider this very simple Java class. The local variable ref’s type is annotated as @NonNull, indicating that ref must be a reference to a non-null object. Save the file as GetStarted.java. import org.checkerframework.checker.nullness.qual.*; public class GetStarted { void sample() { @NonNull Object ref = new Object(); } } 2. Run the Nullness Checker on the class. You can do that from the command line or from an IDE: (a) From the command line, run this command: javac -processor org.checkerframework.checker.nullness.NullnessChecker GetStarted.java where javac is set as in Section 31.6. (b) To compile within your IDE, you must have customized it to use the Checker Framework compiler and to pass the extra arguments (see Chapter 31). The compilation should complete without any errors. 3. Let’s introduce an error now. Modify ref’s assignment to: @NonNull Object ref = null; 4. Run the Nullness Checker again, just as before. This run should emit the following error: GetStarted.java:5: incompatible types. found : @Nullable required: @NonNull Object @NonNull Object ref = null; ^ 1 error The type qualifiers (e.g., @NonNull) are permitted anywhere that you can write a type, including generics and casts; see Section 2.1. Here are some examples: @Interned String intern() { ... } int compareTo(@NonNull String other) { ... } @NonNull List<@Interned String> messages; 14 // return value // parameter // non-null list of interned Strings Chapter 2 Using a checker A pluggable type-checker enables you to detect certain bugs in your code, or to prove that they are not present. The verification happens at compile time. Finding bugs, or verifying their absence, with a checker plugin is a two-step process, whose steps are described in Sections 2.1 and 2.2. 1. The programmer writes annotations, such as @NonNull and @Interned, that specify additional information about Java types. (Or, the programmer uses an inference tool to automatically insert annotations in his code: see Section 3.3.7.) It is possible to annotate only part of your code: see Section 27.1. 2. The checker reports whether the program contains any erroneous code — that is, code that is inconsistent with the annotations. This chapter is structured as follows: • • • • Section 2.1: Section 2.2: Section 2.3: Section 2.4: How to write annotations How to run a checker What the checker guarantees Tips about writing annotations Additional topics that apply to all checkers are covered later in the manual: • • • • • • Chapter 25: Chapter 26: Chapter 27: Chapter 29: Chapter 30: Chapter 31: Advanced type system features Suppressing warnings Handling legacy code Annotating libraries How to create a new checker Integration with external tools Finally, there is a tutorial (https://checkerframework.org/tutorial/) that walks you through using the Checker Framework on the command line, and a separate Nullness Checker tutorial (https://github.com/glts/ safer-spring-petclinic/wiki) by David Bürgin. 2.1 Writing annotations The syntax of type annotations in Java is specified by the Java Language Specification (Java SE 8 edition). Java 5 defines declaration annotations such as @Deprecated, which apply to a class, method, or field, but do not apply to the method’s return type or the field’s type. They are typically written on their own line in the source code. Java 8 defines type annotations, which you write immediately before any use of a type, including in generics and casts. Because array levels are types and receivers have types, you can also write type annotations on them. Here are a few examples of type annotations: 15 @Interned String intern() { ... } int compareTo(@NonNull String other) { ... } String toString(@Tainted MyClass this) { ... } @NonNull List<@Interned String> messages; @Interned String @NonNull [] messages; myDate = (@Initialized Date) beingConstructed; // // // // // // return value parameter receiver ("this" parameter) generics: non-null list of interned Strings arrays: non-null array of interned Strings cast You only need to write annotations on method signatures and fields. Annotations within method bodies are inferred for you; for more details, see Section 25.4. 2.2 Running a checker To run a checker plugin, run the compiler javac as usual, but pass the -processor plugin_class command-line option. A concrete example (using the Nullness Checker) is: javac -processor nullness MyFile.java where javac is as specified in Section 31.6. You can also run a checker from within your favorite IDE or build system. See Chapter 31 for details about Ant (Section 31.2), Maven (Section 31.7), Gradle (Section 31.4), IntelliJ IDEA (Section 31.5), Eclipse (Section 31.3), and tIDE (Section 31.9), and about customizing other IDEs and build tools. The checker is run on only the Java files that javac compiles. This includes all Java files specified on the command line (or created by another annotation processor). It may also include other of your Java files (but not if a more recent .class file exists). Even when the checker does not analyze a class (say, the class was already compiled, or source code is not available), it does check the uses of those classes in the source code being compiled. You can always compile the code without the -processor command-line option, but in that case no checking of the type annotations is performed. Furthermore, only explicitly-written annotations are written to the .class file; defaulted annotations are not, and this will interfere with type-checking of clients that use your code. Therefore, it is strongly recommended that whenever you are creating .class files that will be distributed or compiled against, you run the type-checkers for all the annotations that your have written. 2.2.1 Using annotated libraries When your code uses a library that is not currently being compiled, the Checker Framework looks up the library’s annotations in its class files. Some projects are already distributed with type annotations by their maintainers, so you do not need to do anything special. Over time, this should become more common. For some other libraries, the Checker Framework developers have provided an annotated version of the library. During type-checking, you should use the annotated version of the library to improve type-checking results (to issue fewer false positive warnings). When doing ordinary compilation or while running your code, you can use either the annotated library or the regular distributed version of the library — they behave identically. The annotated libraries appear in the org.checkerframework.annotatedlib group in the Central Repository. • If your project stores .jar files locally, then download the .jar file from the Central Repository. • If your project manages dependencies using a tool such as Gradle or Maven, then update your buildfile to use the org.checkerframework.annotatedlib group. For example, in build.gradle, change api group: ’org.apache.bcel’, name: ’bcel’, version: ’6.2’ to api group: ’org.checkerframework.annotatedlib’, name: ’bcel’, version: ’6.2’ Use the same version number. (Sometimes you will use a slightly larger number, if the Checker Framework developers have improved the type annotations since the last release by the upstream maintainers.) If a newer version of the upstream library is available, then open an issue requesting that the org.checkerframework.annotatedlib version be updated. 16 There are two special cases. The annotated JDK is automatically put on your classpath; you don’t have to do anything special for it. For the Javadoc classes in the JDK’s com.sun.javadoc package, use the stub file checker/resources/javadoc.astub. If a library you wish to use is not available, then you can request that it be annotated, or you can volunteer to write the annotations (see Chapter 29, page 176), which will help you and all other Checker Framework users. 2.2.2 Distributing your annotated project The distributed .jar files can be used for pluggable type-checking of client code. The .jar files are only compatible with a Java 8 JVM. Developers perform pluggable type-checking in-house to detect errors and verify their absence. When you create .class files, run each relevant type system. Create the distributed .jar files from those .class files, and also include the contents of checker-framework/checker/dist/checker-qual.jar from the Checker Framework distribution, to define the annotations. 2.2.3 Summary of command-line options You can pass command-line arguments to a checker via javac’s standard -A option (“A” stands for “annotation”). All of the distributed checkers support the following command-line options. Unsound checking: ignore some errors • -AsuppressWarnings Suppress all warnings matching the given key; see Section 26.3. • -AskipUses, -AonlyUses Suppress all errors and warnings at all uses of a given class — or at all uses except those of a given class. See Section 26.4. • -AskipDefs, -AonlyDefs Suppress all errors and warnings within the definition of a given class — or everywhere except within the definition of a given class. See Section 26.5. • -AignoreRawTypeArguments Ignore subtype tests for type arguments that were inferred for a raw type. If possible, it is better to write the type arguments. See Section 24.1.1. • -AassumeSideEffectFree Unsoundly assume that every method is side-effect-free; see Section 25.4.5. • -AassumeAssertionsAreEnabled, -AassumeAssertionsAreDisabled Whether to assume that assertions are enabled or disabled; see Section 25.4.6. • -AignoreRangeOverflow Ignore the possibility of overflow for range annotations such as @IntRange; see Section 19.3. • -Awarns Treat checker errors as warnings. If you use this, you may wish to also supply -Xmaxwarns 10000, because by default javac prints at most 100 warnings. If you use this, don’t supply -Werror, which is a javac argument to halt compilation if a warning is issued. More sound (strict) checking: enable errors that are disabled by default • -AcheckPurityAnnotations Check the bodies of methods marked @SideEffectFree, @Deterministic, and @Pure to ensure the method satisfies the annotation. By default, the Checker Framework unsoundly trusts the method annotation. See Section 25.4.5. • -AinvariantArrays Make array subtyping invariant; that is, two arrays are subtypes of one another only if they have exactly the same element type. By default, the Checker Framework unsoundly permits covariant array subtyping, just as Java does. See Section 25.1. • -AcheckCastElementType In a cast, require that parameterized type arguments and array elements are the same. By default, the Checker Framework unsoundly permits them to differ, just as Java does. See Section 24.1.6 and Section 25.1. • -AuseDefaultsForUncheckedCode Enables/disables unchecked code defaults. Takes arguments “source,bytecode”. “-source,-bytecode” is the (unsound) default setting. “bytecode” specifies whether the checker should apply unchecked code defaults to bytecode; see Section 25.3.5. Outside the scope of any relevant @AnnotatedFor annotation, “source” specifies whether unchecked code default annotations are applied to source code and suppress all type-checking warnings; see Section 29.4. • -AconcurrentSemantics Whether to assume concurrent semantics (field values may change at any time) or sequential semantics; see Section 32.4.4. 17 • -AconservativeUninferredTypeArguments Whether an error should be issued if type arguments could not be inferred and whether method type arguments that could not be inferred should use conservative defaults. By default, such type arguments are (largely) ignored in later checks. Passing this option uses a conservative value instead. See Issue 979. Type-checking modes: enable/disable functionality • -Alint Enable or disable optional checks; see Section 26.6. • -AsuggestPureMethods Suggest methods that could be marked @SideEffectFree, @Deterministic, or @Pure; see Section 25.4.5. • -AresolveReflection Determine the target of reflective calls, and perform more precise type-checking based no that information; see Section 21. -AresolveReflection=debug causes debugging information to be output. • -Ainfer Output suggested annotations for method signatures and fields. These annotations may reduce the number of type-checking errors when running type-checking in the future; see Section 28.3. • -AshowSuppressWarningKeys With each warning, show all possible keys to suppress that warning. Partially-annotated libraries • • • • -Astubs List of stub files or directories; see Section 29.5.1. -AstubWarnIfNotFound Warn if a stub file entry could not be found; see Section 29.5.1. -AstubWarnIfOverwritesBytecode Warn if a stub file entry overwrite bytecode information; see Section 29.5.1. -AuseDefaultsForUncheckedCode=source Outside the scope of any relevant @AnnotatedFor annotation, use unchecked code default annotations and suppress all type-checking warnings; see Section 29.4. Debugging • -AprintAllQualifiers, -AprintVerboseGenerics, -Adetailedmsgtext, -AprintErrorStack, -Anomsgtext Amount of detail in messages; see Section 30.11.1. • -Aignorejdkastub, -Anocheckjdk, -AstubDebug Stub and JDK libraries; see Section 30.11.2. • -Afilenames, -Ashowchecks, -AshowInferenceSteps Progress tracing; see Section 30.11.3. • -AoutputArgsToFile Output the compiler command-line arguments to a file. Useful when the command line is generated and executed by a tool, such as a build system. This produces a standalone command line that can be executed independently of the tool that generated it can make it easier to reproduce, report, and debug issues. For example, the command line can be modified to enable attaching a debugger. See Section 30.11.4. • -Aflowdotdir, -Averbosecfg, -Acfgviz Draw a visualization of the CFG (control flow graph); see Section 30.11.5. • -AresourceStats, -AatfDoNotCache, -AatfCacheSize Miscellaneous debugging options; see Section 30.11.6. Some checkers support additional options, which are described in that checker’s manual section. For example, -Aquals tells the Subtyping Checker (see Chapter 22) and the Fenum Checker (see Chapter 9) which annotations to check. Here are some standard javac command-line options that you may find useful. Many of them contain the word “processor”, because in javac jargon, a checker is an “annotation processor”. • -processor Names the checker to be run; see Section 2.2 • -processorpath Indicates where to search for the checker; should also contain any qualifiers used by the Subtyping Checker; see Section 22.2 • -proc:{none,only} Controls whether checking happens; -proc:none means to skip checking; -proc:only means to do only checking, without any subsequent compilation; see Section 2.2.4 • -implicit:class Suppresses warnings about implicitly compiled files (not named on the command line); see Section 31.2 • -J Supply an argument to the JVM that is running javac; for example, -J-Xmx2500m to increase its maximum heap size • -doe To “dump on error”, that is, output a stack trace whenever a compiler warning/error is produced. Useful when debugging the compiler or a checker. The Checker Framework does not support -source 1.4 or earlier. You must supply -source 1.5 or later, or no -source command-line argument, when running javac. 18 2.2.4 Checker auto-discovery “Auto-discovery” makes the javac compiler always run a checker plugin, even if you do not explicitly pass the -processor command-line option. This can make your command line shorter, and ensures that your code is checked even if you forget the command-line option. To enable auto-discovery, place a configuration file named META-INF/services/javax.annotation.processing.Processor in your classpath. The file contains the names of the checker plugins to be used, listed one per line. For instance, to run the Nullness Checker and the Interning Checker automatically, the configuration file should contain: org.checkerframework.checker.nullness.NullnessChecker org.checkerframework.checker.interning.InterningChecker You can disable this auto-discovery mechanism by passing the -proc:none command-line option to javac, which disables all annotation processing including all pluggable type-checking. 2.2.5 Shorthand for built-in checkers Ordinarily, javac’s -processor flag requires fully-qualified class names. When running a built-in checker, you may omit the package name and the Checker suffix. The following three commands are equivalent: javac -processor org.checkerframework.checker.nullness.NullnessChecker MyFile.java javac -processor NullnessChecker MyFile.java javac -processor nullness MyFile.java This feature will work when multiple checkers are specified. For example: javac -processor NullnessChecker,RegexChecker MyFile.java javac -processor nullness,regex MyFile.java This feature does not apply to Javac @argfiles. 2.3 What the checker guarantees A checker can guarantee that a particular property holds throughout the code. For example, the Nullness Checker (Chapter 3) guarantees that every expression whose type is a @NonNull type never evaluates to null. The Interning Checker (Chapter 6) guarantees that every expression whose type is an @Interned type evaluates to an interned value. The checker makes its guarantee by examining every part of your program and verifying that no part of the program violates the guarantee. There are some limitations to the guarantee. • A compiler plugin can check only those parts of your program that you run it on. If you compile some parts of your program without running the checker, then there is no guarantee that the entire program satisfies the property being checked. Some examples of un-checked code are: – Code compiled without the -processor switch, including any external library supplied as a .class file. – Code compiled with the -AskipUses, -AonlyUses, -AskipDefs or -AonlyDefs properties (see Chapter 26). – Suppression of warnings, such as via the @SuppressWarnings annotation (see Chapter 26). – Native methods (because the implementation is not Java code, it cannot be checked). In each of these cases, any use of the code is checked — for example, a call to a native method must be compatible with any annotations on the native method’s signature. However, the annotations on the un-checked code are trusted; there is no verification that the implementation of the native method satisfies the annotations. • The Checker Framework is, by default, unsound in a few places where a conservative analysis would issue too many false positive warnings. These are listed in Section 2.2.3. You can supply a command-line argument to make the Checker Framework sound for each of these cases. 19 • Specific checkers may have other limitations; see their documentation for details. A checker can be useful in finding bugs or in verifying part of a program, even if the checker is unable to verify the correctness of an entire program. In order to avoid a flood of unhelpful warnings, many of the checkers avoid issuing the same warning multiple times. For example, in this code: @Nullable Object x = ...; x.toString(); x.toString(); // warning // no warning In this case, the second call to toString cannot possibly throw a null pointer warning — x is non-null if control flows to the second statement. In other cases, a checker avoids issuing later warnings with the same cause even when later code in a method might also fail. This does not affect the soundness guarantee, but a user may need to examine more warnings after fixing the first ones identified. (More often, at least in our experience to date, a single fix corrects all the warnings.) If you find that a checker fails to issue a warning that it should, then please report a bug (see Section 33.2). 2.4 Tips about writing annotations Section 29.1 gives additional tips that are specific to annotating a third-party library. 2.4.1 Write annotations before you run a checker Before you run a checker, annotate the code, based on its documentation. Then, run the checker to uncover bugs in the code or the documentation. Don’t do the opposite, which is to run the checker and then add annotations according to the warnings issued. This approach is less systematic, so you may overlook some annotations. It often leads to confusion and poor results. It leads users to make changes not for any principled reason, but to “make the type-checker happy”, even when the changes are in conflict with the documentation or the code. Also see “Annotations are a specification”, below. 2.4.2 How to get started annotating legacy code Annotating an entire existing program may seem like a daunting task. But, if you approach it systematically and do a little bit at a time, you will find that it is manageable. Start small Start small. Focus on one specific property that matters to you; in other words, run just one checker rather than multiple ones. You may choose a different checker for different programs. Focus on the most mission-critical or error-prone part of your code; don’t try to annotate your whole program at first. It is easiest to add annotations if you know the code or the code contains documentation; you will find that you spend most of your time understanding the code, and very little time actually writing annotations or running the checker. When annotating, be systematic; we recommend annotating an entire class at a time (not just some of the methods) so that you don’t lose track of your work or redo work. For example, working class-by-class avoids confusion about whether an unannotated type means you determined that the default is desirable, or it means you didn’t yet examine that type. You may find it helpful to start annotating the leaves of the call tree — that is, start with methods/classes/packages that have few dependencies on other code or, equivalently, start with code that a lot of your other code depends on. For example, within a package annotate supertypes before you annotated classes that extend or implement them. The reason for this rule is that it is easiest to annotate a class if the code it depends on has already been annotated. Don’t overuse pluggable type-checking. If the regular Java type system can verify a property using Java subclasses, then that is a better choice than pluggable type-checking (see Section 32.1.2). 20 Annotations are a specification When you write annotations, you are writing a specification, and you should think about them that way. Start out by understanding the program so that you can write an accurate specification. Sections 2.4.3 and 2.4.4 give more tips about writing specifications. For each class, read its Javadoc. For instance, if you are adding annotations for the Nullness Checker (Section 3), then you can search the documentation for “null” and then add @Nullable anywhere appropriate. For now, just annotate signatures and fields; there is no need to annotate method bodies. The only reason to even read the method bodies yet is to determine signature annotations for undocumented methods — for example, if the method returns null, you know its return type should be annotated @Nullable, and a parameter that is compared against null may need to be annotated @Nullable. After you have annotated all the signatures, run the checker. Then, fix bugs in code and add/modify annotations as necessary. Don’t get discouraged if you see many type-checker warnings at first. Often, adding just a few missing annotations will eliminate many warnings, and you’ll be surprised how fast the process goes overall. You may wonder about the effect of adding a given annotation (that is, of changing the specification for a given method or class): how many other specification changes (added annotations) will it require, and will it conflict with other code? It’s best to reason about the desired design, but you can also do an experiment. Suppose you are considering adding an annotation to a method parameter. One approach is to manually examine all callees. A more automated approach is to save the checker output before adding the annotation, and to compare it to the checker output after adding the annotation. This helps you to focus on the specific consequences of your change. Chapter 29 tells you how to annotate libraries that your code uses. Section 2.4.6 and Chapter 26 tell you what to do when you are unable to eliminate checker warnings by adding annotations. Write good code Avoid complex code, which is more error-prone. If you write your code to be simple and clean enough for the type-checker to verify, then it will also be easier for programmers to understand. Your code should compile cleanly under the regular Java compiler. If you are not willing to write code that typechecks in Java, then there is little point in using an even more powerful, restrictive type system. As a specific example, your code should not use raw types like List; use parameterized types like List instead (Section 24.1.1). Do not write unnecessary annotations. • Do not annotate local variables unless necessary. The checker infers annotations for local variables (see Section 25.4). Usually, you only need to annotate fields and method signatures. You should add annotations inside method bodies only if the checker is unable to infer the correct annotation. • Do not write annotations that are redundant with defaults. For example, when checking nullness (Chapter 3, page 25), the default annotation is @NonNull, in most locations other than some type bounds (Section 25.3.2). When you are starting out, it might seem helpful to write redundant annotations as a reminder, but that’s like when beginning programmers write a comment about every simple piece of code: // The below code increments variable i by adding 1 to it. i++; As you become comfortable with pluggable type-checking, you will find redundant annotations to be distracting clutter, so avoid putting them in your code in the first place. • Avoid writing @SuppressWarnings annotations unless there is no alternative. It is tempting to think that your code is right and the checker’s warnings are false positives. Sometimes they are, but slow down and convince yourself of that before you dismiss them. Section 2.4.6 discusses what to do when a checker issues a warning about your code. 2.4.3 Annotations indicate normal behavior You should use annotations to specify normal behavior. The annotations indicate all the values that you want to flow to a reference — not every value that might possibly flow there if your program has a bug. 21 Many methods are guaranteed to throw an exception if they are passed null as an argument. Examples include java.lang.Double.valueOf(String) java.lang.String.contains(CharSequence) org.junit.Assert.assertNotNull(Object) com.google.common.base.Preconditions.checkNotNull(Object) @Nullable (see Section 3.2) might seem like a reasonable annotation for the parameter, for two reasons. First, null is a legal argument with a well-defined semantics: throw an exception. Second, @Nullable describes a possible program execution: it might be possible for null to flow there, if your program has a bug. However, it is never useful for a programmer to pass null. It is the programmer’s intention that null never flows there. If null does flow there, the program will not continue normally (whether or not it throws a NullPointerException). Therefore, you should specify such parameters as @NonNull, indicating the intended use of the method. When you specify the parameter as the @NonNull annotation, the checker is able to issue compile-time warnings about possible run-time exceptions, which is its purpose. Specifying the parameter as @Nullable would suppress such warnings, which is undesirable. (Since @NonNull is the default, you don’t have to write anything in the source code to specify the parameter as non-null. You are allowed to write a redundant @NonNull annotation, but it is discouraged.) If a method can possibly throw an exception because its parameter is null, then that parameter’s type should be @NonNull, which guarantees that the type-checker will issue a warning for every client use that has the potential to cause an exception. Don’t write @Nullable on the parameter just because there exist some executions that don’t necessarily throw an exception. 2.4.4 Subclasses must respect superclass annotations An annotation indicates a guarantee that a client can depend upon. A subclass is not permitted to weaken the contract; for example, if a method accepts null as an argument, then every overriding definition must also accept null. A subclass is permitted to strengthen the contract; for example, if a method does not accept null as an argument, then an overriding definition is permitted to accept null. As a bad example, consider an erroneous @Nullable annotation in com/google/common/collect/Multiset.java: 101 ... 122 123 ... 129 130 ... 137 138 139 140 141 public interface Multiset extends Collection { /** * Adds a number of occurrences of an element to this multiset. * @param element the element to add occurrences of; may be {@code null} only * if explicitly allowed by the implementation * @throws NullPointerException if {@code element} is null and this * implementation does not permit null elements. Note that if {@code * occurrences} is zero, the implementation may opt to return normally. */ int add(@Nullable E element, int occurrences); There exist implementations of Multiset that permit null elements, and implementations of Multiset that do not permit null elements. A client with a variable Multiset ms does not know which variety of Multiset ms refers to. However, the @Nullable annotation promises that ms.add(null, 1) is permissible. (Recall from Section 2.4.3 that annotations should indicate normal behavior.) If parameter element on line 141 were to be annotated, the correct annotation would be @NonNull. Suppose a client has a reference to same Multiset ms. The only way the client can be sure not to throw an exception is to pass only non-null elements to ms.add(). A particular class that implements Multiset could declare add to take a @Nullable 22 parameter. That still satisfies the original contract. It strengthens the contract by promising even more: a client with such a reference can pass any non-null value to add(), and may also pass null. However, the best annotation for line 141 is no annotation at all. The reason is that each implementation of the Multiset interface should specify its own nullness properties when it specifies the type parameter for Multiset. For example, two clients could be written as class MyNullPermittingMultiset implements Multiset<@Nullable Object> { ... } class MyNullProhibitingMultiset implements Multiset<@NonNull Object> { ... } or, more generally, as class MyNullPermittingMultiset implements Multiset { ... } class MyNullProhibitingMultiset implements Multiset { ... } Then, the specification is more informative, and the Checker Framework is able to do more precise checking, than if line 141 has an annotation. It is a pleasant feature of the Checker Framework that in many cases, no annotations at all are needed on type parameters such as E in MultiSet. 2.4.5 Annotations on constructor invocations In the checkers distributed with the Checker Framework, an annotation on a constructor invocation is equivalent to a cast on a constructor result. That is, the following two expressions have identical semantics: one is just shorthand for the other. new @Untainted Date() (@Untainted Date) new Date() However, you should rarely have to use this. The Checker Framework will determine the qualifier on the result, based on the “return value” annotation on the constructor definition. The “return value” annotation appears before the constructor name, for example: class MyClass { @Untainted MyClass() { ... } } In general, you should only use an annotation on a constructor invocation when you know that the cast is guaranteed to succeed. 2.4.6 What to do if a checker issues a warning about your code When you run a type-checker on your code, it is likely to issue warnings or errors. Don’t panic! There are three general causes for the warnings: • There is a bug in your code, such as a possible null dereference. Fix your code to prevent that crash. • There is a weakness in the annotations you wrote. In other words, the specification you wrote is incorrect or inadequate. Improve the annotations, usually by writing more annotations in order to better express the specification. • There is a weakness in the type-checker. Your code is safe — it never suffers the error at run time — but the checker cannot prove this fact. If possible, rewrite your code to be simpler for the checker to analyze; this is likely to make it easier for people to understand, too. If that is not possible, suppress the warning (see Chapter 26); be sure to include a code comment explaining how you know the code is correct even though the type-checker cannot deduce that fact. 23 For each warning issued by the checker, you need to determine which of the above categories it falls into. Here is an effective methodology to do so. It relies mostly on manual code examination, but you may also find it useful to write test cases for your code or do other kinds of analysis, to verify your reasoning. 1. Write an explanation of why your code is correct and it never suffers the error at run time. In other words, this is an English proof that the type-checker’s warning is incorrect. Don’t skip any steps in your proof. (For example, don’t write an unsubstantiated claim such as “x is non-null here”; instead, give a justification.) Don’t let your reasoning rely on facts that you do not write down explicitly. For example, remember that calling a method might change the values of object fields; your proof might need to state that certain methods have no side effects. If you cannot write a proof, then there is a bug in your code (you should fix the bug) or your code is too complex for you to understand (you should improve its documentation and/or design). 2. Translate the proof into annotations. Here are some examples. • If your proof includes “variable x is never null at run time”, then annotate ’s type with @NonNull. • If your proof includes “method foo always returns a legal regular expression”, then annotate foo’s return type with @Regex. • If your proof includes “if method join’s first argument is non-null, then join returns a non-null result”, then annotate join’s first parameter and return type with @PolyNull. • If your proof includes “method processOptions has already been called and it set field tz1”, then annotate processOptions’s declaration with @EnsuresNonNull("tz1"). • If your proof includes “method isEmpty returned false, so its argument must have been non-null”, then annotate isEmpty’s declaration with @EnsuresNonNullIf(expression="#1",result=false). All of these are examples of correcting weaknesses in the annotations you wrote. The Checker Framework provides many other powerful annotations; you may be surprised how many proofs you can express in annotations. If you need to annotate a method that is defined in a library that your code uses, see Chapter 29, page 176, Annotating Libraries. If there are complex facts in your proof that cannot be expressed as annotations, then that is a weakness in the type-checker. For example, the Nullness Checker cannot express “in list lst, elements stored at even indices are always non-null, but elements stored at odd elements might be null.” In this case, you have two choices. First, you can suppress the warning (Chapter 26, page 164); be sure to write a comment explaining your reasoning for suppressing the warning. You may wish to submit a feature request (Section 33.2) asking for annotations that handle your use case. Second, you can rewrite the code to make the proof simpler; in the above example, it might be better to use a list of pairs rather than a heterogeneous list. 3. At this point, all the steps in your proof have been formalized as annotations. Re-run the checker and repeat the process for any new or remaining warnings. If every step of your proof can be expressed in annotations, but the checker cannot make one of the deductions (it cannot follow one of the steps), then that is a weakness in the type-checker. First, double-check your reasoning. Then, suppress the warning, along with a comment explaining your reasoning (Chapter 26, page 164). The comment is an excerpt from your English proof, and the proof guides you to the best place to suppress the warning. Finally, please submit a bug report so that the checker can be improved in the future (Section 33.2). If you have trouble understanding a Checker Framework warning message, you can search for its text in this manual. Also see Section 33.1.3 and Chapter 33, Troubleshooting. In particular, Section 33.1.3 explains this same methodology in different words. 24 Chapter 3 Nullness Checker If the Nullness Checker issues no warnings for a given program, then running that program will never throw a null pointer exception. This guarantee enables a programmer to prevent errors from occurring when a program is run. See Section 3.1 for more details about the guarantee and what is checked. The most important annotations supported by the Nullness Checker are @NonNull and @Nullable. @NonNull is rarely written, because it is the default. All of the annotations are explained in Section 3.2. To run the Nullness Checker, supply the -processor org.checkerframework.checker.nullness.NullnessChecker command-line option to javac. For examples, see Section 3.5. The NullnessChecker is actually an ensemble of three pluggable type-checkers that work together: the Nullness Checker proper (which is the main focus of this chapter), the Initialization Checker (Section 3.9), and the Map Key Checker (Chapter 4, page 50). Their type hierarchies are completely independent, but they work together to provide precise nullness checking. 3.1 What the Nullness Checker checks The checker issues a warning in these cases: 1. When an expression of non-@NonNull type is dereferenced, because it might cause a null pointer exception. Dereferences occur not only when a field is accessed, but when an array is indexed, an exception is thrown, a lock is taken in a synchronized block, and more. For a complete description of all checks performed by the Nullness Checker, see the Javadoc for NullnessVisitor. 2. When an expression of @NonNull type might become null, because it is a misuse of the type: the null value could flow to a dereference that the checker does not warn about. As a special case of an of @NonNull type becoming null, the checker also warns whenever a field of @NonNull type is not initialized in a constructor. This example illustrates the programming errors that the checker detects: @Nullable Object obj; // might @NonNull Object nnobj; // never ... obj.toString() // checker nnobj = obj; // checker if (nnobj == null) // checker be null null warning: warning: warning: dereference might cause null pointer exception nnobj may become null redundant test Parameter passing and return values are checked analogously to assignments. The Nullness Checker also checks the correctness, and correct use, of rawness annotations for checking initialization (see Section 3.9.8) and of map key annotations (see Chapter 4, page 50). 25 The checker performs additional checks if certain -Alint command-line options are provided. (See Section 26.6 for more details about the -Alint command-line option.) 1. Options that control soundness: • If you supply the -Alint=forbidnonnullarraycomponents command-line option, then the checker warns if it encounters an array creation with a non-null component type. See Section 3.3.4 for a discussion. 2. Options that warn about poor code style: • If you supply the -Alint=redundantNullComparison command-line option, then the checker warns when a null check is performed against a value that is guaranteed to be non-null, as in ("m" == null). Such a check is unnecessary and might indicate a programmer error or misunderstanding. The lint option is disabled by default because sometimes such checks are part of ordinary defensive programming. 3.2 Nullness annotations The Nullness Checker uses three separate type hierarchies: one for nullness, one for rawness (Section 3.9.8), and one for map keys (Chapter 4, page 50) The Nullness Checker has four varieties of annotations: nullness type qualifiers, nullness method annotations, rawness type qualifiers, and map key type qualifiers. 3.2.1 Nullness qualifiers The nullness hierarchy contains these qualifiers: @Nullable indicates a type that includes the null value. For example, the type Boolean is nullable: a variable of type Boolean always has one of the values TRUE, FALSE, or null. @NonNull indicates a type that does not include the null value. The type boolean is non-null; a variable of type boolean always has one of the values true or false. The type @NonNull Boolean is also non-null: a variable of type @NonNull Boolean always has one of the values TRUE or FALSE — never null. Dereferencing an expression of non-null type can never cause a null pointer exception. The @NonNull annotation is rarely written in a program, because it is the default (see Section 3.3.2). @PolyNull indicates qualifier polymorphism. For a description of @PolyNull, see Section 24.2. @MonotonicNonNull indicates a reference that may be null, but if it ever becomes non-null, then it never becomes null again. This is appropriate for lazily-initialized fields, among other uses. When the variable is read, its type is treated as @Nullable, but when the variable is assigned, its type is treated as @NonNull. Because the Nullness Checker works intraprocedurally (it analyzes one method at a time), when a MonotonicNonNull field is first read within a method, the field cannot be assumed to be non-null. The benefit of MonotonicNonNull over Nullable is its different interaction with flow-sensitive type qualifier refinement (Section 25.4). After a check of a MonotonicNonNull field, all subsequent accesses within that method can be assumed to be NonNull, even after arbitrary external method calls that have access to the given field. It is permitted to initialize a MonotonicNonNull field to null, but the field may not be assigned to null anywhere else in the program. If you supply the noInitForMonotonicNonNull lint flag (for example, supply -Alint=noInitForMonotonicNonNull on the command line), then @MonotonicNonNull fields are not allowed to have initializers. Use of @MonotonicNonNull on a static field is a code smell: it may indicate poor design. You should consider whether it is possible to make the field a member field that is set in the constructor. Figure 3.1 shows part of the type hierarchy for the Nullness type system. (The annotations exist only at compile time; at run time, Java has no multiple inheritance.) 26 @Nullable Object @NonNull Object @Nullable Date @NonNull Date Figure 3.1: Partial type hierarchy for the Nullness type system. Java’s Object is expressed as @Nullable Object. Programmers can omit most type qualifiers, because the default annotation (Section 3.3.2) is usually correct. The Nullness Checker verifies three type hierarchies: this one for nullness, one for initialization (Section 3.9), and one for map keys (Chapter 4, page 50). 3.2.2 Nullness method annotations The Nullness Checker supports several annotations that specify method behavior. These are declaration annotations, not type annotations: they apply to the method itself rather than to some particular type. @RequiresNonNull indicates a method precondition: The annotated method expects the specified variables (typically field references) to be non-null when the method is invoked. @EnsuresNonNull @EnsuresNonNullIf indicates a method postcondition. With @EnsuresNonNull, the given expressions are non-null after the method returns; this is useful for a method that initializes a field, for example. With @EnsuresNonNullIf, if the annotated method returns the given boolean value (true or false), then the given expressions are non-null. See Section 3.3.3 and the Javadoc for examples of their use. 3.2.3 Initialization qualifiers The Nullness Checker invokes an Initialization Checker, whose annotations indicate whether an object is fully initialized — that is, whether all of its fields have been assigned. @Initialized @UnknownInitialization @UnderInitialization Use of these annotations can help you to type-check more code. Figure 3.3 shows its type hierarchy. For details, see Section 3.9. A slightly simpler variant, called the Rawness Initialization Checker, is also available: @Raw @NonRaw @PolyRaw Figure 3.7 shows its type hierarchy. For details, see Section 3.9.8. 3.2.4 Map key qualifiers @KeyFor indicates that a value is a key for a given map — that is, indicates whether map.containsKey(value) would evaluate to true. This annotation is checked by a Map Key Checker (Chapter 4, page 50) that the Nullness Checker invokes. The @KeyFor annotation enables the Nullness Checker to treat calls to Map.get precisely rather than assuming it may always return null. In particular, a call mymap.get(mykey) returns a non-null value if two conditions are satisfied: 27 1. mymap’s values are all non-null; that is, mymap was declared as Map . Note that @NonNull is the default type, so it need not be written explicitly. 2. mykey is a key in mymap; that is, mymap.containsKey(mykey) returns true. You express this fact to the Nullness Checker by declaring mykey as @KeyFor("mymap") KeyType mykey. For a local variable, you generally do not need to write the @KeyFor("mymap") type qualifier, because it can be inferred. If either of these two conditions is violated, then mymap.get(mykey) has the possibility of returning null. 3.3 Writing nullness annotations 3.3.1 Implicit qualifiers The Nullness Checker adds implicit qualifiers, reducing the number of annotations that must appear in your code (see Section 25.3). For example, enum types are implicitly non-null, so you never need to write @NonNull MyEnumType. For more information about implicitly-added nullness qualifiers, see the implementation of NullnessAnnotatedTypeFactory. 3.3.2 Default annotation Unannotated references are treated as if they had a default annotation. The standard defaulting rule is CLIMB-to-top, described in Section 25.3.2. Its effect is to default all types to @NonNull, except that @Nullable is used for casts, locals, instanceof, and implicit bounds. A user can choose a different defaulting rule by writing a @DefaultQualifier annotation on a package, class, or method. In the example below, fields are defaulted to @Nullable instead of @NonNull. @DefaultQualifier(value = Nullable.class, locations = TypeUseLocation.FIELD) class MyClass { Object nullableField = null; @NonNull Object nonNullField = new Object(); } 3.3.3 Conditional nullness The Nullness Checker supports a form of conditional nullness types, via the @EnsuresNonNullIf method annotations. The annotation on a method declares that some expressions are non-null, if the method returns true (false, respectively). Consider java.lang.Class. Method Class.getComponentType() may return null, but it is specified to return a non-null value if Class.isArray() is true. You could declare this relationship in the following way (this particular example is already done for you in the annotated JDK that comes with the Checker Framework): class Class { @EnsuresNonNullIf(expression="getComponentType()", result=true) public native boolean isArray(); public native @Nullable Class> getComponentType(); } A client that checks that a Class reference is indeed that of an array, can then de-reference the result of Class.getComponentType safely without any nullness check. The Checker Framework source code itself uses such a pattern: if (clazz.isArray()) { // no possible null dereference on the following line TypeMirror componentType = typeFromClass(clazz.getComponentType()); ... } 28 Another example is Queue.peek and Queue.poll, which return non-null if isEmpty returns false. The argument to @EnsuresNonNullIf is a Java expression, including method calls (as shown above), method formal parameters, fields, etc.; for details, see Section 25.5. More examples of the use of these annotations appear in the Javadoc for @EnsuresNonNullIf. 3.3.4 Nullness and arrays Suppose that you declare an array to contain non-null elements. Currently, the Nullness Checker does not verify that all the elements of the array are initialized to a non-null value. This is an unsoundness in the checker. To make the Nullness Checker conservatively reject code that may leave a non-null value in an array, use the command-line option -Alint=forbidnonnullarraycomponents. The option is currently disabled because it makes the checker issue many false positive errors. When the -Alint=forbidnonnullarraycomponents option is supplied, the following is not allowed: Object [] oa = new Object[10]; // error (recall that Object means the same thing as @NonNull Object). Instead, your code needs to create a nullable or lazy-nonnull array, initialize each component, and then assign the result to a non-null array: @MonotonicNonNull Object [] temp = new @MonotonicNonNull Object[10]; for (int i = 0; i < temp.length; ++i) { temp[i] = new Object(); } @SuppressWarnings("nullness") // temp array is now fully initialized @NonNull Object [] oa = temp; Note that the checker is currently not powerful enough to ensure that each array component was initialized. Therefore, the last assignment needs to be trusted: that is, a programmer must verify that it is safe, then write a @SuppressWarnings annotation. 3.3.5 Run-time checks for nullness When you perform a run-time check for nullness, such as if (x != null) ..., then the Nullness Checker refines the type of x to @NonNull. The refinement lasts until the end of the scope of the test or until x may be side-effected. For more details, see Section 25.4. 3.3.6 Additional details The Nullness Checker does some special checks in certain circumstances, in order to soundly reduce the number of warnings that it produces. For example, a call to System.getProperty(String) can return null in general, but it will not return null if the argument is one of the built-in-keys listed in the documentation of System.getProperties(). The Nullness Checker is aware of this fact, so you do not have to suppress a warning for a call like System.getProperty("line.separator"). The warning is still issued for code like this: final String s = "line.separator"; nonNullvar = System.getProperty(s); though that case could be handled as well, if desired. (Suppression of the warning is, strictly speaking, not sound, because a library that your code calls, or your code itself, could perversely change the system properties; the Nullness Checker assumes this bizarre coding pattern does not happen.) 29 3.3.7 Inference of @NonNull and @Nullable annotations It can be tedious to write annotations in your code. Tools exist that can automatically infer annotations and insert them in your source code. (This is different than type qualifier refinement for local variables (Section 25.4), which infers a more specific type for local variables and uses them during type-checking but does not insert them in your source code. Type qualifier refinement is always enabled, no matter how annotations on signatures got inserted in your source code.) Your choice of tool depends on what default annotation (see Section 3.3.2) your code uses. You only need one of these tools. • Inference of @Nullable: If your code uses the standard CLIMB-to-top default (Section 25.3.2) or the NonNull default, then use the AnnotateNullable tool of the Daikon invariant detector. • Inference of @NonNull: If your code uses the Nullable default, use one of these tools: – Julia analyzer, – Nit: Nullability Inference Tool, – Non-null checker and inferencer of the JastAdd Extensible Compiler. 3.4 Suppressing nullness warnings When the Nullness Checker reports a warning, it’s best to change the code or its annotations, to eliminate the warning. Alternately, you can suppress the warning, which does not change the code but prevents the Nullness Checker from reporting this particular warning to you. The Checker Framework supplies several ways to suppress warnings, most notably the @SuppressWarnings("nullness") annotation (see Chapter 26). An example use is // might return null @Nullable Object getObject(...) { ... } void myMethod() { @SuppressWarnings("nullness") // with argument x, getObject always returns a non-null value @NonNull Object o2 = getObject(x); The Nullness Checker supports an additional warning suppression key, nullness:generic.argument. Use of @SuppressWarnings("nullness:generic.argument") causes the Nullness Checker to suppress warnings related to misuse of generic type arguments. One use for this key is when a class is declared to take only @NonNull type arguments, but you want to instantiate the class with a @Nullable type argument, as in List<@Nullable Object>. The Nullness Checker also permits you to use assertions or method calls to suppress warnings; see below. 3.4.1 Suppressing warnings with assertions and method calls Occasionally, it is inconvenient or verbose to use the @SuppressWarnings annotation. For example, Java does not permit annotations such as @SuppressWarnings to appear on statements. In such cases, you can use the @AssumeAssertion string in an assert message (see Section 26.2). If you need to suppress a warning within an expression, then sometimes writing an assertion is not convenient. In such a case, you can suppress warnings by writing a call to the NullnessUtil.castNonNull method. The rest of this section discusses the castNonNull method. The Nullness Checker considers both the return value, and also the argument, to be non-null after the castNonNull method call. The Nullness Checker issues no warnings in any of the following code: // One way to use castNonNull as a cast: @NonNull String s = castNonNull(possiblyNull1); // Another way to use castNonNull as a cast: castNonNull(possiblyNull2).toString(); 30 // It is possible, but not recommmended, to use castNonNull as a statement: // (It would be better to write an assert statement with @AssumeAssertion // in its message, instead.) castNonNull(possiblyNull3); possiblyNull3.toString(); The castNonNull method throws AssertionError if Java assertions are enabled and the argument is null. However, it is not intended for general defensive programming; see Section 26.2.1. A potential disadvantage of using the castNonNull method is that your code becomes dependent on the Checker Framework at run time as well as at compile time: you need to include checker-qual.jar on your classpath at run time. If this is a problem, you can copy the implementation of castNonNull into your own code, and possibly renaming it if you do not like the name. Be sure to retain the documentation that indicates that your copy is intended for use only to suppress warnings and not for defensive programming. See Section 26.2.1 for an explanation of the distinction. The Nullness Checker introduces a new method, rather than re-using an existing method such as org.junit.Assert.assertNotNull(Object) or com.google.common.base.Preconditions.checkNotNull(Object). Those methods are commonly used for defensive programming, so it is impossible to know the programmer’s intent when writing them. Therefore, it is important to have a method call that is used only for warning suppression. See Section 26.2.1 for a discussion of the distinction between warning suppression and defensive programming. 3.5 3.5.1 Examples Tiny examples To try the Nullness Checker on a source file that uses the @NonNull qualifier, use the following command (where javac is the Checker Framework compiler that is distributed with the Checker Framework): javac -processor org.checkerframework.checker.nullness.NullnessChecker docs/examples/NullnessExample.java Compilation will complete without warnings. To see the checker warn about incorrect usage of annotations (and therefore the possibility of a null pointer exception at run time), use the following command: javac -processor org.checkerframework.checker.nullness.NullnessChecker docs/examples/NullnessExampleWithWarnings.java The compiler will issue two warnings regarding violation of the semantics of @NonNull. 3.5.2 Example annotated source code Some libraries that are annotated with nullness qualifiers are: • The Nullness Checker itself. • The Plume-lib library. Run the command make check-nullness. • The Daikon invariant detector. Run the command make check-nullness. 3.6 Tips for getting started Here are some tips about getting started using the Nullness Checker on a legacy codebase. For more generic advice (not specific to the Nullness Checker), see Section 2.4.2. Your goal is to add @Nullable annotations to the types of any variables that can be null. (The default is to assume that a variable is non-null unless it has a @Nullable annotation.) Then, you will run the Nullness Checker. Each of its errors indicates either a possible null pointer exception, or a wrong/missing annotation. When there are no more warnings from the checker, you are done! We recommend that you start by searching the code for occurrences of null in the following locations; when you find one, write the corresponding annotation: 31 • in Javadoc: add @Nullable annotations to method signatures (parameters and return types). • return null: add a @Nullable annotation to the return type of the given method. • param == null: when a formal parameter is compared to null, then in most cases you can add a @Nullable annotation to the formal parameter’s type • TypeName field = null;: when a field is initialized to null in its declaration, then it needs either a @Nullable or a @MonotonicNonNull annotation. If the field is always set to a non-null value in the constructor, then you can just change the declaration to Type field;, without an initializer, and write no type annotation (because the default is @NonNull). • declarations of contains, containsKey, containsValue, equals, get, indexOf, lastIndexOf, and remove (with Object as the argument type): change the argument type to @Nullable Object; for remove, also change the return type to @Nullable Object. You should ignore all other occurrences of null within a method body. In particular, you (almost) never need to annotate local variables. Only after this step should you run ant to invoke the Nullness Checker. The reason is that it is quicker to search for places to change than to repeatedly run the checker and fix the errors it tells you about, one at a time. Here are some other tips: • In any file where you write an annotation such as @Nullable, don’t forget to add import org.checkerframework.checker.nullness.qual.*;. • To indicate an array that can be null, write, for example: int @Nullable []. By contrast, @Nullable Object [] means a non-null array that contains possibly-null objects. • If you know that a particular variable is definitely not null, but the Nullness Checker estimates that the variable might be null, then you can make the Nullness Checker trust your judgment by writing an assertion (see Section 26.2): assert var != null : "@AssumeAssertion(nullness)"; • To indicate that a routine returns the same value every time it is called, use @Pure (see Section 25.4.5). • To indicate a method precondition (a contract stating the conditions under which a client is allowed to call it), you can use annotations such as @RequiresNonNull (see Section 3.2.2). 3.7 3.7.1 Nullness_Lite: An Unsound Option of the Nullness Checker for fewer false positives Introduction Nullness_Lite is a lite option of the Nullness Checker in the Checker Framework to detect nullness bugs in java source files. It disables the following features of Nullness Checker to obtain more desireable traits. To be specific, the Nullness Checker with Nullness_Lite option enabled will be faster and easier to use by delibrately giving up soundness. Featrue Disabled Substitute Behavior of the Nullness_Lite option Initialization Checker Assume all values (fields & class variables) initialized Map Key Checker Assume all keys are in the map and Map.get(key) returns @NonNull Invalidation of dataflow Assume no aliasing and all methods are @SideEffectFree Boxing of primitives Assume the boxing of primitives return the same object and BoxedClass.valueOf() are @Pure 3.7.2 Who wants to use Nullness_Lite option? Java developers who would like to get a trustable analysis on their source files, but hesitate to spend time running full verification tool such as Nullness Checker. They can run the Nullenss_Lite option instead to get a fast glimpse on their files before they upgrade to the Nullness Checker. 32 3.7.3 How to use the Nullness_Lite? Please follow the instructions for installation first. To compile the Nullness Checker, please follow the instructions in Section 2.2 for information about running a checker. Users run Nullness_Lite by passing an extra argument when running Nullness Checker from the command line: javac -processor nullness -ANullnessLite * Notice that the behavior is undefined if -ANullnessLite option is passed to a different checker. 3.7.4 More information • See the implementation • See the evaluation on JUnit4 Refer to the complete Nullness_Lite user manual on GitHub for more details. 3.8 Other tools for nullness checking The Checker Framework’s nullness annotations are similar to annotations used in IntelliJ IDEA, FindBugs, JML, the JSR 305 proposal, NetBeans, and other tools. In particular, IDE tools such as Eclipse and IntelliJ should be viewed as bug-finding tools rather than verification tools, since they give up precision, soundness, or both in favor of being fast and easy to use. Also see Section 33.6 for a comparison to other tools. You might prefer to use the Checker Framework because it has a more powerful analysis that can warn you about more null pointer errors in your code. If your code is already annotated with a different nullness annotation, the Checker Framework can type-check your code. It treats annotations from other tools as if you had written the corresponding annotation from the Nullness Checker, as described in Figure 3.2. If the other annotation is a declaration annotation, it may be moved; see Section 27.1.1. The Checker Framework may issue more or fewer errors than another tool. This is expected, since each tool uses a different analysis. Remember that the Checker Framework aims at soundness: it aims to never miss a possible null dereference, while at the same time limiting false reports. Also, note FindBugs’s non-standard meaning for @Nullable (Section 3.8.2). Java permits you to import at most one annotation of a given name. For example, if you use both android.annotation.NonNull and lombok.NonNull in your source code, then you must write at least one of them in fully-qualified form, as @android.annotation.NonNull rather than as @NonNull. 3.8.1 Which tool is right for you? Different tools are appropriate in different circumstances. Here is a brief comparison with FindBugs, but similar points apply to other tools. (For example, the NullAway and Eradicate tools are more like sound type-checking than FindBugs, but all of those tools accept unsoundness — that is, false negatives or missed warnings — in exchange for analysis speed.) The Checker Framework has a more powerful nullness analysis; FindBugs misses some real errors. FindBugs requires you to annotate your code, but usually not as thoroughly as the Checker Framework does. Depending on the importance of your code, you may desire: no nullness checking, the cursory checking of FindBugs, or the thorough checking of the Checker Framework. You might even want to ensure that both tools run, for example if your coworkers or some other organization are still using FindBugs. If you know that you will eventually want to use the Checker Framework, there is no point using FindBugs first; it is easier to go straight to using the Checker Framework. FindBugs can find other errors in addition to nullness errors; here we focus on its nullness checks. Even if you use FindBugs for its other features, you may want to use the Checker Framework for analyses that can be expressed as pluggable type-checking, such as detecting nullness errors. 33 android.annotation.NonNull android.support.annotation.NonNull com.sun.istack.internal.NotNull edu.umd.cs.findbugs.annotations.NonNull javax.annotation.Nonnull javax.validation.constraints.NotNull lombok.NonNull org.eclipse.jdt.annotation.NonNull org.eclipse.jgit.annotations.NonNull org.jetbrains.annotations.NotNull org.jmlspecs.annotation.NonNull org.netbeans.api.annotations.common.NonNull org.springframework.lang.NonNull ⇒ org.checkerframework.checker.nullness.qual.NonNull android.annotation.Nullable android.support.annotation.Nullable com.sun.istack.internal.Nullable edu.umd.cs.findbugs.annotations.Nullable edu.umd.cs.findbugs.annotations.CheckForNull edu.umd.cs.findbugs.annotations.PossiblyNull edu.umd.cs.findbugs.annotations.UnknownNullness javax.annotation.Nullable javax.annotation.CheckForNull ⇒ org.checkerframework.checker.nullness.qual.Nullable org.eclipse.jdt.annotation.Nullable org.eclipse.jgit.annotations.Nullable org.jetbrains.annotations.Nullable org.jmlspecs.annotation.Nullable org.netbeans.api.annotations.common.NullAllowed org.netbeans.api.annotations.common.CheckForNull org.netbeans.api.annotations.common.NullUnknown org.springframework.lang.Nullable Figure 3.2: Correspondence between other nullness annotations and the Checker Framework’s annotations. Regardless of whether you wish to use the FindBugs nullness analysis, you may continue running all of the other FindBugs analyses at the same time as the Checker Framework; there are no interactions among them. If FindBugs (or any other tool) discovers a nullness error that the Checker Framework does not, please report it to us (see Section 33.2) so that we can enhance the Checker Framework. 3.8.2 Incompatibility note about FindBugs @Nullable FindBugs has a non-standard definition of @Nullable. FindBugs’s treatment is not documented in its own Javadoc; it is different from the definition of @Nullable in every other tool for nullness analysis; it means the same thing as @NonNull when applied to a formal parameter; and it invariably surprises programmers. Thus, FindBugs’s @Nullable is detrimental rather than useful as documentation. In practice, your best bet is to not rely on FindBugs for nullness analysis, even if you find FindBugs useful for other purposes. You can skip the rest of this section unless you wish to learn more details. FindBugs suppresses all warnings at uses of a @Nullable variable. (You have to use @CheckForNull to indicate a nullable variable that FindBugs should check.) For example: // declare getObject() to possibly return null 34 @Nullable Object getObject() { ... } void myMethod() { @Nullable Object o = getObject(); // FindBugs issues no warning about calling toString on a possibly-null reference! o.toString(); } The Checker Framework does not emulate this non-standard behavior of FindBugs, even if the code uses FindBugs annotations. With FindBugs, you annotate a declaration, which suppresses checking at all client uses, even the places that you want to check. It is better to suppress warnings at only the specific client uses where the value is known to be non-null; the Checker Framework supports this, if you write @SuppressWarnings at the client uses. The Checker Framework also supports suppressing checking at all client uses, by writing a @SuppressWarnings annotation at the declaration site. Thus, the Checker Framework supports both use cases, whereas FindBugs supports only one and gives the programmer less flexibility. In general, the Checker Framework will issue more warnings than FindBugs, and some of them may be about real bugs in your program. See Section 3.4 for information about suppressing nullness warnings. (FindBugs made a poor choice of names. The choice of names should make a clear distinction between annotations that specify whether a reference is null, and annotations that suppress false warnings. The choice of names should also have been consistent for other tools, and intuitively clear to programmers. The FindBugs choices make the FindBugs annotations less helpful to people, and much less useful for other tools. As a separate issue, the FindBugs analysis is also very imprecise. For type-related analyses, it is best to stay away from the FindBugs nullness annotations, and use a more capable tool like the Checker Framework.) 3.8.3 Relationship to Optional Many null pointer exceptions occur because the programmer forgets to check whether a reference is null before dereferencing it. Java 8’s Optional class provides a partial solution: you cannot dereference the contained value without calling the get method. However, the use of Optional for this purpose is unsatisfactory. First, it adds syntactic complexity, making your code longer and harder to read. (The Optional class provides some operations, such as map and orElse, that you would otherwise have to write; without these its code bloat would be even worse.) Second, there is no guarantee that the programmer remembers to call isPresent before calling get. Thus, use of Optional doesn’t solve the underlying problem — it merely converts a NullPointerException into a NoSuchElementException exception, and in either case your code crashes. The Nullness Checker does not suffer these limitations. It works with existing code and types, it ensures that you check for null wherever necessary, and it infers when the check for null is not necessary based on previous statements in the method. See the article “Nothing is better than Java’s Optional class” for more details and explanation of the benefits of @Nullable over Optional. Java’s Optional class provides utility routines to reduce clutter when using Optional. The Nullness Checker provides an Opt class that provides all the same methods, but written for regular possibly-null Java references. 3.9 Initialization Checker The Initialization Checker determines whether an object is initialized or not. For any object that is not fully initialized, the Nullness Checker treats its fields as possibly-null — even fields annotated as @NonNull. Every object’s fields start out as null. By the time the constructor finishes executing, the @NonNull fields have been set to a different value. Your code can suffer a NullPointerException when using a @NonNull field, if your code uses the field during initialization. The Nullness Checker prevents this problem by warning you anytime that you may be 35 accessing an uninitialized field. This check is useful because it prevents errors in your code. However, the analysis can be confusing to understand. If you wish to disable the initialization checks, pass the command-line argument -AsuppressWarnings=uninitialized when running the Nullness Checker. You will no longer get a guarantee of no null pointer exceptions, but you can still use the Nullness Checker to find most of the null pointer problems in your code. An object is partially initialized from the time that its constructor starts until its constructor finishes. This is relevant to the Nullness Checker because while the constructor is executing — that is, before initialization completes — a @NonNull field may be observed to be null, until that field is set. In particular, the Nullness Checker issues a warning for code like this: public class MyClass { private @NonNull Object f; public MyClass(int x, int y) { // Error because constructor contains no assignment to this.f. // By the time the constructor exits, f must be initialized to a non-null value. } public MyClass(int x) { // Error because this.f is accessed before f is initialized. // At the beginning of the constructor’s execution, accessing this.f // yields null, even though field f has a non-null type. this.f.toString(); } public MyClass(int x, int y, int z) { m(); } public void m() { // Error because this.f is accessed before f is initialized, // even though the access is not in a constructor. // When m is called from the constructor, accessing f yields null, // even though field f has a non-null type. this.f.toString(); } When a field f is declared with a @NonNull type, then code can depend on the fact that the field is not null. However, this guarantee does not hold for a partially-initialized object. The Nullness Checker uses three annotations to indicate whether an object is initialized (all its @NonNull fields have been assigned), under initialization (its constructor is currently executing), or its initialization state is unknown. These distinctions are mostly relevant within the constructor, or for references to this that escape the constructor (say, by being stored in a field or passed to a method before initialization is complete). Use of initialization annotations is rare in most code. The most common use for the @UnderInitialization annotation is for a helper routine that is called by constructor. For example: class MyClass { Object field1; Object field2; Object field3; public MyClass(String arg1) { this.field1 = arg1; init_other_fields(); } 36 // A helper routine that initializes all the fields other than field1. @EnsuresNonNull({"field2", "field3"}) private void init_other_fields(@UnderInitialization(Object.class) MyClass this) { field2 = new Object(); field3 = new Object(); } public MyClass(String arg1, String arg2, String arg3) { this.field1 = arg1; this.field2 = arg2; this.field3 = arg3; checkRep(); } // Verify that the representation invariants are satisfied. // Works as long as the MyClass fields are initialized, even if the reciever’s // class is a subclass of MyClass and not all of the subclass fields are initialized. private void checkRep(@UnderInitialization(MyClass.class) MyClass this) { ... } } Note that it would not be sound to type @code this as fully @link Initialized anywhere in a constructor (with the exception of final classes, for which the set of all fields is known), because there might be subclasses with uninitialized fields. The following example shows why: class A { @NonNull String a; public A() { a = ""; // Now, all fields of A are initialized. // However, if this constructor is invoked as part of ’new B()’, then // the fields of B are not yet initialized. // If we would type ’this’ as @Initialized, then the following call is valid: foo(); } void foo() {} } class B extends A { @NonNull String b; @Override void foo() { // Dereferencing ’b’ is ok, since ’this’ is @Initialized and ’b’ @NonNull. // However, when executing ’new B()’, this line throws a null-pointer exception. b.toString(); } } 37 @UnderInitialization(Object.class) Giraffe @UnknownInitialization Object @Initialized Object @UnderInitialization(Vertebrate.class) Giraffe @UnderInitialization Object @UnknownInitialization Date @Initialized Date @UnderInitialization(Mammal.class) Giraffe @UnderInitialization Date @UnderInitialization(Giraffe.class) Giraffe Figure 3.3: Partial type hierarchy for the Initialization type system. @UnknownInitialization and @UnderInitialization each take an optional parameter indicating how far initialization has proceeded, and the right side of the figure illustrates its type hierarchy in more detail. 3.9.1 Initialization qualifiers The initialization hierarchy is shown in Figure 3.3. The initialization hierarchy contains these qualifiers: @Initialized indicates a type that contains a fully-initialized object. Initialized is the default, so there is little need for a programmer to write this explicitly. @UnknownInitialization indicates a type that may contain a partially-initialized object. In a partially-initialized object, fields that are annotated as @NonNull may be null because the field has not yet been assigned. @UnknownInitialization takes a parameter that is the class the object is definitely initialized up to. For instance, the type @UnknownInitialization(Foo.class) denotes an object in which every fields declared in Foo or its superclasses is initialized, but other fields might not be. Just @UnknownInitialization is equivalent to @UnknownInitialization(Object.class). @UnderInitialization indicates a type that contains a partially-initialized object that is under initialization — that is, its constructor is currently executing. It is otherwise the same as @UnknownInitialization. Within the constructor, this has @UnderInitialization type until all the @NonNull fields have been assigned. A partially-initialized object (this in a constructor) may be passed to a helper method or stored in a variable; if so, the method receiver, or the field, would have to be annotated as @UnknownInitialization or as @UnderInitialization. If a reference has @UnknownInitialization or @UnderInitialization type, then all of its @NonNull fields are treated as @MonotonicNonNull: when read, they are treated as being @Nullable, but when written, they are treated as being @NonNull. The initialization hierarchy is orthogonal to the nullness hierarchy. It is legal for a reference to be @NonNull @UnderInitialization, @Nullable @UnderInitialization, @NonNull @Initialized, or @Nullable @Initialized. The nullness hierarchy tells you about the reference itself: might the reference be null? The initialization hierarchy tells you about the @NonNull fields in the referred-to object: might those fields be temporarily null in contravention of their type annotation? Figure 3.4 contains some examples. 3.9.2 How an object becomes initialized Within the constructor, this starts out with @UnderInitialization type. As soon as all of the @NonNull fields in class C have been initialized, then this is treated as @UnderInitialization(C). This means that this is still being initialized, but all initialization of C’s fields is complete, including all fields of supertypes. Eventually, when all constructors complete, the type is @Initialized. The Initialization Checker issues an error if the constructor fails to initialize any @NonNull field. This ensures that the object is in a legal (initialized) state by the time that the constructor exits. This is different than Java’s test for definite assignment (see JLS ch.16), which does not apply to fields (except blank final ones, defined in JLS §4.12.4) because fields have a default value of null. 38 Declarations class C { @NonNull Object f; @Nullable Object g; ... } @NonNull @Initialized C a; @NonNull @UnderInitialization C b; @Nullable @Initialized C c; @Nullable @UnderInitialization C d; Expression Expression’s nullness type, or checker error a a.f a.g b b.f b.g c c.f c.g d d.f d.g @NonNull @NonNull @Nullable @NonNull @MonotonicNonNull @Nullable @Nullable error: deref of nullable error: deref of nullable @Nullable error: deref of nullable error: deref of nullable Figure 3.4: Examples of the interaction between nullness and initialization. Declarations are shown at the left for reference, but the focus of the table is the expressions and their nullness type or error. All @NonNull fields must either have a default in the field declaration, or be assigned in the constructor or in a helper method that the constructor calls. If your code initializes (some) fields in a helper method, you will need to annotate the helper method with an annotation such as @EnsuresNonNull({"field1", "field2"}) for all the fields that the helper method assigns. 3.9.3 Partial initialization So far, we have discussed initialization as if it is an all-or-nothing property: an object is non-initialized until initialization completes, and then it is initialized. The full truth is a bit more complex: during the initialization process an object can be partially initialized, and as the object’s superclass constructors complete, its initialization status is updated. The Initialization Checker lets you express such properties when necessary. Consider a simple example: class A { Object aField; A() { aField = new Object(); } } class B extends A { Object bField; B() { super(); bField = new Object(); } } Consider what happens during execution of new B(). 1. B’s constructor begins to execute. At this point, neither the fields of A nor those of B have been initialized yet. 39 2. B’s constructor calls A’s constructor, which begins to execute. No fields of A nor of B have been initialized yet. 3. A’s constructor completes. Now, all the fields of A have been initialized, and their invariants (such as that field a is non-null) can be depended on. However, because B’s constructor has not yet completed executing, the object being constructed is not yet fully initialized. When treated as an A (e.g., if only the A fields are accessed), the object is initialized, but when treated as a B, the object is still non-initialized. 4. B’s constructor completes. The object is initialized when treated as an A or a B. (And, the object is fully initialized if B’s constructor was invoked via a new B(). But the type system cannot assume that – there might be a class C extends B { ... }, and B’s constructor might have been invoked from that.) At any moment during initialization, the superclasses of a given class can be divided into those that have completed initialization and those that have not yet completed initialization. More precisely, at any moment there is a point in the class hierarchy such that all the classes above that point are fully initialized, and all those below it are not yet initialized. As initialization proceeds, this dividing line between the initialized and uninitialized classes moves down the type hierarchy. The Nullness Checker lets you indicate where the dividing line is between the initialized and non-initialized classes. The @UnderInitialization(classliteral) indicates the first class that is known to be fully initialized. When you write @UnderInitialization(OtherClass.class) MyClass x;, that means that variable x is initialized for OtherClass and its superclasses, and x is (possibly) uninitialized for MyClass and all subclasses. The example above lists 4 moments during construction. At those moments, the type of the object being constructed is: 1. 2. 3. 4. 3.9.4 @UnderInitialization B @UnderInitialization A @UnderInitialization(A.class) A @UnderInitialization(B.class) B Method calls from the constructor Consider the following incorrect program. class A { Object aField; A() { aField = new Object(); process(5); // illegal call } public void process(int arg) { ... } } The call to process() is not legal. process() is declared to be called on a fully-initialized receiver, which is the default if you do not write a different initialization annotation. At the call to process(), all the fields of A have been set, but this is not fully initialized because fields in subclasses of A have not yet been set. The type of this is @UnderInitialization(A.class), meaning that this is partially-initialized, with the A part of initialization done but the initialization of subclasses not yet complete. The Initialization Checker output indicates this problem: Client.java:7: error: [method.invocation.invalid] call to process(int) not allowed on the given receiver. process(5); // illegal call ^ found : @UnderInitialization(A.class) A required: @Initialized A Here is a subclass and client code that crashes with a NullPointerException. 40 x.f x is @Initialized x is @UnderInitialization x is @UnknownInitialization f is @NonNull @Initialized @NonNull @UnknownInitialization @Nullable @UnknownInitialization @Nullable f is @Nullable @Initialized @Nullable @UnknownInitialization @Nullable @UnknownInitialization @Nullable Figure 3.5: Initialization rules for reading a @NotOnlyInitialized field f. class B extends A { List processed; B() { super(); processed = new ArrayList (); } @Override public void process(int arg) { super(); processed.add(arg); } } class Client { public static void main(String[] args) { new B(); } } You can correct the problem in multiple ways. One solution is to not call methods that can be overridden from the constructor: move the call to process() to after the constructor has completed. Another solution is to change the declaration of process(): public void process(@UnderInitialization(A.class) A this, int arg) { ... } If you choose this solution, you will need to rewrite the definition of B.process() so that it is consistent with the declared receiver type. A non-solution is to prevent subclasses from overriding process() by using final on the method. This doesn’t work because even if process() is not overridden, it might call other methods that are overridden. As final classes cannot have subclasses, they can be handled more flexibly: once all fields of the final class have been initialized, this is fully initialized. 3.9.5 Initialization of circular data structures There is one final aspect of the initialization type system to be considered: the rules governing reading and writing to objects that are currently under initialization (both reading from fields of objects under initialization, as well as writing objects under initialization to fields). By default, only fully-initialized objects can be stored in a field of another object. If this was the only option, then it would not be possible to create circular data structures (such as a doubly-linked list) where fields have a @NonNull type. However, the annotation @NotOnlyInitialized can be used to indicate that a field can store objects that are currently under initialization. In this case, the rules for reading and writing to that field become a little bit more interesting, to soundly support circular structures. The rules for reading from a @NotOnlyInitialized field are summarized in Figure 3.5. Essentially, nothing is known about the initialization status of the value returned unless the receiver was @Initialized. Similarly, Figure 3.6 shows under which conditions an assignment x.f = y is allowed for a @NotOnlyInitialized field f. If the receiver x is @UnderInitialization, then any y can be of any initialization state. If y is known to be fully initialized, then any receiver is allowed. All other assignments are disallowed. 41 x.f = y x is @Initialized x is @UnderInitialization x is @UnknownInitialization y is @Initialized yes yes yes y is @UnderInitialization no yes no y is @UnknownInitialization no yes no Figure 3.6: Rules for deciding when an assignment x.f = y is allowed for a @NotOnlyInitialized field f. These rules allow for the safe initialization of circular structures. For instance, consider a doubly linked list: class List { @NotOnlyInitialized Node sentinel; public List() { this.sentinel = new Node (this); } void insert(@Nullable T data) { this.sentinel.insertAfter(data); } public static void main() { List l = new List (); l.insert(1); l.insert(2); } } class Node { @NotOnlyInitialized Node prev; @NotOnlyInitialized Node next; @NotOnlyInitialized List parent; @Nullable T data; // for sentinel construction Node(@UnderInitialization List parent) { this.parent = parent; this.prev = this; this.next = this; } // for data node construction Node(Node prev, Node next, @Nullable T data) { this.parent = prev.parent; this.prev = prev; 42 this.next = next; this.data = data; } void insertAfter(@Nullable T data) { Node n = new Node (this, this.next, data); this.next.prev = n; this.next = n; } } 3.9.6 How to handle warnings “error: the constructor does not initialize fields: . . . ” Like any warning, “error: the constructor does not initialize fields: . . . ” indicates that either your annotations are incorrect or your code is buggy. You can fix either the annotations or the code. • Declare the field as @Nullable. Recall that if you did not write an annotation, the field defaults to @NonNull. • Declare the field as @MonotonicNonNull. This is appropriate if the field starts out as null but is later set to a non-null value. You may then wish to use the @EnsuresNonNull annotation to indicate which methods set the field, and the @RequiresNonNull annotation to indicate which methods require the field to be non-null. • Initialize the field in the constructor or in the field’s initializer, if the field should be initialized. (In this case, the Initialization Checker has found a bug!) Do not initialize the field to an arbitrary non-null value just to eliminate the warning. Doing so degrades your code: it introduces a value that will confuse other programmers, and it converts a clear NullPointerException into a more obscure error. “call to . . . is not allowed on the given receiver” If your code calls an instance method from a constructor, you may see a message such as the following: Foo.java:123: error: call to initHelper() not allowed on the given receiver. initHelper(); ^ found : @UnderInitialization(com.google.Bar.class) @NonNull MyClass required: @Initialized @NonNull MyClass The problem is that the current object (this) is under initialization, but the receiver formal parameter (Section 32.6.1) of method initHelper() is implicitly annotated as @Initialized. If initHelper() doesn’t depend on its receiver being initialized — that is, it’s OK to call x.initHelper even if x is not initialized — then you can indicate that by using @UnderInitialization or @UnknownInitialization. class MyClass { void initHelper(@UnknownInitialization MyClass this, String param1) { ... } } You are likely to want to annotate initHelper() with @EnsuresNonNull as well; see Section 3.2.2. You may get the “call to . . . is not allowed on the given receiver” error even if your constructor has already initialized all the fields. For this code: public class MyClass { @NonNull Object field; public MyClass() { 43 field = new Object(); helperMethod(); } private void helperMethod() { } } the Nullness Checker issues the following warning: MyClass.java:7: error: call to helperMethod() not allowed on the given receiver. helperMethod(); ^ found : @UnderInitialization(MyClass.class) @NonNull MyClass required: @Initialized @NonNull MyClass 1 error The reason is that even though the object under construction has had all the fields declared in MyClass initialized, there might be a subclass of MyClass. Thus, the receiver of helperMethod should be declared as @UnderInitialization(MyClass.class), which says that initialization has completed for all the MyClass fields but may not have been completed overall. If helperMethod had been a public method that could also be called after initialization was actually complete, then the receiver should have type @UnknownInitialization, which is the supertype of @UnknownInitialization and @UnderInitialization. 3.9.7 More details about initialization checking Suppressing warnings You can suppress warnings related to partially-initialized objects with @SuppressWarnings("initialization"). This can be placed on a single field; on a constructor; or on a class to suppress all initialization warnings for all constructors. To disable initialization checking, supply the command-line argument -AsuppressWarnings=uninitialized. Do not use -AsuppressWarnings=initialization, because doing so will disable all nullness checking as well as all initialization checking. (That is because of an implementation detail of the Nullness and Initialization Checkers: they are actually the same checker, rather than being two separate checkers that are aggregated together.) Use of method annotations A method with a non-initialized receiver may assume that a few fields (but not all of them) are non-null, and it sometimes sets some more fields to non-null values. To express these concepts, use the @RequiresNonNull, @EnsuresNonNull, and @EnsuresNonNullIf method annotations; see Section 3.2.2. Source of the type system The type system enforced by the Initialization Checker is known as “Freedom Before Commitment” [SM11]. Our implementation changes its initialization modifiers (“committed”, “free”, and “unclassified”) to “initialized”, “unknown initialization”, and “under initialization”. Our implementation also has several enhancements. For example, it supports partial initialization (the argument to the @UnknownInitialization and @UnderInitialization annotations. 3.9.8 Rawness Initialization Checker The Checker Framework supports two different initialization checkers that are integrated with the Nullness Checker. You can use whichever one you prefer. One (described in most of Section 3.9) uses the three annotations @Initialized, @UnknownInitialization, and @UnderInitialization. We recommend that you use it. The other (described here in Section 3.9.8) uses the two annotations @Raw and @NonRaw. The rawness type system is slightly easier to use but slightly less expressive. 44 To run the Nullness Checker with the rawness variant of the Initialization Checker, invoke the NullnessRawnessChecker rather than the NullnessChecker; that is, supply the -processor org.checkerframework.checker.nullness.NullnessRawnessChecker command-line option to javac. Although @Raw roughly corresponds to @UnknownInitialization and @NonRaw roughly corresponds to @Initialized, the annotations are not aliased and you must use the ones that correspond to the type-checker that you are running. An object is raw from the time that its constructor starts until its constructor finishes. This is relevant to the Nullness Checker because while the constructor is executing — that is, before initialization completes — a @NonNull field may be observed to be null, until that field is set. In particular, the Nullness Checker issues a warning for code like this: public class MyClass { private @NonNull Object f; public MyClass(int x, int y) { // Error because constructor contains no assignment to this.f. // By the time the constructor exits, f must be initialized to a non-null value. } public MyClass(int x) { // Error because this.f is accessed before f is initialized. // At the beginning of the constructor’s execution, accessing this.f // yields null, even though field f has a non-null type. this.f.toString(); } public MyClass(int x, int y, int z) { m(); this.f = new Object(); } public void m() { // Error because this.f is accessed before f is initialized, // even though the access is not in a constructor. // When m is called from the constructor, accessing f yields null, // even though field f has a non-null type. this.f.toString(); } In general, code can depend that field f is not null, because the field is declared with a @NonNull type. However, this guarantee does not hold for a partially-initialized object. The Nullness Checker uses the @Raw annotation to indicate that an object is not yet fully initialized — that is, not all its @NonNull fields have been assigned. Rawness is mostly relevant within the constructor, or for references to this that escape the constructor (say, by being stored in a field or passed to a method before initialization is complete). Use of rawness annotations is rare in most code. The most common use for the @Raw annotation is for a helper routine that is called by constructor. For example: class MyClass { Object field1; Object field2; Object field3; public MyClass(String arg1) { this.field1 = arg1; init_other_fields(); } // A helper routine that initializes all the fields other than field1 45 @Raw Object @NonRaw Object @Raw Date @NonRaw Date Figure 3.7: Partial type hierarchy for the Rawness Initialization type system. @EnsuresNonNull({"field2", "field3"}) private void init_other_fields(@Raw MyClass this) { field2 = new Object(); field3 = new Object(); } } Rawness qualifiers The rawness hierarchy is shown in Figure 3.7. The rawness hierarchy contains these qualifiers: @Raw indicates a type that may contain a partially-initialized object. In a partially-initialized object, fields that are annotated as @NonNull may be null because the field has not yet been assigned. Within the constructor, this has @Raw type until all the @NonNull fields have been assigned. A partially-initialized object (this in a constructor) may be passed to a helper method or stored in a variable; if so, the method receiver, or the field, would have to be annotated as @Raw. @NonRaw indicates a type that contains a fully-initialized object. NonRaw is the default, so there is little need for a programmer to write this explicitly. @PolyRaw indicates qualifier polymorphism over rawness (see Section 24.2). If a reference has @Raw type, then all of its @NonNull fields are treated as @MonotonicNonNull: when read, they are treated as being @Nullable, but when written, they are treated as being @NonNull. The rawness hierarchy is orthogonal to the nullness hierarchy. It is legal for a reference to be @NonNull @Raw, @Nullable @Raw, @NonNull @NonRaw, or @Nullable @NonRaw. The nullness hierarchy tells you about the reference itself: might the reference be null? The rawness hierarchy tells you about the @NonNull fields in the referred-to object: might those fields be temporarily null in contravention of their type annotation? Figure 3.8 contains some examples. How an object becomes non-raw Within the constructor, this starts out with @Raw type. As soon as all of the @NonNull fields in class C have been initialized, then this is treated as @NonRaw(C). This means that this is still being initialized, but all initialization of C’s fields is complete, including all fields of supertypes. Eventually, when all constructors complete, the type is simply @NonRaw. The Nullness Checker issues an error if the constructor fails to initialize any @NonNull field. This ensures that the object is in a legal (non-raw) state by the time that the constructor exits. This is different than Java’s test for definite assignment (see JLS ch.16), which does not apply to fields (except blank final ones, defined in JLS §4.12.4) because fields have a default value of null. All @NonNull fields must either have a default in the field declaration, or be assigned in the constructor or in a helper method that the constructor calls. If your code initializes (some) fields in a helper method, you will need to annotate the helper method with an annotation such as @EnsuresNonNull({"field1", "field2"}) for all the fields that the helper method assigns. 46 Declarations class C { @NonNull Object f; @Nullable Object g; ... } @NonNull @NonRaw C a; @NonNull @Raw C b; @Nullable @NonRaw C c; @Nullable @Raw C d; Expression Expression’s nullness type, or checker error a a.f a.g b b.f b.g c c.f c.g d d.f d.g @NonNull @NonNull @Nullable @NonNull @MonotonicNonNull @Nullable @Nullable error: deref of nullable error: deref of nullable @Nullable error: deref of nullable error: deref of nullable Figure 3.8: Examples of the interaction between nullness and rawness. Declarations are shown at the left for reference, but the focus of the table is the expressions and their nullness type or error. Partial initialization So far, we have discussed rawness as if it is an all-or-nothing property: an object is fully raw until initialization completes, and then it is no longer raw. The full truth is a bit more complex: during the initialization process, an object can be partially initialized, and as the object’s superclass constructors complete, its rawness changes. The Nullness Checker lets you express such properties when necessary. Consider a simple example: class A { Object a; A() { a = new Object(); } } class B extends A { Object b; B() { super(); b = new Object(); } } Consider what happens during execution of new B(). 1. B’s constructor begins to execute. At this point, neither the fields of A nor those of B have been initialized yet. 2. B’s constructor calls A’s constructor, which begins to execute. No fields of A nor of B have been initialized yet. 3. A’s constructor completes. Now, all the fields of A have been initialized, and their invariants (such as that field a is non-null) can be depended on. However, because B’s constructor has not yet completed executing, the object being constructed is not yet fully initialized. When treated as an A (e.g., if only the A fields are accessed), the object is initialized (non-raw), but when treated as a B, the object is still raw. 47 4. B’s constructor completes. The object is fully initialized (non-raw), if B’s constructor was invoked via a new B() expression. On the other hand, if there was a class C extends B { ... }, and B’s constructor had been invoked from that, then the object currently under construction would not be fully initialized — it would only be initialized when treated as an A or a B, but not when treated as a C. At any moment during initialization, the superclasses of a given class can be divided into those that have completed initialization and those that have not yet completed initialization. More precisely, at any moment there is a point in the class hierarchy such that all the classes above that point are fully initialized, and all those below it are not yet initialized. As initialization proceeds, this dividing line between the initialized and raw classes moves down the type hierarchy. The Nullness Checker lets you indicate where the dividing line is between the initialized and non-initialized classes. You have two equivalent ways to indicate the dividing line: @Raw indicates the first class below the dividing line, or @NonRaw(classliteral) indicates the first class above the dividing line. When you write @Raw MyClass x;, that means that variable x is initialized for all superclasses of MyClass, and (possibly) uninitialized for MyClass and all subclasses. When you write @NonRaw(Foo.class) MyClass x;, that means that variable x is initialized for Foo and all its superclasses, and (possibly) uninitialized for all subclasses of Foo. If A is a direct superclass of B (as in the example above), then @Raw A x; and @NonRaw(B.class) A x; are equivalent declarations. Neither one is the same as @NonRaw A x;, which indicates that, whatever the actual class of the object that x refers to, that object is fully initialized. Since @NonRaw (with no argument) is the default, you will rarely see it written. The example above lists 4 moments during construction. At those moments, the type of the object being constructed is: 1. 2. 3. 4. @Raw Object @Raw Object @NonRaw(A.class) A @NonRaw(B.class) B Example As another example, consider the following 12 declarations: @Raw Object rO; @NonRaw(Object.class) Object nroO; Object o; @Raw A rA; @NonRaw(Object.class) A nroA; @NonRaw(A.class) A nraA; A a; // same as "@Raw A" @NonRaw(Object.class) B nroB; @Raw B rB; @NonRaw(A.class) B nraB; // same as "@Raw B" @NonRaw(B.class) B nrbB; B b; In the following table, the type in cell C1 is a supertype of the type in cell C2 if: C1 is at least as high and at least as far left in the table as C2 is. For example, nraA’s type is a supertype of those of rB, nraB, nrbB, a, and b. (The empty cells on the top row are real types, but are not expressible. The other empty cells are not interesting types.) @Raw Object rO; @NonRaw(Object.class) Object nroO; Object o; @Raw A rA; @NonRaw(Object.class) A nroA; @NonRaw(A.class) A nraA; A a; 48 @NonRaw(Object.class) B nroB; @Raw B rB; @NonRaw(A.class) B nraB; @NonRaw(B.class) B nrbB; B b; More details about rawness checking Suppressing warnings You can suppress warnings related to partially-initialized objects with @SuppressWarnings("rawness"). Do not confuse this with the unrelated @SuppressWarnings("rawtypes") annotation for non-instantiated generic types! Use of method annotations A method with a raw receiver often assumes that a few fields (but not all of them) are nonnull, and sometimes sets some more fields to non-null values. To express these concepts, use the @RequiresNonNull, @EnsuresNonNull, and @EnsuresNonNullIf method annotations; see Section 3.2.2. The terminology “raw” The name “raw” comes from a research paper that proposed this approach [FL03]. A better name might have been “not yet initialized” or “partially initialized”, but the term “raw” is now well-known. The @Raw annotation has nothing to do with the raw types of Java Generics. 49 Chapter 4 Map Key Checker The Map Key Checker tracks which values are keys for which maps. If variable v has type @KeyFor("m")..., then the value of v is a key in Map m. That is, the expression m.containsKey(v) evaluates to true. Section 3.2.4 describes how @KeyFor annotations enable the Nullness Checker (Chapter 3, page 25) to treat calls to Map.get more precisely by refining its result to @NonNull in some cases. You will not typically run the Map Key Checker. It is automatically run by other checkers, in particular the Nullness Checker. You can suppress warnings related to map keys with @SuppressWarnings("keyfor"); see Chapter 26, page 164. 4.1 Map key annotations These qualifiers are part of the Map Key type system: @KeyFor(String[] maps) indicates that the value assigned to the annotated variable is a key for at least the given maps. @UnknownKeyFor is used internally by the type system but should never be written by a programmer. It indicates that the value assigned to the annotated variable is not known to be a key for any map. It is the default type qualifier. @KeyForBottom is used internally by the type system but should never be written by a programmer. @UnknownKeyFor @KeyFor(map1) @KeyFor(map2) @KeyFor({map2,map3}) @KeyFor({map1,map2}) @KeyFor({map1,...,mapn}) @KeyForBottom Figure 4.1: The subtyping relationship of the Map Key Checker’s qualifiers. @KeyFor(A) is a supertype of @KeyFor(B) if and only if A is a subset of B. Qualifiers in gray are used internally by the type system but should never be written by a programmer. 50 4.2 Examples The Map Key Checker keeps track of which variables reference keys to which maps. A variable annotated with @KeyFor(mapSet) can only contain a value that is a key for all the maps in mapSet. For example: Map m, n; @KeyFor("m") String km; @KeyFor("n") String kn; @KeyFor({"m", "n"}) String kmn; km = kmn; // OK - a key for maps m and n is also a key for map m km = kn; // error: a key for map n is not necessarily a key for map m As with any annotation, use of the @KeyFor annotation may force you to slightly refactor your code. For example, this would be illegal: Map m; Collection<@KeyFor("m") String> coll; coll.add(x); // error: element type is @KeyFor("m") String, but x does not have that type m.put(x, ...); The example type-checks if you reorder the two calls: Map m; Collection<@KeyFor("m") String> coll; m.put(x, ...); // after this statement, x has type @KeyFor("m") String coll.add(x); // OK 4.3 Inference of @KeyFor annotations Within a method body, you usually do not have to write @KeyFor explicitly, because the checker infers it based on usage patterns. When the Map Key Checker encounters a run-time check for map keys, such as “if (m.containsKey(k)) ...”, then the Map Key Checker refines the type of k to @KeyFor("m") within the scope of the test (or until k is side-effected within that scope). The Map Key Checker also infers @KeyFor annotations based on iteration over a map’s key set or calls to put or containsKey. For more details about type refinement, see Section 25.4. Suppose we have these declarations: Map m = new Map (); String k = "key"; @KeyFor("m") String km; Ordinarily, the following assignment does not type-check: km = k; // Error since k is not known to be a key for map m. The following examples show cases where the Map Key Checker infers a @KeyFor annotation for variable k based on usage patterns, enabling the km = k assignment to type-check. m.put(k, ...); // At this point, the type of k is refined to @KeyFor("m") String. km = k; // OK if (m.containsKey(k)) { 51 // At this point, the type of k is refined to @KeyFor("m") String. km = k; // OK ... } else { km = k; // Error since k is not known to be a key for map m. ... } The following example shows a case where the Map Key Checker resets its assumption about the type of a field used as a key because that field may have been side-effected. class MyClass { private Map m; private String k; // The type of k defaults to @UnknownKeyFor String private @KeyFor("m") String km; public void myMethod() { if (m.containsKey(k)) { km = k; // OK: the type of k is refined to @KeyFor("m") String sideEffectFreeMethod(); km = k; // OK: the type of k is not affected by the method call // and remains @KeyFor("m") String otherMethod(); km = k; // error: At this point, the type of k is once again // @UnknownKeyFor String, because otherMethod might have // side-effected k such that it is no longer a key for map m. } } @SideEffectFree private void sideEffectFreeMethod() { ... } private void otherMethod() { ... } } 52 Chapter 5 Optional Checker for possibly-present data Java 8 introduced the Optional class, a container that is either empty or contains a non-null value. Using Optional is intended to help programmers remember to check whether data is present or not. However, Optional itself is prone to misuse. The article Nothing is better than the Optional type gives reasons to use regular nullable references rather than Optional. However, if you do use Optional, then the Optional Checker will help you avoid Optional’s pitfalls. Stuart Marks gave 7 rules to avoid problems with Optional: 1. 2. 3. 4. 5. Never, ever, use null for an Optional variable or return value. Never use Optional.get() unless you can prove that the Optional is present. Prefer alternative APIs over Optional.isPresent() and Optional.get(). It’s generally a bad idea to create an Optional for the specific purpose of chaining methods from it to get a value. If an Optional chain has a nested Optional chain, or has an intermediate result of Optional, it’s probably too complex. 6. Avoid using Optional in fields, method parameters, and collections. 7. Don’t use an Optional to wrap any collection type (List, Set, Map). Instead, use an empty collection to represent the absence of values. Rule #1 is guaranteed by the Nullness Checker (Chapter 3, page 25). Rules #2–#7 are guaranteed by the Optional Checker, described in this chapter. (Exception: Rule #5 is not yet implemented and will be checked by the Optional Checker in the future.) Use of the Optional Checker guarantees that your program will not suffer a NullPointerException nor a NoSuchElementException when calling methods on an expression of Optional type. 5.1 How to run the Optional Checker javac -processor optional MyFile.java ... 5.2 Optional annotations These qualifiers make up the Optional type system: @MaybePresent The annotated Optional container may or may not contain a value. This is the default type. @Present The annotated Optional container definitely contains a (non-null) value. @PolyPresent indicates qualifier polymorphism (see Section 24.2). The subtyping hierarchy of the Optional Checker’s qualifiers is shown in Figure 5.1. 53 @MaybePresent @Present Figure 5.1: The subtyping relationship of the Optional Checker’s qualifiers. 54 Chapter 6 Interning Checker If the Interning Checker issues no errors for a given program, then all reference equality tests (i.e., all uses of “==”) are proper; that is, == is not misused where equals() should have been used instead. Interning is a design pattern in which the same object is used whenever two different objects would be considered equal. Interning is also known as canonicalization or hash-consing, and it is related to the flyweight design pattern. Interning has two benefits: it can save memory, and it can speed up testing for equality by permitting use of ==. The Interning Checker prevents two types of errors in your code. First, == should be used only on interned values; using == on non-interned values can result in subtle bugs. For example: Integer x = new Integer(22); Integer y = new Integer(22); System.out.println(x == y); // prints false! The Interning Checker helps programmers to prevent such bugs. Second, the Interning Checker also helps to prevent performance problems that result from failure to use interning. (See Section 2.3 for caveats to the checker’s guarantees.) Interning is such an important design pattern that Java builds it in for these types: String, Boolean, Byte, Character, Integer, Short. Every string literal in the program is guaranteed to be interned (JLS §3.10.5), and the String.intern() method performs interning for strings that are computed at run time. The valueOf methods in wrapper classes always (Boolean, Byte) or sometimes (Character, Integer, Short) return an interned result (JLS §5.1.7). Users can also write their own interning methods for other types. It is a proper optimization to use ==, rather than equals(), whenever the comparison is guaranteed to produce the same result — that is, whenever the comparison is never provided with two different objects for which equals() would return true. Here are three reasons that this property could hold: 1. Interning. A factory method ensures that, globally, no two different interned objects are equals() to one another. (Not every value of the given type is necessarily interned; it is possible for two objects of the class to be equals() to one another, even if one of them is interned.) Interned objects should always be immutable. 2. Global control flow. The program’s control flow is such that the constructor for class C is called a limited number of times, and with specific values that ensure the results are not equals() to one another. Objects of class C can always be compared with ==. Such objects may be mutable or immutable. 3. Local control flow. Even though not all objects of the given type may be compared with ==, the specific objects that can reach a given comparison may be. For example, suppose that an array contains no duplicates. Then searching for the index of an element that is known to be in the array can use ==. To eliminate Interning Checker errors, you will need to annotate the declarations of any expression used as an argument to ==. Thus, the Interning Checker could also have been called the Reference Equality Checker. To run the Interning Checker, supply the -processor org.checkerframework.checker.interning.InterningChecker command-line option to javac. For examples, see Section 6.4. 55 Object @Interned Object Date @Interned Date @InternedDistinct Object @InternedDistinct Date Figure 6.1: Type hierarchy for the Interning type system. 6.1 Interning annotations These qualifiers are part of the Interning type system: @Interned indicates a type that includes only interned values (no non-interned values). @InternedDistinct indicates a type such that each value is not equals() to any other Java value. For details, see Section 6.2.2. @UnknownInterned indicates a type whose values might or might not be interned. It is used internally by the type system and is not written by programmers. @PolyInterned indicates qualifier polymorphism (see Section 24.2). @UsesObjectEquals is a class annotation (not a type annotation) that indicates that this class’s equals method is the same as that of Object. In other words, neither this class nor any of its superclasses overrides the equals method. Since Object.equals uses reference equality, this means that for such a class, == and equals are equivalent, and so the Interning Checker does not issue errors or warnings for either one. 6.2 Annotating your code with @Interned In order to perform checking, you must annotate your code with the @Interned type annotation. A type annotated with @Interned contains the canonical representation of an object: String s1 = ...; @Interned String s2 = ...; // type is (uninterned) "String" // type is "@Interned String" The Interning Checker ensures that only interned values can be assigned to s2. To specify that all objects of a given type are interned, annotate the class declaration: public @Interned class MyInternedClass { ... } This is equivalent to annotating every use of MyInternedClass, in a declaration or elsewhere. For example, enum classes are implicitly so annotated. 6.2.1 Implicit qualifiers The Interning Checker adds implicit qualifiers, reducing the number of annotations that must appear in your code (see Section 25.3). For example, String literals and the null literal are always considered interned, and object creation expressions (using new) are never considered @Interned unless they are annotated as such, as in @Interned Double internedDoubleZero = new @Interned Double(0); // canonical representation for Double zero For a complete description of all implicit interning qualifiers, see the Javadoc for InterningAnnotatedTypeFactory. 6.2.2 InternedDistinct: values not equals() to any other value The @InternedDistinct annotation represents values that are not equals() to any other value. Suppose expression e has type @InternedDistinct. Then e.equals(x) == (e == x). Therefore, it is legal to use == whenever at least one of the operands has type @InternedDistinct. @InternedDistinct is stronger (more restrictive) than @Interned. For example, consider these variables: 56 @Interned String i = "22"; String s = new Integer(22).toString(); The variable i is not @InternedDistinct because i.equals(s) is true. @InternedDistinct is not as restrictive as stating that all objects of a given Java type are interned. The @InternedDistinct annotation is rarely used, because it arises from coding paradigms that are tricky to reason about. One use is on static fields that hold canonical values of a type. Given this declaration: class MyType { final static @InternedDistinct MyType SPECIAL = new MyType(...); ... } it would be legal to write myValue == MyType.SPECIAL rather than myValue.equals(MyType.SPECIAL). The @InternedDistinct is trusted (not verified), because it would be too complex to analyze the equals() method to ensure that no other value is equals() to a @InternedDistinct value. You will need to manually verify that it is only written in locations where its contract is satisfied. For example, here is one set of guidelines that you could check manually: • The constructor is private. • The factory method returns the canonical version for certain values. • The class is final, so that subclasses cannot violate these properties. 6.3 What the Interning Checker checks Objects of an @Interned type may be safely compared using the “==” operator. The checker issues an error in two cases: 1. When a reference (in)equality operator (“==” or “!=”) has an operand of non-@Interned type. As a special case, the operation is permitted if either argument is of @InternedDistinct type 2. When a non-@Interned type is used where an @Interned type is expected. This example shows both sorts of problems: Date date; @Interned Date idate; @InternedDistinct Date ddate; ... if (date == idate) ... // error: reference equality test is unsafe idate = date; // error: idate’s referent might no longer be interned ddate = idate; // error: idate’s referent might be equals() to some other value The checker also issues a warning when .equals is used where == could be safely used. You can disable this behavior via the javac -Alint=-dotequals command-line option. For a complete description of all checks performed by the checker, see the Javadoc for InterningVisitor. You can also restrict which types the checker should examine and type-check, using the -Acheckclass option. For example, to find only the interning errors related to uses of String, you can pass -Acheckclass=java.lang.String. The Interning Checker always checks all subclasses and superclasses of the given class. 57 com.sun.istack.internal.Interned ⇒ org.checkerframework.checker.interning.qual.Interned Figure 6.2: Correspondence between other interning annotations and the Checker Framework’s annotations. 6.3.1 Limitations of the Interning Checker The Interning Checker conservatively assumes that the Character, Integer, and Short valueOf methods return a non-interned value. In fact, these methods sometimes return an interned value and sometimes a non-interned value, depending on the run-time argument (JLS §5.1.7). If you know that the run-time argument to valueOf implies that the result is interned, then you will need to suppress an error. (The Interning Checker should make use of the Value Checker to estimate the upper and lower bounds on char, int, and short values so that it can more precisely determine whether the result of a given valueOf call is interned.) 6.4 Examples To try the Interning Checker on a source file that uses the @Interned qualifier, use the following command: javac -processor org.checkerframework.checker.interning.InterningChecker docs/examples/InterningExample.java Compilation will complete without errors or warnings. To see the checker warn about incorrect usage of annotations, use the following command: javac -processor org.checkerframework.checker.interning.InterningChecker docs/examples/InterningExampleWithWarnings.java The compiler will issue an error regarding violation of the semantics of @Interned. The Daikon invariant detector (http://plse.cs.washington.edu/daikon/) is also annotated with @Interned. From directory java/, run make check-interning. 6.5 Other interning annotations The Checker Framework’s interning annotations are similar to annotations used elsewhere. If your code is already annotated with a different interning annotation, the Checker Framework can type-check your code. It treats annotations from other tools as if you had written the corresponding annotation from the Interning Checker, as described in Figure 6.2. If the other annotation is a declaration annotation, it may be moved; see Section 27.1.1. 58 Chapter 7 Lock Checker The Lock Checker prevents certain concurrency errors by enforcing a locking discipline. A locking discipline indicates which locks must be held when a given operation occurs. You express the locking discipline by declaring a variable’s type to have the qualifier @GuardedBy("lockexpr"). This indicates that the variable’s value may be dereferenced only if the given lock is held. To run the Lock Checker, supply the -processor org.checkerframework.checker.lock.LockChecker commandline option to javac. The -AconcurrentSemantics command-line option is always enabled for the Lock Checker (see Section 32.4.4). 7.1 What the Lock Checker guarantees The Lock Checker gives the following guarantee. Suppose that expression e has type @GuardedBy({"x", "y.z"}). Then the value computed for e is only dereferenced by a thread when the thread holds locks x and y.z. Dereferencing a value is reading or writing one of its fields. The guarantee about e’s value holds not only if the expression e is dereferenced directly, but also if the value was first copied into a variable, returned as the result of a method call, etc. Copying a reference is always permitted by the Lock Checker, regardless of which locks are held. A lock is held if it has been acquired but not yet released. Java has two types of locks. A monitor lock is acquired upon entry to a synchronized method or block, and is released on exit from that method or block. An explicit lock is acquired by a method call such as Lock.lock(), and is released by another method call such as Lock.unlock(). The Lock Checker enforces that any expression whose type implements Lock is used as an explicit lock, and all other expressions are used as monitor locks. Ensuring that your program obeys its locking discipline is an easy and effective way to eliminate a common and important class of errors. If the Lock Checker issues no warnings, then your program obeys its locking discipline. However, your program might still have other types of concurrency errors. For example, you might have specified an inadequate locking discipline because you forgot some @GuardedBy annotations. Your program might release and re-acquire the lock, when correctness requires it to hold it throughout a computation. And, there are other concurrency errors that cannot, or should not, be solved with locks. 7.2 Lock annotations This section describes the lock annotations you can write on types and methods. 7.2.1 Type qualifiers @GuardedBy(exprSet) If a variable x has type @GuardedBy("expr"), then a thread may dereference the value referred to by x only when the thread holds the lock that expr currently evaluates to. 59 @GuardedByUnknown @GuardedBy({}) @GuardedBy("a") @GuardedBy("b") @GuardedBy({"a","b"}) ... @GuardedByBottom Figure 7.1: The subtyping relationship of the Lock Checker’s qualifiers. @GuardedBy({}) is the default type qualifier for unannotated types (except all CLIMB-to-top locations other than upper bounds and exception parameters — see Section 25.3.2). The @GuardedBy annotation can list multiple expressions, as in @GuardedBy({"expr1", "expr2"}), in which case the dereference is permitted only if the thread holds all the locks. Section 25.5 explains which expressions the Lock Checker is able to analyze as lock expressions. These include , i.e. the value of the annotated reference (non-primitive) variable. For example, @GuardedBy(" ") Object o indicates that the value referenced by o is guarded by the intrinsic (monitor) lock of the value referenced by o. @GuardedBy({}), which means the value is always allowed to be dereferenced, is the default type qualifier that is used for all locations where the programmer does not write an explicit locking type qualifier (except all CLIMB-to-top locations other than upper bounds and exception parameters — see Section 25.3.2). (Section 7.5.4 discusses this choice.) It is also the conservative default type qualifier for method parameters in unannotated libraries (see Chapter 29, page 176). @GuardedByUnknown If a variable x has type @GuardedByUnknown, then it is not known which locks protect x’s value. Those locks might even be out of scope (inaccessible) and therefore unable to be written in the annotation. The practical consequence is that the value referred to by x can never be dereferenced. Any value can be assigned to a variable of type @GuardedByUnknown. In particular, if it is written on a formal parameter, then any value, including one whose locks are not currently held, may be passed as an argument. @GuardedByUnknown is the conservative default type qualifier for method receivers in unannotated libraries (see Chapter 29, page 176). @GuardedByBottom If a variable x has type @GuardedByBottom, then the value referred to by x is null and can never be dereferenced. Figure 7.1 shows the type hierarchy of these qualifiers. All @GuardedBy annotations are incomparable: if exprSet1 6= exprSet2, then @GuardedBy(exprSet1) and @GuardedBy(exprSet2) are siblings in the type hierarchy. You might expect that @GuardedBy({"x", "y"}) T is a subtype of @GuardedBy({"x"}) T. The first type requires two locks to be held, and the second requires only one lock to be held and so could be used in any situation where both locks are held. The type system conservatively prohibits this in order to prevent type-checking loopholes that would result from aliasing and side effects — that is, from having two mutable references, of different types, to the same data. See Section 7.4.2 for an example of a problem that would occur if this rule were relaxed. Polymorphic type qualifiers @GuardSatisfied(index) If a variable x has type @GuardSatisfied, then all lock expressions for x’s value are held. As with other qualifier-polymorphism annotations (Section 24.2), the index argument indicates when two values are guarded by the same (unknown) set of locks. @GuardSatisfied is only allowed in method signatures: on formal parameters (including the receiver) and return types. It may not be written on fields. Also, it is a limitation of the current design that @GuardSatisfied may not be written on array elements or on local variables. A return type can only be annotated with @GuardSatisfied(index), not @GuardSatisfied. See Section 7.4.6 for an example of a use of @GuardSatisfied. 60 7.2.2 Declaration annotations The Lock Checker supports several annotations that specify method behavior. These are declaration annotations, not type annotations: they apply to the method itself rather than to some particular type. Method pre-conditions and post-conditions @Holding(String[] locks) All the given lock expressions are held at the method call site. @EnsuresLockHeld(String[] locks) The given lock expressions are locked upon method return if the method terminates successfully. This is useful for annotating a method that acquires a lock such as ReentrantLock.lock(). @EnsuresLockHeldIf(String[] locks, boolean result) If the annotated method returns the given boolean value (true or false), the given lock expressions are locked upon method return if the method terminates successfully. This is useful for annotating a method that conditionally acquires a lock. See Section 7.4.4 for examples. Side effect specifications @LockingFree The method does not acquire or release locks, directly or indirectly. The method is not synchronized, it contains no synchronized blocks, it contains no calls to lock or unlock methods, and it contains no calls to methods that are not themselves @LockingFree. Since @SideEffectFree implies @LockingFree, if both are applicable then you only need to write @SideEffectFree. @ReleasesNoLocks The method maintains a strictly nondecreasing lock hold count on the current thread for any locks that were held prior to the method call. The method might acquire locks but then release them, or might acquire locks but not release them (in which case it should also be annotated with @EnsuresLockHeld or @EnsuresLockHeldIf). This is the default for methods being type-checked that have no @LockingFree, @MayReleaseLocks, @SideEffectFree, or @Pure annotation. @MayReleaseLocks The method may release locks that were held prior to the method being called. You can write this when you are certain the method releases locks, or when you don’t know whether the method releases locks. This is the conservative default for methods in unannotated libraries (see Chapter 29, page 176). 7.3 Type-checking rules In addition to the standard subtyping rules enforcing the subtyping relationship described in Figure 7.1, the Lock Checker enforces the following additional rules. 7.3.1 Polymorphic qualifiers @GuardSatisfied The overall rules for polymorphic qualifiers are given in Section 24.2. Here are additional constraints for (pseudo-)assignments: • If the left-hand side has type @GuardSatisfied (with or without an index), then all locks mentioned in the right-hand side’s @GuardedBy type must be currently held. • A formal parameter with type qualifier @GuardSatisfied without an index cannot be assigned to. • If the left-hand side is a formal parameter with type @GuardSatisfied(index), the right-hand-side must have identical @GuardSatisfied(index) type. If a formal parameter type is annotated with @GuardSatisfied without an index, then that formal parameter type is unrelated to every other type in the @GuardedBy hierarchy, including other occurrences of @GuardSatisfied without an index. @GuardSatisfied may not be used on formal parameters, receivers, or return types of a method annotated with @MayReleaseLocks. 61 7.3.2 Dereferences @GuardedBy An expression of type @GuardedBy(eset) may be dereferenced only if all locks in eset are held. @GuardSatisfied An expression of type @GuardSatisfied may be dereferenced. Not @GuardedBy or @GuardSatisfied An expression whose type is not annotated with @GuardedBy or @GuardSatisfied may not be dereferenced. 7.3.3 Primitive types, boxed primitive types, and Strings Primitive types, boxed primitive types (such as java.lang.Integer), and type java.lang.String are implicitly annotated with @GuardedBy({}). It is an error for the programmer to annotate any of these types with an annotation from the @GuardedBy type hierarchy, including @GuardedBy({}). 7.3.4 Overriding Overriding methods annotated with @Holding If class B overrides method m from class A, then the expressions in B’s @Holding annotation must be a subset of or equal to that of A’s @Holding annotation.. Overriding methods annotated with side effect annotations If class B overrides method m from class A, then the side effect annotation on B’s declaration of m must be at least as strong as that in A’s declaration of m. From weakest to strongest, the side effect annotations processed by the Lock Checker are: @MayReleaseLocks @ReleasesNoLocks @LockingFree @SideEffectFree @Pure 7.3.5 Side effects Releasing explicit locks Any method that releases an explicit lock must be annotated with @MayReleaseLocks. The Lock Checker issues a warning if it encounters a method declaration annotated with @MayReleaseLocks and having a formal parameter or receiver annotated with @GuardSatisfied. This is because the Lock Checker cannot guarantee that the guard will be satisfied throughout the body of a method if that method may release a lock. No side effects on lock expressions If expression expr is used to acquire a lock, then expr must evaluate to the same value, starting from when expr is used to acquire a lock until expr is used to release the lock. An expression is used to acquire a lock if it is the receiver at a call site of a synchronized method, is the expression in a synchronized block, or is the argument to a lock method. Locks are released after possible side effects After a call to a method annotated with @LockingFree, @ReleasesNoLocks, @SideEffectFree, or @Pure, the Lock Checker’s estimate of held locks after a method call is the same as that prior to the method call. After a call to a method annotated with @MayReleaseLocks, the estimate of held locks is conservatively reset to the empty set, except for those locks specified to be held after the call by an @EnsuresLockHeld or @EnsuresLockHeldIf annotation on the method. Assignments to variables also cause the estimate of held locks to be conservatively reduced to a smaller set if the Checker Framework determines that the assignment might have side-effected a lock expression. For more information on side effects, please refer to Section 25.4.5. 7.4 Examples The Lock Checker guarantees that a value that was computed from an expression of @GuardedBy type is dereferenced only when the current thread holds all the expressions in the @GuardedBy annotation. 62 7.4.1 Examples of @GuardedBy The following example demonstrates the basic type-checking rules. class MyClass { final ReentrantLock lock; // Initialized in the constructor @GuardedBy("lock") Object x = new Object(); @GuardedBy("lock") Object y = x; // OK, since dereferences of y will require "lock" to be held. @GuardedBy({}) Object z = x; // ILLEGAL since dereferences of z don’t require "lock" to be held. @GuardedBy("lock") Object myMethod() { // myMethod is implicitly annotated with @ReleasesNoLocks. return x; // OK because the return type is annotated with @GuardedBy("lock") } [...] void exampleMethod() { x.toString(); // ILLEGAL because the lock is not known to be held y.toString(); // ILLEGAL because the lock is not known to be held myMethod().toString(); // ILLEGAL because the lock is not known to be held lock.lock(); x.toString(); // OK: the lock is known to be held y.toString(); // OK: the lock is known to be held, and toString() is annotated with @SideEffectFree. myMethod().toString(); // OK: the lock is known to be held, since myMethod // is implicitly annotated with @ReleasesNoLocks. } } Note that the expression new Object() is inferred to have type @GuardedBy("lock") because it is immediately assigned to a newly-declared variable having type annotation @GuardedBy("lock"). You could explicitly write new @GuardedBy("lock") Object() but it is not required. The following example demonstrates that using as a lock expression allows a guarded value to be dereferenced even when the original variable name the value was originally assigned to falls out of scope. class MyClass { private final @GuardedBy(" ") Object x = new Object(); void method() { x.toString(); // ILLEGAL because x is not known to be held. synchronized(x) { x.toString(); // OK: x is known to be held. } } public @GuardedBy(" ") Object get_x() { return x; // OK, since the return type is @GuardedBy(" "). } } class MyOtherClass { void method() { MyClass m = new MyClass(); final @GuardedBy(" ") Object o = m.get_x(); o.toString(); // ILLEGAL because o is not known to be held. 63 synchronized(o) { o.toString(); // OK: o is known to be held. } } } 7.4.2 @GuardedBy({“a”, “b”}) is not a subtype of @GuardedBy({“a”}) @GuardedBy(exprSet) The following example demonstrates the reason the Lock Checker enforces the following rule: if exprSet1 6= exprSet2, then @GuardedBy(exprSet1) and @GuardedBy(exprSet2) are siblings in the type hierarchy. class MyClass { final Object lockA = new Object(); final Object lockB = new Object(); @GuardedBy("lockA") Object x = new Object(); @GuardedBy({"lockA", "lockB"}) Object y = new Object(); void myMethod() { y = x; // ILLEGAL; if legal, later statement x.toString() would cause trouble synchronized(lockA) { x.toString(); // dereferences y’s value without holding lock lockB } } } If the Lock Checker permitted the assignment y = x;, then the undesired dereference would be possible. 7.4.3 Examples of @Holding The following example shows the interaction between @GuardedBy and @Holding: void helper1(@GuardedBy("myLock") Object a) { a.toString(); // ILLEGAL: the lock is not held synchronized(myLock) { a.toString(); // OK: the lock is held } } @Holding("myLock") void helper2(@GuardedBy("myLock") Object b) { b.toString(); // OK: the lock is held } void helper3(@GuardedBy("myLock") Object d) { d.toString(); // ILLEGAL: the lock is not held } void myMethod2(@GuardedBy("myLock") Object e) { helper1(e); // OK to pass to another routine without holding the lock // (but helper1’s body has an error) e.toString(); // ILLEGAL: the lock is not held synchronized (myLock) { helper2(e); // OK: the lock is held helper3(e); // OK, but helper3’s body has an error } } 64 7.4.4 Examples of @EnsuresLockHeld and @EnsuresLockHeldIf @EnsuresLockHeld and @EnsuresLockHeldIf are primarily intended for annotating JDK locking methods, as in: package java.util.concurrent.locks; class ReentrantLock { @EnsuresLockHeld("this") public void lock(); @EnsuresLockHeldIf (expression="this", result=true) public boolean tryLock(); ... } They can also be used to annotate user methods, particularly for higher-level lock constructs such as a Monitor, as in this simplified example: public class Monitor { private final ReentrantLock lock; // Initialized in the constructor ... @EnsuresLockHeld("lock") public void enter() { lock.lock(); } ... } 7.4.5 Example of @LockingFree, @ReleasesNoLocks, and @MayReleaseLocks @LockingFree is useful when a method does not make any use of synchronization or locks but causes other side effects (hence @SideEffectFree is not appropriate). @SideEffectFree implies @LockingFree, therefore if both are applicable, you should only write @SideEffectFree. @ReleasesNoLocks has a weaker guarantee than @LockingFree, and @MayReleaseLocks provides no guarantees. private Object myField; private final ReentrantLock lock; // Initialized in the constructor private @GuardedBy("lock") Object x; // Initialized in the constructor [...] // This method does not use locks or synchronization, but it cannot // be annotated as @SideEffectFree since it alters myField. @LockingFree void myMethod() { myField = new Object(); } 65 @SideEffectFree int mySideEffectFreeMethod() { return 0; } @MayReleaseLocks void myUnlockingMethod() { lock.unlock(); } @ReleasesNoLocks void myLockingMethod() { lock.lock(); } @MayReleaseLocks void clientMethod() { if (lock.tryLock()) { x.toString(); // OK: the lock is held myMethod(); x.toString(); // OK: the lock is still held since myMethod is locking-free mySideEffectFreeMethod(); x.toString(); // OK: the lock is still held since mySideEffectFreeMethod is side-effect-free myUnlockingMethod(); x.toString(); // ILLEGAL: myUnlockingMethod may have released a lock } if (lock.tryLock()) { x.toString(); // OK: the lock is held myLockingMethod(); x.toString(); // OK: the lock is held } if (lock.isHeldByCurrentThread()) { x.toString(); // OK: the lock is known to be held } } 7.4.6 Polymorphism and method formal parameters with unknown guards The polymorphic @GuardSatisfied type annotation allows a method body to dereference the method’s formal parameters even if the @GuardedBy annotations on the actual parameters are unknown at the method declaration site. The declaration of StringBuffer.append(String str) is annotated as: @LockingFree public @GuardSatisfied(1) StringBuffer append(@GuardSatisfied(1) StringBuffer this, @GuardSatisfied(2) String str) The method manipulates the values of its arguments, so all their locks must be held. However, the declaration does not know what those are and they might not even be in scope at the declaration. Therefore, the declaration cannot use @GuardedBy and must use @GuardSatisfied. The arguments to @GuardSatisfied indicate that the receiver and result (which are the same value) are guarded by the same (unknown, possibly empty) set of locks, and the str parameter may be guarded by a different set of locks. 66 The @LockingFree annotation indicates that this method makes no use of locks or synchronization. Given these annotations on append, the following code type-checks: final ReentrantLock lock1, lock2; // Initialized in the constructor @GuardedBy("lock1") StringBuffer filename; @GuardedBy("lock2") StringBuffer extension; ... lock1.lock(); lock2.lock(); filename = filename.append(extension); 7.5 More locking details This section gives some details that are helpful for understanding how Java locking and the Lock Checker works. 7.5.1 Two types of locking: monitor locks and explicit locks Java provides two types of locking: monitor locks and explicit locks. • A synchronized(E) block acquires the lock on the value of E; similarly, a method declared using the synchronized method modifier acquires the lock on the method receiver when called. (More precisely, the current thread locks the monitor associated with the value of E; see JLS §17.1.) The lock is automatically released when execution exits the block or the method body, respectively. We use the term “monitor lock” for a lock acquired using a synchronized block or synchronized method modifier. • A method call, such as Lock.lock(), acquires a lock that implements the Lock interface. The lock is released by another method call, such as Lock.unlock(). We use the term “explicit lock” for a lock expression acquired in this way. You should not mix the two varieties of locking, and the Lock Checker enforces this. To prevent an object from being used both as a monitor and an explicit lock, the Lock Checker issues a warning if a synchronized(E) block’s expression E has a type that implements Lock. 7.5.2 Held locks and held expressions; aliasing Whereas Java locking is defined in terms of values, Java programs are written in terms of expressions. We say that a lock expression is held if the value to which the expression currently evaluates is held. The Lock Checker conservatively estimates the expressions that are held at each point in a program. The Lock Checker does not track aliasing (different expressions that evaluate to the same value); it only considers the exact expression used to acquire a lock to be held. After any statement that might side-effect a held expression or a lock expression, the Lock Checker conservatively considers the expression to be no longer held. Section 25.5 explains which Java expressions the Lock Checker is able to analyze as lock expressions. The @LockHeld and @LockPossiblyHeld type qualifiers are used internally by the Lock Checker and should never be written by the programmer. If you see a warning mentioning @LockHeld or @LockPossiblyHeld, please contact the Checker Framework developers as it is likely to indicate a bug in the Checker Framework. 7.5.3 Run-time checks for locking When you perform a run-time check for locking, such as if (explicitLock.isHeldByCurrentThread()){...} or if (Thread.holdsLock(monitorLock)){...}, then the Lock Checker considers the lock expression to be held within the scope of the test. For more details, see Section 25.4. 67 7.5.4 Discussion of default qualifier The default qualifier for unannotated types is @GuardedBy({}). This default forces you to write explicit @GuardSatisfied in method signatures in the common case that clients ensure that all locks are held. It might seem that @GuardSatisfied would be a better default for method signatures, but such a default would require even more annotations. The reason is that @GuardSatisfied cannot be used on fields. If @GuardedBy({}) is the default for fields but @GuardSatisfied is the default for parameters and return types, then getters, setters, and many other types of methods do not type-check without explicit lock qualifiers. 7.5.5 Discussion of @Holding A programmer might choose to use the @Holding method annotation in two different ways: to specify correctness constraints for a synchronization protocol, or to summarize intended usage. Both of these approaches are useful, and the Lock Checker supports both. Synchronization protocol @Holding can specify a synchronization protocol that is not expressible as locks over the parameters to a method. For example, a global lock or a lock on a different object might need to be held. By requiring locks to be held, you can create protocol primitives without giving up the benefits of the annotations and checking of them. Method summary that simplifies reasoning @Holding can be a method summary that simplifies reasoning. In this case, the @Holding doesn’t necessarily introduce a new correctness constraint; the program might be correct even if the lock were not already acquired. Rather, here @Holding expresses a fact about execution: when execution reaches this point, the following locks are known to be already held. This fact enables people and tools to reason intra- rather than inter-procedurally. In Java, it is always legal to re-acquire a lock that is already held, and the re-acquisition always works. Thus, whenever you write @Holding("myLock") void myMethod() { ... } it would be equivalent, from the point of view of which locks are held during the body, to write void myMethod() { synchronized (myLock) { ... } } // no-op: re-acquire a lock that is already held It is better to write a @Holding annotation rather than writing the extra synchronized block. Here are reasons: • The annotation documents the fact that the lock is intended to already be held; that is, the method’s contract requires that the lock be held when the method is called. • The Lock Checker enforces that the lock is held when the method is called, rather than masking a programmer error by silently re-acquiring the lock. • The version with a synchronized statement can deadlock if, due to a programmer error, the lock is not already held. The Lock Checker prevents this type of error. • The annotation has no run-time overhead. The lock re-acquisition consumes time, even if it succeeds. 68 net.jcip.annotations.GuardedBy org.checkerframework.checker.lock.qual.GuardedBy (for fields), or ⇒ org.checkerframework.checker.lock.qual.Holding (for methods) javax.annotation.concurrent.GuardedBy Figure 7.2: Correspondence between other lock annotations and the Checker Framework’s annotations. 7.6 Other lock annotations The Checker Framework’s lock annotations are similar to annotations used elsewhere. If your code is already annotated with a different lock annotation, the Checker Framework can type-check your code. It treats annotations from other tools as if you had written the corresponding annotation from the Lock Checker, as described in Figure 7.2. If the other annotation is a declaration annotation, it may be moved; see Section 27.1.1. 7.6.1 Relationship to annotations in Java Concurrency in Practice The book Java Concurrency in Practice [GPB+ 06] defines a @GuardedBy annotation that is the inspiration for ours. The book’s @GuardedBy serves two related but distinct purposes: • When applied to a field, it means that the given lock must be held when accessing the field. The lock acquisition and the field access may occur arbitrarily far in the future. • When applied to a method, it means that the given lock must be held by the caller at the time that the method is called — in other words, at the time that execution passes the @GuardedBy annotation. The Lock Checker renames the method annotation to @Holding, and it generalizes the @GuardedBy annotation into a type annotation that can apply not just to a field but to an arbitrary type (including the type of a parameter, return value, local variable, generic type parameter, etc.). Another important distinction is that the Lock Checker’s annotations express and enforce a locking discipline over values, just like the JLS expresses Java’s locking semantics; by contrast, JCIP’s annotations express a locking discipline that protects variable names and does not prevent race conditions. This makes the annotations more expressive and also more amenable to automated checking. It also accommodates the distinct meanings of the two annotations, and resolves ambiguity when @GuardedBy is written in a location that might apply to either the method or the return type. (The JCIP book gives some rationales for reusing the annotation name for two purposes. One rationale is that there are fewer annotations to learn. Another rationale is that both variables and methods are “members” that can be “accessed” and @GuardedBy creates preconditions for doing so. Variables can be accessed by reading or writing them (putfield, getfield), and methods can be accessed by calling them (invokevirtual, invokeinterface). This informal intuition is inappropriate for a tool that requires precise semantics.) 7.7 Possible extensions The Lock Checker validates some uses of locks, but not all. It would be possible to enrich it with additional annotations. This would increase the programmer annotation burden, but would provide additional guarantees. Lock ordering: Specify that one lock must be acquired before or after another, or specify a global ordering for all locks. This would prevent deadlock. Not-holding: Specify that a method must not be called if any of the listed locks are held. These features are supported by Clang’s thread-safety analysis. 69 Chapter 8 Index Checker for sequence bounds (arrays and strings) The Index Checker warns about potentially out-of-bounds accesses to sequence data structures, such as arrays and strings. The Index Checker prevents IndexOutOfBoundsExceptions that result from an index expression that might be negative or might be equal to or larger than the sequence’s length. It also prevents NegativeArraySizeExceptions that result from a negative array dimension in an array creation expression. (A caveat: the Index Checker does not check for arithmetic overflow. If an expression overflows, the Index Checker might fail to warn about a possible exception. This is unlikely to be a problem in practice unless you have an array whose length is Integer.MAX_VALUE.) The programmer can write annotations that indicate which expressions are indices for which sequences. The Index Checker prohibits any operation that may violate these properties, and the Index Checker takes advantage of these properties when verifying indexing operations. Typically, a programmer writes few annotations, because the Index Checker infers properties of indexes from the code around them. For example, it will infer that x is positive within the then block of an if (x > 0) statement. The programmer does need to write field types and method pre-conditions or post-conditions. For instance, if a method’s formal parameter is used as an index for myArray, the programmer might need to write an @IndexFor("myArray") annotation on the formal parameter’s types. The Index Checker checks fixed-size data structures, whose size is never changed after creation. A fixed-size data structure has no add or remove operation. Examples are strings and arrays, and you can add support for other fixed-size data structures (see Section 8.9). To run the Index Checker, run the command javac -processor index MyJavaFile.java Recall that in Java, type annotations are written before the type; in particular, array annotations appear immediately before “[]”. Here is how to declare a length-9 array of positive integers: @Positive int @ArrayLen(9) [] Multi-dimensional arrays are similar. Here is how to declare a length-2 array of length-4 arrays: String @ArrayLen(2) [] @ArrayLen(4) [] 8.1 Index Checker structure and annotations Internally, the Index Checker computes information about integers that might be indices: • the lower bound on an integer, such as whether it is known to be positive (Section 8.2) 70 • the upper bound on an integer, such as whether it is less than the length of a given sequence (Section 8.3) • whether an integer came from calling the JDK’s binary search routine on an array (Section 8.6) • whether an integer came from calling a string search routine (Section 8.7) and about sequence lengths: • the minimum length of a sequence, such “myArray contains at least 3 elements” (Section 8.4) • whether two sequences have the same length (Section 8.5) The Index Checker checks of all these properties at once, but this manual discusses each type system in a different section. There are some annotations that are shorthand for writing multiple annotations, each from a different type system: @IndexFor(String[] names) The value is a valid index for the named sequences. For example, the String.charAt(int) method is declared as class String { char charAt(@IndexFor("this") index) { ... } } More generally, a variable declared as @IndexFor("someArray") int i has type @IndexFor("someArray") int and its run-time value is guaranteed to be non-negative and less than the length of someArray. You could also express this as @NonNegative @LTLengthOf("someArray") int i, but @IndexFor("someArray") int i is more concise. @IndexOrHigh(String[] names) The value is non-negative and is less than or equal to the length of each named sequence. This type combines @NonNegative and @LTEqLengthOf. For example, the Arrays.fill method is declared as class Arrays { void fill(Object[] a, @IndexFor("#1") int fromIndex, @IndexOrHigh("#1") int toIndex, Object val) } @LengthOf(String[] names) The value is exactly equal to the length of the named sequences. In the implementation, this type aliases @IndexOrHigh, so writing it only adds documentation (although future versions of the Index Checker may use it to improve precision). @IndexOrLow(String[] names) The value is -1 or is a valid index for each named sequence. This type combines @GTENegativeOne and @LTLengthOf. @PolyIndex indicates qualifier polymorphism. This type combines @PolyLowerBound and @PolyUpperBound. For a description of qualifier polymorphism, see Section 24.2. @PolyLength is a special polymorphic qualifier that combines @PolySameLen and @PolyValue from the Constant Value Checker (see Chapter 19, page 119). @PolyLength exists as a shorthand for these two annotations, since they often appear together. 8.2 Lower bounds The Index Checker issues an error when a sequence is indexed by an integer that might be negative. The Lower Bound Checker uses a type system (Figure 8.1) with the following qualifiers: @Positive The value is 1 or greater, so it is not too low to be used as an index. Note that this annotation is trusted by the Constant Value Checker, so if the Constant Value Checker is run on code containing this annotation, the Lower Bound Checker must be run on the same code in order to guarantee soundness. @NonNegative The value is 0 or greater, so it is not too low to be used as an index. @GTENegativeOne The value is -1 or greater. It may not be used as an index for a sequence, because it might be too low. (“GTE” stands for “Greater Than or Equal to”.) @PolyLowerBound indicates qualifier polymorphism. For a description of qualifier polymorphism, see Section 24.2. 71 @UpperBoundUnknown @LTEqLengthOf("myArray") @LowerBoundUnknown @GTENegativeOne @LTLengthOf("myArray") @NonNegative @LTOMLengthOf("myArray") @Positive @UpperBoundBottom @LowerBoundBottom Figure 8.1: The two type hierarchies for integer types used by the Index Checker. On the left is a type system for lower bounds. On the right is a type system for upper bounds. Qualifiers written in gray should never be written in source code; they are used internally by the type system. "myArray" in the Upper Bound qualifiers is an example of an array’s name. @LowerBoundUnknown There is no information about the value. It may not be used as an index for a sequence, because it might be too low. @LowerBoundBottom The value cannot take on any integral types. The bottom type, which should not need to be written by the programmer. 8.3 Upper bounds The Index Checker issues an error when a sequence index might be too high. To do this, it maintains information about which expressions are safe indices for which sequences. The length of a sequence is arr.length for arrays and str.length() for strings. It uses a type system (Figure 8.1) with the following qualifiers: It issues an error when a sequence arr is indexed by an integer that is not of type @LTLengthOf("arr") or @LTOMLengthOf("arr"). @LTLengthOf(String[] names, String[] offset) An expression with this type has value less than the length of each sequence listed in names. The expression may be used as an index into any of those sequences, if it is non-negative. For example, an expression of type @LTLengthOf("a") int might be used as an index to a. The type @LTLengthOf({"a", "b"}) is a subtype of both @LTLengthOf("a") and @LTLengthOf("b"). (“LT” stands for “Less Than”.) @LTLengthOf takes an optional offset element, meaning that the annotated expression plus the offset is less than the length of the given sequence. For example, suppose expression e has type @LTLengthOf(value = {"a", "b"}, offset = {"-1", "x"}). Then e - 1 is less than a.length, and e + x is less than b.length. This helps to make the checker more precise. Programmers rarely need to write the offset element. @LTEqLengthOf(String[] names) An expression with this type has value less than or equal to the length of each sequence listed in names. It may not be used as an index for these sequences, because it might be too high. @LTEqLengthOf({"a", "b"}) is a subtype of both @LTEqLengthOf("a") and @LTEqLengthOf("b"). (“LTEq” stands for “Less Than or Equal to”.) @PolyUpperBound indicates qualifier polymorphism. For a description of qualifier polymorphism, see Section 24.2. 72 @LTOMLengthOf(String[] names) An expression with this type has value at least 2 less than the length of each sequence listed in names. It may always used as an index for a sequence listed in names, if it is non-negative. This type exists to allow the checker to infer the safety of loops of the form: for (int i = 0; i < array.length - 1; ++i) { arr[i] = arr[i+1]; } This annotation should rarely (if ever) be written by the programmer; usually @LTLengthOf(String[] names) should be written instead. @LTOMLengthOf({"a", "b"}) is a subtype of both @LTOMLengthOf("a") and @LTOMLengthOf("b"). (“LTOM” stands for “Less Than One Minus”, because another way of saying “at least 2 less than a.length” is “less than a.length-1”.) @UpperBoundUnknown There is no information about the upper bound on the value of an expression with this type. It may not be used as an index for a sequence, because it might be too high. This type is the top type, and should never need to be written by the programmer. @UpperBoundBottom This is the bottom type for the upper bound type system. It should never need to be written by the programmer. The following method annotations can be used to establish a postcondition of a method which ensures that a certain expression is a valid index for a sequence: @EnsuresLTLengthOf(String[] value, String[] targetValue, String[] offset) When the method with this annotation returns, the expression (or all the expressions) given in the value element is less than the length of the given sequences with the given offsets. More preciesly, the expression has the @LTLengthOf qualifier with the value and offset arguments taken from the targetValue and offset elements of this annotation. @EnsuresLTLengthOfIf(String[] expression, boolean result, String[] targetValue, String[] of If the method with this annotation returns the given boolean value, then the given expression (or all the given expressions) is less than the length of the given sequences with the given offsets. 8.4 Sequence minimum lengths The Index Checker estimates, for each sequence expression, how long its value might be at run time by computing a minimum length that the sequence is guaranteed to have. This enables the Index Checker to verify indices that are compile-time constants. For example, this code: String getThirdElement(String[] arr) { return arr[2]; } is legal if arr has at least three elements, which can be indicated in this way: String getThirdElement(String @MinLen(3) [] arr) { return arr[2]; } When the index is not a compile-time constant, as in arr[i], then the Index Checker depends not on a @MinLen annotation but on i being annotated as @LTLengthOf("arr"). The MinLen type qualifier is implemented in practice by the Constant Value Checker, using @ArrayLenRange annotations (see Chapter 19, page 119). This means that errors related to the minimum lengths of arrays must be suppressed using the "value" argument to @SuppressWarnings. @ArrayLenRange and @ArrayLen annotations can also be used to establish the minimum length of a sequence, if a more precise estimate of length is known. For example, if arr is known to have exactly three elements: 73 @SameLenUnknown @SameLen("a") @SameLen("b") @SameLen({"a", "b"}) @SameLenBottom Figure 8.2: The type hierarchy for arrays of equal length ("a" and "b" are assumed to be in-scope sequences). Qualifiers written in gray should never be written in source code; they are used internally by the type system. String getThirdElement(String @ArrayLen(3) [] arr) { return arr[2]; } The following type qualifiers (from the Chapter 19, page 119) can establish the minimum length of a sequence: @MinLen(int value) The value of an expression of this type is a sequence with at least value elements. The default annotation is @MinLen(0), and it may be applied to non-sequences. @MinLen(x) is a subtype of @MinLen(x − 1). An @MinLen annotation is treated internally as an @ArrayLenRange with only its from field filled. @ArrayLen(int[] value) The value of an expression of this type is a sequence whose length is exactly one of the integers listed in its argument. The argument can contain at most ten integers; larger collections of integers are converted to @ArrayLenRange annotations. The minimum length of a sequence with this annotation is the smallest element of the argument. @ArrayLenRange(int from, int to) The value of an expression of this type is a sequence whose length is bounded by its arguments, inclusive. The minimum length of a sequence with this annotation is its from argument. The following method annotation can be used to establish a postcondition of a method which ensures that a certain sequence has a minimum length: @EnsuresMinLenIf(String[] expression, boolean result, int targetValue) If the method with this annotation returns the given boolean value, then the given expression (or all the given expressions) is a sequence with at least targetValue elements. 8.5 Sequences of the same length The Index Checker determines whether two or more sequences have the same length. This enables it to verify that all the indexing operations are safe in code like the following: boolean lessThan(double[] arr1, double @SameLen("#1") [] arr2) { for (int i = 0; i < arr1.length; i++) { if (arr1[i] < arr2[i]) { return true; } else if (arr1[i] > arr2[i]) { 74 @SearchIndexUnknown @SearchIndex("a") @SearchIndex({"a", "b}) @NegativeIndexFor("a") @NegativeIndexFor({"a", "b"}) @SearchIndexBottom Figure 8.3: The type hierarchy for the Index Checker’s internal type system that captures information about the results of calls to Arrays.binarySearch. return false; } } return false; } When needed, you can specify which sequences have the same length using the following type qualifiers (Figure 8.2): @SameLen(String[] names) An expression with this type represents a sequence that has the same length as the other sequences named in names. In general, @SameLen types that have non-intersecting sets of names are not subtypes of each other. However, if at least one sequence is named by both types, the types are actually the same, because all the named sequences must have the same length. @PolySameLen indicates qualifier polymorphism. For a description of qualifier polymorphism, see Section 24.2. @SameLenUnknown No information is known about which other sequences have the same length as this one. This is the top type, and programmers should never need to write it. @SameLenBottom This is the bottom type, and programmers should rarely need to write it. null has this type. 8.6 Binary search indices The JDK’s Arrays.binarySearch method returns either where the value was found, or a negative value indicating where the value could be inserted. The Search Index Checker represents this concept. The Search Index Checker’s type hierarchy (Figure 8.3) has four type qualifiers: @SearchIndexFor(String[] names) An expression with this type represents an integer that could have been produced by calling Arrays.binarySearch: for each array a specifed in the annotation, the annotated integer is between -a.length-1 and a.length-1, inclusive @NegativeIndexFor(String[] names) An expression with this type represents a “negative index” that is between a.length-1 and -1, inclusive; that is, a value that is both a @SearchIndex and is negative. Applying the bitwise complement operator (~) to an expression of this type produces an expression of type @IndexOrHigh. @SearchIndexBottom This is the bottom type, and programmers should rarely need to write it. 75 @SubstringIndexUnknown @SubstringIndexFor(value="myStr", offset="subStr.length()-1") @SubstringIndexBottom Figure 8.4: The type hierarchy for the Substring Index Checker, which captures information about the results of calls to String.indexOf and String.lastIndexOf. @SearchIndexUnknown No information is known about whether this integer is a search index. This is the top type, and programmers should rarely need to write it. 8.7 Substring indices The methods String.indexOf and String.lastIndexOf return an index of a given substring within a given string, or -1 if no such substring exists. The index i returned from receiver.indexOf(substring) satisfies the following property, which is stated here in three equivalent ways: i == -1 || ( i >= 0 && i <= receiver.length() - substring.length() ) i == -1 || ( @NonNegative && @LTLengthOf(value="receiver", offset="substring.length()-1") ) @SubstringIndexFor(value="receiver", offset="substring.length()-1") The return type of methods String.indexOf and String.lastIndexOf has the annotation @SubstringIndexFor( value="this", offset="#1.length()-1")). This allows writing code such as the following with no warnings from the Index Checker: public static String removeSubstring(String original, String removed) { int i = original.indexOf(removed); if (i != -1) { return original.substring(0, i) + original.substring(i + removed.length()); } return original; } The @SubstringIndexFor annotation is implemented in a Substring Index Checker that runs together with the Index Checker and has its own type hierarchy (Figure 8.4) with three type qualifiers: @SubstringIndexFor(String[] value, String[] offset) An expression with this type represents an integer that could have been produced by calling String.indexOf: the annotated integer is either -1, or it is non-negative and is less than or equal to receiver.length - offset (where the sequence receiver and the offset offset are corresponding elements of the annotation’s arguments). @SubstringIndexBottom This is the bottom type, and programmers should rarely need to write it. @SubstringIndexUnknown No information is known about whether this integer is a substring index. This is the top type, and programmers should rarely need to write it. 8.7.1 The need for the @SubstringIndexFor annotation No other annotation supported by the Index Checker precisely represents the possible return values of methods String.indexOf and String.lastIndexOf. The reason is the methods’ special cases for empty strings and for failed 76 matches. Consider the result i of receiver.indexOf(substring): • i is @GTENegativeOne, because i >= -1. • i is @LTEqLengthOf("receiver"), because i <= receiver.length(). • i is not @IndexOrLow("receiver"), because for receiver = "", substring = "", i = 0, the property i >= -1 && i < receiver.length() does not hold. • i is not @IndexOrHigh("receiver"), because for receiver = "", substring = "b", i = -1, the property i >= 0 && i <= receiver.length() does not hold. • i is not @LTLengthOf(value = "receiver", offset = "substring.length()-1"), because for receiver = "", substring = "abc", i = -1, the property i + substring.length() - 1 < receiver.length() does not hold. The last annotation in the list above, @LTLengthOf(value = "receiver", offset = "substring.length()-1"), is the correct and precise upper bound for all values of i except -1. The offset expresses the fact that we can add substring.length() to this index and still get a valid index for receiver. That is useful for type-checking code that adds the length of the substring to the found index, in order to obtain the rest of the string. However, the upper bound applies only after the index is explicitly checked not to be -1: int i = receiver.indexOf(substring); // i is @GTENegativeOne and @LTEqLengthOf("receiver") // i is not @LTLengthOf(value = "receiver", offset = "substring.length()-1") if (i != -1) { // i is @NonNegative and @LTLengthOf(value = "receiver", offset = "substring.length()-1") int j = i + substring.length(); // j is @IndexOrHigh("receiver") return receiver.substring(j); // this call is safe } The property of the result of indexOf cannot be expressed by any combination of lower-bound (Section 8.2) and upper-bound (Section 8.3) annotations, because the upper-bound annotations apply independently of the lower-bound annotations, but in this case, the upper bound i <= receiver.length() - substring.length() holds only if i >= 0. Therefore, to express this property and make the example type-check without false positives, a new annotation such as @SubstringIndexFor(value = "receiver", offset = "substring.length()-1") is necessary. 8.8 Inequalities The Index Checker estimates which expression’s values are less than other expressions’ values. @LessThan(String[] values) An expression with this type has a value that is less than the value of each expression listed in values. The expressions in values must be composed of final or effectively final variables and constants. @LessThanUnknown There is no information about the value of an expression this type relative to other expressions. This is the top type, and should not be written by the programer. @LessThanBottom This is the bottom type for the less than type system. It should never need to be written by the programmer. 8.9 Annotating fixed-size data structures The Index Checker has built-in support for Strings and arrays. You can add support for additional fixed-size data structures by writing annotations. This allows the Index Checker to typecheck the data structure’s implementation and to typecheck uses of the class. This section gives an example: a fixed-length collection. 77 /** ArrayWrapper is a fixed-size generic collection. */ public class ArrayWrapper { private final Object @SameLen("this") [] delegate; @SuppressWarnings("index") // constructor creates object of size @SameLen(this) by definition ArrayWrapper(@NonNegative int size) { delegate = new Object[size]; } public @LengthOf("this") int size() { return delegate.length; } public void set(@IndexFor("this") int index, T obj) { delegate[index] = obj; } @SuppressWarnings("unchecked") // required for normal Java compilation due to unchecked cast public T get(@IndexFor("this") int index) { return (T) delegate[index]; } } The Index Checker treats methods annotated with @LengthOf("this") as the length of a sequence like arr.length for arrays and str.length() for strings. With these annotations, client code like the following typechecks with no warnings: public static void clearIndex1(ArrayWrapper extends Object> a, @IndexFor("#1") int i) { a.set(i, null); } public static void clearIndex2(ArrayWrapper extends Object> a, int i) { if (0 <= i && i < a.size()) { a.set(i, null); } } 78 Chapter 9 Fake Enum Checker for fake enumerations The Fake Enum Checker, or Fenum Checker, enables you to define a type alias or typedef, in which two different sets of values have the same representation (the same Java type) but are not allowed to be used interchangeably. It is also possible to create a typedef using the Subtyping Checker (Chapter 22, page 132), and that approach is sometimes more appropriate. One common use for the Fake Enum Checker is the fake enumeration pattern (Section 9.6). For example, consider this code adapted from Android’s IntDef documentation: @NavigationMode int NAVIGATION_MODE_STANDARD = 0; @NavigationMode int NAVIGATION_MODE_LIST = 1; @NavigationMode int NAVIGATION_MODE_TABS = 2; @NavigationMode int getNavigationMode(); void setNavigationMode(@NavigationMode int mode); The Fake Enum Checker can issue a compile-time warning if the programmer ever tries to call setNavigationMode with an int that is not a @NavigationMode int. The Fake Enum Checker gives the same safety guarantees as a true enumeration type or typedef, but retaining backward-compatibility with interfaces that use existing Java types. You can apply fenum annotations to any Java type, including all primitive types and also reference types. Thus, you could use it (for example) to represent floating-point values between 0 and 1, or Strings with some particular characteristic. (Note that the Fake Enum Checker does not let you create a shorter alias for a long type name, as a real typedef would if Java supported it.) As explained in Section 9.1, you can either define your own fenum annotations, such as @NavigationMode above, or you can use the existing @Fenum with a string argument. Figure 9.1 shows part of the type hierarchy for the Fenum type system. 9.1 Fake enum annotations The Fake Enum Checker supports two ways to introduce a new fake enum (fenum): 1. Introduce your own specialized fenum annotation with code like this in file MyFenum.java: package myPackage.qual; import import import import java.lang.annotation.Documented; java.lang.annotation.ElementType; java.lang.annotation.Retention; java.lang.annotation.RetentionPolicy; 79 @FenumTop @Fenum("A") @Fenum("B") @FenumC ... @FenumD ... @FenumUnqualified @FenumBottom Figure 9.1: Partial type hierarchy for the Fenum type system. There are two forms of fake enumeration annotations — above, illustrated by @Fenum("A") and @FenumC. See Section 9.1 for descriptions of how to introduce both types of fenums. The type qualifiers in gray (@FenumTop, @FenumUnqualified, and @FenumBottom) should never be written in source code; they are used internally by the type system. @FenumUnqualified is the default qualifier for unannotated types, except for upper bounds which default to @FenumTop. import java.lang.annotation.Target; import org.checkerframework.checker.fenum.qual.FenumTop; import org.checkerframework.framework.qual.SubtypeOf; @Documented @Retention(RetentionPolicy.RUNTIME) @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) @SubtypeOf(FenumTop.class) public @interface MyFenum {} You only need to adapt the italicized package, annotation, and file names in the example. Note that all custom annotations must have the @Target({ElementType.TYPE_USE}) meta-annotation. See section 30.4.1. 2. Use the provided @Fenum annotation, which takes a String argument to distinguish different fenums or type aliases. For example, @Fenum("A") and @Fenum("B") are two distinct type qualifiers. The first approach allows you to define a short, meaningful name suitable for your project, whereas the second approach allows quick prototyping. 9.2 What the Fenum Checker checks The Fenum Checker ensures that unrelated types are not mixed. All types with a particular fenum annotation, or @Fenum(...) with a particular String argument, are disjoint from all unannotated types and from all types with a different fenum annotation or String argument. The checker ensures that only compatible fenum types are used in comparisons and arithmetic operations (if applicable to the annotated type). It is the programmer’s responsibility to ensure that fields with a fenum type are properly initialized before use. Otherwise, one might observe a null reference or zero value in the field of a fenum type. (The Nullness Checker (Chapter 3, page 25) can prevent failure to initialize a reference variable.) 9.3 Running the Fenum Checker The Fenum Checker can be invoked by running the following commands. • If you define your own annotation(s), provide the name(s) of the annotation(s) through the -Aquals option, using a comma-no-space-separated notation: 80 javac -classpath /full/path/to/myProject/bin:/full/path/to/myLibrary/bin \ -processor org.checkerframework.checker.fenum.FenumChecker \ -Aquals=myPackage.qual.MyFenum MyFile.java ... The annotations listed in -Aquals must be accessible to the compiler during compilation in the classpath. In other words, they must already be compiled (and, typically, be on the javac classpath) before you run the Fenum Checker with javac. It is not sufficient to supply their source files on the command line. You can also provide the fully-qualified paths to a set of directories that contain the annotations through the -AqualDirs option, using a colon-no-space-separated notation. For example: javac -classpath /full/path/to/myProject/bin:/full/path/to/myLibrary/bin \ -processor org.checkerframework.checker.fenum.FenumChecker \ -AqualDirs=/full/path/to/myProject/bin:/full/path/to/myLibrary/bin MyFile.java ... Note that in these two examples, the compiled class file of the myPackage.qual.MyFenum annotation must exist in either the myProject/bin directory or the myLibrary/bin directory. The following placement of the class file will work with the above commands: .../myProject/bin/myPackage/qual/MyFenum.class The two options can be used at the same time to provide groups of annotations from directories, and individually named annotations. • If your code uses the @Fenum annotation, you do not need the -Aquals or -AqualDirs option: javac -processor org.checkerframework.checker.fenum.FenumChecker MyFile.java ... For an example of running the Fake Enum Checker on Android code, see https://github.com/karlicoss/ checker-fenum-android-demo. 9.4 Suppressing warnings One example of when you need to suppress warnings is when you initialize the fenum constants to literal values. To remove this warning message, add a @SuppressWarnings annotation to either the field or class declaration, for example: @SuppressWarnings("fenum:assignment.type.incompatible") // initialization of fake enums class MyConsts { public static final @Fenum("A") int ACONST1 = 1; public static final @Fenum("A") int ACONST2 = 2; } 9.5 Example The following example introduces two fenums in class TestStatic and then performs a few typical operations. @SuppressWarnings("fenum:assignment.type.incompatible") public class TestStatic { public static final @Fenum("A") int ACONST1 = 1; public static final @Fenum("A") int ACONST2 = 2; // initialization of fake enums public static final @Fenum("B") int BCONST1 = 4; public static final @Fenum("B") int BCONST2 = 5; } class FenumUser { @Fenum("A") int state1 = TestStatic.ACONST1; @Fenum("B") int state2 = TestStatic.ACONST1; 81 // ok // Incompatible fenums forbidden! void fenumArg(@Fenum("A") int p) {} void foo() state1 = state1 = state1 = { 4; TestStatic.BCONST1; TestStatic.ACONST2; fenumArg(5); fenumArg(TestStatic.BCONST1); fenumArg(TestStatic.ACONST1); // Direct use of value forbidden! // Incompatible fenums forbidden! // ok // Direct use of value forbidden! // Incompatible fenums forbidden! // ok } } Also, see the example project in the docs/examples/fenum-extension directory. 9.6 The fake enumeration pattern Java’s enum keyword lets you define an enumeration type: a finite set of distinct values that are related to one another but are disjoint from all other types, including other enumerations. Before enums were added to Java, there were two ways to encode an enumeration, both of which are error-prone: the fake enum pattern a set of int or String constants (as often found in older C code). the typesafe enum pattern a class with private constructor. Sometimes you need to use the fake enum pattern, rather than a real enum or the typesafe enum pattern. One reason is backward-compatibility. A public API that predates Java’s enum keyword may use int constants; it cannot be changed, because doing so would break existing clients. For example, Java’s JDK still uses int constants in the AWT and Swing frameworks, and Android also uses int constants rather than Java enums. Another reason is performance, especially in environments with limited resources. Use of an int instead of an object can reduce code size, memory requirements, and run time. In cases when code has to use the fake enum pattern, the Fake Enum Checker, or Fenum Checker, gives the same safety guarantees as a true enumeration type. The developer can introduce new types that are distinct from all values of the base type and from all other fake enums. Fenums can be introduced for primitive types as well as for reference types. 9.7 References • Case studies of the Fake Enum Checker: “Building and using pluggable type-checkers” [DDE+ 11] (ICSE 2011, http://homes.cs.washington.edu/ ~mernst/pubs/pluggable-checkers-icse2011.pdf#page=3) • Java Language Specification on enums: https://docs.oracle.com/javase/specs/jls/se8/html/jls-8.html#jls-8.9 • Tutorial trail on enums: https://docs.oracle.com/javase/tutorial/java/javaOO/enum.html • Typesafe enum pattern: http://www.oracle.com/technetwork/java/page1-139488.html • Java Tip 122: Beware of Java typesafe enumerations: https://www.javaworld.com/article/2077487/core-java/java-tip-122--beware-of-java-typesafe-enumeration html 82 Chapter 10 Tainting Checker The Tainting Checker prevents certain kinds of trust errors. A tainted, or untrusted, value is one that comes from an arbitrary, possibly malicious source, such as user input or unvalidated data. In certain parts of your application, using a tainted value can compromise the application’s integrity, causing it to crash, corrupt data, leak private data, etc. For example, a user-supplied pointer, handle, or map key should be validated before being dereferenced. As another example, a user-supplied string should not be concatenated into a SQL query, lest the program be subject to a SQL injection attack. A location in your program where malicious data could do damage is called a sensitive sink. A program must “sanitize” or “untaint” an untrusted value before using it at a sensitive sink. There are two general ways to untaint a value: by checking that it is innocuous/legal (e.g., it contains no characters that can be interpreted as SQL commands when pasted into a string context), or by transforming the value to be legal (e.g., quoting all the characters that can be interpreted as SQL commands). A correct program must use one of these two techniques so that tainted values never flow to a sensitive sink. The Tainting Checker ensures that your program does so. If the Tainting Checker issues no warning for a given program, then no tainted value ever flows to a sensitive sink. However, your program is not necessarily free from all trust errors. As a simple example, you might have forgotten to annotate a sensitive sink as requiring an untainted type, or you might have forgotten to annotate untrusted data as having a tainted type. To run the Tainting Checker, supply the -processor TaintingChecker command-line option to javac. 10.1 Tainting annotations The Tainting type system uses the following annotations: • @Untainted indicates a type that includes only untainted (trusted) values. • @Tainted indicates a type that may include tainted (untrusted) or untainted (trusted) values. @Tainted is a supertype of @Untainted. It is the default qualifier. • @PolyTainted is a qualifier that is polymorphic over tainting (see Section 24.2). 10.2 Tips on writing @Untainted annotations Most programs are designed with a boundary that surrounds sensitive computations, separating them from untrusted values. Outside this boundary, the program may manipulate malicious values, but no malicious values ever pass the boundary to be operated upon by sensitive computations. In some programs, the area outside the boundary is very small: values are sanitized as soon as they are received from an external source. In other programs, the area inside the boundary is very small: values are sanitized only immediately before being used at a sensitive sink. Either approach can work, so long as every possibly-tainted value is sanitized before it reaches a sensitive sink. 83 Once you determine the boundary, annotating your program is easy: put @Tainted outside the boundary, @Untainted inside, and @SuppressWarnings("tainting") at the validation or sanitization routines that are used at the boundary. The Tainting Checker’s standard default qualifier is @Tainted (see Section 25.3.1 for overriding this default). This is the safest default, and the one that should be used for all code outside the boundary (for example, code that reads user input). You can set the default qualifier to @Untainted in code that may contain sensitive sinks. The Tainting Checker does not know the intended semantics of your program, so it cannot warn you if you misannotate a sensitive sink as taking @Tainted data, or if you mis-annotate external data as @Untainted. So long as you correctly annotate the sensitive sinks and the places that untrusted data is read, the Tainting Checker will ensure that all your other annotations are correct and that no undesired information flows exist. As an example, suppose that you wish to prevent SQL injection attacks. You would start by annotating the Statement class to indicate that the execute operations may only operate on untainted queries (Chapter 29 describes how to annotate external libraries): public boolean execute(@Untainted String sql) throws SQLException; public boolean executeUpdate(@Untainted String sql) throws SQLException; 10.3 @Tainted and @Untainted can be used for many purposes The @Tainted and @Untainted annotations have only minimal built-in semantics. In fact, the Tainting Checker provides only a small amount of functionality beyond the Subtyping Checker (Chapter 22). This lack of hard-coded behavior has two consequences. The first consequence is that the annotations can serve many different purposes, such as: • Prevent SQL injection attacks: @Tainted is external input, @Untainted has been checked for SQL syntax. • Prevent cross-site scripting attacks: @Tainted is external input, @Untainted has been checked for JavaScript syntax. • Prevent information leakage: @Tainted is secret data, @Untainted may be displayed to a user. The second consequence is that the Tainting Checker is not useful unless you annotate the appropriate sources, sinks, and untainting/sanitization routines. If you want more specialized semantics, or you want to annotate multiple types of tainting (for example, HTML and SQL) in a single program, then you can copy the definition of the Tainting Checker to create a new annotation and checker with a more specific name and semantics. You will change the copy to rename the annotations, and you will annotate libraries and/or your code to identify sources, sinks, and validation/sanitization routines. See Chapter 30 for more details. 84 Chapter 11 Regex Checker for regular expression syntax The Regex Checker prevents, at compile-time, use of syntactically invalid regular expressions and access of invalid capturing groups. A regular expression, or regex, is a pattern for matching certain strings of text. In Java, a programmer writes a regular expression as a string. At run time, the string is “compiled” into an efficient internal form (Pattern) that is used for text-matching. Regular expression in Java also have capturing groups, which are delimited by parentheses and allow for extraction from text. The syntax of regular expressions is complex, so it is easy to make a mistake. It is also easy to accidentally use a regex feature from another language that is not supported by Java (see section “Comparison to Perl 5” in the Pattern Javadoc). Ordinarily, the programmer does not learn of these errors until run time. The Regex Checker warns about these problems at compile time. For further details, including case studies, see a paper about the Regex Checker [SDE12]. To run the Regex Checker, supply the -processor org.checkerframework.checker.regex.RegexChecker command-line option to javac. 11.1 Regex annotations These qualifiers make up the Regex type system: @Regex indicates that the run-time value is a valid regular expression String. If the optional parameter is supplied to the qualifier, then the number of capturing groups in the regular expression is at least that many. If not provided, the parameter defaults to 0. For example, if an expression’s type is @Regex(1) String, then its run-time value could be "colo(u?)r" or "(brown|beige)" but not "colou?r" nor a non-regex string such as "1) first point". @PolyRegex indicates qualifier polymorphism (see Section 24.2). The subtyping hierarchy of the Regex Checker’s qualifiers is shown in Figure 11.1. 11.2 Annotating your code with @Regex 11.2.1 Implicit qualifiers The Regex Checker adds implicit qualifiers, reducing the number of annotations that must appear in your code (see Section 25.3). The checker implicitly adds the Regex qualifier with the parameter set to the correct number of capturing 85 @UnknownRegex @Regex(0) = @Regex @Regex(1) @Regex(2) . . . @RegexBottom Figure 11.1: The subtyping relationship of the Regex Checker’s qualifiers. Because the parameter to a @Regex qualifier is at least the number of capturing groups in a regular expression, a @Regex qualifier with more capturing groups is a subtype of a @Regex qualifier with fewer capturing groups. Qualifiers in gray are used internally by the type system but should never be written by a programmer. public @Regex String parenthesize(@Regex String regex) { return "(" + regex + ")"; // Even though the parentheses are not @Regex Strings, // the whole expression is a @Regex String } Figure 11.2: An example of the Regex Checker’s support for concatenation of non-regular-expression Strings to produce valid regular expression Strings. groups to any String literal that is a valid regex. The Regex Checker allows the null literal to be assigned to any type qualified with the Regex qualifier. 11.2.2 Capturing groups The Regex Checker validates that a legal capturing group number is passed to Matcher’s group, start and end methods. To do this, the type of Matcher must be qualified with a @Regex annotation with the number of capturing groups in the regular expression. This is handled implicitly by the Regex Checker for local variables (see Section 25.4), but you may need to add @Regex annotations with a capturing group count to Pattern and Matcher fields and parameters. 11.2.3 Concatenation of partial regular expressions In general, concatenating a non-regular-expression String with any other string yields a non-regular-expression String. The Regex Checker can sometimes determine that concatenation of non-regular-expression Strings will produce valid regular expression Strings. For an example see Figure 11.2. 86 String regex = getRegexFromUser(); if (! RegexUtil.isRegex(regex)) { throw new RuntimeException("Error parsing regex " + regex, RegexUtil.regexException(regex)); } Pattern p = Pattern.compile(regex); Figure 11.3: Example use of RegexUtil methods. 11.2.4 Testing whether a string is a regular expression Sometimes, the Regex Checker cannot infer whether a particular expression is a regular expression — and sometimes your code cannot either! In these cases, you can use the isRegex method to perform such a test, and other helper methods to provide useful error messages. A common use is for user-provided regular expressions (such as ones passed on the command-line). Figure 11.3 gives an example of the intended use of the RegexUtil methods. RegexUtil.isRegex returns true if its argument is a valid regular expression. RegexUtil.regexError returns a String error message if its argument is not a valid regular expression, or null if its argument is a valid regular expression. RegexUtil.regexException returns the PatternSyntaxException that Pattern.compile(String) throws when compiling an invalid regular expression. It returns null if its argument is a valid regular expression. An additional version of each of these methods is also provided that takes an additional group count parameter. The RegexUtil.isRegex method verifies that the argument has at least the given number of groups. The RegexUtil.regexError and RegexUtil.regexException methods return a String error message and PatternSyntaxException, respectively, detailing why the given String is not a syntactically valid regular expression with at least the given number of capturing groups. If you detect that a String is not a valid regular expression but would like to report the error higher up the call stack (potentially where you can provide a more detailed error message) you can throw a RegexUtil.CheckedPatternSyntaxException. This exception is functionally the same as a PatternSyntaxException except it is checked to guarantee that the error will be handled up the call stack. For more details, see the Javadoc for RegexUtil.CheckedPatternSyntaxException. A potential disadvantage of using the RegexUtil class is that your code becomes dependent on the Checker Framework at run time as well as at compile time. That is, the checker-qual.jar file must be on the classpath at run time. You can avoid this by copying the RegexUtil class into your own code. 11.2.5 Suppressing warnings If you are positive that a particular string that is being used as a regular expression is syntactically valid, but the Regex Checker cannot conclude this and issues a warning about possible use of an invalid regular expression, then you can use the RegexUtil.asRegex method to suppress the warning. You can think of this method as a cast: it returns its argument unchanged, but with the type @Regex String if it is a valid regular expression. It throws an error if its argument is not a valid regular expression, but you should only use it when you are sure it will not throw an error. There is an additional RegexUtil.asRegex method that takes a capturing group parameter. This method works the same as described above, but returns a @Regex String with the parameter on the annotation set to the value of the capturing group parameter passed to the method. The use case shown in Figure 11.3 should support most cases so the asRegex method should be used rarely. 87 Chapter 12 Format String Checker The Format String Checker prevents use of incorrect format strings in format methods such as System.out.printf and String.format. The Format String Checker warns you if you write an invalid format string, and it warns you if the other arguments are not consistent with the format string (in number of arguments or in their types). Here are examples of errors that the Format String Checker detects at compile time. Section 12.3 provides more details. String.format("%y", 7); // error: invalid format string String.format("%d", "a string"); // error: invalid argument type for %d String.format("%d %s", 7); String.format("%d", 7, 3); String.format("{0}", 7); // error: missing argument for %s // warning: unused argument 3 // warning: unused argument 7, because {0} is wrong syntax To run the Format String Checker, supply the -processor org.checkerframework.checker.formatter.FormatterChecker command-line option to javac. 12.1 Formatting terminology Printf-style formatting takes as an argument a format string and a list of arguments. It produces a new string in which each format specifier has been replaced by the corresponding argument. The format specifier determines how the format argument is converted to a string. A format specifier is introduced by a % character. For example, String.format("The %s is %d.","answer",42) yields "The answer is 42.". "The %s is %d." is the format string, "%s" and "%d" are the format specifiers; "answer" and 42 are format arguments. 12.2 Format String Checker annotations The @Format qualifier on a string type indicates a valid format string. The JDK documentation for the Formatter class explains the requirements for a valid format string. A programmer rarely writes the @Format annotation, as it is inferred for string literals. A programmer may need to write it on fields and on method signatures. The @Format qualifier is parameterized with a list of conversion categories that impose restrictions on the format arguments. Conversion categories are explained in more detail in Section 12.2.1. The type qualifier for "%d %f" is for example @Format({INT, FLOAT}). Consider the below printFloatAndInt method. Its parameter must be a format string that can be used in a format method, where the first format argument is “float-like” and the second format argument is “integer-like”. The type of its parameter, @Format({FLOAT, INT}) String, expresses that contract. 88 @UnknownFormat @Format(...,) @InvalidFormat @FormatBottom Figure 12.1: The Format String Checker type qualifier hierarchy. The figure does not show the subtyping rules among different @Format(...) qualifiers; see Section 12.2.2. void printFloatAndInt(@Format({FLOAT, INT}) String fs) { System.out.printf(fs, 3.1415, 42); } printFloatAndInt("Float %f, Number %d"); printFloatAndInt("Float %f"); // OK // error Figure 12.1 shows all the type qualifiers. The annotations other than @Format are only used internally and cannot be written in your code. @InvalidFormat indicates an invalid format string — that is, a string that cannot be used as a format string. For example, the type of "%y" is @InvalidFormat String. @FormatBottom is the type of the null literal. @UnknownFormat is the default that is applied to strings that are not literals and on which the user has not written a @Format annotation. 12.2.1 Conversion Categories Given a format specifier, only certain format arguments are compatible with it, depending on its “conversion” — its last, or last two, characters. For example, in the format specifier "%d", the conversion d restricts the corresponding format argument to be “integer-like”: String.format("%d", 5); String.format("%d", "hello"); // OK // error Many conversions enforce the same restrictions. A set of restrictions is represented as a conversion category. The “integer like” restriction is for example the conversion category INT. The following conversion categories are defined in the ConversionCategory enumeration: GENERAL imposes no restrictions on a format argument’s type. Applicable for conversions b, B, h, H, s, S. CHAR requires that a format argument represents a Unicode character. Specifically, char, Character, byte, Byte, short, and Short are allowed. int or Integer are allowed if Character.isValidCodePoint(argument) would return true for the format argument. (The Format String Checker permits any int or Integer without issuing a warning or error — see Section 12.3.2.) Applicable for conversions c, C. INT requires that a format argument represents an integral type. Specifically, byte, Byte, short, Short, int and Integer, long, Long, and BigInteger are allowed. Applicable for conversions d, o, x, X. FLOAT requires that a format argument represents a floating-point type. Specifically, float, Float, double, Double, and BigDecimal are allowed. Surprisingly, integer values are not allowed. Applicable for conversions e, E, f, g, G, a, A. TIME requires that a format argument represents a date or time. Specifically, long, Long, Calendar, and Date are allowed. Applicable for conversions t, T. UNUSED imposes no restrictions on a format argument. This is the case if a format argument is not used as replacement for any format specifier. "%2$s" for example ignores the first format argument. 89 Further, all conversion categories accept null. The same format argument may serve as a replacement for multiple format specifiers. Until now, we have assumed that the format specifiers simply consume format arguments left to right. But there are two other ways for a format specifier to select a format argument: • n$ specifies a one-based index n. In the format string "%2$s", the format specifier selects the second format argument. • The < flag references the format argument that was used by the previous format specifier. In the format string "%d % and use it in the body of the type definition; for example, class List { ... T get() {...} ... }. To instantiate a generic type, you write its name along with a type argument; for example, List myDates;. 16.5.1 Defining an effect-polymorphic type To declare that a class is effect-polymorphic, annotate its definition with @PolyUIType. To use the effect variable in the class body, annotate a method with @PolyUIEffect. It is an error to use @PolyUIEffect in a class that is not effect-polymorphic. Consider the following example: @PolyUIType public interface Runnable { @PolyUIEffect void run(); } This declares that class Runnable is parameterized over one generic effect, and that when Runnable is instantiated, the effect argument will be used as the effect for the run method. 16.5.2 Using an effect-polymorphic type To instantiate an effect-polymorphic type, write one of these three type qualifiers before a use of the type: • @AlwaysSafe instantiates the type’s effect to @SafeEffect. • @UI instantiates the type’s effect to @UIEffect. Additionally, it changes the default method effect for the class to @UIEffect. • @PolyUI instantiates the type’s effect to @PolyUIEffect for the same instantiation as the current (containing) class. For example, this is the qualifier of the receiver this inside a method of a @PolyUIType class, which is how one method of an effect-polymorphic class may call an effect-polymorphic method of the same class. As an example: @AlwaysSafe Runnable s = ...; @PolyUI Runnable p = ...; @UI Runnable u = ...; s.run(); p.run(); u.run(); // s.run() is @SafeEffect // p.run() is @PolyUIEffect (context-dependent) // u.run() is @UIEffect It is an error to apply an effect instantiation qualifier to a type that is not effect-polymorphic. 16.5.3 Subclassing a specific instantiation of an effect-polymorphic type Sometimes you may wish to subclass a specific instantiation of an effect-polymorphic type, just as you may extend List . To do this, simply place the effect instantiation qualifier by the name of the type you are defining, e.g.: 109 @UI public class UIRunnable extends Runnable {...} @AlwaysSafe public class SafeRunnable extends Runnable {...} The GUI Effect Checker will automatically apply the qualifier to all classes and interfaces the class being defined extends or implements. (This means you cannot write a class that is a subtype of a @AlwaysSafe Foo and a @UI Bar, but this has not been a problem in our experience.) 16.5.4 Subtyping with polymorphic effects With three effect annotations, we must extend the static sub-effecting relationship: @SafeEffect ≺ @PolyUIEffect ≺ @UIEffect This is the correct sub-effecting relation because it is always safe to call a @SafeEffect method (whether from an effect-polymorphic method or a UI method), and a @UIEffect method may safely call any other method. This induces a subtyping hierarchy on type qualifiers: @AlwaysSafe ≺ @PolyUI ≺ @UI This is sound because a method instantiated according to any qualifier will always be safe to call in place of a method instantiated according to one of its super-qualifiers. This allows clients to pass “safer” instances of some object type to a given method. Effect polymorphism and arguments Sometimes it is useful to have @PolyUI parameters on a method. As a trivial example, this permits us to specify an identity method that works for both @UI Runnable and @AlwaysSafe Runnable: public @PolyUI Runnable id(@PolyUI Runnable r) { return r; } This use of @PolyUI will be handled as is standard for polymorphic qualifiers in the Checker Framework (see Section 24.2). @PolyUIEffect methods should generally not use @PolyUI arguments: it is permitted by the framework, but its interaction with inheritance is subtle, and may not behave as you would hope. The shortest explanation is this: @PolyUI arguments may only be overridden by @PolyUI arguments, even though the implicitly @PolyUI receiver may be overridden with a @AlwaysSafe receiver. As noted earlier (Section 24.1.6), Java’s generics are invariant — A is a subtype of B only if X is identical to Y. Class-level use of @PolyUI behaves slightly differently. Marking a type declaration @PolyUIType is conceptually equivalent to parameterizing the type by some E extends Effect. But in this view, Runnable (really @AlwaysSafe Runnable) would be considered a subtype of Runnable (really @UI Runnable), as explained earlier in this section. Java’s generics do not permit this, which is called covariant subtyping in the effect parameter. Permitting it for all generics leads to problems where a type system can miss errors. Java solves this by making all generics invariant, which rejects more programs than strictly necessary, but leads to an easy-to-explain limitation. For this checker, covariant subtyping of effect parameters is very important: being able to pass an @AlwaysSafe Runnable in place of a @UI Runnable is extremely useful. Since we need to allow some cases for flexibility, but need to reject other cases to avoid missing errors, the distinction is a bit more subtle for this checker. Consider this small example (warning: the following is rejected by the GUI Effect Checker): @PolyUIType public interface Dispatcher { @PolyUIEffect void dispatch(@PolyUI Runnable toRun); } 110 @SafeType public class SafeDispatcher { @Override public void dispatch(@AlwaysSafe Runnable toRun) { runOnBackgroundThread(toRun); } } This may initially seem like harmless code to write, which simply specializes the implicit effect parameter from Dispatcher in the SafeDispatcher implementation. However, the way method effect polymorphism is implemented is by implicitly making the receiver of a @PolyUIEffect method — the object on which the method is invoked — @PolyUI. So if the definitions above were permitted, the following client code would be possible: @AlwaysSafe SafeDispatcher s = ...; @UI Runnable uitask = ...; s.dispatch(uitask); At the call to dispatch, the Checker Framework is free to consider s as its supertype, @UI SafeDispatcher. This permits the framework to choose the same qualifier for both the (implicit) receiver use of @PolyUI and the toRun argument to Dispatcher.dispatch, passing the checker. But this code would then pass a UI-thread-only task to a method which should only accept background thread tasks — exactly what the checker should prevent! To resolve this, the GUI Effect Checker rejects the definitions above, specifically the @AlwaysSafe on SafeDispatcher.dispatch’s parameter, which would need to remain @PolyUI. A subtlety of the code above is that the receiver for SafeDispatcher.dispatch is also overridden, switching from a @PolyUI receiver to a @Safe receiver. That change is permissible. But when that is done, the polymorphic arguments may no longer be interchangeable with the receiver. 16.6 References The ECOOP 2013 paper “JavaUI: Effects for Controlling UI Object Access” includes some case studies on the checker’s efficacy, including descriptions of the relatively few false warnings we encountered. It also contains a more formal description of the effect system. You can obtain the paper at: http://homes.cs.washington.edu/~mernst/pubs/gui-thread-ecoop2013-abstract.html 111 Chapter 17 Units Checker For many applications, it is important to use the correct units of measurement for primitive types. For example, NASA’s Mars Climate Orbiter (cost: $327 million) was lost because of a discrepancy between use of the metric unit Newtons and the imperial measure Pound-force. The Units Checker ensures consistent usage of units. For example, consider the following code: @m int meters = 5 * UnitsTools.m; @s int secs = 2 * UnitsTools.s; @mPERs int speed = meters / secs; Due to the annotations @m and @s, the variables meters and secs are guaranteed to contain only values with meters and seconds as units of measurement. Utility class UnitsTools provides constants with which unqualified integer are multiplied to get values of the corresponding unit. The assignment of an unqualified value to meters, as in meters = 99, will be flagged as an error by the Units Checker. The division meters/secs takes the types of the two operands into account and determines that the result is of type meters per second, signified by the @mPERs qualifier. We provide an extensible framework to define the result of operations on units. 17.1 Units annotations The checker currently supports three varieties of units annotations: kind annotations (@Length, @Mass, . . . ), the SI units (@m, @kg, . . . ), and polymorphic annotations (@PolyUnit). Kind annotations can be used to declare what the expected unit of measurement is, without fixing the particular unit used. For example, one could write a method taking a @Length value, without specifying whether it will take meters or kilometers. The following kind annotations are defined: @Acceleration @Angle @Area @Current @Length @Luminance @Mass @Speed @Substance @Temperature @Time 112 For each kind of unit, the corresponding SI unit of measurement is defined: 1. 2. 3. 4. 5. 6. 7. 8. 9. 10. 11. For @Acceleration: Meter Per Second Square @mPERs2 For @Angle: Radians @radians, and the derived unit Degrees @degrees For @Area: the derived units square millimeters @mm2, square meters @m2, and square kilometers @km2 For @Current: Ampere @A For @Length: Meters @m and the derived units millimeters @mm and kilometers @km For @Luminance: Candela @cd For @Mass: kilograms @kg and the derived unit grams @g For @Speed: meters per second @mPERs and kilometers per hour @kmPERh For @Substance: Mole @mol For @Temperature: Kelvin @K and the derived unit Celsius @C For @Time: seconds @s and the derived units minutes @min and hours @h You may specify SI unit prefixes, using enumeration Prefix. The basic SI units (@s, @m, @g, @A, @K, @mol, @cd) take an optional Prefix enum as argument. For example, to use nanoseconds as unit, you could use @s(Prefix.nano) as a unit type. You can sometimes use a different annotation instead of a prefix; for example, @mm is equivalent to @m(Prefix.milli). Class UnitsTools contains a constant for each SI unit. To create a value of the particular unit, multiply an unqualified value with one of these constants. By using static imports, this allows very natural notation; for example, after statically importing UnitsTools.m, the expression 5 * m represents five meters. As all these unit constants are public, static, and final with value one, the compiler will optimize away these multiplications. The polymorphic annotation @PolyUnit enables you to write a method that takes an argument of any unit type and returns a result of that same type. For more about polymorphic qualifiers, see Section 24.2. For an example of its use, see the @PolyUnit Javadoc. 17.2 Extending the Units Checker You can create new kind annotations and unit annotations that are specific to the particular needs of your project. An easy way to do this is by copying and adapting an existing annotation. (In addition, search for all uses of the annotation’s name throughout the Units Checker implementation, to find other code to adapt; read on for details.) Here is an example of a new unit annotation. @Documented @Retention(RetentionPolicy.RUNTIME) @SubtypeOf({Time.class}) @UnitsMultiple(quantity=s.class, prefix=Prefix.nano) @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) public @interface ns {} The @SubtypeOf meta-annotation specifies that this annotation introduces an additional unit of time. The @UnitsMultiple meta-annotation specifies that this annotation should be a nano multiple of the basic unit @s: @ns and @s(Prefix.nano) behave equivalently and interchangeably. Most annotation definitions do not have a @UnitsMultiple meta-annotation. Note that all custom annotations must have the @Target(ElementType.TYPE_USE) meta-annotation. See section 30.4.1. To take full advantage of the additional unit qualifier, you need to do two additional steps. (1) Provide constants that convert from unqualified types to types that use the new unit. See class UnitsTools for examples (you will need to suppress a checker warning in just those few locations). (2) Put the new unit in relation to existing units. Provide an implementation of the UnitsRelations interface as a meta-annotation to one of the units. See demonstration docs/examples/units-extension/ for an example extension that defines Hertz (hz) as scalar per second, and defines an implementation of UnitsRelations to enforce it. 113 17.3 What the Units Checker checks The Units Checker ensures that unrelated types are not mixed. All types with a particular unit annotation are disjoint from all unannotated types, from all types with a different unit annotation, and from all types with the same unit annotation but a different prefix. Subtyping between the units and the unit kinds is taken into account, as is the @UnitsMultiple meta-annotation. Multiplying a scalar with a unit type results in the same unit type. The division of a unit type by the same unit type results in the unqualified type. Multiplying or dividing different unit types, for which no unit relation is known to the system, will result in a MixedUnits type, which is separate from all other units. If you encounter a MixedUnits annotation in an error message, ensure that your operations are performed on correct units or refine your UnitsRelations implementation. The Units Checker does not change units based on multiplication; for example, if variable mass has the type @kg double, then mass * 1000 has that same type rather than the type @g double. (The Units Checker has no way of knowing whether you intended a conversion, or you were computing the mass of 1000 items. You need to make all conversions explicit in your code, and it’s good style to minimize the number of conversions.) 17.4 Running the Units Checker The Units Checker can be invoked by running the following commands. • If your code uses only the SI units that are provided by the framework, simply invoke the checker: javac -processor org.checkerframework.checker.units.UnitsChecker MyFile.java ... • If you define your own units, provide the fully-qualified class names of the annotations through the -Aunits option, using a comma-no-space-separated notation: javac -classpath /full/path/to/myProject/bin:/full/path/to/myLibrary/bin \ -processor org.checkerframework.checker.units.UnitsChecker \ -Aunits=myPackage.qual.MyUnit,myPackage.qual.MyOtherUnit MyFile.java ... The annotations listed in -Aunits must be accessible to the compiler during compilation in the classpath. In other words, they must already be compiled (and, typically, be on the javac classpath) before you run the Units Checker with javac. It is not sufficient to supply their source files on the command line. • You can also provide the fully-qualified paths to a set of directories that contain units qualifiers through the -AunitsDirs option, using a colon-no-space-separated notation. For example: javac -classpath /full/path/to/myProject/bin:/full/path/to/myLibrary/bin \ -processor org.checkerframework.checker.units.UnitsChecker \ -AunitsDirs=/full/path/to/myProject/bin:/full/path/to/myLibrary/bin MyFile.java ... Note that in these two examples, the compiled class file of the myPackage.qual.MyUnit and myPackage.qual.MyOtherUnit annotations must exist in either the myProject/bin directory or the myLibrary/bin directory. The following placement of the class files will work with the above commands: .../myProject/bin/myPackage/qual/MyUnit.class .../myProject/bin/myPackage/qual/MyOtherUnit.class The two options can be used at the same time to provide groups of annotations from directories, and individually named annotations. Also, see the example project in the docs/examples/units-extension directory. 17.5 Suppressing warnings One example of when you need to suppress warnings is when you initialize a variable with a unit type by a literal value. To remove this warning message, it is best to introduce a constant that represents the unit and to add a @SuppressWarnings annotation to that constant. For examples, see class UnitsTools. 114 17.6 References • The GNU Units tool provides a comprehensive list of units: http://www.gnu.org/software/units/ • The F# units of measurement system inspired some of our syntax: https://en.wikibooks.org/wiki/F_Sharp_Programming/Units_of_Measure 115 Chapter 18 Signedness Checker The Signedness Checker guarantees that signed and unsigned values are not mixed together in a computation. In addition, it prohibits meaningless operations, such as division on an unsigned value. 18.1 Annotations The Signedness Checker uses type annotations to indicate the signedness that the programmer intends an expression to have. These are the qualifiers in the signedness type system: @Unsigned indicates that the programmer intends the value to be interpreted as unsigned. That is, if the most significant bit in the bitwise representation is set, then the bits should be interpreted as a large positive value. @Signed indicates that the programmer intends the value to be interpreted as signed. That is, if the most significant bit in the bitwise representation is set, then the bits should be interpreted as a negative value. This is the default annotation. @Constant indicates that a value is a compile-time constant and could be interpreted as unsigned or signed. This annotation is used internally, and should not be written by the programmer. @UnknownSignedness indicates that a value’s type is not relevant or known to this checker. This annotation is used internally, and should not be written by the programmer. @SignednessBottom indicates that the value is null. This annotation is used internally, and should not be written by the programmer. Signedness is primarily about how the bits of the representation are interpreted, not about the values that it can represent. An unsigned value is always positive, but just because a variable’s value is positive does not mean that it should be marked as @Unsigned. If variable v will be compared to a signed value, or used in arithmetic operations with a signed value, then v should have signed type. @UnknownSignedness @Unsigned @Signed @Constant @SignednessBottom Figure 18.1: The type qualifier hierarchy of the signedness annotations. Qualifiers in gray are used internally by the type system but should never be written by a programmer. 116 18.1.1 Default qualifiers The only type qualifier that the programmer should need to write is @Unsigned. When a programmer leaves an expression unannotated, the Signedness Checker treats it in one of the following ways: • All byte, short, int, and long literals default to @Constant. • All byte, short, int, and long variables default to @Signed. • All other expressions default to @UnknownSignedness. 18.2 Prohibited operations The Signedness Checker prohibits the following uses of operators: • • • • • Division (/) or modulus (%) with an @Unsigned operand. Signed right shift (>>) with an @Unsigned left operand. Unsigned right shift (>>>) with a @Signed left operand. Greater/less than (or equal) comparators (<, <=, >, >=) with an @Unsigned operand. Any other binary operator with one @Unsigned operand and one @Signed operand, with the exception of left shift (<<). Like every type-checker built with the Checker Framework, the Signedness Checker ensures that assignments and pseudo-assignments have consistent types. For example, it is not permitted to assign a @Signed expression to an @Unsigned variable or vice versa. 18.3 Rationale The Signedness Checker prevents misuse of unsigned values in Java code. Most Java operations interpret operands as signed. If applied to unsigned values, those operations would produce unexpected, incorrect results. Consider the following Java code: int s1 = -1; int s2 = -2; @Unsigned int u1 = 0xFFFFFFFF; @Unsigned int u2 = 0xFFFFFFFE; // unsigned: 2^32 - 1, signed: -1 // unsigned: 2^32 - 2, signed: -2 int result; result = s2 / s1; result = u2 / u1; // OK: result is 2, which is correct for -2 / -1 // ERROR: result is 2, which is incorrect for (2^32 - 1) / (2^32 - 2) int s3 = -1; int s4 = 5; @Unsigned int u3 = 0xFFFFFFFF; @Unsigned int u4 = 5; result = s3 % s4; result = u3 % u4; // unsigned: 2^32 - 1, signed: -1 // OK: result is 4, which is correct for -2 % 5 // ERROR: result is 4, which is incorrect for (2^32 - 1) % 5 These examples illustrate why division and modulus with an unsigned operand are illegal. Other uses of operators are prohibited for similar reasons. 117 18.4 Utility routines for manipulating unsigned values Class SignednessUtil provides static utility methods for working with unsigned values. Some of these re-implement functionality in JDK 8, making it available in earlier versions of Java. Others provide new functionality. All of them are properly annotated with @Unsigned where appropriate, so using them may reduce the number of annotations that you need to write. Class SignednessUtilExtra contains more utility methods that reference packages not included in Android. This class is not included in checker-qual.jar, so you may want to copy the methods to your code. 118 Chapter 19 Constant Value Checker The Constant Value Checker is a constant propagation analysis: for each variable, it determines whether that variable’s value can be known at compile time. There are two ways to run the Constant Value Checker. • Typically, it is automatically run by another type checker. • Alternately, you can run just the Constant Value Checker, by supplying the following command-line options to javac: -processor org.checkerframework.common.value.ValueChecker -Astubs=statically-executable.astub 19.1 Annotations The Constant Value Checker uses type annotations to indicate the value of an expression (Section 19.1.1), and it uses method annotations to indicate methods that the Constant Value Checker can execute at compile time (Section 19.1.3). 19.1.1 Type Annotations Typically, the programmer does not write any type annotations. Rather, the type annotations are inferred by the Constant Value Checker. The programmer is also permitted to write type annotations. This is only necessary in locations where the Constant Value Checker does not infer annotations: on fields and method signatures. The main type annotations are @BoolVal, @IntVal, @IntRange, @DoubleVal, and @StringVal. Additional type annotations for arrays and strings are @ArrayLen, @ArrayLenRange, and @MinLen. A polymorphic qualifier (@PolyValue) is also supported (see Section 24.2). Each *Val type annotation takes as an argument a set of values, and its meaning is that at run time, the expression evaluates to one of the values. For example, an expression of type @StringVal("a", "b") evaluates to one of the values "a", "b", or null. The set is limited to 10 entries; if a variable could be more than 10 different values, the Constant Value Checker gives up and its type becomes @IntRange for integral types, @ArrayLenRange for array types, @ArrayLen or @ArrayLenRange for String, and @UnknownVal for all other types. The @ArrayLen annotation means that at run time, the expression evaluates to an array or a string whose length is one of the annotation’s arguments. In the case of too many strings in @StringVal, the values are forgotten and just the lengths are used in @ArrayLen. If this would result in too many lengths, only the minimum and maximum lengths are used in @ArrayLenRange, giving a range of possible lengths of the string. The @StringVal annotation may be applied to a char array. Although byte arrays are often converted to/from strings, the @StringVal annotation may not be applied to them. This is because the conversion depends on the platform’s character set. @IntRange takes two arguments — a lower bound and an upper bound. Its meaning is that at run time, the expression evaluates to a value between the bounds (inclusive). For example, an expression of type @IntRange(from=0, to=255) evaluates to 0, 1, 2, . . . , 254, or 255. An @IntVal and @IntRange annotation that represent the same set of values are semantically identical and interchangeable: they have exactly the same meaning, and using either one has the 119 @UnknownVal @BoolVal(boolean[]) @IntRange(long,long) @IntVal(long[]) @DoubleVal(double[]) @StringVal(String[]) @ArrayLen(int[]) @ArrayLenRange(int,int) @BottomVal @IntRange(from=0,to=200) @DoubleVal({0.0,1.0,2.0}) @IntRange(from=0,to=1) @IntVal({1,2}) @ArrayLenRange(0,200) @ArrayLen({1,2}) @DoubleVal(1.0) @StringVal({"a","aa","b"}) @ArrayLen(1) @IntVal(1) @StringVal({"a","aa"}) @StringVal({"a","b"}) @StringVal("a") Figure 19.1: At the top, the type qualifier hierarchy of the Constant Value Checker annotations. Qualifiers in gray are used internally by the type system but should never be written by a programmer. At the bottom are examples of additional subtyping relationships that depend on the annotations’ arguments. public void foo(boolean int i = 1; // i if (b) { i = 2; // i } // i i = i + 1; // i } b) { has type: @IntVal({1}) int now has type: @IntVal({2}) int now has type: now has type: @IntVal({1,2}) int @IntVal({2,3}) int Figure 19.2: The Constant Value Checker infers different types for a variable on different lines of the program. same effect. @ArrayLenRange has the same relationship to @ArrayLen that @IntRange has to @IntVal. The @MinLen annotation is an alias for @ArrayLenRange (meaning that every @MinLen annotation is automatically converted to an @ArrayLenRange annotation) that only takes one argument, which is the lower bound of the range. The upper bound of the range is the maximum integer value. Figure 19.1 shows the subtyping relationship among the type annotations. For two annotations of the same type, subtypes have a smaller set of possible values, as also shown in the figure. Because int can be casted to double, an @IntVal annotation is a subtype of a @DoubleVal annotation with the same values. Figure 19.2 illustrates how the Constant Value Checker infers type annotations (using flow-sensitive type qualifier refinement, Section 25.4). If your code is already annotated with a different constant value or range annotation, the Checker Framework can type-check your code. It treats annotations from other tools as if you had written the corresponding annotation from the Constant Value Checker, as described in Figure 19.3. If the other annotation is a declaration annotation, it may be moved; see Section 27.1.1. The Constant Value Checker trusts the @Positive, @NonNegative, and @GTENegativeOne annotations. If your code contains any of these annotations, then in order to guarantee soundness, you must run the Index Checker whenever you run the Constant Value Checker. 120 android.support.annotation.IntRange ⇒ org.checkerframework.checker.common.value.qual.IntRange Figure 19.3: Correspondence between other constant value and range annotations and the Checker Framework’s annotations. @StaticallyExecutable @Pure public int foo(int a, int b) { return a + b; } public void int a = int b = int c = } bar() { 5; 4; foo(a, b); // a has type: // b has type: // c has type: @IntVal({5}) int @IntVal({4}) int @IntVal({9}) int Figure 19.4: The @StaticallyExecutable annotation enables constant propagation through method calls. 19.1.2 Compile-time execution of expressions Whenever all the operands of an expression are compile-time constants (that is, their types have constant-value type annotations), the Constant Value Checker attempts to execute the expression. This is independent of any optimizations performed by the compiler and does not affect the code that is generated. The Constant Value Checker statically executes operators that do not throw exceptions (e.g., +, -, <<, !=). 19.1.3 @StaticallyExecutable methods and the classpath The Constant Value Checker statically executes methods annotated with @StaticallyExecutable, if the method has already been compiled and is on the classpath. A @StaticallyExecutable method must be @Pure (side-effect-free and deterministic). Additionally, a @StaticallyExecutable method and any method it calls must be on the classpath for the compiler, because they are reflectively called at compile-time to perform the constant value analysis. To use @StaticallyExecutable on methods in your own code, you should first compile the code without the Constant Value Checker and then add the location of the resulting .class files to the classpath. For example, the command-line arguments to the Checker Framework might include: -processor org.checkerframework.common.value.ValueChecker -Astubs=statically-executable.astub -classpath $CLASSPATH:MY_PROJECT/build/ 19.2 Warnings If the option -AreportEvalWarns options is used, the Constant Value Checker issues a warning if it cannot load and run, at compile time, a method marked as @StaticallyExecutable. If it issues such a warning, then the return value of the method will be @UnknownVal instead of being able to be resolved to a specific value annotation. Some examples of these: • [class.find.failed] Failed to find class named Test. The checker could not find the class specified for resolving a @StaticallyExecutable method. Typically this is caused by not providing the path of a class-file needed to the classpath. • [method.find.failed] Failed to find a method named foo with argument types [@IntVal(3) int]. 121 ... if (i > 5) { // i now has type: @IntRange(from=5, to=Integer.MAX_VALUE) i = i + 1; // If i started out as Integer.MAX_VALUE, then i is now Integer.MIN_VALUE. // i’s type is now @IntRange(from=Integer.MIN_VALUE, to=Integer.MAX_VALUE). // When ignoring overflow, i’s type is now @IntRange(from=6, to=Integer.MAX_VALUE). } Figure 19.5: With the -AignoreRangeOverflow command-line option, the Constant Value Checker ignores overflow for range types, which gives smaller ranges to range types. The checker could not find the method foo(int) specified for resolving a @StaticallyExecutable method, but could find the class. This is usually due to providing an outdated version of the class-file that does not contain the method that was annotated as @StaticallyExecutable. • [method.evaluation.exception] Failed to evaluate method public static int Test.foo(int) because it threw an exception: java.lang.ArithmeticException: / by zero. An exception was thrown when trying to statically execute the method. In this case it was a divide-by-zero exception. If the arguments to the method each only had one value in their annotations then this exception will always occur when the program is actually run as well. If there are multiple possible values then the exception might not be thrown on every execution, depending on the run-time values. There are some other situations in which the Constant Value Checker produces a warning message: • [too.many.values.given] The maximum number of arguments permitted is 10. The Constant Value Checker only tracks up to 10 possible values for an expression. If you write an annotation with more values than will be tracked, the annotation is replaced with @IntRange, @ArrayLen, @ArrayLenRange, or @UnknownVal. 19.3 Unsoundly ignoring overflow The Constant Value Checker takes Java’s overflow rules into account when computing the possible values of expressions. The -AignoreRangeOverflow command-line option makes it ignore the possibility of overflow for range annotations @IntRange and @ArrayLenRange. Figure 19.5 gives an example of behavior with and without the -AignoreRangeOverflow command-line option. As with any unsound behavior in the Checker Framework, this option reduces the number of warnings and errors produced, and may reduce the number of @IntRange qualifiers that you need to write in the source code. However, it is possible that at run time, an expression might evaluate to a value that is not in its @IntRange qualifier. You should either accept that possibility, or verify the lack of overflow using some other tool or manual analysis. 122 Chapter 20 Aliasing Checker The Aliasing Checker identifies expressions that definitely have no aliases. Two expressions are aliased when they have the same non-primitive value; that is, they are references to the identical Java object in the heap. Another way of saying this is that two expressions, exprA and exprB, are aliases of each other when exprA==exprB at the same program point. Assigning to a variable or field typically creates an alias. For example, after the statement a = b;, the variables a and b are aliased. Knowing that an expression is not aliased permits more accurate reasoning about how side effects modify the expression’s value. To run the Aliasing Checker, supply the -processor org.checkerframework.common.aliasing.AliasingChecker command-line option to javac. However, a user rarely runs the Aliasing Checker directly. This type system is mainly intended to be used together with other type systems. For example, the SPARTA information flow type-checker (Section 23.8) uses the Aliasing Checker to improve its type refinement — if an expression has no aliases, a more refined type can often be inferred, otherwise the type-checker makes conservative assumptions. 20.1 Aliasing annotations There are two possible types for an expression: @MaybeAliased is the type of an expression that might have an alias. This is the default, so every unannotated type is @MaybeAliased. (This includes the type of null.) @Unique is the type of an expression that has no aliases. The @Unique annotation is only allowed at local variables, method parameters, constructor results, and method returns. A constructor’s result should be annotated with @Unique only if the constructor’s body does not creates an alias to the constructed object. There are also two annotations, which are currently trusted instead of verified, that can be used on formal parameters (including the receiver parameter, this): @MaybeAliased @Unique Figure 20.1: Type hierarchy for the Aliasing type system. 123 @NonLeaked identifies a formal parameter that is not leaked nor returned by the method body. For example, the formal parameter of the String copy constructor, String(String s), is @NonLeaked because the body of the method only makes a copy of the parameter. @LeakedToResult is used when the parameter may be returned, but it is not otherwise leaked. For example, the receiver parameter of StringBuffer.append(StringBuffer this, String s) is @LeakedToResult, because the method returns the updated receiver. 20.2 Leaking contexts This section lists the expressions that create aliases. These are also called “leaking contexts”. Assignments After an assignment, the left-hand side and the right-hand side are typically aliased. (The only counterexample is when the right-hand side is a fresh expression; see Section 20.4.) @Unique Object u = ...; Object o = u; // (not.unique) type-checking error! If this example type-checked, then u and o would be aliased. For this example to type-check, either the @Unique annotation on the type of u, or the o = u; assignment, must be removed. Method calls and returns (pseudo-assignments) Passing an argument to a method is a “pseudo-assignment” because it effectively assigns the argument to the formal parameter. Return statements are also pseudo-assignments. As with assignments, the left-hand side and right-hand side of pseudo-assignments are typically aliased. Here is an example for argument-passing: void foo(Object o) { ... } @Unique Object u = ...; foo(u); // type-checking error, because foo may create an alias of the passed argument Passing a non-aliased reference to a method does not necessarily create an alias. However, the body of the method might create an alias or leak the reference. Thus, the Aliasing Checker always treats a method call as creating aliases for each argument unless the corresponding formal parameter is marked as @@NonLeaked or @@LeakedToResult. Here is an example for a return statement: Object id(@Unique Object p) { return p; // (not.unique) type-checking error! } If this code type-checked, then it would be possible for clients to write code like this: @Unique Object u = ...; Object o = id(u); after which there is an alias to u even though it is declared as @Unique. However, it is permitted to write Object id(@LeakedToResult Object p) { return p; } after which the following code type-checks: @Unique Object u = ...; id(u); Object o1 = ...; Object o2 = id(o1); // method call result is not used // argument is not @Unique Throws A thrown exception can be captured by a catch block, which creates an alias of the thrown exception. 124 void foo() { @Unique Exception uex = new Exception(); try { throw uex; // (not.unique) type-checking error! } catch (Exception ex) { // uex and ex refer to the same object here. } } Array initializers Array initializers assign the elements in the initializers to corresponding indexes in the array, therefore expressions in an array initializer are leaked. void foo() { @Unique Object o = new Object(); Object[] ar = new Object[] { o }; // (not.unique) type-checking error! // The expressions o and ar[0] are now aliased. } 20.3 Restrictions on where @Unique may be written The @Unique qualifier may not be written on locations such as fields, array elements, and type parameters. As an example of why @Unique may not be written on a field’s type, consider the following code: class MyClass { @Unique Object field; void foo() { MyClass myClass2 = this; // this.field is now an alias of myClass2.field } } That code must not type-check, because field is declared as @Unique but has an alias. The Aliasing Checker solves the problem by forbidding the @Unique qualifier on subcomponents of a structure, such as fields. Other solutions might be possible; they would be more complicated but would permit more code to type-check. @Unique may not be written on a type parameter for similar reasons. The assignment List<@Unique Object> l1 = ...; List<@Unique Object> l2 = l1; must be forbidden because it would alias l1.get(0) with l2.get(0) even though both have type @Unique. The Aliasing Checker forbids this code by rejecting the type List<@Unique Object>. 20.4 Aliasing type refinement Type refinement enables a type checker to treat an expression as a subtype of its declared type. For example, even if you declare a local variable as @MaybeAliased (or don’t write anything, since @MaybeAliased is the default), sometimes the Aliasing Checker can determine that it is actually @Unique. For more details, see Section 25.4. The Aliasing Checker treats type refinement in the usual way, except that at (pseudo-)assignments the right-handside (RHS) may lose its type refinement, before the left-hand-side (LHS) is type-refined. The RHS always loses its type refinement (it is widened to @MaybeAliased, and its declared type must have been @MaybeAliased) except in the following cases: 125 // Annotations on the StringBuffer class, used in the examples below. // class StringBuffer { // @Unique StringBuffer(); // StringBuffer append(@LeakedToResult StringBuffer this, @NonLeaked String s); // } void foo() { StringBuffer sb = new StringBuffer(); // sb is refined to @Unique. StringBuffer sb2 = sb; // sb loses its refinement. // Both sb and sb2 have aliases and because of that have type @MaybeAliased. } void bar() { StringBuffer sb = new StringBuffer(); // sb is refined to @Unique. sb.append("someString"); // sb stays @Unique, as no aliases are created. StringBuffer sb2 = sb.append("someString"); // sb is leaked and becomes @MaybeAliased. // Both sb and sb2 have aliases and because of that have type @MaybeAliased. } Figure 20.2: Example of Aliasing Checker’s type refinement rules. • The RHS is a fresh expression — an expression that returns a different value each time it is evaluated. In practice, this is only method/constructor calls with @Unique return type. A variable/field is not fresh because it can return the same value when evaluated twice. • The LHS is a @NonLeaked formal parameter and the RHS is an argument in a method call or constructor invocation. • The LHS is a @LeakedToResult formal parameter, the RHS is an argument in a method call or constructor invocation, and the method’s return value is discarded — that is, the method call or constructor invocation is written syntactically as a statement rather than as a part of a larger expression or statement. A consequence of the above rules is that most method calls are treated conservatively. If a variable with declared type @MaybeAliased has been refined to @Unique and is used as an argument of a method call, it usually loses its @Unique refined type. Figure 20.2 gives an example of the Aliasing Checker’s type refinement rules. 126 Chapter 21 Reflection resolution A call to Method.invoke might reflectively invoke any method. That method might place requirements on its formal parameters, and it might return any value. To reflect these facts, the annotated JDK contains conservative annotations for Method.invoke. These conservative library annotations often cause a checker to issue false positive warnings when type-checking code that uses reflection. If you supply the -AresolveReflection command-line option, the Checker Framework attempts to resolve reflection. At each call to Method.invoke or Constructor.newInstance, the Checker Framework first soundly estimates which methods might be invoked at runtime. When type-checking the call, the Checker Framework uses a library annotation that indicates the parameter and return types of the possibly-invoked methods. If the estimate of invoked methods is small, these types are precise and the checker issues fewer false positive warnings. If the estimate of invoked methods is large, these types are no better than the conservative library annotations. Reflection resolution is disabled by default, because it increases the time to type-check a program. You should enable reflection resolution with the -AresolveReflection command-line option if, for some call site of Method.invoke or Constructor.newInstance in your program: 1. the conservative library annotations on Method.invoke or Constructor.newInstance cause false positive warnings, 2. the set of possibly-invoked methods or constructors can be known at compile time, and 3. the reflectively invoked methods/constructors are on the class path at compile time. Reflection resolution does not change your source code or generated code. In particular, it does not replace the Method.invoke or Constructor.newInstance calls. The command-line option -AresolveReflection=debug outputs verbose information about the reflection resolution process. Section 21.1 first describes the MethodVal and ClassVal Checkers, which reflection resolution uses internally. Then, Section 21.2 gives examples of reflection resolution. 21.1 MethodVal and ClassVal Checkers The implementation of reflection resolution internally uses the ClassVal Checker (Section 21.1.1) and the MethodVal Checker (Section 21.1.2). They are very similar to the Constant Value Checker (Section 19) in that their annotations estimate the run-time value of an expression. In some cases, you may need to write annotations such as @ClassVal, @MethodVal, @StringVal, and @ArrayLen to aid in reflection resolution. Often, though, these annotations can be inferred (Section 21.1.3). 21.1.1 ClassVal Checker The ClassVal Checker defines the following annotations: 127 @UnknownClass @ClassBound({"java.lang.String","com.example.MyClass"}) @ClassVal({"java.lang.String","com.example.MyClass"}) @ClassBound("java.lang.String") @ClassVal("java.lang.String") @ClassValBottom Figure 21.1: Partial type hierarchy for the ClassVal type system. The type qualifiers in gray (@UnknownClass and @ClassValBottom) should never be written in source code; they are used internally by the type system. @ClassVal(String[] value) If an expression has @ClassVal type with a single argument, then its exact run-time value is known at compile time. For example, @ClassVal("java.util.HashMap") indicates that the Class object represents the java.util.HashMap class. If multiple arguments are given, then the expression’s run-time value is known to be in that set. The arguments are binary names (JLS §13.1). @ClassBound(String[] value) If an expression has @ClassBound type, then its run-time value is known to be upper-bounded by that type. For example, @ClassBound("java.util.HashMap") indicates that the Class object represents java.util.HashMap or a subclass of it. If multiple arguments are given, then the run-time value is equal to or a subclass of some class in that set. The arguments are binary names (JLS §13.1). @UnknownClass Indicates that there is no compile-time information about the run-time value of the class — or that the Java type is not Class. This is the default qualifier, and it may not be written in source code. @ClassValBottom Type given to the null literal. It may not be written in source code. Subtyping rules Figure 21.1 shows part of the type hierarchy of the ClassVal type system. @ClassVal(A) is a subtype of @ClassVal(B) if A is a subset of B. @ClassBound(A) is a subtype of @ClassBound(B) if A is a subset of B. @ClassVal(A) is a subtype of @ClassBound(B) if A is a subset of B. 21.1.2 MethodVal Checker The MethodVal Checker defines the following annotations: @MethodVal(String[] className, String[] methodName, int[] params) Indicates that an expression of type Method or Constructor has a run-time value in a given set. If the set has size n, then each of @MethodVal’s arguments is an array of size n, and the ith method in the set is represented by { className[i], methodName[i], params[i] }. For a constructor, the method name is “ ”. Consider the following example: @MethodVal(className={"java.util.HashMap", "java.util.HashMap"}, methodName={"containsKey", "containsValue"}, params={1, 1}) 128 @UnknownMethod @MethodVal(className={"java.lang.String", "java.lang.String"},methodName={"toString","equals"},params={0,1}) @MethodVal(className="java.lang.String",methodName="equals",params=1) @MethodValBottom Figure 21.2: Partial type hierarchy for the MethodVal type system. The type qualifiers in gray (@UnknownMethod and @MethodValBottom) should never be written in source code; they are used internally by the type system. This @MethodVal annotation indicates that the Method is either HashMap.containsKey with 1 formal parameter or HashMap.containsValue with 1 formal parameter. The @MethodVal type qualifier indicates the number of parameters that the method takes, but not their type. This means that the Checker Framework’s reflection resolution cannot distinguish among overloaded methods. @UnknownMethod Indicates that there is no compile-time information about the run-time value of the method — or that the Java type is not Method or Constructor. This is the default qualifier, and it may not be written in source code. @MethodValBottom Type given to the null literal. It may not be written in source code. Subtyping rules Figure 21.2 shows part of the type hierarchy of the MethodVal type system. @MethodVal(classname=CA, methodname=MA, params=PA) is a subtype of @MethodVal(classname=CB, methodname=MB, params=PB) if ∀indexesi∃an index j : CA[i] = CB[ j], MA[i] = MA[ j], andPA[i] = PB[ j] where CA, MA, and PA are lists of equal size and CB, MB, and PB are lists of equal size. 21.1.3 MethodVal and ClassVal inference The developer rarely has to write @ClassVal or @MethodVal annotations, because the Checker Framework infers them according to Figure 21.3. Most readers can skip this section, which explains the inference rules. The ClassVal Checker infers the exact class name (@ClassVal) for a Class literal (C.class), and for a static method call (e.g., Class.forName(arg), ClassLoader.loadClass(arg), ...) if the argument is a statically computable expression. In contrast, it infers an upper bound (@ClassBound) for instance method calls (e.g., obj.getClass()). The MethodVal Checker infers @MethodVal annotations for Method and Constructor types that have been created using a method call to Java’s Reflection API: • Class.getMethod(String name, Class>... paramTypes) • Class.getConstructor(Class>... paramTypes) Note that an exact class name is necessary to precisely resolve reflectively-invoked constructors since a constructor in a subclass does not override a constructor in its superclass. This means that the MethodVal Checker does not infer a @MethodVal annotation for Class.getConstructor if the type of that class is @ClassBound. In contrast, either an exact class name or a bound is adequate to resolve reflectively-invoked methods because of the subtyping rules for overridden methods. 129 bn is the binary name of C C.class : @ClassVal(bn) s : @StringVal(ν) Class.forName(s) : @ClassVal(ν) e : τ bn is the binary name of τ e.getClass() : @ClassBound(bn) (e : @ClassBound(ν) ∨ e : @ClassVal(ν)) s : @StringVal(µ) p : @ArrayLen(π) e.getMethod(s,p) : @MethodVal(cn=ν,mn=µ,np=π) e : @ClassVal(ν) p : @ArrayLen(π) e.getConstructor(p) : @MethodVal(cn=ν, mn = " ", np = π) Figure 21.3: Example inference rules for @ClassVal, @ClassBound, and @MethodVal. Additional rules exist for expressions with similar semantics but that call methods with different names or signatures. 21.2 Reflection resolution example Consider the following example, in which the Nullness Checker employs reflection resolution to avoid issuing a false positive warning. public class LocationInfo { @NonNull Location getCurrentLocation() { } ... } public class Example { LocationInfo privateLocation = ... ; String getCurrentCity() throws Exception { Method getCurrentLocationObj = LocationInfo.class.getMethod("getCurrentLocation"); Location currentLocation = (Location) getCurrentLocationObj.invoke(privateLocation); return currentLocation.nameOfCity(); } } When reflection resolution is not enabled, the Nullness Checker uses conservative annotations on the Method.invoke method signature: @Nullable Object invoke(@NonNull Object recv, @NonNull Object ... args) This causes the Nullness Checker to issue the following warning even though currentLocation cannot be null. error: [dereference.of.nullable] dereference of possibly-null reference currentLocation return currentLocation.nameOfCity(); ^ 1 error When reflection resolution is enabled, the MethodVal Checker infers that the @MethodVal annotation for getCurrentLocationObj is: @MethodVal(className="LocationInfo", methodName="getCurrentLocation", params=0) Based on this @MethodVal annotation, the reflection resolver determines that the reflective method call represents a call to getCurrentLocation in class LocationInfo. The reflection resolver uses this information to provide the following precise procedure summary to the Nullness Checker, for this call site only: 130 @NonNull Object invoke(@NonNull Object recv, @Nullable Object ... args) Using this more precise signature, the Nullness Checker does not issue the false positive warning shown above. 131 Chapter 22 Subtyping Checker The Subtyping Checker enforces only subtyping rules. It operates over annotations specified by a user on the command line. Thus, users can create a simple type-checker without writing any code beyond definitions of the type qualifier annotations. The Subtyping Checker can accommodate all of the type system enhancements that can be declaratively specified (see Chapter 30). This includes type introduction rules (implicit annotations, e.g., literals are implicitly considered @NonNull) via the @ImplicitFor meta-annotation, and other features such as flow-sensitive type qualifier inference (Section 25.4) and qualifier polymorphism (Section 24.2). The Subtyping Checker is also useful to type system designers who wish to experiment with a checker before writing code; the Subtyping Checker demonstrates the functionality that a checker inherits from the Checker Framework. If you need typestate analysis, then you can extend a typestate checker, much as you would extend the Subtyping Checker if you do not need typestate analysis. For more details (including a definition of “typestate”), see Chapter 23.1. See Section 32.7.1 for a simpler alternative. For type systems that require special checks (e.g., warning about dereferences of possibly-null values), you will need to write code and extend the framework as discussed in Chapter 30. 22.1 Using the Subtyping Checker The Subtyping Checker is used in the same way as other checkers (using the -processor org.checkerframework.common.subtyping.SubtypingChecker option; see Chapter 2), except that it requires an additional annotation processor argument via the standard “-A” switch. One of the two following arguments must be used with the Subtyping Checker: • Provide the fully-qualified class name(s) of the annotation(s) in the custom type system through the -Aquals option, using a comma-no-space-separated notation: javac -classpath /full/path/to/myProject/bin:/full/path/to/myLibrary/bin \ -processor org.checkerframework.common.subtyping.SubtypingChecker \ -Aquals=myPackage.qual.MyQual,myPackage.qual.OtherQual MyFile.java ... The annotations listed in -Aquals must be accessible to the compiler during compilation in the classpath. In other words, they must already be compiled (and, typically, be on the javac classpath) before you run the Subtyping Checker with javac. It is not sufficient to supply their source files on the command line. • Provide the fully-qualified paths to a set of directories that contain the annotations in the custom type system through the -AqualDirs option, using a colon-no-space-separated notation. For example: javac -classpath /full/path/to/myProject/bin:/full/path/to/myLibrary/bin \ -processor org.checkerframework.common.subtyping.SubtypingChecker \ -AqualDirs=/full/path/to/myProject/bin:/full/path/to/myLibrary/bin MyFile.java 132 Note that in these two examples, the compiled class file of the myPackage.qual.MyQual and myPackage.qual.OtherQual annotations must exist in either the myProject/bin directory or the myLibrary/bin directory. The following placement of the class files will work with the above commands: .../myProject/bin/myPackage/qual/MyQual.class .../myLibrary/bin/myPackage/qual/OtherQual.class The two options can be used at the same time to provide groups of annotations from directories, and individually named annotations. To suppress a warning issued by the Subtyping Checker, use a @SuppressWarnings annotation, with the argument being the unqualified, uncapitalized name of any of the annotations passed to -Aquals. This will suppress all warnings, regardless of which of the annotations is involved in the warning. (As a matter of style, you should choose one of the annotations as your @SuppressWarnings key and stick with it for that entire type hierarchy.) 22.2 Subtyping Checker example Consider a hypothetical Encrypted type qualifier, which denotes that the representation of an object (such as a String, CharSequence, or byte[]) is encrypted. To use the Subtyping Checker for the Encrypted type system, follow three steps. 1. Define two annotations for the Encrypted and PossiblyUnencrypted qualifiers: package myPackage.qual; import java.lang.annotation.ElementType; import java.lang.annotation.Target; /** * Denotes that the representation of an object is encrypted. */ @SubtypeOf(PossiblyUnencrypted.class) @ImplicitFor(literal={LiteralKind.NULL}) @DefaultFor({TypeUseLocation.LOWER_BOUND}) @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) public @interface Encrypted {} package myPackage.qual; import import import import org.checkerframework.framework.qual.DefaultQualifierInHierarchy; org.checkerframework.framework.qual.SubtypeOf; java.lang.annotation.ElementType; java.lang.annotation.Target; /** * Denotes that the representation of an object might not be encrypted. */ @DefaultQualifierInHierarchy @SubtypeOf({}) @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) public @interface PossiblyUnencrypted {} Note that all custom annotations must have the @Target(ElementType.TYPE_USE) meta-annotation. See Section 30.4.1. Don’t forget to compile these classes: $ javac myPackage/qual/Encrypted.java myPackage/qual/PossiblyUnencrypted.java 133 The resulting .class files should either be on your classpath, or on the processor path (set via the -processorpath command-line option to javac). 2. Write @Encrypted annotations in your program (say, in file YourProgram.java): import myPackage.qual.Encrypted; ... public @Encrypted String encrypt(String text) { // ... } // Only send encrypted data! public void sendOverInternet(@Encrypted String msg) { // ... } void sendText() { // ... @Encrypted String ciphertext = encrypt(plaintext); sendOverInternet(ciphertext); // ... } void sendPassword() { String password = getUserPassword(); sendOverInternet(password); } You may also need to add @SuppressWarnings annotations to the encrypt and decrypt methods. Analyzing them is beyond the capability of any realistic type system. 3. Invoke the compiler with the Subtyping Checker, specifying the @Encrypted annotation using the -Aquals option. You should add the Encrypted classfile to the processor classpath: javac -processorpath myqualpath -processor org.checkerframework.common.subtyping.SubtypingChecker YourProgram.java:42: incompatible types. found : @myPackage.qual.PossiblyUnencrypted java.lang.String required: @myPackage.qual.Encrypted java.lang.String sendOverInternet(password); ^ 4. You can also provide the fully-qualified paths to a set of directories that contain the qualifiers using the -AqualDirs option, and add the directories to the boot classpath, for example: javac -classpath /full/path/to/myProject/bin:/full/path/to/myLibrary/bin \ -processor org.checkerframework.common.subtyping.SubtypingChecker \ -AqualDirs=/full/path/to/myProject/bin:/full/path/to/myLibrary/bin YourProgram.java Note that in these two examples, the compiled class file of the myPackage.qual.Encrypted and myPackage.qual.PossiblyUnencrypted annotations must exist in either the myProject/bin directory or the myLibrary/bin directory. The following placement of the class files will work with the above commands: .../myProject/bin/myPackage/qual/Encrypted.class .../myProject/bin/myPackage/qual/PossiblyUnencrypted.class Also, see the example project in the docs/examples/subtyping-extension directory. 134 @MyTypeUnknown @MyType @NotMyType @MyTypeBottom Figure 22.1: Type system for a type alias or typedef type system. The type system designer may choose to omit some of these types, but this is the general case. The type system designer’s choice of defaults affects the interpretation of unannotated code, which affects the guarantees given for unannotated code. 22.3 Type aliases and typedefs A type alias or typedef is a type that shares the same representation as another type but is conceptually distinct from it. For example, some strings in your program may be street addresses; others may be passwords; and so on. You wish to indicate, for each string, which one it is, and to avoid mixing up the different types of strings. Likewise, you could distinguish integers that are offsets from those that are absolute values. Creating a new type makes your code easier to understand by conveying the intended use of each variable. It also prevents errors that come from using the wrong type or from mixing incompatible types in an operation. If you want to create a type alias or typedef, you have multiple options: a regular Java subtype, the Units Checker (Chapter 17, page 112), the Fake Enum Checker (Chapter 9, page 79), or the Subtyping Checker. A Java subtype is easy to create and does not require a tool such as the Checker Framework; for instance, you would declare class Address extends String. There are a number of limitations to this “pseudo-typedef”, however [Goe06]. Primitive types and final types (including String) cannot be extended. Equality and identity tests can return incorrect results when a wrapper object is used. Existing return types in code would need to be changed, which is easy with an annotation but disruptive to change the Java type. Therefore, it is best to avoid the pseudo-typedef antipattern. The Units Checker (Chapter 17, page 112) is useful for the particular case of units of measurement, such as kilometers verses miles. The Fake Enum Checker (Chapter 9, page 79) builds in a set of assumptions. If those fit your use case, then it’s easiest to use the Fake Enum Checker (though you can achieve them using the Subtyping Checker). The Fake Enum Checker forbids mixing of fenums of different types, or fenums and unannotated types. For instance, binary operations other than string concatenations are forbidden, such as NORTH+1, NORTH+MONDAY, and NORTH==MONDAY. However, NORTH+SOUTH is permitted. By default, the Subtyping Checker does not forbid any operations. If you choose to use the Subtyping Checker, then you have an additional design choice to make about the type system. In the general case, your type system will look something like Figure 22.1. References whose type is @MyType are known to store only values from your new type. There is no such guarantee for @MyTypeUnknown and @NotMyType, but those types mean different things. An expression of type @NotMyType is guaranteed never to evaluate to a value of your new type. An expression of type @MyTypeUnknown may evaluate to any value — including values of your new type and values not of your new type. (@MyTypeBottom is the type of null and is also used for dead code and erroneous situations; it can be ignored for this discussion.) A key choice for the type system designer is which type is the default. That is, if a programmer does not write @MyType on a given type use, should that type use be interpreted as @MyTypeUnknown or as @NotMyType? • If unannotated types are interpreted as @NotMyType, then the type system enforces very strong separation between your new type and all other types. Values of your type will never mix with values of other types. If you don’t see @MyType written explicitly on a type, you will know that it does not contain values of your type. • If unannotated types are interpreted as @MyTypeUnknown, then a generic, unannotated type may contain a value of your new type. In this case, @NotMyType does not need to exist, and @MyTypeBottom may or may not exist in 135 your type system. A downside of the stronger guarantee that comes from using @NotMyType as the default is the need to write additional annotations. For example, if @NotMyType is the default, this code does not typecheck: void method(Object o) { ... } void use(List list) { method(list.get(0)); } Because (implicit) upper bounds are interpreted as the top type (see Section 24.1.2), this is interpreted as void method(@NotMyType Object o) { ... } <@U extends @MyTypeUnknown Object> void use(List list) { // type error: list.get(0) has type @MyTypeUnknown, method expects @NotMyType method(list.get(0)); } To make the code type-check, it is necessary to write an explicit annotation, either to restrict use’s argument or to expand method’s parameter type. 136 Chapter 23 Third-party checkers The Checker Framework has been used to build other checkers that are not distributed together with the framework. This chapter mentions just a few of them. They are listed in chronological order; older ones appear first and newer ones appear last. They are externally-maintained, so if you have problems or questions, you should contact their maintainers rather than the Checker Framework maintainers. If you want a reference to your checker included in this chapter, send us a link and a short description. 23.1 Typestate checkers In a regular type system, a variable has the same type throughout its scope. In a typestate system, a variable’s type can change as operations are performed on it. The most common example of typestate is for a File object. Assume a file can be in two states, @Open and @Closed. Calling the close() method changes the file’s state. Any subsequent attempt to read, write, or close the file will lead to a run-time error. It would be better for the type system to warn about such problems, or guarantee their absence, at compile time. Just as you can extend the Subtyping Checker to create a type-checker, you can extend a typestate checker to create a type-checker that supports typestate analysis. An extensible typestate analysis by Adam Warski that builds on the Checker Framework is available at http://www.warski.org/typestate.html. 23.1.1 Comparison to flow-sensitive type refinement The Checker Framework’s flow-sensitive type refinement (Section 25.4) implements a form of typestate analysis. For example, after code that tests a variable against null, the Nullness Checker (Chapter 3) treats the variable’s type as @NonNull T, for some T. For many type systems, flow-sensitive type refinement is sufficient. But sometimes, you need full typestate analysis. This section compares the two. (Unused variables (Section 25.7) also have similarities with typestate analysis and can occasionally substitute for it. For brevity, this discussion omits them.) A typestate analysis is easier for a user to create or extend. Flow-sensitive type refinement is built into the Checker Framework and is optionally extended by each checker. Modifying the rules requires writing Java code in your checker. By contrast, it is possible to write a simple typestate checker declaratively, by writing annotations on the methods (such as close()) that change a reference’s typestate. A typestate analysis can change a reference’s type to something that is not consistent with its original definition. For example, suppose that a programmer decides that the @Open and @Closed qualifiers are incomparable — neither is a subtype of the other. A typestate analysis can specify that the close() operation converts an @Open File into a @Closed File. By contrast, flow-sensitive type refinement can only give a new type that is a subtype of the declared 137 type — for flow-sensitive type refinement to be effective, @Closed would need to be a child of @Open in the qualifier hierarchy (and close() would need to be treated specially by the checker). 23.2 Units and dimensions checker A checker for units and dimensions is available at https://www.lexspoon.org/expannots/. Unlike the Units Checker that is distributed with the Checker Framework (see Section 17), this checker includes dynamic checks and permits annotation arguments that are Java expressions. This added flexibility, however, requires that you use a special version both of the Checker Framework and of the javac compiler. 23.3 Thread locality checker Loci [WPM+ 09], a checker for thread locality, is available at http://www.it.uu.se/research/upmarc/loci/. 23.4 Safety-Critical Java checker A checker for Safety-Critical Java (SCJ, JSR 302) [TPV10] is available at http://sss.cs.purdue.edu/projects/ oscj/checker/checker.html. Developer resources are available at the project page https://code.google.com/ archive/p/scj-jsr302/. 23.5 Generic Universe Types checker A checker for Generic Universe Types [DEM11], a lightweight ownership type system, is available from https: //ece.uwaterloo.ca/~wdietl/ownership/. 23.6 EnerJ checker A checker for EnerJ [SDF+ 11], an extension to Java that exposes hardware faults in a safe, principled manner to save energy with only slight sacrifices to the quality of service, is available from http://sampa.cs.washington.edu/ research/approximation/enerj.html. 23.7 CheckLT taint checker CheckLT uses taint tracking to detect illegal information flows, such as unsanitized data that could result in a SQL injection attack. CheckLT is available from http://checklt.github.io/. 23.8 SPARTA information flow type-checker for Android SPARTA is a security toolset aimed at preventing malware from appearing in an app store. SPARTA provides an information-flow type-checker that is customized to Android but can also be applied to other domains. The SPARTA toolset is available from https://checkerframework.org/sparta/. The paper “Collaborative verification of information flow for a high-assurance app store” appeared in CCS 2014. 138 23.9 Immutability checkers: IGJ, OIGJ, and Javari Javari [TE05], IGJ [ZPA+ 07], and OIGJ [ZPL+ 10] are type systems that enforce immutability constraints. Typecheckers for all three type systems were distributed with the Checker Framework through release 1.9.13 (dated 1 April 2016). If you wish to use them, install Checker Framework version 1.9.13. They were removed from the main distribution on June 1, 2016 because the implementations were not being maintained as the Checker Framework evolved. The type systems are valuable, and some people found the typecheckers useful. However, we wanted to focus on distributing checkers that are currently being maintained. 23.10 Read Checker for CERT FIO08-J CERT rule FIO08-J describes a rule for the correct handling of characters/bytes read from a stream. The Read Checker enforces this rule. It is available from https://github.com/opprop/ReadChecker. 23.11 SQL checker that supports multiple dialects jOOQ is a database API that lets you build typesafe SQL queries. jOOQ version 3.0.9 and later ships with a SQL checker that provides even more safety: it ensures that you don’t use SQL features that are not supported by your database implementation. You can learn about the SQL checker at https://blog.jooq.org/2016/05/09/ jsr-308-and-the-checker-framework-add-even-more-typesafety-to-jooq-3-9/. 23.12 Glacier: Class immutability Glacier [CNA+ 17] enforces transitive class immutability in Java. According to its webpage: • Transitive: if a class is immutable, then every field must be immutable. This means that all reachable state from an immutable object’s fields is immutable. • Class: the immutability of an object depends only on its class’s immutability declaration. • Immutability: state in an object is not changable through any reference to the object. 139 Chapter 24 Generics and polymorphism This chapter describes support for Java generics (also known as “parametric polymorphism”) and polymorphism over type qualifiers. Section 24.2 describes support for polymorphism over type qualifiers. 24.1 Generics (parametric polymorphism or type polymorphism) The Checker Framework fully supports type-qualified Java generic types and methods (also known in the research literature as “parametric polymorphism”). When instantiating a generic type, clients supply the qualifier along with the type argument, as in List<@NonNull String>. 24.1.1 Raw types Before running any pluggable type-checker, we recommend that you eliminate raw types from your code (e.g., your code should use List<...> as opposed to List). Your code should compile without warnings when using the standard Java compiler and the -Xlint:unchecked -Xlint:rawtypes command-line options. Using generics helps prevent type errors just as using a pluggable type-checker does, and makes the Checker Framework’s warnings easier to understand. If your code uses raw types, then the Checker Framework will do its best to infer the Java type parameters and the type qualifiers. If it infers imprecise types that lead to type-checking warnings elsewhere, then you have two options. You can convert the raw types such as List to parameterized types such as List , or you can supply the -AignoreRawTypeArguments command-line option. That option causes the Checker Framework to ignore all subtype tests for type arguments that were inferred for a raw type. 24.1.2 Restricting instantiation of a generic class When you define a generic class in Java, the extends clause of the generic type parameter (known as the “upper bound”) requires that the corresponding type argument must be a subtype of the bound. For example, given the definition class G {...}, the upper bound is Number and a client can instantiate it as G or G but not G . You can write a type qualifier on the extends clause to make the upper bound a qualified type. For example, you can declare that a generic list class can hold only non-null values: class MyList {...} MyList<@NonNull String> m1; MyList<@Nullable String> m2; // OK // error 140 That is, in the above example, all arguments that replace T in MyList must be subtypes of @NonNull Object. Conceptually, each generic type parameter has two bounds — a lower bound and an upper bound — and at instantiation, the type argument must be within the bounds. Java only allows you to specify the upper bound; the lower bound is implicitly the bottom type void. The Checker Framework gives you more power: you can specify both an upper and lower bound for type parameters and wildcards. For the upper bound, write a type qualifier on the extends clause, and for the lower bound, write a type qualifier on the type variable. class MyList<@LowerBound T extends @UpperBound Object> { ... } For a concrete example, recall the type system of the Regex Checker (see Figure 11.1, page 86) in which @Regex(0) :> @Regex(1) :> @Regex(2) :> @Regex(3) :> . . . . class MyRegexes<@Regex(5) T extends @Regex(1) String> { ... } MyRegexes<@Regex(0) MyRegexes<@Regex(1) MyRegexes<@Regex(3) MyRegexes<@Regex(5) MyRegexes<@Regex(6) String> String> String> String> String> mu; m1; m3; m5; m6; // // // // // error - @Regex(0) is not a subtype of @Regex(1) OK OK OK error - @Regex(6) is not a supertype of @Regex(5) The above declaration states that the upper bound of the type variable is @Regex(1) String and the lower bound is @Regex(5) void. That is, arguments that replace T in MyList must be subtypes of @Regex(1) String and supertypes of @Regex(5) void. Since void cannot be used to instantiate a generic class, MyList may be instantiated with @Regex(1) String through @Regex(5) String. To specify an exact bound, place the same annotation on both bounds. For example: class MyListOfNonNulls<@NonNull T extends @NonNull Object> { ... } class MyListOfNullables<@Nullable T extends @Nullable Object> { ... } MyListOfNonNulls<@NonNull Number> v1; MyListOfNonNulls<@Nullable Number> v2; MyListOfNullables<@NonNull Number> v4; MyListOfNullables<@Nullable Number> v3; // // // // OK error error OK It is an error if the lower bound is not a subtype of the upper bound. class MyClass<@Nullable T extends @NonNull Object> // error: @Nullable is not a supertype of @NonNull Defaults If the extends clause is omitted, then the upper bound defaults to @TopType Object. If no type annotation is written on the type parameter name, then the lower bound defaults to @BottomType void. If the extends clause is written but contains no type qualifier, then the normal defaulting rules apply to the type in the extends clause (see Section 25.3.2). These rules mean that even though in Java the following two declarations are equivalent: class MyClass class MyClass they may specify different type qualifiers on the upper bound, depending on the type system’s defaulting rules. 141 24.1.3 Type annotations on a use of a generic type variable A type annotation on a use of a generic type variable overrides/ignores any type qualifier (in the same type hierarchy) on the corresponding actual type argument. For example, suppose that T is a formal type parameter. Then using @Nullable T within the scope of T applies the type qualifier @Nullable to the (unqualified) Java type of T. This feature is only rarely used. Here is an example of applying a type annotation to a generic type variable: class MyClass2 { ... @Nullable T myField = null; ... } The type annotation does not restrict how MyClass2 may be instantiated. In other words, both MyClass2<@NonNull String> and MyClass2<@Nullable String> are legal, and in both cases @Nullable T means @Nullable String. In MyClass2<@Interned String>, @Nullable T means @Nullable @Interned String. Defaulting never affects a use of a type variable, even if the type variable use has no explicit annotation. Defaulting helps to choose a single type qualifier for a concrete Java class or interface. By contrast, a type variable use represents a set of possible types. 24.1.4 Annotations on wildcards At an instantiation of a generic type, a Java wildcard indicates that some constraints are known on the type argument, but the type argument is not known exactly. For example, you can indicate that the type parameter for variable ls is some unknown subtype of CharSequence: List extends CharSequence> ls; ls = new ArrayList (); ls = new ArrayList (); // OK // error: Integer is not a subtype of CharSequence For more details about wildcards, see the Java tutorial on wildcards or JLS §4.5.1. You can write a type annotation on the bound of a wildcard: List extends @NonNull CharSequence> ls; ls = new ArrayList<@NonNull String>(); // OK ls = new ArrayList<@Nullable String>(); // error: @Nullable is not a subtype of @NonNull Conceptually, every wildcard has two bounds — an upper bound and a lower bound. Java only permits you to write the upper bound (with extends SomeType>) or the lower bound (with super OtherType>), but not both; the unspecified bound is implicitly the top type Object or the bottom type void. The Checker Framework is more flexible: it lets you simultaneously write annotations on both the top and the bottom type. To annotate the implicit bound, write the type annotation before the ?. For example: List<@LowerBound ? extends @UpperBound CharSequence> lo; List<@UpperBound ? super @NonNull Number> ls; For an unbounded wildcard (>, with neither bound specified), the annotation in front of a wildcard applies to both bounds. The following three declarations are equivalent (except that you cannot write the bottom type void; note that Void does not denote the bottom type): List<@NonNull ?> lnn; List<@NonNull ? extends @NonNull Object> lnn; List<@NonNull ? super @NonNull void> lnn; Note that the annotation in front of a type parameter always applies to its lower bound, because type parameters can only be written with extends and never super. The defaulting rules for wildcards also differ from those of type parameters (see Section 25.3.4). 142 24.1.5 Examples of qualifiers on a type parameter Recall that @Nullable X is a supertype of @NonNull X, for any X. Most of the following types mean different things: class class class class class MyList1<@Nullable T> { ... } MyList1a<@Nullable T extends @Nullable Object> { ... } // same as MyList1 MyList2<@NonNull T extends @NonNull Object> { ... } MyList2a { ... } // same as MyList2 MyList3 { ... } MyList1 and MyList1a must be instantiated with a nullable type. The implementation of MyList1 must be able to consume (store) a null value and produce (retrieve) a null value. MyList2 and MyList2a must be instantiated with non-null type. The implementation of MyList2 has to account for only non-null values — it does not have to account for consuming or producing null. MyList3 may be instantiated either way: with a nullable type or a non-null type. The implementation of MyList3 must consider that it may be instantiated either way — flexible enough to support either instantiation, yet rigorous enough to impose the correct constraints of the specific instantiation. It must also itself comply with the constraints of the potential instantiations. One way to express the difference among MyList1, MyList2, and MyList3 is by comparing what expressions are legal in the implementation of the list — that is, what expressions may appear in the ellipsis in the declarations above, such as inside a method’s body. Suppose each class has, in the ellipsis, these declarations: T t; @Nullable T nble; @NonNull T nn; void add(T arg) { } T get(int i) { } // Section "Type annotations on a use of a generic type variable", below, // further explains the meaning of "@Nullable T" and "@NonNull T". Then the following expressions would be legal, inside a given implementation — that is, also within the ellipses. (Compilable source code appears as file checker-framework/checker/tests/nullness/generics/GenericsExample.java.) MyList1 MyList2 MyList3 t = null; OK error error t = nble; OK error error nble = null; OK OK OK nn = null; error error error t = this.get(0); OK OK OK nble = this.get(0); OK OK OK nn = this.get(0); error OK error this.add(t); OK OK OK this.add(nble); OK error error this.add(nn); OK OK OK The differences are more significant when the qualifier hierarchy is more complicated than just @Nullable and @NonNull. 24.1.6 Covariant type parameters Java types are invariant in their type parameter. This means that A is a subtype of B only if X is identical to Y. For example, ArrayList is a subtype of List , but neither ArrayList nor List is a subtype of List . (If they were, there would be a loophole in the Java type system.) For the same reason, type parameter annotations are treated invariantly. For example, List<@Nullable String> is not a subtype of List . When a type parameter is used in a read-only way — that is, when values of that type are read but are never assigned — then it is safe for the type to be covariant in the type parameter. Use the @Covariant annotation to indicate 143 this. When a type parameter is covariant, two instantiations of the class with different type arguments have the same subtyping relationship as the type arguments do. For example, consider Iterator. Its elements can be read but not written, so Iterator<@Nullable String> can be a subtype of Iterator without introducing a hole in the type system. Therefore, its type parameter is annotated with @Covariant. The first type parameter of Map.Entry is also covariant. Another example would be the type parameter of a hypothetical class ImmutableList. The @Covariant annotation is trusted but not checked. If you incorrectly specify as covariant a type parameter that can be written (say, the class performs a set operation or some other mutation on an object of that type), then you have created an unsoundness in the type system. For example, it would be incorrect to annotate the type parameter of ListIterator as covariant, because ListIterator supports a set operation. 24.1.7 Method type argument inference and type qualifiers Sometimes method type argument inference does not interact well with type qualifiers. In such situations, you might need to provide explicit method type arguments, for which the syntax is as follows: Collections.<@MyTypeAnnotation Object>sort(l, c); This uses Java’s existing syntax for specifying a method call’s type arguments. 24.1.8 The Bottom type Many type systems have a *Bottom type that is used only for the null value, dead code, and some erroneous situations. A programmer should rarely write the bottom type. One use is on a lower bound, to indicate that any type qualifier is permitted. A lower-bounded wildcard indicates that a consumer method can accept a collection containing any Java type above some Java type, and you can add the bottom type qualifier as well: public static void addNumbers(List super @SignednessBottom Integer> list) { ... } 24.2 Qualifier polymorphism The Checker Framework supports type qualifier polymorphism for methods, which permits a single method to have multiple different qualified type signatures. This is similar to Java’s generics, but is used in situations where you cannot use Java generics. If you can use generics, you typically do not need to use a polymorphic qualifier such as @PolyNull. To use a polymorphic qualifier, just write it on a type. For example, you can write @PolyNull anywhere in a method that you would write @NonNull or @Nullable. A polymorphic qualifier can be used in a method signature or body. It may not be used on a class or field. A method written using a polymorphic qualifier conceptually has multiple versions, somewhat like the generics feature of Java or a template in C++. In each version, each instance of the polymorphic qualifier has been replaced by the same other qualifier from the hierarchy. See the examples below in Section 24.2.1. The method body must type-check with all signatures. A method call is type-correct if it type-checks under any one of the signatures. If a call matches multiple signatures, then the compiler uses the most specific matching signature for the purpose of type-checking. This is the same as Java’s rule for resolving overloaded methods. To define a polymorphic qualifier, mark the definition with @PolymorphicQualifier. For example, @PolyNull is a polymorphic type qualifier for the Nullness type system: import java.lang.annotation.ElementType; import java.lang.annotation.Target; import org.checkerframework.framework.qual.PolymorphicQualifier; @PolymorphicQualifier 144 @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) public @interface PolyNull { } See Section 24.2.3 for a way you can sometimes avoid defining a new polymorphic qualifier. 24.2.1 Examples of using polymorphic qualifiers As an example of the use of @PolyNull, method Class.cast returns null if and only if its argument is null: @PolyNull T cast(@PolyNull Object obj) { ... } This is like writing: @NonNull T cast( @NonNull Object obj) { ... } @Nullable T cast(@Nullable Object obj) { ... } except that the latter is not legal Java, since it defines two methods with the same Java signature. As another example, consider // Returns null if either argument is null. @PolyNull T max(@PolyNull T x, @PolyNull T y); which is like writing @NonNull T max( @NonNull T x, @NonNull T y); @Nullable T max(@Nullable T x, @Nullable T y); At a call site, the most specific applicable signature is selected. Another way of thinking about which one of the two max variants is selected is that the nullness annotations of (the declared types of) both arguments are unified to a type that is a supertype of both, also known as the least upper bound or lub. If both arguments are @NonNull, their unification (lub) is @NonNull, and the method return type is @NonNull. But if even one of the arguments is @Nullable, then the unification (lub) is @Nullable, and so is the return type. 24.2.2 Relationship to subtyping and generics Qualifier polymorphism has the same purpose and plays the same role as Java’s generics. You use them in the same cases, such as: • A method operates on collections with different types of elements. • Two different arguments have the same type, without constraining them to be one specific type. • A method returns a value of the same type as its argument. If a method is written using Java generics, it usually does not need qualifier polymorphism. If you can use Java’s generics, then that is often better. On the other hand, if you have legacy code that is not written generically, and you cannot change it to use generics, then you can use qualifier polymorphism to achieve a similar effect, with respect to type qualifiers only. The Java compiler still treats the base Java types non-generically. In some cases, you don’t need qualifier polymorphism because subtyping already provides the needed functionality. String is a supertype of @Interned String, so a method toUpperCase that is declared to take a String parameter can also be called on an @Interned String argument. 145 24.2.3 The @PolyAll qualifier applies to every type system Each type system has its own polymorphic type qualifier. If some method is qualifier-polymorphic over every type qualifier hierarchy, then you can use @PolyAll. This is better than trying to write every @Poly* qualifier on that method. For example, a method that only performs == on array elements will work no matter what the array’s element types are: /** * Searches for the first occurrence of the given element in the array, * testing for equality using == (not the equals method). */ public static int indexOfEq(@PolyAll Object[] a, @Nullable Object elt) { for (int i=0; i s1, Stack<@PolyNull Object> s2) { s1.push(s2.pop()); } In this particular example, it would be cleaner to rewrite your code to use Java generics, if you can do so: void moveBetweenStacks(Stack s1, Stack s2) { s1.push(s2.pop()); } It is unusual, but permitted, to write just one polymorphic qualifier, on a return type. This is just like it is unusual, but permitted, to write just one occurrence of a generic type parameter, on a return type. An example of such a method is Collections.emptyList(). 146 24.2.5 Using a single polymorphic qualifier in a method signature As explained in Section 24.2.4, you will usually use a polymorphic qualifier multiple times in a signature. This section describes situations when it makes sense to write just one polymorphic qualifier in a method signature. Some of these situations can be avoided by writing a generic method, but in legacy code it may not be possible for you to change a method to be generic. Using a single polymorphic qualifier on an element type It can make sense to use a polymorphic qualifier just once, on an array or generic element type. For example, consider a routine that returns the index, in an array, of a given element: public static int indexOf(@PolyNull Object[] a, @Nullable Object elt) { ... } If @PolyNull were replaced with either @Nullable or @NonNull, then one of these safe client calls would be rejected: @Nullable Object[] a1; @NonNull Object[] a2; indexOf(a1, someObject); indexOf(a2, someObject); Of course, it would be better style to use a generic method, as in either of these signatures: public static int indexOf(T[] a, @Nullable Object elt) { ... } public static int indexOf(T[] a, T elt) { ... } This example uses arrays, but analogous examples exist that use collections. Using a single polymorphic qualifier to indicate all arguments are legal A single @PolyAll annotation can indicate that any possible value is permitted to be passed. For example: boolean eq(@PolyAll Object other) { return this == other; } The @PolyAll annotation applies to all type systems. It would be infeasible to write the top qualifier for every possible type system and to update this method’s annotation whenever a new type system is defined. By contrast, a declaration of eq without @PolyAll: boolean eq(Object other) { return this == other; } would reject some calls, in type systems where the default type qualifier applied to Object is not the top type. A related use of a single polymorphic qualifier is to override a generic type. For example, the annotation on Comparable.compareTo() is: public interface Comparable { @Pure int compareTo(@PolyAll @NonNull T a1); } which indicates that, for every type system other than the nullness type system, every value is permitted as an argument, regardless of how the Comparable type was instantiated. For example, this call is legal: 147 Comparable<@MyBottom String> cble; @MyTop String s; ... cble.compareTo(s); 148 Chapter 25 Advanced type system features This chapter describes features that are automatically supported by every checker written with the Checker Framework. You may wish to skim or skip this chapter on first reading. After you have used a checker for a little while and want to be able to express more sophisticated and useful types, or to understand more about how the Checker Framework works, you can return to it. 25.1 Invariant array types Java’s type system is unsound with respect to arrays. That is, the Java type-checker approves code that is unsafe and will cause a run-time crash. Technically, the problem is that Java has “covariant array types”, such as treating String[] as a subtype of Object[]. Consider the following example: String[] strings = new String[] {"hello"}; Object[] objects = strings; objects[0] = new Object(); String myString = strs[0]; The above code puts an Object in the array strings and thence in myString, even though myString = new Object() should be, and is, rejected by the Java type system. Java prevents corruption of the JVM by doing a costly run-time check at every array assignment; nonetheless, it is undesirable to learn about a type error only via a run-time crash rather than at compile time. When you pass the -AinvariantArrays command-line option, the Checker Framework is stricter than Java, in the sense that it treats arrays invariantly rather than covariantly. This means that a type system built upon the Checker Framework is sound: you get a compile-time guarantee without the need for any run-time checks. But it also means that the Checker Framework rejects code that is similar to what Java unsoundly accepts. The guarantee and the compile-time checks are about your extended type system. The Checker Framework does not reject the example code above, which contains no type annotations. Java’s covariant array typing is sound if the array is used in a read-only fashion: that is, if the array’s elements are accessed but the array is not modified. However, facts about read-only usage are not built into any of the type-checkers. Therefore, when using type systems along with -AinvariantArrays, you will need to suppress any warnings that are false positives because the array is treated in a read-only way. 25.2 Context-sensitive type inference for array constructors When you write an expression, the Checker Framework gives it the most precise possible type, depending on the particular expression or value. For example, when using the Regex Checker (Chapter 11, page 85), the string "hello" 149 is given type @Regex String because it is a legal regular expression (whether it is meant to be used as one or not) and the string "(foo" is given the type @Unqualified String because it is not a legal regular expression. Array constructors work differently. When you create an array with the array constructor syntax, such as the right-hand side of this assignment: String[] myStrings = {"hello"}; then the expression does not get the most precise possible type, because doing so could cause inconvenience. Rather, its type is determined by the context in which it is used: the left-hand side if it is in an assignment, the declared formal parameter type if it is in a method call, etc. In particular, if the expression {"hello"} were given the type @Regex String[], then the assignment would be illegal! But the Checker Framework gives the type String[] based on the assignment context, so the code type-checks. If you prefer a specific type for a constructed array, you can indicate that either in the context (change the declaration of myStrings) or in a new construct (change the expression to new @Regex String[] {"hello"}). 25.3 The effective qualifier on a type (defaults and inference) A checker sometimes treats a type as having a slightly different qualifier than what is written on the type — especially if the programmer wrote no qualifier at all. Most readers can skip this section on first reading, because you will probably find the system simply “does what you mean”, without forcing you to write too many qualifiers in your program. In particular, qualifiers in method bodies are extremely rare. Most of this section is applicable only to source code that is being checked by a checker. When the compiler reads a .class file that was checked by a checker, the .class file contains the explicit or defaulted annotations from the source code and no defaulting is necessary. When the compiler reads a .class file that was not checked by a checker, the .class file contains only explicit annotations and defaulting might be necessary; see Section 25.3.5 for these rules. The following steps determine the effective qualifier on a type — the qualifier that the checkers treat as being present. 1. If a type qualifier is present in the source code, that qualifier is used. 2. The type system adds implicit qualifiers. This happens whether or not the programmer has written an explicit type qualifier. Here are some examples of implicit qualifiers: • In the Nullness type system (see Chapter 3, page 25), enum values, string literals, and method receivers are always non-null. • In the Interning type system (see Chapter 6, page 55), string literals and enum values are always interned. If the type has an implicit qualifier, then it is an error to write an explicit qualifier that is equal to (redundant with) or a supertype of (weaker than) the implicit qualifier. A programmer may strengthen (write a subtype of) an implicit qualifier, however. Implicit qualifiers arise from two sources: built-in Implicit qualifiers can be built into a type system (Section 30.7), in which case the type system’s documentation explains all of the type system’s implicit qualifiers. Both of the above examples are built into the Nullness type system. programmer-declared A programmer may introduce an implicit annotation on each use of class C by writing a qualifier on the declaration of class C. If MyClass is declared as class @MyAnno MyClass {...}, then each occurrence of MyClass in the source code is treated as if it were @MyAnno MyClass. 3. If there is no explicit or implicit qualifier on a type, then a default qualifier is applied; see Section 25.3.1. At this point (after step 3), every type has a qualifier. 4. The type system may refine a qualified type on a local variable — that is, treat it as a subtype of how it was declared or defaulted. This refinement is always sound and has the effect of eliminating false positive error messages. See Section 25.4. 150 25.3.1 Default qualifier for unannotated types A type system designer, or an end-user programmer, can cause unannotated Java types to be treated as if they had a default annotation. (Defaulting never applies to uses of type varables, even if they do not have an explicit type annotation.) There are several defaulting mechanisms, for convenience and flexibility. When determining the default qualifier for a use of a type, the following rules are used in order, until one applies. (Some of these currently do not work in stub files.) • Use the innermost user-written @DefaultQualifier, as explained in this section. • Use the default specified by the type system designer (Section 30.4.4); this is usually CLIMB-to-top (Section 25.3.2). • Use @Unqualified, which the framework inserts to avoid ambiguity and simplify the programming interface for type system designers. Users do not have to worry about this detail, but type system implementers can rely on the fact that some qualifier is present. The end-user programmer specifies a default qualifier by writing the @DefaultQualifier annotation on a package, class, method, or variable declaration. The argument to @DefaultQualifier is the Class name of an annotation. The optional second argument indicates where the default applies. If the second argument is omitted, the specified annotation is the default in all locations. See the Javadoc of DefaultQualifier for details. For example, using the Nullness type system (Chapter 3): import org.checkerframework.framework.qual.*; // for DefaultQualifier[s] import org.checkerframework.checker.nullness.qual.NonNull; @DefaultQualifier(NonNull.class) class MyClass { public boolean compile(File myFile) if (!myFile.exists()) // return false; @Nullable File srcPath = ...; // ... if (srcPath.exists()) // ... } { // myFile has type "@NonNull File" no warning: myFile is non-null must annotate to specify "@Nullable File" warning: srcPath might be null @DefaultQualifier(Tainted.class) public boolean isJavaFile(File myfile) { ... } // myFile has type "@Tainted File" } If you wish to write multiple @DefaultQualifier annotations at a single location, use @DefaultQualifiers instead. For example: @DefaultQualifiers({ @DefaultQualifier(NonNull.class), @DefaultQualifier(Tainted.class) }) If @DefaultQualifier[s] is placed on a package (via the package-info.java file), then it applies to the given package and all subpackages. 151 Recall that an annotation on a class definition indicates an implicit qualifier (Section 25.3) that can only be strengthened, not weakened. This can lead to unexpected results if the default qualifier applies to a class definition. Thus, you may want to put explicit qualifiers on class declarations (which prevents the default from taking effect), or exclude class declarations from defaulting. When a programmer omits an extends clause at a declaration of a type parameter, the default still applies to the implicit upper bound. For example, consider these two declarations: class C { ... } class C { ... } // identical to previous line The two declarations are treated identically by Java, and the default qualifier applies to the Object upper bound whether it is implicit or explicit. (The @NonNull default annotation applies only to the upper bound in the extends clause, not to the lower bound in the inexpressible implicit super void clause.) 25.3.2 Defaulting rules and CLIMB-to-top Each type system defines a default qualifier. For example, the default qualifier for the Nullness Checker is @NonNull. That means that when a user writes a type such as Date, the Nullness Checker interprets it as @NonNull Date. The type system applies that default qualifier to most but not all types. In particular, unless otherwise stated, every type system uses the CLIMB-to-top rule. This rule states that the top qualifier in the hierarchy is applied to the CLIMB locations: Casts, Locals, Instanceof, and (some) iMplicit Bounds. For example, when the user writes a type such as Date in such a location, the Nullness Checker interprets it as @Nullable Date (because @Nullable is the top qualifier in the hierarchy, see Figure 3.1). The CLIMB-to-top rule is used only for unannotated source code that is being processed by a checker. For unannotated libraries (code read by the compiler in .class or .jar form), the checker uses conservative defaults (Section 25.3.5). The rest of this section explains the rationale and implementation of CLIMB-to-top. Here is the rationale for CLIMB-to-top: • Local variables are defaulted to top because type refinement (Section 25.4) is applied to local variables. If a local variable starts as the top type, then the Checker Framework refines it to the best (most specific) possible type based on assignments to it. As a result, a programmer rarely writes an explicit annotation on any of those locations. Variables defaulted to top include local variables, resource variables in the try-with-resources construct, variables in for statements, and catch arguments (known as exception parameters in the Java Language Specification). Exception parameters need to have the top type because exceptions of arbitrary qualified types can be thrown and the Checker Framework does not provide runtime checks. • Cast and instanceof types are not really defaulted to top. Rather, they are given the same type as their argument, which is the most specific possible type. That would also have been the effect if they were given the top type and then flow-sensitively refined to the type of their argument. • Implicit upper bounds are defaulted to top to allow them to be instantiated in any way. If a user declared class C { ... }, then we assume that the user intended to allow any instantiation of the class, and the declaration is interpreted as class C { ... } rather than as class C { ... }. The latter would forbid instantiations such as C<@Nullable String>, or would require rewriting of code. On the other hand, if a user writes an explicit bound such as class C { ... }, then the user intends some restriction on instantiation and can write a qualifier on the upper bound as desired. This rule means that the upper bound of class C is defaulted differently than the upper bound of class C . It would be more confusing for “Object” to be defaulted differently in class C and in an instantiation C
Source Exif Data:
File Type : PDF File Type Extension : pdf MIME Type : application/pdf PDF Version : 1.5 Linearized : No Page Count : 249 Page Mode : UseOutlines Author : Title : Subject : Creator : LaTeX with hyperref package Producer : pdfTeX-1.40.18 Create Date : 2018:06:07 15:57:57-07:00 Modify Date : 2018:06:07 15:57:57-07:00 Trapped : False PTEX Fullbanner : This is pdfTeX, Version 3.14159265-2.6-1.40.18 (TeX Live 2017) kpathsea version 6.2.3EXIF Metadata provided by EXIF.tools