From d0a8cb890f54f1a6a4a3da6d193f32692dfd44e4 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 14 Aug 2026 17:07:59 +0800 Subject: [PATCH 1/3] Fix Apron handling of escaped locals --- src/analyses/apron/relationAnalysis.apron.ml | 7 +++++-- tests/regression/89-apron3/05-escaped-local.c | 17 +++++++++++++++++ 2 files changed, 22 insertions(+), 2 deletions(-) create mode 100644 tests/regression/89-apron3/05-escaped-local.c diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index e101074c16..c09b4cb7da 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -134,7 +134,9 @@ struct Priv.write_global ask getg sideg st g x else ( let rel = st.rel in - let g_var = RV.global g in + (* Escaped locals remain represented by their local variable until the + program becomes multithreaded, just like in [read_global]. *) + let g_var = if g.vglob then RV.global g else RV.local g in let x_var = RV.local x in let rel' = RD.add_vars rel [g_var] in let rel' = RD.assign_var rel' g_var x_var in @@ -327,7 +329,7 @@ struct let any_local_reachable = any_local_reachable fundec reachable_from_args in RD.remove_filter_with new_rel (fun var -> match RV.find_metadata var with - | Some (Local _) when not (belongs_to_fundec fundec var || any_local_reachable) -> true (* remove caller locals provided they are unreachable *) + | Some (Local v) when not (belongs_to_fundec fundec var || any_local_reachable || ThreadEscape.has_escaped (Analyses.ask_of_man man) v) -> true (* remove caller locals provided they are unreachable *) | Some (Arg _) when not (List.mem_cmp Apron.Var.compare var arg_vars) -> true (* remove caller args, but keep just added args *) | _ -> false (* keep everything else (just added args, globals, global privs) *) ); @@ -422,6 +424,7 @@ struct let tainted_vars = TaintPartialContexts.conv_varset tainted in let new_rel = RD.keep_filter st.rel (fun var -> match RV.find_metadata var with + | Some (Local v) when ThreadEscape.has_escaped ask v -> false (* escaped locals may be modified through globals *) | Some (Local _) when not (belongs_to_fundec fundec var || any_local_reachable) -> true (* keep caller locals, provided they were not passed to the function *) | Some (Arg _) -> true (* keep caller args *) | Some ((Local _ | Global _)) when not (RD.mem_var new_fun_rel var) -> false (* remove locals and globals, for which no record exists in the new_fun_apr *) diff --git a/tests/regression/89-apron3/05-escaped-local.c b/tests/regression/89-apron3/05-escaped-local.c new file mode 100644 index 0000000000..d60723a7ad --- /dev/null +++ b/tests/regression/89-apron3/05-escaped-local.c @@ -0,0 +1,17 @@ +// PARAM: --set ana.activated[+] apron --enable ana.sv-comp.functions +#include + +static int *target; + +static void modify(void) { + *target = __VERIFIER_nondet_int(); +} + +int main(void) { + int left = __VERIFIER_nondet_int(); + int right = left; + target = &right; + + modify(); + __goblint_check(left == right); // UNKNOWN! +} From 1bdcb709cb3aab16a93c31e6b0964f94d1214d36 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Fri, 14 Aug 2026 17:12:46 +0800 Subject: [PATCH 2/3] Test escaped local after entering multithreaded mode --- .../06-escaped-local-enter-multithreaded.c | 25 +++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 tests/regression/89-apron3/06-escaped-local-enter-multithreaded.c diff --git a/tests/regression/89-apron3/06-escaped-local-enter-multithreaded.c b/tests/regression/89-apron3/06-escaped-local-enter-multithreaded.c new file mode 100644 index 0000000000..01ad65953c --- /dev/null +++ b/tests/regression/89-apron3/06-escaped-local-enter-multithreaded.c @@ -0,0 +1,25 @@ +// PARAM: --set ana.activated[+] apron --enable ana.sv-comp.functions +#include +#include + +static int *target; + +static void *modify(void *arg) { + *target = __VERIFIER_nondet_int(); + return NULL; +} + +static void enter_multithreaded_and_modify(void) { + pthread_t thread; + pthread_create(&thread, NULL, modify, NULL); + pthread_join(thread, NULL); +} + +int main(void) { + int left = __VERIFIER_nondet_int(); + int right = left; + target = &right; + + enter_multithreaded_and_modify(); + __goblint_check(left == right); // UNKNOWN! +} From 022ed5b19a57b17704230edac545a74c4a4e342d Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Tue, 18 Aug 2026 11:22:39 +0800 Subject: [PATCH 3/3] Restore symmetry --- src/analyses/apron/relationAnalysis.apron.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml index c09b4cb7da..c9152f6699 100644 --- a/src/analyses/apron/relationAnalysis.apron.ml +++ b/src/analyses/apron/relationAnalysis.apron.ml @@ -424,8 +424,7 @@ struct let tainted_vars = TaintPartialContexts.conv_varset tainted in let new_rel = RD.keep_filter st.rel (fun var -> match RV.find_metadata var with - | Some (Local v) when ThreadEscape.has_escaped ask v -> false (* escaped locals may be modified through globals *) - | Some (Local _) when not (belongs_to_fundec fundec var || any_local_reachable) -> true (* keep caller locals, provided they were not passed to the function *) + | Some (Local v) when not (belongs_to_fundec fundec var || any_local_reachable || ThreadEscape.has_escaped ask v) -> true (* keep caller locals, provided they were not passed to the function *) | Some (Arg _) -> true (* keep caller args *) | Some ((Local _ | Global _)) when not (RD.mem_var new_fun_rel var) -> false (* remove locals and globals, for which no record exists in the new_fun_apr *) | Some ((Local v | Global v)) when not (TaintPartialContexts.VS.mem v tainted_vars) -> true (* keep locals and globals, which have not been touched by the call *)