defaults for unannotated class files

[Manu Sridharan]

Hi all,

I am a bit confused about the current default handling of unannotated class files / jars by the nullness checker.  My test case has two files T1.java and T2.java:

T1.java
----------
public class T1 {

    public static void checkStr(String s) {
      // uncommenting this line doesn't seem to make a difference,
      // but including just in case
      // s.toString();
    }

}

T2.java
----------
public class T2 {

    public static void main(String[] args) {
        T1.checkStr(null);
    }
}

First, I run javac T1.java, i.e., without the nullness checker.  Then, I run javac -processor org.checkerframework.checker.nullness.NullnessChecker T2.java.  I would expect that with the unsound defaults, I would *not* get an error in this situation, since there are no annotations in the T1.class file.  However, the Checker framework (version 2.1.7) is in fact reporting an error at the call T1.checkStr(null) inside T2.

Have I misunderstood something?  Is the above the expected behavior?  If there is a configuration of the nullness checker that treats unannotated libraries / class files unsoundly (something like assuming all method parameters are @Nullable and all return values are @NonNull), I'd be interested in knowing how to run it.  Thanks!

Best,
Manu

Best,
Manu

[Suzanne Millstein]

---------- Forwarded message ----------
From: Suzanne Millstein <smi...@cs.washington.edu>
Date: Tue, Jan 10, 2017 at 10:01 AM
Subject: Re: defaults for unannotated class files
To: Manu Sridharan <msri...@gmail.com>

Hi Manu,

Yes, this is expected behavior.  The defaults for unannotated class files are the same for unannotated source code, which is @NonNull for parameters and returns.  This is in fact unsound for code that is not type-checked since a return might be null.  The only way to change this default for unannotated class files is to add a package-info.java for the package contain that class that has a @DefaultQualifier annotation.  For example:

@org.checkerframework.framework.qual.DefaultQualifier(
    value = org.checkerframework.checker.nullness.qual.Nullable.class , 
    locations = org.checkerframework.framework.qual.TypeUseLocation.PARAMETER)
package com;

(Import statements are not allowed.)

Sound defaults for unannotated class files can be turned on using -AuseDefaultsForUncheckedCode=-bytecode (See http://types.cs.washington.edu/checker-framework/current/checker-framework-manual.html#defaults-classfile).

-Suzanne

[Manu Sridharan]

Hi Suzanne, thanks for the response!  If I understand correctly, we would need a separate package-info.java file for each third-party library package; is that correct?

Also, a question just out of curiosity.  The documentation states that sound defaults for unannotated class files will be the default in a future release.  What are the considerations involved in switching over to sound defaults?

Thanks again!

Best,
Manu

[Suzanne Millstein]

Hi Manu,

If I understand correctly, we would need a separate package-info.java file for each third-party library package; is that correct?

Yes, one for each top-level package to which the defaults should apply.  The @DefaultQualifier will be applied to each sub-package of the package.  So, if you annotate the com package as in my example, then com.google and com.example will have the same defaults. 

Also, a question just out of curiosity.  The documentation states that sound defaults for unannotated class files will be the default in a future release.  What are the considerations involved in switching over to sound defaults?

We wanted to do a case study first to better understand how useable the Checker Framework is with this option.

-Suzanne 

[Manu Sridharan]

Thanks so much for the quick response!  Best, Manu