pghs975uc
/
infer_clone
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

ppx_compare AccessPath

Browse Source 
Reviewed By: cristianoc

Differential Revision: D4232397

fbshipit-source-id: a72717b
master
Josh Berdine 8 years ago committed by Facebook Github Bot
parent 9bc72ad790
commit 356d081e1f
5 changed files with 46 additions and 92 deletions
Show Stats Download Patch File Download Diff File

4
infer/src/checkers/IdAccessPathMapDomain.ml
Unescape View File

@ -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

2
infer/src/checkers/ThreadSafetyDomain.ml
Unescape View File

@ -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)

88
infer/src/checkers/accessPath.ml
Unescape View File

@ -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)

26
infer/src/checkers/accessPath.mli
Unescape View File

@ -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

18
infer/src/unit/accessPathTests.ml
Unescape View File

@ -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);

Write Preview
Loading…
Cancel
Save