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

[cleanup] give AccessPath.raw its own module

Browse Source 
Summary: This allows us to simplify ThreadSafetyDomain a bit.

Reviewed By: jberdine

Differential Revision: D4452740

fbshipit-source-id: 76fce02
master
Sam Blackshear 8 years ago committed by Facebook Github Bot
parent 4b45d5d8a0
commit df5798336b
8 changed files with 79 additions and 87 deletions
Show Stats Download Patch File Download Diff File

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

@ -11,12 +11,12 @@ open! IStd
module IdMap = Var.Map module IdMap = Var.Map
type astate = AccessPath.raw IdMap.t type astate = AccessPath.Raw.t IdMap.t
include IdMap include IdMap
let pp fmt astate = 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 = let (<=) ~lhs ~rhs =
if phys_equal lhs rhs if phys_equal lhs rhs
@ -26,13 +26,13 @@ let (<=) ~lhs ~rhs =
IdMap.for_all IdMap.for_all
(fun id lhs_ap -> (fun id lhs_ap ->
let rhs_ap = IdMap.find id rhs in 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 if not eq && Config.debug_exceptions
then then
failwithf "Id %a maps to both %a and %a@." failwithf "Id %a maps to both %a and %a@."
Var.pp id Var.pp id
AccessPath.pp_raw lhs_ap AccessPath.Raw.pp lhs_ap
AccessPath.pp_raw rhs_ap; AccessPath.Raw.pp rhs_ap;
eq) eq)
lhs lhs
with Not_found -> false with Not_found -> false
@ -45,12 +45,12 @@ let check_invariant ap1 ap2 = function
(* TODO: fix (13370224) *) (* TODO: fix (13370224) *)
() ()
| id -> | id ->
if not (AccessPath.equal_raw ap1 ap2) if not (AccessPath.Raw.equal ap1 ap2)
then then
failwithf "Id %a maps to both %a and %a@." failwithf "Id %a maps to both %a and %a@."
Var.pp id Var.pp id
AccessPath.pp_raw ap1 AccessPath.Raw.pp ap1
AccessPath.pp_raw ap2 AccessPath.Raw.pp ap2
let join astate1 astate2 = let join astate1 astate2 =
if phys_equal astate1 astate2 if phys_equal astate1 astate2

2
infer/src/checkers/IdAccessPathMapDomain.mli
Unescape View File

@ -13,7 +13,7 @@ open! IStd
module IdMap = Var.Map module IdMap = Var.Map
type astate = AccessPath.raw IdMap.t type astate = AccessPath.Raw.t IdMap.t
include (module type of IdMap) include (module type of IdMap)

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

@ -11,19 +11,10 @@ open! IStd
module F = Format module F = Format
module RawAccessPath = struct module OwnershipDomain = AbstractDomain.InvertedSet(AccessPath.RawSet)
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 TraceElem = struct module TraceElem = struct
module Kind = RawAccessPath module Kind = AccessPath.Raw
type t = { type t = {
site : CallSite.t; site : CallSite.t;

15
infer/src/checkers/ThreadSafetyDomain.mli
Unescape View File

@ -11,18 +11,9 @@ open! IStd
module F = Format module F = Format
module RawAccessPath : sig module OwnershipDomain : module type of AbstractDomain.InvertedSet (AccessPath.RawSet)
type t = AccessPath.raw
val compare : t -> t -> int
val pp : Format.formatter -> t -> unit
val pp_element : Format.formatter -> t -> unit
end
module RawAccessPathSet : PrettyPrintable.PPSet with type elt = RawAccessPath.t module TraceElem : TraceElem.S with module Kind = AccessPath.Raw
module OwnershipDomain : module type of AbstractDomain.InvertedSet (RawAccessPathSet)
module TraceElem : TraceElem.S with module Kind = RawAccessPath
(** A bool that is true if a lock is definitely held. Note that this is unsound because it assumes (** 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, 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 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 val pp_summary : F.formatter -> summary -> unit

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

@ -26,13 +26,29 @@ type access =
let equal_access = [%compare.equal : 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 = type t =
| Abstracted of raw | Abstracted of Raw.t
| Exact of raw | Exact of Raw.t
[@@deriving compare] [@@deriving compare]
let equal = [%compare.equal : t] let equal = [%compare.equal : t]
@ -49,7 +65,7 @@ let of_pvar pvar typ =
let of_id id typ = let of_id id typ =
base_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) *) (* [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 = let rec of_exp_ exp typ accesses acc =
match exp with match exp with
@ -88,7 +104,7 @@ let of_exp exp0 typ0 ~(f_resolve_id : Var.t -> raw option) =
acc in acc in
of_exp_ exp0 typ0 [] [] 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 match of_exp lhs_exp typ ~f_resolve_id with
| [lhs_ap] -> Some lhs_ap | [lhs_ap] -> Some lhs_ap
| _ -> None | _ -> None
@ -125,27 +141,12 @@ let is_exact = function
let (<=) ~lhs ~rhs = let (<=) ~lhs ~rhs =
match lhs, rhs with match lhs, rhs with
| Abstracted _, Exact _ -> false | 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 | (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 let pp fmt = function
| Exact access_path -> pp_raw fmt access_path | Exact access_path -> Raw.pp fmt access_path
| Abstracted access_path -> F.fprintf fmt "%a*" pp_raw access_path | Abstracted access_path -> F.fprintf fmt "%a*" Raw.pp access_path
module BaseMap = PrettyPrintable.MakePPMap(struct module BaseMap = PrettyPrintable.MakePPMap(struct
type t = base type t = base
@ -158,3 +159,9 @@ module AccessMap = PrettyPrintable.MakePPMap(struct
let compare = compare_access let compare = compare_access
let pp_key = pp_access let pp_key = pp_access
end) end)
module RawSet = PrettyPrintable.MakePPSet(struct
type t = Raw.t
let compare = Raw.compare
let pp_element = Raw.pp
end)

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

@ -18,21 +18,24 @@ type access =
| FieldAccess of Ident.fieldname * Typ.t (* field name * field type *) | FieldAccess of Ident.fieldname * Typ.t (* field name * field type *)
[@@deriving compare] [@@deriving compare]
(** root var, and a list of accesses. closest to the root var is first that is, x.f.g is represented module Raw : sig
as (x, [f; g]) *) (** root var, and a list of accesses. closest to the root var is first that is, x.f.g is
type raw = base * access list [@@deriving compare] 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 = type t =
| Abstracted of raw (** abstraction of heap reachable from an access path, e.g. x.f* *) | Abstracted of Raw.t (** 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 *) | Exact of Raw.t (** precise representation of an access path, e.g. x.f.g *)
[@@deriving compare] [@@deriving compare]
val equal_base : base -> base -> bool val equal_base : base -> base -> bool
val equal_access : access -> access -> bool val equal_access : access -> access -> bool
val equal_raw : raw -> raw -> bool
val equal : t -> t -> bool val equal : t -> t -> bool
(** create a base from a pvar *) (** 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 val base_of_id : Ident.t -> Typ.t -> base
(** create an access path from a pvar *) (** 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 *) (** 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] *) (** 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] *) (** 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 (** append new accesses to an existing access path; e.g., `append_access x.f [g, h]` produces
`x.f.g.h` *) `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 (** swap base of existing access path for [base_var] (e.g., `with_base_bvar x y.f.g` produces
`x.f.g` *) `x.f.g` *)
val with_base_var : Var.t -> t -> t val with_base_var : Var.t -> t -> t
(** return true if [ap1] is a prefix of [ap2]. returns true for equal access paths *) (** 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 : Format.formatter -> access -> unit
val pp_access_list : Format.formatter -> access list -> 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 *) (** 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 *) (** return true if [t] is an exact representation of an access path, false if it's an abstraction *)
val is_exact : t -> bool val is_exact : t -> bool
@ -86,3 +87,5 @@ val pp : Format.formatter -> t -> unit
module BaseMap : PrettyPrintable.PPMap with type key = base module BaseMap : PrettyPrintable.PPMap with type key = base
module AccessMap : PrettyPrintable.PPMap with type key = access module AccessMap : PrettyPrintable.PPMap with type key = access
module RawSet : PrettyPrintable.PPSet with type elt = Raw.t

2
infer/src/unit/accessPathTestUtils.mli
Unescape View File

@ -17,4 +17,4 @@ val make_field_access : string -> AccessPath.access
val make_array_access : Typ.t -> 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

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

@ -37,12 +37,12 @@ let tests =
let open OUnit2 in let open OUnit2 in
let equal_test = let equal_test =
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 assert_bool
"equal works for paths" "equal works for paths"
(AccessPath.equal_raw xFG (make_access_path "x" ["f"; "g";])); (AccessPath.Raw.equal xFG (make_access_path "x" ["f"; "g";]));
assert_bool "disequality works for bases" (not (AccessPath.equal_raw x y)); assert_bool "disequality works for bases" (not (AccessPath.Raw.equal x y));
assert_bool "disequality works for paths" (not (AccessPath.equal_raw xF xFG)) in assert_bool "disequality works for paths" (not (AccessPath.Raw.equal xF xFG)) in
"equal">::equal_test_ in "equal">::equal_test_ in
let append_test = let append_test =
@ -50,10 +50,10 @@ let tests =
F.fprintf F.fprintf
fmt fmt
"Expected output %a but got %a" "Expected output %a but got %a"
AccessPath.pp_raw expected AccessPath.Raw.pp expected
AccessPath.pp_raw actual in AccessPath.Raw.pp actual in
let assert_eq input expected = 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_ _ = let append_test_ _ =
assert_eq xF (AccessPath.append x [f_access]); assert_eq xF (AccessPath.append x [f_access]);
assert_eq xFG (AccessPath.append xF [g_access]) in assert_eq xFG (AccessPath.append xF [g_access]) in
@ -86,10 +86,10 @@ let tests =
F.fprintf F.fprintf
fmt fmt
"Expected to make access path %a from expression %a, but got %a" "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 Exp.pp exp
AccessPath.pp_raw actual_ap in AccessPath.Raw.pp actual_ap in
assert_equal ~cmp:AccessPath.equal_raw ~pp_diff actual_ap expected_ap in assert_equal ~cmp:AccessPath.Raw.equal ~pp_diff actual_ap expected_ap in
let of_exp_test_ _ = let of_exp_test_ _ =
let f_fieldname = make_fieldname "f" in let f_fieldname = make_fieldname "f" in
@ -112,8 +112,8 @@ let tests =
let binop_exp = Exp.le xF_exp xFG_exp in let binop_exp = Exp.le xF_exp xFG_exp in
match AccessPath.of_exp binop_exp dummy_typ ~f_resolve_id with match AccessPath.of_exp binop_exp dummy_typ ~f_resolve_id with
| [ap1; ap2] -> | [ap1; ap2] ->
assert_equal ~cmp:AccessPath.equal_raw ap1 xFG; assert_equal ~cmp:AccessPath.Raw.equal ap1 xFG;
assert_equal ~cmp:AccessPath.equal_raw ap2 xF; assert_equal ~cmp:AccessPath.Raw.equal ap2 xF;
| _ -> | _ ->
assert false; assert false;
() in () in
@ -121,7 +121,7 @@ let tests =
let abstraction_test = let abstraction_test =
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 "is_exact" (AccessPath.is_exact x_exact);
assert_bool "not is_exact" (not (AccessPath.is_exact x_abstract)); assert_bool "not is_exact" (not (AccessPath.is_exact x_abstract));
assert_bool "(<=)1" (AccessPath.(<=) ~lhs:x_exact ~rhs:x_abstract); assert_bool "(<=)1" (AccessPath.(<=) ~lhs:x_exact ~rhs:x_abstract);

Write Preview
Loading…
Cancel
Save