Skip to content

Commit

Permalink
Fix plain thread ID is_main unsoundness when ana.thread.include-node …
Browse files Browse the repository at this point in the history
…is disabled
  • Loading branch information
sim642 committed Oct 30, 2024
1 parent 568e97c commit 1bb8db1
Show file tree
Hide file tree
Showing 2 changed files with 30 additions and 1 deletion.
2 changes: 1 addition & 1 deletion src/cdomain/value/cdomains/threadIdDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
29 changes: 29 additions & 0 deletions tests/regression/51-threadjoins/11-join-main-plain-no-node.c
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
//PARAM: --set ana.activated[+] threadJoins --set ana.thread.domain plain --disable ana.thread.include-node
#include <pthread.h>
#include <stdio.h>

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

0 comments on commit 1bb8db1

Please sign in to comment.