diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index 1f7112f43..127c20123 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/infer/src/checkers/ThreadSafety.ml @@ -66,6 +66,11 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | LockedIfTrue | NoEffect + type thread_model = + | Threaded + | Unknown + | ThreadedIfTrue + let is_thread_utils_method method_name_str = function | Typ.Procname.Java java_pname -> String.is_suffix ~suffix:"ThreadUtils" (Typ.Procname.java_get_class_name java_pname) @@ -110,6 +115,15 @@ module TransferFunctions (CFG : ProcCfg.S) = struct | _ -> NoEffect + let get_thread_model = function + | Typ.Procname.Java java_pname -> + if is_thread_utils_method "assertMainThread" (Typ.Procname.Java java_pname) then + Threaded + else if is_thread_utils_method "isMainThread" (Typ.Procname.Java java_pname) then + ThreadedIfTrue + else Unknown + | _ -> Unknown + let add_conditional_ownership_attribute access_path formal_map attribute_map attributes = match FormalMap.get_formal_index (fst access_path) formal_map with | Some formal_index when not (is_owned access_path attribute_map) -> @@ -427,6 +441,26 @@ module TransferFunctions (CFG : ProcCfg.S) = struct add_reads actuals loc astate.accesses astate.locks astate.threads astate.attribute_map proc_data in let astate = { astate with accesses; } in + let astate = + match get_thread_model callee_pname with + | Threaded -> + { astate with threads = true; } + | ThreadedIfTrue -> + begin + match ret_opt with + | Some ret_access_path -> + let attribute_map = + AttributeMapDomain.add_attribute + (ret_access_path, []) + (Choice Choice.OnMainThread) + astate.attribute_map in + { astate with attribute_map; } + | None -> + failwithf + "Procedure %a specified as returning boolean, but returns nothing" + Typ.Procname.pp callee_pname + end + | Unknown -> astate in let astate_callee = (* assuming that modeled procedures do not have useful summaries *) if is_thread_utils_method "assertMainThread" callee_pname diff --git a/infer/tests/codetoanalyze/java/threadsafety/RaceWithMainThread.java b/infer/tests/codetoanalyze/java/threadsafety/RaceWithMainThread.java index 685a93eb0..2ee6338c1 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/RaceWithMainThread.java +++ b/infer/tests/codetoanalyze/java/threadsafety/RaceWithMainThread.java @@ -12,6 +12,7 @@ package codetoanalyze.java.checkers; import javax.annotation.concurrent.ThreadSafe; class OurThreadUtils{ + native boolean isMainThread(); void assertMainThread(){} void assertHoldsLock(Object lock){} } @@ -101,6 +102,8 @@ Integer ff; } } + + void conditional_Bad(boolean b){ if (b) { @@ -110,4 +113,41 @@ Integer ff; ff = 99; } } + + void conditional_isMainThread_Ok(){ + if (o.isMainThread()) + { + ff = 88; + } + } + + void conditional_isMainThread_ElseBranch_Bad(){ + if (o.isMainThread()) + { + synchronized(this){ + ff = 88; + } + } else { + ff = 99; + } + } + + void conditional_isMainThread_Negation_Bad(){ + if (!o.isMainThread()) + { + ff = 88; + } + } + + void conditional_isMainThread_ElseBranch_Ok(){ + if (!o.isMainThread()) + { + synchronized(this){ + ff = 88; + } + } else { + ff = 99; + } + } + } diff --git a/infer/tests/codetoanalyze/java/threadsafety/issues.exp b/infer/tests/codetoanalyze/java/threadsafety/issues.exp index 4610692e4..04c865b06 100644 --- a/infer/tests/codetoanalyze/java/threadsafety/issues.exp +++ b/infer/tests/codetoanalyze/java/threadsafety/issues.exp @@ -64,6 +64,8 @@ codetoanalyze/java/threadsafety/Ownership.java, void Ownership.writeToNotOwnedIn 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.readProtectedUnthreadedBad(), 3, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.RaceWithMainThread.f`] codetoanalyze/java/threadsafety/RaceWithMainThread.java, void RaceWithMainThread.read_unprotected_unthreaded_Bad(), 2, THREAD_SAFETY_VIOLATION, [,access to `codetoanalyze.java.checkers.RaceWithMainThread.f`,,access to `codetoanalyze.java.checkers.RaceWithMainThread.f`] codetoanalyze/java/threadsafety/ReadWriteRaces.java, Object ReadWriteRaces.callUnprotecteReadInCallee(), 1, THREAD_SAFETY_VIOLATION, [,call to Object ReadWriteRaces.unprotectedReadInCallee(),access to `codetoanalyze.java.checkers.ReadWriteRaces.field1`,,access to `codetoanalyze.java.checkers.ReadWriteRaces.field1`]