Fix unsoundness from relation analysis reading special mutexes as integer variables

src/analyses/apron/relationPriv.apron.ml

@@ -607,7 +607,10 @@ struct
         )
       in
       (* Unprotected invariant is one big relation. *)
-      sideg (V.mutex atomic_mutex) rel_side;
+      (* If no globals are contained here, none need to be published *)
+      (* https://github.com/goblint/analyzer/pull/1354 *)
+      if RD.vars rel_side <> [] then
+        sideg (V.mutex atomic_mutex) rel_side;
       let rel_local =
         let newly_unprot var = match AV.find_metadata var with
           | Some (Global g) -> is_unprotected_without ask g atomic_mutex

src/util/library/libraryFunctions.ml

@@ -694,8 +694,8 @@ let linux_userspace_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
   ]
 [@@coverage off]
 
-let big_kernel_lock = AddrOf (Cil.var (Cilfacade.create_var (makeGlobalVar "[big kernel lock]" intType)))
-let console_sem = AddrOf (Cil.var (Cilfacade.create_var (makeGlobalVar "[console semaphore]" intType)))
+let big_kernel_lock = AddrOf (Cil.var (Cilfacade.create_var (makeGlobalVar "[big kernel lock]" voidType)))
+let console_sem = AddrOf (Cil.var (Cilfacade.create_var (makeGlobalVar "[console semaphore]" voidType)))
 
 (** Linux kernel functions. *)
 let linux_kernel_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
@@ -1017,7 +1017,7 @@ let math_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
   ]
 [@@coverage off]
 
-let verifier_atomic_var = Cilfacade.create_var (makeGlobalVar "[__VERIFIER_atomic]" intType)
+let verifier_atomic_var = Cilfacade.create_var (makeGlobalVar "[__VERIFIER_atomic]" voidType)
 let verifier_atomic = AddrOf (Cil.var (Cilfacade.create_var verifier_atomic_var))
 
 (** SV-COMP functions.
@@ -1032,7 +1032,7 @@ let svcomp_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
   ]
 [@@coverage off]
 
-let rtnl_lock = AddrOf (Cil.var (Cilfacade.create_var (makeGlobalVar "[rtnl_lock]" intType)))
+let rtnl_lock = AddrOf (Cil.var (Cilfacade.create_var (makeGlobalVar "[rtnl_lock]" voidType)))
 
 (** LDV Klever functions. *)
 let klever_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[

tests/regression/46-apron2/69-atomic-live.c

@@ -0,0 +1,26 @@
+// SKIP PARAM: --set ana.activated[+] apron --enable ana.sv-comp.functions --set ana.relation.privatization mutex-meet
+#include <pthread.h>
+#include <stdlib.h>
+#include <goblint.h>
+
+pthread_mutex_t mutex;
+
+void *fun(void* args)
+{
+   pthread_mutex_lock(&mutex);
+   pthread_mutex_unlock(&mutex);
+
+   __goblint_assert(1); //Reachable
+
+   __VERIFIER_atomic_begin();
+   __goblint_assert(1); //Reachable
+   __VERIFIER_atomic_end();
+
+  __goblint_assert(1); //Reachable
+}
+
+int main(void)
+{
+ pthread_t t;
+ pthread_create(&t, ((void *)0), fun, ((void *)0));
+}