From 1121efbe59bb5c16a7c0582ef0a302cfa5c6b50d Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Thu, 22 Nov 2018 07:16:30 -0800 Subject: [PATCH] [concurrency] refactor C++ models Reviewed By: jberdine Differential Revision: D13153721 fbshipit-source-id: 316f1922d --- infer/src/absint/LowerHil.ml | 2 +- infer/src/concurrency/ConcurrencyModels.ml | 274 ++++++++++++-------- infer/src/concurrency/ConcurrencyModels.mli | 9 +- infer/src/concurrency/RacerD.ml | 8 +- infer/src/concurrency/starvation.ml | 29 +-- infer/src/concurrency/starvationDomain.ml | 19 +- infer/src/concurrency/starvationDomain.mli | 6 +- 7 files changed, 213 insertions(+), 134 deletions(-) diff --git a/infer/src/absint/LowerHil.ml b/infer/src/absint/LowerHil.ml index 7d211257c..ba9e72806 100644 --- a/infer/src/absint/LowerHil.ml +++ b/infer/src/absint/LowerHil.ml @@ -49,7 +49,7 @@ struct let is_java_unlock pname actuals = (* would check is_java, but we want to include builtins too *) (not (Typ.Procname.is_c_method pname)) - && match ConcurrencyModels.get_lock pname actuals with Unlock -> true | _ -> false + && match ConcurrencyModels.get_lock_effect pname actuals with Unlock _ -> true | _ -> false let exec_instr_actual extras id_map node hil_instr actual_state = diff --git a/infer/src/concurrency/ConcurrencyModels.ml b/infer/src/concurrency/ConcurrencyModels.ml index 348a69c85..9b362f9d1 100644 --- a/infer/src/concurrency/ConcurrencyModels.ml +++ b/infer/src/concurrency/ConcurrencyModels.ml @@ -9,7 +9,11 @@ open! IStd module F = Format module MF = MarkupFormatter -type lock = Lock | Unlock | LockedIfTrue | NoEffect +type lock_effect = + | Lock of HilExp.t list + | Unlock of HilExp.t list + | LockedIfTrue of HilExp.t list + | NoEffect type thread = BackgroundThread | MainThread | MainThreadIfTrue | UnknownThread @@ -41,116 +45,179 @@ let get_thread = function UnknownThread -let cpp_lock_types_matcher = - QualifiedCppName.Match.of_fuzzy_qual_names - [ "apache::thrift::concurrency::ReadWriteMutex" - ; "folly::LockedPtr" - ; "folly::MicroSpinLock" - ; "folly::RWSpinLock" - ; "folly::SharedMutex" - (* NB not impl as in [matcher_lock] as this is just a type, not a call *) - ; "folly::SpinLock" - ; "folly::SpinLockGuard" - ; "std::mutex" ] - - -let get_lock = - let is_cpp_lock = - let matcher_lock = - QualifiedCppName.Match.of_fuzzy_qual_names - [ "apache::thrift::concurrency::ReadWriteMutex::acquireRead" - ; "apache::thrift::concurrency::ReadWriteMutex::acquireWrite" - ; "folly::MicroSpinLock::lock" - ; "folly::RWSpinLock::lock" - ; "folly::RWSpinLock::lock_shared" - ; "folly::SharedMutexImpl::lockExclusiveImpl" - ; "folly::SharedMutexImpl::lockSharedImpl" - ; "folly::SpinLock::lock" - ; "std::lock" - ; "std::mutex::lock" - ; "std::unique_lock::lock" ] +module Clang : sig + val get_lock_effect : Typ.Procname.t -> HilExp.t list -> lock_effect + + val lock_types_matcher : QualifiedCppName.Match.quals_matcher +end = struct + type lock_model = {cls: string; lck: string list; tlk: string list; unl: string list} + + let lock_models = + let def = {cls= ""; lck= ["lock"]; tlk= ["try_lock"]; unl= ["unlock"]} in + let shd = + { cls= "std::shared_mutex" + ; lck= "lock_shared" :: def.lck + ; tlk= "try_lock_shared" :: def.tlk + ; unl= "unlock_shared" :: def.unl } in - let matcher_lock_constructor = - QualifiedCppName.Match.of_fuzzy_qual_names - [ "folly::LockedPtr::LockedPtr" - ; "folly::SpinLockGuard::SpinLockGuard" - ; "std::lock_guard::lock_guard" - ; "std::unique_lock::unique_lock" ] + let rwm = + { cls= "apache::thrift::concurrency::ReadWriteMutex" + ; lck= ["acquireRead"; "acquireWrite"] + ; tlk= ["attemptRead"; "attemptWrite"] + ; unl= ["release"] } in - fun pname actuals -> - QualifiedCppName.Match.match_qualifiers matcher_lock (Typ.Procname.get_qualifiers pname) - || QualifiedCppName.Match.match_qualifiers matcher_lock_constructor - (Typ.Procname.get_qualifiers pname) - (* Passing additional parameter allows to defer the lock *) - && Int.equal 2 (List.length actuals) - and is_cpp_unlock = - let matcher = - QualifiedCppName.Match.of_fuzzy_qual_names - [ "apache::thrift::concurrency::ReadWriteMutex::release" - ; "folly::LockedPtr::~LockedPtr" - ; "folly::MicroSpinLock::unlock" - ; "folly::RWSpinLock::unlock" - ; "folly::RWSpinLock::unlock_shared" - ; "folly::SharedMutexImpl::unlock" - ; "folly::SharedMutexImpl::unlock_shared" - ; "folly::SpinLock::unlock" - ; "folly::SpinLockGuard::~SpinLockGuard" - ; "std::lock_guard::~lock_guard" - ; "std::mutex::unlock" - ; "std::unique_lock::unlock" - ; "std::unique_lock::~unique_lock" ] + [ {def with cls= "apache::thrift::concurrency::Monitor"; tlk= "timedlock" :: def.tlk} + ; {def with cls= "apache::thrift::concurrency::Mutex"; tlk= "timedlock" :: def.tlk} + ; {rwm with cls= "apache::thrift::concurrency::NoStarveReadWriteMutex"} + ; rwm + ; {shd with cls= "boost::shared_mutex"} + ; {def with cls= "boost::mutex"} + ; {def with cls= "folly::MicroSpinLock"} + ; {shd with cls= "folly::RWSpinLock"} + ; {shd with cls= "folly::SharedMutex"} + ; {shd with cls= "folly::SharedMutexImpl"} + ; {def with cls= "folly::SpinLock"} + ; {def with cls= "std::shared_lock"} + ; {def with cls= "std::mutex"} + ; shd + ; {def with cls= "std::unique_lock"; tlk= "owns_lock" :: def.tlk} ] + + + let mk_model_matcher ~f = + let lock_methods = + List.concat_map lock_models ~f:(fun mdl -> + List.map (f mdl) ~f:(fun mtd -> mdl.cls ^ "::" ^ mtd) ) in + let matcher = QualifiedCppName.Match.of_fuzzy_qual_names lock_methods in fun pname -> QualifiedCppName.Match.match_qualifiers matcher (Typ.Procname.get_qualifiers pname) - and is_cpp_trylock = - let matcher = - QualifiedCppName.Match.of_fuzzy_qual_names - ["folly::SpinLock::try_lock"; "std::unique_lock::owns_lock"; "std::unique_lock::try_lock"] + + + let is_lock = mk_model_matcher ~f:(fun mdl -> mdl.lck) + + let is_unlock = mk_model_matcher ~f:(fun mdl -> mdl.unl) + + let is_trylock = mk_model_matcher ~f:(fun mdl -> mdl.tlk) + + let lock_types_matcher = + let class_names = List.map lock_models ~f:(fun mdl -> mdl.cls) in + QualifiedCppName.Match.of_fuzzy_qual_names class_names + + + (* TODO std::scoped_lock *) + + let guards = + [ "apache::thrift::concurrency::Guard" + ; "apache::thrift::concurrency::Synchronized" + ; "apache::thrift::concurrency::RWGuard" + ; "folly::SharedMutex::ReadHolder" + ; "folly::SharedMutex::WriteHolder" + ; "folly::LockedPtr" + ; "folly::SpinLockGuard" + ; "std::lock_guard" + ; "std::shared_lock" + ; "std::unique_lock" ] + + + let get_guard_constructor, get_guard_destructor = + let get_class_and_qual_name guard = + let qual_name = QualifiedCppName.of_qual_string guard in + let class_name, _ = Option.value_exn (QualifiedCppName.extract_last qual_name) in + (class_name, qual_name) in + ( (fun guard -> + let class_name, qual_name = get_class_and_qual_name guard in + let qual_constructor = QualifiedCppName.append_qualifier qual_name ~qual:class_name in + QualifiedCppName.to_qual_string qual_constructor ) + , fun guard -> + let class_name, qual_name = get_class_and_qual_name guard in + let qual_destructor = + QualifiedCppName.append_qualifier qual_name ~qual:("~" ^ class_name) + in + QualifiedCppName.to_qual_string qual_destructor ) + + + let is_guard_lock = + let constructors = List.map guards ~f:get_guard_constructor in + let matcher = QualifiedCppName.Match.of_fuzzy_qual_names constructors in + fun pname actuals -> + QualifiedCppName.Match.match_qualifiers matcher (Typ.Procname.get_qualifiers pname) + (* Passing additional parameter allows to defer the lock *) + && Int.equal 2 (List.length actuals) + + + let is_guard_unlock = + let destructors = List.map guards ~f:get_guard_destructor in + let matcher = QualifiedCppName.Match.of_fuzzy_qual_names destructors in fun pname -> QualifiedCppName.Match.match_qualifiers matcher (Typ.Procname.get_qualifiers pname) - in - fun pname actuals -> + + + let is_std_lock = + let matcher = QualifiedCppName.Match.of_fuzzy_qual_names ["std::lock"] in + fun pname -> + QualifiedCppName.Match.match_qualifiers matcher (Typ.Procname.get_qualifiers pname) + + + let get_lock_effect pname actuals = + let fst_arg = match actuals with x :: _ -> [x] | _ -> [] in + let snd_arg = match actuals with _ :: x :: _ -> [x] | _ -> [] in + if is_std_lock pname then Lock actuals + else if is_lock pname then Lock fst_arg + else if is_guard_lock pname actuals then Lock snd_arg + else if is_unlock pname then Unlock fst_arg + else if is_guard_unlock pname then Unlock snd_arg + else if is_trylock pname then LockedIfTrue fst_arg + else NoEffect +end + +module Java : sig + val get_lock_effect : Typ.Procname.t -> Typ.Procname.Java.t -> HilExp.t list -> lock_effect +end = struct + let std_locks = + [ "java.util.concurrent.locks.Lock" + ; "java.util.concurrent.locks.ReentrantLock" + ; "java.util.concurrent.locks.ReentrantReadWriteLock$ReadLock" + ; "java.util.concurrent.locks.ReentrantReadWriteLock$WriteLock" ] + + + let is_lock classname methodname = + List.mem std_locks classname ~equal:String.equal + && List.mem ["lock"; "lockInterruptibly"] methodname ~equal:String.equal + || String.equal classname "com.facebook.buck.util.concurrent.AutoCloseableReadWriteUpdateLock" + && List.mem ["readLock"; "updateLock"; "writeLock"] methodname ~equal:String.equal + + + let is_unlock classname methodname = + String.equal methodname "unlock" && List.mem std_locks classname ~equal:String.equal + + + let is_trylock classname methodname = + String.equal methodname "tryLock" && List.mem std_locks classname ~equal:String.equal + + + let get_lock_effect pname java_pname actuals = + let fst_arg = match actuals with x :: _ -> [x] | _ -> [] in + if is_thread_utils_method "assertHoldsLock" pname then Lock fst_arg + else + let classname = Typ.Procname.Java.get_class_name java_pname in + let methodname = Typ.Procname.Java.get_method java_pname in + if is_lock classname methodname then Lock fst_arg + else if is_unlock classname methodname then Unlock fst_arg + else if is_trylock classname methodname then LockedIfTrue fst_arg + else NoEffect +end + +let get_lock_effect pname actuals = + let fst_arg = match actuals with x :: _ -> [x] | _ -> [] in + if Typ.Procname.equal pname BuiltinDecl.__set_locked_attribute then Lock fst_arg + else if Typ.Procname.equal pname BuiltinDecl.__delete_locked_attribute then Unlock fst_arg + else match pname with - | Typ.Procname.Java java_pname -> ( - if is_thread_utils_method "assertHoldsLock" (Typ.Procname.Java java_pname) then Lock - else - match - (Typ.Procname.Java.get_class_name java_pname, Typ.Procname.Java.get_method java_pname) - with - | ( ( "java.util.concurrent.locks.Lock" - | "java.util.concurrent.locks.ReentrantLock" - | "java.util.concurrent.locks.ReentrantReadWriteLock$ReadLock" - | "java.util.concurrent.locks.ReentrantReadWriteLock$WriteLock" ) - , ("lock" | "lockInterruptibly") ) -> - Lock - | ( ( "java.util.concurrent.locks.Lock" - | "java.util.concurrent.locks.ReentrantLock" - | "java.util.concurrent.locks.ReentrantReadWriteLock$ReadLock" - | "java.util.concurrent.locks.ReentrantReadWriteLock$WriteLock" ) - , "unlock" ) -> - Unlock - | ( ( "java.util.concurrent.locks.Lock" - | "java.util.concurrent.locks.ReentrantLock" - | "java.util.concurrent.locks.ReentrantReadWriteLock$ReadLock" - | "java.util.concurrent.locks.ReentrantReadWriteLock$WriteLock" ) - , "tryLock" ) -> - LockedIfTrue - | ( "com.facebook.buck.util.concurrent.AutoCloseableReadWriteUpdateLock" - , ("readLock" | "updateLock" | "writeLock") ) -> - Lock - | _ -> - NoEffect ) - | (Typ.Procname.ObjC_Cpp _ | C _) as pname when is_cpp_lock pname actuals -> - Lock - | (Typ.Procname.ObjC_Cpp _ | C _) as pname when is_cpp_unlock pname -> - Unlock - | (Typ.Procname.ObjC_Cpp _ | C _) as pname when is_cpp_trylock pname -> - LockedIfTrue - | pname when Typ.Procname.equal pname BuiltinDecl.__set_locked_attribute -> - Lock - | pname when Typ.Procname.equal pname BuiltinDecl.__delete_locked_attribute -> - Unlock + | Typ.Procname.Java java_pname -> + Java.get_lock_effect pname java_pname actuals + | Typ.Procname.(ObjC_Cpp _ | C _) -> + Clang.get_lock_effect pname actuals | _ -> NoEffect @@ -269,3 +336,6 @@ let runs_on_ui_thread = (MF.monospaced_to_string Annotations.ui_thread)) | _ -> None ) + + +let cpp_lock_types_matcher = Clang.lock_types_matcher diff --git a/infer/src/concurrency/ConcurrencyModels.mli b/infer/src/concurrency/ConcurrencyModels.mli index 48ddde83f..1b3a74369 100644 --- a/infer/src/concurrency/ConcurrencyModels.mli +++ b/infer/src/concurrency/ConcurrencyModels.mli @@ -8,7 +8,12 @@ open! IStd module F = Format -type lock = Lock | Unlock | LockedIfTrue | NoEffect +(** effect of call plus Hil expressions being un/locked, if known *) +type lock_effect = + | Lock of HilExp.t list + | Unlock of HilExp.t list + | LockedIfTrue of HilExp.t list + | NoEffect type thread = BackgroundThread | MainThread | MainThreadIfTrue | UnknownThread @@ -16,7 +21,7 @@ val is_thread_utils_method : string -> Typ.Procname.t -> bool (** return true if the given method name is a utility class for checking what thread we're on TODO: clean this up so it takes only a procname *) -val get_lock : Typ.Procname.t -> HilExp.t list -> lock +val get_lock_effect : Typ.Procname.t -> HilExp.t list -> lock_effect (** describe how this procedure behaves with respect to locking *) val get_thread : Typ.Procname.t -> thread diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index 168cdfc76..9ce13d822 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -414,16 +414,16 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | _ -> ThreadsDomain.AnyThread in - match get_lock callee_pname actuals with - | Lock -> + match get_lock_effect callee_pname actuals with + | Lock _ -> { astate with locks= LocksDomain.acquire_lock astate.locks ; threads= update_for_lock_use astate.threads } - | Unlock -> + | Unlock _ -> { astate with locks= LocksDomain.release_lock astate.locks ; threads= update_for_lock_use astate.threads } - | LockedIfTrue -> + | LockedIfTrue _ -> let attribute_map = AttributeMapDomain.add_attribute ret_access_path (Choice Choice.LockHeld) astate.attribute_map diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index 693880e12..6b4c4b0be 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -58,9 +58,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let open ConcurrencyModels in let open StarvationModels in let is_formal base = FormalMap.is_formal base extras in - let get_path actuals = + let get_lock_path actuals = match actuals with - | HilExp.AccessExpression access_exp :: _ -> ( + | HilExp.AccessExpression access_exp -> ( match AccessExpression.to_access_path access_exp with | (((Var.ProgramVar pvar, _) as base), _) as path when is_formal base || Pvar.is_global pvar -> @@ -68,26 +68,24 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | _ -> (* ignore paths on local or logical variables *) None ) - | HilExp.Constant (Const.Cclass class_id) :: _ -> + | HilExp.Constant (Const.Cclass class_id) -> (* this is a synchronized/lock(CLASSNAME.class) construct *) Some (lock_of_class class_id) | _ -> None in - let do_lock actuals loc astate = - get_path actuals |> Option.value_map ~default:astate ~f:(Domain.acquire astate loc) - in - let do_unlock actuals astate = - get_path actuals |> Option.value_map ~default:astate ~f:(Domain.release astate) + let do_lock locks loc astate = + List.filter_map ~f:get_lock_path locks |> Domain.acquire astate loc in + let do_unlock locks astate = List.filter_map ~f:get_lock_path locks |> Domain.release astate in match instr with | Call (_, Direct callee, actuals, _, loc) -> ( - match get_lock callee actuals with - | Lock -> - do_lock actuals loc astate - | Unlock -> - do_unlock actuals astate - | LockedIfTrue -> + match get_lock_effect callee actuals with + | Lock locks -> + do_lock locks loc astate + | Unlock locks -> + do_unlock locks astate + | LockedIfTrue _ -> astate | NoEffect when should_skip_analysis tenv callee actuals -> astate @@ -141,8 +139,7 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} = | _ -> FormalMap.get_formal_base 0 formals |> Option.map ~f:(fun base -> (base, [])) in - Option.value_map lock ~default:StarvationDomain.empty - ~f:(StarvationDomain.acquire StarvationDomain.empty loc) + StarvationDomain.acquire StarvationDomain.empty loc (Option.to_list lock) in let initial = ConcurrencyModels.runs_on_ui_thread tenv proc_desc diff --git a/infer/src/concurrency/starvationDomain.ml b/infer/src/concurrency/starvationDomain.ml index 70fa7232c..1d797a821 100644 --- a/infer/src/concurrency/starvationDomain.ml +++ b/infer/src/concurrency/starvationDomain.ml @@ -255,12 +255,16 @@ let add_order_pairs lock_state event acc = LockState.fold_over_events add_first_and_eventually lock_state acc -let acquire ({lock_state; events; order} as astate) loc lock = - let new_event = Event.make_acquire lock loc in +let acquire ({lock_state; events; order} as astate) loc locks = + let new_events = List.map locks ~f:(fun lock -> Event.make_acquire lock loc) in { astate with - lock_state= LockState.acquire lock new_event lock_state - ; events= EventDomain.add new_event events - ; order= add_order_pairs lock_state new_event order } + events= List.fold new_events ~init:events ~f:(fun acc e -> EventDomain.add e acc) + ; order= + List.fold new_events ~init:order ~f:(fun acc e -> + OrderDomain.union acc (add_order_pairs lock_state e order) ) + ; lock_state= + List.fold2_exn locks new_events ~init:lock_state ~f:(fun acc lock e -> + LockState.acquire lock e acc ) } let blocking_call callee sev loc ({lock_state; events; order} as astate) = @@ -275,8 +279,9 @@ let strict_mode_call callee loc ({lock_state; events; order} as astate) = events= EventDomain.add new_event events; order= add_order_pairs lock_state new_event order } -let release ({lock_state} as astate) lock = - {astate with lock_state= LockState.release lock lock_state} +let release ({lock_state} as astate) locks = + { astate with + lock_state= List.fold locks ~init:lock_state ~f:(fun acc l -> LockState.release l acc) } let integrate_summary ({lock_state; events; order; ui} as astate) callee_pname loc callee_summary = diff --git a/infer/src/concurrency/starvationDomain.mli b/infer/src/concurrency/starvationDomain.mli index 720e36d16..74d7a5b22 100644 --- a/infer/src/concurrency/starvationDomain.mli +++ b/infer/src/concurrency/starvationDomain.mli @@ -77,9 +77,11 @@ type astate = include AbstractDomain.WithBottom with type astate := astate -val acquire : astate -> Location.t -> Lock.t -> astate +val acquire : astate -> Location.t -> Lock.t list -> astate +(** simultaneously acquire a number of locks, no-op if list is empty *) -val release : astate -> Lock.t -> astate +val release : astate -> Lock.t list -> astate +(** simultaneously release a number of locks, no-op if list is empty *) val blocking_call : Typ.Procname.t -> Event.severity_t -> Location.t -> astate -> astate