Merge pull request #1216 from goblint/priv-atomic

Add some hacky atomic privatizations

Author: sim642

docs/user-guide/annotating.md

@@ -66,3 +66,4 @@ Include `goblint.h` when using these.
 * `__goblint_assume_join(id)` is like `pthread_join(id, NULL)`, but considers the given thread IDs must-joined even if Goblint cannot, e.g. due to non-uniqueness.
   Notably, this annotation can be used after a threads joining loop to make the assumption that the loop correctly joined all those threads.
   _Misuse of this annotation can cause unsoundness._
+* `__goblint_globalize(ptr)` forces all data potentially pointed to by `ptr` to be treated as global by simulating it escaping the thread.

lib/goblint/runtime/include/goblint.h

@@ -3,6 +3,7 @@ void __goblint_assume(int exp);
 void __goblint_assert(int exp);
 
 void __goblint_assume_join(/* pthread_t thread */); // undeclared argument to avoid pthread.h interfering with Linux kernel headers
+void __goblint_globalize(void *ptr);
 
 void __goblint_split_begin(int exp);
 void __goblint_split_end(int exp);

src/analyses/apron/relationPriv.apron.ml

@@ -634,6 +634,8 @@ module type PerGlobalPrivParam =
 sig
   (** Whether to also check unprotectedness by reads for extra precision. *)
   val check_read_unprotected: bool
+
+  include AtomicParam
 end
 
 (** Protection-Based Reading. *)
@@ -671,29 +673,35 @@ struct
 
   let startstate () = P.empty ()
 
-  let read_global ask getg (st: BaseComponents (D).t) x =
+  let read_global (ask: Queries.ask) getg (st: BaseComponents (D).t) x =
     if P.mem x st.priv then
       CPA.find x st.cpa
+    else if Param.handle_atomic && ask.f MustBeAtomic then
+      VD.join (CPA.find x st.cpa) (getg (V.unprotected x)) (* Account for previous unpublished unprotected writes in current atomic section. *)
     else if is_unprotected ask x then
       getg (V.unprotected x) (* CPA unnecessary because all values in GUnprot anyway *)
     else
       VD.join (CPA.find x st.cpa) (getg (V.protected x))
 
-  let write_global ?(invariant=false) ask getg sideg (st: BaseComponents (D).t) x v =
+  let write_global ?(invariant=false) (ask: Queries.ask) getg sideg (st: BaseComponents (D).t) x v =
     if not invariant then (
-      sideg (V.unprotected x) v;
+      if not (Param.handle_atomic && ask.f MustBeAtomic) then
+        sideg (V.unprotected x) v; (* Delay publishing unprotected write in the atomic section. *)
       if !earlyglobs then (* earlyglobs workaround for 13/60 *)
         sideg (V.protected x) v
         (* Unlock after invariant will still side effect refined value (if protected) from CPA, because cannot distinguish from non-invariant write since W is implicit. *)
     );
-    if is_unprotected ask x then
+    if Param.handle_atomic && ask.f MustBeAtomic then
+      {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. *)
+    else if is_unprotected ask x then
       st
     else
       {st with cpa = CPA.add x v st.cpa; priv = P.add x st.priv}
 
   let lock ask getg st m = st
 
   let unlock ask getg sideg (st: BaseComponents (D).t) m =
+    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) ->
         if is_protected_by ask m x then ( (* is_in_Gm *)
@@ -702,6 +710,8 @@ struct
              then inner unlock shouldn't yet publish. *)
           if not Param.check_read_unprotected || is_unprotected_without ask ~write:false x m then
             sideg (V.protected x) v;
+          if atomic then
+            sideg (V.unprotected x) v; (* Publish delayed unprotected write as if it were protected by the atomic section. *)
 
           if is_unprotected_without ask x m then (* is_in_V' *)
             {st with cpa = CPA.remove x st.cpa; priv = P.remove x st.priv}
@@ -1779,8 +1789,10 @@ 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 end))
-        | "protection-read" -> (module ProtectionBasedPriv (struct let check_read_unprotected = true end))
+        | "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 *)
         | "mine" -> (module MinePriv)
         | "mine-nothread" -> (module MineNoThreadPriv)
         | "mine-W" -> (module MineWPriv (struct let side_effect_global_init = true end))

src/analyses/basePriv.ml

@@ -9,6 +9,17 @@ module Q = Queries
 module IdxDom = ValueDomain.IndexDomain
 module VD     = BaseDomain.VD
 
+module type AtomicParam =
+sig
+  val handle_atomic: bool
+  (** Whether to handle SV-COMP atomic blocks (experimental). *)
+end
+
+module NoAtomic: AtomicParam =
+struct
+  let handle_atomic = false
+end
+
 module ConfCheck =
 struct
   module RequireMutexActivatedInit =
@@ -110,7 +121,11 @@ end
 
 module Locksets =
 struct
-  module Lock = LockDomain.Addr
+  module Lock =
+  struct
+    include LockDomain.Addr
+    let name () = "lock"
+  end
 
   module Lockset = SetDomain.ToppedSet (Lock) (struct let topname = "All locks" end)
 
@@ -206,7 +221,7 @@ struct
 
   module LLock =
   struct
-    include Printable.Either (Locksets.Lock) (CilType.Varinfo)
+    include Printable.Either (Locksets.Lock) (struct include CilType.Varinfo let name () = "global" end)
     let mutex m = `Left m
     let global x = `Right x
   end
@@ -218,7 +233,11 @@ struct
   end
 
   (* Map from locks to last written values thread-locally *)
-  module L = MapDomain.MapBot_LiftTop (LLock) (LD)
+  module L =
+  struct
+    include MapDomain.MapBot_LiftTop (LLock) (LD)
+    let name () = "L"
+  end
   module GMutex = MapDomain.MapBot_LiftTop (Digest) (LD)
   module GThread = Lattice.Prod (LMust) (L)
 

src/analyses/commonPriv.ml

@@ -229,7 +229,7 @@ struct
       let mutex_lockset = Lockset.export_locks @@ Lockset.singleton (mutex, true) in
       let protecting = protecting ~write protection v in
       (* TODO: unsound in 29/24, why did we do this before? *)
-      (* if LockDomain.Addr.equal mutex verifier_atomic then
+      (* if LockDomain.Addr.equal mutex (LockDomain.Addr.of_var LF.verifier_atomic_var) then
         true
       else *)
       Mutexes.leq mutex_lockset protecting

src/analyses/mutexAnalysis.ml

@@ -150,6 +150,9 @@ struct
   let special ctx (lval: lval option) (f:varinfo) (args:exp list) : D.t =
     let desc = LibraryFunctions.find f in
     match desc.special args, f.vname, args with
+    | Globalize ptr, _, _ ->
+      let escaped = escape_rval ctx (Analyses.ask_of_ctx ctx) ptr in
+      D.join ctx.local escaped
     | _, "pthread_setspecific" , [key; pt_value] ->
       let escaped = escape_rval ctx (Analyses.ask_of_ctx ctx) pt_value in
       D.join ctx.local escaped

src/analyses/threadEscape.ml

@@ -747,7 +747,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-read", "mine", "mine-nothread", "mine-W", "mine-W-noinit", "lock", "write", "write+lock","mutex-meet-tid"],
+              "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"],
               "default": "protection-read"
             },
             "priv": {
@@ -901,7 +901,7 @@
               "description":
                 "Which relation privatization to use? top/protection/protection-path/mutex-meet/mutex-meet-tid/mutex-meet-tid-cluster12/mutex-meet-tid-cluster2/mutex-meet-tid-cluster-max/mutex-meet-tid-cluster-power",
               "type": "string",
-              "enum": ["top", "protection", "protection-path", "mutex-meet", "mutex-meet-tid", "mutex-meet-tid-cluster12", "mutex-meet-tid-cluster2", "mutex-meet-tid-cluster-max", "mutex-meet-tid-cluster-power"],
+              "enum": ["top", "protection", "protection-path", "mutex-meet", "mutex-meet-atomic", "mutex-meet-tid", "mutex-meet-tid-atomic", "mutex-meet-tid-cluster12", "mutex-meet-tid-cluster2", "mutex-meet-tid-cluster-max", "mutex-meet-tid-cluster-power"],
               "default": "mutex-meet"
             },
             "priv": {

src/config/options.schema.json

@@ -56,6 +56,7 @@ type special =
   | ThreadCreate of { thread: Cil.exp; start_routine: Cil.exp; arg: Cil.exp; multiple: bool }
   | ThreadJoin of { thread: Cil.exp; ret_var: Cil.exp; }
   | ThreadExit of { ret_val: Cil.exp; }
+  | Globalize of Cil.exp
   | Signal of Cil.exp
   | Broadcast of Cil.exp
   | MutexAttrSetType of { attr:Cil.exp; typ: Cil.exp; }

src/util/library/libraryDesc.ml

@@ -759,6 +759,7 @@ let goblint_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__goblint_check", special [__ "exp" []] @@ fun exp -> Assert { exp; check = true; refine = false });
     ("__goblint_assume", special [__ "exp" []] @@ fun exp -> Assert { exp; check = false; refine = true });
     ("__goblint_assert", special [__ "exp" []] @@ fun exp -> Assert { exp; check = true; refine = get_bool "sem.assert.refine" });
+    ("__goblint_globalize", special [__ "ptr" []] @@ fun ptr -> Globalize ptr);
     ("__goblint_split_begin", unknown [drop "exp" []]);
     ("__goblint_split_end", unknown [drop "exp" []]);
     ("__goblint_bounded", special [__ "exp"[]] @@ fun exp -> Bounded { exp });

src/util/library/libraryFunctions.ml

@@ -0,0 +1,42 @@
+// PARAM: --enable ana.sv-comp.functions
+/*-----------------------------------------------------------------------------
+ * mutex.c - Concurrent program using locking to access a shared variable
+ *-----------------------------------------------------------------------------
+ * Author: Frank Schüssele
+ *   Date: 2023-07-11
+ *---------------------------------------------------------------------------*/
+#include <pthread.h>
+#include <goblint.h>
+
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int used;
+pthread_mutex_t m;
+
+void* producer()
+{
+  while (1) {
+    pthread_mutex_lock(&m);
+    used++;
+    used--;
+    pthread_mutex_unlock(&m);
+  }
+
+  return 0;
+}
+
+int main()
+{
+  pthread_t tid;
+
+  pthread_mutex_init(&m, 0);
+  pthread_create(&tid, 0, producer, 0);
+
+  pthread_mutex_lock(&m);
+  __goblint_check(used == 0);
+  pthread_mutex_unlock(&m);
+
+  pthread_mutex_destroy(&m);
+  return 0;
+}

tests/regression/13-privatized/74-mutex.c

@@ -1,4 +1,4 @@
-// PARAM: --enable ana.sv-comp.functions
+// PARAM: --enable ana.sv-comp.functions --set ana.base.privatization protection-atomic
 #include <pthread.h>
 #include <goblint.h>
 
@@ -21,7 +21,7 @@ void *t_fun(void *arg) {
 int main(void) {
   pthread_t id;
   pthread_create(&id, NULL, t_fun, NULL);
-  __goblint_check(myglobal == 5); // TODO
+  __goblint_check(myglobal == 5);
   __VERIFIER_atomic_begin();
   __goblint_check(myglobal == 5);
   __VERIFIER_atomic_end();

tests/regression/29-svcomp/16-atomic_priv.c

@@ -1,4 +1,4 @@
-// PARAM: --enable ana.sv-comp.functions
+// PARAM: --enable ana.sv-comp.functions --set ana.base.privatization protection-atomic
 #include <pthread.h>
 #include <goblint.h>
 
@@ -21,7 +21,7 @@ void *t_fun(void *arg) {
 int main(void) {
   pthread_t id;
   pthread_create(&id, NULL, t_fun, NULL);
-  __goblint_check(myglobal == 5); // TODO
+  __goblint_check(myglobal == 5);
   __VERIFIER_atomic_begin();
   __goblint_check(myglobal == 5);
   __VERIFIER_atomic_end();

tests/regression/29-svcomp/18-atomic_fun_priv.c

@@ -0,0 +1,30 @@
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set ana.base.privatization none
+#include <pthread.h>
+#include <goblint.h>
+
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int myglobal = 5;
+
+void *t_fun(void *arg) {
+  __VERIFIER_atomic_begin();
+  __goblint_check(myglobal == 5);
+  myglobal++;
+  __goblint_check(myglobal == 6);
+  myglobal--;
+  __goblint_check(myglobal == 5);
+  __VERIFIER_atomic_end();
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  __goblint_check(myglobal == 5);
+  __VERIFIER_atomic_begin();
+  __goblint_check(myglobal == 5);
+  __VERIFIER_atomic_end();
+  pthread_join (id, NULL);
+  return 0;
+}

tests/regression/46-apron2/61-atomic_priv.c

@@ -0,0 +1,30 @@
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set ana.base.privatization none
+#include <pthread.h>
+#include <goblint.h>
+
+int myglobal = 5;
+
+// atomic by function name prefix
+void __VERIFIER_atomic_fun() {
+  __goblint_check(myglobal == 5);
+  myglobal++;
+  __goblint_check(myglobal == 6);
+  myglobal--;
+  __goblint_check(myglobal == 5);
+}
+
+void *t_fun(void *arg) {
+  __VERIFIER_atomic_fun();
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  __goblint_check(myglobal == 5);
+  __VERIFIER_atomic_begin();
+  __goblint_check(myglobal == 5);
+  __VERIFIER_atomic_end();
+  pthread_join (id, NULL);
+  return 0;
+}

tests/regression/46-apron2/62-atomic_fun_priv.c

@@ -0,0 +1,28 @@
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set ana.base.privatization none
+#include <pthread.h>
+#include <goblint.h>
+
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int myglobal = 5;
+
+void *t_fun(void *arg) {
+  __VERIFIER_atomic_begin();
+  __goblint_check(myglobal == 5); // TODO
+  myglobal++;
+  __goblint_check(myglobal == 6); // TODO
+  __VERIFIER_atomic_end();
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  __goblint_check(myglobal == 5); // UNKNOWN!
+  __VERIFIER_atomic_begin();
+  __goblint_check(myglobal == 5); // UNKNOWN!
+  __VERIFIER_atomic_end();
+  pthread_join (id, NULL);
+  return 0;
+}

tests/regression/46-apron2/63-atomic_priv_sound.c

@@ -0,0 +1,43 @@
+// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet-atomic --set ana.base.privatization none
+#include <pthread.h>
+#include <goblint.h>
+
+extern void __VERIFIER_atomic_begin();
+extern void __VERIFIER_atomic_end();
+
+int myglobal = 0;
+int myglobal2 = 0;
+int myglobal3 = 0;
+
+void *t_fun(void *arg) {
+  __VERIFIER_atomic_begin();
+  myglobal2++;
+  __VERIFIER_atomic_end();
+  __VERIFIER_atomic_begin();
+  myglobal++;
+  __VERIFIER_atomic_end();
+  return NULL;
+}
+
+void *t2_fun(void *arg) {
+  __VERIFIER_atomic_begin();
+  myglobal3++;
+  __VERIFIER_atomic_end();
+  __VERIFIER_atomic_begin();
+  myglobal++;
+  __VERIFIER_atomic_end();
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id, id2;
+  pthread_create(&id, NULL, t_fun, NULL);
+  pthread_create(&id2, NULL, t2_fun, NULL);
+  __goblint_check(myglobal == 2); // UNKNOWN!
+  __VERIFIER_atomic_begin();
+  __goblint_check(myglobal == 2); // UNKNOWN!
+  __VERIFIER_atomic_end();
+  pthread_join (id, NULL);
+  pthread_join (id2, NULL);
+  return 0;
+}