[threadsafety] run thread safety checker on its own

Summary: The thread safety checker is run independently of other analyses, using the command "infer -a threadsafety -- <build-command>".

Reviewed By: sblackshear

Differential Revision: D4148553

fbshipit-source-id: bc7b3f9

Makefile

@@ -22,7 +22,7 @@ endif
 ifeq ($(BUILD_JAVA_ANALYZERS),yes)
 DIRECT_TESTS += \
   java_checkers_test java_eradicate_test java_infer_test java_tracing_test \
-  java_quandary_test java_crashcontext_test java_harness_test
+  java_quandary_test java_threadsafety_test java_crashcontext_test java_harness_test
 endif
 ifneq ($(XCODE_SELECT),no)
 DIRECT_TESTS += objc_frontend_test objc_errors_test objc_linters_test objcpp_frontend_test objcpp_linters_test

infer/lib/python/inferlib/config.py

@@ -72,6 +72,7 @@ ANALYZER_TRACING = 'tracing'
 ANALYZER_CRASHCONTEXT = 'crashcontext'
 ANALYZER_LINTERS = 'linters'
 ANALYZER_QUANDARY = 'quandary'
+ANALYZER_THREADSAFETY = 'threadsafety'
 
 ANALYZERS = [
     ANALYZER_CAPTURE,
@@ -83,4 +84,5 @@ ANALYZERS = [
     ANALYZER_LINTERS,
     ANALYZER_TRACING,
     ANALYZER_QUANDARY,
+    ANALYZER_THREADSAFETY,
 ]

infer/src/IR/Localise.ml

@@ -82,6 +82,7 @@ let stack_variable_address_escape = "STACK_VARIABLE_ADDRESS_ESCAPE"
 let static_initialization_order_fiasco = "STATIC_INITIALIZATION_ORDER_FIASCO"
 let strong_delegate_warning = "STRONG_DELEGATE_WARNING"
 let tainted_value_reaching_sensitive_function = "TAINTED_VALUE_REACHING_SENSITIVE_FUNCTION"
+let thread_safety_error = "THREAD_SAFETY_ERROR"
 let unary_minus_applied_to_unsigned_expression = "UNARY_MINUS_APPLIED_TO_UNSIGNED_EXPRESSION"
 let unsafe_guarded_by_access = "UNSAFE_GUARDED_BY_ACCESS"
 let uninitialized_value = "UNINITIALIZED_VALUE"

infer/src/IR/Localise.mli

@@ -82,6 +82,7 @@ val use_after_free : t
 val skip_function : t
 val skip_pointer_dereference : t
 val tainted_value_reaching_sensitive_function : t
+val thread_safety_error : t
 
 (** description field of error messages *)
 type error_desc = {

infer/src/backend/InferPrint.re

@@ -323,7 +323,8 @@ let should_report (issue_kind: Exceptions.err_kind) issue_type error_desc =>
       | Crashcontext
       | Infer
       | Linters
-      | Quandary => false
+      | Quandary 
+      | Threadsafety => false
       };
     if analyzer_is_whitelisted {
       true
@@ -385,6 +386,7 @@ let should_report (issue_kind: Exceptions.err_kind) issue_type error_desc =>
                 static_initialization_order_fiasco,
                 strong_delegate_warning,
                 tainted_value_reaching_sensitive_function,
+                thread_safety_error,
                 unsafe_guarded_by_access
               ];
             IList.mem Localise.equal issue_type reportable_issue_types

infer/src/backend/infer.ml

@@ -191,7 +191,7 @@ let analyze = function
         Config.print_usage_exit ()
       );
       (match Config.analyzer with
-       | Infer | Eradicate | Checkers | Tracing | Crashcontext | Quandary ->
+       | Infer | Eradicate | Checkers | Tracing | Crashcontext | Quandary | Threadsafety ->
            (* Still handled by infer.py through capture function above *)
            ()
        | Linters ->

infer/src/base/Config.ml

@@ -18,13 +18,13 @@ module F = Format
 
 
 type analyzer = Capture | Compile | Infer | Eradicate | Checkers | Tracing
-              | Crashcontext | Linters | Quandary
+              | Crashcontext | Linters | Quandary | Threadsafety
 
 let string_to_analyzer =
   [("capture", Capture); ("compile", Compile);
    ("infer", Infer); ("eradicate", Eradicate); ("checkers", Checkers);
    ("tracing", Tracing); ("crashcontext", Crashcontext); ("linters", Linters);
-   ("quandary", Quandary);]
+   ("quandary", Quandary); ("threadsafety", Threadsafety)]
 
 let clang_frontend_action_symbols = [
   ("lint", `Lint);
@@ -551,11 +551,11 @@ and analyzer =
     (* NOTE: if compilation fails here, it means you have added a new analyzer without updating the
        documentation of this option *)
     | Capture | Compile | Infer | Eradicate | Checkers | Tracing | Crashcontext | Linters
-    | Quandary -> () in
+    | Quandary | Threadsafety -> () in
   CLOpt.mk_symbol_opt ~deprecated:["analyzer"] ~long:"analyzer" ~short:"a"
     ~exes:CLOpt.[Toplevel]
     "Specify which analyzer to run (only one at a time is supported):\n\
-     - infer, eradicate, checkers, quandary: run the specified analysis\n\
+     - infer, eradicate, checkers, quandary, threadsafety: run the specified analysis\n\
      - capture: run capture phase only (no analysis)\n\
      - compile: run compilation command without interfering (not supported by all frontends)\n\
      - crashcontext, tracing: experimental (see --crashcontext and --tracing)\n\
@@ -645,7 +645,7 @@ and check_duplicate_symbols =
     ~exes:CLOpt.[Analyze]
     "Check if a symbol with the same name is defined in more than one file."
 
-and checkers, crashcontext, eradicate, quandary =
+and checkers, crashcontext, eradicate, quandary, threadsafety =
   let checkers =
     CLOpt.mk_bool ~deprecated:["checkers"] ~long:"checkers"
       "Activate the checkers instead of the full analysis"
@@ -665,7 +665,12 @@ and checkers, crashcontext, eradicate, quandary =
       "Activate the quandary taint analysis"
       [checkers] []
   in
-  (checkers, crashcontext, eradicate, quandary)
+  let threadsafety =
+    CLOpt.mk_bool_group ~deprecated:["threadsafety"] ~long:"threadsafety"
+      "Activate the thread safety analysis"
+      [checkers] []
+  in
+  (checkers, crashcontext, eradicate, quandary, threadsafety)
 
 and checkers_repeated_calls =
   CLOpt.mk_bool ~long:"checkers-repeated-calls"
@@ -1192,11 +1197,6 @@ and testing_mode =
   CLOpt.mk_bool ~deprecated:["testing_mode"; "-testing_mode"] ~long:"testing-mode" ~short:"tm"
     "Mode for testing, where no headers are translated, and dot files are created (clang only)"
 
-and thread_safety =
-  CLOpt.mk_bool ~long:"thread-safety"
-    ~exes:CLOpt.[Analyze]
-    "Run the experimental thread safety checker. (In conjunction with -a checkers)"
-
 and trace_join =
   CLOpt.mk_bool ~deprecated:["trace_join"] ~long:"trace-join"
     "Detailed tracing information during prop join operations"
@@ -1351,6 +1351,7 @@ let post_parsing_initialization () =
   | Some Crashcontext -> checkers := true; crashcontext := true
   | Some Eradicate -> checkers := true; eradicate := true
   | Some Quandary -> checkers := true; quandary := true
+  | Some Threadsafety -> checkers := true; threadsafety := true
   | Some Tracing -> tracing := true
   | Some (Capture | Compile | Infer | Linters) | None -> ()
 
@@ -1498,13 +1499,13 @@ and symops_per_iteration = !symops_per_iteration
 and test = !test
 and test_filtering = !test_filtering
 and testing_mode = !testing_mode
+and threadsafety = !threadsafety
 and trace_error = !trace_error
 and trace_ondemand = !trace_ondemand
 and trace_join = !trace_join
 and trace_rearrange = !trace_rearrange
 and type_size = !type_size
 and unsafe_malloc = !unsafe_malloc
-and thread_safety = !thread_safety
 and use_compilation_database = !use_compilation_database
 and whole_seconds = !whole_seconds
 and worklist_mode = !worklist_mode
@@ -1526,7 +1527,7 @@ and analysis_blacklist_files_containing analyzer =
 and analysis_suppress_errors analyzer =
   IList.assoc (=) analyzer analysis_suppress_errors_options
 
-let checkers_enabled = not (eradicate || crashcontext || quandary)
+let checkers_enabled = not (eradicate || crashcontext || quandary || threadsafety)
 
 let clang_frontend_do_capture, clang_frontend_do_lint =
   match !clang_frontend_action with

infer/src/base/Config.mli

@@ -16,7 +16,7 @@ open! Utils
 
 (** Various kind of analyzers *)
 type analyzer = Capture | Compile | Infer | Eradicate | Checkers | Tracing
-              | Crashcontext | Linters | Quandary
+              | Crashcontext | Linters | Quandary | Threadsafety
 
 (** Association list of analyzers and their names *)
 val string_to_analyzer : (string * analyzer) list
@@ -254,13 +254,13 @@ val symops_per_iteration : int
 val test : bool
 val test_filtering : bool
 val testing_mode : bool
+val threadsafety : bool
 val trace_error : bool
 val trace_ondemand : bool
 val trace_join : bool
 val trace_rearrange : bool
 val type_size : bool
 val unsafe_malloc : bool
-val thread_safety: bool
 val use_compilation_database : [ `Deps | `NoDeps ] option
 val whole_seconds : bool
 val worklist_mode : int

infer/src/checkers/ThreadSafety.ml

@@ -161,7 +161,7 @@ let report_thread_safety_errors ( _, tenv, pname, pdesc) writestate =
     Checkers.ST.report_error tenv
       pname
       pdesc
-      "CHECKERS_THREAD_SAFETY_WARNING"
+      (Localise.to_string Localise.thread_safety_error)
       (Procdesc.get_loc pdesc)
       description
   in

infer/src/checkers/registerCheckers.ml

@@ -59,7 +59,7 @@ let active_procedure_checkers () =
 
 let active_cluster_checkers () =
   [(Checkers.callback_check_cluster_access, false, Some Config.Java);
-   (ThreadSafety.file_analysis, Config.checkers_enabled && Config.thread_safety, Some Config.Java)
+   (ThreadSafety.file_analysis, Config.threadsafety, Some Config.Java)
   ]
 
 let register () =

infer/tests/codetoanalyze/java/checkers/Makefile

@@ -10,6 +10,6 @@ include $(JAVA_TEST_DIR)/java.make
 
 ANALYZER = checkers
 
-INFER_OPTIONS = --thread-safety --no-filtering --debug-exceptions
+INFER_OPTIONS = --no-filtering --debug-exceptions
 
 JAVA_SOURCE_FILES = $(wildcard *.java)

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

@@ -32,8 +32,5 @@ PrintfArgsChecker.java, void PrintfArgsChecker.formatStringIsNotLiteral(PrintStr
 PrintfArgsChecker.java, void PrintfArgsChecker.notSuppressed(PrintStream), 1, CHECKERS_PRINTF_ARGS
 PrintfArgsChecker.java, void PrintfArgsChecker.stringInsteadOfInteger(PrintStream), 1, CHECKERS_PRINTF_ARGS
 PrintfArgsChecker.java, void PrintfArgsChecker.wrongNumberOfArguments(PrintStream), 1, CHECKERS_PRINTF_ARGS
-ThreadSafeExample.java, void ExtendsThreadSafeExample.newmethodBad(), 0, CHECKERS_THREAD_SAFETY_WARNING
-ThreadSafeExample.java, void ExtendsThreadSafeExample.tsOK(), 0, CHECKERS_THREAD_SAFETY_WARNING
-ThreadSafeExample.java, void ThreadSafeExample.tsBad(), 0, CHECKERS_THREAD_SAFETY_WARNING
 TwoCheckersExample.java, List TwoCheckersExample.shouldRaiseImmutableCastError(), 0, CHECKERS_IMMUTABLE_CAST
 TwoCheckersExample.java, List TwoCheckersExample.shouldRaisePerformanceCriticalError(), 1, CHECKERS_CALLS_EXPENSIVE_METHOD

infer/tests/codetoanalyze/java/threadsafety/Makefile

@@ -0,0 +1,14 @@
+# 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.
+
+JAVA_TEST_DIR = ..
+include $(JAVA_TEST_DIR)/java.make
+
+ANALYZER = threadsafety
+INFER_OPTIONS =  --no-filtering --debug-exceptions
+
+JAVA_SOURCE_FILES = $(wildcard *.java)

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

@@ -0,0 +1,3 @@
+ThreadSafeExample.java, void ExtendsThreadSafeExample.newmethodBad(), 0, THREAD_SAFETY_ERROR
+ThreadSafeExample.java, void ExtendsThreadSafeExample.tsOK(), 0, THREAD_SAFETY_ERROR
+ThreadSafeExample.java, void ThreadSafeExample.tsBad(), 0, THREAD_SAFETY_ERROR