[Checkers] Nullness inference

[Michael Ernst]

Fausto-

> I attach the stub files generated for JFlex. Those for Daikon will be
> sent next week, since I am on a slow internet connection and cannot
> download the Daikon package at the moment.

OK, I understand.  I'll look forward to receiving the others as well.

> For @PolyNull, I understand that it stands for both @Nullable and
> @NonNull, like a template in C++.

Yes, that's quite close to correct.  The text we have been using to explain
it is:

  A method written using a polymorphic qualifier conceptually has multiple
  versions: in each version, every instance of the polymorphic qualifier
  has been conceptually replaced by one of the other qualifiers.

and you can see more explanation at

http://groups.csail.mit.edu/pag/jsr308/current/checkers-manual.html#htoc11

However, we welcome suggestions for improving the exposition!

> However, I wonder whether you can use
> it in every place where a type is allowed. For instance, what is the
> meaning of
> 
> void m(@PolyNull Object obj)
> 
> or
> 
> void m(@PolyNull Object obj1, @PolyNull Object obj2)
> 
> ?

You are right about

  void m(@PolyNull Object obj)

The benefit of polymorphic qualifiers comes when one is used multiple times
in a method, since then each instance turns into the same type qualifier.
Most frequently, the polymorphic qualifier appears on both the return type
and at least one formal parameter.  It can also be useful to have
polymorphic qualifiers on (only) multiple formal parameters, especially if
the method side-effects one of its arguments.

> Are two @PolyNull methods completely independent wrt the choice made for
> their @PolyNull variables?

Yes, that is right.

> For the moment, I generate @PolyNull annotations only for methods
> returning a reference type whose non-nullness has not been proved, but
> which are provably non-null whenever a parameter of the method is
> non-null.

This is the most common case.  It's actually extremely common for, say,
immutability:  the expression x.f is immutable if x is immutable.  I
suspect that this comes up much less frequently in the nullness type
system.  (That's an interesting observation about the differences already.)

> Attached, you see an example PolyNull.java and the stub file
> that my tool generates for it. Non such example is found in JFlex. Do
> you have an example of @PolyNull which should be found for JFlex?

I'm not familiar with the JFlex code, so I don't know of any right now.

> There is no special support for generics in my tool. The problem is that
> the types have been erased in the bytecode.

It's true that the types are erased in the bytecode, and this is a serious
annoyance for analyses.  However, the signatures are available in the class
file (just not in the bytecode part of the class file) if the file has been
compiled with debugging information.  It's possible that this would allow
you to recover part of the information, at least in some important cases.

> I can problably instruct the
> analyzer to use some types or to consult some source code (this might
> take some work, but it is feasable). However, I find many problems. For
> instance, in a map class:
> 
> class Map<T,D> {
>    void put(T from, D to) {}
>    void D get(T from) {}
> }
> 
> it is impossible to prove that get() returns a @NonNull D even through
> the program always puts a @NonNull D inside the map. This is because you
> have to prove that all calls to get() receive a parameter which has been
> already put in the map, a difficult thing to prove.

Yes, this is the classic problem with proving nullness.  Our static checker
gives up in many cases -- if a simple local analysis cannot prove the
desired property, then a user is forced to insert either a
@SuppressWarnings annotation or a run-time check.  I know that your
analysis is much more powerful, and in each case where it can do more
complicated proving, it will produce facts that will require human
intervention when type-checking the inference results.  I'm very curious
how often these will come up in real code, and in good code.

> Can I use your type-checkers on my stub files or should I wait for some
> translator?

I'll leave this question to Mahmood.  (Unless Mahmood tells me I'm the one
who should answer it!)

Happy new year!

                    -Mike