[starvation] C++ deadlock FPs due to recursive and unknown mutexes

Reviewed By: jvillard

Differential Revision: D13376553

fbshipit-source-id: 79ad1a63a
master
Nikos Gorogiannis 6 years ago committed by Facebook Github Bot
parent 9c240ed978
commit 2701073b3e

@ -55,36 +55,61 @@ module Clang : sig
val get_lock_effect : Typ.Procname.t -> HilExp.t list -> lock_effect val get_lock_effect : Typ.Procname.t -> HilExp.t list -> lock_effect
val lock_types_matcher : QualifiedCppName.Match.quals_matcher val lock_types_matcher : QualifiedCppName.Match.quals_matcher
val is_recursive_lock_type : QualifiedCppName.t -> bool
end = struct end = struct
type lock_model = {cls: string; lck: string list; tlk: string list; unl: string list} type lock_model =
{ classname: string
; lock: string list
; trylock: string list
; unlock: string list
; recursive: bool }
let lock_models = let lock_models =
let def = {cls= ""; lck= ["lock"]; tlk= ["try_lock"]; unl= ["unlock"]} in let def =
{classname= ""; lock= ["lock"]; trylock= ["try_lock"]; unlock= ["unlock"]; recursive= false}
in
let shd = let shd =
{ cls= "std::shared_mutex" { def with
; lck= "lock_shared" :: def.lck lock= "lock_shared" :: def.lock
; tlk= "try_lock_shared" :: def.tlk ; trylock= "try_lock_shared" :: def.trylock
; unl= "unlock_shared" :: def.unl } ; unlock= "unlock_shared" :: def.unlock }
in in
let rwm = let rwm =
{ cls= "apache::thrift::concurrency::ReadWriteMutex" { def with
; lck= ["acquireRead"; "acquireWrite"] lock= ["acquireRead"; "acquireWrite"]
; tlk= ["attemptRead"; "attemptWrite"] ; trylock= ["attemptRead"; "attemptWrite"]
; unl= ["release"] } ; unlock= ["release"] }
in in
[ {def with cls= "apache::thrift::concurrency::Monitor"; tlk= "timedlock" :: def.tlk} [ { def with
; {def with cls= "apache::thrift::concurrency::Mutex"; tlk= "timedlock" :: def.tlk} classname= "apache::thrift::concurrency::Monitor"; trylock= "timedlock" :: def.trylock }
; {rwm with cls= "apache::thrift::concurrency::NoStarveReadWriteMutex"} ; { def with
; rwm classname= "apache::thrift::concurrency::Mutex"; trylock= "timedlock" :: def.trylock }
; {shd with cls= "boost::shared_mutex"} ; {rwm with classname= "apache::thrift::concurrency::NoStarveReadWriteMutex"}
; {def with cls= "boost::mutex"} ; {rwm with classname= "apache::thrift::concurrency::ReadWriteMutex"}
; {def with cls= "folly::MicroSpinLock"} ; {shd with classname= "boost::shared_mutex"}
; {shd with cls= "folly::RWSpinLock"} ; {def with classname= "boost::mutex"}
; {shd with cls= "folly::SharedMutex"} ; {def with classname= "folly::MicroSpinLock"}
; {shd with cls= "folly::SharedMutexImpl"} ; {shd with classname= "folly::RWSpinLock"}
; {def with cls= "folly::SpinLock"} ; {shd with classname= "folly::SharedMutex"}
; {def with cls= "std::mutex"} ; {shd with classname= "folly::SharedMutexImpl"}
; shd ] ; {def with classname= "folly::SpinLock"}
; {def with classname= "std::mutex"}
; {def with classname= "std::recursive_mutex"; recursive= true}
; {def with classname= "std::recursive_timed_mutex"; recursive= true}
; {shd with classname= "std::shared_mutex"}
; {def with classname= "std::timed_mutex"} ]
let is_recursive_lock_type qname =
let qname_str = QualifiedCppName.to_qual_string qname in
match List.find lock_models ~f:(fun mdl -> String.equal qname_str mdl.classname) with
| None ->
L.debug Analysis Medium "is_recursive_lock_type: Could not find lock type %a@."
QualifiedCppName.pp qname ;
true
| Some mdl ->
mdl.recursive
let mk_matcher methods = let mk_matcher methods =
@ -98,18 +123,18 @@ end = struct
let mk_model_matcher ~f = let mk_model_matcher ~f =
let lock_methods = let lock_methods =
List.concat_map lock_models ~f:(fun mdl -> List.concat_map lock_models ~f:(fun mdl ->
List.map (f mdl) ~f:(fun mtd -> mdl.cls ^ "::" ^ mtd) ) List.map (f mdl) ~f:(fun mtd -> mdl.classname ^ "::" ^ mtd) )
in in
mk_matcher lock_methods mk_matcher lock_methods
in in
( mk_model_matcher ~f:(fun mdl -> mdl.lck) ( mk_model_matcher ~f:(fun mdl -> mdl.lock)
, mk_model_matcher ~f:(fun mdl -> mdl.unl) , mk_model_matcher ~f:(fun mdl -> mdl.unlock)
, mk_model_matcher ~f:(fun mdl -> mdl.tlk) , mk_model_matcher ~f:(fun mdl -> mdl.trylock)
, mk_matcher ["std::lock"] ) , mk_matcher ["std::lock"] )
let lock_types_matcher = let lock_types_matcher =
let class_names = List.map lock_models ~f:(fun mdl -> mdl.cls) in let class_names = List.map lock_models ~f:(fun mdl -> mdl.classname) in
QualifiedCppName.Match.of_fuzzy_qual_names class_names QualifiedCppName.Match.of_fuzzy_qual_names class_names
@ -285,11 +310,9 @@ let get_current_class_and_annotated_superclasses is_annot tenv pname =
None None
let find_annotated_or_overriden_annotated_method is_annot pname tenv = let find_annotated_or_overriden_annotated_method ~attrs_of_pname is_annot pname tenv =
PatternMatch.override_find PatternMatch.override_find
(fun pn -> (fun pn -> Annotations.pname_has_return_annot pn ~attrs_of_pname is_annot)
Annotations.pname_has_return_annot pn ~attrs_of_pname:Summary.proc_resolve_attributes
is_annot )
tenv pname tenv pname
@ -351,11 +374,12 @@ let runs_on_ui_thread =
in in
let is_annot annot = List.exists annotation_matchers ~f:(fun m -> m annot) in let is_annot annot = List.exists annotation_matchers ~f:(fun m -> m annot) in
let mono_pname = MF.wrap_monospaced Typ.Procname.pp in let mono_pname = MF.wrap_monospaced Typ.Procname.pp in
fun tenv proc_desc -> fun ~attrs_of_pname tenv proc_desc ->
let pname = Procdesc.get_proc_name proc_desc in let pname = Procdesc.get_proc_name proc_desc in
if if
Annotations.pdesc_has_return_annot proc_desc Annotations.ia_is_worker_thread Annotations.pdesc_has_return_annot proc_desc Annotations.ia_is_worker_thread
|| find_annotated_or_overriden_annotated_method Annotations.ia_is_worker_thread pname tenv || find_annotated_or_overriden_annotated_method ~attrs_of_pname
Annotations.ia_is_worker_thread pname tenv
|> Option.is_some |> Option.is_some
|| get_current_class_and_annotated_superclasses Annotations.ia_is_worker_thread tenv pname || get_current_class_and_annotated_superclasses Annotations.ia_is_worker_thread tenv pname
|> Option.value_map ~default:false ~f:(function _, [] -> false | _ -> true) |> Option.value_map ~default:false ~f:(function _, [] -> false | _ -> true)
@ -367,7 +391,7 @@ let runs_on_ui_thread =
(F.asprintf "%a is annotated %s" mono_pname pname (F.asprintf "%a is annotated %s" mono_pname pname
(MF.monospaced_to_string Annotations.ui_thread)) (MF.monospaced_to_string Annotations.ui_thread))
else else
match find_annotated_or_overriden_annotated_method is_annot pname tenv with match find_annotated_or_overriden_annotated_method ~attrs_of_pname is_annot pname tenv with
| Some override_pname -> | Some override_pname ->
Some Some
(F.asprintf "class %a overrides %a, which is annotated %s" mono_pname pname mono_pname (F.asprintf "class %a overrides %a, which is annotated %s" mono_pname pname mono_pname
@ -390,3 +414,10 @@ let runs_on_ui_thread =
let cpp_lock_types_matcher = Clang.lock_types_matcher let cpp_lock_types_matcher = Clang.lock_types_matcher
let is_recursive_lock_type = function
| Typ.CppClass (qname, _) ->
Clang.is_recursive_lock_type qname
| _ ->
(* non-C++ lock types are always considered recursive *)
true

@ -33,7 +33,11 @@ val get_lock_effect : Typ.Procname.t -> HilExp.t list -> lock_effect
val get_thread : Typ.Procname.t -> thread val get_thread : Typ.Procname.t -> thread
(** describe how this procedure behaves with respect to thread access *) (** describe how this procedure behaves with respect to thread access *)
val runs_on_ui_thread : Tenv.t -> Procdesc.t -> string option val runs_on_ui_thread :
attrs_of_pname:(Typ.Procname.t -> ProcAttributes.t option)
-> Tenv.t
-> Procdesc.t
-> string option
(** We don't want to warn on methods that run on the UI thread because they should always be (** We don't want to warn on methods that run on the UI thread because they should always be
single-threaded. Assume that methods annotated with @UiThread, @OnEvent, @OnBind, @OnMount, single-threaded. Assume that methods annotated with @UiThread, @OnEvent, @OnBind, @OnMount,
@OnUnbind, @OnUnmount always run on the UI thread. Also assume that any superclass @OnUnbind, @OnUnmount always run on the UI thread. Also assume that any superclass
@ -44,6 +48,12 @@ val get_current_class_and_annotated_superclasses :
(Annot.Item.t -> bool) -> Tenv.t -> Typ.Procname.t -> (Typ.name * Typ.name list) option (Annot.Item.t -> bool) -> Tenv.t -> Typ.Procname.t -> (Typ.name * Typ.name list) option
val find_annotated_or_overriden_annotated_method : val find_annotated_or_overriden_annotated_method :
(Annot.Item.t -> bool) -> BuiltinDecl.t -> Tenv.t -> BuiltinDecl.t sexp_option attrs_of_pname:(Typ.Procname.t -> ProcAttributes.t option)
-> (Annot.Item.t -> bool)
-> Typ.Procname.t
-> Tenv.t
-> Typ.Procname.t sexp_option
val cpp_lock_types_matcher : QualifiedCppName.Match.quals_matcher val cpp_lock_types_matcher : QualifiedCppName.Match.quals_matcher
val is_recursive_lock_type : Typ.name -> bool

@ -617,7 +617,8 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} =
let initial = let initial =
let threads = let threads =
if if
runs_on_ui_thread tenv proc_desc |> Option.is_some runs_on_ui_thread ~attrs_of_pname:Summary.proc_resolve_attributes tenv proc_desc
|> Option.is_some
|| is_thread_confined_method tenv proc_desc || is_thread_confined_method tenv proc_desc
then ThreadsDomain.AnyThreadButSelf then ThreadsDomain.AnyThreadButSelf
else if Procdesc.is_java_synchronized proc_desc || is_marked_thread_safe proc_desc tenv else if Procdesc.is_java_synchronized proc_desc || is_marked_thread_safe proc_desc tenv

@ -374,7 +374,9 @@ let is_thread_safe_class pname tenv =
let is_thread_safe_method pname tenv = let is_thread_safe_method pname tenv =
find_annotated_or_overriden_annotated_method is_thread_safe pname tenv |> Option.is_some find_annotated_or_overriden_annotated_method ~attrs_of_pname:Summary.proc_resolve_attributes
is_thread_safe pname tenv
|> Option.is_some
let is_marked_thread_safe pdesc tenv = let is_marked_thread_safe pdesc tenv =

@ -80,13 +80,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
in in
let is_java = Procdesc.get_proc_name pdesc |> Typ.Procname.is_java in let is_java = Procdesc.get_proc_name pdesc |> Typ.Procname.is_java in
let do_lock locks loc astate = let do_lock locks loc astate =
List.filter_map ~f:get_lock_path locks |> Domain.acquire ~recursive_locks:is_java astate loc List.filter_map ~f:get_lock_path locks |> Domain.acquire tenv astate loc
in in
let do_unlock locks astate = List.filter_map ~f:get_lock_path locks |> Domain.release astate in let do_unlock locks astate = List.filter_map ~f:get_lock_path locks |> Domain.release astate in
let do_call callee loc astate = let do_call callee loc astate =
Payload.read pdesc callee Payload.read pdesc callee
|> Option.value_map ~default:astate |> Option.value_map ~default:astate ~f:(Domain.integrate_summary tenv astate callee loc)
~f:(Domain.integrate_summary ~recursive_locks:is_java astate callee loc)
in in
match instr with match instr with
| Assign _ | Assume _ | Call (_, Indirect _, _, _, _) | ExitScope _ -> | Assign _ | Assume _ | Call (_, Indirect _, _, _, _) | ExitScope _ ->
@ -98,11 +97,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| Lock locks -> | Lock locks ->
do_lock locks loc astate do_lock locks loc astate
| GuardLock guard -> | GuardLock guard ->
Domain.lock_guard ~recursive_locks:is_java astate guard loc Domain.lock_guard tenv astate guard loc
| GuardConstruct {guard; lock; acquire_now} -> ( | GuardConstruct {guard; lock; acquire_now} -> (
match get_lock_path lock with match get_lock_path lock with
| Some lock_path -> | Some lock_path ->
Domain.add_guard astate guard lock_path ~acquire_now ~recursive_locks:false loc Domain.add_guard tenv astate guard lock_path ~acquire_now loc
| None -> | None ->
log_parse_error "Couldn't parse lock in guard constructor" callee actuals ; log_parse_error "Couldn't parse lock in guard constructor" callee actuals ;
astate ) astate )
@ -146,7 +145,6 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} =
let formals = FormalMap.make proc_desc in let formals = FormalMap.make proc_desc in
let proc_data = ProcData.make proc_desc tenv formals in let proc_data = ProcData.make proc_desc tenv formals in
let loc = Procdesc.get_loc proc_desc 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 = let initial =
if not (Procdesc.is_java_synchronized proc_desc) then StarvationDomain.empty if not (Procdesc.is_java_synchronized proc_desc) then StarvationDomain.empty
else else
@ -159,10 +157,11 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} =
| _ -> | _ ->
FormalMap.get_formal_base 0 formals |> Option.map ~f:(fun base -> (base, [])) FormalMap.get_formal_base 0 formals |> Option.map ~f:(fun base -> (base, []))
in in
StarvationDomain.acquire ~recursive_locks StarvationDomain.empty loc (Option.to_list lock) StarvationDomain.acquire tenv StarvationDomain.empty loc (Option.to_list lock)
in in
let initial = let initial =
ConcurrencyModels.runs_on_ui_thread tenv proc_desc ConcurrencyModels.runs_on_ui_thread ~attrs_of_pname:Summary.proc_resolve_attributes tenv
proc_desc
|> Option.value_map ~default:initial ~f:(StarvationDomain.set_on_ui_thread initial loc) |> Option.value_map ~default:initial ~f:(StarvationDomain.set_on_ui_thread initial loc)
in in
let filter_blocks = let filter_blocks =

@ -6,6 +6,7 @@
*) *)
open! IStd open! IStd
module F = Format module F = Format
module L = Logging
module MF = MarkupFormatter module MF = MarkupFormatter
let pname_pp = MF.wrap_monospaced Typ.Procname.pp let pname_pp = MF.wrap_monospaced Typ.Procname.pp
@ -147,7 +148,7 @@ module LockState = struct
false false
let acquire lock_id lock_event map = let acquire map lock_id lock_event =
let current_value = try find lock_id map with Caml.Not_found -> LockStack.top in let current_value = try find lock_id map with Caml.Not_found -> LockStack.top in
let new_value = LockStack.push lock_event current_value in let new_value = LockStack.push lock_event current_value in
add lock_id new_value map add lock_id new_value map
@ -253,10 +254,34 @@ let ( <= ) ~lhs ~rhs =
&& UIThreadDomain.( <= ) ~lhs:lhs.ui ~rhs:rhs.ui && UIThreadDomain.( <= ) ~lhs:lhs.ui ~rhs:rhs.ui
let is_recursive_lock event tenv =
let is_class_and_recursive_lock = function
| {Typ.desc= Tptr ({desc= Tstruct name}, _)} | {desc= Tstruct name} ->
ConcurrencyModels.is_recursive_lock_type name
| typ ->
L.die L.InternalError "Asked if non-struct type %a is a recursive lock type.@."
(Typ.pp_full Pp.text) typ
in
match event with
| {Event.elem= LockAcquire lock_path} ->
AccessPath.get_typ lock_path tenv |> Option.exists ~f:is_class_and_recursive_lock
| _ ->
false
(** skip adding an order pair [(_, event)] if
- we have no tenv, or,
- [event] is not a lock event, or,
- we do not hold the lock, or,
- the lock is not recursive. *)
let should_skip tenv_opt event lock_state =
Option.exists tenv_opt ~f:(fun tenv ->
LockState.is_taken event lock_state && is_recursive_lock event tenv )
(* for every lock b held locally, add a pair (b, event) *) (* for every lock b held locally, add a pair (b, event) *)
let add_order_pairs ~recursive_locks lock_state event acc = let add_order_pairs tenv_opt lock_state event acc =
(* add no pairs whatsoever if we already hold that lock *) if should_skip tenv_opt event lock_state then acc
if recursive_locks && LockState.is_taken event lock_state then acc
else else
let add_first_and_eventually acc f = let add_first_and_eventually acc f =
match f.Event.elem with match f.Event.elem with
@ -269,32 +294,30 @@ let add_order_pairs ~recursive_locks lock_state event acc =
LockState.fold_over_events add_first_and_eventually lock_state acc LockState.fold_over_events add_first_and_eventually lock_state acc
let acquire ~recursive_locks ({lock_state; events; order} as astate) loc locks = let acquire tenv ({lock_state; events; order} as astate) loc locks =
let new_events = List.map locks ~f:(fun lock -> Event.make_acquire lock loc) in let new_events = List.map locks ~f:(fun lock -> Event.make_acquire lock loc) in
{ astate with { astate with
events= List.fold new_events ~init:events ~f:(fun acc e -> EventDomain.add e acc) events= List.fold new_events ~init:events ~f:(fun acc e -> EventDomain.add e acc)
; order= ; order=
List.fold new_events ~init:order ~f:(fun acc e -> List.fold new_events ~init:order ~f:(fun acc e ->
OrderDomain.union acc (add_order_pairs ~recursive_locks lock_state e order) ) OrderDomain.union acc (add_order_pairs (Some tenv) lock_state e order) )
; lock_state= ; lock_state= List.fold2_exn locks new_events ~init:lock_state ~f:LockState.acquire }
List.fold2_exn locks new_events ~init:lock_state ~f:(fun acc lock e ->
LockState.acquire lock e acc ) }
let make_call_with_event new_event astate = let make_call_with_event tenv_opt new_event astate =
{ astate with { astate with
events= EventDomain.add new_event astate.events events= EventDomain.add new_event astate.events
; order= add_order_pairs ~recursive_locks:false astate.lock_state new_event astate.order } ; order= add_order_pairs tenv_opt astate.lock_state new_event astate.order }
let blocking_call callee sev loc astate = let blocking_call callee sev loc astate =
let new_event = Event.make_blocking_call callee sev loc in let new_event = Event.make_blocking_call callee sev loc in
make_call_with_event new_event astate make_call_with_event None new_event astate
let strict_mode_call callee loc astate = let strict_mode_call callee loc astate =
let new_event = Event.make_strict_mode_call callee loc in let new_event = Event.make_strict_mode_call callee loc in
make_call_with_event new_event astate make_call_with_event None new_event astate
let release ({lock_state} as astate) locks = let release ({lock_state} as astate) locks =
@ -302,26 +325,19 @@ let release ({lock_state} as astate) locks =
lock_state= List.fold locks ~init:lock_state ~f:(fun acc l -> LockState.release l acc) } lock_state= List.fold locks ~init:lock_state ~f:(fun acc l -> LockState.release l acc) }
let integrate_summary ~recursive_locks ({lock_state; events; order; ui} as astate) callee_pname loc let integrate_summary tenv ({lock_state; events; order; ui} as astate) callee_pname loc
callee_summary = callee_summary =
let callsite = CallSite.make callee_pname loc in let callsite = CallSite.make callee_pname loc in
let callee_order = OrderDomain.with_callsite callee_summary.order callsite in let callee_order = OrderDomain.with_callsite callee_summary.order callsite in
let callee_ui = UIThreadDomain.with_callsite callee_summary.ui callsite in let callee_ui = UIThreadDomain.with_callsite callee_summary.ui callsite in
let should_keep event = should_skip (Some tenv) event lock_state |> not in
let filtered_order = let filtered_order =
if recursive_locks then OrderDomain.filter (fun {elem= {eventually}} -> should_keep eventually) callee_order
OrderDomain.filter
(fun {elem= {eventually}} -> LockState.is_taken eventually lock_state |> not)
callee_order
else callee_order
in in
let callee_events = EventDomain.with_callsite callee_summary.events callsite in let callee_events = EventDomain.with_callsite callee_summary.events callsite in
let filtered_events = let filtered_events = EventDomain.filter should_keep callee_events in
if recursive_locks then
EventDomain.filter (fun e -> LockState.is_taken e lock_state |> not) callee_events
else callee_events
in
let order' = let order' =
EventDomain.fold (add_order_pairs ~recursive_locks lock_state) filtered_events filtered_order EventDomain.fold (add_order_pairs (Some tenv) lock_state) filtered_events filtered_order
in in
{ astate with { astate with
events= EventDomain.join events filtered_events events= EventDomain.join events filtered_events
@ -337,9 +353,9 @@ let set_on_ui_thread ({ui} as astate) loc explain =
{astate with ui} {astate with ui}
let add_guard astate guard lock ~acquire_now ~recursive_locks loc = let add_guard tenv astate guard lock ~acquire_now loc =
let astate = {astate with guard_map= GuardToLockMap.add_guard ~guard ~lock astate.guard_map} in let astate = {astate with guard_map= GuardToLockMap.add_guard ~guard ~lock astate.guard_map} in
if acquire_now then acquire ~recursive_locks astate loc [lock] else astate if acquire_now then acquire tenv astate loc [lock] else astate
let remove_guard astate guard = let remove_guard astate guard =
@ -356,10 +372,10 @@ let unlock_guard astate guard =
FlatLock.get lock_opt |> Option.to_list |> release astate ) FlatLock.get lock_opt |> Option.to_list |> release astate )
let lock_guard ~recursive_locks astate guard loc = let lock_guard tenv astate guard loc =
GuardToLockMap.find_opt guard astate.guard_map GuardToLockMap.find_opt guard astate.guard_map
|> Option.value_map ~default:astate ~f:(fun lock_opt -> |> Option.value_map ~default:astate ~f:(fun lock_opt ->
FlatLock.get lock_opt |> Option.to_list |> acquire astate ~recursive_locks loc ) FlatLock.get lock_opt |> Option.to_list |> acquire tenv astate loc )
type summary = t type summary = t

@ -80,7 +80,7 @@ type t =
include AbstractDomain.WithBottom with type t := t include AbstractDomain.WithBottom with type t := t
val acquire : recursive_locks:bool -> t -> Location.t -> Lock.t list -> t val acquire : Tenv.t -> t -> Location.t -> Lock.t list -> t
(** simultaneously acquire a number of locks, no-op if list is empty *) (** simultaneously acquire a number of locks, no-op if list is empty *)
val release : t -> Lock.t list -> t val release : t -> Lock.t list -> t
@ -94,11 +94,10 @@ val set_on_ui_thread : t -> Location.t -> string -> t
(** set the property "runs on UI thread" to true by attaching the given explanation string as to (** set the property "runs on UI thread" to true by attaching the given explanation string as to
why this method is thought to do so *) why this method is thought to do so *)
val add_guard : val add_guard : Tenv.t -> t -> HilExp.t -> Lock.t -> acquire_now:bool -> Location.t -> t
t -> HilExp.t -> Lock.t -> acquire_now:bool -> recursive_locks:bool -> Location.t -> t
(** Install a mapping from the guard expression to the lock provided, and optionally lock it. *) (** Install a mapping from the guard expression to the lock provided, and optionally lock it. *)
val lock_guard : recursive_locks:bool -> t -> HilExp.t -> Location.t -> t val lock_guard : Tenv.t -> t -> HilExp.t -> Location.t -> t
(** Acquire the lock the guard was constructed with. *) (** Acquire the lock the guard was constructed with. *)
val remove_guard : t -> HilExp.t -> t val remove_guard : t -> HilExp.t -> t
@ -111,4 +110,4 @@ type summary = t
val pp_summary : F.formatter -> summary -> unit val pp_summary : F.formatter -> summary -> unit
val integrate_summary : recursive_locks:bool -> t -> Typ.Procname.t -> Location.t -> summary -> t val integrate_summary : Tenv.t -> t -> Typ.Procname.t -> Location.t -> summary -> t

@ -136,4 +136,18 @@ class SelfDeadlock {
std::mutex mutex_; std::mutex mutex_;
}; };
class PathSensitive {
public:
void FP_ok() {
std::lock_guard<std::mutex> l(mutex_);
bool flag = false;
if (flag) {
std::lock_guard<std::mutex> l(mutex_);
}
}
private:
std::mutex mutex_;
};
} // namespace basics } // namespace basics

@ -1,9 +1,7 @@
codetoanalyze/cpp/starvation/basics.cpp, basics::Basic_thread1_bad, 18, DEADLOCK, no_bucket, ERROR, [[Trace 1] `basics::Basic_thread1_bad`,locks `this.mutex_1` in class `basics::Basic*`,locks `this.mutex_2` in class `basics::Basic*`,[Trace 2] `basics::Basic_thread2_bad`,locks `this.mutex_2` in class `basics::Basic*`,locks `this.mutex_1` in class `basics::Basic*`] codetoanalyze/cpp/starvation/basics.cpp, basics::Basic_thread1_bad, 18, DEADLOCK, no_bucket, ERROR, [[Trace 1] `basics::Basic_thread1_bad`,locks `this.mutex_1` in class `basics::Basic*`,locks `this.mutex_2` in class `basics::Basic*`,[Trace 2] `basics::Basic_thread2_bad`,locks `this.mutex_2` in class `basics::Basic*`,locks `this.mutex_1` in class `basics::Basic*`]
codetoanalyze/cpp/starvation/basics.cpp, basics::PathSensitive_FP_ok, 142, DEADLOCK, no_bucket, ERROR, [In method`basics::PathSensitive_FP_ok`,locks `this.mutex_` in class `basics::PathSensitive*`,locks `this.mutex_` in class `basics::PathSensitive*`]
codetoanalyze/cpp/starvation/basics.cpp, basics::SelfDeadlock_complicated_bad, 131, DEADLOCK, no_bucket, ERROR, [In method`basics::SelfDeadlock_complicated_bad`,locks `this.mutex_` in class `basics::SelfDeadlock*`,locks `this.mutex_` in class `basics::SelfDeadlock*`] codetoanalyze/cpp/starvation/basics.cpp, basics::SelfDeadlock_complicated_bad, 131, DEADLOCK, no_bucket, ERROR, [In method`basics::SelfDeadlock_complicated_bad`,locks `this.mutex_` in class `basics::SelfDeadlock*`,locks `this.mutex_` in class `basics::SelfDeadlock*`]
codetoanalyze/cpp/starvation/basics.cpp, basics::SelfDeadlock_interproc1_bad, 114, DEADLOCK, no_bucket, ERROR, [In method`basics::SelfDeadlock_interproc1_bad`,locks `this.mutex_` in class `basics::SelfDeadlock*`,Method call: `basics::SelfDeadlock_interproc2_bad`,locks `this.mutex_` in class `basics::SelfDeadlock*`] codetoanalyze/cpp/starvation/basics.cpp, basics::SelfDeadlock_interproc1_bad, 114, DEADLOCK, no_bucket, ERROR, [In method`basics::SelfDeadlock_interproc1_bad`,locks `this.mutex_` in class `basics::SelfDeadlock*`,Method call: `basics::SelfDeadlock_interproc2_bad`,locks `this.mutex_` in class `basics::SelfDeadlock*`]
codetoanalyze/cpp/starvation/basics.cpp, basics::SelfDeadlock_thread_bad, 105, DEADLOCK, no_bucket, ERROR, [In method`basics::SelfDeadlock_thread_bad`,locks `this.mutex_` in class `basics::SelfDeadlock*`,locks `this.mutex_` in class `basics::SelfDeadlock*`] codetoanalyze/cpp/starvation/basics.cpp, basics::SelfDeadlock_thread_bad, 105, DEADLOCK, no_bucket, ERROR, [In method`basics::SelfDeadlock_thread_bad`,locks `this.mutex_` in class `basics::SelfDeadlock*`,locks `this.mutex_` in class `basics::SelfDeadlock*`]
codetoanalyze/cpp/starvation/basics.cpp, basics::WithGuard_thread1_bad, 44, DEADLOCK, no_bucket, ERROR, [[Trace 1] `basics::WithGuard_thread1_bad`,locks `this.mutex_1` in class `basics::WithGuard*`,locks `this.mutex_2` in class `basics::WithGuard*`,[Trace 2] `basics::WithGuard_thread2_bad`,locks `this.mutex_2` in class `basics::WithGuard*`,locks `this.mutex_1` in class `basics::WithGuard*`] codetoanalyze/cpp/starvation/basics.cpp, basics::WithGuard_thread1_bad, 44, DEADLOCK, no_bucket, ERROR, [[Trace 1] `basics::WithGuard_thread1_bad`,locks `this.mutex_1` in class `basics::WithGuard*`,locks `this.mutex_2` in class `basics::WithGuard*`,[Trace 2] `basics::WithGuard_thread2_bad`,locks `this.mutex_2` in class `basics::WithGuard*`,locks `this.mutex_1` in class `basics::WithGuard*`]
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*`] 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*`]

@ -22,27 +22,17 @@ class Recursive {
public: public:
Recursive() {} Recursive() {}
void FP_multi_ok() { void multi_ok() {
std::lock_guard<std::recursive_mutex> l(recursive_mutex_); std::lock_guard<std::recursive_mutex> l(recursive_mutex_);
{ std::lock_guard<std::recursive_mutex> l(recursive_mutex_); } { std::lock_guard<std::recursive_mutex> l(recursive_mutex_); }
} }
void FP_unknown_ok() { void unknown_ok() {
std::lock_guard<UnknownMutex> l(umutex_); std::lock_guard<UnknownMutex> l(umutex_);
{ std::lock_guard<UnknownMutex> l(umutex_); } { std::lock_guard<UnknownMutex> l(umutex_); }
} }
void FP_path_sensitive_ok() {
std::lock_guard<std::mutex> l(mutex_);
bool flag = false;
if (flag) {
std::lock_guard<std::mutex> l(mutex_);
}
}
private: private:
std::recursive_mutex recursive_mutex_; std::recursive_mutex recursive_mutex_;
std::mutex mutex_;
UnknownMutex umutex_; UnknownMutex umutex_;
}; };

Loading…
Cancel
Save