Separate base privatization with atomic support

goblint · Jan 11, 2024 · f754362 · f754362
1 parent 43552fa
commit f754362
Show file tree

Hide file tree

Showing 5 changed files with 19 additions and 9 deletions.
diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml
@@ -640,6 +640,8 @@ module type PerGlobalPrivParam =
 sig
   (** Whether to also check unprotectedness by reads for extra precision. *)
   val check_read_unprotected: bool
+
+  include AtomicParam
 end
 
 (** Protection-Based Reading. *)
@@ -690,7 +692,7 @@ struct
   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
+    else if Param.handle_atomic && 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 *)
@@ -699,13 +701,13 @@ struct
 
   let write_global ?(invariant=false) (ask: Queries.ask) getg sideg (st: BaseComponents (D).t) x v =
     if not invariant then (
-      if not (ask.f MustBeAtomic) then
+      if not (Param.handle_atomic && 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 ask.f MustBeAtomic then
+    if Param.handle_atomic && 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
@@ -715,7 +717,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
+    let atomic = Param.handle_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 *)
@@ -1804,8 +1806,10 @@ let priv_module: (module S) Lazy.t =
         | "mutex-oplus" -> (module PerMutexOplusPriv)
         | "mutex-meet" -> (module PerMutexMeetPriv)
         | "mutex-meet-tid" -> (module PerMutexMeetTIDPriv)
-        | "protection" -> (module ProtectionBasedPriv (struct let check_read_unprotected = false end))
-        | "protection-read" -> (module ProtectionBasedPriv (struct let check_read_unprotected = true end))
+        | "protection" -> (module ProtectionBasedPriv (struct let check_read_unprotected = false let handle_atomic = false end))
+        | "protection-atomic" -> (module ProtectionBasedPriv (struct let check_read_unprotected = false let handle_atomic = true end))
+        | "protection-read" -> (module ProtectionBasedPriv (struct let check_read_unprotected = true let handle_atomic = false end))
+        | "protection-read-atomic" -> (module ProtectionBasedPriv (struct let check_read_unprotected = true let handle_atomic = true end))
         | "mine" -> (module MinePriv)
         | "mine-nothread" -> (module MineNoThreadPriv)
         | "mine-W" -> (module MineWPriv (struct let side_effect_global_init = true end))

diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
@@ -9,6 +9,12 @@ module Q = Queries
 module IdxDom = ValueDomain.IndexDomain
 module VD     = BaseDomain.VD
 
+module type AtomicParam =
+sig
+  val handle_atomic: bool
+  (** Whether to handle SV-COMP atomic blocks. *)
+end
+
 module ConfCheck =
 struct
   module RequireMutexActivatedInit =

diff --git a/src/common/util/options.schema.json b/src/common/util/options.schema.json
@@ -767,7 +767,7 @@
               "description":
                 "Which privatization to use? none/mutex-oplus/mutex-meet/mutex-meet-tid/protection/protection-read/mine/mine-nothread/mine-W/mine-W-noinit/lock/write/write+lock",
               "type": "string",
-              "enum": ["none", "mutex-oplus", "mutex-meet", "protection", "protection-read", "mine", "mine-nothread", "mine-W", "mine-W-noinit", "lock", "write", "write+lock","mutex-meet-tid"],
+              "enum": ["none", "mutex-oplus", "mutex-meet", "protection", "protection-atomic", "protection-read", "protection-read-atomic", "mine", "mine-nothread", "mine-W", "mine-W-noinit", "lock", "write", "write+lock","mutex-meet-tid"],
               "default": "protection-read"
             },
             "priv": {

diff --git a/tests/regression/29-svcomp/16-atomic_priv.c b/tests/regression/29-svcomp/16-atomic_priv.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.sv-comp.functions
+// PARAM: --enable ana.sv-comp.functions --set ana.base.privatization protection-atomic
 #include <pthread.h>
 #include <goblint.h>
 

diff --git a/tests/regression/29-svcomp/18-atomic_fun_priv.c b/tests/regression/29-svcomp/18-atomic_fun_priv.c
@@ -1,4 +1,4 @@
-// PARAM: --enable ana.sv-comp.functions
+// PARAM: --enable ana.sv-comp.functions --set ana.base.privatization protection-atomic
 #include <pthread.h>
 #include <goblint.h>