Nullness Checker makes wrong assumptions about unannotated libraries

[GoogleCodeExporter]

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.

Original issue reported on code.google.com by msaeed43 on 24 Oct 2009 at 12:22

[GoogleCodeExporter]

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.

Original comment by msaeed43 on 24 Oct 2009 at 12:28

[GoogleCodeExporter]

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.

Original comment by michael.ernst@gmail.com on 26 Oct 2009 at 4:30

[GoogleCodeExporter]

Original comment by michael.ernst@gmail.com on 26 Oct 2009 at 4:31

[GoogleCodeExporter]

Original comment by notn...@gmail.com on 13 Nov 2009 at 4:12

[GoogleCodeExporter]

Original comment by michael.ernst@gmail.com on 21 Nov 2009 at 8:18

• Changed title: Nullness Checker makes wrong assumptions about unannotated libraries

[GoogleCodeExporter]

Original comment by michael.ernst@gmail.com on 26 Jan 2011 at 10:08

• Added labels: Priority-High
• Removed labels: Priority-Medium

[GoogleCodeExporter]

Original comment by michael.ernst@gmail.com on 28 Mar 2013 at 6:24

[GoogleCodeExporter]

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.

Original comment by michael.ernst@gmail.com on 28 Aug 2014 at 7:52

[GoogleCodeExporter]

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.

Original comment by michael.ernst@gmail.com on 16 Oct 2014 at 3:48

[GoogleCodeExporter]

> 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?

Original comment by cus...@google.com on 10 Jan 2015 at 3:02

[GoogleCodeExporter]

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.

Original comment by cus...@google.com on 3 Apr 2015 at 6:09

[GoogleCodeExporter]

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.

Original comment by danbroth...@gmail.com on 9 Apr 2015 at 12:52

[GoogleCodeExporter]

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

Original comment by michael.ernst@gmail.com on 9 Apr 2015 at 12:55

[GoogleCodeExporter]

Thanks Dan!

Original comment by cus...@google.com on 9 Apr 2015 at 3:05

[GoogleCodeExporter]

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

Original comment by cus...@google.com on 10 Jun 2015 at 10:01

[GoogleCodeExporter]

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.

Original comment by jbu...@cs.washington.edu on 10 Jun 2015 at 10:26

[GoogleCodeExporter]

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!

Original comment by michael.ernst@gmail.com on 11 Jun 2015 at 1:19

[GoogleCodeExporter]

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.

Original comment by wdi...@gmail.com on 16 Jun 2015 at 5:06

[GoogleCodeExporter]

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?)

Original comment by cus...@google.com on 16 Jun 2015 at 5:24

[GoogleCodeExporter]

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 
:-)

Original comment by wdi...@gmail.com on 17 Jun 2015 at 4:45

[GoogleCodeExporter]

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?

Original comment by renato.a...@twobotechnologies.com on 1 Jul 2015 at 1:30

[GoogleCodeExporter]

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?

Original comment by michael.ernst@gmail.com on 1 Jul 2015 at 1:36

[GoogleCodeExporter]

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.

Original comment by renato.a...@twobotechnologies.com on 1 Jul 2015 at 2:17

[GoogleCodeExporter]

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.)

Original comment by michael.ernst@gmail.com on 1 Jul 2015 at 2:57

[mernst]

This issue can be resolved by making -AuseDefaultsForUncheckedCode=-source,bytecode be the default behavior. We should do experiments passing that command-line option to see how much work would remain, to make the Checker Framework usable with that configuration.