Keep only NonePriv3 in BasePriv

Author: sim642

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)

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": {