[thread-safety] warning when interface method is called from thread-safe context without annotation

Reviewed By: ngorogiannis

Differential Revision: D5445971

fbshipit-source-id: a3a7dd3

infer/src/checkers/ThreadSafety.ml

@@ -48,7 +48,7 @@ let get_container_write_desc sink =
        -> get_container_write_desc_ call_name (F.asprintf "%a" Var.pp base_var)
       | _
        -> None )
-  | Read _
+  | Read _ | InterfaceCall _
    -> (* TODO: support Read *)
       None
 
@@ -264,6 +264,47 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
   let is_unprotected is_locked is_threaded pdesc =
     not is_locked && not is_threaded && 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
+    | Typ.Procname.Java java_pname -> (
+      match Typ.Procname.java_get_package java_pname with
+      | Some package_name
+       -> String.is_prefix ~prefix:"java." package_name
+          || String.is_prefix ~prefix:"android." package_name
+          || String.is_prefix ~prefix:"com.google." package_name
+      | None
+       -> false )
+    | _
+     -> false
+
+  let is_builder_function = function
+    | Typ.Procname.Java java_pname
+     -> String.is_suffix ~suffix:"$Builder" (Typ.Procname.java_get_class_name java_pname)
+    | _
+     -> false
+
+  let has_return_annot predicate pn =
+    Annotations.pname_has_return_annot pn ~attrs_of_pname:Specs.proc_resolve_attributes predicate
+
+  let add_unannotated_call_access pname (call_flags: CallFlags.t) loc tenv ~locks ~threads
+      attribute_map (proc_data: FormalMap.t ProcData.t) =
+    if call_flags.cf_interface && Typ.Procname.is_java pname
+       && not (is_java_library pname || is_builder_function pname)
+       (* can't ask anyone to annotate interfaces in library code, and Builder's should always be
+          thread-safe (would be unreasonable to ask everyone to annotate them) *)
+       && not (PatternMatch.check_class_attributes Annotations.ia_is_thread_safe tenv pname)
+       && not (has_return_annot Annotations.ia_is_thread_safe pname)
+    then
+      let open Domain in
+      let pre =
+        if is_unprotected locks threads proc_data.pdesc then AccessPrecondition.unprotected
+        else
+          AccessPrecondition.Protected
+            (make_excluder (locks || Procdesc.is_java_synchronized proc_data.pdesc) threads)
+      in
+      AccessDomain.add_access pre (make_unannotated_call_access pname loc) attribute_map
+    else attribute_map
+
   let add_access exp loc ~is_write_access accesses locks threads attribute_map
       (proc_data: FormalMap.t ProcData.t) =
     let open Domain in
@@ -294,12 +335,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
                || is_safe_access access prefix_path proc_data.tenv
             then access_acc
             else
-              (* TODO: I think there's a utility function for this somewhere *)
-              let accesses = AccessDomain.get_accesses pre access_acc in
-              let accesses' =
-                PathDomain.add_sink (make_access access_path ~is_write loc) accesses
-              in
-              AccessDomain.add pre accesses' access_acc
+              AccessDomain.add_access pre (make_field_access access_path ~is_write loc) access_acc
           in
           add_field_accesses pre access_path access_acc' access_list'
     in
@@ -321,9 +357,6 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
     in
     List.fold ~f:add_access_ ~init:accesses (HilExp.get_access_paths exp)
 
-  let has_return_annot predicate pn =
-    Annotations.pname_has_return_annot pn ~attrs_of_pname:Specs.proc_resolve_attributes predicate
-
   let is_functional pname =
     let is_annotated_functional = has_return_annot Annotations.ia_is_functional in
     let is_modeled_functional = function
@@ -472,7 +505,7 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
           (fst receiver_ap, snd receiver_ap @ [AccessPath.FieldAccess dummy_fieldname])
         in
         AccessDomain.add_access (Unprotected (Some 0))
-          (make_access dummy_access_ap ~is_write:true callee_loc) AccessDomain.empty
+          (make_field_access dummy_access_ap ~is_write:true callee_loc) AccessDomain.empty
     in
     (* TODO: for now all formals escape *)
     (* we need a more intelligent escape analysis, that branches on whether
@@ -545,9 +578,13 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         {astate with accesses; attribute_map; escapees}
     | Call (ret_opt, Direct callee_pname, actuals, call_flags, loc)
      -> (
+        let accesses_with_unannotated_calls =
+          add_unannotated_call_access callee_pname call_flags loc tenv ~locks:astate.locks
+            ~threads:astate.threads astate.accesses proc_data
+        in
         let accesses =
-          add_reads actuals loc astate.accesses astate.locks astate.threads astate.attribute_map
-            proc_data
+          add_reads actuals loc accesses_with_unannotated_calls astate.locks astate.threads
+            astate.attribute_map proc_data
         in
         let astate = {astate with accesses} in
         let astate =
@@ -1057,12 +1094,12 @@ let pp_access fmt sink =
   match get_container_write_desc sink with
   | Some container_write_desc
    -> pp_container_access fmt container_write_desc
-  | None
-   -> let access_path =
-        match ThreadSafetyDomain.PathDomain.Sink.kind sink
-        with Read access_path | Write access_path -> access_path
-      in
-      F.fprintf fmt "%a" (MF.wrap_monospaced AccessPath.pp_access_list) (snd access_path)
+  | None ->
+    match ThreadSafetyDomain.PathDomain.Sink.kind sink with
+    | Read access_path | Write access_path
+     -> F.fprintf fmt "%a" (MF.wrap_monospaced AccessPath.pp_access_list) (snd access_path)
+    | InterfaceCall _ as access
+     -> F.fprintf fmt "%a" ThreadSafetyDomain.Access.pp access
 
 let desc_of_sink sink =
   match get_container_write_desc sink with
@@ -1071,7 +1108,11 @@ let desc_of_sink sink =
   | None
    -> let sink_pname = CallSite.pname (ThreadSafetyDomain.PathDomain.Sink.call_site sink) in
       if Typ.Procname.equal sink_pname Typ.Procname.empty_block then
-        F.asprintf "access to %a" pp_access sink
+        match ThreadSafetyDomain.PathDomain.Sink.kind sink with
+        | Read _ | Write _
+         -> F.asprintf "access to %a" pp_access sink
+        | InterfaceCall interface_pname
+         -> F.asprintf "call to %a" Typ.Procname.pp interface_pname
       else F.asprintf "call to %a" Typ.Procname.pp sink_pname
 
 let trace_of_pname orig_sink orig_pdesc callee_pname =
@@ -1130,6 +1171,20 @@ let report_thread_safety_violation tenv pdesc ~make_description ~conflicts acces
   let trace_of_pname = trace_of_pname access pdesc in
   Option.iter ~f:report_one_path (PathDomain.get_reportable_sink_path access ~trace_of_pname)
 
+let report_unannotated_interface_violation tenv pdesc access reported_pname =
+  match reported_pname with
+  | Typ.Procname.Java java_pname
+   -> let class_name = Typ.Procname.java_get_class_name java_pname in
+      let make_description _ _ _ _ _ =
+        F.asprintf
+          "Unprotected call to method of un-annotated interface %s. Consider annotating the class with %a or adding a lock"
+          class_name MF.pp_monospaced "@ThreadSafe"
+      in
+      report_thread_safety_violation tenv pdesc ~make_description ~conflicts:[] access
+  | _
+   -> (* skip reporting on C++ *)
+      ()
+
 let pp_procname_short fmt = function
   | Typ.Procname.Java java
    -> F.fprintf fmt "%s.%s" (Typ.Procname.java_get_class_name java)
@@ -1225,12 +1280,14 @@ let report_unsafe_accesses aggregated_access_map =
   let open ThreadSafetyDomain in
   let is_duplicate_report access pname {reported_sites; reported_writes; reported_reads} =
     CallSite.Set.mem (TraceElem.call_site access) reported_sites
-    || Typ.Procname.Set.mem pname
-         ( match TraceElem.kind access with
+    ||
+    match TraceElem.kind access with
     | Access.Write _
-          -> reported_writes
+     -> Typ.Procname.Set.mem pname reported_writes
     | Access.Read _
-          -> reported_reads )
+     -> Typ.Procname.Set.mem pname reported_reads
+    | Access.InterfaceCall _
+     -> false
   in
   let update_reported access pname reported =
     let reported_sites = CallSite.Set.add (TraceElem.call_site access) reported.reported_sites in
@@ -1241,12 +1298,21 @@ let report_unsafe_accesses aggregated_access_map =
     | Access.Read _
      -> let reported_reads = Typ.Procname.Set.add pname reported.reported_reads in
         {reported with reported_reads; reported_sites}
+    | Access.InterfaceCall _
+     -> reported
   in
   let report_unsafe_access (access, pre, threaded, 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
       match (TraceElem.kind access, pre) with
+      | Access.InterfaceCall unannoted_call_pname, AccessPrecondition.Unprotected _
+       -> (* un-annotated interface call + no lock. warn *)
+          report_unannotated_interface_violation tenv pdesc access unannoted_call_pname ;
+          update_reported access pname reported_acc
+      | Access.InterfaceCall _, AccessPrecondition.Protected _
+       -> (* un-annotated interface call, but it's protected by a lock/thread. don't report *)
+          reported_acc
       | Access.Write _, AccessPrecondition.Unprotected _ -> (
         match Procdesc.get_proc_name pdesc with
         | Java _

infer/src/checkers/ThreadSafetyDomain.ml

@@ -11,17 +11,28 @@ open! IStd
 module F = Format
 
 module Access = struct
-  type t = Read of AccessPath.Raw.t | Write of AccessPath.Raw.t [@@deriving compare]
+  type t =
+    | Read of AccessPath.Raw.t
+    | Write of AccessPath.Raw.t
+    | InterfaceCall of Typ.Procname.t
+    [@@deriving compare]
 
-  let make access_path ~is_write = if is_write then Write access_path else Read access_path
+  let make_field_access access_path ~is_write =
+    if is_write then Write access_path else Read access_path
 
-  let get_access_path = function Read access_path | Write access_path -> Some access_path
+  let get_access_path = function
+    | Read access_path | Write access_path
+     -> Some access_path
+    | InterfaceCall _
+     -> None
 
   let pp fmt = function
     | Read access_path
      -> F.fprintf fmt "Read of %a" AccessPath.Raw.pp access_path
     | Write access_path
      -> F.fprintf fmt "Write to %a" AccessPath.Raw.pp access_path
+    | InterfaceCall pname
+     -> F.fprintf fmt "Call to un-annotated interface method %a" Typ.Procname.pp pname
 end
 
 module TraceElem = struct
@@ -29,9 +40,12 @@ module TraceElem = struct
 
   type t = {site: CallSite.t; kind: Kind.t} [@@deriving compare]
 
-  let is_read {kind} = match kind with Read _ -> true | Write _ -> false
+  let is_read {kind} = match kind with Read _ -> true | InterfaceCall _ | Write _ -> false
 
-  let is_write {kind} = match kind with Read _ -> false | Write _ -> true
+  let is_write {kind} = match kind with InterfaceCall _ | Read _ -> false | Write _ -> true
+
+  let is_interface_call {kind} =
+    match kind with InterfaceCall _ -> true | Read _ | Write _ -> false
 
   let call_site {site} = site
 
@@ -52,9 +66,13 @@ module TraceElem = struct
   end)
 end
 
-let make_access access_path ~is_write loc =
+let make_field_access access_path ~is_write loc =
+  let site = CallSite.make Typ.Procname.empty_block loc in
+  TraceElem.make (Access.make_field_access access_path ~is_write) site
+
+let make_unannotated_call_access pname loc =
   let site = CallSite.make Typ.Procname.empty_block loc in
-  TraceElem.make (Access.make access_path ~is_write) site
+  TraceElem.make (Access.InterfaceCall pname) site
 
 (* In this domain true<=false. The intended denotations [[.]] are
     [[true]] = the set of all states where we know according, to annotations

infer/src/checkers/ThreadSafetyDomain.mli

@@ -11,7 +11,12 @@ open! IStd
 module F = Format
 
 module Access : sig
-  type t = Read of AccessPath.Raw.t | Write of AccessPath.Raw.t [@@deriving compare]
+  type t =
+    | Read of AccessPath.Raw.t  (** Field read *)
+    | Write of AccessPath.Raw.t  (** Field write *)
+    | InterfaceCall of Typ.Procname.t
+        (** Call to method of interface not annotated with @ThreadSafe *)
+    [@@deriving compare]
 
   val get_access_path : t -> AccessPath.Raw.t option
 
@@ -24,6 +29,8 @@ module TraceElem : sig
   val is_write : t -> bool
 
   val is_read : t -> bool
+
+  val is_interface_call : t -> bool
 end
 
 (** A bool that is true if a lock is definitely held. Note that this is unsound because it assumes
@@ -171,6 +178,8 @@ type summary =
 
 include AbstractDomain.WithBottom with type astate := astate
 
-val make_access : AccessPath.Raw.t -> is_write:bool -> Location.t -> TraceElem.t
+val make_field_access : AccessPath.Raw.t -> is_write:bool -> Location.t -> TraceElem.t
+
+val make_unannotated_call_access : Typ.Procname.t -> Location.t -> TraceElem.t
 
 val pp_summary : F.formatter -> summary -> unit

infer/src/checkers/annotations.ml

@@ -179,6 +179,8 @@ let ia_is_returns_ownership ia = ia_ends_with ia returns_ownership
 
 let ia_is_synchronized_collection ia = ia_ends_with ia synchronized_collection
 
+let ia_is_thread_safe ia = ia_ends_with ia thread_safe
+
 let ia_is_true_on_null ia = ia_ends_with ia true_on_null
 
 let ia_is_initializer ia = ia_ends_with ia initializer_

infer/src/checkers/annotations.mli

@@ -124,6 +124,8 @@ val ia_is_returns_ownership : Annot.Item.t -> bool
 
 val ia_is_synchronized_collection : Annot.Item.t -> bool
 
+val ia_is_thread_safe : Annot.Item.t -> bool
+
 val ia_is_thread_confined : Annot.Item.t -> bool
 
 val ia_is_ui_thread : Annot.Item.t -> bool

infer/tests/codetoanalyze/java/threadsafety/Dispatch.java

@@ -0,0 +1,58 @@
+/*
+ * Copyright (c) 2017 - 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 com.facebook.infer.annotation.ThreadSafe;
+
+interface UnannotatedInterface {
+  public void foo();
+}
+
+@ThreadSafe
+interface AnnotatedInterface {
+  public void foo();
+}
+
+interface AnnotatedInterfaceMethod {
+
+  @ThreadSafe public void foo();
+}
+
+class NotThreadSafe {
+  void notThreadSafeOk(UnannotatedInterface i) {
+    i.foo(); // ok
+  }
+}
+
+
+@ThreadSafe
+public class Dispatch {
+
+  void callUnannotatedInterfaceBad(UnannotatedInterface i) {
+    i.foo();
+  }
+
+  void callUnannotatedInterfaceIndirectBad(NotThreadSafe s, UnannotatedInterface i) {
+    s.notThreadSafeOk(i);
+  }
+
+  synchronized void callUnannotatedInterfaceUnderLockOk(NotThreadSafe s, UnannotatedInterface i) {
+    s.notThreadSafeOk(i);
+  }
+
+  void callAnnotatedInterfaceOk(AnnotatedInterface i) {
+    i.foo();
+  }
+
+  void callAnnotatedInterfaceMethodOk(AnnotatedInterfaceMethod i) {
+    i.foo();
+  }
+
+}

infer/tests/codetoanalyze/java/threadsafety/issues.exp

@@ -47,6 +47,8 @@ codetoanalyze/java/threadsafety/DeDup.java, void DeDup.two_reads(), 3, THREAD_SA
 codetoanalyze/java/threadsafety/DeDup.java, void DeDup.two_writes(), 2, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.DeDup.field`]
 codetoanalyze/java/threadsafety/DeDup.java, void DeDup.write_read(), 2, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.DeDup.field`]
 codetoanalyze/java/threadsafety/DeDup.java, void DeDup.write_read(), 3, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,access to `codetoanalyze.java.checkers.DeDup.field`,<Beginning of write trace>,access to `codetoanalyze.java.checkers.DeDup.field`]
+codetoanalyze/java/threadsafety/Dispatch.java, void Dispatch.callUnannotatedInterfaceBad(UnannotatedInterface), 1, THREAD_SAFETY_VIOLATION, [call to void UnannotatedInterface.foo()]
+codetoanalyze/java/threadsafety/Dispatch.java, void Dispatch.callUnannotatedInterfaceIndirectBad(NotThreadSafe,UnannotatedInterface), 1, THREAD_SAFETY_VIOLATION, [call to void NotThreadSafe.notThreadSafeOk(UnannotatedInterface),call to void UnannotatedInterface.foo()]
 codetoanalyze/java/threadsafety/Locks.java, void Locks.FP_unlockOneLock(), 4, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Locks.f`]
 codetoanalyze/java/threadsafety/Locks.java, void Locks.afterReentrantLockUnlockBad(), 3, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Locks.f`]
 codetoanalyze/java/threadsafety/Locks.java, void Locks.afterUnlockBad(), 3, THREAD_SAFETY_VIOLATION, [access to `codetoanalyze.java.checkers.Locks.f`]