Merge pull request #1323 from goblint/threadEscape-combine_assign

Implement `combine_assign` in `threadEscape`

Author: sim642

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 =

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

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
 

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

tests/regression/45-escape/09-id-local-in-global.c

@@ -0,0 +1,25 @@
+#include <pthread.h>
+#include <goblint.h>
+
+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;
+}