Refine Points-To set on locking a mutex

src/analyses/base.ml

@@ -2929,6 +2929,11 @@ struct
           {st' with cpa = CPA.remove !longjmp_return st'.cpa}
         | None -> ctx.local
       end
+    | Events.RefinePointerExp {exp; ad} ->
+      (match exp with
+       | Lval lval ->
+         set ~ctx ctx.local (eval_lv ~ctx ctx.local lval) (Cilfacade.typeOf exp) (Address ad)
+       | _ -> ctx.local) 
     | _ ->
       ctx.local
 end

src/analyses/mutexEventsAnalysis.ml

@@ -24,15 +24,15 @@ struct
     match lv_opt with
     | None ->
       Queries.AD.iter (fun e ->
-          ctx.split () [Events.Lock (e, rw)]
+          ctx.split () [Events.Lock (e, rw); Events.RefinePointerExp {exp = arg; ad = Queries.AD.singleton 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); Events.RefinePointerExp {exp = arg; ad = Queries.AD.singleton 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

src/domains/events.ml

@@ -16,6 +16,7 @@ type t =
   | Assert of exp
   | Unassume of {exp: CilType.Exp.t; uuids: string list}
   | Longjmped of {lval: CilType.Lval.t option}
+  | RefinePointerExp of {exp: CilType.Exp.t; ad: ValueDomain.AD.t}
 
 (** Should event be emitted after transfer function raises [Deadcode]? *)
 let emit_on_deadcode = function
@@ -31,7 +32,8 @@ let emit_on_deadcode = function
   | UpdateExpSplit _ (* Pointless to split on dead. *)
   | Unassume _ (* Avoid spurious writes. *)
   | Assert _ (* Pointless to refine dead. *)
-  | Longjmped _ ->
+  | Longjmped _
+  | RefinePointerExp _ ->
     false
 
 let pretty () = function
@@ -47,3 +49,4 @@ let pretty () = function
   | Assert exp -> dprintf "Assert %a" d_exp exp
   | Unassume {exp; uuids} -> dprintf "Unassume {exp=%a; uuids=%a}" d_exp exp (docList Pretty.text) uuids
   | Longjmped {lval} -> dprintf "Longjmped {lval=%a}" (docOpt (CilType.Lval.pretty ())) lval
+  | RefinePointerExp {exp; ad} -> dprintf "RefinePointerExp {exp=%a; ad=%a}" CilType.Exp.pretty exp ValueDomain.AD.pretty ad 

tests/regression/79-mutex2/01-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/79-mutex2/02-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;
+}