From ec1efbf15a4844caede88271a56d8785c606bd09 Mon Sep 17 00:00:00 2001 From: Michael Schwarz Date: Wed, 20 Sep 2023 19:32:02 +0200 Subject: [PATCH] First steps --- src/analyses/base.ml | 13 +++++++--- src/cdomains/concDomain.ml | 1 + src/cdomains/valueDomain.ml | 6 ++--- tests/regression/40-threadid/09-poc.c | 36 +++++++++++++++++++++++++++ 4 files changed, 49 insertions(+), 7 deletions(-) create mode 100644 tests/regression/40-threadid/09-poc.c diff --git a/src/analyses/base.ml b/src/analyses/base.ml index 71e2661997..e0887adbf6 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -1276,7 +1276,7 @@ struct let v = eval_rv (Analyses.ask_of_ctx ctx) ctx.global ctx.local e in (* ignore (Pretty.eprintf "evalthread %a (%a): %a" d_exp e d_plainexp e VD.pretty v); *) match v with - | Thread a -> a + | Thread a -> snd a | Bot -> Queries.Result.bot q (* TODO: remove *) | _ -> Queries.Result.top q end @@ -2251,9 +2251,14 @@ struct | Address ret_a -> begin match eval_rv (Analyses.ask_of_ctx ctx) gs st id with | Thread a -> - let v = List.fold VD.join (VD.bot ()) (List.map (fun x -> G.thread (ctx.global (V.thread x))) (ValueDomain.Threads.elements a)) in + let v = List.fold VD.join (VD.bot ()) (List.map (fun x -> G.thread (ctx.global (V.thread x))) (ConcDomain.ThreadSet.elements (snd a))) in (* TODO: is this type right? *) - set ~ctx (Analyses.ask_of_ctx ctx) gs st ret_a (Cilfacade.typeOf ret_var) v + let res = set ~ctx (Analyses.ask_of_ctx ctx) gs st ret_a (Cilfacade.typeOf ret_var) v in + (match ConcDomain.ThreadSet.elements (snd a), id with + | _::_, Lval l -> + let lv = eval_lv (Analyses.ask_of_ctx ctx) gs st l in + set ~ctx (Analyses.ask_of_ctx ctx) gs res lv (Cilfacade.typeOf id) (Thread (true, snd a)) + | _ -> res) | _ -> invalidate ~ctx (Analyses.ask_of_ctx ctx) gs st [ret_var] end | _ -> invalidate ~ctx (Analyses.ask_of_ctx ctx) gs st [ret_var] @@ -2677,7 +2682,7 @@ struct Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) (priv_getg ctx.global) (priv_sideg ctx.sideg) st | Events.AssignSpawnedThread (lval, tid) -> (* TODO: is this type right? *) - set ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local (eval_lv (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval) (Cilfacade.typeOfLval lval) (Thread (ValueDomain.Threads.singleton tid)) + set ~ctx (Analyses.ask_of_ctx ctx) ctx.global ctx.local (eval_lv (Analyses.ask_of_ctx ctx) ctx.global ctx.local lval) (Cilfacade.typeOfLval lval) (Thread (false, ConcDomain.ThreadSet.singleton tid)) | Events.Assert exp -> assert_fn ctx exp true | Events.Unassume {exp; uuids} -> diff --git a/src/cdomains/concDomain.ml b/src/cdomains/concDomain.ml index b16cdf1d9f..c93fc0507e 100644 --- a/src/cdomains/concDomain.ml +++ b/src/cdomains/concDomain.ml @@ -2,6 +2,7 @@ module ThreadSet = SetDomain.ToppedSet (ThreadIdDomain.Thread) (struct let topname = "All Threads" end) module MustThreadSet = SetDomain.Reverse(ThreadSet) +module ThreadSetMustJoined = Lattice.Prod (BoolDomain.MustBool) (ThreadSet) module CreatedThreadSet = ThreadSet diff --git a/src/cdomains/valueDomain.ml b/src/cdomains/valueDomain.ml index 9d894b6b34..29d46f32e8 100644 --- a/src/cdomains/valueDomain.ml +++ b/src/cdomains/valueDomain.ml @@ -73,7 +73,7 @@ struct let invalidate_value ask t (v, s, o) = Value.invalidate_value ask t v, s, o end -module Threads = ConcDomain.ThreadSet +module Threads = ConcDomain.ThreadSetMustJoined module JmpBufs = JmpBufDomain.JmpBufSetTaint module rec Compound: sig @@ -146,7 +146,7 @@ struct let typAttr = typeAttrs ai in let len = array_length_idx (IndexDomain.bot ()) length in Array (CArrays.make ~varAttr ~typAttr len (bot_value ai)) - | t when is_thread_type t -> Thread (ConcDomain.ThreadSet.empty ()) + | t when is_thread_type t -> Thread (true, ConcDomain.ThreadSet.empty ()) | t when is_mutexattr_type t -> MutexAttr (MutexAttrDomain.bot ()) | t when is_jmp_buf_type t -> JmpBuf (JmpBufs.Bufs.empty (), false) | TNamed ({ttype=t; _}, _) -> bot_value ~varAttr (unrollType t) @@ -958,7 +958,7 @@ struct | Thread t -> value (* if actually assigning thread, use value *) | _ -> if !AnalysisState.global_initialization then - Thread (ConcDomain.ThreadSet.empty ()) (* if assigning global init (int on linux, ptr to struct on mac), use empty set instead *) + Thread (true, ConcDomain.ThreadSet.empty ()) (* if assigning global init (int on linux, ptr to struct on mac), use empty set instead *) else Top end diff --git a/tests/regression/40-threadid/09-poc.c b/tests/regression/40-threadid/09-poc.c new file mode 100644 index 0000000000..ac0fec7490 --- /dev/null +++ b/tests/regression/40-threadid/09-poc.c @@ -0,0 +1,36 @@ +// PARAM: --set ana.base.arrays.domain partitioned --enable ana.int.interval +#include +#include + + +void *t_fun(void *arg) { + return 5; +} + +int main() { + pthread_t idtmp; + pthread_t id[10]; + int x; + + pthread_create(&id[0], NULL, t_fun, NULL); + x = 8; + + for(int i =0; i < 10; i++) { + pthread_create(&idtmp, NULL, t_fun, NULL); + id[i] = idtmp; + } + + x = 2; + + for(int i =0; i < 10; i++) { + // Pulled into temporary assignment, as set in pthread_join does not provide needed information to + // partitioned arrays + idtmp = id[i]; + pthread_join(idtmp, &x); //Providing a pointer to x to go into the code that handles it + id[i] = idtmp; + } + + // We know all threads who have their tids in the array id have been joined + // Only additional thing that is needed is proof that the array contains all thread ids that have been created + // e.g. by all distinct +}