From bf504c5b70aa6da0485f84510c06e68f056adf23 Mon Sep 17 00:00:00 2001 From: Josh Berdine Date: Wed, 31 May 2017 01:45:55 -0700 Subject: [PATCH] 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 | 2 +- infer/src/checkers/ThreadSafety.ml | 32 +++++++++-- infer/src/checkers/ThreadSafetyDomain.ml | 6 +-- infer/src/checkers/registerCheckers.ml | 1 + .../codetoanalyze/cpp/threadsafety/Makefile | 21 ++++++++ .../codetoanalyze/cpp/threadsafety/basics.cpp | 54 +++++++++++++++++++ .../codetoanalyze/cpp/threadsafety/issues.exp | 5 ++ 7 files changed, 112 insertions(+), 9 deletions(-) create mode 100644 infer/tests/codetoanalyze/cpp/threadsafety/Makefile create mode 100644 infer/tests/codetoanalyze/cpp/threadsafety/basics.cpp create mode 100644 infer/tests/codetoanalyze/cpp/threadsafety/issues.exp diff --git a/Makefile b/Makefile index deaeeb11b..6884c7751 100644 --- a/Makefile +++ b/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 diff --git a/infer/src/checkers/ThreadSafety.ml b/infer/src/checkers/ThreadSafety.ml index 15d65d1fb..2567ce475 100644 --- a/infer/src/checkers/ThreadSafety.ml +++ b/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) - || is_thread_safe_method pdesc tenv in + match Procdesc.get_proc_name pdesc with + | 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. diff --git a/infer/src/checkers/ThreadSafetyDomain.ml b/infer/src/checkers/ThreadSafetyDomain.ml index ba321040d..8d3b0942c 100644 --- a/infer/src/checkers/ThreadSafetyDomain.ml +++ b/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 diff --git a/infer/src/checkers/registerCheckers.ml b/infer/src/checkers/registerCheckers.ml index bc35dda49..8962c302c 100644 --- a/infer/src/checkers/registerCheckers.ml +++ b/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] ] diff --git a/infer/tests/codetoanalyze/cpp/threadsafety/Makefile b/infer/tests/codetoanalyze/cpp/threadsafety/Makefile new file mode 100644 index 000000000..f4740e465 --- /dev/null +++ b/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) diff --git a/infer/tests/codetoanalyze/cpp/threadsafety/basics.cpp b/infer/tests/codetoanalyze/cpp/threadsafety/basics.cpp new file mode 100644 index 000000000..2f0ab5bca --- /dev/null +++ b/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 + +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_; +}; +} diff --git a/infer/tests/codetoanalyze/cpp/threadsafety/issues.exp b/infer/tests/codetoanalyze/cpp/threadsafety/issues.exp new file mode 100644 index 000000000..13fa8f951 --- /dev/null +++ b/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, [,access to `not_guarded`,,access to `not_guarded`] +codetoanalyze/cpp/threadsafety/basics.cpp, basics::Basic_get4, 0, THREAD_SAFETY_VIOLATION, [,access to `suspiciously_read`,,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`]