Improve memset analysis

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 -> ());

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

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

tests/regression/02-base/75-memset.c

@@ -0,0 +1,27 @@
+#include <string.h>
+#include <assert.h>
+
+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;
+}

tests/regression/04-mutex/70-memset_indirect_nr.c

@@ -0,0 +1,30 @@
+#include <pthread.h>
+#include <stdio.h>
+#include <string.h>
+
+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;
+}

tests/regression/04-mutex/71-memset_direct_rc.c

@@ -0,0 +1,20 @@
+#include <pthread.h>
+#include <stdio.h>
+#include <string.h>
+
+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;
+}

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

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