[deadlock] analysis and reporting

Reviewed By: sblackshear

Differential Revision: D7215066

fbshipit-source-id: 8cf5e77

infer/src/absint/AbstractDomain.ml

@@ -331,3 +331,47 @@ module CountDomain (MaxCount : MaxCount) = struct
 
   let pp = Int.pp
 end
+
+module StackDomain (Element : PrettyPrintable.PrintableOrderedType) = struct
+  type astate = Element.t list
+
+  let push = List.cons
+
+  let pop = List.tl_exn
+
+  let is_empty = List.is_empty
+
+  let empty = []
+
+  let pp fmt x = Pp.semicolon_seq Element.pp fmt x
+
+  (* is (rev rhs) a prefix of (rev lhs)? *)
+  let ( <= ) ~lhs ~rhs =
+    let rec aux lhs rhs =
+      match (lhs, rhs) with
+      | _, [] ->
+          true
+      | [], _ ->
+          false
+      | x :: _, y :: _ when not (Int.equal 0 (Element.compare x y)) ->
+          false
+      | _ :: xs, _ :: ys ->
+          aux xs ys
+    in
+    phys_equal lhs rhs || aux (List.rev lhs) (List.rev rhs)
+
+
+  (* compute (rev (longest common prefix)) *)
+  let join lhs rhs =
+    let rec aux acc a b =
+      match (a, b) with
+      | x :: xs, y :: ys when Int.equal 0 (Element.compare x y) ->
+          aux (x :: acc) xs ys
+      | _, _ ->
+          acc
+    in
+    if phys_equal lhs rhs then lhs else aux [] (List.rev lhs) (List.rev rhs)
+
+
+  let widen ~prev ~next ~num_iters:_ = join prev next
+end

infer/src/absint/AbstractDomain.mli

@@ -134,3 +134,20 @@ module CountDomain (MaxCount : MaxCount) : sig
   val add : astate -> astate -> astate
   (** capped sum of two states *)
 end
+
+(** Domain whose members are stacks of elements (lists, last pushed is head of the list),
+    partially ordered by the prefix relation ([c;b;a] <= [b;a]), and whose join computes the
+    longest common prefix (so [c;b;a] join [f;g;b;c;a] = [a]), so the top element is the empty
+    stack. *)
+module StackDomain (Element : PrettyPrintable.PrintableOrderedType) : sig
+  include S with type astate = Element.t list
+
+  val push : Element.t -> astate -> astate
+
+  val pop : astate -> astate
+  (** throws exception on empty *)
+
+  val empty : astate
+
+  val is_empty : astate -> bool
+end

infer/src/concurrency/deadlock.ml

@@ -11,4 +11,168 @@ module F = Format
 module L = Logging
 module MF = MarkupFormatter
 
-let analyze_procedure {Callbacks.summary} = summary
+let debug fmt = F.kasprintf L.d_strln fmt
+
+module Summary = Summary.Make (struct
+  type payload = DeadlockDomain.summary
+
+  let update_payload post (summary: Specs.summary) =
+    {summary with payload= {summary.payload with deadlock= Some post}}
+
+
+  let read_payload (summary: Specs.summary) = summary.payload.deadlock
+end)
+
+module TransferFunctions (CFG : ProcCfg.S) = struct
+  module CFG = CFG
+  module Domain = DeadlockDomain
+
+  type extras = ProcData.no_extras
+
+  let exec_instr (astate: Domain.astate) {ProcData.pdesc} _ (instr: HilInstr.t) =
+    let open RacerDConfig in
+    let get_path actuals =
+      List.hd actuals |> Option.value_map ~default:[] ~f:HilExp.get_access_exprs |> List.hd
+      |> Option.map ~f:AccessExpression.to_access_path
+    in
+    match instr with
+    | Call (_, Direct callee_pname, actuals, _, loc) -> (
+      match Models.get_lock callee_pname actuals with
+      | Lock ->
+          get_path actuals
+          |> Option.value_map ~default:astate ~f:(fun path -> Domain.acquire path astate loc)
+      | Unlock ->
+          get_path actuals
+          |> Option.value_map ~default:astate ~f:(fun path -> Domain.release path astate)
+      | LockedIfTrue ->
+          astate
+      | NoEffect ->
+          Summary.read_summary pdesc callee_pname
+          |> Option.value_map ~default:astate ~f:(fun callee_summary ->
+                 Domain.integrate_summary ~caller_state:astate ~callee_summary callee_pname loc ) )
+    | _ ->
+        astate
+end
+
+module Analyzer = LowerHil.MakeAbstractInterpreter (ProcCfg.Normal) (TransferFunctions)
+
+(* To allow on-demand reporting for deadlocks, we look for order pairs of the form (A,B)
+   where A belongs to the current class and B is potentially another class.  To avoid
+   quadratic/double reporting (ie when we actually analyse B), we allow the check
+   only if the current class is ordered greater or equal to the callee class.  *)
+let should_skip_during_deadlock_reporting _ _ = false
+
+(* currently short-circuited until non-determinism in reporting is dealt with *)
+(* Typ.Name.compare current_class eventually_class < 0 *)
+
+let get_class_of_pname = function
+  | Typ.Procname.Java java_pname ->
+      Some (Typ.Procname.Java.get_class_type_name java_pname)
+  | _ ->
+      None
+
+
+(* let false_if_none a ~f = Option.value_map a ~default:false ~f *)
+(* if same class, report only if the locks order in one of the possible ways *)
+let should_report_if_same_class _ = true
+
+(* currently short-circuited until non-determinism in reporting is dealt with *)
+(* DeadlockDomain.(
+    LockOrder.get_pair caller_elem
+    |> false_if_none ~f:(fun (b, a) ->
+           let b_class_opt, a_class_opt = (LockEvent.owner_class b, LockEvent.owner_class a) in
+           false_if_none b_class_opt ~f:(fun first_class ->
+               false_if_none a_class_opt ~f:(fun eventually_class ->
+                   not (Typ.Name.equal first_class eventually_class) || LockEvent.compare b a >= 0
+               ) ) )) *)
+
+let make_loc_trace pname trace_id start_loc elem =
+  let open DeadlockDomain in
+  let header = Printf.sprintf "[Trace %d]" trace_id in
+  let trace = LockOrder.make_loc_trace elem in
+  let first_step = List.hd_exn trace in
+  if Location.equal first_step.Errlog.lt_loc start_loc then
+    let trace_descr = header ^ " " ^ first_step.Errlog.lt_description in
+    Errlog.make_trace_element 0 start_loc trace_descr [] :: List.tl_exn trace
+  else
+    let trace_descr = Format.asprintf "%s Method start: %a" header Typ.Procname.pp pname in
+    Errlog.make_trace_element 0 start_loc trace_descr [] :: trace
+
+
+let get_summary caller_pdesc callee_pdesc =
+  Summary.read_summary caller_pdesc (Procdesc.get_proc_name callee_pdesc)
+  |> Option.map ~f:(fun summary -> (callee_pdesc, summary))
+
+
+let report_deadlocks get_proc_desc tenv pdesc summary =
+  let open DeadlockDomain in
+  let process_callee_elem caller_pdesc caller_elem callee_pdesc elem =
+    if LockOrder.may_deadlock caller_elem elem && should_report_if_same_class caller_elem then (
+      debug "Possible deadlock:@.%a@.%a@." LockOrder.pp caller_elem LockOrder.pp elem ;
+      let caller_loc = Procdesc.get_loc caller_pdesc in
+      let callee_loc = Procdesc.get_loc callee_pdesc in
+      let caller_pname = Procdesc.get_proc_name caller_pdesc in
+      let callee_pname = Procdesc.get_proc_name callee_pdesc in
+      let lock, lock' =
+        (caller_elem.LockOrder.eventually.LockEvent.lock, elem.LockOrder.eventually.LockEvent.lock)
+      in
+      let error_message =
+        Format.asprintf "Potential deadlock (%a ; %a)" LockIdentity.pp lock LockIdentity.pp lock'
+      in
+      let exn =
+        Exceptions.Checkers (IssueType.potential_deadlock, Localise.verbatim_desc error_message)
+      in
+      let first_trace = List.rev (make_loc_trace caller_pname 1 caller_loc caller_elem) in
+      let second_trace = make_loc_trace callee_pname 2 callee_loc elem in
+      let ltr = List.rev_append first_trace second_trace in
+      Specs.get_summary caller_pname
+      |> Option.iter ~f:(fun summary -> Reporting.log_error summary ~loc:caller_loc ~ltr exn) )
+  in
+  let report_pair current_class elem =
+    LockOrder.get_pair elem
+    |> Option.iter ~f:(fun (_, eventually) ->
+           LockEvent.owner_class eventually
+           |> Option.iter ~f:(fun eventually_class ->
+                  if should_skip_during_deadlock_reporting current_class eventually_class then ()
+                  else
+                    (* get the class of the root variable of the lock in the endpoint event
+                       and retrieve all the summaries of the methods of that class *)
+                    let class_of_eventual_lock =
+                      LockEvent.owner_class eventually |> Option.bind ~f:(Tenv.lookup tenv)
+                    in
+                    let methods =
+                      Option.value_map class_of_eventual_lock ~default:[] ~f:(fun tstruct ->
+                          tstruct.Typ.Struct.methods )
+                    in
+                    let proc_descs = List.rev_filter_map methods ~f:get_proc_desc in
+                    let summaries = List.rev_filter_map proc_descs ~f:(get_summary pdesc) in
+                    (* for each summary related to the endpoint, analyse and report on its pairs *)
+                    List.iter summaries ~f:(fun (callee_pdesc, summary) ->
+                        LockOrderDomain.iter (process_callee_elem pdesc elem callee_pdesc) summary
+                    ) ) )
+  in
+  Procdesc.get_proc_name pdesc |> get_class_of_pname
+  |> Option.iter ~f:(fun curr_class -> LockOrderDomain.iter (report_pair curr_class) summary)
+
+
+let analyze_procedure {Callbacks.proc_desc; get_proc_desc; tenv; summary} =
+  let proc_data = ProcData.make_default proc_desc tenv in
+  let initial =
+    if not (Procdesc.is_java_synchronized proc_desc) then DeadlockDomain.empty
+    else
+      let attrs = Procdesc.get_attributes proc_desc in
+      List.hd attrs.ProcAttributes.formals
+      |> Option.value_map ~default:DeadlockDomain.empty ~f:(fun (name, typ) ->
+             let pvar = Pvar.mk name (Procdesc.get_proc_name proc_desc) in
+             let path = (AccessPath.base_of_pvar pvar typ, []) in
+             DeadlockDomain.acquire path DeadlockDomain.empty (Procdesc.get_loc proc_desc) )
+  in
+  match Analyzer.compute_post proc_data ~initial with
+  | None ->
+      summary
+  | Some lock_state ->
+      let lock_order = DeadlockDomain.to_summary lock_state in
+      let updated_summary = Summary.update_summary lock_order summary in
+      Option.iter updated_summary.Specs.payload.deadlock
+        ~f:(report_deadlocks get_proc_desc tenv proc_desc) ;
+      updated_summary

infer/src/concurrency/deadlockDomain.ml

@@ -9,46 +9,6 @@
 open! IStd
 module F = Format
 
-module StackDomain (Element : PrettyPrintable.PrintableOrderedType) = struct
-  type astate = Element.t list [@@deriving compare]
-
-  let push = List.cons
-
-  let pop = List.tl_exn
-
-  let is_empty = List.is_empty
-
-  let empty = []
-
-  let pp fmt x = Pp.semicolon_seq Element.pp fmt x
-
-  let ( <= ) ~lhs ~rhs =
-    let rec aux lhs rhs =
-      match (lhs, rhs) with
-      | [], _ ->
-          true
-      | _, [] ->
-          false
-      | x :: xs, y :: ys ->
-          Int.equal 0 (Element.compare x y) && aux xs ys
-    in
-    aux (List.rev lhs) (List.rev rhs)
-
-
-  let join lhs rhs =
-    let rec aux acc a b =
-      match (a, b) with
-      | [], _ | _, [] ->
-          acc
-      | x :: xs, y :: ys ->
-          if not (Int.equal 0 (Element.compare x y)) then [] else aux (x :: acc) xs ys
-    in
-    aux [] (List.rev lhs) (List.rev rhs)
-
-
-  let widen ~prev ~next ~num_iters:_ = join prev next
-end
-
 module LockIdentity = struct
   type t = AccessPath.t
 
@@ -66,8 +26,12 @@ module LockIdentity = struct
 
   let equal lock lock' = Int.equal 0 (compare lock lock')
 
+  let equal_modulo_base ((_, typ), aclist) ((_, typ'), aclist') =
+    Typ.equal typ typ' && AccessPath.equal_access_list aclist aclist'
+
+
   let pp fmt (((_, typ), _) as lock) =
-    Format.fprintf fmt "locks %a in class %a" AccessPath.pp lock (Typ.pp Pp.text) typ
+    Format.fprintf fmt "locks %a in class %a" AccessPath.pp lock (Typ.pp_full Pp.text) typ
 end
 
 module LockEvent = struct
@@ -83,14 +47,13 @@ module LockEvent = struct
 
   let locks_equal e e' = LockIdentity.equal e.lock e'.lock
 
-  let pp_trace fmt = function
-    | [] ->
-        ()
-    | trace ->
-        Format.fprintf fmt " (trace: %a)" (Pp.semicolon_seq CallSite.pp) trace
-
-
   let pp fmt e =
+    let pp_trace fmt = function
+      | [] ->
+          ()
+      | trace ->
+          Format.fprintf fmt " (trace: %a)" (Pp.semicolon_seq CallSite.pp) trace
+    in
     Format.fprintf fmt "%a at %a%a" LockIdentity.pp e.lock Location.pp e.loc pp_trace e.trace
 
 
@@ -101,7 +64,7 @@ module LockEvent = struct
 
   let make lock loc = {lock; loc; trace= []}
 
-  let make_loc_trace e =
+  let make_loc_trace ?(reverse= false) e =
     let call_trace, nesting =
       List.fold e.trace ~init:([], 0) ~f:(fun (tr, ns) callsite ->
           let elem_descr =
@@ -112,43 +75,50 @@ module LockEvent = struct
     in
     let endpoint_descr = Format.asprintf "Lock acquisition: %a" LockIdentity.pp e.lock in
     let endpoint = Errlog.make_trace_element nesting e.loc endpoint_descr [] in
-    List.rev (endpoint :: call_trace)
+    let res = endpoint :: call_trace in
+    if reverse then res else List.rev res
 end
 
 module LockOrder = struct
-  type t = {before: LockEvent.t option; after: LockEvent.t} [@@deriving compare]
+  type t = {first: LockEvent.t option; eventually: LockEvent.t} [@@deriving compare]
 
   let pp fmt o =
-    match o.before with
+    match o.first with
     | None ->
-        Format.fprintf fmt "Eventually %a" LockEvent.pp o.after
+        Format.fprintf fmt "Eventually %a" LockEvent.pp o.eventually
     | Some lock ->
         Format.fprintf fmt "First %a and before releasing it %a" LockEvent.pp lock LockEvent.pp
-          o.after
+          o.eventually
 
 
-  let get_pair elem = match elem.before with None -> None | Some b -> Some (b, elem.after)
+  let get_pair elem = match elem.first with None -> None | Some b -> Some (b, elem.eventually)
 
   let may_deadlock elem elem' =
-    match (elem.before, elem'.before) with
+    let locks_equal_modulo_base e e' =
+      LockIdentity.equal_modulo_base e.LockEvent.lock e'.LockEvent.lock
+    in
+    match (elem.first, elem'.first) with
     | Some b, Some b' ->
-        LockEvent.locks_equal b elem'.after && LockEvent.locks_equal b' elem.after
+        locks_equal_modulo_base b elem'.eventually && locks_equal_modulo_base b' elem.eventually
     | _, _ ->
         false
 
 
-  let make_eventually_locks after = {before= None; after}
+  let make_eventually_locks eventually = {first= None; eventually}
 
-  let make_holds_and_locks b after = {before= Some b; after}
+  let make_holds_and_locks b eventually = {first= Some b; eventually}
 
   let with_callsite callsite o =
-    {o with after= {o.after with LockEvent.trace= callsite :: o.after.LockEvent.trace}}
+    { o with
+      eventually= {o.eventually with LockEvent.trace= callsite :: o.eventually.LockEvent.trace} }
 
 
   let make_loc_trace o =
-    let before_trace = Option.value_map o.before ~default:[] ~f:LockEvent.make_loc_trace in
-    let after_trace = LockEvent.make_loc_trace o.after in
-    List.append before_trace after_trace
+    let first_trace =
+      Option.value_map o.first ~default:[] ~f:(LockEvent.make_loc_trace ~reverse:true)
+    in
+    let eventually_trace = LockEvent.make_loc_trace o.eventually in
+    List.rev_append first_trace eventually_trace
 end
 
 module LockOrderDomain = struct
@@ -159,73 +129,86 @@ module LockOrderDomain = struct
 
 
   let is_eventually_locked lock lo =
-    exists (fun pair -> LockEvent.locks_equal pair.LockOrder.after lock) lo
+    exists (fun pair -> LockEvent.locks_equal pair.LockOrder.eventually lock) lo
 end
 
-module LockStack = StackDomain (LockEvent)
+module LockStack = AbstractDomain.StackDomain (LockEvent)
 
 module LockState = struct
-  include AbstractDomain.Pair (LockStack) (LockOrderDomain)
+  include AbstractDomain.InvertedMap (LockIdentity) (LockStack)
 
-  let empty = (LockStack.empty, LockOrderDomain.empty)
+  let is_taken lock map = try not (find lock map |> LockStack.is_empty) with Not_found -> false
 
-  let is_empty (ls, lo) = LockStack.is_empty ls && LockOrderDomain.is_empty lo
+  let acquire lock_event map =
+    let lock_id = lock_event.LockEvent.lock in
+    let current_value = try find lock_id map with Not_found -> LockStack.empty in
+    let new_value = LockStack.push lock_event current_value in
+    add lock_id new_value map
 
-  (* for every lock b held locally, add a pair (b, lock_event), plus (None, lock_event) *)
-  let add_order_pairs ls lock_event acc =
-    (* add no pairs whatsoever if we already hold that lock *)
-    if List.exists ls ~f:(LockEvent.locks_equal lock_event) then acc
+
+  let release lock_id map =
+    let current_value = try find lock_id map with Not_found -> LockStack.empty in
+    if LockStack.is_empty current_value then map
     else
-      let add_eventually_locks acc =
-        (* don't add an eventually-locks pair if there is already another with same endpoint*)
-        if LockOrderDomain.is_eventually_locked lock_event acc then acc
-        else
-          let elem = LockOrder.make_eventually_locks lock_event in
-          LockOrderDomain.add elem acc
-      in
-      let add_holds_and_locks acc before =
-        (* never add a pair of the form (a,a) -- should never happen due to the check above *)
-        let elem = LockOrder.make_holds_and_locks before lock_event in
+      let new_value = LockStack.pop current_value in
+      if LockStack.is_empty new_value then remove lock_id map else add lock_id new_value map
+
+
+  let fold_over_events f map init =
+    let ff _ lock_state acc = List.fold lock_state ~init:acc ~f in
+    fold ff map init
+end
+
+include AbstractDomain.Pair (LockState) (LockOrderDomain)
+
+let empty = (LockState.empty, LockOrderDomain.empty)
+
+let is_empty (ls, lo) = LockState.is_empty ls && LockOrderDomain.is_empty lo
+
+(* for every lock b held locally, add a pair (b, lock_event), plus (None, lock_event) *)
+let add_order_pairs ls lock_event acc =
+  (* add no pairs whatsoever if we already hold that lock *)
+  if LockState.is_taken lock_event.LockEvent.lock ls then acc
+  else
+    let add_eventually_locks acc =
+      (* don't add an eventually-locks pair if there is already another with same endpoint*)
+      if LockOrderDomain.is_eventually_locked lock_event acc then acc
+      else
+        let elem = LockOrder.make_eventually_locks lock_event in
         LockOrderDomain.add elem acc
-      in
-      List.fold ls ~init:acc ~f:add_holds_and_locks |> add_eventually_locks
-
-
-  let lock actuals ((ls, lo) as astate) loc =
-    match actuals with
-    | (HilExp.AccessExpression exp) :: _ ->
-        let newlock_event = LockEvent.make (AccessExpression.to_access_path exp) loc in
-        let lo' =
-          (* do not add any order pairs if we already hold the lock *)
-          if List.exists ls ~f:(LockEvent.locks_equal newlock_event) then lo
-          else add_order_pairs ls newlock_event lo
-        in
-        let ls' = LockStack.push newlock_event ls in
-        (ls', lo')
-    | _ ->
-        astate
-
-
-  let unlock _ (ls, lo) = ((if LockStack.is_empty ls then ls else LockStack.pop ls), lo)
-
-  let integrate_summary ~caller_state:(ls, lo) ~callee_summary callee_pname loc =
-    (* for each pair (b,a) in the callee, add (l,b) and (l,a) to the current state, where
-       l is held locally *)
-    let do_elem elem acc =
-      Option.value_map elem.LockOrder.before ~default:acc ~f:(fun b -> add_order_pairs ls b acc)
-      |> add_order_pairs ls elem.LockOrder.after
     in
-    let callsite = CallSite.make callee_pname loc in
-    (* add callsite to the "after" trace *)
-    let elems = LockOrderDomain.with_callsite callsite callee_summary in
-    let lo' = LockOrderDomain.fold do_elem elems lo in
-    (ls, lo')
+    let add_holds_and_locks acc first =
+      (* never add a pair of the form (a,a) -- should never happen due to the check above *)
+      let elem = LockOrder.make_holds_and_locks first lock_event in
+      LockOrderDomain.add elem acc
+    in
+    LockState.fold_over_events add_holds_and_locks ls acc |> add_eventually_locks
 
 
-  let to_summary astate = snd astate
-end
+let acquire lockid (ls, lo) loc =
+  let newlock_event = LockEvent.make lockid loc in
+  let lo' = add_order_pairs ls newlock_event lo in
+  let ls' = LockState.acquire newlock_event ls in
+  (ls', lo')
+
+
+let release lockid (ls, lo) = (LockState.release lockid ls, lo)
+
+let integrate_summary ~caller_state:(ls, lo) ~callee_summary callee_pname loc =
+  (* for each pair (b,a) in the callee, add (l,b) and (l,a) to the current state, where
+     l is held locally *)
+  let do_elem elem acc =
+    Option.value_map elem.LockOrder.first ~default:acc ~f:(fun b -> add_order_pairs ls b acc)
+    |> add_order_pairs ls elem.LockOrder.eventually
+  in
+  let callsite = CallSite.make callee_pname loc in
+  (* add callsite to the "eventually" trace *)
+  let elems = LockOrderDomain.with_callsite callsite callee_summary in
+  let lo' = LockOrderDomain.fold do_elem elems lo in
+  (ls, lo')
+
 
-include LockState
+let to_summary astate = snd astate
 
 type summary = LockOrderDomain.astate
 

infer/src/concurrency/deadlockDomain.mli

@@ -12,69 +12,57 @@ module F = Format
 
 (** Abstraction of a path that represents a lock, special-casing equality and comparisons
     to work over type, base variable modulo this and access list *)
-module LockIdentity : sig
-  type t = AccessPath.t [@@deriving compare]
-
-  val pp : F.formatter -> t -> unit  [@@warning "-32"]
-end
+module LockIdentity : PrettyPrintable.PrintableOrderedType with type t = AccessPath.t
 
 (** A lock event.  Equality/comparison disregards the call trace but includes location. *)
 module LockEvent : sig
-  type t = private
-    {lock: LockIdentity.t; loc: Location.t; trace: CallSite.t list}
-    [@@deriving compare]
+  type t = private {lock: LockIdentity.t; loc: Location.t; trace: CallSite.t list}
+
+  include PrettyPrintable.PrintableOrderedType with type t := t
 
   val owner_class : t -> Typ.name option
-    [@@warning "-32"]
   (** Class of the root variable of the path representing the lock *)
-
-  val pp : F.formatter -> t -> unit  [@@warning "-32"]
 end
 
-module LockStack : AbstractDomain.WithBottom with type astate = LockEvent.t list
+module LockState : AbstractDomain.WithBottom
 
 (** Represents either
 - the existence of a program path from the current method to the eventual acquisition of a lock
-  ("after"), or,
-- the "before" lock being taken *in the current method* and, before its release, the eventual
-  acquisition of "after" *)
+  ("eventually"), or,
+- the "first" lock being taken *in the current method* and, before its release, the eventual
+  acquisition of "eventually" *)
 module LockOrder : sig
-  type t = private {before: LockEvent.t option; after: LockEvent.t} [@@deriving compare]
+  type t = private {first: LockEvent.t option; eventually: LockEvent.t}
 
-  val pp : F.formatter -> t -> unit
+  include PrettyPrintable.PrintableOrderedType with type t := t
 
   val get_pair : t -> (LockEvent.t * LockEvent.t) option
-    [@@warning "-32"]
-  (** return the pair (b, after) if before is Some b *)
+  (** return the pair (b, eventually) if first is Some b *)
 
-  val may_deadlock : t -> t -> bool  [@@warning "-32"]
+  val may_deadlock : t -> t -> bool
+  (** check if two pairs are symmetric in terms of locks, where locks are compared modulo the
+      variable name at the root of each path. *)
 
-  val make_loc_trace : t -> Errlog.loc_trace  [@@warning "-32"]
+  val make_loc_trace : t -> Errlog.loc_trace
 end
 
 module LockOrderDomain : sig
-  include module type of PrettyPrintable.MakePPSet (LockOrder)
+  include PrettyPrintable.PPSet with type elt = LockOrder.t
 
   include AbstractDomain.WithBottom with type astate = t
 end
 
-module LockState : sig
-  include AbstractDomain.WithBottom with type astate = LockStack.astate * LockOrderDomain.astate
-
-  val lock : HilExp.t list -> astate -> Location.t -> astate  [@@warning "-32"]
+include AbstractDomain.WithBottom
 
-  val unlock : HilExp.t list -> astate -> astate  [@@warning "-32"]
+val acquire : LockIdentity.t -> astate -> Location.t -> astate
 
-  val integrate_summary :
-    caller_state:astate -> callee_summary:LockOrderDomain.t -> Typ.Procname.t -> Location.t
-    -> astate
-    [@@warning "-32"]
-
-  val to_summary : astate -> LockOrderDomain.t  [@@warning "-32"]
-end
+val release : LockIdentity.t -> astate -> astate
 
 type summary = LockOrderDomain.astate
 
-include AbstractDomain.WithBottom with type astate = LockState.astate
-
 val pp_summary : F.formatter -> summary -> unit
+
+val to_summary : astate -> summary
+
+val integrate_summary :
+  caller_state:astate -> callee_summary:summary -> Typ.Procname.t -> Location.t -> astate