Add __goblint_globalize special function

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 data 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/libraryDesc.ml

@@ -56,6 +56,7 @@ type special =
   | ThreadCreate of { thread: Cil.exp; start_routine: Cil.exp; arg: Cil.exp; }
   | 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/analyses/libraryFunctions.ml

@@ -743,6 +743,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/analyses/threadEscape.ml

@@ -142,6 +142,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 ptr in
+      D.join ctx.local escaped
     | _, "pthread_setspecific" , [key; pt_value] ->
       let escaped = escape_rval ctx pt_value in
       D.join ctx.local escaped

tests/regression/46-apron2/70-nondet_inc_with_ghosts-globalize.c

@@ -2,6 +2,7 @@
 // TODO: -atomic unneeded?
 #include <pthread.h>
 #include <assert.h>
+#include <goblint.h>
 
 extern int  __VERIFIER_nondet_int();
 extern void __VERIFIER_atomic_begin();
@@ -27,19 +28,14 @@ void* inc()
   return 0;
 }
 
-void* dummy()
-{
-  return 0;
-}
-
 int main()
 {
   pthread_t tid;
   pthread_create(&tid, 0, inc, 0);
 
   int val = __VERIFIER_nondet_int();
   __VERIFIER_atomic_begin();
-  pthread_create(&tid, 0, dummy, &val); // globalize val by escaping
+  __goblint_globalize(&val);
   g = val; x = val;
   __VERIFIER_atomic_end();