diff --git a/src/analyses/accessAnalysis.ml b/src/analyses/accessAnalysis.ml index fc178d43cb..023635051f 100644 --- a/src/analyses/accessAnalysis.ml +++ b/src/analyses/accessAnalysis.ml @@ -35,6 +35,12 @@ struct unsafe := 0 let side_access ctx ty lv_opt (conf, w, loc, e, a) = + let ty = + if Option.is_some lv_opt then + `Type Cil.voidType (* avoid unsound type split for alloc variables *) + else + ty + in let d = if !GU.should_warn then Access.AS.singleton (conf, w, loc, e, a) @@ -172,8 +178,14 @@ struct | Some fnc -> (fnc act arglist) | _ -> arglist in - List.iter (access_one_top ctx false true) (arg_acc `Read); - List.iter (access_one_top ctx true true ) (arg_acc `Write); + (* TODO: per-argument reach *) + let reach = + match f.vname with + | "memset" | "__builtin_memset" -> false + | _ -> true + in + List.iter (access_one_top ctx false reach) (arg_acc `Read); + List.iter (access_one_top ctx true reach) (arg_acc `Write); (match lv with | Some x -> access_one_top ctx true false (AddrOf x) | None -> ()); diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 29ff8375fa..e1118516ef 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -2112,6 +2112,25 @@ struct let st: store = ctx.local in let gs = ctx.global in match LF.classify f.vname args with + | `Unknown ("memset" | "__builtin_memset") -> + begin match args with + | [dest; ch; count] -> + (* TODO: check count *) + let eval_ch = eval_rv (Analyses.ask_of_ctx ctx) gs st ch in + let dest_lval = mkMem ~addr:(Cil.stripCasts dest) ~off:NoOffset in + let dest_a = eval_lv (Analyses.ask_of_ctx ctx) gs st dest_lval in + (* let dest_typ = Cilfacade.typeOfLval dest_lval in *) + let dest_typ = AD.get_type dest_a in (* TODO: what is the right way? *) + let value = + match eval_ch with + | `Int i when ID.to_int i = Some Z.zero -> + VD.zero_init_value dest_typ + | _ -> + VD.top_value dest_typ + in + set ~ctx:(Some ctx) (Analyses.ask_of_ctx ctx) gs st dest_a dest_typ value + | _ -> failwith "strange memset arguments" + end | `Unknown "F59" (* strcpy *) | `Unknown "F60" (* strncpy *) | `Unknown "F63" (* memcpy *) diff --git a/src/analyses/libraryFunctions.ml b/src/analyses/libraryFunctions.ml index 3bf7bbc277..9d54020181 100644 --- a/src/analyses/libraryFunctions.ml +++ b/src/analyses/libraryFunctions.ml @@ -207,8 +207,8 @@ let invalidate_actions = [ "mempcpy", writes [1];(*keep [1]*) "__builtin___memcpy_chk", writes [1]; "__builtin___mempcpy_chk", writes [1]; - "memset", writesAll;(*unsafe*) - "__builtin_memset", writesAll;(*unsafe*) + "memset", writes [1];(*unsafe*) + "__builtin_memset", writes [1];(*unsafe*) "__builtin___memset_chk", writesAll; "printf", readsAll;(*safe*) "__printf_chk", readsAll;(*safe*) diff --git a/tests/regression/02-base/75-memset.c b/tests/regression/02-base/75-memset.c new file mode 100644 index 0000000000..a143a77833 --- /dev/null +++ b/tests/regression/02-base/75-memset.c @@ -0,0 +1,27 @@ +#include +#include + +struct s { + int x; + int *p; +}; + +int main() { + int x; + memset(&x, 0, sizeof(int)); + assert(x == 0); + memset(&x, x, sizeof(int)); + assert(x == 0); + memset(&x, 1, sizeof(int)); + assert(x == 0); // UNKNOWN + + int *p; + memset(&p, 0, sizeof(int*)); + assert(p == NULL); + + struct s s; + memset(&s, 0, sizeof(struct s)); + assert(s.x == 0); + assert(s.p == NULL); + return 0; +} \ No newline at end of file diff --git a/tests/regression/04-mutex/70-memset_indirect_nr.c b/tests/regression/04-mutex/70-memset_indirect_nr.c new file mode 100644 index 0000000000..77d0a5cb55 --- /dev/null +++ b/tests/regression/04-mutex/70-memset_indirect_nr.c @@ -0,0 +1,30 @@ +#include +#include +#include + +int g; + +struct s { + int *p; +} s = {&g}; + +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; + +void *t_fun(void *arg) { + int *p; + pthread_mutex_lock(&mutex); + p = s.p; // NORACE + pthread_mutex_unlock(&mutex); + (*p)++; // NORACE + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + pthread_mutex_lock(&mutex); + memset(&s, 0, sizeof(s)); // NORACE + pthread_mutex_unlock(&mutex); + pthread_join (id, NULL); + return 0; +} diff --git a/tests/regression/04-mutex/71-memset_direct_rc.c b/tests/regression/04-mutex/71-memset_direct_rc.c new file mode 100644 index 0000000000..367d7fde93 --- /dev/null +++ b/tests/regression/04-mutex/71-memset_direct_rc.c @@ -0,0 +1,20 @@ +#include +#include +#include + +int g; + +pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; + +void *t_fun(void *arg) { + g++; // RACE! + return NULL; +} + +int main(void) { + pthread_t id; + pthread_create(&id, NULL, t_fun, NULL); + memset(&g, 0, sizeof(int)); // RACE! + pthread_join (id, NULL); + return 0; +} diff --git a/tests/regression/06-symbeq/31-zstd-thread-pool.c b/tests/regression/06-symbeq/31-zstd-thread-pool.c index 5a20d03657..290a8a349d 100644 --- a/tests/regression/06-symbeq/31-zstd-thread-pool.c +++ b/tests/regression/06-symbeq/31-zstd-thread-pool.c @@ -158,7 +158,7 @@ static void* POOL_thread(void* opaque) { ZSTD_pthread_cond_wait(&ctx->queuePopCond, &ctx->queueMutex); } /* Pop a job off the queue */ - { POOL_job const job = ctx->queue[ctx->queueHead]; //NORACE + { POOL_job const job = ctx->queue[ctx->queueHead]; // TODO NORACE ctx->queueHead = (ctx->queueHead + 1) % ctx->queueSize; //NORACE ctx->numThreadsBusy++; //NORACE ctx->queueEmpty = (ctx->queueHead == ctx->queueTail); //NORACE diff --git a/tests/regression/06-symbeq/35-zstd-thread-pool-multi.c b/tests/regression/06-symbeq/35-zstd-thread-pool-multi.c index ff2abd7816..83d869a242 100644 --- a/tests/regression/06-symbeq/35-zstd-thread-pool-multi.c +++ b/tests/regression/06-symbeq/35-zstd-thread-pool-multi.c @@ -158,7 +158,7 @@ static void* POOL_thread(void* opaque) { ZSTD_pthread_cond_wait(&ctx->queuePopCond, &ctx->queueMutex); } /* Pop a job off the queue */ - { POOL_job const job = ctx->queue[ctx->queueHead]; //NORACE + { POOL_job const job = ctx->queue[ctx->queueHead]; // TODO NORACE ctx->queueHead = (ctx->queueHead + 1) % ctx->queueSize; //NORACE ctx->numThreadsBusy++; //NORACE ctx->queueEmpty = (ctx->queueHead == ctx->queueTail); //NORACE