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 *)