[infer] std::mutex model to detect simple double lock

Reviewed By: jvillard

Differential Revision: D4705978

fbshipit-source-id: a635fb8

infer/models/cpp/src/Makefile

@@ -2,7 +2,7 @@ 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)
 

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 <infer_model/infer_traits.h>
+#include <infer_model/portability.h>
+
+INFER_NAMESPACE_STD_BEGIN
+
+int __INFER_UNLOCKED = 0;
+
+template <class T>
+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

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) ->

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

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
+  let problem_str = add_by_call_to_opt _problem_str tags proc_name_opt in
-    | Some proc_name ->
-        _problem_str ^ " " ^ by_call_to tags proc_name
-    | None -> _problem_str 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) =

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

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,

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, _ ))
+      | Some (DExp.Dretcall (Dconst (Cfun pname), this_dexp :: _, loc, _ )) ->
-        when is_vector_method pname ->
+          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
-      | Some (DExp.Darrow (dexp, fieldname))
+          else
-        when is_special_field [vector_class] (Some "beginPtr") fieldname ->
+            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

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;

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) ->

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) \

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<mutex>(),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<mutex>,return from a call to LpLockGuard<mutex>_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<mutex>(),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<mutex>]
+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<mutex>, 7, DOUBLE_LOCK, [start of procedure lp_lock<mutex>(),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]

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 <mutex>
+
+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();
+  }
+}

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 <mutex>
+
+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 <typename T>
+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 <typename T>
+class LpLockGuard {
+ public:
+  LpLockGuard(T& lock)
+      : lock_(lock) {
+    lp_lock(&lock_);
+  }
+
+ private:
+  T& lock_;
+};
+
+struct LockMapBucket {
+ public:
+  void good_usage2() {
+    LpLockGuard<std::mutex> lock(bucketLock);
+  }
+
+  void bad_usage3() {
+    LpLockGuard<std::mutex> lock(bucketLock);
+    this->good_usage2();
+  }
+
+ private:
+  std::mutex bucketLock; // Lock protecting against concurrent access
+};