From 80a51be64966b15376f5d1f83e61046d6e522565 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 29 Sep 2023 14:40:07 +0300
Subject: [PATCH 01/11] Add extensive atomic and volatile ignorable races tests

---
 .../regression/04-mutex/62-simple_atomic_nr.c | 83 ++++++++++++++++---
 tests/regression/04-mutex/99-volatile.c       | 51 ++++++++++--
 2 files changed, 114 insertions(+), 20 deletions(-)

diff --git a/tests/regression/04-mutex/62-simple_atomic_nr.c b/tests/regression/04-mutex/62-simple_atomic_nr.c
index d63f303251..fdef44bdd6 100644
--- a/tests/regression/04-mutex/62-simple_atomic_nr.c
+++ b/tests/regression/04-mutex/62-simple_atomic_nr.c
@@ -1,24 +1,83 @@
 #include <pthread.h>
-#include <stdio.h>
 #include <stdatomic.h>
 
-atomic_int myglobal;
-pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
-pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
+atomic_int g1;
+_Atomic int g2;
+_Atomic(int) g3;
+
+atomic_int a1[1];
+_Atomic int a2[1];
+_Atomic(int) a3[1];
+
+struct s {
+  int f0;
+  atomic_int f1;
+  _Atomic int f2;
+  _Atomic(int) f3;
+};
+
+struct s s1;
+_Atomic struct s s2;
+_Atomic(struct s) s3;
+
+typedef atomic_int t_int1;
+typedef _Atomic int t_int2;
+typedef _Atomic(int) t_int3;
+
+t_int1 t1;
+t_int2 t2;
+t_int3 t3;
+
+typedef int t_int0;
+
+_Atomic t_int0 t0;
+_Atomic(t_int0) t00;
+
+atomic_int *p0 = &g1;
+int x;
+// int * _Atomic p1 = &x; // TODO: https://github.com/goblint/cil/issues/64
+// _Atomic(int*) p2 = &x; // TODO: https://github.com/goblint/cil/issues/64
+// atomic_int * _Atomic p3 = &g1; // TODO: https://github.com/goblint/cil/issues/64
+
+atomic_flag flag = ATOMIC_FLAG_INIT;
 
 void *t_fun(void *arg) {
-  pthread_mutex_lock(&mutex1);
-  myglobal=myglobal+1; // NORACE
-  pthread_mutex_unlock(&mutex1);
+  g1++; // NORACE
+  g2++; // NORACE
+  g3++; // NORACE
+  a1[0]++; // NORACE
+  a2[0]++; // NORACE
+  a3[0]++; // NORACE
+  s1.f1++; // NORACE
+  s1.f2++; // NORACE
+  s1.f3++; // NORACE
+  s2.f0++; // NORACE
+  s3.f0++; // NORACE
+  t1++; // NORACE
+  t2++; // NORACE
+  t3++; // NORACE
+  t0++; // NORACE
+  t00++; // NORACE
+  (*p0)++; // NORACE
+  // p1++; // TODO NORACE: https://github.com/goblint/cil/issues/64
+  // p2++; // TODO NORACE: https://github.com/goblint/cil/issues/64
+  // p3++; // TODO NORACE: https://github.com/goblint/cil/issues/64
+  // (*p3)++; // TODO NORACE: https://github.com/goblint/cil/issues/64
+
+  struct s ss = {0};
+  s2 = ss; // NORACE
+  s3 = ss; // NORACE
+
+  atomic_flag_clear(&flag); // NORACE
+  atomic_flag_test_and_set(&flag); // NORACE
   return NULL;
 }
 
 int main(void) {
-  pthread_t id;
+  pthread_t id, id2;
   pthread_create(&id, NULL, t_fun, NULL);
-  pthread_mutex_lock(&mutex2);
-  myglobal=myglobal+1; // NORACE
-  pthread_mutex_unlock(&mutex2);
-  pthread_join (id, NULL);
+  pthread_create(&id2, NULL, t_fun, NULL);
+  pthread_join(id, NULL);
+  pthread_join(id2, NULL);
   return 0;
 }
diff --git a/tests/regression/04-mutex/99-volatile.c b/tests/regression/04-mutex/99-volatile.c
index aaf81f13a1..7c2a255902 100644
--- a/tests/regression/04-mutex/99-volatile.c
+++ b/tests/regression/04-mutex/99-volatile.c
@@ -1,18 +1,53 @@
 // PARAM: --disable ana.race.volatile
 #include <pthread.h>
-#include <stdio.h>
 
-volatile int myglobal;
+volatile int g1;
+
+volatile int a1[1];
+
+struct s {
+  int f0;
+  volatile int f1;
+};
+
+struct s s1;
+volatile struct s s2;
+
+typedef volatile int t_int1;
+
+t_int1 t1;
+
+typedef int t_int0;
+
+volatile t_int0 t0;
+
+volatile int *p0 = &g1;
+int x;
+int * volatile p1 = &x;
+volatile int * volatile p2 = &g1;
 
 void *t_fun(void *arg) {
-  myglobal= 8; //NORACE
+  g1++; // NORACE
+  a1[0]++; // NORACE
+  s1.f1++; // NORACE
+  s2.f0++; // NORACE
+  t1++; // NORACE
+  t0++; // NORACE
+  (*p0)++; // NORACE
+  p1++; // NORACE
+  p2++; // NORACE
+  (*p2)++; // NORACE
+
+  struct s ss = {0};
+  s2 = ss; // NORACE
   return NULL;
 }
 
 int main(void) {
-  pthread_t id;
-  pthread_create(&id, NULL, t_fun, (void*) &myglobal);
-  myglobal = 42; //NORACE
-  pthread_join (id, NULL);
+  pthread_t id, id2;
+  pthread_create(&id, NULL, t_fun, NULL);
+  pthread_create(&id2, NULL, t_fun, NULL);
+  pthread_join(id, NULL);
+  pthread_join(id2, NULL);
   return 0;
-}
\ No newline at end of file
+}

From 8b513e8431e6f6301fca9162e83a2b7ed792dbcd Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 29 Sep 2023 15:39:45 +0300
Subject: [PATCH 02/11] Rewrite ignorable race memo check

---
 src/domains/access.ml | 64 ++++++++++++++++++++++++++++++++++---------
 1 file changed, 51 insertions(+), 13 deletions(-)

diff --git a/src/domains/access.ml b/src/domains/access.ml
index fa6446df16..7b6fa77b06 100644
--- a/src/domains/access.ml
+++ b/src/domains/access.ml
@@ -10,7 +10,7 @@ module M = Messages
 (* Some helper functions to avoid flagging race warnings on atomic types, and
  * other irrelevant stuff, such as mutexes and functions. *)
 
-let is_ignorable_type (t: typ): bool =
+let rec is_ignorable_type (t: typ): bool =
   match t with
   | TNamed ({ tname = "atomic_t" | "pthread_mutex_t" | "pthread_rwlock_t" | "pthread_spinlock_t" | "spinlock_t" | "pthread_cond_t"; _ }, _) -> true
   | TComp ({ cname = "__pthread_mutex_s" | "__pthread_rwlock_arch_t" | "__jmp_buf_tag" | "_pthread_cleanup_buffer" | "__pthread_cleanup_frame" | "__cancel_jmp_buf_tag"; _}, _) -> true
@@ -18,20 +18,59 @@ let is_ignorable_type (t: typ): bool =
     begin match Cilfacade.split_anoncomp_name cname with
       | (true, Some ("__once_flag" | "__pthread_unwind_buf_t" | "__cancel_jmp_buf"), _) -> true (* anonstruct *)
       | (false, Some ("pthread_mutexattr_t" | "pthread_condattr_t" | "pthread_barrierattr_t"), _) -> true (* anonunion *)
-      | _ -> false
+      | _ -> false (* TODO: fall back to attrs case *)
     end
   | TComp ({ cname = "lock_class_key"; _ }, _) -> true
   | TInt (IInt, attr) when hasAttribute "mutex" attr -> true
-  | t when hasAttribute "atomic" (typeAttrs t) -> true (* C11 _Atomic *)
-  | _ -> false
+  | TFun _ -> true
+  | _ ->
+    let attrs = typeAttrsOuter t in
+    let is_ignorable_attr = function
+      | Attr ("volatile", _) when not (get_bool "ana.race.volatile") -> true (* volatile & races on volatiles should not be reported *)
+      | Attr ("atomic", _) -> true (* C11 _Atomic *)
+      | _ -> false
+    in
+    if List.exists is_ignorable_attr attrs then
+      true
+    else (
+      match t with
+      | TNamed ({ttype; _}, attrs) -> is_ignorable_type (typeAddAttributes attrs ttype)
+      | _ -> false
+    )
+
+let rec is_ignorable_type_offset (t: typ) (o: _ Offset.t): bool =
+  if is_ignorable_type t then
+    true
+  else (
+    let blendAttributes baseAttrs = (* copied from Cilfacade.typeOffset *)
+      let (_, _, contageous) = partitionAttributes ~default:AttrName baseAttrs in
+      typeAddAttributes contageous
+    in
+    match o with
+    | `NoOffset -> false (* already checked t *)
+    | `Index (_, o') ->
+      begin match unrollType t with
+        | TArray (et, _, attrs) ->
+          let t' = blendAttributes attrs et in
+          is_ignorable_type_offset t' o'
+        | _ -> false (* index on non-array*)
+      end
+    | `Field (f, o') ->
+      begin match unrollType t with
+        | TComp (_, attrs) ->
+          let t' = blendAttributes attrs f.ftype in
+          is_ignorable_type_offset t' o'
+        | _ -> false (* field on non-compound *)
+      end
+  )
+
+let is_ignorable_mval = function
+  | ({vaddrof = false; vattr; _}, _) when hasAttribute "thread" vattr -> true (* Thread-Local Storage *)
+  | (v, o) -> is_ignorable_type_offset v.vtype o
 
-let is_ignorable = function
-  | None -> false
-  | Some (v,os) when hasAttribute "thread" v.vattr && not (v.vaddrof) -> true (* Thread-Local Storage *)
-  | Some (v,os) when BaseUtil.is_volatile v && not (get_bool "ana.race.volatile")  -> true (* volatile & races on volatiles should not be reported *)
-  | Some (v,os) ->
-    try isFunctionType v.vtype || is_ignorable_type v.vtype
-    with Not_found -> false
+let is_ignorable_memo = function
+  | (`Type _, _) -> false (* TODO: do something *)
+  | (`Var v, o) -> is_ignorable_mval (v, o)
 
 module TSH = Hashtbl.Make (CilType.Typsig)
 
@@ -195,8 +234,7 @@ let get_val_type e: acc_typ =
 
 (** Add access to {!Memo} after distributing. *)
 let add_one ~side memo: unit =
-  let mv = Memo.to_mval memo in
-  let ignorable = is_ignorable mv in
+  let ignorable = is_ignorable_memo memo in
   if M.tracing then M.trace "access" "add_one %a (ignorable = %B)\n" Memo.pretty memo ignorable;
   if not ignorable then
     side memo

From 66071f2555aa6f6be4cb2be8b8795cab2a0e5888 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 29 Sep 2023 15:47:28 +0300
Subject: [PATCH 03/11] Exclude atomic_flag races

---
 src/analyses/libraryFunctions.ml | 6 ++++++
 src/domains/access.ml            | 2 +-
 2 files changed, 7 insertions(+), 1 deletion(-)

diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index c3ca48da93..6ff591e7c4 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -127,6 +127,10 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env });
     ("longjmp", special [__ "env" [r]; __ "value" []] @@ fun env value -> Longjmp { env; value });
     ("atexit", unknown [drop "function" [s]]);
+    ("atomic_flag_clear", unknown [drop "obj" [w]]);
+    ("atomic_flag_clear_explicit", unknown [drop "obj" [w]; drop "order" []]);
+    ("atomic_flag_test_and_set", unknown [drop "obj" [r; w]]);
+    ("atomic_flag_test_and_set_explicit", unknown [drop "obj" [r; w]; drop "order" []]);
   ]
 
 (** C POSIX library functions.
@@ -435,6 +439,8 @@ let gcc_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__builtin_popcountll", unknown [drop "x" []]);
     ("__atomic_store_n", unknown [drop "ptr" [w]; drop "val" []; drop "memorder" []]);
     ("__atomic_load_n", unknown [drop "ptr" [r]; drop "memorder" []]);
+    ("__atomic_clear", unknown [drop "ptr" [w]; drop "memorder" []]);
+    ("__atomic_test_and_set", unknown [drop "ptr" [r; w]; drop "memorder" []]);
     ("__sync_fetch_and_add", unknown (drop "ptr" [r; w] :: drop "value" [] :: VarArgs (drop' [])));
     ("__sync_fetch_and_sub", unknown (drop "ptr" [r; w] :: drop "value" [] :: VarArgs (drop' [])));
     ("__builtin_va_copy", unknown [drop "dest" [w]; drop "src" [r]]);
diff --git a/src/domains/access.ml b/src/domains/access.ml
index 7b6fa77b06..7066e6e349 100644
--- a/src/domains/access.ml
+++ b/src/domains/access.ml
@@ -12,7 +12,7 @@ module M = Messages
 
 let rec is_ignorable_type (t: typ): bool =
   match t with
-  | TNamed ({ tname = "atomic_t" | "pthread_mutex_t" | "pthread_rwlock_t" | "pthread_spinlock_t" | "spinlock_t" | "pthread_cond_t"; _ }, _) -> true
+  | TNamed ({ tname = "atomic_t" | "pthread_mutex_t" | "pthread_rwlock_t" | "pthread_spinlock_t" | "spinlock_t" | "pthread_cond_t" | "atomic_flag"; _ }, _) -> true
   | TComp ({ cname = "__pthread_mutex_s" | "__pthread_rwlock_arch_t" | "__jmp_buf_tag" | "_pthread_cleanup_buffer" | "__pthread_cleanup_frame" | "__cancel_jmp_buf_tag"; _}, _) -> true
   | TComp ({ cname; _}, _) when String.starts_with_stdlib ~prefix:"__anon" cname ->
     begin match Cilfacade.split_anoncomp_name cname with

From df9fda742d767ab92108b127a21b5d137967c312 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 29 Sep 2023 15:58:36 +0300
Subject: [PATCH 04/11] Document refactored race ignore check

---
 src/domains/access.ml | 20 ++++++++++++--------
 1 file changed, 12 insertions(+), 8 deletions(-)

diff --git a/src/domains/access.ml b/src/domains/access.ml
index 7066e6e349..3601624ae6 100644
--- a/src/domains/access.ml
+++ b/src/domains/access.ml
@@ -11,6 +11,7 @@ module M = Messages
  * other irrelevant stuff, such as mutexes and functions. *)
 
 let rec is_ignorable_type (t: typ): bool =
+  (* efficient pattern matching first *)
   match t with
   | TNamed ({ tname = "atomic_t" | "pthread_mutex_t" | "pthread_rwlock_t" | "pthread_spinlock_t" | "spinlock_t" | "pthread_cond_t" | "atomic_flag"; _ }, _) -> true
   | TComp ({ cname = "__pthread_mutex_s" | "__pthread_rwlock_arch_t" | "__jmp_buf_tag" | "_pthread_cleanup_buffer" | "__pthread_cleanup_frame" | "__cancel_jmp_buf_tag"; _}, _) -> true
@@ -18,13 +19,13 @@ let rec is_ignorable_type (t: typ): bool =
     begin match Cilfacade.split_anoncomp_name cname with
       | (true, Some ("__once_flag" | "__pthread_unwind_buf_t" | "__cancel_jmp_buf"), _) -> true (* anonstruct *)
       | (false, Some ("pthread_mutexattr_t" | "pthread_condattr_t" | "pthread_barrierattr_t"), _) -> true (* anonunion *)
-      | _ -> false (* TODO: fall back to attrs case *)
+      | _ -> false (* TODO: fall back to attrs case? *)
     end
-  | TComp ({ cname = "lock_class_key"; _ }, _) -> true
-  | TInt (IInt, attr) when hasAttribute "mutex" attr -> true
+  | TComp ({ cname = "lock_class_key"; _ }, _) -> true (* kernel? *)
+  | TInt (IInt, attr) when hasAttribute "mutex" attr -> true (* kernel? *)
   | TFun _ -> true
-  | _ ->
-    let attrs = typeAttrsOuter t in
+  | _ -> (* check attrs *)
+    let attrs = typeAttrsOuter t in (* only outer because we unroll TNamed ourselves *)
     let is_ignorable_attr = function
       | Attr ("volatile", _) when not (get_bool "ana.race.volatile") -> true (* volatile & races on volatiles should not be reported *)
       | Attr ("atomic", _) -> true (* C11 _Atomic *)
@@ -33,14 +34,17 @@ let rec is_ignorable_type (t: typ): bool =
     if List.exists is_ignorable_attr attrs then
       true
     else (
+      (* unroll TNamed once *)
+      (* can't use unrollType because we want to check TNamed-s at all intermediate typedefs as well *)
       match t with
       | TNamed ({ttype; _}, attrs) -> is_ignorable_type (typeAddAttributes attrs ttype)
       | _ -> false
     )
 
 let rec is_ignorable_type_offset (t: typ) (o: _ Offset.t): bool =
+  (* similar to Cilfacade.typeOffset but we want to check types at all intermediate offsets as well *)
   if is_ignorable_type t then
-    true
+    true (* type at offset so far ignorable, no need to recurse *)
   else (
     let blendAttributes baseAttrs = (* copied from Cilfacade.typeOffset *)
       let (_, _, contageous) = partitionAttributes ~default:AttrName baseAttrs in
@@ -53,7 +57,7 @@ let rec is_ignorable_type_offset (t: typ) (o: _ Offset.t): bool =
         | TArray (et, _, attrs) ->
           let t' = blendAttributes attrs et in
           is_ignorable_type_offset t' o'
-        | _ -> false (* index on non-array*)
+        | _ -> false (* index on non-array *)
       end
     | `Field (f, o') ->
       begin match unrollType t with
@@ -66,7 +70,7 @@ let rec is_ignorable_type_offset (t: typ) (o: _ Offset.t): bool =
 
 let is_ignorable_mval = function
   | ({vaddrof = false; vattr; _}, _) when hasAttribute "thread" vattr -> true (* Thread-Local Storage *)
-  | (v, o) -> is_ignorable_type_offset v.vtype o
+  | (v, o) -> is_ignorable_type_offset v.vtype o (* can't use Cilfacade.typeOffset because we want to check types at all intermediate offsets as well *)
 
 let is_ignorable_memo = function
   | (`Type _, _) -> false (* TODO: do something *)

From 18a1733dc41bbea8178bc7b481c4de48abe43970 Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Fri, 29 Sep 2023 16:20:13 +0300
Subject: [PATCH 05/11] Add atomic library functions from nidhugg benchmark set

---
 src/analyses/libraryFunctions.ml | 13 +++++++++++++
 1 file changed, 13 insertions(+)

diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml
index 6ff591e7c4..1964b7bc1f 100644
--- a/src/analyses/libraryFunctions.ml
+++ b/src/analyses/libraryFunctions.ml
@@ -131,6 +131,8 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("atomic_flag_clear_explicit", unknown [drop "obj" [w]; drop "order" []]);
     ("atomic_flag_test_and_set", unknown [drop "obj" [r; w]]);
     ("atomic_flag_test_and_set_explicit", unknown [drop "obj" [r; w]; drop "order" []]);
+    ("atomic_load", unknown [drop "obj" [r]]);
+    ("atomic_store", unknown [drop "obj" [w]; drop "desired" []]);
   ]
 
 (** C POSIX library functions.
@@ -438,9 +440,20 @@ let gcc_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("__builtin_popcountl", unknown [drop "x" []]);
     ("__builtin_popcountll", unknown [drop "x" []]);
     ("__atomic_store_n", unknown [drop "ptr" [w]; drop "val" []; drop "memorder" []]);
+    ("__atomic_store", unknown [drop "ptr" [w]; drop "val" [r]; drop "memorder" []]);
     ("__atomic_load_n", unknown [drop "ptr" [r]; drop "memorder" []]);
+    ("__atomic_load", unknown [drop "ptr" [r]; drop "ret" [w]; drop "memorder" []]);
     ("__atomic_clear", unknown [drop "ptr" [w]; drop "memorder" []]);
+    ("__atomic_compare_exchange_n", unknown [drop "ptr" [r; w]; drop "expected" [r; w]; drop "desired" []; drop "weak" []; drop "success_memorder" []; drop "failure_memorder" []]);
+    ("__atomic_compare_exchange", unknown [drop "ptr" [r; w]; drop "expected" [r; w]; drop "desired" [r]; drop "weak" []; drop "success_memorder" []; drop "failure_memorder" []]);
+    ("__atomic_fetch_add", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]);
+    ("__atomic_fetch_sub", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]);
+    ("__atomic_fetch_and", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]);
+    ("__atomic_fetch_xor", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]);
+    ("__atomic_fetch_or", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]);
+    ("__atomic_fetch_nand", unknown [drop "ptr" [r; w]; drop "val" []; drop "memorder" []]);
     ("__atomic_test_and_set", unknown [drop "ptr" [r; w]; drop "memorder" []]);
+    ("__atomic_thread_fence", unknown [drop "memorder" []]);
     ("__sync_fetch_and_add", unknown (drop "ptr" [r; w] :: drop "value" [] :: VarArgs (drop' [])));
     ("__sync_fetch_and_sub", unknown (drop "ptr" [r; w] :: drop "value" [] :: VarArgs (drop' [])));
     ("__builtin_va_copy", unknown [drop "dest" [w]; drop "src" [r]]);

From 8c7dbb5d726ffb6084ad9276f1367f2f7032735c Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 29 Sep 2023 16:42:28 +0300
Subject: [PATCH 06/11] Ignore FILE type in races

We are unsound for I/O races anyway.
---
 src/domains/access.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/domains/access.ml b/src/domains/access.ml
index 3601624ae6..69fb5b53fc 100644
--- a/src/domains/access.ml
+++ b/src/domains/access.ml
@@ -13,8 +13,8 @@ module M = Messages
 let rec is_ignorable_type (t: typ): bool =
   (* efficient pattern matching first *)
   match t with
-  | TNamed ({ tname = "atomic_t" | "pthread_mutex_t" | "pthread_rwlock_t" | "pthread_spinlock_t" | "spinlock_t" | "pthread_cond_t" | "atomic_flag"; _ }, _) -> true
-  | TComp ({ cname = "__pthread_mutex_s" | "__pthread_rwlock_arch_t" | "__jmp_buf_tag" | "_pthread_cleanup_buffer" | "__pthread_cleanup_frame" | "__cancel_jmp_buf_tag"; _}, _) -> true
+  | TNamed ({ tname = "atomic_t" | "pthread_mutex_t" | "pthread_rwlock_t" | "pthread_spinlock_t" | "spinlock_t" | "pthread_cond_t" | "atomic_flag" | "FILE" | "__FILE"; _ }, _) -> true
+  | TComp ({ cname = "__pthread_mutex_s" | "__pthread_rwlock_arch_t" | "__jmp_buf_tag" | "_pthread_cleanup_buffer" | "__pthread_cleanup_frame" | "__cancel_jmp_buf_tag" | "_IO_FILE"; _}, _) -> true
   | TComp ({ cname; _}, _) when String.starts_with_stdlib ~prefix:"__anon" cname ->
     begin match Cilfacade.split_anoncomp_name cname with
       | (true, Some ("__once_flag" | "__pthread_unwind_buf_t" | "__cancel_jmp_buf"), _) -> true (* anonstruct *)

From abc97e5773dd68e4745ebf3daac4a1538b9d5bb6 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 29 Sep 2023 16:56:45 +0300
Subject: [PATCH 07/11] Pin goblint-cil with exposed Cil.typeSigAddAttrs

---
 goblint.opam          | 7 +++----
 goblint.opam.locked   | 6 ++++++
 goblint.opam.template | 7 +++----
 3 files changed, 12 insertions(+), 8 deletions(-)

diff --git a/goblint.opam b/goblint.opam
index 661222805b..c84e7a56f0 100644
--- a/goblint.opam
+++ b/goblint.opam
@@ -74,12 +74,11 @@ dev-repo: "git+https://github.com/goblint/analyzer.git"
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 available: os-distribution != "alpine" & arch != "arm64"
-# pin-depends: [
-  # published goblint-cil 2.0.2 is currently up-to-date, so no pin needed
-  # [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#98598d94f796a63751e5a9d39c6b3a9fe1f32330" ]
+pin-depends: [
+  [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#398dca3d94a06a9026b3737aabf100ee3498229f" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   # [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
-# ]
+]
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]
diff --git a/goblint.opam.locked b/goblint.opam.locked
index bb59c41dd1..8556e9eebb 100644
--- a/goblint.opam.locked
+++ b/goblint.opam.locked
@@ -128,3 +128,9 @@ conflicts: [
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]
+pin-depends: [
+  [
+    "goblint-cil.2.0.2"
+    "git+https://github.com/goblint/cil.git#398dca3d94a06a9026b3737aabf100ee3498229f"
+  ]
+]
diff --git a/goblint.opam.template b/goblint.opam.template
index 6259c4d498..d9e1ebf477 100644
--- a/goblint.opam.template
+++ b/goblint.opam.template
@@ -1,12 +1,11 @@
 # on `dune build` goblint.opam will be generated from goblint.opam.template and dune-project
 # also remember to generate/adjust goblint.opam.locked!
 available: os-distribution != "alpine" & arch != "arm64"
-# pin-depends: [
-  # published goblint-cil 2.0.2 is currently up-to-date, so no pin needed
-  # [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#98598d94f796a63751e5a9d39c6b3a9fe1f32330" ]
+pin-depends: [
+  [ "goblint-cil.2.0.2" "git+https://github.com/goblint/cil.git#398dca3d94a06a9026b3737aabf100ee3498229f" ]
   # TODO: add back after release, only pinned for optimization (https://github.com/ocaml-ppx/ppx_deriving/pull/252)
   # [ "ppx_deriving.5.2.1" "git+https://github.com/ocaml-ppx/ppx_deriving.git#0a89b619f94cbbfc3b0fb3255ab4fe5bc77d32d6" ]
-# ]
+]
 post-messages: [
   "Do not benchmark Goblint on OCaml 5 (https://goblint.readthedocs.io/en/latest/user-guide/benchmarking/)." {ocaml:version >= "5.0.0"}
 ]

From 93396c8c43ec961d21dadbe6598be5c4ca768a91 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 29 Sep 2023 16:58:56 +0300
Subject: [PATCH 08/11] Duplicate race ignore check for typsig

---
 src/domains/access.ml | 51 ++++++++++++++++++++++++++++++++++++++++++-
 1 file changed, 50 insertions(+), 1 deletion(-)

diff --git a/src/domains/access.ml b/src/domains/access.ml
index 69fb5b53fc..ac34966880 100644
--- a/src/domains/access.ml
+++ b/src/domains/access.ml
@@ -68,12 +68,61 @@ let rec is_ignorable_type_offset (t: typ) (o: _ Offset.t): bool =
       end
   )
 
+let is_ignorable_typsig (ts: typsig): bool =
+  (* efficient pattern matching first *)
+  match ts with
+  | TSComp (_, ("__pthread_mutex_s" | "__pthread_rwlock_arch_t" | "__jmp_buf_tag" | "_pthread_cleanup_buffer" | "__pthread_cleanup_frame" | "__cancel_jmp_buf_tag" | "_IO_FILE"), _) -> true
+  | TSComp (_, cname, _) when String.starts_with_stdlib ~prefix:"__anon" cname ->
+    begin match Cilfacade.split_anoncomp_name cname with
+      | (true, Some ("__once_flag" | "__pthread_unwind_buf_t" | "__cancel_jmp_buf"), _) -> true (* anonstruct *)
+      | (false, Some ("pthread_mutexattr_t" | "pthread_condattr_t" | "pthread_barrierattr_t"), _) -> true (* anonunion *)
+      | _ -> false (* TODO: fall back to attrs case? *)
+    end
+  | TSComp (_, "lock_class_key", _) -> true (* kernel? *)
+  | TSFun _ -> true
+  | TSBase t -> is_ignorable_type t
+  | _ -> (* check attrs *)
+    let attrs = typeSigAttrs ts in (* only outer because we unroll TNamed ourselves *)
+    let is_ignorable_attr = function
+      | Attr ("volatile", _) when not (get_bool "ana.race.volatile") -> true (* volatile & races on volatiles should not be reported *)
+      | Attr ("atomic", _) -> true (* C11 _Atomic *)
+      | _ -> false
+    in
+    List.exists is_ignorable_attr attrs
+
+let rec is_ignorable_typsig_offset (ts: typsig) (o: _ Offset.t): bool =
+  (* similar to Cilfacade.typeOffset but we want to check types at all intermediate offsets as well *)
+  if is_ignorable_typsig ts then
+    true (* type at offset so far ignorable, no need to recurse *)
+  else (
+    let blendAttributes baseAttrs = (* copied from Cilfacade.typeOffset *)
+      let (_, _, contageous) = partitionAttributes ~default:AttrName baseAttrs in
+      typeSigAddAttrs contageous
+    in
+    match o with
+    | `NoOffset -> false (* already checked t *)
+    | `Index (_, o') ->
+      begin match ts with
+        | TSArray (et, _, attrs) ->
+          let t' = blendAttributes attrs et in
+          is_ignorable_typsig_offset t' o'
+        | _ -> false (* index on non-array *)
+      end
+    | `Field (f, o') ->
+      begin match ts with
+        | TSComp (_, _, attrs) ->
+          let t' = blendAttributes attrs (typeSig f.ftype) in
+          is_ignorable_typsig_offset t' o'
+        | _ -> false (* field on non-compound *)
+      end
+  )
+
 let is_ignorable_mval = function
   | ({vaddrof = false; vattr; _}, _) when hasAttribute "thread" vattr -> true (* Thread-Local Storage *)
   | (v, o) -> is_ignorable_type_offset v.vtype o (* can't use Cilfacade.typeOffset because we want to check types at all intermediate offsets as well *)
 
 let is_ignorable_memo = function
-  | (`Type _, _) -> false (* TODO: do something *)
+  | (`Type ts, o) -> is_ignorable_typsig_offset ts o
   | (`Var v, o) -> is_ignorable_mval (v, o)
 
 module TSH = Hashtbl.Make (CilType.Typsig)

From 1d3c7dd62f7d33f39dc69f95bbba0f83b659686e Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 29 Sep 2023 17:08:53 +0300
Subject: [PATCH 09/11] Extract common comp name and attrs ignoring for races

---
 src/domains/access.ml | 56 +++++++++++++++++++------------------------
 1 file changed, 24 insertions(+), 32 deletions(-)

diff --git a/src/domains/access.ml b/src/domains/access.ml
index ac34966880..832c6a762e 100644
--- a/src/domains/access.ml
+++ b/src/domains/access.ml
@@ -10,28 +10,34 @@ module M = Messages
 (* Some helper functions to avoid flagging race warnings on atomic types, and
  * other irrelevant stuff, such as mutexes and functions. *)
 
-let rec is_ignorable_type (t: typ): bool =
-  (* efficient pattern matching first *)
-  match t with
-  | TNamed ({ tname = "atomic_t" | "pthread_mutex_t" | "pthread_rwlock_t" | "pthread_spinlock_t" | "spinlock_t" | "pthread_cond_t" | "atomic_flag" | "FILE" | "__FILE"; _ }, _) -> true
-  | TComp ({ cname = "__pthread_mutex_s" | "__pthread_rwlock_arch_t" | "__jmp_buf_tag" | "_pthread_cleanup_buffer" | "__pthread_cleanup_frame" | "__cancel_jmp_buf_tag" | "_IO_FILE"; _}, _) -> true
-  | TComp ({ cname; _}, _) when String.starts_with_stdlib ~prefix:"__anon" cname ->
+let is_ignorable_comp_name = function
+  | "__pthread_mutex_s" | "__pthread_rwlock_arch_t" | "__jmp_buf_tag" | "_pthread_cleanup_buffer" | "__pthread_cleanup_frame" | "__cancel_jmp_buf_tag" | "_IO_FILE" -> true
+  | cname when String.starts_with_stdlib ~prefix:"__anon" cname ->
     begin match Cilfacade.split_anoncomp_name cname with
       | (true, Some ("__once_flag" | "__pthread_unwind_buf_t" | "__cancel_jmp_buf"), _) -> true (* anonstruct *)
       | (false, Some ("pthread_mutexattr_t" | "pthread_condattr_t" | "pthread_barrierattr_t"), _) -> true (* anonunion *)
-      | _ -> false (* TODO: fall back to attrs case? *)
+      | _ -> false
     end
-  | TComp ({ cname = "lock_class_key"; _ }, _) -> true (* kernel? *)
+  | "lock_class_key" -> true (* kernel? *)
+  | _ -> false
+
+let is_ignorable_attrs attrs =
+  let is_ignorable_attr = function
+    | Attr ("volatile", _) when not (get_bool "ana.race.volatile") -> true (* volatile & races on volatiles should not be reported *)
+    | Attr ("atomic", _) -> true (* C11 _Atomic *)
+    | _ -> false
+  in
+  List.exists is_ignorable_attr attrs
+
+let rec is_ignorable_type (t: typ): bool =
+  (* efficient pattern matching first *)
+  match t with
+  | TNamed ({ tname = "atomic_t" | "pthread_mutex_t" | "pthread_rwlock_t" | "pthread_spinlock_t" | "spinlock_t" | "pthread_cond_t" | "atomic_flag" | "FILE" | "__FILE"; _ }, _) -> true
+  | TComp ({ cname; _}, _) when is_ignorable_comp_name cname -> true
   | TInt (IInt, attr) when hasAttribute "mutex" attr -> true (* kernel? *)
   | TFun _ -> true
-  | _ -> (* check attrs *)
-    let attrs = typeAttrsOuter t in (* only outer because we unroll TNamed ourselves *)
-    let is_ignorable_attr = function
-      | Attr ("volatile", _) when not (get_bool "ana.race.volatile") -> true (* volatile & races on volatiles should not be reported *)
-      | Attr ("atomic", _) -> true (* C11 _Atomic *)
-      | _ -> false
-    in
-    if List.exists is_ignorable_attr attrs then
+  | _ ->
+    if is_ignorable_attrs (typeAttrsOuter t) then (* only outer because we unroll TNamed ourselves *)
       true
     else (
       (* unroll TNamed once *)
@@ -71,24 +77,10 @@ let rec is_ignorable_type_offset (t: typ) (o: _ Offset.t): bool =
 let is_ignorable_typsig (ts: typsig): bool =
   (* efficient pattern matching first *)
   match ts with
-  | TSComp (_, ("__pthread_mutex_s" | "__pthread_rwlock_arch_t" | "__jmp_buf_tag" | "_pthread_cleanup_buffer" | "__pthread_cleanup_frame" | "__cancel_jmp_buf_tag" | "_IO_FILE"), _) -> true
-  | TSComp (_, cname, _) when String.starts_with_stdlib ~prefix:"__anon" cname ->
-    begin match Cilfacade.split_anoncomp_name cname with
-      | (true, Some ("__once_flag" | "__pthread_unwind_buf_t" | "__cancel_jmp_buf"), _) -> true (* anonstruct *)
-      | (false, Some ("pthread_mutexattr_t" | "pthread_condattr_t" | "pthread_barrierattr_t"), _) -> true (* anonunion *)
-      | _ -> false (* TODO: fall back to attrs case? *)
-    end
-  | TSComp (_, "lock_class_key", _) -> true (* kernel? *)
+  | TSComp (_, cname, _) when is_ignorable_comp_name cname -> true
   | TSFun _ -> true
   | TSBase t -> is_ignorable_type t
-  | _ -> (* check attrs *)
-    let attrs = typeSigAttrs ts in (* only outer because we unroll TNamed ourselves *)
-    let is_ignorable_attr = function
-      | Attr ("volatile", _) when not (get_bool "ana.race.volatile") -> true (* volatile & races on volatiles should not be reported *)
-      | Attr ("atomic", _) -> true (* C11 _Atomic *)
-      | _ -> false
-    in
-    List.exists is_ignorable_attr attrs
+  | _ -> is_ignorable_attrs (typeSigAttrs ts)
 
 let rec is_ignorable_typsig_offset (ts: typsig) (o: _ Offset.t): bool =
   (* similar to Cilfacade.typeOffset but we want to check types at all intermediate offsets as well *)

From 52eac2fbf9287db299514a2b72846cb060c8f234 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 29 Sep 2023 17:16:20 +0300
Subject: [PATCH 10/11] Clean up typsig race ignoring

---
 src/domains/access.ml | 25 +++++++++----------------
 src/util/cilfacade.ml |  9 +++++++++
 2 files changed, 18 insertions(+), 16 deletions(-)

diff --git a/src/domains/access.ml b/src/domains/access.ml
index 832c6a762e..8907ccbc32 100644
--- a/src/domains/access.ml
+++ b/src/domains/access.ml
@@ -52,28 +52,25 @@ let rec is_ignorable_type_offset (t: typ) (o: _ Offset.t): bool =
   if is_ignorable_type t then
     true (* type at offset so far ignorable, no need to recurse *)
   else (
-    let blendAttributes baseAttrs = (* copied from Cilfacade.typeOffset *)
-      let (_, _, contageous) = partitionAttributes ~default:AttrName baseAttrs in
-      typeAddAttributes contageous
-    in
     match o with
     | `NoOffset -> false (* already checked t *)
     | `Index (_, o') ->
       begin match unrollType t with
         | TArray (et, _, attrs) ->
-          let t' = blendAttributes attrs et in
+          let t' = Cilfacade.typeBlendAttributes attrs et in
           is_ignorable_type_offset t' o'
         | _ -> false (* index on non-array *)
       end
     | `Field (f, o') ->
       begin match unrollType t with
         | TComp (_, attrs) ->
-          let t' = blendAttributes attrs f.ftype in
+          let t' = Cilfacade.typeBlendAttributes attrs f.ftype in
           is_ignorable_type_offset t' o'
         | _ -> false (* field on non-compound *)
       end
   )
 
+(** {!is_ignorable_type} for {!typsig}. *)
 let is_ignorable_typsig (ts: typsig): bool =
   (* efficient pattern matching first *)
   match ts with
@@ -82,29 +79,25 @@ let is_ignorable_typsig (ts: typsig): bool =
   | TSBase t -> is_ignorable_type t
   | _ -> is_ignorable_attrs (typeSigAttrs ts)
 
+(** {!is_ignorable_type_offset} for {!typsig}. *)
 let rec is_ignorable_typsig_offset (ts: typsig) (o: _ Offset.t): bool =
-  (* similar to Cilfacade.typeOffset but we want to check types at all intermediate offsets as well *)
   if is_ignorable_typsig ts then
     true (* type at offset so far ignorable, no need to recurse *)
   else (
-    let blendAttributes baseAttrs = (* copied from Cilfacade.typeOffset *)
-      let (_, _, contageous) = partitionAttributes ~default:AttrName baseAttrs in
-      typeSigAddAttrs contageous
-    in
     match o with
     | `NoOffset -> false (* already checked t *)
     | `Index (_, o') ->
       begin match ts with
-        | TSArray (et, _, attrs) ->
-          let t' = blendAttributes attrs et in
-          is_ignorable_typsig_offset t' o'
+        | TSArray (ets, _, attrs) ->
+          let ts' = Cilfacade.typeSigBlendAttributes attrs ets in
+          is_ignorable_typsig_offset ts' o'
         | _ -> false (* index on non-array *)
       end
     | `Field (f, o') ->
       begin match ts with
         | TSComp (_, _, attrs) ->
-          let t' = blendAttributes attrs (typeSig f.ftype) in
-          is_ignorable_typsig_offset t' o'
+          let t' = Cilfacade.typeBlendAttributes attrs f.ftype in
+          is_ignorable_type_offset t' o' (* switch to type because it is more precise with TNamed *)
         | _ -> false (* field on non-compound *)
       end
   )
diff --git a/src/util/cilfacade.ml b/src/util/cilfacade.ml
index eb7330aa19..6d55211c8d 100644
--- a/src/util/cilfacade.ml
+++ b/src/util/cilfacade.ml
@@ -322,6 +322,15 @@ and typeOffset basetyp =
     | t -> raise (TypeOfError (Field_NonCompound (fi, t)))
 
 
+let typeBlendAttributes baseAttrs = (* copied from Cilfacade.typeOffset *)
+  let (_, _, contageous) = partitionAttributes ~default:AttrName baseAttrs in
+  typeAddAttributes contageous
+
+let typeSigBlendAttributes baseAttrs =
+  let (_, _, contageous) = partitionAttributes ~default:AttrName baseAttrs in
+  typeSigAddAttrs contageous
+
+
 (** {!Cil.mkCast} using our {!typeOf}. *)
 let mkCast ~(e: exp) ~(newt: typ) =
   let oldt =

From 01ad122f7d6f0e345d40868a7ecfe253ce57a4a4 Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 29 Sep 2023 17:25:19 +0300
Subject: [PATCH 11/11] Change 05-lval_ls/23-race-null-type-deep to not use
 now-ignored FILE struct

---
 .../05-lval_ls/23-race-null-type-deep.c       | 28 +++++++++++--------
 1 file changed, 17 insertions(+), 11 deletions(-)

diff --git a/tests/regression/05-lval_ls/23-race-null-type-deep.c b/tests/regression/05-lval_ls/23-race-null-type-deep.c
index 6f29964d1e..f7de758d8f 100644
--- a/tests/regression/05-lval_ls/23-race-null-type-deep.c
+++ b/tests/regression/05-lval_ls/23-race-null-type-deep.c
@@ -1,9 +1,15 @@
+// PARAM: --disable sem.unknown_function.invalidate.globals --disable sem.unknown_function.spawn
 #include <pthread.h>
-#include <stdio.h>
+
+struct s {
+  int f;
+};
+
+extern void magic(struct s *p);
 
 void *t_fun(void *arg) {
   void *top;
-  fclose(top); // RACE
+  magic(top); // RACE
   return NULL;
 }
 
@@ -21,31 +27,31 @@ int main(void) {
   void *top;
   switch (r) {
     case 0:
-      feof(NULL); // NORACE
+      magic(NULL); // NORACE
       break;
     case 1:
-      feof(0); // NORACE
+      magic(0); // NORACE
       break;
     case 2:
-      feof(zero); // NORACE
+      magic(zero); // NORACE
       break;
     case 3:
-      feof(1); // RACE
+      magic(1); // RACE
       break;
     case 4:
-      feof(one); // RACE
+      magic(one); // RACE
       break;
     case 5:
-      feof(r); // RACE
+      magic(r); // RACE
       break;
     case 6:
-      feof(null); // NORACE
+      magic(null); // NORACE
       break;
     case 7:
-      feof(unknown); // RACE
+      magic(unknown); // RACE
       break;
     case 8:
-      feof(top); // RACE
+      magic(top); // RACE
       break;
     default:
       break;