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/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

src/analyses/deadlock.ml

@@ -4,110 +4,114 @@ 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 (Tuple3.first 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 (Tuple3.first 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 part_access ctx: MCPAccess.A.t =
+    Obj.obj (ctx.ask (PartAccess Point))
+
+  let event ctx (e: Events.t) octx =
+    match e with
+    | Lock addr ->
+      let after = (addr, ctx.prev_node, part_access octx) in (* use octx for access to use locksets before event *)
+      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 (
+          (* 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
+          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
+          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, before_access), (after_lock, after_node, after_access)) ->
+                [
+                  (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
+            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 _ =
-  MCP.register_analysis (module Spec : MCPSpec)
+  MCP.register_analysis ~dep:["mutex"] (module Spec : MCPSpec)

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

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;

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

src/analyses/region.ml

@@ -69,14 +69,18 @@ struct
       | Some r when Lvals.is_empty r -> false
       | _ -> 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)
+  let access ctx (a: Queries.access) =
+    match a with
+    | Point ->
+      Some (Lvals.empty ())
+    | Memory {exp = e; _} ->
+      (* 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 =

src/analyses/symbLocks.ml

@@ -218,8 +218,12 @@ 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 =
-    add_per_element_access ctx e false
+  let access ctx (a: Queries.access) =
+    match a with
+    | Point ->
+      A.empty ()
+    | Memory {exp = e; _} ->
+      add_per_element_access ctx e false
 end
 
 let _ =

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 =

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

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.Prod3 (Lock) (Node) (MCPAccess.A)
 
-
-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/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