Transitively track null assignment in NullabliltySuggest

Reviewed By: jeremydubreil, sblackshear

Differential Revision: D5158809

fbshipit-source-id: 485c58d

infer/src/checkers/NullabilitySuggest.ml

@@ -11,17 +11,42 @@ open! IStd
 module F = Format
 module L = Logging
 
-module Domain =
+module UseDefChain = struct
-  AbstractDomain.FiniteSet(struct
+  type astate =
-    type t = AccessPath.Raw.t * Location.t
+    | NullDef of (Location.t * AccessPath.Raw.t)
+    | DependsOn of (Location.t * AccessPath.Raw.t)
 
-    (* Ignore location while comparing access paths.
+  (* We explicitly write out the comparator here instead of relying on
-     * They are there just for error reporting purpose, and are pretty much irrelevant
+   * [@@deriving compare], as the alternative may not always guarantee the
-     * from the analysis' perspective *)
+   * desirable order. *)
-    let compare (ap0, _) (ap1, _) = [%compare: AccessPath.Raw.t] ap0 ap1
+  let compare_astate lhs rhs = match lhs, rhs with
+    | NullDef lorig, NullDef rorig ->
+        [%compare : Location.t * AccessPath.Raw.t] rorig lorig
+    | DependsOn ldep, DependsOn rdep ->
+        [%compare : Location.t * AccessPath.Raw.t] rdep ldep
+    | NullDef _, DependsOn _ ->
+        1
+    | DependsOn _, NullDef _ ->
+        -1
 
-    let pp fmt (ap, loc) = F.fprintf fmt "(%a, %a)" AccessPath.Raw.pp ap Location.pp loc
+  let (<=) ~lhs ~rhs =
-  end)
+    compare_astate lhs rhs <= 0
+
+  (* Keep only one chain in join/widen as we are going to report only one
+   * trace to the user eventually. *)
+  let join lhs rhs =
+    if (<=) ~lhs ~rhs then rhs else lhs
+
+  let widen ~prev ~next ~num_iters:_ =
+    join prev next
+
+  let pp fmt = function
+    | NullDef (loc, ap) ->
+        F.fprintf fmt "NullDef(%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
+module Domain = AbstractDomain.Map (AccessPath.Raw) (UseDefChain)
 
 (* Right now this is just a placeholder. We'll change it to something useful when necessary *)
 module Summary = Summary.Make(struct
@@ -38,14 +63,23 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   module Domain = Domain
   type nonrec extras = extras
 
-  let is_null = HilExp.is_null_literal
-
   let is_access_nullable ap proc_data =
     match AccessPath.Raw.get_field_and_annotation ap proc_data.ProcData.tenv with
     | Some (_, annot_item) ->
         Annotations.ia_is_nullable annot_item
     | _ -> false
 
+  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))
+    | HilExp.AccessPath ap ->
+        if Domain.mem ap astate then
+          Some (UseDefChain.DependsOn (loc, ap))
+        else
+          None
+    | _ -> None
+
   let exec_instr (astate : Domain.astate) proc_data _ (instr : HilInstr.t) =
     match instr with
     | Assume _ ->
@@ -55,8 +89,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         (* For now we just assume the callee always return non-null *)
         astate
     | Assign (lhs, rhs, loc) ->
-        if is_null rhs && not (is_access_nullable lhs proc_data) then
+        if not (is_access_nullable lhs proc_data) then
-          Domain.add (lhs, loc) astate
+          match nullable_usedef_chain_of rhs lhs astate loc with
+          | Some udchain ->
+              Domain.add lhs udchain astate
+          | None ->
+              astate
         else
           astate
 end
@@ -67,9 +105,38 @@ module Analyzer =
     (LowerHil.Make (TransferFunctions))
 module Interprocedural = AbstractInterpreter.Interprocedural (Summary)
 
+let make_error_trace astate ap ud =
+  let name_of ap =
+    match AccessPath.Raw.get_last_access ap with
+    | Some (AccessPath.FieldAccess field_name) ->
+        "Field " ^ (Fieldname.to_flat_string field_name)
+    | Some (AccessPath.ArrayAccess _) ->
+        "Some array element"
+    | None ->
+        "Variable"
+  in
+  let open UseDefChain in
+  let rec error_trace_impl depth ap = function
+    | NullDef (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)
+    | DependsOn (loc, dep) ->
+        try
+          let ud' = Domain.find dep astate in
+          let msg = F.sprintf "%s could be assigned here" (name_of ap) in
+          let trace_elem = Errlog.make_trace_element depth loc msg [] in
+          Option.map (error_trace_impl (depth+1) dep ud') ~f:(
+            fun (_, trace) -> loc, trace_elem :: trace
+          )
+        with
+          Not_found -> None
+  in
+  error_trace_impl 0 ap ud
+
 let checker callback =
-  let report nullable_aps (proc_data : extras ProcData.t) =
+  let report astate (proc_data : extras ProcData.t) =
-    let report_access_path (ap, loc) =
+    let report_access_path ap udchain =
       let pname = Procdesc.get_proc_name proc_data.pdesc in
       let issue_kind = Localise.to_issue_id Localise.field_should_be_nullable in
       match AccessPath.Raw.get_field_and_annotation ap proc_data.tenv with
@@ -78,10 +145,16 @@ let checker callback =
             F.asprintf "Field %s should be annotated with @Nullable"
               (Fieldname.to_string field_name) in
           let exn = Exceptions.Checkers (issue_kind, Localise.verbatim_desc message) in
-          Reporting.log_warning pname ~loc exn
+          begin
+            match make_error_trace astate ap udchain with
+            | Some (loc, ltr) ->
+                Reporting.log_warning pname ~loc ~ltr exn
+            | None ->
+                Reporting.log_warning pname exn
+          end
       | _ -> ()
     in
-    Domain.iter report_access_path nullable_aps
+    Domain.iter report_access_path astate
   in
   let compute_post (proc_data : extras ProcData.t) =
     (* Assume all fields are not null in the beginning *)

infer/src/checkers/accessPath.ml

@@ -93,6 +93,9 @@ module Raw = struct
     in
     last_access_info_impl tenv base_typ accesses
 
+  let get_last_access (_, accesses) =
+    List.last accesses
+
   let get_field_and_annotation ap tenv =
     match last_access_info ap tenv with
     | Some base_typ, Some access ->

infer/src/checkers/accessPath.mli

@@ -27,6 +27,9 @@ module Raw : sig
       original access path if the access list is empty *)
   val truncate : t -> t
 
+  (** get the last access in the list. returns None if the list is empty *)
+  val get_last_access : t -> access option
+
   (** get the field name and the annotation of the last access in the list of accesses if
       the list is non-empty and the last access is a field access *)
   val get_field_and_annotation : t -> Tenv.t -> (Fieldname.t * Annot.Item.t) option

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

@@ -44,4 +44,45 @@ public class NullableSuggest {
     OtherClass oc = new OtherClass();
     oc.obj3 = null;
   }
+
+  public void assignNullToNullableFieldTransitiveOk(boolean flag) {
+    Object origin = null;
+    Object intermediate = flag ? origin : new Object();
+    obj1 = intermediate;
+  }
+
+  public void assignNullToFieldTransitiveBad(boolean flag) {
+    Object origin = null;
+    Object intermediate = flag ? origin : new Object();
+    obj0 = intermediate;
+  }
+
+  public void assignNullToNullableFieldTransitiveLoopOk(int n) {
+    Object origin = null;
+    Object arr[] = new Object[n];
+    for (int i = 0; i < n; ++i) {
+      arr[i] = origin;
+    }
+    if (n > 0)
+      obj1 = arr[0];
+  }
+
+  public void assignNullToFieldTransitiveLoopBad(int n) {
+    Object origin = null;
+    Object arr[] = new Object[n];
+    for (int i = 0; i < n; ++i) {
+      arr[i] = origin;
+    }
+    if (n > 0)
+      obj0 = arr[0];
+  }
+
+  public void multipleChainsAlwaysSelectShortestBad(boolean flag) {
+    Object o0 = null;
+    Object o1 = null;
+    if (flag)
+      o1 = o0;
+    obj0 = o1;
+    // The analysis should report error trace o1->obj0, rather than o0->o1->obj0
+  }
 }

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

@@ -36,8 +36,11 @@ codetoanalyze/java/checkers/Leaks.java, void Leaks.basicLeakBad(), 2, RESOURCE_L
 codetoanalyze/java/checkers/Leaks.java, void Leaks.doubleLeakBad(), 3, RESOURCE_LEAK, []
 codetoanalyze/java/checkers/NoAllocationExample.java, void NoAllocationExample.directlyAllocatingMethod(), 1, CHECKERS_ALLOCATES_MEMORY, []
 codetoanalyze/java/checkers/NoAllocationExample.java, void NoAllocationExample.indirectlyAllocatingMethod(), 1, CHECKERS_ALLOCATES_MEMORY, []
-codetoanalyze/java/checkers/NullableSuggest.java, void NullableSuggest.assignNullBad(), 1, FIELD_SHOULD_BE_NULLABLE, []
+codetoanalyze/java/checkers/NullableSuggest.java, void NullableSuggest.assignNullBad(), 1, FIELD_SHOULD_BE_NULLABLE, [Field obj0 is assigned null here]
-codetoanalyze/java/checkers/NullableSuggest.java, void NullableSuggest.assignNullToFieldInOtherClassBad(), 2, FIELD_SHOULD_BE_NULLABLE, []
+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/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]