better error messages for Activity leaks

Reviewed By: cristianoc, jeremydubreil

Differential Revision: D2584915

fb-gh-sync-id: 5b756d2

infer/src/backend/errdesc.ml

@@ -27,8 +27,8 @@ let hpred_is_open_resource prop = function
       None
 
 (** Produce a description of a persistent reference to an Android Activity *)
-let explain_activity_leak pname activity_typ fieldname =
+let explain_activity_leak pname activity_typ fieldname error_path =
-  Localise.desc_activity_leak pname activity_typ fieldname
+  Localise.desc_activity_leak pname activity_typ fieldname error_path
 
 (** Explain a deallocate stack variable error *)
 let explain_deallocate_stack_var pvar ra =

infer/src/backend/errdesc.mli

@@ -41,7 +41,8 @@ val find_boolean_assignment : Cfg.Node.t -> Sil.pvar -> bool -> Cfg.Node.t optio
 val exp_rv_dexp : Cfg.Node.t -> Sil.exp -> Sil.dexp option
 
 (** Produce a description of a persistent reference to an Android Activity *)
-val explain_activity_leak : Procname.t -> Sil.typ -> Ident.fieldname -> Localise.error_desc
+val explain_activity_leak : Procname.t -> Sil.typ -> Ident.fieldname ->
+  (Ident.fieldname option * Sil.typ) list -> Localise.error_desc
 
 (** Produce a description of a pointer dangerously coerced to a boolean in a comparison *)
 val explain_bad_pointer_comparison : Sil.exp -> Cfg.Node.t -> Location.t -> Localise.error_desc

infer/src/backend/interproc.ml

@@ -612,14 +612,15 @@ let forward_tabulate cfg tenv =
 let report_activity_leaks pname sigma tenv =
   (* report an error if an expression in [activity_exps] is reachable from [field_strexp] *)
   let check_reachable_activity_from_fld (fld_name, fld_strexp) activity_exps =
-    let _, reachable_exps =
+    let fld_exps = Prop.strexp_get_exps fld_strexp in
-      let fld_exps = Prop.strexp_get_exps fld_strexp in
+    let reachable_hpreds, reachable_exps =
       Prop.compute_reachable_hpreds sigma fld_exps in
     (* raise an error if any Activity expression is in [reachable_exps] *)
     IList.iter
       (fun (activity_exp, typ) ->
          if Sil.ExpSet.mem activity_exp reachable_exps then
-           let err_desc = Errdesc.explain_activity_leak pname typ fld_name in
+           let leak_path = Prop.get_fld_typ_path fld_exps activity_exp reachable_hpreds in
+           let err_desc = Errdesc.explain_activity_leak pname typ fld_name leak_path in
            let exn = Exceptions.Activity_leak
                (err_desc, try assert false with Assert_failure x -> x) in
            Reporting.log_error pname exn)

infer/src/backend/localise.ml

@@ -365,15 +365,28 @@ let java_unchecked_exn_desc proc_name exn_name pre_str : error_desc =
     "can throw "^(Mangled.to_string exn_name);
     "whenever "^pre_str], None, [])
 
-let desc_activity_leak pname activity_typ fieldname : error_desc =
+let desc_activity_leak pname activity_typ fieldname leak_path : error_desc =
-  let pname_str = Procname.java_get_class pname ^ "." ^ Procname.java_get_method pname in
-  (* intentionally omit space; [typ_to_string] adds an extra space *)
-  let activity_str = Sil.typ_to_string activity_typ ^ "may leak via" in
   let fld_str = Ident.fieldname_to_string fieldname in
-  let leak_msg =
+  let leak_root =
-    if fld_str = "android.os.Handler.sFakeHandlerQueue" then "call to Handler.postDelayed"
+    if fld_str = "android.os.Handler.sFakeHandlerQueue"
-    else "assignment to static field " ^ fld_str in
+    then " runnable passed to Handler.postDelayed |->\n "
-  (["Activity"; activity_str; leak_msg; "during call to"; pname_str] , None, [])
+    else " static field " ^ fld_str ^ " |->\n " in
+  let leak_path_entry_to_str acc entry =
+    let entry_str = match entry with
+      | (Some fld, _) -> Ident.fieldname_to_string fld
+      | (None, typ) -> Sil.typ_to_string typ in
+    (* intentionally omit space; [typ_to_string] adds an extra space *)
+    acc ^ entry_str ^ " |->\n " in
+  let activity_str = Sil.typ_to_string activity_typ in
+  let path_str =
+    let path_prefix =
+      if leak_path = [] then "leaked "
+      else (IList.fold_left leak_path_entry_to_str "" leak_path) ^ " leaked " in
+    path_prefix ^ activity_str in
+  let preamble =
+    let pname_str = Procname.java_get_class pname ^ "." ^ Procname.java_get_method pname in
+    "Activity " ^ activity_str ^ "may leak during method" ^ pname_str ^ ":\n" in
+  ([preamble; leak_root; path_str], None, [])
 
 let desc_assertion_failure loc : error_desc =
   (["could be raised"; at_line (Tags.create ()) loc], None, [])

infer/src/backend/localise.mli

@@ -195,7 +195,8 @@ val desc_null_test_after_dereference : string -> int -> Location.t -> error_desc
 
 val java_unchecked_exn_desc : Procname.t -> Mangled.t -> string -> error_desc
 
-val desc_activity_leak : Procname.t -> Sil.typ -> Ident.fieldname -> error_desc
+val desc_activity_leak : Procname.t -> Sil.typ -> Ident.fieldname ->
+  (Ident.fieldname option * Sil.typ) list -> error_desc
 
 (* Create human-readable error description for assertion failures *)
 val desc_assertion_failure : Location.t -> error_desc

infer/src/backend/prop.ml

@@ -1553,6 +1553,35 @@ let compute_reachable_hpreds sigma exps =
     else compute_reachable_hpreds_rec sigma (reach', exps') in
   compute_reachable_hpreds_rec sigma (Sil.HpredSet.empty, exps)
 
+(** produce a (fieldname, typ) from one of the [src_exps] to [snk_exp] using [reachable_hpreds] *)
+let rec get_fld_typ_path src_exps snk_exp reachable_hpreds =
+  let strexp_matches target_exp = function
+    | (_, Sil.Eexp (e, _)) -> Sil.exp_equal target_exp e
+    | _ -> false in
+  let (snk_exp, path) =
+    Sil.HpredSet.fold
+      (fun hpred (snk_exp, path) -> match hpred with
+         | Sil.Hpointsto (lhs, Sil.Estruct (flds, inst), Sil.Sizeof (typ, _)) ->
+             (match
+                IList.fold_left
+                  (fun acc fld -> if strexp_matches snk_exp fld then Some fld else acc)
+                  None
+                  flds with
+             | Some (fld, _) -> (lhs, (Some fld, typ) :: path)
+             | None -> (snk_exp, path))
+         | Sil.Hpointsto (lhs, Sil.Earray (_, elems, _), Sil.Sizeof (typ, _)) ->
+             if IList.exists (fun pair -> strexp_matches snk_exp pair) elems
+             then
+               (* None means "no field name" ~=~ nameless array index *)
+               (lhs, (None, typ) :: path)
+             else (snk_exp, path)
+         | _ -> (snk_exp, path))
+      reachable_hpreds
+      (snk_exp, []) in
+  if Sil.ExpSet.mem snk_exp src_exps then path
+  else get_fld_typ_path src_exps snk_exp reachable_hpreds
+
+
 (** filter [pi] by removing the pure atoms that do not contain an expression in [exps] *)
 let compute_reachable_atoms pi exps =
   let rec exp_contains = function

infer/src/backend/prop.mli

@@ -483,6 +483,10 @@ val hpred_get_targets : Sil.hpred -> Sil.ExpSet.t
     [exps] *)
 val compute_reachable_hpreds : hpred list -> Sil.ExpSet.t -> Sil.HpredSet.t * Sil.ExpSet.t
 
+(** produce a (fieldname, typ) from one of the [src_exps] to [snk_exp] using [reachable_hpreds] *)
+val get_fld_typ_path : Sil.ExpSet.t -> Sil.exp -> Sil.HpredSet.t ->
+  (Ident.fieldname option * Sil.typ) list
+
 (** filter [pi] by removing the pure atoms that do not contain an expression in [exps] *)
 val compute_reachable_atoms : Sil.atom list -> Sil.ExpSet.t -> Sil.atom list