[infer][nullable checker] treat all aliases as not null when one is checked for null

Reviewed By: sblackshear

Differential Revision: D6235972

fbshipit-source-id: 2e4023b

infer/src/checkers/NullabilityCheck.ml

@@ -175,6 +175,19 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   let find_nullable_ap ap (aps, _) = NullableAP.find ap aps
 
   let assume_pnames_notnull ap (aps, checked_pnames) : Domain.astate =
+    let remove_call_sites ap aps =
+      let add_diff (to_remove: CallSites.t) ap call_sites map =
+        let remaining_call_sites = CallSites.diff call_sites to_remove in
+        if CallSites.is_empty remaining_call_sites then map
+        else NullableAP.add ap remaining_call_sites map
+      in
+      match NullableAP.find_opt ap aps with
+      | None ->
+          aps
+      | Some call_sites ->
+          let updated_aps = NullableAP.fold (add_diff call_sites) aps NullableAP.empty in
+          updated_aps
+    in
     let updated_pnames =
       try
         let call_sites = NullableAP.find ap aps in
@@ -183,7 +196,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           call_sites checked_pnames
       with Not_found -> checked_pnames
     in
-    (NullableAP.remove ap aps, updated_pnames)
+    (remove_call_sites ap aps, updated_pnames)
 
 
   let rec longest_nullable_prefix ap ((nulable_aps, _) as astate) =

infer/tests/codetoanalyze/cpp/nullable/issues.exp

@@ -16,6 +16,7 @@ codetoanalyze/cpp/nullable/method.cpp, callMethodOnNullableObjectBad, 1, NULL_DE
 codetoanalyze/cpp/nullable/method.cpp, callMethodOnNullableObjectOkay, 2, NULL_TEST_AFTER_DEREFERENCE, [start of procedure callMethodOnNullableObjectOkay(),start of procedure mayReturnNullObject,Condition is false,return from a call to T_mayReturnNullObject,Condition is false]
 codetoanalyze/cpp/nullable/method.cpp, dereferenceFieldOfNullableObjectBad, 2, NULLABLE_DEREFERENCE, [dereference of &p,assignment of the nullable value,definition of mayReturnNullObject]
 codetoanalyze/cpp/nullable/method.cpp, dereferenceFieldOfNullableObjectBad, 2, NULL_DEREFERENCE, [start of procedure dereferenceFieldOfNullableObjectBad(),start of procedure mayReturnNullObject,Condition is true,return from a call to T_mayReturnNullObject]
+codetoanalyze/cpp/nullable/method.cpp, dereferenceOfAliasesCheckedForNullOkay, 3, NULL_TEST_AFTER_DEREFERENCE, [start of procedure dereferenceOfAliasesCheckedForNullOkay(),start of procedure mayReturnNullObject,Condition is false,return from a call to T_mayReturnNullObject,Condition is false]
 codetoanalyze/cpp/nullable/method.cpp, methodAlwaysCheckedForNullOkay, 1, NULL_TEST_AFTER_DEREFERENCE, [start of procedure methodAlwaysCheckedForNullOkay(),Condition is true,start of procedure mayReturnNullObject,Condition is false,return from a call to T_mayReturnNullObject,Condition is false]
 codetoanalyze/cpp/nullable/method.cpp, methodAlwaysCheckedForNullOkay, 2, NULL_DEREFERENCE, [start of procedure methodAlwaysCheckedForNullOkay(),Condition is true,start of procedure mayReturnNullObject,Condition is false,return from a call to T_mayReturnNullObject,Condition is true,start of procedure mayReturnNullObject,Condition is false,return from a call to T_mayReturnNullObject]
 codetoanalyze/cpp/nullable/method.cpp, methodCallOnFieldOfNullableObjectBad, 2, NULLABLE_DEREFERENCE, [dereference of &p,assignment of the nullable value,definition of mayReturnNullObject]

infer/tests/codetoanalyze/cpp/nullable/method.cpp

@@ -141,3 +141,11 @@ void onlyReportOnceBad(T* t) {
   // ...
   t->mayReturnNullObject()->doSomething(); // does not report here
 }
+
+void dereferenceOfAliasesCheckedForNullOkay(T* t) {
+  T* s = t->mayReturnNullObject();
+  T* r = s;
+  if (r != nullptr) {
+    s->doSomething();
+  }
+}

infer/tests/codetoanalyze/java/checkers/NullableViolation.java

@@ -98,4 +98,19 @@ public class NullableViolation {
     Object object = getNullableObject();
     object = "Hello";
   }
+
+  void deferenceAliasOfNullableValueCheckedForNullOkay() {
+    T t = returnsNullable();
+    T s = t;
+    if (t != null) {
+      s.x = 42;
+    }
+  }
+
+  void dereferenceWithAssignmentExpressionsOkay() {
+    T t;
+    while ((t = returnsNullable()) != null) {
+      t.doSomething();
+    }
+  }
 }