t-rasmud / checker-framework Goto Github PK

View Code? Open in Web Editor NEW

This project forked from typetools/checker-framework

1.0 1.0 2.0 222.95 MB

Pluggable type-checking for Java

Home Page: http://checkerframework.org/

License: Other

Shell 0.66% Batchfile 0.01% Makefile 0.09% Java 94.09% TeX 5.16%

checker-framework's People

Contributors

Stargazers

Watchers

Forkers

jwaataja xinyuliu12

checker-framework's Issues

Arrays.sort should implement additional type refinement

Arrays.sort currently has builtin support to type-refine @Det T @OrderNonDet [] to @Det T @Det []. This could be slightly more general. It should also type also refine @Det T @PolyDet [] to @Det T @PolyDet("down") []. This would allow methods to accept @Det T @NonDet [] as well. This could also be implemented for sorting on other collections.

This still doesn't allow @PolyDet T @PolyDet [] to be refined from sorting. Another possible addition would be that if the element type is not a collection, then it is type-refined to @PolyDet("down") T @PolyDet("down") []. This would allow parameters with this type to benefit from sorting.

Return types with @PolyDet("use") not allowed

In general, return types should not have @PolyDet("use"), but sometimes it's unavoidable when a type parameter includes it. Consider

import org.checkerframework.checker.determinism.qual.*;
import java.util.*;

public class ReturnList {
  public static <T extends @PolyDet("use") Object> @PolyDet List<T> returnList() {
    return null;
  }
}

Error:

ReturnList.java:5: error: [invalid.polydet.use] @PolyDet("use") annotation is only valid on formal parameters and type parameters of a method.
  public static <T extends @PolyDet("use") Object> @PolyDet List<T> returnList() {
                                                                    ^

This will come up when any return type has a type parameter included in the input. It's possible to write @PolyDet List<@PolyDet T>, but is that the intended usage?

Checker allows constructor types to be a supertype of the class type

It should not be allowed to have constructor types that are a supertype of the class type. So, the following example should not type check.

import org.checkerframework.checker.determinism.qual.*;
@Det class ConstructorIssue2 {
    @NonDet ConstructorIssue2() {}
}

But running the determinism checker on the above example doesn't flag any error.
I haven't been able to replicate this behavior with other checkers.

Annotations in extends clause don't affect valid types

If a class A extends @Det B, then all instances of A should be instances of @Det B, thus it should be impossible to have @NonDet A.

Consider

import org.checkerframework.checker.determinism.qual.*;

public class DetExtends extends @Det Object {
  public static void f(@NonDet DetExtends a) {
  }
}

This currently types check. This also applies to other checkers. Changing @Det to @NonNull and @NonDet to @Nullable results in the same thing.

Adding to Collections of a generic type

This is related to #8 where when you try to add to a List of a specific type, it requires a @NonDet Object. However, when the type is generic, a different issue comes up. These two problems together mean that it's very difficult to write a method that copies a collection. The code below shows an example of this new bug:

import java.util.*;

public class GenericsBug {
  public static <T> Set<T> toSet(List<T> list) {
    Set<T> result = new HashSet<T>();
    for (T element : list) {
      result.add(element);
    }
    return result;
  }
}

It gives the error:

javac -processor DeterminismChecker GenericsBug.java
GenericsBug.java:7: error: [argument.type.incompatible] incompatible types in argument.
      result.add(element);
                 ^
  found   : T extends @PolyDet Object
  required: T extends @NonDet Object
1 error

My theory for why this is is that because the List parameter is @PolyDet, it places an upper bound of @PolyDet on its type parameter. However, this doesn't seem to apply to the local collection, which is using @NonDet Object as an upper bound, which might be the default. However, since the T type should be the same for both collections, adding from one to the other shouldn't cause an issue.

There are several annotations I've tried to add to fix this message, but all of them lead to a different type of error, so there's really no easy to way to get around this.

length field incorrect for @PolyDet arrays

The following code currently type checks:

import org.checkerframework.checker.determinism.qual.*;

public class ArrayLen {
  public static void f(@PolyDet int @PolyDet [] a) {
    @Det int len = a.length;
  }
}

This is invalid because a could have the type @NonDet int @NonDet [] which would have non-deterministic length. The correct type would be @PolyDet("down") as with lists.

This only applies to @PolyDet. The correct error appears when using @NonDet directly:

import org.checkerframework.checker.determinism.qual.*;

public class ArrayLen {
  public static void f(@NonDet int @NonDet [] a) {
    @Det int len = a.length;
  }
}

Error:

ArrayLen.java:5: error: [assignment.type.incompatible] incompatible types in assignment.
    @Det int len = a.length;
                    ^
  found   : @NonDet int
  required: @Det int

"creation not allowed with given receiver" on @PolyDet type parameter

This class produces an error:

import org.checkerframework.checker.determinism.qual.*;

public class ConstructorReceivers<T extends @NonDet Object> {
  public static void f() {
    ConstructorReceivers<@PolyDet Integer> b = new ConstructorReceivers<@PolyDet Integer>();
  }
}

Error:

ConstructorReceivers.java:7: error: [constructor.invocation.invalid] creation of @Det ConstructorReceivers<@NonDet Integer> <init>() not allowed with given receiver;
    ConstructorReceivers<@PolyDet Integer> b = new ConstructorReceivers<@PolyDet Integer>();
                                               ^
  found   : @Det ConstructorReceivers<@PolyDet Integer>
  required: @Det ConstructorReceivers<@NonDet Integer>

The issue goes away when an the constructor takes a @PolyDet parameter rather than an empty parameter list. The problem is that because a ConstructorReceivers is not a collection, there should be no restriction on what its type parameter is.

Error with Arrays.asList

Consider the following class

import org.checkerframework.checker.determinism.qual.*;
import java.util.*;

public class AsListTest {
    public static void f() {
        @Det List<@Det String> list = Arrays.<@Det String>asList("");
    }
}

AsListTest.java:6: error: [invalid.element.type] element type (@Det) cannot be used with collection type (@NonDet)
        @Det List<@Det String> list = Arrays.<@Det String>asList("");
                                                                ^
AsListTest.java:6: error: [type.argument.type.incompatible] incompatible types in type argument.
        @Det List<@Det String> list = Arrays.<@Det String>asList("");
                                              ^
  found   : @Det String
  required: [extends @NonDet Object super @NonDet null]

The first error is incorrect because the asList method should be returning a @Det List not @NonDet. The second error is wrong because the method should be able to accept @Det type parameters. This would probably be fixed by updating the JDK annotations.

@PolyAll doesn't behave like @PolyDet in arrays

The @PolyAll annotation should be equivalent to adding @PolyDet unless something more specific is added, but this is not the case in arrays annotated as @PolyDet. When used as the element type on an array explicitly annotated as @PolyDet, it is instead resolved to @Det. Here, arr is a @Det int @PolyDet [] when it should be @PolyDet int @PolyDet [].

Example

import org.checkerframework.checker.determinism.qual.*;
import org.checkerframework.framework.qual.*;

public class PolyAllDeterminism {
  public static void f(@PolyAll int @PolyDet [] arr) {
    arr = new @PolyDet int @PolyDet[0];
  }
}

Error

PolyAllDeterminism.java:6: error: [assignment.type.incompatible] incompatible types in assignment.
    arr = new @PolyDet int @PolyDet[0];
          ^
  found   : @PolyDet int @PolyDet []
  required: @Det int @PolyDet []

This only happens when the input array is explicitly annotated as @PolyDet. The following code produces no error, as if the default @PolyDet took over.

import org.checkerframework.checker.determinism.qual.*;
import org.checkerframework.framework.qual.*;

public class PolyAllDeterminism {
  public static void f(@PolyAll int[] arr) {
    arr = new @PolyDet int @PolyDet[0];
  }
}

Literals are @NonDet in certain places

String and int literals are always the same across runs, so they should be @Det. The Determinism Checker sometimes flags them as @NonDet when used inside annotations on locally declared arrays.

Example

import org.checkerframework.checker.determinism.qual.*;

public class LiteralsBug {
  public static void f() {
    int @PolyDet("up") [] arr;
  }
}

Error

LiteralsBug.java:5: error: [annotation.type.incompatible] incompatible types in annotation.
    int @PolyDet("up") [] arr;
                 ^
  found   : @NonDet String
  required: @PolyDet String

This error only occurs exactly when a literal is used on the array type in a local declaration. It does not appear when used on the element type, in the expression it's initialized to, or in method signatures.

Two things:

These literals should be @Det.
Expressions involving annotations should be ignored since they have no effect on execution.

One or both of these should be fixed.

Also, this is not exclusive to String literals, it also occurs with ints:

import org.checkerframework.common.value.qual.*;

public class LiteralsBug {
  public static void f() {
    int @MinLen(1) [] arr;
  }
}

LiteralsBug.java:5: error: [annotation.type.incompatible] incompatible types in annotation.
    int @MinLen(1) [] arr;
                ^
  found   : @NonDet int
  required: @PolyDet int

Conditional error message should specify expression type

Expressions used in conditional statements are required to be @Det but there are many instances where we would want to use, e.g. @PolyDet with @SuppressWarnings. The error message says that the conditional expression is not @Det, but doesn't mention what the actual type is, making it difficult to know when to use @SuppressWarnings.

Example:

import org.checkerframework.checker.determinism.qual.*;

public class ConditionalsMessage {
  public static @PolyDet int f(@PolyDet boolean a, @PolyDet int b) {
    return (a) ? b : b;
  }
}

Error:

ConditionalsMessage.java:5: error: [invalid.type.on.conditional] conditional is not @Det. This will result in non-deterministic behavior
    return (a) ? b : b;
           ^

This method is sound, so we would want to use @SuppressWarnings here. However if a were @NonDet this would not be sound. The error message doesn't give a way to differentiate the two and if a is not a parameter it could be difficult or impossible to tell what its type is without testing.

In invalid assignment statements and most other error messages, both the found and required types are specified and giving both in this error message would make the checker easier to use.

Raw types treated differently if class is in annotated JDK

In a raw collection type, the rule that the element type of a collection must be a subtype of the collection itself, is only applied to classes in the annotated JDK. Consider the following class:

import org.checkerframework.checker.determinism.qual.*;
import java.util.*;

public class CollectionTypes {

    public static void f(@Det List a) {
    }

    public static void g(@Det Queue a) {
    }
}

CollectionTypes.java:6: error: [invalid.upper.bound.on.type.argument] upper bound of type argument (@NonDet) must be a subtype of the collection type (@Det)
    public static void f(@Det List a) {
                                   ^

This applies to regular classes and interface types. The error only occurs if the type is one of the collections in the annotated JDK. Whether or not a class is in the annotated JDK shouldn't affect whether there's an error. All these classes are subtypes of Collection, so the check should apply to both.

Collection parameters can't use class level type parameters

On class level type variables, the upper bound should usually be @NonDet so that any type can be used. This causes a problem when creating collections of type other than @NonDet. Consider

import org.checkerframework.checker.determinism.qual.*;
import java.util.*;

public class ClassParam<T extends @NonDet Object> {
  public void f(@PolyDet ClassParam<T> this, List<T> a) {
  }
}

Error:

ClassParam.java:5: error: [invalid.upper.bound.on.type.argument] upper bound of type argument (@NonDet) must be a subtype of the collection type (@PolyDet)
  public void f(@PolyDet ClassParam<T> this, List<T> a) {
                                                     ^

This also happens on fields. As a workaround, fields can be declared @NonDet and @SuppressWarnings can be used whenever that field is used. With parameters, the interface itself would have to be changed, which is undesirable.

Locally created Polymorphic Object resolves to default type qualifier.

When a new Object of type @PolyDet is created locally inside a method, it is treated as a @Det Object (@Det is the default type qualifier in the hierarchy).

Example:

import org.checkerframework.checker.determinism.qual.*;
class TestLocalPoly {
    void testPolyDetLocal(@PolyDet Object input){
        @PolyDet Object local = new @PolyDet Object();
        System.out.println(local);
        System.out.println(input);
    }
}

Since System.out.println is annotated to accept only @Det arguments, both the print lines must flag an error. Instead, the determinism checker reports just the following error:

./checker/tests/determinism/TestLocalPoly.java:10: error: [argument.type.incompatible] incompatible types in argument.
        System.out.println(input);
                           ^
  found   : @PolyDet Object
  required: @Det Object
1 error

This means that local is treated as @Det and not as @PolyDet.

I also experimented with the tainting checker to see if this behavior can be reproduced. Consider this example:

import org.checkerframework.checker.tainting.qual.*;
class TestLocalPoly {
    void testPolyTaintedLocal(@PolyTainted Object input){
        @PolyTainted Object local = new @PolyTainted Object();
    }
}

It gives the following error:

./checker/tests/determinism/TestLocalPoly.java:14: error: [assignment.type.incompatible] incompatible types in assignment.
        @PolyTainted Object local = new @PolyTainted Object();
                                    ^
  found   : @Tainted Object
  required: @PolyTainted Object
1 error

So this means that the new Object created gets the default annotation (@Tainted) instead of @PolyTainted.
This looks like an issue in the framework where the polymorphic annotation at Object creation is not resolved correctly.

Note: The determinism checker does not report [assignment.type.incompatible] error at the Object creation line because @Det is the bottom qualifier in the type hierarchy.

Incorrect Random annotations in JDK

The current annotations for Random are unsound. Consider

public class TestRandom {
    public static void f(@Det Random r, @NonDet int seed) {
        r.setSeed(seed);
    }
}

This should not be allowed because afterward r is still @Det, even though though it was seeded with a random value. A similar problem holds with the nextBytes method.

Incorrect dataflow in enhanced for loop

Example:

import org.checkerframework.checker.determinism.qual.*;
import java.util.HashMap;
import java.util.Map.Entry;
import java.util.Iterator;

public class EnhancedFor {
    void test(@OrderNonDet HashMap<@Det String, @Det String> map) {
        for (Iterator<Entry<String, String>> entries = map.entrySet().iterator(); entries.hasNext(); ) {
            @Det Entry<@Det String, @Det String> item = entries.next();
        }
    }
    void test1(@OrderNonDet HashMap<@Det String, @Det String> map) {
        for (@Det Entry<@Det String, @Det String> item : map.entrySet()) {
        }
    }
}

In this test case, both the for loops are semantically equivalent. However, running the determinism checker with the command javac -processor determinism EnhancedFor.java produces the expected warning (see below) in the first loop but not in the second.

EnhancedFor.java:10: error: [assignment.type.incompatible] incompatible types in assignment.
            @Det Entry<@Det String, @Det String> item = entries.next();
                                                                                                               ^
  found   : @NonDet Entry<@Det String, @Det String>
  required: @Det Entry<@Det String, @Det String>
1 error

Incorrect type while accessing elements of 2 dimensional arrays

Example:

import java.util.ArrayList;
import org.checkerframework.checker.determinism.qual.*;
public class Test2DArrays<T> {
    void testAccess(@Det int @NonDet[] @Det[] arr){
        // :: error: (assignment.type.incompatible)
        @Det int x = arr[0][0];
    }
}

Since arr is an array of type @NonDet[@Det[@Det int]], accessing its elements should return @NonDet and the checker should report an error at the line @Det int x = arr[0][0];. But, the checker does not flag any error for the above code.

@PolyDet("use") with parameters and returns

When used in type parameters, @PolyDet("use") sometimes vanishes when it's required. This makes it so that it can't be used on collections in parameters or returns when there is a method call involved. For example:

import java.util.*;
import org.checkerframework.checker.determinism.qual.*;

public class CarryPolyUse {
  public static <T extends @PolyDet("use") Object> @PolyDet List<T> f(@PolyDet List<T> list) {
    return null;
  }

  public static <T extends @PolyDet("use") Object> @PolyDet List<T> g(@PolyDet List<T> list) {
    return f(list);
  }
}

Error:

CarryPolyUse.java:10: error: [return.type.incompatible] incompatible types in return.
    return f(list);
            ^
  found   : @PolyDet List<T extends @PolyDet Object>
  required: @PolyDet List<T extends @PolyDet("use") Object>
CarryPolyUse.java:10: error: [argument.type.incompatible] incompatible types in argument.
    return f(list);
             ^
  found   : @PolyDet List<T extends @PolyDet("use") Object>
  required: @PolyDet List<T extends @PolyDet Object>

The first error shows that after a method call, @PolyDet("use") is dropped when it's required in the return type, despite the fact that it's the same type parameter and should be the same type, and also that since @PolyDet and @PolyDet("use") are always given the same type, it could be the case that this should be allowed regardless

The second error shows that in the body of a method, the @PolyDet("use") on a type parameter disappears when it's required.

@PolyDet for generic arrays not carried correctly when used in methods

When there is a method that takes a @PolyDet array and returns a @PolyDet result, and this method is called with a @PolyDet or @Det array, what should be a @PolyDet or @Det result is incorrectly typed as @NonDet. This can be seen in the example below:

import org.checkerframework.checker.determinism.qual.*;

public class GenericArraysBug {
  public static <T> String arrToString(T[] arr) {
    return arr.toString();
  }

  public static <T> String callToString(T[] arr) {
    return arrToString(arr);
  }

  public static <T> @Det String callToStringDet(T @Det [] arr) {
    return arrToString(arr);
  }
}

GenericArraysBug.java:9: error: [return.type.incompatible] incompatible types in return.
    return arrToString(arr);
                      ^
  found   : @NonDet String
  required: @PolyDet String
GenericArraysBug.java:13: error: [return.type.incompatible] incompatible types in return.
    return arrToString(arr);
                      ^
  found   : @NonDet String
  required: @Det String

By default, arrToString takes a @PolyDet array and returns a @PolyDet String. This means that both callToString and callToStringDet should be legal. It seems that this problem doesn't occur with calling toString directly as seen in arrToString, where there is no error. This means the issue is probably with how @PolyDet is resolved for parameters or returns.

This only happens with generic arrays.

Sorting with Comparators causes confusing errors

There are several issues with the Arrays.sort method that takes a Comparator. One of them is that it doesn't do type refinement. This can be seen by the fact that the println still produces an error. This isn't an issue with the non-comparator sorting methods. The following is an excerpt from the pull request I opened containing tests for this method.

    void testSort2(@Det Integer @OrderNonDet [] a) {
        IntComparator c = new IntComparator();
        Arrays.sort(a, c);
        System.out.println(a[0]);
    }

    class IntComparator implements Comparator<Integer> {
        public int compare(Integer i1, Integer i2) {
            return 0;
        }
    }

This produces the errors below:

TestArraysSort.java:7: error: [type.argument.type.incompatible] incompatible types in type argument.
        Arrays.sort(a, c);
                   ^
  found   : @PolyDet Integer
  required: [extends @NonDet Object super @OrderNonDet null]
TestArraysSort.java:7: error: [argument.type.incompatible] incompatible types in argument.
        Arrays.sort(a, c);
                       ^
  found   : @Det TestArraysSort.@Det IntComparator
  required: @OrderNonDet Comparator<? extends @NonDet Object super @OrderNonDet Integer>
TestArraysSort.java:8: error: [argument.type.incompatible] incompatible types in argument.
        System.out.println(a[0]);
                            ^
  found   : @NonDet Integer
  required: @Det Object

The other issue is these other two errors with the method and Comparator argument itself. One fix I considered was to make the Comparator itself implement Comparator<@NonDet Integer>. This doesn't work, though, as it seems to require the arguments to the compare method be @PolyDet. This doesn't seem quite correct behavior, but the bigger issue is that the Comparator is not accepted as is, which it seems like it should be. The contract on the type of the comparator in the JDK is ? super T. Here T is Integer so this should be satisfied.

Incorrect treatment of dot operator

The checker seems to mark expressions that should be @PolyDet as @NonDet when they involve this or super. In one method that returns a call to another method getString(), simply using getString() is correctly marked as @PolyDet but using this.getString() is not.

Similarly, using super.toString() should be @PolyDet since it is marked that way in the Object class. However, it is flagged as @NonDet.

The classes are:

public class Foo {
    @Override
    public String toString() {
        return super.toString();
    }
}

and

public class Bar {
    public String toString() {
        return this.getString();
    }

    public String getString() {
        return "foo";
    }
}

The errors are:

Foo.java:8: error: [return.type.incompatible] incompatible types in return.
        return super.toString();
                             ^
  found   : @NonDet String
  required: @PolyDet String

and

Bar.java:15: error: [return.type.incompatible] incompatible types in return.
        return this.getString();
                             ^
  found   : @NonDet String
  required: @PolyDet String

The full errors are attached.
Bar_errors.txt
Foo_errors.txt

NullPointerException on one file

When running the checker on the library plume-util, the checker is failing with a NullPointerException on one file. It seems to work fine for the rest of the files.

I'm not aware of if there could be a simpler case, there doesn't seem to be anything special about this one class. The file is here.

The error is:

error: SourceChecker.typeProcess: unexpected Throwable (NullPointerException) while processing /home/jason/git/plume-util/src/main/java/org/plumelib/util/CollectionsPlume.java
  Compilation unit: /home/jason/git/plume-util/src/main/java/org/plumelib/util/CollectionsPlume.java
  Last visited tree at line 34 column 1:
  public final class CollectionsPlume {
  Exception: java.lang.NullPointerException; Stack trace: org.checkerframework.checker.determinism.DeterminismQualifierPolymorphism.recursiveReplaceForPolyUpOrDown(DeterminismQualifierPolymorphism.java:148)
  org.checkerframework.checker.determinism.DeterminismQualifierPolymorphism.replaceForPolyUpOrDown(DeterminismQualifierPolymorphism.java:108)
  org.checkerframework.checker.determinism.DeterminismQualifierPolymorphism.replace(DeterminismQualifierPolymorphism.java:68)
  org.checkerframework.framework.type.poly.AbstractQualifierPolymorphism$Replacer.scan(AbstractQualifierPolymorphism.java:247)
  org.checkerframework.framework.type.poly.AbstractQualifierPolymorphism$Replacer.scan(AbstractQualifierPolymorphism.java:243)
  org.checkerframework.framework.type.visitor.AnnotatedTypeScanner.visitExecutable(AnnotatedTypeScanner.java:202)
  org.checkerframework.framework.type.AnnotatedTypeMirror$AnnotatedExecutableType.accept(AnnotatedTypeMirror.java:1029)
  org.checkerframework.framework.type.visitor.AnnotatedTypeScanner.scan(AnnotatedTypeScanner.java:103)
  org.checkerframework.framework.type.poly.AbstractQualifierPolymorphism$Replacer.scan(AbstractQualifierPolymorphism.java:248)
  org.checkerframework.framework.type.poly.AbstractQualifierPolymorphism$Replacer.scan(AbstractQualifierPolymorphism.java:243)
  org.checkerframework.framework.type.visitor.AnnotatedTypeScanner.visit(AnnotatedTypeScanner.java:91)
  org.checkerframework.framework.type.poly.AbstractQualifierPolymorphism.annotate(AbstractQualifierPolymorphism.java:147)
  org.checkerframework.framework.type.GenericAnnotatedTypeFactory.methodFromUse(GenericAnnotatedTypeFactory.java:1529)
  org.checkerframework.framework.type.TypeFromExpressionVisitor.visitMethodInvocation(TypeFromExpressionVisitor.java:170)
  org.checkerframework.framework.type.TypeFromExpressionVisitor.visitMethodInvocation(TypeFromExpressionVisitor.java:44)
  com.sun.tools.javac.tree.JCTree$JCMethodInvocation.accept(JCTree.java:1477)
  com.sun.source.util.SimpleTreeVisitor.visit(SimpleTreeVisitor.java:53)
  org.checkerframework.framework.type.TypeFromTree.fromExpression(TypeFromTree.java:36)
  org.checkerframework.framework.type.AnnotatedTypeFactory.fromExpression(AnnotatedTypeFactory.java:1233)
  org.checkerframework.framework.type.AnnotatedTypeFactory.getAnnotatedType(AnnotatedTypeFactory.java:1011)
  org.checkerframework.framework.flow.CFAbstractTransfer.getValueFromFactory(CFAbstractTransfer.java:201)
  org.checkerframework.framework.flow.CFAbstractTransfer.visitMethodInvocation(CFAbstractTransfer.java:925)
  org.checkerframework.checker.determinism.DeterminismTransfer.visitMethodInvocation(DeterminismTransfer.java:50)
  org.checkerframework.checker.determinism.DeterminismTransfer.visitMethodInvocation(DeterminismTransfer.java:41)
  org.checkerframework.dataflow.cfg.node.MethodInvocationNode.accept(MethodInvocationNode.java:76)
  org.checkerframework.dataflow.analysis.Analysis.callTransferFunction(Analysis.java:408)
  org.checkerframework.dataflow.analysis.Analysis.performAnalysisBlock(Analysis.java:234)
  org.checkerframework.dataflow.analysis.Analysis.performAnalysis(Analysis.java:187)
  org.checkerframework.framework.flow.CFAbstractAnalysis.performAnalysis(CFAbstractAnalysis.java:91)
  org.checkerframework.framework.type.GenericAnnotatedTypeFactory.analyze(GenericAnnotatedTypeFactory.java:1214)
  org.checkerframework.framework.type.GenericAnnotatedTypeFactory.performFlowAnalysis(GenericAnnotatedTypeFactory.java:1132)
  org.checkerframework.framework.type.GenericAnnotatedTypeFactory.checkAndPerformFlowAnalysis(GenericAnnotatedTypeFactory.java:1476)
  org.checkerframework.framework.type.GenericAnnotatedTypeFactory.preProcessClassTree(GenericAnnotatedTypeFactory.java:260)
  org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:291)
  org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:159)
  com.sun.tools.javac.tree.JCTree$JCClassDecl.accept(JCTree.java:720)
  com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:50)
  org.checkerframework.framework.source.SourceVisitor.visit(SourceVisitor.java:85)
  org.checkerframework.framework.source.SourceChecker.typeProcess(SourceChecker.java:972)
  org.checkerframework.common.basetype.BaseTypeChecker.typeProcess(BaseTypeChecker.java:494)
  org.checkerframework.javacutil.AbstractTypeProcessor$AttributionTaskListener.finished(AbstractTypeProcessor.java:182)
  com.sun.tools.javac.api.ClientCodeWrapper$WrappedTaskListener.finished(ClientCodeWrapper.java:681)
  com.sun.tools.javac.api.MultiTaskListener.finished(MultiTaskListener.java:111)
  com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1342)
  com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1296)
  com.sun.tools.javac.main.JavaCompiler.compile2(JavaCompiler.java:901)
  com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:860)
  com.sun.tools.javac.main.Main.compile(Main.java:523)
  com.sun.tools.javac.api.JavacTaskImpl.doCall(JavacTaskImpl.java:129)
  com.sun.tools.javac.api.JavacTaskImpl.call(JavacTaskImpl.java:138)
  org.gradle.api.internal.tasks.compile.JdkJavaCompiler.execute(JdkJavaCompiler.java:48)
  org.gradle.api.internal.tasks.compile.JdkJavaCompiler.execute(JdkJavaCompiler.java:35)
  org.gradle.api.internal.tasks.compile.NormalizingJavaCompiler.delegateAndHandleErrors(NormalizingJavaCompiler.java:98)
  org.gradle.api.internal.tasks.compile.NormalizingJavaCompiler.execute(NormalizingJavaCompiler.java:51)
  org.gradle.api.internal.tasks.compile.NormalizingJavaCompiler.execute(NormalizingJavaCompiler.java:37)
  org.gradle.api.internal.tasks.compile.CleaningJavaCompilerSupport.execute(CleaningJavaCompilerSupport.java:35)
  org.gradle.api.internal.tasks.compile.CleaningJavaCompilerSupport.execute(CleaningJavaCompilerSupport.java:25)
  org.gradle.api.tasks.compile.JavaCompile.performCompilation(JavaCompile.java:207)
  org.gradle.api.tasks.compile.JavaCompile.compile(JavaCompile.java:192)
  org.gradle.api.tasks.compile.JavaCompile.compile(JavaCompile.java:124)
  sun.reflect.GeneratedMethodAccessor912.invoke(Unknown Source)
  sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
  java.lang.reflect.Method.invoke(Method.java:498)
  org.gradle.internal.reflect.JavaMethod.invoke(JavaMethod.java:73)
  org.gradle.api.internal.project.taskfactory.IncrementalTaskAction.doExecute(IncrementalTaskAction.java:50)
  org.gradle.api.internal.project.taskfactory.StandardTaskAction.execute(StandardTaskAction.java:39)
  org.gradle.api.internal.project.taskfactory.StandardTaskAction.execute(StandardTaskAction.java:26)
  org.gradle.api.internal.tasks.execution.ExecuteActionsTaskExecuter$1.run(ExecuteActionsTaskExecuter.java:124)
  org.gradle.internal.progress.DefaultBuildOperationExecutor$RunnableBuildOperationWorker.execute(DefaultBuildOperationExecutor.java:336)
  org.gradle.internal.progress.DefaultBuildOperationExecutor$RunnableBuildOperationWorker.execute(DefaultBuildOperationExecutor.java:328)
  org.gradle.internal.progress.DefaultBuildOperationExecutor.execute(DefaultBuildOperationExecutor.java:199)
  org.gradle.internal.progress.DefaultBuildOperationExecutor.run(DefaultBuildOperationExecutor.java:110)
  org.gradle.api.internal.tasks.execution.ExecuteActionsTaskExecuter.executeAction(ExecuteActionsTaskExecuter.java:113)
  org.gradle.api.internal.tasks.execution.ExecuteActionsTaskExecuter.executeActions(ExecuteActionsTaskExecuter.java:95)
  org.gradle.api.internal.tasks.execution.ExecuteActionsTaskExecuter.execute(ExecuteActionsTaskExecuter.java:73)
  org.gradle.api.internal.tasks.execution.OutputDirectoryCreatingTaskExecuter.execute(OutputDirectoryCreatingTaskExecuter.java:51)
  org.gradle.api.internal.tasks.execution.SkipUpToDateTaskExecuter.execute(SkipUpToDateTaskExecuter.java:59)
  org.gradle.api.internal.tasks.execution.ResolveTaskOutputCachingStateExecuter.execute(ResolveTaskOutputCachingStateExecuter.java:54)
  org.gradle.api.internal.tasks.execution.ValidatingTaskExecuter.execute(ValidatingTaskExecuter.java:59)
  org.gradle.api.internal.tasks.execution.SkipEmptySourceFilesTaskExecuter.execute(SkipEmptySourceFilesTaskExecuter.java:101)
  org.gradle.api.internal.tasks.execution.FinalizeInputFilePropertiesTaskExecuter.execute(FinalizeInputFilePropertiesTaskExecuter.java:44)
  org.gradle.api.internal.tasks.execution.CleanupStaleOutputsExecuter.execute(CleanupStaleOutputsExecuter.java:88)
  org.gradle.api.internal.tasks.execution.ResolveTaskArtifactStateTaskExecuter.execute(ResolveTaskArtifactStateTaskExecuter.java:62)
  org.gradle.api.internal.tasks.execution.SkipTaskWithNoActionsExecuter.execute(SkipTaskWithNoActionsExecuter.java:52)
  org.gradle.api.internal.tasks.execution.SkipOnlyIfTaskExecuter.execute(SkipOnlyIfTaskExecuter.java:54)
  org.gradle.api.internal.tasks.execution.ExecuteAtMostOnceTaskExecuter.execute(ExecuteAtMostOnceTaskExecuter.java:43)
  org.gradle.api.internal.tasks.execution.CatchExceptionTaskExecuter.execute(CatchExceptionTaskExecuter.java:34)
  org.gradle.execution.taskgraph.DefaultTaskGraphExecuter$EventFiringTaskWorker$1.run(DefaultTaskGraphExecuter.java:248)
  org.gradle.internal.progress.DefaultBuildOperationExecutor$RunnableBuildOperationWorker.execute(DefaultBuildOperationExecutor.java:336)
  org.gradle.internal.progress.DefaultBuildOperationExecutor$RunnableBuildOperationWorker.execute(DefaultBuildOperationExecutor.java:328)
  org.gradle.internal.progress.DefaultBuildOperationExecutor.execute(DefaultBuildOperationExecutor.java:199)
  org.gradle.internal.progress.DefaultBuildOperationExecutor.run(DefaultBuildOperationExecutor.java:110)
  org.gradle.execution.taskgraph.DefaultTaskGraphExecuter$EventFiringTaskWorker.execute(DefaultTaskGraphExecuter.java:241)
  org.gradle.execution.taskgraph.DefaultTaskGraphExecuter$EventFiringTaskWorker.execute(DefaultTaskGraphExecuter.java:230)
  org.gradle.execution.taskgraph.DefaultTaskPlanExecutor$TaskExecutorWorker.processTask(DefaultTaskPlanExecutor.java:123)
  org.gradle.execution.taskgraph.DefaultTaskPlanExecutor$TaskExecutorWorker.access$200(DefaultTaskPlanExecutor.java:79)
  org.gradle.execution.taskgraph.DefaultTaskPlanExecutor$TaskExecutorWorker$1.execute(DefaultTaskPlanExecutor.java:104)
  org.gradle.execution.taskgraph.DefaultTaskPlanExecutor$TaskExecutorWorker$1.execute(DefaultTaskPlanExecutor.java:98)
  org.gradle.execution.taskgraph.DefaultTaskExecutionPlan.execute(DefaultTaskExecutionPlan.java:623)
  org.gradle.execution.taskgraph.DefaultTaskExecutionPlan.executeWithTask(DefaultTaskExecutionPlan.java:578)
  org.gradle.execution.taskgraph.DefaultTaskPlanExecutor$TaskExecutorWorker.run(DefaultTaskPlanExecutor.java:98)
  org.gradle.internal.concurrent.ExecutorPolicy$CatchAndRecordFailures.onExecute(ExecutorPolicy.java:63)
  org.gradle.internal.concurrent.ManagedExecutorImpl$1.run(ManagedExecutorImpl.java:46)
  java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1149)
  java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:624)
  org.gradle.internal.concurrent.ThreadFactoryImpl$ManagedThreadRunnable.run(ThreadFactoryImpl.java:55)
  java.lang.Thread.run(Thread.java:748)

T extends @NonDet Object not equivalent to T in constructor types

The default for upper bounds on class variables is @NonDet Object. Thus, class A<T> and class A<T extends @nondet Object` should be equivalent. Using each can produce different behavior.

import org.checkerframework.checker.determinism.qual.*;
import java.util.*;

public class ConstructorTypeParam<T> implements @NonDet Iterator<T> {
  public ConstructorTypeParam(@PolyDet List<T> a) {
  }

  public @PolyDet("down") boolean hasNext() {
    return false;
  }

  public T next() {
    return null;
  }
}

Error:

ConstructorTypeParam.java:5: error: [invalid.upper.bound.on.type.argument] upper bound of type argument (@NonDet) must be a subtype of the collection type (@Det)
  public ConstructorTypeParam() {
         ^

Now we add T extends @NonDet Object:

import org.checkerframework.checker.determinism.qual.*;

public class ConstructorTypeParam<T extends @NonDet Object> implements @NonDet Iterator<T> {
  public ConstructorTypeParam() {
  }

  public @PolyDet("down") boolean hasNext() {
    return false;
  }

  public T next() {
    return null;
  }
}

This types check even though it should be semantically equivalent to the previous code. The most likely explanation is that the return type of the constructor is changing.

Test on @NonDet value should make all subsequent computations @NonDet

Consider:

import org.checkerframework.checker.determinism.qual.*;
import java.util.*;

public class Conditionals {
  public static @Det int f(@NonDet boolean b, @Det int i, @Det int j) {
    return (b) ? i : j;
  }
}

This class type-checks without error. Because b is not guaranteed to be the same on each run, which of i or j that is returned could also vary, so the return type should be @NonDet. This is also the case for full if-else statements and loops.

Because the conditions under which code is run, which could be non-deterministic, are not taken into account this is a source of false negatives.

Comparators can't sort arrays

Comparators implement the Comparator<T> interface. Here is an example below:

import java.util.*;
import org.checkerframework.checker.determinism.qual.*;

public class ComparatorTest {
    public static void sortIntArray(Integer[] arr) {
        Arrays.sort(arr, new IntComparator());
    }


    public static class IntComparator implements Comparator<Integer> {
        public int compare(Integer val1, Integer val2) {
            return val1 - val2;
        }
    }
}

This gives the error

ComparatorTest.java:6: error: [argument.type.incompatible] incompatible types in argument.
        Arrays.sort(arr, new IntComparator());
                         ^
  found   : @Det IntComparator
  required: @PolyDet Comparator<? extends @NonDet Object super @PolyDet Integer>

This can be fixed by making IntComparator implement Comparator<@PolyDet Integer>. The problem is that then it cannot sort @NonDet arrays. For example, with the modification below

import java.util.*;
import org.checkerframework.checker.determinism.qual.*;

public class ComparatorTest {
    public static void sortIntArray(@NonDet Integer @NonDet [] arr) {
        Arrays.sort(arr, new IntComparator());
    }


    public static class IntComparator implements Comparator<Integer> {
        public int compare(Integer val1, Integer val2) {
            return val1 - val2;
        }
    }
}

We get the error

ComparatorTest.java:6: error: [argument.type.incompatible] incompatible types in argument.
        Arrays.sort(arr, new IntComparator());
                         ^
  found   : @Det IntComparator
  required: @NonDet Comparator<? extends @NonDet Object super @NonDet Integer>

This case is harder because if we make the Comparator implement Comparator<@NonDet Integer>, there is an issue with actually extending the compare method, since its return type is supposed to be @PolyDet but it would have to be @NonDet here. Then we would lose the ability to sort @Det or @PolyDet arrays, I believe.

This specific issue can be fixed by going into the JDK and annotating the compare method to explicitly take and return @PolyDet values, but it seems there's a larger problem, which is implementing interfaces that specialize the type parameter to a specific type. This causes a conflict because the defaults for type parameters may conflict with what we'd want, which is for this Comparator to be able to compare both @Det, @PolyDet, and @NonDet items for sorting.

Default return types with receivers

In static methods, when there are no unannotated parameters, the return type defaults to @Det rather than @PolyDet. This currently doesn't apply to methods with receivers.

import org.checkerframework.checker.determinism.qual.*;
import java.util.*;

public class ReturnTypeTest {
    String f(@Det ReturnTypeTest this) {
        return null;
    }

    static void g(@Det ReturnTypeTest a) {
        @Det String b = a.f();
    }
}

ReturnTypeTest.java:10: error: [assignment.type.incompatible] incompatible types in assignment.
        @Det String b = a.f();
                           ^
  found   : @NonDet String
  required: @Det String

The return type defaults to @PolyDet which resolves to @NonDet because there are no @PolyDet receivers. It should default to @Det because the same rule should apply to instance methods as static methods.

Array getClass always creates an error

Consider this class

import org.checkerframework.checker.determinism.qual.*;
import java.util.*;

public class ArrayGetClass {
    public static void f(@Det Object @Det [] arr) {
        Class<?> c = arr.getClass();
    }
}

I get the following error

ArrayGetClass.java:6: error: [invalid.array.component.type] component type (@Det) cannot be used with array type (@NonDet)
        Class<?> c = arr.getClass();
                                 ^

The returned class's type parameter should be the same as the Object that getClass was called on, which is a valid array type. So, this shouldn't be an error. I believe the issue is with the fact that the return type actually uses the erasure type, as described here. However, this is unique to arrays, the same problem doesn't occur with subtypes of Collection.

LinkedHashSet treated like HashSet.

There are built in rules to handle constructing instances of HashSet. The checker checks these by seeing if the class being constructed is a subtype of HashSet. This means LinedHashSet is included, even though it has different rules.

Consider the following class

import org.checkerframework.checker.determinism.qual.*;
import java.util.*;

public class LinkedHashSetTest {
    public static void f(@Det List<@Det String> c) {
        @Det Set<@Det String> s = new LinkedHashSet<@Det String>(c);
    }
}

I get this error

LinkedHashSetTest.java:6: error: [assignment.type.incompatible] incompatible types in assignment.
        @Det Set<@Det String> s = new LinkedHashSet<@Det String>(c);
                                  ^
  found   : @OrderNonDet LinkedHashSet<@Det String>
  required: @Det Set<@Det String>

This indicates that the HashSet rules are being used even though LinkedHashSet can be @Det, and in the JDK this method is annotated as @PolyDet LinkedHashSet(@PolyDet Collection<? extends E>), so passing @Det List should create a @Det LinkedHashSet.

Nested generics not expanded correctly

When a type parameter extends a type that references itself, the checker seems to not accept expressions that it should. In the error message it seems like it does one extra level of recursive expansion on the type parameter on the found type.

Take the following class:

public class NestedGenerics<T extends Comparable<T>> {
    public int compare(T[] a1, T[] a2) {
        return a1[0].compareTo(a2[0]);
    }
}

This gives the error:

NestedGenerics.java:7: error: [argument.type.incompatible] incompatible types in argument.
        return a1[0].compareTo(a2[0]);
                                 ^
  found   : T extends @PolyDet("") Comparable<T extends @Det Comparable<T extends @Det Comparable<T>>>
  required: T extends @Det Comparable<T extends @Det Comparable<T>>

In particular, a1[0] and a2[0] are the same type, T, and that type is explicitly Comparable to itself. The issue goes away when not using arrays, which might means this might be related to the issue of returning an array of a generic type.

@PolyDet constructors allow @Det instances made with @NonDet params

When a constructor's return type is @PolyDet, users can circumvent type checking constructor parameters, introducing unsoundness without a warning. Consider the following class:

import org.checkerframework.checker.determinism.qual.*;

public class PolyConstructor {
    @PolyDet PolyConstructor(@PolyDet int i) {
    }

    static void f(@NonDet int i) {
        @Det PolyConstructor p = new @Det PolyConstructor(i);
    }
}

This code should not type check because we construct the PolyConstructor with a @NonDet parameter. Thus, @PolyDet should resolve to @NonDet and the constructed instance should be @NonDet. Adding @Det to the constructor invocation seems to override this. This is equivalent to writing (@Det PolyConstructor) new PolyConstructor(i), which would be a downcast, this should at least issue a warning.

Certain calls to System.getProperty should be built-in

Although calls to System.getProperty can be different on separate runs, there are certain calls that should be considered deterministic. Specifically, the system specific line and path separators are different on different operating systems, but will always produce the same result on the same machine so it would be useful to consider the expressions System.getProperty("line.separator") and System.getProperty("path.separator") to be @Det. These are currently @NonDet and would have to be hard-coded in.

Using the determinism checker with other classes annotated for the determinism checker

The determinism checker defaults fields to @Det. This means that constructors have to take @Det arguments. As an example, with the following class we get an error in the constructor.

public class Strings {
    public static class StringHolder {
        public String data;

        public StringHolder(String data) {
            this.data = data;
        }
    }

    public static StringHolder makeHolder(String data) {
        return new StringHolder(data);
    }
}

This gives the error:

Strings.java:6: error: [assignment.type.incompatible] incompatible types in assignment.
            this.data = data;
                        ^
  found   : @PolyDet String
  required: @Det String

So, these constructor arguments must be annotated as @Det. However, this raises problems when other class use this constructor. There are many instances where we would want to construct a @NonDet or @PolyDet instance of such a class, but doing so would be impossible because the constructor only takes @Det arguments. What we would want would be to be able to create a @PolyDet StringHolder from a @PolyDet String data. However, this isn't possible, as seen below:

public class Strings {
    public static class StringHolder {
        public String data;

        public StringHolder(@Det String data) {
            this.data = data;
        }
    }

    public static StringHolder makeHolder(String data) {
        return new StringHolder(data);
    }
}

which gives the error:

Strings.java:8: error: [assignment.type.incompatible] incompatible types in assignment.
            this.data = data;
                        ^
  found   : @PolyDet String
  required: @Det String

Implement same ".equals" precision for Map as Set.

For sets we have the rule that if the receiver of .equals is an @OrderNonDet Set and the other parameter is the same, then we return @Det. This rule also makes sense for Maps, but when I compile this class:

import java.util.*;
import org.checkerframework.checker.determinism.qual.*;

public class MapTest {

  public @PolyDet("down") boolean f(
      @OrderNonDet Map<@Det String, @Det String> m1,
      @OrderNonDet Map<@Det String, @Det String> m2) {
    return m1.equals(m2);
  }
}

I get this error

MapTest.java:9: error: [return.type.incompatible] incompatible types in return.
    return m1.equals(m2);
                    ^
  type of expression: @NonDet boolean
  method return type: @PolyDet("down") boolean

JDK annotations should be @PolyDet of "up" or "down"

In general, if a method takes a collection and its return type is not a collection, that type should be either @PolyDet("up") or @PolyDet("down"). This should also be the case if a parameter is of type Object because it could accept a collection.

This mainly applies to methods that will be overridden or implemented by unknown clients. The Object class in the JDK is an example. The equals and toString methods will often be @PolyDet("up") when implemented on collections or classes that use collections. Thus, to be as permissive as possible, these two methods should have return @PolyDet("up") rather than @PolyDet.

Default for constructors not @PolyDet

The default for return types is @PolyDet as well as constructors. This doesn't seem to be happening with constructors.

import org.checkerframework.checker.determinism.qual.*;
import java.util.*;

public class DetConstructor {
  public DetConstructor(@PolyDet int a) {
  }

  public static void f(@PolyDet int b) {
    @Det DetConstructor c = new DetConstructor(b);
  }
}

Here we have a constructor that takes a @PolyDet argument. The result type should be @PolyDet but this code types check. This shouldn't be the case because in f we assign this to a @Det instance.

If we explicitly add @PolyDet then we get the expected error:

import org.checkerframework.checker.determinism.qual.*;
import java.util.*;

public class DetConstructor {
  public @PolyDet DetConstructor(@PolyDet int a) {
  }

  public static void f(@PolyDet int b) {
    @Det DetConstructor c = new DetConstructor(b);
  }
}

Error:

etConstructor.java:9: error: [assignment.type.incompatible] incompatible types in assignment.
    @Det DetConstructor c = new DetConstructor(b);
                            ^
  found   : @PolyDet DetConstructor
  required: @Det DetConstructor

NullPointerException on wildcard

The checker crashes when @PolyDet("use") is used with a wildcard.

import org.checkerframework.checker.determinism.qual.*;
import java.util.*;

public class PolyUseBug {
  public static void f(List<? extends @PolyDet("use") Object> a) {
  }
}

Error:

error: SourceChecker.typeProcess: unexpected Throwable (NullPointerException) while processing PolyUseBug.java
  Compilation unit: PolyUseBug.java
  Last visited tree at line 5 column 24:
    public static void f(List<? extends @PolyDet("use") Object> a) {
  Exception: java.lang.NullPointerException; Stack trace: org.checkerframework.checker.determinism.DeterminismVisitor.reportInvalidPolyDetUse(DeterminismVisitor.java:230)
  org.checkerframework.checker.determinism.DeterminismVisitor.isValidUse(DeterminismVisitor.java:99)
  org.checkerframework.common.basetype.BaseTypeValidator.visitDeclared(BaseTypeValidator.java:236)
  org.checkerframework.common.basetype.BaseTypeValidator.visitDeclared(BaseTypeValidator.java:38)
  org.checkerframework.framework.type.AnnotatedTypeMirror$AnnotatedDeclaredType.accept(AnnotatedTypeMirror.java:850)
  org.checkerframework.framework.type.visitor.AnnotatedTypeScanner.scan(AnnotatedTypeScanner.java:103)
  org.checkerframework.framework.type.visitor.AnnotatedTypeScanner.visitWildcard(AnnotatedTypeScanner.java:246)
  org.checkerframework.common.basetype.BaseTypeValidator.visitWildcard(BaseTypeValidator.java:458)
  org.checkerframework.common.basetype.BaseTypeValidator.visitWildcard(BaseTypeValidator.java:38)
  org.checkerframework.framework.type.AnnotatedTypeMirror$AnnotatedWildcardType.accept(AnnotatedTypeMirror.java:1892)
  org.checkerframework.framework.type.visitor.AnnotatedTypeScanner.scan(AnnotatedTypeScanner.java:103)
  org.checkerframework.common.basetype.BaseTypeValidator.visitDeclared(BaseTypeValidator.java:290)
  org.checkerframework.common.basetype.BaseTypeValidator.visitDeclared(BaseTypeValidator.java:38)
  org.checkerframework.framework.type.AnnotatedTypeMirror$AnnotatedDeclaredType.accept(AnnotatedTypeMirror.java:850)
  org.checkerframework.framework.type.visitor.AnnotatedTypeScanner.scan(AnnotatedTypeScanner.java:103)
  org.checkerframework.framework.type.visitor.AnnotatedTypeScanner.visit(AnnotatedTypeScanner.java:91)
  org.checkerframework.common.basetype.BaseTypeValidator.isValid(BaseTypeValidator.java:73)
  org.checkerframework.common.basetype.BaseTypeVisitor.validateType(BaseTypeVisitor.java:3531)
  org.checkerframework.common.basetype.BaseTypeVisitor.validateTypeOf(BaseTypeVisitor.java:3519)
  org.checkerframework.common.basetype.BaseTypeVisitor.visitVariable(BaseTypeVisitor.java:882)
  org.checkerframework.common.basetype.BaseTypeVisitor.visitVariable(BaseTypeVisitor.java:159)
  com.sun.tools.javac.tree.JCTree$JCVariableDecl.accept(JCTree.java:864)
  com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:68)
  org.checkerframework.framework.source.SourceVisitor.scan(SourceVisitor.java:91)
  org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:272)
  org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:159)
  com.sun.source.util.TreeScanner.scan(TreeScanner.java:91)
  com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:99)
  com.sun.source.util.TreeScanner.visitMethod(TreeScanner.java:141)
  org.checkerframework.framework.source.SourceVisitor.visitMethod(SourceVisitor.java:109)
  org.checkerframework.common.basetype.BaseTypeVisitor.visitMethod(BaseTypeVisitor.java:585)
  org.checkerframework.common.basetype.BaseTypeVisitor.visitMethod(BaseTypeVisitor.java:159)
  com.sun.tools.javac.tree.JCTree$JCMethodDecl.accept(JCTree.java:800)
  com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:68)
  org.checkerframework.framework.source.SourceVisitor.scan(SourceVisitor.java:91)
  org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:272)
  org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:159)
  com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:81)
  com.sun.source.util.TreeScanner.scan(TreeScanner.java:91)
  com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:99)
  com.sun.source.util.TreeScanner.visitClass(TreeScanner.java:133)
  org.checkerframework.framework.source.SourceVisitor.visitClass(SourceVisitor.java:97)
  org.checkerframework.common.basetype.BaseTypeVisitor.processClassTree(BaseTypeVisitor.java:350)
  org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:310)
  org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:159)
  com.sun.tools.javac.tree.JCTree$JCClassDecl.accept(JCTree.java:720)
  com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:50)
  org.checkerframework.framework.source.SourceVisitor.visit(SourceVisitor.java:85)
  org.checkerframework.framework.source.SourceChecker.typeProcess(SourceChecker.java:972)
  org.checkerframework.common.basetype.BaseTypeChecker.typeProcess(BaseTypeChecker.java:494)
  org.checkerframework.javacutil.AbstractTypeProcessor$AttributionTaskListener.finished(AbstractTypeProcessor.java:182)
  com.sun.tools.javac.api.ClientCodeWrapper$WrappedTaskListener.finished(ClientCodeWrapper.java:681)
  com.sun.tools.javac.api.MultiTaskListener.finished(MultiTaskListener.java:111)
  com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1342)
  com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1296)
  com.sun.tools.javac.main.JavaCompiler.compile2(JavaCompiler.java:901)
  com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:860)
  com.sun.tools.javac.main.Main.compile(Main.java:523)
  com.sun.tools.javac.main.Main.compile(Main.java:381)
  com.sun.tools.javac.main.Main.compile(Main.java:370)
  com.sun.tools.javac.main.Main.compile(Main.java:361)
  com.sun.tools.javac.Main.compile(Main.java:56)
  com.sun.tools.javac.Main.main(Main.java:42)
1 error

This doesn't occur when @PolyDet("use") is used regularly, or if @PolyDet is used in its place. Also, this error doesn't occur when an explicit type variable is used.

Exceptions can be tedious

Any time errors relating to Exceptions are printed, the determinism checker flags them as @NonDet. This makes code that uses Exceptions hard to work with. For example:

public class Exceptions {
    public int myParse(String num) {
        try {
            int n = Integer.parseInt(num);
            return n;
        } catch (NumberFormatException e) {
            System.out.println(e.toString());
            return 0;
        }
    }
}

This gives:

javac -processor DeterminismChecker Exceptions.java
Exceptions.java:7: error: [argument.type.incompatible] incompatible types in argument.
            System.out.println(e);
                               ^
  found   : @NonDet NumberFormatException
  required: @Det Object
1 error

One issue is that this could be deterministic (although I'm not sure how that could be found be the checker). Secondly, to suppress this warning, e must be cast to @Det some how. To do this requires creating an extra variable, or suppressing determinism for the whole method. These types of catch blocks often contain other printing, such as dumping parameters. Because parameters are usually @PolyDet this means the same treatment must be given to anything printed in catch blocks, which is very time consuming.

Variable arguments causes String.format to break

The String.format method uses a variable length argument list, which isn't handled correctly. This means that the format method requires a @Det argument sometimes when it should only require @PolyDet.

An simple example would be:

public class FormatExample {
    public static String itoa(int value) {
        return String.format("%s", value);
    }
}

which gives the error:

javac -processor DeterminismChecker FormatExample.java
FormatExample.java:3: error: [argument.type.incompatible] incompatible types in argument.
        return String.format("%s", value);
                                   ^
  found   : @PolyDet int
  required: @Det Object
1 error

I believe this argument should return a @PolyDet value and accept a @PolyDet value.

Variable arguments ordering affects required types.

When instantiating a variable arguments array parameter, passing a @Det parameter and then a @PolyDet parameter should be the same as passing @PolyDet and then @Det. Because they would both have one @PolyDet and one @Det argument, the least upper bound would be @PolyDet and a @PolyDet array should be passed to the method.

However, if the @Det argument is passed first, the second is required to be @Det and passing @PolyDet fails.

import org.checkerframework.checker.determinism.qual.*;

public class FormatParameters {
  public static String formatInts(@Det int i, @PolyDet int j) {
    return String.format("%i %i", i, j);
  }

  public static String formatInts2(@PolyDet int i, @Det int j) {
    return String.format("%i %i", i, j);
  }
}

FormatParameters.java:5: error: [argument.type.incompatible] incompatible types in argument.
    return String.format("%i %i", i, j);
                                     ^
  found   : @PolyDet int
  required: @Det Object

The first method causes an error but the second one does not. The only difference is the order of a @Det and @PolyDet argument being passed. These should probably be treated the same.

Construction of @Det HashSet allowed

It should be impossible for a @Det HashSet to exist because iteration is inherently non-deterministic. The following shows this:

import org.checkerframework.checker.determinism.qual.Det;
import java.util.*;

public class HashSetTest {
  public static void f() {
    @Det Set<String> s = new HashSet<String>();
    System.out.println(s.iterator().next());
  }
}

This code type-checks, but there should be an error on the first line of the method.

@PolyDet("up") not accepted by @PolyDet method

Methods that take arguments of type @PolyDet should accept any type from @NonDet to @Det as these will simply set what @PolyDet resolves to. When accessing the contents of an array, which is @PolyDet("up"), it is not possible to pass the result to a method that takes a @PolyDet argument.

Example:

import org.checkerframework.checker.determinism.qual.*;
import java.util.*;

public class ArrayAccess {
  public static void f(@PolyDet int a) {
  }

  public static void g(@PolyDet int @PolyDet [] arr) {
    f(arr[0]);
  }
}

Error:

ArrayAccess.java:9: error: [argument.type.incompatible] incompatible types in argument.
    f(arr[0]);
         ^
  found   : @PolyDet("up") int
  required: @PolyDet int

The error comes from passing this directly. @PolyDet("up") values from other sources don't have this problem and the following produces no error:

  public static void g(@PolyDet int @PolyDet [] arr) {
    @PolyDet("up") int first = arr[0];
    f(first);
  }

Incorrect treatment of Collections

This tokenize method splits a String into tokens. It should return @PolyDet array because this method would be deterministic if the input was deterministic and non-deterministic if it was not. However, there are two places where adding to an ArrayList says the argument is @NonDet when I think it should not be. I was unable to find a simpler case.

This error can be fixed by marking each part of the ArrayList as @NonDet including the type parameter, and this can be done for the return type as well. However, the method shouldn't always return @NonDet, it should depend on the input.

The file appears below:

  /**
   * Splits the argument string into an array of tokens (command-line flags and arguments),
   * respecting single and double quotes.
   *
   * <p>This method is only appropriate when the {@code String[]} version of the arguments is not
   * available &mdash; for example, for the {@code premain} method of a Java agent.
   *
   * @param args the command line to be tokenized
   * @return a string array analogous to the argument to {@code main}.
   */
  // TODO: should this throw some exceptions?
  public static String[] tokenize(String args) {

    // Split the args string on whitespace boundaries accounting for quoted
    // strings.
    args = args.trim();
    List<String> argList = new ArrayList<String>();
    String arg = "";
    char activeQuote = 0;
    for (int ii = 0; ii < args.length(); ii++) {
      char ch = args.charAt(ii);
      if ((ch == '\'') || (ch == '"')) {
        arg += ch;
        ii++;
        while ((ii < args.length()) && (args.charAt(ii) != ch)) {
          arg += args.charAt(ii++);
        }
        arg += ch;
      } else if (Character.isWhitespace(ch)) {
        // System.out.printf ("adding argument '%s'%n", arg);
        argList.add(arg);
        arg = "";
        while ((ii < args.length()) && Character.isWhitespace(args.charAt(ii))) {
          ii++;
        }
        if (ii < args.length()) {
          // Encountered a non-whitespace character.
          // Back up to process it on the next loop iteration.
          ii--;
        }
      } else { // must be part of current argument
        arg += ch;
      }
    }
    if (!arg.equals("")) {
      argList.add(arg);
    }

    String[] argsArray = argList.toArray(new String[argList.size()]);
    return argsArray;
  }

and the error is:

Baz.java:36: error: [argument.type.incompatible] incompatible types in argument.
        argList.add(arg);
                    ^
  found   : @NonDet String
  required: @Det String
Baz.java:51: error: [argument.type.incompatible] incompatible types in argument.
      argList.add(arg);
                  ^
  found   : @NonDet String
  required: @Det String

The full error is attached below:
Baz_errors.txt

@Det required for generic methods

In certain circumstances, @Det Object is required in a type parameter when it should be something else.
Example:

import org.checkerframework.checker.determinism.qual.*;
import java.util.*;

public class GenericMethods<T extends @NonDet Object> {

  public static <U extends @PolyDet("use") Object> U f(@PolyDet GenericMethods<U> h) {
    return null;
  }

  public static <U extends @PolyDet("use") Object> U g() {
    return f(new GenericMethods<U>());
  }
}

Error:

GenericMethods.java:11: error: [type.argument.type.incompatible] incompatible types in type argument.
    return f(new GenericMethods<U>());
            ^
  found   : U extends @PolyDet("use") Object
  required: @Det Object
GenericMethods.java:11: error: [argument.type.incompatible] incompatible types in argument.
    return f(new GenericMethods<U>());
             ^
  found   : @Det GenericMethods<U extends @PolyDet("use") Object>
  required: @Det GenericMethods<U extends @Det Object>

Using @NonDet or @Det as the upper bound of these type parameters results in different but valid errors.

Collection element subtyping rule applied to ".class" expressions and instanceof operator

The rule that the element type of a collection must be a subtype of the collection itself is applied to ".class" expressions, even though this doesn't affect behavior. Consider this class

import org.checkerframework.checker.determinism.qual.*;
import java.util.*;

public class CollectionTypes {

    public static void f() {
        Class<?> c = Collection.class;
    }
}

CollectionTypes.java:7: error: [invalid.upper.bound.on.type.argument] upper bound of type argument (@NonDet) must be a subtype of the collection type (@Det)
        Class<?> c = Collection.class;
                               ^

An expression like this represents a Java class, and doesn't affect behavior, so there shouldn't be an error. Also, there's no way to get around this error, it must be suppressed.

We get the same error with the instanceof operator.

        boolean b = (c instanceof Collection);

CollectionTypes.java:7: error: [invalid.upper.bound.on.type.argument] upper bound of type argument (@NonDet) must be a subtype of the collection type (@Det)
        boolean b = (c instanceof Collection);
                                  ^

Similarly, this shouldn't be an error because Collection is not being used to instantiate any real Object.

Allowing collections( or arrays) of type @NonDet with elements of type @OrderNonDet or @Det results in unsoundness

Currently the determinism checker allows collections of type @NonDet<@OrderNonDet> and @NonDet<@Det>. This can result in undesired side effects in the presence of aliasing. Consider the following example:

import java.util.ArrayList;
import org.checkerframework.checker.determinism.qual.*;

class TestAliasing {
    @NonDet ArrayList<@Det String> list1 = new ArrayList<>();
    void mutate(){}
    void test(@Det ArrayList<@Det String> list2,
            @NonDet int index,
            @Det String str) {
        list1 = list2;
        mutate();
        list1.add(index, str);
    }
}

Here, list1 and list2 are aliases. Since list2 is deterministic, the call list1.add(index, str) should be illegal. But the checker doesn't report any error here because list1 has the type @NonDet<@Det>. Note that in the absence of the call to mutate(), list1 gets type refined to the type of list2 and the checker flags an error. The call to mutate() (which is not side effect free) is therefore required to expose the unsoundness in this example.
One solution to avoid this unsound behavior is to disallow types @NonDet<@OrderNonDet> and @NonDet<@Det>. This will invalidate assignments like list1 = list2 in the above example. Moreover, we don't lose any behavior since the elements extracted from a @NonDet collection always have the type@NonDet.

Objects methods should be @PolyDet("up")

In the Object class, most methods are @PolyDet("up") such as equals and toString. This is because an Object can be a Collection, which has the potential to be @OrderNonDet. In the new annotations for the Objects class, the return types are @PolyDet rather than @PolyDet("up"). The following methods need attention

NullPointerException in LockChecker

The LockChecker throws a NullPointerException on this class:

import org.checkerframework.checker.lock.qual.*;

class LockTest {
    @GuardedBy("lock") LockTest() {}
}

Error:

error: SourceChecker.typeProcess: unexpected Throwable (NullPointerException) while processing LockTest.java
  Compilation unit: LockTest.java
  Last visited tree at line 4 column 5:
      @GuardedBy("lock") LockTest() {}
  Exception: java.lang.NullPointerException; Stack trace: org.checkerframework.framework.util.dependenttypes.DependentTypesHelper.checkType(DependentTypesHelper.java:588)
  org.checkerframework.framework.util.dependenttypes.DependentTypesHelper.checkMethod(DependentTypesHelper.java:671)
  org.checkerframework.common.basetype.BaseTypeVisitor.visitMethod(BaseTypeVisitor.java:562)
  org.checkerframework.checker.lock.LockVisitor.visitMethod(LockVisitor.java:213)
  org.checkerframework.checker.lock.LockVisitor.visitMethod(LockVisitor.java:77)
  com.sun.tools.javac.tree.JCTree$JCMethodDecl.accept(JCTree.java:800)
  com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:68)
  org.checkerframework.framework.source.SourceVisitor.scan(SourceVisitor.java:91)
  org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:272)
  org.checkerframework.common.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:159)
  com.sun.source.util.TreeScanner.scan(TreeScanner.java:91)
  com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:99)
  com.sun.source.util.TreeScanner.visitClass(TreeScanner.java:133)
  org.checkerframework.framework.source.SourceVisitor.visitClass(SourceVisitor.java:97)
  org.checkerframework.common.basetype.BaseTypeVisitor.processClassTree(BaseTypeVisitor.java:350)
  org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:310)
  org.checkerframework.common.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:159)
  com.sun.tools.javac.tree.JCTree$JCClassDecl.accept(JCTree.java:720)
  com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:50)
  org.checkerframework.framework.source.SourceVisitor.visit(SourceVisitor.java:85)
  org.checkerframework.framework.source.SourceChecker.typeProcess(SourceChecker.java:967)
  org.checkerframework.common.basetype.BaseTypeChecker.typeProcess(BaseTypeChecker.java:494)
  org.checkerframework.javacutil.AbstractTypeProcessor$AttributionTaskListener.finished(AbstractTypeProcessor.java:182)
  com.sun.tools.javac.api.ClientCodeWrapper$WrappedTaskListener.finished(ClientCodeWrapper.java:681)
  com.sun.tools.javac.api.MultiTaskListener.finished(MultiTaskListener.java:111)
  com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1342)
  com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1296)
  com.sun.tools.javac.main.JavaCompiler.compile2(JavaCompiler.java:901)
  com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:860)
  com.sun.tools.javac.main.Main.compile(Main.java:523)
  com.sun.tools.javac.main.Main.compile(Main.java:381)
  com.sun.tools.javac.main.Main.compile(Main.java:370)
  com.sun.tools.javac.main.Main.compile(Main.java:361)
  com.sun.tools.javac.Main.compile(Main.java:56)
  com.sun.tools.javac.Main.main(Main.java:42)

This only seems to be an issue with the LockChecker. The same does not occur with, for example, the DeterminismChecker's @PolyDet("use").

Objects.hash is not @NonDet

The hashCode method in Object is @NonDet. The Objects class has the hashCode and hash methods which wrap hashCode. These should be @NonDet as well. Consider the following class

import org.checkerframework.checker.determinism.qual.*;
import java.util.*;

public class HashTest {
    public static void f() {
        @Det int c = Objects.hashCode(new Object());
    }
}

This class type checks, even though the hash code of this Object will change between runs. It could be fixed by adding the Objects class to the annotated JDK.

Incorrect default for inner looping variable

There's an issue with what the default is for looping variables in foreach loops, but only in nested loops and under certain scenarios.

In the following class

public class NestedLoops {
  public static @PolyDet int @PolyDet [] makeArr(@PolyDet int n) {
    return new @PolyDet int @PolyDet [] { n };
  }

  public static void f(@Det int n) {
    for (int i : makeArr(n)) {
      for (int j : makeArr(i)) {
        @Det int m = j;
      }
    }
  }

  public static void f2(@Det int n) {
    for (int i : makeArr(n)) {
      for (@Det int j : makeArr(i)) {
        @Det int m = j;
      }
    }
  }
}

we get the error

NestedLoops.java:11: error: [assignment.type.incompatible] incompatible types in assignment.
        @Det int m = j;
                     ^
  found   : @NonDet int
  required: @Det int

This is odd for several reasons. First, there is no error in f2 where the inner looping variable is @Det, so no type rules are being broken, it's simply that the default here is @NonDet when it should be @Det. Secondly, this only happens with the inner loop, not the outer loop. Finally, I thought the issue might be with how @PolyDet is resolved for variables that were type refined to @Det. This isn't the case though, as changing all instances of @Det to @PolyDet in the above example still gives the same error. Also, when I try a similar piece of code in sequence without foreach loops, there's no error. This means the error is with the foreach loop itself.

Runtime reflection methods not annotated correctly

In Class.java in the JDK for the determinism checker, runtime reflection methods such as getFields and getMethods are annotated as returning @NonDet Object @NonDet [] where Field or Method is used instead of Object. However, I believe these should be @Det Object @OrderNonDet [], as what is in the collection that's returned is deterministic, but the order is not guaranteed.

This would mean that we could get deterministic results by sorting these arrays. For an example, see the ClassDeterministic class in the plume-util library.

t-rasmud / checker-framework Goto Github PK

checker-framework's People

Contributors

Stargazers

Watchers

Forkers

checker-framework's Issues

Example

Error

Example

Error

Recommend Projects

Recommend Topics

Recommend Org