@ThrowsException annotation for methods that always throw an exception

[SwingGuy1024]

This is a feature request for a @ThrowsException method annotation, which indicates that the annotated method throws an exception.
This would be analogous to @TerminatesExecution, in that it would improve the dataflow analysis (flow-sensitive type refinement).

The original suggestion follows.

---

In my project at work, I encountered this line, which throws an exception:

BusinessException.builder()
        .detail(detailedMessage)
        .transitionFrom(ShippingState.RECEIVED)
        .withIdentifier(ProductSourceIdentifier.WAREHOUSE_ID, warehouseId)
        .buildAndThrow();

Should the Nullness Checker encounter this, it has no way of knowing that an exception is guaranteed to be thrown on this line. Granted, I would have written it like this:

throw BusinessException.builder()
        .detail(detailedMessage)
        .transitionFrom(ShippingState.RECEIVED)
        .withIdentifier(ProductSourceIdentifier.WAREHOUSE_ID, warehouseId)
        .build();

But I didn't write this code, and this is done all over the project.

Now suppose the Nullness Checker encountered something like this:

public ConnectionSource getConnection() {
  if (connectionSource == null) {
    BusinessException.builder()
        .doWhateverStuffIsNeeded()
        .buildAndThrow();
  }
  return connectionSource;
}

It would have no way of knowing that an exception gets thrown when connectionSource is null, so it would issue an error, believing that connectionSource could be null.

In principle, this could be handled by an annotation on the buildAndThrow() method that says that it throws an exception, under a condition. So let's imagine there's an annotation @throws(String expression) where it declares it will throw an exception if the expression is true. (This is similar to the JetBrains @contract annotation, which covers the same problem.) Then we could declare the method like this:

@Throws("true")
public void buildAndThrow() { ... }

Now the Nullness Checker would have the information it needs. It would know that an exception is always thrown when connectionSource is null, so would process the method correctly.

The Nullness Checker would be more useful with a facility like this. The preconditions and post conditions are useful, but they don't cover a case like this.

(Please don't suggest that @RequiresNonNull(connectionSource) would solve this problem. In this simplified version, it will, but the actual case was far more complicated, with several method parameters and various tests. In the real-world example where I found this, the only solution that makes sense would be to tell the checker that the buildAndThrow method will throw an exception.)

[mernst]

Thanks for the suggestion. This would not be too hard to implement. The dataflow analysis would treat the annotated method in the same way that it currently treats a throw statement.

[smillst]

This is similar to #1497.

[SwingGuy1024]

I'm looking at my previous example:

public @NonNull ConnectionSource getConnection() {
  if (connectionSource == null) {
    BusinessException.builder()
        .doWhateverStuffIsNeeded()
        .buildAndThrow();
  return connectionSource;
}

I had previously said this needs an annotation that takes an expression. But I now realize that the proposed @ThrowsException can handle this without the expression if it's applied to the buildAndThrow() method.

(Also, for clarity, I added the @NonNull annotation.)

[ThrowsException]

I would love my own exception annotation.

[mernst]

@ThrowsException we will try to accommodate you! (Pull requests are always welcome...)