Skip to content

Commit

Permalink
Keep only NonePriv3 in BasePriv
Browse files Browse the repository at this point in the history
  • Loading branch information
@sim642
sim642 committed Oct 25, 2024
1 parent 814997a commit 5e7c5c7
Show file tree
Hide file tree
Showing 2 changed files with 3 additions and 154 deletions.
153 changes: 1 addition & 152 deletions src/analyses/basePriv.ml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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)
Expand Down
4 changes: 2 additions & 2 deletions src/config/options.schema.json
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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": {
Expand Down

0 comments on commit 5e7c5c7

Please sign in to comment.