Construct feasible races-mhp regression tests for improved history thread ID may_create

Author: sim642

tests/regression/53-races-mhp/04-not-created2.c

@@ -0,0 +1,25 @@
+// PARAM: --set ana.activated[+] mhp --disable ana.thread.include-node
+#include <pthread.h>
+
+int g;
+
+void *b(void *arg) {
+  int *gp = arg;
+  if (gp)
+    (*gp)++; // NORACE
+  return NULL;
+}
+
+void *a(void *arg) {
+  pthread_t id;
+  pthread_create(&id, NULL, b, arg);
+  return NULL;
+}
+
+int main() {
+  pthread_t id, id2;
+  pthread_create(&id, NULL, b, NULL);
+  g++; // NORACE
+  pthread_create(&id2, NULL, a, &g);
+  return 0;
+}

tests/regression/53-races-mhp/05-not-created3.c

@@ -0,0 +1,27 @@
+// PARAM: --set ana.activated[+] mhp --disable ana.thread.include-node
+#include <pthread.h>
+
+int g;
+
+void *a(void *arg) {
+  int *gp = arg;
+  if (gp)
+    (*gp)++; // RACE (self-race in non-unique thread)
+  return NULL;
+}
+
+void *b(void *arg) {
+  pthread_t id, id2;
+  pthread_create(&id, NULL, a, NULL);
+  pthread_create(&id2, NULL, a, &g);
+  return NULL;
+}
+
+
+int main() {
+  pthread_t id, id2;
+  pthread_create(&id, NULL, a, NULL);
+  g++; // NORACE
+  pthread_create(&id2, NULL, b, NULL);
+  return 0;
+}

tests/regression/53-races-mhp/06-not-created4.c

@@ -0,0 +1,36 @@
+// PARAM: --set ana.activated[+] mhp --disable ana.thread.include-node
+#include <pthread.h>
+
+int g;
+
+void *d(void *arg) {
+  int *gp = arg;
+  if (gp)
+    (*gp)++; // RACE (self-race in non-unique thread)
+  return NULL;
+}
+
+void *c(void *arg) {
+  pthread_t id, id2;
+  pthread_create(&id, NULL, d, NULL);
+  pthread_create(&id2, NULL, d, &g);
+  return NULL;
+}
+
+void *b(void *arg) {
+  return NULL;
+}
+
+void *a(void *arg) {
+  pthread_t id, id2;
+  pthread_create(&id, NULL, b, NULL);
+  g++; // NORACE
+  pthread_create(&id2, NULL, c, NULL);
+  return NULL;
+}
+
+int main() {
+  pthread_t id;
+  pthread_create(&id, NULL, a, NULL);
+  return 0;
+}

tests/regression/53-races-mhp/07-not-created5.c

@@ -0,0 +1,27 @@
+// PARAM: --set ana.activated[+] mhp --disable ana.thread.include-node
+#include <pthread.h>
+
+int g;
+
+void *a(void *arg) {
+  int *gp = arg;
+  if (gp)
+    (*gp)++; // RACE (self-race in non-unique thread)
+  return NULL;
+}
+
+void *b(void *arg) {
+  pthread_t id, id2;
+  pthread_create(&id, NULL, a, NULL);
+  pthread_create(&id2, NULL, a, &g);
+  return NULL;
+}
+
+int main() {
+  pthread_t id, id2, id3;
+  pthread_create(&id, NULL, a, NULL);
+  pthread_create(&id, NULL, a, NULL);
+  g++; // NORACE
+  pthread_create(&id, NULL, b, NULL);
+  return 0;
+}

tests/regression/53-races-mhp/08-not-created6.c

@@ -0,0 +1,31 @@
+// PARAM: --set ana.activated[+] mhp --disable ana.thread.include-node
+#include <pthread.h>
+
+int g;
+
+void *b(void *arg) {
+  return NULL;
+}
+
+void *c(void *arg) {
+  int *gp = arg;
+  if (gp)
+    (*gp)++; // RACE (self-race in non-unique thread)
+  return NULL;
+}
+
+void *a(void *arg) {
+  pthread_t id, id2, id3, id4;
+  pthread_create(&id, NULL, b, NULL);
+  pthread_create(&id2, NULL, b, NULL);
+  g++; // NORACE
+  pthread_create(&id, NULL, c, NULL);
+  pthread_create(&id2, NULL, c, &g);
+  return NULL;
+}
+
+int main() {
+  pthread_t id;
+  pthread_create(&id, NULL, a, NULL);
+  return 0;
+}

tests/unit/cdomains/threadIdDomainTest.ml

@@ -50,9 +50,9 @@ let test_history_may_create _ =
   assert_equal true (may_create main (main >> a));
   assert_equal true (may_create main (main >> a >> b));
   assert_equal true (may_create (main >> a) (main >> a >> b));
-  assert_equal false (may_create (main >> a) (main >> a));
-  assert_equal false (may_create (main >> b) (main >> a >> b));
-  assert_equal false (may_create (main >> a >> a) (main >> a >> b));
+  assert_equal false (may_create (main >> a) (main >> a)); (* infeasible for race: definitely_not_started allows equality *)
+  assert_equal false (may_create (main >> b) (main >> a >> b)); (* 53-races-mhp/04-not-created2 *)
+  assert_equal false (may_create (main >> a >> a) (main >> a >> b)); (* infeasible for race: cannot create non-unique (main >> a >> a) before unique (main >> a >> b) *)
 
   (* unique creates non-unique and is prefix: added elements cannot be in prefix *)
   assert_equal true (may_create main (main >> a >> a));
@@ -64,22 +64,22 @@ let test_history_may_create _ =
   assert_equal true (may_create (main >> a) (main >> a >> a));
   assert_equal true (may_create (main >> a >> b) (main >> a >> b >> b));
   assert_equal true (may_create (main >> a >> b) (main >> a >> b >> a));
-  assert_equal false (may_create (main >> a >> b) (main >> a >> a));
-  assert_equal false (may_create (main >> a >> b) (main >> b >> b));
+  assert_equal false (may_create (main >> a >> b) (main >> a >> a)); (* infeasible for race: definitely_not_started requires (main >> a), where this must happen, to be must parent for (main >> a >> a), which it is not *)
+  assert_equal false (may_create (main >> a >> b) (main >> b >> b)); (* infeasible for race: definitely_not_started requires (main >> a), where this must happen, to be must parent for (main >> b >> b), which it is not *)
 
   (* unique creates non-unique and prefixes are incompatible *)
-  assert_equal false (may_create (main >> a) (main >> b >> a >> a));
-  assert_equal false (may_create (main >> a >> b) (main >> b >> a >> c >> c));
-  assert_equal false (may_create (main >> a >> b) (main >> a >> c >> d >> d));
+  assert_equal false (may_create (main >> a) (main >> b >> a >> a)); (* 53-races-mhp/05-not-created3 *)
+  assert_equal false (may_create (main >> a >> b) (main >> b >> a >> c >> c)); (* infeasible for race: definitely_not_started requires (main >> a), where this must happen, to be must parent for (main >> b >> a >> c >> c), which it is not *)
+  assert_equal false (may_create (main >> a >> b) (main >> a >> c >> d >> d)); (* 53-races-mhp/06-not-created4, also passes with simple may_create *)
 
   (* non-unique creates non-unique: prefix must not lengthen *)
-  assert_equal false (may_create (main >> a >> a) (main >> a >> b >> b));
-  assert_equal false (may_create (main >> a >> a) (main >> b >> a >> a));
+  assert_equal false (may_create (main >> a >> a) (main >> a >> b >> b)); (* infeasible for race: cannot create non-unique (main >> a >> a) before unique prefix-ed (main >> a >> b >> b) *)
+  assert_equal false (may_create (main >> a >> a) (main >> b >> a >> a)); (* 53-races-mhp/07-not-created5 *)
   (* non-unique creates non-unique: prefix must be compatible *)
-  assert_equal false (may_create (main >> a >> b >> c >> c) (main >> b >> a >> c >> c));
+  assert_equal false (may_create (main >> a >> b >> c >> c) (main >> b >> a >> c >> c)); (* infeasible for race: definitely_not_started requires (main >> a >> b or main >> a >> b >> c), where this must happen, to be must parent for (main >> b >> a >> c >> c), which it is not *)
   (* non-unique creates non-unique: elements must not be removed *)
-  assert_equal false (may_create (main >> a >> b >> b) (main >> a >> c >> c)); (* from set *)
-  assert_equal false (may_create (main >> a >> b >> b) (main >> b >> b)); (* from prefix *)
+  assert_equal false (may_create (main >> a >> b >> b) (main >> a >> c >> c)); (* from set *) (* 53-races-mhp/08-not-created6, also passes with simple may_create *)
+  assert_equal false (may_create (main >> a >> b >> b) (main >> b >> b)); (* from prefix *) (* infeasible for race: definitely_not_started requires (main >> a or main >> a >> b), where this must happen, to be must parent for (main >> b >> b), which it is not *)
   (* non-unique creates non-unique: removed elements and set must be in new set *)
   (* assert_equal false (may_create (main >> a >> b >> c >> c) (main >> a >> c >> c)); *)
   (* TODO: cannot test due because by construction after prefix check? *)