[infer][backend] basic Activity leak checking

Summary:
Creating a persistent reference to an Activity leads to a nasty form of memory leaks (see http://android-developers.blogspot.com/2009/01/avoiding-memory-leaks.html, https://corner.squareup.com/2015/05/leak-canary.html). There are many ways to create a bad persistent reference to an Activity, but the most obvious one is via a static field.

This diff implements a very simple form of Activity leak checking by inspecting postconditions to see if a subtype of Activity is reachable from a static field (and it reports an error if so). This is a very simple and limited form of leak checking that does not understand the Android lifecycle at all. In particular, if one creates a persistent reference to an Activity and then nulls it out in `onDestroy` (a reasonably common pattern), this approach will wrongly report a bug.

infer/src/backend/interproc.ml

@@ -590,6 +590,40 @@ let forward_tabulate cfg tenv =
   done;
   L.d_strln ".... Work list empty. Stop ...."; L.d_ln ()
 
+(** report an error if any Activity is reachable from a static field *)
+let report_activity_leaks 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
+      Prop.compute_reachable_hpreds sigma fld_exps in
+    (* raise an error if any Activity expression is in [reachable_exps] *)
+    list_iter
+      (fun (activity_exp, typ) ->
+         if Sil.ExpSet.mem activity_exp reachable_exps then
+           let err_desc = Errdesc.explain_activity_leak typ fld_name in
+           raise (Exceptions.Activity_leak (err_desc, try assert false with Assert_failure x -> x)))
+      activity_exps in
+  (* get the set of pointed-to expressions of type T <: Activity *)
+  let activity_exps =
+    list_fold_left
+      (fun exps hpred -> match hpred with
+         | Sil.Hpointsto (_, Sil.Eexp (exp, _), Sil.Sizeof (Sil.Tptr (typ, _), _))
+           when AndroidFramework.is_activity typ tenv ->
+             (exp, typ) :: exps
+         | _ -> exps)
+      []
+      sigma in
+  list_iter
+    (function
+      | Sil.Hpointsto (Sil.Lvar pv, Sil.Estruct (static_flds, _), _) when Sil.pvar_is_global pv ->
+          list_iter
+            (fun (f_name, f_strexp) ->
+               if not (Harness.is_generated_field f_name) then
+                 check_reachable_activity_from_fld (f_name, f_strexp) activity_exps) static_flds
+      | _ -> ())
+    sigma
+
 (** remove locals and formals, and check if the address of a stack variable is left in the result *)
 let remove_locals_formals_and_check pdesc p =
   let pname = Cfg.Procdesc.get_proc_name pdesc in
@@ -646,6 +680,7 @@ let extract_specs tenv pdesc pathset : Prop.normal Specs.spec list =
       (* let () = L.out "@.AFTER abs:@.$%a@." (Prop.pp_prop Utils.pe_text) prop'' in *)
       let pre, post = Prop.extract_spec prop'' in
       let pre' = Prop.normalize (Prop.prop_sub sub pre) in
+      if !Sil.curr_language = Sil.Java then report_activity_leaks (Prop.get_sigma post) tenv;
       let post' =
         if Prover.check_inconsistency_base prop then None
         else Some (Prop.normalize (Prop.prop_sub sub post), path) in

infer/src/backend/prop.ml

@@ -1517,17 +1517,20 @@ let prop_sigma_star (p : 'a t) (sigma : Sil.hpred list) : exposed t =
   let sigma' = sigma @ p.sigma in
   { p with sigma = sigma' }
 
+(** return the set of subexpressions of [strexp] *)
+let strexp_get_exps strexp =
+  let rec strexp_get_exps_rec exps = function
+    | Sil.Eexp (Sil.Const (Sil.Cexn e), _) -> Sil.ExpSet.add e exps
+    | Sil.Eexp (e, _) -> Sil.ExpSet.add e exps
+    | Sil.Estruct (flds, _) ->
+        list_fold_left (fun exps (_, strexp) -> strexp_get_exps_rec exps strexp) exps flds
+    | Sil.Earray (_, elems, _) ->
+        list_fold_left (fun exps (_, strexp) -> strexp_get_exps_rec exps strexp) exps elems in
+  strexp_get_exps_rec Sil.ExpSet.empty strexp
+
 (** get the set of expressions on the righthand side of [hpred] *)
 let hpred_get_targets = function
-  | Sil.Hpointsto (_, rhs, _) ->
-      let rec collect_exps exps = function
-        | Sil.Eexp (Sil.Const (Sil.Cexn e), _) -> Sil.ExpSet.add e exps
-        | Sil.Eexp (e, _) -> Sil.ExpSet.add e exps
-        | Sil.Estruct (flds, _) ->
-            list_fold_left (fun exps (_, strexp) -> collect_exps exps strexp) exps flds
-        | Sil.Earray (_, elems, _) ->
-            list_fold_left (fun exps (index, strexp) -> collect_exps exps strexp) exps elems in
-      collect_exps Sil.ExpSet.empty rhs
+  | Sil.Hpointsto (_, rhs, _) -> strexp_get_exps rhs
   | Sil.Hlseg (_, _, _, e, el) ->
       list_fold_left (fun exps e -> Sil.ExpSet.add e exps) Sil.ExpSet.empty (e :: el)
   | Sil.Hdllseg (_, _, _, oB, oF, iB, el) ->

infer/src/backend/prop.mli

@@ -461,6 +461,9 @@ val prop_iter_gc_fields : unit prop_iter -> unit prop_iter
 
 val find_equal_formal_path : exp -> 'a t -> Sil.exp option
 
+(** return the set of subexpressions of [strexp] *)
+val strexp_get_exps : Sil.strexp -> Sil.ExpSet.t
+
 (** get the set of expressions on the righthand side of [hpred] *)
 val hpred_get_targets : Sil.hpred -> Sil.ExpSet.t
 

infer/src/harness/harness.ml

@@ -28,6 +28,13 @@ let insert_after lst test to_insert =
     | [] -> lst in
   insert_rec lst []
 
+(* clear indicator of artificiality, as any real field must have a non-negative offset *)
+let generated_field_offset = -1
+
+(** Return true if [fieldname] was created by the harness generation *)
+let is_generated_field fieldname =
+  Ident.fieldname_offset fieldname = generated_field_offset
+
 (** find callees that register callbacks and add instrumentation to extract the callback.
     return the set of new global static fields created to extract callbacks and their types *)
 let extract_callbacks procdesc cfg_file cfg tenv harness_name harness_lvar callback_fields =
@@ -55,7 +62,7 @@ let extract_callbacks procdesc cfg_file cfg tenv harness_name harness_lvar callb
           match AndroidFramework.get_callback_registered_by callee args tenv with
           | Some (cb_obj, (Sil.Tptr (cb_typ, Sil.Pk_pointer) as ptr_to_cb_typ)) ->
               let callback_fld_name = create_descriptive_callback_name ptr_to_cb_typ loc in
-              let created_fld = Ident.create_fieldname callback_fld_name 0 in
+              let created_fld = Ident.create_fieldname callback_fld_name generated_field_offset in
               (* create a function that takes the type of the harness class as an argument and modifies
                * the instruction set with callback extraction code. we do this because we need to know
                * the typ of the harness class before we can write to any of its fields, but we cannot

infer/src/harness/harness.mli

@@ -9,5 +9,8 @@
 
 (** Automatically create a harness method to exercise code under test *)
 
+(** Return true if [fieldname] was created by the harness generation *)
+val is_generated_field : Ident.fieldname -> bool
+
 (** Generate a harness method for exe_env and add it to the execution environment *)
 val create_harness : DB.source_file Procname.Map.t -> Sil.tenv -> unit

infer/tests/codetoanalyze/java/infer/ActivityLeaks.java

@@ -0,0 +1,83 @@
+package codetoanalyze.java.infer;
+
+import android.app.Activity;
+import android.content.Context;
+
+public class ActivityLeaks extends Activity {
+
+    static Object sFld;
+
+    public void directLeak() {
+        sFld = this;
+    }
+
+    public void leakThenFix() {
+        sFld = this;
+        sFld = null;
+    }
+
+    public void nonActivityNoLeak() {
+        sFld = new Object();
+    }
+
+    static class Obj {
+        public Object f;
+    }
+
+    public void indirectLeak() {
+        Obj o = new Obj();
+        o.f = this;
+        sFld = o;
+    }
+
+    public void indirectLeakThenFix() {
+        Obj o = new Obj();
+        o.f = this;
+        sFld = o;
+        o.f = null;
+    }
+
+    class NonStaticInner {}
+
+    public void nonStaticInnerClassLeak() {
+        sFld = new NonStaticInner();
+    }
+
+    public void nonStaticInnerClassLeakThenFix() {
+        sFld = new NonStaticInner();
+        sFld = null;
+    }
+
+    private Object o;
+
+    public void leakAfterInstanceFieldWrite() {
+        this.o = new Object();
+        sFld = this;
+    }
+
+    public static class Singleton {
+
+        private static Singleton instance;
+        private Context context;
+
+        private Singleton(Context context) {
+            this.context = context;
+        }
+
+        public static Singleton getInstance(Context context) {
+            if(instance == null) {
+                instance = new Singleton(context);
+            }
+            return instance;
+        }
+    }
+
+    Singleton singletonLeak() {
+        return Singleton.getInstance(this);
+    }
+
+    Singleton singletonNoLeak() {
+        return Singleton.getInstance(this.getApplicationContext());
+    }
+
+}

infer/tests/endtoend/java/infer/ActivityLeaksTest.java

@@ -0,0 +1,60 @@
+/*
+* Copyright (c) 2013 - present Facebook, Inc.
+* All rights reserved.
+*
+* This source code is licensed under the BSD style license found in the
+* LICENSE file in the root directory of this source tree. An additional grant
+* of patent rights can be found in the PATENTS file in the same directory.
+*/
+
+package endtoend.java.infer;
+
+import static org.hamcrest.MatcherAssert.assertThat;
+import static utils.matchers.ResultContainsExactly.containsExactly;
+
+import org.junit.BeforeClass;
+import org.junit.Test;
+
+import java.io.IOException;
+
+import utils.InferException;
+import utils.InferResults;
+
+public class ActivityLeaksTest {
+
+  public static final String SOURCE_FILE =
+      "infer/tests/codetoanalyze/java/infer/ActivityLeaks.java";
+
+  public static final String ACTIVITY_LEAK = "ACTIVITY_LEAK";
+
+  private static InferResults inferResults;
+
+  @BeforeClass
+  public static void loadResults() throws InterruptedException, IOException {
+    inferResults = InferResults.loadInferResults(
+        ActivityLeaksTest.class,
+        SOURCE_FILE);
+  }
+
+  @Test
+  public void matchErrors()
+      throws IOException, InterruptedException, InferException {
+    String[] methods = {
+        "directLeak",
+        "indirectLeak",
+        "nonStaticInnerClassLeak",
+        "leakAfterInstanceFieldWrite",
+        "singletonLeak"
+    };
+    assertThat(
+        "Results should contain " + ACTIVITY_LEAK,
+        inferResults,
+        containsExactly(
+            ACTIVITY_LEAK,
+            SOURCE_FILE,
+            methods
+        )
+    );
+  }
+
+}