From fd898de948c7f733c10a6013968f4abdacaf26da Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sat, 11 Feb 2023 19:31:53 +0100 Subject: [PATCH 1/3] Add problematic test by Felix --- tests/regression/06-symbeq/41-vareq_global.c | 28 ++++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 tests/regression/06-symbeq/41-vareq_global.c diff --git a/tests/regression/06-symbeq/41-vareq_global.c b/tests/regression/06-symbeq/41-vareq_global.c new file mode 100644 index 0000000000..ee78ba80fc --- /dev/null +++ b/tests/regression/06-symbeq/41-vareq_global.c @@ -0,0 +1,28 @@ +//PARAM: --set ana.activated[+] var_eq +#include +#include +#include +int g; + +void *t_fun1(void *arg) { + int *zptr = (int*) arg; + int* gptr = &g; + + *zptr = 42; + *gptr = 42; + sleep(10); + // here the other thread (id2) could potentially change *zptr, as it is linked to the same int z + __goblint_check(*zptr == 42); //UNKNOWN! + __goblint_check(*gptr == 42); //UNKNOWN! + return NULL; +} + +int main() { + pthread_t id1; + int z = 8; + + pthread_create(&id1, NULL, t_fun1, &z); + z = 8; + g = 8; + pthread_join (id1, NULL); +} \ No newline at end of file From c60f4dd5e78589fe42ac0ef46311f5978b81f324 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sat, 11 Feb 2023 19:39:11 +0100 Subject: [PATCH 2/3] Consider escaping values in varEq. --- src/analyses/varEq.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml index 09f983cdd4..fb77f0d511 100644 --- a/src/analyses/varEq.ml +++ b/src/analyses/varEq.ml @@ -336,7 +336,7 @@ struct | Imag _ -> None | Const _ -> Some false | Lval (Var v,_) -> - Some (v.vglob || (ask.f (Queries.IsMultiple v))) + Some (v.vglob || (ask.f (Queries.IsMultiple v) || BaseUtil.is_global ask v)) | Lval (Mem e, _) -> begin match ask.f (Queries.MayPointTo e) with | ls when not (Queries.LS.is_top ls) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) ls) -> From 50f26f80bd5b2e13fe98bfa0fd3a2c269abc068f Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Sat, 11 Feb 2023 20:03:36 +0100 Subject: [PATCH 3/3] Handling escape event in varEq --- src/analyses/varEq.ml | 9 +++++++ tests/regression/06-symbeq/42-vareq_escape.c | 25 ++++++++++++++++++++ 2 files changed, 34 insertions(+) create mode 100644 tests/regression/06-symbeq/42-vareq_escape.c diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml index fb77f0d511..740ee1dfd4 100644 --- a/src/analyses/varEq.ml +++ b/src/analyses/varEq.ml @@ -558,6 +558,15 @@ struct |> List.fold_left (fun st lv -> remove (Analyses.ask_of_ctx ctx) lv st ) ctx.local + | Events.Escape vars -> + if EscapeDomain.EscapedVars.is_top vars then + D.top () + else + let ask = Analyses.ask_of_ctx ctx in + let remove_var st v = + remove ask (Cil.var v) st + in + List.fold_left remove_var ctx.local (EscapeDomain.EscapedVars.elements vars) | _ -> ctx.local end diff --git a/tests/regression/06-symbeq/42-vareq_escape.c b/tests/regression/06-symbeq/42-vareq_escape.c new file mode 100644 index 0000000000..e203c7d9a1 --- /dev/null +++ b/tests/regression/06-symbeq/42-vareq_escape.c @@ -0,0 +1,25 @@ +//PARAM: --set ana.activated[+] var_eq +#include +#include +#include +int g; + +void *t_fun1(void *arg) { + int** ptrptr = (int**) arg; + int* iptr = *ptrptr; + + *iptr = 12; +} + +int main() { + pthread_t id1; + int z = 8; + int i; + int* zptr = &z; + + int j = i; + pthread_create(&id1, NULL, t_fun1, &zptr); + zptr = &i; + __goblint_check(i == j); //UNKNOWN! + pthread_join (id1, NULL); +} \ No newline at end of file