Merge pull request #1082 from goblint/thread-unsafe-funs

Detect calls of thread-unsafe functions as races

src/analyses/libraryFunctions.ml

@@ -84,7 +84,7 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("getchar", unknown []);
     ("putchar", unknown [drop "ch" []]);
     ("puts", unknown [drop "s" [r]]);
-    ("rand", unknown ~attrs:[ThreadUnsafe] []);
+    ("rand", special ~attrs:[ThreadUnsafe] [] Rand);
     ("strerror", unknown ~attrs:[ThreadUnsafe] [drop "errnum" []]);
     ("strspn", unknown [drop "s" [r]; drop "accept" [r]]);
     ("strcspn", unknown [drop "s" [r]; drop "accept" [r]]);
@@ -118,7 +118,6 @@ let c_descs_list: (string * LibraryDesc.t) list = LibraryDsl.[
     ("_setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env }); (* only has one underscore *)
     ("setjmp", special [__ "env" [w]] @@ fun env -> Setjmp { env });
     ("longjmp", special [__ "env" [r]; __ "value" []] @@ fun env value -> Longjmp { env; value });
-    ("rand", special [] Rand);
   ]
 
 (** C POSIX library functions.
@@ -890,70 +889,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
@@ -1165,6 +1164,8 @@ 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 when get_bool "sem.unknown_function.call.args" -> args
+    | Call -> []
     | Spawn when get_bool "sem.unknown_function.spawn" -> args
     | Spawn -> []
   in

src/analyses/mutexAnalysis.ml

@@ -306,6 +306,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

@@ -105,7 +105,7 @@ struct
       let g: V.t = Obj.obj g in
       begin match g with
         | `Left g' -> (* accesses *)
-          (* ignore (Pretty.printf "WarnGlobal %a\n" CilType.Varinfo.pretty g); *)
+          (* ignore (Pretty.printf "WarnGlobal %a\n" Access.MemoRoot.pretty g'); *)
           let trie = G.access (ctx.global g) in
           (** Distribute access to contained fields. *)
           let rec distribute_inner offset (accs, children) ancestor_accs =
@@ -193,6 +193,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 (conf, Call, loc, e, a) ((`Var f), `NoOffset) ;
+    );
+    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 (

src/util/options.schema.json

@@ -1317,6 +1317,13 @@
               "type": "boolean",
               "default": true
             },
+            "call": {
+              "title": "sem.unknown_function.call",
+              "description":
+                "Unknown function call calls reachable functions",
+              "type": "boolean",
+              "default": true
+            },
             "invalidate": {
               "title": "sem.unknown_function.invalidate",
               "type": "object",

tests/regression/04-mutex/90-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/91-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;
+}