[infer] More mutex models

Reviewed By: jvillard

Differential Revision: D4818713

fbshipit-source-id: eb11909

infer/models/c/src/infer_builtins.h

@@ -63,6 +63,15 @@ clock_t __infer_nondet_clock_t();
   if (cond)                           \
     while (1)
 
+#ifdef NO_INFER_FAIL
+#define INFER_EXCLUDE_CONDITION_MSG(cond, msg) INFER_EXCLUDE_CONDITION(cond)
+#else
+void __infer_fail(char*);
+#define INFER_EXCLUDE_CONDITION_MSG(cond, msg) \
+  if (cond)                                    \
+    __infer_fail(msg)
+#endif
+
 // builtin: force arr to be an array
 extern void __require_allocated_array(const void* arr);
 

infer/models/c/src/libc_basic.c

@@ -52,6 +52,7 @@
 #endif
 
 #include <dirent.h>
+#include <errno.h>
 #include <pwd.h>
 #include <pthread.h>
 #include <sys/shm.h>
@@ -87,11 +88,15 @@ struct __dirstream {
 // modelling of errno
 // errno expands to different function calls on mac or other systems
 // the function call returns the address of a global variable called "errno"
+#ifdef errno
+// errno may be defined as a macro to be a per-thread variable
+#undef errno
+#endif
 extern int errno;
 #ifdef __APPLE__
 #define __ERRNO_FUN_NAME __error
 #else
-#define __ERRNO_FUN_NAME __errno_location
+#define __ERRNO_FUN_NAME() __errno_location(void) __THROW __attribute__ ((__const__))
 #endif
 int* __ERRNO_FUN_NAME() { return &errno; }
 
@@ -1458,9 +1463,25 @@ int munmap(void* addr, size_t len) {
   return ret;
 }
 
+/*
+  pthread_mutex_t model:
+  locked = 0 if unlocked, non-zero if locked
+  initialized = 1 if initialized, non-one otherwise
+*/
+typedef struct {
+  int locked;
+  int initialized;
+} __infer_model_pthread_mutex_t;
+
 // returns a nondeterministc value
 int pthread_mutex_destroy(pthread_mutex_t* mutex) {
   INFER_EXCLUDE_CONDITION(mutex == 0);
+  __infer_model_pthread_mutex_t* model = (__infer_model_pthread_mutex_t*)mutex;
+  INFER_EXCLUDE_CONDITION_MSG(model->initialized != 1,
+                              "DESTROYING_UNINITIALIZED_MUTEX");
+  INFER_EXCLUDE_CONDITION_MSG(model->locked != 0,
+                              "DESTROYING_LOCKED_MUTEX");
+  model->initialized = -1;
   return __infer_nondet_int();
 }
 
@@ -1468,24 +1489,53 @@ int pthread_mutex_destroy(pthread_mutex_t* mutex) {
 int pthread_mutex_init(pthread_mutex_t* __restrict mutex,
                        const pthread_mutexattr_t* __restrict attr) {
   INFER_EXCLUDE_CONDITION(mutex == 0);
-  return __infer_nondet_int();
+  __infer_model_pthread_mutex_t* model = (__infer_model_pthread_mutex_t*)mutex;
+  INFER_EXCLUDE_CONDITION(model->initialized == 1);
+  int ret = __infer_nondet_int();
+  if (!ret) {
+    model->initialized = 1;
+    model->locked = 0;
+  }
+  return ret;
 }
 
 // returns a nondeterministc value
 int pthread_mutex_lock(pthread_mutex_t* mutex) {
   INFER_EXCLUDE_CONDITION(mutex == 0);
-  return __infer_nondet_int();
+  __infer_model_pthread_mutex_t* model = (__infer_model_pthread_mutex_t*)mutex;
+  INFER_EXCLUDE_CONDITION_MSG(model->initialized != 1,
+                              "LOCKING_UNINITIALIZED_MUTEX");
+  INFER_EXCLUDE_CONDITION_MSG(model->locked != 0,
+                              "LOCKING_ALREADY_LOCKED_MUTEX");
+  int ret = __infer_nondet_int();
+  if (!ret) {
+    model->locked = 1;
+  }
+  return ret;
 }
 
 // returns a nondeterministc value
 int pthread_mutex_trylock(pthread_mutex_t* mutex) {
   INFER_EXCLUDE_CONDITION(mutex == 0);
+  __infer_model_pthread_mutex_t* model = (__infer_model_pthread_mutex_t*)mutex;
+  INFER_EXCLUDE_CONDITION_MSG(model->initialized != 1,
+                              "TRYLOCKING_UNINITIALIZED_MUTEX");
+  if (model->locked) {
+    return EBUSY;
+  }
+  model->locked = 1;
   return __infer_nondet_int();
 }
 
 // returns a nondeterministc value
 int pthread_mutex_unlock(pthread_mutex_t* mutex) {
   INFER_EXCLUDE_CONDITION(mutex == 0);
+  __infer_model_pthread_mutex_t* model = (__infer_model_pthread_mutex_t*)mutex;
+  INFER_EXCLUDE_CONDITION_MSG(model->initialized != 1,
+                              "UNLOCKING_UNINITIALIZED_MUTEX");
+  INFER_EXCLUDE_CONDITION_MSG(model->locked == 0,
+                              "UNLOCKING_UNLOCKED_MUTEX");
+  model->locked = 0;
   return __infer_nondet_int();
 }
 
@@ -1515,6 +1565,54 @@ int pthread_mutexattr_gettype(const pthread_mutexattr_t* attr, int* type) {
   return __infer_nondet_int();
 }
 
+/*
+  pthread_spinlock_t model:
+  locked: 0 if unlocked, non-zero if locked
+*/
+typedef struct {
+  int locked;
+} __infer_model_pthread_spinlock_t;
+
+#ifdef __APPLE__
+typedef __infer_model_pthread_spinlock_t pthread_spinlock_t;
+#endif
+
+int pthread_spin_destroy(pthread_spinlock_t* lock) {
+  __infer_model_pthread_spinlock_t* model = (__infer_model_pthread_spinlock_t*)lock;
+  INFER_EXCLUDE_CONDITION_MSG(model->locked != 0, "DESTROYING_LOCKED_SPINLOCK");
+  return 0;
+}
+
+int pthread_spin_init(pthread_spinlock_t* lock, int pshared) {
+  __infer_model_pthread_spinlock_t* model = (__infer_model_pthread_spinlock_t*)lock;
+  model->locked = 0;
+  return 0;
+}
+
+int pthread_spin_lock(pthread_spinlock_t* lock) {
+  __infer_model_pthread_spinlock_t* model = (__infer_model_pthread_spinlock_t*)lock;
+  INFER_EXCLUDE_CONDITION_MSG(model->locked != 0, "LOCKING_ALREADY_LOCKED_SPINLOCK");
+  model->locked = 1;
+  return 0;
+}
+
+int pthread_spin_trylock(pthread_spinlock_t* lock) {
+  __infer_model_pthread_spinlock_t* model = (__infer_model_pthread_spinlock_t*)lock;
+  if (model->locked) {
+    return EBUSY;
+  } else {
+    model->locked = 1;
+    return 0;
+  }
+}
+
+int pthread_spin_unlock(pthread_spinlock_t* lock) {
+  __infer_model_pthread_spinlock_t* model = (__infer_model_pthread_spinlock_t*)lock;
+  INFER_EXCLUDE_CONDITION_MSG(model->locked == 0, "UNLOCKING_UNLOCKED_SPINLOCK");
+  model->locked = 0;
+  return 0;
+}
+
 // return a positive non-deterministic number or -1.
 // requires stream to be allocated
 int fileno(FILE* stream) {

infer/models/cpp/src/mutex.cpp

@@ -9,6 +9,7 @@
 
 #pragma once
 
+#include <chrono>
 #include <infer_model/infer_traits.h>
 #include <infer_model/portability.h>
 
@@ -19,15 +20,15 @@ int __INFER_UNLOCKED = 0;
 template <class T>
 void __infer_mutex_deref_first_arg(T* ptr) INFER_MODEL_AS_DEREF_FIRST_ARG;
 
-class mutex {
+class __infer_mutex_model {
  private:
   int* null_if_locked = &__INFER_UNLOCKED;
 
  public:
-  constexpr mutex() noexcept;
-  ~mutex();
-  mutex(const mutex&) = delete;
-  mutex& operator=(const mutex&) = delete;
+  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
@@ -48,4 +49,38 @@ class mutex {
   }
 };
 
+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 <class Rep, class Period>
+  bool try_lock_for(const chrono::duration<Rep, Period>& rel_time) {
+    return mutex_model.try_lock();
+  }
+
+  template <class Clock, class Duration>
+  bool try_lock_until(const chrono::time_point<Clock, Duration>& abs_time) {
+    return mutex_model.try_lock();
+  }
+};
+
 INFER_NAMESPACE_STD_END

infer/src/backend/errdesc.ml

@@ -17,7 +17,11 @@ module F = Format
 module DExp = DecompiledExp
 
 let vector_matcher = QualifiedCppName.Match.of_fuzzy_qual_names ["std::vector"]
-let mutex_matcher = QualifiedCppName.Match.of_fuzzy_qual_names ["std::mutex"]
+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
 
@@ -839,7 +843,8 @@ let create_dereference_desc tenv
             Localise.desc_empty_vector_access (Some pname) (DExp.to_string this_dexp) loc
           else
             desc
-      | Some (DExp.Darrow (dexp, fieldname)) ->
+      | 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 is_special_field vector_matcher (Some "beginPtr") fieldname then

infer/tests/codetoanalyze/c/errors/issues.exp

@@ -36,6 +36,15 @@ codetoanalyze/c/errors/memory_leaks/test.c, common_realloc_leak, 3, MEMORY_LEAK
 codetoanalyze/c/errors/memory_leaks/test.c, conditional_last_instruction, 2, MEMORY_LEAK
 codetoanalyze/c/errors/memory_leaks/test.c, simple_leak, 2, MEMORY_LEAK
 codetoanalyze/c/errors/memory_leaks/test.c, uses_allocator, 3, MEMORY_LEAK
+codetoanalyze/c/errors/mutex/pthread_mutex.c, double_init_bad, 2, PRECONDITION_NOT_MET
+codetoanalyze/c/errors/mutex/pthread_mutex.c, double_lock_bad2, 4, LOCKING_ALREADY_LOCKED_MUTEX
+codetoanalyze/c/errors/mutex/pthread_mutex.c, double_lock_bad2, 4, LOCKING_UNINITIALIZED_MUTEX
+codetoanalyze/c/errors/mutex/pthread_mutex.c, double_lock_uninit_bad, 3, LOCKING_ALREADY_LOCKED_MUTEX
+codetoanalyze/c/errors/mutex/pthread_mutex.c, double_lock_uninit_bad, 3, LOCKING_UNINITIALIZED_MUTEX
+codetoanalyze/c/errors/mutex/pthread_mutex.c, double_unlock_bad, 3, UNLOCKING_UNLOCKED_MUTEX
+codetoanalyze/c/errors/mutex/pthread_mutex.c, double_unlock_bad2, 5, UNLOCKING_UNLOCKED_MUTEX
+codetoanalyze/c/errors/mutex/pthread_spinlock.c, spinlock_double_lock_bad, 3, LOCKING_ALREADY_LOCKED_SPINLOCK
+codetoanalyze/c/errors/mutex/pthread_spinlock.c, spinlock_double_lock_bad2, 3, LOCKING_ALREADY_LOCKED_SPINLOCK
 codetoanalyze/c/errors/null_dereference/angelism.c, bake, 2, NULL_DEREFERENCE
 codetoanalyze/c/errors/null_dereference/angelism.c, call_by_ref_actual_already_in_footprint_bad, 1, NULL_DEREFERENCE
 codetoanalyze/c/errors/null_dereference/angelism.c, struct_value_by_ref_callee_write_no_skip, 3, NULL_DEREFERENCE

infer/tests/codetoanalyze/c/errors/mutex/pthread_mutex.c

@@ -0,0 +1,65 @@
+/*
+ * 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 <pthread.h>
+
+int normal_life_ok(pthread_mutex_t* m) {
+  if (pthread_mutex_init(m, 0))
+    return 0;
+  if (pthread_mutex_lock(m))
+    return 0;
+  if (pthread_mutex_unlock(m))
+    return 0;
+  if (pthread_mutex_destroy(m))
+    return 0;
+  return 1;
+}
+
+int normal_ok2() {
+  pthread_mutex_t m;
+  normal_life_ok(&m);
+}
+
+void FN_double_lock_bad(pthread_mutex_t* m) {
+  pthread_mutex_lock(m);
+  pthread_mutex_lock(m);
+}
+
+void double_lock_uninit_bad() {
+  pthread_mutex_t m;
+  FN_double_lock_bad(&m);
+}
+
+void double_lock_bad2() {
+  pthread_mutex_t m;
+  pthread_mutex_init(&m, 0);
+  FN_double_lock_bad(&m);
+}
+
+void double_unlock_bad(pthread_mutex_t* m) {
+  pthread_mutex_unlock(m);
+  pthread_mutex_unlock(m);
+}
+
+void double_unlock_bad2() {
+  pthread_mutex_t m;
+  pthread_mutex_init(&m, 0);
+  pthread_mutex_lock(&m);
+  double_unlock_bad(&m);
+}
+
+void double_init_bad(pthread_mutex_t* m) {
+  pthread_mutex_init(m, 0);
+  pthread_mutex_init(m, 0);
+}
+
+// Already reported in double_init_bad
+void double_init_ok() {
+  pthread_mutex_t m;
+  double_init_bad(&m);
+}

infer/tests/codetoanalyze/c/errors/mutex/pthread_spinlock.c

@@ -0,0 +1,31 @@
+/*
+ * 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 <pthread.h>
+
+#ifdef __APPLE__
+// Spinlocks do not exist on mac
+typedef struct {
+  int __whatever;
+} pthread_spinlock_t;
+extern int pthread_spin_init(pthread_spinlock_t *__lock, int __pshared);
+extern int pthread_spin_destroy (pthread_spinlock_t *__lock);
+extern int pthread_spin_lock (pthread_spinlock_t *__lock);
+extern int pthread_spin_trylock (pthread_spinlock_t *__lock);
+extern int pthread_spin_unlock (pthread_spinlock_t *__lock);
+#endif
+
+void spinlock_double_lock_bad(pthread_spinlock_t* m) {
+  pthread_spin_lock(m);
+  pthread_spin_lock(m);
+}
+
+void spinlock_double_lock_bad2() {
+  pthread_spinlock_t m;
+  spinlock_double_lock_bad(&m);
+}

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

@@ -26,6 +26,7 @@ codetoanalyze/cpp/errors/mutex/std_mutex_lock_profiling.cpp, LockMapBucket_bad_u
 codetoanalyze/cpp/errors/mutex/std_mutex_lock_profiling.cpp, bad_usage1, 3, PRECONDITION_NOT_MET, [start of procedure bad_usage1(),Skipped call: function or method not found,start of procedure lp_lock<std::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<std::mutex>]
 codetoanalyze/cpp/errors/mutex/std_mutex_lock_profiling.cpp, bad_usage2, 3, PRECONDITION_NOT_MET, [start of procedure bad_usage2(),Skipped call: function or method not found]
 codetoanalyze/cpp/errors/mutex/std_mutex_lock_profiling.cpp, lp_lock<std::mutex>, 7, DOUBLE_LOCK, [start of procedure lp_lock<std::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/mutex/timed_mutex.cpp, alarm1, 2, DOUBLE_LOCK, [start of procedure alarm1()]
 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/timed_mutex.cpp

@@ -0,0 +1,14 @@
+/*
+ * 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::timed_mutex& m) {
+  m.lock();
+  m.lock();
+}