From 899cfadfbdce930ff0033055b6fe89d87595b5dd Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Wed, 5 Apr 2017 14:04:17 -0700 Subject: [PATCH] [access paths] don't compare types of bases Reviewed By: jberdine Differential Revision: D4832309 fbshipit-source-id: 9f39615 --- infer/src/IR/Typ.re | 9 ----- infer/src/IR/Typ.rei | 4 --- infer/src/checkers/ThreadSafetyDomain.ml | 6 ++-- infer/src/checkers/ThreadSafetyDomain.mli | 4 +-- infer/src/checkers/accessPath.ml | 34 +++---------------- infer/src/checkers/accessPath.mli | 4 --- .../java/threadsafety/Containers.java | 13 +++++++ 7 files changed, 23 insertions(+), 51 deletions(-) diff --git a/infer/src/IR/Typ.re b/infer/src/IR/Typ.re index bae457b8e..4393cb0ce 100644 --- a/infer/src/IR/Typ.re +++ b/infer/src/IR/Typ.re @@ -251,15 +251,6 @@ let module Map = Caml.Map.Make T; let module Tbl = Hashtbl.Make T; -/** type comparison that treats T* [] and T** as the same type. Needed for C/C++ */ -let array_sensitive_compare t1 t2 => - switch (t1, t2) { - | (Tptr (Tptr ptr_typ _) _, Tarray (Tptr array_typ _) _) => compare ptr_typ array_typ - | (Tarray (Tptr array_typ _) _, Tptr (Tptr ptr_typ _) _) => compare array_typ ptr_typ - | _ => compare t1 t2 - }; - - /** Pretty print a type with all the details, using the C syntax. */ let rec pp_full pe f => fun diff --git a/infer/src/IR/Typ.rei b/infer/src/IR/Typ.rei index bb5e73e70..ce4ab106b 100644 --- a/infer/src/IR/Typ.rei +++ b/infer/src/IR/Typ.rei @@ -171,10 +171,6 @@ let module Map: Caml.Map.S with type key = t; let module Tbl: Caml.Hashtbl.S with type key = t; -/** type comparison that treats T* [] and T** as the same type. Needed for C/C++ */ -let array_sensitive_compare: t => t => int; - - /** Pretty print a type with all the details. */ let pp_full: Pp.env => F.formatter => t => unit; diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml index eb4aba869..5c1ff1fef 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.UntypedRawSet) +module AccessPathSetDomain = AbstractDomain.InvertedSet(AccessPath.RawSet) module Access = struct type kind = @@ -110,7 +110,7 @@ end module AttributeSetDomain = AbstractDomain.InvertedSet (Attribute.Set) module AttributeMapDomain = struct - include AbstractDomain.InvertedMap (AccessPath.UntypedRawMap) (AttributeSetDomain) + include AbstractDomain.InvertedMap (AccessPath.RawMap) (AttributeSetDomain) let has_attribute access_path attribute t = try @@ -201,7 +201,7 @@ let empty = let locks = false in let accesses = AccessDomain.empty in let id_map = IdAccessPathMapDomain.empty in - let attribute_map = AccessPath.UntypedRawMap.empty in + let attribute_map = AccessPath.RawMap.empty in { threads; locks; accesses; id_map; attribute_map; } let (<=) ~lhs ~rhs = diff --git a/infer/src/checkers/ThreadSafetyDomain.mli b/infer/src/checkers/ThreadSafetyDomain.mli index 165298375..3f765c4f1 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.UntypedRawSet) +module AccessPathSetDomain : module type of AbstractDomain.InvertedSet (AccessPath.RawSet) module Access : sig type kind = @@ -74,7 +74,7 @@ end module AttributeSetDomain : module type of AbstractDomain.InvertedSet (Attribute.Set) module AttributeMapDomain : sig - include module type of AbstractDomain.InvertedMap (AccessPath.UntypedRawMap) (AttributeSetDomain) + include module type of AbstractDomain.InvertedMap (AccessPath.RawMap) (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 41840a8c5..34144152f 100644 --- a/infer/src/checkers/accessPath.ml +++ b/infer/src/checkers/accessPath.ml @@ -11,19 +11,16 @@ open! IStd 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 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 Fieldname.t @@ -31,7 +28,6 @@ type access = let equal_access = [%compare.equal : access] - let equal_access_list l1 l2 = Int.equal (List.compare compare_access l1 l2) 0 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 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 @@ -207,7 +187,3 @@ 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 678d98c88..30daa1ce6 100644 --- a/infer/src/checkers/accessPath.mli +++ b/infer/src/checkers/accessPath.mli @@ -102,7 +102,3 @@ 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 diff --git a/infer/tests/codetoanalyze/java/threadsafety/Containers.java b/infer/tests/codetoanalyze/java/threadsafety/Containers.java index ca0f52273..87ec63cdb 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/Containers.java +++ b/infer/tests/codetoanalyze/java/threadsafety/Containers.java @@ -187,4 +187,17 @@ class Containers { obj.f = new Object(); // should flag } + private static List addOrCreateList(List list) { + if (list == null) { + list = new ArrayList<>(); + } + list.add(new Object()); + return list; + } + + public void addToNullListOk() { + List list = null; + addOrCreateList(list); + } + }