[starvation][whole-program] analyze constructors for initial attribute state

Summary:
A current blind spot is when object construction stores specific executors / runnables to object fields, which are then never mutated and accessed from normal methods.  IOW the attributes established in the constructor are necessary to report properly inside a normal method (assuming these attributes are not invalidated by method code).

To achieve this, first we retain a subset of the final state attributes in the summary (only those that affect instance variables, in constructor methods). Then, when we analyse a non-constructor method:
- we analyse all constructors
- remove all attributes from the attribute map whose key is not an expression of the form `this.x. ...`
- re-localise all remaining keys so that they appear as rooted in the `this` local variable of the current procedure
- join (intersect) all such attribute maps
- use the result in place of initial state as far as the attribute map is concerned for the analysis of the current procedure, which can now start.

This means we can catch idioms that use side-effectful initialisation for configuring certain object fields like executors or runnables.

Reviewed By: jvillard

Differential Revision: D18707890

fbshipit-source-id: 42ac6108f

infer/src/IR/Pvar.mli

@@ -86,7 +86,7 @@ val is_cpp_temporary : t -> bool
 (** return true if this pvar represents a C++ temporary object (see http://en.cppreference.com/w/cpp/language/lifetime) *)
 
 val mk : Mangled.t -> Typ.Procname.t -> t
-(** [mk name proc_name suffix] creates a program var with the given function name and suffix *)
+(** [mk name proc_name] creates a program var with the given function name *)
 
 val mk_abduced_ref_param : Typ.Procname.t -> int -> Location.t -> t
 (** create an abduced variable for a parameter passed by reference *)

infer/src/IR/Var.ml

@@ -44,6 +44,8 @@ let is_footprint = function ProgramVar _ -> false | LogicalVar id -> Ident.is_fo
 
 let is_none = function LogicalVar id -> Ident.is_none id | _ -> false
 
+let is_this = function ProgramVar pv -> Pvar.is_this pv | LogicalVar _ -> false
+
 let get_declaring_function = function
   | LogicalVar _ ->
       None

infer/src/IR/Var.mli

@@ -41,6 +41,8 @@ val is_footprint : t -> bool
 
 val is_none : t -> bool
 
+val is_this : t -> bool
+
 val appears_in_source_code : t -> bool
 (** return true if this variable appears in source code (i.e., is not a LogicalVar or a
     frontend-generated ProgramVar) *)

infer/src/concurrency/starvation.ml

@@ -123,7 +123,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
            {astate with attributes} )
 
 
-  let do_call ProcData.{tenv; summary} lhs callee actuals loc astate =
+  let do_call ProcData.{tenv; summary} lhs callee actuals loc (astate : Domain.t) =
     let open Domain in
     let make_ret_attr return_attribute = {empty_summary with return_attribute} in
     let make_thread thread = {empty_summary with thread} in
@@ -244,6 +244,53 @@ end
 
 module Analyzer = LowerHil.MakeAbstractInterpreter (TransferFunctions (ProcCfg.Normal))
 
+(** Before analyzing Java instance methods (non-constructor, non-static), compute the attributes
+    of instance variables that all constructors agree on after termination. *)
+let add_constructor_attributes tenv procname (astate : Domain.t) =
+  let open Domain in
+  let skip_constructor_analysis =
+    match procname with
+    | Typ.Procname.Java jname ->
+        (* constructor attributes affect instance fields, which static methods cannot access;
+           ditto for the class initializer; finally, don't recurse if already in constructor *)
+        Typ.Procname.Java.(is_static jname || is_constructor jname || is_class_initializer jname)
+    | _ ->
+        (* don't do anything for non-Java code *)
+        true
+  in
+  if skip_constructor_analysis then astate
+  else
+    (* make a local [this] variable, for replacing all constructor attribute map keys' roots *)
+    let local_this = Pvar.mk Mangled.this procname |> Var.of_pvar in
+    let make_local exp =
+      let var, typ = HilExp.AccessExpression.get_base exp in
+      let newvar =
+        assert (Var.is_this var) ;
+        local_this
+      in
+      HilExp.AccessExpression.replace_base ~remove_deref_after_base:false (newvar, typ) exp
+    in
+    let localize_attrs attributes =
+      AttributeDomain.(fold (fun exp attr acc -> add (make_local exp) attr acc) attributes empty)
+    in
+    (* get class of current procedure *)
+    Typ.Procname.get_class_type_name procname
+    (* retrieve its definition *)
+    |> Option.bind ~f:(Tenv.lookup tenv)
+    (* get the list of methods in the class *)
+    |> Option.value_map ~default:[] ~f:(fun (tstruct : Typ.Struct.t) -> tstruct.methods)
+    (* keep only the constructors *)
+    |> List.filter ~f:Typ.Procname.(function Java jname -> Java.is_constructor jname | _ -> false)
+    (* get the summaries of the constructors *)
+    |> List.filter_map ~f:Payload.read_toplevel_procedure
+    (* make instances of [this] local to the current procedure and select only the attributes *)
+    |> List.map ~f:(fun (summary : Domain.summary) -> localize_attrs summary.attributes)
+    (* join all the attribute maps together *)
+    |> List.reduce ~f:AttributeDomain.join
+    |> Option.value ~default:AttributeDomain.top
+    |> fun attributes -> {astate with attributes}
+
+
 let analyze_procedure {Callbacks.exe_env; summary} =
   let proc_desc = Summary.get_proc_desc summary in
   let procname = Procdesc.get_proc_name proc_desc in
@@ -283,7 +330,10 @@ let analyze_procedure {Callbacks.exe_env; summary} =
       else Fn.id
     in
     let initial =
-      Domain.bottom |> set_lock_state_for_synchronized_proc |> set_thread_status_by_annotation
+      Domain.bottom
+      (* set the attributes of instance variables to those achieved by all constructors *)
+      |> add_constructor_attributes tenv procname
+      |> set_lock_state_for_synchronized_proc |> set_thread_status_by_annotation
     in
     Analyzer.compute_post proc_data ~initial
     |> Option.map ~f:filter_blocks

infer/src/concurrency/starvationDomain.ml

@@ -497,7 +497,7 @@ module AttributeDomain = struct
     let pred key _value =
       HilExp.AccessExpression.get_base key
       |> fst
-      |> fun v -> not (List.exists vars ~f:(Var.equal v))
+      |> fun v -> Var.is_this v || not (List.exists vars ~f:(Var.equal v))
     in
     filter pred t
 end
@@ -654,19 +654,23 @@ type summary =
   { critical_pairs: CriticalPairs.t
   ; thread: ThreadDomain.t
   ; scheduled_work: ScheduledWorkDomain.t
+  ; attributes: AttributeDomain.t
   ; return_attribute: Attribute.t }
 
 let empty_summary : summary =
   { critical_pairs= CriticalPairs.bottom
   ; thread= ThreadDomain.bottom
   ; scheduled_work= ScheduledWorkDomain.bottom
+  ; attributes= AttributeDomain.top
   ; return_attribute= Attribute.top }
 
 
 let pp_summary fmt (summary : summary) =
-  F.fprintf fmt "{thread= %a; critical_pairs= %a; scheduled_work= %a; return_attributes= %a}"
+  F.fprintf fmt
+    "{thread= %a; critical_pairs= %a; scheduled_work= %a; attributes= %a; return_attributes= %a}"
     ThreadDomain.pp summary.thread CriticalPairs.pp summary.critical_pairs ScheduledWorkDomain.pp
-    summary.scheduled_work Attribute.pp summary.return_attribute
+    summary.scheduled_work AttributeDomain.pp summary.attributes Attribute.pp
+    summary.return_attribute
 
 
 let integrate_summary ?tenv ?lhs callsite (astate : t) (summary : summary) =
@@ -684,14 +688,31 @@ let integrate_summary ?tenv ?lhs callsite (astate : t) (summary : summary) =
 
 let summary_of_astate : Procdesc.t -> t -> summary =
  fun proc_desc astate ->
+  let proc_name = Procdesc.get_proc_name proc_desc in
+  let is_java_constr =
+    match (proc_name : Typ.Procname.t) with
+    | Java jname ->
+        Typ.Procname.Java.is_constructor jname
+    | _ ->
+        false
+  in
+  let attributes =
+    if is_java_constr then
+      (* only keep attributes that have [this] as their root *)
+      let filter_this exp _ = HilExp.AccessExpression.get_base exp |> fst |> Var.is_this in
+      AttributeDomain.filter filter_this astate.attributes
+    else AttributeDomain.empty
+  in
+  let return_attribute =
+    let return_var_exp =
+      HilExp.AccessExpression.base
+        (Var.of_pvar (Pvar.get_ret_pvar proc_name), Procdesc.get_ret_type proc_desc)
+    in
+    AttributeDomain.find_opt return_var_exp astate.attributes
+    |> Option.value ~default:Attribute.Nothing
+  in
   { critical_pairs= astate.critical_pairs
   ; thread= astate.thread
   ; scheduled_work= astate.scheduled_work
-  ; return_attribute=
+  ; attributes
-      (let return_var_exp =
+  ; return_attribute }
-         HilExp.AccessExpression.base
-           ( Var.of_pvar (Pvar.get_ret_pvar (Procdesc.get_proc_name proc_desc))
-           , Procdesc.get_ret_type proc_desc )
-       in
-       AttributeDomain.find_opt return_var_exp astate.attributes
-       |> Option.value ~default:Attribute.Nothing ) }

infer/src/concurrency/starvationDomain.mli

@@ -187,6 +187,7 @@ type summary =
   { critical_pairs: CriticalPairs.t
   ; thread: ThreadDomain.t
   ; scheduled_work: ScheduledWorkDomain.t
+  ; attributes: AttributeDomain.t  (** final-state attributes that affect instance variables only *)
   ; return_attribute: Attribute.t }
 
 val empty_summary : summary

infer/tests/codetoanalyze/java/starvation-whole-program/AttributeFlows.java

@@ -123,7 +123,7 @@ class AttributeFlows {
         }
       };
 
-  public void FN_postRunnableFieldToUIThreadBad() {
+  public void postRunnableFieldToUIThreadBad() {
     Executors.getForegroundExecutor().execute(runnableField);
   }
 }

infer/tests/codetoanalyze/java/starvation-whole-program/ConstructedAttributes.java

@@ -0,0 +1,64 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+import android.os.Binder;
+import android.os.Handler;
+import android.os.Looper;
+import android.os.RemoteException;
+import java.util.concurrent.Executor;
+
+class ConstructedAttributes {
+  static Binder binder;
+
+  private static void doTransact() {
+    try {
+      binder.transact(0, null, null, 0);
+    } catch (RemoteException e) {
+    }
+  }
+
+  Executor mUiExecutor;
+  Executor mNonUiExecutor;
+  Handler mUiHandler;
+  Runnable mBadRunnable;
+  Runnable mOkRunnable;
+
+  ConstructedAttributes() {
+    mUiExecutor = Executors.getForegroundExecutor();
+    mNonUiExecutor = Executors.getBackgroundExecutor();
+    mUiHandler = new Handler(Looper.getMainLooper());
+    mBadRunnable =
+        new Runnable() {
+          @Override
+          public void run() {
+            doTransact();
+          }
+        };
+
+    mOkRunnable =
+        new Runnable() {
+          @Override
+          public void run() {}
+        };
+  }
+
+  public void postBlockingCallToUIExecutorBad() {
+    mUiExecutor.execute(mBadRunnable);
+  }
+
+  public void postNoopCallToUIExecutorOk() {
+    mUiExecutor.execute(mOkRunnable);
+  }
+
+  public void postBlockingCallToNonUIExecutorOk() {
+    mNonUiExecutor.execute(mBadRunnable);
+  }
+
+  public void postBlockingCallToUIHandlerBad() {
+    mUiHandler.post(mBadRunnable);
+  }
+}

infer/tests/codetoanalyze/java/starvation-whole-program/ImplicitConstructor.java

@@ -0,0 +1,70 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+import android.os.Binder;
+import android.os.Handler;
+import android.os.Looper;
+import android.os.RemoteException;
+import java.util.concurrent.Executor;
+
+class ImplicitConstructor {
+  static Binder binder;
+
+  private static void doTransact() {
+    try {
+      binder.transact(0, null, null, 0);
+    } catch (RemoteException e) {
+    }
+  }
+
+  Executor mUiExecutor = Executors.getForegroundExecutor();
+  Executor mNonUiExecutor = Executors.getBackgroundExecutor();
+  Handler mUiHandler = new Handler(Looper.getMainLooper());
+  Runnable mBadRunnable =
+      new Runnable() {
+        @Override
+        public void run() {
+          doTransact();
+        }
+      };
+
+  Runnable mOkRunnable =
+      new Runnable() {
+        @Override
+        public void run() {}
+      };
+
+  Runnable mAmbiguous;
+
+  ImplicitConstructor() {
+    mAmbiguous = mBadRunnable;
+  }
+
+  ImplicitConstructor(int data) {
+    mAmbiguous = mOkRunnable;
+  }
+
+  public void postBlockingCallToUIExecutorBad() {
+    mUiExecutor.execute(mBadRunnable);
+  }
+
+  public void postNoopCallToUIExecutorOk() {
+    mUiExecutor.execute(mOkRunnable);
+  }
+
+  public void postBlockingCallToNonUIExecutorOk() {
+    mNonUiExecutor.execute(mBadRunnable);
+  }
+
+  public void postBlockingCallToUIHandlerBad() {
+    mUiHandler.post(mBadRunnable);
+  }
+
+  public void postAmbiguousRunnableToUIExecutorOk() {
+    mUiExecutor.execute(mAmbiguous);
+  }
+}

infer/tests/codetoanalyze/java/starvation-whole-program/issues.exp

@@ -1,11 +1,16 @@
 codetoanalyze/java/starvation-whole-program/AttributeFlows.java, AttributeFlows.postBlockingCallToAnnnotatedUIThreadBad():void, 84, STARVATION, no_bucket, ERROR, [`void AttributeFlows.postBlockingCallToAnnnotatedUIThreadBad()`,Method call: `void AttributeFlows$3.run()`,Method call: `void AttributeFlows.doTransact()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`]
 codetoanalyze/java/starvation-whole-program/AttributeFlows.java, AttributeFlows.postBlockingCallToUIThreadBad():void, 41, STARVATION, no_bucket, ERROR, [`void AttributeFlows.postBlockingCallToUIThreadBad()`,Method call: `void AttributeFlows$1.run()`,Method call: `void AttributeFlows.doTransact()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`]
+codetoanalyze/java/starvation-whole-program/AttributeFlows.java, AttributeFlows.postRunnableFieldToUIThreadBad():void, 127, STARVATION, no_bucket, ERROR, [`void AttributeFlows.postRunnableFieldToUIThreadBad()`,Method call: `void AttributeFlows$6.run()`,Method call: `void AttributeFlows.doTransact()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`]
 codetoanalyze/java/starvation-whole-program/AttributeFlows.java, AttributeFlows.postRunnableIndirectlyToUIThreadBad():void, 115, STARVATION, no_bucket, ERROR, [`void AttributeFlows.postRunnableIndirectlyToUIThreadBad()`,Method call: `void AttributeFlows$5.run()`,Method call: `void AttributeFlows.doTransact()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`]
+codetoanalyze/java/starvation-whole-program/ConstructedAttributes.java, ConstructedAttributes.postBlockingCallToUIExecutorBad():void, 50, STARVATION, no_bucket, ERROR, [`void ConstructedAttributes.postBlockingCallToUIExecutorBad()`,Method call: `void ConstructedAttributes$1.run()`,Method call: `void ConstructedAttributes.doTransact()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`]
+codetoanalyze/java/starvation-whole-program/ConstructedAttributes.java, ConstructedAttributes.postBlockingCallToUIHandlerBad():void, 62, STARVATION, no_bucket, ERROR, [`void ConstructedAttributes.postBlockingCallToUIHandlerBad()`,Method call: `void ConstructedAttributes$1.run()`,Method call: `void ConstructedAttributes.doTransact()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`]
 codetoanalyze/java/starvation-whole-program/Deadlock.java, Deadlock.postDeadlockBad():void, 19, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void Deadlock.postDeadlockBad()`,Method call: `void Deadlock$1.run()`, locks `this.monitorA` in `class Deadlock`, locks `this.monitorB` in `class Deadlock`,[Trace 2] `void Deadlock.postDeadlockBad()`,Method call: `void Deadlock$2.run()`, locks `this.monitorB` in `class Deadlock`, locks `this.monitorA` in `class Deadlock`]
 codetoanalyze/java/starvation-whole-program/Deadlock.java, Deadlock.postDeadlockBad():void, 30, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void Deadlock.postDeadlockBad()`,Method call: `void Deadlock$2.run()`, locks `this.monitorB` in `class Deadlock`, locks `this.monitorA` in `class Deadlock`,[Trace 2] `void Deadlock.postDeadlockBad()`,Method call: `void Deadlock$1.run()`, locks `this.monitorA` in `class Deadlock`, locks `this.monitorB` in `class Deadlock`]
 codetoanalyze/java/starvation-whole-program/Deadlock.java, Deadlock.postOnBGThreadBad():void, 73, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void Deadlock.postOnBGThreadBad()`,Method call: `void Deadlock$5.run()`, locks `this.monitorE` in `class Deadlock`, locks `this.monitorF` in `class Deadlock`,[Trace 2] `void Deadlock.postOnBGThreadBad()`,Method call: `void Deadlock$6.run()`, locks `this.monitorF` in `class Deadlock`, locks `this.monitorE` in `class Deadlock`]
 codetoanalyze/java/starvation-whole-program/Deadlock.java, Deadlock.postOnBGThreadBad():void, 84, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void Deadlock.postOnBGThreadBad()`,Method call: `void Deadlock$6.run()`, locks `this.monitorF` in `class Deadlock`, locks `this.monitorE` in `class Deadlock`,[Trace 2] `void Deadlock.postOnBGThreadBad()`,Method call: `void Deadlock$5.run()`, locks `this.monitorE` in `class Deadlock`, locks `this.monitorF` in `class Deadlock`]
 codetoanalyze/java/starvation-whole-program/DirectStarvation.java, DirectStarvation.postBlockingCallToUIThreadBad():void, 29, STARVATION, no_bucket, ERROR, [`void DirectStarvation.postBlockingCallToUIThreadBad()`,Method call: `void DirectStarvation$1.run()`,Method call: `void DirectStarvation.doTransact()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`]
+codetoanalyze/java/starvation-whole-program/ImplicitConstructor.java, ImplicitConstructor.postBlockingCallToUIExecutorBad():void, 52, STARVATION, no_bucket, ERROR, [`void ImplicitConstructor.postBlockingCallToUIExecutorBad()`,Method call: `void ImplicitConstructor$1.run()`,Method call: `void ImplicitConstructor.doTransact()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`]
+codetoanalyze/java/starvation-whole-program/ImplicitConstructor.java, ImplicitConstructor.postBlockingCallToUIHandlerBad():void, 64, STARVATION, no_bucket, ERROR, [`void ImplicitConstructor.postBlockingCallToUIHandlerBad()`,Method call: `void ImplicitConstructor$1.run()`,Method call: `void ImplicitConstructor.doTransact()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`]
 codetoanalyze/java/starvation-whole-program/IndirectStarvation.java, IndirectStarvation.postBlockingCallToBackgroundThreadAndLockBad():void, 32, STARVATION, no_bucket, ERROR, [[Trace 1] `void IndirectStarvation.postBlockingCallToBackgroundThreadAndLockBad()`,Method call: `void IndirectStarvation$1.run()`, locks `this.monitorA` in `class IndirectStarvation`,[Trace 2] `void IndirectStarvation.postBlockingCallToBackgroundThreadAndLockBad()`,Method call: `void IndirectStarvation$2.run()`, locks `this.monitorA` in `class IndirectStarvation`,Method call: `void IndirectStarvation.doTransact()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`]
 codetoanalyze/java/starvation-whole-program/ModeledExecutors.java, ModeledExecutors.postBlockingCallToUIThreadBad():void, 28, STARVATION, no_bucket, ERROR, [`void ModeledExecutors.postBlockingCallToUIThreadBad()`,Method call: `void ModeledExecutors$1.run()`,Method call: `void ModeledExecutors.doTransact()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`]
 codetoanalyze/java/starvation-whole-program/ModeledExecutors.java, ModeledExecutors.scheduleBlockingCallToUIThreadBad():void, 138, STARVATION, no_bucket, ERROR, [`void ModeledExecutors.scheduleBlockingCallToUIThreadBad()`,Method call: `void ModeledExecutors$10.run()`,Method call: `void ModeledExecutors.doTransact()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`]