Fix DisjointDomain TODOs about bot buckets

Author: sim642

src/domain/disjointDomain.ml

@@ -565,17 +565,41 @@ struct
   let nonidempotent_union f m1 m2 = M.nonidempotent_union (fun b1 b2 ->
       B.nonidempotent_union f b1 b2
     ) m1 m2
-  let idempotent_inter f m1 m2 = M.idempotent_inter (fun b1 b2 ->
-      B.idempotent_inter f b1 b2 (* TODO: should remove bot bucket to preserve invariant? *)
+  let idempotent_inter f m1 m2 = M.idempotent_inter_filter (fun b1 b2 ->
+      match B.idempotent_inter f b1 b2 with
+      | b' when B.is_bot b' ->
+        None (* remove bot bucket to preserve invariant *)
+      | exception Lattice.BotValue ->
+        None (* remove bot bucket to preserve invariant *)
+      | b' ->
+        Some b'
     ) m1 m2
-  let nonidempotent_inter f m1 m2 = M.nonidempotent_inter (fun b1 b2 ->
-      B.nonidempotent_inter f b1 b2 (* TODO: should remove bot bucket to preserve invariant? *)
+  let nonidempotent_inter f m1 m2 = M.nonidempotent_inter_filter (fun b1 b2 ->
+      match B.nonidempotent_inter f b1 b2 with
+      | b' when B.is_bot b' ->
+        None (* remove bot bucket to preserve invariant *)
+      | exception Lattice.BotValue ->
+        None (* remove bot bucket to preserve invariant *)
+      | b' ->
+        Some b'
     ) m1 m2
-  let idempotent_inter_filter f m1 m2 = M.idempotent_inter (fun b1 b2 ->
-      B.idempotent_inter_filter f b1 b2 (* TODO: should remove bot bucket to preserve invariant? *)
+  let idempotent_inter_filter f m1 m2 = M.idempotent_inter_filter (fun b1 b2 ->
+      match B.idempotent_inter_filter f b1 b2 with
+      | b' when B.is_bot b' ->
+        None (* remove bot bucket to preserve invariant *)
+      | exception Lattice.BotValue ->
+        None (* remove bot bucket to preserve invariant *)
+      | b' ->
+        Some b'
     ) m1 m2
-  let nonidempotent_inter_filter f m1 m2 = M.nonidempotent_inter (fun b1 b2 ->
-      B.nonidempotent_inter_filter f b1 b2 (* TODO: should remove bot bucket to preserve invariant? *)
+  let nonidempotent_inter_filter f m1 m2 = M.nonidempotent_inter_filter (fun b1 b2 ->
+      match B.nonidempotent_inter_filter f b1 b2 with
+      | b' when B.is_bot b' ->
+        None (* remove bot bucket to preserve invariant *)
+      | exception Lattice.BotValue ->
+        None (* remove bot bucket to preserve invariant *)
+      | b' ->
+        Some b'
     ) m1 m2
   let difference f m1 m2 = M.difference (fun b1 b2 ->
       match B.difference f b1 b2 with