ucr-riple / NullAwayAnnotator

A tool to help adapting code bases to NullAway type system.
MIT License
13 stars 6 forks source link

Use `@Contract` instead of `@NullUnmarked` #202

Open ketkarameya opened 1 year ago

ketkarameya commented 1 year ago

Is your feature request related to a problem? Please describe. Sometimes it is quiet easy to figure out when @Contract("null -> null") should be added at the method declaration itself. Currently, autoannotator adds @Nullunmarked on the invocations.

Describe the solution you'd like Add @Contract

cc: @lazaroclapp

nimakarimipour commented 1 year ago

Hi @ketkarameya Thank you for reporting the requested feature. I will work on it and get back to you.

msridhar commented 1 year ago

Thanks for the report @ketkarameya! We discussed this today and let me summarize the findings. We'd like to only infer @Contract in cases where we can give a guarantee that the inferred annotation is valid. Right now, @Contract verification is not enabled at Uber, and we also discovered the verification is not powerful enough to validate some common cases. Basically, we'd need to enhance the NullAway dataflow analysis to reason about dead code. Consider the following case (adapted from an example by @lazaroclapp):

  @Nullable
  @Contract("_, !null -> !null")
  static Bar bar(final String a, @Nullable final String b) {
    if (b == null) {
      return null;
    }
    return new Bar(a, b);
  }

Currently, NullAway fails to verify this @Contract annotation and reports it may be invalid (when contract checking is enabled). To verify the contract, the analysis has to reason that when b != null the return null statement is unreachable. Currently, NullAway does not do any kind of reasoning about (conditional) code reachability.

So, we are tabling support for @Contract inference until we can enhance NullAway's ability to verify @Contract annotations for these kinds of cases.

ketkarameya commented 1 year ago

Thanks for investigating into this :)