Merge pull request #1078 from goblint/escape_analysis_flow-insens

ThreadEscape: Collect set of escaping threads flow-insensitively

src/analyses/apron/relationAnalysis.apron.ml

@@ -280,12 +280,9 @@ struct
     | None -> true
     | Some v -> any_local_reachable
 
-  let enter ctx r f args =
+  let make_callee_rel ~thread ctx f args =
     let fundec = Node.find_fundec ctx.node in
     let st = ctx.local in
-    if M.tracing then M.tracel "combine" "relation enter f: %a\n" CilType.Varinfo.pretty f.svar;
-    if M.tracing then M.tracel "combine" "relation enter formals: %a\n" (d_list "," CilType.Varinfo.pretty) f.sformals;
-    if M.tracing then M.tracel "combine" "relation enter local: %a\n" D.pretty ctx.local;
     let arg_assigns =
       GobList.combine_short f.sformals args (* TODO: is it right to ignore missing formals/args? *)
       |> List.filter (fun (x, _) -> RD.Tracked.varinfo_tracked x)
@@ -296,12 +293,16 @@ struct
     let new_rel = RD.add_vars st.rel arg_vars in
     (* RD.assign_exp_parallel_with new_rel arg_assigns; (* doesn't need to be parallel since exps aren't arg vars directly *) *)
     (* TODO: parallel version of assign_from_globals_wrapper? *)
-    let ask = Analyses.ask_of_ctx ctx in
-    let new_rel = List.fold_left (fun new_rel (var, e) ->
-        assign_from_globals_wrapper ask ctx.global {st with rel = new_rel} e (fun rel' e' ->
-            RD.assign_exp rel' var e' (no_overflow ask e)
-          )
-      ) new_rel arg_assigns
+    let new_rel =
+      if thread then
+        new_rel
+      else
+        let ask = Analyses.ask_of_ctx ctx in
+        List.fold_left (fun new_rel (var, e) ->
+            assign_from_globals_wrapper ask ctx.global {st with rel = new_rel} e (fun rel' e' ->
+                RD.assign_exp rel' var e' (no_overflow ask e)
+              )
+          ) new_rel arg_assigns
     in
     let any_local_reachable = any_local_reachable fundec reachable_from_args in
     RD.remove_filter_with new_rel (fun var ->
@@ -311,7 +312,11 @@ struct
         | _ -> false (* keep everything else (just added args, globals, global privs) *)
       );
     if M.tracing then M.tracel "combine" "relation enter newd: %a\n" RD.pretty new_rel;
-    [st, {st with rel = new_rel}]
+    new_rel
+
+  let enter ctx r f args =
+    let calle_rel = make_callee_rel ~thread:false ctx f args in
+    [ctx.local, {ctx.local with rel = calle_rel}]
 
   let body ctx f =
     let st = ctx.local in
@@ -627,12 +632,7 @@ struct
       if not (ThreadFlag.has_ever_been_multi (Analyses.ask_of_ctx ctx)) then
         ignore (Priv.enter_multithreaded (Analyses.ask_of_ctx ctx) ctx.global ctx.sideg st);
       let st' = Priv.threadenter (Analyses.ask_of_ctx ctx) ctx.global st in
-      let arg_vars =
-        fd.sformals
-        |> List.filter RD.Tracked.varinfo_tracked
-        |> List.map RV.arg
-      in
-      let new_rel = RD.add_vars st'.rel arg_vars in
+      let new_rel = make_callee_rel ~thread:true ctx fd args in
       [{st' with rel = new_rel}]
     | exception Not_found ->
       (* Unknown functions *)

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,76 +44,127 @@ 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
+            let possibly_started = not not_started in
+            possibly_started
+          | `Top -> true
+          | `Bot -> false
+        in
+        let equal_current current = function
+          | `Lifted tid ->
+            ThreadId.Thread.equal current tid
+          | `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
+            let current_is_unique = ThreadId.Thread.is_unique current in
+            let any_equal_current threads = ThreadIdSet.exists (equal_current current) threads in
+            if not current_is_unique && any_equal_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 ()
   let exitstate  v = D.bot ()
 
   let threadenter ctx lval f args =
+    [D.bot ()]
+
+  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 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)]
-    | _ -> [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 ()
+      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

src/cdomains/apron/affineEqualityDomain.apron.ml

@@ -79,12 +79,14 @@ struct
   let change_d t new_env add del = timing_wrap "dimension change" (change_d t new_env add) del
 
   let add_vars t vars =
+    let t = copy t in
     let env' = add_vars t.env vars in
     change_d t env' true false
 
   let add_vars t vars = timing_wrap "add_vars" (add_vars t) vars
 
   let drop_vars t vars del =
+    let t = copy t in
     let env' = remove_vars t.env vars in
     change_d t env' false del
 
@@ -111,12 +113,14 @@ struct
     t.env <- t'.env
 
   let keep_filter t f =
+    let t = copy t in
     let env' = keep_filter t.env f in
     change_d t env' false false
 
   let keep_filter t f = timing_wrap "keep_filter" (keep_filter t) f
 
   let keep_vars t vs =
+    let t = copy t in
     let env' = keep_vars t.env vs in
     change_d t env' false false
 

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;
+}
+