Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Consider supporting simple null equality checks in boolean-based Contract annotations #667

Closed
carterkozak opened this issue Sep 30, 2022 · 4 comments

Comments

@carterkozak
Copy link
Contributor

Firstly, NullAway is fantastic and I can't thank you enough for building it!

I've adopted @Contract annotations in a few places with great success on methods along the lines of MyPreconditions.checkNotNull(value) (contract null -> fail), however I'd love to see support for boolean parameters when the provided argument is a simple null check e.g. MyPreconditions.checkArgument(obj != null) (contract false -> fail).

In practice, the current limitation means that the following code fails as described inline:

class Test {
  @Contract("false -> fail")
  static void checkState(boolean value) {
      if (!value) {
        throw new IllegalStateException();
      }
  }
  
  String test(@Nullable Object input) {
    checkState(input != null);
    // NullAway doesn't take the check into account, describing a dereferenced expression
    return input.toString();
  }
}

Would you accept a contribution to handle such cases?

Concretely, my proposed solution would be to support boolean values in contracts only when the arg was provided as arg == null, null == arg, arg != null, or null != arg, thus the contract could be understood as a null check. I think this is a reasonable middle-ground without adding boolean-logic-dataflow support for cases where the argument itself is stored elsewhere e.g.

void test(@Nullable input) {
  boolean value = input == null;
  checkState(value); // I am not suggesting that such indirection be supported.
}

Thanks again for your work, any feedback is appreciated :-)

@msridhar
Copy link
Collaborator

msridhar commented Oct 1, 2022

This is an interesting idea! And it seems related to #666, which asks for support of Guava's Verify.verify(...). In #608 we added built-in support for Guava's Preconditions.checkArgument(...) and checkState(...). That approach just handles whatever boolean condition expression is passed directly to those methods, but not dataflow through locals, like you suggest (it works by rewriting the control-flow graph to expose the condition and exception-throwing behavior to NullAway). The current code has hardcoded matching for the Preconditions methods, but it seems straightforward to extend it to work for Verify.verify(...). We could use the same approach to handle calls to any method annotated @Contract("false -> fail"). Maybe this is what you were thinking in terms of implementation?

The only thing is that I'd probably want @lazaroclapp to review a change like this one before we land it (both at a high level and also the code in the PR), and he is on holiday for the next couple of weeks. I am optimistic we would accept a change like this if you want to go ahead and work on the PR, but we will have to wait for his review before it lands.

Let me know what you think, and I can give tips / feedback on implementation strategy.

@carterkozak
Copy link
Contributor Author

carterkozak commented Oct 2, 2022

Thank you for the information, I really appreciate it!

The approach used for Guava's Preconditions in #608 is beautifully elegant, however I think there are a few key differences that we may want to consider:

  • In the preconditions example, we have a good idea what kind of exception may be thrown by Preconditions methods (although the handler always provides an IllegalArgumentException despite checkState throwing IllegalStateException, I think this is fine because the node is added after a method call, but it may be helpful to provide the additional specificity here: pr PreconditionsHandler reflects Guava Preconditions exception types #668)
  • Preconditions boolean methods are void, while contracts may be used on methods which also return. I'm not entirely clear on how the inserted node interacts with other code when more complex structures are involved (mid-expression, for example), so this is an area I'll have to investigate further.
  • Contract methods may be used with boolean-in and boolean-out e.g. @Contract("true -> true; false -> false"). I suspect this is rare, but we could support something along these lines depending on the approach:
    @Contract("true -> true; false -> false")
    static boolean identity(boolean value) {
      return value;
    }
    String test(@Nullable Object o1) {
      if (identity(o1 != null)) {
        // o1 cannot be null here
        return o1.toString();
      }
      return "null";
    }

carterkozak added a commit to carterkozak/NullAway that referenced this issue Oct 2, 2022
For example, the following method will behave equivalently to
guava `Preconditions.checkState` with regards to null checks:
```java
@contract("false -> fail")
static void check(boolean pass) {
  if (!pass) throw new RuntimeException();
}
```

This implementation works in a couple of layers:
Firstly, contracts with a single boolean resultin in failure
are handled by inserting a conditional throw node inline following
the annotated method. This provides support for complex boolean
logic input validateion.
Secondly, simple null equal-to and not-equal-to checks are handled
by the existing ContractHandler. These don't support such complex
inputs, however they are able to work correctly with boolean
outputs rather than exclusively `fail` cases.

Note that this PR also fixes an assumption in the `ContractHandler`
which assumed that `null -> true` implied `!null -> false` which
isn't guaranteed unless otherwise specified -- fixing this allows
for several new test cases to work as expected.
I've also updated the ContractHandler to use more precise language
around antecedent nullness, previously null antecedents were
described as nullable. Please let me know if I've misunderstood
the logic, but reframing the values helped me to understand the
logic.
@carterkozak
Copy link
Contributor Author

Upon investigation, the second case I was worried about seems to work just fine: non-void methods aren't impacted by inserting a conditional throw.

I've created PR #669. I'd really appreciate if you (or anyone else) would like to provide feedback, but no rush :-)

(disclaimer: I'm not attached to the code, that's just how I prefer to quickly build an understanding of a codebase -- I won't be offended if folks want to throw it out and try something entirely different!)

carterkozak added a commit to carterkozak/NullAway that referenced this issue Oct 6, 2022
For example, the following method will behave equivalently to
guava `Preconditions.checkState` with regards to null checks:
```java
@contract("false -> fail")
static void check(boolean pass) {
  if (!pass) throw new RuntimeException();
}
```

This implementation works in a couple of layers:
Firstly, contracts with a single boolean resultin in failure
are handled by inserting a conditional throw node inline following
the annotated method. This provides support for complex boolean
logic input validateion.
Secondly, simple null equal-to and not-equal-to checks are handled
by the existing ContractHandler. These don't support such complex
inputs, however they are able to work correctly with boolean
outputs rather than exclusively `fail` cases.

Note that this PR also fixes an assumption in the `ContractHandler`
which assumed that `null -> true` implied `!null -> false` which
isn't guaranteed unless otherwise specified -- fixing this allows
for several new test cases to work as expected.
I've also updated the ContractHandler to use more precise language
around antecedent nullness, previously null antecedents were
described as nullable. Please let me know if I've misunderstood
the logic, but reframing the values helped me to understand the
logic.
carterkozak added a commit to carterkozak/NullAway that referenced this issue Oct 10, 2022
For example, the following method will behave equivalently to
guava `Preconditions.checkState` with regards to null checks:
```java
@contract("false -> fail")
static void check(boolean pass) {
  if (!pass) throw new RuntimeException();
}
```

This implementation works in a couple of layers:
Firstly, contracts with a single boolean resultin in failure
are handled by inserting a conditional throw node inline following
the annotated method. This provides support for complex boolean
logic input validateion.
Secondly, simple null equal-to and not-equal-to checks are handled
by the existing ContractHandler. These don't support such complex
inputs, however they are able to work correctly with boolean
outputs rather than exclusively `fail` cases.

Note that this PR also fixes an assumption in the `ContractHandler`
which assumed that `null -> true` implied `!null -> false` which
isn't guaranteed unless otherwise specified -- fixing this allows
for several new test cases to work as expected.
I've also updated the ContractHandler to use more precise language
around antecedent nullness, previously null antecedents were
described as nullable. Please let me know if I've misunderstood
the logic, but reframing the values helped me to understand the
logic.
carterkozak added a commit to carterkozak/NullAway that referenced this issue Oct 26, 2022
For example, the following method will behave equivalently to
guava `Preconditions.checkState` with regards to null checks:
```java
@contract("false -> fail")
static void check(boolean pass) {
  if (!pass) throw new RuntimeException();
}
```

This implementation works in a couple of layers:
Firstly, contracts with a single boolean resultin in failure
are handled by inserting a conditional throw node inline following
the annotated method. This provides support for complex boolean
logic input validateion.
Secondly, simple null equal-to and not-equal-to checks are handled
by the existing ContractHandler. These don't support such complex
inputs, however they are able to work correctly with boolean
outputs rather than exclusively `fail` cases.

Note that this PR also fixes an assumption in the `ContractHandler`
which assumed that `null -> true` implied `!null -> false` which
isn't guaranteed unless otherwise specified -- fixing this allows
for several new test cases to work as expected.
I've also updated the ContractHandler to use more precise language
around antecedent nullness, previously null antecedents were
described as nullable. Please let me know if I've misunderstood
the logic, but reframing the values helped me to understand the
logic.
@msridhar
Copy link
Collaborator

Closing since #669 was merged

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants