Handle thread escaping via global and after thread creation

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 _ =

tests/regression/45-escape/01-local-in-pthread.c

@@ -0,0 +1,29 @@
+#include <pthread.h>
+#include <assert.h>
+
+#include <pthread.h>
+#include <stdio.h>
+#include <unistd.h>
+
+
+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;
+}

tests/regression/45-escape/02-local-in-global.c

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

tests/regression/45-escape/03-local-in-pthread-a.c

@@ -0,0 +1,30 @@
+#include <pthread.h>
+#include <assert.h>
+
+#include <pthread.h>
+#include <stdio.h>
+#include <unistd.h>
+
+
+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;
+}

tests/regression/45-escape/04-imprecision.c

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