Merge pull request #495 from goblint/escape-unknown

Fix known addresses not escaping when address set contains unknown

Author: sim642

src/analyses/base.ml

@@ -985,12 +985,14 @@ struct
         match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with
         | `Top -> Queries.Result.top q
         | `Bot -> Queries.Result.bot q (* TODO: remove *)
-        | `Address a when AD.is_top a || AD.mem Addr.UnknownPtr a ->
-          Q.LS.top ()
         | `Address a ->
-          let xs = List.map addrToLvalSet (reachable_vars (Analyses.ask_of_ctx ctx) [a] ctx.global ctx.local) in
+          let a' = AD.remove Addr.UnknownPtr a in (* run reachable_vars without unknown just to be safe *)
+          let xs = List.map addrToLvalSet (reachable_vars (Analyses.ask_of_ctx ctx) [a'] ctx.global ctx.local) in
           let addrs = List.fold_left (Q.LS.join) (Q.LS.empty ()) xs in
-          addrs
+          if AD.mem Addr.UnknownPtr a then
+            Q.LS.add (dummyFunDec.svar, `NoOffset) addrs (* add unknown back *)
+          else
+            addrs
         | _ -> Q.LS.empty ()
       end
     | Q.ReachableUkTypes e -> begin

src/analyses/malloc_null.ml

@@ -108,7 +108,7 @@ struct
         match ask.f (Queries.ReachableFrom e) with
         | a when not (Queries.LS.is_top a)  ->
           let to_extra (v,o) xs = AD.from_var_offset (v,(conv_offset o)) :: xs  in
-          Queries.LS.fold to_extra a []
+          Queries.LS.fold to_extra (Queries.LS.remove (dummyFunDec.svar, `NoOffset) a) []
         (* Ignore soundness warnings, as invalidation proper will raise them. *)
         | _ -> []
       in

src/analyses/threadEscape.ml

@@ -60,9 +60,11 @@ struct
     | 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 a (D.empty ())
+      Queries.LS.fold to_extra (Queries.LS.remove (dummyFunDec.svar, `NoOffset) a) (D.empty ())
     (* Ignore soundness warnings, as invalidation proper will raise them. *)
-    | _ -> D.empty ()
+    | 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
@@ -84,6 +86,7 @@ struct
       match args with
       | [ptc_arg] ->
         let escaped = fctx.local in (* reuse reachable computation from threadenter *)
+        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

src/analyses/uninit.ml

@@ -89,7 +89,7 @@ struct
       match ask (Queries.ReachableFrom e) with
       | a when not (Queries.LS.is_top a) ->
         let to_extra (v,o) xs = (v, Base.Offs.from_offset (conv_offset o), true) :: xs  in
-        Queries.LS.fold to_extra a []
+        Queries.LS.fold to_extra (Queries.LS.remove (dummyFunDec.svar, `NoOffset) a) []
       (* Ignore soundness warnings, as invalidation proper will raise them. *)
       | _ -> []
     in
@@ -227,7 +227,7 @@ struct
         match ask.f (Queries.ReachableFrom e) with
         | a when not (Queries.LS.is_top a) ->
           let to_extra (v,o) xs = AD.from_var_offset (v,(conv_offset o)) :: xs  in
-          Queries.LS.fold to_extra a []
+          Queries.LS.fold to_extra (Queries.LS.remove (dummyFunDec.svar, `NoOffset) a) []
         (* Ignore soundness warnings, as invalidation proper will raise them. *)
         | _ -> []
       in

tests/regression/02-base/70-escape-unknown.c

@@ -0,0 +1,28 @@
+#include <pthread.h>
+#include <assert.h>
+
+int *p;
+
+void *t_fun(void *arg) {
+  if (arg != NULL) {
+    *((int*)arg) = 42;
+  }
+  return NULL;
+}
+
+int main() {
+  pthread_t id, id2;
+  int *r; // unknown
+  int i = 5;
+
+  pthread_create(&id, NULL, t_fun, NULL); // enter multithreaded
+
+  p = r;
+  p = &i;
+
+  pthread_create(&id2, NULL, t_fun, p); // i should escape, even if p contains unknown
+
+  assert(i == 5); // UNKNOWN!
+
+  return 0;
+}