[thread-safety] Model assertManThread and assertHoldsLock

Reviewed By: sblackshear

Differential Revision: D4706409

fbshipit-source-id: c822c74

infer/src/checkers/ThreadSafety.ml

@@ -51,8 +51,17 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     | Unlock
     | NoEffect
 
+
+  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)
+        && String.equal (Typ.Procname.java_get_method java_pname) method_name_str
+    | _ -> false
+
   let get_lock_model = function
     | Typ.Procname.Java java_pname ->
+        if is_thread_utils_method "assertHoldsLock" (Typ.Procname.Java java_pname) then Lock
+        else
           begin
             match Typ.Procname.java_get_class_name java_pname, Typ.Procname.java_get_method java_pname with
             | ("java.util.concurrent.locks.Lock"
@@ -355,7 +364,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                   AccessDomain.empty
             | None ->
                 AccessDomain.empty in
-          Some (false, callee_accesses, AttributeSetDomain.empty)
+          Some (false, false, callee_accesses, AttributeSetDomain.empty)
       | _ ->
           failwithf
             "Call to %a is marked as a container write, but has no receiver"
@@ -414,6 +423,9 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     | Sil.Call (ret_opt, Const (Cfun callee_pname), actuals, loc, _) ->
         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; }
+          else
             match get_lock_model callee_pname with
             | Lock ->
                 { astate with locks = true; }
@@ -422,7 +434,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             | NoEffect ->
                 match
                   get_summary pdesc callee_pname actuals ~f_resolve_id loc tenv with
-              | Some (callee_locks, callee_accesses, return_attributes) ->
+                | Some ( callee_threads, callee_locks, callee_accesses, return_attributes) ->
                     let call_site = CallSite.make callee_pname loc in
                     let combine_accesses_for_pre pre ~caller_accesses ~callee_accesses =
                       let combined_accesses =
@@ -436,6 +448,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                         ~caller_accesses:astate.accesses
                         ~callee_accesses in
                     let locks' = callee_locks || astate.locks in
+                    let threads' = callee_threads || astate.threads in
                     let astate' =
                       if is_unprotected locks' pdesc
                       then
@@ -519,7 +532,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                         astate.attribute_map
                         ~f_resolve_id
                         extras in
-                  { astate' with locks = locks'; attribute_map; }
+                    { astate' with locks = locks'; threads = threads'; attribute_map; }
                 | None ->
                     if is_box callee_pname
                     then
@@ -751,8 +764,9 @@ let analyze_procedure callback =
     Typ.Procname.is_constructor proc_name || FbThreadSafety.is_custom_init tenv proc_name in
   let open ThreadSafetyDomain in
   let has_lock = false in
+  let known_on_ui_thread = false in
   let return_attrs = AttributeSetDomain.empty in
-  let empty = has_lock, AccessDomain.empty, return_attrs in
+  let empty =  known_on_ui_thread, has_lock, AccessDomain.empty, return_attrs in
   (* convert the abstract state to a summary by dropping the id map *)
   let compute_post ({ ProcData.pdesc; tenv; extras; } as proc_data) =
     if should_analyze_proc pdesc tenv
@@ -785,7 +799,7 @@ let analyze_procedure callback =
             ThreadSafetyDomain.empty in
 
         match Analyzer.compute_post proc_data ~initial with
-        | Some { locks; accesses; attribute_map; } ->
+        | Some { threads; locks; accesses; attribute_map; } ->
             let return_var_ap =
               AccessPath.of_pvar
                 (Pvar.get_ret_pvar (Procdesc.get_proc_name pdesc))
@@ -793,7 +807,7 @@ let analyze_procedure callback =
             let return_attributes =
               try AttributeMapDomain.find return_var_ap attribute_map
               with Not_found -> AttributeSetDomain.empty in
-            Some (locks, accesses, return_attributes)
+            Some (threads, locks, accesses, return_attributes)
         | None ->
             None
       end
@@ -817,7 +831,10 @@ let make_results_table get_proc_desc file_env =
   (* make a Map sending each element e of list l to (f e) *)
   let map_post_computation_over_procs f l =
     List.fold
-      ~f:(fun m p -> ResultsTableType.add p (f p) m)
+      ~f:(fun m p -> match f p with
+          | (true,_,_,_) -> m (* Don't put a post there *)
+          | _ -> ResultsTableType.add p (f p) m
+        )
       ~init:ResultsTableType.empty
       l in
   let compute_post_for_procedure = (* takes proc_env as arg *)
@@ -918,7 +935,7 @@ let filter_conflicting_sinks sink trace =
 let collect_conflicting_writes sink tab =
   let procs_and_writes =
     List.map
-      ~f:(fun (key, (_, accesses, _)) ->
+      ~f:(fun (key, (_, _, accesses, _)) ->
           let conflicting_writes =
             filter_conflicting_sinks sink (get_all_accesses Write accesses) in
           key, conflicting_writes
@@ -989,7 +1006,7 @@ let report_thread_safety_violations ( _, tenv, pname, pdesc) make_description tr
   let open ThreadSafetyDomain in
   let trace_of_pname callee_pname =
     match Summary.read_summary pdesc callee_pname with
-    | Some (_, accesses, _) -> get_possibly_unsafe_writes accesses
+    | Some (_, _, accesses, _) -> get_possibly_unsafe_writes accesses
     | _ -> PathDomain.empty in
   let report_one_path ((_, sinks) as path) =
     let initial_sink, _ = List.last_exn sinks in
@@ -1104,7 +1121,7 @@ let process_results_table file_env tab =
     (should_report_on_all_procs || is_thread_safe_method pdesc tenv)
     && should_report_on_proc proc_env in
   ResultsTableType.iter (* report errors for each method *)
-    (fun proc_env (_, accesses, _) ->
+    (fun proc_env (_, _, accesses, _) ->
        if should_report proc_env
        then
          let open ThreadSafetyDomain in

infer/src/checkers/ThreadSafetyDomain.ml

@@ -68,6 +68,10 @@ let make_access access_path access_kind loc =
 
 module LocksDomain = AbstractDomain.BooleanAnd
 
+(*At first we are modelling the distinction "true, known to be UI thread"
+  and "false, don't know definitley to be main tread". Can refine later *)
+module ThreadsDomain = AbstractDomain.BooleanAnd
+
 module PathDomain = SinkTrace.Make(TraceElem)
 
 module Attribute = struct
@@ -158,25 +162,29 @@ end
 
 type astate =
   {
+    threads: ThreadsDomain.astate;
     locks : LocksDomain.astate;
     accesses : AccessDomain.astate;
     id_map : IdAccessPathMapDomain.astate;
     attribute_map : AttributeMapDomain.astate;
   }
 
-type summary = LocksDomain.astate * AccessDomain.astate * AttributeSetDomain.astate
+type summary = ThreadsDomain.astate * LocksDomain.astate
+               * AccessDomain.astate * AttributeSetDomain.astate
 
 let empty =
+  let threads = false in
   let locks = false in
   let accesses = AccessDomain.empty in
   let id_map = IdAccessPathMapDomain.empty in
   let attribute_map = AccessPath.UntypedRawMap.empty in
-  { locks; accesses; id_map; attribute_map; }
+  { threads; locks; accesses; id_map; attribute_map; }
 
 let (<=) ~lhs ~rhs =
   if phys_equal lhs rhs
   then true
   else
+    ThreadsDomain.(<=) ~lhs:lhs.threads ~rhs:rhs.threads &&
     LocksDomain.(<=) ~lhs:lhs.locks ~rhs:rhs.locks &&
     AccessDomain.(<=) ~lhs:lhs.accesses ~rhs:rhs.accesses &&
     IdAccessPathMapDomain.(<=) ~lhs:lhs.id_map ~rhs:rhs.id_map &&
@@ -187,37 +195,41 @@ let join astate1 astate2 =
   then
     astate1
   else
+    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
     let id_map = IdAccessPathMapDomain.join astate1.id_map astate2.id_map in
     let attribute_map = AttributeMapDomain.join astate1.attribute_map astate2.attribute_map in
-    { locks; accesses; id_map; attribute_map; }
+    { threads; locks; accesses; id_map; attribute_map; }
 
 let widen ~prev ~next ~num_iters =
   if phys_equal prev next
   then
     prev
   else
+    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
     let id_map = IdAccessPathMapDomain.widen ~prev:prev.id_map ~next:next.id_map ~num_iters in
     let attribute_map =
       AttributeMapDomain.widen ~prev:prev.attribute_map ~next:next.attribute_map ~num_iters in
-    { locks; accesses; id_map; attribute_map; }
+    { threads; locks; accesses; id_map; attribute_map; }
 
-let pp_summary fmt (locks, accesses, return_attributes) =
+let pp_summary fmt (threads, locks, accesses, return_attributes) =
   F.fprintf
     fmt
-    "Locks: %a Accesses %a Return Attributes: %a"
+    "Threads: %a Locks: %a Accesses %a Return Attributes: %a"
+    ThreadsDomain.pp threads
     LocksDomain.pp locks
     AccessDomain.pp accesses
     AttributeSetDomain.pp return_attributes
 
-let pp fmt { locks; accesses; id_map; attribute_map; } =
+let pp fmt { threads; locks; accesses; id_map; attribute_map; } =
   F.fprintf
     fmt
-    "Locks: %a Accesses %a Id Map: %a Attribute Map:\
+    "Threads: %a Locks: %a Accesses %a Id Map: %a Attribute Map:\
      %a"
+    ThreadsDomain.pp threads
     LocksDomain.pp locks
     AccessDomain.pp accesses
     IdAccessPathMapDomain.pp id_map

infer/src/checkers/ThreadSafetyDomain.mli

@@ -39,6 +39,8 @@ 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 PathDomain : module type of SinkTrace.Make(TraceElem)
 
 module Attribute : sig
@@ -101,6 +103,8 @@ end
 
 type astate =
   {
+    threads : ThreadsDomain.astate;
+    (** boolean that is true if we know we are on UI/main thread *)
     locks : LocksDomain.astate;
     (** boolean that is true if a lock must currently be held *)
     accesses : AccessDomain.astate;
@@ -113,7 +117,8 @@ type astate =
 
 (** same as astate, but without [id_map]/[owned] (since they are local) and with the addition of the
     attributes associated with the return value *)
-type summary = LocksDomain.astate * AccessDomain.astate * AttributeSetDomain.astate
+type summary = ThreadsDomain.astate * LocksDomain.astate
+               * AccessDomain.astate * AttributeSetDomain.astate
 
 include AbstractDomain.WithBottom with type astate := astate
 

infer/tests/codetoanalyze/java/threadsafety/RaceWithMainThread.java

@@ -0,0 +1,44 @@
+/*
+ * Copyright (c) 2016 - present Facebook, Inc.
+ * All rights reserved.
+ *
+ * This source code is licensed under the BSD style license found in the
+ * LICENSE file in the root directory of this source tree. An additional grant
+ * of patent rights can be found in the PATENTS file in the same directory.
+ */
+
+package codetoanalyze.java.checkers;
+
+import javax.annotation.concurrent.ThreadSafe;
+
+class OurThreadUtils{
+  void assertMainThread(){}
+  void assertHoldsLock(Object lock){}
+}
+
+@ThreadSafe
+class RaceWithMainThread{
+
+  Integer f;
+  OurThreadUtils o;
+
+  void main_thread_OK(){
+      o.assertMainThread();
+      f = 88;
+   }
+
+   void main_thread_indirect_OK() {
+     main_thread_OK();
+     f = 77;
+   }
+
+  void holds_lock_OK(){
+      o.assertHoldsLock(this);
+      f = 88;
+   }
+
+   void holds_lock_indirect_OK() {
+     holds_lock_OK();
+     f = 77;
+   }
+}