Skip to content

Commit

Permalink
Merge pull request #1503 from goblint/priv-mval
Browse files Browse the repository at this point in the history 
Continue refactoring of must-locksets to use definite mvals instead of addresses
  • Loading branch information
@sim642
sim642 committed Jul 28, 2024
2 parents bccb230 + 90fc5aa commit d86fe48
Show file tree
Hide file tree
Showing 7 changed files with 94 additions and 102 deletions.
28 changes: 14 additions & 14 deletions src/analyses/apron/relationPriv.apron.ml
View file
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 | `JoinCall | `Return | `Init | `Thread] -> relation_components_t

Expand Down Expand Up @@ -483,7 +483,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 @@ -589,9 +589,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 @@ -604,7 +604,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 @@ -721,7 +721,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 @@ -980,7 +980,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 @@ -993,7 +993,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 @@ -1106,8 +1106,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 @@ -1130,7 +1130,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 @@ -1314,7 +1314,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 @@ -1326,7 +1326,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

0 comments on commit d86fe48

Please sign in to comment.