[infer][java] Suggest @Nullable on fields that are compared to null

Reviewed By: sblackshear

Differential Revision: D5189028

fbshipit-source-id: 708423b

infer/src/checkers/NullabilitySuggest.ml

@@ -15,7 +15,8 @@ module MF = MarkupFormatter
 module UseDefChain = struct
   type astate =
     | DependsOn of (Location.t * AccessPath.Raw.t)
-    | NullDef of (Location.t * AccessPath.Raw.t)
+    | NullDefCompare of (Location.t * AccessPath.Raw.t)
+    | NullDefAssign of (Location.t * AccessPath.Raw.t)
   [@@deriving compare]
 
   let (<=) ~lhs ~rhs =
@@ -30,8 +31,10 @@ module UseDefChain = struct
     join prev next
 
   let pp fmt = function
-    | NullDef (loc, ap) ->
-        F.fprintf fmt "NullDef(%a, %a)" Location.pp loc AccessPath.Raw.pp ap
+    | NullDefAssign (loc, ap) ->
+        F.fprintf fmt "NullDefAssign(%a, %a)" Location.pp loc AccessPath.Raw.pp ap
+    | NullDefCompare (loc, ap) ->
+        F.fprintf fmt "NullDefCompare(%a, %a)" Location.pp loc AccessPath.Raw.pp ap
     | DependsOn (loc, ap) ->
         F.fprintf fmt "DependsOn(%a, %a)" Location.pp loc AccessPath.Raw.pp ap
 end
@@ -61,19 +64,40 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   let nullable_usedef_chain_of exp lhs astate loc =
     match exp with
     | HilExp.Constant (Cint n) when IntLit.isnull n ->
-        Some (UseDefChain.NullDef (loc, lhs))
+        Some (UseDefChain.NullDefAssign (loc, lhs))
     | HilExp.AccessPath ap ->
-        if Domain.mem ap astate then
-          Some (UseDefChain.DependsOn (loc, ap))
-        else
-          None
+        begin
+          try
+            match Domain.find ap astate with
+            | UseDefChain.NullDefCompare _ ->
+                (* Stop NullDefCompare from propagating here because we want to prevent
+                 * the checker from suggesting @Nullable on y in the following case:
+                 * if (x == null) ... else { y = x; } *)
+                None
+            | _ ->
+                Some (UseDefChain.DependsOn (loc, ap))
+          with
+          | Not_found -> None
+        end
+    | _ -> None
+
+  let extract_null_compare_expr = function
+    | HilExp.BinaryOperator ((Eq | Ne), HilExp.AccessPath ap, exp)
+    | HilExp.BinaryOperator ((Eq | Ne), exp, HilExp.AccessPath ap) ->
+        Option.some_if (HilExp.is_null_literal exp) ap
     | _ -> None
 
   let exec_instr (astate : Domain.astate) proc_data _ (instr : HilInstr.t) =
     match instr with
-    | Assume _ ->
-        (* For now we just assume that conditionals does not have any implications on nullability *)
-        astate
+    | Assume (expr, _, _, loc) ->
+        begin
+          match extract_null_compare_expr expr with
+          | Some ap when not (is_access_nullable ap proc_data) ->
+              let udchain = UseDefChain.NullDefCompare (loc, ap) in
+              Domain.add ap udchain astate
+          | _ ->
+              astate
+        end
     | Call _ ->
         (* For now we just assume the callee always return non-null *)
         astate
@@ -106,10 +130,14 @@ let make_error_trace astate ap ud =
   in
   let open UseDefChain in
   let rec error_trace_impl depth ap = function
-    | NullDef (loc, src) ->
+    | NullDefAssign (loc, src) ->
         let msg = F.sprintf "%s is assigned null here" (name_of src) in
         let ltr = [Errlog.make_trace_element depth loc msg []] in
         Some (loc, ltr)
+    | NullDefCompare (loc, src) ->
+        let msg = F.sprintf "%s is compared to null here" (name_of src) in
+        let ltr = [Errlog.make_trace_element depth loc msg []] in
+        Some (loc, ltr)
     | DependsOn (loc, dep) ->
         try
           let ud' = Domain.find dep astate in

infer/tests/codetoanalyze/java/checkers/ExpensiveCallExample.java

@@ -15,7 +15,7 @@ import android.view.View;
 
 import com.facebook.infer.annotation.Expensive;
 import com.facebook.infer.annotation.PerformanceCritical;
-
+import javax.annotation.Nullable;
 
 interface AnnotatedInterface {
 
@@ -100,7 +100,7 @@ class PerformanceCriticalSubclass extends PerformanceCriticalClass {
 
 public class ExpensiveCallExample implements AnnotatedInterface {
 
-  Other mOther;
+  @Nullable Other mOther;
 
   void nonExpensiveMethod() {}
 

infer/tests/codetoanalyze/java/checkers/NullableSuggest.java

@@ -63,8 +63,9 @@ public class NullableSuggest {
     for (int i = 0; i < n; ++i) {
       arr[i] = origin;
     }
-    if (n > 0)
+    if (n > 0) {
       obj1 = arr[0];
+    }
   }
 
   public void assignNullToFieldTransitiveLoopBad(int n) {
@@ -73,16 +74,35 @@ public class NullableSuggest {
     for (int i = 0; i < n; ++i) {
       arr[i] = origin;
     }
-    if (n > 0)
+    if (n > 0) {
       obj0 = arr[0];
+    }
   }
 
   public void multipleChainsAlwaysSelectShortestBad(boolean flag) {
     Object o0 = null;
     Object o1 = null;
-    if (flag)
+    if (flag) {
       o1 = o0;
+    }
     obj0 = o1;
     // The analysis should report error trace o1->obj0, rather than o0->o1->obj0
   }
+
+  public void compareNullToFieldBad() {
+    OtherClass oc = new OtherClass();
+    if (obj0 == null) {
+      // Pretend that we did something here...
+    }
+    else {
+      // The analysis should not suggest @Nullable on OtherClass.obj2 here
+      oc.obj2 = obj0;
+    }
+  }
+
+  public void compareNullToNullableFieldOk() {
+    if (obj1 == null) {
+      // Pretend that we did something here...
+    }
+  }
 }

infer/tests/codetoanalyze/java/checkers/issues.exp

@@ -40,7 +40,8 @@ codetoanalyze/java/checkers/NullableSuggest.java, void NullableSuggest.assignNul
 codetoanalyze/java/checkers/NullableSuggest.java, void NullableSuggest.assignNullToFieldInOtherClassBad(), 2, FIELD_SHOULD_BE_NULLABLE, [Field obj2 is assigned null here]
 codetoanalyze/java/checkers/NullableSuggest.java, void NullableSuggest.assignNullToFieldTransitiveBad(boolean), 3, FIELD_SHOULD_BE_NULLABLE, [Field obj0 could be assigned here,Variable could be assigned here,Variable could be assigned here,Variable is assigned null here]
 codetoanalyze/java/checkers/NullableSuggest.java, void NullableSuggest.assignNullToFieldTransitiveLoopBad(int), 7, FIELD_SHOULD_BE_NULLABLE, [Field obj0 could be assigned here,Some array element could be assigned here,Variable is assigned null here]
-codetoanalyze/java/checkers/NullableSuggest.java, void NullableSuggest.multipleChainsAlwaysSelectShortestBad(boolean), 5, FIELD_SHOULD_BE_NULLABLE, [Field obj0 could be assigned here,Variable is assigned null here]
+codetoanalyze/java/checkers/NullableSuggest.java, void NullableSuggest.compareNullToFieldBad(), 2, FIELD_SHOULD_BE_NULLABLE, [Field obj0 is compared to null here]
+codetoanalyze/java/checkers/NullableSuggest.java, void NullableSuggest.multipleChainsAlwaysSelectShortestBad(boolean), 6, FIELD_SHOULD_BE_NULLABLE, [Field obj0 could be assigned here,Variable is assigned null here]
 codetoanalyze/java/checkers/PrintfArgsChecker.java, void PrintfArgsChecker.formatStringIsNotLiteral(PrintStream), 2, CHECKERS_PRINTF_ARGS, [Format string must be string literal]
 codetoanalyze/java/checkers/PrintfArgsChecker.java, void PrintfArgsChecker.stringInsteadOfInteger(PrintStream), 1, CHECKERS_PRINTF_ARGS, [printf(...) at line 40: parameter 2 is expected to be of type java.lang.Integer but java.lang.String was given.]
 codetoanalyze/java/checkers/PrintfArgsChecker.java, void PrintfArgsChecker.wrongNumberOfArguments(PrintStream), 1, CHECKERS_PRINTF_ARGS, [format string arguments don't mach provided arguments in printf(...) at line 44]