Introduce method contracts

[sdeleuze]

With projects like Spring, Micrometer and many others starting to leverage JSpecify combined with a nullness checker, there is a very popular ask (both from Spring commiters and from community members) that we need parameter contracts to be able to achieve 0 checker errors (green build) without too much annotations like @SupressWarnings("NullAway"). The scope of JSpecify 1.0.0 does not allow to reach that IMO reasonable goal, leading to the proliferation of multiple variants of @Contract (JetBrains one, Spring one) annotation + requiring special support in the various checkers. This is not ideal.

Method level @Contract leverages its own expression language, and my understanding is that a majority of members of the JSpecify working group (including me) want to avoid such expression language. I tend to think we could replace the method level @Contract annotation with an expression language by a parameter level annotation with enums. It would cover the majority of the use cases, even if not 100%.

I am wondering if it could make sense for JSpecify to introduce a new annotation like @ParameterContract (name to be refined, hopefully with a shorter one), with no retention at runtime, defined as follow:

@Documented
@Target(ElementType.PARAMETER)
public @interface ParameterContract {
	Condition when();
	Effect then();
}

public enum Condition {
	NONE,
	IS_TRUE,
	IS_FALSE,
	IS_NULL,
	IS_NON_NULL
}

public enum Effect {
	RETURN_TRUE,
	RETURN_FALSE,
	RETURN_NULL,
	RETURN_NON_NULL,
	RETURN_SAME_NULLNESS,
	FAIL
}

So

@Contract("null -> false")
public static boolean hasLength(@Nullable String str) {
	return (str != null && !str.isEmpty());
}

Would translate to:

public static boolean hasLength(@Nullable @ParameterContract(when = IS_NULL, then = RETURN_FALSE) String str) {
	return (str != null && !str.isEmpty());
}

I made the exercise with https://github.com/spring-projects/spring-framework to see how far we could go with @ParameterContract, and it seems to cover 97.5% of our use cases which is IMO pretty good. We could live with a couple of remaining @SupressWarnings("NullAway") for the few remaining unsupported use case.

In details:

• 32x @Contract("null -> false") -> @ParameterContract(when = Condition.IS_NULL, then = Effect.RETURN_FALSE)
• 13x @Contract("null -> null") -> @ParameterContract(when = Condition.IS_NULL, then = Effect.RETURN_NULL)
• 12x @Contract("null, _ -> fail") -> @ParameterContract(when = Condition.IS_NULL, then = Effect.FAIL)
• 8x @Contract("null -> null; !null -> !null") -> @ParameterContract(when = Condition.NONE, then = Effect.RETURN_SAME_NULLNESS)
• 6x @Contract("null, _ -> false; _, null -> false") -> @ParameterContract(when = Condition.IS_NULL, then = Effect.RETURN_FALSE)
• 5x @Contract("_, null -> fail") -> @ParameterContract(when = Condition.IS_NULL, then = Effect.FAIL)
• 5x @Contract("null -> true") -> @ParameterContract(when = Condition.IS_NULL, then = Effect.RETURN_TRUE)
• 5x @Contract("null, _ -> false") -> @ParameterContract(when = Condition.IS_NULL, then = Effect.RETURN_FALSE)
• 4x @Contract("_, null -> false") -> @ParameterContract(when = Condition.IS_NULL, then = Effect.RETURN_FALSE)
• 4x @Contract("_, null, _ -> fail") -> @ParameterContract(when = Condition.IS_NULL, then = Effect.FAIL)
• 4x @Contract("false, _ -> fail") -> @ParameterContract(when = Condition.IS_FALSE, then = Effect.FAIL)
• 3x @Contract("_ -> fail") -> @ParameterContract(when = Condition.NONE, then = Effect.FAIL)
• 2x @Contract("!null, _ -> fail") -> @ParameterContract(when = Condition.IS_NON_NULL, then = Effect.FAIL)
• 2x @Contract("null -> fail") -> @ParameterContract(when = Condition.IS_NULL, then = Effect.FAIL)
• 2x @Contract("null, _ -> param2; _, null -> param1") -> Not covered (no support for returning parameter values)
• 1x @Contract("_, !null -> fail") -> @ParameterContract(when = Condition.IS_NON_NULL, then = Effect.FAIL)
• 1x @Contract("_, false -> fail") -> @ParameterContract(when = Condition.IS_FALSE, then = Effect.FAIL)
• 1x @Contract("_, null -> true") -> @ParameterContract(when = Condition.IS_NULL, then = Effect.TRUE)
• 1x @Contract("_, null -> true; null, _ -> false") -> @ParameterContract(when = Condition.IS_NULL, then = Effect.FAIL)
• 1x @Contract("_, null, _ -> fail; _, _, null -> fail") -> @ParameterContract(when = Condition.IS_NULL, then = Effect.FAIL)
• 1x @Contract("_, null, null -> fail") -> Not covered (no support for contract with conditions involving multiple parameters)
• 1x @Contract("_, true -> fail") -> @ParameterContract(when = Value.TRUE, then = Effect.FAIL)
• 1x @Contract("null, _ -> false; _, null -> false;") -> @ParameterContract(when = Condition.IS_NULL, then = Effect.RETURN_FALSE)
• 1x @Contract("null, _ -> null") -> @ParameterContract(when = Condition.IS_NULL, then = Effect.RETURN_NULL)
• 1x @Contract("null, _ -> null; _, null -> null") -> @ParameterContract(when = Condition.IS_NULL, then = Effect.RETURN_NULL)
• 1x @Contract("null, _ -> true") -> @ParameterContract(when = Condition.IS_NULL, then = Effect.RETURN_TRUE)
• 1x @Contract("null, _, _ -> null") -> @ParameterContract(when = Condition.IS_NULL, then = Effect.RETURN_NULL)

Any thoughts?

[wakingrufus]

Is this meant to also conver contracts like -> new and -> this ? Or just null-related contracts?

[agentgt]

The challenging part is not the DSL. It would be trivial to write such a parser and even have that as some stand alone library that everyone could use.

The challenging part is that this a lot of this basically an extension of @PolyNull and at the moment despite the name JSpecify is mostly about "types" and not "contracts" aka extension of the type system instead of static design by contract (there is a subtle complicated difference). PolyNull is very difficult to represent in a type system without a bunch of weird rules and the rest of the rules are like a dependent type system.

Now I'm not positive but I think it is going to be very difficult to have PolyNull methods in a Valhalla future that work like PolyNull. Solid chance they are nullable return always. That is my concern is the contracts could indeed conflict with Valhalla typing.

we need parameter contracts to be able to achieve 0 checker errors (green build) without too much annotations like @SupressWarnings("NullAway"). The scope of JSpecify 1.0.0 does not allow to reach that IMO reasonable goal,

The question is should the scope be increased instead of say a new project? I realize Spring is a big player and so is IntelliJ but I get concerned based on a long history of working with Java where big players in a committee have sway for their needs while completely forgetting the little guys that need to implement. They also often create barrier such that they are the only ones to offer a solution. I'm sure you have seen this with the ancient JSRs. Are we going to end up with the case of IntelliJ being the only solution because of complexity? I think that would be sad.

Also I think we should see what Valhalla does because you might be creating more work for yourself. Like ask yourself the methods where you need these contracts can they be replaced with better modern ones that don't need contract and just deprecate the PolyNull like ones? For example many of Spring's utility methods already can be replaced with whats built into String and is it really a good idea to flow type change based on the return of a boolean? For example in the case of hasLength you would favor Guava's String utilities emptyToNull and nullToEmpty. Like ideally we use the type system that is builtin to Java as much as possible.

Many of these things btw can be solved with pattern matching:

var result = switch(emptyToNull(s)) {
  case s -> s; // or some giant imperative block
  case null -> "default"
}

Now let me give you an example how embracing or encouraging PolyNull or similar can be a problem:

Optional<T> opt;
var x = opt.orElse(null); // could fail here
// or y is not null
var x = opt.orElse(y); 
x.toString() // or could fail here because the compiler still says x could be nullable

You see in the plain Java world with type orElse definition is supposed to return T except that T can be nullable regardless of the nullability of T (replace T with int where null is not possible).

That is at the moment till we see what happens with Valhalla.

Optional<T!> opt;
var x = opt.orElse(null);

Could possible be a compiler failure or not. Or it is assumed nullable where as your contract says it should not be and thus you will get compiler errors but the contract says you should not.

So a lot of this Condition stuff I think needs to wait and it begs the question... maybe that one annotation is doing too much?

[sdeleuze]

I get concerned based on a long history of working with Java where big players in a committee have sway for their needs while completely forgetting the little guys that need to implement.

For the record, this ask originates mostly from smaller OSS projects concerned about having to introduce their own @Contract that I relay, that's not a big player specific ask.

[agentgt]

For the record, this ask originates mostly from smaller OSS projects concerned about having to introduce their own @Contract that I relay, that's not a big player specific ask.

Yes but it so happens the only implementation that is basically already done is IntelliJ and they are the only ones selling a tool. I admit I'm probably overly jaded but even now there is a lot of ... let us make sure we are compatible with Kotlin. That is probably a good thing and I assume mostly altruistic goals... Frankly I should probably just delete that comment as its kind of rude to assume.

Honestly my bigger concern is conflict with whatever Valhalla does. It seems like the easiest path is for Spring is just to replace or update its utility methods (and or not use them).

And I don't discount that this an incredibly annoying problem. For example most tools have some sort of pseudo hard coded white list of methods where the flow type changes. A classic case is Objects.requireNonNull which hilariously would be fine if you use the return value but Error Prone has some weird rule where if you do: x = Objects.requireNonNull(x) it complains despite that being one of the safest way to flip/cast x to nonnull. Checkerframework will flat out not allow it since it requires the x to be NonNull on input unless you change the astub.

So you can see there is already lots of conflicts between the tools and a lot of this is interpreting previous code of how it should be annotated and or you allow things like PolyNull.

Thats why I said it is almost a separate project. Like how does one interpret the current and potential future of the JDK without official annotations (I suppose it is sort of orthogonal but still what the JDK does is going to be the bigger influence).

The current set of annotations though are pretty future safe.

[sdeleuze]

I will have a deeper look to your other concerns, links with @PolyNull, and of course I expect a variety of opinions on that topic from the rest of the JSpecify working group who has more in mind than me @PolyNull constraints and challenges. This can also be an opportunity for related discussion with the Valhalla working group.

I don't want to rush anything, but there is a missing part in the JSpecify scope that I see in every OSS project leveraging checkers, I don't believe projects should modify APIs and break apps to make nullness checker happy, so I would like us to work on that topic and get that ball rolling, regardless of the outcome.

[agentgt]

And my hope is you don't think I'm a debbie downer (or some sort of OSS over proprietary solution pusher) or just say no to any new feature. My explanation was to show just how complicated this can be and the potential risk.

I said PolyNull but what I really mean is the complexity of Flow analysis. That complexity is not just pushed on to the tools but the users themselves.

Like just doing

if (hasLength(x)) {
  // x is not null here
}
else {
  // x is nullable here
}

Is inherently more difficult to follow than normal non flow Java types. Like in that if block you need a tool to show you that x is now flipped its type. You can't always easily infer it with code inspection on say github.

Also flow analysis varies greatly in those tools.

For example:

if (hasLength(x)) {
  if (x == null) { // should this be legal?
  }
}
else {
  // x is nullable here
}

That varies by tool and only Checkerframework and Eclipse at the moment will or can actually complain (replace x as int to make the == failure easier to understand). JSpecify currently has no opinion on this but Valhalla very much could.

So I'm just trying to show all the areas of issues to give feedback.

[sdeleuze]

Is this meant to also conver contracts like -> new and -> this ? Or just null-related contracts?

@wakingrufus Not sure, but I would begin by exploring if we can reach a consensus on only the nullness related use case initially, to not open too many doors at the same time.

[cpovirk]

Thanks for the writeup and all the data! I have a lot of uncertainty in this area, so it's very helpful.

I have no answers, but here are a few thoughts:

• I agree that tool support is a big question. If we could get Kotlin, IntelliJ, NullAway, and EISOP on board, I'd feel a lot better. (Sorry, Eclipse. Obviously I'd be happy to see them, too. What other projects are I forgetting?)
  • [update: Kotlin added experimental support for their conditional returnsNotNull() contract.]
• I would also love to think more about the Valhalla issue raised. I am under the impression that Valhalla nullness markers would likely produce only warnings at first in javac (maybe forever?), so we may well see users who disable all those warnings and turn things over to another nullness checker like the ones they use today.
• For @PolyNull, I should someday clean up my speech about how @PolyNull is complicated when used on type variables. If we are to support that here, I'd want to be clear on what it means.
• Some of the historical concerns about an expression language (such as those here) are concerns about using any single annotation for a variety of use cases. Those would apply to a general @ParameterContract annotation.
• Another concern about an expression language is that it's less discoverable and autocompletable than alternatives. The proposed @ParameterContract annotation would avoid that.
• Annotations that have enum elements (like Condition and Effect here) can cause trouble when people use them with incomplete classpaths. We have tried to avoid them in the past. We may end up wanting to avoid them here.

[cpovirk]

(I forgot to invoke @kevinb9n for any Valhalla thoughts (or other thoughts :)).)

[agentgt]

In my mind I kind of equate a lot of this that people need to expect possible code changes and practices other than just adding annotations just like how when Java added generics there were still places you had to make changes instead of just adding the generic. In some cases @SuppressWarnings is the best option for backward compat.

For my own parsing and perhaps others:

32x @Contract("null -> false") -> @ParameterContract(when = Condition.IS_NULL, then = Effect.RETURN_FALSE)

Which is equivalent to:

boolean func(@Nullable X x);

And what is supposed to be inferred is that if func is passed null it will return false and thus x maybe null if the return is false and thus if true x can be inferred as @NonNull going forward in that block of code (e.g. method).

I'm fairly sure most of these are hasLength which I'm going to be frank should be replaced with a better method as I mentioned earlier. Like imagine expecting boolean func(Optional<X> x) to have guarantees that it is Optional.empty() if false. It is confusing and I bet a lot of its usage is cargo culting copy and paste.

13x @Contract("null -> null") -> @ParameterContract(when = Condition.IS_NULL, then = Effect.RETURN_NULL)

Roughly equal to:

@Nullable R func(@Nullable X x);

This one should be already handled by JSpecify and you should mostly not be getting warnings. I say mostly because this one cannot be modeled exactly with out adding a null type. That is because if I pass in null that I know is null like the literal null I always get null.

That is you need @Null X x = null; and @Null R would be returned (as in guaranteed to be null). I'm not sure how that distinction is worthwhile other than I guess the IDE saying you will absolutely get a null pointer vs might get a null pointer.

This is btw different from PolyNull because if X is not null you could still get a null (also PolyNull is usually used for the same base type but let us ignore that).

I would be curious what warnings you get with these kinds methods with JSpecify checker @sdeleuze or was this just an example of the Contract usage?

12x @Contract("null, _ -> fail") ->  @ParameterContract(when = Condition.IS_NULL, then = Effect.FAIL)

void func(@Nullable X x, String description); 
// or
@NonNull X func(@Nullable X x, String description);

This is the classic assertNotNull or Objects.requireNonNull where you may or may not do reassignment. Some tools just have a giant list of methods they know that do this which I think is Eclipse and NullAway. Checker has annotations to do it with any method. (I assume the second variable is a description on the assert).

This can be fixed with reassignment w/o flow analysis and indeed Objects.requireNonNull guarantees NonNull return.

I'm surprised this was not number one or number two. IMO this one is less of a problem because usually these are assertions, you can reassign, and most people use the same libraries or JDK for this stuff so the whitelist hack mostly works. In fact I think Eclipse has the Spring Assert methods hard coded in. I assume NullAway has some configuration somewhere.

8x @Contract("null -> null; !null -> !null") -> @ParameterContract(when = Condition.NONE, then = Effect.RETURN_SAME_NULLNESS)

Classic PolyNull. JSpecify cannot model this easily and people follow this pattern all over the place including the JDK. I'm surprised this was not the number one or number two.

This is why I was so concentrated on mentioning PolyNull because the first two which make up a huge amount of your count particularly hasLength can be fixed and may not even be a problem.

[kevinb9n]

(Valhalla plans subject to change!)

Just confirming that in Valhalla we are planning "merely" to make Foo? and Foo! types representable, with the type-checking you'd expect, and we'll have nothing fun addressing "polynull" use cases or more complex nullity contracts.

But also, yes, we plan to only generate warnings, and probably in a handful of different nullity subcategories which the user can either silence or upgrade to errors selectively.

So for the user who wants smarter nullity contracts, they will want to keep using either @PolyNull and similar things or this @Contract, and then probably they will just turn off the javac nullity warnings and rely on their tools instead.

(It would be nice if javac could still do what it can and the tools just augment that behavior, but for that to work, we would need a way that a javac plugin can actually subtract warnings and not just add them. Or basically a very custom nullity-specific plugin API, all of which just feels weird.)

For our polynull methods like T? cast(T? object), we might just introduce fauxverloads like T! castNonNull(T! object) alongside them, which is not as good, but is something. Oh, but hopefully we will have a postfix cast-to-nonnull operator like Kotlin has, and maybe that's enough.

Happy to answer other questions.

[sdeleuze]

@agentgt BTW I appreciate your detailed feedback, I will take the type to digest it and answer, likely next week.

[sdeleuze]

@agentgt Sorry for the delay, busy times.

To me, @PolyNull looks like a special case of what is described here. Also from a design perspective, since JSpecify 1.0 has shipped and the working group agreed on not introducing @Implies (aka meta annotation support), I think I prefer we don't attempt to refine the semantics of current annotations but rather add some additional contracts that provide hints for checkers.

Given @kevinb9n feedback and what I hear from Project Valhalla, I have low concern that the contracts discussed here may introduce something incompatible with Project Valhalla. But does not hurt to wait for the first drafts to check.

I hear your perspective that we could refactor some code so avoid the need for some of those contracts. All the projects I have seen adopting JSpecify needs those kind of contracts to be able to get the checks green, some of those APIs are public or JDK APIs that we can't change, so I understand the hope but in practice that will not happen. And in some case, this is not desirable from an API design perspective.

About your ask for those potential annotations to be a different project, again to be discussed with the working group, but based on my understanding, JSpecify name and scope is IMO a good fit for such contract. I don't think JSpecify is current able to fulfil its core mission to provide a tooling neutral way to check your code base nullness without some kind of complementary contracts, so every projects introduce its own @Contract, keeping the same duplication issue that we had pre-JSpecify with a proliferation of custom annotations. But I agree that extends the scope of the jspecify artifact with something slightly more opinionated and that should be discussed in detail.

That said, I think we don't have yet an API design strong enough to be evaluated for inclusion yet. @cpovirk has rightfully raised the IMO blocking issue that enums as annotation attributes generates compilation warnings when JSpecify is not on the classpath, so we are back to the drawing board. We will post an update once we get a refined API design to discuss.