[Checkers] Nullness inference

[Mahmood Ali]

>
Greetings,

> For the library mode, I did not yet tested it for nullness.
I see.

> If you prefer, I can output everything in a single file. It is just a
> bit messy. It depends on how hard it is for you to deal with multiple
> files.
You can output everything in a single file for the moment (or simple  
have a script that concatenate all the files) for the time-being.   
Having a stub-path is a desired feature, and has been requested  
multiple times, it's about time to do it.

>> I should also note that julia inferred the parameter types for
>> PolyNull.id2() incorrectly.  For a method declared as:
>>
>>  public Object id2(Object p1, Object p2) {
>>    if (p1 == p2) return p1;
>>    else return p2;
>>  }
>>
>> The declaration should be
>>  public @PolyNull Object id2(@PolyNull Object l1, @PolyNull Object
>> l2);
>> not (notice l1 declaration)
>>  public @PolyNull Object id2(@Nullable Object l1, @PolyNull Object
>> l2);
>
> For me (and
> for julia) it is enough for l2 (i.e. p2) to be non-null to infer that
> the return value is non-null.
This is true.  Please forgive me for my lack of explanation: The  
declaration inferred by Julie describe method specification correctly,  
but makes the body not type-check according to the Checker.

The Flow sensitive analysis in the Checker Framework is limited and  
doesn't perform analysis related to a polymorphic qualifier (to a  
first-order approximation).  It would not infer that in the true  
branch of if statement p1 and p2 have the same type (i.e. @PolyNull  
Object), so p1 type will be @Nullable Object is not a subtype of  
@PolyNull Object.

The same behavior occurs for the following method:
  @PolyNull Object idNullness(@PolyNull Object p) {
    if (p == null) return null;   // line not type check with checker
    else return "m";
  }

The Checker here wouldn't not infer that in the true branch null type  
is actually what's expected as the return value.

This behavior is analogues to Java (not quite C++).  Consider the  
following method (similar to id2):
  <T> T id2(Object p1, T p2) {
    if (p1 == p2) return p1;  // <-- doesn't type check in Java
    else return p2;
  }

While the declaration of the method accurately describe the method  
specification, the body doesn't type check as the type of p1, Object,  
isn't is a subtype of the return type, T.

Hope that explained the discrepancy.

Regards,
Mahmood