From 1d05f0fefa2e1acf5a35f90365df4b7ba4bdd858 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Thu, 12 Oct 2023 13:00:52 +0300
Subject: [PATCH] Add hacky atomic protection privatization

---
 src/analyses/basePriv.ml                        | 16 ++++++++++++----
 src/analyses/mutexAnalysis.ml                   |  4 ++--
 tests/regression/29-svcomp/16-atomic_priv.c     |  2 +-
 tests/regression/29-svcomp/18-atomic_fun_priv.c |  2 +-
 4 files changed, 16 insertions(+), 8 deletions(-)

diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
index 0154924a1c..82bdebe617 100644
--- a/src/analyses/basePriv.ml
+++ b/src/analyses/basePriv.ml
@@ -687,22 +687,27 @@ struct
 
   let startstate () = P.empty ()
 
-  let read_global ask getg (st: BaseComponents (D).t) x =
+  let read_global (ask: Queries.ask) getg (st: BaseComponents (D).t) x =
     if P.mem x st.priv then
       CPA.find x st.cpa
+    else if ask.f MustBeAtomic then
+      VD.join (CPA.find x st.cpa) (getg (V.unprotected x))
     else if is_unprotected ask x then
       getg (V.unprotected x) (* CPA unnecessary because all values in GUnprot anyway *)
     else
       VD.join (CPA.find x st.cpa) (getg (V.protected x))
 
-  let write_global ?(invariant=false) ask getg sideg (st: BaseComponents (D).t) x v =
+  let write_global ?(invariant=false) (ask: Queries.ask) getg sideg (st: BaseComponents (D).t) x v =
     if not invariant then (
-      sideg (V.unprotected x) v;
+      if not (ask.f MustBeAtomic) then
+        sideg (V.unprotected x) v;
       if !earlyglobs then (* earlyglobs workaround for 13/60 *)
         sideg (V.protected x) v
         (* Unlock after invariant will still side effect refined value (if protected) from CPA, because cannot distinguish from non-invariant write since W is implicit. *)
     );
-    if is_unprotected ask x then
+    if ask.f MustBeAtomic then
+      {st with cpa = CPA.add x v st.cpa; priv = P.add x st.priv}
+    else if is_unprotected ask x then
       st
     else
       {st with cpa = CPA.add x v st.cpa; priv = P.add x st.priv}
@@ -710,6 +715,7 @@ struct
   let lock ask getg st m = st
 
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
+    let atomic = LockDomain.Addr.equal m (LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var) in
     (* TODO: what about G_m globals in cpa that weren't actually written? *)
     CPA.fold (fun x v (st: BaseComponents (D).t) ->
         if is_protected_by ask m x then ( (* is_in_Gm *)
@@ -718,6 +724,8 @@ struct
              then inner unlock shouldn't yet publish. *)
           if not Param.check_read_unprotected || is_unprotected_without ask ~write:false x m then
             sideg (V.protected x) v;
+          if atomic then
+            sideg (V.unprotected x) v;
 
           if is_unprotected_without ask x m then (* is_in_V' *)
             {st with cpa = CPA.remove x st.cpa; priv = P.remove x st.priv}
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index ee050f55ca..702b3b4224 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -229,9 +229,9 @@ struct
       let mutex_lockset = Lockset.export_locks @@ Lockset.singleton (mutex, true) in
       let protecting = protecting ~write protection v in
       (* TODO: unsound in 29/24, why did we do this before? *)
-      (* if LockDomain.Addr.equal mutex verifier_atomic then
+      if LockDomain.Addr.equal mutex (LockDomain.Addr.of_var LF.verifier_atomic_var) then
         true
-      else *)
+      else
       Mutexes.leq mutex_lockset protecting
     | Queries.MustLockset ->
       let held_locks = Lockset.export_locks (Lockset.filter snd ls) in
diff --git a/tests/regression/29-svcomp/16-atomic_priv.c b/tests/regression/29-svcomp/16-atomic_priv.c
index 92e1896f58..103769cc33 100644
--- a/tests/regression/29-svcomp/16-atomic_priv.c
+++ b/tests/regression/29-svcomp/16-atomic_priv.c
@@ -21,7 +21,7 @@ void *t_fun(void *arg) {
 int main(void) {
   pthread_t id;
   pthread_create(&id, NULL, t_fun, NULL);
-  __goblint_check(myglobal == 5); // TODO
+  __goblint_check(myglobal == 5);
   __VERIFIER_atomic_begin();
   __goblint_check(myglobal == 5);
   __VERIFIER_atomic_end();
diff --git a/tests/regression/29-svcomp/18-atomic_fun_priv.c b/tests/regression/29-svcomp/18-atomic_fun_priv.c
index 0449f9af0d..cb7e790ebd 100644
--- a/tests/regression/29-svcomp/18-atomic_fun_priv.c
+++ b/tests/regression/29-svcomp/18-atomic_fun_priv.c
@@ -21,7 +21,7 @@ void *t_fun(void *arg) {
 int main(void) {
   pthread_t id;
   pthread_create(&id, NULL, t_fun, NULL);
-  __goblint_check(myglobal == 5); // TODO
+  __goblint_check(myglobal == 5);
   __VERIFIER_atomic_begin();
   __goblint_check(myglobal == 5);
   __VERIFIER_atomic_end();