diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index 127c20123..7195ab786 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -1201,6 +1201,36 @@ let report_unsafe_accesses ~is_file_threadsafe aggregated_access_map = empty_reported |> ignore +(* equivalence relation computing whether two access paths may refer to the + same heap location. *) +let may_alias p1 p2 = + let open AccessPath in + match List.last_exn (snd p1), List.last_exn (snd p2) with + | FieldAccess _, ArrayAccess _ | ArrayAccess _, FieldAccess _ -> false + (* fields in Infer contain class name *) + | FieldAccess f1, FieldAccess f2 -> + String.equal (Fieldname.java_get_field f1) (Fieldname.java_get_field f2) + | ArrayAccess _, ArrayAccess _ -> true (*FIXME*) + +(* take a results table and quotient it by the may_alias relation *) +let quotient_access_map acc_map = + let rec aux acc m = + if AccessListMap.is_empty m then + acc + else + let k, _ = AccessListMap.choose m in + let (k_part, non_k_part) = AccessListMap.partition (fun k' _ -> may_alias k k') m in + let k_accesses = + AccessListMap.fold + (fun _ v acc' -> List.append v acc') + k_part + [] + in + let new_acc = AccessListMap.add k k_accesses acc in + aux new_acc non_k_part + in + aux AccessListMap.empty acc_map + (* create a map from [abstraction of a memory loc] -> accesses that may touch that memory loc. for now, our abstraction is an access path like x.f.g whose concretization is the set of memory cells that x.f.g may point to during execution *) @@ -1227,7 +1257,7 @@ let make_results_table file_env = match Summary.read_summary proc_desc proc_name with | Some summary -> aggregate_post summary tenv proc_desc acc | None -> acc in - List.fold ~f:aggregate_posts file_env ~init:AccessListMap.empty + List.fold ~f:aggregate_posts file_env ~init:AccessListMap.empty |> quotient_access_map (** Principles for race reporting. diff --git a/infer/tests/codetoanalyze/java/threadsafety/Alias.java b/infer/tests/codetoanalyze/java/threadsafety/Alias.java new file mode 100644 index 000000000..c68266421 --- /dev/null +++ b/infer/tests/codetoanalyze/java/threadsafety/Alias.java @@ -0,0 +1,33 @@ +/* + * 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; + +@ThreadSafe +class Alias{ + A a,b; + + public void foo() { + int x; + synchronized(this){ + a = b; + a.f = 101; + } + x = b.f; // may_alias + } + + public void bar(A a,A b) { + int x; + synchronized(this){ + a.f = 101; + } + x = b.f; // no may_alias needed, argument treatment suffices + } +} + +class A { int f = 0; } diff --git a/infer/tests/codetoanalyze/java/threadsafety/issues.exp b/infer/tests/codetoanalyze/java/threadsafety/issues.exp index 04c865b06..a4f8923b0 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/issues.exp +++ b/infer/tests/codetoanalyze/java/threadsafety/issues.exp @@ -1,3 +1,5 @@ +codetoanalyze/java/threadsafety/Alias.java, void Alias.bar(A,A), 5, THREAD_SAFETY_VIOLATION, [,access to `A.f`,,access to `Alias.a.A.f`] +codetoanalyze/java/threadsafety/Alias.java, void Alias.foo(), 6, THREAD_SAFETY_VIOLATION, [,access to `Alias.b.A.f`,,access to `Alias.a.A.f`] codetoanalyze/java/threadsafety/AndroidModels.java, void AndroidModels.someResourceMethodsNotFunctionalBad(), 2, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.AndroidModels.mField`] codetoanalyze/java/threadsafety/Annotations.java, boolean Annotations.FP_functionalAcrossUnboxingOk(), 2, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Annotations.mBool2`] codetoanalyze/java/threadsafety/Annotations.java, double Annotations.functionalDoubleBad(), 2, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Annotations.mDouble`]