Bug in store propagation

[jdmota]

Example

import org.checkerframework.checker.nullness.qual.Nullable;

class Bug {
  void foo(@Nullable Object obj) {
    if (obj != null) {
    
    }
    if (true) {
      obj.toString(); // OK??
    }
  }
  
  void bar(@Nullable Object obj) {
    boolean bool = obj != null;
    if (true) {
      obj.toString();
    }
  }
}

java -jar "checker-framework-3.3.0/checker/dist/checker.jar" -processor org.checkerframework.checker.nullness.NullnessChecker Bug.java

Online demo

Expected result

Bug.java:9: error: [dereference.of.nullable] dereference of possibly-null reference obj
      obj.toString();
      ^
Bug.java:16: error: [dereference.of.nullable] dereference of possibly-null reference obj
      obj.toString();
      ^
2 errors

Current result

Bug.java:16: error: [dereference.of.nullable] dereference of possibly-null reference obj
      obj.toString();
      ^
1 error

Possible explanation

Only recently I started working with Checker, so I am not sure, but I suspect what the issue might be. Since FlowRule.EACH_TO_EACH is considered the normal case for store propagation, the "then" and "else" stores resulting from the analysis of the first obj != null are propagated "each to each" to the true expression and then to the second if statement. I believe that this is incorrect. Probably FlowRule.EACH_TO_EACH should only apply if what immediatly follows is a conditional block? The reason why the second error is caught, I believe, is because CFAbstractTransfer#visitVariableDeclaration returns a RegularTransferResult, which already combines the two stores, so the propagation works as expected.

[mernst]

Thanks for the bug report! Here is a slightly expanded version that shows the expected behavior in a simpler case too (where the Nullness Checker works as expected).

import org.checkerframework.checker.nullness.qual.Nullable;

class Bug {
  void m1(@Nullable Object obj) {
    if (true) {
      // :: (dereference.of.nullable)
      obj.toString();
    }
  }

  void m2(@Nullable Object obj) {
    if (obj != null) {
    
    }
    if (true) {
      // :: (dereference.of.nullable)
      obj.toString(); // BUG: no warning about this dereference
    }
  }
  
  void m3(@Nullable Object obj) {
    boolean bool = obj != null;
    if (true) {
      // :: (dereference.of.nullable)
      obj.toString();
    }
  }
}

[wmdietl]

Thanks for reporting this bug!

It looks like an incorrect CFG is generated when there is an if (true). Only a single condition is generated, instead of two, and the Block before is:

Before: org.checkerframework.checker.nullness.NullnessStore (
obj > CFAbstractValue{annotations=[@org.checkerframework.checker.initialization.qual.Initialized, @org.checkerframework.checker.nullness.qual.Nullable], underlyingType=@org.checkerframework.checker.nullness.qual.Nullable java.lang.Object}
initialized fields = []
invariant fields = {}
isPolyNonNull = false
)
~~~~~~~~~
obj [ LocalVariable ] > CFAbstractValue{annotations=[@org.checkerframework.checker.initialization.qual.Initialized, @org.checkerframework.checker.nullness.qual.Nullable], underlyingType=@org.checkerframework.checker.nullness.qual.Nullable java.lang.Object}
null [ NullLiteral ] > CFAbstractValue{annotations=[@org.checkerframework.checker.initialization.qual.Initialized, @org.checkerframework.checker.nullness.qual.Nullable], underlyingType=<nulltype>}
(obj != null) [ NotEqual ] > CFAbstractValue{annotations=[@org.checkerframework.checker.initialization.qual.Initialized, @org.checkerframework.checker.nullness.qual.NonNull], underlyingType=boolean}
true [ BooleanLiteral ] > CFAbstractValue{annotations=[@org.checkerframework.checker.initialization.qual.Initialized, @org.checkerframework.checker.nullness.qual.NonNull], underlyingType=boolean

With a different condition and without a condition, the expected error is produced.

Are you running into this issue with something other than if (true)? Did you find this with real code?

[jdmota]

I did not find it in real code but maybe I can provide some context. I found this issue while developing a plugin with support for typestates. I had something like this:

MyIterator it = new MyIterator();

it.hasNext();
if (true) {
    it.next();
}

And it was not showing an error. My implementation looks at the hasNext invocation and produces a "then" store where it is in the "Next" state and an "else" store where it is in the "end" state. The next call is only allowed in the "Next" state.

I was not sure if I did something wrong, or if the issue was with Checker. So I attempted to produce an example with the nullness plugin, and found, what seems to be, a similar issue: the "then" and "else" stores are propagated "each to each", even though what immediately follows the method invocation is not a conditional block, but a regular block with a true node.

Overriding Analysis#propagateStoresTo seems to fix my particular issue, but I am not sure if this is correct.

protected void propagateStoresTo(...) {
    switch (flowRule) {
        case EACH_TO_EACH:
            if (currentInput.containsTwoStores()
                && succ.getType() == CONDITIONAL_BLOCK // Addition
            ) {

Edit: I suspect that different conditions do not produce an error because CFAbstractTransfer ends up merging the two stores by returning RegularTransferResult while handling certain nodes. But if a node is not handled, conditional results remain conditional. For example, a condition like new Object() instanceof Object also reproduces the issue (demo).

[jdmota]

Found another interesting example:

import org.checkerframework.checker.nullness.qual.Nullable;

class Bug {
  void foo(@Nullable Object obj) {
    if ((obj != null) == false) {
      // :: (dereference.of.nullable)
      obj.toString(); // BUG: no warning about this dereference
    }
  }
  
  void bar(@Nullable Object obj) {
    if (!(obj == null) == false) {
      // :: (dereference.of.nullable)
      obj.toString(); // BUG: no warning about this dereference
    }
  }
  
  void baz(@Nullable Object obj) {
    if ((obj == null) == true) {
      // :: (dereference.of.nullable)
      obj.toString();
    }
  }
}

Demo

[wmdietl]

I filed #3274 to fix the original bug report from this issue.
The suggestion to check for conditional blocks doesn't work: if the condition contains method calls, there are other blocks in between. Several tests failed when I tried that.

The proposed fix removes an optimization, but I doubt it will have a performance impact.
I didn't immediately see how to modify the CFG to properly merge the stores. See my comment in the PR.
The fix also works for the instanceof example.

I can reproduce your comment about your new typestate checker using the Regex Checker:

    void bar(String s) {
        RegexUtil.isRegex(s);
        if (true) {
            // :: error: (argument.type.incompatible)
            Pattern.compile(s); // Error missing
        }
    }

#3274 doesn't fix that issue. I'll look into wrapping all ExpressionStatements into an assignment to a temporary variable, turning the above code into:

    void bar(String s) {
        boolean res = RegexUtil.isRegex(s);
        if (true) {
            // :: error: (argument.type.incompatible)
            Pattern.compile(s);
        }
    }

which correctly gives an error.

I've started #3275 for your latest comment, which seems unrelated to this issue.
Thanks for finding these corner cases!