Fix pthread mutex type from initializer on OSX

docs/user-guide/assumptions.md

@@ -10,7 +10,7 @@ _NB! This list is likely incomplete._
 
     > An implementation may map this mutex to one of the other mutex types.
 
-    including `PTHREAD_MUTEX_RECURSIVE`, on Linux it seems to be mapped to `PTHREAD_MUTEX_NORMAL`.
+    including `PTHREAD_MUTEX_RECURSIVE`, on Linux and OSX it seems to be mapped to `PTHREAD_MUTEX_NORMAL`.
     Goblint assumes this to be the case.
 
     This affects the `maylocks` analysis.

src/analyses/mutexTypeAnalysis.ml

@@ -36,6 +36,19 @@ struct
           in
           ctx.sideg (v,o) kind;
           ctx.local
+        | Field ({fname = "__sig"; _}, NoOffset) when ValueDomain.Compound.is_mutex_type t -> (* OSX *)
+          let kind: MAttr.t = match Cil.constFold true rval with
+            | Const (CInt (c, _, _)) ->
+              begin match Z.to_int c with (* magic constants from https://opensource.apple.com/source/libpthread/libpthread-301.30.1/pthread/pthread_impl.h.auto.html *)
+                | 0x32AAABA7 -> `Lifted NonRec (* _PTHREAD_MUTEX_SIG_init *)
+                | 0x32AAABA1 -> `Lifted NonRec (* _PTHREAD_ERRORCHECK_MUTEX_SIG_init *)
+                | 0x32AAABA2 -> `Lifted Recursive (* _PTHREAD_RECURSIVE_MUTEX_SIG_init *)
+                | _ -> `Top
+              end
+            | _ -> `Top
+          in
+          ctx.sideg (v,o) kind;
+          ctx.local
         | Index (i,o') ->
           let o'' = O.of_offs (`Index (i, `NoOffset)) in
           helper (O.add_offset o o'') (Cilfacade.typeOffset t (Index (i,NoOffset))) o'

tests/regression/71-doublelocking/05-rec.c

@@ -10,7 +10,9 @@ int g;
 
 pthread_mutex_t mut = PTHREAD_MUTEX_INITIALIZER;
 
-#ifndef __APPLE__
+#ifdef __APPLE__
+pthread_mutex_t mut2 = PTHREAD_RECURSIVE_MUTEX_INITIALIZER;
+#else
 pthread_mutex_t mut2 = PTHREAD_RECURSIVE_MUTEX_INITIALIZER_NP;
 #endif
 
@@ -36,12 +38,10 @@ int main(int argc, char const *argv[])
     pthread_create(&t1,NULL,f1,NULL);
     pthread_join(t1, NULL);
 
-#ifndef __APPLE__
     pthread_mutex_lock(&mut2); //NOWARN
     pthread_mutex_lock(&mut2); //NOWARN
     pthread_mutex_unlock(&mut2);
     pthread_mutex_unlock(&mut2);
-#endif
 
     return 0;
 }

tests/regression/71-doublelocking/08-other-type.c

@@ -10,13 +10,12 @@ int g;
 
 pthread_mutex_t mut = PTHREAD_MUTEX_INITIALIZER;
 
-#ifndef __APPLE__
+#ifdef __APPLE__
+pthread_mutex_t mut2 = PTHREAD_RECURSIVE_MUTEX_INITIALIZER;
+pthread_mutex_t mut3 = PTHREAD_ERRORCHECK_MUTEX_INITIALIZER;
+#else
 pthread_mutex_t mut2 = PTHREAD_RECURSIVE_MUTEX_INITIALIZER_NP;
 pthread_mutex_t mut3 = PTHREAD_ERRORCHECK_MUTEX_INITIALIZER_NP;
-#else
-// OS X does not define PTHREAD_ERRORCHECK_MUTEX_INITIALIZER_NP
-// we thus use the default one there, which should also create warnings
-pthread_mutex_t mut3;
 #endif
 
 
@@ -55,12 +54,10 @@ int main(int argc, char const *argv[])
     pthread_create(&t2,NULL,f2,NULL);
     pthread_join(t1, NULL);
 
-#ifndef __APPLE__
     pthread_mutex_lock(&mut2); //NOWARN
     pthread_mutex_lock(&mut2); //NOWARN
     pthread_mutex_unlock(&mut2); //NOWARN
     pthread_mutex_unlock(&mut2);
-#endif
 
     return 0;
 }

tests/regression/71-doublelocking/13-rec-struct.c

@@ -16,7 +16,9 @@ typedef struct s s_t;
 
 s_t mut = { PTHREAD_MUTEX_INITIALIZER };
 
-#ifndef __APPLE__
+#ifdef __APPLE__
+s_t mut2 = { PTHREAD_RECURSIVE_MUTEX_INITIALIZER };
+#else
 s_t mut2 = { PTHREAD_RECURSIVE_MUTEX_INITIALIZER_NP };
 #endif
 
@@ -42,12 +44,10 @@ int main(int argc, char const *argv[])
     pthread_create(&t1,NULL,f1,NULL);
     pthread_join(t1, NULL);
 
-#ifndef __APPLE__
     pthread_mutex_lock(&mut2.m); //NOWARN
     pthread_mutex_lock(&mut2.m); //NOWARN
     pthread_mutex_unlock(&mut2.m);
     pthread_mutex_unlock(&mut2.m);
-#endif
 
     return 0;
 }

tests/regression/71-doublelocking/19-default-init.c

@@ -6,7 +6,6 @@
 #include <assert.h>
 
 int g;
-pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER;
 
 void* f1(void* ptr) {
     pthread_mutex_t* mut = (pthread_mutex_t*) ptr;
@@ -34,7 +33,7 @@ int main(int argc, char const *argv[])
 {
     pthread_t t1;
     pthread_t t2;
-    pthread_mutex_t mut = &mutex;
+    pthread_mutex_t mut = PTHREAD_MUTEX_INITIALIZER;
 
     pthread_create(&t1,NULL,f1,&mut);
 

tests/regression/71-doublelocking/20-default-init-osx.c

@@ -0,0 +1,109 @@
+// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType' --set pre.cppflags[+] "-DGOBLINT_NO_PTHREAD_ONCE"
+// Here, we do not include pthread.h, to emulate the behavior of OS X.
+#define NULL ((void *)0)
+typedef signed char __int8_t;
+typedef unsigned char __uint8_t;
+typedef short __int16_t;
+typedef unsigned short __uint16_t;
+typedef int __int32_t;
+typedef unsigned int __uint32_t;
+typedef long long __int64_t;
+typedef unsigned long long __uint64_t;
+typedef long __darwin_intptr_t;
+typedef unsigned int __darwin_natural_t;
+typedef int __darwin_ct_rune_t;
+
+
+struct __darwin_pthread_handler_rec {
+ void (*__routine)(void *);
+ void *__arg;
+ struct __darwin_pthread_handler_rec *__next;
+};
+
+struct _opaque_pthread_attr_t {
+ long __sig;
+ char __opaque[56];
+};
+
+struct _opaque_pthread_mutex_t {
+ long __sig;
+ char __opaque[56];
+};
+
+struct _opaque_pthread_t {
+ long __sig;
+ struct __darwin_pthread_handler_rec *__cleanup_stack;
+ char __opaque[8176];
+};
+
+typedef struct _opaque_pthread_attr_t __darwin_pthread_attr_t;
+typedef struct _opaque_pthread_mutex_t __darwin_pthread_mutex_t;
+typedef struct _opaque_pthread_t *__darwin_pthread_t;
+
+typedef __darwin_pthread_attr_t pthread_attr_t;
+typedef __darwin_pthread_mutex_t pthread_mutex_t;
+typedef __darwin_pthread_t pthread_t;
+
+int pthread_create(pthread_t _Nullable restrict,
+  const pthread_attr_t * _Nullable restrict,
+  void * ,
+  void *);
+
+int pthread_join(pthread_t , void *);
+int pthread_mutex_lock(pthread_mutex_t *);
+int pthread_mutex_unlock(pthread_mutex_t *);
+
+/*
+ * [Internal] data structure signatures
+ */
+#define _PTHREAD_MUTEX_SIG_init		0x32AAABA7
+
+/*
+ * Mutex variables
+ */
+#define PTHREAD_MUTEX_INITIALIZER {_PTHREAD_MUTEX_SIG_init, {0}}
+
+
+int g;
+
+void* f1(void* ptr) {
+    pthread_mutex_t* mut = (pthread_mutex_t*) ptr;
+
+    pthread_mutex_lock(mut);
+    pthread_mutex_lock(mut); //WARN
+
+    return NULL;
+}
+
+
+void* f2(void* ptr) {
+    pthread_mutex_t* mut = (pthread_mutex_t*) ptr;
+
+    pthread_mutex_lock(mut);
+    pthread_mutex_unlock(mut);
+
+    // default mutex type may be mapped to recursive, so shouldn't be removed, but Goblint assumes it to be non-recursive
+    return NULL; // NOWARN (assumption)
+}
+
+
+
+int main(int argc, char const *argv[])
+{
+    pthread_t t1;
+    pthread_t t2;
+    pthread_mutex_t mut = PTHREAD_MUTEX_INITIALIZER;
+
+    pthread_create(&t1,NULL,f1,&mut);
+
+
+    pthread_mutex_lock(&mut);
+    pthread_mutex_lock(&mut); //WARN
+
+
+    pthread_join(t1, NULL);
+
+    pthread_create(&t2,NULL,f2,&mut);
+
+    return 0;
+}