Support method parameters in @EnsuresNonnull{If} annotations

[agrieve]

Similar to bug #431

The checkerframework version of this annotation shows the syntax for this as:

   @EnsuresNonNullIf("#1")
   public boolean equals(@Nullable Object obj) { ... }

Not sure if it also supports just listing the parameter's name...

Here's an example in Chrome of where this would be useful:

    private void initializeDevices() {
        int[] deviceIds = mInputManager.getInputDeviceIds();
        for (int i = 0; i < deviceIds.length; i++) {
            InputDevice inputDevice = InputDevice.getDevice(deviceIds[i]);
            if (isGamepadDevice(inputDevice)) {
                // NullAway currently complains that inputDevice might be null.
                registerGamepad(inputDevice);
            }
        }
    }

    @EnsuresNonNullIf("#1") // Would love this to work!
    private static boolean isGamepadDevice(InputDevice inputDevice) {
        if (inputDevice == null) return false;

        if (Objects.equals(inputDevice.getName(), "uinput-fpc")) return false;

        return ((inputDevice.getSources() & InputDevice.SOURCE_JOYSTICK)
                == InputDevice.SOURCE_JOYSTICK);
    }

[msridhar]

Hi @agrieve I think you can do this with a @Contract annotation? https://github.com/uber/NullAway/wiki/Supported-Annotations#contracts Like for isGamepadDevice, you could write @Contract("null -> false") and I think it should work. For extra safety, I recommend passing -XepOpt:NullAway:CheckContracts=true to also verify the @Contract annotations are correct (we should really turn that on by default). Let us know if that would work for you. Also you can define your own annotation with simple name @Contract if you don't want to take a dependency on JetBrains annotations.

[msridhar]

Admittedly the current situation, with a mix of @Contract and @EnsuresNonNull{If} support, is a bit confusing. We could take as an action item supporting the method parameter syntax of @EnsuresNonNull{If} annotations, though at this point it would have to be low priority.

[agrieve]

Ah, I thought that would be "check this returns false if the parameter is null", but not "returning false implies this is null". E.g. in my example it returns false even when the arg could be non-null.

[msridhar]

I always get confused by this stuff 🙂, but I think @Contract("null -> false") means if the parameter is null, the method definitely returns false. This is useful for NullAway since it implies that if the method returns true, the parameter cannot be null. So it should remove the false warning at the caller in your example.

[msridhar]

@agrieve could you confirm that @Contract("null -> false") would work for you for this case? Just to confirm there is no expressivity issue here, we just want to support the similar syntax for the ensures annotations

[agrieve]

Just tried it out, and it does seem to be working! So indeed, I guess this is just a request to have:

@EnsuresNonNull("#1")

be an alias for:

@Contract("null -> fail")

And

@EnsuresNonNullIf("#1")

be an alias for:

@Contract("null -> false")