Merge pull request #1458 from goblint/issue1457

`BaseAnalysis`: For non-definite AD, join over **all** components not just `cpa` in `set`

Author: michael-schwarz

src/analyses/base.ml

@@ -1738,7 +1738,7 @@ struct
       (* if M.tracing then M.tracel "set" ~var:firstvar "new state1 %a" CPA.pretty nst; *)
       (* If the address was definite, then we just return it. If the address
        * was ambiguous, we have to join it with the initial state. *)
-      let nst = if AD.cardinal lval > 1 then { nst with cpa = CPA.join st.cpa nst.cpa } else nst in
+      let nst = if AD.cardinal lval > 1 then D.join st nst else nst in
       (* if M.tracing then M.tracel "set" ~var:firstvar "new state2 %a" CPA.pretty nst; *)
       nst
     with

tests/regression/13-privatized/80-nondet-struct-ptr.c

@@ -0,0 +1,54 @@
+// PARAM: --set ana.base.privatization protection --enable ana.int.enums
+#include<pthread.h>
+#include<stdlib.h>
+struct a {
+  int b;
+};
+
+struct a *ptr;
+struct a *straightandnarrow;
+
+pthread_mutex_t m;
+
+void doit() {
+  void *newa = malloc(sizeof(struct a));
+
+  pthread_mutex_lock(&m);
+  ptr->b = 5;
+
+  int fear = straightandnarrow->b;
+  __goblint_check(fear == 5); //UNKNOWN!
+
+  ptr = newa;
+  pthread_mutex_unlock(&m);
+
+  pthread_mutex_lock(&m);
+  int hope = straightandnarrow->b;
+  __goblint_check(hope == 5); //UNKNOWN!
+  pthread_mutex_unlock(&m);
+
+}
+
+void* k(void *arg) {
+  doit();
+  return NULL;
+}
+
+int main() {
+    int top;
+    struct a other = { 0 };
+    struct a other2 = { 42 };
+    if(top) {
+      ptr = &other;
+    } else {
+      ptr = &other2;
+    }
+
+    straightandnarrow = &other;
+
+    pthread_t t1;
+    pthread_create(&t1, 0, k, 0);
+
+    doit();
+    return 0;
+}

tests/regression/13-privatized/81-nondet-local-pointer.c

@@ -0,0 +1,55 @@
+// PARAM: --set ana.base.privatization protection --enable ana.int.enums
+// Like 80-nondet-struct-ptr.c, but somewhat simplified to not use structs and malloc etc
+#include<pthread.h>
+#include<stdlib.h>
+struct a {
+  int b;
+};
+
+int *ptr;
+int *immer_da_oane;
+
+pthread_mutex_t m;
+
+void doit() {
+  pthread_mutex_lock(&m);
+  *ptr = 5;
+
+  // Should be either 5 or 0, depending on which one the pointer points to
+  int fear = *immer_da_oane;
+  __goblint_check(fear == 5); //UNKNOWN!
+
+  pthread_mutex_unlock(&m);
+
+  pthread_mutex_lock(&m);
+  int hope = *immer_da_oane;
+  __goblint_check(hope == 5); //UNKNOWN!
+  pthread_mutex_unlock(&m);
+
+}
+
+void* k(void *arg) {
+  // Force MT
+  return NULL;
+}
+
+int main() {
+    int top;
+
+    int da_oane = 0;
+    int de_andre = 42;
+
+    if(top) {
+      ptr = &da_oane;
+    } else {
+      ptr = &de_andre;
+    }
+
+    immer_da_oane = &da_oane;
+
+    pthread_t t1;
+    pthread_create(&t1, 0, k, 0);
+
+    doit();
+    return 0;
+}

tests/regression/13-privatized/82-nondet-global-pointer.c

@@ -0,0 +1,56 @@
+// PARAM: --set ana.base.privatization protection --enable ana.int.enums
+// Like 81-nondet-struct-ptr.c, but with syntactic globals instead of escaping ones.
+#include<pthread.h>
+#include<stdlib.h>
+struct a {
+  int b;
+};
+
+int *ptr;
+int *immer_da_oane;
+
+int da_oane = 0;
+int de_andre = 42;
+
+pthread_mutex_t m;
+
+void doit() {
+  pthread_mutex_lock(&m);
+  *ptr = 5;
+
+  // Should be either 0 or 5, depending on which one ptr points to
+  int fear = *immer_da_oane;
+  __goblint_check(fear == 5); //UNKNOWN!
+
+  pthread_mutex_unlock(&m);
+
+  pthread_mutex_lock(&m);
+  // This works
+  int hope = *immer_da_oane;
+  __goblint_check(hope == 5); //UNKNOWN!
+  pthread_mutex_unlock(&m);
+
+}
+
+void* k(void *arg) {
+  // Force MT
+  return NULL;
+}
+
+int main() {
+    int top;
+
+    if(top) {
+      ptr = &da_oane;
+    } else {
+      ptr = &de_andre;
+    }
+
+    immer_da_oane = &da_oane;
+
+    pthread_t t1;
+    pthread_create(&t1, 0, k, 0);
+
+    doit();
+    return 0;
+}

tests/regression/13-privatized/83-nondet-struct-ptr-write.c

@@ -0,0 +1,54 @@
+// PARAM: --set ana.base.privatization write --enable ana.int.enums
+#include<pthread.h>
+#include<stdlib.h>
+struct a {
+  int b;
+};
+
+struct a *ptr;
+struct a *straightandnarrow;
+
+pthread_mutex_t m;
+
+void doit() {
+  void *newa = malloc(sizeof(struct a));
+
+  pthread_mutex_lock(&m);
+  ptr->b = 5;
+
+  int fear = straightandnarrow->b;
+  __goblint_check(fear == 5); //UNKNOWN!
+
+  ptr = newa;
+  pthread_mutex_unlock(&m);
+
+  pthread_mutex_lock(&m);
+  int hope = straightandnarrow->b;
+  __goblint_check(hope == 5); //UNKNOWN!
+  pthread_mutex_unlock(&m);
+
+}
+
+void* k(void *arg) {
+  doit();
+  return NULL;
+}
+
+int main() {
+    int top;
+    struct a other = { 0 };
+    struct a other2 = { 42 };
+    if(top) {
+      ptr = &other;
+    } else {
+      ptr = &other2;
+    }
+
+    straightandnarrow = &other;
+
+    pthread_t t1;
+    pthread_create(&t1, 0, k, 0);
+
+    doit();
+    return 0;
+}

tests/regression/13-privatized/84-nondet-local-pointer-write.c

@@ -0,0 +1,54 @@
+// PARAM: --set ana.base.privatization write --enable ana.int.enums
+#include<pthread.h>
+#include<stdlib.h>
+struct a {
+  int b;
+};
+
+int *ptr;
+int *immer_da_oane;
+
+pthread_mutex_t m;
+
+void doit() {
+  pthread_mutex_lock(&m);
+  *ptr = 5;
+
+  // Should be either 5 or 0, depending on which one the pointer points to
+  int fear = *immer_da_oane;
+  __goblint_check(fear == 5); //UNKNOWN!
+
+  pthread_mutex_unlock(&m);
+
+  pthread_mutex_lock(&m);
+  int hope = *immer_da_oane;
+  __goblint_check(hope == 5); //UNKNOWN!
+  pthread_mutex_unlock(&m);
+
+}
+
+void* k(void *arg) {
+  // Force MT
+  return NULL;
+}
+
+int main() {
+    int top;
+
+    int da_oane = 0;
+    int de_andre = 42;
+
+    if(top) {
+      ptr = &da_oane;
+    } else {
+      ptr = &de_andre;
+    }
+
+    immer_da_oane = &da_oane;
+
+    pthread_t t1;
+    pthread_create(&t1, 0, k, 0);
+
+    doit();
+    return 0;
+}

tests/regression/13-privatized/85-nondet-global-pointer-write.c

@@ -0,0 +1,55 @@
+// PARAM: --set ana.base.privatization write --enable ana.int.enums
+#include<pthread.h>
+#include<stdlib.h>
+struct a {
+  int b;
+};
+
+int *ptr;
+int *immer_da_oane;
+
+int da_oane = 0;
+int de_andre = 42;
+
+pthread_mutex_t m;
+
+void doit() {
+  pthread_mutex_lock(&m);
+  *ptr = 5;
+
+  // Should be either 0 or 5, depending on which one ptr points to
+  int fear = *immer_da_oane;
+  __goblint_check(fear == 5); //UNKNOWN!
+
+  pthread_mutex_unlock(&m);
+
+  pthread_mutex_lock(&m);
+  // This works
+  int hope = *immer_da_oane;
+  __goblint_check(hope == 5); //UNKNOWN!
+  pthread_mutex_unlock(&m);
+
+}
+
+void* k(void *arg) {
+  // Force MT
+  return NULL;
+}
+
+int main() {
+    int top;
+
+    if(top) {
+      ptr = &da_oane;
+    } else {
+      ptr = &de_andre;
+    }
+
+    immer_da_oane = &da_oane;
+
+    pthread_t t1;
+    pthread_create(&t1, 0, k, 0);
+
+    doit();
+    return 0;
+}

tests/regression/13-privatized/86-nondet-struct-ptr-lock.c

@@ -0,0 +1,54 @@
+// PARAM: --set ana.base.privatization lock --enable ana.int.enums
+#include<pthread.h>
+#include<stdlib.h>
+struct a {
+  int b;
+};
+
+struct a *ptr;
+struct a *straightandnarrow;
+
+pthread_mutex_t m;
+
+void doit() {
+  void *newa = malloc(sizeof(struct a));
+
+  pthread_mutex_lock(&m);
+  ptr->b = 5;
+
+  int fear = straightandnarrow->b;
+  __goblint_check(fear == 5); //UNKNOWN!
+
+  ptr = newa;
+  pthread_mutex_unlock(&m);
+
+  pthread_mutex_lock(&m);
+  int hope = straightandnarrow->b;
+  __goblint_check(hope == 5); //UNKNOWN!
+  pthread_mutex_unlock(&m);
+
+}
+
+void* k(void *arg) {
+  doit();
+  return NULL;
+}
+
+int main() {
+    int top;
+    struct a other = { 0 };
+    struct a other2 = { 42 };
+    if(top) {
+      ptr = &other;
+    } else {
+      ptr = &other2;
+    }
+
+    straightandnarrow = &other;
+
+    pthread_t t1;
+    pthread_create(&t1, 0, k, 0);
+
+    doit();
+    return 0;
+}