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`]