Merge pull request #1441 from goblint/issue_1140

Fix unsoundness from relation analysis reading special mutexes as integer variables
goblint · May 7, 2024 · 29db9c2 · 29db9c2
2 parents 23ff80c + 1dcb3c9
commit 29db9c2
Show file tree

Hide file tree

Showing 3 changed files with 34 additions and 5 deletions.
diff --git a/src/analyses/apron/relationPriv.apron.ml b/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

diff --git a/src/util/library/libraryFunctions.ml b/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.[

diff --git a/tests/regression/46-apron2/69-atomic-live.c b/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));
+}