diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index e5f812f79..2c737a469 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -1455,30 +1455,9 @@ let report_unsafe_accesses aggregated_access_map = aggregated_access_map empty_reported |> ignore -(* equivalence relation computing whether two access paths may refer to the - same heap location. *) -let may_alias tenv p1 p2 = - let open Typ in - let open AccessPath in - phys_equal p1 p2 - || - match (List.last_exn (snd p1), List.last_exn (snd p2)) with - | FieldAccess _, ArrayAccess _ | ArrayAccess _, FieldAccess _ - -> false - (* fields in Java contain the class name /declaring/ them - thus two fields can be aliases *iff* they are equal *) - | FieldAccess f1, FieldAccess f2 - -> Typ.Fieldname.equal f1 f2 - (* if arrays of objects that have an inheritance rel then they can alias *) - | ( ArrayAccess {desc= Tptr ({desc= Tstruct tn1}, _)} - , ArrayAccess {desc= Tptr ({desc= Tstruct tn2}, _)} ) - -> PatternMatch.is_subtype tenv tn1 tn2 || PatternMatch.is_subtype tenv tn2 tn1 - (* primitive type arrays can alias if the prim. type is the same *) - | ArrayAccess t1, ArrayAccess t2 - -> equal_desc t1.desc t2.desc +let sound = false let may_alias_container tenv p1 p2 = - let sound = false in if sound then (* this is much too noisy: we'll warn that accesses to *any* Map can race with accesses to any other Map, etc. Instead, do something simple and unsound: just assume that two accesses can @@ -1503,6 +1482,29 @@ let may_alias_container tenv p1 p2 = | _ -> AccessPath.Raw.equal p1 p2 +(* equivalence relation computing whether two access paths may refer to the + same heap location. *) +let may_alias tenv p1 p2 = + let open Typ in + let open AccessPath in + phys_equal p1 p2 + || + match (List.last_exn (snd p1), List.last_exn (snd p2)) with + | FieldAccess _, ArrayAccess _ | ArrayAccess _, FieldAccess _ + -> false + (* fields in Java contain the class name /declaring/ them + thus two fields can be aliases *iff* they are equal *) + | FieldAccess f1, FieldAccess f2 + -> Typ.Fieldname.equal f1 f2 + (* if arrays of objects that have an inheritance rel then they can alias *) + | ( ArrayAccess {desc= Tptr ({desc= Tstruct tn1}, _)} + , ArrayAccess {desc= Tptr ({desc= Tstruct tn2}, _)} ) + -> if sound then PatternMatch.is_subtype tenv tn1 tn2 || PatternMatch.is_subtype tenv tn2 tn1 + else may_alias_container tenv p1 p2 + (* primitive type arrays can alias if the prim. type is the same *) + | ArrayAccess t1, ArrayAccess t2 + -> if sound then equal_desc t1.desc t2.desc else may_alias_container tenv p1 p2 + (* take a results table and quotient it by the may_alias relation *) let quotient_access_map acc_map = let rec aux acc m = diff --git a/infer/tests/codetoanalyze/java/threadsafety/Arrays.java b/infer/tests/codetoanalyze/java/threadsafety/Arrays.java new file mode 100644 index 000000000..e190a58ad --- /dev/null +++ b/infer/tests/codetoanalyze/java/threadsafety/Arrays.java @@ -0,0 +1,80 @@ +/* + * Copyright (c) 2017 - present Facebook, Inc. + * All rights reserved. + * + * This source code is licensed under the BSD style license found in the + * LICENSE file in the root directory of this source tree. An additional grant + * of patent rights can be found in the PATENTS file in the same directory. + */ +import javax.annotation.concurrent.ThreadSafe; + +// Test may_alias treatment of arrays +// two arrays of types in a subtype relation may alias, and race + +@ThreadSafe +class Parent {} + +@ThreadSafe +class Child extends Parent {} + +@ThreadSafe +class Arrays { + Child[] childArr = new Child[5]; + Parent[] parentArr = childArr; // actual aliasing not required, but for documentation + final String[] strArr1 = new String[5]; + final String[] strArr2 = new String[5]; + + void arrayParameterWriteBad(int[] name1) { + name1[2] = 4; + } + + // we'll report this because name1 and name2 may alias + int arrayParameterReadBad(int[] name2) { + return name2[2]; + } + + int arrayParameterLiteralReadOk() { + return (new int[] { 2, 3})[1]; + } + + public void writeWriteRaceBad(String s) { + strArr1[2] = s; + } + + // same array + public String readWriteRaceBad(String s) { + synchronized (this) { + strArr1[2] = s; + } + return strArr1[2]; + } + + // arrays are same type, but can't alias + public String notReadWriteRace1Ok(String s) { + synchronized (this) { + strArr1[0] = s; + } + return strArr2[0]; + } + + // arrays are compatible types and can alias + public Child FN_readWriteAliasRaceBad() { + synchronized(this) { + parentArr[3] = null; + } + return childArr[3]; + } + + String[] type1Arr[]; + Parent[] type2Arr; + + // arrays are different types and thus cannot alias + public Parent noRaceOk() { + synchronized(this) { + type1Arr[3] = null; + } + + return type2Arr[3]; + } + +} diff --git a/infer/tests/codetoanalyze/java/threadsafety/SubArr.java b/infer/tests/codetoanalyze/java/threadsafety/SubArr.java deleted file mode 100644 index 22de86501..000000000 --- a/infer/tests/codetoanalyze/java/threadsafety/SubArr.java +++ /dev/null @@ -1,42 +0,0 @@ -/* - * Copyright (c) 2017 - present Facebook, Inc. - * All rights reserved. - * - * This source code is licensed under the BSD style license found in the - * LICENSE file in the root directory of this source tree. An additional grant - * of patent rights can be found in the PATENTS file in the same directory. - */ -import javax.annotation.concurrent.ThreadSafe; - -// Test may_alias treatment of arrays -// two arrays of types in a subtype relation may alias, and race - -@ThreadSafe -class Parent {} - -@ThreadSafe -class Child extends Parent {} - -@ThreadSafe -class SubArr { - Child[] childArr = new Child[5]; - Parent[] parentArr = childArr; // actual aliasing not required, but for documentation - String[] strArr = new String[5]; - - public Child RWrace() { - synchronized(this) { - parentArr[3] = null; - } - - return childArr[4]; - } - - public String NOrace() { - synchronized(this) { - parentArr[3] = null; - } - - return strArr[2]; - } - -} diff --git a/infer/tests/codetoanalyze/java/threadsafety/issues.exp b/infer/tests/codetoanalyze/java/threadsafety/issues.exp index 1666ff936..5ec5f8f16 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/issues.exp +++ b/infer/tests/codetoanalyze/java/threadsafety/issues.exp @@ -14,6 +14,10 @@ codetoanalyze/java/threadsafety/Annotations.java, void Annotations.read_from_non codetoanalyze/java/threadsafety/Annotations.java, void Annotations.read_off_UI_thread_Bad(), 1, THREAD_SAFETY_VIOLATION, [,access to `codetoanalyze.java.checkers.Annotations.f`,,access to `codetoanalyze.java.checkers.Annotations.f`] codetoanalyze/java/threadsafety/Annotations.java, void ThreadSafeAlias.threadSafeAliasBad1(), 1, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.ThreadSafeAlias.field`] codetoanalyze/java/threadsafety/Annotations.java, void ThreadSafeAlias.threadSafeAliasBad2(), 1, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.ThreadSafeAlias.field`] +codetoanalyze/java/threadsafety/Arrays.java, String Arrays.readWriteRaceBad(String), 4, THREAD_SAFETY_VIOLATION, [,access to `Arrays.strArr1.[_]`,,access to `Arrays.strArr1.[_]`] +codetoanalyze/java/threadsafety/Arrays.java, int Arrays.arrayParameterReadBad(int[]), 1, THREAD_SAFETY_VIOLATION, [,access to `[_]`,,access to `[_]`] +codetoanalyze/java/threadsafety/Arrays.java, void Arrays.arrayParameterWriteBad(int[]), 1, THREAD_SAFETY_VIOLATION, [access to `[_]`] +codetoanalyze/java/threadsafety/Arrays.java, void Arrays.writeWriteRaceBad(String), 1, THREAD_SAFETY_VIOLATION, [access to `Arrays.strArr1.[_]`] codetoanalyze/java/threadsafety/Builders.java, Builders$Obj Builders.buildThenMutateBad(Builders$Obj), 2, THREAD_SAFETY_VIOLATION, [,call to Builders$Obj$Builder Builders$Obj$Builder.setFromObj(Builders$Obj),access to `codetoanalyze.java.checkers.Builders$Obj.g`,,access to `codetoanalyze.java.checkers.Builders$Obj.g`] codetoanalyze/java/threadsafety/Builders.java, Builders$Obj Builders.buildThenMutateBad(Builders$Obj), 3, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Builders$Obj.g`] codetoanalyze/java/threadsafety/Builders.java, Builders$Obj Builders.mutateBad(Builders$Obj), 1, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Builders$Obj.g`] @@ -90,7 +94,6 @@ codetoanalyze/java/threadsafety/ReadWriteRaces.java, void ReadWriteRaces.m1(), 2 codetoanalyze/java/threadsafety/ReadWriteRaces.java, void ReadWriteRaces.m2(), 1, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.ReadWriteRaces.racy`] codetoanalyze/java/threadsafety/ReadWriteRaces.java, void ReadWriteRaces.m3(), 1, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.ReadWriteRaces.racy`] codetoanalyze/java/threadsafety/ReadWriteRaces.java, void ReadWriteRaces.readInCalleeOutsideSyncBad(int), 1, THREAD_SAFETY_VIOLATION, [,call to int C.get(),access to `codetoanalyze.java.checkers.C.x`,,call to void C.set(int),access to `codetoanalyze.java.checkers.C.x`] -codetoanalyze/java/threadsafety/SubArr.java, Child SubArr.RWrace(), 5, THREAD_SAFETY_VIOLATION, [,access to `SubArr.childArr.[_]`,,access to `SubArr.parentArr.[_]`] codetoanalyze/java/threadsafety/SubFld.java, int SubFld.getG(), 6, THREAD_SAFETY_VIOLATION, [,call to int SuperFld.getG(),access to `SuperFld.g`,,access to `SuperFld.g`] codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ExtendsThreadSafeExample.newmethodBad(), 1, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.ExtendsThreadSafeExample.field`] codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ExtendsThreadSafeExample.tsOK(), 1, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.ExtendsThreadSafeExample.field`]