From b4b54025bf2db8f48673b7a94c8e5507ab7c3807 Mon Sep 17 00:00:00 2001 From: Mehdi Bouaziz Date: Tue, 28 Aug 2018 01:36:40 -0700 Subject: [PATCH] Remove C++ mutex DOUBLE_LOCK checker Reviewed By: jeremydubreil Differential Revision: D9496910 fbshipit-source-id: 7a4138978 --- infer/models/cpp/src/mutex.cpp | 82 ------------------- infer/src/IR/Exceptions.ml | 10 +-- infer/src/IR/Exceptions.mli | 3 - infer/src/IR/Localise.ml | 14 ---- infer/src/IR/Localise.mli | 4 - infer/src/backend/errdesc.ml | 15 +--- infer/src/base/IssueType.ml | 2 - infer/src/base/IssueType.mli | 2 - infer/src/biabduction/Rearrange.ml | 2 - infer/src/biabduction/Tabulation.ml | 2 - .../tests/codetoanalyze/cpp/errors/issues.exp | 14 +--- .../cpp/errors/mutex/std_mutex.cpp | 6 +- .../errors/mutex/std_mutex_lock_profiling.cpp | 6 +- .../cpp/errors/mutex/timed_mutex.cpp | 4 +- 14 files changed, 14 insertions(+), 152 deletions(-) delete mode 100644 infer/models/cpp/src/mutex.cpp diff --git a/infer/models/cpp/src/mutex.cpp b/infer/models/cpp/src/mutex.cpp deleted file mode 100644 index 3a11ee3a2..000000000 --- a/infer/models/cpp/src/mutex.cpp +++ /dev/null @@ -1,82 +0,0 @@ -/* - * Copyright (c) 2017-present, Facebook, Inc. - * - * This source code is licensed under the MIT license found in the - * LICENSE file in the root directory of this source tree. - */ - -#pragma once - -#include -#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 __infer_mutex_model { - private: - int* null_if_locked = &__INFER_UNLOCKED; - - public: - constexpr __infer_mutex_model() noexcept; - ~__infer_mutex_model(); - __infer_mutex_model(const __infer_mutex_model&) = delete; - __infer_mutex_model& operator=(const __infer_mutex_model&) = 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; } -}; - -class mutex { - private: - __infer_mutex_model mutex_model; - - public: - void lock() { mutex_model.lock(); } - - bool try_lock() { return mutex_model.try_lock(); } - - void unlock() { mutex_model.unlock(); } -}; - -class timed_mutex { - private: - __infer_mutex_model mutex_model; - - public: - void lock() { mutex_model.lock(); } - - bool try_lock() { return mutex_model.try_lock(); } - - void unlock() { mutex_model.unlock(); } - - template - bool try_lock_for(const chrono::duration& rel_time) { - return mutex_model.try_lock(); - } - - template - bool try_lock_until(const chrono::time_point& abs_time) { - return mutex_model.try_lock(); - } -}; - -INFER_NAMESPACE_STD_END diff --git a/infer/src/IR/Exceptions.ml b/infer/src/IR/Exceptions.ml index 98852463e..d401d7d2f 100644 --- a/infer/src/IR/Exceptions.ml +++ b/infer/src/IR/Exceptions.ml @@ -72,8 +72,6 @@ exception Deallocation_mismatch of Localise.error_desc * L.ocaml_pos exception Divide_by_zero of Localise.error_desc * L.ocaml_pos -exception Double_lock of Localise.error_desc * L.ocaml_pos - exception Empty_vector_access of Localise.error_desc * L.ocaml_pos exception Eradicate of IssueType.t * Localise.error_desc @@ -301,13 +299,6 @@ let recognize_exception exn = ; visibility= Exn_user ; severity= Some Error ; category= Checker } - | Double_lock (desc, ocaml_pos) -> - { name= IssueType.double_lock - ; description= desc - ; ocaml_pos= Some ocaml_pos - ; visibility= Exn_user - ; severity= Some Error - ; category= Prover } | Eradicate (kind, desc) -> { name= kind ; description= desc @@ -607,6 +598,7 @@ let severity_string = function | Warning -> "WARNING" + (** pretty print an error *) let pp_err loc severity ex_name desc ocaml_pos_opt fmt () = let kind = severity_string (if equal_severity severity Info then Warning else severity) in diff --git a/infer/src/IR/Exceptions.mli b/infer/src/IR/Exceptions.mli index 67c3e7074..eee291597 100644 --- a/infer/src/IR/Exceptions.mli +++ b/infer/src/IR/Exceptions.mli @@ -69,8 +69,6 @@ exception Deallocate_static_memory of Localise.error_desc exception Deallocation_mismatch of Localise.error_desc * Logging.ocaml_pos -exception Double_lock of Localise.error_desc * Logging.ocaml_pos - exception Divide_by_zero of Localise.error_desc * Logging.ocaml_pos exception Field_not_null_checked of Localise.error_desc * Logging.ocaml_pos @@ -144,7 +142,6 @@ exception Use_after_free of Localise.error_desc * Logging.ocaml_pos exception Wrong_argument_number of Logging.ocaml_pos - val severity_string : severity -> string (** string describing an error kind *) diff --git a/infer/src/IR/Localise.ml b/infer/src/IR/Localise.ml index 1fadcc8d1..a44f78e8a 100644 --- a/infer/src/IR/Localise.ml +++ b/infer/src/IR/Localise.ml @@ -40,8 +40,6 @@ module Tags = struct (** Weak variable captured in a block that causes a warning *) let weak_captured_var_src = "weak_captured_var_src" - let double_lock = "double_lock" - let empty_vector_access = "empty_vector_access" let create () = ref [] @@ -354,16 +352,6 @@ let java_unchecked_exn_desc proc_name exn_name pre_str : error_desc = ; "whenever " ^ pre_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 pname_opt in - Tags.update 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 accessed_fld guarded_by_str loc = let line_info = at_line (Tags.create ()) loc in let accessed_fld_str = Typ.Fieldname.to_string accessed_fld in @@ -522,8 +510,6 @@ let is_parameter_not_null_checked_desc desc = has_tag desc Tags.parameter_not_nu let is_field_not_null_checked_desc desc = has_tag desc Tags.field_not_null_checked -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 (primitive_pname, called_pname, loc) = diff --git a/infer/src/IR/Localise.mli b/infer/src/IR/Localise.mli index c9b3462e2..f38325e2a 100644 --- a/infer/src/IR/Localise.mli +++ b/infer/src/IR/Localise.mli @@ -129,10 +129,6 @@ 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/errdesc.ml b/infer/src/backend/errdesc.ml index 65cdfc0f0..5a05351aa 100644 --- a/infer/src/backend/errdesc.ml +++ b/infer/src/backend/errdesc.ml @@ -16,11 +16,6 @@ module DExp = DecompiledExp let vector_matcher = QualifiedCppName.Match.of_fuzzy_qual_names ["std::vector"] -let mutex_matcher = - QualifiedCppName.Match.of_fuzzy_qual_names - ["std::__infer_mutex_model"; "std::mutex"; "std::timed_mutex"] - - let is_one_of_classes = QualifiedCppName.Match.match_qualifiers let is_method_of_objc_cpp_class pname matcher = @@ -32,8 +27,6 @@ let is_method_of_objc_cpp_class pname matcher = false -let is_mutex_method pname = is_method_of_objc_cpp_class pname mutex_matcher - let is_vector_method pname = is_method_of_objc_cpp_class pname vector_matcher let is_special_field matcher field_name_opt field = @@ -901,15 +894,11 @@ let create_dereference_desc proc_name tenv ?(use_buckets= false) ?(outermost_arr | _ -> desc ) | 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 + 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)) | Some (DExp.Ddot (dexp, fieldname)) -> - if is_special_field mutex_matcher (Some "null_if_locked") fieldname then - Localise.desc_double_lock None (DExp.to_string dexp) loc - else if + if is_special_field vector_matcher (Some "beginPtr") fieldname || is_special_field vector_matcher (Some "endPtr") fieldname then Localise.desc_empty_vector_access None (DExp.to_string dexp) loc diff --git a/infer/src/base/IssueType.ml b/infer/src/base/IssueType.ml index 82d1ea1d6..c53693fae 100644 --- a/infer/src/base/IssueType.ml +++ b/infer/src/base/IssueType.ml @@ -149,8 +149,6 @@ let deallocation_mismatch = from_string "DEALLOCATION_MISMATCH" let divide_by_zero = from_string ~enabled:false "DIVIDE_BY_ZERO" -let double_lock = from_string "DOUBLE_LOCK" - let do_not_report = from_string "DO_NOT_REPORT" let empty_vector_access = from_string "EMPTY_VECTOR_ACCESS" diff --git a/infer/src/base/IssueType.mli b/infer/src/base/IssueType.mli index e18705813..d212b49ff 100644 --- a/infer/src/base/IssueType.mli +++ b/infer/src/base/IssueType.mli @@ -104,8 +104,6 @@ val deallocation_mismatch : t val divide_by_zero : t -val double_lock : t - val do_not_report : t (** an issue type that should never be reported *) diff --git a/infer/src/biabduction/Rearrange.ml b/infer/src/biabduction/Rearrange.ml index 63e24bc3c..083aeccab 100644 --- a/infer/src/biabduction/Rearrange.ml +++ b/infer/src/biabduction/Rearrange.ml @@ -1634,8 +1634,6 @@ 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_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__)) ) ; diff --git a/infer/src/biabduction/Tabulation.ml b/infer/src/biabduction/Tabulation.ml index 6f6297e64..361bcc80b 100644 --- a/infer/src/biabduction/Tabulation.ml +++ b/infer/src/biabduction/Tabulation.ml @@ -1347,8 +1347,6 @@ 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_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__)) diff --git a/infer/tests/codetoanalyze/cpp/errors/issues.exp b/infer/tests/codetoanalyze/cpp/errors/issues.exp index dab383bfd..e49ae97b2 100644 --- a/infer/tests/codetoanalyze/cpp/errors/issues.exp +++ b/infer/tests/codetoanalyze/cpp/errors/issues.exp @@ -41,17 +41,9 @@ codetoanalyze/cpp/errors/models/pair.cpp, pair::deref_pair_null1_bad, 3, NULL_DE codetoanalyze/cpp/errors/models/pair.cpp, pair::deref_pair_null3_bad, 3, NULL_DEREFERENCE, B1, ERROR, [start of procedure pair::deref_pair_null3_bad(),start of procedure pair::pairOfZeroNull2(),return from a call to pair::pairOfZeroNull2] codetoanalyze/cpp/errors/models/swap.cpp, swap_null_bad, 4, NULL_DEREFERENCE, B1, ERROR, [start of procedure swap_null_bad()] codetoanalyze/cpp/errors/models/throw_wrapper.cpp, nothrow_if_null_bad, 4, NULL_DEREFERENCE, B1, ERROR, [start of procedure nothrow_if_null_bad(),start of procedure get_null(),return from a call to get_null,Taking true branch,start of procedure do_nothing(),return from a call to do_nothing] -codetoanalyze/cpp/errors/mutex/std_mutex.cpp, alarm1, 2, DOUBLE_LOCK, B2, ERROR, [start of procedure alarm1()] -codetoanalyze/cpp/errors/mutex/std_mutex.cpp, alarm2, 2, DOUBLE_LOCK, B2, ERROR, [start of procedure alarm2()] -codetoanalyze/cpp/errors/mutex/std_mutex.cpp, alarm2, 2, DOUBLE_LOCK, B5, ERROR, [start of procedure alarm2()] -codetoanalyze/cpp/errors/mutex/std_mutex.cpp, alarm3, 6, DOUBLE_LOCK, B1, ERROR, [start of procedure alarm3(),Skipping mutex: method has no implementation,Taking true branch,Taking true branch] -codetoanalyze/cpp/errors/mutex/std_mutex_lock_profiling.cpp, LockMapBucket_bad_usage3, 2, PRECONDITION_NOT_MET, no_bucket, WARNING, [start of procedure bad_usage3,start of procedure LpLockGuard,start of procedure lp_lock(),start of procedure detail::try_lock_impl(),Taking true branch,return from a call to detail::try_lock_impl,Switch condition is true. Entering switch case,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, no_bucket, WARNING, [start of procedure bad_usage1(),Skipping mutex: method has no implementation,start of procedure lp_lock(),start of procedure detail::try_lock_impl(),Taking true branch,return from a call to detail::try_lock_impl,Switch condition is true. Entering switch case,return from a call to lp_lock] -codetoanalyze/cpp/errors/mutex/std_mutex_lock_profiling.cpp, bad_usage2, 3, PRECONDITION_NOT_MET, no_bucket, WARNING, [start of procedure bad_usage2(),Skipping mutex: method has no implementation] -codetoanalyze/cpp/errors/mutex/std_mutex_lock_profiling.cpp, lp_lock, 7, DOUBLE_LOCK, B5, ERROR, [start of procedure lp_lock(),start of procedure detail::try_lock_impl(),Taking false branch,return from a call to detail::try_lock_impl,Switch condition is false. Skipping switch case,Switch condition is true. Entering switch case,start of procedure detail::lock_impl(),return from a call to detail::lock_impl] -codetoanalyze/cpp/errors/mutex/timed_mutex.cpp, alarm1, 2, DOUBLE_LOCK, B2, ERROR, [start of procedure alarm1()] -codetoanalyze/cpp/errors/mutex/timed_mutex.cpp, try_lock_bad, 2, DOUBLE_LOCK, B2, ERROR, [start of procedure try_lock_bad()] -codetoanalyze/cpp/errors/mutex/timed_mutex.cpp, try_lock_bad, 2, DOUBLE_LOCK, B5, ERROR, [start of procedure try_lock_bad()] +codetoanalyze/cpp/errors/mutex/std_mutex.cpp, ends_locked, 3, Cannot_star, no_bucket, ERROR, [start of procedure ends_locked(),Loop condition is true. Entering loop body,start of procedure ensure_unlocked(),start of procedure ensure_locked(),Skipping try_lock: method has no implementation,return from a call to ensure_locked,Skipping unlock: method has no implementation,return from a call to ensure_unlocked] +codetoanalyze/cpp/errors/mutex/std_mutex.cpp, starts_with_lock, 3, Cannot_star, no_bucket, ERROR, [start of procedure starts_with_lock(),Loop condition is true. Entering loop body,Skipping lock: method has no implementation] +codetoanalyze/cpp/errors/mutex/std_mutex_lock_profiling.cpp, lp_lock, 7, Cannot_star, no_bucket, ERROR, [start of procedure lp_lock(),start of procedure detail::try_lock_impl(),Taking false branch,return from a call to detail::try_lock_impl,Switch condition is false. Skipping switch case,Switch condition is true. Entering switch case] codetoanalyze/cpp/errors/npe/boxed_ptr.cpp, boxed_ptr::smart_ptr_null_field_deref, 2, NULL_DEREFERENCE, B5, ERROR, [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, B5, ERROR, [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, B5, ERROR, [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 index a890b6cb7..9eaafad69 100644 --- a/infer/tests/codetoanalyze/cpp/errors/mutex/std_mutex.cpp +++ b/infer/tests/codetoanalyze/cpp/errors/mutex/std_mutex.cpp @@ -6,12 +6,12 @@ */ #include -void alarm1(std::mutex& m) { +void alarm1_FN(std::mutex& m) { m.lock(); m.lock(); } -void alarm2(std::mutex& m) { +void alarm2_FN(std::mutex& m) { m.try_lock(); m.lock(); } @@ -43,7 +43,7 @@ void starts_with_lock(std::mutex& m) { } } -void alarm3() { +void alarm3_FN() { std::mutex m; ends_locked(m); starts_with_lock(m); 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 index 7727e417d..1ae8bc77b 100644 --- a/infer/tests/codetoanalyze/cpp/errors/mutex/std_mutex_lock_profiling.cpp +++ b/infer/tests/codetoanalyze/cpp/errors/mutex/std_mutex_lock_profiling.cpp @@ -46,13 +46,13 @@ void good_usage() { lp_lock(&m); } -void bad_usage1() { +void bad_usage1_FN() { std::mutex m; lp_lock(&m); lp_lock(&m); } -void bad_usage2() { +void bad_usage2_FN() { std::mutex m; m.lock(); lp_lock(&m); @@ -71,7 +71,7 @@ struct LockMapBucket { public: void good_usage2() { LpLockGuard lock(bucketLock); } - void bad_usage3() { + void bad_usage3_FN() { LpLockGuard lock(bucketLock); this->good_usage2(); } diff --git a/infer/tests/codetoanalyze/cpp/errors/mutex/timed_mutex.cpp b/infer/tests/codetoanalyze/cpp/errors/mutex/timed_mutex.cpp index a0795ef57..255169cf8 100644 --- a/infer/tests/codetoanalyze/cpp/errors/mutex/timed_mutex.cpp +++ b/infer/tests/codetoanalyze/cpp/errors/mutex/timed_mutex.cpp @@ -7,12 +7,12 @@ #include #include -void alarm1(std::timed_mutex& m) { +void alarm1_FN(std::timed_mutex& m) { m.lock(); m.lock(); } -void try_lock_bad(std::timed_mutex& m) { +void try_lock_bad_FN(std::timed_mutex& m) { m.try_lock(); m.lock(); }