Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Split "paradox" into 3 categories. #135

Merged
merged 5 commits into from
Oct 2, 2020
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Jump to
Jump to file
Failed to load files.
Diff view
Diff view
10 changes: 5 additions & 5 deletions samples/AnnotatedInnerOfNonParameterized.java
Original file line number Diff line number Diff line change
Expand Up @@ -27,23 +27,23 @@ class DoublyNested {}

@Nullable Nested x4;

// jspecify_nullness_paradox
// jspecify_nullness_intrinsically_not_nullable
@Nullable AnnotatedInnerOfNonParameterized.Nested x5;

AnnotatedInnerOfNonParameterized.@Nullable Nested x6;

// jspecify_nullness_paradox
// jspecify_nullness_intrinsically_not_nullable
@Nullable AnnotatedInnerOfNonParameterized.Nested.DoublyNested x7;

// jspecify_nullness_paradox
// jspecify_nullness_intrinsically_not_nullable
AnnotatedInnerOfNonParameterized.@Nullable Nested.DoublyNested x8;

AnnotatedInnerOfNonParameterized.Nested.@Nullable DoublyNested x9;

// jspecify_nullness_paradox
// jspecify_nullness_intrinsically_not_nullable
Lib<@Nullable AnnotatedInnerOfNonParameterized.Nested.DoublyNested> l1;

// jspecify_nullness_paradox
// jspecify_nullness_intrinsically_not_nullable
Lib<AnnotatedInnerOfNonParameterized.@Nullable Nested.DoublyNested> l2;

Lib<AnnotatedInnerOfNonParameterized.Nested.DoublyNested> l3;
Expand Down
10 changes: 5 additions & 5 deletions samples/AnnotatedInnerOfParameterized.java
Original file line number Diff line number Diff line change
Expand Up @@ -27,23 +27,23 @@ class DoublyNested {}

@Nullable Nested x4;

// jspecify_nullness_paradox
// jspecify_nullness_intrinsically_not_nullable
@Nullable AnnotatedInnerOfParameterized<?>.Nested x5;

AnnotatedInnerOfParameterized<?>.@Nullable Nested x6;

// jspecify_nullness_paradox
// jspecify_nullness_intrinsically_not_nullable
@Nullable AnnotatedInnerOfParameterized<?>.Nested.DoublyNested x7;

// jspecify_nullness_paradox
// jspecify_nullness_intrinsically_not_nullable
AnnotatedInnerOfParameterized<?>.@Nullable Nested.DoublyNested x8;

AnnotatedInnerOfParameterized<?>.Nested.@Nullable DoublyNested x9;

// jspecify_nullness_paradox
// jspecify_nullness_intrinsically_not_nullable
Lib<@Nullable AnnotatedInnerOfParameterized<?>.Nested.DoublyNested> l1;

// jspecify_nullness_paradox
// jspecify_nullness_intrinsically_not_nullable
Lib<AnnotatedInnerOfParameterized<?>.@Nullable Nested.DoublyNested> l2;

Lib<AnnotatedInnerOfParameterized<?>.Nested.DoublyNested> l3;
Expand Down
6 changes: 3 additions & 3 deletions samples/AnnotatedTypeParameter.java
Original file line number Diff line number Diff line change
Expand Up @@ -19,12 +19,12 @@

@DefaultNonNull
class AnnotatedTypeParameter {
// jspecify_nullness_paradox
// jspecify_unrecognized_location
interface Lib1<@Nullable T> {}

// jspecify_nullness_paradox
// jspecify_unrecognized_location
interface Lib2<@Nullable T extends Object> {}

// jspecify_nullness_paradox
// jspecify_unrecognized_location
interface Lib3<@Nullable T extends @Nullable Object> {}
}
6 changes: 3 additions & 3 deletions samples/AnnotatedTypeParameterUnspec.java
Original file line number Diff line number Diff line change
Expand Up @@ -20,12 +20,12 @@

@DefaultNonNull
class AnnotatedTypeParameterUnspec {
// jspecify_nullness_paradox
// jspecify_unrecognized_location
interface Lib1<@NullnessUnspecified T> {}

// jspecify_nullness_paradox
// jspecify_unrecognized_location
interface Lib2<@NullnessUnspecified T extends Object> {}

// jspecify_nullness_paradox
// jspecify_unrecognized_location
interface Lib3<@NullnessUnspecified T extends @Nullable Object> {}
}
10 changes: 5 additions & 5 deletions samples/AnnotatedWildcard.java
Original file line number Diff line number Diff line change
Expand Up @@ -21,18 +21,18 @@
class AnnotatedWildcard {
interface Lib<T extends @Nullable Object> {}

// jspecify_nullness_paradox
// jspecify_unrecognized_location
Lib<@Nullable ?> x1;

// jspecify_nullness_paradox
// jspecify_unrecognized_location
Lib<@Nullable ? extends Object> x2;

// jspecify_nullness_paradox
// jspecify_unrecognized_location
Lib<@Nullable ? super Object> x3;

// jspecify_nullness_paradox
// jspecify_unrecognized_location
Lib<@Nullable ? extends @Nullable Object> x4;

// jspecify_nullness_paradox
// jspecify_unrecognized_location
Lib<@Nullable ? super @Nullable Object> x5;
}
10 changes: 5 additions & 5 deletions samples/AnnotatedWildcardUnspec.java
Original file line number Diff line number Diff line change
Expand Up @@ -22,18 +22,18 @@
class AnnotatedWildcardUnspec {
interface Lib<T extends @Nullable Object> {}

// jspecify_nullness_paradox
// jspecify_unrecognized_location
Lib<@NullnessUnspecified ?> x1;

// jspecify_nullness_paradox
// jspecify_unrecognized_location
Lib<@NullnessUnspecified ? extends Object> x2;

// jspecify_nullness_paradox
// jspecify_unrecognized_location
Lib<@NullnessUnspecified ? super Object> x3;

// jspecify_nullness_paradox
// jspecify_unrecognized_location
Lib<@NullnessUnspecified ? extends @Nullable Object> x4;

// jspecify_nullness_paradox
// jspecify_unrecognized_location
Lib<@NullnessUnspecified ? super @Nullable Object> x5;
}
Original file line number Diff line number Diff line change
Expand Up @@ -20,8 +20,8 @@

@DefaultNonNull
class MultipleAnnotations {
// jspecify_nullness_paradox
// jspecify_conflicting_annotations
@Nullable @NullnessUnspecified Object x1;
// jspecify_nullness_paradox
// jspecify_conflicting_annotations
@NullnessUnspecified @Nullable Object x2;
}
10 changes: 5 additions & 5 deletions samples/NotNullAwareAnnotatedInnerOfNonParameterized.java
Original file line number Diff line number Diff line change
Expand Up @@ -25,23 +25,23 @@ class DoublyNested {}

@Nullable Nested x4;

// jspecify_nullness_paradox
// jspecify_nullness_intrinsically_not_nullable
@Nullable NotNullAwareAnnotatedInnerOfNonParameterized.Nested x5;

NotNullAwareAnnotatedInnerOfNonParameterized.@Nullable Nested x6;

// jspecify_nullness_paradox
// jspecify_nullness_intrinsically_not_nullable
@Nullable NotNullAwareAnnotatedInnerOfNonParameterized.Nested.DoublyNested x7;

// jspecify_nullness_paradox
// jspecify_nullness_intrinsically_not_nullable
NotNullAwareAnnotatedInnerOfNonParameterized.@Nullable Nested.DoublyNested x8;

NotNullAwareAnnotatedInnerOfNonParameterized.Nested.@Nullable DoublyNested x9;

// jspecify_nullness_paradox
// jspecify_nullness_intrinsically_not_nullable
Lib<@Nullable NotNullAwareAnnotatedInnerOfNonParameterized.Nested.DoublyNested> l1;

// jspecify_nullness_paradox
// jspecify_nullness_intrinsically_not_nullable
Lib<NotNullAwareAnnotatedInnerOfNonParameterized.@Nullable Nested.DoublyNested> l2;

Lib<NotNullAwareAnnotatedInnerOfNonParameterized.Nested.DoublyNested> l3;
Expand Down
10 changes: 5 additions & 5 deletions samples/NotNullAwareAnnotatedInnerOfParameterized.java
Original file line number Diff line number Diff line change
Expand Up @@ -25,23 +25,23 @@ class DoublyNested {}

@Nullable Nested x4;

// jspecify_nullness_paradox
// jspecify_nullness_intrinsically_not_nullable
@Nullable NotNullAwareAnnotatedInnerOfParameterized<?>.Nested x5;

NotNullAwareAnnotatedInnerOfParameterized<?>.@Nullable Nested x6;

// jspecify_nullness_paradox
// jspecify_nullness_intrinsically_not_nullable
@Nullable NotNullAwareAnnotatedInnerOfParameterized<?>.Nested.DoublyNested x7;

// jspecify_nullness_paradox
// jspecify_nullness_intrinsically_not_nullable
NotNullAwareAnnotatedInnerOfParameterized<?>.@Nullable Nested.DoublyNested x8;

NotNullAwareAnnotatedInnerOfParameterized<?>.Nested.@Nullable DoublyNested x9;

// jspecify_nullness_paradox
// jspecify_nullness_intrinsically_not_nullable
Lib<@Nullable NotNullAwareAnnotatedInnerOfParameterized<?>.Nested.DoublyNested> l1;

// jspecify_nullness_paradox
// jspecify_nullness_intrinsically_not_nullable
Lib<NotNullAwareAnnotatedInnerOfParameterized<?>.@Nullable Nested.DoublyNested> l2;

Lib<NotNullAwareAnnotatedInnerOfParameterized<?>.Nested.DoublyNested> l3;
Expand Down
6 changes: 3 additions & 3 deletions samples/NotNullAwareAnnotatedTypeParameter.java
Original file line number Diff line number Diff line change
Expand Up @@ -17,12 +17,12 @@
import org.jspecify.annotations.Nullable;

class NotNullAwareAnnotatedTypeParameter {
// jspecify_nullness_paradox
// jspecify_unrecognized_location
interface Lib1<@Nullable T> {}

// jspecify_nullness_paradox
// jspecify_unrecognized_location
interface Lib2<@Nullable T extends Object> {}

// jspecify_nullness_paradox
// jspecify_unrecognized_location
interface Lib3<@Nullable T extends @Nullable Object> {}
}
6 changes: 3 additions & 3 deletions samples/NotNullAwareAnnotatedTypeParameterUnspec.java
Original file line number Diff line number Diff line change
Expand Up @@ -18,12 +18,12 @@
import org.jspecify.annotations.NullnessUnspecified;

class NotNullAwareAnnotatedTypeParameterUnspec {
// jspecify_nullness_paradox
// jspecify_unrecognized_location
interface Lib1<@NullnessUnspecified T> {}

// jspecify_nullness_paradox
// jspecify_unrecognized_location
interface Lib2<@NullnessUnspecified T extends Object> {}

// jspecify_nullness_paradox
// jspecify_unrecognized_location
interface Lib3<@NullnessUnspecified T extends @Nullable Object> {}
}
10 changes: 5 additions & 5 deletions samples/NotNullAwareAnnotatedWildcard.java
Original file line number Diff line number Diff line change
Expand Up @@ -19,18 +19,18 @@
class NotNullAwareAnnotatedWildcard {
interface Lib<T extends @Nullable Object> {}

// jspecify_nullness_paradox
// jspecify_unrecognized_location
Lib<@Nullable ?> x1;

// jspecify_nullness_paradox
// jspecify_unrecognized_location
Lib<@Nullable ? extends Object> x2;

// jspecify_nullness_paradox
// jspecify_unrecognized_location
Lib<@Nullable ? super Object> x3;

// jspecify_nullness_paradox
// jspecify_unrecognized_location
Lib<@Nullable ? extends @Nullable Object> x4;

// jspecify_nullness_paradox
// jspecify_unrecognized_location
Lib<@Nullable ? super @Nullable Object> x5;
}
10 changes: 5 additions & 5 deletions samples/NotNullAwareAnnotatedWildcardUnspec.java
Original file line number Diff line number Diff line change
Expand Up @@ -20,18 +20,18 @@
class NotNullAwareAnnotatedWildcardUnspec {
interface Lib<T extends @Nullable Object> {}

// jspecify_nullness_paradox
// jspecify_unrecognized_location
Lib<@NullnessUnspecified ?> x1;

// jspecify_nullness_paradox
// jspecify_unrecognized_location
Lib<@NullnessUnspecified ? extends Object> x2;

// jspecify_nullness_paradox
// jspecify_unrecognized_location
Lib<@NullnessUnspecified ? super Object> x3;

// jspecify_nullness_paradox
// jspecify_unrecognized_location
Lib<@NullnessUnspecified ? extends @Nullable Object> x4;

// jspecify_nullness_paradox
// jspecify_unrecognized_location
Lib<@NullnessUnspecified ? super @Nullable Object> x5;
}
4 changes: 2 additions & 2 deletions samples/PrimitiveAnnotations.java
Original file line number Diff line number Diff line change
Expand Up @@ -19,9 +19,9 @@

@DefaultNonNull
class PrimitiveAnnotations {
// jspecify_nullness_paradox
// jspecify_nullness_intrinsically_not_nullable
@Nullable int x1;
// jspecify_nullness_paradox
// jspecify_nullness_intrinsically_not_nullable
@Nullable int[] x2;

int x3;
Expand Down
4 changes: 2 additions & 2 deletions samples/PrimitiveAnnotationsUnspec.java
Original file line number Diff line number Diff line change
Expand Up @@ -19,9 +19,9 @@

@DefaultNonNull
class PrimitiveAnnotationsUnspec {
// jspecify_nullness_paradox
// jspecify_nullness_intrinsically_not_nullable
@NullnessUnspecified int x1;
// jspecify_nullness_paradox
// jspecify_nullness_intrinsically_not_nullable
@NullnessUnspecified int[] x2;

int x3;
Expand Down
17 changes: 14 additions & 3 deletions samples/README.md
Original file line number Diff line number Diff line change
Expand Up @@ -91,7 +91,7 @@ Sample inputs demonstrate 2 cases:
1. JSpecify annotations are applied in a way that is
[structurally illegal](https://docs.google.com/document/d/15NND5nBxMkZ-Us6wz3Pfbt4ODIaWaJ6JDs4w6h9kUaY/edit#heading=h.ib00ltjpj1xa).

<!-- TODO: Are we happy with the term "illegal?" If so, use it in the comment text instead of "paradox?" -->
<!-- TODO: Are we happy with the term "illegal?" -->

2. The second case is more nuanced: Based on JSpecify annotations and rules,
the code's types can all be augmented with nullness information. We could
Expand All @@ -110,9 +110,20 @@ cases above.

A comment on a given line provides information about the following line.

Such a comment contains one of 3 special sequences:
Such a comment contains one of 5 special sequences. The first 3 cover case 1
from above:

- `jspecify_nullness_paradox`: for case 1 above
- `jspecify_conflicting_annotations`: for cases like `@Nullable
@NullnessUnspecified Foo`

- `jspecify_unrecognized_location`: for cases like `class @Nullable Foo {}`,
in which JSpecify does not currently specify meaning for annotations on a
given location but we can imagine uses for them

- `jspecify_nullness_intrinsically_not_nullable`: for cases like `@Nullable
int`

The remaining 2 cover case 2:

- `jspecify_nullness_mismatch`: for certain instances of case 2

Expand Down