diff --git a/infer/annotations/src/main/java/com/facebook/infer/annotation/Lockless.java b/infer/annotations/src/main/java/com/facebook/infer/annotation/Lockless.java new file mode 100644 index 000000000..6456d87c1 --- /dev/null +++ b/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 {} diff --git a/infer/man/man1/infer-full.txt b/infer/man/man1/infer-full.txt index 4b6df5c00..fcb0fdf80 100644 --- a/infer/man/man1/infer-full.txt +++ b/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), diff --git a/infer/man/man1/infer-report.txt b/infer/man/man1/infer-report.txt index 144146ebc..df59be235 100644 --- a/infer/man/man1/infer-report.txt +++ b/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), diff --git a/infer/man/man1/infer.txt b/infer/man/man1/infer.txt index 57e5c174e..b47e25b45 100644 --- a/infer/man/man1/infer.txt +++ b/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), diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index 05c1c6e67..44638213b 100644 --- a/infer/src/base/IssueType.ml +++ b/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" diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index f3b969298..5e558fad3 100644 --- a/infer/src/base/IssueType.mli +++ b/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 diff --git a/infer/src/checkers/annotations.ml b/infer/src/checkers/annotations.ml index 926755f29..1c10b61bd 100644 --- a/infer/src/checkers/annotations.ml +++ b/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" diff --git a/infer/src/checkers/annotations.mli b/infer/src/checkers/annotations.mli index 7ad4b0d92..6489069b2 100644 --- a/infer/src/checkers/annotations.mli +++ b/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 diff --git a/infer/src/concurrency/starvation.ml b/infer/src/concurrency/starvation.ml index 59d0309cb..9e55ad4c4 100644 --- a/infer/src/concurrency/starvation.ml +++ b/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 diff --git a/infer/tests/codetoanalyze/java/starvation/LocklessTests.java b/infer/tests/codetoanalyze/java/starvation/LocklessTests.java new file mode 100644 index 000000000..dd213a12b --- /dev/null +++ b/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() {} +} diff --git a/infer/tests/codetoanalyze/java/starvation/issues.exp b/infer/tests/codetoanalyze/java/starvation/issues.exp index d5d8ad073..065133d31 100644 --- a/infer/tests/codetoanalyze/java/starvation/issues.exp +++ b/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]