From 070f7cafe81e6956d5d4981ea110fd54abca2a89 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Mon, 5 Jun 2023 14:45:15 +0200 Subject: [PATCH 01/22] Add test case where escaped local has unsound value. --- tests/regression/74-escape/01-local-esacpe.c | 42 ++++++++++++++++++++ 1 file changed, 42 insertions(+) create mode 100644 tests/regression/74-escape/01-local-esacpe.c diff --git a/tests/regression/74-escape/01-local-esacpe.c b/tests/regression/74-escape/01-local-esacpe.c new file mode 100644 index 0000000000..40a6f788be --- /dev/null +++ b/tests/regression/74-escape/01-local-esacpe.c @@ -0,0 +1,42 @@ +#include +#include +#include +#include + +int g = 0; +int *p = &g; + +int let_escape(){ + int x = 23; + g = 23; + + __goblint_check(x == 23); + p = &x; + sleep(5); + __goblint_check(x == 23); //UNKNOWN! +} + +void *thread1(void *pp){ + let_escape(); //RACE + return NULL; +} + +void write_through_pointer(){ + sleep(2); + *p = 1; //RACE +} + +void *thread2(void *p){ + write_through_pointer(); + return NULL; +} + +int main(){ + pthread_t t1; + pthread_t t2; + pthread_create(&t1, NULL, thread1, NULL); + pthread_create(&t2, NULL, thread2, NULL); + pthread_join(t1, NULL); + pthread_join(t2, NULL); +} + From 843e0dc5b940f7899963e4fe477f7ff31c9a9f13 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Mon, 5 Jun 2023 14:58:43 +0200 Subject: [PATCH 02/22] Remove race annotation, as this is secondary for this test case. --- tests/regression/74-escape/01-local-esacpe.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/regression/74-escape/01-local-esacpe.c b/tests/regression/74-escape/01-local-esacpe.c index 40a6f788be..96e7a75efb 100644 --- a/tests/regression/74-escape/01-local-esacpe.c +++ b/tests/regression/74-escape/01-local-esacpe.c @@ -17,13 +17,13 @@ int let_escape(){ } void *thread1(void *pp){ - let_escape(); //RACE + let_escape(); return NULL; } void write_through_pointer(){ sleep(2); - *p = 1; //RACE + *p = 1; } void *thread2(void *p){ From 87a10f9ce83876bbbc9f3bd24d9f15a7424dcc63 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Tue, 6 Jun 2023 09:47:49 +0200 Subject: [PATCH 03/22] Move failing test with local escaping into escape test folder, simplify it. --- .../06-local-escp.c} | 21 +++++++------------ 1 file changed, 7 insertions(+), 14 deletions(-) rename tests/regression/{74-escape/01-local-esacpe.c => 45-escape/06-local-escp.c} (76%) diff --git a/tests/regression/74-escape/01-local-esacpe.c b/tests/regression/45-escape/06-local-escp.c similarity index 76% rename from tests/regression/74-escape/01-local-esacpe.c rename to tests/regression/45-escape/06-local-escp.c index 96e7a75efb..7ae6b4d1d1 100644 --- a/tests/regression/74-escape/01-local-esacpe.c +++ b/tests/regression/45-escape/06-local-escp.c @@ -1,3 +1,4 @@ +// SKIP #include #include #include @@ -6,28 +7,20 @@ int g = 0; int *p = &g; -int let_escape(){ - int x = 23; - g = 23; +void *thread1(void *pp){ + int x = 23; __goblint_check(x == 23); p = &x; - sleep(5); + sleep(2); __goblint_check(x == 23); //UNKNOWN! -} - -void *thread1(void *pp){ - let_escape(); return NULL; } -void write_through_pointer(){ - sleep(2); +void *thread2(void *ignored){ + sleep(1); + int *i = p; *p = 1; -} - -void *thread2(void *p){ - write_through_pointer(); return NULL; } From f2c2145cbd21855870eeb2a45ebe03ec2a1b20bd Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Tue, 6 Jun 2023 10:55:14 +0200 Subject: [PATCH 04/22] ThreadEscape: Extract function emitting events. --- src/analyses/threadEscape.ml | 23 ++++++++++++----------- 1 file changed, 12 insertions(+), 11 deletions(-) diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml index 43d3ac4de5..a903a238f7 100644 --- a/src/analyses/threadEscape.ml +++ b/src/analyses/threadEscape.ml @@ -42,10 +42,15 @@ struct if M.tracing then M.tracel "escape" "mpt %a: %a\n" d_exp e Queries.LS.pretty a; D.empty () + let emit_escaped ctx escaped = + if not (D.is_empty escaped) then (* avoid emitting unnecessary event *) + ctx.emit (Events.Escape escaped) + (* queries *) let query ctx (type a) (q: a Queries.t): a Queries.result = match q with - | Queries.MayEscape v -> D.mem v ctx.local + | Queries.MayEscape v -> + D.mem v ctx.local | _ -> Queries.Result.top q (* transfer functions *) @@ -57,8 +62,8 @@ struct let escaped = reachable ask rval in let escaped = D.filter (fun v -> not v.vglob) escaped in if M.tracing then M.tracel "escape" "assign vs: %a | %a\n" D.pretty vs D.pretty escaped; - if not (D.is_empty escaped) && ThreadFlag.has_ever_been_multi ask then (* avoid emitting unnecessary event *) - ctx.emit (Events.Escape escaped); + if ThreadFlag.has_ever_been_multi ask then (* avoid emitting unnecessary event *) + emit_escaped ctx escaped; D.iter (fun v -> ctx.sideg v escaped; ) vs; @@ -73,8 +78,7 @@ struct | _, "pthread_setspecific" , [key; pt_value] -> let escaped = reachable (Analyses.ask_of_ctx ctx) pt_value in let escaped = D.filter (fun v -> not v.vglob) escaped in - if not (D.is_empty escaped) then (* avoid emitting unnecessary event *) - ctx.emit (Events.Escape escaped); + emit_escaped ctx escaped; 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 @@ -87,8 +91,7 @@ struct | [ptc_arg] -> let escaped = reachable (Analyses.ask_of_ctx ctx) ptc_arg in let escaped = D.filter (fun v -> not v.vglob) escaped in - if not (D.is_empty escaped) then (* avoid emitting unnecessary event *) - ctx.emit (Events.Escape escaped); + emit_escaped ctx escaped; 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] @@ -101,8 +104,7 @@ struct let escaped = reachable (Analyses.ask_of_ctx ctx) ptc_arg in let escaped = D.filter (fun v -> not v.vglob) escaped in if M.tracing then M.tracel "escape" "%a: %a\n" d_exp ptc_arg D.pretty escaped; - if not (D.is_empty escaped) then (* avoid emitting unnecessary event *) - ctx.emit (Events.Escape escaped); + emit_escaped ctx escaped; escaped | _ -> D.bot () @@ -110,8 +112,7 @@ struct 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); + emit_escaped ctx escaped; ctx.local | _ -> ctx.local end From df407b1ac8e1f86532f933b6bd09a8bdcf03fb25 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Tue, 6 Jun 2023 12:42:45 +0200 Subject: [PATCH 05/22] Add simple failiing test case due to unsound escape analysis. --- .../07-local-in-global-after-create.c | 22 +++++++++++++++++++ 1 file changed, 22 insertions(+) create mode 100644 tests/regression/45-escape/07-local-in-global-after-create.c diff --git a/tests/regression/45-escape/07-local-in-global-after-create.c b/tests/regression/45-escape/07-local-in-global-after-create.c new file mode 100644 index 0000000000..fbb955e1fc --- /dev/null +++ b/tests/regression/45-escape/07-local-in-global-after-create.c @@ -0,0 +1,22 @@ +// SKIP +#include +#include + +int* gptr; + +void *foo(void* p){ + *gptr = 17; + return NULL; +} + +int main(){ + int x = 0; + __goblint_check(x==0); + pthread_t thread; + pthread_create(&thread, NULL, foo, NULL); + gptr = &x; + sleep(3); + __goblint_check(x == 0); // UNKNOWN! + pthread_join(thread, NULL); + return 0; +} From 9143b2a3d00a9bcabd081394bfbfaca8c0f2b94a Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Tue, 6 Jun 2023 18:58:35 +0200 Subject: [PATCH 06/22] ThreadEscape: collect which threads escaped variables in flow-insensitive invariant. --- src/analyses/threadEscape.ml | 71 ++++++++++++++++++++++++------------ 1 file changed, 48 insertions(+), 23 deletions(-) diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml index a903a238f7..0b6ccb0076 100644 --- a/src/analyses/threadEscape.ml +++ b/src/analyses/threadEscape.ml @@ -16,11 +16,13 @@ module Spec = struct include Analyses.IdentitySpec + module ThreadIdSet = SetDomain.Make (ThreadIdDomain.ThreadLifted) + let name () = "escape" module D = EscapeDomain.EscapedVars module C = EscapeDomain.EscapedVars module V = VarinfoV - module G = EscapeDomain.EscapedVars + module G = ThreadIdSet let reachable (ask: Queries.ask) e: D.t = match ask.f (Queries.ReachableFrom e) with @@ -42,15 +44,47 @@ struct if M.tracing then M.tracel "escape" "mpt %a: %a\n" d_exp e Queries.LS.pretty a; D.empty () - let emit_escaped ctx escaped = - if not (D.is_empty escaped) then (* avoid emitting unnecessary event *) - ctx.emit (Events.Escape escaped) + let escape ctx escaped = + let threadid = ctx.ask Queries.CurrentThreadId in + let threadid = G.singleton threadid in + + (* avoid emitting unnecessary event *) + if not (D.is_empty escaped) then begin + ctx.emit (Events.Escape escaped); + M.tracel "escape" "escaping: %a\n" D.pretty escaped; + D.iter (fun v -> + ctx.sideg v threadid) escaped + end (* queries *) let query ctx (type a) (q: a Queries.t): a Queries.result = match q with | Queries.MayEscape v -> - D.mem v ctx.local + let threads = ctx.global v in + if ThreadIdSet.is_empty threads then + false + else if not (ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx)) then + false + else begin + let possibly_started current = function + | `Lifted tid -> + let not_started = MHP.definitely_not_started (current, ctx.ask Queries.CreatedThreads) tid in + let possibly_started = not not_started in + M.tracel "escape" "possibly_started: %a %a -> %b\n" ThreadIdDomain.Thread.pretty tid ThreadIdDomain.Thread.pretty current possibly_started; + possibly_started + | `Top + | `Bot -> false + in + match ctx.ask Queries.CurrentThreadId with + | `Lifted current -> + let possibly_started = ThreadIdSet.exists (possibly_started current) threads in + possibly_started || D.mem v ctx.local + | `Top -> + true + | `Bot -> + M.warn ~category:MessageCategory.Analyzer "CurrentThreadId is bottom."; + false + end | _ -> Queries.Result.top q (* transfer functions *) @@ -63,24 +97,19 @@ struct let escaped = D.filter (fun v -> not v.vglob) escaped in if M.tracing then M.tracel "escape" "assign vs: %a | %a\n" D.pretty vs D.pretty escaped; if ThreadFlag.has_ever_been_multi ask then (* avoid emitting unnecessary event *) - emit_escaped ctx escaped; - D.iter (fun v -> - ctx.sideg v escaped; - ) vs; + escape ctx escaped; D.join ctx.local escaped - ) - else + ) else begin + M.tracel "escape" "nothing in rval: %a was escaped\n" D.pretty vs; ctx.local + end let special ctx (lval: lval option) (f:varinfo) (args:exp list) : D.t = let desc = LibraryFunctions.find f in match desc.special args, f.vname, args with | _, "pthread_setspecific" , [key; pt_value] -> - let escaped = reachable (Analyses.ask_of_ctx ctx) pt_value in - let escaped = D.filter (fun v -> not v.vglob) escaped in - emit_escaped ctx escaped; - 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) + (* TODO: handle *) + ctx.local | _ -> ctx.local let startstate v = D.bot () @@ -89,11 +118,7 @@ struct let threadenter ctx lval f args = match args with | [ptc_arg] -> - let escaped = reachable (Analyses.ask_of_ctx ctx) ptc_arg in - let escaped = D.filter (fun v -> not v.vglob) escaped in - emit_escaped ctx escaped; - 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] | _ -> [ctx.local] let threadspawn ctx lval f args fctx = @@ -104,7 +129,7 @@ struct let escaped = reachable (Analyses.ask_of_ctx ctx) ptc_arg in let escaped = D.filter (fun v -> not v.vglob) escaped in if M.tracing then M.tracel "escape" "%a: %a\n" d_exp ptc_arg D.pretty escaped; - emit_escaped ctx escaped; + escape ctx escaped; escaped | _ -> D.bot () @@ -112,7 +137,7 @@ struct match e with | Events.EnterMultiThreaded -> let escaped = ctx.local in - emit_escaped ctx escaped; + escape ctx escaped; ctx.local | _ -> ctx.local end From cbfe7b6ddbf37c8ee21a5a50cde56646f9a23b78 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Wed, 7 Jun 2023 10:24:48 +0200 Subject: [PATCH 07/22] ThreadEscape: also answer whether variable escaped in singlethreaded mode, support pthread_setspecific again. The base analysis relies on variables being considered escaped even in single-threaded mode, when determining which local variables to pass to a callee: Locals possibly reachable via globals need to be considered escaped. --- src/analyses/threadEscape.ml | 59 ++++++++++++++++++++++-------------- 1 file changed, 36 insertions(+), 23 deletions(-) diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml index 0b6ccb0076..538e7247d0 100644 --- a/src/analyses/threadEscape.ml +++ b/src/analyses/threadEscape.ml @@ -44,17 +44,24 @@ struct if M.tracing then M.tracel "escape" "mpt %a: %a\n" d_exp e Queries.LS.pretty a; D.empty () - let escape ctx escaped = - let threadid = ctx.ask Queries.CurrentThreadId in - let threadid = G.singleton threadid in + let thread_id ctx = + ctx.ask Queries.CurrentThreadId + (** Emit an escape event: + Only necessary when code has ever been multithreaded, + or when about to go multithreaded. *) + let emit_escape_event ctx escaped = (* avoid emitting unnecessary event *) - if not (D.is_empty escaped) then begin - ctx.emit (Events.Escape escaped); - M.tracel "escape" "escaping: %a\n" D.pretty escaped; - D.iter (fun v -> - ctx.sideg v threadid) escaped - end + if not (D.is_empty escaped) then + ctx.emit (Events.Escape escaped) + + (** Side effect escapes: In contrast to the emitting the event, side-effecting is + necessary in single threaded mode, since we rely on escape status in Base + for passing locals reachable via globals *) + let side_effect_escape ctx escaped threadid = + let threadid = G.singleton threadid in + D.iter (fun v -> + ctx.sideg v threadid) escaped (* queries *) let query ctx (type a) (q: a Queries.t): a Queries.result = @@ -63,14 +70,11 @@ struct let threads = ctx.global v in if ThreadIdSet.is_empty threads then false - else if not (ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx)) then - false else begin let possibly_started current = function | `Lifted tid -> let not_started = MHP.definitely_not_started (current, ctx.ask Queries.CreatedThreads) tid in let possibly_started = not not_started in - M.tracel "escape" "possibly_started: %a %a -> %b\n" ThreadIdDomain.Thread.pretty tid ThreadIdDomain.Thread.pretty current possibly_started; possibly_started | `Top | `Bot -> false @@ -87,20 +91,25 @@ struct end | _ -> Queries.Result.top q + let escape_rval ctx (rval:exp) = + let ask = Analyses.ask_of_ctx ctx in + let escaped = reachable ask rval in + let escaped = D.filter (fun v -> not v.vglob) escaped in + + let thread_id = thread_id ctx in + side_effect_escape ctx escaped thread_id; + if ThreadFlag.has_ever_been_multi ask then (* avoid emitting unnecessary event *) + emit_escape_event ctx escaped; + escaped + (* transfer functions *) let assign ctx (lval:lval) (rval:exp) : D.t = let ask = Analyses.ask_of_ctx ctx in let vs = mpt ask (AddrOf lval) in - if M.tracing then M.tracel "escape" "assign vs: %a\n" D.pretty vs; if D.exists (fun v -> v.vglob || has_escaped ask v) vs then ( - let escaped = reachable ask rval in - let escaped = D.filter (fun v -> not v.vglob) escaped in - if M.tracing then M.tracel "escape" "assign vs: %a | %a\n" D.pretty vs D.pretty escaped; - if ThreadFlag.has_ever_been_multi ask then (* avoid emitting unnecessary event *) - escape ctx escaped; + let escaped = escape_rval ctx rval in D.join ctx.local escaped ) else begin - M.tracel "escape" "nothing in rval: %a was escaped\n" D.pretty vs; ctx.local end @@ -108,8 +117,8 @@ struct let desc = LibraryFunctions.find f in match desc.special args, f.vname, args with | _, "pthread_setspecific" , [key; pt_value] -> - (* TODO: handle *) - ctx.local + let escaped = escape_rval ctx pt_value in + D.join ctx.local escaped | _ -> ctx.local let startstate v = D.bot () @@ -129,7 +138,9 @@ struct let escaped = reachable (Analyses.ask_of_ctx ctx) ptc_arg in let escaped = D.filter (fun v -> not v.vglob) escaped in if M.tracing then M.tracel "escape" "%a: %a\n" d_exp ptc_arg D.pretty escaped; - escape ctx escaped; + let thread_id = thread_id ctx in + emit_escape_event ctx escaped; + side_effect_escape ctx escaped thread_id; escaped | _ -> D.bot () @@ -137,7 +148,9 @@ struct match e with | Events.EnterMultiThreaded -> let escaped = ctx.local in - escape ctx escaped; + let thread_id = thread_id ctx in + emit_escape_event ctx escaped; + side_effect_escape ctx escaped thread_id; ctx.local | _ -> ctx.local end From 7533309ce1d56bf85c372ab6004f9141d2d1b75b Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Wed, 7 Jun 2023 10:29:44 +0200 Subject: [PATCH 08/22] Add test case, extend test case with interval checks. --- tests/regression/45-escape/06-local-escp.c | 3 ++ .../regression/45-escape/08-local-escp-main.c | 31 +++++++++++++++++++ 2 files changed, 34 insertions(+) create mode 100644 tests/regression/45-escape/08-local-escp-main.c diff --git a/tests/regression/45-escape/06-local-escp.c b/tests/regression/45-escape/06-local-escp.c index 7ae6b4d1d1..d89d569e45 100644 --- a/tests/regression/45-escape/06-local-escp.c +++ b/tests/regression/45-escape/06-local-escp.c @@ -14,6 +14,9 @@ void *thread1(void *pp){ p = &x; sleep(2); __goblint_check(x == 23); //UNKNOWN! + __goblint_check(x <= 23); + __goblint_check(x >= 1); + return NULL; } diff --git a/tests/regression/45-escape/08-local-escp-main.c b/tests/regression/45-escape/08-local-escp-main.c new file mode 100644 index 0000000000..19b4bc7940 --- /dev/null +++ b/tests/regression/45-escape/08-local-escp-main.c @@ -0,0 +1,31 @@ +//PARAM: --enable ana.int.interval +#include +#include +#include +#include + +int g = 0; +int *p = &g; + + +void *thread1(void *pp){ + int x = 23; + __goblint_check(x == 23); + p = &x; + sleep(2); + __goblint_check(x == 23); //UNKNOWN! + __goblint_check(x <= 23); + __goblint_check(x >= 1); + + int y = x; + return NULL; +} + +int main(){ + pthread_t t1; + pthread_t t2; + pthread_create(&t1, NULL, thread1, NULL); + sleep(1); + *p = 1; +} + From fb90c453d01a6f6060fe62036671ed6782ba362c Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Wed, 7 Jun 2023 10:32:17 +0200 Subject: [PATCH 09/22] Indent threadEscape.ml --- src/analyses/threadEscape.ml | 26 +++++++++++++------------- 1 file changed, 13 insertions(+), 13 deletions(-) diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml index 538e7247d0..8a935cf639 100644 --- a/src/analyses/threadEscape.ml +++ b/src/analyses/threadEscape.ml @@ -61,7 +61,7 @@ struct let side_effect_escape ctx escaped threadid = let threadid = G.singleton threadid in D.iter (fun v -> - ctx.sideg v threadid) escaped + ctx.sideg v threadid) escaped (* queries *) let query ctx (type a) (q: a Queries.t): a Queries.result = @@ -88,7 +88,7 @@ struct | `Bot -> M.warn ~category:MessageCategory.Analyzer "CurrentThreadId is bottom."; false - end + end | _ -> Queries.Result.top q let escape_rval ctx (rval:exp) = @@ -132,17 +132,17 @@ struct let threadspawn ctx lval f args fctx = D.join ctx.local @@ - match args with - | [ptc_arg] -> - (* not reusing fctx.local to avoid unnecessarily early join of extra *) - let escaped = reachable (Analyses.ask_of_ctx ctx) ptc_arg in - let escaped = D.filter (fun v -> not v.vglob) escaped in - if M.tracing then M.tracel "escape" "%a: %a\n" d_exp ptc_arg D.pretty escaped; - let thread_id = thread_id ctx in - emit_escape_event ctx escaped; - side_effect_escape ctx escaped thread_id; - escaped - | _ -> D.bot () + match args with + | [ptc_arg] -> + (* not reusing fctx.local to avoid unnecessarily early join of extra *) + let escaped = reachable (Analyses.ask_of_ctx ctx) ptc_arg in + let escaped = D.filter (fun v -> not v.vglob) escaped in + if M.tracing then M.tracel "escape" "%a: %a\n" d_exp ptc_arg D.pretty escaped; + let thread_id = thread_id ctx in + emit_escape_event ctx escaped; + side_effect_escape ctx escaped thread_id; + escaped + | _ -> D.bot () let event ctx e octx = match e with From 558ae513d7b9b15a078f33bfe2e6425c0119be26 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Wed, 7 Jun 2023 11:24:58 +0200 Subject: [PATCH 10/22] ThreadEscape: add escaped to local state in threadenter. --- src/analyses/threadEscape.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml index 8a935cf639..f7335dde54 100644 --- a/src/analyses/threadEscape.ml +++ b/src/analyses/threadEscape.ml @@ -127,7 +127,10 @@ struct let threadenter ctx lval f args = match args with | [ptc_arg] -> - [ctx.local] + let escaped = reachable (Analyses.ask_of_ctx ctx) ptc_arg in + let escaped = D.filter (fun v -> not v.vglob) escaped in + emit_escape_event ctx escaped; + [D.join ctx.local escaped] | _ -> [ctx.local] let threadspawn ctx lval f args fctx = From 3fd471c81ee24a40046d940d03e296a7ef189e4c Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Wed, 14 Jun 2023 10:43:37 +0200 Subject: [PATCH 11/22] Enable intervals for test case. --- tests/regression/45-escape/06-local-escp.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/regression/45-escape/06-local-escp.c b/tests/regression/45-escape/06-local-escp.c index d89d569e45..50d27e200e 100644 --- a/tests/regression/45-escape/06-local-escp.c +++ b/tests/regression/45-escape/06-local-escp.c @@ -1,4 +1,4 @@ -// SKIP +// PARAM: --enable ana.int.interval #include #include #include From 006d4ea93506d906e3da230d2ada85f585987303 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Wed, 14 Jun 2023 11:09:07 +0200 Subject: [PATCH 12/22] ThreadEscape: Check for uniquness of thread. If the current thread is non-unqiue and may escape the variable queried with (MayEscape v), then v may be escaped. --- src/analyses/threadEscape.ml | 21 ++++++++++++++++++--- 1 file changed, 18 insertions(+), 3 deletions(-) diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml index f7335dde54..85d4df754a 100644 --- a/src/analyses/threadEscape.ml +++ b/src/analyses/threadEscape.ml @@ -73,16 +73,31 @@ struct else begin let possibly_started current = function | `Lifted tid -> - let not_started = MHP.definitely_not_started (current, ctx.ask Queries.CreatedThreads) tid in + let threads = ctx.ask Queries.CreatedThreads in + let not_started = MHP.definitely_not_started (current, threads) tid in + M.tracel "threadescape" "tid: %a, not_started: %b\n" ThreadIdDomain.FlagConfiguredTID.pretty tid not_started; let possibly_started = not not_started in possibly_started - | `Top + | `Top -> true + | `Bot -> false + in + let equal_current_not_unique current = function + | `Lifted tid -> + ThreadId.Thread.equal current tid && not (ThreadId.Thread.is_unique current) + | `Top -> true | `Bot -> false in match ctx.ask Queries.CurrentThreadId with | `Lifted current -> let possibly_started = ThreadIdSet.exists (possibly_started current) threads in - possibly_started || D.mem v ctx.local + if possibly_started then + true + else if ThreadIdSet.exists (equal_current_not_unique current) threads then + (* Another instance of the non-unqiue current thread may have escaped the variable *) + true + else + (* Check whether current unique thread has escaped the variable *) + D.mem v ctx.local | `Top -> true | `Bot -> From 7d70907c5c10e9b24aa52997863422721985374e Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Wed, 14 Jun 2023 12:34:02 +0200 Subject: [PATCH 13/22] RelationAnalysis.threadenter: include reachable thread create args in rel. Reuse implementation of enter in threadenter to determine what to add to rel. --- src/analyses/apron/relationAnalysis.apron.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index 7e03e7b98e..877ec7a55a 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -280,7 +280,7 @@ struct | None -> true | Some v -> any_local_reachable - let enter ctx r f args = + let make_callee_rel ctx f args = let fundec = Node.find_fundec ctx.node in let st = ctx.local in if M.tracing then M.tracel "combine" "relation enter f: %a\n" CilType.Varinfo.pretty f.svar; @@ -311,7 +311,12 @@ struct | _ -> false (* keep everything else (just added args, globals, global privs) *) ); if M.tracing then M.tracel "combine" "relation enter newd: %a\n" RD.pretty new_rel; - [st, {st with rel = new_rel}] + new_rel + + let enter ctx r f args = + let callee_rel = make_callee_rel ctx f args in + let callee_st = {ctx.local with rel = callee_rel} in + [ctx.local, callee_st] let body ctx f = let st = ctx.local in @@ -627,12 +632,7 @@ struct if not (ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx)) then ignore (Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st); let st' = Priv.threadenter (Analyses.ask_of_ctx ctx) ctx.global st in - let arg_vars = - fd.sformals - |> List.filter RD.Tracked.varinfo_tracked - |> List.map RV.arg - in - let new_rel = RD.add_vars st'.rel arg_vars in + let new_rel = make_callee_rel ctx fd args in [{st' with rel = new_rel}] | exception Not_found -> (* Unknown functions *) From 44d560e3b015522f3996504e6cd0b4f09eba7dc9 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Wed, 14 Jun 2023 12:39:57 +0200 Subject: [PATCH 14/22] ThreadEscape.threadenter: set local state (i.e., variables secaped in thread) to empty set. Previous solution that had a non-empty state was required only due to RelationAnalysis that did not pass reachable variables to the created thread in threadenter. --- src/analyses/threadEscape.ml | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml index 85d4df754a..feacee7981 100644 --- a/src/analyses/threadEscape.ml +++ b/src/analyses/threadEscape.ml @@ -140,13 +140,7 @@ struct let exitstate v = D.bot () let threadenter ctx lval f args = - match args with - | [ptc_arg] -> - let escaped = reachable (Analyses.ask_of_ctx ctx) ptc_arg in - let escaped = D.filter (fun v -> not v.vglob) escaped in - emit_escape_event ctx escaped; - [D.join ctx.local escaped] - | _ -> [ctx.local] + [D.bot ()] let threadspawn ctx lval f args fctx = D.join ctx.local @@ From fb9356377647338adc0f98fcfeac60124fafb631 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Wed, 14 Jun 2023 12:41:31 +0200 Subject: [PATCH 15/22] Remove debug output. --- src/analyses/threadEscape.ml | 1 - 1 file changed, 1 deletion(-) diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml index feacee7981..9871d26a94 100644 --- a/src/analyses/threadEscape.ml +++ b/src/analyses/threadEscape.ml @@ -75,7 +75,6 @@ struct | `Lifted tid -> let threads = ctx.ask Queries.CreatedThreads in let not_started = MHP.definitely_not_started (current, threads) tid in - M.tracel "threadescape" "tid: %a, not_started: %b\n" ThreadIdDomain.FlagConfiguredTID.pretty tid not_started; let possibly_started = not not_started in possibly_started | `Top -> true From 83e87e53e7a3ef06987c0230da1c3e92d1d225e4 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Wed, 14 Jun 2023 17:11:38 +0200 Subject: [PATCH 16/22] Revert "RelationAnalysis.threadenter: include reachable thread create args in rel." This reverts commit 7d70907c5c10e9b24aa52997863422721985374e. --- src/analyses/apron/relationAnalysis.apron.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index 877ec7a55a..7e03e7b98e 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -280,7 +280,7 @@ struct | None -> true | Some v -> any_local_reachable - let make_callee_rel ctx f args = + let enter ctx r f args = let fundec = Node.find_fundec ctx.node in let st = ctx.local in if M.tracing then M.tracel "combine" "relation enter f: %a\n" CilType.Varinfo.pretty f.svar; @@ -311,12 +311,7 @@ struct | _ -> false (* keep everything else (just added args, globals, global privs) *) ); if M.tracing then M.tracel "combine" "relation enter newd: %a\n" RD.pretty new_rel; - new_rel - - let enter ctx r f args = - let callee_rel = make_callee_rel ctx f args in - let callee_st = {ctx.local with rel = callee_rel} in - [ctx.local, callee_st] + [st, {st with rel = new_rel}] let body ctx f = let st = ctx.local in @@ -632,7 +627,12 @@ struct if not (ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx)) then ignore (Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st); let st' = Priv.threadenter (Analyses.ask_of_ctx ctx) ctx.global st in - let new_rel = make_callee_rel ctx fd args in + let arg_vars = + fd.sformals + |> List.filter RD.Tracked.varinfo_tracked + |> List.map RV.arg + in + let new_rel = RD.add_vars st'.rel arg_vars in [{st' with rel = new_rel}] | exception Not_found -> (* Unknown functions *) From 6b6c00f812791e478623e3e6ac2df453401b81d8 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Wed, 14 Jun 2023 17:56:01 +0200 Subject: [PATCH 17/22] Fix apron threadenter for unreached fixedpoint for 63/16. --- src/analyses/apron/relationAnalysis.apron.ml | 28 +++++++++++++++----- 1 file changed, 21 insertions(+), 7 deletions(-) diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index 7e03e7b98e..3908e24577 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -280,7 +280,7 @@ struct | None -> true | Some v -> any_local_reachable - let enter ctx r f args = + let make_callee_rel ~thread ctx f args = let fundec = Node.find_fundec ctx.node in let st = ctx.local in if M.tracing then M.tracel "combine" "relation enter f: %a\n" CilType.Varinfo.pretty f.svar; @@ -311,7 +311,11 @@ struct | _ -> false (* keep everything else (just added args, globals, global privs) *) ); if M.tracing then M.tracel "combine" "relation enter newd: %a\n" RD.pretty new_rel; - [st, {st with rel = new_rel}] + new_rel + + let enter ctx r f args = + let calle_rel = make_callee_rel ~thread:false ctx f args in + [ctx.local, {ctx.local with rel = calle_rel}] let body ctx f = let st = ctx.local in @@ -627,12 +631,22 @@ struct if not (ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx)) then ignore (Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st); let st' = Priv.threadenter (Analyses.ask_of_ctx ctx) ctx.global st in - let arg_vars = - fd.sformals - |> List.filter RD.Tracked.varinfo_tracked - |> List.map RV.arg + (* TODO: Deduplicate with enter *) + let arg_assigns = + GobList.combine_short fd.sformals args (* TODO: is it right to ignore missing formals/args? *) + |> List.filter (fun (x, _) -> RD.Tracked.varinfo_tracked x) + |> List.map (Tuple2.map1 RV.arg) in - let new_rel = RD.add_vars st'.rel arg_vars in + let reachable_from_args = List.fold (fun ls e -> Queries.LS.join ls (ctx.ask (ReachableFrom e))) (Queries.LS.empty ()) args in + let arg_vars = List.map fst arg_assigns in + let new_rel = RD.add_vars st.rel arg_vars in + let any_local_reachable = any_local_reachable fd reachable_from_args in + RD.remove_filter_with new_rel (fun var -> + match RV.find_metadata var with + | Some (Local _) when not (pass_to_callee fd any_local_reachable var) -> true (* remove caller locals provided they are unreachable *) + | Some (Arg _) when not (List.mem_cmp RD.Var.compare var arg_vars) -> true (* remove caller args, but keep just added args *) + | _ -> false (* keep everything else (just added args, globals, global privs) *) + ); [{st' with rel = new_rel}] | exception Not_found -> (* Unknown functions *) From 3d60727a3e07e76e4c308e5ef62fb1f5277471b1 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Wed, 14 Jun 2023 18:11:28 +0200 Subject: [PATCH 18/22] RelationAnalysis.threadenter: Deduplicate code with enter. --- src/analyses/apron/relationAnalysis.apron.ml | 37 +++++++------------- 1 file changed, 12 insertions(+), 25 deletions(-) diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index 3908e24577..4d8ad8a78e 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -283,9 +283,6 @@ struct let make_callee_rel ~thread ctx f args = let fundec = Node.find_fundec ctx.node in let st = ctx.local in - if M.tracing then M.tracel "combine" "relation enter f: %a\n" CilType.Varinfo.pretty f.svar; - if M.tracing then M.tracel "combine" "relation enter formals: %a\n" (d_list "," CilType.Varinfo.pretty) f.sformals; - if M.tracing then M.tracel "combine" "relation enter local: %a\n" D.pretty ctx.local; let arg_assigns = GobList.combine_short f.sformals args (* TODO: is it right to ignore missing formals/args? *) |> List.filter (fun (x, _) -> RD.Tracked.varinfo_tracked x) @@ -296,12 +293,17 @@ struct let new_rel = RD.add_vars st.rel arg_vars in (* RD.assign_exp_parallel_with new_rel arg_assigns; (* doesn't need to be parallel since exps aren't arg vars directly *) *) (* TODO: parallel version of assign_from_globals_wrapper? *) - let ask = Analyses.ask_of_ctx ctx in - let new_rel = List.fold_left (fun new_rel (var, e) -> - assign_from_globals_wrapper ask ctx.global {st with rel = new_rel} e (fun rel' e' -> - RD.assign_exp rel' var e' (no_overflow ask e) - ) - ) new_rel arg_assigns + let new_rel = + if thread then + (* TODO: Why does test 63/16 not reach fixpoint without copy here? *) + RD.copy new_rel + else + let ask = Analyses.ask_of_ctx ctx in + List.fold_left (fun new_rel (var, e) -> + assign_from_globals_wrapper ask ctx.global {st with rel = new_rel} e (fun rel' e' -> + RD.assign_exp rel' var e' (no_overflow ask e) + ) + ) new_rel arg_assigns in let any_local_reachable = any_local_reachable fundec reachable_from_args in RD.remove_filter_with new_rel (fun var -> @@ -631,22 +633,7 @@ struct if not (ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx)) then ignore (Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st); let st' = Priv.threadenter (Analyses.ask_of_ctx ctx) ctx.global st in - (* TODO: Deduplicate with enter *) - let arg_assigns = - GobList.combine_short fd.sformals args (* TODO: is it right to ignore missing formals/args? *) - |> List.filter (fun (x, _) -> RD.Tracked.varinfo_tracked x) - |> List.map (Tuple2.map1 RV.arg) - in - let reachable_from_args = List.fold (fun ls e -> Queries.LS.join ls (ctx.ask (ReachableFrom e))) (Queries.LS.empty ()) args in - let arg_vars = List.map fst arg_assigns in - let new_rel = RD.add_vars st.rel arg_vars in - let any_local_reachable = any_local_reachable fd reachable_from_args in - RD.remove_filter_with new_rel (fun var -> - match RV.find_metadata var with - | Some (Local _) when not (pass_to_callee fd any_local_reachable var) -> true (* remove caller locals provided they are unreachable *) - | Some (Arg _) when not (List.mem_cmp RD.Var.compare var arg_vars) -> true (* remove caller args, but keep just added args *) - | _ -> false (* keep everything else (just added args, globals, global privs) *) - ); + let new_rel = make_callee_rel ~thread:true ctx fd args in [{st' with rel = new_rel}] | exception Not_found -> (* Unknown functions *) From a8c67225b724653b22c17e9449be6108a7e35d2c Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Mon, 26 Jun 2023 13:57:14 +0200 Subject: [PATCH 19/22] Extract check for thread-uniqueness out. --- src/analyses/threadEscape.ml | 17 ++++++++++------- 1 file changed, 10 insertions(+), 7 deletions(-) diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml index 9871d26a94..8a14f4102e 100644 --- a/src/analyses/threadEscape.ml +++ b/src/analyses/threadEscape.ml @@ -80,9 +80,9 @@ struct | `Top -> true | `Bot -> false in - let equal_current_not_unique current = function + let equal_current current = function | `Lifted tid -> - ThreadId.Thread.equal current tid && not (ThreadId.Thread.is_unique current) + ThreadId.Thread.equal current tid | `Top -> true | `Bot -> false in @@ -91,12 +91,15 @@ struct let possibly_started = ThreadIdSet.exists (possibly_started current) threads in if possibly_started then true - else if ThreadIdSet.exists (equal_current_not_unique current) threads then - (* Another instance of the non-unqiue current thread may have escaped the variable *) - true else - (* Check whether current unique thread has escaped the variable *) - D.mem v ctx.local + let current_is_unique = ThreadId.Thread.is_unique current in + let any_equal_current threads = ThreadIdSet.exists (equal_current current) threads in + if not current_is_unique && any_equal_current threads then + (* Another instance of the non-unqiue current thread may have escaped the variable *) + true + else + (* Check whether current unique thread has escaped the variable *) + D.mem v ctx.local | `Top -> true | `Bot -> From 491dfbd1b1f13fdd8cb5330bdb16c068a7de925b Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Mon, 26 Jun 2023 14:43:07 +0200 Subject: [PATCH 20/22] Move copy of relation to ensure that ctx.local.rel is not changed by following desctructive update. This ensures that new_rel is a disctinct object from ctx.local.rel to ensure that the latter is not modified by RD.remove_filter_with. --- src/analyses/apron/relationAnalysis.apron.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index 4d8ad8a78e..ab659e00ce 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -295,8 +295,7 @@ struct (* TODO: parallel version of assign_from_globals_wrapper? *) let new_rel = if thread then - (* TODO: Why does test 63/16 not reach fixpoint without copy here? *) - RD.copy new_rel + new_rel else let ask = Analyses.ask_of_ctx ctx in List.fold_left (fun new_rel (var, e) -> @@ -306,6 +305,9 @@ struct ) new_rel arg_assigns in let any_local_reachable = any_local_reachable fundec reachable_from_args in + + (* Copy to ensure that ctx.local.rel is not changed *) + let new_rel = RD.copy new_rel in RD.remove_filter_with new_rel (fun var -> match RV.find_metadata var with | Some (Local _) when not (pass_to_callee fundec any_local_reachable var) -> true (* remove caller locals provided they are unreachable *) From 44233f6ecc1ccf0d7af402ad1bd52889982dce55 Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Mon, 26 Jun 2023 14:48:34 +0200 Subject: [PATCH 21/22] Move RD.copy up, so that copy is performed on possibly smaller rel. --- src/analyses/apron/relationAnalysis.apron.ml | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index ab659e00ce..2b1165e3e0 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -290,7 +290,9 @@ struct in let reachable_from_args = List.fold (fun ls e -> Queries.LS.join ls (ctx.ask (ReachableFrom e))) (Queries.LS.empty ()) args in let arg_vars = List.map fst arg_assigns in - let new_rel = RD.add_vars st.rel arg_vars in + (* Copy to ensure that ctx.local.rel is not changed by remove_filter_with*) + let new_rel = RD.copy st.rel in + let new_rel = RD.add_vars new_rel arg_vars in (* RD.assign_exp_parallel_with new_rel arg_assigns; (* doesn't need to be parallel since exps aren't arg vars directly *) *) (* TODO: parallel version of assign_from_globals_wrapper? *) let new_rel = @@ -305,9 +307,6 @@ struct ) new_rel arg_assigns in let any_local_reachable = any_local_reachable fundec reachable_from_args in - - (* Copy to ensure that ctx.local.rel is not changed *) - let new_rel = RD.copy new_rel in RD.remove_filter_with new_rel (fun var -> match RV.find_metadata var with | Some (Local _) when not (pass_to_callee fundec any_local_reachable var) -> true (* remove caller locals provided they are unreachable *) From 90016e1acf0f7cae06bcee0baa5f6a6419c8028b Mon Sep 17 00:00:00 2001 From: Julian Erhard Date: Mon, 3 Jul 2023 13:05:25 +0200 Subject: [PATCH 22/22] AffineEqualityDomain: Perform explicit copy in add_vars, drop_vars, keep_vars, keep_filter. The operations on a relational domain (wihtout _with suffix) should ensure that the returned object is not physically equal. This way, the explicit copy in relationAnalysis.make_callee_rel can be avoided. --- src/analyses/apron/relationAnalysis.apron.ml | 4 +--- src/cdomains/apron/affineEqualityDomain.apron.ml | 4 ++++ 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index 2b1165e3e0..8988a83c76 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -290,9 +290,7 @@ struct in let reachable_from_args = List.fold (fun ls e -> Queries.LS.join ls (ctx.ask (ReachableFrom e))) (Queries.LS.empty ()) args in let arg_vars = List.map fst arg_assigns in - (* Copy to ensure that ctx.local.rel is not changed by remove_filter_with*) - let new_rel = RD.copy st.rel in - let new_rel = RD.add_vars new_rel arg_vars in + let new_rel = RD.add_vars st.rel arg_vars in (* RD.assign_exp_parallel_with new_rel arg_assigns; (* doesn't need to be parallel since exps aren't arg vars directly *) *) (* TODO: parallel version of assign_from_globals_wrapper? *) let new_rel = diff --git a/src/cdomains/apron/affineEqualityDomain.apron.ml b/src/cdomains/apron/affineEqualityDomain.apron.ml index 6c24a46c6e..a6f00fdba0 100644 --- a/src/cdomains/apron/affineEqualityDomain.apron.ml +++ b/src/cdomains/apron/affineEqualityDomain.apron.ml @@ -79,12 +79,14 @@ struct let change_d t new_env add del = timing_wrap "dimension change" (change_d t new_env add) del let add_vars t vars = + let t = copy t in let env' = add_vars t.env vars in change_d t env' true false let add_vars t vars = timing_wrap "add_vars" (add_vars t) vars let drop_vars t vars del = + let t = copy t in let env' = remove_vars t.env vars in change_d t env' false del @@ -111,12 +113,14 @@ struct t.env <- t'.env let keep_filter t f = + let t = copy t in let env' = keep_filter t.env f in change_d t env' false false let keep_filter t f = timing_wrap "keep_filter" (keep_filter t) f let keep_vars t vs = + let t = copy t in let env' = keep_vars t.env vs in change_d t env' false false