roterdam / checker-framework Goto Github PK

The Nullness Checker lets a programmer specify the nullness of method
parameters.  But some routines have expectations for static variables as
well.  It would be nice to have a way to express those expectations -- and,
more importantly, to check them at call sites!

For instance, one might write

  @NonNullVariable("MyClass.displayFormat")
  void print() {
    ... use MyClass.displayFormat ...
  }

@NonNullVariable is a method annotation.  You might want to treat it as
both a pre- and post-condition, though for an @LazyNonNull variable, the
precondition implies the postcondition.  It would have to be non-null at
every call site.

For my current use case, supporting just fields of the current class is
sufficient.  Eventually, it would be nice to support more general
variables.

Stub files need to support:
1. Import statements on demand
2. Array suppport
3. package and non-type-qualifier annotations
4. Error recovery

The Nullness Checker issues no warnings for uses of unannotated libraries
where its methods returns null.

From Mike:


I speculate that maybe with NNEL as the default, that the Checker Framework
by default assumes all parameters and return values are non-null in
unannotated code.  This is an unfortunate default.

One idea for working around it would be to set the default to NNEL if there
is any evidence in the class of consideration of the nullness checker:
 * class was mentioned explicitly on the command line
 * import of any of its packages
 * use of any of its annotations or methods
 * use of @SuppressWarnings with any of its keys
If none of this evidence is present, the default would be "non-null except
return values are @Nullable and public fields are @PolyNull".

I'm not convinced this is a perfect solution, but it does seem to be an
improvement over the current situation.

These commands succeed:

  cd checkers
  ant -e -find build.xml all-tests

However, this fails:

  cd checkers/tests/src/tests/
  ant -e -find build.xml all-tests

The apparent problem is that paths are set relative to the directory from
which ant was invoked.

Section 15.1.1 "Generics (parametric polymorphism or type polymorphism)" of
the Checker Framework manual claims that it is posible to write this
annotation:

@DefaultQualifier(value="Nullable", locations={DefaultLocation.UPPER_BOUNDS})

It may be possible to write it, but no support for it is implemented yet.
This needs to be implemented.

In checkers/jdk/nullness/src/java/lang/Class.java, I would like to write
something like the following to indicate that if getSuperclass ever returns
non-null for a given receiver, it will always return non-null for the
receiver.

  public native @LazyNonNull Class<? super T> getSuperclass();

When I write this, I get

/home/mernst/research/types/checker-framework/checkers/jdk/nullness/src/java/lan
g/Class.java:27:
annotation type not applicable to this kind of declaration
  public native @LazyNonNull Class<? super T> getSuperclass();
                ^

More generally, there could be an annotation indicating that a given method
always returns the same value no matter how often it is called.  That is
stronger than the above, but would work for me, and may be more generally
useful.  One could use the term pure for this; I'm not sure if that is the
best terminology.

For background, the Daikon warning that makes me need this feature is:

daikon/config/Configuration.java:248: warning: dereference of possibly-null
reference type.getSuperclass()
               && type.getSuperclass().getName().equals("java.lang.Enum")) {
                                    ^

where the relevant code is

    } else if ((type.getSuperclass() != null)
               && type.getSuperclass().getName().equals("java.lang.Enum")) {

Or, is there some other way to solve the problem?

What steps will reproduce the problem?
1. cd demos/nonnull-interned-demo
2. ant check-demo
3. hg status

What is the expected output? What do you see instead?

All of the changes should be reverted.
However, one did not get reverted.
The output of the "hg status" command is:

% hg status
M demos/nonnull-interned-demo/junit/src/org/junit/Assert.java

The Checker Framework follows the steps of Java with regards to Array subtype 
covariant rules 
rather than the invariant parameterized type,  In other words, the Checker 
framework enforces 
the following condition (where < is subtype)

  @A A[] < @B B[]

iff

  A < B && @A < @B

However, this is unsafe.  Java make up for that using the Runtime checks, but 
the checker 
framework doesn't provide any.

Consider changing the subtype rules in Checker Framework so it would be 
invariant with respect 
to the annottion only, so `@A A[] < @B B[]` iff `A < B && A == B`.

However, this is quite limiting.  Both of these meanings are valid and 
required, whether in 
generics or array.  To illustrate, consider the following two cases:

1. Meant as co-variant:  Consider PrintStream.println(@Nullable Object 
@Nullable []).
Such method is read-only and should accept any object or any nullness type.  
Really, it should 
be declared as '<? extends @Nullable Object> @Nullable []` (invalid 
declaration).

The proposal would basically forbid any call of mutable objects array to 
PrintStream.println().

2. Meant as invariant:  Consider the simple case:
  @NonNull Object[] nonnullArray = ...
  @Nullable Object[] nullableArray = nonnullArray;
  nullableArray[0] = null;

Here the checker framework should prevent the assignment of nonnullArray to 
nullableArray.

There are no tests for these cherkers:
 * i18n
 * linear
 * regex
 * tainting

The Eclipse plug-in for the Checker Framework should be named that.
Currently, it has many names that include "jsr308" or "JSR 308".
These should be changed.

What steps will reproduce the problem?

class Test {
 static <F extends Object> void test1(Collection<F> collection) {
   collection.add(null);  // fails, as expected
 }
 static <F extends @Nullable Object> void test2(Collection<F>
collection) { 
   collection.add(null); // works, why?
 }
}


What is the expected output? What do you see instead?

I'd expect test2 would issue a warning because F can be eg @NonNull String,
and we'd be adding a null to a collection that doesn't accept nulls.


What version of the product are you using? On what operating system?

Linux, javac 1.7.0-jsr308-1.0.1


Please provide any additional information below.

The annotated libraries (stubs) contain unsightly package names.

For example, this:

  public static java.io.File createTempFile(java.lang.String a1, @Nullable
java.lang.String a2, @Nullable java.io.File a3) throws java.io.IOException

could instead be

  public static File createTempFile(String a1, @Nullable String a2,
@Nullable File a3) throws IOException

It would be good to fix this throughout, as part of the cleanup that is
verifying that they are complete.

Consider adding AssertNonNullIfTrue() to handle cases like:

  if (file.isDirectory()) {
    // file.list() is nonnull
  }

JSR 308 permits annotations to be written before a type parameter
declaration (including a wildcard).

The enhancement request is to interpret these as annotations on any
implicit type bounds.

Under this syntax proposal, this code:

     List<@Nullable T>
     Consumer<@Nullable ? super A>
     List<@Nullable ? super @NonNull Number>

would be interpreted as:

     List<T extends @Nullable Object>
     Consumer<? super A extends @Nullable Object>
     List<? super @NonNull Number extends @Nullable Object>

For code that intermixes classes that need different defaults, this syntax
is more compact.  The implementation will let us evaluate this proposal.

What steps will reproduce the problem?

Currently 'class MyClass<@Nullable T> { ... }' compiles but @Nullable has
no effect.


What is the expected output? What do you see instead?

I'd like this to be either 
- equivalent to 'class MyClass<T extends @Nullable Object>' (preferred), or
- rejected by the nullness checker

As it is, a syntax that most would intuitively suppose to work has no
effect, moreover, the problem is only noticed when you try to use the class.


What version of the product are you using? On what operating system?

Linux, javac 1.7.0-jsr308-1.0.1


Please provide any additional information below.

See the following two email threads for more info:
https://groups.google.com/group/checker-framework-discuss/browse_thread/thread/d
4f8c5d02cbc937?hl=en
https://groups.google.com/group/checker-framework-discuss/browse_thread/thread/7
ceecbaebbbccb3c?hl=en

Support nullness:collection-typeargs to avoid errors regarding using 
collections with nullable 
elements 'List<@Nullable Object>'.

Verify that @AssertNonNullIfTrue annotations are correct:  issue a warning
if they do not accurately describe the method they annotate.

If the nullness check condition result is known at compile time, emit an error 
for a redundant 
check.

Example:
  String s = "any value";
  if (s != null) {  // redundant check
  }

The Checker Framework doesn't parse intersection bound type annotations (e.g. ? 
extends @A 
Number & @B Cloneable).

What steps will reproduce the problem?

class Test {
  /*@PolyNull*/ String identity(/*@PolyNull*/ String str) { return str; }
  void test1() { identity(null); }
  void test2() { identity((/*@Nullable*/ String) null); }
}

What is the expected output? What do you see instead?

Expected: both test1 and test2 should compile cleanly.
Actual: test2 compiles, but test1 has a warning:

 incompatible types.
  void test1() { identity(null); }
                          ^
  found   : @Nullable <nulltype>
  required: @PolyNull String


What version of the product are you using? On what operating system?

1.0.3a

Please provide any additional information below.

What steps will reproduce the problem?

Run the checker on:

import java.util.Set;
import java.util.Arrays;

class AaTest {
  static <X> void test(Set<X>... args) { test2(Arrays.asList(args)); }
  static <X> void test2(Iterable<Set<X>> args) {}
}

What is the expected output? What do you see instead?

Expected: no warnings about @Raw
Actual:

incompatible types.
  static <X> void test(Set<X>... args) { test2(Arrays.asList(args)); }
                                                            ^
  found   : @NonRaw List<@NonRaw Set<@NonRaw X extends @Raw Object>>
  required: @NonRaw Iterable<@NonRaw Set<? extends @NonRaw Object>>


What version of the product are you using? On what operating system?

Linux, v1.0.3a

Please provide any additional information below.

In the Nullness Checker test suite, the @Ignore on testConditionalNullness
should be removed, and that test case made to work.

Currently, the flow-sensitive analysis gives results that are not correct
for multithreaded code.  For example, after testing a field against null,
it is not valid to assume that the field is non-null, even on the next
instruction, because another thread could have re-assigned it.

The feature request is to add a multithreaded mode.

Type refinement would be operational only in the following circumstances:
 * for local variables
 * for a variable that is @GuardedBy a lock that is held
 * un-assignable (e.g., final)

(There may be other cases that I have overlooked.)

The visitor may not have access to some symbol and annotation information if 
they are available in 
a different class.  The symbol information availability depend on the order in 
which they are 
specified.

tests/nullness/ImplementInterface.java tests this behavior.

Flow only infers types of the raw location, but not generic types or
arrays.  While fully supporting generic types and arrays are planned in
"mid-to-long" future, it might be beneficial to support array and
collection accesses:

  if (array[i] != null) {
    array[i].toString();
  }

Or

  if (list.get(0) != null) {
    list.get(0).toString();
  }

Sound analysis is a bit difficult to achieve, as the following checks need
to be enforced:
1. The index variable doesn't get modified or re-assigned (might even
require it to be a final)
2. In case of array, the array doesn't modified either by modifying the
array with that particular index (e.g. array[i] = null) or by escaping
(e.g. Arrays.sort(array))
3. In the case, collection, the same as true as before, however,
modifications are tougher to detect (e.g. list.insertAtFirst(...) ->
changes order of list)

As a comprimize, it makes sense to require the the use be in the first
statement after the assertion/check.

  if (array[i] != null) {
    array[i].toString();   // valid
    array[i].toString();   // invalid now!
  }

The heuristics used for Collection.toArray(T[]) are unsafe.  Please document 
and improve it so it 
would only special case the following:

1. empty array initializer argument e.g. list.toArray(new String[] { })
2. new array with size 0 e.g. list.toArray(new String[0]);
3. new array of the collection size e.g. list.toArray(new String[list.size()]);

Try running ant on the Checker Framework tests.  The output doesn't tell
you what test failed, only the line number at which it failed.

Here is an example, when running "ant nullness-tests":

nullness-tests:

-run-tests:
Running tests.NullnessTest
2 out of 2 expected diagnostics were found.

1 unexpected diagnostic was found:
:28: (type.incompatible)
)
Tests run: 46, Failures: 1, Errors: 1, Time elapsed: 19.078 sec

BUILD FAILED

Flow should take advantage of contextual scoping and conditional branching.  
The interning checker for example should type-check the following method 
cleanly:

    @Interned Object object(Object s) {
      if (s == null) return s; else return null;
    }

Currently the code for this is specific to NullnessFlow.  It should be re-
factored out so it is accessible from other checkers as well.

Checker Framework project uses 1.0.2 javaparser; the latest version is 1.0.7.

What steps will reproduce the problem?

Run the nullness checker, v1.0.3a, on

import java.util.Set;
import java.util.Arrays;

class AaTest {
  static <X> void test(Set<? super X>... args) { test2(Arrays.asList(args)); }
  static <X> void test2(Iterable<Set<? super X>> args) {}
}

What is the expected output? What do you see instead?

Expected: compiler should not crash.
Actual:

java.lang.Error: NullnessSubchecker processor threw unexpected exception
when processing ...
        at checkers.source.SourceChecker.typeProcess(SourceChecker.java:226)
        at checkers.util.AggregateChecker.typeProcess(AggregateChecker.java:59)
        at
com.sun.source.util.AbstractTypeProcessor$AttributionTaskListener.finished(Abstr
actTypeProcessor.java:206)
        at
com.sun.source.util.AbstractTypeProcessor$TaskListeners.finished(AbstractTypePro
cessor.java:236)
        at
com.sun.source.util.AbstractTypeProcessor$TaskListeners.finished(AbstractTypePro
cessor.java:236)
        at com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1201)
        at com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1160)
        at
com.sun.tools.javac.main.JavaCompiler.compile2(JavaCompiler.java:851)
        at com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:810)
        at com.sun.tools.javac.main.Main.compile(Main.java:400)
        at com.sun.tools.javac.main.Main.compile(Main.java:318)
        at com.sun.tools.javac.main.Main.compile(Main.java:309)
        at com.sun.tools.javac.Main.compile(Main.java:82)
        at com.sun.tools.javac.Main.main(Main.java:67)
Caused by: java.lang.IllegalArgumentException: unrecognized qualifier: null
        at
checkers.util.GraphQualifierHierarchy.isSubtype(GraphQualifierHierarchy.java:221
)
        at
checkers.types.QualifierHierarchy.isSubtype(QualifierHierarchy.java:78)
        at checkers.types.TypeHierarchy.isSubtypeImpl(TypeHierarchy.java:112)
        at checkers.types.TypeHierarchy.isSubtype(TypeHierarchy.java:66)
        at
checkers.types.TypeHierarchy.isSubtypeAsTypeArgument(TypeHierarchy.java:176)
        at
checkers.types.TypeHierarchy.isSubtypeTypeArguments(TypeHierarchy.java:151)
        at checkers.types.TypeHierarchy.isSubtypeImpl(TypeHierarchy.java:120)
        at
checkers.types.TypeHierarchy.isSubtypeAsArrayComponent(TypeHierarchy.java:218)
        at checkers.types.TypeHierarchy.isSubtypeImpl(TypeHierarchy.java:118)
        at checkers.types.TypeHierarchy.isSubtype(TypeHierarchy.java:66)
        at
checkers.basetype.BaseTypeChecker.isSubtype(BaseTypeChecker.java:322)
        at
checkers.basetype.BaseTypeVisitor.commonAssignmentCheck(BaseTypeVisitor.java:552
)
        at
checkers.basetype.BaseTypeVisitor.commonAssignmentCheck(BaseTypeVisitor.java:535
)
        at
checkers.basetype.BaseTypeVisitor.checkArguments(BaseTypeVisitor.java:700)
        at
checkers.basetype.BaseTypeVisitor.visitMethodInvocation(BaseTypeVisitor.java:287
)
        at
com.sun.tools.javac.tree.JCTree$JCMethodInvocation.accept(JCTree.java:1311)
        at com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:67)
        at checkers.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:117)
        at com.sun.source.util.TreeScanner.scan(TreeScanner.java:90)
        at com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:98)
        at
com.sun.source.util.TreeScanner.visitMethodInvocation(TreeScanner.java:267)
        at
checkers.basetype.BaseTypeVisitor.visitMethodInvocation(BaseTypeVisitor.java:293
)
        at
com.sun.tools.javac.tree.JCTree$JCMethodInvocation.accept(JCTree.java:1311)
        at com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:67)
        at checkers.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:117)
        at
com.sun.source.util.TreeScanner.visitExpressionStatement(TreeScanner.java:239)
        at
com.sun.tools.javac.tree.JCTree$JCExpressionStatement.accept(JCTree.java:1151)
        at com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:67)
        at checkers.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:117)
        at com.sun.source.util.TreeScanner.scan(TreeScanner.java:90)
        at com.sun.source.util.TreeScanner.visitBlock(TreeScanner.java:159)
        at com.sun.tools.javac.tree.JCTree$JCBlock.accept(JCTree.java:777)
        at com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:67)
        at checkers.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:117)
        at com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:80)
        at com.sun.source.util.TreeScanner.visitMethod(TreeScanner.java:143)
        at
checkers.basetype.BaseTypeVisitor.visitMethod(BaseTypeVisitor.java:192)
        at
checkers.nullness.NullnessVisitor.visitMethod(NullnessVisitor.java:226)
        at
checkers.nullness.NullnessVisitor.visitMethod(NullnessVisitor.java:40)
        at com.sun.tools.javac.tree.JCTree$JCMethodDecl.accept(JCTree.java:677)
        at com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:67)
        at checkers.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:117)
        at com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:80)
        at com.sun.source.util.TreeScanner.scan(TreeScanner.java:90)
        at com.sun.source.util.TreeScanner.scanAndReduce(TreeScanner.java:98)
        at com.sun.source.util.TreeScanner.visitClass(TreeScanner.java:132)
        at
checkers.basetype.BaseTypeVisitor.visitClass(BaseTypeVisitor.java:134)
        at com.sun.tools.javac.tree.JCTree$JCClassDecl.accept(JCTree.java:601)
        at com.sun.source.util.TreePathScanner.scan(TreePathScanner.java:49)
        at checkers.source.SourceChecker.typeProcess(SourceChecker.java:220)
        ... 13 more
An exception has occurred in the compiler (1.7.0-jsr308-1.0.3a). Please
report this bug so we can fix it.  For instructions, see
http://types.cs.washington.edu/checker-framework/current/README-jsr308.html#repo
rting-bugs
.  Thank you.

What version of the product are you using? On what operating system?

Linux, 1.7.0-jsr308-1.0.3a).

Please provide any additional information below.

This seems to be a regression, the problem did not occur in 1.0.2 I think.

What steps will reproduce the problem?

class AaTest {
  Object nullObject;
  public Object getNull() { return nullObject; }
}

What is the expected output? What do you see instead?

Expected: a warning somewhere (getNull() returns 'null')
Actual: no warnings

What version of the product are you using? On what operating system?

Linux, checker v1.0.3a

Please provide any additional information below.

What steps will reproduce the problem?

class MyClass<T extends /*@Nullable*/ Object> {}

/*@DefaultQualifier(value="Nullable", 
locations=DefaultLocation.UPPER_BOUNDS)*/
class Test {
  void test() { ignore(newInstance()); }
  static void ignore(MyClass<?>... consumer) {}
  static <T> MyClass<T> newInstance() { return new MyClass<T>(); }
}

What is the expected output? What do you see instead?

Expected: compile cleanly.  Actual:

 incompatible types.
  void test() { ignore(newInstance()); }
                                  ^
  found   : @NonNull MyClass<? extends @Nullable Object>
  required: @NonNull MyClass<? extends @NonNull Object>


What version of the product are you using? On what operating system?

1.0.4

Please provide any additional information below.

The javaparser subproject of the Checker Framework was branched off
http://code.google.com/p/javaparser/, version 1.0.2.  javaparser is now up
to version 1.0.7.

The Checker Framework's version needs to be updated to the latest uptream
version.  Then, our changes need to be offered to the upstream maintainer.
Ideally, the Checker Framework won't need its own custom version.

With the following stub file

package java.lang.reflect;

class Method {
  @Nullable Object invoke(@Nullable Object obj, @Nullable Object... args);
}

a call

method.invoke(null, new Object()) 

produces 

  method.invoke(null,
                                                             ^
  found   : @Nullable <nulltype>
  required: @NonNull Object


It seems that the Method.invoke does match the stub definition.  The
following change from Object... to Object[] in the stub file makes
everything work ok:

class Method {
  @Nullable Object invoke(@Nullable Object obj, @Nullable Object[] args);
}


What version of the product are you using? On what operating system?

checker framework 1.0.1, linux

Each annotation defined in the Checker Framework should have a proper
@Target meta-annotation.

In some cases, such as checkers.regex.quals.Regex, the @Target
meta-annotation is missing.
In other cases, such as checkers.nullness.quals,NonNull, the @Target
meta-annotation is missing because an incorrect one was commented out.

What steps will reproduce the problem?

class AaTest {
  <A extends /*@Nullable*/ Object> void test() {
    A a = null;
  }
}

What is the expected output? What do you see instead?

Expected: compile cleanly.
Actual:
incompatible types.
    A a = null;
          ^
  found   : @Nullable <nulltype>
  required: @Nullable A extends @Nullable Object


What version of the product are you using? On what operating system?

Linux, checker v1.0.3a

Please provide any additional information below.

What steps will reproduce the problem?

interface Consumer<T> {
  void consume(T object);
}

class AaTest {
  Consumer<String> testCast(Consumer<Object> consumer) {
    return cast(consumer);
  }

  private static <T> Consumer<T> cast(final Consumer<? super T> consumer) {
    return new Consumer<T>() {
      @Override public void consume(T object) {
        consumer.consume(object);
      }
    };
  }
}

What is the expected output? What do you see instead?

Expected to compile cleanly.  Actually, I get the following error:

incompatible types.
    return cast(consumer);
               ^
  found   : @NonRaw Consumer<@Raw String>
  required: @NonRaw Consumer<@NonRaw String>



What version of the product are you using? On what operating system?

1.0.4

Please provide any additional information below.

What steps will reproduce the problem?

interface Consumer<A extends /*@Nullable*/ Object> {
  public void consume(A object);
}

class Utils {
  public static <A extends /*@Nullable*/ Object>
      Consumer<A> cast(final Consumer<? super A> consumer) {
    return new Consumer<A>() {
      @Override public void consume(A object) {
        consumer.consume(object);   // error 1: see issue 28 for details
      }
    };
  }
  public static <A extends /*@Nullable*/ Object> Consumer<A> 
      getConsumer() {
    // null for simplicity, but could be anything
    Consumer</*@Nullable*/ Object> nullConsumer = null;  
    return cast(nullConsumer);  // error2: this issue
  }
}

What is the expected output? What do you see instead?

Ignore error 1 (see issue 28 instead).
Error 2: I get

 incompatible types.
   return cast(nullConsumer);
              ^
 found   : @NonRaw Consumer<@Raw A extends @Raw Object>
 required: @NonRaw Consumer<@NonRaw A extends @NonRaw Object>

I don't understand what @Raw/@NonRaw has to do with anything here.
I'd expect this code to compile cleanly.

What version of the product are you using? On what operating system?

Linux, javac 1.7.0-jsr308-1.0.1


Please provide any additional information below.

Flow shouldn't override assignment info when analyzing conditional statements:

  String s = "m";
  if (s != null) { } else { }
  s.toString(); // valid

OpenJDK now has support for new features from Project Coin
(http://openjdk.java.net/projects/coin/), the module system, and possibly
other features.  The Checker Framework and the checkers in it should be
updated to handle the new language features.

It would be helpful to add an AssertNonNullIfFalse annotation, similar to
AssertNonNullIfTrue.

What steps will reproduce the problem?

import java.util.List;

class AaTest<A extends /*@Nullable*/ Object> {
  void test(List<? extends A> list) { test2(list.get(0)); }
  void test2(A x) {};
}

What is the expected output? What do you see instead?

Expected: compile cleanly.
Actual:
 incompatible types.
  void test(List<? extends A> list) { test2(list.get(0)); }
                                                    ^
  found   : ? extends @Nullable A extends @Nullable Object
  required: @Nullable A extends @Nullable Object


What version of the product are you using? On what operating system?

Linux, checker v1.0.3a

Please provide any additional information below.

Seems a regression, I don't think this problem existed in previous versions.

When running the IGJChecker on String.java, it throws an
IllegalArgumentException.  The output from the compiler is saved in
"output.txt"

What steps will reproduce the problem?
1.Download the files into one folder
2. type `make test1`

What is the expected output? What do you see instead?

When processing String.java, the IGJChecker throws an
IllegalArgumenException, the output of which is in output.txt

Please use labels and text to provide additional information.

If all of the bodies are removed and replaced with "throw new
RuntimeException()", the processor runs to completion.  To test this, run
`make test2`

It might be nice to have a @Poly or @PolyAll annotation, that indicates
that the given type should be considered as having every annotation that is
meta-annotated with @PolymorphicQualifier.

For example, the annotation

  public @Poly Object identity(@Poly Object x) { return x; }

would be interpreted as

  public
  @PolyInterned @PolyNull @PolyRaw @PolyRead @PolyTainted Object
  identity(@PolyInterned @PolyNull @PolyRaw @PolyRead @PolyTainted Object x) {
    return x;
  }

The advantage is that these annotations can often be shared.  This will
reduce the effort (& confusion) for people who are writing a new checker or
annotating a new library.

One disadvantage is that it will probably be necessary to have a way to
read multiple annotated libraries -- one with the @Poly annotation, and
then the checker-specific one.  Actually, isn't this already necessary, for
instance when running multiple checkers in a single compiler invocation?
If we merge all annotations into the .jar files, then this is easily
handled.

Another disadvantage is that the full type will not be immediately apparent
by reading either of the libraries.

I'm not sure how often this will be useful.  The Nullness type system uses
very few @PolyNull annotations (just 5 at present).  I don't know whether a
lot of other ones are missing.

The Checker Framework currently doesn't support annotated Throwable (e.g. 
annotations in catch 
clauses, throw clauses, or declared throwable of a method).

Once done, enable tests/basic/ThrowCatch tests.

Convert all skeleton jdks into jdk.jar files.

Stopping bugs:
 - Script generating jdk files ignores inner files for now.

AssertNonNullIfTrue can only specify method invocations and fields, it 
should be extended so it can handle method arguments as well, so it could 
handle calls to the following method:

    @AssertNonNullIfTrue({"a1", "a2"})
    static boolean areAllNonNull(Object a1, Object a2) {
        return a1 != null && a2 != null;
    }

The problem here is that the parameter names may not be available once 
the class is compiled without debugging info.  So we would need to resort 
to an index expression, possibly with an Java-invalid prefix letter, e.g. # $.

Once done, enable AssertParameterNullness test case.
AssertParameterNullness).

I’ve another minor bug report fort he nullness checker (Version 0.9.7, 12 
Aug 2009):

The skeleton java.lang.IllegalStateException  doesn’t import the used 
Nullness annotation and therefore doesn’t compile.
Adding “import checkers.nullness.quals.*;” fixes the problem. 

What steps will reproduce the problem?
Execute the following commands:
mkdir -p ~/tmp
cd ~/tmp
svn checkout http://google-collections.googlecode.com/svn/trunk/
google-collections-read-only
cd src/com/google/common/collect
javac -processor checkers.nullness.NullnessChecker Maps.java

What is the expected output? What do you see instead?
I expect the Nullness Checker to produce warnings.
Instead, it crashes.  See attached file.

The problem goes away if you comment out these two methods:
filterValues on line 886
filterEntries on line 923

Using checker framework 0.9.9.

following class nullness.Test16:
<class>
package nullness;

import java.util.*;
import javax.swing.*;
public final class Test16 {

  public static void main(String[] args) {
     List<Object> vals = new ArrayList<Object>();
     IntegerValue v1 = new IntegerValue();
     BooleanValue v2 = new BooleanValue();
     List<? extends JComponent> li = Arrays.asList(v1,v2);
     for(JComponent ci : li)
     {
        System.out.println("\t"+ci.getClass().getName());
     }
     System.out.println("?");
  }

  static class IntegerValue extends JTextField {  }
  static class BooleanValue extends JCheckBox {  }
}
</class>

Causes both IGJ and Javari checkers to fail:

java.lang.Error: IGJ processor threw unexpected exception when processing 
Test16.java
    at checkers.source.SourceChecker.typeProcess
(SourceChecker.java:228)
    at 
com.sun.source.util.AbstractTypeProcessor$AttributionTaskListener.finished
(AbstractTypeProcessor.java:206)
    at com.sun.source.util.AbstractTypeProcessor$TaskListeners.finished
(AbstractTypeProcessor.java:236)
    at com.sun.source.util.AbstractTypeProcessor$TaskListeners.finished
(AbstractTypeProcessor.java:236)
    at com.sun.source.util.AbstractTypeProcessor$TaskListeners.finished
(AbstractTypeProcessor.java:236)
    at com.sun.source.util.AbstractTypeProcessor$TaskListeners.finished
(AbstractTypeProcessor.java:236)
    at com.sun.source.util.AbstractTypeProcessor$TaskListeners.finished
(AbstractTypeProcessor.java:236)
    at com.sun.source.util.AbstractTypeProcessor$TaskListeners.finished
(AbstractTypeProcessor.java:236)
    at com.sun.source.util.AbstractTypeProcessor$TaskListeners.finished
(AbstractTypeProcessor.java:236)
    at com.sun.tools.javac.main.JavaCompiler.flow
(JavaCompiler.java:1201)
    at com.sun.tools.javac.main.JavaCompiler.flow
(JavaCompiler.java:1160)
    at com.sun.tools.javac.main.JavaCompiler.compile2
(JavaCompiler.java:851)
    at com.sun.tools.javac.main.JavaCompiler.compile
(JavaCompiler.java:810)
    at com.sun.tools.javac.main.Main.compile(Main.java:400)
    at com.sun.tools.javac.main.Main.compile(Main.java:318)
    at com.sun.tools.javac.main.Main.compile(Main.java:309)
    at com.sun.tools.javac.Main.compile(Main.java:82)
    at com.sun.tools.javac.Main.main(Main.java:67)
Caused by: java.lang.NullPointerException
    at 
checkers.igj.IGJAnnotatedTypeFactory$ImmutabilityTemplateCollector.visitDec
lared(IGJAnnotatedTypeFactory.java:579)
    at 
checkers.igj.IGJAnnotatedTypeFactory$ImmutabilityTemplateCollector.visitDec
lared(IGJAnnotatedTypeFactory.java:500)
    at checkers.types.AnnotatedTypeMirror$AnnotatedDeclaredType.accept
(AnnotatedTypeMirror.java:518)
    at checkers.types.visitors.SimpleAnnotatedTypeVisitor.visit
(SimpleAnnotatedTypeVisitor.java:55)
    at 
checkers.igj.IGJAnnotatedTypeFactory$ImmutabilityTemplateCollector.visit
(IGJAnnotatedTypeFactory.java:533)
    at checkers.igj.IGJAnnotatedTypeFactory.methodFromUse
(IGJAnnotatedTypeFactory.java:407)
    at 
checkers.types.TypeFromTree$TypeFromExpression.visitMethodInvocation
(TypeFromTree.java:203)
    at 
checkers.types.TypeFromTree$TypeFromExpression.visitMethodInvocation
(TypeFromTree.java:59)
    at com.sun.tools.javac.tree.JCTree$JCMethodInvocation.accept
(JCTree.java:1311)
    at com.sun.source.util.SimpleTreeVisitor.visit
(SimpleTreeVisitor.java:52)
    at checkers.types.AnnotatedTypeFactory.fromTreeWithVisitor
(AnnotatedTypeFactory.java:381)
    at checkers.types.AnnotatedTypeFactory.fromExpression
(AnnotatedTypeFactory.java:318)
    at checkers.types.AnnotatedTypeFactory.getAnnotatedType
(AnnotatedTypeFactory.java:197)
    at checkers.types.AnnotatedTypeFactory.getAnnotatedType
(AnnotatedTypeFactory.java:812)
    at checkers.flow.Flow.propagate(Flow.java:328)
    at checkers.flow.Flow.visitVariable(Flow.java:620)
    at checkers.flow.Flow.visitVariable(Flow.java:55)
    at com.sun.tools.javac.tree.JCTree$JCVariableDecl.accept
(JCTree.java:723)
    at com.sun.source.util.TreePathScanner.scan
(TreePathScanner.java:67)
    at checkers.flow.Flow.scan(Flow.java:206)
    at checkers.flow.Flow.scan(Flow.java:55)
    at com.sun.source.util.TreeScanner.scanAndReduce
(TreeScanner.java:80)
    at com.sun.source.util.TreeScanner.scan(TreeScanner.java:90)
    at com.sun.source.util.TreeScanner.visitBlock(TreeScanner.java:159)
    at checkers.flow.Flow.visitBlock(Flow.java:911)
    at checkers.flow.Flow.visitBlock(Flow.java:55)
    at com.sun.tools.javac.tree.JCTree$JCBlock.accept(JCTree.java:777)
    at com.sun.source.util.TreePathScanner.scan
(TreePathScanner.java:67)
    at checkers.flow.Flow.scan(Flow.java:206)
    at checkers.flow.Flow.scan(Flow.java:55)
    at com.sun.source.util.TreeScanner.scanAndReduce
(TreeScanner.java:80)
    at com.sun.source.util.TreeScanner.visitMethod
(TreeScanner.java:143)
    at checkers.flow.Flow.visitMethod(Flow.java:926)
    at checkers.flow.Flow.visitMethod(Flow.java:55)
    at com.sun.tools.javac.tree.JCTree$JCMethodDecl.accept
(JCTree.java:677)
    at com.sun.source.util.TreePathScanner.scan
(TreePathScanner.java:67)
    at checkers.flow.Flow.scan(Flow.java:206)
    at checkers.flow.Flow.visitClass(Flow.java:564)
    at checkers.flow.Flow.visitClass(Flow.java:55)
    at com.sun.tools.javac.tree.JCTree$JCClassDecl.accept
(JCTree.java:601)
    at com.sun.source.util.TreePathScanner.scan
(TreePathScanner.java:49)
    at checkers.flow.Flow.scan(Flow.java:203)
    at checkers.types.BasicAnnotatedTypeFactory.annotateImplicit
(BasicAnnotatedTypeFactory.java:165)
    at checkers.types.AnnotatedTypeFactory.getAnnotatedType
(AnnotatedTypeFactory.java:201)
    at checkers.types.AnnotatedTypeFactory.getAnnotatedType
(AnnotatedTypeFactory.java:783)
    at checkers.basetype.BaseTypeVisitor.visitClass
(BaseTypeVisitor.java:127)
    at com.sun.tools.javac.tree.JCTree$JCClassDecl.accept
(JCTree.java:601)
    at com.sun.source.util.TreePathScanner.scan
(TreePathScanner.java:49)
    at checkers.source.SourceChecker.typeProcess
(SourceChecker.java:222)
    ... 17 more
An exception has occurred in the compiler (1.7.0-jsr308-0.9.9). Please 
report this bug so we can fix it.  For instructions, see 
http://types.cs.washington.edu/checker-framework/current/README-
jsr308.html#reporting-bugs .  Thank you.
java.lang.Error: IGJ processor threw unexpected exception when processing 
Test16.java
    at checkers.source.SourceChecker.typeProcess
(SourceChecker.java:228)
    at 
com.sun.source.util.AbstractTypeProcessor$AttributionTaskListener.finished
(AbstractTypeProcessor.java:206)
    at com.sun.source.util.AbstractTypeProcessor$TaskListeners.finished
(AbstractTypeProcessor.java:236)
    at com.sun.source.util.AbstractTypeProcessor$TaskListeners.finished
(AbstractTypeProcessor.java:236)
    at com.sun.source.util.AbstractTypeProcessor$TaskListeners.finished
(AbstractTypeProcessor.java:236)
    at com.sun.source.util.AbstractTypeProcessor$TaskListeners.finished
(AbstractTypeProcessor.java:236)
    at com.sun.source.util.AbstractTypeProcessor$TaskListeners.finished
(AbstractTypeProcessor.java:236)
    at com.sun.source.util.AbstractTypeProcessor$TaskListeners.finished
(AbstractTypeProcessor.java:236)
    at com.sun.source.util.AbstractTypeProcessor$TaskListeners.finished
(AbstractTypeProcessor.java:236)
    at com.sun.tools.javac.main.JavaCompiler.flow
(JavaCompiler.java:1201)
    at com.sun.tools.javac.main.JavaCompiler.flow
(JavaCompiler.java:1160)
    at com.sun.tools.javac.main.JavaCompiler.compile2
(JavaCompiler.java:851)
    at com.sun.tools.javac.main.JavaCompiler.compile
(JavaCompiler.java:810)
    at com.sun.tools.javac.main.Main.compile(Main.java:400)
    at com.sun.tools.javac.main.Main.compile(Main.java:318)
    at com.sun.tools.javac.main.Main.compile(Main.java:309)
    at com.sun.tools.javac.Main.compile(Main.java:82)
    at com.sun.tools.javac.Main.main(Main.java:67)
Caused by: java.lang.NullPointerException
    at 
checkers.igj.IGJAnnotatedTypeFactory$ImmutabilityTemplateCollector.visitDec
lared(IGJAnnotatedTypeFactory.java:579)
    at 
checkers.igj.IGJAnnotatedTypeFactory$ImmutabilityTemplateCollector.visitDec
lared(IGJAnnotatedTypeFactory.java:500)
    at checkers.types.AnnotatedTypeMirror$AnnotatedDeclaredType.accept
(AnnotatedTypeMirror.java:518)
    at checkers.types.visitors.SimpleAnnotatedTypeVisitor.visit
(SimpleAnnotatedTypeVisitor.java:55)
    at 
checkers.igj.IGJAnnotatedTypeFactory$ImmutabilityTemplateCollector.visit
(IGJAnnotatedTypeFactory.java:533)
    at checkers.igj.IGJAnnotatedTypeFactory.methodFromUse
(IGJAnnotatedTypeFactory.java:407)
    at 
checkers.types.TypeFromTree$TypeFromExpression.visitMethodInvocation
(TypeFromTree.java:203)
    at 
checkers.types.TypeFromTree$TypeFromExpression.visitMethodInvocation
(TypeFromTree.java:59)
    at com.sun.tools.javac.tree.JCTree$JCMethodInvocation.accept
(JCTree.java:1311)
    at com.sun.source.util.SimpleTreeVisitor.visit
(SimpleTreeVisitor.java:52)
    at checkers.types.AnnotatedTypeFactory.fromTreeWithVisitor
(AnnotatedTypeFactory.java:381)
    at checkers.types.AnnotatedTypeFactory.fromExpression
(AnnotatedTypeFactory.java:318)
    at checkers.types.AnnotatedTypeFactory.getAnnotatedType
(AnnotatedTypeFactory.java:197)
    at checkers.types.AnnotatedTypeFactory.getAnnotatedType
(AnnotatedTypeFactory.java:812)
    at checkers.flow.Flow.propagate(Flow.java:328)
    at checkers.flow.Flow.visitVariable(Flow.java:620)
    at checkers.flow.Flow.visitVariable(Flow.java:55)
    at com.sun.tools.javac.tree.JCTree$JCVariableDecl.accept
(JCTree.java:723)
    at com.sun.source.util.TreePathScanner.scan
(TreePathScanner.java:67)
    at checkers.flow.Flow.scan(Flow.java:206)
    at checkers.flow.Flow.scan(Flow.java:55)
    at com.sun.source.util.TreeScanner.scanAndReduce
(TreeScanner.java:80)
    at com.sun.source.util.TreeScanner.scan(TreeScanner.java:90)
    at com.sun.source.util.TreeScanner.visitBlock(TreeScanner.java:159)
    at checkers.flow.Flow.visitBlock(Flow.java:911)
    at checkers.flow.Flow.visitBlock(Flow.java:55)
    at com.sun.tools.javac.tree.JCTree$JCBlock.accept(JCTree.java:777)
    at com.sun.source.util.TreePathScanner.scan
(TreePathScanner.java:67)
    at checkers.flow.Flow.scan(Flow.java:206)
    at checkers.flow.Flow.scan(Flow.java:55)
    at com.sun.source.util.TreeScanner.scanAndReduce
(TreeScanner.java:80)
    at com.sun.source.util.TreeScanner.visitMethod
(TreeScanner.java:143)
    at checkers.flow.Flow.visitMethod(Flow.java:926)
    at checkers.flow.Flow.visitMethod(Flow.java:55)
    at com.sun.tools.javac.tree.JCTree$JCMethodDecl.accept
(JCTree.java:677)
    at com.sun.source.util.TreePathScanner.scan
(TreePathScanner.java:67)
    at checkers.flow.Flow.scan(Flow.java:206)
    at checkers.flow.Flow.visitClass(Flow.java:564)
    at checkers.flow.Flow.visitClass(Flow.java:55)
    at com.sun.tools.javac.tree.JCTree$JCClassDecl.accept
(JCTree.java:601)
    at com.sun.source.util.TreePathScanner.scan
(TreePathScanner.java:49)
    at checkers.flow.Flow.scan(Flow.java:203)
    at checkers.types.BasicAnnotatedTypeFactory.annotateImplicit
(BasicAnnotatedTypeFactory.java:165)
    at checkers.types.AnnotatedTypeFactory.getAnnotatedType
(AnnotatedTypeFactory.java:201)
    at checkers.types.AnnotatedTypeFactory.getAnnotatedType
(AnnotatedTypeFactory.java:783)
    at checkers.basetype.BaseTypeVisitor.visitClass
(BaseTypeVisitor.java:127)
    at com.sun.tools.javac.tree.JCTree$JCClassDecl.accept
(JCTree.java:601)
    at com.sun.source.util.TreePathScanner.scan
(TreePathScanner.java:49)
    at checkers.source.SourceChecker.typeProcess
(SourceChecker.java:222)
    ... 17 more
INTERNAL COMPILATION ERROR (exit code 4 but no recognized error messages)
 (unchecked: 1)
Compilation failed, duration = 1 s


###################### Javari also fails:



Caused by: java.lang.IllegalArgumentException: unrecognized qualifier: null
    at checkers.util.GraphQualifierHierarchy.isSubtype
(GraphQualifierHierarchy.java:213)
    at checkers.types.QualifierHierarchy.isSubtype
(QualifierHierarchy.java:73)
    at checkers.types.TypeHierarchy.isSubtypeImpl
(TypeHierarchy.java:111)
    at checkers.types.TypeHierarchy.isSubtype(TypeHierarchy.java:66)
    at checkers.basetype.BaseTypeChecker.isSubtype
(BaseTypeChecker.java:322)
    at checkers.javari.JavariChecker.isSubtype(JavariChecker.java:69)
    at checkers.basetype.BaseTypeVisitor.commonAssignmentCheck
(BaseTypeVisitor.java:550)
    at checkers.basetype.BaseTypeVisitor.commonAssignmentCheck
(BaseTypeVisitor.java:533)
    at checkers.basetype.BaseTypeVisitor.checkArguments
(BaseTypeVisitor.java:689)
    at checkers.basetype.BaseTypeVisitor.visitMethodInvocation
(BaseTypeVisitor.java:287)
    at com.sun.tools.javac.tree.JCTree$JCMethodInvocation.accept
(JCTree.java:1311)
    at com.sun.source.util.TreePathScanner.scan
(TreePathScanner.java:67)
    at checkers.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:117)
    at com.sun.source.util.TreeScanner.scanAndReduce
(TreeScanner.java:80)
    at com.sun.source.util.TreeScanner.visitVariable
(TreeScanner.java:150)
    at checkers.basetype.BaseTypeVisitor.visitVariable
(BaseTypeVisitor.java:212)
    at com.sun.tools.javac.tree.JCTree$JCVariableDecl.accept
(JCTree.java:723)
    at com.sun.source.util.TreePathScanner.scan
(TreePathScanner.java:67)
    at checkers.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:117)
    at com.sun.source.util.TreeScanner.scanAndReduce
(TreeScanner.java:80)
    at com.sun.source.util.TreeScanner.scan(TreeScanner.java:90)
    at com.sun.source.util.TreeScanner.visitBlock(TreeScanner.java:159)
    at com.sun.tools.javac.tree.JCTree$JCBlock.accept(JCTree.java:777)
    at com.sun.source.util.TreePathScanner.scan
(TreePathScanner.java:67)
    at checkers.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:117)
    at com.sun.source.util.TreeScanner.scanAndReduce
(TreeScanner.java:80)
    at com.sun.source.util.TreeScanner.visitMethod
(TreeScanner.java:143)
    at checkers.basetype.BaseTypeVisitor.visitMethod
(BaseTypeVisitor.java:192)
    at com.sun.tools.javac.tree.JCTree$JCMethodDecl.accept
(JCTree.java:677)
    at com.sun.source.util.TreePathScanner.scan
(TreePathScanner.java:67)
    at checkers.basetype.BaseTypeVisitor.scan(BaseTypeVisitor.java:117)
    at com.sun.source.util.TreeScanner.scanAndReduce
(TreeScanner.java:80)
    at com.sun.source.util.TreeScanner.scan(TreeScanner.java:90)
    at com.sun.source.util.TreeScanner.scanAndReduce
(TreeScanner.java:98)
    at com.sun.source.util.TreeScanner.visitClass(TreeScanner.java:132)
    at checkers.basetype.BaseTypeVisitor.visitClass
(BaseTypeVisitor.java:134)
    at checkers.javari.JavariVisitor.visitClass(JavariVisitor.java:52)
    at checkers.javari.JavariVisitor.visitClass(JavariVisitor.java:23)
    at com.sun.tools.javac.tree.JCTree$JCClassDecl.accept
(JCTree.java:601)
    at com.sun.source.util.TreePathScanner.scan
(TreePathScanner.java:49)
    at checkers.source.SourceChecker.typeProcess
(SourceChecker.java:222)
    ... 16 more