Detect calls of thread-unsafe functions as races

src/analyses/libraryFunctions.ml

@@ -797,70 +797,70 @@ struct
 
   let writesAllButFirst n f a x =
     match a with
-    | Write | Spawn -> f a x @ drop n x
+    | Write | Call | Spawn -> f a x @ drop n x
     | Read  -> f a x
     | Free  -> []
 
   let readsAllButFirst n f a x =
     match a with
-    | Write | Spawn -> f a x
+    | Write | Call | Spawn -> f a x
     | Read  -> f a x @ drop n x
     | Free  -> []
 
   let reads ns a x =
     let i, o = partition ns x in
     match a with
-    | Write | Spawn -> o
+    | Write | Call | Spawn -> o
     | Read  -> i
     | Free  -> []
 
   let writes ns a x =
     let i, o = partition ns x in
     match a with
-    | Write | Spawn -> i
+    | Write | Call | Spawn -> i
     | Read  -> o
     | Free  -> []
 
   let frees ns a x =
     let i, o = partition ns x in
     match a with
-    | Write | Spawn -> []
+    | Write | Call | Spawn -> []
     | Read  -> o
     | Free  -> i
 
   let readsFrees rs fs a x =
     match a with
-    | Write | Spawn -> []
+    | Write | Call | Spawn -> []
     | Read  -> keep rs x
     | Free  -> keep fs x
 
   let onlyReads ns a x =
     match a with
-    | Write | Spawn -> []
+    | Write | Call | Spawn -> []
     | Read  -> keep ns x
     | Free  -> []
 
   let onlyWrites ns a x =
     match a with
-    | Write | Spawn -> keep ns x
+    | Write | Call | Spawn -> keep ns x
     | Read  -> []
     | Free  -> []
 
   let readsWrites rs ws a x =
     match a with
-    | Write | Spawn -> keep ws x
+    | Write | Call | Spawn -> keep ws x
     | Read  -> keep rs x
     | Free  -> []
 
   let readsAll a x =
     match a with
-    | Write | Spawn -> []
+    | Write | Call | Spawn -> []
     | Read  -> x
     | Free  -> []
 
   let writesAll a x =
     match a with
-    | Write | Spawn -> x
+    | Write | Call | Spawn -> x
     | Read  -> []
     | Free  -> []
 end
@@ -1158,6 +1158,7 @@ let unknown_desc ~f name = (* TODO: remove name argument, unknown function shoul
     | Read when GobConfig.get_bool "sem.unknown_function.read.args" -> args
     | Read -> []
     | Free -> []
+    | Call -> [] (* TODO: option *)
     | Spawn when get_bool "sem.unknown_function.spawn" -> args
     | Spawn -> []
   in

src/analyses/mutexAnalysis.ml

@@ -254,6 +254,7 @@ struct
             let write = match kind with
               | Write | Free -> true
               | Read -> false
+              | Call
               | Spawn -> false (* TODO: nonsense? *)
             in
             let s = GProtecting.make ~write ~recovered:is_recovered_to_st locks in

src/analyses/raceAnalysis.ml

@@ -153,6 +153,19 @@ struct
     | _ ->
       ctx.local
 
+  let special ctx (lvalOpt: lval option) (f:varinfo) (arglist:exp list) : D.t =
+    (* perform shallow and deep invalidate according to Library descriptors *)
+    let desc = LibraryFunctions.find f in
+    if List.mem LibraryDesc.ThreadUnsafe desc.attrs then (
+      let e = Lval (Var f, NoOffset) in
+      let conf = 110 in
+      let loc = Option.get !Node.current_node in
+      let vo = Some f in
+      let a = Obj.obj (ctx.ask (PartAccess (Memory {exp=e; var_opt=vo; kind=Call}))) in
+      side_access ctx (`Type f.vtype) (Some (f, `NoOffset)) (conf, Call, loc, e, a);
+    );
+    ctx.local
+
   let finalize () =
     let total = !safe + !unsafe + !vulnerable in
     if total > 0 then (

src/domains/accessKind.ml

@@ -1,9 +1,10 @@
 (** Kinds of memory accesses. *)
 
 type t =
-  | Write  (** argument may be read or written to *)
+  | Write  (** argument may be written to *)
   | Read   (** argument may be read *)
   | Free   (** argument may be freed *)
+  | Call   (** argument may be called *)
   | Spawn  (** argument may be spawned *)
 [@@deriving eq, ord, hash]
 (** Specifies what is known about an argument. *)
@@ -12,6 +13,7 @@ let show: t -> string = function
   | Write -> "write"
   | Read -> "read"
   | Free -> "free"
+  | Call -> "call"
   | Spawn -> "spawn"
 
 include Printable.SimpleShow (

tests/regression/04-mutex/77-thread-unsafe_fun_rc.c

@@ -0,0 +1,22 @@
+#include <pthread.h>
+#include <stdio.h>
+
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+pthread_mutex_t mutex2 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  rand(); // RACE!
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  pthread_mutex_lock(&mutex2);
+  rand(); // RACE!
+  pthread_mutex_unlock(&mutex2);
+  pthread_join (id, NULL);
+  return 0;
+}

tests/regression/04-mutex/78-thread-unsafe_fun_nr.c

@@ -0,0 +1,21 @@
+#include <pthread.h>
+#include <stdio.h>
+
+pthread_mutex_t mutex1 = PTHREAD_MUTEX_INITIALIZER;
+
+void *t_fun(void *arg) {
+  pthread_mutex_lock(&mutex1);
+  rand(); // NORACE
+  pthread_mutex_unlock(&mutex1);
+  return NULL;
+}
+
+int main(void) {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+  pthread_mutex_lock(&mutex1);
+  rand(); // NORACE
+  pthread_mutex_unlock(&mutex1);
+  pthread_join (id, NULL);
+  return 0;
+}