Merge pull request #1492 from goblint/issue_1489

Fix `mutex-meet` for malloc after thread creation

Author: sim642

src/analyses/apron/relationPriv.apron.ml

@@ -503,7 +503,7 @@ struct
     in
     let get_mutex_inits = getg V.mutex_inits in
     let get_mutex_inits' = RD.keep_vars get_mutex_inits [g_var] in
-    if not (RD.mem_var get_mutex_inits' g_var) then (* TODO: is this just a workaround for an escape bug? https://github.com/goblint/analyzer/pull/1354/files#r1498882657 *)
+    if RD.mem_var get_mutex_global_g g_var && not (RD.mem_var get_mutex_inits' g_var) then (* TODO: is this just a workaround for an escape bug? https://github.com/goblint/analyzer/pull/1354/files#r1498882657 *)
       (* This is an escaped variable whose value was never side-effected to get_mutex_inits' *)
       get_mutex_global_g
     else

tests/regression/46-apron2/90-malloc.c

@@ -0,0 +1,21 @@
+// SKIP PARAM: --set ana.activated[+] apron  --set ana.relation.privatization mutex-meet --set ana.apron.domain interval --set sem.int.signed_overflow assume_none
+// Checks that assinging to malloc'ed memory does not cause both branches to be dead
+#include <pthread.h>
+#include <goblint.h>
+void nop(void* arg) {
+}
+
+void main() {
+  pthread_t thread;
+  pthread_create(&thread, 0, &nop, 0);
+
+  long *k = malloc(sizeof(long));
+  *k = 5;
+  if (1)
+    ;
+
+  __goblint_check(*k >= 5); // Reachable and true
+
+  *k = *k+1;
+  __goblint_check(*k >= 5); // Reachable and true
+}

tests/regression/46-apron2/91-malloc-tid.c

@@ -0,0 +1,21 @@
+// SKIP PARAM: --set ana.activated[+] apron --set ana.path_sens[+] threadflag  --set ana.relation.privatization mutex-meet-tid --set ana.apron.domain interval --set sem.int.signed_overflow assume_none
+// Checks that assinging to malloc'ed memory does not cause both branches to be dead
+#include <pthread.h>
+#include <goblint.h>
+void nop(void* arg) {
+}
+
+void main() {
+  pthread_t thread;
+  pthread_create(&thread, 0, &nop, 0);
+
+  long *k = malloc(sizeof(long));
+  *k = 5;
+  if (1)
+    ;
+
+  __goblint_check(*k >= 5); // Reachable and true
+
+  *k = *k+1;
+  __goblint_check(*k >= 5); // Reachable and true
+}

tests/regression/46-apron2/92-malloc-atomic.c

@@ -0,0 +1,21 @@
+// SKIP PARAM: --set ana.activated[+] apron  --set ana.relation.privatization mutex-meet-atomic --set ana.apron.domain interval --set sem.int.signed_overflow assume_none
+// Checks that assinging to malloc'ed memory does not cause both branches to be dead
+#include <pthread.h>
+#include <goblint.h>
+void nop(void* arg) {
+}
+
+void main() {
+  pthread_t thread;
+  pthread_create(&thread, 0, &nop, 0);
+
+  long *k = malloc(sizeof(long));
+  *k = 5;
+  if (1)
+    ;
+
+  __goblint_check(*k >= 5); // Reachable and true
+
+  *k = *k+1;
+  __goblint_check(*k >= 5); // Reachable and true
+}