diff --git a/infer/src/concurrency/MethodMatcher.ml b/infer/src/concurrency/MethodMatcher.ml index 084387e17..971ce07d2 100644 --- a/infer/src/concurrency/MethodMatcher.ml +++ b/infer/src/concurrency/MethodMatcher.ml @@ -8,8 +8,13 @@ open! IStd module L = Logging -let call_matches ?(search_superclasses = true) ?(method_prefix = false) - ?(actuals_pred = fun _ -> true) clazz methods = +(** [call_matches C methods] builds a method matcher for calls [C.foo] where + [foo] is in [methods]. Named arguments change behaviour: + - [search_superclasses=true] will match calls [S.foo] where [S] is a superclass of [C]. + - [method_prefix=true] will match calls [C.foo] where [foo] is a prefix of a string in [methods] + - [actuals_pred] is a predicate that runs on the expressions fed as arguments to the call, and + which must return [true] for the matcher to return [true]. *) +let call_matches ~search_superclasses ~method_prefix ~actuals_pred clazz methods = let method_matcher = if method_prefix then fun current_method target_method -> String.is_prefix current_method ~prefix:target_method @@ -18,7 +23,7 @@ let call_matches ?(search_superclasses = true) ?(method_prefix = false) let class_matcher = if search_superclasses then let target = "class " ^ clazz in - let is_target tname _ = Typ.Name.to_string tname |> String.equal target in + let is_target tname _tstruct = Typ.Name.to_string tname |> String.equal target in fun tenv pname -> Typ.Procname.get_class_type_name pname |> Option.exists ~f:(PatternMatch.supertype_exists tenv is_target) diff --git a/infer/src/concurrency/MethodMatcher.mli b/infer/src/concurrency/MethodMatcher.mli index 6dfd859f2..ae9bcec1b 100644 --- a/infer/src/concurrency/MethodMatcher.mli +++ b/infer/src/concurrency/MethodMatcher.mli @@ -10,23 +10,6 @@ open! IStd (** pattern matcher for Java methods *) type t = Tenv.t -> Typ.Procname.t -> HilExp.t list -> bool -val call_matches : - ?search_superclasses:bool - -> ?method_prefix:bool - -> ?actuals_pred:(HilExp.t list -> bool) - -> string - -> string list - -> t Staged.t - [@@warning "-32"] -(** [call_matches C methods] builds a method matcher for calls [C.foo] where - [foo] is in [methods]. Optional arguments change default behaviour: - - [search_superclasses=true] will match calls [S.foo] where [S] is a superclass of [C]. - Defaults to [true]. - - [method_prefix=true] will match calls [C.foo] where [foo] is a prefix of a string in [methods] - Defaults to [false]. - - [actuals_pred] is a predicate that runs on the expressions fed as arguments to the call, and - which must return [true] for the matcher to return [true]. The default returns [true]. *) - type record = { search_superclasses: bool ; method_prefix: bool diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index 8c68eb449..1f0a6191e 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -141,41 +141,43 @@ module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Normal) (TransferFun let analyze_procedure {Callbacks.proc_desc; tenv; summary} = let open StarvationDomain in let pname = Procdesc.get_proc_name proc_desc in - let formals = FormalMap.make proc_desc in - let proc_data = ProcData.make proc_desc tenv formals in - let loc = Procdesc.get_loc proc_desc in - let recursive_locks = Procdesc.get_proc_name proc_desc |> Typ.Procname.is_java in - let initial = - if not (Procdesc.is_java_synchronized proc_desc) then StarvationDomain.empty - else - let lock = - match pname with - | Typ.Procname.Java java_pname when Typ.Procname.Java.is_static java_pname -> - (* this is crafted so as to match synchronized(CLASSNAME.class) constructs *) - Typ.Procname.Java.get_class_type_name java_pname - |> Typ.Name.name |> Ident.string_to_name |> lock_of_class |> Option.some - | _ -> - FormalMap.get_formal_base 0 formals |> Option.map ~f:(fun base -> (base, [])) - in - StarvationDomain.acquire ~recursive_locks StarvationDomain.empty loc (Option.to_list lock) - in - let initial = - ConcurrencyModels.runs_on_ui_thread tenv proc_desc - |> Option.value_map ~default:initial ~f:(StarvationDomain.set_on_ui_thread initial loc) - in - let filter_blocks = - if is_nonblocking tenv proc_desc then fun ({events; order} as astate) -> - { astate with - events= EventDomain.filter (function {elem= MayBlock _} -> false | _ -> true) events - ; order= - OrderDomain.filter - (function {elem= {eventually= {elem= MayBlock _}}} -> false | _ -> true) - order } - else Fn.id - in - Analyzer.compute_post proc_data ~initial - |> Option.map ~f:filter_blocks - |> Option.value_map ~default:summary ~f:(fun astate -> Payload.update_summary astate summary) + if StarvationModels.should_skip_analysis tenv pname [] then summary + else + let formals = FormalMap.make proc_desc in + let proc_data = ProcData.make proc_desc tenv formals in + let loc = Procdesc.get_loc proc_desc in + let recursive_locks = Procdesc.get_proc_name proc_desc |> Typ.Procname.is_java in + let initial = + if not (Procdesc.is_java_synchronized proc_desc) then StarvationDomain.empty + else + let lock = + match pname with + | Typ.Procname.Java java_pname when Typ.Procname.Java.is_static java_pname -> + (* this is crafted so as to match synchronized(CLASSNAME.class) constructs *) + Typ.Procname.Java.get_class_type_name java_pname + |> Typ.Name.name |> Ident.string_to_name |> lock_of_class |> Option.some + | _ -> + FormalMap.get_formal_base 0 formals |> Option.map ~f:(fun base -> (base, [])) + in + StarvationDomain.acquire ~recursive_locks StarvationDomain.empty loc (Option.to_list lock) + in + let initial = + ConcurrencyModels.runs_on_ui_thread tenv proc_desc + |> Option.value_map ~default:initial ~f:(StarvationDomain.set_on_ui_thread initial loc) + in + let filter_blocks = + if is_nonblocking tenv proc_desc then fun ({events; order} as astate) -> + { astate with + events= EventDomain.filter (function {elem= MayBlock _} -> false | _ -> true) events + ; order= + OrderDomain.filter + (function {elem= {eventually= {elem= MayBlock _}}} -> false | _ -> true) + order } + else Fn.id + in + Analyzer.compute_post proc_data ~initial + |> Option.map ~f:filter_blocks + |> Option.value_map ~default:summary ~f:(fun astate -> Payload.update_summary astate summary) (** per-procedure report map, which takes care of deduplication *) diff --git a/infer/tests/codetoanalyze/cpp/starvation/.inferconfig b/infer/tests/codetoanalyze/cpp/starvation/.inferconfig new file mode 100644 index 000000000..ea4a770a6 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/starvation/.inferconfig @@ -0,0 +1,4 @@ +{ + "force-delete-results-dir": true, + "starvation-skip-analysis" : [ { "classname": "skipped::Skip", "methods": ["skipped_ok"] } ] +} diff --git a/infer/tests/codetoanalyze/cpp/starvation/issues.exp b/infer/tests/codetoanalyze/cpp/starvation/issues.exp index 7287cb436..63cc252b3 100644 --- a/infer/tests/codetoanalyze/cpp/starvation/issues.exp +++ b/infer/tests/codetoanalyze/cpp/starvation/issues.exp @@ -6,3 +6,4 @@ codetoanalyze/cpp/starvation/basics.cpp, basics::WithGuard_thread1_bad, 44, DEAD codetoanalyze/cpp/starvation/recursive.cpp, Recursive_FP_multi_ok, 26, DEADLOCK, no_bucket, ERROR, [In method`Recursive_FP_multi_ok`,locks `this.recursive_mutex_` in class `Recursive*`,locks `this.recursive_mutex_` in class `Recursive*`] codetoanalyze/cpp/starvation/recursive.cpp, Recursive_FP_path_sensitive_ok, 36, DEADLOCK, no_bucket, ERROR, [In method`Recursive_FP_path_sensitive_ok`,locks `this.mutex_` in class `Recursive*`,locks `this.mutex_` in class `Recursive*`] codetoanalyze/cpp/starvation/recursive.cpp, Recursive_FP_unknown_ok, 31, DEADLOCK, no_bucket, ERROR, [In method`Recursive_FP_unknown_ok`,locks `this.umutex_` in class `Recursive*`,locks `this.umutex_` in class `Recursive*`] +codetoanalyze/cpp/starvation/skip.cpp, skipped::Skip_not_skipped_bad, 19, DEADLOCK, no_bucket, ERROR, [In method`skipped::Skip_not_skipped_bad`,Method call: `skipped::Skip_private_deadlock`,locks `this.mutex_` in class `skipped::Skip*`,locks `this.mutex_` in class `skipped::Skip*`] diff --git a/infer/tests/codetoanalyze/cpp/starvation/skip.cpp b/infer/tests/codetoanalyze/cpp/starvation/skip.cpp new file mode 100644 index 000000000..414fe1826 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/starvation/skip.cpp @@ -0,0 +1,30 @@ +/* + * Copyright (c) 2018-present, Facebook, Inc. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + */ + +#include + +// the deadlock here is masked by the starvation-skip-analysis option in +// .inferconfig +namespace skipped { +class Skip { + public: + Skip() {} + + void skipped_ok() { private_deadlock(); } + + void not_skipped_bad() { private_deadlock(); } + + private: + std::mutex mutex_; + + void private_deadlock() { + std::lock_guard l(mutex_); + { std::lock_guard l(mutex_); } + } +}; + +} // namespace skipped