From dc0df887e22adc34ff93f170f337ddcc7b9aff19 Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Tue, 29 Aug 2023 12:27:57 +0300
Subject: [PATCH 01/19] Add MustLocksetA and MustProtectedVarsA to queries

---
 src/domains/queries.ml | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index 0388ce2995..8680103d7a 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -81,6 +81,7 @@ type _ t =
   | MayBePublicWithout: maybepublicwithout -> MayBool.t t
   | MustBeProtectedBy: mustbeprotectedby -> MustBool.t t
   | MustLockset: LS.t t
+  | MustLocksetA: AD.t t
   | MustBeAtomic: MustBool.t t
   | MustBeSingleThreaded: {since_start: bool} -> MustBool.t t
   | MustBeUniqueThread: MustBool.t t
@@ -115,6 +116,7 @@ type _ t =
   | MustJoinedThreads: ConcDomain.MustThreadSet.t t
   | ThreadsJoinedCleanly: MustBool.t t
   | MustProtectedVars: mustprotectedvars -> LS.t t
+  | MustProtectedVarsA: mustprotectedvars -> AD.t t
   | Invariant: invariant_context -> Invariant.t t
   | InvariantGlobal: Obj.t -> Invariant.t t (** Argument must be of corresponding [Spec.V.t]. *)
   | WarnGlobal: Obj.t -> Unit.t t (** Argument must be of corresponding [Spec.V.t]. *)
@@ -145,6 +147,7 @@ struct
     | ReachableFrom _ -> (module AD)
     | Regions _ -> (module LS)
     | MustLockset -> (module LS)
+    | MustLocksetA -> (module AD)
     | EvalFunvar _ -> (module LS)
     | ReachableUkTypes _ -> (module TS)
     | MayEscape _ -> (module MayBool)
@@ -180,6 +183,7 @@ struct
     | MustJoinedThreads -> (module ConcDomain.MustThreadSet)
     | ThreadsJoinedCleanly -> (module MustBool)
     | MustProtectedVars _ -> (module LS)
+    | MustProtectedVarsA _ -> (module AD)
     | Invariant _ -> (module Invariant)
     | InvariantGlobal _ -> (module Invariant)
     | WarnGlobal _ -> (module Unit)
@@ -209,6 +213,7 @@ struct
     | ReachableFrom _ -> AD.top ()
     | Regions _ -> LS.top ()
     | MustLockset -> LS.top ()
+    | MustLocksetA -> AD.top ()
     | EvalFunvar _ -> LS.top ()
     | ReachableUkTypes _ -> TS.top ()
     | MayEscape _ -> MayBool.top ()
@@ -244,6 +249,7 @@ struct
     | MustJoinedThreads -> ConcDomain.MustThreadSet.top ()
     | ThreadsJoinedCleanly -> MustBool.top ()
     | MustProtectedVars _ -> LS.top ()
+    | MustProtectedVarsA _ -> AD.top ()
     | Invariant _ -> Invariant.top ()
     | InvariantGlobal _ -> Invariant.top ()
     | WarnGlobal _ -> Unit.top ()
@@ -274,6 +280,7 @@ struct
     | Any (MayBePublicWithout _) -> 8
     | Any (MustBeProtectedBy _) -> 9
     | Any MustLockset -> 10
+    | Any MustLocksetA -> 1010
     | Any MustBeAtomic -> 11
     | Any (MustBeSingleThreaded _)-> 12
     | Any MustBeUniqueThread -> 13
@@ -299,6 +306,7 @@ struct
     | Any (IterSysVars _) -> 37
     | Any (InvariantGlobal _) -> 38
     | Any (MustProtectedVars _) -> 39
+    | Any (MustProtectedVarsA _) -> 3939
     | Any MayAccessed -> 40
     | Any MayBeTainted -> 41
     | Any (PathQuery _) -> 42
@@ -356,6 +364,7 @@ struct
       | Any (IterSysVars (vq1, vf1)), Any (IterSysVars (vq2, vf2)) -> VarQuery.compare vq1 vq2 (* not comparing fs *)
       | Any (MutexType m1), Any (MutexType m2) -> Mval.Unit.compare m1 m2
       | Any (MustProtectedVars m1), Any (MustProtectedVars m2) -> compare_mustprotectedvars m1 m2
+      | Any (MustProtectedVarsA m1), Any (MustProtectedVarsA m2) -> compare_mustprotectedvars m1 m2
       | Any (MayBeModifiedSinceSetjmp e1), Any (MayBeModifiedSinceSetjmp e2) -> JmpBufDomain.BufferEntry.compare e1 e2
       | Any (MustBeSingleThreaded {since_start=s1;}),  Any (MustBeSingleThreaded {since_start=s2;}) -> Stdlib.compare s1 s2
       | Any (TmpSpecial lv1), Any (TmpSpecial lv2) -> Mval.Exp.compare lv1 lv2
@@ -395,6 +404,7 @@ struct
     | Any (MutexType m) -> Mval.Unit.hash m
     | Any (InvariantGlobal vi) -> Hashtbl.hash vi
     | Any (MustProtectedVars m) -> hash_mustprotectedvars m
+    | Any (MustProtectedVarsA m) -> hash_mustprotectedvars m
     | Any (MayBeModifiedSinceSetjmp e) -> JmpBufDomain.BufferEntry.hash e
     | Any (MustBeSingleThreaded {since_start}) -> Hashtbl.hash since_start
     | Any (TmpSpecial lv) -> Mval.Exp.hash lv
@@ -417,6 +427,7 @@ struct
     | Any (MayBePublicWithout x) -> Pretty.dprintf "MayBePublicWithout _"
     | Any (MustBeProtectedBy x) -> Pretty.dprintf "MustBeProtectedBy _"
     | Any MustLockset -> Pretty.dprintf "MustLockset"
+    | Any MustLocksetA -> Pretty.dprintf "MustLocksetA"
     | Any MustBeAtomic -> Pretty.dprintf "MustBeAtomic"
     | Any (MustBeSingleThreaded {since_start}) -> Pretty.dprintf "MustBeSingleThreaded since_start=%b" since_start
     | Any MustBeUniqueThread -> Pretty.dprintf "MustBeUniqueThread"
@@ -445,6 +456,7 @@ struct
     | Any MustJoinedThreads -> Pretty.dprintf "MustJoinedThreads"
     | Any ThreadsJoinedCleanly -> Pretty.dprintf "ThreadsJoinedCleanly"
     | Any (MustProtectedVars m) -> Pretty.dprintf "MustProtectedVars _"
+    | Any (MustProtectedVarsA m) -> Pretty.dprintf "MustProtectedVarsA _"
     | Any (Invariant i) -> Pretty.dprintf "Invariant _"
     | Any (WarnGlobal vi) -> Pretty.dprintf "WarnGlobal _"
     | Any (IterSysVars _) -> Pretty.dprintf "IterSysVars _"

From 326b8e66d7ed97d21ce894bf0a32612487038815 Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Tue, 29 Aug 2023 12:28:42 +0300
Subject: [PATCH 02/19] Use MustLocksetA and MustProtectedVarsA in
 mutexAnalysis

---
 src/analyses/base.ml          |  1 +
 src/analyses/commonPriv.ml    | 19 +++++++++----------
 src/analyses/mutexAnalysis.ml | 10 ++--------
 3 files changed, 12 insertions(+), 18 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 4183261ddb..d7c7d4429b 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2542,6 +2542,7 @@ struct
                 | MayBePublicWithout _
                 | MustBeProtectedBy _
                 | MustLockset
+                | MustLocksetA
                 | MustBeAtomic
                 | MustBeSingleThreaded _
                 | MustBeUniqueThread
diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index 1b92cb320d..4aca250ba5 100644
--- a/src/analyses/commonPriv.ml
+++ b/src/analyses/commonPriv.ml
@@ -61,12 +61,13 @@ struct
 
   let protected_vars (ask: Q.ask): varinfo list =
     let module VS = Set.Make (CilType.Varinfo) in
-    Q.LS.fold (fun (v, _) acc ->
-        let m = ValueDomain.Addr.of_var v in (* TODO: don't ignore offsets *)
-        Q.LS.fold (fun l acc ->
-            VS.add (fst l) acc (* always `NoOffset from mutex analysis *)
-          ) (ask.f (Q.MustProtectedVars {mutex = m; write = true})) acc
-      ) (ask.f Q.MustLockset) VS.empty
+    Q.AD.fold (fun m acc ->
+        Q.AD.fold (fun l acc ->
+            match l with
+            | Q.AD.Addr.Addr (v,_) -> VS.add v acc (* always `NoOffset from mutex analysis *)
+            | _ -> acc
+          ) (ask.f (Q.MustProtectedVarsA {mutex = m; write = true})) acc
+      ) (ask.f Q.MustLocksetA) VS.empty
     |> VS.elements
 end
 
@@ -126,10 +127,8 @@ struct
     if !AnalysisState.global_initialization then
       Lockset.empty ()
     else
-      let ls = ask.f Queries.MustLockset in
-      Q.LS.fold (fun (var, offs) acc ->
-          Lockset.add (Lock.of_mval (var, Lock.Offs.of_exp offs)) acc
-        ) ls (Lockset.empty ())
+      let ad = ask.f Queries.MustLocksetA in
+      Q.AD.fold (fun mls acc -> Lockset.add mls acc) ad (Lockset.empty ())
 
   (* TODO: reversed SetDomain.Hoare *)
   module MinLocksets = HoareDomain.Set_LiftTop (MustLockset) (struct let topname = "All locksets" end) (* reverse Lockset because Hoare keeps maximal, but we need minimal *)
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index 7d8298a0a4..bc03216ba6 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -231,15 +231,9 @@ struct
         true
       else *)
       Mutexes.leq mutex_lockset protecting
-    | Queries.MustLockset ->
+    | Queries.MustLocksetA ->
       let held_locks = Lockset.export_locks (Lockset.filter snd ls) in
-      let ls = Mutexes.fold (fun addr ls ->
-          match Addr.to_mval addr with
-          | Some (var, offs) -> Queries.LS.add (var, Addr.Offs.to_exp offs) ls
-          | None -> ls
-        ) held_locks (Queries.LS.empty ())
-      in
-      ls
+      Mutexes.fold (fun addr ls -> Queries.AD.add addr ls) held_locks (Queries.AD.empty ())
     | Queries.MustBeAtomic ->
       let held_locks = Lockset.export_locks (Lockset.filter snd ls) in
       Mutexes.mem (LockDomain.Addr.of_var LF.verifier_atomic_var) held_locks

From 2bf93536925839af61816451656586208012f763 Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Tue, 29 Aug 2023 14:44:53 +0300
Subject: [PATCH 03/19] Use MustProtectedVarsA in mutexAnalysis

---
 src/analyses/mutexAnalysis.ml | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index bc03216ba6..9bde708566 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -242,6 +242,11 @@ struct
       VarSet.fold (fun v acc ->
           Queries.LS.add (v, `NoOffset) acc
         ) protected (Queries.LS.empty ())
+    | Queries.MustProtectedVarsA {mutex = m; write} ->
+      let protected = GProtected.get ~write Strong (G.protected (ctx.global (V.protected m))) in
+      VarSet.fold (fun v acc ->
+          Queries.AD.join (Queries.AD.of_var v) acc
+        ) protected (Queries.AD.empty ())
     | Queries.IterSysVars (Global g, f) ->
       f (Obj.repr (V.protecting g)) (* TODO: something about V.protected? *)
     | WarnGlobal g ->

From 65567a603f6b3fb8c7c869fa1bbc6f8a23d69691 Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Tue, 29 Aug 2023 14:50:29 +0300
Subject: [PATCH 04/19] Remove MustLockset and MustProtectedVars from queries

---
 src/analyses/base.ml          |  1 -
 src/analyses/mutexAnalysis.ml |  5 -----
 src/domains/queries.ml        | 16 ++--------------
 3 files changed, 2 insertions(+), 20 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index d7c7d4429b..a7330459f0 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2541,7 +2541,6 @@ struct
                 | MayBePublic _
                 | MayBePublicWithout _
                 | MustBeProtectedBy _
-                | MustLockset
                 | MustLocksetA
                 | MustBeAtomic
                 | MustBeSingleThreaded _
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index 9bde708566..55172c48eb 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -237,11 +237,6 @@ struct
     | Queries.MustBeAtomic ->
       let held_locks = Lockset.export_locks (Lockset.filter snd ls) in
       Mutexes.mem (LockDomain.Addr.of_var LF.verifier_atomic_var) held_locks
-    | Queries.MustProtectedVars {mutex = m; write} ->
-      let protected = GProtected.get ~write Strong (G.protected (ctx.global (V.protected m))) in
-      VarSet.fold (fun v acc ->
-          Queries.LS.add (v, `NoOffset) acc
-        ) protected (Queries.LS.empty ())
     | Queries.MustProtectedVarsA {mutex = m; write} ->
       let protected = GProtected.get ~write Strong (G.protected (ctx.global (V.protected m))) in
       VarSet.fold (fun v acc ->
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index 8680103d7a..a160e6dd7b 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -80,7 +80,6 @@ type _ t =
   | MayBePublic: maybepublic -> MayBool.t t (* old behavior with write=false *)
   | MayBePublicWithout: maybepublicwithout -> MayBool.t t
   | MustBeProtectedBy: mustbeprotectedby -> MustBool.t t
-  | MustLockset: LS.t t
   | MustLocksetA: AD.t t
   | MustBeAtomic: MustBool.t t
   | MustBeSingleThreaded: {since_start: bool} -> MustBool.t t
@@ -115,7 +114,6 @@ type _ t =
   | CreatedThreads: ConcDomain.ThreadSet.t t
   | MustJoinedThreads: ConcDomain.MustThreadSet.t t
   | ThreadsJoinedCleanly: MustBool.t t
-  | MustProtectedVars: mustprotectedvars -> LS.t t
   | MustProtectedVarsA: mustprotectedvars -> AD.t t
   | Invariant: invariant_context -> Invariant.t t
   | InvariantGlobal: Obj.t -> Invariant.t t (** Argument must be of corresponding [Spec.V.t]. *)
@@ -146,7 +144,6 @@ struct
     | MayPointTo _ -> (module AD)
     | ReachableFrom _ -> (module AD)
     | Regions _ -> (module LS)
-    | MustLockset -> (module LS)
     | MustLocksetA -> (module AD)
     | EvalFunvar _ -> (module LS)
     | ReachableUkTypes _ -> (module TS)
@@ -182,7 +179,6 @@ struct
     | CreatedThreads ->  (module ConcDomain.ThreadSet)
     | MustJoinedThreads -> (module ConcDomain.MustThreadSet)
     | ThreadsJoinedCleanly -> (module MustBool)
-    | MustProtectedVars _ -> (module LS)
     | MustProtectedVarsA _ -> (module AD)
     | Invariant _ -> (module Invariant)
     | InvariantGlobal _ -> (module Invariant)
@@ -212,7 +208,6 @@ struct
     | MayPointTo _ -> AD.top ()
     | ReachableFrom _ -> AD.top ()
     | Regions _ -> LS.top ()
-    | MustLockset -> LS.top ()
     | MustLocksetA -> AD.top ()
     | EvalFunvar _ -> LS.top ()
     | ReachableUkTypes _ -> TS.top ()
@@ -248,7 +243,6 @@ struct
     | CreatedThreads -> ConcDomain.ThreadSet.top ()
     | MustJoinedThreads -> ConcDomain.MustThreadSet.top ()
     | ThreadsJoinedCleanly -> MustBool.top ()
-    | MustProtectedVars _ -> LS.top ()
     | MustProtectedVarsA _ -> AD.top ()
     | Invariant _ -> Invariant.top ()
     | InvariantGlobal _ -> Invariant.top ()
@@ -279,8 +273,7 @@ struct
     | Any (MayBePublic _) -> 7
     | Any (MayBePublicWithout _) -> 8
     | Any (MustBeProtectedBy _) -> 9
-    | Any MustLockset -> 10
-    | Any MustLocksetA -> 1010
+    | Any MustLocksetA -> 10
     | Any MustBeAtomic -> 11
     | Any (MustBeSingleThreaded _)-> 12
     | Any MustBeUniqueThread -> 13
@@ -305,8 +298,7 @@ struct
     | Any (Invariant _) -> 36
     | Any (IterSysVars _) -> 37
     | Any (InvariantGlobal _) -> 38
-    | Any (MustProtectedVars _) -> 39
-    | Any (MustProtectedVarsA _) -> 3939
+    | Any (MustProtectedVarsA _) -> 39
     | Any MayAccessed -> 40
     | Any MayBeTainted -> 41
     | Any (PathQuery _) -> 42
@@ -363,7 +355,6 @@ struct
       | Any (InvariantGlobal vi1), Any (InvariantGlobal vi2) -> Stdlib.compare (Hashtbl.hash vi1) (Hashtbl.hash vi2)
       | Any (IterSysVars (vq1, vf1)), Any (IterSysVars (vq2, vf2)) -> VarQuery.compare vq1 vq2 (* not comparing fs *)
       | Any (MutexType m1), Any (MutexType m2) -> Mval.Unit.compare m1 m2
-      | Any (MustProtectedVars m1), Any (MustProtectedVars m2) -> compare_mustprotectedvars m1 m2
       | Any (MustProtectedVarsA m1), Any (MustProtectedVarsA m2) -> compare_mustprotectedvars m1 m2
       | Any (MayBeModifiedSinceSetjmp e1), Any (MayBeModifiedSinceSetjmp e2) -> JmpBufDomain.BufferEntry.compare e1 e2
       | Any (MustBeSingleThreaded {since_start=s1;}),  Any (MustBeSingleThreaded {since_start=s2;}) -> Stdlib.compare s1 s2
@@ -403,7 +394,6 @@ struct
     | Any (Invariant i) -> hash_invariant_context i
     | Any (MutexType m) -> Mval.Unit.hash m
     | Any (InvariantGlobal vi) -> Hashtbl.hash vi
-    | Any (MustProtectedVars m) -> hash_mustprotectedvars m
     | Any (MustProtectedVarsA m) -> hash_mustprotectedvars m
     | Any (MayBeModifiedSinceSetjmp e) -> JmpBufDomain.BufferEntry.hash e
     | Any (MustBeSingleThreaded {since_start}) -> Hashtbl.hash since_start
@@ -426,7 +416,6 @@ struct
     | Any (MayBePublic x) -> Pretty.dprintf "MayBePublic _"
     | Any (MayBePublicWithout x) -> Pretty.dprintf "MayBePublicWithout _"
     | Any (MustBeProtectedBy x) -> Pretty.dprintf "MustBeProtectedBy _"
-    | Any MustLockset -> Pretty.dprintf "MustLockset"
     | Any MustLocksetA -> Pretty.dprintf "MustLocksetA"
     | Any MustBeAtomic -> Pretty.dprintf "MustBeAtomic"
     | Any (MustBeSingleThreaded {since_start}) -> Pretty.dprintf "MustBeSingleThreaded since_start=%b" since_start
@@ -455,7 +444,6 @@ struct
     | Any CreatedThreads -> Pretty.dprintf "CreatedThreads"
     | Any MustJoinedThreads -> Pretty.dprintf "MustJoinedThreads"
     | Any ThreadsJoinedCleanly -> Pretty.dprintf "ThreadsJoinedCleanly"
-    | Any (MustProtectedVars m) -> Pretty.dprintf "MustProtectedVars _"
     | Any (MustProtectedVarsA m) -> Pretty.dprintf "MustProtectedVarsA _"
     | Any (Invariant i) -> Pretty.dprintf "Invariant _"
     | Any (WarnGlobal vi) -> Pretty.dprintf "WarnGlobal _"

From 4bf3680a0889e97f7e1cd845241139ccc95d144a Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Tue, 29 Aug 2023 14:55:02 +0300
Subject: [PATCH 05/19] Rename MustLocksetA -> MustLockset, MustProtectedVarsA
 -> MustProtectedVars

---
 src/analyses/base.ml          |  2 +-
 src/analyses/commonPriv.ml    |  6 +++---
 src/analyses/mutexAnalysis.ml |  4 ++--
 src/domains/queries.ml        | 24 ++++++++++++------------
 4 files changed, 18 insertions(+), 18 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index a7330459f0..4183261ddb 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2541,7 +2541,7 @@ struct
                 | MayBePublic _
                 | MayBePublicWithout _
                 | MustBeProtectedBy _
-                | MustLocksetA
+                | MustLockset
                 | MustBeAtomic
                 | MustBeSingleThreaded _
                 | MustBeUniqueThread
diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index 4aca250ba5..199fae98b0 100644
--- a/src/analyses/commonPriv.ml
+++ b/src/analyses/commonPriv.ml
@@ -66,8 +66,8 @@ struct
             match l with
             | Q.AD.Addr.Addr (v,_) -> VS.add v acc (* always `NoOffset from mutex analysis *)
             | _ -> acc
-          ) (ask.f (Q.MustProtectedVarsA {mutex = m; write = true})) acc
-      ) (ask.f Q.MustLocksetA) VS.empty
+          ) (ask.f (Q.MustProtectedVars {mutex = m; write = true})) acc
+      ) (ask.f Q.MustLockset) VS.empty
     |> VS.elements
 end
 
@@ -127,7 +127,7 @@ struct
     if !AnalysisState.global_initialization then
       Lockset.empty ()
     else
-      let ad = ask.f Queries.MustLocksetA in
+      let ad = ask.f Queries.MustLockset in
       Q.AD.fold (fun mls acc -> Lockset.add mls acc) ad (Lockset.empty ())
 
   (* TODO: reversed SetDomain.Hoare *)
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index 55172c48eb..9cc019db76 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -231,13 +231,13 @@ struct
         true
       else *)
       Mutexes.leq mutex_lockset protecting
-    | Queries.MustLocksetA ->
+    | Queries.MustLockset ->
       let held_locks = Lockset.export_locks (Lockset.filter snd ls) in
       Mutexes.fold (fun addr ls -> Queries.AD.add addr ls) held_locks (Queries.AD.empty ())
     | Queries.MustBeAtomic ->
       let held_locks = Lockset.export_locks (Lockset.filter snd ls) in
       Mutexes.mem (LockDomain.Addr.of_var LF.verifier_atomic_var) held_locks
-    | Queries.MustProtectedVarsA {mutex = m; write} ->
+    | Queries.MustProtectedVars {mutex = m; write} ->
       let protected = GProtected.get ~write Strong (G.protected (ctx.global (V.protected m))) in
       VarSet.fold (fun v acc ->
           Queries.AD.join (Queries.AD.of_var v) acc
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index a160e6dd7b..b10d1b673d 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -80,7 +80,7 @@ type _ t =
   | MayBePublic: maybepublic -> MayBool.t t (* old behavior with write=false *)
   | MayBePublicWithout: maybepublicwithout -> MayBool.t t
   | MustBeProtectedBy: mustbeprotectedby -> MustBool.t t
-  | MustLocksetA: AD.t t
+  | MustLockset: AD.t t
   | MustBeAtomic: MustBool.t t
   | MustBeSingleThreaded: {since_start: bool} -> MustBool.t t
   | MustBeUniqueThread: MustBool.t t
@@ -114,7 +114,7 @@ type _ t =
   | CreatedThreads: ConcDomain.ThreadSet.t t
   | MustJoinedThreads: ConcDomain.MustThreadSet.t t
   | ThreadsJoinedCleanly: MustBool.t t
-  | MustProtectedVarsA: mustprotectedvars -> AD.t t
+  | MustProtectedVars: mustprotectedvars -> AD.t t
   | Invariant: invariant_context -> Invariant.t t
   | InvariantGlobal: Obj.t -> Invariant.t t (** Argument must be of corresponding [Spec.V.t]. *)
   | WarnGlobal: Obj.t -> Unit.t t (** Argument must be of corresponding [Spec.V.t]. *)
@@ -144,7 +144,7 @@ struct
     | MayPointTo _ -> (module AD)
     | ReachableFrom _ -> (module AD)
     | Regions _ -> (module LS)
-    | MustLocksetA -> (module AD)
+    | MustLockset -> (module AD)
     | EvalFunvar _ -> (module LS)
     | ReachableUkTypes _ -> (module TS)
     | MayEscape _ -> (module MayBool)
@@ -179,7 +179,7 @@ struct
     | CreatedThreads ->  (module ConcDomain.ThreadSet)
     | MustJoinedThreads -> (module ConcDomain.MustThreadSet)
     | ThreadsJoinedCleanly -> (module MustBool)
-    | MustProtectedVarsA _ -> (module AD)
+    | MustProtectedVars _ -> (module AD)
     | Invariant _ -> (module Invariant)
     | InvariantGlobal _ -> (module Invariant)
     | WarnGlobal _ -> (module Unit)
@@ -208,7 +208,7 @@ struct
     | MayPointTo _ -> AD.top ()
     | ReachableFrom _ -> AD.top ()
     | Regions _ -> LS.top ()
-    | MustLocksetA -> AD.top ()
+    | MustLockset -> AD.top ()
     | EvalFunvar _ -> LS.top ()
     | ReachableUkTypes _ -> TS.top ()
     | MayEscape _ -> MayBool.top ()
@@ -243,7 +243,7 @@ struct
     | CreatedThreads -> ConcDomain.ThreadSet.top ()
     | MustJoinedThreads -> ConcDomain.MustThreadSet.top ()
     | ThreadsJoinedCleanly -> MustBool.top ()
-    | MustProtectedVarsA _ -> AD.top ()
+    | MustProtectedVars _ -> AD.top ()
     | Invariant _ -> Invariant.top ()
     | InvariantGlobal _ -> Invariant.top ()
     | WarnGlobal _ -> Unit.top ()
@@ -273,7 +273,7 @@ struct
     | Any (MayBePublic _) -> 7
     | Any (MayBePublicWithout _) -> 8
     | Any (MustBeProtectedBy _) -> 9
-    | Any MustLocksetA -> 10
+    | Any MustLockset -> 10
     | Any MustBeAtomic -> 11
     | Any (MustBeSingleThreaded _)-> 12
     | Any MustBeUniqueThread -> 13
@@ -298,7 +298,7 @@ struct
     | Any (Invariant _) -> 36
     | Any (IterSysVars _) -> 37
     | Any (InvariantGlobal _) -> 38
-    | Any (MustProtectedVarsA _) -> 39
+    | Any (MustProtectedVars _) -> 39
     | Any MayAccessed -> 40
     | Any MayBeTainted -> 41
     | Any (PathQuery _) -> 42
@@ -355,7 +355,7 @@ struct
       | Any (InvariantGlobal vi1), Any (InvariantGlobal vi2) -> Stdlib.compare (Hashtbl.hash vi1) (Hashtbl.hash vi2)
       | Any (IterSysVars (vq1, vf1)), Any (IterSysVars (vq2, vf2)) -> VarQuery.compare vq1 vq2 (* not comparing fs *)
       | Any (MutexType m1), Any (MutexType m2) -> Mval.Unit.compare m1 m2
-      | Any (MustProtectedVarsA m1), Any (MustProtectedVarsA m2) -> compare_mustprotectedvars m1 m2
+      | Any (MustProtectedVars m1), Any (MustProtectedVars m2) -> compare_mustprotectedvars m1 m2
       | Any (MayBeModifiedSinceSetjmp e1), Any (MayBeModifiedSinceSetjmp e2) -> JmpBufDomain.BufferEntry.compare e1 e2
       | Any (MustBeSingleThreaded {since_start=s1;}),  Any (MustBeSingleThreaded {since_start=s2;}) -> Stdlib.compare s1 s2
       | Any (TmpSpecial lv1), Any (TmpSpecial lv2) -> Mval.Exp.compare lv1 lv2
@@ -394,7 +394,7 @@ struct
     | Any (Invariant i) -> hash_invariant_context i
     | Any (MutexType m) -> Mval.Unit.hash m
     | Any (InvariantGlobal vi) -> Hashtbl.hash vi
-    | Any (MustProtectedVarsA m) -> hash_mustprotectedvars m
+    | Any (MustProtectedVars m) -> hash_mustprotectedvars m
     | Any (MayBeModifiedSinceSetjmp e) -> JmpBufDomain.BufferEntry.hash e
     | Any (MustBeSingleThreaded {since_start}) -> Hashtbl.hash since_start
     | Any (TmpSpecial lv) -> Mval.Exp.hash lv
@@ -416,7 +416,7 @@ struct
     | Any (MayBePublic x) -> Pretty.dprintf "MayBePublic _"
     | Any (MayBePublicWithout x) -> Pretty.dprintf "MayBePublicWithout _"
     | Any (MustBeProtectedBy x) -> Pretty.dprintf "MustBeProtectedBy _"
-    | Any MustLocksetA -> Pretty.dprintf "MustLocksetA"
+    | Any MustLockset -> Pretty.dprintf "MustLockset"
     | Any MustBeAtomic -> Pretty.dprintf "MustBeAtomic"
     | Any (MustBeSingleThreaded {since_start}) -> Pretty.dprintf "MustBeSingleThreaded since_start=%b" since_start
     | Any MustBeUniqueThread -> Pretty.dprintf "MustBeUniqueThread"
@@ -444,7 +444,7 @@ struct
     | Any CreatedThreads -> Pretty.dprintf "CreatedThreads"
     | Any MustJoinedThreads -> Pretty.dprintf "MustJoinedThreads"
     | Any ThreadsJoinedCleanly -> Pretty.dprintf "ThreadsJoinedCleanly"
-    | Any (MustProtectedVarsA m) -> Pretty.dprintf "MustProtectedVarsA _"
+    | Any (MustProtectedVars m) -> Pretty.dprintf "MustProtectedVars _"
     | Any (Invariant i) -> Pretty.dprintf "Invariant _"
     | Any (WarnGlobal vi) -> Pretty.dprintf "WarnGlobal _"
     | Any (IterSysVars _) -> Pretty.dprintf "IterSysVars _"

From 586a5959a6ba4090f25088c000c94a2a710611c6 Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Tue, 29 Aug 2023 15:00:20 +0300
Subject: [PATCH 06/19] Add EvalFunvarA to queries

---
 src/domains/queries.ml | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index b10d1b673d..1f17b198b6 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -88,6 +88,7 @@ type _ t =
   | ThreadCreateIndexedNode: ThreadNodeLattice.t t
   | MayBeThreadReturn: MayBool.t t
   | EvalFunvar: exp -> LS.t t
+  | EvalFunvarA: exp -> AD.t t
   | EvalInt: exp -> ID.t t
   | EvalStr: exp -> SD.t t
   | EvalLength: exp -> ID.t t (* length of an array or string *)
@@ -146,6 +147,7 @@ struct
     | Regions _ -> (module LS)
     | MustLockset -> (module AD)
     | EvalFunvar _ -> (module LS)
+    | EvalFunvarA _ -> (module AD)
     | ReachableUkTypes _ -> (module TS)
     | MayEscape _ -> (module MayBool)
     | MayBePublic _ -> (module MayBool)
@@ -210,6 +212,7 @@ struct
     | Regions _ -> LS.top ()
     | MustLockset -> AD.top ()
     | EvalFunvar _ -> LS.top ()
+    | EvalFunvarA _ -> AD.top ()
     | ReachableUkTypes _ -> TS.top ()
     | MayEscape _ -> MayBool.top ()
     | MayBePublic _ -> MayBool.top ()
@@ -280,6 +283,7 @@ struct
     | Any CurrentThreadId -> 14
     | Any MayBeThreadReturn -> 15
     | Any (EvalFunvar _) -> 16
+    | Any (EvalFunvarA _) -> 1616
     | Any (EvalInt _) -> 17
     | Any (EvalStr _) -> 18
     | Any (EvalLength _) -> 19
@@ -330,6 +334,7 @@ struct
       | Any (MayBePublicWithout x1), Any (MayBePublicWithout x2) -> compare_maybepublicwithout x1 x2
       | Any (MustBeProtectedBy x1), Any (MustBeProtectedBy x2) -> compare_mustbeprotectedby x1 x2
       | Any (EvalFunvar e1), Any (EvalFunvar e2) -> CilType.Exp.compare e1 e2
+      | Any (EvalFunvarA e1), Any (EvalFunvarA e2) -> CilType.Exp.compare e1 e2
       | Any (EvalInt e1), Any (EvalInt e2) -> CilType.Exp.compare e1 e2
       | Any (EvalStr e1), Any (EvalStr e2) -> CilType.Exp.compare e1 e2
       | Any (EvalLength e1), Any (EvalLength e2) -> CilType.Exp.compare e1 e2
@@ -375,6 +380,7 @@ struct
     | Any (MayBePublicWithout x) -> hash_maybepublicwithout x
     | Any (MustBeProtectedBy x) -> hash_mustbeprotectedby x
     | Any (EvalFunvar e) -> CilType.Exp.hash e
+    | Any (EvalFunvarA e) -> CilType.Exp.hash e
     | Any (EvalInt e) -> CilType.Exp.hash e
     | Any (EvalStr e) -> CilType.Exp.hash e
     | Any (EvalLength e) -> CilType.Exp.hash e
@@ -424,6 +430,7 @@ struct
     | Any ThreadCreateIndexedNode -> Pretty.dprintf "ThreadCreateIndexedNode"
     | Any MayBeThreadReturn -> Pretty.dprintf "MayBeThreadReturn"
     | Any (EvalFunvar e) -> Pretty.dprintf "EvalFunvar %a" CilType.Exp.pretty e
+    | Any (EvalFunvarA e) -> Pretty.dprintf "EvalFunvarA %a" CilType.Exp.pretty e
     | Any (EvalInt e) -> Pretty.dprintf "EvalInt %a" CilType.Exp.pretty e
     | Any (EvalStr e) -> Pretty.dprintf "EvalStr %a" CilType.Exp.pretty e
     | Any (EvalLength e) -> Pretty.dprintf "EvalLength %a" CilType.Exp.pretty e

From f15b41fb6fe467c4b4ef113306bea23008d830a5 Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Tue, 29 Aug 2023 15:08:10 +0300
Subject: [PATCH 07/19] Use EvalFunvarA in base

---
 src/analyses/base.ml | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 4183261ddb..2272a953ca 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1207,6 +1207,11 @@ struct
         let fs = eval_funvar ctx e in
         List.fold_left (fun xs v -> Q.LS.add (v,`NoOffset) xs) (Q.LS.empty ()) fs
       end
+    | Q.EvalFunvarA e ->
+      begin
+        let fs = eval_funvar ctx e in
+        List.fold_left (fun ad v -> Q.AD.join (Q.AD.of_var v) ad) (Q.AD.empty ()) fs
+      end
     | Q.EvalJumpBuf e ->
       begin match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with
         | Address jmp_buf ->

From bdd90b4c4f7cffa3130b126d1a7b746ee1d9d3d4 Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Tue, 29 Aug 2023 15:35:27 +0300
Subject: [PATCH 08/19] Use EvalFunvarA in constraints

---
 src/framework/constraints.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 740d1f85a9..9bbfef9c89 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -299,12 +299,12 @@ struct
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
     match q with
-    | Queries.EvalFunvar e ->
+    | Queries.EvalFunvarA e ->
       let (d,l) = ctx.local in
       if leq0 l then
-        Queries.LS.empty ()
+        Queries.AD.empty ()
       else
-        query' ctx (Queries.EvalFunvar e)
+        query' ctx (Queries.EvalFunvarA e)
     | q -> query' ctx q
 end
 
@@ -754,8 +754,8 @@ struct
         [v]
       | _ ->
         (* Depends on base for query. *)
-        let ls = ctx.ask (Queries.EvalFunvar e) in
-        Queries.LS.fold (fun ((x,_)) xs -> x::xs) ls []
+        let ad = ctx.ask (Queries.EvalFunvarA e) in
+        List.filter_map (fun addr -> Queries.AD.Addr.to_var addr) (Queries.AD.elements ad)
     in
     let one_function f =
       match f.vtype with

From e9e53a71080bcbca164906cd8bef1a1d420c5345 Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Tue, 29 Aug 2023 15:39:07 +0300
Subject: [PATCH 09/19] Remove EvalFunvar queries

---
 src/analyses/base.ml   | 5 -----
 src/domains/queries.ml | 9 +--------
 2 files changed, 1 insertion(+), 13 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 2272a953ca..c272bf1a63 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1202,11 +1202,6 @@ struct
 
   let query ctx (type a) (q: a Q.t): a Q.result =
     match q with
-    | Q.EvalFunvar e ->
-      begin
-        let fs = eval_funvar ctx e in
-        List.fold_left (fun xs v -> Q.LS.add (v,`NoOffset) xs) (Q.LS.empty ()) fs
-      end
     | Q.EvalFunvarA e ->
       begin
         let fs = eval_funvar ctx e in
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index 1f17b198b6..648a0c561e 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -87,7 +87,6 @@ type _ t =
   | CurrentThreadId: ThreadIdDomain.ThreadLifted.t t
   | ThreadCreateIndexedNode: ThreadNodeLattice.t t
   | MayBeThreadReturn: MayBool.t t
-  | EvalFunvar: exp -> LS.t t
   | EvalFunvarA: exp -> AD.t t
   | EvalInt: exp -> ID.t t
   | EvalStr: exp -> SD.t t
@@ -146,7 +145,6 @@ struct
     | ReachableFrom _ -> (module AD)
     | Regions _ -> (module LS)
     | MustLockset -> (module AD)
-    | EvalFunvar _ -> (module LS)
     | EvalFunvarA _ -> (module AD)
     | ReachableUkTypes _ -> (module TS)
     | MayEscape _ -> (module MayBool)
@@ -211,7 +209,6 @@ struct
     | ReachableFrom _ -> AD.top ()
     | Regions _ -> LS.top ()
     | MustLockset -> AD.top ()
-    | EvalFunvar _ -> LS.top ()
     | EvalFunvarA _ -> AD.top ()
     | ReachableUkTypes _ -> TS.top ()
     | MayEscape _ -> MayBool.top ()
@@ -282,8 +279,7 @@ struct
     | Any MustBeUniqueThread -> 13
     | Any CurrentThreadId -> 14
     | Any MayBeThreadReturn -> 15
-    | Any (EvalFunvar _) -> 16
-    | Any (EvalFunvarA _) -> 1616
+    | Any (EvalFunvarA _) -> 16
     | Any (EvalInt _) -> 17
     | Any (EvalStr _) -> 18
     | Any (EvalLength _) -> 19
@@ -333,7 +329,6 @@ struct
       | Any (MayBePublic x1), Any (MayBePublic x2) -> compare_maybepublic x1 x2
       | Any (MayBePublicWithout x1), Any (MayBePublicWithout x2) -> compare_maybepublicwithout x1 x2
       | Any (MustBeProtectedBy x1), Any (MustBeProtectedBy x2) -> compare_mustbeprotectedby x1 x2
-      | Any (EvalFunvar e1), Any (EvalFunvar e2) -> CilType.Exp.compare e1 e2
       | Any (EvalFunvarA e1), Any (EvalFunvarA e2) -> CilType.Exp.compare e1 e2
       | Any (EvalInt e1), Any (EvalInt e2) -> CilType.Exp.compare e1 e2
       | Any (EvalStr e1), Any (EvalStr e2) -> CilType.Exp.compare e1 e2
@@ -379,7 +374,6 @@ struct
     | Any (MayBePublic x) -> hash_maybepublic x
     | Any (MayBePublicWithout x) -> hash_maybepublicwithout x
     | Any (MustBeProtectedBy x) -> hash_mustbeprotectedby x
-    | Any (EvalFunvar e) -> CilType.Exp.hash e
     | Any (EvalFunvarA e) -> CilType.Exp.hash e
     | Any (EvalInt e) -> CilType.Exp.hash e
     | Any (EvalStr e) -> CilType.Exp.hash e
@@ -429,7 +423,6 @@ struct
     | Any CurrentThreadId -> Pretty.dprintf "CurrentThreadId"
     | Any ThreadCreateIndexedNode -> Pretty.dprintf "ThreadCreateIndexedNode"
     | Any MayBeThreadReturn -> Pretty.dprintf "MayBeThreadReturn"
-    | Any (EvalFunvar e) -> Pretty.dprintf "EvalFunvar %a" CilType.Exp.pretty e
     | Any (EvalFunvarA e) -> Pretty.dprintf "EvalFunvarA %a" CilType.Exp.pretty e
     | Any (EvalInt e) -> Pretty.dprintf "EvalInt %a" CilType.Exp.pretty e
     | Any (EvalStr e) -> Pretty.dprintf "EvalStr %a" CilType.Exp.pretty e

From 9fef5946d61b009ea31d2090870ed73a5b8755de Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Tue, 29 Aug 2023 15:39:46 +0300
Subject: [PATCH 10/19] Rename EvalFunvarA -> EvalFunvar

---
 src/analyses/base.ml         |  2 +-
 src/domains/queries.ml       | 14 +++++++-------
 src/framework/constraints.ml |  6 +++---
 3 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index c272bf1a63..5dfbe3c64a 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1202,7 +1202,7 @@ struct
 
   let query ctx (type a) (q: a Q.t): a Q.result =
     match q with
-    | Q.EvalFunvarA e ->
+    | Q.EvalFunvar e ->
       begin
         let fs = eval_funvar ctx e in
         List.fold_left (fun ad v -> Q.AD.join (Q.AD.of_var v) ad) (Q.AD.empty ()) fs
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index 648a0c561e..8626fb9d11 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -87,7 +87,7 @@ type _ t =
   | CurrentThreadId: ThreadIdDomain.ThreadLifted.t t
   | ThreadCreateIndexedNode: ThreadNodeLattice.t t
   | MayBeThreadReturn: MayBool.t t
-  | EvalFunvarA: exp -> AD.t t
+  | EvalFunvar: exp -> AD.t t
   | EvalInt: exp -> ID.t t
   | EvalStr: exp -> SD.t t
   | EvalLength: exp -> ID.t t (* length of an array or string *)
@@ -145,7 +145,7 @@ struct
     | ReachableFrom _ -> (module AD)
     | Regions _ -> (module LS)
     | MustLockset -> (module AD)
-    | EvalFunvarA _ -> (module AD)
+    | EvalFunvar _ -> (module AD)
     | ReachableUkTypes _ -> (module TS)
     | MayEscape _ -> (module MayBool)
     | MayBePublic _ -> (module MayBool)
@@ -209,7 +209,7 @@ struct
     | ReachableFrom _ -> AD.top ()
     | Regions _ -> LS.top ()
     | MustLockset -> AD.top ()
-    | EvalFunvarA _ -> AD.top ()
+    | EvalFunvar _ -> AD.top ()
     | ReachableUkTypes _ -> TS.top ()
     | MayEscape _ -> MayBool.top ()
     | MayBePublic _ -> MayBool.top ()
@@ -279,7 +279,7 @@ struct
     | Any MustBeUniqueThread -> 13
     | Any CurrentThreadId -> 14
     | Any MayBeThreadReturn -> 15
-    | Any (EvalFunvarA _) -> 16
+    | Any (EvalFunvar _) -> 16
     | Any (EvalInt _) -> 17
     | Any (EvalStr _) -> 18
     | Any (EvalLength _) -> 19
@@ -329,7 +329,7 @@ struct
       | Any (MayBePublic x1), Any (MayBePublic x2) -> compare_maybepublic x1 x2
       | Any (MayBePublicWithout x1), Any (MayBePublicWithout x2) -> compare_maybepublicwithout x1 x2
       | Any (MustBeProtectedBy x1), Any (MustBeProtectedBy x2) -> compare_mustbeprotectedby x1 x2
-      | Any (EvalFunvarA e1), Any (EvalFunvarA e2) -> CilType.Exp.compare e1 e2
+      | Any (EvalFunvar e1), Any (EvalFunvar e2) -> CilType.Exp.compare e1 e2
       | Any (EvalInt e1), Any (EvalInt e2) -> CilType.Exp.compare e1 e2
       | Any (EvalStr e1), Any (EvalStr e2) -> CilType.Exp.compare e1 e2
       | Any (EvalLength e1), Any (EvalLength e2) -> CilType.Exp.compare e1 e2
@@ -374,7 +374,7 @@ struct
     | Any (MayBePublic x) -> hash_maybepublic x
     | Any (MayBePublicWithout x) -> hash_maybepublicwithout x
     | Any (MustBeProtectedBy x) -> hash_mustbeprotectedby x
-    | Any (EvalFunvarA e) -> CilType.Exp.hash e
+    | Any (EvalFunvar e) -> CilType.Exp.hash e
     | Any (EvalInt e) -> CilType.Exp.hash e
     | Any (EvalStr e) -> CilType.Exp.hash e
     | Any (EvalLength e) -> CilType.Exp.hash e
@@ -423,7 +423,7 @@ struct
     | Any CurrentThreadId -> Pretty.dprintf "CurrentThreadId"
     | Any ThreadCreateIndexedNode -> Pretty.dprintf "ThreadCreateIndexedNode"
     | Any MayBeThreadReturn -> Pretty.dprintf "MayBeThreadReturn"
-    | Any (EvalFunvarA e) -> Pretty.dprintf "EvalFunvarA %a" CilType.Exp.pretty e
+    | Any (EvalFunvar e) -> Pretty.dprintf "EvalFunvar %a" CilType.Exp.pretty e
     | Any (EvalInt e) -> Pretty.dprintf "EvalInt %a" CilType.Exp.pretty e
     | Any (EvalStr e) -> Pretty.dprintf "EvalStr %a" CilType.Exp.pretty e
     | Any (EvalLength e) -> Pretty.dprintf "EvalLength %a" CilType.Exp.pretty e
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 9bbfef9c89..3ea62a2f4c 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -299,12 +299,12 @@ struct
 
   let query ctx (type a) (q: a Queries.t): a Queries.result =
     match q with
-    | Queries.EvalFunvarA e ->
+    | Queries.EvalFunvar e ->
       let (d,l) = ctx.local in
       if leq0 l then
         Queries.AD.empty ()
       else
-        query' ctx (Queries.EvalFunvarA e)
+        query' ctx (Queries.EvalFunvar e)
     | q -> query' ctx q
 end
 
@@ -754,7 +754,7 @@ struct
         [v]
       | _ ->
         (* Depends on base for query. *)
-        let ad = ctx.ask (Queries.EvalFunvarA e) in
+        let ad = ctx.ask (Queries.EvalFunvar e) in
         List.filter_map (fun addr -> Queries.AD.Addr.to_var addr) (Queries.AD.elements ad)
     in
     let one_function f =

From 8e42121dd7a75bdc44568defb29e44dc5cec66a4 Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Tue, 29 Aug 2023 15:45:30 +0300
Subject: [PATCH 11/19] Add MayBeTaintedA to queries

---
 src/domains/queries.ml | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index 8626fb9d11..2cefb3f318 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -121,6 +121,7 @@ type _ t =
   | IterSysVars: VarQuery.t * Obj.t VarQuery.f -> Unit.t t (** [iter_vars] for [Constraints.FromSpec]. [Obj.t] represents [Spec.V.t]. *)
   | MayAccessed: AccessDomain.EventSet.t t
   | MayBeTainted: LS.t t
+  | MayBeTaintedA: AD.t t
   | MayBeModifiedSinceSetjmp: JmpBufDomain.BufferEntry.t -> VS.t t
   | TmpSpecial:  Mval.Exp.t -> ML.t t
 
@@ -186,6 +187,7 @@ struct
     | IterSysVars _ -> (module Unit)
     | MayAccessed -> (module AccessDomain.EventSet)
     | MayBeTainted -> (module LS)
+    | MayBeTaintedA -> (module AD)
     | MayBeModifiedSinceSetjmp _ -> (module VS)
     | TmpSpecial _ -> (module ML)
 
@@ -250,6 +252,7 @@ struct
     | IterSysVars _ -> Unit.top ()
     | MayAccessed -> AccessDomain.EventSet.top ()
     | MayBeTainted -> LS.top ()
+    | MayBeTaintedA -> AD.top ()
     | MayBeModifiedSinceSetjmp _ -> VS.top ()
     | TmpSpecial _ -> ML.top ()
 end
@@ -301,6 +304,7 @@ struct
     | Any (MustProtectedVars _) -> 39
     | Any MayAccessed -> 40
     | Any MayBeTainted -> 41
+    | Any MayBeTaintedA -> 4141
     | Any (PathQuery _) -> 42
     | Any DYojson -> 43
     | Any (EvalValue _) -> 44
@@ -453,6 +457,7 @@ struct
     | Any (EvalMutexAttr a) ->  Pretty.dprintf "EvalMutexAttr _"
     | Any MayAccessed -> Pretty.dprintf "MayAccessed"
     | Any MayBeTainted -> Pretty.dprintf "MayBeTainted"
+    | Any MayBeTaintedA -> Pretty.dprintf "MayBeTaintedA"
     | Any DYojson -> Pretty.dprintf "DYojson"
     | Any MayBeModifiedSinceSetjmp buf -> Pretty.dprintf "MayBeModifiedSinceSetjmp %a" JmpBufDomain.BufferEntry.pretty buf
     | Any (TmpSpecial lv) -> Pretty.dprintf "TmpSpecial %a" Mval.Exp.pretty lv

From 392834b054524c2eeac202de7b7ffce375717be3 Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Tue, 29 Aug 2023 17:01:14 +0300
Subject: [PATCH 12/19] Use MayBeTaintedA in base

---
 src/analyses/base.ml | 69 ++++++++++++++++++++++++--------------------
 1 file changed, 38 insertions(+), 31 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 5dfbe3c64a..6f0f3a099a 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2386,34 +2386,38 @@ struct
     in
     if get_bool "sem.noreturn.dead_code" && Cil.hasAttribute "noreturn" f.vattr then raise Deadcode else st
 
-  let combine_st ctx (local_st : store) (fun_st : store) (tainted_lvs : Q.LS.t) : store =
+  let combine_st ctx (local_st : store) (fun_st : store) (tainted_lvs : AD.t) : store =
     let ask = (Analyses.ask_of_ctx ctx) in
-    Q.LS.fold (fun (v, o) st ->
-        if CPA.mem v fun_st.cpa then
-          let lval = Mval.Exp.to_cil (v,o) in
-          let address = eval_lv ask ctx.global st lval in
-          let lval_type = (AD.type_of address) in
-          if M.tracing then M.trace "taintPC" "updating %a; type: %a\n" Mval.Exp.pretty (v, o) d_type lval_type;
-          match (CPA.find_opt v (fun_st.cpa)), lval_type with
-          | None, _ -> st
-          (* partitioned arrays cannot be copied by individual lvalues, so if tainted just copy the whole callee value for the array variable *)
-          | Some (Array a), _ when (CArrays.domain_of_t a) = PartitionedDomain -> {st with cpa = CPA.add v (Array a) st.cpa}
-          (* "get" returned "unknown" when applied to a void type, so special case void types. This caused problems with some sv-comps (e.g. regtest 64 11) *)
-          | Some voidVal, TVoid _ -> {st with cpa = CPA.add v voidVal st.cpa}
-          | _, _ -> begin
-              let new_val = get ask ctx.global fun_st address None in
-              if M.tracing then M.trace "taintPC" "update val: %a\n\n" VD.pretty new_val;
-              let st' = set_savetop ~ctx ask ctx.global st address lval_type new_val in
-              let partDep = Dep.find_opt v fun_st.deps in
-              match partDep with
-              | None -> st'
-              (* if a var partitions an array, all cpa-info for arrays it may partition are added from callee to caller *)
-              | Some deps -> {st' with cpa = (Dep.VarSet.fold (fun v accCPA -> let val_opt = CPA.find_opt v fun_st.cpa in
-                                                                match val_opt with
-                                                                | None -> accCPA
-                                                                | Some new_val -> CPA.add v new_val accCPA ) deps st'.cpa)}
-            end
-        else st) tainted_lvs local_st
+    AD.fold (fun addr st ->
+        match addr with
+        | Addr.Addr (v,o) ->
+          if CPA.mem v fun_st.cpa then
+            let lval = Addr.Mval.to_cil (v,o) in
+            let address = eval_lv ask ctx.global st lval in
+            let lval_type = Addr.type_of addr in
+            if M.tracing then M.trace "taintPC" "updating %a; type: %a\n" Addr.Mval.pretty (v,o) d_type lval_type;
+            match (CPA.find_opt v (fun_st.cpa)), lval_type with
+            | None, _ -> st
+            (* partitioned arrays cannot be copied by individual lvalues, so if tainted just copy the whole callee value for the array variable *)
+            | Some (Array a), _ when (CArrays.domain_of_t a) = PartitionedDomain -> {st with cpa = CPA.add v (Array a) st.cpa}
+            (* "get" returned "unknown" when applied to a void type, so special case void types. This caused problems with some sv-comps (e.g. regtest 64 11) *)
+            | Some voidVal, TVoid _ -> {st with cpa = CPA.add v voidVal st.cpa}
+            | _, _ -> begin
+                let new_val = get ask ctx.global fun_st address None in
+                if M.tracing then M.trace "taintPC" "update val: %a\n\n" VD.pretty new_val;
+                let st' = set_savetop ~ctx ask ctx.global st address lval_type new_val in
+                let partDep = Dep.find_opt v fun_st.deps in
+                match partDep with
+                | None -> st'
+                (* if a var partitions an array, all cpa-info for arrays it may partition are added from callee to caller *)
+                | Some deps -> {st' with cpa = (Dep.VarSet.fold (fun v accCPA -> let val_opt = CPA.find_opt v fun_st.cpa in
+                                                                  match val_opt with
+                                                                  | None -> accCPA
+                                                                  | Some new_val -> CPA.add v new_val accCPA ) deps st'.cpa)}
+              end
+          else st
+        | _ -> st
+      ) tainted_lvs local_st
 
   let combine_env ctx lval fexp f args fc au (f_ask: Queries.ask) =
     let combine_one (st: D.t) (fun_st: D.t) =
@@ -2427,10 +2431,10 @@ struct
         (* Remove the return value as this is dealt with separately. *)
         let cpa_noreturn = CPA.remove (return_varinfo ()) fun_st.cpa in
         let ask = (Analyses.ask_of_ctx ctx) in
-        let tainted = f_ask.f Q.MayBeTainted in
-        if M.tracing then M.trace "taintPC" "combine for %s in base: tainted: %a\n" f.svar.vname Q.LS.pretty tainted;
+        let tainted = f_ask.f Q.MayBeTaintedA in
+        if M.tracing then M.trace "taintPC" "combine for %s in base: tainted: %a\n" f.svar.vname AD.pretty tainted;
         if M.tracing then M.trace "taintPC" "combine base:\ncaller: %a\ncallee: %a\n" CPA.pretty st.cpa CPA.pretty fun_st.cpa;
-        if Q.LS.is_top tainted then
+        if AD.is_top tainted then
           let cpa_local = CPA.filter (fun x _ -> not (is_global ask x)) st.cpa in
           let cpa' = CPA.fold CPA.add cpa_noreturn cpa_local in (* add cpa_noreturn to cpa_local *)
           if M.tracing then M.trace "taintPC" "combined: %a\n" CPA.pretty cpa';
@@ -2445,7 +2449,10 @@ struct
           let cpa_caller' = CPA.fold CPA.add cpa_new cpa_caller in
           if M.tracing then M.trace "taintPC" "cpa_caller': %a\n" CPA.pretty cpa_caller';
           (* remove lvals from the tainted set that correspond to variables for which we just added a new mapping from the callee*)
-          let tainted = Q.LS.filter (fun (v, _) ->  not (CPA.mem v cpa_new)) tainted in
+          let tainted = AD.filter (function
+              | Addr.Addr (v,_) -> not (CPA.mem v cpa_new)
+              | _ -> false
+            ) tainted in
           let st_combined = combine_st ctx {st with cpa = cpa_caller'} fun_st tainted in
           if M.tracing then M.trace "taintPC" "combined: %a\n" CPA.pretty st_combined.cpa;
           { fun_st with cpa = st_combined.cpa }

From 224615f63b07448ba45afb79f42c2d8284d4b968 Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Tue, 29 Aug 2023 20:19:38 +0300
Subject: [PATCH 13/19] Use MayBeTaintedA

---
 src/analyses/apron/relationAnalysis.apron.ml |  2 +-
 src/analyses/condVars.ml                     |  2 +-
 src/analyses/modifiedSinceLongjmp.ml         | 10 +++--
 src/analyses/poisonVariables.ml              | 18 +++++----
 src/analyses/taintPartialContexts.ml         | 42 ++++++++------------
 src/analyses/varEq.ml                        | 11 +++--
 src/cdomains/addressDomain.ml                |  2 +
 7 files changed, 46 insertions(+), 41 deletions(-)

diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index ca60e5dc30..64b367be68 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -407,7 +407,7 @@ struct
     let arg_vars = f.sformals |> List.filter (RD.Tracked.varinfo_tracked) |> List.map RV.arg in
     if M.tracing then M.tracel "combine" "relation remove vars: %a\n" (docList (fun v -> Pretty.text (RD.Var.to_string v))) arg_vars;
     RD.remove_vars_with new_fun_rel arg_vars; (* fine to remove arg vars that also exist in caller because unify from new_rel adds them back with proper constraints *)
-    let tainted = f_ask.f Queries.MayBeTainted in
+    let tainted = f_ask.f Queries.MayBeTaintedA in
     let tainted_vars = TaintPartialContexts.conv_varset tainted in
     let new_rel = RD.keep_filter st.rel (fun var ->
         match RV.find_metadata var with
diff --git a/src/analyses/condVars.ml b/src/analyses/condVars.ml
index 04246bf28a..282f5bf020 100644
--- a/src/analyses/condVars.ml
+++ b/src/analyses/condVars.ml
@@ -146,7 +146,7 @@ struct
     (* combine caller's state with globals from callee *)
     (* TODO (precision): globals with only global vars are kept, the rest is lost -> collect which globals are assigned to *)
     (* D.merge (fun k s1 s2 -> match s2 with Some ss2 when (fst k).vglob && D.only_global_exprs ss2 -> s2 | _ when (fst k).vglob -> None | _ -> s1) ctx.local au *)
-    let tainted = TaintPartialContexts.conv_varset (f_ask.f Queries.MayBeTainted) in
+    let tainted = TaintPartialContexts.conv_varset (f_ask.f Queries.MayBeTaintedA) in
     D.only_untainted ctx.local tainted (* tainted globals might have changed... *)
 
   let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
diff --git a/src/analyses/modifiedSinceLongjmp.ml b/src/analyses/modifiedSinceLongjmp.ml
index 0375bd3f74..3cc10196fd 100644
--- a/src/analyses/modifiedSinceLongjmp.ml
+++ b/src/analyses/modifiedSinceLongjmp.ml
@@ -24,10 +24,14 @@ struct
     not v.vglob (* *) && not (BaseUtil.is_volatile v) && v.vstorage <> Static
 
   let relevants_from_ls ls =
-    if Queries.LS.is_top ls then
+    if Queries.AD.is_top ls then
       VS.top ()
     else
-      Queries.LS.fold (fun (v, _) acc -> if is_relevant v then VS.add v acc else acc) ls (VS.empty ())
+      Queries.AD.fold (fun addr acc ->
+          match addr with
+          | Queries.AD.Addr.Addr (v, _) when is_relevant v -> VS.add v acc
+          | _ -> acc
+        ) ls (VS.empty ())
 
   let relevants_from_ad ad =
     (* TODO: what about AD with both known and unknown pointers? *)
@@ -45,7 +49,7 @@ struct
     [ctx.local, D.bot ()] (* enter with bot as opposed to IdentitySpec *)
 
   let combine_env ctx lval fexp f args fc au (f_ask: Queries.ask) =
-    let taintedcallee = relevants_from_ls (f_ask.f Queries.MayBeTainted) in
+    let taintedcallee = relevants_from_ls (f_ask.f Queries.MayBeTaintedA) in
     add_to_all_defined taintedcallee ctx.local
 
   let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask:Queries.ask) : D.t =
diff --git a/src/analyses/poisonVariables.ml b/src/analyses/poisonVariables.ml
index f69e5b2fbc..ddbb6a5a40 100644
--- a/src/analyses/poisonVariables.ml
+++ b/src/analyses/poisonVariables.ml
@@ -15,12 +15,16 @@ struct
 
   let context _ _ = ()
 
-  let check_mval tainted ((v, offset): Queries.LS.elt) =
-    if not v.vglob && VS.mem v tainted then
-      M.warn ~category:(Behavior (Undefined Other)) "Reading poisonous variable %a" CilType.Varinfo.pretty v
+  let check_mval tainted (addr: Queries.AD.elt) =
+    match addr with
+    | Queries.AD.Addr.Addr (v,_) ->
+      if not v.vglob && VS.mem v tainted then
+        M.warn ~category:(Behavior (Undefined Other)) "Reading poisonous variable %a" CilType.Varinfo.pretty v
+    | _ -> ()
 
-  let rem_mval tainted ((v, offset): Queries.LS.elt) = match offset with
-    | `NoOffset -> VS.remove v tainted
+  let rem_mval tainted (addr: Queries.AD.elt) =
+    match addr with
+    | Queries.AD.Addr.Addr (v,`NoOffset) -> VS.remove v tainted
     | _ -> tainted (* If there is an offset, it is a bit harder to remove, as we don't know where the indeterminate value is *)
 
 
@@ -90,7 +94,7 @@ struct
         | ad ->
           Queries.AD.iter (function
               (* Use original access state instead of current with removed written vars. *)
-              | Queries.AD.Addr.Addr (v,o) -> check_mval octx.local (v, ValueDomain.Offs.to_exp o)
+              | Queries.AD.Addr.Addr (v,o) -> check_mval octx.local (Queries.AD.Addr.Addr (v,o))
               | _ -> ()
             ) ad
       end;
@@ -103,7 +107,7 @@ struct
         | ad ->
           Queries.AD.fold (fun addr vs ->
               match addr with
-              | Queries.AD.Addr.Addr (v,o) -> rem_mval vs (v, ValueDomain.Offs.to_exp o)
+              | Queries.AD.Addr.Addr _ -> rem_mval vs addr
               | _ -> vs
             ) ad ctx.local
       end
diff --git a/src/analyses/taintPartialContexts.ml b/src/analyses/taintPartialContexts.ml
index d4ea17d2e0..39183ef087 100644
--- a/src/analyses/taintPartialContexts.ml
+++ b/src/analyses/taintPartialContexts.ml
@@ -6,31 +6,19 @@
 open GoblintCil
 open Analyses
 
-module D = SetDomain.ToppedSet (Mval.Exp) (struct let topname = "All" end)
-
-let to_mvals ad =
-  (* TODO: should one handle ad with unknown pointers separately like in (all) other analyses? *)
-  Queries.AD.fold (fun addr mvals ->
-      match addr with
-      | Queries.AD.Addr.Addr (v,o) -> D.add (v, ValueDomain.Offs.to_exp o) mvals
-      | _ -> mvals
-    ) ad (D.empty ())
+module AD = ValueDomain.AD
 
 module Spec =
 struct
   include Analyses.IdentitySpec
 
   let name () = "taintPartialContexts"
-  module D = D
+  module D = AD
   module C = Lattice.Unit
 
   (* Add Lval or any Lval which it may point to to the set *)
   let taint_lval ctx (lval:lval) : D.t =
-    let d = ctx.local in
-    (match lval with
-     | (Var v, offs) -> D.add (v, Offset.Exp.of_cil offs) d
-     | (Mem e, _) -> D.union (to_mvals (ctx.ask (Queries.MayPointTo e))) d
-    )
+    D.union (ctx.ask (Queries.MayPointTo (AddrOf lval))) ctx.local
 
   (* this analysis is context insensitive*)
   let context _ _ = ()
@@ -45,14 +33,12 @@ struct
     let d_return =
       if D.is_top d then
         d
-      else (
+      else
         let locals = f.sformals @ f.slocals in
-        D.filter (fun (v, _) ->
-            not (List.exists (fun local ->
-                CilType.Varinfo.equal v local && not (ctx.ask (Queries.IsMultiple local))
-              ) locals)
+        D.filter (function
+            | AD.Addr.Addr (v,_) -> not (List.exists (fun local -> CilType.Varinfo.equal v local && not (ctx.ask (Queries.IsMultiple local))) locals)
+            | _ -> false
           ) d
-      )
     in
     if M.tracing then M.trace "taintPC" "returning from %s: tainted vars: %a\n without locals: %a\n" f.svar.vname D.pretty d D.pretty d_return;
     d_return
@@ -94,9 +80,10 @@ struct
       else
         deep_addrs
     in
-    let d = List.fold_left (fun accD addr -> D.union accD (to_mvals (ctx.ask (Queries.MayPointTo addr)))) d shallow_addrs
+    (* TODO: should one handle ad with unknown pointers separately like in (all) other analyses? *)
+    let d = List.fold_left (fun accD addr -> D.union accD (ctx.ask (Queries.MayPointTo addr))) d shallow_addrs
     in
-    let d = List.fold_left (fun accD addr -> D.union accD (to_mvals (ctx.ask (Queries.ReachableFrom addr)))) d deep_addrs
+    let d = List.fold_left (fun accD addr -> D.union accD (ctx.ask (Queries.ReachableFrom addr))) d deep_addrs
     in
     d
 
@@ -111,7 +98,7 @@ struct
 
   let query ctx (type a) (q: a Queries.t) : a Queries.result =
     match q with
-    | MayBeTainted -> (ctx.local : Queries.LS.t)
+    | MayBeTaintedA -> (ctx.local : Queries.AD.t)
     | _ -> Queries.Result.top q
 
 end
@@ -122,5 +109,8 @@ let _ =
 module VS = SetDomain.ToppedSet(Basetype.Variables) (struct let topname = "All" end)
 
 (* Convert Lval set to (less precise) Varinfo set. *)
-let conv_varset (lval_set : Spec.D.t) : VS.t =
-  if Spec.D.is_top lval_set then VS.top () else VS.of_list (List.map (fun (v, _) -> v) (Spec.D.elements lval_set))
+let conv_varset (addr_set : Spec.D.t) : VS.t =
+  if Spec.D.is_top addr_set then 
+    VS.top ()
+  else 
+    VS.of_list (List.filter_map (fun addr -> Spec.D.Addr.to_var_may addr) (Spec.D.elements addr_set))
diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index 77823d99d7..3bfd188aba 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -433,14 +433,19 @@ struct
     | false -> [ctx.local,nst]
 
   let combine_env ctx lval fexp f args fc au (f_ask: Queries.ask) =
-    let tainted = f_ask.f Queries.MayBeTainted in
+    let tainted = f_ask.f Queries.MayBeTaintedA in
     let d_local =
       (* if we are multithreaded, we run the risk, that some mutex protected variables got unlocked, so in this case caller state goes to top
          TODO: !!Unsound, this analysis does not handle this case -> regtest 63 08!! *)
-      if Queries.LS.is_top tainted || not (ctx.ask (Queries.MustBeSingleThreaded {since_start = true})) then
+      if Queries.AD.is_top tainted || not (ctx.ask (Queries.MustBeSingleThreaded {since_start = true})) then
         D.top ()
       else
-        let taint_exp = Queries.ES.of_list (List.map Mval.Exp.to_cil_exp (Queries.LS.elements tainted)) in
+        let taint_exp =
+          Queries.AD.elements tainted
+          |> List.filter_map Addr.to_mval
+          |> List.map Addr.Mval.to_cil_exp
+          |> Queries.ES.of_list
+        in
         D.filter (fun exp -> not (Queries.ES.mem exp taint_exp)) ctx.local
     in
     let d = D.meet au d_local in
diff --git a/src/cdomains/addressDomain.ml b/src/cdomains/addressDomain.ml
index 9f6ee56cbf..5981caf9ea 100644
--- a/src/cdomains/addressDomain.ml
+++ b/src/cdomains/addressDomain.ml
@@ -440,4 +440,6 @@ struct
     let r = narrow x y in
     if M.tracing then M.traceu "ad" "-> %a\n" pretty r;
     r
+
+  let filter f ad = fold (fun addr ad -> if f addr then add addr ad else ad) ad (empty ())
 end

From 26151efbaf3d2cb107a69209ca5414c96d9b1cd2 Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Tue, 29 Aug 2023 20:21:09 +0300
Subject: [PATCH 14/19] Remove MayBeTainted from queries

---
 src/domains/queries.ml | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index 2cefb3f318..65c915e472 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -120,7 +120,6 @@ type _ t =
   | WarnGlobal: Obj.t -> Unit.t t (** Argument must be of corresponding [Spec.V.t]. *)
   | IterSysVars: VarQuery.t * Obj.t VarQuery.f -> Unit.t t (** [iter_vars] for [Constraints.FromSpec]. [Obj.t] represents [Spec.V.t]. *)
   | MayAccessed: AccessDomain.EventSet.t t
-  | MayBeTainted: LS.t t
   | MayBeTaintedA: AD.t t
   | MayBeModifiedSinceSetjmp: JmpBufDomain.BufferEntry.t -> VS.t t
   | TmpSpecial:  Mval.Exp.t -> ML.t t
@@ -186,7 +185,6 @@ struct
     | WarnGlobal _ -> (module Unit)
     | IterSysVars _ -> (module Unit)
     | MayAccessed -> (module AccessDomain.EventSet)
-    | MayBeTainted -> (module LS)
     | MayBeTaintedA -> (module AD)
     | MayBeModifiedSinceSetjmp _ -> (module VS)
     | TmpSpecial _ -> (module ML)
@@ -251,7 +249,6 @@ struct
     | WarnGlobal _ -> Unit.top ()
     | IterSysVars _ -> Unit.top ()
     | MayAccessed -> AccessDomain.EventSet.top ()
-    | MayBeTainted -> LS.top ()
     | MayBeTaintedA -> AD.top ()
     | MayBeModifiedSinceSetjmp _ -> VS.top ()
     | TmpSpecial _ -> ML.top ()
@@ -303,8 +300,7 @@ struct
     | Any (InvariantGlobal _) -> 38
     | Any (MustProtectedVars _) -> 39
     | Any MayAccessed -> 40
-    | Any MayBeTainted -> 41
-    | Any MayBeTaintedA -> 4141
+    | Any MayBeTaintedA -> 41
     | Any (PathQuery _) -> 42
     | Any DYojson -> 43
     | Any (EvalValue _) -> 44
@@ -456,7 +452,6 @@ struct
     | Any (MutexType (v,o)) ->  Pretty.dprintf "MutexType _"
     | Any (EvalMutexAttr a) ->  Pretty.dprintf "EvalMutexAttr _"
     | Any MayAccessed -> Pretty.dprintf "MayAccessed"
-    | Any MayBeTainted -> Pretty.dprintf "MayBeTainted"
     | Any MayBeTaintedA -> Pretty.dprintf "MayBeTaintedA"
     | Any DYojson -> Pretty.dprintf "DYojson"
     | Any MayBeModifiedSinceSetjmp buf -> Pretty.dprintf "MayBeModifiedSinceSetjmp %a" JmpBufDomain.BufferEntry.pretty buf

From 0d3af6cfeb416e039a0058670be588bcf40a74bc Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Tue, 29 Aug 2023 20:23:02 +0300
Subject: [PATCH 15/19] Rename MayBeTaintedA -> MayBeTainted

---
 src/analyses/apron/relationAnalysis.apron.ml |  2 +-
 src/analyses/base.ml                         |  2 +-
 src/analyses/condVars.ml                     |  2 +-
 src/analyses/modifiedSinceLongjmp.ml         |  2 +-
 src/analyses/taintPartialContexts.ml         |  2 +-
 src/analyses/varEq.ml                        |  2 +-
 src/domains/queries.ml                       | 10 +++++-----
 7 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/src/analyses/apron/relationAnalysis.apron.ml b/src/analyses/apron/relationAnalysis.apron.ml
index 64b367be68..ca60e5dc30 100644
--- a/src/analyses/apron/relationAnalysis.apron.ml
+++ b/src/analyses/apron/relationAnalysis.apron.ml
@@ -407,7 +407,7 @@ struct
     let arg_vars = f.sformals |> List.filter (RD.Tracked.varinfo_tracked) |> List.map RV.arg in
     if M.tracing then M.tracel "combine" "relation remove vars: %a\n" (docList (fun v -> Pretty.text (RD.Var.to_string v))) arg_vars;
     RD.remove_vars_with new_fun_rel arg_vars; (* fine to remove arg vars that also exist in caller because unify from new_rel adds them back with proper constraints *)
-    let tainted = f_ask.f Queries.MayBeTaintedA in
+    let tainted = f_ask.f Queries.MayBeTainted in
     let tainted_vars = TaintPartialContexts.conv_varset tainted in
     let new_rel = RD.keep_filter st.rel (fun var ->
         match RV.find_metadata var with
diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 6f0f3a099a..24596f5072 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -2431,7 +2431,7 @@ struct
         (* Remove the return value as this is dealt with separately. *)
         let cpa_noreturn = CPA.remove (return_varinfo ()) fun_st.cpa in
         let ask = (Analyses.ask_of_ctx ctx) in
-        let tainted = f_ask.f Q.MayBeTaintedA in
+        let tainted = f_ask.f Q.MayBeTainted in
         if M.tracing then M.trace "taintPC" "combine for %s in base: tainted: %a\n" f.svar.vname AD.pretty tainted;
         if M.tracing then M.trace "taintPC" "combine base:\ncaller: %a\ncallee: %a\n" CPA.pretty st.cpa CPA.pretty fun_st.cpa;
         if AD.is_top tainted then
diff --git a/src/analyses/condVars.ml b/src/analyses/condVars.ml
index 282f5bf020..04246bf28a 100644
--- a/src/analyses/condVars.ml
+++ b/src/analyses/condVars.ml
@@ -146,7 +146,7 @@ struct
     (* combine caller's state with globals from callee *)
     (* TODO (precision): globals with only global vars are kept, the rest is lost -> collect which globals are assigned to *)
     (* D.merge (fun k s1 s2 -> match s2 with Some ss2 when (fst k).vglob && D.only_global_exprs ss2 -> s2 | _ when (fst k).vglob -> None | _ -> s1) ctx.local au *)
-    let tainted = TaintPartialContexts.conv_varset (f_ask.f Queries.MayBeTaintedA) in
+    let tainted = TaintPartialContexts.conv_varset (f_ask.f Queries.MayBeTainted) in
     D.only_untainted ctx.local tainted (* tainted globals might have changed... *)
 
   let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask: Queries.ask) : D.t =
diff --git a/src/analyses/modifiedSinceLongjmp.ml b/src/analyses/modifiedSinceLongjmp.ml
index 3cc10196fd..fafbe54840 100644
--- a/src/analyses/modifiedSinceLongjmp.ml
+++ b/src/analyses/modifiedSinceLongjmp.ml
@@ -49,7 +49,7 @@ struct
     [ctx.local, D.bot ()] (* enter with bot as opposed to IdentitySpec *)
 
   let combine_env ctx lval fexp f args fc au (f_ask: Queries.ask) =
-    let taintedcallee = relevants_from_ls (f_ask.f Queries.MayBeTaintedA) in
+    let taintedcallee = relevants_from_ls (f_ask.f Queries.MayBeTainted) in
     add_to_all_defined taintedcallee ctx.local
 
   let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask:Queries.ask) : D.t =
diff --git a/src/analyses/taintPartialContexts.ml b/src/analyses/taintPartialContexts.ml
index 39183ef087..660766667e 100644
--- a/src/analyses/taintPartialContexts.ml
+++ b/src/analyses/taintPartialContexts.ml
@@ -98,7 +98,7 @@ struct
 
   let query ctx (type a) (q: a Queries.t) : a Queries.result =
     match q with
-    | MayBeTaintedA -> (ctx.local : Queries.AD.t)
+    | MayBeTainted -> (ctx.local : Queries.AD.t)
     | _ -> Queries.Result.top q
 
 end
diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index 3bfd188aba..1159ff8b1b 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -433,7 +433,7 @@ struct
     | false -> [ctx.local,nst]
 
   let combine_env ctx lval fexp f args fc au (f_ask: Queries.ask) =
-    let tainted = f_ask.f Queries.MayBeTaintedA in
+    let tainted = f_ask.f Queries.MayBeTainted in
     let d_local =
       (* if we are multithreaded, we run the risk, that some mutex protected variables got unlocked, so in this case caller state goes to top
          TODO: !!Unsound, this analysis does not handle this case -> regtest 63 08!! *)
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index 65c915e472..e51ee90f68 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -120,7 +120,7 @@ type _ t =
   | WarnGlobal: Obj.t -> Unit.t t (** Argument must be of corresponding [Spec.V.t]. *)
   | IterSysVars: VarQuery.t * Obj.t VarQuery.f -> Unit.t t (** [iter_vars] for [Constraints.FromSpec]. [Obj.t] represents [Spec.V.t]. *)
   | MayAccessed: AccessDomain.EventSet.t t
-  | MayBeTaintedA: AD.t t
+  | MayBeTainted: AD.t t
   | MayBeModifiedSinceSetjmp: JmpBufDomain.BufferEntry.t -> VS.t t
   | TmpSpecial:  Mval.Exp.t -> ML.t t
 
@@ -185,7 +185,7 @@ struct
     | WarnGlobal _ -> (module Unit)
     | IterSysVars _ -> (module Unit)
     | MayAccessed -> (module AccessDomain.EventSet)
-    | MayBeTaintedA -> (module AD)
+    | MayBeTainted -> (module AD)
     | MayBeModifiedSinceSetjmp _ -> (module VS)
     | TmpSpecial _ -> (module ML)
 
@@ -249,7 +249,7 @@ struct
     | WarnGlobal _ -> Unit.top ()
     | IterSysVars _ -> Unit.top ()
     | MayAccessed -> AccessDomain.EventSet.top ()
-    | MayBeTaintedA -> AD.top ()
+    | MayBeTainted -> AD.top ()
     | MayBeModifiedSinceSetjmp _ -> VS.top ()
     | TmpSpecial _ -> ML.top ()
 end
@@ -300,7 +300,7 @@ struct
     | Any (InvariantGlobal _) -> 38
     | Any (MustProtectedVars _) -> 39
     | Any MayAccessed -> 40
-    | Any MayBeTaintedA -> 41
+    | Any MayBeTainted -> 41
     | Any (PathQuery _) -> 42
     | Any DYojson -> 43
     | Any (EvalValue _) -> 44
@@ -452,7 +452,7 @@ struct
     | Any (MutexType (v,o)) ->  Pretty.dprintf "MutexType _"
     | Any (EvalMutexAttr a) ->  Pretty.dprintf "EvalMutexAttr _"
     | Any MayAccessed -> Pretty.dprintf "MayAccessed"
-    | Any MayBeTaintedA -> Pretty.dprintf "MayBeTaintedA"
+    | Any MayBeTainted -> Pretty.dprintf "MayBeTainted"
     | Any DYojson -> Pretty.dprintf "DYojson"
     | Any MayBeModifiedSinceSetjmp buf -> Pretty.dprintf "MayBeModifiedSinceSetjmp %a" JmpBufDomain.BufferEntry.pretty buf
     | Any (TmpSpecial lv) -> Pretty.dprintf "TmpSpecial %a" Mval.Exp.pretty lv

From cb08d337d202fe2ac6154390f8973f9195c5a7ab Mon Sep 17 00:00:00 2001
From: Simmo Saan <simmo.saan@gmail.com>
Date: Fri, 15 Sep 2023 11:03:07 +0300
Subject: [PATCH 16/19] Simplify some AD conversions, add TODOs

---
 src/analyses/commonPriv.ml           |  2 +-
 src/analyses/poisonVariables.ml      | 11 +++--------
 src/analyses/taintPartialContexts.ml |  2 +-
 src/analyses/varEq.ml                |  3 +--
 src/cdomains/lockDomain.ml           |  2 +-
 src/framework/constraints.ml         |  2 +-
 6 files changed, 8 insertions(+), 14 deletions(-)

diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index 199fae98b0..7d06844c1b 100644
--- a/src/analyses/commonPriv.ml
+++ b/src/analyses/commonPriv.ml
@@ -128,7 +128,7 @@ struct
       Lockset.empty ()
     else
       let ad = ask.f Queries.MustLockset in
-      Q.AD.fold (fun mls acc -> Lockset.add mls acc) ad (Lockset.empty ())
+      Q.AD.fold (fun mls acc -> Lockset.add mls acc) ad (Lockset.empty ()) (* TODO: use AD as Lockset *)
 
   (* TODO: reversed SetDomain.Hoare *)
   module MinLocksets = HoareDomain.Set_LiftTop (MustLockset) (struct let topname = "All locksets" end) (* reverse Lockset because Hoare keeps maximal, but we need minimal *)
diff --git a/src/analyses/poisonVariables.ml b/src/analyses/poisonVariables.ml
index ddbb6a5a40..acd687835e 100644
--- a/src/analyses/poisonVariables.ml
+++ b/src/analyses/poisonVariables.ml
@@ -92,11 +92,8 @@ struct
         | ad when Queries.AD.is_top ad && not (VS.is_empty octx.local) ->
           M.warn ~category:(Behavior (Undefined Other)) "reading unknown memory location, may be tainted!"
         | ad ->
-          Queries.AD.iter (function
-              (* Use original access state instead of current with removed written vars. *)
-              | Queries.AD.Addr.Addr (v,o) -> check_mval octx.local (Queries.AD.Addr.Addr (v,o))
-              | _ -> ()
-            ) ad
+          (* Use original access state instead of current with removed written vars. *)
+          Queries.AD.iter (check_mval octx.local) ad
       end;
       ctx.local
     | Access {ad; kind = Write; _} ->
@@ -106,9 +103,7 @@ struct
           ctx.local
         | ad ->
           Queries.AD.fold (fun addr vs ->
-              match addr with
-              | Queries.AD.Addr.Addr _ -> rem_mval vs addr
-              | _ -> vs
+              rem_mval vs addr
             ) ad ctx.local
       end
     | _ -> ctx.local
diff --git a/src/analyses/taintPartialContexts.ml b/src/analyses/taintPartialContexts.ml
index eaafbf01f5..feb9599977 100644
--- a/src/analyses/taintPartialContexts.ml
+++ b/src/analyses/taintPartialContexts.ml
@@ -113,4 +113,4 @@ let conv_varset (addr_set : Spec.D.t) : VS.t =
   if Spec.D.is_top addr_set then
     VS.top ()
   else
-    VS.of_list (List.filter_map (fun addr -> Spec.D.Addr.to_var_may addr) (Spec.D.elements addr_set))
+    VS.of_list (Spec.D.to_var_may addr_set)
diff --git a/src/analyses/varEq.ml b/src/analyses/varEq.ml
index db164a313c..dcd49c9f02 100644
--- a/src/analyses/varEq.ml
+++ b/src/analyses/varEq.ml
@@ -441,8 +441,7 @@ struct
         D.top ()
       else
         let taint_exp =
-          Queries.AD.elements tainted
-          |> List.filter_map Addr.to_mval
+          Queries.AD.to_mval tainted
           |> List.map Addr.Mval.to_cil_exp
           |> Queries.ES.of_list
         in
diff --git a/src/cdomains/lockDomain.ml b/src/cdomains/lockDomain.ml
index 0de5afc32c..4bc97b34ab 100644
--- a/src/cdomains/lockDomain.ml
+++ b/src/cdomains/lockDomain.ml
@@ -7,7 +7,7 @@ module IdxDom = ValueDomain.IndexDomain
 
 open GoblintCil
 
-module Mutexes = SetDomain.ToppedSet (Addr) (struct let topname = "All mutexes" end) (* TODO HoareDomain? *)
+module Mutexes = SetDomain.ToppedSet (Addr) (struct let topname = "All mutexes" end) (* TODO: AD? *)
 module Simple = Lattice.Reverse (Mutexes)
 module Priorities = IntDomain.Lifted
 
diff --git a/src/framework/constraints.ml b/src/framework/constraints.ml
index 3ea62a2f4c..26fdfac606 100644
--- a/src/framework/constraints.ml
+++ b/src/framework/constraints.ml
@@ -755,7 +755,7 @@ struct
       | _ ->
         (* Depends on base for query. *)
         let ad = ctx.ask (Queries.EvalFunvar e) in
-        List.filter_map (fun addr -> Queries.AD.Addr.to_var addr) (Queries.AD.elements ad)
+        Queries.AD.to_var_may ad (* TODO: don't convert, handle UnknownPtr below *)
     in
     let one_function f =
       match f.vtype with

From a32be380cd024523408b4e1348eab0d65da2842c Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Mon, 18 Sep 2023 15:06:56 +0300
Subject: [PATCH 17/19] Use AddressDomain in eval_funvar

---
 src/analyses/base.ml | 28 ++++++++++------------------
 1 file changed, 10 insertions(+), 18 deletions(-)

diff --git a/src/analyses/base.ml b/src/analyses/base.ml
index 1364c009d5..912e298143 100644
--- a/src/analyses/base.ml
+++ b/src/analyses/base.ml
@@ -1097,20 +1097,15 @@ struct
     | Int x -> ValueDomain.ID.to_int x
     | _ -> None
 
-  let eval_funvar ctx fval: varinfo list =
-    let exception OnlyUnknown in
-    try
-      let fp = eval_fv (Analyses.ask_of_ctx ctx) ctx.global ctx.local fval in
-      if AD.mem Addr.UnknownPtr fp then begin
-        let others = AD.to_var_may fp in
-        if others = [] then raise OnlyUnknown;
-        M.warn ~category:Imprecise "Function pointer %a may contain unknown functions." d_exp fval;
-        dummyFunDec.svar :: others
-      end else
-        AD.to_var_may fp
-    with SetDomain.Unsupported _ | OnlyUnknown ->
-      M.warn ~category:Unsound "Unknown call to function %a." d_exp fval;
-      [dummyFunDec.svar]
+  let eval_funvar ctx fval: Queries.AD.t =
+    let fp = eval_fv (Analyses.ask_of_ctx ctx) ctx.global ctx.local fval in
+    if AD.is_top fp then begin
+      if AD.cardinal fp = 1 then
+        (M.warn ~category:Unsound "Unknown call to function %a." d_exp fval;)
+      else
+        (M.warn ~category:Imprecise "Function pointer %a may contain unknown functions." d_exp fval;)
+    end;
+    fp
 
   (** Evaluate expression as address.
       Avoids expensive Apron EvalInt if the Int result would be useless to us anyway. *)
@@ -1204,10 +1199,7 @@ struct
   let query ctx (type a) (q: a Q.t): a Q.result =
     match q with
     | Q.EvalFunvar e ->
-      begin
-        let fs = eval_funvar ctx e in
-        List.fold_left (fun ad v -> Q.AD.join (Q.AD.of_var v) ad) (Q.AD.empty ()) fs
-      end
+      eval_funvar ctx e
     | Q.EvalJumpBuf e ->
       begin match eval_rv_address (Analyses.ask_of_ctx ctx) ctx.global ctx.local e with
         | Address jmp_buf ->

From 3879fdc2a1f3ced2cc11c15cacd36250219b6744 Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Mon, 18 Sep 2023 15:12:19 +0300
Subject: [PATCH 18/19] Use relevants_from_ad instead of relevants_from_ls

---
 src/analyses/modifiedSinceLongjmp.ml | 16 +++-------------
 1 file changed, 3 insertions(+), 13 deletions(-)

diff --git a/src/analyses/modifiedSinceLongjmp.ml b/src/analyses/modifiedSinceLongjmp.ml
index fafbe54840..5dae8748cb 100644
--- a/src/analyses/modifiedSinceLongjmp.ml
+++ b/src/analyses/modifiedSinceLongjmp.ml
@@ -23,7 +23,8 @@ struct
     (* Only checks for v.vglob on purpose, acessing espaced locals after longjmp is UB like for any local *)
     not v.vglob (* *) && not (BaseUtil.is_volatile v) && v.vstorage <> Static
 
-  let relevants_from_ls ls =
+  let relevants_from_ad ls =
+    (* TODO: what about AD with both known and unknown pointers? *)
     if Queries.AD.is_top ls then
       VS.top ()
     else
@@ -33,23 +34,12 @@ struct
           | _ -> acc
         ) ls (VS.empty ())
 
-  let relevants_from_ad ad =
-    (* TODO: what about AD with both known and unknown pointers? *)
-    if Queries.AD.is_top ad then
-      VS.top ()
-    else
-      Queries.AD.fold (fun addr vs ->
-          match addr with
-          | Queries.AD.Addr.Addr (v,_) -> if is_relevant v then VS.add v vs else vs
-          | _ -> vs
-        ) ad (VS.empty ())
-
   (* transfer functions *)
   let enter ctx (lval: lval option) (f:fundec) (args:exp list) : (D.t * D.t) list =
     [ctx.local, D.bot ()] (* enter with bot as opposed to IdentitySpec *)
 
   let combine_env ctx lval fexp f args fc au (f_ask: Queries.ask) =
-    let taintedcallee = relevants_from_ls (f_ask.f Queries.MayBeTainted) in
+    let taintedcallee = relevants_from_ad (f_ask.f Queries.MayBeTainted) in
     add_to_all_defined taintedcallee ctx.local
 
   let combine_assign ctx (lval:lval option) fexp (f:fundec) (args:exp list) fc (au:D.t) (f_ask:Queries.ask) : D.t =

From 29179999053aa95fcdfe44b3fb83f501be9f7b07 Mon Sep 17 00:00:00 2001
From: karoliineh <karoliine.holter@ut.ee>
Date: Mon, 18 Sep 2023 15:47:48 +0300
Subject: [PATCH 19/19] Use VS domain instead of AD for MustProtectedVars

---
 src/analyses/commonPriv.ml    | 11 +++--------
 src/analyses/mutexAnalysis.ml |  4 ++--
 src/domains/queries.ml        |  6 +++---
 3 files changed, 8 insertions(+), 13 deletions(-)

diff --git a/src/analyses/commonPriv.ml b/src/analyses/commonPriv.ml
index 7d06844c1b..db75455b40 100644
--- a/src/analyses/commonPriv.ml
+++ b/src/analyses/commonPriv.ml
@@ -60,15 +60,10 @@ struct
     ask.f (Q.MustBeProtectedBy {mutex=m; global=x; write=true; protection})
 
   let protected_vars (ask: Q.ask): varinfo list =
-    let module VS = Set.Make (CilType.Varinfo) in
     Q.AD.fold (fun m acc ->
-        Q.AD.fold (fun l acc ->
-            match l with
-            | Q.AD.Addr.Addr (v,_) -> VS.add v acc (* always `NoOffset from mutex analysis *)
-            | _ -> acc
-          ) (ask.f (Q.MustProtectedVars {mutex = m; write = true})) acc
-      ) (ask.f Q.MustLockset) VS.empty
-    |> VS.elements
+        Q.VS.join (ask.f (Q.MustProtectedVars {mutex = m; write = true})) acc
+      ) (ask.f Q.MustLockset) (Q.VS.empty ())
+    |> Q.VS.elements
 end
 
 module MutexGlobals =
diff --git a/src/analyses/mutexAnalysis.ml b/src/analyses/mutexAnalysis.ml
index 9cc019db76..5a61976ef5 100644
--- a/src/analyses/mutexAnalysis.ml
+++ b/src/analyses/mutexAnalysis.ml
@@ -240,8 +240,8 @@ struct
     | Queries.MustProtectedVars {mutex = m; write} ->
       let protected = GProtected.get ~write Strong (G.protected (ctx.global (V.protected m))) in
       VarSet.fold (fun v acc ->
-          Queries.AD.join (Queries.AD.of_var v) acc
-        ) protected (Queries.AD.empty ())
+          Queries.VS.add v acc
+        ) protected (Queries.VS.empty ())
     | Queries.IterSysVars (Global g, f) ->
       f (Obj.repr (V.protecting g)) (* TODO: something about V.protected? *)
     | WarnGlobal g ->
diff --git a/src/domains/queries.ml b/src/domains/queries.ml
index e51ee90f68..3a0e493640 100644
--- a/src/domains/queries.ml
+++ b/src/domains/queries.ml
@@ -114,7 +114,7 @@ type _ t =
   | CreatedThreads: ConcDomain.ThreadSet.t t
   | MustJoinedThreads: ConcDomain.MustThreadSet.t t
   | ThreadsJoinedCleanly: MustBool.t t
-  | MustProtectedVars: mustprotectedvars -> AD.t t
+  | MustProtectedVars: mustprotectedvars -> VS.t t
   | Invariant: invariant_context -> Invariant.t t
   | InvariantGlobal: Obj.t -> Invariant.t t (** Argument must be of corresponding [Spec.V.t]. *)
   | WarnGlobal: Obj.t -> Unit.t t (** Argument must be of corresponding [Spec.V.t]. *)
@@ -179,7 +179,7 @@ struct
     | CreatedThreads ->  (module ConcDomain.ThreadSet)
     | MustJoinedThreads -> (module ConcDomain.MustThreadSet)
     | ThreadsJoinedCleanly -> (module MustBool)
-    | MustProtectedVars _ -> (module AD)
+    | MustProtectedVars _ -> (module VS)
     | Invariant _ -> (module Invariant)
     | InvariantGlobal _ -> (module Invariant)
     | WarnGlobal _ -> (module Unit)
@@ -243,7 +243,7 @@ struct
     | CreatedThreads -> ConcDomain.ThreadSet.top ()
     | MustJoinedThreads -> ConcDomain.MustThreadSet.top ()
     | ThreadsJoinedCleanly -> MustBool.top ()
-    | MustProtectedVars _ -> AD.top ()
+    | MustProtectedVars _ -> VS.top ()
     | Invariant _ -> Invariant.top ()
     | InvariantGlobal _ -> Invariant.top ()
     | WarnGlobal _ -> Unit.top ()