diff --git a/infer/models/c/src/infer_builtins.h b/infer/models/c/src/infer_builtins.h index 2a978ae17..2c32756cd 100644 --- a/infer/models/c/src/infer_builtins.h +++ b/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); diff --git a/infer/models/c/src/libc_basic.c b/infer/models/c/src/libc_basic.c index 6f2911bc0..2b74a1a99 100644 --- a/infer/models/c/src/libc_basic.c +++ b/infer/models/c/src/libc_basic.c @@ -52,6 +52,7 @@ #endif #include +#include #include #include #include @@ -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) { diff --git a/infer/models/cpp/src/mutex.cpp b/infer/models/cpp/src/mutex.cpp index 26c2bdd33..f950344c8 100644 --- a/infer/models/cpp/src/mutex.cpp +++ b/infer/models/cpp/src/mutex.cpp @@ -9,6 +9,7 @@ #pragma once +#include #include #include @@ -19,15 +20,15 @@ int __INFER_UNLOCKED = 0; template 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 + 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/backend/errdesc.ml b/infer/src/backend/errdesc.ml index c4e68a168..b1a3a9efc 100644 --- a/infer/src/backend/errdesc.ml +++ b/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 diff --git a/infer/tests/codetoanalyze/c/errors/issues.exp b/infer/tests/codetoanalyze/c/errors/issues.exp index 60f209240..8b5013eb7 100644 --- a/infer/tests/codetoanalyze/c/errors/issues.exp +++ b/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 diff --git a/infer/tests/codetoanalyze/c/errors/mutex/pthread_mutex.c b/infer/tests/codetoanalyze/c/errors/mutex/pthread_mutex.c new file mode 100644 index 000000000..a36dfa458 --- /dev/null +++ b/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 + +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); +} diff --git a/infer/tests/codetoanalyze/c/errors/mutex/pthread_spinlock.c b/infer/tests/codetoanalyze/c/errors/mutex/pthread_spinlock.c new file mode 100644 index 000000000..bd34e067b --- /dev/null +++ b/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 + +#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); +} diff --git a/infer/tests/codetoanalyze/cpp/errors/issues.exp b/infer/tests/codetoanalyze/cpp/errors/issues.exp index fda9aad76..7d2f512ee 100644 --- a/infer/tests/codetoanalyze/cpp/errors/issues.exp +++ b/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(),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(),Skipped call: function or method not found] 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/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] diff --git a/infer/tests/codetoanalyze/cpp/errors/mutex/timed_mutex.cpp b/infer/tests/codetoanalyze/cpp/errors/mutex/timed_mutex.cpp new file mode 100644 index 000000000..46ff2e6a1 --- /dev/null +++ b/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 + +void alarm1(std::timed_mutex& m) { + m.lock(); + m.lock(); +}