equality between Java enums is not handled correctly

[carocad]

Hey guys,
I have a very simple class in Java with:

public final class Message {

            private final Action action;
            private final IIdentifier id;
            private final Payload payload;

            public Message(Action action, IIdentifier id, Payload payload) {
                this.action = action;
                this.id = id;
                this.payload = payload;
            }

            public Message(Action action, IIdentifier id) {
                this.action = action;
                this.id = id;
                this.payload = null;
            }

            public boolean hasAction() {
                return this.action != null;
            }

            public Action getAction() {
                return this.action;
            }

            public boolean hasId() {
                return this.id != null;
            }

            public IIdentifier getId() {
                return this.id;
            }

            public boolean hasPayload() {
                return this.payload != null;
            }

            public Payload getPayload() {
                return this.payload;
            }

       public Status consistencyCheck() {
            if( !this.hasAction()) return Status.MISSING_ACTION;

            if( !this.hasId()) return Status.MISSING_PROPERTY_ID;

            if(this.action != Action.READ && !this.hasPayload()) {
                return Status.MISSING_PAYLOAD_VALUE;
            }

            return Status.OK;
        }

and then on another file I call

public Status route(IGateway sender, Message msg) {
        Status status = msg.consistencyCheck();

        if (status == Status.OK) {
            if(gateways.containsKey(msg.getId().getChannel().getSubject())) {
               ....
            }
        }

The problem is that Infer reports the call to msg.getId() as a null_dereference even though the consistencyCheck obviously states that such an state is not possible due to the Status.OK return value.

... error: NULL_DEREFERENCE
  object returned by msg.getId() could be null and is dereferenced at line 69

Let me know if you need more information and thanks a lot for the great tool :)

Infer version v0.9.2
OS: Mac OS X 10.11

[jeremydubreil]

Thanks for reporting this. Is Status an enum type or a standard class with static constants ? I will try to reproduce it. It may be that Infer does not recognize that Status.OK is actually different from Status.MISSING_ACTION.

[carocad]

@jeremydubreil Status is a normal very basic enum. Here is the main part in case you need it:

public enum Status {

    OK(0),

    MISSING_ACTION(12),
    MISSING_CHANNEL_ID(13),
    MISSING_PROPERTY_ID(14),
    MISSING_PAYLOAD_VALUE(15),

    public final int code;

    Status(int code) {
        this.code = code;
    }
}

Hope it helps

[xennygrimmato]

@jeremydubreil I encountered an identical false positive today. Any progress on this one?

[jvillard]

I looked a bit into this and can reproduce with the following example:

enum Status {
    OK(0),
    MISSING_PROPERTY_ID(14);

    public final int code;

    Status(int code) {
        this.code = code;
    }
}

class IIdentifier {
  public void getChannel() { }
}

class Message {
  private final IIdentifier id = new IIdentifier();

  public IIdentifier getId() {
    return this.id;
  }

  public Status consistencyCheck() {
    if(this.id == null) return Status.MISSING_PROPERTY_ID;

    return Status.OK;
  }
}

class Foo {
  public Status route(Message msg) {
    Status status = msg.consistencyCheck();

    if (status == Status.OK) {
      msg.getId().getChannel();
    }
    return status;
  }
}

If I make consistencyCheck() return a boolean or an int instead of the enum then infer doesn't report the error. Looking at the debug output of infer, the condition status == Status.OK doesn't remove the other case. Maybe infer thinks they are objects and there are no reasons why they should alias? It seems to compare the addresses of the objects themselves:

n$3=*&status:Status* [line 34];
n$4=*&#GB<>$Status.Status.OK:Status [line 34];
PRUNE(!(n$3 != n$4), true); [line 34];

So, in short, it seems that the support of Java enums could be improved.