Merge pull request #1628 from goblint/must-relock

Error on must-relocking of non-recursive mutex

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

tests/regression/03-practical/21-pfscan_combine_minimal.c

@@ -18,15 +18,15 @@ 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;
 }
 
 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);

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

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;
 }
 

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;
 }