Track multiplicities for mustLocks

src/analyses/deadlock.ml

@@ -37,7 +37,7 @@ struct
         ) ctx.local;
       D.add after ctx.local
 
-    let remove ctx l =
+    let remove ctx ?(warn=true) l =
       let inLockAddrs (e, _, _) = Lock.equal l e in
       D.filter (neg inLockAddrs) ctx.local
   end

src/analyses/locksetAnalysis.ml

@@ -30,7 +30,7 @@ sig
   module V: SpecSysVar
 
   val add: (D.t, G.t, D.t, V.t) ctx -> LockDomain.Lockset.Lock.t -> D.t
-  val remove: (D.t, G.t, D.t, V.t) ctx -> ValueDomain.Addr.t -> D.t
+  val remove: (D.t, G.t, D.t, V.t) ctx -> ?warn:bool -> ValueDomain.Addr.t -> D.t
 end
 
 module MakeMay (Arg: MayArg) =

src/analyses/mayLocks.ml

@@ -29,8 +29,8 @@ struct
     else
       D.add l ctx.local
 
-  let remove ctx l =
-    if not (D.mem l ctx.local) then M.warn "Releasing a mutex that is definitely not held";
+  let remove ctx ?(warn=true) l =
+    if warn && not (D.mem l ctx.local) then M.warn "Releasing a mutex that is definitely not held";
     match D.Addr.to_var_offset l with
     | Some (v,o) ->
       (let mtype = ctx.ask (Queries.MutexType (v, Lval.OffsetNoIdx.of_offs o)) in

src/analyses/mutexAnalysis.ml

@@ -15,7 +15,32 @@ module Spec =
 struct
   module Arg =
   struct
-    module D = Lockset
+    module Count = Lattice.Reverse(
+        Lattice.Chain (struct
+          let n () = 5
+          let names x = if x = (n () - 1) then "top" else Format.asprintf "%d" x
+        end))
+
+    module Multiplicity = struct
+      include MapDomain.MapBot_LiftTop (ValueDomain.Addr) (Count)
+      let increment v x =
+        let current = find v x in
+        if current = (4) then
+          x
+        else
+          add v (current + 1) x
+
+      let decrement v x =
+        let current = find v x in
+        if current = 0 then
+          (x, true)
+        else
+          (add v (current - 1) x, current-1 = 0)
+    end
+    module D = struct include Lattice.Prod(Lockset)(Multiplicity)
+      let empty () = (Lockset.empty (), Multiplicity.empty ())
+    end
+
 
     (** Global data is collected using dirty side-effecting. *)
 
@@ -111,20 +136,36 @@ struct
       let create_protected protected = `Lifted2 protected
     end
 
-    let add ctx l =
-      D.add l ctx.local
-
-    let remove ctx l =
-      if not (D.mem (l,true) ctx.local || D.mem (l,false) ctx.local) then M.warn "unlocking mutex which may not be held";
-      D.remove (l, true) (D.remove (l, false) ctx.local)
+    let add ctx (l:Mutexes.elt*bool) =
+      let s,m = ctx.local in
+      let s' = Lockset.add l s in
+      match Addr.to_var_offset (fst l) with
+      | Some mval when MutexTypeAnalysis.must_be_recursive ctx mval ->
+        (s', Multiplicity.increment (fst l) m)
+      | _ -> (s', m)
+
+    let remove ctx ?(warn=true) l =
+      let s, m = ctx.local in
+      let rm s = Lockset.remove (l, true) (Lockset.remove (l, false) s) in
+      if warn &&  (not (Lockset.mem (l,true) s || Lockset.mem (l,false) s)) then M.warn "unlocking mutex which may not be held";
+      match Addr.to_var_offset l with
+      | Some mval when MutexTypeAnalysis.must_be_recursive ctx mval ->
+        let m',rmed = Multiplicity.decrement l m in
+        if rmed then
+          (rm s, m')
+        else
+          (s, m')
+      | _ -> (rm s, m)
 
     let remove_all ctx =
       (* Mutexes.iter (fun m ->
            ctx.emit (MustUnlock m)
          ) (D.export_locks ctx.local); *)
       (* TODO: used to have remove_nonspecial, which kept v.vname.[0] = '{' variables *)
       M.warn "unlocking unknown mutex which may not be held";
-      D.empty ()
+      (Lockset.empty (), Multiplicity.empty ())
+
+    let empty () = (Lockset.empty (), Multiplicity.empty ())
   end
   include LocksetAnalysis.MakeMust (Arg)
   let name () = "mutex"
@@ -160,22 +201,23 @@ struct
       `Index (i_exp, conv_offset_inv o)
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
+    let ls, m = ctx.local in
     (* get the set of mutexes protecting the variable v in the given mode *)
     let protecting ~write mode v = GProtecting.get ~write mode (G.protecting (ctx.global (V.protecting v))) in
     let non_overlapping locks1 locks2 = Mutexes.is_empty @@ Mutexes.inter locks1 locks2 in
     match q with
-    | Queries.MayBePublic _ when Lockset.is_bot ctx.local -> false
+    | Queries.MayBePublic _ when Lockset.is_bot ls -> false
     | Queries.MayBePublic {global=v; write; protection} ->
-      let held_locks = Lockset.export_locks (Lockset.filter snd ctx.local) in
+      let held_locks = Lockset.export_locks (Lockset.filter snd ls) in
       let protecting = protecting ~write protection v in
       (* TODO: unsound in 29/24, why did we do this before? *)
       (* if Mutexes.mem verifier_atomic (Lockset.export_locks ctx.local) then
         false
       else *)
       non_overlapping held_locks protecting
-    | Queries.MayBePublicWithout _ when Lockset.is_bot ctx.local -> false
+    | Queries.MayBePublicWithout _ when Lockset.is_bot ls -> false
     | Queries.MayBePublicWithout {global=v; write; without_mutex; protection} ->
-      let held_locks = Lockset.export_locks (Lockset.remove (without_mutex, true) (Lockset.filter snd ctx.local)) in
+      let held_locks = Lockset.export_locks @@ fst @@ Arg.remove ctx ~warn:false without_mutex in
       let protecting = protecting ~write protection v in
       (* TODO: unsound in 29/24, why did we do this before? *)
       (* if Mutexes.mem verifier_atomic (Lockset.export_locks (Lockset.remove (without_mutex, true) ctx.local)) then
@@ -191,7 +233,7 @@ struct
       else *)
       Mutexes.leq mutex_lockset protecting
     | Queries.MustLockset ->
-      let held_locks = Lockset.export_locks (Lockset.filter snd ctx.local) in
+      let held_locks = Lockset.export_locks (Lockset.filter snd ls) in
       let ls = Mutexes.fold (fun addr ls ->
           match Addr.to_var_offset addr with
           | Some (var, offs) -> Queries.LS.add (var, conv_offset_inv offs) ls
@@ -200,7 +242,7 @@ struct
       in
       ls
     | Queries.MustBeAtomic ->
-      let held_locks = Lockset.export_locks (Lockset.filter snd ctx.local) in
+      let held_locks = Lockset.export_locks (Lockset.filter snd ls) in
       Mutexes.mem (LockDomain.Addr.from_var LF.verifier_atomic_var) held_locks
     | Queries.MustProtectedVars {mutex = m; write} ->
       let protected = GProtected.get ~write Strong (G.protected (ctx.global (V.protected m))) in
@@ -234,17 +276,17 @@ struct
   struct
     include D
     let name () = "lock"
-    let may_race ls1 ls2 =
+    let may_race (ls1,_) (ls2,_) =
       (* not mutually exclusive *)
-      not @@ D.exists (fun ((m1, w1) as l1) ->
+      not @@ Lockset.exists (fun ((m1, w1) as l1) ->
           if w1 then
             (* write lock is exclusive with write lock or read lock *)
-            D.mem l1 ls2 || D.mem (m1, false) ls2
+            Lockset.mem l1 ls2 || Lockset.mem (m1, false) ls2
           else
             (* read lock is exclusive with just write lock *)
-            D.mem (m1, true) ls2
+            Lockset.mem (m1, true) ls2
         ) ls1
-    let should_print ls = not (is_empty ls)
+    let should_print ls = not (Lockset.is_empty (fst ls))
   end
 
   let access ctx (a: Queries.access) =
@@ -260,8 +302,8 @@ struct
         (*privatization*)
         match var_opt with
         | Some v ->
-          if not (Lockset.is_bot octx.local) then
-            let locks = Lockset.export_locks (Lockset.filter snd octx.local) in
+          if not (Lockset.is_bot (fst octx.local)) then
+            let locks = Lockset.export_locks (Lockset.filter snd (fst octx.local)) in
             let write = match kind with
               | Write | Free -> true
               | Read -> false

src/analyses/mutexTypeAnalysis.ml

@@ -71,5 +71,8 @@ struct
     | _ -> Queries.Result.top q
 end
 
+let must_be_recursive ctx (v,o) =
+  ctx.ask (Queries.MutexType (v, Lval.OffsetNoIdx.of_offs o)) = `Lifted MutexAttrDomain.MutexKind.Recursive
+
 let _ =
   MCP.register_analysis (module Spec : MCPSpec)