ThreadEscape: Collect set of escaping threads flow-insensitively

src/analyses/threadEscape.ml

@@ -16,11 +16,13 @@ module Spec =
 struct
   include Analyses.IdentitySpec
 
+  module ThreadIdSet = SetDomain.Make (ThreadIdDomain.ThreadLifted)
+
   let name () = "escape"
   module D = EscapeDomain.EscapedVars
   module C = EscapeDomain.EscapedVars
   module V = VarinfoV
-  module G = EscapeDomain.EscapedVars
+  module G = ThreadIdSet
 
   let reachable (ask: Queries.ask) e: D.t =
     match ask.f (Queries.ReachableFrom e) with
@@ -42,41 +44,96 @@ struct
       if M.tracing then M.tracel "escape" "mpt %a: %a\n" d_exp e Queries.LS.pretty a;
       D.empty ()
 
+  let thread_id ctx =
+    ctx.ask Queries.CurrentThreadId
+
+  (** Emit an escape event:
+      Only necessary when code has ever been multithreaded,
+      or when about to go multithreaded. *)
+  let emit_escape_event ctx escaped =
+    (* avoid emitting unnecessary event *)
+    if not (D.is_empty escaped) then
+      ctx.emit (Events.Escape escaped)
+
+  (** Side effect escapes: In contrast to the emitting the event, side-effecting is
+      necessary in single threaded mode, since we rely on escape status in Base
+      for passing locals reachable via globals *)
+  let side_effect_escape ctx escaped threadid =
+    let threadid = G.singleton threadid in
+    D.iter (fun v ->
+        ctx.sideg v threadid) escaped
+
   (* queries *)
   let query ctx (type a) (q: a Queries.t): a Queries.result =
     match q with
-    | Queries.MayEscape v -> D.mem v ctx.local
+    | Queries.MayEscape v ->
+      let threads = ctx.global v in
+      if ThreadIdSet.is_empty threads then
+        false
+      else begin
+        let possibly_started current = function
+          | `Lifted tid ->
+            let threads = ctx.ask Queries.CreatedThreads in
+            let not_started = MHP.definitely_not_started (current, threads) tid in
+            M.tracel "threadescape" "tid: %a, not_started: %b\n" ThreadIdDomain.FlagConfiguredTID.pretty tid not_started;
+            let possibly_started = not not_started in
+            possibly_started
+          | `Top -> true
+          | `Bot -> false
+        in
+        let equal_current_not_unique current = function
+          | `Lifted tid ->
+            ThreadId.Thread.equal current tid && not (ThreadId.Thread.is_unique current)
+          | `Top -> true
+          | `Bot -> false
+        in
+        match ctx.ask Queries.CurrentThreadId with
+        | `Lifted current ->
+          let possibly_started = ThreadIdSet.exists (possibly_started current) threads in
+          if possibly_started then
+            true
+          else if ThreadIdSet.exists (equal_current_not_unique current) threads then
+            (* Another instance of the non-unqiue current thread may have escaped the variable *)
+            true
+          else
+            (* Check whether current unique thread has escaped the variable *)
+            D.mem v ctx.local
+        | `Top ->
+          true
+        | `Bot ->
+          M.warn ~category:MessageCategory.Analyzer "CurrentThreadId is bottom.";
+          false
+      end
     | _ -> Queries.Result.top q
 
+  let escape_rval ctx (rval:exp) =
+    let ask = Analyses.ask_of_ctx ctx in
+    let escaped = reachable ask rval in
+    let escaped = D.filter (fun v -> not v.vglob) escaped in
+
+    let thread_id = thread_id ctx in
+    side_effect_escape ctx escaped thread_id;
+    if ThreadFlag.has_ever_been_multi ask then (* avoid emitting unnecessary event *)
+      emit_escape_event ctx escaped;
+    escaped
+
   (* transfer functions *)
   let assign ctx (lval:lval) (rval:exp) : D.t =
     let ask = Analyses.ask_of_ctx ctx in
     let vs = mpt ask (AddrOf lval) in
-    if M.tracing then M.tracel "escape" "assign vs: %a\n" D.pretty vs;
     if D.exists (fun v -> v.vglob || has_escaped ask v) vs then (
-      let escaped = reachable ask rval in
-      let escaped = D.filter (fun v -> not v.vglob) escaped in
-      if M.tracing then M.tracel "escape" "assign vs: %a | %a\n" D.pretty vs D.pretty escaped;
-      if not (D.is_empty escaped) && ThreadFlag.has_ever_been_multi ask then (* avoid emitting unnecessary event *)
-        ctx.emit (Events.Escape escaped);
-      D.iter (fun v ->
-          ctx.sideg v escaped;
-        ) vs;
+      let escaped = escape_rval ctx rval in
       D.join ctx.local escaped
-    )
-    else
+    ) else begin
       ctx.local
+    end
 
   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 = reachable (Analyses.ask_of_ctx ctx) pt_value in
-      let escaped = D.filter (fun v -> not v.vglob) escaped in
-      if not (D.is_empty escaped) then (* avoid emitting unnecessary event *)
-        ctx.emit (Events.Escape escaped);
-      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)
+      let escaped = escape_rval ctx pt_value in
+      D.join ctx.local escaped
     | _ -> ctx.local
 
   let startstate v = D.bot ()
@@ -87,31 +144,31 @@ struct
     | [ptc_arg] ->
       let escaped = reachable (Analyses.ask_of_ctx ctx) ptc_arg in
       let escaped = D.filter (fun v -> not v.vglob) escaped in
-      if not (D.is_empty escaped) then (* avoid emitting unnecessary event *)
-        ctx.emit (Events.Escape escaped);
-      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)]
+      emit_escape_event ctx escaped;
+      [D.join ctx.local escaped]
     | _ -> [ctx.local]
 
   let threadspawn ctx lval f args fctx =
     D.join ctx.local @@
-      match args with
-      | [ptc_arg] ->
-        (* not reusing fctx.local to avoid unnecessarily early join of extra *)
-        let escaped = reachable (Analyses.ask_of_ctx ctx) ptc_arg in
-        let escaped = D.filter (fun v -> not v.vglob) escaped in
-        if M.tracing then M.tracel "escape" "%a: %a\n" d_exp ptc_arg D.pretty escaped;
-        if not (D.is_empty escaped) then (* avoid emitting unnecessary event *)
-          ctx.emit (Events.Escape escaped);
-        escaped
-      | _ -> D.bot ()
+    match args with
+    | [ptc_arg] ->
+      (* not reusing fctx.local to avoid unnecessarily early join of extra *)
+      let escaped = reachable (Analyses.ask_of_ctx ctx) ptc_arg in
+      let escaped = D.filter (fun v -> not v.vglob) escaped in
+      if M.tracing then M.tracel "escape" "%a: %a\n" d_exp ptc_arg D.pretty escaped;
+      let thread_id = thread_id ctx in
+      emit_escape_event ctx escaped;
+      side_effect_escape ctx escaped thread_id;
+      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);
+      let thread_id = thread_id ctx in
+      emit_escape_event ctx escaped;
+      side_effect_escape ctx escaped thread_id;
       ctx.local
     | _ -> ctx.local
 end

tests/regression/45-escape/06-local-escp.c

@@ -0,0 +1,38 @@
+// PARAM:  --enable ana.int.interval
+#include<stdlib.h>
+#include<pthread.h>
+#include<goblint.h>
+#include<unistd.h>
+
+int g = 0;
+int *p = &g;
+
+
+void *thread1(void *pp){
+	int x = 23;
+	__goblint_check(x == 23);
+	p = &x;
+	sleep(2);
+	__goblint_check(x == 23); //UNKNOWN!
+	__goblint_check(x <= 23);
+	__goblint_check(x >= 1);
+
+	return NULL;
+}
+
+void *thread2(void *ignored){
+	sleep(1);
+	int *i = p;
+	*p = 1;
+	return NULL;
+}
+
+int main(){
+	pthread_t t1;
+	pthread_t t2;
+	pthread_create(&t1, NULL, thread1, NULL);
+	pthread_create(&t2, NULL, thread2, NULL);
+	pthread_join(t1, NULL);
+	pthread_join(t2, NULL);
+}
+

tests/regression/45-escape/07-local-in-global-after-create.c

@@ -0,0 +1,22 @@
+// SKIP
+#include <pthread.h>
+#include <goblint.h>
+
+int* gptr;
+
+void *foo(void* p){
+    *gptr = 17;
+    return NULL;
+}
+
+int main(){
+    int x = 0;
+    __goblint_check(x==0);
+    pthread_t thread;
+    pthread_create(&thread, NULL, foo, NULL);
+    gptr = &x;
+    sleep(3);
+    __goblint_check(x == 0); // UNKNOWN!
+    pthread_join(thread, NULL);
+    return 0;
+}

tests/regression/45-escape/08-local-escp-main.c

@@ -0,0 +1,31 @@
+//PARAM: --enable ana.int.interval
+#include<stdlib.h>
+#include<pthread.h>
+#include<goblint.h>
+#include<unistd.h>
+
+int g = 0;
+int *p = &g;
+
+
+void *thread1(void *pp){
+	int x = 23;
+	__goblint_check(x == 23);
+	p = &x;
+	sleep(2);
+	__goblint_check(x == 23); //UNKNOWN!
+	__goblint_check(x <= 23);
+	__goblint_check(x >= 1);
+
+	int y = x;
+	return NULL;
+}
+
+int main(){
+	pthread_t t1;
+	pthread_t t2;
+	pthread_create(&t1, NULL, thread1, NULL);
+	sleep(1);
+	*p = 1;
+}
+