Skip to content

Commit 569489e

Browse files
michael-schwarzmichael-schwarz
committed
Back to master
1 parent 35b3972 commit 569489e

File tree

1 file changed

+30
-74
lines changed

1 file changed

+30
-74
lines changed

‎src/analyses/basePriv.ml‎

Lines changed: 30 additions & 74 deletions
Original file line numberDiff line numberDiff line change
@@ -866,47 +866,6 @@ sig
866866
include AtomicParam
867867
end
868868

869-
module P =
870-
struct
871-
include MustVars
872-
let name () = "P"
873-
end
874-
875-
module Sigma' =
876-
struct
877-
include CPA
878-
let name () = "Protected Changes"
879-
end
880-
881-
module type ProtectionDom =
882-
sig
883-
include Lattice.S
884-
val add: bool -> varinfo -> VD.t -> t -> t
885-
val remove: varinfo -> t -> t
886-
val precise_side: varinfo -> VD.t -> t -> VD.t option
887-
val empty: unit -> t
888-
val getP: t -> P.t
889-
end
890-
891-
module ProtectionCPASide: ProtectionDom =
892-
struct
893-
include P
894-
895-
let add _ x _ t = P.add x t
896-
let precise_side x v t = Some v
897-
let getP t = t
898-
end
899-
900-
module ProtectionChangesOnlySide: ProtectionDom =
901-
struct
902-
include Lattice.Prod (P) (Sigma')
903-
let add invariant x v t = P.add x @@ fst t, if not invariant then Sigma'.add x v @@ snd t else snd t
904-
let remove x t = P.remove x @@ fst t, Sigma'.remove x @@ snd t
905-
let precise_side x v t = Sigma'.find_opt x @@ snd t
906-
let empty () = P.empty (), Sigma'.empty ()
907-
let getP t = fst t
908-
end
909-
910869
(** Protection-Based Reading. *)
911870
module ProtectionBasedV = struct
912871
module VUnprot =
@@ -928,24 +887,30 @@ module ProtectionBasedV = struct
928887
end
929888

930889
(** Protection-Based Reading. *)
931-
module ProtectionBasedPriv (D: ProtectionDom) (Param: PerGlobalPrivParam)(Wrapper:PrivatizationWrapper): S =
890+
module ProtectionBasedPriv (Param: PerGlobalPrivParam)(Wrapper:PrivatizationWrapper): S =
932891
struct
933892
include NoFinalize
934893
include ConfCheck.RequireMutexActivatedInit
935894
open Protection
936895

896+
module P =
897+
struct
898+
include MustVars
899+
let name () = "P"
900+
end
901+
937902
(* W is implicitly represented by CPA domain *)
938-
module D = D
903+
module D = P
939904

940905
module Wrapper = Wrapper (VD)
941906
module G = Wrapper.G
942907
module V = ProtectionBasedV.V
943908

944-
let startstate () = D.empty ()
909+
let startstate () = P.empty ()
945910

946911
let read_global (ask: Queries.ask) getg (st: BaseComponents (D).t) x =
947912
let getg = Wrapper.getg ask getg in
948-
if P.mem x @@ D.getP st.priv then
913+
if P.mem x st.priv then
949914
CPA.find x st.cpa
950915
else if Param.handle_atomic && ask.f MustBeAtomic then
951916
VD.join (CPA.find x st.cpa) (getg (V.unprotected x)) (* Account for previous unpublished unprotected writes in current atomic section. *)
@@ -956,7 +921,6 @@ struct
956921

957922
let write_global ?(invariant=false) (ask: Queries.ask) getg sideg (st: BaseComponents (D).t) x v =
958923
let sideg = Wrapper.sideg ask sideg in
959-
let unprotected = is_unprotected ask x in
960924
if not invariant then (
961925
if not (Param.handle_atomic && ask.f MustBeAtomic) then
962926
sideg (V.unprotected x) v; (* Delay publishing unprotected write in the atomic section. *)
@@ -965,11 +929,11 @@ struct
965929
(* Unlock after invariant will still side effect refined value (if protected) from CPA, because cannot distinguish from non-invariant write since W is implicit. *)
966930
);
967931
if Param.handle_atomic && ask.f MustBeAtomic then
968-
{st with cpa = CPA.add x v st.cpa; priv = D.add invariant x v st.priv} (* Keep write local as if it were protected by the atomic section. *)
969-
else if unprotected then
932+
{st with cpa = CPA.add x v st.cpa; priv = P.add x st.priv} (* Keep write local as if it were protected by the atomic section. *)
933+
else if is_unprotected ask x then
970934
st
971935
else
972-
{st with cpa = CPA.add x v st.cpa; priv = D.add invariant x v st.priv}
936+
{st with cpa = CPA.add x v st.cpa; priv = P.add x st.priv}
973937

974938
let lock ask getg st m = st
975939

@@ -979,22 +943,16 @@ struct
979943
(* TODO: what about G_m globals in cpa that weren't actually written? *)
980944
CPA.fold (fun x v (st: BaseComponents (D).t) ->
981945
if is_protected_by ask m x then ( (* is_in_Gm *)
982-
(* Only apply sides for values that were actually written to globals!
983-
This excludes invariants inferred through guards. *)
984-
begin match D.precise_side x v st.priv with
985-
| Some v -> begin
986-
(* Extra precision in implementation to pass tests:
987-
If global is read-protected by multiple locks,
988-
then inner unlock shouldn't yet publish. *)
989-
if not Param.check_read_unprotected || is_unprotected_without ask ~write:false x m then
990-
sideg (V.protected x) v;
991-
if atomic then
992-
sideg (V.unprotected x) v; (* Publish delayed unprotected write as if it were protected by the atomic section. *)
993-
end
994-
| None -> ()
995-
end;
946+
(* Extra precision in implementation to pass tests:
947+
If global is read-protected by multiple locks,
948+
then inner unlock shouldn't yet publish. *)
949+
if not Param.check_read_unprotected || is_unprotected_without ask ~write:false x m then
950+
sideg (V.protected x) v;
951+
if atomic then
952+
sideg (V.unprotected x) v; (* Publish delayed unprotected write as if it were protected by the atomic section. *)
953+
996954
if is_unprotected_without ask x m then (* is_in_V' *)
997-
{st with cpa = CPA.remove x st.cpa; priv = D.remove x st.priv}
955+
{st with cpa = CPA.remove x st.cpa; priv = P.remove x st.priv}
998956
else
999957
st
1000958
)
@@ -1010,7 +968,7 @@ struct
1010968
if is_global ask x && is_unprotected ask x then (
1011969
sideg (V.unprotected x) v;
1012970
sideg (V.protected x) v; (* must be like enter_multithreaded *)
1013-
{st with cpa = CPA.remove x st.cpa; priv = D.remove x st.priv}
971+
{st with cpa = CPA.remove x st.cpa; priv = P.remove x st.priv}
1014972
)
1015973
else
1016974
st
@@ -1049,7 +1007,7 @@ struct
10491007
if is_global ask x then (
10501008
sideg (V.unprotected x) v;
10511009
sideg (V.protected x) v;
1052-
{st with cpa = CPA.remove x st.cpa; priv = D.remove x st.priv}
1010+
{st with cpa = CPA.remove x st.cpa; priv = P.remove x st.priv}
10531011
)
10541012
else
10551013
st
@@ -2158,21 +2116,19 @@ end
21582116

21592117
let priv_module: (module S) Lazy.t =
21602118
lazy (
2161-
let changes_only = get_bool "ana.base.priv.protection.changes-only" in
2162-
let module ProtDom: ProtectionDom = (val if changes_only then (module ProtectionChangesOnlySide : ProtectionDom) else (module ProtectionCPASide)) in
21632119
let module Priv: S =
21642120
(val match get_string "ana.base.privatization" with
21652121
| "none" -> (module NonePriv: S)
21662122
| "vojdani" -> (module VojdaniPriv: S)
21672123
| "mutex-oplus" -> (module PerMutexOplusPriv)
21682124
| "mutex-meet" -> (module PerMutexMeetPriv)
21692125
| "mutex-meet-tid" -> (module PerMutexMeetTIDPriv (ThreadDigest))
2170-
| "protection" -> (module ProtectionBasedPriv (ProtDom) (struct let check_read_unprotected = false let handle_atomic = false end)(NoWrapper))
2171-
| "protection-tid" -> (module ProtectionBasedPriv (ProtDom) (struct let check_read_unprotected = false let handle_atomic = false end)(DigestWrapper(ThreadNotStartedDigest)))
2172-
| "protection-atomic" -> (module ProtectionBasedPriv (ProtDom) (struct let check_read_unprotected = false let handle_atomic = true end)(NoWrapper)) (* experimental *)
2173-
| "protection-read" -> (module ProtectionBasedPriv (ProtDom) (struct let check_read_unprotected = true let handle_atomic = false end)(NoWrapper))
2174-
| "protection-read-tid" -> (module ProtectionBasedPriv (ProtDom) (struct let check_read_unprotected = true let handle_atomic = false end)(DigestWrapper(ThreadNotStartedDigest)))
2175-
| "protection-read-atomic" -> (module ProtectionBasedPriv (ProtDom) (struct let check_read_unprotected = true let handle_atomic = true end)(NoWrapper)) (* experimental *)
2126+
| "protection" -> (module ProtectionBasedPriv (struct let check_read_unprotected = false let handle_atomic = false end)(NoWrapper))
2127+
| "protection-tid" -> (module ProtectionBasedPriv (struct let check_read_unprotected = false let handle_atomic = false end)(DigestWrapper(ThreadNotStartedDigest)))
2128+
| "protection-atomic" -> (module ProtectionBasedPriv (struct let check_read_unprotected = false let handle_atomic = true end)(NoWrapper)) (* experimental *)
2129+
| "protection-read" -> (module ProtectionBasedPriv (struct let check_read_unprotected = true let handle_atomic = false end)(NoWrapper))
2130+
| "protection-read-tid" -> (module ProtectionBasedPriv (struct let check_read_unprotected = true let handle_atomic = false end)(DigestWrapper(ThreadNotStartedDigest)))
2131+
| "protection-read-atomic" -> (module ProtectionBasedPriv (struct let check_read_unprotected = true let handle_atomic = true end)(NoWrapper)) (* experimental *)
21762132
| "mine" -> (module MinePriv)
21772133
| "mine-nothread" -> (module MineNoThreadPriv)
21782134
| "mine-W" -> (module MineWPriv (struct let side_effect_global_init = true end))

0 commit comments

Comments
 (0)