Merge pull request #1644 from goblint/issue_1558_master

Make `update_offset` idempotent for blobs

Author: michael-schwarz

src/cdomain/value/cdomains/valueDomain.ml

@@ -1001,28 +1001,31 @@ struct
             else
               mu (Blob (join x (do_update_offset ask x offs value exp l' o' v t), s, zeroinit))
           end
-        | Blob (x,s,zeroinit), _ ->
+        | Blob (x,s,zeroinit), `NoOffset -> (* `NoOffset is only remaining possibility for Blob here *)
           begin
-            let l', o' = shift_one_over l o in
-            let x = zero_init_calloced_memory zeroinit 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
-                  && GobOption.exists (fun blob_size -> (* Size of blob is known *)
-                      (not @@ Cil.isVoidType t     (* Size of value is known *)
-                       && Z.equal blob_size (Z.of_int @@ Cil.alignOf_int t))
-                      || blob_destructive
-                    ) blob_size_opt
-                | _ -> false
-              end
-            in
-            if do_strong_update then
-              Blob ((do_update_offset ask x offs value exp l' o' v t), s, zeroinit)
-            else
-              mu (Blob (join x (do_update_offset ask x offs value exp l' o' v t), s, zeroinit))
+            match value with
+            | Blob (x2, s2, zeroinit2) -> mu (Blob (join x x2, ID.join s s2, zeroinit))
+            | _ ->
+              let l', o' = shift_one_over l o in
+              let x = zero_init_calloced_memory zeroinit 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
+                    && GobOption.exists (fun blob_size -> (* Size of blob is known *)
+                        (not @@ Cil.isVoidType t     (* Size of value is known *)
+                         && Z.equal blob_size (Z.of_int @@ Cil.alignOf_int t))
+                        || blob_destructive
+                      ) blob_size_opt
+                  | _ -> false
+                end
+              in
+              if do_strong_update then
+                Blob ((do_update_offset ask x offs value exp l' o' v t), s, zeroinit)
+              else
+                mu (Blob (join x (do_update_offset ask x offs value exp l' o' v t), s, zeroinit))
           end
         | Thread _, _ ->
           (* hack for pthread_t variables *)

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!
+}