diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml index 08131eda40..eb82a28ac7 100644 --- a/src/analyses/threadEscape.ml +++ b/src/analyses/threadEscape.ml @@ -23,6 +23,36 @@ struct let name () = "escape" module D = EscapeDomain.EscapedVars module C = EscapeDomain.EscapedVars + module V = VarinfoV + module G = EscapeDomain.EscapedVars + + let rec cut_offset x = + match x with + | `NoOffset -> `NoOffset + | `Index (_,o) -> `NoOffset + | `Field (f,o) -> `Field (f, cut_offset o) + + let reachable (ask: Queries.ask) e: D.t = + match ask.f (Queries.ReachableFrom e) with + | a when not (Queries.LS.is_top a) -> + (* let to_extra (v,o) set = D.add (Addr.from_var_offset (v, cut_offset o)) set in *) + let to_extra (v,o) set = D.add v set in + Queries.LS.fold to_extra (Queries.LS.remove (dummyFunDec.svar, `NoOffset) a) (D.empty ()) + (* Ignore soundness warnings, as invalidation proper will raise them. *) + | a -> + if M.tracing then M.tracel "escape" "reachable %a: %a\n" d_exp e Queries.LS.pretty a; + D.empty () + + let mpt (ask: Queries.ask) e: D.t = + match ask.f (Queries.MayPointTo e) with + | a when not (Queries.LS.is_top a) -> + (* let to_extra (v,o) set = D.add (Addr.from_var_offset (v, cut_offset o)) set in *) + let to_extra (v,o) set = D.add v set in + Queries.LS.fold to_extra (Queries.LS.remove (dummyFunDec.svar, `NoOffset) a) (D.empty ()) + (* Ignore soundness warnings, as invalidation proper will raise them. *) + | a -> + if M.tracing then M.tracel "escape" "mpt %a: %a\n" d_exp e Queries.LS.pretty a; + D.empty () (* queries *) let query ctx (type a) (q: a Queries.t): a Queries.result = @@ -32,7 +62,21 @@ struct (* transfer functions *) let assign ctx (lval:lval) (rval:exp) : D.t = - ctx.local + let ask = Analyses.ask_of_ctx ctx in + let lvs = mpt ask (AddrOf lval) in + if M.tracing then M.tracel "escape" "assign lvs: %a\n" D.pretty lvs; + if D.exists (fun v -> v.vglob || has_escaped ask v) lvs then ( + let escaped = reachable ask rval in + if M.tracing then M.tracel "escape" "assign lvs: %a | %a\n" D.pretty lvs D.pretty escaped; + if not (D.is_empty escaped) && ThreadFlag.is_multi ask then (* avoid emitting unnecessary event *) + ctx.emit (Events.Escape escaped); + D.iter (fun lv -> + ctx.sideg lv escaped + ) lvs; + D.join ctx.local escaped + ) + else + ctx.local let branch ctx (exp:exp) (tv:bool) : D.t = ctx.local @@ -49,23 +93,6 @@ struct let combine ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) : D.t = au - let rec cut_offset x = - match x with - | `NoOffset -> `NoOffset - | `Index (_,o) -> `NoOffset - | `Field (f,o) -> `Field (f, cut_offset o) - - let reachable (ask: Queries.ask) e: D.t = - match ask.f (Queries.ReachableFrom e) with - | a when not (Queries.LS.is_top a) -> - (* let to_extra (v,o) set = D.add (Addr.from_var_offset (v, cut_offset o)) set in *) - let to_extra (v,o) set = D.add v set in - Queries.LS.fold to_extra (Queries.LS.remove (dummyFunDec.svar, `NoOffset) a) (D.empty ()) - (* Ignore soundness warnings, as invalidation proper will raise them. *) - | a -> - if M.tracing then M.tracel "escape" "reachable %a: %a\n" d_exp e Queries.LS.pretty a; - D.empty () - let special ctx (lval: lval option) (f:varinfo) (arglist:exp list) : D.t = ctx.local @@ -78,8 +105,9 @@ struct let escaped = reachable (Analyses.ask_of_ctx ctx) ptc_arg in if not (D.is_empty escaped) then (* avoid emitting unnecessary event *) ctx.emit (Events.Escape escaped); - [escaped] - | _ -> [D.bot ()] + let extra = D.fold (fun v acc -> D.join acc (ctx.global v)) escaped (D.empty ()) in (* TODO: must transitively join escapes of every ctx.global v as well? *) + [D.join ctx.local (D.join escaped extra)] + | _ -> [ctx.local] let threadspawn ctx lval f args fctx = D.join ctx.local @@ @@ -91,6 +119,15 @@ struct ctx.emit (Events.Escape escaped); escaped | _ -> D.bot () + + let event ctx e octx = + match e with + | Events.EnterMultiThreaded -> + let escaped = ctx.local in + if not (D.is_empty escaped) then (* avoid emitting unnecessary event *) + ctx.emit (Events.Escape escaped); + ctx.local + | _ -> ctx.local end let _ = diff --git a/tests/regression/45-escape/01-local-in-pthread.c b/tests/regression/45-escape/01-local-in-pthread.c new file mode 100644 index 0000000000..8157b55b3a --- /dev/null +++ b/tests/regression/45-escape/01-local-in-pthread.c @@ -0,0 +1,29 @@ +#include +#include + +#include +#include +#include + + +void *foo(void* p){ + sleep(2); + int* ip = *((int**) p); + printf("ip is %d\n", *ip); + *ip = 42; + return NULL; +} + +int main(){ + int x = 0; + int *xp = &x; + int** ptr = &xp; + int x2 = 35; + pthread_t thread; + pthread_create(&thread, NULL, foo, ptr); + *ptr = &x2; + sleep(4); // to make sure that we actually fail the assert when running. + assert(x2 == 35); // UNKNOWN! + pthread_join(thread, NULL); + return 0; +} diff --git a/tests/regression/45-escape/02-local-in-global.c b/tests/regression/45-escape/02-local-in-global.c new file mode 100644 index 0000000000..1c4632e484 --- /dev/null +++ b/tests/regression/45-escape/02-local-in-global.c @@ -0,0 +1,21 @@ +#include +#include + +int* gptr; + +void *foo(void* p){ + *gptr = 17; + return NULL; +} + +int main(){ + int x = 0; + gptr = &x; + assert(x==0); + pthread_t thread; + pthread_create(&thread, NULL, foo, NULL); + sleep(3); + assert(x == 0); // UNKNOWN! + pthread_join(thread, NULL); + return 0; +} diff --git a/tests/regression/45-escape/03-local-in-pthread-a.c b/tests/regression/45-escape/03-local-in-pthread-a.c new file mode 100644 index 0000000000..91cd7d2db1 --- /dev/null +++ b/tests/regression/45-escape/03-local-in-pthread-a.c @@ -0,0 +1,30 @@ +#include +#include + +#include +#include +#include + + +void *foo(void* p){ + sleep(2); + int* ip = *((int**) p); + printf("ip is %d\n", *ip); + // To check that in (01) even without modification both &x and &x2 are possible here + assert(*ip == 0); //UNKNOWN! + assert(*ip == 35); //UNKNOWN! + return NULL; +} + +int main(){ + int x = 0; + int *xp = &x; + int** ptr = &xp; + int x2 = 35; + pthread_t thread; + pthread_create(&thread, NULL, foo, ptr); + *ptr = &x2; + sleep(4); // to make sure that we actually fail the assert when running. + pthread_join(thread, NULL); + return 0; +} diff --git a/tests/regression/45-escape/04-imprecision.c b/tests/regression/45-escape/04-imprecision.c new file mode 100644 index 0000000000..50b0b90128 --- /dev/null +++ b/tests/regression/45-escape/04-imprecision.c @@ -0,0 +1,28 @@ +#include +#include + +int* gptr; + +void *foo(void* p){ + *gptr = 17; + return NULL; +} + +// The asserts about y would hold in the concrete, as y actually never escapes the current thread, but we are currently not precise enough to account for this + +int main(){ + int x = 0; + int y = 0; + gptr = &y; + gptr = &x; + assert(x==0); + pthread_t thread; + pthread_create(&thread, NULL, foo, NULL); + sleep(3); + assert(x == 0); // UNKNOWN! + assert(y == 0); //TODO + y = 5; + assert(y == 5); //TODO + pthread_join(thread, NULL); + return 0; +}