diff --git a/infer/src/concurrency/AbstractAddress.ml b/infer/src/concurrency/AbstractAddress.ml new file mode 100644 index 000000000..338aee063 --- /dev/null +++ b/infer/src/concurrency/AbstractAddress.ml @@ -0,0 +1,183 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) +open! IStd +module F = Format +module L = Logging +module MF = MarkupFormatter + +(** var type used only for printing, not comparisons *) +module IgnoreVar = struct + type t = Var.t + + let compare _x _y = 0 + + let equal _x _y = true +end + +(** access path that does not ignore the type (like the original AccessPath.t) but which instead + ignores the root variable for comparisons; this is taken care of by the root type *) +type path = (IgnoreVar.t * Typ.t) * AccessPath.access list [@@deriving compare, equal] + +type root = + | Global of Mangled.t + | Class of Typ.name + | Parameter of int (** method parameter represented by its 0-indexed position *) +[@@deriving compare, equal] + +type t = {root: root; path: path} [@@deriving compare, equal] + +let get_typ tenv t = AccessPath.get_typ t.path tenv + +let rec norm_path tenv ((typ, (accesses : AccessPath.access list)) as path) = + match accesses with + | (FieldAccess fieldname as access) :: rest when Fieldname.is_java_outer_instance fieldname -> ( + match AccessPath.get_access_type tenv typ access with + | Some typ' -> + norm_path tenv (typ', rest) + | None -> + path ) + | _ -> + path + + +let equal_across_threads tenv t1 t2 = + match (t1.root, t2.root) with + | Global _, Global _ | Class _, Class _ -> + (* globals and class objects must be identical across threads *) + equal t1 t2 + | Parameter _, Parameter _ -> + let ((_, typ1), accesses1), ((_, typ2), accesses2) = (t1.path, t2.path) in + (* parameter position/names can be ignored across threads, if types and accesses are equal *) + let path1, path2 = (norm_path tenv (typ1, accesses1), norm_path tenv (typ2, accesses2)) in + [%equal: Typ.t * AccessPath.access list] path1 path2 + | _, _ -> + false + + +let is_class_object = function {root= Class _} -> true | _ -> false + +(* using an indentifier for a class object, create an access path representing that lock; + this is for synchronizing on Java class objects only *) +let path_of_java_class = + let typ = Typ.(mk (Tstruct Name.Java.java_lang_class)) in + let typ' = Typ.(mk (Tptr (typ, Pk_pointer))) in + fun class_id -> + let ident = Ident.create_normal class_id 0 in + AccessPath.of_id ident typ' + + +let make_global path mangled = {root= Global mangled; path} + +let make_parameter path index = {root= Parameter index; path} + +let make_class path typename = {root= Class typename; path} + +(** convert an expression to a canonical form for a lock identifier *) +let rec make formal_map (hilexp : HilExp.t) = + match hilexp with + | AccessExpression access_exp -> ( + let path = HilExp.AccessExpression.to_access_path access_exp in + match fst (fst path) with + | Var.LogicalVar _ -> + (* ignore logical variables *) + None + | Var.ProgramVar pvar when Pvar.is_global pvar -> + Some (make_global path (Pvar.get_name pvar)) + | Var.ProgramVar _ -> + FormalMap.get_formal_index (fst path) formal_map + (* ignores non-formals *) + |> Option.map ~f:(make_parameter path) ) + | Constant (Cclass class_id) -> + (* this is a synchronized/lock(CLASSNAME.class) construct *) + let path = path_of_java_class class_id in + let typename = Ident.name_to_string class_id |> Typ.Name.Java.from_string in + Some (make_class path typename) + | Cast (_, hilexp) | Exception hilexp | UnaryOperator (_, hilexp, _) -> + make formal_map hilexp + | BinaryOperator _ | Closure _ | Constant _ | Sizeof _ -> + None + + +let make_java_synchronized formals procname = + match procname with + | Procname.Java java_pname when Procname.Java.is_static java_pname -> + (* this is crafted so as to match synchronized(CLASSNAME.class) constructs *) + let typename = Procname.Java.get_class_type_name java_pname in + let path = Typ.Name.name typename |> Ident.string_to_name |> path_of_java_class in + Some (make_class path typename) + | Procname.Java _ -> + FormalMap.get_formal_base 0 formals |> Option.map ~f:(fun base -> make_parameter (base, []) 0) + | _ -> + L.die InternalError "Non-Java methods cannot be synchronized.@\n" + + +let pp fmt {root; path} = + let pp_path fmt ((var, typ), accesses) = + F.fprintf fmt "(%a:%a)" Var.pp var (Typ.pp_full Pp.text) typ ; + if not (List.is_empty accesses) then F.fprintf fmt ".%a" AccessPath.pp_access_list accesses + in + match root with + | Global mangled -> + F.fprintf fmt "G<%a>{%a}" Mangled.pp mangled pp_path path + | Class typename -> + F.fprintf fmt "C<%a>{%a}" Typ.Name.pp typename pp_path path + | Parameter idx -> + F.fprintf fmt "P<%i>{%a}" idx pp_path path + + +let root_class {path= (_, {Typ.desc}), _} = + match desc with Typ.Tstruct name | Typ.Tptr ({desc= Tstruct name}, _) -> Some name | _ -> None + + +let describe fmt lock = + let describe_lock fmt lock = (MF.wrap_monospaced AccessPath.pp) fmt lock.path in + let describe_typename = MF.wrap_monospaced Typ.Name.pp in + let describe_owner fmt lock = + root_class lock |> Option.iter ~f:(F.fprintf fmt " in %a" describe_typename) + in + F.fprintf fmt "%a%a" describe_lock lock describe_owner lock + + +let compare_wrt_reporting {path= (_, typ1), _} {path= (_, typ2), _} = + (* use string comparison on types as a stable order to decide whether to report a deadlock *) + String.compare (Typ.to_string typ1) (Typ.to_string typ2) + + +(** A substitution from formal position indices to actuals. Since we only care about locks, use + [None] to denote an argument that cannot be resolved to a lock object. *) +type subst = t option Array.t + +let pp_subst fmt subst = + PrettyPrintable.pp_collection fmt ~pp_item:(Pp.option pp) (Array.to_list subst) + + +let make_subst formal_map actuals = + let actuals = Array.of_list actuals in + let len = + (* deal with var args functions *) + Int.max (FormalMap.cardinal formal_map) (Array.length actuals) + in + let subst = Array.create ~len None in + FormalMap.iter + (fun _base idx -> + if idx < Array.length actuals then subst.(idx) <- make formal_map actuals.(idx) ) + formal_map ; + subst + + +let apply_subst (subst : subst) lock = + match lock.root with + | Global _ | Class _ -> + Some lock + | Parameter index -> ( + try + match subst.(index) with + | None -> + None + | Some actual -> + Some {actual with path= AccessPath.append actual.path (snd lock.path)} + with Invalid_argument _ -> None ) diff --git a/infer/src/concurrency/AbstractAddress.mli b/infer/src/concurrency/AbstractAddress.mli new file mode 100644 index 000000000..071137d45 --- /dev/null +++ b/infer/src/concurrency/AbstractAddress.mli @@ -0,0 +1,65 @@ +(* + * Copyright (c) Facebook, Inc. and its affiliates. + * + * This source code is licensed under the MIT license found in the + * LICENSE file in the root directory of this source tree. + *) + +open! IStd +module F = Format + +(** Type meant to represent abstract addresses based on access paths. It currently distinguishes + between paths + + - rooted at formal parameters (these are identified by the parameter index and the path without + the root variable, though that variable is kept for pretty printing); + - rooted at global variables; + - non access-path expressions representing class objects (java only). + + Notably, there are no addresses rooted at locals (because proving aliasing between those is + difficult). + + There are two notions of equality: + + - Equality for comparing two addresses within the same thread/process/trace. Under this, + identical globals and identical class objects compare equal. Parameter-rooted paths compare + equal if their parameter indices, types and lists of accesses are equal. + - Equality for comparing two addresses in two distinct threads/traces. Globals and class objects + are compared in the same way, but parameter-rooted paths need only only have equal access + lists (ie [x.f.g == y.f.g]). This allows demonically aliasing parameters in *distinct* + threads. *) + +include PrettyPrintable.PrintableOrderedType + +val describe : F.formatter -> t -> unit +(** human readable description *) + +val equal : t -> t -> bool + +val equal_across_threads : Tenv.t -> t -> t -> bool + +val compare_wrt_reporting : t -> t -> int +(** a stable order for avoiding reporting deadlocks twice based on the root variable type *) + +val root_class : t -> Typ.name option +(** Class of the root variable of the path representing the lock *) + +val get_typ : Tenv.t -> t -> Typ.t option + +val make : FormalMap.t -> HilExp.t -> t option + +val make_java_synchronized : FormalMap.t -> Procname.t -> t option +(** create the monitor locked when entering a synchronized java method *) + +val is_class_object : t -> bool +(** is the lock a class object such as in [synchronized(MyClass.class){}] or + [static synchronized void foo()] *) + +(** substitution type : a map from (0-based) positional index to lock options *) +type subst + +val pp_subst : F.formatter -> subst -> unit [@@warning "-32"] + +val make_subst : FormalMap.t -> HilExp.t list -> subst + +val apply_subst : subst -> t -> t option diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index ee8f7198f..709e7877a 100644 --- a/infer/src/concurrency/starvation.ml +++ b/infer/src/concurrency/starvation.ml @@ -712,7 +712,7 @@ let report_on_pair tenv summary (pair : Domain.CriticalPair.t) report_map = let ltr = CriticalPair.make_trace ~header:"In method " pname pair in ReportMap.add_deadlock tenv pdesc loc ltr error_message report_map | LockAcquire lock when not Config.starvation_whole_program -> - Lock.owner_class lock + Lock.root_class lock |> Option.value_map ~default:report_map ~f:(fun other_class -> (* get the class of the root variable of the lock in the lock acquisition and retrieve all the summaries of the methods of that class; diff --git a/infer/src/concurrency/starvationDomain.ml b/infer/src/concurrency/starvationDomain.ml index 9f448520e..2ded6cc4f 100644 --- a/infer/src/concurrency/starvationDomain.ml +++ b/infer/src/concurrency/starvationDomain.ml @@ -83,179 +83,9 @@ module ThreadDomain = struct end module Lock = struct - (** var type used only for printing, not comparisons *) - module IgnoreVar = struct - type t = Var.t - - let compare _x _y = 0 - - let equal _x _y = true - end - - (** access path that does not ignore the type (like the original AccessPath.t) but which instead - ignores the root variable for comparisons; this is taken care of by the root type *) - type path = (IgnoreVar.t * Typ.t) * AccessPath.access list [@@deriving compare, equal] - - type root = - | Global of Mangled.t - | Class of Typ.name - | Parameter of int (** method parameter represented by its 0-indexed position *) - [@@deriving compare, equal] - - type t = {root: root; path: path} [@@deriving compare, equal] - - let rec norm_path tenv ((typ, (accesses : AccessPath.access list)) as path) = - match accesses with - | (FieldAccess fieldname as access) :: rest when Fieldname.is_java_outer_instance fieldname -> ( - match AccessPath.get_access_type tenv typ access with - | Some typ' -> - norm_path tenv (typ', rest) - | None -> - path ) - | _ -> - path - - - let equal_across_threads tenv t1 t2 = - match (t1.root, t2.root) with - | Global _, Global _ | Class _, Class _ -> - (* globals and class objects must be identical across threads *) - equal t1 t2 - | Parameter _, Parameter _ -> - let ((_, typ1), accesses1), ((_, typ2), accesses2) = (t1.path, t2.path) in - (* parameter position/names can be ignored across threads, if types and accesses are equal *) - let path1, path2 = (norm_path tenv (typ1, accesses1), norm_path tenv (typ2, accesses2)) in - [%equal: Typ.t * AccessPath.access list] path1 path2 - | _, _ -> - false - - - let is_class_object = function {root= Class _} -> true | _ -> false - - (* using an indentifier for a class object, create an access path representing that lock; - this is for synchronizing on Java class objects only *) - let path_of_java_class = - let typ = Typ.(mk (Tstruct Name.Java.java_lang_class)) in - let typ' = Typ.(mk (Tptr (typ, Pk_pointer))) in - fun class_id -> - let ident = Ident.create_normal class_id 0 in - AccessPath.of_id ident typ' - - - let make_global path mangled = {root= Global mangled; path} - - let make_parameter path index = {root= Parameter index; path} - - let make_class path typename = {root= Class typename; path} - - (** convert an expression to a canonical form for a lock identifier *) - let rec make formal_map (hilexp : HilExp.t) = - match hilexp with - | AccessExpression access_exp -> ( - let path = HilExp.AccessExpression.to_access_path access_exp in - match fst (fst path) with - | Var.LogicalVar _ -> - (* ignore logical variables *) - None - | Var.ProgramVar pvar when Pvar.is_global pvar -> - Some (make_global path (Pvar.get_name pvar)) - | Var.ProgramVar _ -> - FormalMap.get_formal_index (fst path) formal_map - (* ignores non-formals *) - |> Option.map ~f:(make_parameter path) ) - | Constant (Cclass class_id) -> - (* this is a synchronized/lock(CLASSNAME.class) construct *) - let path = path_of_java_class class_id in - let typename = Ident.name_to_string class_id |> Typ.Name.Java.from_string in - Some (make_class path typename) - | Cast (_, hilexp) | Exception hilexp | UnaryOperator (_, hilexp, _) -> - make formal_map hilexp - | BinaryOperator _ | Closure _ | Constant _ | Sizeof _ -> - None - - - let make_java_synchronized formals procname = - match procname with - | Procname.Java java_pname when Procname.Java.is_static java_pname -> - (* this is crafted so as to match synchronized(CLASSNAME.class) constructs *) - let typename = Procname.Java.get_class_type_name java_pname in - let path = Typ.Name.name typename |> Ident.string_to_name |> path_of_java_class in - Some (make_class path typename) - | Procname.Java _ -> - FormalMap.get_formal_base 0 formals - |> Option.map ~f:(fun base -> make_parameter (base, []) 0) - | _ -> - L.die InternalError "Non-Java methods cannot be synchronized.@\n" - - - let pp fmt {root; path} = - let pp_path fmt ((var, typ), accesses) = - F.fprintf fmt "(%a:%a)" Var.pp var (Typ.pp_full Pp.text) typ ; - if not (List.is_empty accesses) then F.fprintf fmt ".%a" AccessPath.pp_access_list accesses - in - match root with - | Global mangled -> - F.fprintf fmt "G<%a>{%a}" Mangled.pp mangled pp_path path - | Class typename -> - F.fprintf fmt "C<%a>{%a}" Typ.Name.pp typename pp_path path - | Parameter idx -> - F.fprintf fmt "P<%i>{%a}" idx pp_path path - - - let owner_class {path= (_, {Typ.desc}), _} = - match desc with Typ.Tstruct name | Typ.Tptr ({desc= Tstruct name}, _) -> Some name | _ -> None - - - let describe fmt lock = - let describe_lock fmt lock = (MF.wrap_monospaced AccessPath.pp) fmt lock.path in - let describe_typename = MF.wrap_monospaced Typ.Name.pp in - let describe_owner fmt lock = - owner_class lock |> Option.iter ~f:(F.fprintf fmt " in %a" describe_typename) - in - F.fprintf fmt "%a%a" describe_lock lock describe_owner lock - + include AbstractAddress let pp_locks fmt lock = F.fprintf fmt " locks %a" describe lock - - let compare_wrt_reporting {path= (_, typ1), _} {path= (_, typ2), _} = - (* use string comparison on types as a stable order to decide whether to report a deadlock *) - String.compare (Typ.to_string typ1) (Typ.to_string typ2) - - - (** A substitution from formal position indices to actuals. Since we only care about locks, use - [None] to denote an argument that cannot be resolved to a lock object. *) - type subst = t option Array.t - - let[@warning "-32"] pp_subst fmt subst = - PrettyPrintable.pp_collection fmt ~pp_item:(Pp.option pp) (Array.to_list subst) - - - let make_subst formal_map actuals = - let actuals = Array.of_list actuals in - let len = - (* deal with var args functions *) - Int.max (FormalMap.cardinal formal_map) (Array.length actuals) - in - let subst = Array.create ~len None in - FormalMap.iter - (fun _base idx -> - if idx < Array.length actuals then subst.(idx) <- make formal_map actuals.(idx) ) - formal_map ; - subst - - - let apply_subst (subst : subst) lock = - match lock.root with - | Global _ | Class _ -> - Some lock - | Parameter index -> ( - try - match subst.(index) with - | None -> - None - | Some actual -> - Some {actual with path= AccessPath.append actual.path (snd lock.path)} - with Invalid_argument _ -> None ) end module Event = struct @@ -502,7 +332,7 @@ let is_recursive_lock event tenv = in match event with | Event.LockAcquire lock_path -> - AccessPath.get_typ lock_path.path tenv |> Option.exists ~f:is_class_and_recursive_lock + Lock.get_typ tenv lock_path |> Option.exists ~f:is_class_and_recursive_lock | _ -> false diff --git a/infer/src/concurrency/starvationDomain.mli b/infer/src/concurrency/starvationDomain.mli index 2e294bfc4..a3bf2862b 100644 --- a/infer/src/concurrency/starvationDomain.mli +++ b/infer/src/concurrency/starvationDomain.mli @@ -34,35 +34,9 @@ end only have equal access lists (ie [x.f.g == y.f.g]). This allows demonically aliasing parameters in *distinct* threads. This relation is used in [may_deadlock]. *) module Lock : sig - include PrettyPrintable.PrintableOrderedType - - val equal : t -> t -> bool - - val owner_class : t -> Typ.name option - (** Class of the root variable of the path representing the lock *) + include module type of AbstractAddress val pp_locks : F.formatter -> t -> unit - - val describe : F.formatter -> t -> unit - - val make : FormalMap.t -> HilExp.t -> t option - (** make a lock if the expression is rooted at a global or a formal parameter, or represents a - class object *) - - val make_java_synchronized : FormalMap.t -> Procname.t -> t option - (** create the monitor locked when entering a synchronized java method *) - - val is_class_object : t -> bool - (** is the lock a class object such as in [synchronized(MyClass.class){}] or - [static synchronized void foo()] *) - - val compare_wrt_reporting : t -> t -> int - (** a stable order for avoiding reporting deadlocks twice based on the root variable type *) - - (** substitution type : a map from (0-based) positional index to lock options *) - type subst - - val make_subst : FormalMap.t -> HilExp.t list -> subst end module Event : sig