From d5a81da55ddfe292e42634abd907be8c5ac4af2f Mon Sep 17 00:00:00 2001
From: Karoliine Holter <karoliine.holter@hotmail.com>
Date: Tue, 21 Nov 2023 11:13:35 +0200
Subject: [PATCH] Add get_unknownptrs and has_unknownptr and use
 remove_unknownptrs instead of remove

---
 src/analyses/base.ml               |  3 ++-
 src/analyses/condVars.ml           |  4 ++--
 src/analyses/extractPthread.ml     |  2 +-
 src/cdomains/addressDomain.ml      | 12 ++++++++++++
 src/cdomains/addressDomain_intf.ml |  2 ++
 5 files changed, 19 insertions(+), 4 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 3dd0775ba1..08b686e244 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1325,10 +1325,11 @@ struct
         | Bot -> Queries.Result.bot q (* TODO: remove *)
         | Address a ->
           let a' = AD.remove_unknownptrs a in (* run reachable_vars without unknown just to be safe: TODO why? *)
+          let u = AD.get_unknownptrs a in
           let addrs = reachable_vars (Analyses.ask_of_ctx ctx) [a'] ctx.global ctx.local in
           let addrs' = List.fold_left (AD.join) (AD.empty ()) addrs in
           if AD.may_be_unknown a then
-            AD.add UnknownPtr addrs' (* add unknown back *)
+            AD.union u addrs' (* add unknowns back *)
           else
             addrs'
         | Int i ->
diff --git a/src/analyses/condVars.ml b/src/analyses/condVars.ml
index 3b23dc03fc..0c739d0e9a 100644
--- a/src/analyses/condVars.ml
+++ b/src/analyses/condVars.ml
@@ -65,9 +65,9 @@ struct
 
   let mayPointTo ctx exp =
     let ad = ctx.ask (Queries.MayPointTo exp) in
-    let a' = if Queries.AD.mem UnknownPtr ad then (
+    let a' = if Queries.AD.has_unknownptr ad then (
         M.info ~category:Unsound "mayPointTo: query result for %a contains TOP!" d_exp exp; (* UNSOUND *)
-        Queries.AD.remove UnknownPtr ad
+        Queries.AD.remove_unknownptrs ad
       ) else ad
     in
     List.filter_map (function
diff --git a/src/analyses/extractPthread.ml b/src/analyses/extractPthread.ml
index f084a21edb..7cacd86693 100644
--- a/src/analyses/extractPthread.ml
+++ b/src/analyses/extractPthread.ml
@@ -878,7 +878,7 @@ module Spec : Analyses.MCPSpec = struct
   module ExprEval = struct
     let eval_ptr ctx exp =
       ctx.ask (Queries.MayPointTo exp)
-      |> Queries.AD.remove UnknownPtr (* UNSOUND *)
+      |> Queries.AD.remove_unknownptrs (* UNSOUND *)
       |> Queries.AD.to_var_may
 
     let eval_var ctx exp =
diff --git a/src/cdomains/addressDomain.ml b/src/cdomains/addressDomain.ml
index d33b80405d..ec71dd9cfd 100644
--- a/src/cdomains/addressDomain.ml
+++ b/src/cdomains/addressDomain.ml
@@ -469,6 +469,18 @@ struct
       | UnknownPtr _ -> false
       | _ -> true
     ) ad
+
+  let get_unknownptrs ad = filter (function
+      | UnknownPtr _ -> true
+      | _ -> false
+    ) ad
+
+  let has_unknownptr ad = fold (fun a acc ->
+      match a with
+      | UnknownPtr _ -> true
+      | _ -> acc
+    ) ad false
+
   let unknownptrs_origins doc ad =
     fold (fun addr acc ->
         match addr with
diff --git a/src/cdomains/addressDomain_intf.ml b/src/cdomains/addressDomain_intf.ml
index f95556af77..b02335b997 100644
--- a/src/cdomains/addressDomain_intf.ml
+++ b/src/cdomains/addressDomain_intf.ml
@@ -195,6 +195,8 @@ sig
     val string_comparison: t -> t -> int option -> ID.t
     val string_writing_defined: t -> bool
     val remove_unknownptrs: t -> t
+    val get_unknownptrs: t -> t
+    val has_unknownptr: t -> bool
     val unknownptrs_origins: GoblintCil.Pretty.doc -> t -> (GoblintCil.Pretty.doc * Messages.Location.t option) list
   end
 end