From e69d13c0cd4cf73a9bbda511627ee1844a39bbbc Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 18 Sep 2023 11:49:06 +0300 Subject: [PATCH 1/2] Add thread self creation non-terminating test from libaco --- tests/regression/10-synch/07-thread_self_create.c | 15 +++++++++++++++ 1 file changed, 15 insertions(+) create mode 100644 tests/regression/10-synch/07-thread_self_create.c diff --git a/tests/regression/10-synch/07-thread_self_create.c b/tests/regression/10-synch/07-thread_self_create.c new file mode 100644 index 0000000000..473a26a25b --- /dev/null +++ b/tests/regression/10-synch/07-thread_self_create.c @@ -0,0 +1,15 @@ +// PARAM: --set ana.activated[+] thread +// Checks termination of thread analysis with a thread who is its own single parent. +#include + +void *t_fun(void *arg) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + return 0; +} From 2486404315e4e7d44512134637d1eaff78def99e Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 18 Sep 2023 11:55:59 +0300 Subject: [PATCH 2/2] Fix 10-synch/07-thread_self_create --- src/analyses/threadAnalysis.ml | 22 +++++++++++++++------- 1 file changed, 15 insertions(+), 7 deletions(-) diff --git a/src/analyses/threadAnalysis.ml b/src/analyses/threadAnalysis.ml index d6a93744bc..1e679a4707 100644 --- a/src/analyses/threadAnalysis.ml +++ b/src/analyses/threadAnalysis.ml @@ -32,13 +32,21 @@ struct let rec is_not_unique ctx tid = let (rep, parents, _) = ctx.global tid in - let n = TS.cardinal parents in - (* A thread is not unique if it is - * a) repeatedly created, - * b) created in multiple threads, or - * c) created by a thread that is itself multiply created. - * Note that starting threads have empty ancestor sets! *) - rep || n > 1 || n > 0 && is_not_unique ctx (TS.choose parents) + if rep then + true (* repeatedly created *) + else ( + let n = TS.cardinal parents in + if n > 1 then + true (* created in multiple threads *) + else if n > 0 then ( + (* created by single thread *) + let parent = TS.choose parents in + (* created by itself thread-recursively or by a thread that is itself multiply created *) + T.equal tid parent || is_not_unique ctx parent (* equal check needed to avoid infinte self-recursion *) + ) + else + false (* no ancestors, starting thread *) + ) let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t = let desc = LibraryFunctions.find f in