diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml index 76741c04c..3d9596af4 100644 --- a/infer/src/checkers/ThreadSafetyDomain.ml +++ b/infer/src/checkers/ThreadSafetyDomain.ml @@ -11,7 +11,7 @@ open! IStd module F = Format -module AccessPathSetDomain = AbstractDomain.InvertedSet(AccessPath.RawSet) +module AccessPathSetDomain = AbstractDomain.InvertedSet(AccessPath.UntypedRawSet) module TraceElem = struct module Kind = AccessPath.Raw @@ -74,7 +74,7 @@ end module AttributeSetDomain = AbstractDomain.InvertedSet (Attribute.Set) module AttributeMapDomain = struct - include AbstractDomain.InvertedMap (AccessPath.RawMap) (AttributeSetDomain) + include AbstractDomain.InvertedMap (AccessPath.UntypedRawMap) (AttributeSetDomain) let has_attribute access_path attribute t = try @@ -114,7 +114,7 @@ let empty = let conditional_writes = ConditionalWritesDomain.empty in let unconditional_writes = PathDomain.empty in let id_map = IdAccessPathMapDomain.empty in - let attribute_map = AccessPath.RawMap.empty in + let attribute_map = AccessPath.UntypedRawMap.empty in { locks; reads; conditional_writes; unconditional_writes; id_map; attribute_map; } let (<=) ~lhs ~rhs = diff --git a/infer/src/checkers/ThreadSafetyDomain.mli b/infer/src/checkers/ThreadSafetyDomain.mli index 83e80f581..cfe139fda 100644 --- a/infer/src/checkers/ThreadSafetyDomain.mli +++ b/infer/src/checkers/ThreadSafetyDomain.mli @@ -11,7 +11,7 @@ open! IStd module F = Format -module AccessPathSetDomain : module type of AbstractDomain.InvertedSet (AccessPath.RawSet) +module AccessPathSetDomain : module type of AbstractDomain.InvertedSet (AccessPath.UntypedRawSet) module TraceElem : TraceElem.S with module Kind = AccessPath.Raw @@ -47,7 +47,7 @@ end module AttributeSetDomain : module type of AbstractDomain.InvertedSet (Attribute.Set) module AttributeMapDomain : sig - include module type of AbstractDomain.InvertedMap (AccessPath.RawMap) (AttributeSetDomain) + include module type of AbstractDomain.InvertedMap (AccessPath.UntypedRawMap) (AttributeSetDomain) val has_attribute : AccessPath.Raw.t -> Attribute.t -> astate -> bool diff --git a/infer/src/checkers/accessPath.ml b/infer/src/checkers/accessPath.ml index e0187b976..4cf8c527e 100644 --- a/infer/src/checkers/accessPath.ml +++ b/infer/src/checkers/accessPath.ml @@ -19,6 +19,11 @@ type base = Var.t * _array_sensitive_typ [@@deriving compare] 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 = | ArrayAccess of Typ.t | FieldAccess of Ident.fieldname @@ -66,6 +71,22 @@ module Raw = struct | base, accesses -> F.fprintf fmt "%a.%a" pp_base base pp_access_list accesses 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 = | Abstracted of Raw.t | Exact of Raw.t @@ -183,3 +204,7 @@ module AccessMap = PrettyPrintable.MakePPMap(struct module RawSet = PrettyPrintable.MakePPSet(Raw) module RawMap = PrettyPrintable.MakePPMap(Raw) + +module UntypedRawSet = PrettyPrintable.MakePPSet(UntypedRaw) + +module UntypedRawMap = PrettyPrintable.MakePPMap(UntypedRaw) diff --git a/infer/src/checkers/accessPath.mli b/infer/src/checkers/accessPath.mli index 7315f18b8..61176c90a 100644 --- a/infer/src/checkers/accessPath.mli +++ b/infer/src/checkers/accessPath.mli @@ -100,3 +100,7 @@ module AccessMap : PrettyPrintable.PPMap with type key = access module RawSet : PrettyPrintable.PPSet with type elt = Raw.t module RawMap : PrettyPrintable.PPMap with type key = Raw.t + +module UntypedRawSet : PrettyPrintable.PPSet with type elt = Raw.t + +module UntypedRawMap : PrettyPrintable.PPMap with type key = Raw.t