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"} ] diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index fda08a09dd..102459e572 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -127,6 +127,12 @@ 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" []]); + ("atomic_load", unknown [drop "obj" [r]]); + ("atomic_store", unknown [drop "obj" [w]; drop "desired" []]); ] (** C POSIX library functions. @@ -434,7 +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]]); diff --git a/src/domains/access.ml b/src/domains/access.ml index fa6446df16..8907ccbc32 100644 --- a/src/domains/access.ml +++ b/src/domains/access.ml @@ -10,28 +10,105 @@ 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 = - 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 - | 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 end - | TComp ({ cname = "lock_class_key"; _ }, _) -> true - | TInt (IInt, attr) when hasAttribute "mutex" attr -> true - | t when hasAttribute "atomic" (typeAttrs t) -> true (* C11 _Atomic *) + | "lock_class_key" -> true (* kernel? *) | _ -> false -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_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 + | _ -> + if is_ignorable_attrs (typeAttrsOuter t) then (* only outer because we unroll TNamed ourselves *) + 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 (* type at offset so far ignorable, no need to recurse *) + else ( + match o with + | `NoOffset -> false (* already checked t *) + | `Index (_, o') -> + begin match unrollType t with + | TArray (et, _, attrs) -> + 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' = 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 + | TSComp (_, cname, _) when is_ignorable_comp_name cname -> true + | TSFun _ -> true + | 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 = + if is_ignorable_typsig ts then + true (* type at offset so far ignorable, no need to recurse *) + else ( + match o with + | `NoOffset -> false (* already checked t *) + | `Index (_, o') -> + begin match ts with + | 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' = 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 + ) + +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 ts, o) -> is_ignorable_typsig_offset ts o + | (`Var v, o) -> is_ignorable_mval (v, o) module TSH = Hashtbl.Make (CilType.Typsig) @@ -195,8 +272,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 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 = 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 -#include #include -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 -#include -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 +} 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 -#include + +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;