|
|
@ -11,19 +11,16 @@ open! IStd
|
|
|
|
|
|
|
|
|
|
|
|
module F = Format
|
|
|
|
module F = Format
|
|
|
|
|
|
|
|
|
|
|
|
type _array_sensitive_typ = Typ.t
|
|
|
|
type _typ = Typ.t
|
|
|
|
|
|
|
|
|
|
|
|
let compare__array_sensitive_typ = Typ.array_sensitive_compare
|
|
|
|
let compare__typ _ _ = 0
|
|
|
|
|
|
|
|
|
|
|
|
type base = Var.t * _array_sensitive_typ [@@deriving compare]
|
|
|
|
(* ignore types while comparing bases. we can't trust the types from all of our frontends to be
|
|
|
|
|
|
|
|
consistent, and the variable names should already be enough to distinguish the bases. *)
|
|
|
|
|
|
|
|
type base = Var.t * _typ [@@deriving compare]
|
|
|
|
|
|
|
|
|
|
|
|
let equal_base = [%compare.equal : base]
|
|
|
|
let equal_base = [%compare.equal : base]
|
|
|
|
|
|
|
|
|
|
|
|
let compare_base_untyped (base_var1, _) (base_var2, _) =
|
|
|
|
|
|
|
|
if phys_equal base_var1 base_var2
|
|
|
|
|
|
|
|
then 0
|
|
|
|
|
|
|
|
else Var.compare base_var1 base_var2
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
type access =
|
|
|
|
type access =
|
|
|
|
| ArrayAccess of Typ.t
|
|
|
|
| ArrayAccess of Typ.t
|
|
|
|
| FieldAccess of Fieldname.t
|
|
|
|
| FieldAccess of Fieldname.t
|
|
|
@ -31,7 +28,6 @@ type access =
|
|
|
|
|
|
|
|
|
|
|
|
let equal_access = [%compare.equal : access]
|
|
|
|
let equal_access = [%compare.equal : access]
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let equal_access_list l1 l2 = Int.equal (List.compare compare_access l1 l2) 0
|
|
|
|
let equal_access_list l1 l2 = Int.equal (List.compare compare_access l1 l2) 0
|
|
|
|
|
|
|
|
|
|
|
|
let pp_base fmt (pvar, _) =
|
|
|
|
let pp_base fmt (pvar, _) =
|
|
|
@ -74,22 +70,6 @@ module Raw = struct
|
|
|
|
| base, accesses -> F.fprintf fmt "%a.%a" pp_base base pp_access_list accesses
|
|
|
|
| base, accesses -> F.fprintf fmt "%a.%a" pp_base base pp_access_list accesses
|
|
|
|
end
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
|
|
module UntypedRaw = struct
|
|
|
|
|
|
|
|
type t = Raw.t
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(* untyped comparison *)
|
|
|
|
|
|
|
|
let compare ((base1, accesses1) as raw1) ((base2, accesses2) as raw2) =
|
|
|
|
|
|
|
|
if phys_equal raw1 raw2
|
|
|
|
|
|
|
|
then
|
|
|
|
|
|
|
|
0
|
|
|
|
|
|
|
|
else
|
|
|
|
|
|
|
|
let n = compare_base_untyped base1 base2 in
|
|
|
|
|
|
|
|
if n <> 0 then n
|
|
|
|
|
|
|
|
else List.compare compare_access accesses1 accesses2
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
let pp = Raw.pp
|
|
|
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
type t =
|
|
|
|
type t =
|
|
|
|
| Abstracted of Raw.t
|
|
|
|
| Abstracted of Raw.t
|
|
|
|
| Exact of Raw.t
|
|
|
|
| Exact of Raw.t
|
|
|
@ -207,7 +187,3 @@ module AccessMap = PrettyPrintable.MakePPMap(struct
|
|
|
|
module RawSet = PrettyPrintable.MakePPSet(Raw)
|
|
|
|
module RawSet = PrettyPrintable.MakePPSet(Raw)
|
|
|
|
|
|
|
|
|
|
|
|
module RawMap = PrettyPrintable.MakePPMap(Raw)
|
|
|
|
module RawMap = PrettyPrintable.MakePPMap(Raw)
|
|
|
|
|
|
|
|
|
|
|
|
module UntypedRawSet = PrettyPrintable.MakePPSet(UntypedRaw)
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
module UntypedRawMap = PrettyPrintable.MakePPMap(UntypedRaw)
|
|
|
|
|
|
|
|