From 750cc65092ec14055e41534ab175d8dcabfdc7fa Mon Sep 17 00:00:00 2001 From: Kyriakos Nikolaos Gkorogiannis Date: Fri, 26 May 2017 11:00:40 -0700 Subject: [PATCH] [threadsafety] fix false negative on locations that may alias. Reviewed By: sblackshear Differential Revision: D5137332 fbshipit-source-id: 87e009c --- infer/src/checkers/ThreadSafety.ml | 32 +++++++++++++++++- .../java/threadsafety/Alias.java | 33 +++++++++++++++++++ .../java/threadsafety/issues.exp | 2 ++ 3 files changed, 66 insertions(+), 1 deletion(-) create mode 100644 infer/tests/codetoanalyze/java/threadsafety/Alias.java 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`]