From f65ac4f09432a50ca88d2ea743edf04373f35814 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Tue, 21 Mar 2017 12:40:33 -0700 Subject: [PATCH] [infer] std::mutex model to detect simple double lock Reviewed By: jvillard Differential Revision: D4705978 fbshipit-source-id: a635fb8 --- infer/models/cpp/src/Makefile | 6 +- infer/models/cpp/src/mutex.cpp | 51 +++++++++++ infer/src/IR/Exceptions.ml | 4 + infer/src/IR/Exceptions.mli | 1 + infer/src/IR/Localise.ml | 24 ++++- infer/src/IR/Localise.mli | 5 ++ infer/src/backend/InferPrint.re | 1 + infer/src/backend/errdesc.ml | 24 +++-- infer/src/backend/rearrange.ml | 4 +- infer/src/backend/tabulation.ml | 4 +- infer/tests/codetoanalyze/cpp/errors/Makefile | 1 + .../tests/codetoanalyze/cpp/errors/issues.exp | 8 ++ .../cpp/errors/mutex/std_mutex.cpp | 74 ++++++++++++++++ .../errors/mutex/std_mutex_lock_profiling.cpp | 88 +++++++++++++++++++ 14 files changed, 280 insertions(+), 15 deletions(-) create mode 100644 infer/models/cpp/src/mutex.cpp create mode 100644 infer/tests/codetoanalyze/cpp/errors/mutex/std_mutex.cpp create mode 100644 infer/tests/codetoanalyze/cpp/errors/mutex/std_mutex_lock_profiling.cpp diff --git a/infer/models/cpp/src/Makefile b/infer/models/cpp/src/Makefile index 0a324bf2c..f5b7a14b6 100644 --- a/infer/models/cpp/src/Makefile +++ b/infer/models/cpp/src/Makefile @@ -2,12 +2,12 @@ SOURCES=$(wildcard *.cpp) CSOURCES=$(wildcard c_src/*.c) OBJECTS=$(patsubst %.c,%_cxx.o, $(CSOURCES)) $(patsubst %.cpp,%.o, $(SOURCES)) CXX=clang++ -CXXFLAGS=-c -w -std=c++11 +CXXFLAGS=-c -w -std=c++11 -isystem../include -all: $(OBJECTS) +all: $(OBJECTS) clean: - @rm -rf $(OBJECTS) + @rm -rf $(OBJECTS) %.o: %.cpp $(CXX) $(CXXFLAGS) $< -o $@ diff --git a/infer/models/cpp/src/mutex.cpp b/infer/models/cpp/src/mutex.cpp new file mode 100644 index 000000000..26c2bdd33 --- /dev/null +++ b/infer/models/cpp/src/mutex.cpp @@ -0,0 +1,51 @@ +/* + * 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. + */ + +#pragma once + +#include +#include + +INFER_NAMESPACE_STD_BEGIN + +int __INFER_UNLOCKED = 0; + +template +void __infer_mutex_deref_first_arg(T* ptr) INFER_MODEL_AS_DEREF_FIRST_ARG; + +class mutex { + private: + int* null_if_locked = &__INFER_UNLOCKED; + + public: + constexpr mutex() noexcept; + ~mutex(); + mutex(const mutex&) = delete; + mutex& operator=(const mutex&) = delete; + + void lock() { + __infer_mutex_deref_first_arg(null_if_locked); // HACK + null_if_locked = nullptr; + } + + bool try_lock() { + if (null_if_locked) { + null_if_locked = nullptr; + return true; + } else { + return false; + } + } + + void unlock() { + null_if_locked = &__INFER_UNLOCKED; + } +}; + +INFER_NAMESPACE_STD_END diff --git a/infer/src/IR/Exceptions.ml b/infer/src/IR/Exceptions.ml index 1879ed35e..2a8b85b61 100644 --- a/infer/src/IR/Exceptions.ml +++ b/infer/src/IR/Exceptions.ml @@ -65,6 +65,7 @@ exception Deallocate_stack_variable of Localise.error_desc exception Deallocate_static_memory of Localise.error_desc exception Deallocation_mismatch of Localise.error_desc * L.ml_loc exception Divide_by_zero of Localise.error_desc * L.ml_loc +exception Double_lock of Localise.error_desc * L.ml_loc exception Empty_vector_access of Localise.error_desc * L.ml_loc exception Eradicate of string * Localise.error_desc exception Field_not_null_checked of Localise.error_desc * L.ml_loc @@ -175,6 +176,9 @@ let recognize_exception exn = | Divide_by_zero (desc, ml_loc) -> (Localise.divide_by_zero, desc, Some ml_loc, Exn_user, High, Some Kerror, Checker) + | Double_lock (desc, ml_loc) -> + (Localise.double_lock, + desc, Some ml_loc, Exn_user, High, Some Kerror, Prover) | Eradicate (kind_s, desc) -> (Localise.from_string kind_s, desc, None, Exn_user, High, None, Prover) | Empty_vector_access (desc, ml_loc) -> diff --git a/infer/src/IR/Exceptions.mli b/infer/src/IR/Exceptions.mli index 193628a6e..b5ece3491 100644 --- a/infer/src/IR/Exceptions.mli +++ b/infer/src/IR/Exceptions.mli @@ -59,6 +59,7 @@ exception Dangling_pointer_dereference of exception Deallocate_stack_variable of Localise.error_desc exception Deallocate_static_memory of Localise.error_desc exception Deallocation_mismatch of Localise.error_desc * Logging.ml_loc +exception Double_lock of Localise.error_desc * Logging.ml_loc exception Divide_by_zero of Localise.error_desc * Logging.ml_loc exception Field_not_null_checked of Localise.error_desc * Logging.ml_loc exception Empty_vector_access of Localise.error_desc * Logging.ml_loc diff --git a/infer/src/IR/Localise.ml b/infer/src/IR/Localise.ml index 50df5596c..19b983a2f 100644 --- a/infer/src/IR/Localise.ml +++ b/infer/src/IR/Localise.ml @@ -62,6 +62,7 @@ let deallocate_stack_variable = from_string "DEALLOCATE_STACK_VARIABLE" let deallocate_static_memory = from_string "DEALLOCATE_STATIC_MEMORY" let deallocation_mismatch = from_string "DEALLOCATION_MISMATCH" let divide_by_zero = from_string "DIVIDE_BY_ZERO" +let double_lock = from_string "DOUBLE_LOCK" let empty_vector_access = from_string "EMPTY_VECTOR_ACCESS" let eradicate_condition_redundant = from_string "ERADICATE_CONDITION_REDUNDANT" ~hum:"Condition Redundant" @@ -194,6 +195,7 @@ module Tags = struct let field_not_null_checked = "field_not_null_checked" (* describes a NPE that comes from field not nullable *) let nullable_src = "nullable_src" (* @Nullable-annoted field/param/retval that causes a warning *) let weak_captured_var_src = "weak_captured_var_src" (* Weak variable captured in a block that causes a warning *) + let double_lock = "double_lock" let empty_vector_access = "empty_vector_access" let create () = ref [] let add tags tag value = tags := (tag, value) :: !tags @@ -301,6 +303,12 @@ let by_call_to tags proc_name = let by_call_to_ra tags ra = "by " ^ call_to_at_line tags ra.PredSymb.ra_pname ra.PredSymb.ra_loc +let add_by_call_to_opt problem_str tags proc_name_opt = + match proc_name_opt with + | Some proc_name -> + problem_str ^ " " ^ by_call_to tags proc_name + | None -> problem_str + let rec format_typ = function | Typ.Tptr (typ, _) when Config.curr_language_is Config.Java -> format_typ typ @@ -337,10 +345,7 @@ let pointer_or_object () = if Config.curr_language_is Config.Java then "object" else "pointer" let _deref_str_null proc_name_opt _problem_str tags = - let problem_str = match proc_name_opt with - | Some proc_name -> - _problem_str ^ " " ^ by_call_to tags proc_name - | None -> _problem_str in + let problem_str = add_by_call_to_opt _problem_str tags proc_name_opt in { tags = tags; value_pre = Some (pointer_or_object ()); value_post = None; @@ -497,6 +502,15 @@ let desc_context_leak pname context_typ fieldname leak_path : error_desc = "Context " ^ context_str ^ " may leak during method " ^ pname_str ^ ":\n" in { no_desc with descriptions = [preamble ^ MF.code_to_string (leak_root ^ path_str)] } +let desc_double_lock pname_opt object_str loc = + let mutex_str = Format.sprintf "Mutex %s" object_str in + let tags = Tags.create () in + let msg = "could be locked and is locked again" in + let msg = add_by_call_to_opt msg tags pname_opt in + Tags.add tags Tags.double_lock object_str; + let descriptions = [mutex_str; msg; at_line tags loc] in + { no_desc with descriptions; tags = !tags } + let desc_unsafe_guarded_by_access pname accessed_fld guarded_by_str loc = let line_info = at_line (Tags.create ()) loc in let accessed_fld_str = Fieldname.to_string accessed_fld in @@ -625,6 +639,8 @@ let is_parameter_field_not_null_checked_desc desc = is_parameter_not_null_checked_desc desc || is_field_not_null_checked_desc desc +let is_double_lock_desc desc = has_tag desc Tags.double_lock + let desc_allocation_mismatch alloc dealloc = let tags = Tags.create () in let using is_alloc (primitive_pname, called_pname, loc) = diff --git a/infer/src/IR/Localise.mli b/infer/src/IR/Localise.mli index 2d9882d2c..e352e34dc 100644 --- a/infer/src/IR/Localise.mli +++ b/infer/src/IR/Localise.mli @@ -54,6 +54,7 @@ val deallocate_stack_variable : t val deallocate_static_memory : t val deallocation_mismatch : t val divide_by_zero : t +val double_lock : t val empty_vector_access : t val eradicate_condition_redundant : t val eradicate_condition_redundant_nonnull : t @@ -235,6 +236,10 @@ val desc_deallocate_static_memory : string -> Typ.Procname.t -> Location.t -> er val desc_divide_by_zero : string -> Location.t -> error_desc +val desc_double_lock : Typ.Procname.t option -> string -> Location.t -> error_desc + +val is_double_lock_desc : error_desc -> bool + val desc_empty_vector_access : Typ.Procname.t option -> string -> Location.t -> error_desc val is_empty_vector_access_desc : error_desc -> bool diff --git a/infer/src/backend/InferPrint.re b/infer/src/backend/InferPrint.re index 874c3a5cb..31b6f8ec0 100644 --- a/infer/src/backend/InferPrint.re +++ b/infer/src/backend/InferPrint.re @@ -340,6 +340,7 @@ let should_report (issue_kind: Exceptions.err_kind) issue_type error_desc eclass Localise.[ Localise.from_string Config.default_failure_name, context_leak, + double_lock, empty_vector_access, memory_leak, quandary_taint_error, diff --git a/infer/src/backend/errdesc.ml b/infer/src/backend/errdesc.ml index e57f8a805..9e0b3ca8e 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -16,6 +16,7 @@ module L = Logging module F = Format module DExp = DecompiledExp +let mutex_class = ["std"; "mutex"] let vector_class = ["std"; "vector"] let is_one_of_classes class_name classes = @@ -31,6 +32,9 @@ let is_method_of_objc_cpp_class pname classes = is_one_of_classes class_name classes | _ -> false +let is_mutex_method pname = + is_method_of_objc_cpp_class pname [mutex_class] + let is_vector_method pname = is_method_of_objc_cpp_class pname [vector_class] @@ -830,12 +834,20 @@ let create_dereference_desc tenv Localise.parameter_field_not_null_checked_desc desc vfs | _ -> desc) - | Some (DExp.Dretcall (Dconst (Cfun pname), this_dexp :: _, loc, _ )) - when is_vector_method pname -> - Localise.desc_empty_vector_access (Some pname) (DExp.to_string this_dexp) loc - | Some (DExp.Darrow (dexp, fieldname)) - when is_special_field [vector_class] (Some "beginPtr") fieldname -> - Localise.desc_empty_vector_access None (DExp.to_string dexp) loc + | Some (DExp.Dretcall (Dconst (Cfun pname), this_dexp :: _, loc, _ )) -> + if is_mutex_method pname then + Localise.desc_double_lock (Some pname) (DExp.to_string this_dexp) loc + else if is_vector_method pname then + Localise.desc_empty_vector_access (Some pname) (DExp.to_string this_dexp) loc + else + desc + | Some (DExp.Darrow (dexp, fieldname)) -> + if is_special_field [mutex_class] (Some "null_if_locked") fieldname then + Localise.desc_double_lock None (DExp.to_string dexp) loc + else if is_special_field [vector_class] (Some "beginPtr") fieldname then + Localise.desc_empty_vector_access None (DExp.to_string dexp) loc + else + desc | _ -> desc else desc in if use_buckets then Buckets.classify_access desc access_opt' de_opt is_nullable diff --git a/infer/src/backend/rearrange.ml b/infer/src/backend/rearrange.ml index dfc2ca87f..6cc3de71b 100644 --- a/infer/src/backend/rearrange.ml +++ b/infer/src/backend/rearrange.ml @@ -1400,7 +1400,9 @@ let check_dereference_error tenv pdesc (prop : Prop.normal Prop.t) lexp loc = raise (Exceptions.Parameter_not_null_checked (err_desc, __POS__)) else if Localise.is_field_not_null_checked_desc err_desc then raise (Exceptions.Field_not_null_checked (err_desc, __POS__)) - else if (Localise.is_empty_vector_access_desc err_desc) then + else if Localise.is_double_lock_desc err_desc then + raise (Exceptions.Double_lock (err_desc, __POS__)) + else if Localise.is_empty_vector_access_desc err_desc then raise (Exceptions.Empty_vector_access (err_desc, __POS__)) else raise (Exceptions.Null_dereference (err_desc, __POS__)) end; diff --git a/infer/src/backend/tabulation.ml b/infer/src/backend/tabulation.ml index 42a84c0cb..7c0da830e 100644 --- a/infer/src/backend/tabulation.ml +++ b/infer/src/backend/tabulation.ml @@ -1188,7 +1188,9 @@ let exe_call_postprocess tenv ret_id trace_call callee_pname callee_attrs loc re raise (Exceptions.Parameter_not_null_checked (desc, __POS__)) else if Localise.is_field_not_null_checked_desc desc then raise (Exceptions.Field_not_null_checked (desc, __POS__)) - else if (Localise.is_empty_vector_access_desc desc) then + else if Localise.is_double_lock_desc desc then + raise (Exceptions.Double_lock (desc, __POS__)) + else if Localise.is_empty_vector_access_desc desc then raise (Exceptions.Empty_vector_access (desc, __POS__)) else raise (Exceptions.Null_dereference (desc, __POS__)) | Dereference_error (Deref_freed _, desc, path_opt) -> diff --git a/infer/tests/codetoanalyze/cpp/errors/Makefile b/infer/tests/codetoanalyze/cpp/errors/Makefile index 475c625c5..1ddb53328 100644 --- a/infer/tests/codetoanalyze/cpp/errors/Makefile +++ b/infer/tests/codetoanalyze/cpp/errors/Makefile @@ -19,6 +19,7 @@ SOURCES = \ include_header/include_templ.cpp \ $(wildcard memory_leaks/*.cpp) \ $(wildcard models/*.cpp) \ + $(wildcard mutex/*.cpp) \ $(wildcard npe/*.cpp) \ $(wildcard numeric/*.cpp) \ $(wildcard overwrite_attribute/*.cpp) \ diff --git a/infer/tests/codetoanalyze/cpp/errors/issues.exp b/infer/tests/codetoanalyze/cpp/errors/issues.exp index 59c82d438..4eb9d2963 100644 --- a/infer/tests/codetoanalyze/cpp/errors/issues.exp +++ b/infer/tests/codetoanalyze/cpp/errors/issues.exp @@ -18,6 +18,14 @@ codetoanalyze/cpp/errors/memory_leaks/object_leak.cpp, object_leak, 0, MEMORY_LE codetoanalyze/cpp/errors/memory_leaks/raii_malloc.cpp, memory_leak, 0, MEMORY_LEAK, [start of procedure memory_leak()] codetoanalyze/cpp/errors/models/move.cpp, move::div0_moved_from, 3, DIVIDE_BY_ZERO, [start of procedure move::div0_moved_from(),start of procedure X,return from a call to move::X_X,start of procedure X,return from a call to move::X_X] codetoanalyze/cpp/errors/models/move.cpp, move::div0_moved_to, 3, DIVIDE_BY_ZERO, [start of procedure move::div0_moved_to(),start of procedure X,return from a call to move::X_X,start of procedure X,return from a call to move::X_X] +codetoanalyze/cpp/errors/mutex/std_mutex.cpp, alarm1, 2, DOUBLE_LOCK, [start of procedure alarm1()] +codetoanalyze/cpp/errors/mutex/std_mutex.cpp, alarm2, 2, DOUBLE_LOCK, [start of procedure alarm2()] +codetoanalyze/cpp/errors/mutex/std_mutex.cpp, alarm2, 2, DOUBLE_LOCK, [start of procedure alarm2()] +codetoanalyze/cpp/errors/mutex/std_mutex.cpp, alarm3, 6, DOUBLE_LOCK, [start of procedure alarm3(),Condition is true,Condition is true] +codetoanalyze/cpp/errors/mutex/std_mutex_lock_profiling.cpp, LockMapBucket_bad_usage3, 2, PRECONDITION_NOT_MET, [start of procedure bad_usage3,start of procedure LpLockGuard,start of procedure lp_lock(),start of procedure detail::try_lock_impl(),Condition is true,return from a call to detail::try_lock_impl,Condition is true,return from a call to lp_lock,return from a call to LpLockGuard_LpLockGuard] +codetoanalyze/cpp/errors/mutex/std_mutex_lock_profiling.cpp, bad_usage1, 3, PRECONDITION_NOT_MET, [start of procedure bad_usage1(),start of procedure lp_lock(),start of procedure detail::try_lock_impl(),Condition is true,return from a call to detail::try_lock_impl,Condition is true,return from a call to lp_lock] +codetoanalyze/cpp/errors/mutex/std_mutex_lock_profiling.cpp, bad_usage2, 3, PRECONDITION_NOT_MET, [start of procedure bad_usage2()] +codetoanalyze/cpp/errors/mutex/std_mutex_lock_profiling.cpp, lp_lock, 7, DOUBLE_LOCK, [start of procedure lp_lock(),start of procedure detail::try_lock_impl(),Condition is false,return from a call to detail::try_lock_impl,Condition is false,Condition is true,start of procedure detail::lock_impl(),return from a call to detail::lock_impl] codetoanalyze/cpp/errors/npe/boxed_ptr.cpp, boxed_ptr::smart_ptr_null_field_deref, 2, NULL_DEREFERENCE, [start of procedure boxed_ptr::smart_ptr_null_field_deref(),start of procedure SmartPtr,return from a call to boxed_ptr::SmartPtr_SmartPtr,start of procedure get,return from a call to boxed_ptr::SmartPtr_get] codetoanalyze/cpp/errors/npe/boxed_ptr.cpp, boxed_ptr::smart_ptr_null_method_deref, 2, NULL_DEREFERENCE, [start of procedure boxed_ptr::smart_ptr_null_method_deref(),start of procedure SmartPtr,return from a call to boxed_ptr::SmartPtr_SmartPtr,start of procedure get,return from a call to boxed_ptr::SmartPtr_get] codetoanalyze/cpp/errors/npe/boxed_ptr.cpp, boxed_ptr::smart_ptr_null_method_deref2, 2, NULL_DEREFERENCE, [start of procedure boxed_ptr::smart_ptr_null_method_deref2(),start of procedure SmartPtr,return from a call to boxed_ptr::SmartPtr_SmartPtr,start of procedure get,return from a call to boxed_ptr::SmartPtr_get] diff --git a/infer/tests/codetoanalyze/cpp/errors/mutex/std_mutex.cpp b/infer/tests/codetoanalyze/cpp/errors/mutex/std_mutex.cpp new file mode 100644 index 000000000..491cd92d2 --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/errors/mutex/std_mutex.cpp @@ -0,0 +1,74 @@ +/* + * 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 + +void alarm1(std::mutex& m) { + m.lock(); + m.lock(); +} + +void alarm2(std::mutex& m) { + m.try_lock(); + m.lock(); +} + +void no_alarm1(std::mutex& m) { + for (int i = 0; i < 999999; i++) { + m.try_lock(); + } +} + +void ensure_locked(std::mutex& m) { + m.try_lock(); +} + +void ensure_unlocked(std::mutex& m) { + ensure_locked(m); + m.unlock(); +} + +void ends_locked(std::mutex& m) { + for (int i = 0; i < 999999; i++) { + ensure_unlocked(m); + ensure_locked(m); + } +} + +void starts_with_lock(std::mutex& m) { + for (int i = 0; i < 999999; i++) { + m.lock(); + ensure_unlocked(m); + } +} + +void alarm3() { + std::mutex m; + ends_locked(m); + starts_with_lock(m); +} + +void no_alarm3(bool b) { + std::mutex m; + if (b) { + m.lock(); + } + if (b) { + m.unlock(); + } +} + +void alarm3(bool b) { + std::mutex m; + if (b) { + m.lock(); + } + if (b) { + m.lock(); + } +} diff --git a/infer/tests/codetoanalyze/cpp/errors/mutex/std_mutex_lock_profiling.cpp b/infer/tests/codetoanalyze/cpp/errors/mutex/std_mutex_lock_profiling.cpp new file mode 100644 index 000000000..3379a841b --- /dev/null +++ b/infer/tests/codetoanalyze/cpp/errors/mutex/std_mutex_lock_profiling.cpp @@ -0,0 +1,88 @@ +/* + * 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 detail { + +inline int lock_impl(std::mutex* lock) { + lock->lock(); + return 0; +} + +inline int try_lock_impl(std::mutex* lock) { + if (lock->try_lock()) { + return 0; + } + return EBUSY; +} + +} + +template +int lp_lock(T* lock) { + int rv = detail::try_lock_impl(lock); + + switch (rv) { + case 0: + return 0; + case EBUSY: { + rv = detail::lock_impl(lock); + if (rv == 0) { + return 0; + } + /* fallthrough */ + } + default: + return rv; + } +} + +void good_usage() { + std::mutex m; + lp_lock(&m); +} + +void bad_usage1() { + std::mutex m; + lp_lock(&m); + lp_lock(&m); +} + +void bad_usage2() { + std::mutex m; + m.lock(); + lp_lock(&m); +} + +template +class LpLockGuard { + public: + LpLockGuard(T& lock) + : lock_(lock) { + lp_lock(&lock_); + } + + private: + T& lock_; +}; + +struct LockMapBucket { + public: + void good_usage2() { + LpLockGuard lock(bucketLock); + } + + void bad_usage3() { + LpLockGuard lock(bucketLock); + this->good_usage2(); + } + + private: + std::mutex bucketLock; // Lock protecting against concurrent access +};