diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index e69757c7a8..078cab2ce8 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -653,7 +653,7 @@ struct let threadspawn (ask:Queries.ask) get set (st: BaseComponents (D).t) = let is_recovered_st = ask.f (Queries.MustBeSingleThreaded {since_start = false}) && not @@ ask.f (Queries.MustBeSingleThreaded {since_start = true}) in - let unprotected_after x = ask.f (Q.MayBePublic {global=x; write=true; protection=Weak}) in + let unprotected_after x = ask.f (Q.MayBePublic {global=x; kind=Write; protection=Weak}) in if is_recovered_st then (* Remove all things that are now unprotected *) let cpa' = CPA.fold (fun x v cpa -> @@ -771,7 +771,7 @@ struct (* Extra precision in implementation to pass tests: If global is read-protected by multiple locks, then inner unlock shouldn't yet publish. *) - if not Param.check_read_unprotected || is_unprotected_without ask ~write:false x m then + if not Param.check_read_unprotected || is_unprotected_without ask ~kind:ReadWrite x m then sideg (V.protected x) v; if atomic then sideg (V.unprotected x) v; (* Publish delayed unprotected write as if it were protected by the atomic section. *) diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml index 915b3da063..5c994824fd 100644 --- a/src/analyses/commonPriv.ml +++ b/src/analyses/commonPriv.ml @@ -82,26 +82,28 @@ end module Protection = struct open Q.Protection + open Q.ProtectionKind + let is_unprotected ask ?(protection=Strong) x: bool = let multi = if protection = Weak then ThreadFlag.is_currently_multi ask else ThreadFlag.has_ever_been_multi ask in (!GobConfig.earlyglobs && not multi && not (is_excluded_from_earlyglobs x)) || ( multi && - ask.f (Q.MayBePublic {global=x; write=true; protection}) + ask.f (Q.MayBePublic {global=x; kind=Write; protection}) ) - let is_unprotected_without ask ?(write=true) ?(protection=Strong) x m: bool = + let is_unprotected_without ask ?(kind=Write) ?(protection=Strong) x m: bool = (if protection = Weak then ThreadFlag.is_currently_multi ask else ThreadFlag.has_ever_been_multi ask) && - ask.f (Q.MayBePublicWithout {global=x; write; without_mutex=m; protection}) + ask.f (Q.MayBePublicWithout {global=x; kind; without_mutex=m; protection}) let is_protected_by ask ?(protection=Strong) m x: bool = is_global ask x && not (VD.is_immediate_type x.vtype) && - ask.f (Q.MustBeProtectedBy {mutex=m; global=x; write=true; protection}) + ask.f (Q.MustBeProtectedBy {mutex=m; global=x; kind=Write; protection}) let protected_vars (ask: Q.ask): varinfo list = LockDomain.MustLockset.fold (fun ml acc -> - Q.VS.join (ask.f (Q.MustProtectedVars {mutex = ml; write = true})) acc + Q.VS.join (ask.f (Q.MustProtectedVars {mutex = ml; kind = Write})) acc ) (ask.f Q.MustLockset) (Q.VS.empty ()) |> Q.VS.elements end diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml index 9b6aa4f4ca..0b9b80064a 100644 --- a/src/analyses/mutexAnalysis.ml +++ b/src/analyses/mutexAnalysis.ml @@ -60,25 +60,31 @@ struct let name () = "strong protection * weak protection" - let get ~write protection (s,w) = + let get ~kind protection (s,w) = let (rw, w) = match protection with | Queries.Protection.Strong -> s | Weak -> w in - if write then w else rw + match kind with + | Queries.ProtectionKind.Write -> w + | ReadWrite -> rw end (** Collects information about which variables are protected by which mutexes *) module GProtecting: sig include Lattice.S - val make: write:bool -> recovered:bool -> MustLockset.t -> t - val get: write:bool -> Queries.Protection.t -> t -> MustLockset.t + val make: kind:Queries.ProtectionKind.t -> recovered:bool -> MustLockset.t -> t + val get: kind:Queries.ProtectionKind.t -> Queries.Protection.t -> t -> MustLockset.t end = struct include MakeP (MustLockset) - let make ~write ~recovered locks = + let make ~kind ~recovered locks = (* If the access is not a write, set to T so intersection with current write-protecting is identity *) - let wlocks = if write then locks else MustLockset.all () in + let wlocks = + match kind with + | Queries.ProtectionKind.Write -> locks + | ReadWrite -> MustLockset.all () + in if recovered then (* If we are in single-threaded mode again, this does not need to be added to set of mutexes protecting in mt-mode only *) ((locks, wlocks), (MustLockset.all (), MustLockset.all ())) @@ -90,17 +96,16 @@ struct (** Collects information about which mutex protects which variable *) module GProtected: sig include Lattice.S - val make: write:bool -> VarSet.t -> t - val get: write:bool -> Queries.Protection.t -> t -> VarSet.t + val make: kind:Queries.ProtectionKind.t -> VarSet.t -> t + val get: kind:Queries.ProtectionKind.t -> Queries.Protection.t -> t -> VarSet.t end = struct include MakeP (VarSet) - let make ~write vs = + let make ~kind vs = let vs_empty = VarSet.empty () in - if write then - ((vs_empty, vs), (vs_empty, vs)) - else - ((vs, vs_empty), (vs, vs_empty)) + match kind with + | Queries.ProtectionKind.Write -> ((vs_empty, vs), (vs_empty, vs)) + | ReadWrite -> ((vs, vs_empty), (vs, vs_empty)) end module G = @@ -196,28 +201,28 @@ struct let query (ctx: (D.t, _, _, V.t) ctx) (type a) (q: a Queries.t): a Queries.result = let ls, m = ctx.local in (* get the set of mutexes protecting the variable v in the given mode *) - let protecting ~write mode v = GProtecting.get ~write mode (G.protecting (ctx.global (V.protecting v))) in + let protecting ~kind mode v = GProtecting.get ~kind mode (G.protecting (ctx.global (V.protecting v))) in match q with | Queries.MayBePublic _ when MustLocksetRW.is_all ls -> false - | Queries.MayBePublic {global=v; write; protection} -> + | Queries.MayBePublic {global=v; kind; protection} -> let held_locks = MustLocksetRW.to_must_lockset (MustLocksetRW.filter snd ls) in - let protecting = protecting ~write protection v in + let protecting = protecting ~kind protection v in (* TODO: unsound in 29/24, why did we do this before? *) (* if Mutexes.mem verifier_atomic (Lockset.export_locks ctx.local) then false else *) MustLockset.disjoint held_locks protecting | Queries.MayBePublicWithout _ when MustLocksetRW.is_all ls -> false - | Queries.MayBePublicWithout {global=v; write; without_mutex; protection} -> + | Queries.MayBePublicWithout {global=v; kind; without_mutex; protection} -> let held_locks = MustLockset.remove without_mutex (MustLocksetRW.to_must_lockset ls) in - let protecting = protecting ~write protection v in + let protecting = protecting ~kind protection v in (* TODO: unsound in 29/24, why did we do this before? *) (* if Mutexes.mem verifier_atomic (Lockset.export_locks (Lockset.remove (without_mutex, true) ctx.local)) then false else *) MustLockset.disjoint held_locks protecting - | Queries.MustBeProtectedBy {mutex = ml; global=v; write; protection} -> - let protecting = protecting ~write protection v in + | Queries.MustBeProtectedBy {mutex = ml; global=v; kind; protection} -> + let protecting = protecting ~kind protection v in (* TODO: unsound in 29/24, why did we do this before? *) (* if LockDomain.Addr.equal mutex (LockDomain.Addr.of_var LF.verifier_atomic_var) then true @@ -229,8 +234,8 @@ struct | Queries.MustBeAtomic -> let held_locks = MustLocksetRW.to_must_lockset (MustLocksetRW.filter snd ls) in MustLockset.mem (LF.verifier_atomic_var, `NoOffset) held_locks (* TODO: Mval.of_var *) - | Queries.MustProtectedVars {mutex; write} -> - let protected = GProtected.get ~write Strong (G.protected (ctx.global (V.protected mutex))) in + | Queries.MustProtectedVars {mutex; kind} -> + let protected = GProtected.get ~kind Strong (G.protected (ctx.global (V.protected mutex))) in VarSet.fold (fun v acc -> Queries.VS.add v acc ) protected (Queries.VS.empty ()) @@ -241,13 +246,13 @@ struct begin match g with | `Left g' -> (* protecting *) if GobConfig.get_bool "dbg.print_protection" then ( - let protecting = GProtecting.get ~write:false Strong (G.protecting (ctx.global g)) in (* readwrite protecting *) + let protecting = GProtecting.get ~kind:ReadWrite Strong (G.protecting (ctx.global g)) in (* readwrite protecting *) let s = MustLockset.cardinal protecting in M.info_noloc ~category:Race "Variable %a read-write protected by %d mutex(es): %a" CilType.Varinfo.pretty g' s MustLockset.pretty protecting ) | `Right m -> (* protected *) if GobConfig.get_bool "dbg.print_protection" then ( - let protected = GProtected.get ~write:false Strong (G.protected (ctx.global g)) in (* readwrite protected *) + let protected = GProtected.get ~kind:ReadWrite Strong (G.protected (ctx.global g)) in (* readwrite protected *) let s = VarSet.cardinal protected in max_protected := max !max_protected s; sum_protected := !sum_protected + s; @@ -289,21 +294,21 @@ struct | Some v -> if not (MustLocksetRW.is_all (fst octx.local)) then let locks = MustLocksetRW.to_must_lockset (MustLocksetRW.filter snd (fst octx.local)) in - let write = match kind with - | Write | Free -> true - | Read -> false + let kind = match kind with + | Write | Free -> Queries.ProtectionKind.Write + | Read -> ReadWrite | Call - | Spawn -> false (* TODO: nonsense? *) + | Spawn -> ReadWrite (* TODO: nonsense? *) in - let s = GProtecting.make ~write ~recovered:is_recovered_to_st locks in + let s = GProtecting.make ~kind ~recovered:is_recovered_to_st locks in ctx.sideg (V.protecting v) (G.create_protecting s); if !AnalysisState.postsolving then ( - let protecting mode = GProtecting.get ~write mode (G.protecting (ctx.global (V.protecting v))) in + let protecting mode = GProtecting.get ~kind mode (G.protecting (ctx.global (V.protecting v))) in let held_strong = protecting Strong in let held_weak = protecting Weak in let vs = VarSet.singleton v in - let protected = G.create_protected @@ GProtected.make ~write vs in + let protected = G.create_protected @@ GProtected.make ~kind vs in MustLockset.iter (fun ml -> ctx.sideg (V.protected ml) protected) held_strong; (* If the mutex set here is top, it is actually not accessed *) if is_recovered_to_st && not @@ MustLockset.is_all held_weak then diff --git a/src/domains/queries.ml b/src/domains/queries.ml index b0ede0cfbf..07d5f4758d 100644 --- a/src/domains/queries.ml +++ b/src/domains/queries.ml @@ -36,6 +36,11 @@ module MustBool = BoolDomain.MustBool module Unit = Lattice.Unit +module ProtectionKind = +struct + type t = ReadWrite | Write [@@deriving ord, hash] +end + (** Different notions of protection for a global variables g by a mutex m m protects g strongly if: - whenever g is accessed after the program went multi-threaded for the first time, m is held @@ -48,10 +53,10 @@ module Protection = struct end (* Helper definitions for deriving complex parts of Any.compare below. *) -type maybepublic = {global: CilType.Varinfo.t; write: bool; protection: Protection.t} [@@deriving ord, hash] -type maybepublicwithout = {global: CilType.Varinfo.t; write: bool; without_mutex: LockDomain.MustLock.t; protection: Protection.t} [@@deriving ord, hash] -type mustbeprotectedby = {mutex: LockDomain.MustLock.t; global: CilType.Varinfo.t; write: bool; protection: Protection.t} [@@deriving ord, hash] -type mustprotectedvars = {mutex: LockDomain.MustLock.t; write: bool} [@@deriving ord, hash] +type maybepublic = {global: CilType.Varinfo.t; kind: ProtectionKind.t; protection: Protection.t} [@@deriving ord, hash] +type maybepublicwithout = {global: CilType.Varinfo.t; kind: ProtectionKind.t; without_mutex: LockDomain.MustLock.t; protection: Protection.t} [@@deriving ord, hash] +type mustbeprotectedby = {mutex: LockDomain.MustLock.t; global: CilType.Varinfo.t; kind: ProtectionKind.t; protection: Protection.t} [@@deriving ord, hash] +type mustprotectedvars = {mutex: LockDomain.MustLock.t; kind: ProtectionKind.t} [@@deriving ord, hash] type access = | Memory of {exp: CilType.Exp.t; var_opt: CilType.Varinfo.t option; kind: AccessKind.t} (** Memory location access (race). *) | Point (** Program point and state access (MHP), independent of memory location. *)