diff --git a/docs/user-guide/annotating.md b/docs/user-guide/annotating.md index cdfb892ffe..af632e60ed 100644 --- a/docs/user-guide/annotating.md +++ b/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. diff --git a/lib/goblint/runtime/include/goblint.h b/lib/goblint/runtime/include/goblint.h index af87035d33..8b32bf6ccb 100644 --- a/lib/goblint/runtime/include/goblint.h +++ b/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); diff --git a/src/analyses/libraryDesc.ml b/src/analyses/libraryDesc.ml index 4997b306a9..9117281e13 100644 --- a/src/analyses/libraryDesc.ml +++ b/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; } diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 8152e5b886..de3ff82ead 100644 --- a/src/analyses/libraryFunctions.ml +++ b/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 }); diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml index 21a8b69c93..6942e29bd7 100644 --- a/src/analyses/threadEscape.ml +++ b/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 diff --git a/tests/regression/46-apron2/70-nondet_inc_with_ghosts-globalize.c b/tests/regression/46-apron2/70-nondet_inc_with_ghosts-globalize.c index 2e01b017b8..07d90808ed 100644 --- a/tests/regression/46-apron2/70-nondet_inc_with_ghosts-globalize.c +++ b/tests/regression/46-apron2/70-nondet_inc_with_ghosts-globalize.c @@ -2,6 +2,7 @@ // TODO: -atomic unneeded? #include #include +#include extern int __VERIFIER_nondet_int(); extern void __VERIFIER_atomic_begin(); @@ -27,11 +28,6 @@ void* inc() return 0; } -void* dummy() -{ - return 0; -} - int main() { pthread_t tid; @@ -39,7 +35,7 @@ int main() 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();