From fb7159c0fe7aa1e0ed887f807db7feb3c9699114 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sat, 16 Sep 2023 16:33:40 +0200 Subject: [PATCH 1/2] Add some setjump/longjump test for race detection --- tests/regression/68-longjmp/52-races.c | 36 +++++++++++++ tests/regression/68-longjmp/53-races-no.c | 37 ++++++++++++++ .../regression/68-longjmp/54-races-actually.c | 51 +++++++++++++++++++ .../68-longjmp/55-races-no-return.c | 51 +++++++++++++++++++ 4 files changed, 175 insertions(+) create mode 100644 tests/regression/68-longjmp/52-races.c create mode 100644 tests/regression/68-longjmp/53-races-no.c create mode 100644 tests/regression/68-longjmp/54-races-actually.c create mode 100644 tests/regression/68-longjmp/55-races-no-return.c diff --git a/tests/regression/68-longjmp/52-races.c b/tests/regression/68-longjmp/52-races.c new file mode 100644 index 0000000000..5c7ac6daa6 --- /dev/null +++ b/tests/regression/68-longjmp/52-races.c @@ -0,0 +1,36 @@ +// PARAM: --enable ana.int.interval +#include +#include +#include +#include +#include + +jmp_buf env_buffer; +int global = 0; +pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; + +void *t_fun(void *arg) { + pthread_mutex_lock(&mutex1); + global = 3; // NORACE + pthread_mutex_unlock(&mutex1); + return NULL; +} + +int bar() { + pthread_mutex_lock(&mutex1); + longjmp(env_buffer, 2); + pthread_mutex_unlock(&mutex1); + return 8; +} + +int main() { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + + if(!setjmp( env_buffer )) { + bar(); + } + + global = 5; // NORACE + pthread_mutex_unlock(&mutex1); +} diff --git a/tests/regression/68-longjmp/53-races-no.c b/tests/regression/68-longjmp/53-races-no.c new file mode 100644 index 0000000000..7247f14941 --- /dev/null +++ b/tests/regression/68-longjmp/53-races-no.c @@ -0,0 +1,37 @@ +// PARAM: --enable ana.int.interval +#include +#include +#include +#include +#include + +jmp_buf env_buffer; +int global = 0; +pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; + +void *t_fun(void *arg) { + pthread_mutex_lock(&mutex1); + global = 3; // NORACE + pthread_mutex_unlock(&mutex1); + return NULL; +} + +int bar() { + pthread_mutex_lock(&mutex1); + if(global ==3) { + longjmp(env_buffer, 2); + } + return 8; +} + +int main() { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + + if(!setjmp( env_buffer )) { + bar(); + } + + global = 5; // NORACE + pthread_mutex_unlock(&mutex1); +} diff --git a/tests/regression/68-longjmp/54-races-actually.c b/tests/regression/68-longjmp/54-races-actually.c new file mode 100644 index 0000000000..12f1f791c5 --- /dev/null +++ b/tests/regression/68-longjmp/54-races-actually.c @@ -0,0 +1,51 @@ +// PARAM: --enable ana.int.interval +#include +#include +#include +#include +#include + +jmp_buf env_buffer; +int global = 0; +pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; + +void *t_fun(void *arg) { + pthread_mutex_lock(&mutex1); + global = 3; // RACE + pthread_mutex_unlock(&mutex1); + return NULL; +} + +int bar() { + pthread_mutex_lock(&mutex1); + if(global == 3) { + longjmp(env_buffer, 2); + } else { + longjmp(env_buffer, 4); + } + return 8; +} + +int main() { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + int n = 0; + + switch(setjmp( env_buffer )) { + case 0: + bar(); + break; + case 2: + n=1; + pthread_mutex_unlock(&mutex1); + break; + default: + break; + } + + global = 5; //RACE + + if(n == 0) { + pthread_mutex_unlock(&mutex1); + } +} diff --git a/tests/regression/68-longjmp/55-races-no-return.c b/tests/regression/68-longjmp/55-races-no-return.c new file mode 100644 index 0000000000..ad0e5d4707 --- /dev/null +++ b/tests/regression/68-longjmp/55-races-no-return.c @@ -0,0 +1,51 @@ +// PARAM: --enable ana.int.interval +#include +#include +#include +#include +#include + +jmp_buf env_buffer; +int global = 0; +pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER; + +void *t_fun(void *arg) { + pthread_mutex_lock(&mutex1); + global = 3; //NORACE + pthread_mutex_unlock(&mutex1); + return NULL; +} + +int bar() { + pthread_mutex_lock(&mutex1); + if(global == 7) { + longjmp(env_buffer, 2); + } else { + longjmp(env_buffer, 4); + } + return 8; +} + +int main() { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + int n = 0; + + switch(setjmp( env_buffer )) { + case 0: + bar(); + break; + case 2: + n=1; + pthread_mutex_unlock(&mutex1); + break; + default: + break; + } + + global = 5; //NORACE + + if(n == 0) { + pthread_mutex_unlock(&mutex1); + } +} From 18fe6d1b55fb54f193e1b5ce8506c937ce2d571d Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sat, 16 Sep 2023 16:47:51 +0200 Subject: [PATCH 2/2] 68/[52-55] Don't include `goblint.h`, it is unused --- tests/regression/68-longjmp/52-races.c | 1 - tests/regression/68-longjmp/53-races-no.c | 1 - tests/regression/68-longjmp/54-races-actually.c | 3 +-- tests/regression/68-longjmp/55-races-no-return.c | 1 - 4 files changed, 1 insertion(+), 5 deletions(-) diff --git a/tests/regression/68-longjmp/52-races.c b/tests/regression/68-longjmp/52-races.c index 5c7ac6daa6..4cde97d954 100644 --- a/tests/regression/68-longjmp/52-races.c +++ b/tests/regression/68-longjmp/52-races.c @@ -2,7 +2,6 @@ #include #include #include -#include #include jmp_buf env_buffer; diff --git a/tests/regression/68-longjmp/53-races-no.c b/tests/regression/68-longjmp/53-races-no.c index 7247f14941..4692f6ca18 100644 --- a/tests/regression/68-longjmp/53-races-no.c +++ b/tests/regression/68-longjmp/53-races-no.c @@ -2,7 +2,6 @@ #include #include #include -#include #include jmp_buf env_buffer; diff --git a/tests/regression/68-longjmp/54-races-actually.c b/tests/regression/68-longjmp/54-races-actually.c index 12f1f791c5..62423cd884 100644 --- a/tests/regression/68-longjmp/54-races-actually.c +++ b/tests/regression/68-longjmp/54-races-actually.c @@ -2,7 +2,6 @@ #include #include #include -#include #include jmp_buf env_buffer; @@ -44,7 +43,7 @@ int main() { } global = 5; //RACE - + if(n == 0) { pthread_mutex_unlock(&mutex1); } diff --git a/tests/regression/68-longjmp/55-races-no-return.c b/tests/regression/68-longjmp/55-races-no-return.c index ad0e5d4707..850fc54fa5 100644 --- a/tests/regression/68-longjmp/55-races-no-return.c +++ b/tests/regression/68-longjmp/55-races-no-return.c @@ -2,7 +2,6 @@ #include #include #include -#include #include jmp_buf env_buffer;