[threadsafety] Model isMainThread()

Reviewed By: sblackshear

Differential Revision: D5129265

fbshipit-source-id: 14a37b1

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

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;
+   }
+ }
+
 }

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, [<Beginning of read trace>,access to `codetoanalyze.java.checkers.Ownership.field`,<Beginning of write trace>,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, [<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`]