[starvation][whole-program] add model for `Main`

Summary: Schedule work from main methods.

Reviewed By: ezgicicek

Differential Revision: D21880733

fbshipit-source-id: c45dc55aa

infer/src/IR/JavaSplitName.ml

@@ -32,6 +32,8 @@ let java_lang_object_array = make ~package:"java.lang" "Object[]"
 
 let java_lang_string = make ~package:"java.lang" "String"
 
+let java_lang_string_array = make ~package:"java.lang" "String[]"
+
 let void = make "void"
 
 let pp_type_verbosity ~verbose fmt = function

infer/src/IR/JavaSplitName.mli

@@ -28,6 +28,9 @@ val java_lang_object_array : t
 val java_lang_string : t
 (** [java.lang.String] type *)
 
+val java_lang_string_array : t
+(** [java.lang.String\[\]] type *)
+
 val void : t
 (** Java [void] type *)
 

infer/src/backend/StarvationGlobalAnalysis.ml

@@ -29,7 +29,10 @@ let iter_summary ~f exe_env (summary : Summary.t) =
   |> Option.iter ~f:(fun ({scheduled_work; critical_pairs} : summary) ->
          let pname = Summary.get_proc_name summary in
          let tenv = Exe_env.get_tenv exe_env pname in
-         if ConcurrencyModels.is_android_lifecycle_method tenv pname then f pname critical_pairs ;
+         if
+           StarvationModels.is_java_main_method pname
+           || ConcurrencyModels.is_android_lifecycle_method tenv pname
+         then f pname critical_pairs ;
          ScheduledWorkDomain.iter
            (fun work -> get_summary_of_scheduled_work work |> Option.iter ~f:(f pname))
            scheduled_work )

infer/src/concurrency/StarvationModels.ml

@@ -399,3 +399,17 @@ let is_assume_true =
     ; { default with
         classname= "com.google.common.base.Preconditions"
       ; methods= ["checkArgument"; "checkState"] } ]
+
+
+let is_java_main_method (pname : Procname.t) =
+  let check_main_args args =
+    match args with [arg] -> JavaSplitName.(equal java_lang_string_array arg) | _ -> false
+  in
+  match pname with
+  | C _ | Linters_dummy_method | Block _ | ObjC_Cpp _ | WithBlockParameters _ ->
+      false
+  | Java java_pname ->
+      Procname.Java.is_static java_pname
+      && String.equal "main" (Procname.get_method pname)
+      && Typ.equal Typ.void (Procname.Java.get_return_typ java_pname)
+      && check_main_args (Procname.Java.get_parameters java_pname)

infer/src/concurrency/StarvationModels.mli

@@ -76,3 +76,6 @@ val is_future_is_done : Tenv.t -> Procname.t -> HilExp.t list -> bool
 
 val is_assume_true : Tenv.t -> Procname.t -> HilExp.t list -> bool
 (** is the callee equivalent to assuming its first argument true *)
+
+val is_java_main_method : Procname.t -> bool
+(** does the method look like a Java [main] *)

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

@@ -0,0 +1,31 @@
+/*
+ * 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.
+ */
+
+class MainMethod {
+
+  static Object monitorA, monitorB;
+
+  public static void main(String args[]) {
+    Thread t =
+        new Thread(
+            new Runnable() {
+              @Override
+              public void run() {
+                synchronized (monitorA) {
+                  synchronized (monitorB) {
+                  }
+                }
+              }
+            });
+    t.start();
+
+    synchronized (monitorB) {
+      synchronized (monitorA) {
+      }
+    }
+  }
+}

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

@@ -11,6 +11,8 @@ codetoanalyze/java/starvation-whole-program/DirectStarvation.java, DirectStarvat
 codetoanalyze/java/starvation-whole-program/ImplicitConstructor.java, ImplicitConstructor.postBlockingCallToUIExecutorBad():void, 54, 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, 66, 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.this$0.monitorA` in `class IndirectStarvation$1`,[Trace 2] `void IndirectStarvation.postBlockingCallToBackgroundThreadAndLockBad()`,Method call: `void IndirectStarvation$2.run()`, locks `this.this$0.monitorA` in `class IndirectStarvation$2`,Method call: `void IndirectStarvation.doTransact()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`]
+codetoanalyze/java/starvation-whole-program/MainMethod.java, MainMethod.main(java.lang.String[]):void, 24, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void MainMethod.main(String[])`,Method call: `void MainMethod$1.run()`, locks `MainMethod.monitorA` in `class MainMethod`, locks `MainMethod.monitorB` in `class MainMethod`,[Trace 2] `void MainMethod.main(String[])`, locks `MainMethod.monitorB` in `class MainMethod`, locks `MainMethod.monitorA` in `class MainMethod`]
+codetoanalyze/java/starvation-whole-program/MainMethod.java, MainMethod.main(java.lang.String[]):void, 26, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void MainMethod.main(String[])`, locks `MainMethod.monitorB` in `class MainMethod`, locks `MainMethod.monitorA` in `class MainMethod`,[Trace 2] `void MainMethod.main(String[])`,Method call: `void MainMethod$1.run()`, locks `MainMethod.monitorA` in `class MainMethod`, locks `MainMethod.monitorB` in `class MainMethod`]
 codetoanalyze/java/starvation-whole-program/ModeledExecutors.java, ModeledExecutors.postToUIThreadBad():void, 165, STARVATION, no_bucket, ERROR, [`void ModeledExecutors.postToUIThreadBad()`,Method call: `void ModeledExecutors$12.run()`,Method call: `void ModeledExecutors.doTransact()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`]
 codetoanalyze/java/starvation-whole-program/ModeledExecutors.java, ModeledExecutors.scheduleBlockingCallToUIThreadBad():void, 140, 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)`]
 codetoanalyze/java/starvation-whole-program/ModeledExecutors.java, ModeledExecutors.scheduleGuaranteedDelayedDeadlockBad():void, 97, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void ModeledExecutors.scheduleGuaranteedDelayedDeadlockBad()`,Method call: `void ModeledExecutors$7.run()`, locks `this.this$0.monitorA` in `class ModeledExecutors$7`, locks `this.this$0.monitorB` in `class ModeledExecutors$7`,[Trace 2] `void ModeledExecutors.scheduleGuaranteedDelayedDeadlockBad()`,Method call: `void ModeledExecutors$8.run()`, locks `this.this$0.monitorB` in `class ModeledExecutors$8`, locks `this.this$0.monitorA` in `class ModeledExecutors$8`]