Specify what tools should do when the classpath is incomplete, or decide not to specify it

[cpovirk]

When developers declare a dependency on a library of annotations (like JSpecify), they sometimes choose to declare the dependency in a way that tells tools: "When someone depends on my library, don't include that annotation library on that user's classpath, either at build time or at runtime." I think this is a bad idea in general (and so I want to discourage it: #294), but it raises additional questions for tools that implement JSpecify rules.

For example, consider:

@Green private final @Nullable String s;

That would appear to declare a field with type String?. However, if @Green is declared such that it @Implies(NonNull.class), then @Green and @Nullable conflict, and so the type of the field is String* [edit: at least in null-umarked code; for discussion of null-marked code, see the simpler example below] (#216).

If the .class file for @Green is not available on the classpath, then we don't know which of those types is correct.

For that matter, even in the simpler case of one annotation on the field...

@NullMarked
class Foo {
  @Green private final String s;
}

...we can't know if the field type is String!! or String? unless we have the .class file for @Green.

[cpovirk]

One possibility is for JSpecify not to speak to this situation: If someone tries to compile without a complete classpath, then that's a weird enough case that we're not going to get into it. Our job, after all, is to say what annotations mean, not what annotations and a classpath that's incomplete in a specific way mean. [edit: Not to mention that tools might put specific annotations on the classpath themselves, and the set of such annotations may change over time. And not to mention that the .class file for a given annotation might be present but the .class file for one of its element values might not. And are tools that operate with reduced classpaths likely to behave consistently?]

Note, though, that this is a common case: As long as there's any frequently used library that asks tools to omit any of its annotations from its deps, tools will encounter that scenario frequently. The library and its omitted annotations don't have to have anything to do with JSpecify or nullness; the point is that, once there's an annotation whose .class file a tool can't see, the tool generally can't know if it has anything to do with JSpecify or nullness.

So this is going to come up. We could decide not to speak to it on principle or on the theory that each tool will have to choose the behavior that works best for its own internal error-handling implementation. But we can't claim "It won't come up" or even "It won't come up for users unless those specific users do something unwise."

[cpovirk]

If we do choose to specify how to handle this scenario, I see at least 2 broad options, though each has (sigh) sub-options. (As usual, we're definitely not going to specify "Tools must refuse to analyze the code at all.")

(Given all the complexities here, I'm inclined to keep dumping information into this thread: Even if we choose not to specify this in JSpecify, the information may be useful to some tool vendor that wishes to consciously choose a behavior—and then test it so as to avoid accidentally changing the behavior and breaking users.)

Options to come in two followup posts, even though the result is going to be unreadable in any case....

[cpovirk]

Option A: If a .class file for an annotation is missing, pretend that that annotation isn't there

So (again assuming that @Green is not on the classpath):

• @Green private final String s; is identical to private final String s;.
• @Green private final @Nullable String s; is identical to private final @Nullable String s;.
• @Implies({Green.class, Nullable.class}) is equivalent to @Implies(Nullable.class).

One advantage to this is that it's easy to implement (well, unless your tool errors out entirely if you try to read any annotations alongside a missing annotation) and easy to explain.

Another advantage is that it gives the desired behavior when the missing annotations have nothing to do with JSpecify, nullness, etc. Thus, if we can convince people to at least not omit JSpecify and "related" annotations from their classpath, then the right thing happens, even if those people continue to omit other annotations from their classpath.

The downside is that it can lead tools to conclude that a type means exactly the opposite of what was intended:

@NullMarked
class Foo {
  @MyNullable private final String s;
}

If @MyNullable is not on the classpath, then the type of the field is String!!, even though it was "clearly" intended to be String?.

The good news is that this is unlikely to happen to code that uses only the main JSpecify annotations: That way, either...

• Both @Nullable and @NullMarked will be on the classpath, so @Nullable String fields will be String?, or...
• Neither will be on the classpath, so @Nullable String fields will be String* (which is still better than String!!). (OK, the closing paragraph below presents another option, but that one ends up behaving identically to the first bullet.)

Finally, I mentioned sub-options: The question here is whether tools can (should/must?) treat the JSpecify annotations (or any other annotations) specially: For @Green private final @Nullable String s;, tools that exist today are very likely to respect the @Nullable annotation even if it's not on the classpath. Would we want them to stop (for consistency)? Would they stop even if we wanted them to? :)

[cpovirk]

Option B: If a .class file for an annotation is missing, "poison" everything to either (1) inapplicable or (2) unspecified

Under this rule, both...

• @Green private final String s; and...
• @Green private final @Nullable String s...

...are equivalent, and we would have to choose whether they're equivalent to...

1. private final [@Nullable @NonNull] String s or to...
2. private final "@UnspecifiedNullness" String s

(1) and (2) would be equivalent in null-unmarked code, but in null-marked code, (1) would produce String!! and (2) would produce String*.

Thus, (1) is susceptible to the same "type means exactly the opposite of what was intended" problem as Option A. And (1) is worse because it has that problem for @Green private final @Nullable String s;, too, while Option A did not.

The advantage of (1) is that it feels like a natural extension of our existing rule that, if we ever see a conflict, we behave as if none of the conflicting annotations are there. We'd simply be extending that rule to include "if we see a possible conflict, ...." (Now maybe another way to spin that is that we should reconsider that rule, too!)

An advantage of (2) is that it will never produce an incorrect specification; it will always fall back to unspecified.

A disadvantage of (2) is that it can fall back to unspecified a lot. Contrast Option A, which specifies a type that is very likely (but not guaranteed!) to be correct for "hygienic" users. (In that regard, the tradeoff reminds me of #250.)

A gross result of (2) is that it makes it possible for users to define an "@UnspecifiedNullness" annotation (well, a fragile version of one) of their own, even if we don't provide one (#137).

One aspect of (2) that I'd want to think more about is whether it's well-defined. It's easy to say that an annotation gives a type unspecified nullness. But will ever other JSpecify-relevant domain have a concept of "unspecified?" Not to mention that we've been saying that @Implies can be used with non-JSpecify annotations (#182), which are even less likely to have such a concept. (For example, an API is either deprecated or not deprecated; there's no "unspecified.") So would we specify that the answer is "(2) if the domain has a concept of 'unspecified'; otherwise, (1)?"

For that matter, under either (1) or (2), what happens with null-marked-ness? If a class uses a single declaration annotation that we can't access (maybe when it even is on the classpath, just not accessible to us?), do we (1) ignore any @NullMarked annotation on the class or even (2?) "undo" a @NullMarked annotation on its package?

[kevinb9n]

In defense of Option A:

• The job of annotations is to convey information
• The job of the tool is to act on information received
• When information went missing in transit, there's no information received to affect the tool's behavior

I say "may be" missing, since the tool would probably still act on @jspecify.Nullable, just not @ImpliesNullable.

The tool would do well to warn about the situation itself, as I commented in #294, but aside from that I don't think it should freak out in every individual case.

[cpovirk]

#308 reminds me that, regardless of how we decide #308, we need to know something about the annotation that's being implied in order to know if the implication is valid: Either we need to know whether it defines required elements (#240), or we need to know whether it defines any elements at all (#308).

This whole discussion probably leads yet again into https://github.com/jspecify/jspecify/wiki/two-kinds-of-analysis

[Mooninaut]

Tools should by default warn or error on unavailable annotations (I lean towards recommending error for interactive tools and warning for batch tools), and provide an option whether to suppress the error, continue with a warning, or stop.

This falls under the principle that JSpecify recommends, but does not prescribe tool behavior.

Alternatively, as time goes on I am more and more leaning towards the idea that semantic annotations' definitions should lie in external file(s) that are provided to static analysis tools by means other than the classpath, which would avoid this issue.

[kevinb9n]

I think we may want to focus on doing even less than "recommending" tool behavior. As Chris said earlier:

One possibility is for JSpecify not to speak to this situation ... Our job, after all, is to say what annotations mean, not what annotations and a classpath that's incomplete in a specific way mean.

I think we might benefit from wielding this principle as a "get out of jail free" card more often. As long as it's well-defined what information is being communicated by the author's choice to use our annotations, we're fulfilling our purpose.

NOTE: the JSpecify project can also add value just by being a "forum" between "all" the tool owners and some library owners, where we can discuss recommendations for cases like this. I'm happy for that to happen, possibly even under a label in this issue tracker itself (not that that's my ideal choice). The thing is: it can still do good while being a whole lot easier than our having to work the topic into our specs, tests, user docs, etc.