diff --git a/src/analyses/apron/relationPriv.apron.ml b/src/analyses/apron/relationPriv.apron.ml index 41af766c99..13c8efed10 100644 --- a/src/analyses/apron/relationPriv.apron.ml +++ b/src/analyses/apron/relationPriv.apron.ml @@ -853,8 +853,9 @@ struct module NC = Cluster(RD) module Cluster = NC module LRD = NC.LRD + module DigestD = DigestD (Digest) (LRD) - include PerMutexTidCommon (Digest) (LRD) + include PerMutexTidCommon (DigestD) (LRD) module AV = RD.V module P = UnitP @@ -937,8 +938,7 @@ struct (* unlock *) let rel_side = RD.keep_vars rel_local [g_var] in let rel_side = Cluster.unlock (W.singleton g) rel_side in - let digest = Digest.current ask in - let sidev = GMutex.singleton digest rel_side in + let sidev = DigestD.make ask rel_side in sideg (V.global g) (G.create_global sidev); let l' = L.add lm rel_side l in let rel_local' = @@ -975,8 +975,7 @@ struct else let rel_side = keep_only_protected_globals ask m rel in let rel_side = Cluster.unlock w rel_side in - let digest = Digest.current ask in - let sidev = GMutex.singleton digest rel_side in + let sidev = DigestD.make ask rel_side in sideg (V.mutex m) (G.create_mutex sidev); let lm = LLock.mutex m in let l' = L.add lm rel_side l in @@ -1060,8 +1059,7 @@ struct in let rel_side = RD.keep_vars rel g_vars in let rel_side = Cluster.unlock (W.top ()) rel_side in (* top W to avoid any filtering *) - let digest = Digest.current ask in - let sidev = GMutex.singleton digest rel_side in + let sidev = DigestD.make ask rel_side in sideg V.mutex_inits (G.create_mutex sidev); (* Introduction into local state not needed, will be read via initializer *) (* Also no side-effect to mutex globals needed, the value here will either by read via the initializer, *) diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 88e9c985cf..4d6b0aa8d2 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -395,7 +395,8 @@ module PerMutexMeetTIDPriv (Digest: Digest): S = struct open Queries.Protection include PerMutexMeetPrivBase - include PerMutexTidCommon (Digest) (CPA) + module DigestD = DigestD (Digest) (CPA) + include PerMutexTidCommon (DigestD) (CPA) let iter_sys_vars getg vq vf = match vq with @@ -465,8 +466,7 @@ struct CPA.add x v st.cpa in if M.tracing then M.tracel "priv" "WRITE GLOBAL SIDE %a = %a\n" CilType.Varinfo.pretty x VD.pretty v; - let digest = Digest.current ask in - let sidev = GMutex.singleton digest (CPA.singleton x v) in + let sidev = DigestD.make ask (CPA.singleton x v) in let l' = L.add lm (CPA.singleton x v) l in let is_recovered_st = ask.f (Queries.MustBeSingleThreaded {since_start = false}) && not @@ ask.f (Queries.MustBeSingleThreaded {since_start = true}) in let l' = if is_recovered_st then @@ -508,8 +508,7 @@ struct {st with cpa = cpa'; priv = (w',lmust,l)} else let is_in_Gm x _ = is_protected_by ~protection:Weak ask m x in - let digest = Digest.current ask in - let sidev = GMutex.singleton digest (CPA.filter is_in_Gm st.cpa) in + let sidev = DigestD.make ask (CPA.filter is_in_Gm st.cpa) in sideg (V.mutex m) (G.create_mutex sidev); let lm = LLock.mutex m in let l' = L.add lm (CPA.filter is_in_Gm st.cpa) l in @@ -559,13 +558,12 @@ struct let escape ask getg sideg (st: BaseComponents (D).t) escaped = let escaped_cpa = CPA.filter (fun x _ -> EscapeDomain.EscapedVars.mem x escaped) st.cpa in - let digest = Digest.current ask in - let sidev = GMutex.singleton digest escaped_cpa in + let sidev = DigestD.make ask escaped_cpa in sideg V.mutex_inits (G.create_mutex sidev); let cpa' = CPA.fold (fun x v acc -> if EscapeDomain.EscapedVars.mem x escaped (* && is_unprotected ask x *) then ( if M.tracing then M.tracel "priv" "ESCAPE SIDE %a = %a\n" CilType.Varinfo.pretty x VD.pretty v; - let sidev = GMutex.singleton digest (CPA.singleton x v) in + let sidev = DigestD.make ask (CPA.singleton x v) in sideg (V.global x) (G.create_global sidev); CPA.remove x acc ) @@ -578,8 +576,7 @@ struct let enter_multithreaded ask getg sideg (st: BaseComponents (D).t) = let cpa = st.cpa in let cpa_side = CPA.filter (fun x _ -> is_global ask x) cpa in - let digest = Digest.current ask in - let sidev = GMutex.singleton digest cpa_side in + let sidev = DigestD.make ask cpa_side in sideg V.mutex_inits (G.create_mutex sidev); (* Introduction into local state not needed, will be read via initializer *) (* Also no side-effect to mutex globals needed, the value here will either by read via the initializer, *) diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml index 0d4962d18b..08af204fd0 100644 --- a/src/analyses/commonPriv.ml +++ b/src/analyses/commonPriv.ml @@ -185,7 +185,19 @@ struct | _ -> false end -module DigestD (Digest: Digest) (LD: Lattice.S) = +module type DigestD = +sig + include Lattice.S + type value + + val get_relevant_writes_nofilter: Q.ask -> t -> value + val merge_all: t -> value + val make: Q.ask -> value -> t + + val map: (value -> value) -> t -> t +end + +module DigestD (Digest: Digest) (LD: Lattice.S): DigestD with type value = LD.t = struct include MapDomain.MapBot_LiftTop (Digest) (LD) @@ -200,12 +212,13 @@ struct let merge_all v = fold (fun _ v acc -> LD.join acc v) v (LD.bot ()) + + let make ask v = + singleton (Digest.current ask) v end -module PerMutexTidCommon (Digest: Digest) (LD: Lattice.S) = +module PerMutexTidCommon (DigestD: DigestD) (LD: Lattice.S) = struct - module DigestD = DigestD (Digest) (LD) - include ConfCheck.RequireThreadFlagPathSensInit module TID = ThreadIdDomain.Thread