Nullness Checker makes wrong assumptions about unannotated libraries about checker-framework HOT 25 OPEN

I have started working on this item.  However, there are few complexities here:

1. It's unlikely that inner/member classes (for iterators, comparables, etc).  
The
test for presence of relevant annotations, should run on the enclosing class, 
not the
inner classes.  The inner/member classes have a good likelyhood that they don't
contain any annotations.

2. We should separate external libraries (usually found in binary), from source
classes that are being type-checked.  NNEL is desirable for an unannotated 
source, so
the programmer can start with NNEL and would get fewer errors before he starts
writing the annotations.

I agree with #1:  The test for mentions of the nullness checker needs to be 
per-file,
not just per-class.  Thanks.

For #2, is this handled by the check of whether the class was explicitly 
mentioned on
the command line?  Or, when a programmer is ready to start on unannotated 
source,
just adding "import checkers.nullness.quals.*;" would trigger NNEL.

Here is a proposed solution:

Create a command-line option that switches between two defaulting rules for
unannotated bytecode:
 * flexible: top for parameters, bottom for return; allows all calls.
 * conservative: bottom for parameters, top for return; forbids most calls.

Here are more specifics for the conservative proposal.  This text is copied 
from issue #370 to this issue where it belongs: 

When reading from classfiles (but not in other circumstances), if an upper 
bound is of Java type Object and has no annotation, then treat the upper bound 
as having the top annotation.  For the nullness type system, this would be 
@Nullable.  Make no changes in other situations, including those where the 
upper bound is not Object and those where the upper bound is Object but has an 
annotation.

> When reading from classfiles (but not in other circumstances), if an upper 
bound is of Java type Object and has no annotation, then treat the upper bound 
as having the top annotation.  For the nullness type system, this would be 
@Nullable.

Has there been any progress on this?

Is anyone working on this? And if not, would you accept a patch to implement 
the proposal described in #9? This continues to be the main source of problems 
for us.

I have been working on this, and have a patch to fix it.  I have made the 
defaulting configurable, and will send my patch to wdietl for review this week.

Terrific!  Thanks very much, Dan.  We look forward to it.

Thanks Dan!

Dan, have you had any time to work on this?

Thank you for the continued interest.

This issue is actively being worked on at the moment.  The review comments have 
been addressed.  We will update this issue when it's completed.

Let me expand a bit on the status of this issue.

We have code-reviewed your patch, made improvements to it, and pushed it to the 
main Checker Framework repository.  So, the Checker Framework now has this 
capability, which is great.

We have not yet publicly announced this feature.  That is because we are 
testing it locally.  These tests have indicated the need for tooling that 
indicates what library annotations are missing and that makes it easier for a 
user to add library annotations.

Once we have created that tooling, we will enable the feature by default (there 
will be a command-line option to disable it) and we will announce it to users.

So, we continue to actively work on this feature; our quietness does not mean 
that we are ignoring it.  If you want to participate in the testing and 
improvements, we would welcome your help, but we will continue to work on it 
regardless.

Thanks again!

I've added a new option "safeDefaultsForUncheckedBytecode" to already enable 
the new safe defaults. Provide the "-AsafeDefaultsForUncheckedBytecode" option 
on the command line.

As Mike pointed out, we're aware of additional infrastructure needs to make use 
of the safe defaults convenient. If you're willing to experiment with the new 
defaults, we would very much appreciate your comments.

Thanks!
cu, WMD.

Thanks very much for the update! I'll try out the new flag and report back.

(Is the bug thread a good place for that, or would a thread on 
checker-framework-dev@ be better?)

If you find multiple issues or code examples that don't behave as expected, it 
would be easier to start separate threads on checker-framework-dev@.
If you like the implemented behavior a quick comment here would be appreciated 
:-)

In my case, I don't want to mess with the defaults for all methods (even though 
I would like to be able to do what this proposal says), I just want to be able 
to annotate some methods from certain libraries (including the Java Standard 
library) without changing its source code. I believe this could be achieved by 
allowing a config file (or even a Java file) that lets us 'decorate' existing 
methods with type annotations.

For example, I would provide a file to add annotations to Java's Optional that 
looks like this:

// Optional.java (method signature overrides)
class Optional<T> {
  Optional<T> ofNullable(@Nullable T t) {} // declaration is ignored
}

Even though I didn't provide overrides for all Optional methods, it should be 
fine as that may be all I need! All other methods' signatures are just taken 
from the actual class file.

What do you think about this?

Regarding comment 21, the capability you are asking for already exists.

Please see Chapter 28, "Annotating Libraries", in the Checker Framework manual:
http://types.cs.washington.edu/checker-framework/current/checker-framework-manua
l.html#annotating-libraries
In particular, see section 28.2, "Using stub classes":
http://types.cs.washington.edu/checker-framework/current/checker-framework-manua
l.html#stub

Is there some way we could have made this section of the manual easier to find, 
when you read the manual looking for a way to annotate a library without 
changing its source code?

Yes, I found no reference to this when reading about how to suppress warnings 
for the NullnessChecker. Reading quickly the large number of chapter names, I 
missed the relevant section. I did read quite a lot in other chapters, and 
still didn't see any mention to this feature.

I will give this a try! Thanks.

Ah, that's because annotating a library is not a technique for suppressing a 
warning.  Suppressing a warning is leaving a type incompatibility in the source 
code but preventing the type-checker from issuing a warning about it.  By 
contrast, you are changing the annotations to eliminate or fix the type 
incompatibility -- you are fixing the warning rather than eliminating it.  (And 
that's the desirable approach!)

I'll add some text in the manual to clarify this distinction.

I'm glad that you are now on the right track.  Please let us know if you have 
any further problems.  (But probably elsewhere, if it is not related to Issue 
#12.)