Use patricia-tree library more

src/analyses/commonPriv.ml

@@ -169,7 +169,7 @@ struct
 
   module W =
   struct
-    include MapDomain.MapBot_LiftTop (Basetype.Variables) (MinLocksets)
+    include MapDomain.PatriciaMapBot_LiftTop (Basetype.Variables) (MinLocksets)
     let name () = "W"
   end
 
@@ -178,7 +178,7 @@ struct
     (* Note different Map order! *)
     (* MapTop because default value in P must be top of MinLocksets,
        as opposed to bottom in W. *)
-    include MapDomain.MapTop_LiftBot (Basetype.Variables) (MinLocksets)
+    include MapDomain.PatriciaMapTop_LiftBot (Basetype.Variables) (MinLocksets)
     let name () = "P"
 
     (* TODO: change MinLocksets.exists/top instead? *)

src/analyses/loopTermination.ml

@@ -36,7 +36,7 @@ struct
   end
 
   (** We want to record termination information of loops and use the loop statements for that. *)
-  module G = MapDomain.MapBot (CilType.Stmt) (BoolDomain.MustBool)
+  module G = MapDomain.PatriciaMapBot (CilType.Stmt) (BoolDomain.MustBool)
 
   let startstate _ = ()
   let exitstate = startstate

src/analyses/startStateAnalysis.ml

@@ -12,7 +12,7 @@ module Spec : Analyses.MCPSpec =
 struct
   let name () = "startState"
   module AD = ValueDomain.AD
-  module D = MapDomain.MapBot (Basetype.Variables) (AD)
+  module D = MapDomain.PatriciaMapBot (Basetype.Variables) (AD)
   module C = D
 
   include Analyses.IdentitySpec

src/cdomains/baseDomain.ml

@@ -20,7 +20,7 @@ end
 module PartDeps =
 struct
   module VarSet = SetDomain.Make(Basetype.Variables)
-  include MapDomain.MapBot_LiftTop(Basetype.Variables)(VarSet)
+  include MapDomain.PatriciaMapBot_LiftTop(Basetype.Variables)(VarSet)
   let name () = "array partitioning deps"
 end
 

src/common/util/cilType.ml

@@ -390,6 +390,7 @@ struct
   let equal x y = Varinfo.equal x.svar y.svar
   let compare x y = Varinfo.compare x.svar y.svar
   let hash x = Varinfo.hash x.svar
+  let tag x = Varinfo.tag x.svar
 
   (* Output *)
   let pretty () x = Varinfo.pretty () x.svar
@@ -512,6 +513,7 @@ struct
   let equal x y = x.sid = y.sid
   let compare x y = Stdlib.compare x.sid y.sid
   let hash x = x.sid
+  let tag x = x.sid
 
   (* Output *)
   let pretty () x = dn_stmt () x

src/domain/disjointDomain.ml

@@ -98,19 +98,14 @@ struct
       end
     | None -> m
   let diff m1 m2 =
-    M.merge (fun _ b1 b2 ->
-        match b1, b2 with
-        | Some b1, Some b2 ->
-          begin match B.diff 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'
-          end
-        | Some _, None -> b1
-        | None, _ -> None
+    M.difference (fun b1 b2 ->
+        match B.diff 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 of_list es = List.fold_left (fun acc e ->
@@ -127,32 +122,24 @@ struct
     M.widen m1 m2
 
   let meet m1 m2 =
-    M.merge (fun _ b1 b2 ->
-        match b1, b2 with
-        | Some b1, Some b2 ->
-          begin match B.meet 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'
-          end
-        | _, _ -> None
+    M.nonidempotent_inter_filter (fun b1 b2 -> (* TODO: idempotent_inter_filter if not using int domain refinement *)
+        match B.meet 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 narrow m1 m2 =
-    M.merge (fun _ b1 b2 ->
-        match b1, b2 with
-        | Some b1, Some b2 ->
-          begin match B.narrow 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'
-          end
-        | _, _ -> None
+    M.nonidempotent_inter_filter (fun b1 b2 -> (* TODO: idempotent_inter_filter if not using int domain refinement *)
+        match B.narrow 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 union = join
@@ -578,45 +565,75 @@ 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
+  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_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 nonidempotent_inter f m1 m2 = M.nonidempotent_inter (fun b1 b2 ->
-      B.nonidempotent_inter f b1 b2
+  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_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
+      | 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 merge f m1 m2 = failwith "ProjectiveMap.merge" (* TODO: ? *)
 
   let widen m1 m2 =
     Lattice.assert_valid_widen ~leq ~pretty_diff m1 m2;
     M.widen m1 m2
 
   let meet m1 m2 =
-    M.merge (fun _ b1 b2 ->
-        match b1, b2 with
-        | Some b1, Some b2 ->
-          begin match B.meet 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'
-          end
-        | _, _ -> None
+    M.nonidempotent_inter_filter (fun b1 b2 -> (* TODO: idempotent_inter_filter if not using int domain refinement *)
+        match B.meet 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 narrow m1 m2 =
-    M.merge (fun _ b1 b2 ->
-        match b1, b2 with
-        | Some b1, Some b2 ->
-          begin match B.narrow 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'
-          end
-        | _, _ -> None
+    M.nonidempotent_inter_filter (fun b1 b2 -> (* TODO: idempotent_inter_filter if not using int domain refinement *)
+        match B.narrow 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
 
   include MapDomain.Print (E) (V) (
@@ -778,7 +795,9 @@ struct
     in
     snd (S.fold f s2 (s1, S.empty ()))
   let idempotent_inter _ _ _ = failwith "PairwiseMap.idempotent_inter" (* TODO: ? *)
-  let merge f m1 m2 = failwith "PairwiseMap.merge" (* TODO: ? *)
+  let idempotent_inter_filter _ _ _ = failwith "PairwiseMap.idempotent_inter_filter" (* TODO: ? *)
+  let nonidempotent_inter_filter _ _ _ = failwith "PairwiseMap.nonidempotent_inter_filter" (* TODO: ? *)
+  let difference _ _ _ = failwith "PairwiseMap.difference" (* TODO: ? *)
 
   let leq s1 s2 =
     S.for_all (fun b1 ->