Optimize none base privatization, add eager Vojdani privatization

src/analyses/basePriv.ml

@@ -174,6 +174,172 @@ 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 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
   include NoFinalize
@@ -683,6 +849,108 @@ struct
 end
 
 
+(** Vojdani privatization with eager reading. *)
+module VojdaniPriv: S =
+struct
+  include NoFinalize
+  include ConfCheck.RequireMutexActivatedInit
+  open Protection
+
+  module D = Lattice.Unit
+  module G = VD
+  module V = VarinfoV
+
+  let startstate () = ()
+
+  let read_global (ask: Queries.ask) getg (st: BaseComponents (D).t) x =
+    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 =
+    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 (* 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 =
+    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
+          v
+      ) st.cpa
+    in
+    {st with cpa = cpa'}
+
+  let unlock ask getg sideg (st: BaseComponents (D).t) m =
+    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.cpa;
+    st
+
+  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 && is_unprotected ask ~write:false 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 = protected_vars ask
+end
+
+
 module type PerGlobalPrivParam =
 sig
   (** Whether to also check unprotectedness by reads for extra precision. *)
@@ -1909,6 +2177,9 @@ 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)
         | "mutex-meet-tid" -> (module PerMutexMeetTIDPriv (ThreadDigest))

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 ->

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

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! *)