Refine Points-To set on locking a mutex

src/analyses/mutexEventsAnalysis.ml

@@ -21,18 +21,24 @@ struct
   let eval_exp_addr (a: Queries.ask) exp = a.f (Queries.MayPointTo exp)
 
   let lock ctx rw may_fail nonzero_return_when_aquired a lv_opt arg =
+    let compute_refine_split (e:Mutexes.elt) = match e with
+      | Addr a ->
+        let e' = BinOp(Eq, arg, AddrOf ((PreValueDomain.Mval.to_cil a)), intType) in
+        [Events.SplitBranch  (e',true)]
+      | _ -> []
+    in
     match lv_opt with
     | None ->
       Queries.AD.iter (fun e ->
-          ctx.split () [Events.Lock (e, rw)]
+          ctx.split () (Events.Lock (e, rw) :: compute_refine_split e)
         ) (eval_exp_addr a arg);
       if may_fail then
         ctx.split () [];
       raise Analyses.Deadcode
     | Some lv ->
       let sb = Events.SplitBranch (Lval lv, nonzero_return_when_aquired) in
       Queries.AD.iter (fun e ->
-          ctx.split () [sb; Events.Lock (e, rw)];
+          ctx.split () (sb :: Events.Lock (e, rw) :: compute_refine_split e);
         ) (eval_exp_addr a arg);
       if may_fail then (
         let fail_exp = if nonzero_return_when_aquired then Lval lv else BinOp(Gt, Lval lv, zero, intType) in

tests/regression/04-mutex/96-split.c

@@ -0,0 +1,20 @@
+#include<pthread.h>
+
+pthread_mutex_t m1;
+pthread_mutex_t m2;
+
+int main(int argc, char const *argv[])
+{
+    int top;
+    pthread_mutex_t* ptr;
+    ptr = &m1;
+
+    if(top) {
+        ptr = &m2;
+    }
+
+    pthread_mutex_lock(ptr);
+    pthread_mutex_unlock(ptr); //NOWARN
+
+    return 0;
+}

tests/regression/04-mutex/97-split-mt.c

@@ -0,0 +1,37 @@
+#include<pthread.h>
+
+pthread_mutex_t m1;
+pthread_mutex_t m2;
+pthread_mutex_t* ptr;
+
+void other() {
+    int top;
+    ptr = &m2;
+
+    if(top) {
+        ptr = &m1;
+    }
+}
+
+int main(int argc, char const *argv[])
+{
+    int top;
+
+    ptr = &m1;
+
+    if(top) {
+        ptr = &m2;
+    }
+
+    pthread_t mischievous;
+    pthread_create(&mischievous, NULL, other, NULL);
+
+
+    pthread_mutex_lock(ptr);
+
+    // This has to produce a warning, as the other thread may have changed what
+    // ptr points to such that it's not the same mutex being unlocked here.
+    pthread_mutex_unlock(ptr); //WARN
+
+    return 0;
+}