Skip to content
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

Continue refactoring of must-locksets to use definite mvals instead of addresses #1503

Merged
merged 5 commits into from
Jul 28, 2024
Merged

Continue refactoring of must-locksets to use definite mvals instead of addresses #1503

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
682eb0c
Refactor many privatizations to use LockDomain.MustLockset
sim642 Jun 4, 2024
3e1d228
Merge branch 'priv-nondefinite-mutex' into priv-mval
sim642 Jun 4, 2024
aeae2a9
Refactor privatizations' lock and unlock mutex type to Mustlock
sim642 Jun 4, 2024
500b452
Remove now-unnecessary must lockset functions
sim642 Jun 4, 2024
90fc5aa
Refine MustBeProtectedBy and MayBePublicWithout query mutex type
sim642 Jun 4, 2024
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
28 changes: 14 additions & 14 deletions src/analyses/apron/relationPriv.apron.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,8 +33,8 @@ module type S =
the state when following conditional guards. *)
val write_global: ?invariant:bool -> Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> varinfo -> varinfo -> relation_components_t

val lock: Q.ask -> (V.t -> G.t) -> relation_components_t -> LockDomain.Addr.t -> relation_components_t
val unlock: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> LockDomain.Addr.t -> relation_components_t
val lock: Q.ask -> (V.t -> G.t) -> relation_components_t -> LockDomain.MustLock.t -> relation_components_t
val unlock: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> LockDomain.MustLock.t -> relation_components_t

val sync: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> relation_components_t -> [`Normal | `Join | `Return | `Init | `Thread] -> relation_components_t

Expand Down Expand Up @@ -471,7 +471,7 @@ struct

let startstate () = ()

let atomic_mutex = LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var
let atomic_mutex = LockDomain.MustLock.of_var LibraryFunctions.verifier_atomic_var

let get_m_with_mutex_inits ask getg m =
let get_m = getg (V.mutex m) in
Expand Down Expand Up @@ -577,9 +577,9 @@ struct
let write_escape = write_global_internal ~skip_meet:true

let lock ask getg (st: relation_components_t) m =
let atomic = Param.handle_atomic && LockDomain.Addr.equal m (atomic_mutex) in
let atomic = Param.handle_atomic && LockDomain.MustLock.equal m atomic_mutex in
(* TODO: somehow actually unneeded here? *)
if not atomic && Locksets.(not (Lockset.mem m (current_lockset ask))) then (
if not atomic && Locksets.(not (MustLockset.mem m (current_lockset ask))) then (
let rel = st.rel in
let get_m = get_m_with_mutex_inits ask getg m in
(* Additionally filter get_m in case it contains variables it no longer protects. E.g. in 36/22. *)
Expand All @@ -592,7 +592,7 @@ struct
st (* sound w.r.t. recursive lock *)

let unlock ask getg sideg (st: relation_components_t) m: relation_components_t =
let atomic = Param.handle_atomic && LockDomain.Addr.equal m (atomic_mutex) in
let atomic = Param.handle_atomic && LockDomain.MustLock.equal m atomic_mutex in
let rel = st.rel in
if not atomic then (
let rel_side = keep_only_protected_globals ask m rel in
Expand Down Expand Up @@ -703,7 +703,7 @@ module type ClusterArg = functor (RD: RelationDomain.RD) ->
sig
module LRD: Lattice.S

val keep_only_protected_globals: Q.ask -> LockDomain.Addr.t -> LRD.t -> LRD.t
val keep_only_protected_globals: Q.ask -> LockDomain.MustLock.t -> LRD.t -> LRD.t
val keep_global: varinfo -> LRD.t -> LRD.t

val lock: RD.t -> LRD.t -> LRD.t -> RD.t
Expand Down Expand Up @@ -962,7 +962,7 @@ struct

let get_m_with_mutex_inits inits ask getg m =
let get_m = get_relevant_writes ask m (G.mutex @@ getg (V.mutex m)) in
if M.tracing then M.traceli "relationpriv" "get_m_with_mutex_inits %a\n get=%a" LockDomain.Addr.pretty m LRD.pretty get_m;
if M.tracing then M.traceli "relationpriv" "get_m_with_mutex_inits %a\n get=%a" LockDomain.MustLock.pretty m LRD.pretty get_m;
let r =
if not inits then
get_m
Expand All @@ -975,7 +975,7 @@ struct
if M.tracing then M.traceu "relationpriv" "-> %a" LRD.pretty r;
r

let atomic_mutex = LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var
let atomic_mutex = LockDomain.MustLock.of_var LibraryFunctions.verifier_atomic_var

let get_mutex_global_g_with_mutex_inits inits ask getg g =
let get_mutex_global_g =
Expand Down Expand Up @@ -1088,8 +1088,8 @@ struct
{rel = rel_local; priv = (W.add g w,lmust,l)} (* Keep write local as if it were protected by the atomic section. *)

let lock ask getg (st: relation_components_t) m =
let atomic = Param.handle_atomic && LockDomain.Addr.equal m (atomic_mutex) in
if not atomic && Locksets.(not (Lockset.mem m (current_lockset ask))) then (
let atomic = Param.handle_atomic && LockDomain.MustLock.equal m atomic_mutex in
if not atomic && Locksets.(not (MustLockset.mem m (current_lockset ask))) then (
let rel = st.rel in
let _,lmust,l = st.priv in
let lm = LLock.mutex m in
Expand All @@ -1112,7 +1112,7 @@ struct
RD.keep_filter oct protected

let unlock ask getg sideg (st: relation_components_t) m: relation_components_t =
let atomic = Param.handle_atomic && LockDomain.Addr.equal m (atomic_mutex) in
let atomic = Param.handle_atomic && LockDomain.MustLock.equal m atomic_mutex in
let rel = st.rel in
let w,lmust,l = st.priv in
if not atomic then (
Expand Down Expand Up @@ -1290,7 +1290,7 @@ struct
r

let lock ask getg st m =
if M.tracing then M.traceli "relationpriv" "lock %a" LockDomain.Addr.pretty m;
if M.tracing then M.traceli "relationpriv" "lock %a" LockDomain.MustLock.pretty m;
if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pretty st;
let getg x =
let r = getg x in
Expand All @@ -1302,7 +1302,7 @@ struct
r

let unlock ask getg sideg st m =
if M.tracing then M.traceli "relationpriv" "unlock %a" LockDomain.Addr.pretty m;
if M.tracing then M.traceli "relationpriv" "unlock %a" LockDomain.MustLock.pretty m;
if M.tracing then M.trace "relationpriv" "st: %a" RelComponents.pretty st;
let getg x =
let r = getg x in
Expand Down
Loading
Loading