Merge pull request #984 from goblint/issue-939

Handle escaping in `varEq` analysis

Author: michael-schwarz

src/analyses/varEq.ml

@@ -336,7 +336,7 @@ struct
     | Imag _ -> None
     | Const _ -> Some false
     | Lval (Var v,_) ->
-      Some (v.vglob || (ask.f (Queries.IsMultiple v)))
+      Some (v.vglob || (ask.f (Queries.IsMultiple v) || BaseUtil.is_global ask v))
     | Lval (Mem e, _) ->
       begin match ask.f (Queries.MayPointTo e) with
         | ls when not (Queries.LS.is_top ls) && not (Queries.LS.mem (dummyFunDec.svar, `NoOffset) ls) ->
@@ -558,6 +558,15 @@ struct
       |> List.fold_left (fun st lv ->
           remove (Analyses.ask_of_ctx ctx) lv st
         ) ctx.local
+    | Events.Escape vars ->
+      if EscapeDomain.EscapedVars.is_top vars then 
+        D.top () 
+      else
+      let ask = Analyses.ask_of_ctx ctx in
+      let remove_var st v =
+        remove ask (Cil.var v) st
+      in
+      List.fold_left remove_var ctx.local (EscapeDomain.EscapedVars.elements vars)
     | _ ->
       ctx.local
 end

tests/regression/06-symbeq/41-vareq_global.c

@@ -0,0 +1,28 @@
+//PARAM: --set ana.activated[+] var_eq
+#include <goblint.h>
+#include <pthread.h>
+#include <unistd.h>
+int g;
+
+void *t_fun1(void *arg) {
+  int *zptr = (int*) arg;
+  int* gptr = &g;
+
+  *zptr = 42;
+  *gptr = 42;
+  sleep(10);
+  // here the other thread (id2) could potentially change *zptr, as it is linked to the same int z
+  __goblint_check(*zptr == 42);  //UNKNOWN!
+  __goblint_check(*gptr == 42);  //UNKNOWN!
+  return NULL;
+}
+
+int main() {
+  pthread_t id1;
+  int z = 8;
+
+  pthread_create(&id1, NULL, t_fun1, &z);
+  z = 8;
+  g = 8;
+  pthread_join (id1, NULL);
+}

tests/regression/06-symbeq/42-vareq_escape.c

@@ -0,0 +1,25 @@
+//PARAM: --set ana.activated[+] var_eq
+#include <goblint.h>
+#include <pthread.h>
+#include <unistd.h>
+int g;
+
+void *t_fun1(void *arg) {
+  int** ptrptr = (int**) arg;
+  int* iptr = *ptrptr;
+
+  *iptr = 12;
+}
+
+int main() {
+  pthread_t id1;
+  int z = 8;
+  int i;
+  int* zptr = &z;
+
+  int j = i;
+  pthread_create(&id1, NULL, t_fun1, &zptr);
+  zptr = &i; 
+  __goblint_check(i == j); //UNKNOWN!
+  pthread_join (id1, NULL);
+}