Cannot get JSpecify annotations to work like org.eclipse.jdt.annotation specifically with generics

[agentgt]

@stephan-herrmann

I cannot replace Eclipses null annotations with JSpecify because generics appear to be not marked.

Here is the project.

https://github.com/agentgt/jdt-null-issue

The project does not work with headless at the moment because there appears to be another bug with plexus eclipse compiler not finding jspecify however it does emit the same warnings as the UI so I will paste its output here:

[WARNING] COMPILATION WARNING :
[INFO] -------------------------------------------------------------
[WARNING] /Users/agent/projects/jdt-null-issue/src/main/java/bug/ezkv/package-info.java:[2,9] A default nullness annotation has not been specified for the package bug.ezkv
[WARNING] /Users/agent/projects/jdt-null-issue/src/main/java/bug/ezkv/FlagSet.java:[25,24] Null constraint mismatch: The type 'E extends java.lang.Enum<E>' is not a valid substitute for the type parameter 'E extends java.lang.@NonNull Enum<E>'
[WARNING] /Users/agent/projects/jdt-null-issue/src/main/java/bug/ezkv/FlagSet.java:[27,18] Null constraint mismatch: The type 'E extends java.lang.Enum<E>' is not a valid substitute for the type parameter 'E extends java.lang.@NonNull Enum<E>'
[WARNING] /Users/agent/projects/jdt-null-issue/src/main/java/bug/ezkv/FlagSet.java:[36,62] Null constraint mismatch: The type 'E extends java.lang.Enum<E>' is not a valid substitute for the type parameter 'E extends java.lang.@NonNull Enum<E>'
[WARNING] /Users/agent/projects/jdt-null-issue/src/main/java/bug/ezkv/FlagSet.java:[47,37] Null constraint mismatch: The type 'E extends java.lang.Enum<E>' is not a valid substitute for the type parameter 'E extends java.lang.@NonNull Enum<E>'
[WARNING] /Users/agent/projects/jdt-null-issue/src/main/java/bug/ezkv/FlagSet.java:[55,22] Missing non-null annotation: inherited method from java.lang.Iterable<E> specifies this parameter as @org.jspecify.annotations.NonNull
[WARNING] /Users/agent/projects/jdt-null-issue/src/main/java/bug/ezkv/FlagSet.java:[60,34] Missing nullable annotation: inherited method from java.util.Set<E> specifies this parameter as @org.jspecify.annotations.Nullable
[WARNING] /Users/agent/projects/jdt-null-issue/src/main/java/bug/ezkv/FlagSet.java:[65,9] The return type is incompatible with 'java.util.@NonNull Iterator<E extends java.lang.Enum<E>>' returned from java.util.Set<E>.iterator() (mismatching null constraints)
[WARNING] /Users/agent/projects/jdt-null-issue/src/main/java/bug/ezkv/FlagSet.java:[90,9] The return type is incompatible with 'java.lang.Object @org.jspecify.annotations.NonNull[]' returned from java.util.Set<E>.toArray() (mismatching null constraints)
[WARNING] /Users/agent/projects/jdt-null-issue/src/main/java/bug/ezkv/FlagSet.java:[95,27] Missing non-null annotation: inherited method from java.util.Set<E> specifies this parameter as @org.jspecify.annotations.NonNull
[WARNING] /Users/agent/projects/jdt-null-issue/src/main/java/bug/ezkv/FlagSet.java:[116,29] Missing non-null annotation: inherited method from java.util.Set<E> specifies this parameter as @org.jspecify.annotations.NonNull
[WARNING] /Users/agent/projects/jdt-null-issue/src/main/java/bug/ezkv/FlagSet.java:[121,24] Missing non-null annotation: inherited method from java.util.Set<E> specifies this parameter as @org.jspecify.annotations.NonNull
[WARNING] /Users/agent/projects/jdt-null-issue/src/main/java/bug/ezkv/FlagSet.java:[126,27] Missing non-null annotation: inherited method from java.util.Set<E> specifies this parameter as @org.jspecify.annotations.NonNull
[WARNING] /Users/agent/projects/jdt-null-issue/src/main/java/bug/ezkv/FlagSet.java:[153,26] Missing non-null annotation: inherited method from java.util.Collection<E> specifies this parameter as @org.jspecify.annotations.NonNull
[WARNING] /Users/agent/projects/jdt-null-issue/src/main/java/bug/ezkv/FlagSet.java:[158,9] The return type is incompatible with 'java.util.@NonNull Spliterator<E extends java.lang.Enum<E>>' returned from java.util.Set<E>.spliterator() (mismatching null constraints)
[WARNING] /Users/agent/projects/jdt-null-issue/src/main/java/bug/ezkv/FlagSet.java:[163,9] The return type is incompatible with 'java.util.stream.@NonNull Stream<E extends java.lang.Enum<E>>' returned from java.util.Collection<E>.stream() (mismatching null constraints)
[WARNING] /Users/agent/projects/jdt-null-issue/src/main/java/bug/ezkv/FlagSet.java:[168,9] The return type is incompatible with 'java.util.stream.@NonNull Stream<E extends java.lang.Enum<E>>' returned from java.util.Collection<E>.parallelStream() (mismatching null constraints)
[WARNING] /Users/agent/projects/jdt-null-issue/src/main/java/bug/package-info.java:[2,9] A default nullness annotation has not been specified for the package bug
[INFO] 18 warnings
[INFO] -------------------------------------------------------------
[INFO] -------------------------------------------------------------
[ERROR] COMPILATION ERROR :
[INFO] -------------------------------------------------------------
[ERROR] /Users/agent/projects/jdt-null-issue/src/main/java/module-info.java:[3,11] org.jspecify cannot be resolved to a module
[ERROR] /Users/agent/projects/jdt-null-issue/src/main/java/bug/ezkv/package-info.java:[1,2] The type org.jspecify.annotations.NullMarked is not accessible
[ERROR] /Users/agent/projects/jdt-null-issue/src/main/java/bug/ezkv/FlagSet.java:[16,8] The type org.jspecify.annotations.Nullable is not accessible
[ERROR] /Users/agent/projects/jdt-null-issue/src/main/java/bug/ezkv/FlagSet.java:[60,25] Nullable cannot be resolved to a type
[ERROR] /Users/agent/projects/jdt-null-issue/src/main/java/bug/ezkv/FlagSet.java:[80,27] Nullable cannot be resolved to a type
[ERROR] /Users/agent/projects/jdt-null-issue/src/main/java/bug/ezkv/FlagSet.java:[101,14] Nullable cannot be resolved to a type
[ERROR] /Users/agent/projects/jdt-null-issue/src/main/java/bug/ezkv/FlagSet.java:[111,25] Nullable cannot be resolved to a type
[ERROR] /Users/agent/projects/jdt-null-issue/src/main/java/bug/ezkv/FlagSet.java:[148,14] Nullable cannot be resolved to a type
[ERROR] /Users/agent/projects/jdt-null-issue/src/main/java/bug/ezkv/FlagSet.java:[232,18] Nullable cannot be resolved to a type
[ERROR] /Users/agent/projects/jdt-null-issue/src/main/java/bug/package-info.java:[1,2] The type org.jspecify.annotations.NullMarked is not accessible
[INFO] 10 errors

EDIT here are the errors in the UI

Description	Resource	Path	Location	Type
Null constraint mismatch: The type 'E extends Enum<E>' is not a valid substitute for the type parameter 'E extends @NonNull Enum<E>'	FlagSet.java	/jdt-null-issue/src/main/java/bug/ezkv	line 25	Java Problem
Null constraint mismatch: The type 'E extends Enum<E>' is not a valid substitute for the type parameter 'E extends @NonNull Enum<E>'	FlagSet.java	/jdt-null-issue/src/main/java/bug/ezkv	line 27	Java Problem
Null constraint mismatch: The type 'E extends Enum<E>' is not a valid substitute for the type parameter 'E extends @NonNull Enum<E>'	FlagSet.java	/jdt-null-issue/src/main/java/bug/ezkv	line 36	Java Problem
Null constraint mismatch: The type 'E extends Enum<E>' is not a valid substitute for the type parameter 'E extends @NonNull Enum<E>'	FlagSet.java	/jdt-null-issue/src/main/java/bug/ezkv	line 47	Java Problem
Null type safety (type annotations): The expression of type 'String' needs unchecked conversion to conform to '@NonNull String'	FlagSet.java	/jdt-null-issue/src/main/java/bug/ezkv	line 208	Java Problem

While I have checked in all the eclipse settings I'm going to show the relevant ones below:

org.eclipse.jdt.core.builder.annotationPath.allLocations=enabled
org.eclipse.jdt.core.compiler.annotation.inheritNullAnnotations=disabled
org.eclipse.jdt.core.compiler.annotation.missingNonNullByDefaultAnnotation=warning
org.eclipse.jdt.core.compiler.annotation.nonnull=org.jspecify.annotations.NonNull
org.eclipse.jdt.core.compiler.annotation.nonnull.secondary=org.eclipse.jdt.annotation.NonNull
org.eclipse.jdt.core.compiler.annotation.nonnullbydefault=org.jspecify.annotations.NullMarked
org.eclipse.jdt.core.compiler.annotation.nonnullbydefault.secondary=org.eclipse.jdt.annotation.NonNullByDefault
org.eclipse.jdt.core.compiler.annotation.notowning=org.eclipse.jdt.annotation.NotOwning
org.eclipse.jdt.core.compiler.annotation.nullable=org.jspecify.annotations.Nullable
org.eclipse.jdt.core.compiler.annotation.nullable.secondary=org.eclipse.jdt.annotation.Nullable
org.eclipse.jdt.core.compiler.annotation.nullanalysis=enabled

My guess is to why this is happening is that annotations besides the eclipse ones are assumed not to target generics.

That is all other annotations are treated like:

DefaultLocation[] value() default { PARAMETER, RETURN_TYPE, FIELD} // missing TYPE_BOUND, TYPE_ARGUMENT };

To import my reproducible project you may need to adjust the .classpath to add the EEA. I have not added every EEA of the JDK but just the ones I know it needs.

    <classpathentry kind="con" path="org.eclipse.jdt.launching.JRE_CONTAINER/org.eclipse.jdt.internal.debug.ui.launcher.StandardVMType/JavaSE-21">
        <attributes>
            <!-- I'm using a workspace path to find the eea -->
            <attribute name="annotationpath" value="/jdt-null-issue/etc/eea"/>
            <attribute name="maven.pomderived" value="true"/>
        </attributes>
    </classpathentry>

I'm going to tag @sebthom as they are also one of the few that know Eclipse null analysis.

If I replace all the annotations with the Eclipse ones (and make the Eclipse ones primary) the issues go away.

@stephan-herrmann I'm happy to help anyway including code diving. I know promised help before but I have finally finished a bulk of opensource work and eager on making Eclipse null analysis one of the best jspecify-like options.

[agentgt]

It also could be because the JSpecify annotations have a true module-info.java. This is based on the headless compiler errors (these errors are not in the UI).

[ERROR] /Users/agent/projects/jdt-null-issue/src/main/java/bug/package-info.java:[1,2] The type org.jspecify.annotations.NullMarked is not accessible

See #2538 also

For me to investigate...

eclipse.jdt.core/org.eclipse.jdt.core.compiler.batch/src/org/eclipse/jdt/internal/compiler/lookup/BinaryTypeBinding.java

Line 2250 in 8d1cb65

static int getNonNullByDefaultValue(IBinaryAnnotation annotation, LookupEnvironment environment) {

By assumptions were correct. It is the above code that does the magic based on annotation value. A workaround is to make your own Eclipse JDT annotation with the same value() enum names.

@Documented
@Retention(RetentionPolicy.CLASS)
public @interface FakeNonNullByDefault {

	DefaultLocation[] value() default {  DefaultLocation.PARAMETER, DefaultLocation.RETURN_TYPE, DefaultLocation.FIELD, DefaultLocation.TYPE_BOUND, DefaultLocation.TYPE_ARGUMENT };

	public enum DefaultLocation {
		PARAMETER,
		RETURN_TYPE,
		FIELD,
		TYPE_PARAMETER,
		TYPE_BOUND,
		TYPE_ARGUMENT,
		ARRAY_CONTENTS
	}
}

Or just use JDT Eclipse annotations only on the package-info.java (and the jspecify ones).

[agentgt]

@stephan-herrmann

I added the fake Eclipse JDT annotation hack for this repo and it worked:
https://github.com/jstachio/ezkv

And it already found a bug (in my code): https://github.com/jstachio/ezkv/blob/f6f2f373e3e1a4bf23147b5aaea86e195bd2a800/ezkv-kvs/src/main/java/io/jstach/ezkv/kvs/DefaultKeyValuesResourceParser.java#L279

(rk.type() can never be null but further up rk could be null but should have added filtered before the continue).

I have Checkerframework, Errorprone, and Nullaway (currently off) for that project and none of them found that issue. That is why I think the Eclipse null analysis is so valuable!

I guess maybe we have something hardcoded for JSpecify or should have some option of where we can add default locations by annotation name?

[srikanth-sankaran]

I have Checkerframework, Errorprone, and Nullaway (currently off) for that project and none of them found that issue. That is why I think the Eclipse null analysis is so valuable!

I

Thanks for sharing this feedback!