From 341e719fd45c1f6bd1b0a57c2d93364460024d69 Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Mon, 8 Jun 2020 02:41:30 -0700 Subject: [PATCH] [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 | 2 ++ infer/src/IR/JavaSplitName.mli | 3 ++ infer/src/backend/StarvationGlobalAnalysis.ml | 5 ++- infer/src/concurrency/StarvationModels.ml | 14 +++++++++ infer/src/concurrency/StarvationModels.mli | 3 ++ .../starvation-whole-program/MainMethod.java | 31 +++++++++++++++++++ .../java/starvation-whole-program/issues.exp | 2 ++ 7 files changed, 59 insertions(+), 1 deletion(-) create mode 100644 infer/tests/codetoanalyze/java/starvation-whole-program/MainMethod.java diff --git a/infer/src/IR/JavaSplitName.ml b/infer/src/IR/JavaSplitName.ml index f878c5f91..3eb61564d 100644 --- a/infer/src/IR/JavaSplitName.ml +++ b/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 diff --git a/infer/src/IR/JavaSplitName.mli b/infer/src/IR/JavaSplitName.mli index 9b439a7df..69217a880 100644 --- a/infer/src/IR/JavaSplitName.mli +++ b/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 *) diff --git a/infer/src/backend/StarvationGlobalAnalysis.ml b/infer/src/backend/StarvationGlobalAnalysis.ml index 0dbf0b2fa..9da0bbcf0 100644 --- a/infer/src/backend/StarvationGlobalAnalysis.ml +++ b/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 ) diff --git a/infer/src/concurrency/StarvationModels.ml b/infer/src/concurrency/StarvationModels.ml index d0fc76792..0aa434c81 100644 --- a/infer/src/concurrency/StarvationModels.ml +++ b/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) diff --git a/infer/src/concurrency/StarvationModels.mli b/infer/src/concurrency/StarvationModels.mli index 47516e103..7998a7258 100644 --- a/infer/src/concurrency/StarvationModels.mli +++ b/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] *) diff --git a/infer/tests/codetoanalyze/java/starvation-whole-program/MainMethod.java b/infer/tests/codetoanalyze/java/starvation-whole-program/MainMethod.java new file mode 100644 index 000000000..101f5be1b --- /dev/null +++ b/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) { + } + } + } +} diff --git a/infer/tests/codetoanalyze/java/starvation-whole-program/issues.exp b/infer/tests/codetoanalyze/java/starvation-whole-program/issues.exp index ebd47cd83..1d5b69e39 100644 --- a/infer/tests/codetoanalyze/java/starvation-whole-program/issues.exp +++ b/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`]