[thread-safety] use untyped access path maps/sets in thread-safety analysis

Reviewed By: jeremydubreil

Differential Revision: D4550031

fbshipit-source-id: 6168722

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 =

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
 

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)

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