[starvation] skip analysis option should be used at top level too

Reviewed By: mbouaziz

Differential Revision: D13377043

fbshipit-source-id: 16e67ac86
master
Nikos Gorogiannis 6 years ago committed by Facebook Github Bot
parent a8dbaf082d
commit 9c240ed978

@ -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 <named args> 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)

@ -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

@ -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 *)

@ -0,0 +1,4 @@
{
"force-delete-results-dir": true,
"starvation-skip-analysis" : [ { "classname": "skipped::Skip", "methods": ["skipped_ok"] } ]
}

@ -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*`]

@ -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 <mutex>
// 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<std::mutex> l(mutex_);
{ std::lock_guard<std::mutex> l(mutex_); }
}
};
} // namespace skipped
Loading…
Cancel
Save