From c0d51c321042153900101d7cf92b489cf119e425 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sun, 3 Nov 2024 17:24:42 +0100 Subject: [PATCH 1/3] Fix `thread` for non-unique spawns --- src/analyses/threadAnalysis.ml | 10 +++--- .../40-threadid/12-multiple-created-only.c | 26 ++++++++++++++++ tests/regression/40-threadid/13-no-crash.c | 31 +++++++++++++++++++ 3 files changed, 61 insertions(+), 6 deletions(-) create mode 100644 tests/regression/40-threadid/12-multiple-created-only.c create mode 100644 tests/regression/40-threadid/13-no-crash.c diff --git a/src/analyses/threadAnalysis.ml b/src/analyses/threadAnalysis.ml index 07f46e915d..a67c26092c 100644 --- a/src/analyses/threadAnalysis.ml +++ b/src/analyses/threadAnalysis.ml @@ -95,9 +95,7 @@ struct let startstate v = D.bot () let threadenter ctx ~multiple lval f args = - if multiple then - (let tid = ThreadId.get_current_unlift (Analyses.ask_of_ctx ctx) in - ctx.sideg tid (true, TS.bot (), false)); + (* ctx is of creator, side-effects to denote non-uniqueness are performed in threadspawn *) [D.bot ()] let threadspawn ctx ~multiple lval f args fctx = @@ -106,9 +104,9 @@ struct let repeated = D.mem tid ctx.local in let eff = match creator with - | `Lifted ctid -> (repeated, TS.singleton ctid, false) - | `Top -> (true, TS.bot (), false) - | `Bot -> (false, TS.bot (), false) + | `Lifted ctid -> (repeated || multiple, TS.singleton ctid, false) + | `Top -> (true, TS.bot (), false) + | `Bot -> (false || multiple, TS.bot (), false) in ctx.sideg tid eff; D.join ctx.local (D.singleton tid) diff --git a/tests/regression/40-threadid/12-multiple-created-only.c b/tests/regression/40-threadid/12-multiple-created-only.c new file mode 100644 index 0000000000..e65021caaf --- /dev/null +++ b/tests/regression/40-threadid/12-multiple-created-only.c @@ -0,0 +1,26 @@ +// PARAM: --set ana.activated[+] thread --set ana.activated[+] threadid --set ana.thread.domain plain + +#include +#include + +int myglobal; +int myglobal2; + +void* bla(void *arg) { + // This is created multiple times, it should race with itself + myglobal = 10; //RACE + return NULL; +} + +void* other(void) { + // This is created only once, it should not be marked as non-unique + unknown(bla); + myglobal2 = 30; //NORACE +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, other, NULL); + + return 0; +} diff --git a/tests/regression/40-threadid/13-no-crash.c b/tests/regression/40-threadid/13-no-crash.c new file mode 100644 index 0000000000..c9a6c7d88b --- /dev/null +++ b/tests/regression/40-threadid/13-no-crash.c @@ -0,0 +1,31 @@ +// PARAM: --set ana.context.gas_value 0 --set ana.activated[+] thread --set ana.activated[+] threadid + +#include +#include + +int myglobal; +int myglobal2; + +void *t_flurb(void *arg) { + myglobal=40; //RACE + return NULL; +} + +void* bla(void *arg) { + return NULL; +} + +void *t_fun(void *arg) { + unknown(t_flurb); // NOCRASH + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + pthread_create(&id, NULL, t_fun, NULL); + + unknown(bla); + + return 0; +} From 1bb50df301ddfd63b9a15677c3bf6f9cf5d026ff Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 4 Nov 2024 10:38:13 +0100 Subject: [PATCH 2/3] Use multiple also in bot case Co-authored-by: Simmo Saan --- src/analyses/threadAnalysis.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/threadAnalysis.ml b/src/analyses/threadAnalysis.ml index a67c26092c..435e1a6afe 100644 --- a/src/analyses/threadAnalysis.ml +++ b/src/analyses/threadAnalysis.ml @@ -106,7 +106,7 @@ struct match creator with | `Lifted ctid -> (repeated || multiple, TS.singleton ctid, false) | `Top -> (true, TS.bot (), false) - | `Bot -> (false || multiple, TS.bot (), false) + | `Bot -> (multiple, TS.bot (), false) in ctx.sideg tid eff; D.join ctx.local (D.singleton tid) From eb149f9520a05664bb1d7addd90d6a23f44f5832 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Mon, 4 Nov 2024 10:39:24 +0100 Subject: [PATCH 3/3] Move tests --- .../29-multiple-created-only.c} | 0 .../{40-threadid/13-no-crash.c => 10-synch/30-no-crash.c} | 0 2 files changed, 0 insertions(+), 0 deletions(-) rename tests/regression/{40-threadid/12-multiple-created-only.c => 10-synch/29-multiple-created-only.c} (100%) rename tests/regression/{40-threadid/13-no-crash.c => 10-synch/30-no-crash.c} (100%) diff --git a/tests/regression/40-threadid/12-multiple-created-only.c b/tests/regression/10-synch/29-multiple-created-only.c similarity index 100% rename from tests/regression/40-threadid/12-multiple-created-only.c rename to tests/regression/10-synch/29-multiple-created-only.c diff --git a/tests/regression/40-threadid/13-no-crash.c b/tests/regression/10-synch/30-no-crash.c similarity index 100% rename from tests/regression/40-threadid/13-no-crash.c rename to tests/regression/10-synch/30-no-crash.c