Refactor mutex analyses

src/analyses/apron/apronAnalysis.apron.ml

@@ -408,16 +408,18 @@ struct
   let threadspawn ctx lval f args fctx =
     ctx.local
 
-  let event ctx e aprx =
+  let event ctx e octx =
     let st = ctx.local in
     match e with
-    | Events.Lock addr when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *)
-      Priv.lock (Analyses.ask_of_ctx aprx) aprx.global st addr
+    | Events.Lock (addr, _) when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *)
+      Priv.lock (Analyses.ask_of_ctx ctx) ctx.global st addr
     | Events.Unlock addr when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *)
-      Priv.unlock (Analyses.ask_of_ctx aprx) aprx.global aprx.sideg st addr
+      if addr = UnknownPtr then
+        M.info ~category:Unsound "Unknown mutex unlocked, apron privatization unsound"; (* TODO: something more sound *)
+      Priv.unlock (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st addr
     (* No need to handle escape because escaped variables are always referenced but this analysis only considers unreferenced variables. *)
     | Events.EnterMultiThreaded ->
-      Priv.enter_multithreaded (Analyses.ask_of_ctx aprx) aprx.global aprx.sideg st
+      Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st
     | _ ->
       st
 

src/analyses/apron/apronPriv.apron.ml

@@ -438,12 +438,17 @@ struct
     {st with apr = apr_local'}
 
   let lock ask getg (st: apron_components_t) m =
-    let apr = st.apr in
-    let get_m = get_m_with_mutex_inits ask getg m in
-    (* Additionally filter get_m in case it contains variables it no longer protects. E.g. in 36/22. *)
-    let get_m = keep_only_protected_globals ask m get_m in
-    let apr' = AD.meet apr get_m in
-    {st with apr = apr'}
+    (* TODO: somehow actually unneeded here? *)
+    if Locksets.(not (Lockset.mem m (current_lockset ask))) then (
+      let apr = st.apr in
+      let get_m = get_m_with_mutex_inits ask getg m in
+      (* Additionally filter get_m in case it contains variables it no longer protects. E.g. in 36/22. *)
+      let get_m = keep_only_protected_globals ask m get_m in
+      let apr' = AD.meet apr get_m in
+      {st with apr = apr'}
+    )
+    else
+      st (* sound w.r.t. recursive lock *)
 
   let unlock ask getg sideg (st: apron_components_t) m: apron_components_t =
     let apr = st.apr in
@@ -942,15 +947,19 @@ struct
     {apr = apr_local'; priv = (W.add g w,LMust.add lm lmust,l')}
 
   let lock ask getg (st: apron_components_t) m =
-    let apr = st.apr in
-    let _,lmust,l = st.priv in
-    let lm = LLock.mutex m in
-    let get_m = get_m_with_mutex_inits (not (LMust.mem lm lmust)) ask getg m in
-    let local_m = BatOption.default (LAD.bot ()) (L.find_opt lm l) in
-    (* Additionally filter get_m in case it contains variables it no longer protects. E.g. in 36/22. *)
-    let local_m = Cluster.keep_only_protected_globals ask m local_m in
-    let apr = Cluster.lock apr local_m get_m in
-    {st with apr}
+    if Locksets.(not (Lockset.mem m (current_lockset ask))) then (
+      let apr = st.apr in
+      let _,lmust,l = st.priv in
+      let lm = LLock.mutex m in
+      let get_m = get_m_with_mutex_inits (not (LMust.mem lm lmust)) ask getg m in
+      let local_m = BatOption.default (LAD.bot ()) (L.find_opt lm l) in
+      (* Additionally filter get_m in case it contains variables it no longer protects. E.g. in 36/22. *)
+      let local_m = Cluster.keep_only_protected_globals ask m local_m in
+      let apr = Cluster.lock apr local_m get_m in
+      {st with apr}
+    )
+    else
+      st (* sound w.r.t. recursive lock *)
 
   let unlock ask getg sideg (st: apron_components_t) m: apron_components_t =
     let apr = st.apr in

src/analyses/base.ml

@@ -2367,15 +2367,17 @@ struct
   let event ctx e octx =
     let st: store = ctx.local in
     match e with
-    | Events.Lock addr when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *)
+    | Events.Lock (addr, _) when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *)
       if M.tracing then M.tracel "priv" "LOCK EVENT %a\n" LockDomain.Addr.pretty addr;
-      Priv.lock (Analyses.ask_of_ctx octx) (priv_getg octx.global) st addr
+      Priv.lock (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) st addr
     | Events.Unlock addr when ThreadFlag.is_multi (Analyses.ask_of_ctx ctx) -> (* TODO: is this condition sound? *)
-      Priv.unlock (Analyses.ask_of_ctx octx) (priv_getg octx.global) (priv_sideg octx.sideg) st addr
+      if addr = UnknownPtr then
+        M.info ~category:Unsound "Unknown mutex unlocked, base privatization unsound"; (* TODO: something more sound *)
+      Priv.unlock (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) st addr
     | Events.Escape escaped ->
-      Priv.escape (Analyses.ask_of_ctx octx) (priv_getg octx.global) (priv_sideg octx.sideg) st escaped
+      Priv.escape (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) st escaped
     | Events.EnterMultiThreaded ->
-      Priv.enter_multithreaded (Analyses.ask_of_ctx octx) (priv_getg octx.global) (priv_sideg octx.sideg) st
+      Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) st
     | Events.AssignSpawnedThread (lval, tid) ->
       (* TODO: is this type right? *)
       set ~ctx:(Some ctx) (Analyses.ask_of_ctx ctx) ctx.global ctx.local (eval_lv (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval) (Cilfacade.typeOfLval lval) (`Thread (ValueDomain.Threads.singleton tid))

src/analyses/basePriv.ml

@@ -276,18 +276,23 @@ struct
     cpa' *)
 
   let lock ask getg (st: BaseComponents (D).t) m =
-    let get_m = get_m_with_mutex_inits ask getg m in
-    (* Really we want is_unprotected, but pthread_cond_wait emits unlock-lock events,
-       where our (necessary) original context still has the mutex,
-       so the query would be on the wrong lockset.
-       TODO: Fixing the event contexts is hard: https://github.com/goblint/analyzer/pull/487#discussion_r765905029.
-       Therefore, just use _without to exclude the mutex we shouldn't have.
-       In non-cond locks we don't have it anyway, so there's no difference.
-       No other privatization uses is_unprotected, so this hack is only needed here. *)
-    let is_in_V x _ = is_protected_by ask m x && is_unprotected_without ask x m in
-    let cpa' = CPA.filter is_in_V get_m in
-    if M.tracing then M.tracel "priv" "PerMutexOplusPriv.lock m=%a cpa'=%a\n" LockDomain.Addr.pretty m CPA.pretty cpa';
-    {st with cpa = CPA.fold CPA.add cpa' st.cpa}
+    if Locksets.(not (Lockset.mem m (current_lockset ask))) then (
+      let get_m = get_m_with_mutex_inits ask getg m in
+      (* Really we want is_unprotected, but pthread_cond_wait emits unlock-lock events,
+        where our (necessary) original context still has the mutex,
+        so the query would be on the wrong lockset.
+        TODO: Fixing the event contexts is hard: https://github.com/goblint/analyzer/pull/487#discussion_r765905029.
+        Therefore, just use _without to exclude the mutex we shouldn't have.
+        In non-cond locks we don't have it anyway, so there's no difference.
+        No other privatization uses is_unprotected, so this hack is only needed here. *)
+      let is_in_V x _ = is_protected_by ask m x && is_unprotected_without ask x m in
+      let cpa' = CPA.filter is_in_V get_m in
+      if M.tracing then M.tracel "priv" "PerMutexOplusPriv.lock m=%a cpa'=%a\n" LockDomain.Addr.pretty m CPA.pretty cpa';
+      {st with cpa = CPA.fold CPA.add cpa' st.cpa}
+    )
+    else
+      st (* sound w.r.t. recursive lock *)
+
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
     let is_in_Gm x _ = is_protected_by ask m x in
     let side_m_cpa = CPA.filter is_in_Gm st.cpa in
@@ -351,15 +356,20 @@ struct
     ignore (Pretty.printf "WRITE GLOBAL %a %a = %a\n" d_varinfo x VD.pretty v CPA.pretty cpa');
     cpa' *)
 
-  let lock ask getg (st: BaseComponents (D).t) m =
-    let get_m = get_m_with_mutex_inits ask getg m in
-    (* Additionally filter get_m in case it contains variables it no longer protects. *)
-    let is_in_Gm x _ = is_protected_by ask m x in
-    let get_m = CPA.filter is_in_Gm get_m in
-    let long_meet m1 m2 = CPA.long_map2 VD.meet m1 m2 in
-    let meet = long_meet st.cpa get_m in
-    if M.tracing then M.tracel "priv" "LOCK %a:\n  get_m: %a\n  meet: %a\n" LockDomain.Addr.pretty m CPA.pretty get_m CPA.pretty meet;
-    {st with cpa = meet}
+  let lock (ask: Queries.ask) getg (st: BaseComponents (D).t) m =
+    if Locksets.(not (Lockset.mem m (current_lockset ask))) then (
+      let get_m = get_m_with_mutex_inits ask getg m in
+      (* Additionally filter get_m in case it contains variables it no longer protects. *)
+      let is_in_Gm x _ = is_protected_by ask m x in
+      let get_m = CPA.filter is_in_Gm get_m in
+      let long_meet m1 m2 = CPA.long_map2 VD.meet m1 m2 in
+      let meet = long_meet st.cpa get_m in
+      if M.tracing then M.tracel "priv" "LOCK %a:\n  get_m: %a\n  meet: %a\n" LockDomain.Addr.pretty m CPA.pretty get_m CPA.pretty meet;
+      {st with cpa = meet}
+    )
+    else
+      st (* sound w.r.t. recursive lock *)
+
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
     let is_in_Gm x _ = is_protected_by ask m x in
     sideg (V.mutex m) (CPA.filter is_in_Gm st.cpa);

src/analyses/commonPriv.ml

@@ -127,7 +127,7 @@ struct
     if !GU.global_initialization then
       Lockset.empty ()
     else
-      let ls = ask.f Queries.CurrentLockset in
+      let ls = ask.f Queries.MustLockset in
       Q.LS.fold (fun (var, offs) acc ->
           Lockset.add (Lock.from_var_offset (var, conv_offset offs)) acc
         ) ls (Lockset.empty ())

src/analyses/deadlock.ml

@@ -4,55 +4,52 @@ open Prelude.Ana
 open Analyses
 open DeadlockDomain
 
+
 module Spec =
 struct
-  include Analyses.IdentitySpec
-
-  let name () = "deadlock"
-
-  module D = MayLockEvents
-  module C = D
-  module V = Lock
 
   module LockEventPair = Printable.Prod (LockEvent) (LockEvent)
   module MayLockEventPairs = SetDomain.Make (LockEventPair)
-  module G =
-  struct
-    include MapDomain.MapBot (Lock) (MayLockEventPairs)
-    let leq x y = !GU.postsolving || leq x y (* HACK: to pass verify*)
-  end
 
-  let side_lock_event_pair ctx before after =
-    let d =
-      if !GU.should_warn then
-        G.singleton (Tuple3.first after) (MayLockEventPairs.singleton (before, after))
-      else
-        G.bot () (* HACK: just to pass validation with MCP DomVariantLattice *)
-    in
-    ctx.sideg (Tuple3.first before) d
+  module Arg =
+  struct
+    module D = MayLockEvents
+    module V = Lock
 
+    module G =
+    struct
+      include MapDomain.MapBot (Lock) (MayLockEventPairs)
+      let leq x y = !GU.postsolving || leq x y (* HACK: to pass verify*)
+    end
 
-  (* Some required states *)
-  let startstate _ : D.t = D.empty ()
-  let threadenter ctx lval f args = [D.empty ()]
-  let exitstate  _ : D.t = D.empty ()
+    let side_lock_event_pair ctx before after =
+      let d =
+        if !GU.should_warn then
+          G.singleton (Tuple3.first after) (MayLockEventPairs.singleton (before, after))
+        else
+          G.bot () (* HACK: just to pass validation with MCP DomVariantLattice *)
+      in
+      ctx.sideg (Tuple3.first before) d
 
-  let part_access ctx: MCPAccess.A.t =
-    Obj.obj (ctx.ask (PartAccess Point))
+    let part_access ctx: MCPAccess.A.t =
+      Obj.obj (ctx.ask (PartAccess Point))
 
-  let event ctx (e: Events.t) octx =
-    match e with
-    | Lock addr ->
-      let after = (addr, ctx.prev_node, part_access octx) in (* use octx for access to use locksets before event *)
+    let add ctx ((l, _): LockDomain.Lockset.Lock.t) =
+      let after: LockEvent.t = (l, ctx.prev_node, part_access ctx) in (* use octx for access to use locksets before event *)
       D.iter (fun before ->
           side_lock_event_pair ctx before after
         ) ctx.local;
       D.add after ctx.local
-    | Unlock addr ->
-      let inLockAddrs (e, _, _) = Lock.equal addr e in
+
+    let remove ctx l =
+      let inLockAddrs (e, _, _) = Lock.equal l e in
       D.filter (neg inLockAddrs) ctx.local
-    | _ ->
-      ctx.local
+  end
+
+  include LocksetAnalysis.MakeMay (Arg)
+  let name () = "deadlock"
+
+  module G = Arg.G (* help type checker using explicit constraint *)
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
     match q with
@@ -64,15 +61,22 @@ struct
       (* TODO: find all cycles/SCCs *)
       let global_visited_locks = LH.create 100 in
 
+      let may_equal l1 l2 = match l1, l2 with
+        | ValueDomain.Addr.UnknownPtr, _
+        | _, ValueDomain.Addr.UnknownPtr ->
+          true
+        | _, _ -> Lock.equal l1 l2
+      in
+
       (* DFS *)
       let rec iter_lock (path_visited_locks: LS.t) (path_visited_lock_event_pairs: LockEventPair.t list) (lock: Lock.t) =
-        if LS.mem lock path_visited_locks then (
+        if LS.mem lock path_visited_locks || LS.mem ValueDomain.Addr.UnknownPtr path_visited_locks || (not (LS.is_empty path_visited_locks) && lock = ValueDomain.Addr.UnknownPtr) then (
           (* cycle may not return to first lock, but an intermediate one, cut off the non-cyclic stem *)
           let path_visited_lock_event_pairs =
             (* path_visited_lock_event_pairs cannot be empty *)
             List.hd path_visited_lock_event_pairs ::
             List.take_while (fun (_, (after_lock, _, _)) ->
-                not (Lock.equal after_lock lock)
+                not (may_equal after_lock lock)
               ) (List.tl path_visited_lock_event_pairs)
           in
           let mhp =
@@ -114,4 +118,4 @@ struct
 end
 
 let _ =
-  MCP.register_analysis ~dep:["mutex"] (module Spec : MCPSpec)
+  MCP.register_analysis ~dep:["mutexEvents"] (module Spec : MCPSpec)

src/analyses/locksetAnalysis.ml

@@ -0,0 +1,88 @@
+(** Basic lockset analyses. *)
+
+open Prelude.Ana
+open Analyses
+
+
+module type DS =
+sig
+  include Lattice.S
+  val empty: unit -> t
+end
+
+module Make (D: DS) =
+struct
+  include Analyses.IdentitySpec
+  let name () = "lockset"
+
+  module D = D
+  module C = D
+
+  let startstate v = D.empty ()
+  let threadenter ctx lval f args = [D.empty ()]
+  let exitstate  v = D.empty ()
+end
+
+
+module type MayArg =
+sig
+  module D: DS
+  module G: Lattice.S
+  module V: Printable.S
+
+  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
+end
+
+module MakeMay (Arg: MayArg) =
+struct
+  include Make (Arg.D)
+  let name () = "mayLockset"
+
+  module G = Arg.G
+  module V = Arg.V
+
+  let event ctx e octx =
+    match e with
+    | Events.Lock l ->
+      Arg.add ctx l (* add all locks, including blob and unknown *)
+    | Events.Unlock UnknownPtr ->
+      ctx.local (* don't remove any locks, including unknown itself *)
+    | Events.Unlock Addr (v, _) when ctx.ask (IsMultiple v) ->
+      ctx.local (* don't remove non-unique lock *)
+    | Events.Unlock l ->
+      Arg.remove ctx l (* remove definite lock or none in parallel if ambiguous *)
+    | _ ->
+      ctx.local
+end
+
+
+module type MustArg =
+sig
+  include MayArg
+  val remove_all: (D.t, _, D.t, _) ctx -> D.t
+end
+
+module MakeMust (Arg: MustArg) =
+struct
+  include Make (Arg.D)
+  let name () = "mustLockset"
+
+  module G = Arg.G
+  module V = Arg.V
+
+  let event ctx e octx =
+    match e with
+    | Events.Lock (UnknownPtr, _) ->
+      ctx.local (* don't add unknown lock *)
+    | Events.Lock (Addr (v, _), _) when ctx.ask (IsMultiple v) ->
+      ctx.local (* don't add non-unique lock *)
+    | Events.Lock l ->
+      Arg.add ctx l (* add definite lock or none in parallel if ambiguous *)
+    | Events.Unlock UnknownPtr ->
+      Arg.remove_all ctx (* remove all locks *)
+    | Events.Unlock l ->
+      Arg.remove ctx l (* remove definite lock or all in parallel if ambiguous (blob lock is never added) *)
+    | _ ->
+      ctx.local
+end