Minimal thread safety analysis for C++

Summary:
This is a minimal change to (poorly) recognize and model std::mutex
lock and unlock methods, and to surface all thread safety issues for
C++ based on the computed summaries with no filtering.

This ignores much of the Java analysis, including everything about the
Threads domain.  The S/N is comically low at this point.

Reviewed By: sblackshear

Differential Revision: D5120485

fbshipit-source-id: 0f08caa

Makefile

@@ -32,7 +32,7 @@ BUILD_SYSTEMS_TESTS += \
 
 DIRECT_TESTS += \
   c_bufferoverrun c_errors c_frontend \
-  cpp_bufferoverrun cpp_errors cpp_frontend cpp_quandary cpp_siof \
+  cpp_bufferoverrun cpp_errors cpp_frontend cpp_quandary cpp_siof cpp_threadsafety \
 
 ifneq ($(BUCK),no)
 BUILD_SYSTEMS_TESTS += buck-clang-db

infer/src/checkers/ThreadSafety.ml

@@ -82,7 +82,17 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
         && String.equal (Typ.Procname.java_get_method java_pname) method_name_str
     | _ -> false
 
-  let get_lock_model = function
+  let get_lock_model =
+    let is_std_mutex_lock =
+      let matcher = QualifiedCppName.Match.of_fuzzy_qual_names ["std::mutex::lock"] in
+      fun pname ->
+        QualifiedCppName.Match.match_qualifiers matcher (Typ.Procname.get_qualifiers pname)
+    and is_std_mutex_unlock =
+      let matcher = QualifiedCppName.Match.of_fuzzy_qual_names ["std::mutex::unlock"] in
+      fun pname ->
+        QualifiedCppName.Match.match_qualifiers matcher (Typ.Procname.get_qualifiers pname)
+    in
+    function
     | Typ.Procname.Java java_pname ->
         if is_thread_utils_method "assertHoldsLock" (Typ.Procname.Java java_pname) then Lock
         else
@@ -113,6 +123,10 @@ module TransferFunctions (CFG : ProcCfg.S) = struct
             | _ ->
                 NoEffect
           end
+    | (Typ.Procname.ObjC_Cpp _ as pname) when is_std_mutex_lock pname ->
+        Lock
+    | (Typ.Procname.ObjC_Cpp _ as pname) when is_std_mutex_unlock pname ->
+        Unlock
     | pname when Typ.Procname.equal pname BuiltinDecl.__set_locked_attribute ->
         Lock
     | pname when Typ.Procname.equal pname BuiltinDecl.__delete_locked_attribute ->
@@ -1200,8 +1214,16 @@ let report_unsafe_accesses ~is_file_threadsafe aggregated_access_map =
           - the method/class of the access is thread-safe (or an override or superclass is), or
           - any access is in a field marked thread-safe (or an override) *)
        let should_report pdesc tenv =
-         ((is_file_threadsafe || accessed_by_threadsafe_method) && should_report_on_proc pdesc tenv)
+         match Procdesc.get_proc_name pdesc with
-         || is_thread_safe_method pdesc tenv in
+         | Java _ ->
+             ((is_file_threadsafe || accessed_by_threadsafe_method)
+              && should_report_on_proc pdesc tenv)
+             || is_thread_safe_method pdesc tenv
+         | ObjC_Cpp _ ->
+             true
+         | _ ->
+             false
+       in
        let reportable_accesses =
          List.filter ~f:(fun (_, _, _, tenv, pdesc) -> should_report pdesc tenv) grouped_accesses in
        List.fold
@@ -1271,7 +1293,7 @@ let make_results_table file_env =
 
 (**
    Principles for race reporting.
-   Two accesses are excluded if they are both protetected by the same lock or
+   Two accesses are excluded if they are both protected by the same lock or
    are known to be on the same thread. Otherwise they are in conflict. We want to report
    conflicting accesses one of which is a write.
 
@@ -1280,7 +1302,7 @@ let make_results_table file_env =
    -- If a protected access races with an unprotected one, we don't
    report the protected but we do report the unprotected one (and we
    point to the protected from the unprotected one).
-   This way the report is at the line number ina race-pair where the programmer should take action.
+   This way the report is at the line number in a race-pair where the programmer should take action.
    -- Similarly, if a threaded and unthreaded (not known to be threaded) access race,
    we report at the unthreaded site.
 

infer/src/checkers/ThreadSafetyDomain.ml

@@ -23,7 +23,7 @@ module Access = struct
 
   let pp fmt (access_path, access_kind) = match access_kind with
     | Read -> F.fprintf fmt "Read of %a" AccessPath.Raw.pp access_path
-    | Write -> F.fprintf fmt "Write of %a" AccessPath.Raw.pp access_path
+    | Write -> F.fprintf fmt "Write to %a" AccessPath.Raw.pp access_path
 end
 
 module TraceElem = struct
@@ -77,10 +77,10 @@ module LocksDomain = AbstractDomain.BooleanAnd
 
 (* In this domain false<=true. The intended denotations [[.]] are
    [[true]] = the set of all states where we know according, to annotations
-             or assertions, that we are on the UI thread (or some oter specific thread).
+             or assertions, that we are on the UI thread (or some other specific thread).
    [[false]] = the set of all states
    The use of || for join in this domain enforces that, to not know for sure you are threaded,
-   it is enough to be unthreaded in one branch. (See RaceWithMainThread.java for  examples)
+   it is enough to be unthreaded in one branch. (See RaceWithMainThread.java for examples)
 *)
 module ThreadsDomain = AbstractDomain.BooleanAnd
 

infer/src/checkers/registerCheckers.ml

@@ -50,6 +50,7 @@ let checkers = [
   "thread safety", Config.threadsafety,
   [Procedure ThreadSafety.analyze_procedure, Config.Clang;
    Procedure ThreadSafety.analyze_procedure, Config.Java;
+   Cluster ThreadSafety.file_analysis, Config.Clang;
    Cluster ThreadSafety.file_analysis, Config.Java]
 ]
 

infer/tests/codetoanalyze/cpp/threadsafety/Makefile

@@ -0,0 +1,21 @@
+# 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.
+
+TESTS_DIR = ../../..
+
+ANALYZER = checkers
+# see explanations in cpp/errors/Makefile for the custom isystem
+CLANG_OPTIONS = -x c++ -std=c++11 -nostdinc++ -isystem$(ROOT_DIR) -isystem$(CLANG_INCLUDES)/c++/v1/ -c
+INFER_OPTIONS = --threadsafety --ml-buckets cpp --no-filtering --debug-exceptions --project-root $(TESTS_DIR) --no-failures-allowed
+INFER_OPTIONS += --debug
+INFERPRINT_OPTIONS = --issues-tests
+
+SOURCES = $(wildcard *.cpp)
+
+include $(TESTS_DIR)/clang.make
+
+infer-out/report.json: $(MAKEFILE_LIST)

infer/tests/codetoanalyze/cpp/threadsafety/basics.cpp

@@ -0,0 +1,54 @@
+/*
+ * 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.
+ */
+
+#include <mutex>
+
+namespace basics {
+
+class Basic {
+ public:
+  Basic() {}
+
+  void set(int new_value) {
+    not_guarded = new_value;
+    mutex_.lock();
+    well_guarded = new_value;
+    suspiciously_read = new_value;
+    mutex_.unlock();
+    suspiciously_written = new_value;
+  }
+
+  int get1() {
+    int result;
+    mutex_.lock();
+    result = well_guarded;
+    mutex_.unlock();
+    return result;
+  }
+
+  int get2() {
+    int result;
+    mutex_.lock();
+    result = suspiciously_written;
+    mutex_.unlock();
+    return result;
+  }
+
+  int get3() { return not_guarded; }
+
+  int get4() { return suspiciously_read; }
+
+ private:
+  int well_guarded;
+  int suspiciously_read;
+  int suspiciously_written;
+  int not_guarded;
+  std::mutex mutex_;
+};
+}

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

@@ -0,0 +1,5 @@
+codetoanalyze/cpp/threadsafety/basics.cpp, basics::Basic_get2, 3, THREAD_SAFETY_VIOLATION, [access to `suspiciously_written`]
+codetoanalyze/cpp/threadsafety/basics.cpp, basics::Basic_get3, 0, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,access to `not_guarded`,<Beginning of write trace>,access to `not_guarded`]
+codetoanalyze/cpp/threadsafety/basics.cpp, basics::Basic_get4, 0, THREAD_SAFETY_VIOLATION, [<Beginning of read trace>,access to `suspiciously_read`,<Beginning of write trace>,access to `suspiciously_read`]
+codetoanalyze/cpp/threadsafety/basics.cpp, basics::Basic_set, 1, THREAD_SAFETY_VIOLATION, [access to `not_guarded`]
+codetoanalyze/cpp/threadsafety/basics.cpp, basics::Basic_set, 6, THREAD_SAFETY_VIOLATION, [access to `suspiciously_written`]