Avoid spurious writes for invariants in base mutex-meet-tid

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

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' =
@@ -584,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 (

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 <pthread.h>
+#include <goblint.h>
+
+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;
+}