From 3970a2fde041afba272b4a93e3a7c4a73f05cdca Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 28 Oct 2024 13:48:12 +0200 Subject: [PATCH 1/6] Add regression test for joining main thread --- .../regression/51-threadjoins/09-join-main.c | 23 +++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 tests/regression/51-threadjoins/09-join-main.c diff --git a/tests/regression/51-threadjoins/09-join-main.c b/tests/regression/51-threadjoins/09-join-main.c new file mode 100644 index 0000000000..249de594bf --- /dev/null +++ b/tests/regression/51-threadjoins/09-join-main.c @@ -0,0 +1,23 @@ +//PARAM: --set ana.activated[+] threadJoins +#include + +pthread_t mainid; + +int g = 10; + +void *t_fun(void *arg) { + pthread_join(mainid, NULL); + g++; // TODO NORACE + return NULL; +} + + +int main(void) { + mainid = pthread_self(); + + pthread_t id2; + pthread_create(&id2, NULL, t_fun, NULL); + + g++; // TODO NORACE + return 0; +} From 3d048eb1035479f26854a23402bb2aad0e53fd31 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 28 Oct 2024 13:48:37 +0200 Subject: [PATCH 2/6] Add pthread_self support --- src/analyses/base.ml | 9 +++++++++ src/util/library/libraryDesc.ml | 1 + src/util/library/libraryFunctions.ml | 2 +- tests/regression/51-threadjoins/09-join-main.c | 4 ++-- 4 files changed, 13 insertions(+), 3 deletions(-) diff --git a/src/analyses/base.ml b/src/analyses/base.ml index cea2c8bcee..e5bcbfede5 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2651,6 +2651,15 @@ struct | Unknown, "__goblint_assume_join" -> let id = List.hd args in Priv.thread_join ~force:true (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) id st + | ThreadSelf, _ -> + begin match lv, ThreadId.get_current (Analyses.ask_of_ctx ctx) with + | Some lv, `Lifted tid -> + set ~ctx st (eval_lv ~ctx st lv) (Cilfacade.typeOfLval lv) (Thread (ValueDomain.Threads.singleton tid)) + | Some lv, _ -> + invalidate_ret_lv st + | None, _ -> + st + end | Alloca size, _ -> begin match lv with | Some lv -> diff --git a/src/util/library/libraryDesc.ml b/src/util/library/libraryDesc.ml index 80cf86b1e2..6f34de1864 100644 --- a/src/util/library/libraryDesc.ml +++ b/src/util/library/libraryDesc.ml @@ -56,6 +56,7 @@ type special = | ThreadCreate of { thread: Cil.exp; start_routine: Cil.exp; arg: Cil.exp; multiple: bool } | ThreadJoin of { thread: Cil.exp; ret_var: Cil.exp; } | ThreadExit of { ret_val: Cil.exp; } + | ThreadSelf | Globalize of Cil.exp | Signal of Cil.exp | Broadcast of Cil.exp diff --git a/src/util/library/libraryFunctions.ml b/src/util/library/libraryFunctions.ml index 31fcf0510e..fbcaa4fe60 100644 --- a/src/util/library/libraryFunctions.ml +++ b/src/util/library/libraryFunctions.ml @@ -504,7 +504,7 @@ let pthread_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[ ("pthread_attr_setstacksize", unknown [drop "attr" [w]; drop "stacksize" []]); ("pthread_attr_getscope", unknown [drop "attr" [r]; drop "scope" [w]]); ("pthread_attr_setscope", unknown [drop "attr" [w]; drop "scope" []]); - ("pthread_self", unknown []); + ("pthread_self", special [] ThreadSelf); ("pthread_sigmask", unknown [drop "how" []; drop "set" [r]; drop "oldset" [w]]); ("pthread_setspecific", unknown ~attrs:[InvalidateGlobals] [drop "key" []; drop "value" [w_deep]]); ("pthread_getspecific", unknown ~attrs:[InvalidateGlobals] [drop "key" []]); diff --git a/tests/regression/51-threadjoins/09-join-main.c b/tests/regression/51-threadjoins/09-join-main.c index 249de594bf..1d61eedf89 100644 --- a/tests/regression/51-threadjoins/09-join-main.c +++ b/tests/regression/51-threadjoins/09-join-main.c @@ -7,7 +7,7 @@ int g = 10; void *t_fun(void *arg) { pthread_join(mainid, NULL); - g++; // TODO NORACE + g++; // NORACE return NULL; } @@ -18,6 +18,6 @@ int main(void) { pthread_t id2; pthread_create(&id2, NULL, t_fun, NULL); - g++; // TODO NORACE + g++; // NORACE return 0; } From 01bff20b3fea1bb077c12ba9b0b7d7eba6d27c72 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 28 Oct 2024 14:00:52 +0200 Subject: [PATCH 3/6] Make 51-threadjoins/09-join-main runnable --- tests/regression/51-threadjoins/09-join-main.c | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/tests/regression/51-threadjoins/09-join-main.c b/tests/regression/51-threadjoins/09-join-main.c index 1d61eedf89..196ef8bc00 100644 --- a/tests/regression/51-threadjoins/09-join-main.c +++ b/tests/regression/51-threadjoins/09-join-main.c @@ -1,13 +1,16 @@ //PARAM: --set ana.activated[+] threadJoins #include +#include pthread_t mainid; int g = 10; void *t_fun(void *arg) { - pthread_join(mainid, NULL); + int r = pthread_join(mainid, NULL); // TSan doesn't like this... + printf("j: %d\n", r); g++; // NORACE + printf("t_fun: %d\n", g); return NULL; } @@ -19,5 +22,8 @@ int main(void) { pthread_create(&id2, NULL, t_fun, NULL); g++; // NORACE + printf("main: %d\n", g); + + pthread_exit(NULL); // exit main thread but keep id2 alive, otherwise main returning kills id2 return 0; } From bdc288e9706d3bfd0ae09785b891bc545ac3225e Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 28 Oct 2024 15:27:55 +0200 Subject: [PATCH 4/6] Copy 51-threadjoins/09-join-main for plain thread IDs --- .../51-threadjoins/10-join-main-plain.c | 29 +++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 tests/regression/51-threadjoins/10-join-main-plain.c diff --git a/tests/regression/51-threadjoins/10-join-main-plain.c b/tests/regression/51-threadjoins/10-join-main-plain.c new file mode 100644 index 0000000000..8bcb2b3a79 --- /dev/null +++ b/tests/regression/51-threadjoins/10-join-main-plain.c @@ -0,0 +1,29 @@ +//PARAM: --set ana.activated[+] threadJoins --set ana.thread.domain plain +#include +#include + +pthread_t mainid; + +int g = 10; + +void *t_fun(void *arg) { + int r = pthread_join(mainid, NULL); // TSan doesn't like this... + printf("j: %d\n", r); + g++; // RACE (imprecise by plain thread IDs) + printf("t_fun: %d\n", g); + return NULL; +} + + +int main(void) { + mainid = pthread_self(); + + pthread_t id2; + pthread_create(&id2, NULL, t_fun, NULL); + + g++; // TODO NORACE + printf("main: %d\n", g); + + pthread_exit(NULL); // exit main thread but keep id2 alive, otherwise main returning kills id2 + return 0; +} From 568e97cf331e7b0cd0b7b035dadaa198435867a6 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 28 Oct 2024 15:29:04 +0200 Subject: [PATCH 5/6] Improve plain thread ID is_unique --- src/cdomain/value/cdomains/threadIdDomain.ml | 2 +- tests/regression/51-threadjoins/10-join-main-plain.c | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml index fff6734f27..290a6b316b 100644 --- a/src/cdomain/value/cdomains/threadIdDomain.ml +++ b/src/cdomain/value/cdomains/threadIdDomain.ml @@ -86,7 +86,7 @@ struct | ({vname; _}, None) -> List.mem vname @@ GobConfig.get_string_list "mainfun" | _ -> false - let is_unique _ = false (* TODO: should this consider main unique? *) + let is_unique = is_main let may_create _ _ = true let is_must_parent _ _ = false end diff --git a/tests/regression/51-threadjoins/10-join-main-plain.c b/tests/regression/51-threadjoins/10-join-main-plain.c index 8bcb2b3a79..5b2c188bf5 100644 --- a/tests/regression/51-threadjoins/10-join-main-plain.c +++ b/tests/regression/51-threadjoins/10-join-main-plain.c @@ -21,7 +21,7 @@ int main(void) { pthread_t id2; pthread_create(&id2, NULL, t_fun, NULL); - g++; // TODO NORACE + g++; // NORACE printf("main: %d\n", g); pthread_exit(NULL); // exit main thread but keep id2 alive, otherwise main returning kills id2 From 1bb8db120146e371451cd3b1c34bfcf2d44e798b Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 30 Oct 2024 15:36:48 +0200 Subject: [PATCH 6/6] Fix plain thread ID is_main unsoundness when ana.thread.include-node is disabled --- src/cdomain/value/cdomains/threadIdDomain.ml | 2 +- .../11-join-main-plain-no-node.c | 29 +++++++++++++++++++ 2 files changed, 30 insertions(+), 1 deletion(-) create mode 100644 tests/regression/51-threadjoins/11-join-main-plain-no-node.c diff --git a/src/cdomain/value/cdomains/threadIdDomain.ml b/src/cdomain/value/cdomains/threadIdDomain.ml index 290a6b316b..226905ed6f 100644 --- a/src/cdomain/value/cdomains/threadIdDomain.ml +++ b/src/cdomain/value/cdomains/threadIdDomain.ml @@ -83,7 +83,7 @@ struct (v, None) let is_main = function - | ({vname; _}, None) -> List.mem vname @@ GobConfig.get_string_list "mainfun" + | ({vname; _}, None) -> GobConfig.get_bool "ana.thread.include-node" && List.mem vname @@ GobConfig.get_string_list "mainfun" | _ -> false let is_unique = is_main diff --git a/tests/regression/51-threadjoins/11-join-main-plain-no-node.c b/tests/regression/51-threadjoins/11-join-main-plain-no-node.c new file mode 100644 index 0000000000..7f235fd1d8 --- /dev/null +++ b/tests/regression/51-threadjoins/11-join-main-plain-no-node.c @@ -0,0 +1,29 @@ +//PARAM: --set ana.activated[+] threadJoins --set ana.thread.domain plain --disable ana.thread.include-node +#include +#include + +pthread_t mainid; + +int g = 10; + +void *t_fun(void *arg) { + int r = pthread_join(mainid, NULL); // TSan doesn't like this... + printf("j: %d\n", r); + g++; // RACE (imprecise by plain thread IDs) + printf("t_fun: %d\n", g); + return NULL; +} + + +int main(void) { + mainid = pthread_self(); + + pthread_t id2; + pthread_create(&id2, NULL, t_fun, NULL); + + g++; // RACE (imprecise by plain thread IDs not knowing if main is actual main or spawned by program) + printf("main: %d\n", g); + + pthread_exit(NULL); // exit main thread but keep id2 alive, otherwise main returning kills id2 + return 0; +}