[concurrency] refactor C++ models

Reviewed By: jberdine

Differential Revision: D13153721

fbshipit-source-id: 316f1922d

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 =

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 =
+module Clang : sig
-  QualifiedCppName.Match.of_fuzzy_qual_names
+  val get_lock_effect : Typ.Procname.t -> HilExp.t list -> lock_effect
-    [ "apache::thrift::concurrency::ReadWriteMutex"
+
+  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 rwm =
+      { cls= "apache::thrift::concurrency::ReadWriteMutex"
+      ; lck= ["acquireRead"; "acquireWrite"]
+      ; tlk= ["attemptRead"; "attemptWrite"]
+      ; unl= ["release"] }
+    in
+    [ {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)
+
+
+  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::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" ]
+    ; "std::lock_guard"
-
+    ; "std::shared_lock"
-
+    ; "std::unique_lock" ]
-let get_lock =
+
-  let is_cpp_lock =
+
-    let matcher_lock =
+  let get_guard_constructor, get_guard_destructor =
-      QualifiedCppName.Match.of_fuzzy_qual_names
+    let get_class_and_qual_name guard =
-        [ "apache::thrift::concurrency::ReadWriteMutex::acquireRead"
+      let qual_name = QualifiedCppName.of_qual_string guard in
-        ; "apache::thrift::concurrency::ReadWriteMutex::acquireWrite"
+      let class_name, _ = Option.value_exn (QualifiedCppName.extract_last qual_name) in
-        ; "folly::MicroSpinLock::lock"
+      (class_name, qual_name)
-        ; "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" ]
     in
-    let matcher_lock_constructor =
+    ( (fun guard ->
-      QualifiedCppName.Match.of_fuzzy_qual_names
+        let class_name, qual_name = get_class_and_qual_name guard in
-        [ "folly::LockedPtr::LockedPtr"
+        let qual_constructor = QualifiedCppName.append_qualifier qual_name ~qual:class_name in
-        ; "folly::SpinLockGuard::SpinLockGuard"
+        QualifiedCppName.to_qual_string qual_constructor )
-        ; "std::lock_guard::lock_guard"
+    , fun guard ->
-        ; "std::unique_lock::unique_lock" ]
+        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_lock (Typ.Procname.get_qualifiers pname)
+      QualifiedCppName.Match.match_qualifiers matcher (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
+  let is_guard_unlock =
-        [ "apache::thrift::concurrency::ReadWriteMutex::release"
+    let destructors = List.map guards ~f:get_guard_destructor in
-        ; "folly::LockedPtr::~LockedPtr"
+    let matcher = QualifiedCppName.Match.of_fuzzy_qual_names destructors in
-        ; "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" ]
-    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
+  let is_std_lock =
-        ["folly::SpinLock::try_lock"; "std::unique_lock::owns_lock"; "std::unique_lock::try_lock"]
+    let matcher = QualifiedCppName.Match.of_fuzzy_qual_names ["std::lock"] in
-    in
     fun pname ->
       QualifiedCppName.Match.match_qualifiers matcher (Typ.Procname.get_qualifiers pname)
-  in
+
-  fun pname actuals ->
+
-    match pname with
+  let get_lock_effect pname actuals =
-    | Typ.Procname.Java java_pname -> (
+    let fst_arg = match actuals with x :: _ -> [x] | _ -> [] in
-        if is_thread_utils_method "assertHoldsLock" (Typ.Procname.Java java_pname) then Lock
+    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
-          match
+      let classname = Typ.Procname.Java.get_class_name java_pname in
-            (Typ.Procname.Java.get_class_name java_pname, Typ.Procname.Java.get_method java_pname)
+      let methodname = Typ.Procname.Java.get_method java_pname in
-          with
+      if is_lock classname methodname then Lock fst_arg
-          | ( ( "java.util.concurrent.locks.Lock"
+      else if is_unlock classname methodname then Unlock fst_arg
-              | "java.util.concurrent.locks.ReentrantLock"
+      else if is_trylock classname methodname then LockedIfTrue fst_arg
-              | "java.util.concurrent.locks.ReentrantReadWriteLock$ReadLock"
+      else NoEffect
-              | "java.util.concurrent.locks.ReentrantReadWriteLock$WriteLock" )
+end
-            , ("lock" | "lockInterruptibly") ) ->
+
-              Lock
+let get_lock_effect pname actuals =
-          | ( ( "java.util.concurrent.locks.Lock"
+  let fst_arg = match actuals with x :: _ -> [x] | _ -> [] in
-              | "java.util.concurrent.locks.ReentrantLock"
+  if Typ.Procname.equal pname BuiltinDecl.__set_locked_attribute then Lock fst_arg
-              | "java.util.concurrent.locks.ReentrantReadWriteLock$ReadLock"
+  else if Typ.Procname.equal pname BuiltinDecl.__delete_locked_attribute then Unlock fst_arg
-              | "java.util.concurrent.locks.ReentrantReadWriteLock$WriteLock" )
+  else
-            , "unlock" ) ->
+    match pname with
-              Unlock
+    | Typ.Procname.Java java_pname ->
-          | ( ( "java.util.concurrent.locks.Lock"
+        Java.get_lock_effect pname java_pname actuals
-              | "java.util.concurrent.locks.ReentrantLock"
+    | Typ.Procname.(ObjC_Cpp _ | C _) ->
-              | "java.util.concurrent.locks.ReentrantReadWriteLock$ReadLock"
+        Clang.get_lock_effect pname actuals
-              | "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
     | _ ->
         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

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

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
+            match get_lock_effect callee_pname actuals with
-            | Lock ->
+            | 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

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 =
+    let do_lock locks loc astate =
-      get_path actuals |> Option.value_map ~default:astate ~f:(Domain.acquire astate loc)
+      List.filter_map ~f:get_lock_path locks |> Domain.acquire astate loc
-    in
-    let do_unlock actuals astate =
-      get_path actuals |> Option.value_map ~default:astate ~f:(Domain.release astate)
     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
+      match get_lock_effect callee actuals with
-      | Lock ->
+      | Lock locks ->
-          do_lock actuals loc astate
+          do_lock locks loc astate
-      | Unlock ->
+      | Unlock locks ->
-          do_unlock actuals astate
+          do_unlock locks astate
-      | LockedIfTrue ->
+      | 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
+      StarvationDomain.acquire StarvationDomain.empty loc (Option.to_list lock)
-        ~f:(StarvationDomain.acquire StarvationDomain.empty loc)
   in
   let initial =
     ConcurrencyModels.runs_on_ui_thread tenv proc_desc

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 acquire ({lock_state; events; order} as astate) loc locks =
-  let new_event = Event.make_acquire lock loc in
+  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= List.fold new_events ~init:events ~f:(fun acc e -> EventDomain.add e acc)
-  ; events= EventDomain.add new_event events
+  ; order=
-  ; order= add_order_pairs lock_state new_event 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 =
+let release ({lock_state} as astate) locks =
-  {astate with lock_state= LockState.release lock lock_state}
+  { 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 =

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