MayLock Analysis & Sanity Checks of Mutex Usage & Analysis of Mutex Types

src/analyses/mutexTypeAnalysis.ml

@@ -26,16 +26,30 @@ struct
 
   (* transfer functions *)
   let assign ctx (lval:lval) (rval:exp) : D.t =
+    (* replaces the rightmost offset with r *)
+    let rec replace_no_offset o r = match o with
+      | `NoOffset -> r
+      | `Field (f,o) -> `Field (f, replace_no_offset o r)
+      | `Index (i,o) -> `Index (i, replace_no_offset o r)
+    in
     match lval with
-    | Var v, Field ({fname = "__data"; _}, Field ({fname = "__kind"; _}, NoOffset)) when ValueDomain.Compound.is_mutex_type v.vtype ->
-      let kind =
-        (match Cil.constFold true rval with
-         | Const (CInt (c, _, _)) -> MAttr.of_int c
-         | _ -> `Top)
+    | (Var v, o) ->
+      let rec helper o t = function
+        | Field ({fname = "__data"; _}, Field ({fname = "__kind"; _}, NoOffset)) when ValueDomain.Compound.is_mutex_type t ->
+          let kind =
+            (match Cil.constFold true rval with
+             | Const (CInt (c, _, _)) -> MAttr.of_int c
+             | _ -> `Top)
+          in
+
+          let r = G.singleton ((v,o)) kind in
+          ctx.sideg v r;
+          ctx.local
+        | Index (i,o') -> helper (replace_no_offset o (`Index (Lval.any_index_exp,`NoOffset))) (Cilfacade.typeOffset t (Index (i,NoOffset))) o'
+        | Field (f,o') -> helper (replace_no_offset o (`Field (f,`NoOffset)))  (Cilfacade.typeOffset t (Field (f,NoOffset))) o'
+        | NoOffset -> ctx.local
       in
-      let r = G.singleton ((v,`NoOffset)) kind in
-      ctx.sideg v r;
-      ctx.local
+      helper `NoOffset v.vtype o
     | _ -> ctx.local
 
   let branch ctx (exp:exp) (tv:bool) : D.t =

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

@@ -0,0 +1,53 @@
+// 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;
+
+struct s {
+    pthread_mutex_t m;
+};
+
+typedef struct s s_t;
+
+s_t mut = { PTHREAD_MUTEX_INITIALIZER };
+
+#ifndef __APPLE__
+s_t mut2 = { PTHREAD_RECURSIVE_MUTEX_INITIALIZER_NP };
+#endif
+
+
+void* f1(void* ptr) {
+    int top;
+
+    g = 1;
+    if(top) {
+        pthread_mutex_lock(&mut.m);
+    }
+    pthread_mutex_lock(&mut.m); //WARN
+    pthread_mutex_unlock(&mut.m);
+    return NULL;
+}
+
+
+int main(int argc, char const *argv[])
+{
+    pthread_t t1;
+    pthread_t t2;
+
+    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;
+}