Pass unknown pointers through reachable query

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,7 +60,7 @@ 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. *)
     | a ->
       if M.tracing then M.tracel "escape" "reachable %a: %a\n" d_exp e Queries.LS.pretty a;

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