diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index bb50c96432..3710d2db9c 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -121,14 +121,17 @@ struct let add ctx ((addr, rw): AddrRW.t): D.t = match addr with - | Addr mv -> + | Addr ((v, o) as mv) -> let (s, m) = ctx.local in let s' = MustLocksetRW.add_mval_rw (mv, rw) s in let m' = - if MutexTypeAnalysis.must_be_recursive ctx mv then - MustMultiplicity.increment mv m - else + match ctx.ask (Queries.MutexType (v, Offset.Unit.of_offs o)) with + | `Lifted Recursive -> MustMultiplicity.increment mv m + | `Lifted NonRec -> + if MustLocksetRW.mem_mval mv s then + M.error ~category:M.Category.Behavior.Undefined.double_locking "Acquiring a non-recursive mutex that is already held"; m + | `Bot | `Top -> m in (s', m') | NullPtr -> diff --git a/tests/regression/03-practical/21-pfscan_combine_minimal.c b/tests/regression/03-practical/21-pfscan_combine_minimal.c index abdef0627b..b8fc7948b2 100644 --- a/tests/regression/03-practical/21-pfscan_combine_minimal.c +++ b/tests/regression/03-practical/21-pfscan_combine_minimal.c @@ -18,7 +18,7 @@ int pqueue_init(PQUEUE *qp) void pqueue_close(PQUEUE *qp ) { - pthread_mutex_lock(& qp->mtx); + pthread_mutex_lock(& qp->mtx); // TODO (OSX): WARN (must double locking) qp->closed = 1; pthread_mutex_unlock(& qp->mtx); return; @@ -26,7 +26,7 @@ void pqueue_close(PQUEUE *qp ) int pqueue_put(PQUEUE *qp) { - pthread_mutex_lock(& qp->mtx); + pthread_mutex_lock(& qp->mtx); // TODO (OSX): WARN (must double locking) if (qp->closed) { // pfscan actually has a bug and is missing the following unlock at early return // pthread_mutex_unlock(& qp->mtx); diff --git a/tests/regression/04-mutex/32-allfuns.c b/tests/regression/04-mutex/32-allfuns.c index b59c487c53..e6b88e47ce 100644 --- a/tests/regression/04-mutex/32-allfuns.c +++ b/tests/regression/04-mutex/32-allfuns.c @@ -8,11 +8,11 @@ pthread_mutex_t B_mutex = PTHREAD_MUTEX_INITIALIZER; void t1() { pthread_mutex_lock(&A_mutex); myglobal++; //RACE! - pthread_mutex_lock(&A_mutex); + pthread_mutex_unlock(&A_mutex); } void t2() { pthread_mutex_lock(&B_mutex); myglobal++; //RACE! - pthread_mutex_lock(&B_mutex); + pthread_mutex_unlock(&B_mutex); } diff --git a/tests/regression/09-regions/31-equ_rc.c b/tests/regression/09-regions/31-equ_rc.c index 7cea370c58..2f3aff7f63 100644 --- a/tests/regression/09-regions/31-equ_rc.c +++ b/tests/regression/09-regions/31-equ_rc.c @@ -15,7 +15,7 @@ struct s { void *t_fun(void *arg) { pthread_mutex_lock(&A.mutex); B.datum = 5; // RACE! - pthread_mutex_lock(&A.mutex); + pthread_mutex_unlock(&A.mutex); return NULL; } diff --git a/tests/regression/09-regions/32-equ_nr.c b/tests/regression/09-regions/32-equ_nr.c index d9b909546e..a242448ba8 100644 --- a/tests/regression/09-regions/32-equ_nr.c +++ b/tests/regression/09-regions/32-equ_nr.c @@ -15,7 +15,7 @@ struct s { void *t_fun(void *arg) { pthread_mutex_lock(&A.mutex); A.datum = 5; // NORACE - pthread_mutex_lock(&A.mutex); + pthread_mutex_unlock(&A.mutex); return NULL; }