Reimplement deadlock analysis and extend with MHP

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"

src/analyses/deadlock.ml

@@ -4,109 +4,94 @@ open Prelude.Ana
 open Analyses
 open DeadlockDomain
 
-let forbiddenList : ( (myowntypeEntry*myowntypeEntry) list ref) = ref []
-
 module Spec =
 struct
-  include Analyses.DefaultSpec
+  include Analyses.IdentitySpec
 
   let name () = "deadlock"
 
-  (* The domain for the analysis *)
-  module D = DeadlockDomain.Lockset (* MayLockset *)
-  module C = DeadlockDomain.Lockset
-
-  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
+  module D = MayLockEvents
+  module C = D
+  module V = Lock
+
+  module LockEventPair = Printable.Prod (LockEvent) (LockEvent)
+  module MayLockEventPairs = SetDomain.Make (LockEventPair)
+  module G =
+  struct
+    include MapDomain.MapBot (Lock) (MayLockEventPairs)
+    let leq x y = !GU.postsolving || leq x y (* HACK: to pass verify*)
+  end
+
+  let side_lock_event_pair ctx before after =
+    let d =
+      if !GU.should_warn then
+        G.singleton (fst after) (MayLockEventPairs.singleton (before, after))
+      else
+        G.bot () (* HACK: just to pass validation with MCP DomVariantLattice *)
     in
-
-    (* Check forbidden list *)
-    if !Goblintutil.postsolving then begin
-      D.iter (fun e -> List.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;
-
-      (* 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
-      ) lockList
-    end
+    ctx.sideg (fst before) d
 
 
   (* 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
-    | `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 {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 ->
+      let after = (addr, ctx.prev_node) 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
+    | _ ->
+      ctx.local
+
+  let query ctx (type a) (q: a Queries.t): a Queries.result =
+    match q with
+    | WarnGlobal g ->
+      let g: V.t = Obj.obj g in
+
+      let module LH = Hashtbl.Make (Lock) in
+      let module LS = Set.Make (Lock) in
+      (* TODO: find all cycles/SCCs *)
+      let global_visited_locks = LH.create 100 in
+
+      (* DFS *)
+      let rec iter_lock (path_visited_locks: LS.t) (path_visited_lock_event_pairs: LockEventPair.t list) (lock: Lock.t) =
+        if LS.mem lock path_visited_locks then (
+          (* 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 ();
+          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
+
+      Stats.time "deadlock" (iter_lock LS.empty []) g
+    | _ -> Queries.Result.top q
 end
 
 let _ =

src/cdomains/deadlockDomain.ml

@@ -1,24 +1,7 @@
 open Cil
 open Pretty
 
-type myowntypeEntry = {addr : ValueDomain.Addr.t ; loc : location}
+module Lock = LockDomain.Addr
+module LockEvent = Printable.Prod (Lock) (Node)
 
-
-module MyLock : Printable.S with type t = myowntypeEntry =
-struct
-  include Printable.Std (* for default invariant, tag, ... *)
-
-  type t = myowntypeEntry
-  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 Lockset = SetDomain.ToppedSet (MyLock) (struct let topname = "all locks" end)
+module MayLockEvents = SetDomain.ToppedSet (LockEvent) (struct let topname = "All lock events" end)

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

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",

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);

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);

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);

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);

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);