Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Fix thread analysis termination with a self-creating thread #1173

Merged
merged 2 commits into from
Sep 19, 2023
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
22 changes: 15 additions & 7 deletions src/analyses/threadAnalysis.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
15 changes: 15 additions & 0 deletions tests/regression/10-synch/07-thread_self_create.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,15 @@
// PARAM: --set ana.activated[+] thread
// Checks termination of thread analysis with a thread who is its own single parent.
#include <pthread.h>

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;
}
Loading