From 783428fc21847ff4b34c069ee11b74bb1f0b9444 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 2 Aug 2024 15:26:00 +0300 Subject: [PATCH 1/8] Add Vojdani eager privatization Recreated from 6c54d0439979fc5101d3d25e1bec86cf9974abde. --- src/analyses/basePriv.ml | 126 +++++++++++++++++++++++++++++++++ src/analyses/commonPriv.ml | 8 +-- src/config/options.schema.json | 4 +- 3 files changed, 132 insertions(+), 6 deletions(-) diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 08413d54b1..e37a001058 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -683,6 +683,131 @@ struct end +(** Vojdani privatization with eager reading. *) +module VojdaniPriv: S = +struct + include NoFinalize + include ConfCheck.RequireMutexActivatedInit + open Protection + + module D = Lattice.Unit + + module Wrapper = NoWrapper (VD) + module G = Wrapper.G + module V = VarinfoV + + let startstate () = () + + let read_global (ask: Queries.ask) getg (st: BaseComponents (D).t) x = + let getg = Wrapper.getg ask getg in + if is_unprotected ask ~write:false x then + VD.join (CPA.find x st.cpa) (getg x) + else + CPA.find x st.cpa + + 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 is_unprotected ask ~write:false x then + sideg x v; + if !earlyglobs then (* earlyglobs workaround for 13/60 *) + sideg x v + ); + {st with cpa = CPA.add x v st.cpa} + + let lock ask getg (st: BaseComponents (D).t) m = + let getg = Wrapper.getg ask getg in + CPA.fold (fun x v (st: BaseComponents (D).t) -> + if is_protected_by ask ~write:false m x && is_unprotected ask ~write:false x then ( (* is_in_Gm *) + {st with cpa = CPA.add x (VD.join (CPA.find x st.cpa) (getg x)) st.cpa} + ) + else + st + ) st.cpa st + + let unlock ask getg sideg (st: BaseComponents (D).t) m = + let sideg = Wrapper.sideg ask sideg in + (* TODO: what about G_m globals in cpa that weren't actually written? *) + CPA.fold (fun x v (st: BaseComponents (D).t) -> + if is_protected_by ask ~write:false m x then ( (* is_in_Gm *) + if is_unprotected_without ask ~write:false x m then (* is_in_V' *) + sideg x v; + st + ) + else + st + ) st.cpa st + + let sync ask getg sideg (st: BaseComponents (D).t) reason = + let branched_sync () = + (* required for branched thread creation *) + let sideg = Wrapper.sideg ask sideg in + CPA.fold (fun x v (st: BaseComponents (D).t) -> + if is_global ask x && is_unprotected ask ~write:false x then ( + sideg x v; + st + ) + else + st + ) st.cpa st + in + match reason with + | `Join when ConfCheck.branched_thread_creation () -> + branched_sync () + | `JoinCall when ConfCheck.branched_thread_creation_at_call ask -> + branched_sync () + | `Join + | `JoinCall + | `Return + | `Normal + | `Init + | `Thread -> + st + + let escape ask getg sideg (st: BaseComponents (D).t) escaped = + let sideg = Wrapper.sideg ask sideg in + let cpa' = CPA.fold (fun x v acc -> + if EscapeDomain.EscapedVars.mem x escaped then ( + sideg x v; + acc + ) + else + acc + ) st.cpa st.cpa + in + {st with cpa = cpa'} + + let enter_multithreaded ask getg sideg (st: BaseComponents (D).t) = + let sideg = Wrapper.sideg ask sideg in + CPA.fold (fun x v (st: BaseComponents (D).t) -> + if is_global ask x then ( + sideg x v; + st + ) + else + st + ) st.cpa st + + let threadenter ask st = st + let threadspawn ask get set st = st + + let thread_join ?(force=false) ask get e st = st + let thread_return ask get set tid st = st + + let iter_sys_vars getg vq vf = + match vq with + | VarQuery.Global g -> + vf g; + | _ -> () + + let invariant_global ask getg g = + let getg = Wrapper.getg ask getg in + ValueDomain.invariant_global getg g + + let invariant_vars ask getg st = protected_vars ask +end + + module type PerGlobalPrivParam = sig (** Whether to also check unprotectedness by reads for extra precision. *) @@ -1909,6 +2034,7 @@ let priv_module: (module S) Lazy.t = let module Priv: S = (val match get_string "ana.base.privatization" with | "none" -> (module NonePriv: S) + | "vojdani" -> (module VojdaniPriv: S) | "mutex-oplus" -> (module PerMutexOplusPriv) | "mutex-meet" -> (module PerMutexMeetPriv) | "mutex-meet-tid" -> (module PerMutexMeetTIDPriv (ThreadDigest)) diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml index 003cdfa96c..5d7f19d46f 100644 --- a/src/analyses/commonPriv.ml +++ b/src/analyses/commonPriv.ml @@ -82,22 +82,22 @@ end module Protection = struct open Q.Protection - let is_unprotected ask ?(protection=Strong) x: bool = + let is_unprotected ask ?(write=true) ?(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; write; protection}) ) let is_unprotected_without ask ?(write=true) ?(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}) - let is_protected_by ask ?(protection=Strong) m x: bool = + let is_protected_by ask ?(write=true) ?(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; write; protection}) let protected_vars (ask: Q.ask): varinfo list = LockDomain.MustLockset.fold (fun ml acc -> diff --git a/src/config/options.schema.json b/src/config/options.schema.json index 0cb1b6ee67..dbb9ff7d2a 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -759,9 +759,9 @@ "privatization": { "title": "ana.base.privatization", "description": - "Which privatization to use? none/mutex-oplus/mutex-meet/mutex-meet-tid/protection/protection-read/mine/mine-nothread/mine-W/mine-W-noinit/lock/lock-tid/write/write-tid/write+lock/write+lock-tid", + "Which privatization to use? none/vojdani/mutex-oplus/mutex-meet/mutex-meet-tid/protection/protection-read/mine/mine-nothread/mine-W/mine-W-noinit/lock/lock-tid/write/write-tid/write+lock/write+lock-tid", "type": "string", - "enum": ["none", "mutex-oplus", "mutex-meet", "protection", "protection-tid", "protection-atomic", "protection-read", "protection-read-tid", "protection-read-atomic", "mine", "mine-nothread", "mine-W", "mine-W-noinit", "lock", "lock-tid", "write", "write-tid", "write+lock", "write+lock-tid", "mutex-meet-tid"], + "enum": ["none", "vojdani", "mutex-oplus", "mutex-meet", "protection", "protection-tid", "protection-atomic", "protection-read", "protection-read-tid", "protection-read-atomic", "mine", "mine-nothread", "mine-W", "mine-W-noinit", "lock", "lock-tid", "write", "write-tid", "write+lock", "write+lock-tid", "mutex-meet-tid"], "default": "protection-read" }, "priv": { From f1942f82084d8f80f680b097fd3c744f1e65bdca Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 2 Aug 2024 15:27:08 +0300 Subject: [PATCH 2/8] Remove NoWrapper from VojdaniPriv --- src/analyses/basePriv.ml | 12 +----------- 1 file changed, 1 insertion(+), 11 deletions(-) diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index e37a001058..4a29b52472 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -691,22 +691,18 @@ struct open Protection module D = Lattice.Unit - - module Wrapper = NoWrapper (VD) - module G = Wrapper.G + module G = VD module V = VarinfoV let startstate () = () let read_global (ask: Queries.ask) getg (st: BaseComponents (D).t) x = - let getg = Wrapper.getg ask getg in if is_unprotected ask ~write:false x then VD.join (CPA.find x st.cpa) (getg x) else CPA.find x st.cpa 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 is_unprotected ask ~write:false x then sideg x v; @@ -716,7 +712,6 @@ struct {st with cpa = CPA.add x v st.cpa} let lock ask getg (st: BaseComponents (D).t) m = - let getg = Wrapper.getg ask getg in CPA.fold (fun x v (st: BaseComponents (D).t) -> if is_protected_by ask ~write:false m x && is_unprotected ask ~write:false x then ( (* is_in_Gm *) {st with cpa = CPA.add x (VD.join (CPA.find x st.cpa) (getg x)) st.cpa} @@ -726,7 +721,6 @@ struct ) st.cpa st let unlock ask getg sideg (st: BaseComponents (D).t) m = - let sideg = Wrapper.sideg ask sideg in (* TODO: what about G_m globals in cpa that weren't actually written? *) CPA.fold (fun x v (st: BaseComponents (D).t) -> if is_protected_by ask ~write:false m x then ( (* is_in_Gm *) @@ -741,7 +735,6 @@ struct let sync ask getg sideg (st: BaseComponents (D).t) reason = let branched_sync () = (* required for branched thread creation *) - let sideg = Wrapper.sideg ask sideg in CPA.fold (fun x v (st: BaseComponents (D).t) -> if is_global ask x && is_unprotected ask ~write:false x then ( sideg x v; @@ -765,7 +758,6 @@ struct st let escape ask getg sideg (st: BaseComponents (D).t) escaped = - let sideg = Wrapper.sideg ask sideg in let cpa' = CPA.fold (fun x v acc -> if EscapeDomain.EscapedVars.mem x escaped then ( sideg x v; @@ -778,7 +770,6 @@ struct {st with cpa = cpa'} let enter_multithreaded ask getg sideg (st: BaseComponents (D).t) = - let sideg = Wrapper.sideg ask sideg in CPA.fold (fun x v (st: BaseComponents (D).t) -> if is_global ask x then ( sideg x v; @@ -801,7 +792,6 @@ struct | _ -> () let invariant_global ask getg g = - let getg = Wrapper.getg ask getg in ValueDomain.invariant_global getg g let invariant_vars ask getg st = protected_vars ask From 97d3992f00ef02dd8d6be03c285c3878d768ad0d Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 2 Aug 2024 15:42:19 +0300 Subject: [PATCH 3/8] Simplify VojdaniPriv --- src/analyses/basePriv.ml | 67 ++++++++++++++++------------------------ 1 file changed, 27 insertions(+), 40 deletions(-) diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 4a29b52472..6248d6c6a6 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -707,42 +707,37 @@ struct if is_unprotected ask ~write:false x then sideg x v; if !earlyglobs then (* earlyglobs workaround for 13/60 *) - sideg x v + sideg x v (* TODO: is this needed for anything? 13/60 doesn't work for other reasons *) ); {st with cpa = CPA.add x v st.cpa} let lock ask getg (st: BaseComponents (D).t) m = - CPA.fold (fun x v (st: BaseComponents (D).t) -> - if is_protected_by ask ~write:false m x && is_unprotected ask ~write:false x then ( (* is_in_Gm *) - {st with cpa = CPA.add x (VD.join (CPA.find x st.cpa) (getg x)) st.cpa} - ) + let cpa' = CPA.mapi (fun x v -> + if is_protected_by ask ~write:false m x && is_unprotected ask ~write:false x then (* is_in_Gm *) + VD.join (CPA.find x st.cpa) (getg x) else - st - ) st.cpa st + v + ) st.cpa + in + {st with cpa = cpa'} let unlock ask getg sideg (st: BaseComponents (D).t) m = - (* TODO: what about G_m globals in cpa that weren't actually written? *) - CPA.fold (fun x v (st: BaseComponents (D).t) -> + CPA.iter (fun x v -> if is_protected_by ask ~write:false m x then ( (* is_in_Gm *) if is_unprotected_without ask ~write:false x m then (* is_in_V' *) - sideg x v; - st + sideg x v ) - else - st - ) st.cpa st + ) st.cpa; + st let sync ask getg sideg (st: BaseComponents (D).t) reason = let branched_sync () = (* required for branched thread creation *) - CPA.fold (fun x v (st: BaseComponents (D).t) -> - if is_global ask x && is_unprotected ask ~write:false x then ( - sideg x v; - st - ) - else - st - ) st.cpa st + CPA.iter (fun x v -> + if is_global ask x && is_unprotected ask ~write:false x then + sideg x v + ) st.cpa; + st in match reason with | `Join when ConfCheck.branched_thread_creation () -> @@ -758,26 +753,18 @@ struct st let escape ask getg sideg (st: BaseComponents (D).t) escaped = - let cpa' = CPA.fold (fun x v acc -> - if EscapeDomain.EscapedVars.mem x escaped then ( - sideg x v; - acc - ) - else - acc - ) st.cpa st.cpa - in - {st with cpa = cpa'} + CPA.iter (fun x v -> + if EscapeDomain.EscapedVars.mem x escaped then + sideg x v + ) st.cpa; + st let enter_multithreaded ask getg sideg (st: BaseComponents (D).t) = - CPA.fold (fun x v (st: BaseComponents (D).t) -> - if is_global ask x then ( - sideg x v; - st - ) - else - st - ) st.cpa st + CPA.iter (fun x v -> + if is_global ask x then + sideg x v + ) st.cpa; + st let threadenter ask st = st let threadspawn ask get set st = st From c5030e18f68a764ab0bf1692d5d42e8dbf057198 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 2 Aug 2024 15:55:24 +0300 Subject: [PATCH 4/8] Add none privatization without sync --- src/analyses/basePriv.ml | 79 ++++++++++++++++++++++++++++++++++ src/config/options.schema.json | 4 +- 2 files changed, 81 insertions(+), 2 deletions(-) diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 6248d6c6a6..63f7751180 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -174,6 +174,84 @@ struct let invariant_vars ask getg st = [] end +module NonePriv2: S = +struct + include NoFinalize + + module G = VD + module V = VarinfoV + module D = Lattice.Unit + + let init () = () + + let startstate () = () + + let lock ask getg st m = st + let unlock ask getg sideg st m = st + + let read_global (ask: Queries.ask) getg (st: BaseComponents (D).t) x = + VD.join (CPA.find x st.cpa) (getg x) + + let write_global ?(invariant=false) (ask: Queries.ask) getg sideg (st: BaseComponents (D).t) x v = + if not invariant then + sideg x v; + {st with cpa = CPA.add x v st.cpa} (* TODO: pointless when invariant *) + + let sync ask getg sideg (st: BaseComponents (D).t) reason = + let branched_sync () = + (* required for branched thread creation *) + CPA.iter (fun x v -> + if is_global ask x then + sideg x v + ) st.cpa; + st + in + match reason with + | `Join when ConfCheck.branched_thread_creation () -> + branched_sync () + | `JoinCall when ConfCheck.branched_thread_creation_at_call ask -> + branched_sync () + | `Join + | `JoinCall + | `Return + | `Normal + | `Init + | `Thread -> + st + + let escape ask getg sideg (st: BaseComponents (D).t) escaped = + CPA.iter (fun x v -> + if EscapeDomain.EscapedVars.mem x escaped then + sideg x v + ) st.cpa; + st + + let enter_multithreaded ask getg sideg (st: BaseComponents (D).t) = + CPA.iter (fun x v -> + if is_global ask x then + sideg x v + ) st.cpa; + st + + let threadenter ask st = st + let threadspawn ask get set st = st + + let thread_join ?(force=false) ask get e st = st + let thread_return ask get set tid st = st + + let iter_sys_vars getg vq vf = + match vq with + | VarQuery.Global g -> + vf g; + | _ -> () + + let invariant_global ask getg g = + ValueDomain.invariant_global getg g + + let invariant_vars ask getg st = [] +end + + module PerMutexPrivBase = struct include NoFinalize @@ -2011,6 +2089,7 @@ let priv_module: (module S) Lazy.t = let module Priv: S = (val match get_string "ana.base.privatization" with | "none" -> (module NonePriv: S) + | "none2" -> (module NonePriv2: S) | "vojdani" -> (module VojdaniPriv: S) | "mutex-oplus" -> (module PerMutexOplusPriv) | "mutex-meet" -> (module PerMutexMeetPriv) diff --git a/src/config/options.schema.json b/src/config/options.schema.json index dbb9ff7d2a..a923bfb8ec 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -759,9 +759,9 @@ "privatization": { "title": "ana.base.privatization", "description": - "Which privatization to use? none/vojdani/mutex-oplus/mutex-meet/mutex-meet-tid/protection/protection-read/mine/mine-nothread/mine-W/mine-W-noinit/lock/lock-tid/write/write-tid/write+lock/write+lock-tid", + "Which privatization to use? none/none2/vojdani/mutex-oplus/mutex-meet/mutex-meet-tid/protection/protection-read/mine/mine-nothread/mine-W/mine-W-noinit/lock/lock-tid/write/write-tid/write+lock/write+lock-tid", "type": "string", - "enum": ["none", "vojdani", "mutex-oplus", "mutex-meet", "protection", "protection-tid", "protection-atomic", "protection-read", "protection-read-tid", "protection-read-atomic", "mine", "mine-nothread", "mine-W", "mine-W-noinit", "lock", "lock-tid", "write", "write-tid", "write+lock", "write+lock-tid", "mutex-meet-tid"], + "enum": ["none", "none2", "vojdani", "mutex-oplus", "mutex-meet", "protection", "protection-tid", "protection-atomic", "protection-read", "protection-read-tid", "protection-read-atomic", "mine", "mine-nothread", "mine-W", "mine-W-noinit", "lock", "lock-tid", "write", "write-tid", "write+lock", "write+lock-tid", "mutex-meet-tid"], "default": "protection-read" }, "priv": { From 7d6b8948c6bee675179a6adb1d7cbc4281752000 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 2 Aug 2024 16:01:23 +0300 Subject: [PATCH 5/8] Add none privatization without sync and local state --- src/analyses/basePriv.ml | 89 ++++++++++++++++++++++++++++++++++ src/config/options.schema.json | 2 +- 2 files changed, 90 insertions(+), 1 deletion(-) diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 63f7751180..8e938925bf 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -251,6 +251,94 @@ struct let invariant_vars ask getg st = [] end +module NonePriv3: S = +struct + include NoFinalize + + module G = VD + module V = VarinfoV + module D = Lattice.Unit + + let init () = () + + let startstate () = () + + let lock ask getg st m = st + let unlock ask getg sideg st m = st + + let read_global (ask: Queries.ask) getg (st: BaseComponents (D).t) x = + getg x + + let write_global ?(invariant=false) (ask: Queries.ask) getg sideg (st: BaseComponents (D).t) x v = + if not invariant then + sideg x v; + st + + let sync ask getg sideg (st: BaseComponents (D).t) reason = + let branched_sync () = + (* required for branched thread creation *) + CPA.fold (fun x v (st: BaseComponents (D).t) -> + if is_global ask x then ( + sideg x v; + {st with cpa = CPA.remove x st.cpa} + ) + else + st + ) st.cpa st + in + match reason with + | `Join when ConfCheck.branched_thread_creation () -> + branched_sync () + | `JoinCall when ConfCheck.branched_thread_creation_at_call ask -> + branched_sync () + | `Join + | `JoinCall + | `Return + | `Normal + | `Init + | `Thread -> + st + + let escape ask getg sideg (st: BaseComponents (D).t) escaped = + let cpa' = CPA.fold (fun x v acc -> + if EscapeDomain.EscapedVars.mem x escaped then ( + sideg x v; + CPA.remove x acc + ) + else + acc + ) st.cpa st.cpa + in + {st with cpa = cpa'} + + let enter_multithreaded ask getg sideg (st: BaseComponents (D).t) = + CPA.fold (fun x v (st: BaseComponents (D).t) -> + if is_global ask x then ( + sideg x v; + {st with cpa = CPA.remove x st.cpa} + ) + else + st + ) st.cpa st + + let threadenter ask st = st + let threadspawn ask get set st = st + + let thread_join ?(force=false) ask get e st = st + let thread_return ask get set tid st = st + + let iter_sys_vars getg vq vf = + match vq with + | VarQuery.Global g -> + vf g; + | _ -> () + + let invariant_global ask getg g = + ValueDomain.invariant_global getg g + + let invariant_vars ask getg st = [] +end + module PerMutexPrivBase = struct @@ -2090,6 +2178,7 @@ let priv_module: (module S) Lazy.t = (val match get_string "ana.base.privatization" with | "none" -> (module NonePriv: S) | "none2" -> (module NonePriv2: S) + | "none3" -> (module NonePriv3: S) | "vojdani" -> (module VojdaniPriv: S) | "mutex-oplus" -> (module PerMutexOplusPriv) | "mutex-meet" -> (module PerMutexMeetPriv) diff --git a/src/config/options.schema.json b/src/config/options.schema.json index a923bfb8ec..c516f516f5 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -761,7 +761,7 @@ "description": "Which privatization to use? none/none2/vojdani/mutex-oplus/mutex-meet/mutex-meet-tid/protection/protection-read/mine/mine-nothread/mine-W/mine-W-noinit/lock/lock-tid/write/write-tid/write+lock/write+lock-tid", "type": "string", - "enum": ["none", "none2", "vojdani", "mutex-oplus", "mutex-meet", "protection", "protection-tid", "protection-atomic", "protection-read", "protection-read-tid", "protection-read-atomic", "mine", "mine-nothread", "mine-W", "mine-W-noinit", "lock", "lock-tid", "write", "write-tid", "write+lock", "write+lock-tid", "mutex-meet-tid"], + "enum": ["none", "none2", "none3", "vojdani", "mutex-oplus", "mutex-meet", "protection", "protection-tid", "protection-atomic", "protection-read", "protection-read-tid", "protection-read-atomic", "mine", "mine-nothread", "mine-W", "mine-W-noinit", "lock", "lock-tid", "write", "write-tid", "write+lock", "write+lock-tid", "mutex-meet-tid"], "default": "protection-read" }, "priv": { From 0c29208b76d9fbd6bf05dc7df17f52f4ab3d8edf Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Mon, 5 Aug 2024 14:43:36 +0300 Subject: [PATCH 6/8] Fix none base privatization unsoundness in 02-base/51-spawn-special --- src/framework/constraints.ml | 12 +++++++++++- 1 file changed, 11 insertions(+), 1 deletion(-) diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index 7df4167acd..8cf4f47005 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -671,8 +671,18 @@ struct ignore (getl (Function fd, c)) | exception Not_found -> (* unknown function *) - M.error ~category:Imprecise ~tags:[Category Unsound] "Created a thread from unknown function %s" f.vname + M.error ~category:Imprecise ~tags:[Category Unsound] "Created a thread from unknown function %s" f.vname; (* actual implementation (e.g. invalidation) is done by threadenter *) + (* must still sync for side effects, e.g. none privatization soundness in 02-base/51-spawn-special *) + let rec sync_ctx = + { ctx with + ask = (fun (type a) (q: a Queries.t) -> S.query sync_ctx q); + local = d; + prev_node = Function dummyFunDec; + } + in + (* TODO: more accurate ctx? *) + ignore (sync sync_ctx) ) ds in (* ... nice, right! *) From 5e7c5c7bd766823e7033f7b245a056ecb226e658 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 25 Oct 2024 15:34:01 +0300 Subject: [PATCH 7/8] Keep only NonePriv3 in BasePriv --- src/analyses/basePriv.ml | 153 +-------------------------------- src/config/options.schema.json | 4 +- 2 files changed, 3 insertions(+), 154 deletions(-) diff --git a/src/analyses/basePriv.ml b/src/analyses/basePriv.ml index 511aebe3e2..9b3dce88e0 100644 --- a/src/analyses/basePriv.ml +++ b/src/analyses/basePriv.ml @@ -101,160 +101,11 @@ module DigestWrapper(Digest: Digest):PrivatizationWrapper = functor (GBase:Latt end) -(* No Privatization *) +(** No Privatization. *) module NonePriv: S = struct include NoFinalize - module G = BaseDomain.VD - module V = VarinfoV - module D = Lattice.Unit - - let init () = () - - let startstate () = () - - let lock ask getg st m = st - let unlock ask getg sideg st m = st - - let escape ask getg sideg st escaped = st - let enter_multithreaded ask getg sideg st = st - let threadenter = old_threadenter - let threadspawn ask getg sideg st = st - - let iter_sys_vars getg vq vf = - match vq with - | VarQuery.Global g -> vf g - | _ -> () - - - let read_global ask getg (st: BaseComponents (D).t) x = - getg x - - let write_global ?(invariant=false) ask getg sideg (st: BaseComponents (D).t) x v = - if invariant then ( - (* Do not impose invariant, will not hold without privatization *) - if M.tracing then M.tracel "set" ~var:x.vname "update_one_addr: BAD! effect = '%B', or else is private! " (not invariant); - st - ) - else ( - (* Here, an effect should be generated, but we add it to the local - * state, waiting for the sync function to publish it. *) - (* Copied from MainFunctor.update_variable *) - if ((get_bool "exp.volatiles_are_top") && (is_always_unknown x)) then - {st with cpa = CPA.add x (VD.top ()) st.cpa} - else - {st with cpa = CPA.add x v st.cpa} - ) - - let sync ask getg sideg (st: BaseComponents (D).t) reason = - (* For each global variable, we create the side effect *) - let side_var (v: varinfo) (value) (st: BaseComponents (D).t) = - if M.tracing then M.traceli "globalize" ~var:v.vname "Tracing for %s" v.vname; - let res = - if is_global ask v then begin - if M.tracing then M.tracec "globalize" "Publishing its value: %a" VD.pretty value; - sideg v value; - {st with cpa = CPA.remove v st.cpa} - end else - st - in - if M.tracing then M.traceu "globalize" "Done!"; - res - in - (* We fold over the local state, and side effect the globals *) - CPA.fold side_var st.cpa st - - let thread_join ?(force=false) ask get e st = st - let thread_return ask get set tid st = st - - let invariant_global ask getg g = - ValueDomain.invariant_global getg g - - let invariant_vars ask getg st = [] -end - -module NonePriv2: S = -struct - include NoFinalize - - module G = VD - module V = VarinfoV - module D = Lattice.Unit - - let init () = () - - let startstate () = () - - let lock ask getg st m = st - let unlock ask getg sideg st m = st - - let read_global (ask: Queries.ask) getg (st: BaseComponents (D).t) x = - VD.join (CPA.find x st.cpa) (getg x) - - let write_global ?(invariant=false) (ask: Queries.ask) getg sideg (st: BaseComponents (D).t) x v = - if not invariant then - sideg x v; - {st with cpa = CPA.add x v st.cpa} (* TODO: pointless when invariant *) - - let sync ask getg sideg (st: BaseComponents (D).t) reason = - let branched_sync () = - (* required for branched thread creation *) - CPA.iter (fun x v -> - if is_global ask x then - sideg x v - ) st.cpa; - st - in - match reason with - | `Join when ConfCheck.branched_thread_creation () -> - branched_sync () - | `JoinCall f when ConfCheck.branched_thread_creation_at_call ask f -> - branched_sync () - | `Join - | `JoinCall _ - | `Return - | `Normal - | `Init - | `Thread -> - st - - let escape ask getg sideg (st: BaseComponents (D).t) escaped = - CPA.iter (fun x v -> - if EscapeDomain.EscapedVars.mem x escaped then - sideg x v - ) st.cpa; - st - - let enter_multithreaded ask getg sideg (st: BaseComponents (D).t) = - CPA.iter (fun x v -> - if is_global ask x then - sideg x v - ) st.cpa; - st - - let threadenter ask st = st - let threadspawn ask get set st = st - - let thread_join ?(force=false) ask get e st = st - let thread_return ask get set tid st = st - - let iter_sys_vars getg vq vf = - match vq with - | VarQuery.Global g -> - vf g; - | _ -> () - - let invariant_global ask getg g = - ValueDomain.invariant_global getg g - - let invariant_vars ask getg st = [] -end - -module NonePriv3: S = -struct - include NoFinalize - module G = VD module V = VarinfoV module D = Lattice.Unit @@ -2177,8 +2028,6 @@ let priv_module: (module S) Lazy.t = let module Priv: S = (val match get_string "ana.base.privatization" with | "none" -> (module NonePriv: S) - | "none2" -> (module NonePriv2: S) - | "none3" -> (module NonePriv3: S) | "vojdani" -> (module VojdaniPriv: S) | "mutex-oplus" -> (module PerMutexOplusPriv) | "mutex-meet" -> (module PerMutexMeetPriv) diff --git a/src/config/options.schema.json b/src/config/options.schema.json index b65de6332b..0a862148eb 100644 --- a/src/config/options.schema.json +++ b/src/config/options.schema.json @@ -759,9 +759,9 @@ "privatization": { "title": "ana.base.privatization", "description": - "Which privatization to use? none/none2/vojdani/mutex-oplus/mutex-meet/mutex-meet-tid/protection/protection-read/mine/mine-nothread/mine-W/mine-W-noinit/lock/lock-tid/write/write-tid/write+lock/write+lock-tid", + "Which privatization to use? none/vojdani/mutex-oplus/mutex-meet/mutex-meet-tid/protection/protection-read/mine/mine-nothread/mine-W/mine-W-noinit/lock/lock-tid/write/write-tid/write+lock/write+lock-tid", "type": "string", - "enum": ["none", "none2", "none3", "vojdani", "mutex-oplus", "mutex-meet", "protection", "protection-tid", "protection-atomic", "protection-read", "protection-read-tid", "protection-read-atomic", "mine", "mine-nothread", "mine-W", "mine-W-noinit", "lock", "lock-tid", "write", "write-tid", "write+lock", "write+lock-tid", "mutex-meet-tid"], + "enum": ["none", "vojdani", "mutex-oplus", "mutex-meet", "protection", "protection-tid", "protection-atomic", "protection-read", "protection-read-tid", "protection-read-atomic", "mine", "mine-nothread", "mine-W", "mine-W-noinit", "lock", "lock-tid", "write", "write-tid", "write+lock", "write+lock-tid", "mutex-meet-tid"], "default": "protection-read" }, "priv": { From 7a595a1393049e8a3c4832647d1324e29f3f4bf9 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 25 Oct 2024 15:42:44 +0300 Subject: [PATCH 8/8] Update comment about unknown function spawn sync --- src/framework/constraints.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml index 6aa451cbe4..04959348e1 100644 --- a/src/framework/constraints.ml +++ b/src/framework/constraints.ml @@ -83,7 +83,7 @@ struct (* unknown function *) M.error ~category:Imprecise ~tags:[Category Unsound] "Created a thread from unknown function %s" f.vname; (* actual implementation (e.g. invalidation) is done by threadenter *) - (* must still sync for side effects, e.g. none privatization soundness in 02-base/51-spawn-special *) + (* must still sync for side effects, e.g. old sync-based none privatization soundness in 02-base/51-spawn-special *) let rec sync_ctx = { ctx with ask = (fun (type a) (q: a Queries.t) -> S.query sync_ctx q);