From 356d081e1fb099c89575ff50ce30d8fee385e2f3 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Tue, 29 Nov 2016 16:38:21 -0800 Subject: [PATCH] ppx_compare AccessPath Reviewed By: cristianoc Differential Revision: D4232397 fbshipit-source-id: a72717b --- infer/src/checkers/IdAccessPathMapDomain.ml | 4 +- infer/src/checkers/ThreadSafetyDomain.ml | 2 +- infer/src/checkers/accessPath.ml | 88 ++++++--------------- infer/src/checkers/accessPath.mli | 26 +++--- infer/src/unit/accessPathTests.ml | 18 ++--- 5 files changed, 46 insertions(+), 92 deletions(-) diff --git a/infer/src/checkers/IdAccessPathMapDomain.ml b/infer/src/checkers/IdAccessPathMapDomain.ml index dd5fed01a..a6bacfea1 100644 --- a/infer/src/checkers/IdAccessPathMapDomain.ml +++ b/infer/src/checkers/IdAccessPathMapDomain.ml @@ -30,7 +30,7 @@ let (<=) ~lhs ~rhs = IdMap.for_all (fun id lhs_ap -> let rhs_ap = IdMap.find id rhs in - let eq = AccessPath.raw_equal lhs_ap rhs_ap in + let eq = AccessPath.equal_raw lhs_ap rhs_ap in assert eq; eq) lhs @@ -51,7 +51,7 @@ let join astate1 astate2 = (* TODO: fix (13370224) *) () | _ -> - assert (AccessPath.raw_equal ap1 ap2) in + assert (AccessPath.equal_raw ap1 ap2) in check_invariant (); ap1_opt | Some _, None -> ap1_opt diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml index 92c5f1b4d..55ebf2875 100644 --- a/infer/src/checkers/ThreadSafetyDomain.ml +++ b/infer/src/checkers/ThreadSafetyDomain.ml @@ -8,7 +8,7 @@ *) module PPrawpath = PrettyPrintable.MakePPSet(struct type t = AccessPath.raw - let compare = AccessPath.raw_compare + let compare = AccessPath.compare_raw let pp_element = AccessPath.pp_raw end) diff --git a/infer/src/checkers/accessPath.ml b/infer/src/checkers/accessPath.ml index fced84744..20364c92b 100644 --- a/infer/src/checkers/accessPath.ml +++ b/infer/src/checkers/accessPath.ml @@ -11,72 +11,32 @@ open! Utils module F = Format -type base = Var.t * Typ.t +type _array_sensitive_typ = Typ.t + +let compare__array_sensitive_typ = Typ.array_sensitive_compare + +type base = Var.t * _array_sensitive_typ [@@deriving compare] + +let equal_base base1 base2 = + compare_base base1 base2 = 0 type access = - | FieldAccess of Ident.fieldname * Typ.t | ArrayAccess of Typ.t + | FieldAccess of Ident.fieldname * Typ.t +[@@deriving compare] -type raw = base * access list - -type t = - | Exact of raw - | Abstracted of raw +let equal_access access1 access2 = + compare_access access1 access2 = 0 -let base_compare ((var1, typ1) as base1) ((var2, typ2) as base2) = - if base1 == base2 - then 0 - else - let n = Var.compare var1 var2 in - if n <> 0 - then n - else Typ.array_sensitive_compare typ1 typ2 - -let base_equal base1 base2 = - base_compare base1 base2 = 0 - -let access_compare access1 access2 = - if access1 == access2 - then - 0 - else - match access1, access2 with - | FieldAccess (f1, typ1), FieldAccess (f2, typ2) -> - let n = Ident.compare_fieldname f1 f2 in - if n <> 0 - then n - else Typ.compare typ1 typ2 - | ArrayAccess typ1, ArrayAccess typ2 -> - Typ.compare typ1 typ2 - | FieldAccess _, _ -> 1 - | _, FieldAccess _ -> -1 - -let access_equal access1 access2 = - access_compare access1 access2 = 0 - -let raw_compare ((base1, accesses1) as ap1) ((base2, accesses2) as ap2) = - if ap1 == ap2 - then 0 - else - let n = base_compare base1 base2 in - if n <> 0 - then n - else if accesses1 == accesses2 - then 0 - else IList.compare access_compare accesses1 accesses2 +type raw = base * access list [@@deriving compare] -let raw_equal ap1 ap2 = - raw_compare ap1 ap2 = 0 +let equal_raw ap1 ap2 = + compare_raw ap1 ap2 = 0 -let compare ap1 ap2 = - if ap1 == ap2 - then - 0 - else - match ap1, ap2 with - | Exact ap1, Exact ap2 | Abstracted ap1, Abstracted ap2 -> raw_compare ap1 ap2 - | Exact _, Abstracted _ -> 1 - | Abstracted _, Exact _ -> (-1) +type t = + | Abstracted of raw + | Exact of raw +[@@deriving compare] let equal ap1 ap2 = compare ap1 ap2 = 0 @@ -151,13 +111,13 @@ let rec is_prefix_path path1 path2 = match path1, path2 with | [], _ -> true | _, [] -> false - | access1 :: p1, access2 :: p2 -> access_equal access1 access2 && is_prefix_path p1 p2 + | access1 :: p1, access2 :: p2 -> equal_access access1 access2 && is_prefix_path p1 p2 let is_prefix ((base1, path1) as ap1) ((base2, path2) as ap2) = if ap1 == ap2 then true else - base_equal base1 base2 && is_prefix_path path1 path2 + equal_base base1 base2 && is_prefix_path path1 path2 let extract = function | Exact ap | Abstracted ap -> ap @@ -169,7 +129,7 @@ let is_exact = function let (<=) ~lhs ~rhs = match lhs, rhs with | Abstracted _, Exact _ -> false - | Exact lhs_ap, Exact rhs_ap -> raw_equal lhs_ap rhs_ap + | Exact lhs_ap, Exact rhs_ap -> equal_raw lhs_ap rhs_ap | (Exact lhs_ap | Abstracted lhs_ap), Abstracted rhs_ap -> is_prefix rhs_ap lhs_ap let pp_base fmt (pvar, _) = @@ -193,12 +153,12 @@ let pp fmt = function module BaseMap = PrettyPrintable.MakePPMap(struct type t = base - let compare = base_compare + let compare = compare_base let pp_key = pp_base end) module AccessMap = PrettyPrintable.MakePPMap(struct type t = access - let compare = access_compare + let compare = compare_access let pp_key = pp_access end) diff --git a/infer/src/checkers/accessPath.mli b/infer/src/checkers/accessPath.mli index 1d8fd179b..e883a8e16 100644 --- a/infer/src/checkers/accessPath.mli +++ b/infer/src/checkers/accessPath.mli @@ -9,31 +9,29 @@ (** Module for naming heap locations via the path used to access them (e.g., x.f.g, y[a].b) *) -type base = Var.t * Typ.t +type base = Var.t * Typ.t [@@deriving compare] type access = - | FieldAccess of Ident.fieldname * Typ.t (* field name * field type *) | ArrayAccess of Typ.t (* array element type. index is unknown *) + | 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 +type raw = base * access list [@@deriving compare] type t = - | Exact of raw (** precise representation of an access path, e.g. x.f.g *) | 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 *) +[@@deriving compare] -val base_compare : base -> base -> int - -val base_equal : base -> base -> bool - -val raw_compare : raw -> raw -> int +val equal_base : base -> base -> bool -val raw_equal : raw -> raw -> bool +val equal_access : access -> access -> bool -val access_compare : access -> access -> int +val equal_raw : raw -> raw -> bool -val access_equal : access -> access -> bool +val equal : t -> t -> bool (** create a base from a pvar *) val base_of_pvar : Pvar.t -> Typ.t -> base @@ -70,10 +68,6 @@ val pp_access_list : Format.formatter -> access list -> unit val pp_raw : Format.formatter -> raw -> unit -val compare : t -> t -> int - -val equal : t -> t -> bool - (** extract a raw access path from its wrapper *) val extract : t -> raw diff --git a/infer/src/unit/accessPathTests.ml b/infer/src/unit/accessPathTests.ml index 014fddb9d..9843cb883 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.raw_equal x (make_access_path "x" [])); + assert_bool "equal works for bases" (AccessPath.equal_raw x (make_access_path "x" [])); assert_bool "equal works for paths" - (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 + (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 "equal">::equal_test_ in let append_test = @@ -53,7 +53,7 @@ let tests = AccessPath.pp_raw expected AccessPath.pp_raw actual in let assert_eq input expected = - assert_equal ~cmp:AccessPath.raw_equal ~pp_diff input expected in + assert_equal ~cmp:AccessPath.equal_raw ~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 @@ -89,7 +89,7 @@ let tests = AccessPath.pp_raw expected_ap Exp.pp exp AccessPath.pp_raw actual_ap in - assert_equal ~cmp:AccessPath.raw_equal ~pp_diff actual_ap expected_ap in + assert_equal ~cmp:AccessPath.equal_raw ~pp_diff actual_ap expected_ap in let of_exp_test_ _ = let f_fieldname = make_fieldname "f" in @@ -112,8 +112,8 @@ 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.raw_equal ap1 xFG; - assert_equal ~cmp:AccessPath.raw_equal ap2 xF; + assert_equal ~cmp:AccessPath.equal_raw ap1 xFG; + assert_equal ~cmp:AccessPath.equal_raw ap2 xF; | _ -> assert false; () in @@ -121,7 +121,7 @@ let tests = let abstraction_test = let abstraction_test_ _ = - assert_bool "extract" (AccessPath.raw_equal (AccessPath.extract xF_exact) xF); + assert_bool "extract" (AccessPath.equal_raw (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);