From f754362c61302119850cd97fe777678ebfc565b8 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Thu, 11 Jan 2024 16:01:20 +0200 Subject: [PATCH] Separate base privatization with atomic support --- src/analyses/basePriv.ml | 16 ++++++++++------ src/analyses/commonPriv.ml | 6 ++++++ src/common/util/options.schema.json | 2 +- tests/regression/29-svcomp/16-atomic_priv.c | 2 +- tests/regression/29-svcomp/18-atomic_fun_priv.c | 2 +- 5 files changed, 19 insertions(+), 9 deletions(-) diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 069a3698dd..6aad979aab 100644 --- 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 index 63ba7abd54..5294c7dd50 100644 --- 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 index 7c921c4f53..bb4fa194df 100644 --- 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 index 103769cc33..2f39c0ee3a 100644 --- 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 #include diff --git a/tests/regression/29-svcomp/18-atomic_fun_priv.c b/tests/regression/29-svcomp/18-atomic_fun_priv.c index cb7e790ebd..13c03ffb48 100644 --- 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 #include