Merge pull request #542 from goblint/ppx_deriving_hash

Add sim642/ppx_deriving_hash

dune-project

@@ -31,6 +31,7 @@
     qcheck-core
     (ppx_distr_guards (>= 0.2))
     ppx_deriving
+    ppx_deriving_hash
     ppx_deriving_yojson
     (ppx_blob (>= 0.6.0))
     (ocaml-monadic (>= 0.5))

goblint.opam

@@ -27,6 +27,7 @@ depends: [
   "qcheck-core"
   "ppx_distr_guards" {>= "0.2"}
   "ppx_deriving"
+  "ppx_deriving_hash"
   "ppx_deriving_yojson"
   "ppx_blob" {>= "0.6.0"}
   "ocaml-monadic" {>= "0.5"}

goblint.opam.locked

@@ -66,6 +66,7 @@ depends: [
   "ppx_blob" {= "0.7.2"}
   "ppx_derivers" {= "1.2.1"}
   "ppx_deriving" {= "5.2.1"}
+  "ppx_deriving_hash" {= "0.1.1"}
   "ppx_deriving_yojson" {= "3.6.1"}
   "ppx_distr_guards" {= "0.3"}
   "ppxlib" {= "0.23.0"}

src/analyses/base.ml

@@ -80,9 +80,6 @@ struct
    * Helpers
    **************************************************************************)
 
-  let hash    (x,_)             = Hashtbl.hash x
-  let leq     (x1,_) (y1,_) = CPA.leq   x1 y1
-
   let is_privglob v = GobConfig.get_bool "annotation.int.privglobs" && v.vglob
 
   let project_val p_opt value is_glob =

src/analyses/tutorials/signs.ml

@@ -8,7 +8,7 @@ module Signs =
 struct
   include Printable.Std
 
-  type t = Neg | Zero | Pos [@@deriving eq, ord, to_yojson]
+  type t = Neg | Zero | Pos [@@deriving eq, ord, hash, to_yojson]
   let name () = "signs"
   let show x = match x with
     | Neg -> "-"
@@ -19,7 +19,6 @@ struct
       type nonrec t = t
       let show = show
     end)
-  let hash = Hashtbl.hash
 
   (* TODO: An attempt to abstract integers, but it's just a little wrong... *)
   let of_int i =

src/cdomains/apron/apronDomain.apron.ml

@@ -881,7 +881,7 @@ sig
   val eval_int : t -> exp -> IntDomain.IntDomTuple.t
 end
 
-type ('a, 'b) aproncomponents_t = { apr : 'a; priv : 'b; } [@@deriving eq, ord, to_yojson]
+type ('a, 'b) aproncomponents_t = { apr : 'a; priv : 'b; } [@@deriving eq, ord, hash, to_yojson]
 
 module D2 (Man: Manager) : S2 with module Man = Man =
 struct
@@ -897,11 +897,10 @@ sig
 end =
 struct
   module AD = D2
-  type t = (D2.t, PrivD.t) aproncomponents_t [@@deriving eq, ord, to_yojson]
+  type t = (D2.t, PrivD.t) aproncomponents_t [@@deriving eq, ord, hash, to_yojson]
 
   include Printable.Std
   open Pretty
-  let hash (r: t)  = D2.hash r.apr + PrivD.hash r.priv * 33
 
   let show r =
     let first  = D2.show r.apr in

src/cdomains/arincDomain.ml

@@ -28,10 +28,11 @@ module Pred = struct
 end
 
 (* define record type here so that fields are accessable outside of D *)
-type process = { pid: Pid.t; pri: Pri.t; per: Per.t; cap: Cap.t; pmo: Pmo.t; pre: PrE.t; pred: Pred.t; ctx: Ctx.t } [@@deriving eq, ord, to_yojson]
+type process = { pid: Pid.t; pri: Pri.t; per: Per.t; cap: Cap.t; pmo: Pmo.t; pre: PrE.t; pred: Pred.t; ctx: Ctx.t } [@@deriving eq, ord, hash, to_yojson]
+
 module D =
 struct
-  type t = process [@@deriving eq, ord, to_yojson]
+  type t = process [@@deriving eq, ord, hash, to_yojson]
   include Printable.Std
 
   let name () = "ARINC state"
@@ -42,9 +43,6 @@ struct
       type nonrec t = t
       let show = show
     end)
-  (* Printable.S *)
-  (* let hash = Hashtbl.hash *)
-  let hash x = Hashtbl.hash (Pid.hash x.pid, Pri.hash x.pri, Per.hash x.per, Cap.hash x.cap, Pmo.hash x.pmo, PrE.hash x.pre, Pred.hash x.pred, Ctx.hash x.ctx)
 
   (* modify fields *)
   let pid f d = { d with pid = f d.pid }

src/cdomains/baseDomain.ml

@@ -75,20 +75,19 @@ type 'a basecomponents_t = {
   deps: PartDeps.t;
   weak: WeakUpdates.t;
   priv: 'a;
-} [@@deriving eq, ord]
+} [@@deriving eq, ord, hash]
+
 
 module BaseComponents (PrivD: Lattice.S):
 sig
   include Lattice.S with type t = PrivD.t basecomponents_t
   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]
+  type t = PrivD.t basecomponents_t [@@deriving eq, ord, hash]
 
   include Printable.Std
   open Pretty
-  let hash r  = CPA.hash r.cpa + PartDeps.hash r.deps * 17 + WeakUpdates.hash r.weak * 51 + PrivD.hash r.priv * 33
-
 
   let show r =
     let first  = CPA.show r.cpa in

src/cdomains/basetype.ml

@@ -50,8 +50,7 @@ module RawStrings: Printable.S with type t = string =
 struct
   include Printable.Std
   open Pretty
-  type t = string [@@deriving eq, ord, to_yojson]
-  let hash (x:t) = Hashtbl.hash x
+  type t = string [@@deriving eq, ord, hash, to_yojson]
   let show x = "\"" ^ x ^ "\""
   let pretty () x = text (show x)
   let name () = "raw strings"
@@ -68,8 +67,7 @@ module RawBools: Printable.S with type t = bool =
 struct
   include Printable.Std
   open Pretty
-  type t = bool [@@deriving eq, ord, to_yojson]
-  let hash (x:t) = Hashtbl.hash x
+  type t = bool [@@deriving eq, ord, hash, to_yojson]
   let show (x:t) =  if x then "true" else "false"
   let pretty () x = text (show x)
   let name () = "raw bools"

src/cdomains/exp.ml

@@ -237,8 +237,7 @@ end
 module LockingPattern =
 struct
   include Printable.Std
-  type t = Exp.t * Exp.t * Exp.t [@@deriving eq, ord, to_yojson]
-  let hash = Hashtbl.hash
+  type t = Exp.t * Exp.t * Exp.t [@@deriving eq, ord, hash, to_yojson]
   let name () = "Per-Element locking triple"
 
   let pretty () (x,y,z) = text "(" ++ d_exp () x ++ text ", "++ d_exp () y ++ text ", "++ d_exp () z ++ text ")"

src/cdomains/fileDomain.ml

@@ -5,8 +5,8 @@ module D = LvalMapDomain
 
 module Val =
 struct
-  type mode = Read | Write
-  type s = Open of string*mode | Closed | Error
+  type mode = Read | Write [@@deriving eq, ord, hash]
+  type s = Open of string*mode | Closed | Error [@@deriving eq, ord, hash]
   let name = "File handles"
   let var_state = Closed
   let string_of_mode = function Read -> "Read" | Write -> "Write"
@@ -19,7 +19,6 @@ struct
   let opened   s = s <> Closed && s <> Error
   let closed   s = s = Closed
   let writable s = match s with Open((_,Write)) -> true | _ -> false
-  let compare = compare
 end
 
 

src/cdomains/intDomain.ml

@@ -280,7 +280,7 @@ module IntDomLifter (I : S) =
 struct
   open Cil
   type int_t = I.int_t
-  type t = { v : I.t; ikind : ikind }
+  type t = { v : I.t; ikind : (ikind [@equal (=)] [@compare Stdlib.compare] [@hash fun x -> Hashtbl.hash x]) } [@@deriving eq, ord, hash]
 
   (* Helper functions *)
   let check_ikinds x y = if x.ikind <> y.ikind then raise (IncompatibleIKinds ("ikinds " ^ Prelude.Ana.sprint Cil.d_ikind x.ikind ^ " and " ^ Prelude.Ana.sprint Cil.d_ikind y.ikind ^ " are incompatible. Values: " ^ Prelude.Ana.sprint I.pretty x.v ^ " and " ^ Prelude.Ana.sprint I.pretty y.v)) else ()
@@ -304,30 +304,7 @@ struct
   let meet = lift2 I.meet
   let widen = lift2 I.widen
   let narrow = lift2 I.narrow
-  let equal x y = if x.ikind <> y.ikind then false else I.equal x.v y.v
-
-  let hash x =
-    let ikind_to_int (ikind: ikind) = match ikind with (* TODO replace with `int_of_string % Batteries.dump` or derive *)
-    | IChar 	-> 0
-    | ISChar 	-> 1
-    | IUChar 	-> 2
-    | IBool 	-> 3
-    | IInt 	  -> 4
-    | IUInt 	-> 5
-    | IShort 	-> 6
-    | IUShort -> 7
-    | ILong 	-> 8
-    | IULong 	-> 9
-    | ILongLong -> 10
-    | IULongLong -> 11
-    | IInt128 -> 12
-    | IUInt128 -> 13
-    in
-    3 * (I.hash x.v) + 5 * (ikind_to_int x.ikind)
-  let compare x y = let ik_c = compare x.ikind y.ikind in
-    if ik_c <> 0
-      then ik_c
-      else I.compare x.v y.v
+
   let show x = I.show x.v  (* TODO add ikind to output *)
   let pretty () x = I.pretty () x.v (* TODO add ikind to output *)
   let pretty_diff () (x, y) = I.pretty_diff () (x.v, y.v) (* TODO check ikinds, add them to output *)
@@ -495,7 +472,6 @@ module Std (B: sig
   include Printable.Std
   let name = B.name (* overwrite the one from Printable.Std *)
   open B
-  let hash = Hashtbl.hash
   let is_top x = failwith "is_top not implemented for IntDomain.Std"
   let is_bot x = B.equal x (bot_of Cil.IInt) (* Here we assume that the representation of bottom is independent of the ikind
                                                 This may be true for intdomain implementations, but not e.g. for IntDomLifter. *)
@@ -517,7 +493,7 @@ module IntervalFunctor(Ints_t : IntOps.IntOps): S with type int_t = Ints_t.t and
 struct
   let name () = "intervals"
   type int_t = Ints_t.t
-  type t = (Ints_t.t * Ints_t.t) option [@@deriving eq, ord]
+  type t = (Ints_t.t * Ints_t.t) option [@@deriving eq, ord, hash]
 
   let min_int ik = Ints_t.of_bigint @@ fst @@ Size.range ik
   let max_int ik = Ints_t.of_bigint @@ snd @@ Size.range ik
@@ -937,7 +913,7 @@ module Integers(Ints_t : IntOps.IntOps): IkindUnawareS with type t = Ints_t.t an
 struct
   include Printable.Std
   let name () = "integers"
-  type t = Ints_t.t [@@deriving eq, ord]
+  type t = Ints_t.t [@@deriving eq, ord, hash]
   type int_t = Ints_t.t
   let top () = raise Unknown
   let bot () = raise Error
@@ -946,7 +922,6 @@ struct
   let show (x: Ints_t.t) = if (Ints_t.to_int64 x) = GU.inthack then "*" else Ints_t.to_string x
 
   include Std (struct type nonrec t = t let name = name let top_of = top_of let bot_of = bot_of let show = show let equal = equal end)
-  let hash (x:t) = ((Ints_t.to_int x) - 787) * 17
   (* is_top and is_bot are never called, but if they were, the Std impl would raise their exception, so we overwrite them: *)
   let is_top _ = false
   let is_bot _ = false
@@ -1249,7 +1224,7 @@ struct
     | `Excluded of S.t * R.t
     | `Definite of BigInt.t
     | `Bot
-  ] [@@deriving eq, ord]
+  ] [@@deriving eq, ord, hash]
   type int_t = BigInt.t
   let name () = "def_exc"
 
@@ -1273,11 +1248,6 @@ struct
     | `Excluded (s,l) -> "Not " ^ S.show s ^ short_size l
 
   include Std (struct type nonrec t = t let name = name let top_of = top_of let bot_of = bot_of let show = show let equal = equal end)
-  let hash (x:t) =
-    match x with
-    | `Excluded (s,r) -> S.hash s + R.hash r
-    | `Definite i -> 83*BigInt.hash i
-    | `Bot -> 61426164
 
   let maximal = function
     | `Definite x -> Some x
@@ -1659,15 +1629,14 @@ end
 module MakeBooleans (N: BooleansNames) =
 struct
   type int_t = IntOps.Int64Ops.t
-  type t = bool [@@deriving eq, ord, to_yojson]
+  type t = bool [@@deriving eq, ord, hash, to_yojson]
   let name () = "booleans"
   let top () = true
   let bot () = false
   let top_of ik = top ()
   let bot_of ik = bot ()
   let show x = if x then N.truename else N.falsename
   include Std (struct type nonrec t = t let name = name let top_of = top_of let bot_of = bot_of let show = show let equal = equal end)
-  let hash = function true -> 51534333 | _ -> 561123444
   let is_top x = x (* override Std *)
 
   let equal_to i x = if x then `Top else failwith "unsupported: equal_to with bottom"
@@ -1725,7 +1694,7 @@ module Enums : S with type int_t = BigInt.t = struct
   let range_ikind = Cil.IInt
   let size t = R.of_interval range_ikind (let a,b = Size.bits_i64 t in Int64.neg a,b)
 
-  type t = Inc of BISet.t | Exc of BISet.t * R.t [@@deriving eq, ord] (* inclusion/exclusion set *)
+  type t = Inc of BISet.t | Exc of BISet.t * R.t [@@deriving eq, ord, hash] (* inclusion/exclusion set *)
 
   type int_t = BI.t
   let name () = "enums"
@@ -1750,10 +1719,6 @@ module Enums : S with type int_t = BigInt.t = struct
 
   include Std (struct type nonrec t = t let name = name let top_of = top_of let bot_of = bot_of let show = show let equal = equal end)
 
-  let hash = function
-    | Inc x -> BISet.hash x
-    | Exc (x, r) -> 31 * R.hash r + 37  * BISet.hash x
-
   (* Normalization function for enums, that handles overflows for Inc.
      As we do not compute on Excl, we do not have to perform any overflow handling for it. *)
   let norm ikind v =
@@ -2066,7 +2031,7 @@ struct
   type int_t = Ints_t.t
 
   (* represents congruence class of c mod m, None is bot *)
-  type t = (Ints_t.t * Ints_t.t) option [@@deriving eq, ord]
+  type t = (Ints_t.t * Ints_t.t) option [@@deriving eq, ord, hash]
 
   let ( *: ) = Ints_t.mul
   let (+:) = Ints_t.add

src/cdomains/lval.ml

@@ -7,7 +7,7 @@ type ('a, 'b) offs = [
   | `NoOffset
   | `Field of 'a * ('a,'b) offs
   | `Index of 'b * ('a,'b) offs
-] [@@deriving eq, ord]
+] [@@deriving eq, ord, hash]
 
 
 let rec listify ofs =
@@ -171,7 +171,7 @@ struct
   module Offs = Offset (Idx)
   (* A SafePtr is a pointer that does not point to any variables of the analyzed program (assuming external functions don't return random pointers but only pointers to things they can reach).
    * UnknownPtr includes SafePtr *)
-  type t = Addr of (CilType.Varinfo.t * Offs.t) | StrPtr of string | NullPtr | SafePtr | UnknownPtr [@@deriving eq, ord]
+  type t = Addr of (CilType.Varinfo.t * Offs.t) | StrPtr of string | NullPtr | SafePtr | UnknownPtr [@@deriving eq, ord, hash]
   (* TODO: StrPtr equals problematic if the same literal appears more than once *)
   include Printable.Std
   let name () = "Normal Lvals"
@@ -261,9 +261,8 @@ struct
     | UnknownPtr -> voidPtrType
 
   let hash = function
-    | Addr (v,o) -> v.vid + 2 * Offs.hash o
     | SafePtr | UnknownPtr -> Hashtbl.hash UnknownPtr (* SafePtr <= UnknownPtr ==> same hash *)
-    | x -> Hashtbl.hash x
+    | x -> hash x
 
   let is_zero_offset x = Offs.cmp_zero_offset x = `MustZero
 
@@ -459,9 +458,8 @@ end
 module CilLval =
 struct
   include Printable.Std
-  type t = CilType.Varinfo.t * (CilType.Fieldinfo.t, Basetype.CilExp.t) offs [@@deriving eq, ord]
+  type t = CilType.Varinfo.t * (CilType.Fieldinfo.t, Basetype.CilExp.t) offs [@@deriving eq, ord, hash]
 
-  let hash    = Hashtbl.hash
   let name () = "simplified lval"
 
   let class_tag (v,o) =

src/cdomains/lvalMapDomain.ml

@@ -60,28 +60,17 @@ sig
 end
 
 module Value (Impl: sig
-    type s (* state *)
+    type s (* state *) [@@deriving eq, ord, hash]
     val name: string
     val var_state: s
     val string_of_state: s -> string
-    val compare: s -> s -> int
   end) : S with type s = Impl.s =
 struct
-  type k = Lval.CilLval.t
-  type s = Impl.s
+  type k = Lval.CilLval.t [@@deriving eq, ord, hash]
+  type s = Impl.s [@@deriving eq, ord, hash]
   module R = struct
     include Printable.Blank
-    type t = { key: k; loc: location list; state: s }
-    let hash = Hashtbl.hash
-    let equal a b = Lval.CilLval.equal a.key b.key && a.loc = b.loc (* FIXME: polymorphic list equal! *) && a.state = b.state
-
-    let compare a b =
-      let r = Lval.CilLval.compare a.key b.key in
-      if r <> 0 then r else
-        let r = compare a.loc b.loc in (* FIXME: polymorphic list compare! *)
-        if r <> 0 then r else
-          Impl.compare a.state b.state
-
+    type t = { key: k; loc: CilType.Location.t list; state: s } [@@deriving eq, ord, hash]
     let to_yojson _ = failwith "TODO to_yojson"
     let name () = "LValMapDomainValue"
   end