From 3878a2283d60a07d5dcb767e0c788e1997b5d5fa Mon Sep 17 00:00:00 2001
From: Michael Schwarz <michael.schwarz93@gmail.com>
Date: Fri, 9 Aug 2024 19:20:52 +0200
Subject: [PATCH] Make `update_offset` idempotent for blobs

---
 src/cdomain/value/cdomains/valueDomain.ml     | 43 ++++++++++---------
 tests/regression/13-privatized/95-mm-calloc.c | 28 ++++++++++++
 2 files changed, 51 insertions(+), 20 deletions(-)
 create mode 100644 tests/regression/13-privatized/95-mm-calloc.c

diff --git a/src/cdomain/value/cdomains/valueDomain.ml b/src/cdomain/value/cdomains/valueDomain.ml
index 869cacdd4e..0531fb772b 100644
--- a/src/cdomain/value/cdomains/valueDomain.ml
+++ b/src/cdomain/value/cdomains/valueDomain.ml
@@ -982,26 +982,29 @@ struct
           end
         | Blob (x,s,orig), _ ->
           begin
-            let l', o' = shift_one_over l o in
-            let x = zero_init_calloced_memory orig x t in
-            (* Strong update of scalar variable is possible if the variable is unique and size of written value matches size of blob being written to. *)
-            let do_strong_update =
-              begin match v with
-                | (Var var, _) ->
-                  let blob_size_opt = ID.to_int s in
-                  not @@ ask.is_multiple var
-                  && Option.is_some blob_size_opt (* Size of blob is known *)
-                  && ((
-                      not @@ Cil.isVoidType t     (* Size of value is known *)
-                      && Z.equal (Option.get blob_size_opt) (Z.of_int @@ Cil.alignOf_int t)
-                    ) || blob_destructive)
-                | _ -> false
-              end
-            in
-            if do_strong_update then
-              Blob ((do_update_offset ask x offs value exp l' o' v t), s, orig)
-            else
-              mu (Blob (join x (do_update_offset ask x offs value exp l' o' v t), s, orig))
+            match offs, value with
+            | `NoOffset, Blob (x2, s2, orig2) -> mu (Blob (join x x2, ID.join s s2,ZeroInit.join orig orig2))
+            | _ ->
+              let l', o' = shift_one_over l o in
+              let x = zero_init_calloced_memory orig x t in
+              (* Strong update of scalar variable is possible if the variable is unique and size of written value matches size of blob being written to. *)
+              let do_strong_update =
+                begin match v with
+                  | (Var var, _) ->
+                    let blob_size_opt = ID.to_int s in
+                    not @@ ask.is_multiple var
+                    && Option.is_some blob_size_opt (* Size of blob is known *)
+                    && ((
+                        not @@ Cil.isVoidType t     (* Size of value is known *)
+                        && Z.equal (Option.get blob_size_opt) (Z.of_int @@ Cil.alignOf_int t)
+                      ) || blob_destructive)
+                  | _ -> false
+                end
+              in
+              if do_strong_update then
+                Blob ((do_update_offset ask x offs value exp l' o' v t), s, orig)
+              else
+                mu (Blob (join x (do_update_offset ask x offs value exp l' o' v t), s, orig))
           end
         | Thread _, _ ->
           (* hack for pthread_t variables *)
diff --git a/tests/regression/13-privatized/95-mm-calloc.c b/tests/regression/13-privatized/95-mm-calloc.c
new file mode 100644
index 0000000000..60a88379fc
--- /dev/null
+++ b/tests/regression/13-privatized/95-mm-calloc.c
@@ -0,0 +1,28 @@
+// PARAM: --set ana.base.privatization mutex-meet
+#include<pthread.h>
+#include<stdlib.h>
+#include<stdio.h>
+struct a {
+  void (*b)();
+};
+
+int g = 0;
+
+struct a* t;
+void m() {
+  // Reachable!
+  g = 1;
+}
+
+void* j(void* arg) {};
+
+void main() {
+  pthread_t tid;
+  pthread_create(&tid, 0, j, NULL);
+  t = calloc(1, sizeof(struct a));
+  t->b = &m;
+  struct a r = *t;
+  r.b();
+
+  __goblint_check(g ==0); //UNKNOWN!
+}