Boolean variables aliased to data-flow facts in type refinement

[GoogleCodeExporter]

It would be nice if the checker could detect that 'test' being true implies 'o' 
is non-null.

=== Test.java ===
import javax.annotation.Nullable;

abstract class Test {
  abstract @Nullable Object n();

  void f(boolean flag) {
    Object o = n();
    boolean test = o != null;
    if (test) {
      g(o);
    }
  }

  void g(Object o) {}
}
===

$ javac -version -processor 
org.checkerframework.checker.nullness.NullnessChecker Test.java
javac 1.8.0-jsr308-1.8.11
Test.java:10: error: [argument.type.incompatible] incompatible types in 
argument.
      g(o);
        ^
  found   : @Initialized @Nullable Object
  required: @Initialized @NonNull Object
1 error

Original issue reported on code.google.com by cus...@google.com on 5 Mar 2015 at 3:44

See more test cases in #6296.

[GoogleCodeExporter]

Original comment by michael.ernst@gmail.com on 6 Mar 2015 at 5:20

• Added labels: Dataflow

[GoogleCodeExporter]

Original comment by michael.ernst@gmail.com on 6 Mar 2015 at 5:21

• Added labels: Type-Enhancement
• Removed labels: Type-Defect

[hrj]

If this sort of data flow analysis is within the scope of this project, then shouldn't this be high priority?

I get a lot of warnings in my project that can be boiled down to this issue. However, I don't know where to draw a line. The "halting problem" limits the amount of analysis that can be done at compile time.

But atleast those code paths that don't involve a loop, goto or a recursive function call should be analysable, in theory.

[mernst]

This enhancement request is definitely within scope. I don't see control flow as a challenge here; the dataflow analysis handles control flow well. I think this issue could be solved by enriching the abstract domains.

Currently the dataflow analysis computes and propagates information about which expressions are null. It would need to be enhanced to also compute and propagate information about the relationship between the values of Boolean expressions and the nullness of expressions. That way, it would be able to refine the nullness of expressions such as o within the then clause of if (test) { ... }. This could be implemented for all type systems and other dataflow analyses, without special-casing it for nullness.

I don't think this is conceptually difficult, but it isn't trivial either, and we are currently busy with a few other features. If you were willing to help out with this extension to the dataflow analysis, we would gratefully accept that.

Thanks!

[mernst]

Above I suggested tracking the relationship between the values of Boolean expressions and the inferred/refined qualifiers on expressions.

A simpler approach would be to track, for each boolean variable, an expression that it is equivalent to. Then, at an if statement that uses the boolean variable, the Checker Framework would expand the variable into its definition, for the purpose of flow-sensitive refinement. (Naturally, all methods called in the expression would have to be pure, and if any of the variables in that expression might be changed, the fact would be erased.)