[lockless] detect lock acquisitions from methods annotated @Lockless

Summary: Catch methods annotated (transitively) as `Lockless` which acquire a lock (transitively).

Reviewed By: artempyanykh

Differential Revision: D17396575

fbshipit-source-id: f9f2cfc1b

infer/annotations/src/main/java/com/facebook/infer/annotation/Lockless.java

@@ -0,0 +1,20 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+package com.facebook.infer.annotation;
+
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+@Retention(RetentionPolicy.CLASS)
+@Target({ElementType.CONSTRUCTOR, ElementType.METHOD, ElementType.TYPE})
+
+// Any method, override of a method annotated @Lockless,
+// or a method whose class or superclass is annotated @Lockless, may not acquire a lock
+public @interface Lockless {}

infer/man/man1/infer-full.txt

@@ -421,6 +421,7 @@ OPTIONS
              IVAR_NOT_NULL_CHECKED (enabled by default),
              Internal_error (enabled by default),
              JAVASCRIPT_INJECTION (enabled by default),
+             LOCKLESS_VIOLATION (enabled by default),
              LOCK_CONSISTENCY_VIOLATION (enabled by default),
              LOGGING_PRIVATE_DATA (enabled by default),
              Leak_after_array_abstraction (enabled by default),

infer/man/man1/infer-report.txt

@@ -170,6 +170,7 @@ OPTIONS
              IVAR_NOT_NULL_CHECKED (enabled by default),
              Internal_error (enabled by default),
              JAVASCRIPT_INJECTION (enabled by default),
+             LOCKLESS_VIOLATION (enabled by default),
              LOCK_CONSISTENCY_VIOLATION (enabled by default),
              LOGGING_PRIVATE_DATA (enabled by default),
              Leak_after_array_abstraction (enabled by default),

infer/man/man1/infer.txt

@@ -421,6 +421,7 @@ OPTIONS
              IVAR_NOT_NULL_CHECKED (enabled by default),
              Internal_error (enabled by default),
              JAVASCRIPT_INJECTION (enabled by default),
+             LOCKLESS_VIOLATION (enabled by default),
              LOCK_CONSISTENCY_VIOLATION (enabled by default),
              LOGGING_PRIVATE_DATA (enabled by default),
              Leak_after_array_abstraction (enabled by default),

infer/src/base/IssueType.ml

@@ -328,6 +328,8 @@ let leak_in_footprint = register_from_string "Leak_in_footprint"
 
 let lock_consistency_violation = register_from_string "LOCK_CONSISTENCY_VIOLATION"
 
+let lockless_violation = register_from_string "LOCKLESS_VIOLATION"
+
 let logging_private_data = register_from_string "LOGGING_PRIVATE_DATA"
 
 let expensive_loop_invariant_call = register_from_string "EXPENSIVE_LOOP_INVARIANT_CALL"

infer/src/base/IssueType.mli

@@ -216,6 +216,8 @@ val leak_after_array_abstraction : t
 
 val leak_in_footprint : t
 
+val lockless_violation : t
+
 val lock_consistency_violation : t
 
 val logging_private_data : t

infer/src/checkers/annotations.ml

@@ -51,6 +51,8 @@ let inject_prop = "InjectProp"
 
 let inject_view = "InjectView"
 
+let lockless = "Lockless"
+
 let nonnull = "Nonnull"
 
 let no_allocation = "NoAllocation"

infer/src/checkers/annotations.mli

@@ -17,6 +17,8 @@ val expensive : string
 
 val inject_prop : string
 
+val lockless : string
+
 val no_allocation : string
 
 val nullable : string

infer/src/concurrency/starvation.ml

@@ -190,7 +190,9 @@ module ReportMap : sig
 
   val add_starvation : StarvationDomain.Event.severity_t -> report_add_t
 
-  val add_strict_mode_volation : report_add_t
+  val add_strict_mode_violation : report_add_t
+
+  val add_lockless_violation : report_add_t
 
   val log : IssueLog.t -> Tenv.t -> Procdesc.t -> t -> IssueLog.t
 end = struct
@@ -198,6 +200,7 @@ end = struct
     | Starvation of StarvationDomain.Event.severity_t
     | Deadlock of int
     | StrictModeViolation of int
+    | LocklessViolation of int
 
   type report_t = {problem: problem; pname: Typ.Procname.t; ltr: Errlog.loc_trace; message: string}
 
@@ -225,11 +228,16 @@ end = struct
     add loc report map
 
 
-  let add_strict_mode_volation pname loc ltr message (map : t) =
+  let add_strict_mode_violation pname loc ltr message (map : t) =
     let report = {problem= StrictModeViolation (-List.length ltr); pname; ltr; message} in
     add loc report map
 
 
+  let add_lockless_violation pname loc ltr message (map : t) =
+    let report = {problem= LocklessViolation (-List.length ltr); pname; ltr; message} in
+    add loc report map
+
+
   let log start_issue_log tenv pdesc map =
     let log_report ~issue_log loc {problem; pname; ltr; message} =
       let issue_type =
@@ -240,6 +248,8 @@ end = struct
             IssueType.starvation
         | StrictModeViolation _ ->
             IssueType.strict_mode_violation
+        | LocklessViolation _ ->
+            IssueType.lockless_violation
       in
       if Reporting.is_suppressed tenv pdesc issue_type then issue_log
       else
@@ -274,6 +284,12 @@ end = struct
       | _ ->
           None
     in
+    let filter_map_lockless_violation = function
+      | {problem= LocklessViolation l} as r ->
+          Some (l, r)
+      | _ ->
+          None
+    in
     let compare_reports weight_compare (w, r) (w', r') =
       match weight_compare w w' with 0 -> String.compare r.message r'.message | result -> result
     in
@@ -281,7 +297,9 @@ end = struct
       let deadlocks = List.filter_map problems ~f:filter_map_deadlock in
       let starvations = List.filter_map problems ~f:filter_map_starvation in
       let strict_mode_violations = List.filter_map problems ~f:filter_map_strict_mode_violation in
+      let lockless_violations = List.filter_map problems ~f:filter_map_lockless_violation in
       log_reports (compare_reports Int.compare) loc deadlocks issue_log
+      |> log_reports (compare_reports Int.compare) loc lockless_violations
       |> log_reports (compare_reports StarvationDomain.Event.compare_severity_t) loc starvations
       |> log_reports (compare_reports Int.compare) loc strict_mode_violations
     in
@@ -345,6 +363,38 @@ let fold_reportable_summaries (tenv, current_summary) clazz ~init ~f =
   List.fold methods ~init ~f
 
 
+let report_lockless_violations (tenv, summary) {StarvationDomain.events} report_map =
+  let open StarvationDomain in
+  (* this is inneficient as it climbs the hierarchy potentially twice *)
+  let is_annotated_lockless tenv pname =
+    let check annot = Annotations.(ia_ends_with annot lockless) in
+    let check_attributes pname =
+      PatternMatch.check_class_attributes check tenv pname
+      || Annotations.pname_has_return_annot pname
+           ~attrs_of_pname:Summary.OnDisk.proc_resolve_attributes check
+    in
+    PatternMatch.override_exists check_attributes tenv pname
+  in
+  let pname = Summary.get_proc_name summary in
+  if not (is_annotated_lockless tenv pname) then report_map
+  else
+    let report_violation (event : Event.t) report_map =
+      match event.elem with
+      | LockAcquire _ ->
+          let error_message =
+            Format.asprintf "Method %a is annotated %s but%a." pname_pp pname
+              (MF.monospaced_to_string Annotations.lockless)
+              Event.pp_human event
+          in
+          let loc = Event.get_loc event in
+          let ltr = Event.make_trace pname event in
+          ReportMap.add_lockless_violation pname loc ltr error_message report_map
+      | _ ->
+          report_map
+    in
+    EventDomain.fold report_violation events report_map
+
+
 (*  Note about how many times we report a deadlock: normally twice, at each trace starting point.
          Due to the fact we look for deadlocks in the summaries of the class at the root of a path,
          this will fail when (a) the lock is of class type (ie as used in static sync methods), because
@@ -463,7 +513,7 @@ let report_starvation env {StarvationDomain.events; ui} report_map' =
             ui_explain
         in
         let ltr = trace @ ui_trace in
-        ReportMap.add_strict_mode_volation current_pname loc ltr error_message report_map
+        ReportMap.add_strict_mode_violation current_pname loc ltr error_message report_map
     | LockAcquire endpoint_lock ->
         Lock.owner_class endpoint_lock
         |> Option.value_map ~default:report_map ~f:(fun endpoint_class ->
@@ -496,6 +546,7 @@ let reporting {Callbacks.procedures; source_file} =
       Payload.read_toplevel_procedure (Procdesc.get_proc_name proc_desc)
       |> Option.value_map ~default:issue_log ~f:(fun summary ->
              report_deadlocks env summary ReportMap.empty
+             |> report_lockless_violations env summary
              |> report_starvation env summary
              |> ReportMap.log issue_log tenv proc_desc )
     else issue_log

infer/tests/codetoanalyze/java/starvation/LocklessTests.java

@@ -0,0 +1,58 @@
+/*
+ * Copyright (c) Facebook, Inc. and its affiliates.
+ *
+ * This source code is licensed under the MIT license found in the
+ * LICENSE file in the root directory of this source tree.
+ */
+
+import com.facebook.infer.annotation.Lockless;
+
+class LocklessTests {}
+
+interface Listener {
+  @Lockless
+  void locklessMethod();
+
+  void normalMethod();
+}
+
+class LocklessTestsA implements Listener {
+  // should warn
+  @Override
+  public void locklessMethod() {
+    synchronized (this) {
+    }
+  }
+
+  // no warnings here
+  @Override
+  public void normalMethod() {
+    synchronized (this) {
+    }
+  }
+}
+
+class LocklessTestsB implements Listener {
+  // should warn
+  @Lockless
+  @Override
+  public synchronized void locklessMethod() {}
+
+  // no warnings here
+  @Override
+  public synchronized void normalMethod() {}
+}
+
+class LocklessTestsC implements Listener {
+  private synchronized void takeLock() {}
+
+  // should warn
+  @Override
+  public void locklessMethod() {
+    takeLock();
+  }
+
+  // no warnings here
+  @Override
+  public synchronized void normalMethod() {}
+}

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

@@ -24,6 +24,9 @@ codetoanalyze/java/starvation/Interclass.java, Interclass.interclass1Bad(Intercl
 codetoanalyze/java/starvation/Interproc.java, Interproc.interproc1Bad(InterprocA):void, 9, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void Interproc.interproc1Bad(InterprocA)`, locks `this` in `class Interproc`,Method call: `void Interproc.interproc2Bad(InterprocA)`, locks `b` in `class InterprocA`,[Trace 2] `void InterprocA.interproc1Bad(Interproc)`, locks `this` in `class InterprocA`,Method call: `void InterprocA.interproc2Bad(Interproc)`, locks `d` in `class Interproc`]
 codetoanalyze/java/starvation/Intraproc.java, Intraproc.intraBad(IntraprocA):void, 10, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void Intraproc.intraBad(IntraprocA)`, locks `this` in `class Intraproc`, locks `o` in `class IntraprocA`,[Trace 2] `void IntraprocA.intraBad(Intraproc)`, locks `this` in `class IntraprocA`, locks `o` in `class Intraproc`]
 codetoanalyze/java/starvation/LegacySync.java, LegacySync.onUiThreadOpBad():java.lang.Object, 25, STARVATION, no_bucket, ERROR, [[Trace 1] `Object LegacySync.onUiThreadOpBad()`, locks `this.table` in `class LegacySync`,[Trace 2] `void LegacySync.notOnUiThreadSyncedBad()`, locks `this.table` in `class LegacySync`,calls `Object Future.get()`,[Trace 1 on UI thread] `Object LegacySync.onUiThreadOpBad()`,`Object LegacySync.onUiThreadOpBad()` is annotated `UiThread`]
+codetoanalyze/java/starvation/LocklessTests.java, LocklessTestsA.locklessMethod():void, 23, LOCKLESS_VIOLATION, no_bucket, ERROR, [`void LocklessTestsA.locklessMethod()`, locks `this` in `class LocklessTestsA`]
+codetoanalyze/java/starvation/LocklessTests.java, LocklessTestsB.locklessMethod():void, 39, LOCKLESS_VIOLATION, no_bucket, ERROR, [`void LocklessTestsB.locklessMethod()`, locks `this` in `class LocklessTestsB`]
+codetoanalyze/java/starvation/LocklessTests.java, LocklessTestsC.locklessMethod():void, 52, LOCKLESS_VIOLATION, no_bucket, ERROR, [`void LocklessTestsC.locklessMethod()`,Method call: `void LocklessTestsC.takeLock()`, locks `this` in `class LocklessTestsC`]
 codetoanalyze/java/starvation/MainThreadTest.java, AnnotatedClass.callTransactBad(MainThreadTest):void, 30, STARVATION, no_bucket, ERROR, [`void AnnotatedClass.callTransactBad(MainThreadTest)`,Method call: `void MainThreadTest.doTransact()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`,[Trace on UI thread] `void AnnotatedClass.callTransactBad(MainThreadTest)`,class `AnnotatedClass` is annotated `UiThread`]
 codetoanalyze/java/starvation/MainThreadTest.java, MainThreadTest.callTransactBad():void, 23, STARVATION, no_bucket, ERROR, [`void MainThreadTest.callTransactBad()`,Method call: `void MainThreadTest.doTransact()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`,[Trace on UI thread] `void MainThreadTest.callTransactBad()`,`void MainThreadTest.callTransactBad()` is annotated `UiThread`]
 codetoanalyze/java/starvation/MyActivity.java, MyActivity.onCreate(android.os.Bundle):void, 28, STARVATION, no_bucket, ERROR, [`void MyActivity.onCreate(Bundle)`,Method call: `void MyActivity.bad()`,calls `boolean Binder.transact(int,Parcel,Parcel,int)`,[Trace on UI thread] `void MyActivity.onCreate(Bundle)`,`void MyActivity.onCreate(Bundle)` is a standard UI-thread method]