[threadsafety] Model more xThreadUtil methods

Reviewed By: sblackshear

Differential Revision: D5137061

fbshipit-source-id: ffd030c
master
Peter O'Hearn 8 years ago committed by Facebook Github Bot
parent de32a6728e
commit 34ae89cf35

@ -71,9 +71,14 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
| Unknown | Unknown
| ThreadedIfTrue | ThreadedIfTrue
let is_thread_utils_type java_pname =
let pn = (Typ.Procname.java_get_class_name java_pname) in
String.is_suffix ~suffix:"ThreadUtils" pn
|| String.is_suffix ~suffix:"ThreadUtil" pn
let is_thread_utils_method method_name_str = function let is_thread_utils_method method_name_str = function
| Typ.Procname.Java java_pname -> | Typ.Procname.Java java_pname ->
String.is_suffix ~suffix:"ThreadUtils" (Typ.Procname.java_get_class_name java_pname) is_thread_utils_type java_pname
&& String.equal (Typ.Procname.java_get_method java_pname) method_name_str && String.equal (Typ.Procname.java_get_method java_pname) method_name_str
| _ -> false | _ -> false
@ -117,11 +122,17 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
let get_thread_model = function let get_thread_model = function
| Typ.Procname.Java java_pname -> | Typ.Procname.Java java_pname ->
if is_thread_utils_method "assertMainThread" (Typ.Procname.Java java_pname) then if is_thread_utils_type java_pname then
Threaded match Typ.Procname.java_get_method java_pname with
else if is_thread_utils_method "isMainThread" (Typ.Procname.Java java_pname) then | "assertMainThread"
ThreadedIfTrue | "checkOnMainThread"
| "assertOnUiThread" -> Threaded
| "isMainThread"
| "isUiThread" -> ThreadedIfTrue
| _ -> Unknown
else Unknown else Unknown
(*Note we are not modelling assertOnNonUiThread or
assertOnBackgroundThread. These treated as Unknown*)
| _ -> Unknown | _ -> Unknown
let add_conditional_ownership_attribute access_path formal_map attribute_map attributes = let add_conditional_ownership_attribute access_path formal_map attribute_map attributes =

@ -12,22 +12,35 @@ package codetoanalyze.java.checkers;
import javax.annotation.concurrent.ThreadSafe; import javax.annotation.concurrent.ThreadSafe;
class OurThreadUtils{ class OurThreadUtils{
native boolean isMainThread(); native static boolean isMainThread();
void assertMainThread(){} static void assertMainThread(){}
void assertHoldsLock(Object lock){} static void assertHoldsLock(Object lock){}
} }
class OurThreadUtil{ /*This is like AndroidThreadUtil*/
native static boolean isUiThread();
static void assertOnUiThread(){}
}
@ThreadSafe @ThreadSafe
class RaceWithMainThread{ class RaceWithMainThread{
Integer f; Integer f;
OurThreadUtils o;
void main_thread_OK(){ void main_thread_OK(){
o.assertMainThread(); OurThreadUtils.assertMainThread();
f = 88; f = 88;
} }
Integer f1;
void main_thread1_OK(){
OurThreadUtil.assertOnUiThread();
f1 = 88;
}
void main_thread_indirect_OK() { void main_thread_indirect_OK() {
main_thread_OK(); main_thread_OK();
f = 77; f = 77;
@ -35,7 +48,7 @@ class RaceWithMainThread{
void read_from_main_thread_OK(){ void read_from_main_thread_OK(){
Integer x; Integer x;
o.assertMainThread(); OurThreadUtils.assertMainThread();
x = f; x = f;
} }
@ -44,6 +57,11 @@ class RaceWithMainThread{
x = f; x = f;
} }
void read_unprotected_unthreaded1_Bad(){
Integer x;
x = f1;
}
/*There is a particularly subtle idiom which avoids races, where a /*There is a particularly subtle idiom which avoids races, where a
variable can be read without protection on the main thread, if variable can be read without protection on the main thread, if
it is written with protection on the main thread and read with it is written with protection on the main thread and read with
@ -53,7 +71,7 @@ class RaceWithMainThread{
Integer i; Integer i;
void protected_write_on_main_thread_OK() { void protected_write_on_main_thread_OK() {
o.assertMainThread(); OurThreadUtils.assertMainThread();
synchronized (this) { synchronized (this) {
i = 99; i = 99;
} }
@ -61,7 +79,7 @@ class RaceWithMainThread{
void unprotected_read_on_main_thread_OK() { void unprotected_read_on_main_thread_OK() {
Integer x; Integer x;
o.assertMainThread(); OurThreadUtils.assertMainThread();
x = i; x = i;
} }
@ -82,7 +100,7 @@ class RaceWithMainThread{
Integer g; Integer g;
void holds_lock_OK(){ void holds_lock_OK(){
o.assertHoldsLock(this); OurThreadUtils.assertHoldsLock(this);
g = 88; g = 88;
} }
@ -97,7 +115,7 @@ Integer ff;
if (b) if (b)
{ /*People not literally putting this assert inside if's, { /*People not literally putting this assert inside if's,
but implicitly by method calls */ but implicitly by method calls */
o. assertMainThread(); OurThreadUtils.assertMainThread();
ff = 88; ff = 88;
} }
} }
@ -107,7 +125,7 @@ Integer ff;
void conditional_Bad(boolean b){ void conditional_Bad(boolean b){
if (b) if (b)
{ {
o.assertMainThread(); OurThreadUtils.assertMainThread();
ff = 88; ff = 88;
} else { } else {
ff = 99; ff = 99;
@ -115,14 +133,22 @@ Integer ff;
} }
void conditional_isMainThread_Ok(){ void conditional_isMainThread_Ok(){
if (o.isMainThread()) if (OurThreadUtils.isMainThread())
{
ff = 88;
}
}
void conditional_isUiThread_Ok(){
if (OurThreadUtil.isUiThread())
{ {
ff = 88; ff = 88;
} }
} }
void conditional_isMainThread_ElseBranch_Bad(){ void conditional_isMainThread_ElseBranch_Bad(){
if (o.isMainThread()) if (OurThreadUtils.isMainThread())
{ {
synchronized(this){ synchronized(this){
ff = 88; ff = 88;
@ -132,15 +158,27 @@ Integer ff;
} }
} }
void conditional_isUiThread_ElseBranch_Bad(){
if (OurThreadUtil.isUiThread())
{
synchronized(this){
ff = 88;
}
} else {
ff = 99;
}
}
void conditional_isMainThread_Negation_Bad(){ void conditional_isMainThread_Negation_Bad(){
if (!o.isMainThread()) if (!OurThreadUtils.isMainThread())
{ {
ff = 88; ff = 88;
} }
} }
void conditional_isMainThread_ElseBranch_Ok(){ void conditional_isMainThread_ElseBranch_Ok(){
if (!o.isMainThread()) if (!OurThreadUtils.isMainThread())
{ {
synchronized(this){ synchronized(this){
ff = 88; ff = 88;

@ -68,7 +68,9 @@ codetoanalyze/java/threadsafety/Ownership.java, void Ownership.writeToOwnedInCal
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_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_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_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`]
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.readProtectedUnthreadedBad(), 3, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.RaceWithMainThread.f`]
codetoanalyze/java/threadsafety/RaceWithMainThread.java, void RaceWithMainThread.read_unprotected_unthreaded1_Bad(), 2, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,access to `codetoanalyze.java.checkers.RaceWithMainThread.f1`,<Beginning of write trace>,access to `codetoanalyze.java.checkers.RaceWithMainThread.f1`]
codetoanalyze/java/threadsafety/RaceWithMainThread.java, void RaceWithMainThread.read_unprotected_unthreaded_Bad(), 2, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,access to `codetoanalyze.java.checkers.RaceWithMainThread.f`,<Beginning of write trace>,access to `codetoanalyze.java.checkers.RaceWithMainThread.f`] codetoanalyze/java/threadsafety/RaceWithMainThread.java, void RaceWithMainThread.read_unprotected_unthreaded_Bad(), 2, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,access to `codetoanalyze.java.checkers.RaceWithMainThread.f`,<Beginning of write trace>,access to `codetoanalyze.java.checkers.RaceWithMainThread.f`]
codetoanalyze/java/threadsafety/ReadWriteRaces.java, Object ReadWriteRaces.callUnprotecteReadInCallee(), 1, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,call to Object ReadWriteRaces.unprotectedReadInCallee(),access to `codetoanalyze.java.checkers.ReadWriteRaces.field1`,<Beginning of write trace>,access to `codetoanalyze.java.checkers.ReadWriteRaces.field1`] codetoanalyze/java/threadsafety/ReadWriteRaces.java, Object ReadWriteRaces.callUnprotecteReadInCallee(), 1, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,call to Object ReadWriteRaces.unprotectedReadInCallee(),access to `codetoanalyze.java.checkers.ReadWriteRaces.field1`,<Beginning of write trace>,access to `codetoanalyze.java.checkers.ReadWriteRaces.field1`]
codetoanalyze/java/threadsafety/ReadWriteRaces.java, Object ReadWriteRaces.unprotectedRead1(), 1, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,access to `codetoanalyze.java.checkers.ReadWriteRaces.field1`,<Beginning of write trace>,access to `codetoanalyze.java.checkers.ReadWriteRaces.field1`] codetoanalyze/java/threadsafety/ReadWriteRaces.java, Object ReadWriteRaces.unprotectedRead1(), 1, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,access to `codetoanalyze.java.checkers.ReadWriteRaces.field1`,<Beginning of write trace>,access to `codetoanalyze.java.checkers.ReadWriteRaces.field1`]

Loading…
Cancel
Save