Merge pull request #1398 from goblint/protection-tid

Ego-Lane-Derived-Digests for Privatizations: `ProtectionBasedTIDPriv`

src/analyses/base.ml

@@ -1243,7 +1243,7 @@ struct
       (* TODO: account for single-threaded values without earlyglobs. *)
       match g with
       | `Left g' -> (* priv *)
-        Priv.invariant_global (priv_getg ctx.global) g'
+        Priv.invariant_global (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) g'
       | `Right _ -> (* thread return *)
         Invariant.none
     )

src/analyses/basePriv.ml

@@ -42,7 +42,7 @@ sig
   val thread_join: ?force:bool -> Q.ask -> (V.t -> G.t) -> Cil.exp -> BaseComponents (D).t -> BaseComponents (D).t
   val thread_return: Q.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> ThreadIdDomain.Thread.t -> BaseComponents (D).t -> BaseComponents (D).t
 
-  val invariant_global: (V.t -> G.t) -> V.t -> Invariant.t
+  val invariant_global: Q.ask -> (V.t -> G.t) -> V.t -> Invariant.t
   val invariant_vars: Q.ask -> (V.t -> G.t) -> BaseComponents (D).t -> varinfo list
 
   val init: unit -> unit
@@ -131,7 +131,7 @@ struct
   let thread_join ?(force=false) ask get e st = st
   let thread_return ask get set tid st = st
 
-  let invariant_global getg g =
+  let invariant_global ask getg g =
     ValueDomain.invariant_global getg g
 
   let invariant_vars ask getg st = []
@@ -211,7 +211,7 @@ struct
   let thread_join ?(force=false) ask get e st = st
   let thread_return ask get set tid st = st
 
-  let invariant_global getg = function
+  let invariant_global ask getg = function
     | `Right g' -> (* global *)
       ValueDomain.invariant_global (read_unprotected_global getg) g'
     | _ -> (* mutex *)
@@ -621,7 +621,7 @@ struct
     let get_mutex_inits' = CPA.find x get_mutex_inits in
     VD.join get_mutex_global_x' get_mutex_inits'
 
-  let invariant_global getg = function
+  let invariant_global ask getg = function
     | `Middle  g -> (* global *)
       ValueDomain.invariant_global (read_unprotected_global getg) g
     | `Left _
@@ -639,21 +639,7 @@ sig
 end
 
 (** Protection-Based Reading. *)
-module ProtectionBasedPriv (Param: PerGlobalPrivParam): S =
-struct
-  include NoFinalize
-  include ConfCheck.RequireMutexActivatedInit
-  open Protection
-
-  module P =
-  struct
-    include MustVars
-    let name () = "P"
-  end
-  (* W is implicitly represented by CPA domain *)
-  module D = P
-
-  module G = VD
+module ProtectionBasedV = struct
   module VUnprot =
   struct
     include VarinfoV (* [g]' *)
@@ -670,10 +656,64 @@ struct
     let unprotected x = `Left x
     let protected x = `Right x
   end
+end
+
+(** Protection-Based Reading. *)
+module type ProtectionBasedWrapper =
+sig
+  module G: Lattice.S
+
+  val getg: Q.ask -> (ProtectionBasedV.V.t -> G.t) -> ProtectionBasedV.V.t -> VD.t
+  val sideg: Q.ask -> (ProtectionBasedV.V.t -> G.t -> unit) -> ProtectionBasedV.V.t -> VD.t -> unit
+end
+
+
+module NoWrapper: ProtectionBasedWrapper =
+struct
+  module G = VD
+
+  let getg _ getg = getg
+  let sideg _ sideg = sideg
+end
+
+module DigestWrapper(Digest: Digest): ProtectionBasedWrapper = struct
+  module G = MapDomain.MapBot_LiftTop (Digest) (VD)
+
+  let getg ask getg x =
+    let vs = getg x in
+    G.fold (fun d v acc ->
+        if not (Digest.accounted_for ask ~current:(Digest.current ask) ~other:d) then
+          VD.join v acc
+        else
+          acc) vs (VD.bot ())
+
+  let sideg ask sideg x v =
+    let sidev = G.singleton (Digest.current ask) v in
+    sideg x sidev
+end
+
+module ProtectionBasedPrivWrapper (Param: PerGlobalPrivParam)(Wrapper:ProtectionBasedWrapper): S =
+struct
+  include NoFinalize
+  include ConfCheck.RequireMutexActivatedInit
+  open Protection
+
+  module P =
+  struct
+    include MustVars
+    let name () = "P"
+  end
+
+  (* W is implicitly represented by CPA domain *)
+  module D = P
+
+  module G = Wrapper.G
+  module V = ProtectionBasedV.V
 
   let startstate () = P.empty ()
 
   let read_global (ask: Queries.ask) getg (st: BaseComponents (D).t) x =
+    let getg = Wrapper.getg ask getg in
     if P.mem x st.priv then
       CPA.find x st.cpa
     else if Param.handle_atomic && ask.f MustBeAtomic then
@@ -684,6 +724,7 @@ struct
       VD.join (CPA.find x st.cpa) (getg (V.protected x))
 
   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 not (Param.handle_atomic && ask.f MustBeAtomic) then
         sideg (V.unprotected x) v; (* Delay publishing unprotected write in the atomic section. *)
@@ -701,6 +742,7 @@ struct
   let lock ask getg st m = st
 
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
+    let sideg = Wrapper.sideg ask sideg in
     let atomic = Param.handle_atomic && LockDomain.Addr.equal m (LockDomain.Addr.of_var LibraryFunctions.verifier_atomic_var) in
     (* TODO: what about G_m globals in cpa that weren't actually written? *)
     CPA.fold (fun x v (st: BaseComponents (D).t) ->
@@ -723,6 +765,7 @@ struct
       ) st.cpa st
 
   let sync ask getg sideg (st: BaseComponents (D).t) reason =
+    let sideg = Wrapper.sideg ask sideg in
     match reason with
     | `Join -> (* required for branched thread creation *)
       CPA.fold (fun x v (st: BaseComponents (D).t) ->
@@ -741,6 +784,7 @@ 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 (V.unprotected x) v;
@@ -754,6 +798,7 @@ 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 (V.unprotected x) v;
@@ -777,7 +822,8 @@ struct
       vf (V.protected g);
     | _ -> ()
 
-  let invariant_global getg g =
+  let invariant_global ask getg g =
+    let getg = Wrapper.getg ask getg in
     match g with
     | `Left g' -> (* unprotected *)
       ValueDomain.invariant_global (fun g -> getg (V.unprotected g)) g'
@@ -841,7 +887,7 @@ struct
 
   open Locksets
 
-  let invariant_global getg = function
+  let invariant_global ask getg = function
     | `Right g' -> (* global *)
       ValueDomain.invariant_global (fun x ->
           GWeak.fold (fun s' tm acc ->
@@ -1633,7 +1679,7 @@ struct
   let threadenter ask st = time "threadenter" (Priv.threadenter ask) st
   let threadspawn ask get set st = time "threadspawn" (Priv.threadspawn ask get set) st
   let iter_sys_vars getg vq vf = time "iter_sys_vars" (Priv.iter_sys_vars getg vq) vf
-  let invariant_global getg v = time "invariant_global" (Priv.invariant_global getg) v
+  let invariant_global ask getg v = time "invariant_global" (Priv.invariant_global ask getg) v
   let invariant_vars ask getg st = time "invariant_vars" (Priv.invariant_vars ask getg) st
 
   let thread_join ?(force=false) ask get e st = time "thread_join" (Priv.thread_join ~force ask get e) st
@@ -1789,10 +1835,12 @@ let priv_module: (module S) Lazy.t =
         | "mutex-oplus" -> (module PerMutexOplusPriv)
         | "mutex-meet" -> (module PerMutexMeetPriv)
         | "mutex-meet-tid" -> (module PerMutexMeetTIDPriv (ThreadDigest))
-        | "protection" -> (module ProtectionBasedPriv (struct let check_read_unprotected = false let handle_atomic = false end))
-        | "protection-atomic" -> (module ProtectionBasedPriv (struct let check_read_unprotected = false let handle_atomic = true end)) (* experimental *)
-        | "protection-read" -> (module ProtectionBasedPriv (struct let check_read_unprotected = true let handle_atomic = false end))
-        | "protection-read-atomic" -> (module ProtectionBasedPriv (struct let check_read_unprotected = true let handle_atomic = true end)) (* experimental *)
+        | "protection" -> (module ProtectionBasedPrivWrapper (struct let check_read_unprotected = false let handle_atomic = false end)(NoWrapper))
+        | "protection-tid" -> (module ProtectionBasedPrivWrapper (struct let check_read_unprotected = false let handle_atomic = false end)(DigestWrapper(ThreadNotStartedDigest)))
+        | "protection-atomic" -> (module ProtectionBasedPrivWrapper (struct let check_read_unprotected = false let handle_atomic = true end)(NoWrapper)) (* experimental *)
+        | "protection-read" -> (module ProtectionBasedPrivWrapper (struct let check_read_unprotected = true let handle_atomic = false end)(NoWrapper))
+        | "protection-read-tid" -> (module ProtectionBasedPrivWrapper (struct let check_read_unprotected = true let handle_atomic = false end)(DigestWrapper(ThreadNotStartedDigest)))
+        | "protection-read-atomic" -> (module ProtectionBasedPrivWrapper (struct let check_read_unprotected = true let handle_atomic = true end)(NoWrapper)) (* experimental *)
         | "mine" -> (module MinePriv)
         | "mine-nothread" -> (module MineNoThreadPriv)
         | "mine-W" -> (module MineWPriv (struct let side_effect_global_init = true end))

src/analyses/basePriv.mli

@@ -31,7 +31,7 @@ sig
   val thread_join: ?force:bool -> Queries.ask -> (V.t -> G.t) -> Cil.exp -> BaseDomain.BaseComponents (D).t -> BaseDomain.BaseComponents (D).t
   val thread_return: Queries.ask -> (V.t -> G.t) -> (V.t -> G.t -> unit) -> ThreadIdDomain.Thread.t -> BaseDomain.BaseComponents (D).t -> BaseDomain.BaseComponents (D).t
 
-  val invariant_global: (V.t -> G.t) -> V.t -> Invariant.t
+  val invariant_global: Queries.ask -> (V.t -> G.t) -> V.t -> Invariant.t
   (** Provides [Queries.InvariantGlobal] result for base.
 
       Should account for all unprotected/weak values of global variables. *)

src/analyses/commonPriv.ml

@@ -174,6 +174,9 @@ sig
   val accounted_for: Q.ask -> current:t -> other:t -> bool
 end
 
+(** Digest to be used for analyses that account for all join-local contributions in some locally tracked datastructure, akin to the L component from the analyses in
+    @see <https://doi.org/10.1007/978-3-031-30044-8_2> Schwarz, M., Saan, S., Seidl, H., Erhard, J., Vojdani, V. Clustered Relational Thread-Modular Abstract Interpretation with Local Traces.
+*)
 module ThreadDigest: Digest =
 struct
   include ThreadIdDomain.ThreadLifted
@@ -197,6 +200,25 @@ struct
     | _ -> false
 end
 
+(** Ego-Lane Derived digest based on whether given threads have been started yet, can be used to refine any analysis
+    @see PhD thesis of M. Schwarz once it is published ;)
+*)
+module ThreadNotStartedDigest:Digest =
+struct
+  include ThreadIdDomain.ThreadLifted
+
+  module TID = ThreadIdDomain.Thread
+
+  let current (ask: Q.ask) =
+    ThreadId.get_current ask
+
+  let accounted_for (ask: Q.ask) ~(current: t) ~(other: t) =
+    match current, other with
+    | `Lifted current, `Lifted other ->
+      MHP.definitely_not_started (current, ask.f Q.CreatedThreads) other
+    | _ -> false
+end
+
 module PerMutexTidCommon (Digest: Digest) (LD:Lattice.S) =
 struct
   include ConfCheck.RequireThreadFlagPathSensInit

src/analyses/threadEscape.ml

@@ -80,7 +80,10 @@ struct
       if ThreadIdSet.is_empty threads then
         false
       else begin
-        let possibly_started current = function
+        let other_possibly_started current = function
+          | `Lifted tid when (ThreadId.Thread.equal current tid && ThreadId.Thread.is_unique current) ->
+            (* if our own (unique) thread is started here, that is not a problem *)
+            false
           | `Lifted tid ->
             let threads = ctx.ask Queries.CreatedThreads in
             let not_started = MHP.definitely_not_started (current, threads) tid in
@@ -97,14 +100,14 @@ struct
         in
         match ctx.ask Queries.CurrentThreadId with
         | `Lifted current ->
-          let possibly_started = ThreadIdSet.exists (possibly_started current) threads in
+          let possibly_started = ThreadIdSet.exists (other_possibly_started current) threads in
           if possibly_started then
             true
           else
             let current_is_unique = ThreadId.Thread.is_unique current in
             let any_equal_current threads = ThreadIdSet.exists (equal_current current) threads in
             if not current_is_unique && any_equal_current threads then
-              (* Another instance of the non-unqiue current thread may have escaped the variable *)
+              (* Another instance of the non-unique current thread may have escaped the variable *)
               true
             else
               (* Check whether current unique thread has escaped the variable *)

src/analyses/useAfterFree.ml

@@ -36,8 +36,11 @@ struct
     (* If we're single-threaded or there are no threads freeing the memory, we have nothing to WARN about *)
     if ctx.ask (Queries.MustBeSingleThreaded { since_start = true }) || G.is_empty freeing_threads then ()
     else begin
-      let possibly_started current tid joined_threads =
+      let other_possibly_started current tid joined_threads =
         match tid with
+        | `Lifted tid when (ThreadId.Thread.equal current tid && ThreadId.Thread.is_unique current) ->
+          (* if our own (unique) thread is started here, that is not a problem *)
+          false
         | `Lifted tid ->
           let created_threads = ctx.ask Queries.CreatedThreads in
           let not_started = MHP.definitely_not_started (current, created_threads) tid in
@@ -58,7 +61,7 @@ struct
       let bug_name = if is_double_free then "Double Free" else "Use After Free" in
       match get_current_threadid ctx with
       | `Lifted current ->
-        let possibly_started = G.exists (possibly_started current) freeing_threads in
+        let possibly_started = G.exists (other_possibly_started current) freeing_threads in
         if possibly_started then begin
           if is_double_free then set_mem_safety_flag InvalidFree else set_mem_safety_flag InvalidDeref;
           M.warn ~category:(Behavior behavior) ~tags:[CWE cwe_number] "There's a thread that's been started in parallel with the memory-freeing threads for heap variable %a. %s might occur" CilType.Varinfo.pretty heap_var bug_name

src/cdomain/value/cdomains/threadIdDomain.ml

@@ -55,7 +55,7 @@ struct
             (struct let name = "no index" end)))
         (struct let name = "no node" end))
 
-  let show (f, ni_opt) = 
+  let show (f, ni_opt) =
     let vname = f.vname in
     match ni_opt with
     | None -> vname
@@ -143,6 +143,9 @@ struct
   let is_must_parent (p,s) (p',s') =
     if not (S.is_empty s) then
       false
+    else if P.equal p' p && S.is_empty s' then (* s is already empty *)
+      (* We do not consider a thread its own parent *)
+      false
     else
       let cdef_ancestor = P.common_suffix p p' in
       P.equal p cdef_ancestor

src/config/options.schema.json

@@ -754,7 +754,7 @@
               "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/write/write+lock",
               "type": "string",
-              "enum": ["none", "mutex-oplus", "mutex-meet", "protection", "protection-atomic", "protection-read", "protection-read-atomic", "mine", "mine-nothread", "mine-W", "mine-W-noinit", "lock", "write", "write+lock","mutex-meet-tid"],
+              "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", "write", "write+lock","mutex-meet-tid"],
               "default": "protection-read"
             },
             "priv": {

tests/regression/02-base/01-thread_creation.c

@@ -21,7 +21,7 @@ int main() {
   glob1 = 7;
   __goblint_check(glob1 == 7);
 
-  // Creat the thread
+  // Create the thread
   pthread_create(&id, NULL, t_fun, NULL);
 
   // The values should remain the same

tests/regression/13-privatized/75-protection-tid.c

@@ -0,0 +1,42 @@
+// PARAM: --set ana.base.privatization protection-tid
+#include <pthread.h>
+#include <goblint.h>
+
+int g;
+pthread_mutex_t m;
+
+void* spoiler() {
+  int x;
+  pthread_mutex_lock(&m);
+  x=g;
+  pthread_mutex_unlock(&m);
+}
+
+void* producer()
+{
+  pthread_mutex_lock(&m);
+  g = 8;
+  pthread_mutex_unlock(&m);
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid1;
+  pthread_t tid2;
+
+  pthread_create(&tid1, 0, spoiler, 0);
+
+  pthread_mutex_lock(&m);
+  __goblint_check(g == 0);
+  pthread_mutex_unlock(&m);
+
+  pthread_create(&tid2, 0, producer, 0);
+
+
+  pthread_mutex_lock(&m);
+  __goblint_check(g == 0); //UNKNOWN!
+  pthread_mutex_unlock(&m);
+
+  return 0;
+}