Document refactored race ignore check

src/domains/access.ml

@@ -11,20 +11,21 @@ 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
   | 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 *)
       | (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 *)