diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index f4b87a72c..47cb4a0c1 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -180,6 +180,12 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let add_access exp loc ~is_write_access accesses locks threads ownership (proc_data: extras ProcData.t) = let open Domain in + let is_static_access = function + | Var.ProgramVar pvar -> + Pvar.is_static_local pvar + | _ -> + false + in (* we don't want to warn on accesses to the field if it is (a) thread-confined, or (b) volatile *) let is_safe_access access prefix_path tenv = @@ -196,48 +202,39 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | _ -> false in - let is_static_access ((base: Var.t), _) = - match base with ProgramVar pvar -> Pvar.is_static_local pvar | _ -> false - in - let rec add_field_accesses pre prefix_path access_acc = function + let rec add_field_accesses prefix_path access_acc = function | [] -> access_acc - | access :: access_list' -> - let is_write = if List.is_empty access_list' then is_write_access else false in - let access_path = (fst prefix_path, snd prefix_path @ [access]) in - let access_acc' = - if OwnershipDomain.is_owned prefix_path ownership - || is_safe_access access prefix_path proc_data.tenv - then access_acc - else + | access :: access_list -> + let prefix_path' = (fst prefix_path, snd prefix_path @ [access]) in + let add_field_access pre = + let is_write = if List.is_empty access_list then is_write_access else false in + let access_acc' = AccessDomain.add_access pre - (TraceElem.make_field_access access_path ~is_write loc) + (TraceElem.make_field_access prefix_path' ~is_write loc) access_acc + in + add_field_accesses prefix_path' access_acc' access_list in - add_field_accesses pre access_path access_acc' access_list' - in - let add_access_ acc (base, accesses) = - let base_access_path = (base, []) in - if List.is_empty accesses || OwnershipDomain.is_owned base_access_path ownership - || is_static_access base - then acc - else - let pre = - match AccessPrecondition.make_protected locks threads proc_data.pdesc with - | AccessPrecondition.Protected _ as excluder -> - excluder - | _ -> - match OwnershipDomain.get_owned base_access_path ownership with - | OwnershipAbstractValue.OwnedIf formal_indexes -> - AccessPrecondition.make_unprotected formal_indexes - | OwnershipAbstractValue.Owned -> - assert false - | OwnershipAbstractValue.Unowned -> - AccessPrecondition.totally_unprotected - in - add_field_accesses pre base_access_path acc accesses + if is_safe_access access prefix_path proc_data.tenv then + add_field_accesses prefix_path' access_acc access_list + else + match AccessPrecondition.make_protected locks threads proc_data.pdesc with + | AccessPrecondition.Protected _ as excluder -> + add_field_access excluder + | _ -> + match OwnershipDomain.get_owned prefix_path ownership with + | OwnershipAbstractValue.OwnedIf formal_indexes -> + add_field_access (AccessPrecondition.make_unprotected formal_indexes) + | OwnershipAbstractValue.Owned -> + add_field_accesses prefix_path' access_acc access_list + | OwnershipAbstractValue.Unowned -> + add_field_access AccessPrecondition.totally_unprotected in - List.fold ~f:add_access_ ~init:accesses (HilExp.get_access_paths exp) + List.fold + ~f:(fun acc (base, accesses) -> + if is_static_access (fst base) then acc else add_field_accesses (base, []) acc accesses) + ~init:accesses (HilExp.get_access_paths exp) let is_functional pname = @@ -1720,3 +1717,4 @@ let file_analysis {Callbacks.procedures} = else (module MayAliasQuotientedAccessListMap) ) class_env)) (aggregate_by_class procedures) + diff --git a/infer/tests/codetoanalyze/java/racerd/ShallowOwnership.java b/infer/tests/codetoanalyze/java/racerd/ShallowOwnership.java new file mode 100644 index 000000000..4d2267f62 --- /dev/null +++ b/infer/tests/codetoanalyze/java/racerd/ShallowOwnership.java @@ -0,0 +1,34 @@ +/* + * 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 com.facebook.infer.annotation.ThreadSafe; + +@ThreadSafe +class ShallowOwnership { + ShallowOwnership next; + static ShallowOwnership global; + + void globalNotOwnedBad() { + global.next = null; + } + + void reassignBaseToGlobalBad(){ + ShallowOwnership x = new ShallowOwnership(); + x = global; + x.next = null; + } + + void reassignPathToGlobalBad() { + ShallowOwnership x = new ShallowOwnership(); + x.next = global; + x.next.next = null; + } + +} diff --git a/infer/tests/codetoanalyze/java/racerd/issues.exp b/infer/tests/codetoanalyze/java/racerd/issues.exp index 4415c50b6..e3a37bbe8 100644 --- a/infer/tests/codetoanalyze/java/racerd/issues.exp +++ b/infer/tests/codetoanalyze/java/racerd/issues.exp @@ -97,6 +97,9 @@ codetoanalyze/java/racerd/ReadWriteRaces.java, void ReadWriteRaces.m1(), 2, THRE codetoanalyze/java/racerd/ReadWriteRaces.java, void ReadWriteRaces.m2(), 1, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.ReadWriteRaces.racy`] codetoanalyze/java/racerd/ReadWriteRaces.java, void ReadWriteRaces.m3(), 1, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.ReadWriteRaces.racy`] codetoanalyze/java/racerd/ReadWriteRaces.java, void ReadWriteRaces.readInCalleeOutsideSyncBad(int), 1, THREAD_SAFETY_VIOLATION, [,call to int C.get(),access to `&this.codetoanalyze.java.checkers.C.x`,,call to void C.set(int),access to `&this.codetoanalyze.java.checkers.C.x`] +codetoanalyze/java/racerd/ShallowOwnership.java, void ShallowOwnership.globalNotOwnedBad(), 1, THREAD_SAFETY_VIOLATION, [access to `&#GB$ShallowOwnership.ShallowOwnership.global.ShallowOwnership.next`] +codetoanalyze/java/racerd/ShallowOwnership.java, void ShallowOwnership.reassignBaseToGlobalBad(), 3, THREAD_SAFETY_VIOLATION, [access to `&x.ShallowOwnership.next`] +codetoanalyze/java/racerd/ShallowOwnership.java, void ShallowOwnership.reassignPathToGlobalBad(), 3, THREAD_SAFETY_VIOLATION, [access to `&x.ShallowOwnership.next.ShallowOwnership.next`] codetoanalyze/java/racerd/SubFld.java, int SubFld.getG(), 6, THREAD_SAFETY_VIOLATION, [,call to int SuperFld.getG(),access to `&this.SuperFld.g`,,access to `&this.SuperFld.g`] codetoanalyze/java/racerd/ThreadSafeExample.java, Object ThreadSafeExample.FP_lazyInitOk(), 6, THREAD_SAFETY_VIOLATION, [,access to `&this.codetoanalyze.java.checkers.ThreadSafeExample.sStaticField`,,access to `&this.codetoanalyze.java.checkers.ThreadSafeExample.sStaticField`] codetoanalyze/java/racerd/ThreadSafeExample.java, void ExtendsThreadSafeExample.newmethodBad(), 1, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.ExtendsThreadSafeExample.field`]