Merge pull request #1095 from goblint/ppx-lattice-easy

Add PPX derivers for lattices of tuple and record types

dune-project

@@ -45,6 +45,7 @@ Goblint includes analyses for assertions, overflows, deadlocks, etc and can be e
     (ppx_deriving (>= 6.0.2))
     (ppx_deriving_hash (>= 0.1.2))
     (ppx_deriving_yojson (>= 3.7.0))
+    (ppxlib (>= 0.30.0)) ; ppx_easy_deriving
     (ounit2 :with-test)
     (qcheck-ounit :with-test)
     (odoc :with-doc)

goblint.opam

@@ -45,6 +45,7 @@ depends: [
   "ppx_deriving" {>= "6.0.2"}
   "ppx_deriving_hash" {>= "0.1.2"}
   "ppx_deriving_yojson" {>= "3.7.0"}
+  "ppxlib" {>= "0.30.0"}
   "ounit2" {with-test}
   "qcheck-ounit" {with-test}
   "odoc" {with-doc}

scripts/goblint-lib-modules.py

@@ -42,6 +42,10 @@
     "Goblint_build_info",
     "Dune_build_info",
 
+    # ppx-s
+    "Ppx_deriving_printable",
+    "Ppx_deriving_lattice",
+
     "MessageCategory", # included in Messages
     "PreValueDomain", # included in ValueDomain
 

src/cdomain/value/cdomains/floatDomain.ml

@@ -1134,7 +1134,7 @@ module FloatDomTupleImpl = struct
   module F1 = FloatIntervalImplLifted
   open Batteries
 
-  type t = F1.t option [@@deriving to_yojson, eq, ord]
+  type t = F1.t option [@@deriving eq, ord, hash]
 
   let name () = "floatdomtuple"
 
@@ -1181,10 +1181,6 @@ module FloatDomTupleImpl = struct
     Option.map_default identity ""
       (mapp { fp= (fun (type a) (module F : FloatDomain with type t = a) x -> F.name () ^ ":" ^ F.show x); } x)
 
-  let hash x =
-    Option.map_default identity 0
-      (mapp { fp= (fun (type a) (module F : FloatDomain with type t = a) -> F.hash); } x)
-
   let of_const fkind =
     create { fi= (fun (type a) (module F : FloatDomain with type t = a) -> F.of_const fkind); }
 

src/cdomain/value/cdomains/intDomain.ml

@@ -3338,7 +3338,7 @@ module IntDomTupleImpl = struct
   module I5 = IntervalSetFunctor (IntOps.BigIntOps)
 
   type t = I1.t option * I2.t option * I3.t option * I4.t option * I5.t option
-  [@@deriving to_yojson, eq, ord]
+  [@@deriving eq, ord, hash]
 
   let name () = "intdomtuple"
 
@@ -3665,7 +3665,6 @@ module IntDomTupleImpl = struct
            |> to_list
            |> String.concat "; "
   let to_yojson = [%to_yojson: Yojson.Safe.t list] % to_list % mapp { fp = fun (type a) (module I:SOverflow with type t = a) x -> I.to_yojson x }
-  let hash = List.fold_left (lxor) 0 % to_list % mapp { fp = fun (type a) (module I:SOverflow with type t = a) -> I.hash }
 
   (* `map/opt_map` are used by `project` *)
   let opt_map b f =

src/cdomains/apron/relationDomain.apron.ml

@@ -146,7 +146,7 @@ end
 type ('a, 'b) relcomponents_t = {
   rel: 'a;
   priv: 'b;
-} [@@deriving eq, ord, hash, to_yojson]
+} [@@deriving eq, ord, hash, to_yojson, relift, lattice]
 
 module RelComponents (D3: S3) (PrivD: Lattice.S):
 sig
@@ -155,13 +155,11 @@ sig
 end =
 struct
   module RD = D3
-  type t = (RD.t, PrivD.t) relcomponents_t [@@deriving eq, ord, hash, to_yojson]
+  type t = (RD.t, PrivD.t) relcomponents_t [@@deriving eq, ord, hash, to_yojson, relift, lattice]
 
   include Printable.Std
   open Pretty
 
-  let relift {rel; priv} = {rel = RD.relift rel; priv = PrivD.relift priv}
-
   let show r =
     let first  = RD.show r.rel in
     let third  = PrivD.show r.priv in
@@ -185,26 +183,11 @@ struct
     let tr = QCheck.pair (RD.arbitrary ()) (PrivD.arbitrary ()) in
     QCheck.map ~rev:to_tuple of_tuple tr
 
-  let bot () = {rel = RD.bot (); priv = PrivD.bot ()}
-  let is_bot {rel; priv} = RD.is_bot rel && PrivD.is_bot priv
-  let top () = {rel = RD.top (); priv = PrivD.bot ()}
-  let is_top {rel; priv} = RD.is_top rel && PrivD.is_top priv
-
-  let leq {rel=x1; priv=x3 } {rel=y1; priv=y3} =
-    RD.leq x1 y1 && PrivD.leq x3 y3
-
   let pretty_diff () (({rel=x1; priv=x3}:t),({rel=y1; priv=y3}:t)): Pretty.doc =
     if not (RD.leq x1 y1) then
       RD.pretty_diff () (x1,y1)
     else
       PrivD.pretty_diff () (x3,y3)
-
-  let op_scheme op1 op3 {rel=x1; priv=x3} {rel=y1; priv=y3}: t =
-    {rel = op1 x1 y1; priv = op3 x3 y3 }
-  let join = op_scheme RD.join PrivD.join
-  let meet = op_scheme RD.meet PrivD.meet
-  let widen = op_scheme RD.widen PrivD.widen
-  let narrow = op_scheme RD.narrow PrivD.narrow
 end
 
 

src/cdomains/baseDomain.ml

@@ -38,7 +38,7 @@ type 'a basecomponents_t = {
   deps: PartDeps.t;
   weak: WeakUpdates.t;
   priv: 'a;
-} [@@deriving eq, ord, hash]
+} [@@deriving eq, ord, hash, relift, lattice]
 
 
 module BaseComponents (PrivD: Lattice.S):
@@ -47,7 +47,7 @@ sig
   val op_scheme: (CPA.t -> CPA.t -> CPA.t) -> (PartDeps.t -> PartDeps.t -> PartDeps.t) -> (WeakUpdates.t -> WeakUpdates.t -> WeakUpdates.t) -> (PrivD.t -> PrivD.t -> PrivD.t) -> t -> t -> t
 end =
 struct
-  type t = PrivD.t basecomponents_t [@@deriving eq, ord, hash]
+  type t = PrivD.t basecomponents_t [@@deriving eq, ord, hash, relift, lattice]
 
   include Printable.Std
   open Pretty
@@ -90,14 +90,6 @@ struct
     let tr = QCheck.quad (CPA.arbitrary ()) (PartDeps.arbitrary ()) (WeakUpdates.arbitrary ()) (PrivD.arbitrary ()) in
     QCheck.map ~rev:to_tuple of_tuple tr
 
-  let bot () = { cpa = CPA.bot (); deps = PartDeps.bot (); weak = WeakUpdates.bot (); priv = PrivD.bot ()}
-  let is_bot {cpa; deps; weak; priv} = CPA.is_bot cpa && PartDeps.is_bot deps && WeakUpdates.is_bot weak && PrivD.is_bot priv
-  let top () = {cpa = CPA.top (); deps = PartDeps.top ();  weak = WeakUpdates.top () ; priv = PrivD.top ()}
-  let is_top {cpa; deps; weak; priv} = CPA.is_top cpa && PartDeps.is_top deps && WeakUpdates.is_top weak && PrivD.is_top priv
-
-  let leq {cpa=x1; deps=x2; weak=x3; priv=x4 } {cpa=y1; deps=y2; weak=y3; priv=y4} =
-    CPA.leq x1 y1 && PartDeps.leq x2 y2 && WeakUpdates.leq x3 y3 && PrivD.leq x4 y4
-
   let pretty_diff () (({cpa=x1; deps=x2; weak=x3; priv=x4}:t),({cpa=y1; deps=y2; weak=y3; priv=y4}:t)): Pretty.doc =
     if not (CPA.leq x1 y1) then
       CPA.pretty_diff () (x1,y1)
@@ -110,13 +102,6 @@ struct
 
   let op_scheme op1 op2 op3 op4 {cpa=x1; deps=x2; weak=x3; priv=x4} {cpa=y1; deps=y2; weak=y3; priv=y4}: t =
     {cpa = op1 x1 y1; deps = op2 x2 y2; weak = op3 x3 y3; priv = op4 x4 y4 }
-  let join = op_scheme CPA.join PartDeps.join WeakUpdates.join PrivD.join
-  let meet = op_scheme CPA.meet PartDeps.meet WeakUpdates.meet PrivD.meet
-  let widen = op_scheme CPA.widen PartDeps.widen WeakUpdates.widen PrivD.widen
-  let narrow = op_scheme CPA.narrow PartDeps.narrow WeakUpdates.narrow PrivD.narrow
-
-  let relift {cpa; deps; weak; priv} =
-    {cpa = CPA.relift cpa; deps = PartDeps.relift deps; weak = WeakUpdates.relift weak; priv = PrivD.relift priv}
 end
 
 module type ExpEvaluator =

src/cdomains/mHP.ml

@@ -11,10 +11,7 @@ type t = {
   tid: ThreadIdDomain.ThreadLifted.t;
   created: ConcDomain.ThreadSet.t;
   must_joined: ConcDomain.ThreadSet.t;
-} [@@deriving eq, ord, hash]
-
-let relift {tid; created; must_joined} =
-  {tid = ThreadIdDomain.ThreadLifted.relift tid; created = ConcDomain.ThreadSet.relift created; must_joined = ConcDomain.ThreadSet.relift must_joined}
+} [@@deriving eq, ord, hash, relift]
 
 let current (ask:Queries.ask) =
   {

src/cdomains/pthreadDomain.ml

@@ -25,7 +25,7 @@ end
 module D = struct
   include Printable.StdLeaf
 
-  type t = { tid : Tid.t; pred : Pred.t; ctx : Ctx.t } [@@deriving eq, ord, hash, to_yojson]
+  type t = { tid : Tid.t; pred : Pred.t; ctx : Ctx.t } [@@deriving eq, ord, hash, relift, to_yojson, lattice]
 
   (** printing *)
   let show x =
@@ -35,26 +35,15 @@ module D = struct
       (Pred.show x.pred)
       (Ctx.show x.ctx)
 
-  include Printable.SimpleShow(struct type nonrec t = t let show = show end) (* TODO: overrides derived to_yojson *)
+  include Printable.SimpleShow (struct
+      type nonrec t = t
+      let show = show
+    end) (* TODO: overrides derived to_yojson *)
 
   let name () = "pthread state"
 
   let make tid pred ctx = { tid; pred; ctx }
-  let bot () = { tid = Tid.bot (); pred = Pred.bot (); ctx = Ctx.bot () }
-  let is_bot x = Tid.is_bot x.tid && Pred.is_bot x.pred && Ctx.is_bot x.ctx
   let any_is_bot x = Tid.is_bot x.tid || Pred.is_bot x.pred
-  let top () = { tid = Tid.top (); pred = Pred.top (); ctx = Ctx.top () }
-  let is_top x = Tid.is_top x.tid && Pred.is_top x.pred && Ctx.is_top x.ctx
-
-  let leq x y = Tid.leq x.tid y.tid && Pred.leq x.pred y.pred && Ctx.leq x.ctx y.ctx
-
-  let op_scheme op1 op2 op3 x y : t =
-    { tid = op1 x.tid y.tid; pred = op2 x.pred y.pred; ctx = op3 x.ctx y.ctx }
-
-  let join = op_scheme Tid.join Pred.join Ctx.join
-  let widen = join
-  let meet = op_scheme Tid.meet Pred.meet Ctx.meet
-  let narrow = meet
 
   let pretty_diff () (x,y) =
     if not (Tid.leq x.tid y.tid) then

src/common/domains/printable.ml

@@ -479,7 +479,7 @@ module ProdConf (C: ProdConfiguration) (Base1: S) (Base2: S)=
 struct
   include C
 
-  type t = Base1.t * Base2.t [@@deriving eq, ord, hash]
+  type t = Base1.t * Base2.t [@@deriving eq, ord, hash, relift]
 
   include Std
 
@@ -518,16 +518,14 @@ struct
     `Assoc [ (Base1.name (), Base1.to_yojson x); (Base2.name (), Base2.to_yojson y) ]
 
   let arbitrary () = QCheck.pair (Base1.arbitrary ()) (Base2.arbitrary ())
-
-  let relift (x,y) = (Base1.relift x, Base2.relift y)
 end
 
 module Prod = ProdConf (struct let expand_fst = true let expand_snd = true end)
 module ProdSimple = ProdConf (struct let expand_fst = false let expand_snd = false end)
 
 module Prod3 (Base1: S) (Base2: S) (Base3: S) =
 struct
-  type t = Base1.t * Base2.t * Base3.t [@@deriving eq, ord, hash]
+  type t = Base1.t * Base2.t * Base3.t [@@deriving eq, ord, hash, relift]
   include Std
 
   let show (x,y,z) =
@@ -569,39 +567,9 @@ struct
 
   let name () = Base1.name () ^ " * " ^ Base2.name () ^ " * " ^ Base3.name ()
 
-  let relift (x,y,z) = (Base1.relift x, Base2.relift y, Base3.relift z)
   let arbitrary () = QCheck.triple (Base1.arbitrary ()) (Base2.arbitrary ()) (Base3.arbitrary ())
 end
 
-module Prod4 (Base1: S) (Base2: S) (Base3: S) (Base4: S) = struct
-  type t = Base1.t * Base2.t * Base3.t * Base4.t [@@deriving eq, ord, hash]
-  include Std
-
-  let show (x,y,z,w) = "(" ^ Base1.show x ^ ", " ^ Base2.show y ^ ", " ^ Base3.show z ^ ", " ^ Base4.show w ^ ")"
-
-  let pretty () (x,y,z,w) =
-    text "(" ++
-    Base1.pretty () x
-    ++ text ", " ++
-    Base2.pretty () y
-    ++ text ", " ++
-    Base3.pretty () z
-    ++ text ", " ++
-    Base4.pretty () w
-    ++ text ")"
-
-  let printXml f (x,y,z,w) =
-    BatPrintf.fprintf f "<value>\n<map>\n<key>\n%s\n</key>\n%a<key>\n%s\n</key>\n%a<key>\n%s\n</key>\n%a<key>\n%s\n</key>\n%a</map>\n</value>\n" (XmlUtil.escape (Base1.name ())) Base1.printXml x (XmlUtil.escape (Base2.name ())) Base2.printXml y (XmlUtil.escape (Base3.name ())) Base3.printXml z (XmlUtil.escape (Base4.name ())) Base4.printXml w
-
-  let to_yojson (x, y, z, w) =
-    `Assoc [ (Base1.name (), Base1.to_yojson x); (Base2.name (), Base2.to_yojson y); (Base3.name (), Base3.to_yojson z); (Base4.name (), Base4.to_yojson w) ]
-
-  let name () = Base1.name () ^ " * " ^ Base2.name () ^ " * " ^ Base3.name () ^ " * " ^ Base4.name ()
-
-  let relift (x,y,z,w) = (Base1.relift x, Base2.relift y, Base3.relift z, Base4.relift w)
-  let arbitrary () = QCheck.quad (Base1.arbitrary ()) (Base2.arbitrary ()) (Base3.arbitrary ()) (Base4.arbitrary ())
-end
-
 module PQueue (Base: S) =
 struct
   type t = Base.t BatDeque.dq

src/common/dune

@@ -23,7 +23,8 @@
   (pps
     ppx_deriving.std
     ppx_deriving_hash
-    ppx_deriving_yojson))
+    ppx_deriving_yojson
+    ppx_deriving_printable))
  (instrumentation (backend bisect_ppx)))
 
 (documentation)

src/domain/dune

@@ -14,7 +14,8 @@
   (pps
     ppx_deriving.std
     ppx_deriving_hash
-    ppx_deriving_yojson))
+    ppx_deriving_yojson
+    ppx_deriving_lattice))
  (instrumentation (backend bisect_ppx)))
 
 (documentation)

src/domain/lattice.ml

@@ -422,27 +422,17 @@ module Lift2 = Lift2Conf (Printable.DefaultConf)
 
 module ProdConf (C: Printable.ProdConfiguration) (Base1: S) (Base2: S) =
 struct
-  include Printable.ProdConf (C) (Base1) (Base2)
-
-  let bot () = (Base1.bot (), Base2.bot ())
-  let is_bot (x1,x2) = Base1.is_bot x1 && Base2.is_bot x2
-  let top () = (Base1.top (), Base2.top ())
-  let is_top (x1,x2) = Base1.is_top x1 && Base2.is_top x2
-
-  let leq (x1,x2) (y1,y2) = Base1.leq x1 y1 && Base2.leq x2 y2
+  open struct (* open to avoid leaking P and causing conflicts *)
+    module P = Printable.ProdConf (C) (Base1) (Base2)
+  end
+  type t = Base1.t * Base2.t [@@deriving lattice]
+  include (P: module type of P with type t := t)
 
   let pretty_diff () ((x1,x2:t),(y1,y2:t)): Pretty.doc =
     if Base1.leq x1 y1 then
       Base2.pretty_diff () (x2,y2)
     else
       Base1.pretty_diff () (x1,y1)
-
-  let op_scheme op1 op2 (x1,x2) (y1,y2): t = (op1 x1 y1, op2 x2 y2)
-  let join = op_scheme Base1.join Base2.join
-  let meet = op_scheme Base1.meet Base2.meet
-  let narrow = op_scheme Base1.narrow Base2.narrow
-  let widen = op_scheme Base1.widen Base2.widen
-
 end
 
 
@@ -451,14 +441,11 @@ module ProdSimple = ProdConf (struct let expand_fst = false let expand_snd = fal
 
 module Prod3 (Base1: S) (Base2: S) (Base3: S) =
 struct
-  include Printable.Prod3 (Base1) (Base2) (Base3)
-
-  let bot () = (Base1.bot (), Base2.bot (), Base3.bot ())
-  let is_bot (x1,x2,x3) = Base1.is_bot x1 && Base2.is_bot x2 && Base3.is_bot x3
-  let top () = (Base1.top (), Base2.top (), Base3.top ())
-  let is_top (x1,x2,x3) = Base1.is_top x1 && Base2.is_top x2 && Base3.is_top x3
-
-  let leq (x1,x2,x3) (y1,y2,y3) = Base1.leq x1 y1 && Base2.leq x2 y2 && Base3.leq x3 y3
+  open struct (* open to avoid leaking P and causing conflicts *)
+    module P = Printable.Prod3 (Base1) (Base2) (Base3)
+  end
+  type t = Base1.t * Base2.t * Base3.t [@@deriving lattice]
+  include (P: module type of P with type t := t)
 
   let pretty_diff () ((x1,x2,x3:t),(y1,y2,y3:t)): Pretty.doc =
     if not (Base1.leq x1 y1) then
@@ -467,39 +454,6 @@ struct
       Base2.pretty_diff () (x2,y2)
     else
       Base3.pretty_diff () (x3,y3)
-
-  let op_scheme op1 op2 op3 (x1,x2,x3) (y1,y2,y3): t = (op1 x1 y1, op2 x2 y2, op3 x3 y3)
-  let join = op_scheme Base1.join Base2.join Base3.join
-  let meet = op_scheme Base1.meet Base2.meet Base3.meet
-  let widen = op_scheme Base1.widen Base2.widen Base3.widen
-  let narrow = op_scheme Base1.narrow Base2.narrow Base3.narrow
-end
-
-module Prod4 (Base1: S) (Base2: S) (Base3: S) (Base4: S) =
-struct
-  include Printable.Prod4 (Base1) (Base2) (Base3) (Base4)
-
-  let bot () = (Base1.bot (), Base2.bot (), Base3.bot (), Base4.bot ())
-  let is_bot (x1,x2,x3,x4) = Base1.is_bot x1 && Base2.is_bot x2 && Base3.is_bot x3 && Base4.is_bot x4
-  let top () = (Base1.top (), Base2.top (), Base3.top (), Base4.top ())
-  let is_top (x1,x2,x3,x4) = Base1.is_top x1 && Base2.is_top x2 && Base3.is_top x3 && Base4.is_top x4
-  let leq (x1,x2,x3,x4) (y1,y2,y3,y4) = Base1.leq x1 y1 && Base2.leq x2 y2 && Base3.leq x3 y3 && Base4.leq x4 y4
-
-  let pretty_diff () ((x1,x2,x3,x4:t),(y1,y2,y3,y4:t)): Pretty.doc =
-    if not (Base1.leq x1 y1) then
-      Base1.pretty_diff () (x1,y1)
-    else if not (Base2.leq x2 y2) then
-      Base2.pretty_diff () (x2,y2)
-    else if not (Base3.leq x3 y3) then
-      Base3.pretty_diff () (x3,y3)
-    else
-      Base4.pretty_diff () (x4,y4)
-
-  let op_scheme op1 op2 op3 op4 (x1,x2,x3,x4) (y1,y2,y3,y4): t = (op1 x1 y1, op2 x2 y2, op3 x3 y3, op4 x4 y4)
-  let join = op_scheme Base1.join Base2.join Base3.join Base4.join
-  let meet = op_scheme Base1.meet Base2.meet Base3.meet Base4.meet
-  let widen = op_scheme Base1.widen Base2.widen Base3.widen Base4.widen
-  let narrow = op_scheme Base1.narrow Base2.narrow Base3.narrow Base4.narrow
 end
 
 module LiftBot (Base : S) =