From 8e54444f8fd5ee0e05780c59f09a2d76cfb433d7 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 15 Aug 2024 15:42:27 +0300 Subject: [PATCH] Construct feasible races-mhp regression tests for improved history thread ID may_create --- .../regression/53-races-mhp/04-not-created2.c | 25 +++++++++++++ .../regression/53-races-mhp/05-not-created3.c | 27 ++++++++++++++ .../regression/53-races-mhp/06-not-created4.c | 36 +++++++++++++++++++ .../regression/53-races-mhp/07-not-created5.c | 27 ++++++++++++++ .../regression/53-races-mhp/08-not-created6.c | 31 ++++++++++++++++ tests/unit/cdomains/threadIdDomainTest.ml | 26 +++++++------- 6 files changed, 159 insertions(+), 13 deletions(-) create mode 100644 tests/regression/53-races-mhp/04-not-created2.c create mode 100644 tests/regression/53-races-mhp/05-not-created3.c create mode 100644 tests/regression/53-races-mhp/06-not-created4.c create mode 100644 tests/regression/53-races-mhp/07-not-created5.c create mode 100644 tests/regression/53-races-mhp/08-not-created6.c diff --git a/tests/regression/53-races-mhp/04-not-created2.c b/tests/regression/53-races-mhp/04-not-created2.c new file mode 100644 index 0000000000..5bf2bff134 --- /dev/null +++ b/tests/regression/53-races-mhp/04-not-created2.c @@ -0,0 +1,25 @@ +// PARAM: --set ana.activated[+] mhp --disable ana.thread.include-node +#include + +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; +} diff --git a/tests/regression/53-races-mhp/05-not-created3.c b/tests/regression/53-races-mhp/05-not-created3.c new file mode 100644 index 0000000000..ab62f44fa1 --- /dev/null +++ b/tests/regression/53-races-mhp/05-not-created3.c @@ -0,0 +1,27 @@ +// PARAM: --set ana.activated[+] mhp --disable ana.thread.include-node +#include + +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; +} diff --git a/tests/regression/53-races-mhp/06-not-created4.c b/tests/regression/53-races-mhp/06-not-created4.c new file mode 100644 index 0000000000..87fe8c8a5b --- /dev/null +++ b/tests/regression/53-races-mhp/06-not-created4.c @@ -0,0 +1,36 @@ +// PARAM: --set ana.activated[+] mhp --disable ana.thread.include-node +#include + +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; +} diff --git a/tests/regression/53-races-mhp/07-not-created5.c b/tests/regression/53-races-mhp/07-not-created5.c new file mode 100644 index 0000000000..e096690720 --- /dev/null +++ b/tests/regression/53-races-mhp/07-not-created5.c @@ -0,0 +1,27 @@ +// PARAM: --set ana.activated[+] mhp --disable ana.thread.include-node +#include + +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; +} diff --git a/tests/regression/53-races-mhp/08-not-created6.c b/tests/regression/53-races-mhp/08-not-created6.c new file mode 100644 index 0000000000..73b5530efa --- /dev/null +++ b/tests/regression/53-races-mhp/08-not-created6.c @@ -0,0 +1,31 @@ +// PARAM: --set ana.activated[+] mhp --disable ana.thread.include-node +#include + +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; +} diff --git a/tests/unit/cdomains/threadIdDomainTest.ml b/tests/unit/cdomains/threadIdDomainTest.ml index 22b30c8c07..3e352738fd 100644 --- a/tests/unit/cdomains/threadIdDomainTest.ml +++ b/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? *)