Add problematic examples for #1457

Author: michael-schwarz

tests/regression/13-privatized/80-treachery-and-lies.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-how-could-we-have-been-so-blind.c

@@ -0,0 +1,55 @@
+// PARAM: --set ana.base.privatization protection --enable ana.int.enums
+// Like 80-treachery-and-lies.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-well-laid-out-plans.c

@@ -0,0 +1,56 @@
+// PARAM: --set ana.base.privatization protection --enable ana.int.enums
+// Like 81-how-could-we-have-been-so-blind.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-treachery-and-lies-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-how-could-we-have-been-so-blind-write.c

@@ -0,0 +1,55 @@
+// PARAM: --set ana.base.privatization write --enable ana.int.enums
+// Like 80-treachery-and-lies.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/85-well-laid-out-plans-write.c

@@ -0,0 +1,56 @@
+// PARAM: --set ana.base.privatization write --enable ana.int.enums
+// Like 81-how-could-we-have-been-so-blind.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/86-treachery-and-lies-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;
+}