From 4be9ab0c429f83a25703df3e3ebaeb55152025f8 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Thu, 10 Jun 2021 18:08:35 +0200 Subject: [PATCH 01/12] Add test for local that escapes after thread creation --- .../37-escape/01-local-in-pthread.c | 29 +++++++++++++++++++ 1 file changed, 29 insertions(+) create mode 100644 tests/regression/37-escape/01-local-in-pthread.c diff --git a/tests/regression/37-escape/01-local-in-pthread.c b/tests/regression/37-escape/01-local-in-pthread.c new file mode 100644 index 0000000000..8157b55b3a --- /dev/null +++ b/tests/regression/37-escape/01-local-in-pthread.c @@ -0,0 +1,29 @@ +#include +#include + +#include +#include +#include + + +void *foo(void* p){ + sleep(2); + int* ip = *((int**) p); + printf("ip is %d\n", *ip); + *ip = 42; + return NULL; +} + +int main(){ + int x = 0; + int *xp = &x; + int** ptr = &xp; + int x2 = 35; + pthread_t thread; + pthread_create(&thread, NULL, foo, ptr); + *ptr = &x2; + sleep(4); // to make sure that we actually fail the assert when running. + assert(x2 == 35); // UNKNOWN! + pthread_join(thread, NULL); + return 0; +} From 9be146c0224f6169d620ebed53cbab87631a18d7 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 11 Jun 2021 10:58:50 +0200 Subject: [PATCH 02/12] Example of escaping via global --- .../regression/37-escape/02-local-in-global.c | 20 +++++++++++++++++++ 1 file changed, 20 insertions(+) create mode 100644 tests/regression/37-escape/02-local-in-global.c diff --git a/tests/regression/37-escape/02-local-in-global.c b/tests/regression/37-escape/02-local-in-global.c new file mode 100644 index 0000000000..bca91393fd --- /dev/null +++ b/tests/regression/37-escape/02-local-in-global.c @@ -0,0 +1,20 @@ +#include +#include + +int* gptr; + +void *foo(void* p){ + *gptr = 17; + return NULL; +} + +int main(){ + int x = 0; + gptr = &x; + pthread_t thread; + pthread_create(&thread, NULL, foo, NULL); + sleep(3); + assert(x == 0); // UNKNOWN! + pthread_join(thread, NULL); + return 0; +} From 0caaf3641f9e26d9adb301d0e25bd9d85c6ec82a Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 1 Sep 2021 13:42:32 +0300 Subject: [PATCH 03/12] Rename 37-escape -> 41-escape to avoid duplicate group --- tests/regression/{37-escape => 41-escape}/01-local-in-pthread.c | 0 tests/regression/{37-escape => 41-escape}/02-local-in-global.c | 0 2 files changed, 0 insertions(+), 0 deletions(-) rename tests/regression/{37-escape => 41-escape}/01-local-in-pthread.c (100%) rename tests/regression/{37-escape => 41-escape}/02-local-in-global.c (100%) diff --git a/tests/regression/37-escape/01-local-in-pthread.c b/tests/regression/41-escape/01-local-in-pthread.c similarity index 100% rename from tests/regression/37-escape/01-local-in-pthread.c rename to tests/regression/41-escape/01-local-in-pthread.c diff --git a/tests/regression/37-escape/02-local-in-global.c b/tests/regression/41-escape/02-local-in-global.c similarity index 100% rename from tests/regression/37-escape/02-local-in-global.c rename to tests/regression/41-escape/02-local-in-global.c From 09c2e6bb99d66beb3adc29d9dcb15c761735f66c Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 1 Sep 2021 14:16:13 +0300 Subject: [PATCH 04/12] Attempt to fix issue #246 --- src/analyses/threadEscape.ml | 52 +++++++++++++++++++++++++----------- 1 file changed, 36 insertions(+), 16 deletions(-) diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml index f8dbc07099..e9cf198cec 100644 --- a/src/analyses/threadEscape.ml +++ b/src/analyses/threadEscape.ml @@ -25,6 +25,30 @@ struct module C = EscapeDomain.EscapedVars module G = Lattice.Unit + let rec cut_offset x = + match x with + | `NoOffset -> `NoOffset + | `Index (_,o) -> `NoOffset + | `Field (f,o) -> `Field (f, cut_offset o) + + let reachable (ask: Queries.ask) e: D.t = + match ask.f (Queries.ReachableFrom e) with + | a when not (Queries.LS.is_top a) -> + (* let to_extra (v,o) set = D.add (Addr.from_var_offset (v, cut_offset o)) set in *) + let to_extra (v,o) set = D.add v set in + Queries.LS.fold to_extra a (D.empty ()) + (* Ignore soundness warnings, as invalidation proper will raise them. *) + | _ -> D.empty () + + let mpt (ask: Queries.ask) e: D.t = + match ask.f (Queries.MayPointTo e) with + | a when not (Queries.LS.is_top a) -> + (* let to_extra (v,o) set = D.add (Addr.from_var_offset (v, cut_offset o)) set in *) + let to_extra (v,o) set = D.add v set in + Queries.LS.fold to_extra a (D.empty ()) + (* Ignore soundness warnings, as invalidation proper will raise them. *) + | _ -> D.empty () + (* queries *) let query ctx (type a) (q: a Queries.t): a Queries.result = match q with @@ -33,7 +57,18 @@ struct (* transfer functions *) let assign ctx (lval:lval) (rval:exp) : D.t = - ctx.local + let ask = Analyses.ask_of_ctx ctx in + let lvs = mpt ask (AddrOf lval) in + ignore (Pretty.printf "assign lvs %a: %a\n" CilType.Location.pretty !Tracing.current_loc D.pretty lvs); + if D.exists (fun v -> v.vglob || has_escaped ask v) lvs then ( + let escaped = reachable ask rval in + ignore (Pretty.printf "assign lvs %a: %a | %a\n" CilType.Location.pretty !Tracing.current_loc D.pretty lvs D.pretty escaped); + if not (D.is_empty escaped) then (* avoid emitting unnecessary event *) + ctx.emit (Events.Escape escaped); + D.join ctx.local escaped + ) + else + ctx.local let branch ctx (exp:exp) (tv:bool) : D.t = ctx.local @@ -50,21 +85,6 @@ struct let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) : D.t = au - let rec cut_offset x = - match x with - | `NoOffset -> `NoOffset - | `Index (_,o) -> `NoOffset - | `Field (f,o) -> `Field (f, cut_offset o) - - let reachable (ask: Queries.ask) e: D.t = - match ask.f (Queries.ReachableFrom e) with - | a when not (Queries.LS.is_top a) -> - (* let to_extra (v,o) set = D.add (Addr.from_var_offset (v, cut_offset o)) set in *) - let to_extra (v,o) set = D.add v set in - Queries.LS.fold to_extra a (D.empty ()) - (* Ignore soundness warnings, as invalidation proper will raise them. *) - | _ -> D.empty () - let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t = ctx.local From 5f07c2d4bc8de2731980b11645137534e97a67f9 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 14 Apr 2022 11:47:55 +0300 Subject: [PATCH 05/12] Avoid unnecessary thread escapes via global in singlethreaded mode --- src/analyses/threadEscape.ml | 20 ++++++++++++-------- 1 file changed, 12 insertions(+), 8 deletions(-) diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml index 75f65a1e68..154e8b7e8a 100644 --- a/src/analyses/threadEscape.ml +++ b/src/analyses/threadEscape.ml @@ -61,14 +61,18 @@ struct (* transfer functions *) let assign ctx (lval:lval) (rval:exp) : D.t = let ask = Analyses.ask_of_ctx ctx in - let lvs = mpt ask (AddrOf lval) in - ignore (Pretty.printf "assign lvs %a: %a\n" CilType.Location.pretty !Tracing.current_loc D.pretty lvs); - if D.exists (fun v -> v.vglob || has_escaped ask v) lvs then ( - let escaped = reachable ask rval in - ignore (Pretty.printf "assign lvs %a: %a | %a\n" CilType.Location.pretty !Tracing.current_loc D.pretty lvs D.pretty escaped); - if not (D.is_empty escaped) then (* avoid emitting unnecessary event *) - ctx.emit (Events.Escape escaped); - D.join ctx.local escaped + if ThreadFlag.is_multi ask then ( + let lvs = mpt ask (AddrOf lval) in + ignore (Pretty.printf "assign lvs %a: %a\n" CilType.Location.pretty !Tracing.current_loc D.pretty lvs); + if D.exists (fun v -> v.vglob || has_escaped ask v) lvs then ( + let escaped = reachable ask rval in + ignore (Pretty.printf "assign lvs %a: %a | %a\n" CilType.Location.pretty !Tracing.current_loc D.pretty lvs D.pretty escaped); + if not (D.is_empty escaped) then (* avoid emitting unnecessary event *) + ctx.emit (Events.Escape escaped); + D.join ctx.local escaped + ) + else + ctx.local ) else ctx.local From f1a7beb8f28c23d5802b53e4fc66437ddfc71176 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 14 Apr 2022 11:56:28 +0300 Subject: [PATCH 06/12] Collect thread escapes in singlethreaded mode but publish later --- src/analyses/threadEscape.ml | 33 +++++++++++++++++++-------------- 1 file changed, 19 insertions(+), 14 deletions(-) diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml index 154e8b7e8a..cda20dfe5b 100644 --- a/src/analyses/threadEscape.ml +++ b/src/analyses/threadEscape.ml @@ -61,18 +61,14 @@ struct (* transfer functions *) let assign ctx (lval:lval) (rval:exp) : D.t = let ask = Analyses.ask_of_ctx ctx in - if ThreadFlag.is_multi ask then ( - let lvs = mpt ask (AddrOf lval) in - ignore (Pretty.printf "assign lvs %a: %a\n" CilType.Location.pretty !Tracing.current_loc D.pretty lvs); - if D.exists (fun v -> v.vglob || has_escaped ask v) lvs then ( - let escaped = reachable ask rval in - ignore (Pretty.printf "assign lvs %a: %a | %a\n" CilType.Location.pretty !Tracing.current_loc D.pretty lvs D.pretty escaped); - if not (D.is_empty escaped) then (* avoid emitting unnecessary event *) - ctx.emit (Events.Escape escaped); - D.join ctx.local escaped - ) - else - ctx.local + let lvs = mpt ask (AddrOf lval) in + ignore (Pretty.printf "assign lvs %a: %a\n" CilType.Location.pretty !Tracing.current_loc D.pretty lvs); + if D.exists (fun v -> v.vglob || has_escaped ask v) lvs then ( + let escaped = reachable ask rval in + ignore (Pretty.printf "assign lvs %a: %a | %a\n" CilType.Location.pretty !Tracing.current_loc D.pretty lvs D.pretty escaped); + if not (D.is_empty escaped) && ThreadFlag.is_multi ask then (* avoid emitting unnecessary event *) + ctx.emit (Events.Escape escaped); + D.join ctx.local escaped ) else ctx.local @@ -104,8 +100,8 @@ struct let escaped = reachable (Analyses.ask_of_ctx ctx) ptc_arg in if not (D.is_empty escaped) then (* avoid emitting unnecessary event *) ctx.emit (Events.Escape escaped); - [escaped] - | _ -> [D.bot ()] + [D.join ctx.local escaped] + | _ -> [ctx.local] let threadspawn ctx lval f args fctx = D.join ctx.local @@ @@ -117,6 +113,15 @@ struct ctx.emit (Events.Escape escaped); escaped | _ -> D.bot () + + let event ctx e octx = + match e with + | Events.EnterMultiThreaded -> + let escaped = ctx.local in + if not (D.is_empty escaped) then (* avoid emitting unnecessary event *) + ctx.emit (Events.Escape escaped); + ctx.local + | _ -> ctx.local end let _ = From 0a5bd39c32a39a5aa653f0a2a819a902ace19859 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 14 Apr 2022 12:11:54 +0300 Subject: [PATCH 07/12] Fix delayed thread escapes via per-escapee global unknowns --- src/analyses/threadEscape.ml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml index cda20dfe5b..256d5d9968 100644 --- a/src/analyses/threadEscape.ml +++ b/src/analyses/threadEscape.ml @@ -23,6 +23,8 @@ struct let name () = "escape" module D = EscapeDomain.EscapedVars module C = EscapeDomain.EscapedVars + module V = VarinfoV + module G = EscapeDomain.EscapedVars let rec cut_offset x = match x with @@ -68,6 +70,9 @@ struct ignore (Pretty.printf "assign lvs %a: %a | %a\n" CilType.Location.pretty !Tracing.current_loc D.pretty lvs D.pretty escaped); if not (D.is_empty escaped) && ThreadFlag.is_multi ask then (* avoid emitting unnecessary event *) ctx.emit (Events.Escape escaped); + D.iter (fun lv -> + ctx.sideg lv escaped + ) lvs; D.join ctx.local escaped ) else @@ -100,7 +105,8 @@ struct let escaped = reachable (Analyses.ask_of_ctx ctx) ptc_arg in if not (D.is_empty escaped) then (* avoid emitting unnecessary event *) ctx.emit (Events.Escape escaped); - [D.join ctx.local escaped] + let extra = D.fold (fun v acc -> D.join acc (ctx.global v)) escaped (D.empty ()) in + [D.join ctx.local (D.join escaped extra)] | _ -> [ctx.local] let threadspawn ctx lval f args fctx = From 9c0939c1fecca5fe58c5ac9d7233b123db66edb6 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sat, 16 Apr 2022 13:42:52 +0200 Subject: [PATCH 08/12] 45/02: Add assert that precision is maintained in single-threaded mode --- tests/regression/45-escape/02-local-in-global.c | 1 + 1 file changed, 1 insertion(+) diff --git a/tests/regression/45-escape/02-local-in-global.c b/tests/regression/45-escape/02-local-in-global.c index bca91393fd..1c4632e484 100644 --- a/tests/regression/45-escape/02-local-in-global.c +++ b/tests/regression/45-escape/02-local-in-global.c @@ -11,6 +11,7 @@ void *foo(void* p){ int main(){ int x = 0; gptr = &x; + assert(x==0); pthread_t thread; pthread_create(&thread, NULL, foo, NULL); sleep(3); From 98131e1483ebfbe982fe4b0af183c0f13c8f457b Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sat, 16 Apr 2022 14:29:55 +0200 Subject: [PATCH 09/12] Add example --- .../45-escape/03-local-in-pthread-a.c | 30 +++++++++++++++++++ 1 file changed, 30 insertions(+) create mode 100644 tests/regression/45-escape/03-local-in-pthread-a.c diff --git a/tests/regression/45-escape/03-local-in-pthread-a.c b/tests/regression/45-escape/03-local-in-pthread-a.c new file mode 100644 index 0000000000..91cd7d2db1 --- /dev/null +++ b/tests/regression/45-escape/03-local-in-pthread-a.c @@ -0,0 +1,30 @@ +#include +#include + +#include +#include +#include + + +void *foo(void* p){ + sleep(2); + int* ip = *((int**) p); + printf("ip is %d\n", *ip); + // To check that in (01) even without modification both &x and &x2 are possible here + assert(*ip == 0); //UNKNOWN! + assert(*ip == 35); //UNKNOWN! + return NULL; +} + +int main(){ + int x = 0; + int *xp = &x; + int** ptr = &xp; + int x2 = 35; + pthread_t thread; + pthread_create(&thread, NULL, foo, ptr); + *ptr = &x2; + sleep(4); // to make sure that we actually fail the assert when running. + pthread_join(thread, NULL); + return 0; +} From da7782ab8b4784694e0dca7bf48a6c6710bc1d2c Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sat, 16 Apr 2022 14:32:48 +0200 Subject: [PATCH 10/12] Add potential stretch goal --- tests/regression/45-escape/04-imprecision.c | 28 +++++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 tests/regression/45-escape/04-imprecision.c diff --git a/tests/regression/45-escape/04-imprecision.c b/tests/regression/45-escape/04-imprecision.c new file mode 100644 index 0000000000..50b0b90128 --- /dev/null +++ b/tests/regression/45-escape/04-imprecision.c @@ -0,0 +1,28 @@ +#include +#include + +int* gptr; + +void *foo(void* p){ + *gptr = 17; + return NULL; +} + +// The asserts about y would hold in the concrete, as y actually never escapes the current thread, but we are currently not precise enough to account for this + +int main(){ + int x = 0; + int y = 0; + gptr = &y; + gptr = &x; + assert(x==0); + pthread_t thread; + pthread_create(&thread, NULL, foo, NULL); + sleep(3); + assert(x == 0); // UNKNOWN! + assert(y == 0); //TODO + y = 5; + assert(y == 5); //TODO + pthread_join(thread, NULL); + return 0; +} From a3032bbe36b19b8f191c4afea5522ad8130fa1d3 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 20 Apr 2022 15:45:57 +0300 Subject: [PATCH 11/12] Change threadEscape debug prints to tracing --- src/analyses/threadEscape.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml index 256d5d9968..ad26da8781 100644 --- a/src/analyses/threadEscape.ml +++ b/src/analyses/threadEscape.ml @@ -64,10 +64,10 @@ struct let assign ctx (lval:lval) (rval:exp) : D.t = let ask = Analyses.ask_of_ctx ctx in let lvs = mpt ask (AddrOf lval) in - ignore (Pretty.printf "assign lvs %a: %a\n" CilType.Location.pretty !Tracing.current_loc D.pretty lvs); + if M.tracing then M.tracel "escape" "assign lvs: %a\n" D.pretty lvs; if D.exists (fun v -> v.vglob || has_escaped ask v) lvs then ( let escaped = reachable ask rval in - ignore (Pretty.printf "assign lvs %a: %a | %a\n" CilType.Location.pretty !Tracing.current_loc D.pretty lvs D.pretty escaped); + if M.tracing then M.tracel "escape" "assign lvs: %a | %a\n" D.pretty lvs D.pretty escaped; if not (D.is_empty escaped) && ThreadFlag.is_multi ask then (* avoid emitting unnecessary event *) ctx.emit (Events.Escape escaped); D.iter (fun lv -> From 207e4c7e359d21dccca4f56e94e27190cfeb17b3 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Wed, 20 Apr 2022 15:48:15 +0300 Subject: [PATCH 12/12] Add threadEscape TODO about transitive global joining --- src/analyses/threadEscape.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml index ad26da8781..eb82a28ac7 100644 --- a/src/analyses/threadEscape.ml +++ b/src/analyses/threadEscape.ml @@ -105,7 +105,7 @@ struct let escaped = reachable (Analyses.ask_of_ctx ctx) ptc_arg in if not (D.is_empty escaped) then (* avoid emitting unnecessary event *) ctx.emit (Events.Escape escaped); - let extra = D.fold (fun v acc -> D.join acc (ctx.global v)) escaped (D.empty ()) in + let extra = D.fold (fun v acc -> D.join acc (ctx.global v)) escaped (D.empty ()) in (* TODO: must transitively join escapes of every ctx.global v as well? *) [D.join ctx.local (D.join escaped extra)] | _ -> [ctx.local]