ThreadCreate analysis to improve partially context-sensitive threadID analysis

src/analyses/threadId.ml

@@ -32,24 +32,31 @@ struct
   module N = Lattice.Flat (VNI) (struct let bot_name = "unknown node" let top_name = "unknown node" end)
   module TD = Thread.D
 
-  module D = Lattice.Prod3 (N) (ThreadLifted) (TD)
+  (** Uniqueness Counter * TID * (All thread creates of current thread * All thread creates of the current function and its callees) *)
+  module D = Lattice.Prod3 (N) (ThreadLifted) (Lattice.Prod(TD)(TD))
   module C = D
   module P = IdentityP (D)
 
   let tids = ref (Hashtbl.create 20)
 
   let name () = "threadid"
 
-  let startstate v = (N.bot (), ThreadLifted.bot (), TD.bot ())
-  let exitstate  v = (N.bot (), `Lifted (Thread.threadinit v ~multiple:false), TD.bot ())
+  let context fd ((n,current,td) as d) =
+    if GobConfig.get_bool "ana.thread.context.create-edges" then
+      d
+    else
+      (n, current, (TD.bot (), TD.bot ()))
+
+  let startstate v = (N.bot (), ThreadLifted.bot (), (TD.bot (),TD.bot ()))
+  let exitstate  v = (N.bot (), `Lifted (Thread.threadinit v ~multiple:false), (TD.bot (), TD.bot ()))
 
   let morphstate v _ =
     let tid = Thread.threadinit v ~multiple:false in
     if GobConfig.get_bool "dbg.print_tids" then
       Hashtbl.replace !tids tid ();
-    (N.bot (), `Lifted (tid), TD.bot ())
+    (N.bot (), `Lifted (tid), (TD.bot (), TD.bot ()))
 
-  let create_tid (_, current, td) ((node, index): Node.t * int option) v =
+  let create_tid (_, current, (td, _)) ((node, index): Node.t * int option) v =
     match current with
     | `Lifted current ->
       let+ tid = Thread.threadenter (current, td) node index v in
@@ -62,7 +69,18 @@ struct
   let is_unique ctx =
     ctx.ask Queries.MustBeUniqueThread
 
-  let created (_, current, td) =
+  let enter ctx lval f args =
+    let (n, current, (td, _)) = ctx.local in
+    [ctx.local, (n, current, (td,TD.bot ()))]
+
+  let combine_env ctx lval fexp f args fc ((n,current,(_, au_ftd)) as au) f_ask =
+    let (_, _, (td, ftd)) = ctx.local in
+    if not (GobConfig.get_bool "ana.thread.context.create-edges") then
+      (n,current,(TD.join td au_ftd, TD.join ftd au_ftd))
+    else
+      au
+
+  let created (_, current, (td, _)) =
     match current with
     | `Lifted current -> BatOption.map_default (ConcDomain.ThreadSet.of_list) (ConcDomain.ThreadSet.top ()) (Thread.created current td)
     | _ -> ConcDomain.ThreadSet.top ()
@@ -115,15 +133,15 @@ struct
     | `Lifted node, count -> node, Some count
     | (`Bot | `Top), _ -> ctx.prev_node, None
 
-  let threadenter ctx lval f args =
+  let threadenter ctx lval f args:D.t list =
     let n, i = indexed_node_for_ctx ctx in
     let+ tid = create_tid ctx.local (n, i) f in
-    (`Lifted (f, n, i), tid, TD.bot ())
+    (`Lifted (f, n, i), tid, (TD.bot (), TD.bot ()))
 
   let threadspawn ctx lval f args fctx =
-    let (current_n, current, td) = ctx.local in
+    let (current_n, current, (td,tdl)) = ctx.local in
     let v, n, i = match fctx.local with `Lifted vni, _, _ -> vni | _ -> failwith "ThreadId.threadspawn" in
-    (current_n, current, Thread.threadspawn td n i v)
+    (current_n, current, (Thread.threadspawn td n i v, Thread.threadspawn tdl n i v))
 
   type marshal = (Thread.t,unit) Hashtbl.t (* TODO: don't use polymorphic Hashtbl *)
   let init (m:marshal option): unit =

src/util/options.schema.json

@@ -989,6 +989,19 @@
               "description": "Number of unique thread IDs allocated for each pthread_create node.",
               "type": "integer",
               "default": 0
+            },
+            "context": {
+              "title": "ana.thread.context",
+              "type": "object",
+              "properties": {
+                "create-edges": {
+                  "title": "ana.thread.context.create-edges",
+                  "description": "threadID analysis: Encountered create edges in context.",
+                  "type": "boolean",
+                  "default": true
+                }
+              },
+              "additionalProperties": false
             }
           },
           "additionalProperties": false

tests/regression/40-threadid/05-nc-simple.c

@@ -0,0 +1,32 @@
+// PARAM: --disable ana.thread.context.create-edges
+#include <goblint.h>
+#include <pthread.h>
+
+int glob;
+
+void *t_FST(void *arg) {
+}
+
+void *t_SND(void *arg) {
+  glob = 1; //NORACE
+}
+
+int nothing () {
+}
+
+
+int main() {
+
+  pthread_t id;
+  pthread_create(&id, NULL, t_FST, NULL);
+
+  nothing();
+
+  glob = 2; //NORACE
+
+  pthread_t id;
+  pthread_create(&id, NULL, t_SND, NULL);
+
+  nothing();
+
+}

tests/regression/40-threadid/06-nc-deep.c

@@ -0,0 +1,76 @@
+// PARAM: --disable ana.thread.context.create-edges
+#include <goblint.h>
+#include <pthread.h>
+
+int glob_noCreate;
+int glob_create;
+
+void *t_INIT(void *arg) {
+}
+
+void *t_noCreate(void *arg) {
+  glob_noCreate =1; //NORACE
+}
+
+void *t_create(void *arg) {
+  glob_create =1; //RACE
+}
+
+void noCreate1 () {
+  noCreate2();
+}
+void noCreate2 () {
+  noCreate3();
+}
+void noCreate3 () {
+  noCreate4();
+}
+void noCreate4 () {
+  noCreate5();
+}
+void noCreate5 () {
+}
+
+void create1 () {
+  create2();
+}
+void create2 () {
+  create3();
+}
+void create3 () {
+  create4();
+}
+void create4 () {
+  create5();
+}
+void create5 () {
+  pthread_t id;
+  pthread_create(&id, NULL, t_create, NULL);
+}
+
+int main() {
+
+  pthread_t id;
+  pthread_create(&id, NULL, t_INIT, NULL);
+
+  //no create
+  noCreate1();
+
+  glob_noCreate = 2; //NORACE
+
+  pthread_t id;
+  pthread_create(&id, NULL, t_noCreate, NULL);
+
+  noCreate1();
+
+  //create
+  create1();
+
+  glob_create = 2; //RACE
+
+  pthread_t id;
+  pthread_create(&id, NULL, t_create, NULL);
+
+  create1();
+
+}

tests/regression/40-threadid/07-nc-createEdges.c

@@ -0,0 +1,37 @@
+// PARAM: --disable ana.thread.context.create-edges
+#include <goblint.h>
+#include <pthread.h>
+
+int glob;
+
+void *t_init(void *arg) {
+}
+
+void *t_norace(void *arg) {
+  glob = 1; //NORACE
+}
+
+void *t_other(void *arg) {
+}
+
+int create_other () {
+  pthread_t id;
+  pthread_create(&id, NULL, t_other, NULL);
+}
+
+
+int main() {
+  //enter multithreaded mode
+  pthread_t id;
+  pthread_create(&id, NULL, t_init, NULL);
+
+  create_other();
+
+  glob = 2; //NORACE
+
+  pthread_t id;
+  pthread_create(&id, NULL, t_norace, NULL);
+
+  create_other();
+
+}

tests/regression/40-threadid/08-nc-fromThread.c

@@ -0,0 +1,35 @@
+// PARAM: --disable ana.thread.context.create-edges
+#include <goblint.h>
+#include <pthread.h>
+
+int glob;
+
+void *t_norace(void *arg) {
+  glob = 1; //NORACE
+}
+
+void *t_other(void *arg) {
+}
+
+int create_other () {
+  pthread_t id;
+  pthread_create(&id, NULL, t_other, NULL);
+}
+
+void *t_fun(void *arg) {
+  create_other();
+
+  glob = 2; //NORACE
+
+  pthread_t id;
+  pthread_create(&id, NULL, t_norace, NULL);
+
+  create_other();
+}
+
+int main() {
+  pthread_t id;
+  pthread_create(&id, NULL, t_fun, NULL);
+
+  create_other();
+}