diff --git a/src/analyses/threadId.ml b/src/analyses/threadId.ml index ff47cf10b8..4acf88a7ef 100644 --- a/src/analyses/threadId.ml +++ b/src/analyses/threadId.ml @@ -32,7 +32,8 @@ 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) @@ -40,16 +41,22 @@ struct 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 = diff --git a/src/util/options.schema.json b/src/util/options.schema.json index 02fc929a8a..f905ec0e1e 100644 --- a/src/util/options.schema.json +++ b/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 diff --git a/tests/regression/40-threadid/05-nc-simple.c b/tests/regression/40-threadid/05-nc-simple.c new file mode 100644 index 0000000000..a5c198097c --- /dev/null +++ b/tests/regression/40-threadid/05-nc-simple.c @@ -0,0 +1,32 @@ +// PARAM: --disable ana.thread.context.create-edges +#include +#include + +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(); + +} diff --git a/tests/regression/40-threadid/06-nc-deep.c b/tests/regression/40-threadid/06-nc-deep.c new file mode 100644 index 0000000000..6578bb355b --- /dev/null +++ b/tests/regression/40-threadid/06-nc-deep.c @@ -0,0 +1,76 @@ +// PARAM: --disable ana.thread.context.create-edges +#include +#include + +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(); + +} diff --git a/tests/regression/40-threadid/07-nc-createEdges.c b/tests/regression/40-threadid/07-nc-createEdges.c new file mode 100644 index 0000000000..2d11e13fc1 --- /dev/null +++ b/tests/regression/40-threadid/07-nc-createEdges.c @@ -0,0 +1,37 @@ +// PARAM: --disable ana.thread.context.create-edges +#include +#include + +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(); + +} diff --git a/tests/regression/40-threadid/08-nc-fromThread.c b/tests/regression/40-threadid/08-nc-fromThread.c new file mode 100644 index 0000000000..4fd37b6f87 --- /dev/null +++ b/tests/regression/40-threadid/08-nc-fromThread.c @@ -0,0 +1,35 @@ +// PARAM: --disable ana.thread.context.create-edges +#include +#include + +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(); +}