Merge pull request #1410 from goblint/mutex-init-null-attr

Fix NULL pointer dereference error for NULL mutexattr

src/analyses/base.ml

@@ -1375,10 +1375,13 @@ struct
     | Q.EvalInt e ->
       query_evalint ~ctx ctx.local e
     | Q.EvalMutexAttr e -> begin
-        let e:exp = Lval (Cil.mkMem ~addr:e ~off:NoOffset) in
-        match eval_rv ~ctx ctx.local e with
-        | MutexAttr a -> a
-        | v -> MutexAttrDomain.top ()
+        match eval_rv_address ~ctx ctx.local e with
+        | Address a ->
+          begin match get ~ctx ~top:(MutexAttr (MutexAttrDomain.top ())) ctx.local a None with (* ~top corresponds to default NULL *)
+            | MutexAttr a -> a
+            | _ -> MutexAttrDomain.top ()
+          end
+        | _ -> MutexAttrDomain.top ()
       end
     | Q.EvalLength e -> begin
         match eval_rv_address ~ctx ctx.local e with

tests/regression/71-doublelocking/17-default-dyn.c

@@ -0,0 +1,52 @@
+// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType'
+#define _GNU_SOURCE
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+#include <assert.h>
+
+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 cannot be removed
+    return NULL; // WARN
+}
+
+
+
+int main(int argc, char const *argv[])
+{
+    pthread_t t1;
+    pthread_t t2;
+    pthread_mutex_t mut;
+    pthread_mutex_init(&mut, NULL); // NOWARN (no null pointer error)
+
+
+    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;
+}