diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index 2af25d7f4..875b3b42d 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -22,10 +22,11 @@ module Summary = Summary.Make (struct end) (*Bit of redundancy with code in is_unprotected, might alter later *) -let make_excluder locks threads = - if locks && not threads then ThreadSafetyDomain.Excluder.Lock - else if not locks && threads then ThreadSafetyDomain.Excluder.Thread - else if locks && threads then ThreadSafetyDomain.Excluder.Both +let make_excluder locks thread = + let is_main_thread = ThreadSafetyDomain.ThreadsDomain.is_main 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 else L.(die InternalError) "called when neither lock nor thread known" module TransferFunctions (CFG : ProcCfg.S) = struct @@ -36,7 +37,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct type lock_model = Lock | Unlock | LockedIfTrue | NoEffect - type thread_model = Threaded | Unknown | ThreadedIfTrue + type thread_model = MainThread | MainThreadIfTrue | Unknown type container_access_model = ContainerRead | ContainerWrite @@ -122,14 +123,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct -> if is_thread_utils_type java_pname then match Typ.Procname.java_get_method java_pname with | "assertMainThread" | "checkOnMainThread" | "assertOnUiThread" - -> Threaded + -> MainThread | "isMainThread" | "isUiThread" - -> ThreadedIfTrue + -> MainThreadIfTrue | _ -> Unknown else Unknown - (*Note we are not modelling assertOnNonUiThread or - assertOnBackgroundThread. These treated as Unknown*) + (* TODO: we can model this now *) + (* Note we are not modelling assertOnNonUiThread or assertOnBackgroundThread. These treated as Unknown *) | _ -> Unknown @@ -292,8 +293,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let attribute_map' = AttributeMapDomain.add ret_access_path ret_attributes attribute_map in (ownership', attribute_map') - let is_unprotected is_locked is_threaded pdesc = - not is_locked && not is_threaded && not (Procdesc.is_java_synchronized pdesc) + let is_unprotected is_locked thread pdesc = + not is_locked && not (ThreadSafetyDomain.ThreadsDomain.is_main thread) + && not (Procdesc.is_java_synchronized pdesc) (** return true if this function is library code from the JDK core libraries or Android *) let is_java_library = function @@ -518,7 +520,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct Some { thumbs_up= true ; locks= false - ; threads= false + ; threads= ThreadsDomain.Unknown ; accesses= callee_accesses ; return_ownership= OwnershipAbstractValue.unowned ; return_attributes= AttributeSetDomain.empty @@ -606,9 +608,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct let astate = {astate with accesses} in let astate = match get_thread_model callee_pname with - | Threaded - -> {astate with threads= true} - | ThreadedIfTrue -> ( + | MainThread + -> {astate with threads= ThreadsDomain.Main} + | MainThreadIfTrue -> ( match ret_opt with | Some ret_access_path -> let attribute_map = @@ -625,7 +627,8 @@ module TransferFunctions (CFG : ProcCfg.S) = struct in let astate_callee = (* assuming that modeled procedures do not have useful summaries *) - if is_thread_utils_method "assertMainThread" callee_pname then {astate with threads= true} + if is_thread_utils_method "assertMainThread" callee_pname then + {astate with threads= ThreadsDomain.Main} else match get_lock_model callee_pname actuals with | Lock @@ -663,7 +666,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct in let thumbs_up = thumbs_up && astate.thumbs_up in let locks = locks || astate.locks in - let threads = threads || astate.threads in + let 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 *) @@ -866,7 +869,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct -> let locks = bool_value in {acc with locks} | Choice.OnMainThread - -> let threads = bool_value in + -> let threads = if bool_value then ThreadsDomain.Main else ThreadsDomain.Background in {acc with threads} in let accesses = @@ -917,7 +920,7 @@ let is_call_to_immutable_collection_method tenv = function | _ -> false -(* Methods in @ThreadConfined classes and methods annotated with @ThreadConfied are assumed to all +(* Methods in @ThreadConfined classes and methods annotated with @ThreadConfined are assumed to all run on the same thread. For the moment we won't warn on accesses resulting from use of such methods at all. In future we should account for races between these methods and methods from completely different classes that don't necessarily run on the same thread as the confined @@ -985,7 +988,7 @@ let is_thread_safe_method pdesc tenv = let empty_post : ThreadSafetyDomain.summary = { ThreadSafetyDomain.thumbs_up= true - ; threads= false + ; threads= ThreadSafetyDomain.ThreadsDomain.Unknown ; locks= false ; accesses= ThreadSafetyDomain.AccessDomain.empty ; return_ownership= ThreadSafetyDomain.OwnershipAbstractValue.unowned @@ -1003,7 +1006,13 @@ let analyze_procedure {Callbacks.proc_desc; tenv; summary} = let formal_map = FormalMap.make proc_desc in let proc_data = ProcData.make_default proc_desc tenv in let initial = - let threads = runs_on_ui_thread proc_desc || is_thread_confined_method tenv proc_desc in + 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 + in if is_initializer tenv (Procdesc.get_proc_name proc_desc) then let add_owned_formal acc formal_index = match FormalMap.get_formal_base formal_index formal_map with @@ -1240,7 +1249,11 @@ let make_unprotected_write_description tenv pname final_sink_site initial_sink_s let make_read_write_race_description conflicts tenv pname final_sink_site initial_sink_site final_sink = - let race_with_main_thread = List.exists ~f:(fun (_, _, threaded, _, _) -> threaded) conflicts in + let race_with_main_thread = + List.exists + ~f:(fun (_, _, thread, _, _) -> ThreadSafetyDomain.ThreadsDomain.is_main thread) + conflicts + in let conflicting_proc_names = List.map ~f:(fun (_, _, _, _, pdesc) -> Procdesc.get_proc_name pdesc) conflicts |> Typ.Procname.Set.of_list @@ -1315,7 +1328,15 @@ let should_report_on_proc proc_desc tenv = currently not distinguishing different locks, and are treating "known to be confined to a thread" as if "known to be confined to UI thread". *) -let report_unsafe_accesses aggregated_access_map = +let report_unsafe_accesses + (aggregated_access_map: + ( ThreadSafetyDomain.TraceElem.t + * ThreadSafetyDomain.AccessPrecondition.t + * ThreadSafetyDomain.ThreadsDomain.astate + * Tenv.t + * Procdesc.t ) + list + AccessListMap.t) = let open ThreadSafetyDomain in let is_duplicate_report access pname {reported_sites; reported_writes; reported_reads} = if Config.filtering then CallSite.Set.mem (TraceElem.call_site access) reported_sites @@ -1343,7 +1364,7 @@ let report_unsafe_accesses aggregated_access_map = -> reported else reported in - let report_unsafe_access (access, pre, threaded, tenv, pdesc) accesses reported_acc = + let report_unsafe_access (access, pre, thread, tenv, pdesc) accesses reported_acc = let pname = Procdesc.get_proc_name pdesc in if is_duplicate_report access pname reported_acc then reported_acc else @@ -1360,7 +1381,7 @@ let report_unsafe_accesses aggregated_access_map = , (AccessPrecondition.Unprotected _ | AccessPrecondition.TotallyUnprotected) ) -> ( match Procdesc.get_proc_name pdesc with | Java _ - -> if threaded then reported_acc + -> if ThreadsDomain.is_main thread then reported_acc else ( (* unprotected write. warn. *) report_thread_safety_violation tenv pdesc IssueType.thread_safety_violation @@ -1385,8 +1406,9 @@ let report_unsafe_accesses aggregated_access_map = in let all_writes = List.filter - ~f:(fun (other_access, pre, other_threaded, _, _) -> - TraceElem.is_write other_access && not (threaded && other_threaded) + ~f:(fun (other_access, pre, other_thread, _, _) -> + TraceElem.is_write other_access + && not (ThreadsDomain.is_main thread && ThreadsDomain.is_main other_thread) && is_cpp_protected_write pre) accesses in diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml index e41889947..f24de2a8b 100644 --- a/infer/src/checkers/ThreadSafetyDomain.ml +++ b/infer/src/checkers/ThreadSafetyDomain.ml @@ -109,7 +109,60 @@ let make_unannotated_call_access pname loc = all branches. *) module LocksDomain = AbstractDomain.BooleanAnd -module ThreadsDomain = AbstractDomain.BooleanAnd + +module ThreadsDomain = struct + type astate = Unknown | Main | Background | Any + + let empty = Unknown + + let ( <= ) ~lhs ~rhs = + match (lhs, rhs) with + | Unknown, Unknown | Main, Main | Background, Background | Any, Any + -> true + | Unknown, _ + -> true + | _, Unknown + -> false + | _, Any + -> true + | Any, _ + -> false + | _ + -> (* Unknown is bottom, Any is top, other elements are incomparable *) + false + + let join astate1 astate2 = + match (astate1, astate2) with + | Unknown, astate | astate, Unknown + -> astate + | Any, _ | _, Any + -> Any + | Main, Main | Background, Background + -> astate1 + | Main, Background | Background, Main + -> Any + + 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" ) + + let is_unknown = function Unknown -> true | _ -> false + + let is_empty = is_unknown + + let is_main = function Main -> true | _ -> false +end + module ThumbsUpDomain = AbstractDomain.BooleanAnd module PathDomain = SinkTrace.Make (TraceElem) @@ -320,7 +373,7 @@ type astate = let empty = let thumbs_up = true in - let threads = false in + let threads = ThreadsDomain.Unknown in let locks = false in let accesses = AccessDomain.empty in let ownership = OwnershipDomain.empty in @@ -329,7 +382,7 @@ let empty = {thumbs_up; threads; locks; accesses; ownership; attribute_map; escapees} let is_empty {thumbs_up; threads; locks; accesses; ownership; attribute_map; escapees} = - thumbs_up && not threads && not locks && AccessDomain.is_empty accesses + thumbs_up && ThreadsDomain.is_unknown threads && not locks && AccessDomain.is_empty accesses && OwnershipDomain.is_empty ownership && AttributeMapDomain.is_empty attribute_map && EscapeeDomain.is_empty escapees @@ -344,7 +397,7 @@ let ( <= ) ~lhs ~rhs = let join astate1 astate2 = if phys_equal astate1 astate2 then astate1 else - let thumbs_up = ThreadsDomain.join astate1.thumbs_up astate2.thumbs_up in + let thumbs_up = ThumbsUpDomain.join astate1.thumbs_up astate2.thumbs_up in let threads = ThreadsDomain.join astate1.threads astate2.threads in let locks = LocksDomain.join astate1.locks astate2.locks in let accesses = AccessDomain.join astate1.accesses astate2.accesses in @@ -356,7 +409,7 @@ let join astate1 astate2 = let widen ~prev ~next ~num_iters = if phys_equal prev next then prev else - let thumbs_up = ThreadsDomain.widen ~prev:prev.thumbs_up ~next:next.thumbs_up ~num_iters in + let thumbs_up = ThumbsUpDomain.widen ~prev:prev.thumbs_up ~next:next.thumbs_up ~num_iters in let threads = ThreadsDomain.widen ~prev:prev.threads ~next:next.threads ~num_iters in let locks = LocksDomain.widen ~prev:prev.locks ~next:next.locks ~num_iters in let accesses = AccessDomain.widen ~prev:prev.accesses ~next:next.accesses ~num_iters in diff --git a/infer/src/checkers/ThreadSafetyDomain.mli b/infer/src/checkers/ThreadSafetyDomain.mli index 899880391..89b26022e 100644 --- a/infer/src/checkers/ThreadSafetyDomain.mli +++ b/infer/src/checkers/ThreadSafetyDomain.mli @@ -42,7 +42,19 @@ end and which memory locations correspond to the same lock. *) module LocksDomain : AbstractDomain.S with type astate = bool -module ThreadsDomain : AbstractDomain.S with type astate = bool +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. *) + + include AbstractDomain.WithBottom with type astate := astate + + val is_main : astate -> bool +end module ThumbsUpDomain : AbstractDomain.S with type astate = bool @@ -176,8 +188,8 @@ module FormalsDomain : sig end type astate = - { thumbs_up: ThreadsDomain.astate (** boolean that is true if we think we have a proof *) - ; threads: ThreadsDomain.astate (** boolean that is true if we know we are on UI/main thread *) + { thumbs_up: ThumbsUpDomain.astate (** boolean that is true if we think we have a proof *) + ; threads: ThreadsDomain.astate (** current thread: main, background, or unknown *) ; locks: LocksDomain.astate (** boolean that is true if a lock must currently be held *) ; accesses: AccessDomain.astate (** read and writes accesses performed without ownership permissions *) diff --git a/infer/tests/codetoanalyze/java/threadsafety/Annotations.java b/infer/tests/codetoanalyze/java/threadsafety/Annotations.java index 342c38980..3e4b78599 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/Annotations.java +++ b/infer/tests/codetoanalyze/java/threadsafety/Annotations.java @@ -164,25 +164,25 @@ class Annotations implements Interface { } /* Like in RaceWithMainThread.java with assertMainThread() */ - void conditional_Ok(boolean b){ + void conditional1_ok(boolean b){ if (b) { - write_on_main_thread_Ok(); - } /* BooleanAnd for threaded would hose you here and lead to a report */ + write_on_main_thread_ok(); + } } Integer ii; @ThreadConfined(ThreadConfined.UI) - void write_on_main_thread_Ok(){ + void write_on_main_thread_ok(){ ii = 22; } - void conditional_Bad(boolean b){ + void conditional2_ok(boolean b){ if (b) { - write_on_main_thread_Ok(); + write_on_main_thread_ok(); } else { - ii = 99; // Using || for threaded hoses this; no report + ii = 99; // this might or might not run on the main thread; don't warn } } diff --git a/infer/tests/codetoanalyze/java/threadsafety/RaceWithMainThread.java b/infer/tests/codetoanalyze/java/threadsafety/RaceWithMainThread.java index 59fa19810..5fb2b67c7 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/RaceWithMainThread.java +++ b/infer/tests/codetoanalyze/java/threadsafety/RaceWithMainThread.java @@ -109,9 +109,9 @@ class RaceWithMainThread{ g = 77; } -Integer ff; + Integer ff; - void conditional_Ok(boolean b){ + void conditional1_Ok(boolean b){ if (b) { /*People not literally putting this assert inside if's, but implicitly by method calls */ @@ -120,15 +120,13 @@ Integer ff; } } - - - void conditional_Bad(boolean b){ + void conditional2_Ok(boolean b){ if (b) { OurThreadUtils.assertMainThread(); ff = 88; } else { - ff = 99; + ff = 99; // this might or might now run on the main thread; don't warn } } diff --git a/infer/tests/codetoanalyze/java/threadsafety/issues.exp b/infer/tests/codetoanalyze/java/threadsafety/issues.exp index 89c303f67..e12115794 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/issues.exp +++ b/infer/tests/codetoanalyze/java/threadsafety/issues.exp @@ -6,7 +6,6 @@ codetoanalyze/java/threadsafety/Annotations.java, double Annotations.functionalD codetoanalyze/java/threadsafety/Annotations.java, int Annotations.FP_functionalAcrossBoxingLongOk(), 2, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Annotations.mBoxedLong2`] codetoanalyze/java/threadsafety/Annotations.java, int Annotations.functionalAcrossUnboxingLongBad(), 2, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Annotations.mLong2`] codetoanalyze/java/threadsafety/Annotations.java, long Annotations.functionaLongBad(), 2, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Annotations.mLong`] -codetoanalyze/java/threadsafety/Annotations.java, void Annotations.conditional_Bad(boolean), 5, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Annotations.ii`] codetoanalyze/java/threadsafety/Annotations.java, void Annotations.functionalAndNonfunctionalBad(), 1, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Annotations.mInt`] codetoanalyze/java/threadsafety/Annotations.java, void Annotations.mutateOffUiThreadBad(), 1, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Annotations.f`] codetoanalyze/java/threadsafety/Annotations.java, void Annotations.mutateSubfieldOfConfinedBad(), 1, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Annotations.encapsulatedField.codetoanalyze.java.checkers.Obj.f`] @@ -73,7 +72,6 @@ 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 `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 `codetoanalyze.java.checkers.Obj.f`] codetoanalyze/java/threadsafety/Ownership.java, void Ownership.writeToOwnedInCalleeOk2(), 4, THREAD_SAFETY_VIOLATION, [,access to `codetoanalyze.java.checkers.Ownership.field`,,access to `codetoanalyze.java.checkers.Ownership.field`] -codetoanalyze/java/threadsafety/RaceWithMainThread.java, void RaceWithMainThread.conditional_Bad(boolean), 6, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.RaceWithMainThread.ff`] codetoanalyze/java/threadsafety/RaceWithMainThread.java, void RaceWithMainThread.conditional_isMainThread_ElseBranch_Bad(), 7, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.RaceWithMainThread.ff`] codetoanalyze/java/threadsafety/RaceWithMainThread.java, void RaceWithMainThread.conditional_isMainThread_Negation_Bad(), 3, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.RaceWithMainThread.ff`] codetoanalyze/java/threadsafety/RaceWithMainThread.java, void RaceWithMainThread.conditional_isUiThread_ElseBranch_Bad(), 7, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.RaceWithMainThread.ff`]