diff --git a/src/analyses/base.ml b/src/analyses/base.ml index c470bca026..fb2b5af517 100644 --- a/src/analyses/base.ml +++ b/src/analyses/base.ml @@ -6,6 +6,7 @@ open Pretty open Analyses open GobConfig open BaseUtil +open ReturnUtil module A = Analyses module H = Hashtbl module Q = Queries @@ -143,13 +144,6 @@ struct * Initializing my variables **************************************************************************) - let return_varstore = ref dummyFunDec.svar - let return_varinfo () = !return_varstore - let return_var () = AD.of_var (return_varinfo ()) - let return_lval (): lval = (Var (return_varinfo ()), NoOffset) - - let longjmp_return = ref dummyFunDec.svar - let heap_var on_stack ctx = let info = match (ctx.ask (Q.AllocVar {on_stack})) with | `Lifted vinfo -> vinfo @@ -2930,8 +2924,6 @@ end module type MainSpec = sig include MCPSpec include BaseDomain.ExpEvaluator - val return_lval: unit -> Cil.lval - val return_varinfo: unit -> Cil.varinfo end let main_module: (module MainSpec) Lazy.t = diff --git a/src/analyses/region.ml b/src/analyses/region.ml index 5b10586aba..a6ffa54ed6 100644 --- a/src/analyses/region.ml +++ b/src/analyses/region.ml @@ -109,8 +109,7 @@ struct let old_regpart = ctx.global () in let regpart, reg = match exp with | Some exp -> - let module BS = (val Base.get_main ()) in - Reg.assign (BS.return_lval ()) exp (old_regpart, reg) + Reg.assign (ReturnUtil.return_lval ()) exp (old_regpart, reg) | None -> (old_regpart, reg) in let regpart, reg = Reg.kill_vars locals (Reg.remove_vars locals (regpart, reg)) in @@ -143,12 +142,11 @@ struct match au with | `Lifted reg -> begin let old_regpart = ctx.global () in - let module BS = (val Base.get_main ()) in let regpart, reg = match lval with | None -> (old_regpart, reg) - | Some lval -> Reg.assign lval (AddrOf (BS.return_lval ())) (old_regpart, reg) + | Some lval -> Reg.assign lval (AddrOf (ReturnUtil.return_lval ())) (old_regpart, reg) in - let regpart, reg = Reg.remove_vars [BS.return_varinfo ()] (regpart, reg) in + let regpart, reg = Reg.remove_vars [ReturnUtil.return_varinfo ()] (regpart, reg) in if not (RegPart.leq regpart old_regpart) then ctx.sideg () regpart; `Lifted reg diff --git a/src/analyses/threadEscape.ml b/src/analyses/threadEscape.ml index 21a8b69c93..f5ff3dc50a 100644 --- a/src/analyses/threadEscape.ml +++ b/src/analyses/threadEscape.ml @@ -117,8 +117,7 @@ struct end | _ -> Queries.Result.top q - let escape_rval ctx (rval:exp) = - let ask = Analyses.ask_of_ctx ctx in + let escape_rval ctx ask (rval:exp) = let escaped = reachable ask rval in let escaped = D.filter (fun v -> not v.vglob) escaped in @@ -133,17 +132,26 @@ struct let ask = Analyses.ask_of_ctx ctx in let vs = mpt ask (AddrOf lval) in if D.exists (fun v -> v.vglob || has_escaped ask v) vs then ( - let escaped = escape_rval ctx rval in + let escaped = escape_rval ctx ask rval in D.join ctx.local escaped ) else begin ctx.local end + let combine_assign ctx (lval:lval option) (fexp:exp) f args fc au f_ask : D.t = + let ask = Analyses.ask_of_ctx ctx in + match lval with + | Some lval when D.exists (fun v -> v.vglob || has_escaped ask v) (mpt ask (AddrOf lval)) -> + let rval = Lval (ReturnUtil.return_lval ()) in + let escaped = escape_rval ctx f_ask rval in (* Using f_ask because the return value is only accessible in the context of that function at this point *) + D.join ctx.local escaped + | _ -> ctx.local + let special ctx (lval: lval option) (f:varinfo) (args:exp list) : D.t = let desc = LibraryFunctions.find f in match desc.special args, f.vname, args with | _, "pthread_setspecific" , [key; pt_value] -> - let escaped = escape_rval ctx pt_value in + let escaped = escape_rval ctx (Analyses.ask_of_ctx ctx) pt_value in D.join ctx.local escaped | _ -> ctx.local diff --git a/src/util/returnUtil.ml b/src/util/returnUtil.ml new file mode 100644 index 0000000000..a97f538970 --- /dev/null +++ b/src/util/returnUtil.ml @@ -0,0 +1,9 @@ +open GoblintCil +module AD = ValueDomain.AD + +let return_varstore = ref dummyFunDec.svar +let return_varinfo () = !return_varstore +let return_var () = AD.of_var (return_varinfo ()) +let return_lval (): lval = (Var (return_varinfo ()), NoOffset) + +let longjmp_return = ref dummyFunDec.svar \ No newline at end of file diff --git a/tests/regression/45-escape/09-id-local-in-global.c b/tests/regression/45-escape/09-id-local-in-global.c new file mode 100644 index 0000000000..aa5a12c012 --- /dev/null +++ b/tests/regression/45-escape/09-id-local-in-global.c @@ -0,0 +1,25 @@ +#include +#include + +int* gptr; + +void *foo(void* p){ + *gptr = 17; + return NULL; +} + +int* id(int* x) { + return x; +} + +int main(){ + int x = 0; + gptr = id(&x); + __goblint_check(x==0); + pthread_t thread; + pthread_create(&thread, NULL, foo, NULL); + sleep(3); + __goblint_check(x == 0); // UNKNOWN! + pthread_join(thread, NULL); + return 0; +}