facebook / infer

A static analyzer for Java, C, C++, and Objective-C
http://fbinfer.com/
MIT License
14.89k stars 2.01k forks source link

[Java] False positive for null dereference #1644

Open Jiehong opened 2 years ago

Jiehong commented 2 years ago

Information

Logs

Unfortunately, I am unable to create a smaller reproducer so far (and the code where infer finds this is not shareable), but the logs are pretty clear:

source.java:789: error: Null Dereference
  object `inProgress` last assigned on line 788 could be null and is dereferenced by call to `updateInProgressStatus(...)` at line 789.
  787.         final boolean inProgress =
  788.             task.getStatus() != null && task.getStatus().equals(Task.Status.IN_PROGRESS);
  789. >       updateInProgressStatus(connection, task, inProgress);
  790.       }

So, infer thinks that inProgress can be null which is not possible for 2 reasons:

So this is fairly weird.

I think that Infer should know better that a && comparison must return a boolean, but also that boolean types (or any primitive type, cannot be null, by definition). It's a good invariant to check for I think.

Test 1: rewrite the code with an if

If I try to change the code a bit, then infer is happy, even though it's the exact same behaviour:

      final boolean inProgress;
      if (task.getStatus() != null && task.getStatus().equals(Task.Status.IN_PROGRESS)) {
        inProgress = true;
      } else {
        inProgress = false;
      }
      updateInProgressStatus(connection, task, inProgress);

Infer still complains about it:

source.java:793: error: Null Dereference
#14 410.1   object `inProgress` last assigned on line 791 could be null and is dereferenced by call to `updateInProgressStatus(...)` at line 793.
#14 410.1   791.           inProgress = false;
#14 410.1   792.         }
#14 410.1   793. >       updateInProgressStatus(connection, task, inProgress);
#14 410.1   794.       }
#14 410.1   795.

Test 2: Test 1 but with inverted if condition

I was curious to see if inverting the if condition would help infer think it's correct:

      final boolean inProgress;
      if (task.getStatus() == null || !task.getStatus().equals(Task.Status.IN_PROGRESS)) {
        inProgress = false;
      } else {
        inProgress = true;
      }
      updateInProgressStatus(connection, task, inProgress);

But infer still thinks that this isn't correct:

 object `inProgress` last assigned on line 789 could be null and is dereferenced by call to `updateInProgressStatus(...)` at line 793.
#15 422.4   791.           inProgress = true;
#15 422.4   792.         }
#15 422.4   793. >       updateInProgressStatus(connection, task, inProgress);
#15 422.4   794.       }

Test 3: yet another form

This time by assigning the variable first, and overriding it instead:

      boolean inProgress = false;
      if (task.getStatus() != null && task.getStatus().equals(Task.Status.IN_PROGRESS)) {
        inProgress = true;
      }
      updateInProgressStatus(connection, task, inProgress);

But, still the same:

#15 423.7 source.java:791: error: Null Dereference
#15 423.7   object `inProgress` last assigned on line 787 could be null and is dereferenced by call to `updateInProgressStatus(...)` at line 791.
#15 423.7   789.           inProgress = true;
#15 423.7   790.         }
#15 423.7   791. >       updateInProgressStatus(connection, task, inProgress);
#15 423.7   792.       }

Test 4

This time, I remove the if assignment (but then it's no longer strictly equivalent):

      boolean inProgress = false;
      updateInProgressStatus(connection, task, inProgress);

Still, the same:

#15 433.3 source.java:788: error: Null Dereference
#15 433.3   object `inProgress` last assigned on line 787 could be null and is dereferenced by call to `updateInProgressStatus(...)` at line 788.
#15 433.3   787.         boolean inProgress = false;
#15 433.3   788. >       updateInProgressStatus(connection, task, inProgress);
#15 433.3   789.       }
#15 433.3   790.

Test 5

I move that inProgress variable set inside updateInProgressStatus method (first line in the method), and now infer is happy (finally).