From 8d68957b55dfb2c6eb72dd5fc39098d4997c02f5 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 9 Jan 2025 16:48:55 +0200 Subject: [PATCH 1/2] Add test for base mutex-meet-tid where spurious write from invariant ruins precision --- src/analyses/apron/relationPriv.apron.ml | 2 ++ src/analyses/basePriv.ml | 1 + .../13-privatized/97-refine-protected3.c | 30 +++++++++++++++++++ 3 files changed, 33 insertions(+) create mode 100644 tests/regression/13-privatized/97-refine-protected3.c diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index 257bec24d8..542982f452 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -552,6 +552,7 @@ struct (** Like write global but has option to skip meet with current value, as the value will not have been side-effected to a useful location thus far *) let write_global_internal ?(skip_meet=false) ?(invariant=false) (ask: Q.ask) getg sideg (st: relation_components_t) g x: relation_components_t = + (* TODO: use invariant? *) let atomic = Param.handle_atomic && ask.f MustBeAtomic in let rel = st.rel in (* lock *) @@ -1102,6 +1103,7 @@ struct rel_local (* Keep write local as if it were protected by the atomic section. *) let write_global ?(invariant=false) (ask:Q.ask) getg sideg (st: relation_components_t) g x: relation_components_t = + (* TODO: use invariant? *) let atomic = Param.handle_atomic && ask.f MustBeAtomic in let w,lmust,l = st.priv in let lm = LLock.global g in diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index ff4a53f6ac..676500e329 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -565,6 +565,7 @@ struct v let write_global ?(invariant=false) ask getg sideg (st: BaseComponents (D).t) x v = + (* TODO: use invariant? *) let w,lmust,l = st.priv in let lm = LLock.global x in let cpa' = diff --git a/tests/regression/13-privatized/97-refine-protected3.c b/tests/regression/13-privatized/97-refine-protected3.c new file mode 100644 index 0000000000..134400b96f --- /dev/null +++ b/tests/regression/13-privatized/97-refine-protected3.c @@ -0,0 +1,30 @@ +// PARAM: --set ana.base.privatization mutex-meet-tid --set ana.path_sens[+] threadflag +#include +#include + +int g = 0; + +pthread_mutex_t A = PTHREAD_MUTEX_INITIALIZER; + +void *t_fun(void *arg) { + pthread_mutex_lock(&A); + g = 1; + pthread_mutex_unlock(&A); + pthread_mutex_lock(&A); + __goblint_check(g == 1); + pthread_mutex_unlock(&A); + return NULL; +} + +int main() { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + + pthread_mutex_lock(&A); + if (g) // protected globals should be refined, but should not emit writes that ruin check in t_fun + __goblint_check(g); + else + __goblint_check(!g); + pthread_mutex_unlock(&A); + return 0; +} From 923bb18184c30cc136748e915a95711ebd77b5f7 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 9 Jan 2025 16:53:55 +0200 Subject: [PATCH 2/2] Avoid spurious writes for invariants in base mutex-meet-tid --- src/analyses/basePriv.ml | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 676500e329..100765aaf3 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -585,8 +585,14 @@ struct else l' in - sideg (V.global x) (G.create_global sidev); - {st with cpa = cpa'; priv = (W.add x w,LMust.add lm lmust,l')} + let w' = if not invariant then + W.add x w + else + w (* No need to add invariant to W because it doesn't matter for reads after invariant, only unlocks. *) + in + if not invariant then + sideg (V.global x) (G.create_global sidev); + {st with cpa = cpa'; priv = (w',LMust.add lm lmust,l')} let lock (ask: Queries.ask) getg (st: BaseComponents (D).t) m = if Locksets.(not (MustLockset.mem m (current_lockset ask))) then (