From 1a0c73ab99e3d7feed5bf6ae744139bb1ccf956d Mon Sep 17 00:00:00 2001 From: Nikos Gorogiannis Date: Tue, 4 Feb 2020 02:47:28 -0800 Subject: [PATCH] [starvation] decouple AbstractAddress from starvation Summary: - Thread the two types into one instead of having a record where the `path` field doesn't always make sense (`Class` case). - Improved pretty printing of class objects (java only). - Move starvation-specific stuff out of `AbstractAddress` (eg `make_java_synchronized`). - Slight optimisation of `apply_subst` for when a parameter is used without additional accesses inside a method (then, the substitution need not modify the term substituted for the parameter in any way). Reviewed By: ezgicicek Differential Revision: D19639922 fbshipit-source-id: 1cebecf5d --- infer/src/concurrency/AbstractAddress.ml | 153 ++++++++---------- infer/src/concurrency/AbstractAddress.mli | 19 +-- infer/src/concurrency/starvationDomain.ml | 21 +++ infer/src/concurrency/starvationDomain.mli | 6 + .../codetoanalyze/java/starvation/issues.exp | 3 +- 5 files changed, 106 insertions(+), 96 deletions(-) diff --git a/infer/src/concurrency/AbstractAddress.ml b/infer/src/concurrency/AbstractAddress.ml index 338aee063..880612986 100644 --- a/infer/src/concurrency/AbstractAddress.ml +++ b/infer/src/concurrency/AbstractAddress.ml @@ -19,18 +19,25 @@ module IgnoreVar = struct 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 *) + ignores the root variable for comparisons. *) 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 *) +type t = + | Global of {path: AccessPath.t} (** [AccessPath] so as to include root var in comparison *) + | Class of {typename: Typ.Name.t} (** Java-only class object identified by typename *) + | Parameter of {index: int; path: path} + (** method parameter represented by its 0-indexed position *) [@@deriving compare, equal] -type t = {root: root; path: path} [@@deriving compare, equal] +let get_typ tenv = + let class_type = Typ.(mk (Tstruct Name.Java.java_lang_class)) in + let some_ptr_to_class_type = Some Typ.(mk (Tptr (class_type, Pk_pointer))) in + function + | Class _ -> + some_ptr_to_class_type + | Global {path} | Parameter {path} -> + AccessPath.get_typ path tenv -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 @@ -45,38 +52,18 @@ let rec norm_path tenv ((typ, (accesses : AccessPath.access list)) as 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 + match (t1, t2) with + | Parameter {path= (_, typ1), accesses1}, Parameter {path= (_, typ2), accesses2} -> (* 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} + (* globals and class objects must be identical across threads *) + equal t1 t2 -let make_parameter path index = {root= Parameter index; path} -let make_class path typename = {root= Class typename; path} +let is_class_object = function Class _ -> true | _ -> false -(** 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 -> ( @@ -86,69 +73,58 @@ let rec make formal_map (hilexp : HilExp.t) = (* ignore logical variables *) None | Var.ProgramVar pvar when Pvar.is_global pvar -> - Some (make_global path (Pvar.get_name pvar)) + Some (Global {path}) | Var.ProgramVar _ -> FormalMap.get_formal_index (fst path) formal_map (* ignores non-formals *) - |> Option.map ~f:(make_parameter path) ) + |> Option.map ~f:(fun index -> Parameter {index; path}) ) | Constant (Cclass class_id) -> - (* this is a synchronized/lock(CLASSNAME.class) construct *) - let path = path_of_java_class class_id in + (* this is a synchronized(CLASSNAME.class) or class object construct *) let typename = Ident.name_to_string class_id |> Typ.Name.Java.from_string in - Some (make_class path typename) + Some (Class {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 fmt t = 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) + match t with + | Global {path} -> + F.fprintf fmt "G{%a}" pp_path path + | Class {typename} -> + F.fprintf fmt "C{%s}" (Typ.Name.name typename) + | Parameter {index; path} -> + F.fprintf fmt "P<%i>{%a}" index pp_path path + + +let root_class = function + | Class {typename} -> + Some typename + | Global {path= (_, {desc}), _} | Parameter {path= (_, {desc}), _} -> ( + match desc with + | Tstruct typename | Tptr ({desc= Tstruct typename}, _) -> + Some typename + | _ -> + None ) + + +let describe fmt t = + let describe_root fmt t = + root_class t |> Option.iter ~f:(F.fprintf fmt " in %a" (MF.wrap_monospaced Typ.Name.pp)) 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) + let describe_class_object fmt typename = F.fprintf fmt "%s.class" (Typ.Name.name typename) in + match t with + | Class {typename} -> + MF.wrap_monospaced describe_class_object fmt typename + | Global {path} | Parameter {path} -> + F.fprintf fmt "%a%a" (MF.wrap_monospaced AccessPath.pp) path describe_root t -(** 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 = @@ -169,15 +145,26 @@ let make_subst formal_map actuals = subst -let apply_subst (subst : subst) lock = - match lock.root with +let apply_subst (subst : subst) t = + match t with | Global _ | Class _ -> - Some lock - | Parameter index -> ( + Some t + | Parameter {index; path= _, []} -> ( + try + (* Special case for when the parameter is used without additional accesses, eg [x] as opposed to [x.f[].g]. *) + subst.(index) + with Invalid_argument _ -> None ) + | Parameter {index; path} -> ( try + (* Here we know that there are additional accesses on the parameter *) match subst.(index) with | None -> None - | Some actual -> - Some {actual with path= AccessPath.append actual.path (snd lock.path)} + | Some (Class _ as t') as c -> + L.internal_error "Cannot dereference class object %a in path %a@." pp t' pp t ; + c + | Some (Parameter param) -> + Some (Parameter {param with path= AccessPath.append param.path (snd path)}) + | Some (Global global) -> + Some (Global {path= AccessPath.append global.path (snd path)}) with Invalid_argument _ -> None ) diff --git a/infer/src/concurrency/AbstractAddress.mli b/infer/src/concurrency/AbstractAddress.mli index 071137d45..03661a024 100644 --- a/infer/src/concurrency/AbstractAddress.mli +++ b/infer/src/concurrency/AbstractAddress.mli @@ -25,9 +25,8 @@ module F = Format 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. *) + are compared in the same way, but parameter-rooted paths need only have equal access lists (ie + [x.f.g == y.f.g]). This allows demonically aliasing parameters in *distinct* threads. *) include PrettyPrintable.PrintableOrderedType @@ -38,24 +37,20 @@ 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 *) +(** Class of the root variable of the expression representing the address *) 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 *) +(** convert an expression to a canonical form for an address *) val is_class_object : t -> bool -(** is the lock a class object such as in [synchronized(MyClass.class){}] or +(** is the address a Java 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 *) +(** A substitution from formal position indices to address options. [None] is used to for actuals + that cannot be resolved to an address (eg local-rooted paths or arithmetic expressions). *) type subst val pp_subst : F.formatter -> subst -> unit [@@warning "-32"] diff --git a/infer/src/concurrency/starvationDomain.ml b/infer/src/concurrency/starvationDomain.ml index 2ded6cc4f..56c039009 100644 --- a/infer/src/concurrency/starvationDomain.ml +++ b/infer/src/concurrency/starvationDomain.ml @@ -86,6 +86,27 @@ module Lock = struct include AbstractAddress let pp_locks fmt lock = F.fprintf fmt " locks %a" describe lock + + 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_str = Procname.Java.get_class_type_name java_pname |> Typ.Name.name in + let hilexp = HilExp.(Constant (Cclass (Ident.string_to_name typename_str))) in + make formals hilexp + | Procname.Java _ -> + FormalMap.get_formal_base 0 formals + |> Option.bind ~f:(fun base -> + let hilexp = HilExp.(AccessExpression (AccessExpression.base base)) in + make formals hilexp ) + | _ -> + L.die InternalError "Non-Java methods cannot be synchronized.@\n" + + + let compare_wrt_reporting t1 t2 = + let mk_str t = root_class t |> Option.value_map ~default:"" ~f:Typ.Name.to_string in + (* use string comparison on types as a stable order to decide whether to report a deadlock *) + String.compare (mk_str t1) (mk_str t2) end module Event = struct diff --git a/infer/src/concurrency/starvationDomain.mli b/infer/src/concurrency/starvationDomain.mli index a3bf2862b..168a2ec79 100644 --- a/infer/src/concurrency/starvationDomain.mli +++ b/infer/src/concurrency/starvationDomain.mli @@ -37,6 +37,12 @@ module Lock : sig include module type of AbstractAddress val pp_locks : F.formatter -> t -> unit + + val make_java_synchronized : FormalMap.t -> Procname.t -> t option + (** create the monitor locked when entering a synchronized java method *) + + val compare_wrt_reporting : t -> t -> int + (** a stable order for avoiding reporting deadlocks twice based on the root variable type *) end module Event : sig diff --git a/infer/tests/codetoanalyze/java/starvation/issues.exp b/infer/tests/codetoanalyze/java/starvation/issues.exp index fcfd76d6b..8c6788bea 100644 --- a/infer/tests/codetoanalyze/java/starvation/issues.exp +++ b/infer/tests/codetoanalyze/java/starvation/issues.exp @@ -53,7 +53,8 @@ codetoanalyze/java/starvation/PubPriv.java, PubPriv.callAnotherWayBad():void, 53 codetoanalyze/java/starvation/PubPriv.java, PubPriv.callOneWayBad():void, 49, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void PubPriv.callOneWayBad()`,Method call: `void PubPriv.oneWayOk()`, locks `this.lockA` in `class PubPriv`, locks `this.lockB` in `class PubPriv`,[Trace 2] `void PubPriv.callAnotherWayBad()`,Method call: `void PubPriv.anotherWayOk()`, locks `this.lockB` in `class PubPriv`, locks `this.lockA` in `class PubPriv`] codetoanalyze/java/starvation/PubPriv.java, PubPriv.transactBad():void, 21, STARVATION, no_bucket, ERROR, [`void PubPriv.transactBad()`,Method call: `void PubPriv.doTransactOk()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`] codetoanalyze/java/starvation/ServiceOnUIThread.java, ServiceOnUIThread.onBind(android.content.Intent):android.os.IBinder, 19, STARVATION, no_bucket, ERROR, [`IBinder ServiceOnUIThread.onBind(Intent)`,Method call: `void ServiceOnUIThread.transactBad()`,calls `boolean IBinder.transact(int,Parcel,Parcel,int)`] -codetoanalyze/java/starvation/StaticLock.java, StaticLock.lockOtherClassOneWayBad():void, 23, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void StaticLock.lockOtherClassOneWayBad()`, locks `StaticLock$0` in `class java.lang.Class`, locks `this` in `class StaticLock`,[Trace 2] `void StaticLock.lockOtherClassAnotherWayBad()`, locks `this` in `class StaticLock`,Method call: `void StaticLock.staticSynced()`, locks `StaticLock$0` in `class java.lang.Class`] +codetoanalyze/java/starvation/StaticLock.java, StaticLock.lockOtherClassAnotherWayBad():void, 30, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void StaticLock.lockOtherClassAnotherWayBad()`, locks `this` in `class StaticLock`,Method call: `void StaticLock.staticSynced()`, locks `StaticLock.class`,[Trace 2] `void StaticLock.lockOtherClassOneWayBad()`, locks `StaticLock.class`, locks `this` in `class StaticLock`] +codetoanalyze/java/starvation/StaticLock.java, StaticLock.lockOtherClassOneWayBad():void, 23, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void StaticLock.lockOtherClassOneWayBad()`, locks `StaticLock.class`, locks `this` in `class StaticLock`,[Trace 2] `void StaticLock.lockOtherClassAnotherWayBad()`, locks `this` in `class StaticLock`,Method call: `void StaticLock.staticSynced()`, locks `StaticLock.class`] codetoanalyze/java/starvation/StrictModeViolation.java, StrictModeViolation.violateStrictModeBad():void, 17, STRICT_MODE_VIOLATION, no_bucket, ERROR, [`void StrictModeViolation.violateStrictModeBad()`,calls `boolean File.canRead()`] codetoanalyze/java/starvation/StrictModeViolation.java, StrictModeViolation.violateStrictModeBad():void, 18, STRICT_MODE_VIOLATION, no_bucket, ERROR, [`void StrictModeViolation.violateStrictModeBad()`,calls `boolean File.canWrite()`] codetoanalyze/java/starvation/StrictModeViolation.java, StrictModeViolation.violateStrictModeBad():void, 19, STRICT_MODE_VIOLATION, no_bucket, ERROR, [`void StrictModeViolation.violateStrictModeBad()`,calls `boolean File.createNewFile()`]