From d5d9e5f22809a53065d180e6199fb6b3618828d4 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 21 Mar 2022 13:07:24 +0200
Subject: [PATCH 01/31] Use global constraint unknown for deadlock orders
 (issue #650)

---
 src/analyses/deadlock.ml | 36 +++++++++++++++++++++++-------------
 1 file changed, 23 insertions(+), 13 deletions(-)

diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml
index 8ee2433aed..9e7fd729c6 100644
--- a/src/analyses/deadlock.ml
+++ b/src/analyses/deadlock.ml
@@ -4,8 +4,6 @@ open Prelude.Ana
 open Analyses
 open DeadlockDomain
 
-let forbiddenList : ( (myowntypeEntry*myowntypeEntry) list ref) = ref []
-
 module Spec =
 struct
   include Analyses.DefaultSpec
@@ -15,28 +13,40 @@ struct
   (* The domain for the analysis *)
   module D = DeadlockDomain.Lockset (* MayLockset *)
   module C = DeadlockDomain.Lockset
+  module V = Printable.UnitConf (struct let name = "deadlock" end)
+  module G =
+  struct
+    include SetDomain.Make (Printable.Prod (MyLock) (MyLock))
+    let leq x y = !GU.postsolving || leq x y (* HACK: to pass verify*)
+  end
+
+  let addLockingInfo ctx newLock lockList =
 
-  let addLockingInfo newLock lockList =
     let add_comb a b =
-      if List.exists (fun (x,y) -> MyLock.equal x a && MyLock.equal y b) !forbiddenList then ()
-      else forbiddenList := (a,b)::!forbiddenList
+      let d =
+        if !GU.should_warn then
+          G.singleton (a, b)
+        else
+          G.bot () (* HACK: just to pass validation with MCP DomVariantLattice *)
+      in
+      ctx.sideg () d
     in
 
     (* Check forbidden list *)
-    if !Goblintutil.postsolving then begin
-      D.iter (fun e -> List.iter (fun (a,b) ->
+    if true || !Goblintutil.postsolving then begin (* TODO: only postsolving *)
+      D.iter (fun e -> G.iter (fun (a,b) ->
           if ((MyLock.equal a e) && (MyLock.equal b newLock)) then (
             Messages.warn "Deadlock warning: Locking order %a, %a at %a, %a violates order at %a, %a." ValueDomain.Addr.pretty e.addr ValueDomain.Addr.pretty newLock.addr CilType.Location.pretty e.loc CilType.Location.pretty newLock.loc CilType.Location.pretty b.loc CilType.Location.pretty a.loc;
             Messages.warn ~loc:a.loc "Deadlock warning: Locking order %a, %a at %a, %a violates order at %a, %a." ValueDomain.Addr.pretty newLock.addr ValueDomain.Addr.pretty e.addr CilType.Location.pretty b.loc CilType.Location.pretty a.loc CilType.Location.pretty e.loc CilType.Location.pretty newLock.loc;
           )
-          else () ) !forbiddenList ) lockList;
+          else () ) (ctx.global ()) ) lockList;
 
       (* Add forbidden order *)
       D.iter (
         fun lock ->
           add_comb newLock lock;
-          let transAddList = List.find_all (fun (a,b) -> MyLock.equal a lock) !forbiddenList in
-          List.iter (fun (a,b) -> add_comb newLock b) transAddList
+          let transAddList = G.filter (fun (a,b) -> MyLock.equal a lock) (ctx.global ()) in
+          G.iter (fun (a,b) -> add_comb newLock b) transAddList
       ) lockList
     end
 
@@ -96,9 +106,9 @@ struct
       match LibraryFunctions.classify f.vname arglist with
       | `Lock (_, _, _) ->
         List.fold_left (fun d lockAddr ->
-          addLockingInfo {addr = lockAddr; loc = !Tracing.current_loc } ctx.local;
-          D.add {addr = lockAddr; loc = !Tracing.current_loc } ctx.local
-        ) ctx.local (eval_exp_addr (Analyses.ask_of_ctx ctx) (List.hd arglist))
+            addLockingInfo ctx {addr = lockAddr; loc = !Tracing.current_loc } ctx.local;
+            D.add {addr = lockAddr; loc = !Tracing.current_loc } ctx.local
+          ) ctx.local (eval_exp_addr (Analyses.ask_of_ctx ctx) (List.hd arglist))
       | `Unlock ->
         let lockAddrs = eval_exp_addr (Analyses.ask_of_ctx ctx) (List.hd arglist) in
         if List.compare_length_with lockAddrs 1 = 0 then

From c1d79cca8fa11be3476ea83770c232501690b6db Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 21 Mar 2022 14:02:34 +0200
Subject: [PATCH 02/31] Use WarnGlobal for deadlock warnings (issue #650)

---
 src/analyses/deadlock.ml | 59 +++++++++++++++++++++++++++++-----------
 1 file changed, 43 insertions(+), 16 deletions(-)

diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml
index 9e7fd729c6..13ea49dce7 100644
--- a/src/analyses/deadlock.ml
+++ b/src/analyses/deadlock.ml
@@ -32,23 +32,11 @@ struct
       ctx.sideg () d
     in
 
-    (* Check forbidden list *)
-    if true || !Goblintutil.postsolving then begin (* TODO: only postsolving *)
-      D.iter (fun e -> G.iter (fun (a,b) ->
-          if ((MyLock.equal a e) && (MyLock.equal b newLock)) then (
-            Messages.warn "Deadlock warning: Locking order %a, %a at %a, %a violates order at %a, %a." ValueDomain.Addr.pretty e.addr ValueDomain.Addr.pretty newLock.addr CilType.Location.pretty e.loc CilType.Location.pretty newLock.loc CilType.Location.pretty b.loc CilType.Location.pretty a.loc;
-            Messages.warn ~loc:a.loc "Deadlock warning: Locking order %a, %a at %a, %a violates order at %a, %a." ValueDomain.Addr.pretty newLock.addr ValueDomain.Addr.pretty e.addr CilType.Location.pretty b.loc CilType.Location.pretty a.loc CilType.Location.pretty e.loc CilType.Location.pretty newLock.loc;
-          )
-          else () ) (ctx.global ()) ) lockList;
-
-      (* Add forbidden order *)
-      D.iter (
-        fun lock ->
-          add_comb newLock lock;
-          let transAddList = G.filter (fun (a,b) -> MyLock.equal a lock) (ctx.global ()) in
-          G.iter (fun (a,b) -> add_comb newLock b) transAddList
+    (* Add forbidden order *)
+    D.iter (
+      fun lock ->
+        add_comb newLock lock;
       ) lockList
-    end
 
 
   (* Some required states *)
@@ -117,6 +105,45 @@ struct
         else ctx.local
       | _ -> ctx.local
 
+  let query ctx (type a) (q: a Queries.t): a Queries.result =
+    match q with
+    | WarnGlobal _ -> (* just repr of () *)
+      let order_set = ctx.global () in
+      ignore (Pretty.printf "deadlock: %a\n" G.pretty order_set);
+      let module LH = Hashtbl.Make (MyLock) in
+      let order = LH.create 12 in
+      G.iter (fun (a, b) ->
+          LH.modify_def (D.empty ()) a (D.add b) order
+        ) order_set;
+
+      (* TODO: find all cycles/SCCs *)
+      let global_visited_nodes = LH.create 100 in
+
+      (* DFS *)
+      let rec iter_node path_visited_nodes path_visited_nodes' node =
+        if D.mem node path_visited_nodes then (
+          let pieces =
+            List.map (fun lock ->
+                let doc = MyLock.pretty () lock in
+                (doc, Some lock.loc)
+              ) path_visited_nodes'
+          in
+          M.msg_group Warning "Deadlock order" pieces
+        )
+        else if not (LH.mem global_visited_nodes node) then begin
+          LH.replace global_visited_nodes node ();
+          let new_path_visited_nodes = D.add node path_visited_nodes in
+          let new_path_visited_nodes' = node :: path_visited_nodes' in
+          D.iter (fun to_node ->
+              iter_node new_path_visited_nodes new_path_visited_nodes' to_node
+            ) (LH.find_default order node (D.empty ()))
+        end
+      in
+
+      LH.iter (fun a _ ->
+          iter_node (D.empty ()) [] a
+        ) order
+    | _ -> Queries.Result.top q
 end
 
 let _ =

From 9164bce68e964ce96064d98747971bf2fd61fb1f Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 21 Mar 2022 14:39:11 +0200
Subject: [PATCH 03/31] Add all before and after locks to deadlock warning
 (issue #650)

---
 scripts/update_suite.rb        |  1 +
 src/analyses/deadlock.ml       | 31 +++++++++++++++++++------------
 src/cdomains/deadlockDomain.ml | 19 ++++++++++++-------
 3 files changed, 32 insertions(+), 19 deletions(-)

diff --git a/scripts/update_suite.rb b/scripts/update_suite.rb
index c5717cc5e7..5c19c38a11 100755
--- a/scripts/update_suite.rb
+++ b/scripts/update_suite.rb
@@ -153,6 +153,7 @@ def collect_warnings
                     when /\(conf\. \d+\)/            then "race"
                     when /lockset:/                  then "race" # osek races have their own legacy-like output
                     when /Deadlock/                  then "deadlock"
+                    when /lock (before|after):/           then "deadlock"
                     when /Assertion .* will fail/    then "fail"
                     when /Assertion .* will succeed/ then "success"
                     when /Assertion .* is unknown/   then "unknown"
diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml
index 13ea49dce7..b5d4337954 100644
--- a/src/analyses/deadlock.ml
+++ b/src/analyses/deadlock.ml
@@ -16,7 +16,7 @@ struct
   module V = Printable.UnitConf (struct let name = "deadlock" end)
   module G =
   struct
-    include SetDomain.Make (Printable.Prod (MyLock) (MyLock))
+    include SetDomain.Make (Printable.Prod (MyLock0) (MyLock0))
     let leq x y = !GU.postsolving || leq x y (* HACK: to pass verify*)
   end
 
@@ -109,23 +109,28 @@ struct
     match q with
     | WarnGlobal _ -> (* just repr of () *)
       let order_set = ctx.global () in
-      ignore (Pretty.printf "deadlock: %a\n" G.pretty order_set);
       let module LH = Hashtbl.Make (MyLock) in
-      let order = LH.create 12 in
+      let order: G.t LH.t LH.t = LH.create 12 in
       G.iter (fun (a, b) ->
-          LH.modify_def (D.empty ()) a (D.add b) order
+          LH.modify_def (LH.create 1) a (fun h ->
+              LH.modify_def (G.empty ()) b (G.add (a, b)) h;
+              h
+            ) order
         ) order_set;
 
       (* TODO: find all cycles/SCCs *)
       let global_visited_nodes = LH.create 100 in
 
       (* DFS *)
-      let rec iter_node path_visited_nodes path_visited_nodes' node =
+      let rec iter_node path_visited_nodes (path_visited_nodes': G.elt list) node =
         if D.mem node path_visited_nodes then (
           let pieces =
-            List.map (fun lock ->
-                let doc = MyLock.pretty () lock in
-                (doc, Some lock.loc)
+            List.concat_map (fun (a, b) ->
+                [
+                  (* backwards to get correct printout order *)
+                  (Pretty.dprintf "lock before: %a" MyLock.pretty b, Some b.loc);
+                  (Pretty.dprintf "lock after: %a" MyLock.pretty a, Some a.loc);
+                ]
               ) path_visited_nodes'
           in
           M.msg_group Warning "Deadlock order" pieces
@@ -133,10 +138,12 @@ struct
         else if not (LH.mem global_visited_nodes node) then begin
           LH.replace global_visited_nodes node ();
           let new_path_visited_nodes = D.add node path_visited_nodes in
-          let new_path_visited_nodes' = node :: path_visited_nodes' in
-          D.iter (fun to_node ->
-              iter_node new_path_visited_nodes new_path_visited_nodes' to_node
-            ) (LH.find_default order node (D.empty ()))
+          LH.iter (fun to_node gs ->
+              G.iter (fun g ->
+                  let new_path_visited_nodes' = g :: path_visited_nodes' in
+                  iter_node new_path_visited_nodes new_path_visited_nodes' to_node
+                ) gs
+            ) (LH.find_default order node (LH.create 0))
         end
       in
 
diff --git a/src/cdomains/deadlockDomain.ml b/src/cdomains/deadlockDomain.ml
index 607b3ab8f3..31c91ce8d4 100644
--- a/src/cdomains/deadlockDomain.ml
+++ b/src/cdomains/deadlockDomain.ml
@@ -1,24 +1,29 @@
 open Cil
 open Pretty
 
-type myowntypeEntry = {addr : ValueDomain.Addr.t ; loc : location}
+type myowntypeEntry = {addr : ValueDomain.Addr.t ; loc : CilType.Location.t} [@@deriving eq, ord, hash]
 
 
-module MyLock : Printable.S with type t = myowntypeEntry =
+module MyLock0 : Printable.S with type t = myowntypeEntry =
 struct
   include Printable.Std (* for default invariant, tag, ... *)
 
-  type t = myowntypeEntry
+  type t = myowntypeEntry [@@deriving eq, ord, hash]
   module Ad = ValueDomain.Addr
   let name () = "address with location"
-  let equal x y = Ad.equal x.addr y.addr (* ignores loc field *)
-  let hash x = Ad.hash x.addr
-  let compare x y = Ad.compare x.addr y.addr (* ignores loc field *)
-  (* TODO: deadlock analysis output doesn't even use these, but manually outputs locations *)
   let show x = (Ad.show x.addr) ^ "@" ^ (CilType.Location.show x.loc)
   let pretty () x = Ad.pretty () x.addr ++ text "@" ++ CilType.Location.pretty () x.loc
   let printXml c x = Ad.printXml c x.addr
   let to_yojson x = `String (show x)
 end
 
+module MyLock : Printable.S with type t = myowntypeEntry =
+struct
+  include MyLock0
+  module Ad = ValueDomain.Addr
+  let equal x y = Ad.equal x.addr y.addr (* ignores loc field *)
+  let hash x = Ad.hash x.addr
+  let compare x y = Ad.compare x.addr y.addr (* ignores loc field *)
+end
+
 module Lockset = SetDomain.ToppedSet (MyLock) (struct let topname = "all locks" end)

From 1e873f4356401b4119a7ecc42fd0c5b9b46d0c6e Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 21 Mar 2022 14:40:03 +0200
Subject: [PATCH 04/31] Enable and extend all deadlock tests

---
 tests/regression/15-deadlock/01-basic_deadlock.c     | 4 ++--
 tests/regression/15-deadlock/02-basic_nodeadlock.c   | 4 ++--
 tests/regression/15-deadlock/03-triple_deadlock.c    | 8 ++++----
 tests/regression/15-deadlock/04-triple_nodeadlock.c  | 6 +++---
 tests/regression/15-deadlock/05-may_deadlock.c       | 4 ++--
 tests/regression/15-deadlock/06-may_nodeadlock.c     | 4 ++--
 tests/regression/15-deadlock/07-account_deadlock.c   | 2 +-
 tests/regression/15-deadlock/08-account_nodeadlock.c | 2 +-
 tests/regression/15-deadlock/09-account_correct.c    | 4 ++--
 tests/regression/15-deadlock/10-account_incorrect.c  | 4 ++--
 10 files changed, 21 insertions(+), 21 deletions(-)

diff --git a/tests/regression/15-deadlock/01-basic_deadlock.c b/tests/regression/15-deadlock/01-basic_deadlock.c
index a0cce14b45..84bd44b00a 100644
--- a/tests/regression/15-deadlock/01-basic_deadlock.c
+++ b/tests/regression/15-deadlock/01-basic_deadlock.c
@@ -7,7 +7,7 @@ pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
 pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
 
 void *t1(void *arg) {
-  pthread_mutex_lock(&mutex1);
+  pthread_mutex_lock(&mutex1); // DEADLOCK
   pthread_mutex_lock(&mutex2); // DEADLOCK
   g1 = g2 + 1;
   pthread_mutex_unlock(&mutex2);
@@ -16,7 +16,7 @@ void *t1(void *arg) {
 }
 
 void *t2(void *arg) {
-  pthread_mutex_lock(&mutex2);
+  pthread_mutex_lock(&mutex2); // DEADLOCK
   pthread_mutex_lock(&mutex1); // DEADLOCK
   g2 = g1 + 1;
   pthread_mutex_unlock(&mutex1);
diff --git a/tests/regression/15-deadlock/02-basic_nodeadlock.c b/tests/regression/15-deadlock/02-basic_nodeadlock.c
index 66de92c652..97d9992b42 100644
--- a/tests/regression/15-deadlock/02-basic_nodeadlock.c
+++ b/tests/regression/15-deadlock/02-basic_nodeadlock.c
@@ -7,7 +7,7 @@ pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
 pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
 
 void *t1(void *arg) {
-  pthread_mutex_lock(&mutex1);
+  pthread_mutex_lock(&mutex1); // NODEADLOCK
   pthread_mutex_lock(&mutex2); // NODEADLOCK
   g1 = g2 + 1;
   pthread_mutex_unlock(&mutex2);
@@ -16,7 +16,7 @@ void *t1(void *arg) {
 }
 
 void *t2(void *arg) {
-  pthread_mutex_lock(&mutex1);
+  pthread_mutex_lock(&mutex1); // NODEADLOCK
   pthread_mutex_lock(&mutex2); // NODEADLOCK
   g2 = g1 + 1;
   pthread_mutex_unlock(&mutex2);
diff --git a/tests/regression/15-deadlock/03-triple_deadlock.c b/tests/regression/15-deadlock/03-triple_deadlock.c
index abff21b16d..7ba5cdabd5 100644
--- a/tests/regression/15-deadlock/03-triple_deadlock.c
+++ b/tests/regression/15-deadlock/03-triple_deadlock.c
@@ -1,4 +1,4 @@
-// SKIP PARAM: --set ana.activated[+] deadlock
+// PARAM: --set ana.activated[+] deadlock
 #include <pthread.h>
 #include <stdio.h>
 
@@ -8,7 +8,7 @@ pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
 pthread_mutex_t mutex3 = PTHREAD_MUTEX_INITIALIZER;
 
 void *t1(void *arg) {
-  pthread_mutex_lock(&mutex1);
+  pthread_mutex_lock(&mutex1); // DEADLOCK
   pthread_mutex_lock(&mutex2); // DEADLOCK
   g1 = g2 + 1;
   pthread_mutex_unlock(&mutex2);
@@ -17,7 +17,7 @@ void *t1(void *arg) {
 }
 
 void *t2(void *arg) {
-  pthread_mutex_lock(&mutex2);
+  pthread_mutex_lock(&mutex2); // DEADLOCK
   pthread_mutex_lock(&mutex3); // DEADLOCK
   g2 = g3 - 1;
   pthread_mutex_unlock(&mutex3);
@@ -26,7 +26,7 @@ void *t2(void *arg) {
 }
 
 void *t3(void *arg) {
-  pthread_mutex_lock(&mutex3);
+  pthread_mutex_lock(&mutex3); // DEADLOCK
   pthread_mutex_lock(&mutex1); // DEADLOCK
   g3 = g1 + 1;
   pthread_mutex_unlock(&mutex1);
diff --git a/tests/regression/15-deadlock/04-triple_nodeadlock.c b/tests/regression/15-deadlock/04-triple_nodeadlock.c
index 8849c642e4..89883f4995 100644
--- a/tests/regression/15-deadlock/04-triple_nodeadlock.c
+++ b/tests/regression/15-deadlock/04-triple_nodeadlock.c
@@ -8,7 +8,7 @@ pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
 pthread_mutex_t mutex3 = PTHREAD_MUTEX_INITIALIZER;
 
 void *t1(void *arg) {
-  pthread_mutex_lock(&mutex1);
+  pthread_mutex_lock(&mutex1);  // NODEADLOCK
   pthread_mutex_lock(&mutex2);  // NODEADLOCK
   g1 = g2 + 1;
   pthread_mutex_unlock(&mutex2);
@@ -17,7 +17,7 @@ void *t1(void *arg) {
 }
 
 void *t2(void *arg) {
-  pthread_mutex_lock(&mutex2);
+  pthread_mutex_lock(&mutex2); // NODEADLOCK
   pthread_mutex_lock(&mutex3); // NODEADLOCK
   g2 = g3 - 1;
   pthread_mutex_unlock(&mutex3);
@@ -26,7 +26,7 @@ void *t2(void *arg) {
 }
 
 void *t3(void *arg) {
-  pthread_mutex_lock(&mutex1);
+  pthread_mutex_lock(&mutex1); // NODEADLOCK
   pthread_mutex_lock(&mutex3); // NODEADLOCK
   g3 = g1 + 1;
   pthread_mutex_unlock(&mutex3);
diff --git a/tests/regression/15-deadlock/05-may_deadlock.c b/tests/regression/15-deadlock/05-may_deadlock.c
index 99f95093b0..04673eba27 100644
--- a/tests/regression/15-deadlock/05-may_deadlock.c
+++ b/tests/regression/15-deadlock/05-may_deadlock.c
@@ -7,7 +7,7 @@ pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
 pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
 
 void *t1(void *arg) {
-  pthread_mutex_lock(&mutex1);
+  pthread_mutex_lock(&mutex1); // DEADLOCK
   pthread_mutex_lock(&mutex2); // DEADLOCK
   g1 = g2 + 1;
   pthread_mutex_unlock(&mutex2);
@@ -18,7 +18,7 @@ void *t1(void *arg) {
 void *t2(void *arg) {
   int k = rand() % 2;
   if (k)
-    pthread_mutex_lock(&mutex2);
+    pthread_mutex_lock(&mutex2); // DEADLOCK
   pthread_mutex_lock(&mutex1); // DEADLOCK
   g2 = g1 + 1;
   pthread_mutex_unlock(&mutex1);
diff --git a/tests/regression/15-deadlock/06-may_nodeadlock.c b/tests/regression/15-deadlock/06-may_nodeadlock.c
index cc79c795a3..8656de4c85 100644
--- a/tests/regression/15-deadlock/06-may_nodeadlock.c
+++ b/tests/regression/15-deadlock/06-may_nodeadlock.c
@@ -7,7 +7,7 @@ pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
 pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
 
 void *t1(void *arg) {
-  pthread_mutex_lock(&mutex1);
+  pthread_mutex_lock(&mutex1); // NODEADLOCK
   pthread_mutex_lock(&mutex2); // NODEADLOCK
   g1 = g2 + 1;
   pthread_mutex_unlock(&mutex2);
@@ -18,7 +18,7 @@ void *t1(void *arg) {
 void *t2(void *arg) {
   int k = rand() % 2;
   if (k)
-    pthread_mutex_lock(&mutex2);
+    pthread_mutex_lock(&mutex2); // NODEADLOCK
   else
     pthread_mutex_lock(&mutex1); // NODEADLOCK
   g2 = g1 + 1;
diff --git a/tests/regression/15-deadlock/07-account_deadlock.c b/tests/regression/15-deadlock/07-account_deadlock.c
index bfa4661a36..7819cc51eb 100644
--- a/tests/regression/15-deadlock/07-account_deadlock.c
+++ b/tests/regression/15-deadlock/07-account_deadlock.c
@@ -10,7 +10,7 @@ typedef struct {
 bank_account A, B;
 
 void deposit(bank_account *f, bank_account *t, int ammount) {
-  pthread_mutex_lock(&f->mutex);
+  pthread_mutex_lock(&f->mutex);  // DEADLOCK
   pthread_mutex_lock(&t->mutex);  // DEADLOCK
   t->balance += ammount;
   f->balance -= ammount;
diff --git a/tests/regression/15-deadlock/08-account_nodeadlock.c b/tests/regression/15-deadlock/08-account_nodeadlock.c
index 36e0996cce..74252d9380 100644
--- a/tests/regression/15-deadlock/08-account_nodeadlock.c
+++ b/tests/regression/15-deadlock/08-account_nodeadlock.c
@@ -10,7 +10,7 @@ typedef struct {
 bank_account A, B;
 
 void deposit(bank_account *f, bank_account *t, int ammount) {
-  pthread_mutex_lock(&f->mutex);
+  pthread_mutex_lock(&f->mutex);  // NODEADLOCK
   pthread_mutex_lock(&t->mutex);  // NODEADLOCK
   t->balance += ammount;
   f->balance -= ammount;
diff --git a/tests/regression/15-deadlock/09-account_correct.c b/tests/regression/15-deadlock/09-account_correct.c
index 305a4d8428..617003b106 100644
--- a/tests/regression/15-deadlock/09-account_correct.c
+++ b/tests/regression/15-deadlock/09-account_correct.c
@@ -23,10 +23,10 @@ void deposit(bank_account *f, bank_account *t, int ammount) {
     return;
 
   if (f->id < t->id) {
-    pthread_mutex_lock(&f->mutex);
+    pthread_mutex_lock(&f->mutex); // NODEADLOCK
     pthread_mutex_lock(&t->mutex); // NODEADLOCK
   } else {
-    pthread_mutex_lock(&t->mutex);
+    pthread_mutex_lock(&t->mutex); // NODEADLOCK
     pthread_mutex_lock(&f->mutex); // NODEADLOCK
   }
 
diff --git a/tests/regression/15-deadlock/10-account_incorrect.c b/tests/regression/15-deadlock/10-account_incorrect.c
index 8c532fdfc8..a6a7b75da3 100644
--- a/tests/regression/15-deadlock/10-account_incorrect.c
+++ b/tests/regression/15-deadlock/10-account_incorrect.c
@@ -23,10 +23,10 @@ void deposit(bank_account *f, bank_account *t, int ammount) {
     return;
 
   if (f->id < t->id) {
-    pthread_mutex_lock(&f->mutex);
+    pthread_mutex_lock(&f->mutex); // DEADLOCK
     pthread_mutex_lock(&t->mutex); // DEADLOCK
   } else {
-    pthread_mutex_lock(&f->mutex);
+    pthread_mutex_lock(&f->mutex); // DEADLOCK
     pthread_mutex_lock(&t->mutex); // DEADLOCK
   }
 

From 6623816e33620e8c2096fcb357ef711da4ab8c19 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 21 Mar 2022 14:55:53 +0200
Subject: [PATCH 05/31] Remove location-insensitive DeadlockDomain.MyLock

---
 src/analyses/deadlock.ml       | 17 +++++++++--------
 src/cdomains/deadlockDomain.ml | 11 +----------
 2 files changed, 10 insertions(+), 18 deletions(-)

diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml
index b5d4337954..624b1c8fc2 100644
--- a/src/analyses/deadlock.ml
+++ b/src/analyses/deadlock.ml
@@ -16,7 +16,7 @@ struct
   module V = Printable.UnitConf (struct let name = "deadlock" end)
   module G =
   struct
-    include SetDomain.Make (Printable.Prod (MyLock0) (MyLock0))
+    include SetDomain.Make (Printable.Prod (MyLock) (MyLock))
     let leq x y = !GU.postsolving || leq x y (* HACK: to pass verify*)
   end
 
@@ -109,11 +109,12 @@ struct
     match q with
     | WarnGlobal _ -> (* just repr of () *)
       let order_set = ctx.global () in
-      let module LH = Hashtbl.Make (MyLock) in
+      let module LH = Hashtbl.Make (ValueDomain.Addr) in
+      let module LS = Set.Make (ValueDomain.Addr) in
       let order: G.t LH.t LH.t = LH.create 12 in
       G.iter (fun (a, b) ->
-          LH.modify_def (LH.create 1) a (fun h ->
-              LH.modify_def (G.empty ()) b (G.add (a, b)) h;
+          LH.modify_def (LH.create 1) a.addr (fun h ->
+              LH.modify_def (G.empty ()) b.addr (G.add (a, b)) h;
               h
             ) order
         ) order_set;
@@ -122,8 +123,8 @@ struct
       let global_visited_nodes = LH.create 100 in
 
       (* DFS *)
-      let rec iter_node path_visited_nodes (path_visited_nodes': G.elt list) node =
-        if D.mem node path_visited_nodes then (
+      let rec iter_node (path_visited_nodes: LS.t) (path_visited_nodes': G.elt list) (node: LS.elt) =
+        if LS.mem node path_visited_nodes then (
           let pieces =
             List.concat_map (fun (a, b) ->
                 [
@@ -137,7 +138,7 @@ struct
         )
         else if not (LH.mem global_visited_nodes node) then begin
           LH.replace global_visited_nodes node ();
-          let new_path_visited_nodes = D.add node path_visited_nodes in
+          let new_path_visited_nodes = LS.add node path_visited_nodes in
           LH.iter (fun to_node gs ->
               G.iter (fun g ->
                   let new_path_visited_nodes' = g :: path_visited_nodes' in
@@ -148,7 +149,7 @@ struct
       in
 
       LH.iter (fun a _ ->
-          iter_node (D.empty ()) [] a
+          iter_node LS.empty [] a
         ) order
     | _ -> Queries.Result.top q
 end
diff --git a/src/cdomains/deadlockDomain.ml b/src/cdomains/deadlockDomain.ml
index 31c91ce8d4..a9877e4b25 100644
--- a/src/cdomains/deadlockDomain.ml
+++ b/src/cdomains/deadlockDomain.ml
@@ -4,7 +4,7 @@ open Pretty
 type myowntypeEntry = {addr : ValueDomain.Addr.t ; loc : CilType.Location.t} [@@deriving eq, ord, hash]
 
 
-module MyLock0 : Printable.S with type t = myowntypeEntry =
+module MyLock : Printable.S with type t = myowntypeEntry =
 struct
   include Printable.Std (* for default invariant, tag, ... *)
 
@@ -17,13 +17,4 @@ struct
   let to_yojson x = `String (show x)
 end
 
-module MyLock : Printable.S with type t = myowntypeEntry =
-struct
-  include MyLock0
-  module Ad = ValueDomain.Addr
-  let equal x y = Ad.equal x.addr y.addr (* ignores loc field *)
-  let hash x = Ad.hash x.addr
-  let compare x y = Ad.compare x.addr y.addr (* ignores loc field *)
-end
-
 module Lockset = SetDomain.ToppedSet (MyLock) (struct let topname = "all locks" end)

From 94c379d6c6ad12e23d3dc224777cbb9a68217e09 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 21 Mar 2022 14:59:59 +0200
Subject: [PATCH 06/31] Use IdentitySpec for deadlock analysis

---
 src/analyses/deadlock.ml | 30 +-----------------------------
 1 file changed, 1 insertion(+), 29 deletions(-)

diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml
index 624b1c8fc2..a4b16f555a 100644
--- a/src/analyses/deadlock.ml
+++ b/src/analyses/deadlock.ml
@@ -6,7 +6,7 @@ open DeadlockDomain
 
 module Spec =
 struct
-  include Analyses.DefaultSpec
+  include Analyses.IdentitySpec
 
   let name () = "deadlock"
 
@@ -42,36 +42,8 @@ struct
   (* Some required states *)
   let startstate _ : D.t = D.empty ()
   let threadenter ctx lval f args = [D.empty ()]
-  let threadspawn ctx lval f args fctx = ctx.local
   let exitstate  _ : D.t = D.empty ()
 
-  (* ======== Transfer functions ======== *)
-  (* Called for assignments, branches, ... *)
-
-  (* Assignment lval <- exp *)
-  let assign ctx (lval:lval) (rval:exp) : D.t =
-    ctx.local
-
-  (* Branch *)
-  let branch ctx (exp:exp) (tv:bool) : D.t =
-    ctx.local
-
-  (* Body of a function starts *)
-  let body ctx (f:fundec) : D.t =
-    ctx.local
-
-  (* Returns from a function *)
-  let return ctx (exp:exp option) (f:fundec) : D.t =
-    ctx.local
-
-  (* Calls/Enters a function *)
-  let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
-    [D.bot (),ctx.local]
-
-  (* Leaves a function *)
-  let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) : D.t =
-    au
-
   (* Helper function to convert query-offsets to valuedomain-offsets *)
   let rec conv_offset x =
     match x with

From 74bd3c163efaf16a3e9114c886fe5148224bb6b2 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 21 Mar 2022 15:08:49 +0200
Subject: [PATCH 07/31] Use Lock and Unlock events for deadlock analysis

---
 src/analyses/deadlock.ml | 42 ++++++++++------------------------------
 1 file changed, 10 insertions(+), 32 deletions(-)

diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml
index a4b16f555a..4181bef295 100644
--- a/src/analyses/deadlock.ml
+++ b/src/analyses/deadlock.ml
@@ -44,38 +44,16 @@ struct
   let threadenter ctx lval f args = [D.empty ()]
   let exitstate  _ : D.t = D.empty ()
 
-  (* Helper function to convert query-offsets to valuedomain-offsets *)
-  let rec conv_offset x =
-    match x with
-    | `NoOffset    -> `NoOffset
-    | `Index (Const (CInt (i,ikind,s)),o) -> `Index (IntDomain.of_const (i,ikind,s), conv_offset o)
-    | `Index (_,o) -> `Index (ValueDomain.IndexDomain.top (), conv_offset o)
-    | `Field (f,o) -> `Field (f, conv_offset o)
-
-  (* Query the value (of the locking argument) to a list of locks. *)
-  let eval_exp_addr (a: Queries.ask) exp =
-    let gather_addr (v,o) b = ValueDomain.Addr.from_var_offset (v,conv_offset o) :: b in
-    match a.f (Queries.MayPointTo exp) with
-    | a when not (Queries.LS.is_top a) ->
-      Queries.LS.fold gather_addr (Queries.LS.remove (dummyFunDec.svar, `NoOffset) a) []
-    | b -> Messages.warn "Could not evaluate '%a' to an points-to set, instead got '%a'." d_exp exp Queries.LS.pretty b; []
-
-  (* Called when calling a special/unknown function *)
-  let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t =
-    if D.is_top ctx.local then ctx.local else
-      match LibraryFunctions.classify f.vname arglist with
-      | `Lock (_, _, _) ->
-        List.fold_left (fun d lockAddr ->
-            addLockingInfo ctx {addr = lockAddr; loc = !Tracing.current_loc } ctx.local;
-            D.add {addr = lockAddr; loc = !Tracing.current_loc } ctx.local
-          ) ctx.local (eval_exp_addr (Analyses.ask_of_ctx ctx) (List.hd arglist))
-      | `Unlock ->
-        let lockAddrs = eval_exp_addr (Analyses.ask_of_ctx ctx) (List.hd arglist) in
-        if List.compare_length_with lockAddrs 1 = 0 then
-          let inLockAddrs e = List.exists (fun r -> ValueDomain.Addr.equal r e.addr) lockAddrs in
-          D.filter (neg inLockAddrs) ctx.local
-        else ctx.local
-      | _ -> ctx.local
+  let event ctx (e: Events.t) octx =
+    match e with
+    | Lock addr ->
+      addLockingInfo ctx {addr; loc = !Tracing.current_loc } ctx.local;
+      D.add {addr; loc = !Tracing.current_loc } ctx.local
+    | Unlock addr ->
+      let inLockAddrs e = ValueDomain.Addr.equal addr e.addr in
+      D.filter (neg inLockAddrs) ctx.local
+    | _ ->
+      ctx.local
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
     match q with

From e7d96b7783203aae787b937460aed5fb47817886 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 21 Mar 2022 15:21:09 +0200
Subject: [PATCH 08/31] Refactor DeadlockDomain

---
 src/analyses/deadlock.ml       | 27 +++++++++++++--------------
 src/cdomains/deadlockDomain.ml | 19 +++----------------
 2 files changed, 16 insertions(+), 30 deletions(-)

diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml
index 4181bef295..a1c6899534 100644
--- a/src/analyses/deadlock.ml
+++ b/src/analyses/deadlock.ml
@@ -10,13 +10,12 @@ struct
 
   let name () = "deadlock"
 
-  (* The domain for the analysis *)
-  module D = DeadlockDomain.Lockset (* MayLockset *)
-  module C = DeadlockDomain.Lockset
+  module D = MayLockEvents
+  module C = D
   module V = Printable.UnitConf (struct let name = "deadlock" end)
   module G =
   struct
-    include SetDomain.Make (Printable.Prod (MyLock) (MyLock))
+    include SetDomain.Make (Printable.Prod (LockEvent) (LockEvent))
     let leq x y = !GU.postsolving || leq x y (* HACK: to pass verify*)
   end
 
@@ -47,10 +46,10 @@ struct
   let event ctx (e: Events.t) octx =
     match e with
     | Lock addr ->
-      addLockingInfo ctx {addr; loc = !Tracing.current_loc } ctx.local;
-      D.add {addr; loc = !Tracing.current_loc } ctx.local
+      addLockingInfo ctx (addr, !Tracing.current_loc) ctx.local;
+      D.add (addr, !Tracing.current_loc) ctx.local
     | Unlock addr ->
-      let inLockAddrs e = ValueDomain.Addr.equal addr e.addr in
+      let inLockAddrs (e, _) = Lock.equal addr e in
       D.filter (neg inLockAddrs) ctx.local
     | _ ->
       ctx.local
@@ -59,12 +58,12 @@ struct
     match q with
     | WarnGlobal _ -> (* just repr of () *)
       let order_set = ctx.global () in
-      let module LH = Hashtbl.Make (ValueDomain.Addr) in
-      let module LS = Set.Make (ValueDomain.Addr) in
+      let module LH = Hashtbl.Make (Lock) in
+      let module LS = Set.Make (Lock) in
       let order: G.t LH.t LH.t = LH.create 12 in
       G.iter (fun (a, b) ->
-          LH.modify_def (LH.create 1) a.addr (fun h ->
-              LH.modify_def (G.empty ()) b.addr (G.add (a, b)) h;
+          LH.modify_def (LH.create 1) (fst a) (fun h ->
+              LH.modify_def (G.empty ()) (fst b) (G.add (a, b)) h;
               h
             ) order
         ) order_set;
@@ -76,11 +75,11 @@ struct
       let rec iter_node (path_visited_nodes: LS.t) (path_visited_nodes': G.elt list) (node: LS.elt) =
         if LS.mem node path_visited_nodes then (
           let pieces =
-            List.concat_map (fun (a, b) ->
+            List.concat_map (fun ((alock, aloc), (block, bloc)) ->
                 [
                   (* backwards to get correct printout order *)
-                  (Pretty.dprintf "lock before: %a" MyLock.pretty b, Some b.loc);
-                  (Pretty.dprintf "lock after: %a" MyLock.pretty a, Some a.loc);
+                  (Pretty.dprintf "lock before: %a" Lock.pretty block, Some bloc);
+                  (Pretty.dprintf "lock after: %a" Lock.pretty alock, Some aloc);
                 ]
               ) path_visited_nodes'
           in
diff --git a/src/cdomains/deadlockDomain.ml b/src/cdomains/deadlockDomain.ml
index a9877e4b25..86580596ad 100644
--- a/src/cdomains/deadlockDomain.ml
+++ b/src/cdomains/deadlockDomain.ml
@@ -1,20 +1,7 @@
 open Cil
 open Pretty
 
-type myowntypeEntry = {addr : ValueDomain.Addr.t ; loc : CilType.Location.t} [@@deriving eq, ord, hash]
+module Lock = LockDomain.Addr
+module LockEvent = Printable.Prod (Lock) (CilType.Location)
 
-
-module MyLock : Printable.S with type t = myowntypeEntry =
-struct
-  include Printable.Std (* for default invariant, tag, ... *)
-
-  type t = myowntypeEntry [@@deriving eq, ord, hash]
-  module Ad = ValueDomain.Addr
-  let name () = "address with location"
-  let show x = (Ad.show x.addr) ^ "@" ^ (CilType.Location.show x.loc)
-  let pretty () x = Ad.pretty () x.addr ++ text "@" ++ CilType.Location.pretty () x.loc
-  let printXml c x = Ad.printXml c x.addr
-  let to_yojson x = `String (show x)
-end
-
-module Lockset = SetDomain.ToppedSet (MyLock) (struct let topname = "all locks" end)
+module MayLockEvents = SetDomain.ToppedSet (LockEvent) (struct let topname = "All lock events" end)

From bd1a8345a61f51b1c7e088d2ddacc95205f79b7d Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 21 Mar 2022 15:31:21 +0200
Subject: [PATCH 09/31] Split deadlock analysis global unknowns (issue #650)

---
 src/analyses/deadlock.ml | 36 +++++++++++++++---------------------
 1 file changed, 15 insertions(+), 21 deletions(-)

diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml
index a1c6899534..02900c8baa 100644
--- a/src/analyses/deadlock.ml
+++ b/src/analyses/deadlock.ml
@@ -12,10 +12,13 @@ struct
 
   module D = MayLockEvents
   module C = D
-  module V = Printable.UnitConf (struct let name = "deadlock" end)
+  module V = Lock
+
+  module LockEventPair = Printable.Prod (LockEvent) (LockEvent)
+  module MayLockEventPairs = SetDomain.Make (LockEventPair)
   module G =
   struct
-    include SetDomain.Make (Printable.Prod (LockEvent) (LockEvent))
+    include MapDomain.MapBot (Lock) (MayLockEventPairs)
     let leq x y = !GU.postsolving || leq x y (* HACK: to pass verify*)
   end
 
@@ -24,11 +27,11 @@ struct
     let add_comb a b =
       let d =
         if !GU.should_warn then
-          G.singleton (a, b)
+          G.singleton (fst b) (MayLockEventPairs.singleton (a, b))
         else
           G.bot () (* HACK: just to pass validation with MCP DomVariantLattice *)
       in
-      ctx.sideg () d
+      ctx.sideg (fst a) d
     in
 
     (* Add forbidden order *)
@@ -56,23 +59,16 @@ struct
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
     match q with
-    | WarnGlobal _ -> (* just repr of () *)
-      let order_set = ctx.global () in
+    | WarnGlobal g ->
+      let g: V.t = Obj.obj g in
+
       let module LH = Hashtbl.Make (Lock) in
       let module LS = Set.Make (Lock) in
-      let order: G.t LH.t LH.t = LH.create 12 in
-      G.iter (fun (a, b) ->
-          LH.modify_def (LH.create 1) (fst a) (fun h ->
-              LH.modify_def (G.empty ()) (fst b) (G.add (a, b)) h;
-              h
-            ) order
-        ) order_set;
-
       (* TODO: find all cycles/SCCs *)
       let global_visited_nodes = LH.create 100 in
 
       (* DFS *)
-      let rec iter_node (path_visited_nodes: LS.t) (path_visited_nodes': G.elt list) (node: LS.elt) =
+      let rec iter_node (path_visited_nodes: LS.t) (path_visited_nodes': LockEventPair.t list) (node: Lock.t) =
         if LS.mem node path_visited_nodes then (
           let pieces =
             List.concat_map (fun ((alock, aloc), (block, bloc)) ->
@@ -88,18 +84,16 @@ struct
         else if not (LH.mem global_visited_nodes node) then begin
           LH.replace global_visited_nodes node ();
           let new_path_visited_nodes = LS.add node path_visited_nodes in
-          LH.iter (fun to_node gs ->
-              G.iter (fun g ->
+          G.iter (fun to_node gs ->
+              MayLockEventPairs.iter (fun g ->
                   let new_path_visited_nodes' = g :: path_visited_nodes' in
                   iter_node new_path_visited_nodes new_path_visited_nodes' to_node
                 ) gs
-            ) (LH.find_default order node (LH.create 0))
+            ) (ctx.global node)
         end
       in
 
-      LH.iter (fun a _ ->
-          iter_node LS.empty [] a
-        ) order
+      iter_node LS.empty [] g
     | _ -> Queries.Result.top q
 end
 

From 200ff8a9dd06af733db405fc7844c3f9fb8be3c3 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 21 Mar 2022 15:36:35 +0200
Subject: [PATCH 10/31] Flip deadlock analysis pairs from forbidden to actual

---
 src/analyses/deadlock.ml | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml
index 02900c8baa..26efbe093a 100644
--- a/src/analyses/deadlock.ml
+++ b/src/analyses/deadlock.ml
@@ -34,10 +34,9 @@ struct
       ctx.sideg (fst a) d
     in
 
-    (* Add forbidden order *)
     D.iter (
       fun lock ->
-        add_comb newLock lock;
+        add_comb lock newLock;
       ) lockList
 
 
@@ -73,11 +72,10 @@ struct
           let pieces =
             List.concat_map (fun ((alock, aloc), (block, bloc)) ->
                 [
-                  (* backwards to get correct printout order *)
-                  (Pretty.dprintf "lock before: %a" Lock.pretty block, Some bloc);
-                  (Pretty.dprintf "lock after: %a" Lock.pretty alock, Some aloc);
+                  (Pretty.dprintf "lock before: %a" Lock.pretty alock, Some aloc);
+                  (Pretty.dprintf "lock after: %a" Lock.pretty block, Some bloc);
                 ]
-              ) path_visited_nodes'
+              ) (List.rev path_visited_nodes') (* backwards to get correct printout order *)
           in
           M.msg_group Warning "Deadlock order" pieces
         )

From 98eed4ba1b86d021bbb89b3ed50a520535afdbfc Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 21 Mar 2022 15:41:26 +0200
Subject: [PATCH 11/31] Refactor Deadlock.addLockingInfo

---
 src/analyses/deadlock.ml | 29 ++++++++++++-----------------
 1 file changed, 12 insertions(+), 17 deletions(-)

diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml
index 26efbe093a..d3acf7d331 100644
--- a/src/analyses/deadlock.ml
+++ b/src/analyses/deadlock.ml
@@ -22,22 +22,14 @@ struct
     let leq x y = !GU.postsolving || leq x y (* HACK: to pass verify*)
   end
 
-  let addLockingInfo ctx newLock lockList =
-
-    let add_comb a b =
-      let d =
-        if !GU.should_warn then
-          G.singleton (fst b) (MayLockEventPairs.singleton (a, b))
-        else
-          G.bot () (* HACK: just to pass validation with MCP DomVariantLattice *)
-      in
-      ctx.sideg (fst a) d
+  let side_lock_event_pair ctx before after =
+    let d =
+      if !GU.should_warn then
+        G.singleton (fst after) (MayLockEventPairs.singleton (before, after))
+      else
+        G.bot () (* HACK: just to pass validation with MCP DomVariantLattice *)
     in
-
-    D.iter (
-      fun lock ->
-        add_comb lock newLock;
-      ) lockList
+    ctx.sideg (fst before) d
 
 
   (* Some required states *)
@@ -48,8 +40,11 @@ struct
   let event ctx (e: Events.t) octx =
     match e with
     | Lock addr ->
-      addLockingInfo ctx (addr, !Tracing.current_loc) ctx.local;
-      D.add (addr, !Tracing.current_loc) ctx.local
+      let after = (addr, !Tracing.current_loc) in
+      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
       D.filter (neg inLockAddrs) ctx.local

From 0cae493831a3244902a0a9311965997d392422d9 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 21 Mar 2022 15:46:14 +0200
Subject: [PATCH 12/31] Refactor Deadlock WarnGlobal

---
 src/analyses/deadlock.ml | 32 ++++++++++++++++----------------
 1 file changed, 16 insertions(+), 16 deletions(-)

diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml
index d3acf7d331..436e5e8aec 100644
--- a/src/analyses/deadlock.ml
+++ b/src/analyses/deadlock.ml
@@ -59,34 +59,34 @@ struct
       let module LH = Hashtbl.Make (Lock) in
       let module LS = Set.Make (Lock) in
       (* TODO: find all cycles/SCCs *)
-      let global_visited_nodes = LH.create 100 in
+      let global_visited_locks = LH.create 100 in
 
       (* DFS *)
-      let rec iter_node (path_visited_nodes: LS.t) (path_visited_nodes': LockEventPair.t list) (node: Lock.t) =
-        if LS.mem node path_visited_nodes then (
-          let pieces =
+      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 (
+          let msgs =
             List.concat_map (fun ((alock, aloc), (block, bloc)) ->
                 [
                   (Pretty.dprintf "lock before: %a" Lock.pretty alock, Some aloc);
                   (Pretty.dprintf "lock after: %a" Lock.pretty block, Some bloc);
                 ]
-              ) (List.rev path_visited_nodes') (* backwards to get correct printout order *)
+              ) (List.rev path_visited_lock_event_pairs) (* backwards to get correct printout order *)
           in
-          M.msg_group Warning "Deadlock order" pieces
+          M.msg_group Warning "Deadlock order" msgs
         )
-        else if not (LH.mem global_visited_nodes node) then begin
-          LH.replace global_visited_nodes node ();
-          let new_path_visited_nodes = LS.add node path_visited_nodes in
-          G.iter (fun to_node gs ->
-              MayLockEventPairs.iter (fun g ->
-                  let new_path_visited_nodes' = g :: path_visited_nodes' in
-                  iter_node new_path_visited_nodes new_path_visited_nodes' to_node
-                ) gs
-            ) (ctx.global node)
+        else if not (LH.mem global_visited_locks lock) then begin
+          LH.replace global_visited_locks lock ();
+          let new_path_visited_locks = LS.add lock path_visited_locks in
+          G.iter (fun to_lock lock_event_pairs ->
+              MayLockEventPairs.iter (fun lock_event_pair ->
+                  let new_path_visited_lock_event_pairs' = lock_event_pair :: path_visited_lock_event_pairs in
+                  iter_lock new_path_visited_locks new_path_visited_lock_event_pairs' to_lock
+                ) lock_event_pairs
+            ) (ctx.global lock)
         end
       in
 
-      iter_node LS.empty [] g
+      iter_lock LS.empty [] g
     | _ -> Queries.Result.top q
 end
 

From 81c7a9d016bb29a0ea7164ffad10411274473cd6 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 21 Mar 2022 15:47:18 +0200
Subject: [PATCH 13/31] Add deadlock warn_global timing

---
 src/analyses/deadlock.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml
index 436e5e8aec..3d665aa07b 100644
--- a/src/analyses/deadlock.ml
+++ b/src/analyses/deadlock.ml
@@ -86,7 +86,7 @@ struct
         end
       in
 
-      iter_lock LS.empty [] g
+      Stats.time "deadlock" (iter_lock LS.empty []) g
     | _ -> Queries.Result.top q
 end
 

From a666d9fb0b9ac851c674651dae2e423fbb51d9ff Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 21 Mar 2022 15:52:57 +0200
Subject: [PATCH 14/31] Add Deadlock message category

---
 src/analyses/deadlock.ml     | 11 ++++++-----
 src/util/messageCategory.ml  |  5 +++++
 src/util/options.schema.json |  6 ++++++
 3 files changed, 17 insertions(+), 5 deletions(-)

diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml
index 3d665aa07b..ec2a43b0c8 100644
--- a/src/analyses/deadlock.ml
+++ b/src/analyses/deadlock.ml
@@ -65,14 +65,15 @@ struct
       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 (
           let msgs =
-            List.concat_map (fun ((alock, aloc), (block, bloc)) ->
+            List.rev path_visited_lock_event_pairs (* backwards to get correct printout order *)
+            |> List.concat_map (fun ((before_lock, before_loc), (after_lock, after_loc)) ->
                 [
-                  (Pretty.dprintf "lock before: %a" Lock.pretty alock, Some aloc);
-                  (Pretty.dprintf "lock after: %a" Lock.pretty block, Some bloc);
+                  (Pretty.dprintf "lock before: %a" Lock.pretty before_lock, Some before_loc);
+                  (Pretty.dprintf "lock after: %a" Lock.pretty after_lock, Some after_loc);
                 ]
-              ) (List.rev path_visited_lock_event_pairs) (* backwards to get correct printout order *)
+              )
           in
-          M.msg_group Warning "Deadlock order" msgs
+          M.msg_group Warning ~category:Deadlock "Locking order cycle" msgs
         )
         else if not (LH.mem global_visited_locks lock) then begin
           LH.replace global_visited_locks lock ();
diff --git a/src/util/messageCategory.ml b/src/util/messageCategory.ml
index f644c0ac1f..cbfc643409 100644
--- a/src/util/messageCategory.ml
+++ b/src/util/messageCategory.ml
@@ -27,6 +27,7 @@ type category =
   | Behavior of behavior
   | Integer of integer
   | Race
+  | Deadlock
   | Cast of cast
   | Deadcode
   | Unknown
@@ -160,6 +161,7 @@ let should_warn e =
     | Behavior _ -> "behavior"
     | Integer _ -> "integer"
     | Race -> "race"
+    | Deadlock -> "deadlock"
     | Cast _ -> "cast"
     | Deadcode -> "deadcode"
     | Unknown -> "unknown"
@@ -174,6 +176,7 @@ let path_show e =
   | Behavior x -> "Behavior" :: Behavior.path_show x
   | Integer x -> "Integer" :: Integer.path_show x
   | Race -> ["Race"]
+  | Deadlock -> ["Deadlock"]
   | Cast x -> "Cast" :: Cast.path_show x
   | Deadcode -> ["Deadcode"]
   | Unknown -> ["Unknown"]
@@ -197,6 +200,7 @@ let categoryName = function
   | Assert -> "Assert"
 
   | Race -> "Race"
+  | Deadlock -> "Deadlock"
   | Cast x -> "Cast"
   | Deadcode -> "Deadcode"
   | Unknown -> "Unknown"
@@ -218,6 +222,7 @@ let from_string_list (s: string list) =
     | "behavior" -> Behavior.from_string_list t
     | "integer" -> Integer.from_string_list t
     | "race" -> Race
+    | "deadlock" -> Deadlock
     | "cast" -> Cast.from_string_list t
     | "deadcode" -> Deadcode
     | "analyzer" -> Analyzer
diff --git a/src/util/options.schema.json b/src/util/options.schema.json
index 9f114ec749..4edff233e0 100644
--- a/src/util/options.schema.json
+++ b/src/util/options.schema.json
@@ -1575,6 +1575,12 @@
           "type": "boolean",
           "default": true
         },
+        "deadlock": {
+          "title": "warn.deadlock",
+          "description": "Deadlock warnings",
+          "type": "boolean",
+          "default": true
+        },
         "deadcode": {
           "title": "warn.deadcode",
           "description": "Dead code warnings",

From 6e86f3927dd5c5d7449069fc42cedd540d7cfb53 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 21 Mar 2022 16:03:51 +0200
Subject: [PATCH 15/31] Normalize deadlock cycles to prevent equivalent
 warnings

---
 src/analyses/deadlock.ml | 19 +++++++++++--------
 1 file changed, 11 insertions(+), 8 deletions(-)

diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml
index ec2a43b0c8..816095a524 100644
--- a/src/analyses/deadlock.ml
+++ b/src/analyses/deadlock.ml
@@ -64,14 +64,17 @@ struct
       (* 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 (
-          let msgs =
-            List.rev path_visited_lock_event_pairs (* backwards to get correct printout order *)
-            |> List.concat_map (fun ((before_lock, before_loc), (after_lock, after_loc)) ->
-                [
-                  (Pretty.dprintf "lock before: %a" Lock.pretty before_lock, Some before_loc);
-                  (Pretty.dprintf "lock after: %a" Lock.pretty after_lock, Some after_loc);
-                ]
-              )
+          (* normalize path_visited_lock_event_pairs such that we don't get the same cycle multiple times, starting from different events *)
+          let min = List.min ~cmp:LockEventPair.compare path_visited_lock_event_pairs in
+          let (mini, _) = List.findi (fun i x -> LockEventPair.equal min x) path_visited_lock_event_pairs in
+          let (init, tail) = List.split_at mini path_visited_lock_event_pairs in
+          let normalized = List.rev_append init (List.rev tail) in (* backwards to get correct printout order *)
+          let msgs = List.concat_map (fun ((before_lock, before_loc), (after_lock, after_loc)) ->
+              [
+                (Pretty.dprintf "lock before: %a" Lock.pretty before_lock, Some before_loc);
+                (Pretty.dprintf "lock after: %a" Lock.pretty after_lock, Some after_loc);
+              ]
+            ) normalized
           in
           M.msg_group Warning ~category:Deadlock "Locking order cycle" msgs
         )

From 90fdc00daff55a811d72f2de181e76276743e14e Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 21 Mar 2022 16:15:38 +0200
Subject: [PATCH 16/31] Replace Cil.location with Node in deadlock event (issue
 #650)

---
 src/analyses/deadlock.ml       | 8 ++++----
 src/cdomains/deadlockDomain.ml | 2 +-
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml
index 816095a524..4904ef5654 100644
--- a/src/analyses/deadlock.ml
+++ b/src/analyses/deadlock.ml
@@ -40,7 +40,7 @@ struct
   let event ctx (e: Events.t) octx =
     match e with
     | Lock addr ->
-      let after = (addr, !Tracing.current_loc) in
+      let after = (addr, ctx.prev_node) in
       D.iter (fun before ->
           side_lock_event_pair ctx before after
         ) ctx.local;
@@ -69,10 +69,10 @@ struct
           let (mini, _) = List.findi (fun i x -> LockEventPair.equal min x) path_visited_lock_event_pairs in
           let (init, tail) = List.split_at mini path_visited_lock_event_pairs in
           let normalized = List.rev_append init (List.rev tail) in (* backwards to get correct printout order *)
-          let msgs = List.concat_map (fun ((before_lock, before_loc), (after_lock, after_loc)) ->
+          let msgs = List.concat_map (fun ((before_lock, before_node), (after_lock, after_node)) ->
               [
-                (Pretty.dprintf "lock before: %a" Lock.pretty before_lock, Some before_loc);
-                (Pretty.dprintf "lock after: %a" Lock.pretty after_lock, Some after_loc);
+                (Pretty.dprintf "lock before: %a" Lock.pretty before_lock, Some (UpdateCil.getLoc before_node));
+                (Pretty.dprintf "lock after: %a" Lock.pretty after_lock, Some (UpdateCil.getLoc after_node));
               ]
             ) normalized
           in
diff --git a/src/cdomains/deadlockDomain.ml b/src/cdomains/deadlockDomain.ml
index 86580596ad..bad86aaf57 100644
--- a/src/cdomains/deadlockDomain.ml
+++ b/src/cdomains/deadlockDomain.ml
@@ -2,6 +2,6 @@ open Cil
 open Pretty
 
 module Lock = LockDomain.Addr
-module LockEvent = Printable.Prod (Lock) (CilType.Location)
+module LockEvent = Printable.Prod (Lock) (Node)
 
 module MayLockEvents = SetDomain.ToppedSet (LockEvent) (struct let topname = "All lock events" end)

From 6745cdf7434a758aa2bac292aa416991d8ef0d67 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Mon, 21 Mar 2022 16:17:39 +0200
Subject: [PATCH 17/31] Realign case in update_suite.rb

---
 scripts/update_suite.rb | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/scripts/update_suite.rb b/scripts/update_suite.rb
index 5c19c38a11..5b8b2d0563 100755
--- a/scripts/update_suite.rb
+++ b/scripts/update_suite.rb
@@ -153,7 +153,7 @@ def collect_warnings
                     when /\(conf\. \d+\)/            then "race"
                     when /lockset:/                  then "race" # osek races have their own legacy-like output
                     when /Deadlock/                  then "deadlock"
-                    when /lock (before|after):/           then "deadlock"
+                    when /lock (before|after):/      then "deadlock"
                     when /Assertion .* will fail/    then "fail"
                     when /Assertion .* will succeed/ then "success"
                     when /Assertion .* is unknown/   then "unknown"

From 50ba58fb34350da6e81714afc38673c242b1b819 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 22 Mar 2022 10:30:19 +0200
Subject: [PATCH 18/31] Add mutex analysis dependency to deadlock analysis

Otherwise no Lock/Unlock events get emitted.
---
 src/analyses/deadlock.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml
index 4904ef5654..f38f35dc2f 100644
--- a/src/analyses/deadlock.ml
+++ b/src/analyses/deadlock.ml
@@ -95,4 +95,4 @@ struct
 end
 
 let _ =
-  MCP.register_analysis (module Spec : MCPSpec)
+  MCP.register_analysis ~dep:["mutex"] (module Spec : MCPSpec)

From 74eb3e370f275ef1825b2a5fb877cf7f1ae9be52 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 22 Mar 2022 11:11:59 +0200
Subject: [PATCH 19/31] Add TODO no deadlock test due to common mutex

---
 .../15-deadlock/11-common_mutex_nodeadlock.c  | 41 +++++++++++++++++++
 1 file changed, 41 insertions(+)
 create mode 100644 tests/regression/15-deadlock/11-common_mutex_nodeadlock.c

diff --git a/tests/regression/15-deadlock/11-common_mutex_nodeadlock.c b/tests/regression/15-deadlock/11-common_mutex_nodeadlock.c
new file mode 100644
index 0000000000..ae71830f7d
--- /dev/null
+++ b/tests/regression/15-deadlock/11-common_mutex_nodeadlock.c
@@ -0,0 +1,41 @@
+// PARAM: --set ana.activated[+] deadlock
+#include <pthread.h>
+#include <stdio.h>
+
+int g1, g2;
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t mutex3 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t1(void *arg) {
+  pthread_mutex_lock(&mutex3); // NODEADLOCK
+  pthread_mutex_lock(&mutex1); // TODO NODEADLOCK (common mutex3)
+  pthread_mutex_lock(&mutex2); // TODO NODEADLOCK (common mutex3)
+  g1 = g2 + 1;
+  pthread_mutex_unlock(&mutex2);
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+void *t2(void *arg) {
+  pthread_mutex_lock(&mutex3); // NODEADLOCK
+  pthread_mutex_lock(&mutex2); // TODO NODEADLOCK (common mutex3)
+  pthread_mutex_lock(&mutex1); // TODO NODEADLOCK (common mutex3)
+  g2 = g1 + 1;
+  pthread_mutex_unlock(&mutex1);
+  pthread_mutex_unlock(&mutex2);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id1, id2;
+  int i;
+  for (i = 0; i < 10000; i++) {
+    pthread_create(&id1, NULL, t1, NULL);
+    pthread_create(&id2, NULL, t2, NULL);
+    pthread_join (id1, NULL);
+    pthread_join (id2, NULL);
+    printf("%d: g1 = %d, g2 = %d.\n", i, g1, g2);
+  }
+  return 0;
+}

From eea313c5148208457f8b83343b68c57224c59213 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 22 Mar 2022 11:12:41 +0200
Subject: [PATCH 20/31] Fix deadlock cycle print containing stem locks

---
 src/analyses/deadlock.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml
index f38f35dc2f..77d7aed230 100644
--- a/src/analyses/deadlock.ml
+++ b/src/analyses/deadlock.ml
@@ -64,6 +64,14 @@ struct
       (* 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 (
+          (* 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)
+              ) (List.tl path_visited_lock_event_pairs)
+          in
           (* normalize path_visited_lock_event_pairs such that we don't get the same cycle multiple times, starting from different events *)
           let min = List.min ~cmp:LockEventPair.compare path_visited_lock_event_pairs in
           let (mini, _) = List.findi (fun i x -> LockEventPair.equal min x) path_visited_lock_event_pairs in

From 78d601ccff5ceefcf7c2de452bb1df8375436eb5 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 22 Mar 2022 11:38:20 +0200
Subject: [PATCH 21/31] Add deadlock non-concurrency example from Kroenig et al
 ASE16

---
 .../15-deadlock/12-ase16_nodeadlock.c         | 65 +++++++++++++++++++
 1 file changed, 65 insertions(+)
 create mode 100644 tests/regression/15-deadlock/12-ase16_nodeadlock.c

diff --git a/tests/regression/15-deadlock/12-ase16_nodeadlock.c b/tests/regression/15-deadlock/12-ase16_nodeadlock.c
new file mode 100644
index 0000000000..50e5156c04
--- /dev/null
+++ b/tests/regression/15-deadlock/12-ase16_nodeadlock.c
@@ -0,0 +1,65 @@
+// PARAM: --set ana.activated[+] deadlock --set ana.activated[+] threadJoins
+// From https://arxiv.org/abs/1607.06927
+#include <pthread.h>
+
+int x;
+pthread_mutex_t m1 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t m2 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t m3 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t m4 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t m5 = PTHREAD_MUTEX_INITIALIZER;
+
+void func1() {
+  x = 0; // RACE!
+}
+
+int func2(int a) {
+  pthread_mutex_lock(&m5); // TODO NODEADLOCK (thread joined)
+  pthread_mutex_lock(&m4); // TODO NODEADLOCK (thread joined)
+  if (a)
+    x = 3; // NORACE (thread joined)
+  else
+    x = 4;
+  pthread_mutex_unlock(&m4);
+  pthread_mutex_unlock(&m5);
+  return 0;
+}
+
+void *thread() {
+  pthread_mutex_lock(&m1); // NODEADLOCK
+  pthread_mutex_lock(&m2); // TODO NODEADLOCK (common m1)
+  pthread_mutex_lock(&m3); // TODO NODEADLOCK (common m1)
+  x = 1; // NORACE (thread joined)
+  pthread_mutex_unlock(&m3);
+  pthread_mutex_unlock(&m2);
+  pthread_mutex_unlock(&m1);
+
+  pthread_mutex_lock(&m4); // TODO NODEADLOCK (thread joined)
+  pthread_mutex_lock(&m5); // TODO NODEADLOCK (thread joined)
+  x = 2; // RACE!
+  pthread_mutex_unlock(&m5);
+  pthread_mutex_unlock(&m4);
+
+  return NULL;
+}
+
+int main() {
+  pthread_t tid;
+
+  pthread_create(&tid, NULL, thread, NULL);
+
+  pthread_mutex_lock(&m1); // NODEADLOCK
+  pthread_mutex_lock(&m3); // TODO NODEADLOCK (common m1)
+  pthread_mutex_lock(&m2); // TODO NODEADLOCK (common m1)
+  func1();
+  pthread_mutex_unlock(&m2);
+  pthread_mutex_unlock(&m3);
+  pthread_mutex_unlock(&m1);
+
+  pthread_join(tid, NULL);
+
+  int r;
+  r = func2(5);
+
+  return 0;
+}

From fb5fca3c0c3b5f8c11b92d871d7985026af78e56 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 22 Mar 2022 11:43:58 +0200
Subject: [PATCH 22/31] Exclude deadlocks by non-concurrency (MHP) (issue #650)

---
 src/analyses/deadlock.ml                      | 45 ++++++++++++-------
 src/analyses/mutexAnalysis.ml                 |  2 +-
 src/analyses/region.ml                        | 18 +++++---
 src/analyses/symbLocks.ml                     |  5 ++-
 src/cdomains/deadlockDomain.ml                |  2 +-
 .../15-deadlock/11-common_mutex_nodeadlock.c  |  8 ++--
 .../15-deadlock/12-ase16_nodeadlock.c         | 16 +++----
 7 files changed, 57 insertions(+), 39 deletions(-)

diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml
index 77d7aed230..16bc0376db 100644
--- a/src/analyses/deadlock.ml
+++ b/src/analyses/deadlock.ml
@@ -25,11 +25,11 @@ struct
   let side_lock_event_pair ctx before after =
     let d =
       if !GU.should_warn then
-        G.singleton (fst after) (MayLockEventPairs.singleton (before, after))
+        G.singleton (Tuple3.first after) (MayLockEventPairs.singleton (before, after))
       else
         G.bot () (* HACK: just to pass validation with MCP DomVariantLattice *)
     in
-    ctx.sideg (fst before) d
+    ctx.sideg (Tuple3.first before) d
 
 
   (* Some required states *)
@@ -37,16 +37,19 @@ struct
   let threadenter ctx lval f args = [D.empty ()]
   let exitstate  _ : D.t = D.empty ()
 
+  let part_access ctx: MCPAccess.A.t =
+    Obj.obj (ctx.ask (PartAccess {exp=MyCFG.unknown_exp; var_opt=None; write=false}))
+
   let event ctx (e: Events.t) octx =
     match e with
     | Lock addr ->
-      let after = (addr, ctx.prev_node) in
+      let after = (addr, ctx.prev_node, part_access octx) 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 inLockAddrs (e, _, _) = Lock.equal addr e in
       D.filter (neg inLockAddrs) ctx.local
     | _ ->
       ctx.local
@@ -68,23 +71,31 @@ struct
           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, _)) ->
+            List.take_while (fun (_, (after_lock, _, _)) ->
                 not (Lock.equal after_lock lock)
               ) (List.tl path_visited_lock_event_pairs)
           in
-          (* normalize path_visited_lock_event_pairs such that we don't get the same cycle multiple times, starting from different events *)
-          let min = List.min ~cmp:LockEventPair.compare path_visited_lock_event_pairs in
-          let (mini, _) = List.findi (fun i x -> LockEventPair.equal min x) path_visited_lock_event_pairs in
-          let (init, tail) = List.split_at mini path_visited_lock_event_pairs in
-          let normalized = List.rev_append init (List.rev tail) in (* backwards to get correct printout order *)
-          let msgs = List.concat_map (fun ((before_lock, before_node), (after_lock, after_node)) ->
-              [
-                (Pretty.dprintf "lock before: %a" Lock.pretty before_lock, Some (UpdateCil.getLoc before_node));
-                (Pretty.dprintf "lock after: %a" Lock.pretty after_lock, Some (UpdateCil.getLoc after_node));
-              ]
-            ) normalized
+          let mhp =
+            Enum.cartesian_product (List.enum path_visited_lock_event_pairs) (List.enum path_visited_lock_event_pairs)
+            |> Enum.for_all (fun (((_, (_, _, access1)) as p1), ((_, (_, _, access2)) as p2)) ->
+                LockEventPair.equal p1 p2 || MCPAccess.A.may_race access1 access2
+              )
           in
-          M.msg_group Warning ~category:Deadlock "Locking order cycle" msgs
+          if mhp then (
+            (* normalize path_visited_lock_event_pairs such that we don't get the same cycle multiple times, starting from different events *)
+            let min = List.min ~cmp:LockEventPair.compare path_visited_lock_event_pairs in
+            let (mini, _) = List.findi (fun i x -> LockEventPair.equal min x) path_visited_lock_event_pairs in
+            let (init, tail) = List.split_at mini path_visited_lock_event_pairs in
+            let normalized = List.rev_append init (List.rev tail) in (* backwards to get correct printout order *)
+            let msgs = List.concat_map (fun ((before_lock, before_node, _), (after_lock, after_node, _)) ->
+                [
+                  (Pretty.dprintf "lock before: %a" Lock.pretty before_lock, Some (UpdateCil.getLoc before_node));
+                  (Pretty.dprintf "lock after: %a" Lock.pretty after_lock, Some (UpdateCil.getLoc after_node));
+                ]
+              ) normalized
+            in
+            M.msg_group Warning ~category:Deadlock "Locking order cycle" msgs
+          )
         )
         else if not (LH.mem global_visited_locks lock) then begin
           LH.replace global_visited_locks lock ();
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index 21bc76686b..3c836d0ed6 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -163,7 +163,7 @@ struct
   end
 
   let access ctx e vo w =
-    if w then
+    if e = MyCFG.unknown_exp || w then
       (* when writing: ignore reader locks *)
       Lockset.filter snd ctx.local
     else
diff --git a/src/analyses/region.ml b/src/analyses/region.ml
index 9c326117de..d5e6e9818a 100644
--- a/src/analyses/region.ml
+++ b/src/analyses/region.ml
@@ -70,13 +70,17 @@ struct
       | _ -> true
   end
   let access ctx e vo w =
-    (* TODO: remove regions that cannot be reached from the var*)
-    let rec unknown_index = function
-      | `NoOffset -> `NoOffset
-      | `Field (f, os) -> `Field (f, unknown_index os)
-      | `Index (i, os) -> `Index (MyCFG.unknown_exp, unknown_index os) (* forget specific indices *)
-    in
-    Option.map (Lvals.of_list % List.map (Tuple2.map2 unknown_index)) (get_region ctx e)
+    if e = MyCFG.unknown_exp then
+      Some (Lvals.empty ())
+    else (
+      (* TODO: remove regions that cannot be reached from the var*)
+      let rec unknown_index = function
+        | `NoOffset -> `NoOffset
+        | `Field (f, os) -> `Field (f, unknown_index os)
+        | `Index (i, os) -> `Index (MyCFG.unknown_exp, unknown_index os) (* forget specific indices *)
+      in
+      Option.map (Lvals.of_list % List.map (Tuple2.map2 unknown_index)) (get_region ctx e)
+    )
 
   (* transfer functions *)
   let assign ctx (lval:lval) (rval:exp) : D.t =
diff --git a/src/analyses/symbLocks.ml b/src/analyses/symbLocks.ml
index 258694f42f..07616a2f2c 100644
--- a/src/analyses/symbLocks.ml
+++ b/src/analyses/symbLocks.ml
@@ -219,7 +219,10 @@ struct
     let should_print lp = not (is_empty lp)
   end
   let access ctx e vo w =
-    add_per_element_access ctx e false
+    if e = MyCFG.unknown_exp then
+      A.empty ()
+    else
+      add_per_element_access ctx e false
 end
 
 let _ =
diff --git a/src/cdomains/deadlockDomain.ml b/src/cdomains/deadlockDomain.ml
index bad86aaf57..888477519e 100644
--- a/src/cdomains/deadlockDomain.ml
+++ b/src/cdomains/deadlockDomain.ml
@@ -2,6 +2,6 @@ open Cil
 open Pretty
 
 module Lock = LockDomain.Addr
-module LockEvent = Printable.Prod (Lock) (Node)
+module LockEvent = Printable.Prod3 (Lock) (Node) (MCPAccess.A)
 
 module MayLockEvents = SetDomain.ToppedSet (LockEvent) (struct let topname = "All lock events" end)
diff --git a/tests/regression/15-deadlock/11-common_mutex_nodeadlock.c b/tests/regression/15-deadlock/11-common_mutex_nodeadlock.c
index ae71830f7d..ef23346ade 100644
--- a/tests/regression/15-deadlock/11-common_mutex_nodeadlock.c
+++ b/tests/regression/15-deadlock/11-common_mutex_nodeadlock.c
@@ -9,8 +9,8 @@ pthread_mutex_t mutex3 = PTHREAD_MUTEX_INITIALIZER;
 
 void *t1(void *arg) {
   pthread_mutex_lock(&mutex3); // NODEADLOCK
-  pthread_mutex_lock(&mutex1); // TODO NODEADLOCK (common mutex3)
-  pthread_mutex_lock(&mutex2); // TODO NODEADLOCK (common mutex3)
+  pthread_mutex_lock(&mutex1); // NODEADLOCK (common mutex3)
+  pthread_mutex_lock(&mutex2); // NODEADLOCK (common mutex3)
   g1 = g2 + 1;
   pthread_mutex_unlock(&mutex2);
   pthread_mutex_unlock(&mutex1);
@@ -19,8 +19,8 @@ void *t1(void *arg) {
 
 void *t2(void *arg) {
   pthread_mutex_lock(&mutex3); // NODEADLOCK
-  pthread_mutex_lock(&mutex2); // TODO NODEADLOCK (common mutex3)
-  pthread_mutex_lock(&mutex1); // TODO NODEADLOCK (common mutex3)
+  pthread_mutex_lock(&mutex2); // NODEADLOCK (common mutex3)
+  pthread_mutex_lock(&mutex1); // NODEADLOCK (common mutex3)
   g2 = g1 + 1;
   pthread_mutex_unlock(&mutex1);
   pthread_mutex_unlock(&mutex2);
diff --git a/tests/regression/15-deadlock/12-ase16_nodeadlock.c b/tests/regression/15-deadlock/12-ase16_nodeadlock.c
index 50e5156c04..1cbdf2e704 100644
--- a/tests/regression/15-deadlock/12-ase16_nodeadlock.c
+++ b/tests/regression/15-deadlock/12-ase16_nodeadlock.c
@@ -14,8 +14,8 @@ void func1() {
 }
 
 int func2(int a) {
-  pthread_mutex_lock(&m5); // TODO NODEADLOCK (thread joined)
-  pthread_mutex_lock(&m4); // TODO NODEADLOCK (thread joined)
+  pthread_mutex_lock(&m5); // NODEADLOCK (thread joined)
+  pthread_mutex_lock(&m4); // NODEADLOCK (thread joined)
   if (a)
     x = 3; // NORACE (thread joined)
   else
@@ -27,15 +27,15 @@ int func2(int a) {
 
 void *thread() {
   pthread_mutex_lock(&m1); // NODEADLOCK
-  pthread_mutex_lock(&m2); // TODO NODEADLOCK (common m1)
-  pthread_mutex_lock(&m3); // TODO NODEADLOCK (common m1)
+  pthread_mutex_lock(&m2); // NODEADLOCK (common m1)
+  pthread_mutex_lock(&m3); // NODEADLOCK (common m1)
   x = 1; // NORACE (thread joined)
   pthread_mutex_unlock(&m3);
   pthread_mutex_unlock(&m2);
   pthread_mutex_unlock(&m1);
 
-  pthread_mutex_lock(&m4); // TODO NODEADLOCK (thread joined)
-  pthread_mutex_lock(&m5); // TODO NODEADLOCK (thread joined)
+  pthread_mutex_lock(&m4); // NODEADLOCK (thread joined)
+  pthread_mutex_lock(&m5); // NODEADLOCK (thread joined)
   x = 2; // RACE!
   pthread_mutex_unlock(&m5);
   pthread_mutex_unlock(&m4);
@@ -49,8 +49,8 @@ int main() {
   pthread_create(&tid, NULL, thread, NULL);
 
   pthread_mutex_lock(&m1); // NODEADLOCK
-  pthread_mutex_lock(&m3); // TODO NODEADLOCK (common m1)
-  pthread_mutex_lock(&m2); // TODO NODEADLOCK (common m1)
+  pthread_mutex_lock(&m3); // NODEADLOCK (common m1)
+  pthread_mutex_lock(&m2); // NODEADLOCK (common m1)
   func1();
   pthread_mutex_unlock(&m2);
   pthread_mutex_unlock(&m3);

From b4d7b0f1cd0237e84220b3e7dcdc91c8f94219d4 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 22 Mar 2022 11:47:27 +0200
Subject: [PATCH 23/31] Add access information to deadlock warnings

---
 src/analyses/deadlock.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml
index 16bc0376db..8ac8d0f96e 100644
--- a/src/analyses/deadlock.ml
+++ b/src/analyses/deadlock.ml
@@ -87,10 +87,10 @@ struct
             let (mini, _) = List.findi (fun i x -> LockEventPair.equal min x) path_visited_lock_event_pairs in
             let (init, tail) = List.split_at mini path_visited_lock_event_pairs in
             let normalized = List.rev_append init (List.rev tail) in (* backwards to get correct printout order *)
-            let msgs = List.concat_map (fun ((before_lock, before_node, _), (after_lock, after_node, _)) ->
+            let msgs = List.concat_map (fun ((before_lock, before_node, before_access), (after_lock, after_node, after_access)) ->
                 [
-                  (Pretty.dprintf "lock before: %a" Lock.pretty before_lock, Some (UpdateCil.getLoc before_node));
-                  (Pretty.dprintf "lock after: %a" Lock.pretty after_lock, Some (UpdateCil.getLoc after_node));
+                  (Pretty.dprintf "lock before: %a with %a" Lock.pretty before_lock MCPAccess.A.pretty before_access, Some (UpdateCil.getLoc before_node));
+                  (Pretty.dprintf "lock after: %a with %a" Lock.pretty after_lock MCPAccess.A.pretty after_access, Some (UpdateCil.getLoc after_node));
                 ]
               ) normalized
             in

From 6fa2ac256ebe72dca7802a963e81a11b292d7351 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Tue, 22 Mar 2022 12:06:00 +0200
Subject: [PATCH 24/31] Refactor MCPSpec.access argument to be variant

This is better than the special meaning of unknown_exp
---
 src/analyses/accessAnalysis.ml |  2 +-
 src/analyses/deadlock.ml       |  2 +-
 src/analyses/mCP.ml            |  8 ++++----
 src/analyses/mHPAnalysis.ml    |  2 +-
 src/analyses/mutexAnalysis.ml  |  8 +++++---
 src/analyses/region.ml         |  8 ++++----
 src/analyses/symbLocks.ml      |  7 ++++---
 src/analyses/threadFlag.ml     |  2 +-
 src/analyses/threadId.ml       |  2 +-
 src/domains/queries.ml         | 12 ++++++++----
 src/framework/analyses.ml      |  4 ++--
 11 files changed, 32 insertions(+), 25 deletions(-)

diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml
index 7514b80b6c..fc178d43cb 100644
--- a/src/analyses/accessAnalysis.ml
+++ b/src/analyses/accessAnalysis.ml
@@ -48,7 +48,7 @@ struct
     let part_access ctx (e:exp) (vo:varinfo option) (w: bool): MCPAccess.A.t =
       ctx.emit (Access {var_opt=vo; write=w});
       (*partitions & locks*)
-      Obj.obj (ctx.ask (PartAccess {exp=e; var_opt=vo; write=w}))
+      Obj.obj (ctx.ask (PartAccess (Memory {exp=e; var_opt=vo; write=w})))
     in
     let add_access conf vo oo =
       let a = part_access ctx e vo w in
diff --git a/src/analyses/deadlock.ml b/src/analyses/deadlock.ml
index 8ac8d0f96e..575aa14a55 100644
--- a/src/analyses/deadlock.ml
+++ b/src/analyses/deadlock.ml
@@ -38,7 +38,7 @@ struct
   let exitstate  _ : D.t = D.empty ()
 
   let part_access ctx: MCPAccess.A.t =
-    Obj.obj (ctx.ask (PartAccess {exp=MyCFG.unknown_exp; var_opt=None; write=false}))
+    Obj.obj (ctx.ask (PartAccess Point))
 
   let event ctx (e: Events.t) octx =
     match e with
diff --git a/src/analyses/mCP.ml b/src/analyses/mCP.ml
index 8d5638be5b..b6f15a7dde 100644
--- a/src/analyses/mCP.ml
+++ b/src/analyses/mCP.ml
@@ -275,8 +275,8 @@ struct
           (* WarnGlobal is special: it only goes to corresponding analysis and the argument variant is unlifted for it *)
           let (n, g): V.t = Obj.obj g in
           f ~q:(WarnGlobal (Obj.repr g)) (Result.top ()) (n, spec n, assoc n ctx.local)
-        | Queries.PartAccess {exp; var_opt; write} ->
-          Obj.repr (access ctx exp var_opt write)
+        | Queries.PartAccess a ->
+          Obj.repr (access ctx a)
         (* | EvalInt e ->
            (* TODO: only query others that actually respond to EvalInt *)
            (* 2x speed difference on SV-COMP nla-digbench-scaling/ps6-ll_valuebound5.c *)
@@ -291,11 +291,11 @@ struct
     let querycache = QueryHash.create 13 in
     query' ~querycache QuerySet.empty ctx q
 
-  and access (ctx:(D.t, G.t, C.t, V.t) ctx) e vo w: MCPAccess.A.t =
+  and access (ctx:(D.t, G.t, C.t, V.t) ctx) a: MCPAccess.A.t =
     let ctx'' = outer_ctx "access" ctx in
     let f (n, (module S: MCPSpec), d) =
       let ctx' : (S.D.t, S.G.t, S.C.t, S.V.t) ctx = inner_ctx "access" ctx'' n d in
-      (n, repr (S.access ctx' e vo w))
+      (n, repr (S.access ctx' a))
     in
     BatList.map f (spec_list ctx.local) (* map without deadcode *)
 
diff --git a/src/analyses/mHPAnalysis.ml b/src/analyses/mHPAnalysis.ml
index 0331057bc7..4a3af12a79 100644
--- a/src/analyses/mHPAnalysis.ml
+++ b/src/analyses/mHPAnalysis.ml
@@ -14,7 +14,7 @@ struct
     let should_print _ = true
   end
 
-  let access ctx e vo w: MHP.t =
+  let access ctx _: MHP.t =
     {
       tid = ctx.ask CurrentThreadId;
       created = ctx.ask CreatedThreads;
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index 3c836d0ed6..e2cf12540e 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -162,11 +162,13 @@ struct
     let should_print ls = not (is_empty ls)
   end
 
-  let access ctx e vo w =
-    if e = MyCFG.unknown_exp || w then
+  let access ctx (a: Queries.access) =
+    match a with
+    | Point
+    | Memory {write = true; _} ->
       (* when writing: ignore reader locks *)
       Lockset.filter snd ctx.local
-    else
+    | Memory _ ->
       (* when reading: bump reader locks to exclusive as they protect reads *)
       Lockset.map (fun (x,_) -> (x,true)) ctx.local
 
diff --git a/src/analyses/region.ml b/src/analyses/region.ml
index d5e6e9818a..01ba3ebf96 100644
--- a/src/analyses/region.ml
+++ b/src/analyses/region.ml
@@ -69,10 +69,11 @@ struct
       | Some r when Lvals.is_empty r -> false
       | _ -> true
   end
-  let access ctx e vo w =
-    if e = MyCFG.unknown_exp then
+  let access ctx (a: Queries.access) =
+    match a with
+    | Point ->
       Some (Lvals.empty ())
-    else (
+    | Memory {exp = e; _} ->
       (* TODO: remove regions that cannot be reached from the var*)
       let rec unknown_index = function
         | `NoOffset -> `NoOffset
@@ -80,7 +81,6 @@ struct
         | `Index (i, os) -> `Index (MyCFG.unknown_exp, unknown_index os) (* forget specific indices *)
       in
       Option.map (Lvals.of_list % List.map (Tuple2.map2 unknown_index)) (get_region ctx e)
-    )
 
   (* transfer functions *)
   let assign ctx (lval:lval) (rval:exp) : D.t =
diff --git a/src/analyses/symbLocks.ml b/src/analyses/symbLocks.ml
index 07616a2f2c..f64db691f9 100644
--- a/src/analyses/symbLocks.ml
+++ b/src/analyses/symbLocks.ml
@@ -218,10 +218,11 @@ struct
     let may_race lp lp2 = is_empty @@ inter lp lp2
     let should_print lp = not (is_empty lp)
   end
-  let access ctx e vo w =
-    if e = MyCFG.unknown_exp then
+  let access ctx (a: Queries.access) =
+    match a with
+    | Point ->
       A.empty ()
-    else
+    | Memory {exp = e; _} ->
       add_per_element_access ctx e false
 end
 
diff --git a/src/analyses/threadFlag.ml b/src/analyses/threadFlag.ml
index 2f92d55d43..75b80d50a5 100644
--- a/src/analyses/threadFlag.ml
+++ b/src/analyses/threadFlag.ml
@@ -72,7 +72,7 @@ struct
     let may_race m1 m2 = m1 && m2 (* kill access when single threaded *)
     let should_print m = not m
   end
-  let access ctx e vo w =
+  let access ctx _ =
     is_multi (Analyses.ask_of_ctx ctx)
 
   let threadenter ctx lval f args =
diff --git a/src/analyses/threadId.ml b/src/analyses/threadId.ml
index aa0947e62b..00ddc5d6bc 100644
--- a/src/analyses/threadId.ml
+++ b/src/analyses/threadId.ml
@@ -104,7 +104,7 @@ struct
     let should_print = Option.is_some
   end
 
-  let access ctx e vo w =
+  let access ctx _ =
     if is_unique ctx then
       let tid = fst ctx.local in
       Some tid
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index 1dc44b3002..79cdefe96c 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -59,7 +59,11 @@ module Unit = Lattice.Unit
 type maybepublic = {global: CilType.Varinfo.t; write: bool} [@@deriving ord, hash]
 type maybepublicwithout = {global: CilType.Varinfo.t; write: bool; without_mutex: PreValueDomain.Addr.t} [@@deriving ord, hash]
 type mustbeprotectedby = {mutex: PreValueDomain.Addr.t; global: CilType.Varinfo.t; write: bool} [@@deriving ord, hash]
-type partaccess = {exp: CilType.Exp.t; var_opt: CilType.Varinfo.t option; write: bool} [@@deriving ord, hash]
+type memory_access = {exp: CilType.Exp.t; var_opt: CilType.Varinfo.t option; write: bool} [@@deriving ord, hash]
+type access =
+  | Memory of memory_access (** Memory location access (race). *)
+  | Point (** Program point and state access (MHP), independent of memory location. *)
+[@@deriving ord, hash] (* TODO: fix ppx_deriving_hash on variant with inline record *)
 
 (** GADT for queries with specific result type. *)
 type _ t =
@@ -86,7 +90,7 @@ type _ t =
   | BlobSize: exp -> ID.t t (* size of a dynamically allocated `Blob pointed to by exp *)
   | PrintFullState: Unit.t t
   | CondVars: exp -> ES.t t
-  | PartAccess: partaccess -> Obj.t t (** Only queried by access analysis. [Obj.t] represents [MCPAccess.A.t], needed to break dependency cycle. *)
+  | PartAccess: access -> Obj.t t (** Only queried by access and deadlock analysis. [Obj.t] represents [MCPAccess.A.t], needed to break dependency cycle. *)
   | IterPrevVars: iterprevvar -> Unit.t t
   | IterVars: itervar -> Unit.t t
   | MustBeEqual: exp * exp -> MustBool.t t (* are two expression known to must-equal ? *)
@@ -273,7 +277,7 @@ struct
       | Any (EvalLength e1), Any (EvalLength e2) -> CilType.Exp.compare e1 e2
       | Any (BlobSize e1), Any (BlobSize e2) -> CilType.Exp.compare e1 e2
       | Any (CondVars e1), Any (CondVars e2) -> CilType.Exp.compare e1 e2
-      | Any (PartAccess p1), Any (PartAccess p2) -> compare_partaccess p1 p2
+      | Any (PartAccess p1), Any (PartAccess p2) -> compare_access p1 p2
       | Any (IterPrevVars ip1), Any (IterPrevVars ip2) -> compare_iterprevvar ip1 ip2
       | Any (IterVars i1), Any (IterVars i2) -> compare_itervar i1 i2
       | Any (MustBeEqual (e1, e2)), Any (MustBeEqual (e3, e4)) ->
@@ -308,7 +312,7 @@ struct
     | Any (EvalLength e) -> CilType.Exp.hash e
     | Any (BlobSize e) -> CilType.Exp.hash e
     | Any (CondVars e) -> CilType.Exp.hash e
-    | Any (PartAccess p) -> hash_partaccess p
+    | Any (PartAccess p) -> hash_access p
     | Any (IterPrevVars i) -> 0
     | Any (IterVars i) -> 0
     | Any (MustBeEqual (e1, e2)) -> [%hash: CilType.Exp.t * CilType.Exp.t] (e1, e2)
diff --git a/src/framework/analyses.ml b/src/framework/analyses.ml
index d6244d60e1..f7b4e40efd 100644
--- a/src/framework/analyses.ml
+++ b/src/framework/analyses.ml
@@ -391,7 +391,7 @@ sig
   val event : (D.t, G.t, C.t, V.t) ctx -> Events.t -> (D.t, G.t, C.t, V.t) ctx -> D.t
 
   module A: MCPA
-  val access: (D.t, G.t, C.t, V.t) ctx -> exp -> varinfo option -> bool -> A.t
+  val access: (D.t, G.t, C.t, V.t) ctx -> Queries.access -> A.t
 end
 
 type analyzed_data = {
@@ -569,7 +569,7 @@ struct
   (* Everything is context sensitive --- override in MCP and maybe elsewhere*)
 
   module A = UnitA
-  let access _ _ _ _ = ()
+  let access _ _ = ()
 end
 
 (* Even more default implementations. Most transfer functions acting as identity functions. *)

From 123e0cbac6f56a671fcd42c5c3655c36f1982893 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Fri, 25 Mar 2022 13:55:54 +0100
Subject: [PATCH 25/31] Additional MHP criterion

---
 src/cdomains/mHP.ml | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/cdomains/mHP.ml b/src/cdomains/mHP.ml
index 86e7676097..9b4d773a3c 100644
--- a/src/cdomains/mHP.ml
+++ b/src/cdomains/mHP.ml
@@ -45,6 +45,12 @@ let definitely_not_started (current, created) other =
     else
       not @@ ConcDomain.ThreadSet.exists (ident_or_may_be_created) created
 
+let exists_definitely_not_started_in_joined (current,created) other_joined =
+  if ConcDomain.ThreadSet.is_top other_joined then
+    false
+  else
+    ConcDomain.ThreadSet.exists (definitely_not_started (current,created)) other_joined
+
 (** Must the thread with thread id other be already joined  *)
 let must_be_joined other joined =
   if ConcDomain.ThreadSet.is_top joined then
@@ -64,6 +70,8 @@ let may_happen_in_parallel one two =
       false
     else if must_be_joined tid2 must_joined || must_be_joined tid must_joined2 then
       false
+    else if exists_definitely_not_started_in_joined (tid,created) must_joined2 || exists_definitely_not_started_in_joined (tid2,created2) must_joined then
+      false
     else
       true
   | _ -> true

From 68d6d5bfbd6fbad3dedfb05ff9e63e48462c2f39 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Fri, 25 Mar 2022 13:56:21 +0100
Subject: [PATCH 26/31] Two sophisticated examples

---
 .../regression/15-deadlock/13-deadlock-mhp.c  | 36 ++++++++++
 .../regression/15-deadlock/15-deadlock-mhp2.c | 66 +++++++++++++++++++
 2 files changed, 102 insertions(+)
 create mode 100644 tests/regression/15-deadlock/13-deadlock-mhp.c
 create mode 100644 tests/regression/15-deadlock/15-deadlock-mhp2.c

diff --git a/tests/regression/15-deadlock/13-deadlock-mhp.c b/tests/regression/15-deadlock/13-deadlock-mhp.c
new file mode 100644
index 0000000000..7cc3be7ec7
--- /dev/null
+++ b/tests/regression/15-deadlock/13-deadlock-mhp.c
@@ -0,0 +1,36 @@
+// PARAM: --set ana.activated[+] deadlock --set ana.activated[+] threadJoins
+// From https://arxiv.org/abs/1607.06927
+#include <pthread.h>
+
+int x;
+pthread_mutex_t m1 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t m2 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t m3 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t m4 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t m5 = PTHREAD_MUTEX_INITIALIZER;
+
+void *thread() {
+  pthread_mutex_lock(&m2); //DEADLOCK
+  pthread_mutex_lock(&m1); //DEADLOCK
+  pthread_mutex_unlock(&m2);
+  pthread_mutex_unlock(&m1);
+
+  return NULL;
+}
+
+void *noOpThread() {
+  return NULL;
+}
+
+int main() {
+  pthread_t tid1;
+  pthread_t tid2;
+
+  pthread_create(&tid1, NULL, noOpThread, NULL);
+
+  pthread_mutex_lock(&m1);
+  pthread_create(&tid2, NULL, thread, NULL);
+  pthread_mutex_lock(&m2); //DEADLOCK
+
+  return 0;
+}
diff --git a/tests/regression/15-deadlock/15-deadlock-mhp2.c b/tests/regression/15-deadlock/15-deadlock-mhp2.c
new file mode 100644
index 0000000000..dcca675bad
--- /dev/null
+++ b/tests/regression/15-deadlock/15-deadlock-mhp2.c
@@ -0,0 +1,66 @@
+// PARAM: --set ana.activated[+] deadlock --set ana.activated[+] threadJoins
+#include <pthread.h>
+
+int x;
+pthread_mutex_t m1 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t m2 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t m3 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t m4 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t m5 = PTHREAD_MUTEX_INITIALIZER;
+pthread_t decoy;
+
+
+void *noOpThread() {
+  return NULL;
+}
+
+void *thread2() {
+  pthread_mutex_lock(&m3);
+  pthread_mutex_lock(&m1);
+
+  pthread_mutex_unlock(&m3);
+  pthread_mutex_unlock(&m1);
+
+  return NULL;
+}
+
+void *thread() {
+  pthread_mutex_lock(&m2);
+  pthread_mutex_lock(&m3);
+
+  pthread_mutex_lock(&m5);
+  pthread_create(&decoy, NULL, noOpThread, NULL);
+  pthread_mutex_unlock(&m5);
+
+
+  pthread_mutex_unlock(&m3);
+  pthread_mutex_unlock(&m2);
+
+  return NULL;
+}
+
+int main() {
+  pthread_t tid1;
+  pthread_t tid2;
+
+  pthread_create(&tid1, NULL, thread, NULL);
+  pthread_create(&tid2, NULL, thread2, NULL);
+
+  pthread_mutex_lock(&m1);
+
+  pthread_mutex_lock(&m5);
+  pthread_t dec = decoy;
+  pthread_mutex_unlock(&m5);
+
+  if(dec != NULL) {
+    pthread_join(dec,NULL);
+    pthread_mutex_lock(&m2);
+
+    pthread_mutex_unlock(&m1);
+    pthread_mutex_unlock(&m2);
+  } else {
+    pthread_mutex_unlock(&m1);
+  }
+
+  return 0;
+}

From 3124e376b93054e742b6cd302e5c71bf8ccf2949 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Fri, 25 Mar 2022 13:56:57 +0100
Subject: [PATCH 27/31] Add problematic example with missed must deadlock

---
 .../15-deadlock/14-missing-unlock.c           | 36 +++++++++++++++++++
 1 file changed, 36 insertions(+)
 create mode 100644 tests/regression/15-deadlock/14-missing-unlock.c

diff --git a/tests/regression/15-deadlock/14-missing-unlock.c b/tests/regression/15-deadlock/14-missing-unlock.c
new file mode 100644
index 0000000000..9b2152cc77
--- /dev/null
+++ b/tests/regression/15-deadlock/14-missing-unlock.c
@@ -0,0 +1,36 @@
+// PARAM: --set ana.activated[+] deadlock --set ana.activated[+] threadJoins
+#include <pthread.h>
+
+int x;
+pthread_mutex_t m1 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t m2 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t m3 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t m4 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t m5 = PTHREAD_MUTEX_INITIALIZER;
+
+void *thread() {
+  pthread_mutex_lock(&m2);
+  pthread_mutex_lock(&m1);
+  // We forgot to unlock
+  // pthread_mutex_unlock(&m2);
+  pthread_mutex_unlock(&m1);
+
+  return NULL;
+}
+
+void *noOpThread() {
+  return NULL;
+}
+
+int main() {
+  pthread_t tid1;
+  pthread_t tid2;
+
+  pthread_create(&tid1, NULL, noOpThread, NULL);
+
+  pthread_create(&tid2, NULL, thread, NULL);
+  pthread_join(tid2,NULL);
+  pthread_mutex_lock(&m2); //DEADLOCK
+
+  return 0;
+}

From 0af55e0c96f5a1fdf906d9e995bafa05612ebef1 Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Fri, 25 Mar 2022 14:06:50 +0100
Subject: [PATCH 28/31] Rm wrong comment

---
 tests/regression/15-deadlock/13-deadlock-mhp.c | 1 -
 1 file changed, 1 deletion(-)

diff --git a/tests/regression/15-deadlock/13-deadlock-mhp.c b/tests/regression/15-deadlock/13-deadlock-mhp.c
index 7cc3be7ec7..aaad11f611 100644
--- a/tests/regression/15-deadlock/13-deadlock-mhp.c
+++ b/tests/regression/15-deadlock/13-deadlock-mhp.c
@@ -1,5 +1,4 @@
 // PARAM: --set ana.activated[+] deadlock --set ana.activated[+] threadJoins
-// From https://arxiv.org/abs/1607.06927
 #include <pthread.h>
 
 int x;

From 4fa94b70a09f2b3a711aecab02c9dfd76213afe3 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 25 Mar 2022 17:29:18 +0200
Subject: [PATCH 29/31] Skip 15-deadlock/14-missing-unlock

---
 tests/regression/15-deadlock/14-missing-unlock.c | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/tests/regression/15-deadlock/14-missing-unlock.c b/tests/regression/15-deadlock/14-missing-unlock.c
index 9b2152cc77..2454c06ab7 100644
--- a/tests/regression/15-deadlock/14-missing-unlock.c
+++ b/tests/regression/15-deadlock/14-missing-unlock.c
@@ -1,4 +1,5 @@
-// PARAM: --set ana.activated[+] deadlock --set ana.activated[+] threadJoins
+// SKIP PARAM: --set ana.activated[+] deadlock --set ana.activated[+] threadJoins
+// TODO: https://github.com/goblint/analyzer/issues/667
 #include <pthread.h>
 
 int x;
@@ -30,7 +31,7 @@ int main() {
 
   pthread_create(&tid2, NULL, thread, NULL);
   pthread_join(tid2,NULL);
-  pthread_mutex_lock(&m2); //DEADLOCK
+  pthread_mutex_lock(&m2); // TODO DEADLOCK
 
   return 0;
 }

From 1f737fd62f2edb1194b560e5abba5694f6764e93 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 25 Mar 2022 17:41:11 +0200
Subject: [PATCH 30/31] Clean up and fully annotate mhp deadlock tests

---
 .../regression/15-deadlock/13-deadlock-mhp.c  |  6 +----
 .../regression/15-deadlock/15-deadlock-mhp2.c | 22 +++++++++----------
 2 files changed, 11 insertions(+), 17 deletions(-)

diff --git a/tests/regression/15-deadlock/13-deadlock-mhp.c b/tests/regression/15-deadlock/13-deadlock-mhp.c
index aaad11f611..c31a174863 100644
--- a/tests/regression/15-deadlock/13-deadlock-mhp.c
+++ b/tests/regression/15-deadlock/13-deadlock-mhp.c
@@ -1,12 +1,8 @@
 // PARAM: --set ana.activated[+] deadlock --set ana.activated[+] threadJoins
 #include <pthread.h>
 
-int x;
 pthread_mutex_t m1 = PTHREAD_MUTEX_INITIALIZER;
 pthread_mutex_t m2 = PTHREAD_MUTEX_INITIALIZER;
-pthread_mutex_t m3 = PTHREAD_MUTEX_INITIALIZER;
-pthread_mutex_t m4 = PTHREAD_MUTEX_INITIALIZER;
-pthread_mutex_t m5 = PTHREAD_MUTEX_INITIALIZER;
 
 void *thread() {
   pthread_mutex_lock(&m2); //DEADLOCK
@@ -27,7 +23,7 @@ int main() {
 
   pthread_create(&tid1, NULL, noOpThread, NULL);
 
-  pthread_mutex_lock(&m1);
+  pthread_mutex_lock(&m1); // DEADLOCK
   pthread_create(&tid2, NULL, thread, NULL);
   pthread_mutex_lock(&m2); //DEADLOCK
 
diff --git a/tests/regression/15-deadlock/15-deadlock-mhp2.c b/tests/regression/15-deadlock/15-deadlock-mhp2.c
index dcca675bad..5ef912400c 100644
--- a/tests/regression/15-deadlock/15-deadlock-mhp2.c
+++ b/tests/regression/15-deadlock/15-deadlock-mhp2.c
@@ -1,12 +1,10 @@
 // PARAM: --set ana.activated[+] deadlock --set ana.activated[+] threadJoins
 #include <pthread.h>
 
-int x;
 pthread_mutex_t m1 = PTHREAD_MUTEX_INITIALIZER;
 pthread_mutex_t m2 = PTHREAD_MUTEX_INITIALIZER;
 pthread_mutex_t m3 = PTHREAD_MUTEX_INITIALIZER;
 pthread_mutex_t m4 = PTHREAD_MUTEX_INITIALIZER;
-pthread_mutex_t m5 = PTHREAD_MUTEX_INITIALIZER;
 pthread_t decoy;
 
 
@@ -15,8 +13,8 @@ void *noOpThread() {
 }
 
 void *thread2() {
-  pthread_mutex_lock(&m3);
-  pthread_mutex_lock(&m1);
+  pthread_mutex_lock(&m3); // NODEADLOCK (decoy not yet created)
+  pthread_mutex_lock(&m1); // NODEADLOCK (decoy not yet created)
 
   pthread_mutex_unlock(&m3);
   pthread_mutex_unlock(&m1);
@@ -25,12 +23,12 @@ void *thread2() {
 }
 
 void *thread() {
-  pthread_mutex_lock(&m2);
-  pthread_mutex_lock(&m3);
+  pthread_mutex_lock(&m2); // NODEADLOCK (decoy not yet created)
+  pthread_mutex_lock(&m3); // NODEADLOCK (decoy not yet created)
 
-  pthread_mutex_lock(&m5);
+  pthread_mutex_lock(&m4); // NODEADLOCK (not in cycle)
   pthread_create(&decoy, NULL, noOpThread, NULL);
-  pthread_mutex_unlock(&m5);
+  pthread_mutex_unlock(&m4);
 
 
   pthread_mutex_unlock(&m3);
@@ -46,15 +44,15 @@ int main() {
   pthread_create(&tid1, NULL, thread, NULL);
   pthread_create(&tid2, NULL, thread2, NULL);
 
-  pthread_mutex_lock(&m1);
+  pthread_mutex_lock(&m1); // NODEADLOCK (decoy not yet created)
 
-  pthread_mutex_lock(&m5);
+  pthread_mutex_lock(&m4); // NODEADLOCK (not in cycle)
   pthread_t dec = decoy;
-  pthread_mutex_unlock(&m5);
+  pthread_mutex_unlock(&m4);
 
   if(dec != NULL) {
     pthread_join(dec,NULL);
-    pthread_mutex_lock(&m2);
+    pthread_mutex_lock(&m2); // NODEADLOCK (decoy not yet created)
 
     pthread_mutex_unlock(&m1);
     pthread_mutex_unlock(&m2);

From 3d724f8d54606db004aed9c4e410368eff89413e Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 25 Mar 2022 18:49:16 +0200
Subject: [PATCH 31/31] Remove unused globals from
 15-deadlock/14-missing-unlock

---
 tests/regression/15-deadlock/14-missing-unlock.c | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/tests/regression/15-deadlock/14-missing-unlock.c b/tests/regression/15-deadlock/14-missing-unlock.c
index 2454c06ab7..6381da08c5 100644
--- a/tests/regression/15-deadlock/14-missing-unlock.c
+++ b/tests/regression/15-deadlock/14-missing-unlock.c
@@ -2,12 +2,8 @@
 // TODO: https://github.com/goblint/analyzer/issues/667
 #include <pthread.h>
 
-int x;
 pthread_mutex_t m1 = PTHREAD_MUTEX_INITIALIZER;
 pthread_mutex_t m2 = PTHREAD_MUTEX_INITIALIZER;
-pthread_mutex_t m3 = PTHREAD_MUTEX_INITIALIZER;
-pthread_mutex_t m4 = PTHREAD_MUTEX_INITIALIZER;
-pthread_mutex_t m5 = PTHREAD_MUTEX_INITIALIZER;
 
 void *thread() {
   pthread_mutex_lock(&m2);