[deadlock] abstract domain

Reviewed By: sblackshear

Differential Revision: D7078994

fbshipit-source-id: 87d07d4

infer/src/IR/Typ.ml

@@ -473,6 +473,8 @@ let d_list (tl: t list) = L.add_print_action (L.PTtyp_list, Obj.repr tl)
 
 let name typ = match typ.desc with Tstruct name -> Some name | _ -> None
 
+let inner_name typ = match typ.desc with Tptr ({desc= Tstruct name}, _) -> Some name | _ -> None
+
 let unsome s = function
   | Some default_typ ->
       default_typ

infer/src/IR/Typ.mli

@@ -237,6 +237,9 @@ val d_list : t list -> unit
 val name : t -> Name.t option
 (** The name of a type *)
 
+val inner_name : t -> Name.t option
+(** Name of the type of a Tstruct pointed to by a Tptr *)
+
 val strip_ptr : t -> t
 (** turn a *T into a T. fails if [t] is not a pointer type *)
 

infer/src/absint/Var.ml

@@ -15,6 +15,14 @@ type t = LogicalVar of Ident.t | ProgramVar of Pvar.t [@@deriving compare]
 
 let equal = [%compare.equal : t]
 
+let compare_modulo_this x y =
+  match (x, y) with
+  | ProgramVar i, ProgramVar j ->
+      Pvar.compare_modulo_this i j
+  | _, _ ->
+      compare x y
+
+
 let of_id id = LogicalVar id
 
 let of_pvar pvar = ProgramVar pvar

infer/src/absint/Var.mli

@@ -15,6 +15,8 @@ type t = private LogicalVar of Ident.t | ProgramVar of Pvar.t [@@deriving compar
 
 val equal : t -> t -> bool
 
+val compare_modulo_this : t -> t -> int
+
 val of_id : Ident.t -> t
 
 val of_pvar : Pvar.t -> t

infer/src/backend/specs.ml

@@ -279,7 +279,8 @@ type payload =
   ; siof: SiofDomain.astate option
   ; typestate: unit TypeState.t option
   ; uninit: UninitDomain.summary option
-  ; cost: CostDomain.summary option }
+  ; cost: CostDomain.summary option
+  ; deadlock: DeadlockDomain.summary option }
 
 type summary =
   { phase: phase  (** in FOOTPRINT phase or in RE_EXECUTION PHASE *)
@@ -422,14 +423,15 @@ let pp_payload pe fmt
     ; buffer_overrun
     ; annot_map
     ; uninit
-    ; cost } =
+    ; cost
+    ; deadlock } =
   let pp_opt prefix pp fmt = function
     | Some x ->
         F.fprintf fmt "%s: %a@\n" prefix pp x
     | None ->
         ()
   in
-  F.fprintf fmt "%a%a%a%a%a%a%a%a%a%a%a@\n"
+  F.fprintf fmt "%a%a%a%a%a%a%a%a%a%a%a%a@\n"
     (pp_opt "PrePosts" (pp_specs pe))
     (Option.map ~f:NormSpec.tospecs preposts)
     (pp_opt "TypeState" (TypeState.pp TypeState.unit_ext))
@@ -448,6 +450,8 @@ let pp_payload pe fmt
     uninit
     (pp_opt "Cost" CostDomain.pp_summary)
     cost
+    (pp_opt "Deadlock" DeadlockDomain.pp_summary)
+    deadlock
 
 
 let pp_summary_text fmt summary =
@@ -637,7 +641,8 @@ let empty_payload =
   ; litho= None
   ; buffer_overrun= None
   ; uninit= None
-  ; cost= None }
+  ; cost= None
+  ; deadlock= None }
 
 
 (** [init_summary (depend_list, nodes,

infer/src/backend/specs.mli

@@ -105,7 +105,8 @@ type payload =
   ; siof: SiofDomain.astate option
   ; typestate: unit TypeState.t option
   ; uninit: UninitDomain.summary option
-  ; cost: CostDomain.summary option }
+  ; cost: CostDomain.summary option
+  ; deadlock: DeadlockDomain.summary option }
 
 (** Procedure summary *)
 type summary =

infer/src/base/Config.ml

@@ -678,6 +678,7 @@ and ( annotation_reachability
     , check_nullable
     , cost
     , crashcontext
+    , deadlock
     , eradicate
     , fragment_retains_view
     , immutable_cast
@@ -718,6 +719,7 @@ and ( annotation_reachability
   and crashcontext =
     mk_checker ~long:"crashcontext"
       "the crashcontext checker for Java stack trace context reconstruction"
+  and deadlock = mk_checker ~long:"deadlock" ~default:false "deadlock analysis"
   and eradicate =
     mk_checker ~long:"eradicate" "the eradicate @Nullable checker for Java annotations"
   and fragment_retains_view =
@@ -790,6 +792,7 @@ and ( annotation_reachability
   , check_nullable
   , cost
   , crashcontext
+  , deadlock
   , eradicate
   , fragment_retains_view
   , immutable_cast
@@ -2387,6 +2390,8 @@ and cxx_infer_headers = !cxx_infer_headers
 
 and cxx_scope_guards = !cxx_scope_guards
 
+and deadlock = !deadlock
+
 and debug_level_analysis = !debug_level_analysis
 
 and debug_level_capture = !debug_level_capture

infer/src/base/Config.mli

@@ -314,6 +314,8 @@ val cxx_infer_headers : bool
 
 val cxx_scope_guards : Yojson.Basic.json
 
+val deadlock : bool
+
 val debug_level_analysis : int
 
 val debug_level_capture : int

infer/src/base/IssueType.ml

@@ -279,6 +279,8 @@ let parameter_not_null_checked = from_string "PARAMETER_NOT_NULL_CHECKED"
 
 let pointer_size_mismatch = from_string "POINTER_SIZE_MISMATCH"
 
+let potential_deadlock = from_string "DEADLOCK"
+
 let precondition_not_found = from_string "PRECONDITION_NOT_FOUND"
 
 let precondition_not_met = from_string "PRECONDITION_NOT_MET"

infer/src/base/IssueType.mli

@@ -196,6 +196,8 @@ val parameter_not_null_checked : t
 
 val pointer_size_mismatch : t
 
+val potential_deadlock : t  [@@warning "-32"]
+
 val precondition_not_found : t
 
 val precondition_not_met : t

infer/src/checkers/registerCheckers.ml

@@ -102,7 +102,10 @@ let all_checkers =
   ; { name= "cost analysis"
     ; active= Config.cost
     ; callbacks= [(Procedure Cost.checker, Language.Clang); (Procedure Cost.checker, Language.Java)]
-    } ]
+    }
+  ; { name= "Deadlock analysis"
+    ; active= Config.deadlock
+    ; callbacks= [(Procedure Deadlock.analyze_procedure, Language.Java)] } ]
 
 
 let get_active_checkers () =

infer/src/concurrency/deadlock.ml

@@ -0,0 +1,14 @@
+(*
+ * Copyright (c) 2018 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+open! IStd
+module F = Format
+module L = Logging
+module MF = MarkupFormatter
+
+let analyze_procedure {Callbacks.summary} = summary

infer/src/concurrency/deadlock.mli

@@ -0,0 +1,12 @@
+(*
+ * Copyright (c) 2018 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+
+open! IStd
+
+val analyze_procedure : Callbacks.proc_callback_t

infer/src/concurrency/deadlockDomain.ml

@@ -0,0 +1,232 @@
+(*
+ * Copyright (c) 2018 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+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
+
+  (* compare type, base variable modulo this and access list *)
+  let compare (((base, typ), aclist) as lock) (((base', typ'), aclist') as lock') =
+    if phys_equal lock lock' then 0
+    else
+      let res = Typ.compare typ typ' in
+      if not (Int.equal res 0) then res
+      else
+        let res = Var.compare_modulo_this base base' in
+        if not (Int.equal res 0) then res
+        else List.compare AccessPath.compare_access aclist aclist'
+
+
+  let equal lock lock' = Int.equal 0 (compare lock lock')
+
+  let pp fmt (((_, typ), _) as lock) =
+    Format.fprintf fmt "locks %a in class %a" AccessPath.pp lock (Typ.pp Pp.text) typ
+end
+
+module LockEvent = struct
+  type t = {lock: LockIdentity.t; loc: Location.t; trace: CallSite.t list}
+
+  (* ignore trace when comparing *)
+  let compare e e' =
+    if phys_equal e e' then 0
+    else
+      let res = LockIdentity.compare e.lock e'.lock in
+      if not (Int.equal res 0) then res else Location.compare e.loc e'.loc
+
+
+  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 =
+    Format.fprintf fmt "%a at %a%a" LockIdentity.pp e.lock Location.pp e.loc pp_trace e.trace
+
+
+  let owner_class e =
+    let (_, typ), _ = e.lock in
+    Typ.inner_name typ
+
+
+  let make lock loc = {lock; loc; trace= []}
+
+  let make_loc_trace e =
+    let call_trace, nesting =
+      List.fold e.trace ~init:([], 0) ~f:(fun (tr, ns) callsite ->
+          let elem_descr =
+            Format.asprintf "Method call: %a" Typ.Procname.pp (CallSite.pname callsite)
+          in
+          let elem = Errlog.make_trace_element ns (CallSite.loc callsite) elem_descr [] in
+          (elem :: tr, ns + 1) )
+    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)
+end
+
+module LockOrder = struct
+  type t = {before: LockEvent.t option; after: LockEvent.t} [@@deriving compare]
+
+  let pp fmt o =
+    match o.before with
+    | None ->
+        Format.fprintf fmt "Eventually %a" LockEvent.pp o.after
+    | Some lock ->
+        Format.fprintf fmt "First %a and before releasing it %a" LockEvent.pp lock LockEvent.pp
+          o.after
+
+
+  let get_pair elem = match elem.before with None -> None | Some b -> Some (b, elem.after)
+
+  let may_deadlock elem elem' =
+    match (elem.before, elem'.before) with
+    | Some b, Some b' ->
+        LockEvent.locks_equal b elem'.after && LockEvent.locks_equal b' elem.after
+    | _, _ ->
+        false
+
+
+  let make_eventually_locks after = {before= None; after}
+
+  let make_holds_and_locks b after = {before= Some b; after}
+
+  let with_callsite callsite o =
+    {o with after= {o.after with LockEvent.trace= callsite :: o.after.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
+end
+
+module LockOrderDomain = struct
+  include AbstractDomain.FiniteSet (LockOrder)
+
+  let with_callsite callsite lo =
+    fold (fun o acc -> add (LockOrder.with_callsite callsite o) acc) lo empty
+
+
+  let is_eventually_locked lock lo =
+    exists (fun pair -> LockEvent.locks_equal pair.LockOrder.after lock) lo
+end
+
+module LockStack = StackDomain (LockEvent)
+
+module LockState = struct
+  include AbstractDomain.Pair (LockStack) (LockOrderDomain)
+
+  let empty = (LockStack.empty, LockOrderDomain.empty)
+
+  let is_empty (ls, lo) = LockStack.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 List.exists ls ~f:(LockEvent.locks_equal lock_event) 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
+      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
+        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 to_summary astate = snd astate
+end
+
+include LockState
+
+type summary = LockOrderDomain.astate
+
+let pp_summary = LockOrderDomain.pp

infer/src/concurrency/deadlockDomain.mli

@@ -0,0 +1,80 @@
+(*
+ * Copyright (c) 2018 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ *)
+
+open! IStd
+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
+
+(** 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]
+
+  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
+
+(** 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" *)
+module LockOrder : sig
+  type t = private {before: LockEvent.t option; after: LockEvent.t} [@@deriving compare]
+
+  val pp : F.formatter -> t -> unit
+
+  val get_pair : t -> (LockEvent.t * LockEvent.t) option
+    [@@warning "-32"]
+  (** return the pair (b, after) if before is Some b *)
+
+  val may_deadlock : t -> t -> bool  [@@warning "-32"]
+
+  val make_loc_trace : t -> Errlog.loc_trace  [@@warning "-32"]
+end
+
+module LockOrderDomain : sig
+  include module type of PrettyPrintable.MakePPSet (LockOrder)
+
+  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"]
+
+  val unlock : HilExp.t list -> astate -> astate  [@@warning "-32"]
+
+  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
+
+type summary = LockOrderDomain.astate
+
+include AbstractDomain.WithBottom with type astate = LockState.astate
+
+val pp_summary : F.formatter -> summary -> unit