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

src/analyses/mayLocks.ml

@@ -15,9 +15,9 @@ struct
         M.warn ~category:M.Category.Behavior.Undefined.double_locking "Acquiring a (possibly non-recursive) mutex that may be already held";
         ctx.local
       in
-      match D.Addr.to_var_must l with
-      | Some v ->
-        (let mtype = ctx.ask (Queries.MutexType v) in
+      match D.Addr.to_var_offset l with
+      | Some (v,o) ->
+        (let mtype = ctx.ask (Queries.MutexType (v, MutexTypeAnalysis.offs_no_index o)) in
          match mtype with
          | `Lifted MutexAttrDomain.MutexKind.Recursive -> ctx.local
          | `Lifted MutexAttrDomain.MutexKind.NonRec ->
@@ -30,9 +30,9 @@ struct
 
   let remove ctx l =
     if not (D.mem l ctx.local) then M.warn "Releasing a mutex that is definitely not held";
-    match D.Addr.to_var_must l with
-    | Some v ->
-      (let mtype = ctx.ask (Queries.MutexType v) in
+    match D.Addr.to_var_offset l with
+    | Some (v,o) ->
+      (let mtype = ctx.ask (Queries.MutexType (v, MutexTypeAnalysis.offs_no_index o)) in
        match mtype with
        | `Lifted MutexAttrDomain.MutexKind.NonRec -> D.remove l ctx.local
        | _ -> ctx.local (* we cannot remove them here *))

src/analyses/mutexTypeAnalysis.ml

@@ -6,6 +6,13 @@ open Analyses
 module MAttr = ValueDomain.MutexAttr
 module LF = LibraryFunctions
 
+(* Removing indexes here avoids complicated lookups inside the map for a varinfo, at the price that different types of mutexes in arrays are not dinstinguished *)
+let rec offs_no_index o =
+  match o with
+  | `NoOffset -> `NoOffset
+  | `Field (f,o) -> `Field (f, offs_no_index o)
+  | `Index (i,o) -> `Index (Lval.any_index_exp, offs_no_index o)
+
 module Spec : Analyses.MCPSpec with module D = Lattice.Unit and module C = Lattice.Unit =
 struct
   include Analyses.DefaultSpec
@@ -14,7 +21,8 @@ struct
   let name () = "pthreadMutexType"
   module D = Lattice.Unit
   module C = Lattice.Unit
-  module G = MAttr
+
+  module G = MapDomain.MapBot_LiftTop (Lval.CilLval) (MAttr)
 
   (* transfer functions *)
   let assign ctx (lval:lval) (rval:exp) : D.t =
@@ -25,7 +33,8 @@ struct
          | Const (CInt (c, _, _)) -> MAttr.of_int c
          | _ -> `Top)
       in
-      ctx.sideg v kind;
+      let r = G.singleton ((v,`NoOffset)) kind in
+      ctx.sideg v r;
       ctx.local
     | _ -> ctx.local
 
@@ -53,7 +62,10 @@ struct
     | MutexInit {mutex = mutex; attr = attr} ->
       let mutexes = ctx.ask (Queries.MayPointTo mutex) in
       let attr = ctx.ask (Queries.EvalMutexAttr attr) in
-      Queries.LS.iter (function (v, _) -> ctx.sideg v attr) mutexes;
+      (* It is correct to iter over these sets here, as mutexes need to be intialized before being used, and an analysis that detects usage before initialization is a different analysis. *)
+      Queries.LS.iter (function (v, o) ->
+          let r = G.singleton (v, offs_no_index o) attr in
+          ctx.sideg v r) mutexes;
       ctx.local
     | _ -> ctx.local
 
@@ -64,7 +76,7 @@ struct
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
     match q with
-    | Queries.MutexType v -> (ctx.global v:MutexAttrDomain.t)
+    | Queries.MutexType ((v,o):Lval.CilLval.t) -> let r = ctx.global v in (G.find (v,o) r:MutexAttrDomain.t)
     | _ -> Queries.Result.top q
 end
 

src/domains/queries.ml

@@ -83,7 +83,7 @@ type _ t =
   | HeapVar: VI.t t
   | IsHeapVar: varinfo -> MayBool.t t (* TODO: is may or must? *)
   | IsMultiple: varinfo -> MustBool.t t (* Is no other copy of this local variable reachable via pointers? *)
-  | MutexType: varinfo -> MutexAttrDomain.t t
+  | MutexType: Lval.CilLval.t -> MutexAttrDomain.t t
   | EvalThread: exp -> ConcDomain.ThreadSet.t t
   | EvalMutexAttr: exp -> MutexAttrDomain.t t
   | EvalJumpBuf: exp -> JmpBufDomain.JmpBufSet.t t
@@ -321,7 +321,7 @@ struct
       | Any (Invariant i1), Any (Invariant i2) -> compare_invariant_context i1 i2
       | Any (InvariantGlobal vi1), Any (InvariantGlobal vi2) -> Stdlib.compare (Hashtbl.hash vi1) (Hashtbl.hash vi2)
       | Any (IterSysVars (vq1, vf1)), Any (IterSysVars (vq2, vf2)) -> VarQuery.compare vq1 vq2 (* not comparing fs *)
-      | Any (MutexType v1), Any (MutexType v2) -> CilType.Varinfo.compare v1 v2
+      | Any (MutexType v1), Any (MutexType v2) -> Lval.CilLval.compare v1 v2
       | Any (MustProtectedVars m1), Any (MustProtectedVars m2) -> compare_mustprotectedvars m1 m2
       | Any (MayBeModifiedSinceSetjmp e1), Any (MayBeModifiedSinceSetjmp e2) -> JmpBufDomain.BufferEntry.compare e1 e2
       | Any (MustBeSingleThreaded {since_start=s1;}),  Any (MustBeSingleThreaded {since_start=s2;}) -> Stdlib.compare s1 s2
@@ -358,7 +358,7 @@ struct
     | Any (EvalJumpBuf e) -> CilType.Exp.hash e
     | Any (WarnGlobal vi) -> Hashtbl.hash vi
     | Any (Invariant i) -> hash_invariant_context i
-    | Any (MutexType v) -> CilType.Varinfo.hash v
+    | Any (MutexType v) -> Lval.CilLval.hash v
     | Any (InvariantGlobal vi) -> Hashtbl.hash vi
     | Any (MustProtectedVars m) -> hash_mustprotectedvars m
     | Any (MayBeModifiedSinceSetjmp e) -> JmpBufDomain.BufferEntry.hash e

tests/regression/71-doublelocking/12-rec-dyn-struct.c

@@ -0,0 +1,56 @@
+// PARAM: --set ana.activated[+] 'maylocks' --set ana.activated[+] 'pthreadMutexType'
+// Like 06, but tests mutexattr survives joins
+#define _GNU_SOURCE
+#include<pthread.h>
+#include<stdio.h>
+#include<unistd.h>
+#include <assert.h>
+
+int g;
+struct s {
+    pthread_mutex_t mut;
+};
+
+typedef struct s s_t;
+
+
+void* f1(void* ptr) {
+    pthread_mutex_t* mut = &(((s_t*) ptr)->mut);
+
+    pthread_mutex_lock(mut); //NOWARN
+    pthread_mutex_lock(mut); //NOWARN
+    pthread_mutex_unlock(mut);
+    pthread_mutex_unlock(mut);
+    return NULL;
+}
+
+
+int main(int argc, char const *argv[])
+{
+    pthread_t t1;
+    s_t mut_str;
+
+    pthread_mutexattr_t attr;
+
+    if(argc == 2) {
+        pthread_mutexattr_settype(&attr, PTHREAD_MUTEX_RECURSIVE);
+    } else {
+        pthread_mutexattr_settype(&attr, PTHREAD_MUTEX_RECURSIVE);
+    }
+
+    pthread_mutex_init(&mut_str.mut, &attr);
+
+
+    pthread_create(&t1,NULL,f1,&mut_str);
+
+
+    pthread_mutex_lock(&mut_str.mut); //NOWARN
+    pthread_mutex_lock(&mut_str.mut); //NOWARN
+    pthread_mutex_unlock(&mut_str.mut);
+    pthread_mutex_unlock(&mut_str.mut);
+
+    pthread_join(t1, NULL);
+
+
+    return 0;
+}