1# Sample inputs 2 3Currently, the main purpose of these samples is to act as a source of test cases 4for authors of nullness checkers that wish to use JSpecify nullness information. 5 6## Disclaimers 7 8These sample inputs are informative, not normative. 9 10They use annotations whose names and meanings are not finalized. Notably, they 11currently use an explicit `@NullnessUnspecified` annotation, even though that 12annotation was not part of our 0.1 milestone and will quite possibly not be part 13of our 1.0 release. (Still, we haven't yet removed the `@NullnessUnspecified` 14usages: First, we're not yet certain whether we'll include that annotation or 15not. Second, the annotation provides an easier way to demonstrate rules that can 16arise without it but are easier to demonstrate with it. We probably wouldn't 17write such samples if we were starting from scratch today, but we wrote them 18when we started, and they appear to provide some value on net.) 19 20They have mostly not been code reviewed. 21 22We do not know if this is even the format that we want our sample inputs to be 23in. 24 25Whatever our final samples look like, we do **not** expect to present them as 26"conformance tests" that require any behavior from tools: 27 28- JSpecify nullness information may be of use to many kinds of tools, not just 29 "nullness checkers." But these samples are written in a way that makes them 30 most useful to authors of nullness checkers. Authors of other tools -- those 31 that render API descriptions, generate source code, perform refactorings, 32 etc. -- are not best served by the samples' focus on 33 `jspecify_nullness_mismatch`, etc. 34 35- The goal of JSpecify is to provide one source of nullness information. Tools 36 may use some, all, or none of that information. They may also use 37 information from other sources. 38 39 - Some examples of "information from other sources": 40 41 - looking at the *implementation* of a method to decide whether it can 42 return `null` 43 - looking at non-JSpecify nullness annotations in code 44 - looking at "overlay" or "stub" information about nullness for 45 well-known APIs 46 - looking at whether the parameter to a call to `Map.get` is known to 47 be present in that map 48 - defining a rule to treat all unannotated type usages the same, when 49 the JSpecify rules give some of them "unspecified nullness" 50 51- Based on the information they have available for any given piece of code, 52 tools always have the option to issue a warning / error / other diagnostic 53 for that code, and they always have the option not to. (Even for a tool that 54 uses *all* JSpecify information and *only* JSpecify information, that 55 information is, at its heart, *information* for tools to apply as their 56 authors see fit.) 57 58## Syntax 59 60<!-- TODO: Update links to point to the markup-format spec and glossary. --> 61 62A special comment on a given line of a `.java` file provides information about 63the following line. 64 65The first three special comments indicate that JSpecify annotations are applied 66in ways that are 67[unrecognized](http://jspecify.org/spec#recognized-locations-type-use). Tools 68are likely to report an error in the case of the first two, somewhat less likely 69to report an error in the case of the third (since they might choose to give 70their meaning to annotations there), and not *obligated* to do anything for any 71of the cases: 72 73- `jspecify_conflicting_annotations`: for cases like `@Nullable 74 @NullnessUnspecified Foo` 75 76- `jspecify_nullness_intrinsically_not_nullable`: for cases like `@Nullable 77 int` 78 79- `jspecify_unrecognized_location`: for the other cases in which JSpecify does 80 not give meaning to an annotation, like `class @Nullable Foo {}`. 81 82The last two comments indicate a nullness violation: an inconsistency between 83two annotations, or between annotations and source code. You can think of these 84as extending the normal JLS type rules to cover types that have been augmented 85with nullness information. (For example, the value of a `return` statement must 86be convertible to the method's return type, and the receiver in a method call 87should not be `@Nullable`.) Nullness checkers are likely to report an error for 88each `jspecify_nullness_mismatch` comment, are likely to make many different 89decisions in whether to issues a diagnostic (error, warning, or no diagnostic) 90for any particular `jspecify_nullness_not_enough_information` comment, and are 91not *obligated* to do anything for any particular comment. (For some background 92on that, see the disclaimers above. Also, note that a nullness checker can be 93sound even if it does not issue errors for some cases of 94`jspecify_nullness_mismatch` or `jspecify_nullness_not_enough_information`!) 95 96- `jspecify_nullness_mismatch` 97 98- `jspecify_nullness_not_enough_information`: for nullness violations that 99 involve 100 [unspecified nullness](https://docs.google.com/document/d/1KQrBxwaVIPIac_6SCf--w-vZBeHkTvtaqPSU_icIccc/edit#bookmark=id.xb9w6p3ilsq3). 101 102TODO: Consider additional features: 103 104- multiline comments 105- other locations for comments 106- multiple findings per line/comment 107- comments that apply to larger ranges -- possibly to syntax elements (like 108 statements) rather than lines 109- comments that apply only to a particular part of the line 110 111## Directory structure 112 113See 114[JSpecify: test-data format: Directory structure](https://docs.google.com/document/d/1JVH2p61kReO8bW4AKnbkpybPYlUulVmyNrR1WRIEE_k/edit#bookmark=id.2t1r58i5a03s). 115TODO(#134): Inline that here if Tagir can sign the CLA and contribute it. 116 117Additionally: 118 119Fully qualified class names must be unique across all directories. 120 121> This permits all files to be compiled in a single tool invocation. 122 123TODO: Consider requiring that all individual-file samples be in the top-level 124directory. 125 126Each file must contain a single top-level class. TODO(#133): Consider relaxing 127this. 128 129TODO: Consider requiring a file's path to match its package and class: 130 131- individual-file samples: `Foo.java` for `Foo` 132 133- full-directory samples: `sampleFoo/Foo.java` for `Foo`, 134 `sampleFoo/bar/Foo.java` for `bar.Foo` 135 136- We may need additional accommodations for JPMS support to demonstrate 137 module-level defaulting. 138 139## Restrictions 140 141Files must be UTF-8 encoded. 142 143Files must contain only printable ASCII characters and `\n`. 144 145Files must be compatible with Java 8. TODO(#131): Decide how to label files that 146require a higher version so that we can allow them. (But still encourage 147sticking to Java 8 except for tests that specifically exercise newer features.) 148 149Files must compile without error using stock javac. 150 151Files must not depend on any classes other than the JSpecify annotations. This 152includes the Java platform APIs. Exception: Files may use `java.lang.Object`, 153but they still must not use its methods. 154 155> For example, files may use `Object` as a bound, parameter, or return type. 156 157Files should avoid depending on the presence of absence of "smart" checker 158features, such as: 159 160- looking inside the body of a method to determine what parameters it 161 dereferences or what it returns 162 163 - To that end, prefer abstract methods when practical. 164 165- flow-sensitive typing 166 167We also encourage writing files that demonstrate individual behaviors in 168isolation. For example, we encourage writing files to minimize how much they 169rely on type inference -- except, of course, for any files explicitly intended 170to demonstrate type inference. 171 172## More TODOs 173 174TODO: Consider how to map between samples and related GitHub issues (comments, 175filenames?). 176