Merge pull request #2002 from goblint/patricia-tree

Use Codex patricia-tree library for base map domain

Author: sim642

dune-project

@@ -39,6 +39,7 @@ Goblint includes analyses for assertions, overflows, deadlocks, etc and can be e
     (ocaml (>= 4.14))
     (goblint-cil (>= 2.0.9)) ; TODO no way to define as pin-depends? Used goblint.opam.template to add it for now. https://github.com/ocaml/dune/issues/3231. Alternatively, removing this line and adding cil as a git submodule and `(vendored_dirs cil)` as ./dune also works. This way, no more need to reinstall the pinned cil opam package on changes. However, then cil is cleaned and has to be rebuild together with goblint.
     (batteries (>= 3.9.0))
+    (patricia-tree (>= 0.13.0))
     (zarith (>= 1.12))
     (yojson (and (>= 2.0.0) (< 3))) ; json-data-encoding has incompatible yojson representation for yojson 3
     (qcheck-core (>= 0.19))

goblint.opam

@@ -41,6 +41,7 @@ depends: [
   "ocaml" {>= "4.14"}
   "goblint-cil" {>= "2.0.9"}
   "batteries" {>= "3.9.0"}
+  "patricia-tree" {>= "0.13.0"}
   "zarith" {>= "1.12"}
   "yojson" {>= "2.0.0" & < "3"}
   "qcheck-core" {>= "0.19"}

goblint.opam.locked

@@ -88,6 +88,7 @@ depends: [
   "odoc-parser" {= "3.0.0" & with-doc}
   "ordering" {= "3.19.1"}
   "ounit2" {= "2.2.7" & with-test}
+  "patricia-tree" {= "0.13.0"}
   "pp" {= "2.0.0"}
   "ppx_blob" {= "0.9.0"}
   "ppx_derivers" {= "1.2.1"}

src/analyses/basePriv.ml

@@ -442,7 +442,7 @@ struct
       (* Additionally filter get_m in case it contains variables it no longer protects. *)
       let is_in_Gm x _ = is_protected_by ask m x in
       let get_m = CPA.filter is_in_Gm get_m in
-      let long_meet m1 m2 = CPA.long_map2 VD.meet m1 m2 in
+      let long_meet m1 m2 = CPA.nonidempotent_union VD.meet m1 m2 in (* TODO: idempotent_union if not using int domain refinement *)
       let meet = long_meet st.cpa get_m in
       if M.tracing then M.tracel "priv" "LOCK %a:\n  get_m: %a\n  meet: %a" LockDomain.MustLock.pretty m CPA.pretty get_m CPA.pretty meet;
       {st with cpa = meet}
@@ -508,7 +508,7 @@ struct
     | VarQuery.Global g -> vf (V.global g)
     | _ -> ()
 
-  let long_meet m1 m2 = CPA.long_map2 VD.meet m1 m2
+  let long_meet m1 m2 = CPA.nonidempotent_union VD.meet m1 m2 (* TODO: idempotent_union if not using int domain refinement *)
 
   let update_if_mem var value m =
     if CPA.mem var m then

src/cdomains/baseDomain.ml

@@ -5,7 +5,7 @@ module VD = ValueDomain.Compound
 
 module CPA =
 struct
-  module M0 = MapDomain.MapBot (Basetype.Variables) (VD)
+  module M0 = MapDomain.PatriciaMapBot (Basetype.Variables) (VD)
   module M =
   struct
     include M0

src/common/util/cilType.ml

@@ -365,6 +365,7 @@ struct
   let equal x y = x.vid = y.vid
   let compare x y = Stdlib.compare x.vid y.vid
   let hash x = x.vid
+  let tag x = x.vid
 
   (* Output *)
   let show x = x.vname

src/domain/disjointDomain.ml

@@ -572,11 +572,17 @@ struct
   let mapi f m = M.map (fun b ->
       B.mapi f b
     ) m
-  let long_map2 f m1 m2 = M.long_map2 (fun b1 b2 ->
-      B.long_map2 f b1 b2
+  let idempotent_union f m1 m2 = M.idempotent_union (fun b1 b2 ->
+      B.idempotent_union f b1 b2
     ) m1 m2
-  let map2 f m1 m2 = M.map2 (fun b1 b2 ->
-      B.map2 f b1 b2
+  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
+    ) m1 m2
+  let nonidempotent_inter f m1 m2 = M.nonidempotent_inter (fun b1 b2 ->
+      B.nonidempotent_inter f b1 b2
     ) m1 m2
   let merge f m1 m2 = failwith "ProjectiveMap.merge" (* TODO: ? *)
 
@@ -627,6 +633,7 @@ struct
 
   let filter p m = failwith "ProjectiveMap.filter"
 
+  let reflexive_subset_domain_for_all2 _ _ _ = failwith "ProjectiveMap.reflexive_subset_domain_for_all2"
   let leq_with_fct _ _ _ = failwith "ProjectiveMap.leq_with_fct"
   let join_with_fct _ _ _ = failwith "ProjectiveMap.join_with_fct"
   let widen_with_fct _ _ _ = failwith "ProjectiveMap.widen_with_fct"
@@ -735,28 +742,29 @@ struct
   let mapi f m = S.map (fun b ->
       B.mapi f b
     ) m
-  let long_map2 f s1 s2 =
+  let nonidempotent_union f s1 s2 =
     let f b2 (s1, acc) =
       let e2 = fst (B.choose b2) in
       let (s1_match, s1_rest) = S.partition (fun b1 -> C.cong (fst (B.choose b1)) e2) s1 in
       let b' = match S.choose s1_match with
         | b1 ->
           assert (S.cardinal s1_match = 1);
-          B.long_map2 f b1 b2
+          B.nonidempotent_union f b1 b2
         | exception Not_found -> b2
       in
       (s1_rest, S.add b' acc)
     in
     let (s1', acc) = S.fold f s2 (s1, empty ()) in
     S.union s1' acc
-  let map2 f s1 s2 =
+  let idempotent_union _ _ _ = failwith "PairwiseMap.idempotent_union" (* TODO: ? *)
+  let nonidempotent_inter f s1 s2 =
     let f b2 (s1, acc) =
       let e2 = fst (B.choose b2) in
       let (s1_match, s1_rest) = S.partition (fun b1 -> C.cong (fst (B.choose b1)) e2) s1 in
       let acc' = match S.choose s1_match with
         | b1 ->
           assert (S.cardinal s1_match = 1);
-          begin match B.map2 f b1 b2 with
+          begin match B.nonidempotent_inter f b1 b2 with
             | b' when B.is_bot b' ->
               acc (* remove bot bucket to preserve invariant *)
             | exception Lattice.BotValue ->
@@ -769,6 +777,7 @@ struct
       (s1_rest, acc')
     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 leq s1 s2 =
@@ -885,6 +894,7 @@ struct
 
   let filter p s = failwith "PairwiseMap.filter"
 
+  let reflexive_subset_domain_for_all2 _ _ _ = failwith "PairwiseMap.reflexive_subset_domain_for_all2"
   let leq_with_fct _ _ _ = failwith "PairwiseMap.leq_with_fct"
   let join_with_fct _ _ _ = failwith "PairwiseMap.join_with_fct"
   let widen_with_fct _ _ _ = failwith "PairwiseMap.widen_with_fct"

src/domain/dune

@@ -8,7 +8,8 @@
    batteries.unthreaded
    goblint_std
    goblint_common
-   goblint-cil)
+   goblint-cil
+   patricia-tree)
  (flags :standard -open Goblint_std)
  (preprocess
   (pps

src/domain/hoareDomain.ml

@@ -277,7 +277,7 @@ struct
 
   let elements (s: t): (key * R.t) list = bindings s
   let of_list (l: (key * R.t) list): t = List.fold_left (fun acc (x, r) -> add x r acc) (empty ()) l
-  let union = long_map2 R.union
+  let union = idempotent_union R.union
 
 
   (* copied & modified from SetDomain.Hoare_NoTop *)