Skip to content

Add explicit W set to base protection privatization #1693

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

Add explicit W set to base protection privatization #1693

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
734c149
Add explicit W set to base protection privatization
sim642 Feb 20, 2025
bb0be36
Promote base protection privatization changes in cram test
sim642 Feb 20, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
58 changes: 38 additions & 20 deletions src/analyses/basePriv.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -899,18 +899,25 @@ struct
let name () = "P"
end

(* W is implicitly represented by CPA domain *)
module D = P
(** May written variables. *)
module W =
struct
include MayVars
let name () = "W"
end

module D = Lattice.Prod (P) (W)

module Wrapper = Wrapper (VD)
module G = Wrapper.G
module V = ProtectionBasedV.V

let startstate () = P.empty ()
let startstate () = P.empty (), W.empty ()

let read_global (ask: Queries.ask) getg (st: BaseComponents (D).t) x =
let getg = Wrapper.getg ask getg in
if P.mem x st.priv then
let (p, _) = st.priv in
if P.mem x p then
CPA.find x st.cpa
else if Param.handle_atomic && ask.f MustBeAtomic then
VD.join (CPA.find x st.cpa) (getg (V.unprotected x)) (* Account for previous unpublished unprotected writes in current atomic section. *)
Expand All @@ -921,28 +928,35 @@ struct

let write_global ?(invariant=false) (ask: Queries.ask) getg sideg (st: BaseComponents (D).t) x v =
let sideg = Wrapper.sideg ask sideg in
if not invariant then (
if not (Param.handle_atomic && ask.f MustBeAtomic) then
sideg (V.unprotected x) v; (* Delay publishing unprotected write in the atomic section. *)
if !earlyglobs && not (ThreadFlag.is_currently_multi ask) then (* earlyglobs workaround for 13/60 *)
sideg (V.protected x) v (* Also side to protected because with earlyglobs enter_multithreaded does not side everything to protected *)
(* Unlock after invariant will still side effect refined value (if protected) from CPA, because cannot distinguish from non-invariant write since W is implicit. *)
);
let (p, w) = st.priv in
let w' =
if not invariant then (
if not (Param.handle_atomic && ask.f MustBeAtomic) then
sideg (V.unprotected x) v; (* Delay publishing unprotected write in the atomic section. *)
if !earlyglobs && not (ThreadFlag.is_currently_multi ask) then (* earlyglobs workaround for 13/60 *)
sideg (V.protected x) v; (* Also side to protected because with earlyglobs enter_multithreaded does not side everything to protected *)
(* Unlock after invariant will still side effect refined value (if protected) from CPA, because cannot distinguish from non-invariant write since W is implicit. *)
W.add x w
)
else
w
in
if Param.handle_atomic && ask.f MustBeAtomic then
{st with cpa = CPA.add x v st.cpa; priv = P.add x st.priv} (* Keep write local as if it were protected by the atomic section. *)
{st with cpa = CPA.add x v st.cpa; priv = (P.add x p, w')} (* Keep write local as if it were protected by the atomic section. *)
else if is_unprotected ask x then
st
else
{st with cpa = CPA.add x v st.cpa; priv = P.add x st.priv}
{st with cpa = CPA.add x v st.cpa; priv = (P.add x p, w')}

let lock ask getg st m = st

let unlock ask getg sideg (st: BaseComponents (D).t) m =
let sideg = Wrapper.sideg ask sideg in
let atomic = Param.handle_atomic && LockDomain.MustLock.equal m (LockDomain.MustLock.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) ->
let (_, w) = st.priv in
W.fold (fun x (st: BaseComponents (D).t) ->
if is_protected_by ask m x then ( (* is_in_Gm *)
let v = CPA.find x st.cpa in
(* Extra precision in implementation to pass tests:
If global is read-protected by multiple locks,
then inner unlock shouldn't yet publish. *)
Expand All @@ -951,14 +965,16 @@ struct
if atomic then
sideg (V.unprotected x) v; (* Publish delayed unprotected write as if it were protected by the atomic section. *)

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}
if is_unprotected_without ask x m then ( (* is_in_V' *)
let (p, w) = st.priv in
{st with cpa = CPA.remove x st.cpa; priv = (P.remove x p, W.remove x w)}
)
else
st
)
else
st
) st.cpa st
) w st

let sync ask getg sideg (st: BaseComponents (D).t) reason =
let branched_sync () =
Expand All @@ -968,7 +984,8 @@ struct
if is_global ask x && is_unprotected ask x then (
sideg (V.unprotected x) v;
sideg (V.protected x) v; (* must be like enter_multithreaded *)
{st with cpa = CPA.remove x st.cpa; priv = P.remove x st.priv}
let (p, w) = st.priv in
{st with cpa = CPA.remove x st.cpa; priv = (P.remove x p, W.remove x w)}
)
else
st
Expand Down Expand Up @@ -1007,7 +1024,8 @@ struct
if is_global ask x then (
sideg (V.unprotected x) v;
sideg (V.protected x) v;
{st with cpa = CPA.remove x st.cpa; priv = P.remove x st.priv}
let (p, w) = st.priv in
{st with cpa = CPA.remove x st.cpa; priv = (P.remove x p, W.remove x w)}
)
else
st
Expand Down
20 changes: 10 additions & 10 deletions tests/regression/00-sanity/33-hoare-over-paths.t
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,7 +18,7 @@
Local {
r -> ⊤
}
}, {}, {}, {}),
}, {}, {}, (P:{}, W:{})),
threadid:(wrapper call:unknown node, Thread:[main], created:(current function:bot, callees:bot)),
threadflag:Singlethreaded,
threadreturn:true,
Expand All @@ -41,7 +41,7 @@
r ->
(Not {0}([-31,31]))
}
}, {}, {}, {}),
}, {}, {}, (P:{}, W:{})),
threadid:(wrapper call:unknown node, Thread:[main], created:(current function:bot, callees:bot)),
threadflag:Singlethreaded,
threadreturn:true,
Expand All @@ -63,7 +63,7 @@
Local {
r -> 0
}
}, {}, {}, {}),
}, {}, {}, (P:{}, W:{})),
threadid:(wrapper call:unknown node, Thread:[main], created:(current function:bot, callees:bot)),
threadflag:Singlethreaded,
threadreturn:true,
Expand All @@ -85,7 +85,7 @@
Local {
r -> 0
}
}, {}, {}, {}),
}, {}, {}, (P:{}, W:{})),
threadid:(wrapper call:unknown node, Thread:[main], created:(current function:bot, callees:bot)),
threadflag:Singlethreaded,
threadreturn:true,
Expand All @@ -107,7 +107,7 @@
Local {
r -> 0
}
}, {}, {}, {}),
}, {}, {}, (P:{}, W:{})),
threadid:(wrapper call:unknown node, Thread:[main], created:(current function:bot, callees:bot)),
threadflag:Singlethreaded,
threadreturn:true,
Expand All @@ -129,7 +129,7 @@
Local {
r -> 0
}
}, {}, {}, {}),
}, {}, {}, (P:{}, W:{})),
threadid:(wrapper call:unknown node, Thread:[main], created:(current function:bot, callees:bot)),
threadflag:Singlethreaded,
threadreturn:true,
Expand All @@ -150,7 +150,7 @@
Local {
r -> 0
}
}, {}, {}, {}),
}, {}, {}, (P:{}, W:{})),
threadid:(wrapper call:unknown node, Thread:[main], created:(current function:bot, callees:bot)),
threadflag:Singlethreaded,
threadreturn:true,
Expand All @@ -169,7 +169,7 @@
Global {
m -> mutex
}
}, {}, {}, {}),
}, {}, {}, (P:{}, W:{})),
threadid:(wrapper call:unknown node, Thread:[main], created:(current function:bot, callees:bot)),
threadflag:Singlethreaded,
threadreturn:true,
Expand All @@ -191,7 +191,7 @@
Temp {
RETURN -> 0
}
}, {}, {}, {}),
}, {}, {}, (P:{}, W:{})),
threadid:(wrapper call:unknown node, Thread:[main], created:(current function:bot, callees:bot)),
threadflag:Singlethreaded,
threadreturn:true,
Expand All @@ -212,7 +212,7 @@
Temp {
RETURN -> 0
}
}, {}, {}, {}),
}, {}, {}, (P:{}, W:{})),
threadid:(wrapper call:unknown node, Thread:[main], created:(current function:bot, callees:bot)),
threadflag:Singlethreaded,
threadreturn:true,
Expand Down
Loading