From 3bcfbd6a6498e2b671ce37f0a6170474edc7be0d Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Fri, 9 Mar 2018 09:17:10 -0800 Subject: [PATCH] [deadlock] abstract domain Reviewed By: sblackshear Differential Revision: D7078994 fbshipit-source-id: 87d07d4 --- infer/src/IR/Typ.ml | 2 + infer/src/IR/Typ.mli | 3 + infer/src/absint/Var.ml | 8 + infer/src/absint/Var.mli | 2 + infer/src/backend/specs.ml | 13 +- infer/src/backend/specs.mli | 3 +- infer/src/base/Config.ml | 5 + infer/src/base/Config.mli | 2 + infer/src/base/IssueType.ml | 2 + infer/src/base/IssueType.mli | 2 + infer/src/checkers/registerCheckers.ml | 5 +- infer/src/concurrency/deadlock.ml | 14 ++ infer/src/concurrency/deadlock.mli | 12 ++ infer/src/concurrency/deadlockDomain.ml | 232 +++++++++++++++++++++++ infer/src/concurrency/deadlockDomain.mli | 80 ++++++++ 15 files changed, 379 insertions(+), 6 deletions(-) create mode 100644 infer/src/concurrency/deadlock.ml create mode 100644 infer/src/concurrency/deadlock.mli create mode 100644 infer/src/concurrency/deadlockDomain.ml create mode 100644 infer/src/concurrency/deadlockDomain.mli diff --git a/infer/src/IR/Typ.ml b/infer/src/IR/Typ.ml index b730ffb05..597a95235 100644 --- a/infer/src/IR/Typ.ml +++ b/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 diff --git a/infer/src/IR/Typ.mli b/infer/src/IR/Typ.mli index aa9d590d9..0a63525a7 100644 --- a/infer/src/IR/Typ.mli +++ b/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 *) diff --git a/infer/src/absint/Var.ml b/infer/src/absint/Var.ml index 1e51fd9b7..b351956a7 100644 --- a/infer/src/absint/Var.ml +++ b/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 diff --git a/infer/src/absint/Var.mli b/infer/src/absint/Var.mli index f52fbc492..c74905c6b 100644 --- a/infer/src/absint/Var.mli +++ b/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 diff --git a/infer/src/backend/specs.ml b/infer/src/backend/specs.ml index c31423df5..6c39a0c2d 100644 --- a/infer/src/backend/specs.ml +++ b/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, diff --git a/infer/src/backend/specs.mli b/infer/src/backend/specs.mli index 9c45539f1..0d00fa516 100644 --- a/infer/src/backend/specs.mli +++ b/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 = diff --git a/infer/src/base/Config.ml b/infer/src/base/Config.ml index 27dcd6c53..bcf57ce1b 100644 --- a/infer/src/base/Config.ml +++ b/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 diff --git a/infer/src/base/Config.mli b/infer/src/base/Config.mli index 76178fb60..edcd7a9b8 100644 --- a/infer/src/base/Config.mli +++ b/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 diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index 4d22b28a5..467d589cb 100644 --- a/infer/src/base/IssueType.ml +++ b/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" diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index 9db97408b..66594a279 100644 --- a/infer/src/base/IssueType.mli +++ b/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 diff --git a/infer/src/checkers/registerCheckers.ml b/infer/src/checkers/registerCheckers.ml index 7597b5c7e..297d574f9 100644 --- a/infer/src/checkers/registerCheckers.ml +++ b/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 () = diff --git a/infer/src/concurrency/deadlock.ml b/infer/src/concurrency/deadlock.ml new file mode 100644 index 000000000..003870d3a --- /dev/null +++ b/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 diff --git a/infer/src/concurrency/deadlock.mli b/infer/src/concurrency/deadlock.mli new file mode 100644 index 000000000..13beba0f3 --- /dev/null +++ b/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 diff --git a/infer/src/concurrency/deadlockDomain.ml b/infer/src/concurrency/deadlockDomain.ml new file mode 100644 index 000000000..406a1f580 --- /dev/null +++ b/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 diff --git a/infer/src/concurrency/deadlockDomain.mli b/infer/src/concurrency/deadlockDomain.mli new file mode 100644 index 000000000..e3c9184cd --- /dev/null +++ b/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