From 880d59f91c2d47d7d6337d4edb7c0a314c753dca Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Sat, 27 Jan 2024 23:36:50 +0100
Subject: [PATCH] Refine Points-To set on locking a mutex

---
 src/analyses/base.ml                  |  5 +++++
 src/analyses/mutexEventsAnalysis.ml   |  4 ++--
 src/domains/events.ml                 |  5 ++++-
 tests/regression/79-mutex2/01-split.c | 20 ++++++++++++++++++++
 4 files changed, 31 insertions(+), 3 deletions(-)
 create mode 100644 tests/regression/79-mutex2/01-split.c

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 42e43b623a..c20fb71447 100644
--- a/src/analyses/base.ml
+++ b/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
diff --git a/src/analyses/mutexEventsAnalysis.ml b/src/analyses/mutexEventsAnalysis.ml
index 162527b32b..84190e6df4 100644
--- a/src/analyses/mutexEventsAnalysis.ml
+++ b/src/analyses/mutexEventsAnalysis.ml
@@ -24,7 +24,7 @@ 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 () [];
@@ -32,7 +32,7 @@ struct
     | 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
diff --git a/src/domains/events.ml b/src/domains/events.ml
index 06561bddbe..78fedeafa2 100644
--- a/src/domains/events.ml
+++ b/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 
\ No newline at end of file
diff --git a/tests/regression/79-mutex2/01-split.c b/tests/regression/79-mutex2/01-split.c
new file mode 100644
index 0000000000..0ca07f5b4d
--- /dev/null
+++ b/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;
+}
\ No newline at end of file