Nullness Checker and compile-time constant branch conditions

[tarun14110]

Getting false positive while using Nullness checker.

public class Main {
    public void example() {
        String str = null;

        if (true) {
            str = new String();
            }
        if (true) {
            str.charAt(0);
            }
    }
}

Error: [dereference.of.nullable] dereference of possibly-null reference str line 10

[mernst]

I agree that this is a false positive warning. Does it come up in well-written real-world code?

For any given false positive warning, it is theoretically possible to improve the Checker Framework to eliminate it. Not all of them are worth fixing, though. By design, each type system in the Checker Framework has limited expressiveness. Our goal is to implement enough functionality to handle common, well-written real-world code, not to cover every possible situation. A simple type system is easier for users to understand, less likely to contain bugs, and more efficient.

By the way, here is a simpler test case.

public class Main {
  public void example() {
    String str = null;
    if (true) {
      str = new String();
    }
    str.charAt(0);              // false positive warning
  }

  public void example2() {
    String str = null;
    str = new String();
    str.charAt(0);              // no warning
  }
}

[tarun14110]

Yeah, that is a Minimal Working Example of a real life code. Like, there can be some booleans in the large codebase, which after some iterations of development cycles may always be true or false and are used in some if conditions. Obviously, that's bad coding practice, but won't these kind of false positives confuses user ? Yeah, there is trade off between efficiency and accuracy.

[kanha95]

@tarun14110 It's always better to suppress such warnings where ambiguity prevails. The Nullness Checker does not exclusively focuses on all such positive warnings, rather it provides a generalized solution to real world industrial codes.

[mernst]

@kanha95 @tarun14110 I disagree that "It's always better to suppress such warnings". Sometimes, it is best to fix a bug. Sometimes, it is best to rewrite the code in a cleaner style that can be type-checked successfully. When you must suppress a warning, then it's good to report it, as @tarun14110 did. Thanks for the bug report, and for confirming that it's a real-world test case.

[kanha95]

@mernst Yes professor, i do agree it's a bug! But when we run the same piece of code without checker framework then also it will raise a warning saying "De-referencing possible null pointer". JDK 8 comes with inbuilt annotations to catch such statements. So, i don't think checker framework should completely ignore this type of warning. But yes, it would be better if instead of an error, a warning message is issued.

[mernst]

Can you point me at the inbuilt Java 8 annotations that raise the warning "De-referencing possible null pointer"? And at the exact command line, that does not use the Checker Framework, that yields this warning? Thanks!

[kanha95]

@mernst I apologize professor. It's not the JDK 8 inbuilt annotation rather it's the inbuilt annotation processor of net-beans that was issuing the warning. I misinterpreted it.

[JasonMrX]

@mernst @tarun14110 @kanha95 This is an interesting issue.

public class Main {
  public void example() {
    String str = null;
    if (true) {
      str = new String();
    }
    str.charAt(0);              // false positive warning
  }
}

The reason for this code snippet to issue false positive warning is that the dataflow framework refines str as the LUB of @NonNull and @Nullable, which is still @Nullable, regardless the fact that the condition in the if branch is always true. I also noticed this issue while working on the @IntRange annotation. I found if (true) everywhere in the test cases, however at the beginning, I am surprise to see that even if the control always flows into this branch, the refined annotation is still taking the LUB instead.

As in the dataflow framework, we do have value analysis for boolean values, I am thinking maybe we can use this information to eliminate the "dead" branches to make the control flow refinement more precise. At the same time, we could provide user hints to make the code cleaner and well written, for example:

void example(@IntVal({1, 2}) int a) {
    int b = 0;
    if (a == 3) { 
        // warning: dead branch
        // maybe you should delete this branch, 
        // or check if the range of variable 'a' is incorrect.
        b = 3;
    }
    // b is still @IntVal({0}) but not @IntVal({0, 3});
}

[kanha95]

@JasonMrX Thanks for the information. I agree with all your points. But i have one doubt. You said "even if the control always flows into this branch, the refined annotation is still taking the LUB instead", which is @Nullable.

Consider this case:

public class Main { public void example() { String str = new String();

//dead branch
if (false) {
  str = null;
}

str.charAt(0);              // false positive warning

} }

Here also the warning is observed even if there is a completely dead branch. Can you explain this?

[JasonMrX]

This is exactly my point. Sorry for not making it clear enough. Here is an more detailed example:

public class Main {
  public void example() {
    String str;
    if (true) {
      str = new String(); // invariant: "the control flow ALWAYS flows into this branch"
    else {
      str = null;
    }
    str.charAt(0);
    // Checker framework: taking the LUB of @NonNull and @Nullable regardless the invariant above.
    // My expectation: only take @NonNull
  }
  public void example2() {
    String str;
    if (false) {
      str = null; // invariant: "the control flow NEVER flows into this branch"
    else {
      str = new String();
    }
    str.charAt(0);
    // Checker framework: taking the LUB of @NonNull and @Nullable regardless the invariant above.
    // My expectation: only take @NonNull
  }
}

The two examples are talking about the same thing. I am not native English speaker. Hope this is clear enough.

[wmdietl]

Regarding dead code, there were several previous discussions, e.g. here: https://groups.google.com/d/msg/checker-framework-dev/0VCUgeg5iHA/OrFroJo5BQAJ

In the end (so far) we always decided against doing something special.

More generally, we currently treat each conditional block individually and don't carry forward information to another block that might have the same (or a stronger/weaker) condition. We simply compute the LUB at a merge point. Similarly, the Java definite assignment check prevents code like this:

    void foo(boolean b) {
        Object l;
        if (b) {
            l = new Object();
        }
        if (b) {
            l.toString();
        }
    }

even though it is perfectly fine.

Improving this would require storing more information past merge points, requiring more memory and slowing down the analysis. Let's keep this issue open to see how frequently it comes up. If you have a link to open-source software that has this issue, please add it.

Would a better title for the issue be something like "False positives because of condition inter-dependencies"?

[mernst]

I agree that the store should not record arbitrary boolean conditions, together with the dataflow facts that are true under that boolean condition.

I think we should keep this issue open only for the special case when the condition is known, at compile time, to be true or false. In those cases, it seems to make sense to do a more precise analysis. This could be done in two ways:

• CFG construction doesn't introduce a branch; the generated CFG is straightline, without the dead branch. However, the boolean value might not be known at CFG construction time; a later analysis might determine it.
• dataflow analysis causes the dead code not to affect the store after the merge. Two ways to do this are:
  • special-case merging to use only the live branch, when the other branch is known to be dead
  • on the dead branch, set all abstract values to bottom, so that the lub at the merge will result in the values from the live branch

Perhaps there would be other ways to determine this.

[ashishrana160796]

In response to @wmdietl's comment about pointing to a open-source software that uses such scenario.

From aima-java( https://github.com/aimacode/aima-java ) an open-source software implementing A.I algorithms. This problem does appear in AlphaBetaSearch.java. Where considering the algorithm for this issue, refinement via comparison with alpha & beta values does happen. Here, see the snippet :

public ACTION makeDecision(STATE state) {
        metrics = new Metrics();
        ACTION result = null;
        double resultValue = Double.NEGATIVE_INFINITY;
        PLAYER player = game.getPlayer(state);
        for (ACTION action : game.getActions(state)) {
            double value = minValue(game.getResult(state, action), player,
                    Double.NEGATIVE_INFINITY, Double.POSITIVE_INFINITY);
            if (value > resultValue) {
                result = action;
                resultValue = value;
            }
        }
        return result;
    }

From this algorithm and its approach to handle it. This rather looks like common way of solving problems like comparing to neg or pos infinity value and knowing for sure that instance will definitely gets assigned non-null value.

Directory location : /aima-java-aima3e-v1.9.1/aima-core/src/main/java/aima/core/search/adversarial Attached File : AlphaBetaSearch.txt

[ashishrana160796]

Keeping real life codes and constant branch conditions in mind the following code scenario can also be added to this discussion that produces false positives but is also getting used real open-source codes :

Object refine() {
        Object result = null;
        try {
            result = new Object();
            // do something without sideffects 
          } catch (Exception e) {
            // A specific exception related to above failed task.
            e.printStackTrace();
        }
        // last flow branch never getting executed.
        // but still producing errors.
        return result;
    }