From df5798336b8ca35ca31a37314205e7f4722d8e23 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Tue, 24 Jan 2017 10:31:51 -0800 Subject: [PATCH] [cleanup] give AccessPath.raw its own module Summary: This allows us to simplify ThreadSafetyDomain a bit. Reviewed By: jberdine Differential Revision: D4452740 fbshipit-source-id: 76fce02 --- infer/src/checkers/IdAccessPathMapDomain.ml | 16 +++--- infer/src/checkers/IdAccessPathMapDomain.mli | 2 +- infer/src/checkers/ThreadSafetyDomain.ml | 13 +---- infer/src/checkers/ThreadSafetyDomain.mli | 15 ++---- infer/src/checkers/accessPath.ml | 55 +++++++++++--------- infer/src/checkers/accessPath.mli | 35 +++++++------ infer/src/unit/accessPathTestUtils.mli | 2 +- infer/src/unit/accessPathTests.ml | 28 +++++----- 8 files changed, 79 insertions(+), 87 deletions(-) diff --git a/infer/src/checkers/IdAccessPathMapDomain.ml b/infer/src/checkers/IdAccessPathMapDomain.ml index 8eb00b008..7d9098f23 100644 --- a/infer/src/checkers/IdAccessPathMapDomain.ml +++ b/infer/src/checkers/IdAccessPathMapDomain.ml @@ -11,12 +11,12 @@ open! IStd module IdMap = Var.Map -type astate = AccessPath.raw IdMap.t +type astate = AccessPath.Raw.t IdMap.t include IdMap let pp fmt astate = - IdMap.pp ~pp_value:AccessPath.pp_raw fmt astate + IdMap.pp ~pp_value:AccessPath.Raw.pp fmt astate let (<=) ~lhs ~rhs = if phys_equal lhs rhs @@ -26,13 +26,13 @@ let (<=) ~lhs ~rhs = IdMap.for_all (fun id lhs_ap -> let rhs_ap = IdMap.find id rhs in - let eq = AccessPath.equal_raw lhs_ap rhs_ap in + let eq = AccessPath.Raw.equal lhs_ap rhs_ap in if not eq && Config.debug_exceptions then failwithf "Id %a maps to both %a and %a@." Var.pp id - AccessPath.pp_raw lhs_ap - AccessPath.pp_raw rhs_ap; + AccessPath.Raw.pp lhs_ap + AccessPath.Raw.pp rhs_ap; eq) lhs with Not_found -> false @@ -45,12 +45,12 @@ let check_invariant ap1 ap2 = function (* TODO: fix (13370224) *) () | id -> - if not (AccessPath.equal_raw ap1 ap2) + if not (AccessPath.Raw.equal ap1 ap2) then failwithf "Id %a maps to both %a and %a@." Var.pp id - AccessPath.pp_raw ap1 - AccessPath.pp_raw ap2 + AccessPath.Raw.pp ap1 + AccessPath.Raw.pp ap2 let join astate1 astate2 = if phys_equal astate1 astate2 diff --git a/infer/src/checkers/IdAccessPathMapDomain.mli b/infer/src/checkers/IdAccessPathMapDomain.mli index 622ba359a..72a18e583 100644 --- a/infer/src/checkers/IdAccessPathMapDomain.mli +++ b/infer/src/checkers/IdAccessPathMapDomain.mli @@ -13,7 +13,7 @@ open! IStd module IdMap = Var.Map -type astate = AccessPath.raw IdMap.t +type astate = AccessPath.Raw.t IdMap.t include (module type of IdMap) diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml index df0d74940..894b7cda4 100644 --- a/infer/src/checkers/ThreadSafetyDomain.ml +++ b/infer/src/checkers/ThreadSafetyDomain.ml @@ -11,19 +11,10 @@ open! IStd module F = Format -module RawAccessPath = struct - type t = AccessPath.raw - let compare = AccessPath.compare_raw - let pp = AccessPath.pp_raw - let pp_element = pp -end - -module RawAccessPathSet = PrettyPrintable.MakePPSet(RawAccessPath) - -module OwnershipDomain = AbstractDomain.InvertedSet(RawAccessPathSet) +module OwnershipDomain = AbstractDomain.InvertedSet(AccessPath.RawSet) module TraceElem = struct - module Kind = RawAccessPath + module Kind = AccessPath.Raw type t = { site : CallSite.t; diff --git a/infer/src/checkers/ThreadSafetyDomain.mli b/infer/src/checkers/ThreadSafetyDomain.mli index 112dbf259..a2e2b17a9 100644 --- a/infer/src/checkers/ThreadSafetyDomain.mli +++ b/infer/src/checkers/ThreadSafetyDomain.mli @@ -11,18 +11,9 @@ open! IStd module F = Format -module RawAccessPath : sig - type t = AccessPath.raw - val compare : t -> t -> int - val pp : Format.formatter -> t -> unit - val pp_element : Format.formatter -> t -> unit -end +module OwnershipDomain : module type of AbstractDomain.InvertedSet (AccessPath.RawSet) -module RawAccessPathSet : PrettyPrintable.PPSet with type elt = RawAccessPath.t - -module OwnershipDomain : module type of AbstractDomain.InvertedSet (RawAccessPathSet) - -module TraceElem : TraceElem.S with module Kind = RawAccessPath +module TraceElem : TraceElem.S with module Kind = AccessPath.Raw (** A bool that is true if a lock is definitely held. Note that this is unsound because it assumes the existence of one global lock. In the case that a lock is held on the access to a variable, @@ -74,6 +65,6 @@ type summary = include AbstractDomain.WithBottom with type astate := astate -val make_access : RawAccessPath.t -> Location.t -> TraceElem.t +val make_access : AccessPath.Raw.t -> Location.t -> TraceElem.t val pp_summary : F.formatter -> summary -> unit diff --git a/infer/src/checkers/accessPath.ml b/infer/src/checkers/accessPath.ml index 63ecded86..19c7746ab 100644 --- a/infer/src/checkers/accessPath.ml +++ b/infer/src/checkers/accessPath.ml @@ -26,13 +26,29 @@ type access = let equal_access = [%compare.equal : access] -type raw = base * access list [@@deriving compare] +let pp_base fmt (pvar, _) = + Var.pp fmt pvar -let equal_raw = [%compare.equal : raw] +let pp_access fmt = function + | FieldAccess (field_name, _) -> Ident.pp_fieldname fmt field_name + | ArrayAccess _ -> F.fprintf fmt "[_]" + +let pp_access_list fmt accesses = + let pp_sep _ _ = F.fprintf fmt "." in + F.pp_print_list ~pp_sep pp_access fmt accesses + +module Raw = struct + type t = base * access list [@@deriving compare] + let equal = [%compare.equal : t] + + let pp fmt = function + | base, [] -> pp_base fmt base + | base, accesses -> F.fprintf fmt "%a.%a" pp_base base pp_access_list accesses +end type t = - | Abstracted of raw - | Exact of raw + | Abstracted of Raw.t + | Exact of Raw.t [@@deriving compare] let equal = [%compare.equal : t] @@ -49,7 +65,7 @@ let of_pvar pvar typ = let of_id id typ = base_of_id id typ, [] -let of_exp exp0 typ0 ~(f_resolve_id : Var.t -> raw option) = +let of_exp exp0 typ0 ~(f_resolve_id : Var.t -> Raw.t option) = (* [typ] is the type of the last element of the access path (e.g., typeof(g) for x.f.g) *) let rec of_exp_ exp typ accesses acc = match exp with @@ -88,7 +104,7 @@ let of_exp exp0 typ0 ~(f_resolve_id : Var.t -> raw option) = acc in of_exp_ exp0 typ0 [] [] -let of_lhs_exp lhs_exp typ ~(f_resolve_id : Var.t -> raw option) = +let of_lhs_exp lhs_exp typ ~(f_resolve_id : Var.t -> Raw.t option) = match of_exp lhs_exp typ ~f_resolve_id with | [lhs_ap] -> Some lhs_ap | _ -> None @@ -125,27 +141,12 @@ let is_exact = function let (<=) ~lhs ~rhs = match lhs, rhs with | Abstracted _, Exact _ -> false - | Exact lhs_ap, Exact rhs_ap -> equal_raw lhs_ap rhs_ap + | Exact lhs_ap, Exact rhs_ap -> Raw.equal lhs_ap rhs_ap | (Exact lhs_ap | Abstracted lhs_ap), Abstracted rhs_ap -> is_prefix rhs_ap lhs_ap -let pp_base fmt (pvar, _) = - Var.pp fmt pvar - -let pp_access fmt = function - | FieldAccess (field_name, _) -> Ident.pp_fieldname fmt field_name - | ArrayAccess _ -> F.fprintf fmt "[_]" - -let pp_access_list fmt accesses = - let pp_sep _ _ = F.fprintf fmt "." in - F.pp_print_list ~pp_sep pp_access fmt accesses - -let pp_raw fmt = function - | base, [] -> pp_base fmt base - | base, accesses -> F.fprintf fmt "%a.%a" pp_base base pp_access_list accesses - let pp fmt = function - | Exact access_path -> pp_raw fmt access_path - | Abstracted access_path -> F.fprintf fmt "%a*" pp_raw access_path + | Exact access_path -> Raw.pp fmt access_path + | Abstracted access_path -> F.fprintf fmt "%a*" Raw.pp access_path module BaseMap = PrettyPrintable.MakePPMap(struct type t = base @@ -158,3 +159,9 @@ module AccessMap = PrettyPrintable.MakePPMap(struct let compare = compare_access let pp_key = pp_access end) + +module RawSet = PrettyPrintable.MakePPSet(struct + type t = Raw.t + let compare = Raw.compare + let pp_element = Raw.pp + end) diff --git a/infer/src/checkers/accessPath.mli b/infer/src/checkers/accessPath.mli index b196ce72c..b65ba3ef1 100644 --- a/infer/src/checkers/accessPath.mli +++ b/infer/src/checkers/accessPath.mli @@ -18,21 +18,24 @@ type access = | FieldAccess of Ident.fieldname * Typ.t (* field name * field type *) [@@deriving compare] -(** root var, and a list of accesses. closest to the root var is first that is, x.f.g is represented - as (x, [f; g]) *) -type raw = base * access list [@@deriving compare] +module Raw : sig + (** root var, and a list of accesses. closest to the root var is first that is, x.f.g is + representedas (x, [f; g]) *) + type t = base * access list [@@deriving compare] + + val equal : t -> t -> bool + val pp : Format.formatter -> t -> unit +end type t = - | Abstracted of raw (** abstraction of heap reachable from an access path, e.g. x.f* *) - | Exact of raw (** precise representation of an access path, e.g. x.f.g *) + | Abstracted of Raw.t (** abstraction of heap reachable from an access path, e.g. x.f* *) + | Exact of Raw.t (** precise representation of an access path, e.g. x.f.g *) [@@deriving compare] val equal_base : base -> base -> bool val equal_access : access -> access -> bool -val equal_raw : raw -> raw -> bool - val equal : t -> t -> bool (** create a base from a pvar *) @@ -42,36 +45,34 @@ val base_of_pvar : Pvar.t -> Typ.t -> base val base_of_id : Ident.t -> Typ.t -> base (** create an access path from a pvar *) -val of_pvar : Pvar.t -> Typ.t -> raw +val of_pvar : Pvar.t -> Typ.t -> Raw.t (** create an access path from an ident *) -val of_id : Ident.t -> Typ.t -> raw +val of_id : Ident.t -> Typ.t -> Raw.t (** extract the raw access paths that occur in [exp], resolving identifiers using [f_resolve_id] *) -val of_exp : Exp.t -> Typ.t -> f_resolve_id:(Var.t -> raw option) -> raw list +val of_exp : Exp.t -> Typ.t -> f_resolve_id:(Var.t -> Raw.t option) -> Raw.t list (** convert [lhs_exp] to a raw access path, resolving identifiers using [f_resolve_id] *) -val of_lhs_exp : Exp.t -> Typ.t -> f_resolve_id:(Var.t -> raw option) -> raw option +val of_lhs_exp : Exp.t -> Typ.t -> f_resolve_id:(Var.t -> Raw.t option) -> Raw.t option (** append new accesses to an existing access path; e.g., `append_access x.f [g, h]` produces `x.f.g.h` *) -val append : raw -> access list -> raw +val append : Raw.t -> access list -> Raw.t (** swap base of existing access path for [base_var] (e.g., `with_base_bvar x y.f.g` produces `x.f.g` *) val with_base_var : Var.t -> t -> t (** return true if [ap1] is a prefix of [ap2]. returns true for equal access paths *) -val is_prefix : raw -> raw -> bool +val is_prefix : Raw.t -> Raw.t -> bool val pp_access : Format.formatter -> access -> unit val pp_access_list : Format.formatter -> access list -> unit -val pp_raw : Format.formatter -> raw -> unit - (** extract a raw access path from its wrapper *) -val extract : t -> raw +val extract : t -> Raw.t (** return true if [t] is an exact representation of an access path, false if it's an abstraction *) val is_exact : t -> bool @@ -86,3 +87,5 @@ val pp : Format.formatter -> t -> unit module BaseMap : PrettyPrintable.PPMap with type key = base module AccessMap : PrettyPrintable.PPMap with type key = access + +module RawSet : PrettyPrintable.PPSet with type elt = Raw.t diff --git a/infer/src/unit/accessPathTestUtils.mli b/infer/src/unit/accessPathTestUtils.mli index cbbf91bb9..b4ffefcea 100644 --- a/infer/src/unit/accessPathTestUtils.mli +++ b/infer/src/unit/accessPathTestUtils.mli @@ -17,4 +17,4 @@ val make_field_access : string -> AccessPath.access val make_array_access : Typ.t -> AccessPath.access -val make_access_path : string -> string list -> AccessPath.raw +val make_access_path : string -> string list -> AccessPath.Raw.t diff --git a/infer/src/unit/accessPathTests.ml b/infer/src/unit/accessPathTests.ml index d65f1c74d..352f27f2a 100644 --- a/infer/src/unit/accessPathTests.ml +++ b/infer/src/unit/accessPathTests.ml @@ -37,12 +37,12 @@ let tests = let open OUnit2 in let equal_test = let equal_test_ _ = - assert_bool "equal works for bases" (AccessPath.equal_raw x (make_access_path "x" [])); + assert_bool "equal works for bases" (AccessPath.Raw.equal x (make_access_path "x" [])); assert_bool "equal works for paths" - (AccessPath.equal_raw xFG (make_access_path "x" ["f"; "g";])); - assert_bool "disequality works for bases" (not (AccessPath.equal_raw x y)); - assert_bool "disequality works for paths" (not (AccessPath.equal_raw xF xFG)) in + (AccessPath.Raw.equal xFG (make_access_path "x" ["f"; "g";])); + assert_bool "disequality works for bases" (not (AccessPath.Raw.equal x y)); + assert_bool "disequality works for paths" (not (AccessPath.Raw.equal xF xFG)) in "equal">::equal_test_ in let append_test = @@ -50,10 +50,10 @@ let tests = F.fprintf fmt "Expected output %a but got %a" - AccessPath.pp_raw expected - AccessPath.pp_raw actual in + AccessPath.Raw.pp expected + AccessPath.Raw.pp actual in let assert_eq input expected = - assert_equal ~cmp:AccessPath.equal_raw ~pp_diff input expected in + assert_equal ~cmp:AccessPath.Raw.equal ~pp_diff input expected in let append_test_ _ = assert_eq xF (AccessPath.append x [f_access]); assert_eq xFG (AccessPath.append xF [g_access]) in @@ -86,10 +86,10 @@ let tests = F.fprintf fmt "Expected to make access path %a from expression %a, but got %a" - AccessPath.pp_raw expected_ap + AccessPath.Raw.pp expected_ap Exp.pp exp - AccessPath.pp_raw actual_ap in - assert_equal ~cmp:AccessPath.equal_raw ~pp_diff actual_ap expected_ap in + AccessPath.Raw.pp actual_ap in + assert_equal ~cmp:AccessPath.Raw.equal ~pp_diff actual_ap expected_ap in let of_exp_test_ _ = let f_fieldname = make_fieldname "f" in @@ -112,16 +112,16 @@ let tests = let binop_exp = Exp.le xF_exp xFG_exp in match AccessPath.of_exp binop_exp dummy_typ ~f_resolve_id with | [ap1; ap2] -> - assert_equal ~cmp:AccessPath.equal_raw ap1 xFG; - assert_equal ~cmp:AccessPath.equal_raw ap2 xF; + assert_equal ~cmp:AccessPath.Raw.equal ap1 xFG; + assert_equal ~cmp:AccessPath.Raw.equal ap2 xF; | _ -> assert false; - () in + () in "of_exp">::of_exp_test_ in let abstraction_test = let abstraction_test_ _ = - assert_bool "extract" (AccessPath.equal_raw (AccessPath.extract xF_exact) xF); + assert_bool "extract" (AccessPath.Raw.equal (AccessPath.extract xF_exact) xF); assert_bool "is_exact" (AccessPath.is_exact x_exact); assert_bool "not is_exact" (not (AccessPath.is_exact x_abstract)); assert_bool "(<=)1" (AccessPath.(<=) ~lhs:x_exact ~rhs:x_abstract);