From 268e0b9b5f1969b1d4f05c47a9d28534a481fa92 Mon Sep 17 00:00:00 2001 From: Sam Blackshear Date: Wed, 31 Jan 2018 12:28:39 -0800 Subject: [PATCH] [racerd] generalize access preconditions Summary: Previously, we could understand than an access was safe either because it was possibly owned or protected by a thread/lock, but not both. If an access was both protected by a lock and rooted in a paramer (i.e., possibly owned), we would forget the ownership part of the precondition and remember only the lock bit. This leads to false positives in cases where an access protected by a lock is owned, but another unowned access to the same memory is not protected by a lock (see the new `unownedLockedWriteOk` E2E test for an example). This diff makes access safety conditions disjunctive so we can simultaneously track whether an access is owned and whether an access is protected by a thread/lock. This will fix false positives like the one explained in T24015160. Reviewed By: jberdine Differential Revision: D6671489 fbshipit-source-id: d17715f --- infer/src/concurrency/RacerD.ml | 261 +++++++++--------- infer/src/concurrency/RacerDDomain.ml | 66 ++--- infer/src/concurrency/RacerDDomain.mli | 54 ++-- .../codetoanalyze/java/racerd/Dispatch.java | 13 + .../codetoanalyze/java/racerd/Locks.java | 32 ++- .../java/racerd/RaceWithMainThread.java | 38 ++- .../codetoanalyze/java/racerd/issues.exp | 3 + 7 files changed, 266 insertions(+), 201 deletions(-) diff --git a/infer/src/concurrency/RacerD.ml b/infer/src/concurrency/RacerD.ml index 34a614ee3..35984942a 100644 --- a/infer/src/concurrency/RacerD.ml +++ b/infer/src/concurrency/RacerD.ml @@ -161,7 +161,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct && not (has_return_annot thread_safe_or_thread_confined pname) then let open Domain in - let pre = AccessPrecondition.make_protected locks threads proc_data.pdesc in + let pre = AccessData.make locks threads False proc_data.pdesc in AccessDomain.add_access pre (TraceElem.make_unannotated_call_access pname loc) attribute_map else attribute_map @@ -208,17 +208,18 @@ module TransferFunctions (CFG : ProcCfg.S) = struct 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 + match OwnershipDomain.get_owned prefix_path ownership with + | OwnershipAbstractValue.OwnedIf formal_indexes -> + let pre = + AccessData.make locks threads + (AccessData.Precondition.Conjunction formal_indexes) proc_data.pdesc + in + add_field_access pre + | OwnershipAbstractValue.Owned -> + add_field_accesses prefix_path' access_acc access_list + | OwnershipAbstractValue.Unowned -> + let pre = AccessData.make locks threads False proc_data.pdesc in + add_field_access pre in List.fold ~f:(fun acc (base, accesses) -> @@ -339,7 +340,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct false - let make_container_access callee_pname ~is_write receiver_ap callee_loc tenv = + let make_container_access callee_pname ~is_write receiver_ap callee_loc tenv caller_pdesc + (astate: Domain.astate) = (* create a dummy write that represents mutating the contents of the container *) let open Domain in let callee_accesses = @@ -348,9 +350,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let container_access = TraceElem.make_container_access receiver_ap ~is_write callee_pname callee_loc in - AccessDomain.add_access - (AccessPrecondition.make_unprotected (IntSet.singleton 0)) - container_access AccessDomain.empty + let pre = + AccessData.make astate.locks astate.threads + (AccessData.Precondition.Conjunction (IntSet.singleton 0)) caller_pdesc + in + AccessDomain.add_access pre container_access AccessDomain.empty in (* if a container c is owned in cpp, make c[i] owned for all i *) let return_ownership = @@ -368,7 +372,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct ; return_attributes= AttributeSetDomain.empty } - let get_summary caller_pdesc callee_pname actuals callee_loc tenv = + let get_summary caller_pdesc callee_pname actuals callee_loc tenv (astate: Domain.astate) = let open RacerDConfig in let get_receiver_ap actuals = match List.hd actuals with @@ -382,9 +386,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct match (Models.get_container_access callee_pname tenv, callee_pname) with | Some ContainerWrite, _ -> make_container_access callee_pname ~is_write:true (get_receiver_ap actuals) callee_loc tenv + caller_pdesc astate | Some ContainerRead, _ -> make_container_access callee_pname ~is_write:false (get_receiver_ap actuals) callee_loc - tenv + tenv caller_pdesc astate | None, _ -> Summary.read_summary caller_pdesc callee_pname @@ -459,6 +464,84 @@ module TransferFunctions (CFG : ProcCfg.S) = struct AccessDomain.map expand_pre accesses + let add_callee_accesses (caller_astate: Domain.astate) accesses locks threads actuals + callee_pname pdesc loc = + let open Domain in + let update_caller_accesses pre callee_accesses caller_accesses = + let combined_accesses = + PathDomain.with_callsite callee_accesses (CallSite.make callee_pname loc) + |> PathDomain.join (AccessDomain.get_accesses pre caller_accesses) + in + AccessDomain.add pre combined_accesses caller_accesses + in + let conjoin_ownership_pre actual_exp actual_indexes : AccessData.Precondition.t = + match actual_exp with + | HilExp.Constant _ -> + (* the actual is a constant, so it's owned in the caller. *) + Conjunction actual_indexes + | HilExp.AccessPath actual_access_path + -> ( + if OwnershipDomain.is_owned actual_access_path caller_astate.ownership then + (* the actual passed to the current callee is owned. drop all the conditional accesses + for that actual, since they're all safe *) + Conjunction actual_indexes + else + let base = fst actual_access_path in + match OwnershipDomain.get_owned (base, []) caller_astate.ownership with + | OwnedIf formal_indexes -> + (* the actual passed to the current callee is rooted in a formal *) + Conjunction (IntSet.union formal_indexes actual_indexes) + | Unowned | Owned -> + match OwnershipDomain.get_owned actual_access_path caller_astate.ownership with + | OwnedIf formal_indexes -> + (* access path conditionally owned if [formal_indexes] are owned *) + Conjunction (IntSet.union formal_indexes actual_indexes) + | Owned -> + assert false + | Unowned -> + (* access path not rooted in a formal and not conditionally owned *) + False ) + | _ -> + (* couldn't find access path, don't know if it's owned. assume not *) + False + in + let update_ownership_pre actual_index (acc: AccessData.Precondition.t) = + match acc with + | False -> + (* precondition can't be satisfied *) + acc + | Conjunction actual_indexes -> + match List.nth actuals actual_index with + | Some actual -> + conjoin_ownership_pre actual actual_indexes + | None -> + L.internal_error "Bad actual index %d for callee %a with %d actuals." actual_index + Typ.Procname.pp callee_pname (List.length actuals) ; + acc + in + let update_accesses (pre: AccessData.t) callee_accesses accesses_acc = + (* update precondition with caller ownership info *) + let ownership_precondition' = + match pre.ownership_precondition with + | Conjunction indexes -> + let empty_pre = AccessData.Precondition.Conjunction IntSet.empty in + IntSet.fold update_ownership_pre indexes empty_pre + | False -> + pre.ownership_precondition + in + if AccessData.Precondition.is_true ownership_precondition' then accesses_acc + else + let locks' = locks || pre.lock in + (* if the access occurred on a main thread in the callee, we should remember this when + moving it to the callee. if we don't know what thread it ran on, use the caller's + thread *) + let threads' = if pre.thread then ThreadsDomain.AnyThreadButSelf else threads in + let pre' = AccessData.make locks' threads' ownership_precondition' pdesc in + update_caller_accesses pre' callee_accesses accesses_acc + in + AccessDomain.fold update_accesses accesses caller_astate.accesses + + let exec_instr (astate: Domain.astate) ({ProcData.tenv; extras; pdesc} as proc_data) _ (instr: HilInstr.t) = let open Domain in @@ -537,7 +620,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct "Procedure %a specified as returning boolean, but returns nothing" Typ.Procname.pp callee_pname ) | NoEffect -> - let summary_opt = get_summary pdesc callee_pname actuals loc tenv in + let summary_opt = get_summary pdesc callee_pname actuals loc tenv astate in let callee_pdesc = extras callee_pname in match Option.map summary_opt ~f:(fun summary -> @@ -548,13 +631,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct {summary with accesses= rebased_accesses} ) with | Some {threads; locks; accesses; return_ownership; return_attributes} -> - let update_caller_accesses pre callee_accesses caller_accesses = - let combined_accesses = - PathDomain.with_callsite callee_accesses (CallSite.make callee_pname loc) - |> PathDomain.join (AccessDomain.get_accesses pre caller_accesses) - in - AccessDomain.add pre combined_accesses caller_accesses - in let locks = locks || astate.locks in let threads = match (astate.threads, threads) with @@ -565,73 +641,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | _ -> ThreadsDomain.join threads astate.threads in - (* add [ownership_accesses] to the [accesses_acc] with a protected pre if - [exp] is owned, and an appropriate unprotected pre otherwise *) - let add_ownership_access ownership_accesses actual_exp accesses_acc = - match actual_exp with - | HilExp.Constant _ -> - (* the actual is a constant, so it's owned in the caller. *) - accesses_acc - | HilExp.AccessPath actual_access_path -> - if OwnershipDomain.is_owned actual_access_path astate.ownership then - (* the actual passed to the current callee is owned. drop all the - conditional accesses for that actual, since they're all safe *) - accesses_acc - else - let pre = - match AccessPrecondition.make_protected locks threads pdesc with - | AccessPrecondition.Protected _ as excluder (* access protected *) -> - excluder - | _ -> - let base = fst actual_access_path in - match OwnershipDomain.get_owned (base, []) astate.ownership with - | OwnershipAbstractValue.OwnedIf formal_indexes -> - (* the actual passed to the current callee is rooted in a - formal *) - AccessPrecondition.make_unprotected formal_indexes - | OwnershipAbstractValue.Unowned | OwnershipAbstractValue.Owned -> - match - OwnershipDomain.get_owned actual_access_path astate.ownership - with - | OwnershipAbstractValue.OwnedIf formal_indexes -> - (* access path conditionally owned if [formal_indexes] are - owned *) - AccessPrecondition.make_unprotected formal_indexes - | OwnershipAbstractValue.Owned -> - assert false - | OwnershipAbstractValue.Unowned -> - (* access path not rooted in a formal and not conditionally - owned *) - AccessPrecondition.totally_unprotected - in - update_caller_accesses pre ownership_accesses accesses_acc - | _ -> - (* couldn't find access path, don't know if it's owned *) - update_caller_accesses AccessPrecondition.totally_unprotected - ownership_accesses accesses_acc - in let accesses = - let update_accesses pre callee_accesses accesses_acc = - match pre with - | AccessPrecondition.Protected _ -> - update_caller_accesses pre callee_accesses accesses_acc - | AccessPrecondition.TotallyUnprotected -> - let pre' = AccessPrecondition.make_protected locks threads pdesc in - update_caller_accesses pre' callee_accesses accesses_acc - | AccessPrecondition.Unprotected formal_indexes -> - IntSet.fold - (fun index acc -> - match List.nth actuals index with - | Some actual -> - add_ownership_access callee_accesses actual acc - | None -> - L.internal_error - "Bad actual index %d for callee %a with %d actuals." index - Typ.Procname.pp callee_pname (List.length actuals) ; - acc ) - formal_indexes accesses_acc - in - AccessDomain.fold update_accesses accesses astate.accesses + add_callee_accesses astate accesses locks threads actuals callee_pname pdesc + loc in let ownership, attribute_map = propagate_return ret_opt return_ownership return_attributes actuals astate @@ -1255,7 +1267,7 @@ let make_unprotected_write_description pname final_sink_site initial_sink_site f type reported_access = { access: RacerDDomain.TraceElem.t ; threads: RacerDDomain.ThreadsDomain.astate - ; precondition: RacerDDomain.AccessPrecondition.t + ; precondition: RacerDDomain.AccessData.t ; tenv: Tenv.t ; procdesc: Procdesc.t } @@ -1370,20 +1382,17 @@ let report_unsafe_accesses (aggregated_access_map: reported_access list AccessLi let pname = Procdesc.get_proc_name procdesc in if is_duplicate_report access pname reported_acc then reported_acc else - match (TraceElem.kind access, precondition) with - | ( Access.InterfaceCall unannoted_call_pname - , (AccessPrecondition.Unprotected _ | AccessPrecondition.TotallyUnprotected) ) -> - if ThreadsDomain.is_any threads && is_marked_thread_safe procdesc tenv then ( + match TraceElem.kind access with + | Access.InterfaceCall unannoted_call_pname -> + if AccessData.is_unprotected precondition && ThreadsDomain.is_any threads + && is_marked_thread_safe procdesc tenv + then ( (* un-annotated interface call + no lock in method marked thread-safe. warn *) report_unannotated_interface_violation tenv procdesc access threads unannoted_call_pname ; update_reported access pname reported_acc ) else reported_acc - | Access.InterfaceCall _, AccessPrecondition.Protected _ -> - (* un-annotated interface call, but it's protected by a lock/thread. don't report *) - reported_acc - | ( (Access.Write _ | ContainerWrite _) - , (AccessPrecondition.Unprotected _ | AccessPrecondition.TotallyUnprotected) ) -> ( + | Access.Write _ | ContainerWrite _ -> ( match Procdesc.get_proc_name procdesc with | Java _ -> let writes_on_background_thread = @@ -1401,7 +1410,8 @@ let report_unsafe_accesses (aggregated_access_map: reported_access list AccessLi else None ) accesses in - if not (List.is_empty writes_on_background_thread && not (ThreadsDomain.is_any threads)) + if AccessData.is_unprotected precondition + && (not (List.is_empty writes_on_background_thread) || ThreadsDomain.is_any threads) then let conflict = List.hd writes_on_background_thread in report_thread_safety_violation tenv procdesc @@ -1413,19 +1423,11 @@ let report_unsafe_accesses (aggregated_access_map: reported_access list AccessLi (* Do not report unprotected writes when an access can't run in parallel with itself, or for ObjC_Cpp *) reported_acc ) - | (Access.Write _ | ContainerWrite _), AccessPrecondition.Protected _ -> - (* protected write, do nothing *) - reported_acc - | ( (Access.Read _ | ContainerRead _) - , (AccessPrecondition.Unprotected _ | AccessPrecondition.TotallyUnprotected) ) -> + | (Access.Read _ | ContainerRead _) when AccessData.is_unprotected precondition -> (* unprotected read. report all writes as conflicts for java. for c++ filter out unprotected writes *) let is_cpp_protected_write pre = - match pre with - | AccessPrecondition.Unprotected _ | TotallyUnprotected -> - Typ.Procname.is_java pname - | AccessPrecondition.Protected _ -> - true + Typ.Procname.is_java pname || not (AccessData.is_unprotected pre) in let is_conflict other_access pre other_thread = TraceElem.is_write other_access @@ -1447,27 +1449,24 @@ let report_unsafe_accesses (aggregated_access_map: reported_access list AccessLi ~report_kind:(ReadWriteRace conflict.access) access threads ; update_reported access pname reported_acc else reported_acc - | (Access.Read _ | ContainerRead _), AccessPrecondition.Protected excl -> - (* protected read. report unprotected writes and opposite protected writes as conflicts - Thread and Lock are opposites of one another, and Both has no opposite *) - let is_opposite = function - | Excluder.Lock, Excluder.Thread -> - true - | Excluder.Thread, Excluder.Lock -> - true - | _, _ -> - false + | Access.Read _ | ContainerRead _ -> + (* protected read. report unprotected writes and opposite protected writes as conflicts *) + let can_conflict (pre1: AccessData.t) (pre2: AccessData.t) = + if pre1.lock && pre2.lock then false + else if pre1.thread && pre2.thread then false + else true in let conflicting_writes = List.filter - ~f:(fun {access; precondition; threads= other_threads} -> - TraceElem.is_write access - && - match precondition with - | Unprotected _ | TotallyUnprotected -> - ThreadsDomain.is_any other_threads - | Protected other_excl -> - is_opposite (excl, other_excl) ) + ~f: + (fun { access= other_access + ; precondition= other_precondition + ; threads= other_threads } -> + if AccessData.is_unprotected other_precondition then + TraceElem.is_write other_access && ThreadsDomain.is_any other_threads + else + TraceElem.is_write other_access && can_conflict precondition other_precondition + ) accesses in if not (List.is_empty conflicting_writes) then diff --git a/infer/src/concurrency/RacerDDomain.ml b/infer/src/concurrency/RacerDDomain.ml index 0f83a94d7..491798b3a 100644 --- a/infer/src/concurrency/RacerDDomain.ml +++ b/infer/src/concurrency/RacerDDomain.ml @@ -322,7 +322,7 @@ module OwnershipDomain = struct (* -returns Owned if any prefix is owned on any prefix, else OwnedIf if it is +returns Owned if any prefix is owned on any prefix, else OwnedIf if it is OwnedIf in the astate, else UnOwned *) let get_owned access_path astate = @@ -361,55 +361,43 @@ module AttributeMapDomain = struct add access_path attribute_set t end -module Excluder = struct - type t = Thread | Lock | Both [@@deriving compare] +module AccessData = struct + module Precondition = struct + type t = Conjunction of IntSet.t | False [@@deriving compare] - let pp fmt = function - | Thread -> - F.fprintf fmt "Thread" - | Lock -> - F.fprintf fmt "Lock" - | Both -> - F.fprintf fmt "both Thread and Lock" -end + (* precondition is true if the conjunction of owned indexes is empty *) + let is_true = function False -> false | Conjunction set -> IntSet.is_empty set -module AccessPrecondition = struct - type t = - | Protected of Excluder.t - | Unprotected of IntSet.t - | TotallyUnprotected - [@@deriving compare] - - let pp fmt = function - | Protected excl -> - F.fprintf fmt "ProtectedBy(%a)" Excluder.pp excl - | TotallyUnprotected -> - F.fprintf fmt "TotallyUnprotected" - | Unprotected indexes -> - F.fprintf fmt "Unprotected(%a)" - (PrettyPrintable.pp_collection ~pp_item:Int.pp) - (IntSet.elements indexes) + let pp fmt = function + | Conjunction indexes -> + F.fprintf fmt "Owned(%a)" + (PrettyPrintable.pp_collection ~pp_item:Int.pp) + (IntSet.elements indexes) + | False -> + F.fprintf fmt "False" + end + type t = {thread: bool; lock: bool; ownership_precondition: Precondition.t} [@@deriving compare] - let make_protected locks thread pdesc = - let is_main_thread = ThreadsDomain.is_any_but_self thread in - let locked = locks || Procdesc.is_java_synchronized pdesc in - if not locked && not is_main_thread then TotallyUnprotected - else if locked && is_main_thread then Protected Excluder.Both - else if locked then Protected Excluder.Lock - else Protected Excluder.Thread + let make locks threads ownership_precondition pdesc = + (* shouldn't be creating metadata for accesses that are known to be owned; we should discard + such accesses *) + assert (not (Precondition.is_true ownership_precondition)) ; + let thread = ThreadsDomain.is_any_but_self threads in + let lock = locks || Procdesc.is_java_synchronized pdesc in + {thread; lock; ownership_precondition} - let make_unprotected indexes = - assert (not (IntSet.is_empty indexes)) ; - Unprotected indexes + let is_unprotected {thread; lock; ownership_precondition} = + not thread && not lock && not (Precondition.is_true ownership_precondition) - let totally_unprotected = TotallyUnprotected + let pp fmt {thread; lock; ownership_precondition} = + F.fprintf fmt "Thread: %b Lock: %b Pre: %a" thread lock Precondition.pp ownership_precondition end module AccessDomain = struct - include AbstractDomain.Map (AccessPrecondition) (PathDomain) + include AbstractDomain.Map (AccessData) (PathDomain) let add_access precondition access_path t = let precondition_accesses = try find precondition t with Not_found -> PathDomain.empty in diff --git a/infer/src/concurrency/RacerDDomain.mli b/infer/src/concurrency/RacerDDomain.mli index dcfec4c2f..34a5792b4 100644 --- a/infer/src/concurrency/RacerDDomain.mli +++ b/infer/src/concurrency/RacerDDomain.mli @@ -141,48 +141,44 @@ module AttributeMapDomain : sig val add_attribute : AccessPath.t -> Attribute.t -> astate -> astate end -(** Excluders: Two things can provide for mutual exclusion: holding a lock, - and knowing that you are on a particular thread. Here, we - abstract it to "some" lock and "any particular" thread (typically, UI thread) - For a more precide semantics we would replace Thread by representatives of - thread id's and Lock by multiple differnet lock id's. - Both indicates that you both know the thread and hold a lock. - There is no need for a lattice relation between Thread, Lock and Both: - you don't ever join Thread and Lock, rather, they are treated pointwise. - **) -module Excluder : sig - type t = Thread | Lock | Both [@@deriving compare] -end +(** Data shared among a set of accesses: current thread, lock(s) held, ownership precondition *) +module AccessData : sig + (** Precondition for owned access; access is owned if it evaluates to ture *) + module Precondition : sig + type t = + | Conjunction of IntSet.t + (** Conjunction of "formal index must be owned" predicates. + true if empty *) + | False + [@@deriving compare] + + val is_true : t -> bool + (** return [true] if the precondition evaluates to true *) + + val pp : F.formatter -> t -> unit [@@warning "-32"] + end -module AccessPrecondition : sig type t = private - | Protected of Excluder.t - (** access potentially protected for mutual exclusion by - lock or thread or both *) - | Unprotected of IntSet.t - (** access rooted in formal(s) at indexes i. Safe if actuals passed at given indexes are - owned (i.e., !owned(i) implies an unsafe access). *) - | TotallyUnprotected (** access is unsafe unless a lock is held in a caller *) + {thread: bool; lock: bool; ownership_precondition: Precondition.t} [@@deriving compare] - val pp : F.formatter -> t -> unit - - val make_protected : LocksDomain.astate -> ThreadsDomain.astate -> Procdesc.t -> t + val make : LocksDomain.astate -> ThreadsDomain.astate -> Precondition.t -> Procdesc.t -> t - val make_unprotected : IntSet.t -> t + val is_unprotected : t -> bool + (** return true if not protected by lock, thread, or ownership *) - val totally_unprotected : t + val pp : F.formatter -> t -> unit end -(** map of access precondition |-> set of accesses. the map should hold all accesses to a +(** map of access metadata |-> set of accesses. the map should hold all accesses to a possibly-unowned access path *) module AccessDomain : sig - include module type of AbstractDomain.Map (AccessPrecondition) (PathDomain) + include module type of AbstractDomain.Map (AccessData) (PathDomain) - val add_access : AccessPrecondition.t -> TraceElem.t -> astate -> astate + val add_access : AccessData.t -> TraceElem.t -> astate -> astate (** add the given (access, precondition) pair to the map *) - val get_accesses : AccessPrecondition.t -> astate -> PathDomain.astate + val get_accesses : AccessData.t -> astate -> PathDomain.astate (** get all accesses with the given precondition *) end diff --git a/infer/tests/codetoanalyze/java/racerd/Dispatch.java b/infer/tests/codetoanalyze/java/racerd/Dispatch.java index 3d8605430..fd1f97315 100644 --- a/infer/tests/codetoanalyze/java/racerd/Dispatch.java +++ b/infer/tests/codetoanalyze/java/racerd/Dispatch.java @@ -75,4 +75,17 @@ public class Dispatch { t.foo(); } + public void callUnderLock(AnnotatedInterface i) { + synchronized(this) { + i.foo(); + } + } + +} + +class Some { + + void callFromElsewhere(Dispatch d, AnnotatedInterface i) { + d.callUnderLock(i); + } } diff --git a/infer/tests/codetoanalyze/java/racerd/Locks.java b/infer/tests/codetoanalyze/java/racerd/Locks.java index 43edc0e5f..30d480612 100644 --- a/infer/tests/codetoanalyze/java/racerd/Locks.java +++ b/infer/tests/codetoanalyze/java/racerd/Locks.java @@ -18,7 +18,6 @@ import java.util.concurrent.locks.ReentrantReadWriteLock; @ThreadSafe public class Locks { - Integer f; Lock mLock; @@ -233,4 +232,35 @@ public class Locks { } } + Object mField2; + + private synchronized void lockedWriteInCallee() { + this.mField2 = null; + } + + public static void ownedLockedReadOk() { + Locks owned = new Locks(); + owned.lockedWriteInCallee(); + } + + public Object unownedReadOk() { + // safe because the only other access to mField is owned + return this.mField2; + } + + Object mField3; + + private synchronized void lockedWriteInCallee2() { + this.mField3 = null; + } + + public void unownedLockedWriteOk() { + lockedWriteInCallee2(); + } + + public Object unownedReadBad() { + return this.mField3; + } + + } diff --git a/infer/tests/codetoanalyze/java/racerd/RaceWithMainThread.java b/infer/tests/codetoanalyze/java/racerd/RaceWithMainThread.java index e64011f5a..9c78610b8 100644 --- a/infer/tests/codetoanalyze/java/racerd/RaceWithMainThread.java +++ b/infer/tests/codetoanalyze/java/racerd/RaceWithMainThread.java @@ -199,8 +199,44 @@ class RaceWithMainThread{ mFld = null; } -} + int mOnlyWrittenOnMain; + + private void conditionalMainThreadWrite1(boolean b) { + if (b) { + OurThreadUtil.assertOnUiThread(); + mOnlyWrittenOnMain = 7; + } + } + // make sure we don't forget what thread the callee write occurred on + public void conditionalMainThreadWriteOk() { + conditionalMainThreadWrite1(true); + } + + int mWrittenOffMain; + + private void conditionalMainThreadWrite2(boolean b) { + if (b) { + OurThreadUtil.assertOnUiThread(); + } else { + mOnlyWrittenOnMain = 7; + } + } + + public void conditionalMainThreadWriteBad() { + conditionalMainThreadWrite2(false); + } + + int mSharedField; + + public void writeAfterConditionalMainThreadInCalleeBad() { + conditionalMainThreadWrite1(true); + // one branch of the callee runs on the main thread, but that doesn't mean we can assume that + // the caller does too + mSharedField = 7; + } + +} // not marked thread-safe class Unmarked { diff --git a/infer/tests/codetoanalyze/java/racerd/issues.exp b/infer/tests/codetoanalyze/java/racerd/issues.exp index 0472c0036..2eccaef79 100644 --- a/infer/tests/codetoanalyze/java/racerd/issues.exp +++ b/infer/tests/codetoanalyze/java/racerd/issues.exp @@ -53,6 +53,7 @@ codetoanalyze/java/racerd/Dispatch.java, void Dispatch.callUnannotatedInterfaceI codetoanalyze/java/racerd/Inference.java, int Inference.read4OutsideSyncBad(), 1, THREAD_SAFETY_VIOLATION, [,access to `&this.codetoanalyze.java.checkers.Inference.mField4`,,access to `&this.codetoanalyze.java.checkers.Inference.mField4`] codetoanalyze/java/racerd/Inference.java, int Inference.unprotectedRead1Bad(), 1, THREAD_SAFETY_VIOLATION, [,access to `&this.codetoanalyze.java.checkers.Inference.mField1`,,access to `&this.codetoanalyze.java.checkers.Inference.mField1`] codetoanalyze/java/racerd/Inference.java, int Inference.unprotectedRead2Bad(), 1, THREAD_SAFETY_VIOLATION, [,access to `&this.codetoanalyze.java.checkers.Inference.mField2`,,access to `&this.codetoanalyze.java.checkers.Inference.mField2`] +codetoanalyze/java/racerd/Locks.java, Object Locks.unownedReadBad(), 1, THREAD_SAFETY_VIOLATION, [,access to `&this.codetoanalyze.java.checkers.Locks.mField3`,,call to void Locks.lockedWriteInCallee2(),access to `&this.codetoanalyze.java.checkers.Locks.mField3`] codetoanalyze/java/racerd/Locks.java, boolean Locks.readOutsideLock1Bad(), 3, THREAD_SAFETY_VIOLATION, [,access to `&this.codetoanalyze.java.checkers.Locks.mField`,,access to `&this.codetoanalyze.java.checkers.Locks.mField`] codetoanalyze/java/racerd/Locks.java, boolean Locks.readOutsideLock2Bad(), 1, THREAD_SAFETY_VIOLATION, [,access to `&this.codetoanalyze.java.checkers.Locks.mField`,,access to `&this.codetoanalyze.java.checkers.Locks.mField`] codetoanalyze/java/racerd/Locks.java, void Locks.FP_unlockOneLock(), 4, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.Locks.f`] @@ -82,6 +83,7 @@ codetoanalyze/java/racerd/Ownership.java, void Ownership.writeToNotOwnedInCallee codetoanalyze/java/racerd/Ownership.java, void Ownership.writeToNotOwnedInCalleeBad3(Obj), 1, THREAD_SAFETY_VIOLATION, [call to void Ownership.callWriteToFormal(Obj),call to void Ownership.writeToFormal(Obj),access to `&formal.codetoanalyze.java.checkers.Obj.f`] codetoanalyze/java/racerd/Ownership.java, void Ownership.writeToOwnedInCalleeOk2(), 4, THREAD_SAFETY_VIOLATION, [,access to `&this.codetoanalyze.java.checkers.Ownership.field`,,access to `&this.codetoanalyze.java.checkers.Ownership.field`] codetoanalyze/java/racerd/RaceWithMainThread.java, void RaceWithMainThread.conditional2_bad(boolean), 6, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.ff`] +codetoanalyze/java/racerd/RaceWithMainThread.java, void RaceWithMainThread.conditionalMainThreadWriteBad(), 1, THREAD_SAFETY_VIOLATION, [call to void RaceWithMainThread.conditionalMainThreadWrite2(boolean),access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.mOnlyWrittenOnMain`] codetoanalyze/java/racerd/RaceWithMainThread.java, void RaceWithMainThread.conditional_isMainThread_ElseBranch_Bad(), 7, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.ff`] codetoanalyze/java/racerd/RaceWithMainThread.java, void RaceWithMainThread.conditional_isMainThread_Negation_Bad(), 3, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.ff`] codetoanalyze/java/racerd/RaceWithMainThread.java, void RaceWithMainThread.conditional_isUiThread_ElseBranch_Bad(), 7, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.ff`] @@ -89,6 +91,7 @@ codetoanalyze/java/racerd/RaceWithMainThread.java, void RaceWithMainThread.confu codetoanalyze/java/racerd/RaceWithMainThread.java, void RaceWithMainThread.readProtectedUnthreadedBad(), 3, THREAD_SAFETY_VIOLATION, [,access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.f`,,access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.f`] codetoanalyze/java/racerd/RaceWithMainThread.java, void RaceWithMainThread.read_unprotected_unthreaded1_Bad(), 2, THREAD_SAFETY_VIOLATION, [,access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.f1`,,access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.f1`] codetoanalyze/java/racerd/RaceWithMainThread.java, void RaceWithMainThread.read_unprotected_unthreaded_Bad(), 2, THREAD_SAFETY_VIOLATION, [,access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.f`,,access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.f`] +codetoanalyze/java/racerd/RaceWithMainThread.java, void RaceWithMainThread.writeAfterConditionalMainThreadInCalleeBad(), 4, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.mSharedField`] codetoanalyze/java/racerd/ReadWriteRaces.java, Object ReadWriteRaces.callUnprotecteReadInCallee(), 1, THREAD_SAFETY_VIOLATION, [,call to Object ReadWriteRaces.unprotectedReadInCallee(),access to `&this.codetoanalyze.java.checkers.ReadWriteRaces.field1`,,access to `&this.codetoanalyze.java.checkers.ReadWriteRaces.field1`] codetoanalyze/java/racerd/ReadWriteRaces.java, Object ReadWriteRaces.unprotectedRead1(), 1, THREAD_SAFETY_VIOLATION, [,access to `&this.codetoanalyze.java.checkers.ReadWriteRaces.field1`,,access to `&this.codetoanalyze.java.checkers.ReadWriteRaces.field1`] codetoanalyze/java/racerd/ReadWriteRaces.java, Object ReadWriteRaces.unprotectedRead2(), 1, THREAD_SAFETY_VIOLATION, [,access to `&this.codetoanalyze.java.checkers.ReadWriteRaces.field2`,,access to `&this.codetoanalyze.java.checkers.ReadWriteRaces.field2`]