From 9cf74e0ce53425f9e968b94eaddebc518957f5f9 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Thu, 30 Jul 2015 09:13:36 -0600 Subject: [PATCH] [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 | 35 ++++++++ infer/src/backend/prop.ml | 21 +++-- infer/src/backend/prop.mli | 3 + infer/src/harness/harness.ml | 9 +- infer/src/harness/harness.mli | 3 + .../java/infer/ActivityLeaks.java | 83 +++++++++++++++++++ .../java/infer/ActivityLeaksTest.java | 60 ++++++++++++++ 7 files changed, 204 insertions(+), 10 deletions(-) create mode 100644 infer/tests/codetoanalyze/java/infer/ActivityLeaks.java create mode 100644 infer/tests/endtoend/java/infer/ActivityLeaksTest.java diff --git a/infer/src/backend/interproc.ml b/infer/src/backend/interproc.ml index 99fbc9734..4dd381eb4 100644 --- a/infer/src/backend/interproc.ml +++ b/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 diff --git a/infer/src/backend/prop.ml b/infer/src/backend/prop.ml index 131f5b4e1..8f3e931dc 100644 --- a/infer/src/backend/prop.ml +++ b/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) -> diff --git a/infer/src/backend/prop.mli b/infer/src/backend/prop.mli index 77e0c0e75..c77022ded 100644 --- a/infer/src/backend/prop.mli +++ b/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 diff --git a/infer/src/harness/harness.ml b/infer/src/harness/harness.ml index 855d71fb7..f67baa22b 100644 --- a/infer/src/harness/harness.ml +++ b/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 diff --git a/infer/src/harness/harness.mli b/infer/src/harness/harness.mli index f0c979e8e..cecd5c82e 100644 --- a/infer/src/harness/harness.mli +++ b/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 diff --git a/infer/tests/codetoanalyze/java/infer/ActivityLeaks.java b/infer/tests/codetoanalyze/java/infer/ActivityLeaks.java new file mode 100644 index 000000000..aa76cef94 --- /dev/null +++ b/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()); + } + +} diff --git a/infer/tests/endtoend/java/infer/ActivityLeaksTest.java b/infer/tests/endtoend/java/infer/ActivityLeaksTest.java new file mode 100644 index 000000000..d899478dd --- /dev/null +++ b/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 + ) + ); + } + +}