diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index adcfd42ed..51c321716 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -23,7 +23,7 @@ end) (*Bit of redundancy with code in is_unprotected, might alter later *) let make_excluder locks thread = - let is_main_thread = ThreadSafetyDomain.ThreadsDomain.is_main thread in + let is_main_thread = ThreadSafetyDomain.ThreadsDomain.is_any_but_self thread in if locks && not is_main_thread then ThreadSafetyDomain.Excluder.Lock else if not locks && is_main_thread then ThreadSafetyDomain.Excluder.Thread else if locks && is_main_thread then ThreadSafetyDomain.Excluder.Both @@ -292,7 +292,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct (ownership', attribute_map') let is_unprotected is_locked thread pdesc = - not is_locked && not (ThreadSafetyDomain.ThreadsDomain.is_main thread) + not is_locked && not (ThreadSafetyDomain.ThreadsDomain.is_any_but_self thread) && not (Procdesc.is_java_synchronized pdesc) (** return true if this function is library code from the JDK core libraries or Android *) @@ -513,8 +513,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct in (* we need a more intelligent escape analysis, that branches on whether we own the container *) Some - { locks= false - ; threads= ThreadsDomain.Unknown + { + locks= false + ; threads= ThreadsDomain.empty ; accesses= callee_accesses ; return_ownership= OwnershipAbstractValue.unowned ; return_attributes= AttributeSetDomain.empty } @@ -586,9 +587,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let astate = match get_thread_model callee_pname with | BackgroundThread - -> {astate with threads= ThreadsDomain.Background} + -> {astate with threads= ThreadsDomain.AnyThread} | MainThread - -> {astate with threads= ThreadsDomain.Main} + -> {astate with threads= ThreadsDomain.AnyThreadButSelf} | MainThreadIfTrue -> ( match ret_opt with | Some ret_access_path @@ -607,7 +608,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let astate_callee = (* assuming that modeled procedures do not have useful summaries *) if is_thread_utils_method "assertMainThread" callee_pname then - {astate with threads= ThreadsDomain.Main} + {astate with threads= ThreadsDomain.AnyThreadButSelf} else match get_lock_model callee_pname actuals with | Lock @@ -637,7 +638,15 @@ module TransferFunctions (CFG : ProcCfg.S) = struct AccessDomain.add pre combined_accesses caller_accesses in let locks = locks || astate.locks in - let threads = ThreadsDomain.join threads astate.threads in + let threads = + match (astate.threads, threads) with + | _, ThreadsDomain.AnyThreadButSelf | AnyThreadButSelf, _ + -> ThreadsDomain.AnyThreadButSelf + | _, ThreadsDomain.AnyThread + -> astate.threads + | _ + -> ThreadsDomain.join threads astate.threads + in let unprotected = is_unprotected locks threads pdesc in (* add [ownership_accesses] to the [accesses_acc] with a protected pre if [exp] is owned, and an appropriate unprotected pre otherwise *) @@ -834,7 +843,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct -> let locks = bool_value in {acc with locks} | Choice.OnMainThread - -> let threads = if bool_value then ThreadsDomain.Main else ThreadsDomain.Background in + -> let threads = + if bool_value then ThreadsDomain.AnyThreadButSelf else ThreadsDomain.AnyThread + in {acc with threads} in let accesses = @@ -849,7 +860,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct match eval_bexp access_path assume_exp with | Some bool_value -> (* prune (prune_exp) can only evaluate to true if the choice is [bool_value]. - add the constraint that the the choice must be [bool_value] to the state *) + add the constraint that the the choice must be [bool_value] to the state *) List.fold ~f:(add_choice bool_value) ~init:astate choices | None -> astate ) @@ -944,15 +955,43 @@ let should_analyze_proc pdesc tenv = && not (is_call_to_immutable_collection_method tenv pn) && not (pdesc_is_assumed_thread_safe pdesc tenv) -let is_thread_safe_method pdesc tenv = +let get_current_class_and_threadsafe_superclasses tenv pname = + match pname with + | Typ.Procname.Java java_pname + -> let current_class = Typ.Procname.java_get_class_type_name java_pname in + let thread_safe_annotated_classes = + PatternMatch.find_superclasses_with_attributes is_thread_safe tenv current_class + in + Some (current_class, thread_safe_annotated_classes) + | _ + -> None + +let is_thread_safe_class pname tenv = + not + ((* current class not marked thread-safe *) + PatternMatch.check_current_class_attributes Annotations.ia_is_not_thread_safe tenv pname) + && + (* current class or superclass is marked thread-safe *) + match get_current_class_and_threadsafe_superclasses tenv pname with + | Some (_, thread_safe_annotated_classes) + -> not (List.is_empty thread_safe_annotated_classes) + | _ + -> false + +let is_thread_safe_method pname tenv = PatternMatch.override_exists (fun pn -> Annotations.pname_has_return_annot pn ~attrs_of_pname:Specs.proc_resolve_attributes is_thread_safe) - tenv (Procdesc.get_proc_name pdesc) + tenv pname + +let is_marked_thread_safe pdesc tenv = + let pname = Procdesc.get_proc_name pdesc in + is_thread_safe_class pname tenv || is_thread_safe_method pname tenv let empty_post : ThreadSafetyDomain.summary = - { threads= ThreadSafetyDomain.ThreadsDomain.Unknown + { + threads= ThreadSafetyDomain.ThreadsDomain.empty ; locks= false ; accesses= ThreadSafetyDomain.AccessDomain.empty ; return_ownership= ThreadSafetyDomain.OwnershipAbstractValue.unowned @@ -971,10 +1010,9 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} = let initial = let threads = if runs_on_ui_thread proc_desc || is_thread_confined_method tenv proc_desc then - (* note: modeling @ThreadConfined as running on main thread for now, but should probably - change in the future *) - ThreadsDomain.Main - else ThreadsDomain.Unknown + ThreadsDomain.AnyThreadButSelf + else if is_marked_thread_safe proc_desc tenv then ThreadsDomain.AnyThread + else ThreadsDomain.NoThread in if is_initializer tenv (Procdesc.get_proc_name proc_desc) then let add_owned_formal acc formal_index = @@ -1027,34 +1065,34 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} = module AccessListMap = Caml.Map.Make (ThreadSafetyDomain.Access) -let get_current_class_and_threadsafe_superclasses tenv pname = - match pname with - | Typ.Procname.Java java_pname - -> let current_class = Typ.Procname.java_get_class_type_name java_pname in - let thread_safe_annotated_classes = - PatternMatch.find_superclasses_with_attributes is_thread_safe tenv current_class - in - Some (current_class, thread_safe_annotated_classes) - | _ - -> None - -(*shouldn't happen*) - -(** The addendum message says that a superclass is marked @ThreadSafe, - when the current class is not so marked*) -let calculate_addendum_message tenv pname = +(** Explain why we are reporting this access *) +let get_reporting_explanation tenv pname thread = + let thread_assumption = + if ThreadSafetyDomain.ThreadsDomain.is_any thread then + F.asprintf + "so we assume that this method can run in parallel with other non-private methods in the class (incuding itself)" + else + "and another access to the same memory may occur on a background thread even though this access may not" + in match get_current_class_and_threadsafe_superclasses tenv pname with - | Some (current_class, thread_safe_annotated_classes) - -> if not (List.mem ~equal:Typ.Name.equal thread_safe_annotated_classes current_class) then - match thread_safe_annotated_classes with - | hd :: _ - -> F.asprintf "@\n Note: Superclass %a is marked %a." (MF.wrap_monospaced Typ.Name.pp) hd - MF.pp_monospaced "@ThreadSafe" - | [] - -> "" - else "" + | Some (current_class, (thread_safe_class :: _ as thread_safe_annotated_classes)) + -> if List.mem ~equal:Typ.Name.equal thread_safe_annotated_classes current_class then + F.asprintf "@\n Reporting because the current class is annotated %a, %s." MF.pp_monospaced + "@ThreadSafe" thread_assumption + else + F.asprintf "@\n Reporting because a superclass %a is annotated %a, %s." + (MF.wrap_monospaced Typ.Name.pp) thread_safe_class MF.pp_monospaced "@ThreadSafe" + thread_assumption | _ - -> "" + -> if is_thread_safe_method pname tenv then + F.asprintf + "@\n Reporting because current method is annotated %a or overrides an annotated method, %s." + MF.pp_monospaced "@ThreadSafe" thread_assumption + else if ThreadSafetyDomain.ThreadsDomain.is_any thread then + F.asprintf "@\n Reporting because this access may occur on a background thread." + else + F.asprintf + "@\n Reporting because another access to the same memory may run on a background thread." let filter_by_access access_filter trace = let open ThreadSafetyDomain in @@ -1140,7 +1178,7 @@ let make_trace_with_conflicts conflicts original_path pdesc = | [] -> original_trace -let report_thread_safety_violation tenv pdesc issue_type ~make_description ~conflicts access = +let report_thread_safety_violation tenv pdesc issue_type ~make_description ~conflicts access thread = let open ThreadSafetyDomain in let pname = Procdesc.get_proc_name pdesc in let report_one_path (_, sinks as path) = @@ -1150,7 +1188,9 @@ let report_thread_safety_violation tenv pdesc issue_type ~make_description ~conf let final_sink_site = PathDomain.Sink.call_site final_sink in let loc = CallSite.loc initial_sink_site in let ltr = make_trace_with_conflicts conflicts path pdesc in - let description = make_description tenv pname final_sink_site initial_sink_site final_sink in + let description = + make_description tenv pname final_sink_site initial_sink_site final_sink thread + in let exn = Exceptions.Checkers (issue_type.IssueType.unique_id, Localise.verbatim_desc description) in @@ -1159,17 +1199,17 @@ let report_thread_safety_violation tenv pdesc issue_type ~make_description ~conf let trace_of_pname = trace_of_pname access pdesc in Option.iter ~f:report_one_path (PathDomain.get_reportable_sink_path access ~trace_of_pname) -let report_unannotated_interface_violation tenv pdesc access reported_pname = +let report_unannotated_interface_violation tenv pdesc access thread reported_pname = match reported_pname with | Typ.Procname.Java java_pname -> let class_name = Typ.Procname.java_get_class_name java_pname in - let make_description _ _ _ _ _ = + let make_description _ _ _ _ _ _ = F.asprintf "Unprotected call to method of un-annotated interface %s. Consider annotating the class with %a, adding a lock, or using an interface that is known to be thread-safe." class_name MF.pp_monospaced "@ThreadSafe" in report_thread_safety_violation tenv pdesc IssueType.interface_not_thread_safe - ~make_description ~conflicts:[] access + ~make_description ~conflicts:[] access thread | _ -> (* skip reporting on C++ *) () @@ -1181,21 +1221,16 @@ let pp_procname_short fmt = function | pname -> Typ.Procname.pp fmt pname -let make_unprotected_write_description tenv pname final_sink_site initial_sink_site final_sink = +let make_unprotected_write_description tenv pname final_sink_site initial_sink_site final_sink + write_thread = Format.asprintf "Unprotected write. Non-private method %a%s %s %a outside of synchronization.%s" (MF.wrap_monospaced pp_procname_short) pname (if CallSite.equal final_sink_site initial_sink_site then "" else " indirectly") ( if ThreadSafetyDomain.TraceElem.is_container_write final_sink then "mutates" else "writes to field" ) - pp_access final_sink (calculate_addendum_message tenv pname) + pp_access final_sink (get_reporting_explanation tenv pname write_thread) -let make_read_write_race_description ~read_is_sync conflicts tenv pname final_sink_site - initial_sink_site final_sink = - let race_with_main_thread = - List.exists - ~f:(fun (_, _, thread, _, _) -> ThreadSafetyDomain.ThreadsDomain.is_main thread) - conflicts - in +let make_read_write_race_description ~read_is_sync conflicts tenv pname final_sink_site initial_sink_site final_sink read_thread = let conflicting_proc_names = List.map ~f:(fun (_, _, _, _, pdesc) -> Procdesc.get_proc_name pdesc) conflicts |> Typ.Procname.Set.of_list @@ -1206,19 +1241,16 @@ let make_read_write_race_description ~read_is_sync conflicts tenv pname final_si else Typ.Procname.Set.pp fmt conflicts in let conflicts_description = - Format.asprintf "Potentially races with%s writes in method%s %a. %s" + Format.asprintf "Potentially races with%s writes in method%s %a." (if read_is_sync then " unsynchronized" else " synchronized") (if Typ.Procname.Set.cardinal conflicting_proc_names > 1 then "s" else "") (MF.wrap_monospaced pp_conflicts) conflicting_proc_names - ( if race_with_main_thread then - "\n Note: some of these write conflicts are confined to the UI or another thread, but the current method is not specified to be. Consider adding synchronization or a @ThreadConfined annotation to the current method." - else "" ) in - Format.asprintf "Read/Write race. Non-private method %a%s reads%s from %a. %s %s" + Format.asprintf "Read/Write race. Non-private method %a%s reads%s from %a. %s%s" (MF.wrap_monospaced pp_procname_short) pname (if CallSite.equal final_sink_site initial_sink_site then "" else " indirectly") (if read_is_sync then " with synchronization" else " without synchronization") - pp_access final_sink conflicts_description (calculate_addendum_message tenv pname) + pp_access final_sink conflicts_description (get_reporting_explanation tenv pname read_thread) (** type for remembering what we have already reported to avoid duplicates. our policy is to report each kind of access (read/write) to the same field reachable from the same procedure only once. @@ -1239,7 +1271,7 @@ let empty_reported = requested via @ThreadSafe *) let should_report_on_proc proc_desc tenv = let proc_name = Procdesc.get_proc_name proc_desc in - is_thread_safe_method proc_desc tenv + is_thread_safe_method proc_name tenv || not (Typ.Procname.java_is_autogen_method proc_name) && Procdesc.get_access proc_desc <> PredSymb.Private && not (Annotations.pdesc_return_annot_ends_with proc_desc Annotations.visibleForTesting) @@ -1315,9 +1347,11 @@ let report_unsafe_accesses match (TraceElem.kind access, pre) with | ( Access.InterfaceCall unannoted_call_pname , (AccessPrecondition.Unprotected _ | AccessPrecondition.TotallyUnprotected) ) - -> (* un-annotated interface call + no lock. warn *) - report_unannotated_interface_violation tenv pdesc access unannoted_call_pname ; - update_reported access pname reported_acc + -> if ThreadsDomain.is_any thread && is_marked_thread_safe pdesc tenv then ( + (* un-annotated interface call + no lock in method marked thread-safe. warn *) + report_unannotated_interface_violation tenv pdesc access thread 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 @@ -1325,14 +1359,15 @@ let report_unsafe_accesses , (AccessPrecondition.Unprotected _ | AccessPrecondition.TotallyUnprotected) ) -> ( match Procdesc.get_proc_name pdesc with | Java _ - -> if ThreadsDomain.is_main thread then reported_acc - else ( - (* unprotected write. warn. *) - report_thread_safety_violation tenv pdesc IssueType.thread_safety_violation - ~make_description:make_unprotected_write_description ~conflicts:[] access ; - update_reported access pname reported_acc ) + -> (** TODO: use a better warning message when the thread is anything but Any (perhaps + show the write that this may race with) *) + (* unprotected write. warn. *) + report_thread_safety_violation tenv pdesc IssueType.thread_safety_violation + ~make_description:make_unprotected_write_description ~conflicts:[] access thread ; + update_reported access pname reported_acc | _ - -> (* Do not report unprotected writes for ObjC_Cpp *) + -> (* 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 *) @@ -1352,7 +1387,8 @@ let report_unsafe_accesses List.filter ~f:(fun (other_access, pre, other_thread, _, _) -> TraceElem.is_write other_access - && not (ThreadsDomain.is_main thread && ThreadsDomain.is_main other_thread) + && ( not (Typ.Procname.is_java pname) || ThreadsDomain.is_any thread + || ThreadsDomain.is_any other_thread ) && is_cpp_protected_write pre) accesses in @@ -1361,7 +1397,7 @@ let report_unsafe_accesses report_thread_safety_violation tenv pdesc IssueType.thread_safety_violation ~make_description:(make_read_write_race_description ~read_is_sync:false all_writes) ~conflicts:(List.map ~f:(fun (access, _, _, _, _) -> access) all_writes) - access ; + access thread ; update_reported access pname reported_acc ) | (Access.Read _ | ContainerRead _), AccessPrecondition.Protected excl -> (* protected read. @@ -1395,7 +1431,7 @@ let report_unsafe_accesses ~make_description: (make_read_write_race_description ~read_is_sync:true conflicting_writes) ~conflicts:(List.map ~f:(fun (access, _, _, _, _) -> access) conflicting_writes) - access ; + access thread ; update_reported access pname reported_acc ) in AccessListMap.fold @@ -1405,11 +1441,6 @@ let report_unsafe_accesses { reported_acc with reported_writes= Typ.Procname.Set.empty; reported_reads= Typ.Procname.Set.empty } in - let accessed_by_threadsafe_method = - List.exists - ~f:(fun (_, _, _, tenv, pdesc) -> is_thread_safe_method pdesc tenv) - grouped_accesses - in let class_has_mutex_member objc_cpp tenv = let class_name = Typ.Procname.objc_cpp_get_class_type_name objc_cpp in let matcher = QualifiedCppName.Match.of_fuzzy_qual_names ["std::mutex"] in @@ -1421,31 +1452,14 @@ let report_unsafe_accesses in let should_report pdesc tenv = match Procdesc.get_proc_name pdesc with - | Java _ as pname + | Java _ -> (* report if - the method/class of the access is thread-safe (or an override or superclass is), or - any access is in a field marked thread-safe (or an override) *) - ( accessed_by_threadsafe_method - || - let is_class_threadsafe = - not - (let current_class_marked_not_threadsafe = - PatternMatch.check_current_class_attributes Annotations.ia_is_not_thread_safe - tenv pname - in - current_class_marked_not_threadsafe) - && - let current_class_or_super_marked_threadsafe = - match get_current_class_and_threadsafe_superclasses tenv pname with - | Some (_, thread_safe_annotated_classes) - -> not (List.is_empty thread_safe_annotated_classes) - | _ - -> false - in - current_class_or_super_marked_threadsafe - in - is_class_threadsafe ) + List.exists + ~f:(fun (_, _, thread, _, _) -> ThreadsDomain.is_any thread) + grouped_accesses && should_report_on_proc pdesc tenv | ObjC_Cpp objc_cpp -> (* do not report if a procedure is private *) diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml index 03d06ff14..cd2f28c5e 100644 --- a/infer/src/checkers/ThreadSafetyDomain.ml +++ b/infer/src/checkers/ThreadSafetyDomain.ml @@ -130,56 +130,50 @@ let make_unannotated_call_access pname loc = module LocksDomain = AbstractDomain.BooleanAnd module ThreadsDomain = struct - type astate = Unknown | Main | Background | Any + type astate = NoThread | AnyThreadButSelf | AnyThread [@@deriving compare] - let empty = Unknown + let empty = NoThread + (* NoThread < AnyThreadButSelf < Any *) let ( <= ) ~lhs ~rhs = match (lhs, rhs) with - | Unknown, Unknown | Main, Main | Background, Background | Any, Any + | NoThread, _ -> true - | Unknown, _ - -> true - | _, Unknown + | _, NoThread -> false - | _, Any + | _, AnyThread -> true - | Any, _ + | AnyThread, _ -> false | _ - -> (* Unknown is bottom, Any is top, other elements are incomparable *) - false + -> Int.equal 0 (compare_astate lhs rhs) let join astate1 astate2 = match (astate1, astate2) with - | Unknown, astate | astate, Unknown + | NoThread, astate | astate, NoThread -> astate - | Any, _ | _, Any - -> Any - | Main, Main | Background, Background - -> astate1 - | Main, Background | Background, Main - -> Any + | AnyThread, _ | _, AnyThread + -> AnyThread + | AnyThreadButSelf, AnyThreadButSelf + -> AnyThreadButSelf let widen ~prev ~next ~num_iters:_ = join prev next let pp fmt astate = F.fprintf fmt ( match astate with - | Unknown - -> "Unknown" - | Main - -> "Main" - | Background - -> "Background" - | Any - -> "Any" ) + | NoThread + -> "NoThread" + | AnyThreadButSelf + -> "AnyThreadButSelf" + | AnyThread + -> "AnyThread" ) - let is_unknown = function Unknown -> true | _ -> false + let is_empty = function NoThread -> true | _ -> false - let is_empty = is_unknown + let is_any_but_self = function AnyThreadButSelf -> true | _ -> false - let is_main = function Main -> true | _ -> false + let is_any = function AnyThread -> true | _ -> false end module PathDomain = SinkTrace.Make (TraceElem) @@ -354,7 +348,7 @@ type astate = ; attribute_map: AttributeMapDomain.astate } let empty = - let threads = ThreadsDomain.Unknown in + let threads = ThreadsDomain.empty in let locks = false in let accesses = AccessDomain.empty in let ownership = OwnershipDomain.empty in @@ -362,7 +356,7 @@ let empty = {threads; locks; accesses; ownership; attribute_map} let is_empty {threads; locks; accesses; ownership; attribute_map} = - ThreadsDomain.is_unknown threads && not locks && AccessDomain.is_empty accesses + ThreadsDomain.is_empty threads && not locks && AccessDomain.is_empty accesses && OwnershipDomain.is_empty ownership && AttributeMapDomain.is_empty attribute_map let ( <= ) ~lhs ~rhs = diff --git a/infer/src/checkers/ThreadSafetyDomain.mli b/infer/src/checkers/ThreadSafetyDomain.mli index 948fdd3cc..b208c5255 100644 --- a/infer/src/checkers/ThreadSafetyDomain.mli +++ b/infer/src/checkers/ThreadSafetyDomain.mli @@ -46,18 +46,26 @@ end and which memory locations correspond to the same lock. *) module LocksDomain : AbstractDomain.S with type astate = bool +(** Abstraction of threads that may run in parallel with the current thread. + NoThread < AnyThreadExceptSelf < AnyThread *) module ThreadsDomain : sig type astate = - | Unknown (** Unknown thread; bottom element of the lattice *) - | Main (** Main thread. Accesses here cannot race with other accesses on the main thread *) - | Background - (** Background thread. Accesses here can race with the main thread or other background - threads *) - | Any (** Any thread; top element of the lattice. *) + | NoThread + (** No threads can run in parallel with the current thread (concretization: empty set). We + assume this by default unless we see evidence to the contrary (annotations, use of locks, + etc.) *) + | AnyThreadButSelf + (** Current thread can run in parallel with other threads, but not with itself. + (concretization : { t | t \in TIDs ^ t != t_cur } ) *) + | AnyThread + (** Current thread can run in parallel with any thread, including itself (concretization: set + of all TIDs ) *) include AbstractDomain.WithBottom with type astate := astate - val is_main : astate -> bool + val is_any_but_self : astate -> bool + + val is_any : astate -> bool end module PathDomain : module type of SinkTrace.Make (TraceElem) diff --git a/infer/tests/codetoanalyze/java/threadsafety/Annotations.java b/infer/tests/codetoanalyze/java/threadsafety/Annotations.java index 3e4b78599..b907fe7b3 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/Annotations.java +++ b/infer/tests/codetoanalyze/java/threadsafety/Annotations.java @@ -177,12 +177,12 @@ class Annotations implements Interface { ii = 22; } - void conditional2_ok(boolean b){ + void conditional2_bad(boolean b){ if (b) { write_on_main_thread_ok(); } else { - ii = 99; // this might or might not run on the main thread; don't warn + ii = 99; // this might or might not run on the main thread; warn } } diff --git a/infer/tests/codetoanalyze/java/threadsafety/RaceWithMainThread.java b/infer/tests/codetoanalyze/java/threadsafety/RaceWithMainThread.java index a07dc97f7..e64011f5a 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/RaceWithMainThread.java +++ b/infer/tests/codetoanalyze/java/threadsafety/RaceWithMainThread.java @@ -121,13 +121,13 @@ class RaceWithMainThread{ } } - void conditional2_Ok(boolean b){ + void conditional2_bad(boolean b){ if (b) { OurThreadUtils.assertMainThread(); ff = 88; } else { - ff = 99; // this might or might now run on the main thread; don't warn + ff = 99; // this might or might now run on the main thread; warn } } @@ -200,3 +200,27 @@ class RaceWithMainThread{ } } + + +// not marked thread-safe +class Unmarked { + + int mField; + + void writeOnUiThreadOk() { + OurThreadUtil.assertOnUiThread(); + mField = 7; + } + + int readOnUiThreadOk() { + OurThreadUtil.assertOnUiThread(); + return mField; + } + + int readOffUiThreadOk() { + // even though this read isn't known to be on the UI thread, we shouldn't assume that it occurs + // on a background thread + return mField; + } + +} diff --git a/infer/tests/codetoanalyze/java/threadsafety/ThreadSafeExample.java b/infer/tests/codetoanalyze/java/threadsafety/ThreadSafeExample.java index b99b93db8..7c35361d0 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/ThreadSafeExample.java +++ b/infer/tests/codetoanalyze/java/threadsafety/ThreadSafeExample.java @@ -123,6 +123,17 @@ public class ThreadSafeExample{ return this.sharedField; // ok because it only races with a private method } + Object sStaticField; + + public Object FP_lazyInitOk() { + synchronized (ThreadSafeExample.class) { + if (sStaticField != null) { + sStaticField = new Object(); + } + } + return sStaticField; // we'll warn here, although this is fine + } + } class ExtendsThreadSafeExample extends ThreadSafeExample{ @@ -165,3 +176,21 @@ class YesThreadSafeExtendsNotThreadSafeExample extends NotThreadSafeExtendsThrea } } + +class Unannotated { + int mField; + + // although ThreadSafeExample is annotated @ThreadSafe, mutating fields of this class in a + // non-threadsafe context should be allowed + void callThreadSafeAnnotatedCode1Ok(ThreadSafeExample o) { + o.f = null; + } + + void callThreadSafeAnnotatedCode2Ok(ThreadSafeExample o) { + o.tsBad(); + } + + void mutateMyFieldOk() { + this.mField = 1; + } +} diff --git a/infer/tests/codetoanalyze/java/threadsafety/ThreadSafeMethods.java b/infer/tests/codetoanalyze/java/threadsafety/ThreadSafeMethods.java index ccc1c0e0e..24b10ab95 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/ThreadSafeMethods.java +++ b/infer/tests/codetoanalyze/java/threadsafety/ThreadSafeMethods.java @@ -95,8 +95,8 @@ class ThreadSafeMethods { this.field5 = new Object(); } - // unprotected read of a field that is read safely in a method marked thread-safe - public Object readSameFieldAsThreadSafeMethod3Bad() { + // none of the writes are marked thread-safe/locked, no reason to report + public Object readSameFieldAsThreadSafeMethodOk() { return this.field5; } diff --git a/infer/tests/codetoanalyze/java/threadsafety/issues.exp b/infer/tests/codetoanalyze/java/threadsafety/issues.exp index bfc5bd923..10e19f897 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/issues.exp +++ b/infer/tests/codetoanalyze/java/threadsafety/issues.exp @@ -6,6 +6,7 @@ codetoanalyze/java/threadsafety/Annotations.java, double Annotations.functionalD codetoanalyze/java/threadsafety/Annotations.java, int Annotations.FP_functionalAcrossBoxingLongOk(), 2, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.Annotations.mBoxedLong2`] codetoanalyze/java/threadsafety/Annotations.java, int Annotations.functionalAcrossUnboxingLongBad(), 2, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.Annotations.mLong2`] codetoanalyze/java/threadsafety/Annotations.java, long Annotations.functionaLongBad(), 2, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.Annotations.mLong`] +codetoanalyze/java/threadsafety/Annotations.java, void Annotations.conditional2_bad(boolean), 5, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.Annotations.ii`] codetoanalyze/java/threadsafety/Annotations.java, void Annotations.functionalAndNonfunctionalBad(), 1, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.Annotations.mInt`] codetoanalyze/java/threadsafety/Annotations.java, void Annotations.mutateOffUiThreadBad(), 1, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.Annotations.f`] codetoanalyze/java/threadsafety/Annotations.java, void Annotations.mutateSubfieldOfConfinedBad(), 1, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.Annotations.encapsulatedField.codetoanalyze.java.checkers.Obj.f`] @@ -71,6 +72,7 @@ codetoanalyze/java/threadsafety/Ownership.java, void Ownership.writeToNotOwnedIn codetoanalyze/java/threadsafety/Ownership.java, void Ownership.writeToNotOwnedInCalleeBad2(), 2, THREAD_SAFETY_VIOLATION, [call to void Ownership.writeToFormal(Obj),access to `&formal.codetoanalyze.java.checkers.Obj.f`] codetoanalyze/java/threadsafety/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/threadsafety/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/threadsafety/RaceWithMainThread.java, void RaceWithMainThread.conditional2_bad(boolean), 6, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.ff`] codetoanalyze/java/threadsafety/RaceWithMainThread.java, void RaceWithMainThread.conditional_isMainThread_ElseBranch_Bad(), 7, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.ff`] codetoanalyze/java/threadsafety/RaceWithMainThread.java, void RaceWithMainThread.conditional_isMainThread_Negation_Bad(), 3, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.ff`] codetoanalyze/java/threadsafety/RaceWithMainThread.java, void RaceWithMainThread.conditional_isUiThread_ElseBranch_Bad(), 7, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.RaceWithMainThread.ff`] @@ -87,6 +89,7 @@ codetoanalyze/java/threadsafety/ReadWriteRaces.java, void ReadWriteRaces.m2(), 1 codetoanalyze/java/threadsafety/ReadWriteRaces.java, void ReadWriteRaces.m3(), 1, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.ReadWriteRaces.racy`] codetoanalyze/java/threadsafety/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/threadsafety/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/threadsafety/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/threadsafety/ThreadSafeExample.java, void ExtendsThreadSafeExample.newmethodBad(), 1, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.ExtendsThreadSafeExample.field`] codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ExtendsThreadSafeExample.tsOK(), 1, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.ExtendsThreadSafeExample.field`] codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.callPublicMethodBad(), 1, THREAD_SAFETY_VIOLATION, [call to void ThreadSafeExample.assignInPrivateMethodOk(),access to `&this.codetoanalyze.java.checkers.ThreadSafeExample.f`] @@ -98,7 +101,6 @@ codetoanalyze/java/threadsafety/ThreadSafeExample.java, void ThreadSafeExample.t codetoanalyze/java/threadsafety/ThreadSafeExample.java, void YesThreadSafeExtendsNotThreadSafeExample.subsubmethodBad(), 1, THREAD_SAFETY_VIOLATION, [access to `&this.codetoanalyze.java.checkers.YesThreadSafeExtendsNotThreadSafeExample.subsubfield`] codetoanalyze/java/threadsafety/ThreadSafeMethods.java, Object ThreadSafeMethods.readSameFieldAsThreadSafeMethod1Bad(), 1, THREAD_SAFETY_VIOLATION, [,access to `&this.codetoanalyze.java.checkers.ThreadSafeMethods.field1`,,access to `&this.codetoanalyze.java.checkers.ThreadSafeMethods.field1`] codetoanalyze/java/threadsafety/ThreadSafeMethods.java, Object ThreadSafeMethods.readSameFieldAsThreadSafeMethod2Bad(), 1, THREAD_SAFETY_VIOLATION, [,access to `&this.codetoanalyze.java.checkers.ThreadSafeMethods.field4`,,access to `&this.codetoanalyze.java.checkers.ThreadSafeMethods.field4`] -codetoanalyze/java/threadsafety/ThreadSafeMethods.java, Object ThreadSafeMethods.readSameFieldAsThreadSafeMethod3Bad(), 1, THREAD_SAFETY_VIOLATION, [,access to `&this.codetoanalyze.java.checkers.ThreadSafeMethods.field5`,,access to `&this.codetoanalyze.java.checkers.ThreadSafeMethods.field5`] codetoanalyze/java/threadsafety/ThreadSafeMethods.java, Object ThreadSafeMethods.readSameFieldAsThreadSafeMethodWhileSynchronized1Bad(), 1, THREAD_SAFETY_VIOLATION, [,access to `&this.codetoanalyze.java.checkers.ThreadSafeMethods.field1`,,access to `&this.codetoanalyze.java.checkers.ThreadSafeMethods.field1`] codetoanalyze/java/threadsafety/ThreadSafeMethods.java, Object ThreadSafeMethods.synchronizedReadBad(), 1, THREAD_SAFETY_VIOLATION, [,access to `&this.codetoanalyze.java.checkers.ThreadSafeMethods.field5`,,access to `&this.codetoanalyze.java.checkers.ThreadSafeMethods.field5`] codetoanalyze/java/threadsafety/ThreadSafeMethods.java, Object ThreadSafeMethods.threadSafeMethodReadBad(), 1, THREAD_SAFETY_VIOLATION, [,access to `&this.codetoanalyze.java.checkers.ThreadSafeMethods.field2`,,access to `&this.codetoanalyze.java.checkers.ThreadSafeMethods.field2`]