diff --git a/sledge/nonstdlib/set.ml b/sledge/nonstdlib/set.ml index f6b5f0ffe..51d4d72ca 100644 --- a/sledge/nonstdlib/set.ml +++ b/sledge/nonstdlib/set.ml @@ -16,6 +16,24 @@ end) : S with type elt = Elt.t = struct type elt = Elt.t type t = S.t [@@deriving compare, equal] + module Provide_hash (Elt : sig + type t = elt [@@deriving hash] + end) = + struct + let hash_fold_t h s = + let length = ref 0 in + let s = + S.fold + (fun x h -> + incr length ; + Elt.hash_fold_t h x ) + s h + in + Hash.fold_int s !length + + let hash = Hash.of_fold hash_fold_t + end + let sexp_of_t s = S.to_list s |> Sexplib.Conv.sexp_of_list Elt.sexp_of_t module Provide_of_sexp (Elt : sig diff --git a/sledge/nonstdlib/set_intf.ml b/sledge/nonstdlib/set_intf.ml index d457f105c..772ef38b3 100644 --- a/sledge/nonstdlib/set_intf.ml +++ b/sledge/nonstdlib/set_intf.ml @@ -11,11 +11,19 @@ module type S = sig type elt type t [@@deriving compare, equal, sexp_of] + module Provide_hash (_ : sig + type t = elt [@@deriving hash] + end) : sig + type t [@@deriving hash] + end + with type t := t + module Provide_of_sexp (_ : sig type t = elt [@@deriving of_sexp] end) : sig - val t_of_sexp : Sexp.t -> t + type t [@@deriving of_sexp] end + with type t := t (** {1 Construct} *) diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml index 19695863b..0a2adf96b 100644 --- a/sledge/src/llair/exp.ml +++ b/sledge/src/llair/exp.ml @@ -79,6 +79,7 @@ include T module Set = struct include Set.Make (T) + include Provide_hash (T) include Provide_of_sexp (T) end diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli index d94b04b52..b4cd3c6a7 100644 --- a/sledge/src/llair/exp.mli +++ b/sledge/src/llair/exp.mli @@ -99,8 +99,11 @@ module Reg : sig module Set : sig include Set.S with type elt := t - val sexp_of_t : t -> Sexp.t - val t_of_sexp : Sexp.t -> t + include sig + type t [@@deriving hash, sexp] + end + with type t := t + val pp : t pp end @@ -122,8 +125,11 @@ module Global : sig module Set : sig include Set.S with type elt := t - val sexp_of_t : t -> Sexp.t - val t_of_sexp : Sexp.t -> t + include sig + type t [@@deriving sexp] + end + with type t := t + val pp : t pp end diff --git a/sledge/src/llair/llair.ml b/sledge/src/llair/llair.ml index f7a4a3516..cd0d7454f 100644 --- a/sledge/src/llair/llair.ml +++ b/sledge/src/llair/llair.ml @@ -28,10 +28,10 @@ type inst = | Free of {ptr: Exp.t; loc: Loc.t} | Nondet of {reg: Reg.t option; msg: string; loc: Loc.t} | Abort of {loc: Loc.t} -[@@deriving sexp] +[@@deriving compare, equal, hash, sexp] -type cmnd = inst iarray [@@deriving sexp] -type label = string [@@deriving sexp] +type cmnd = inst iarray [@@deriving compare, equal, hash, sexp] +type label = string [@@deriving compare, equal, hash, sexp] type jump = {mutable dst: block; mutable retreating: bool} @@ -69,6 +69,106 @@ and func = ; entry: block ; loc: Loc.t } +(* compare *) + +(* functions are uniquely identified by [name] *) +let compare_func x y = if x == y then 0 else Function.compare x.name y.name +let equal_func x y = x == y || Function.equal x.name y.name +let hash_fold_func s x = Function.hash_fold_t s x.name + +(* blocks in a [t] are uniquely identified by [sort_index] *) +let compare_block x y = + if x == y then 0 else Int.compare x.sort_index y.sort_index + +let equal_block x y = x == y || Int.equal x.sort_index y.sort_index +let hash_fold_block s x = Int.hash_fold_t s x.sort_index + +module Compare : sig + type nonrec jump = jump [@@deriving compare, equal] + type nonrec 'a call = 'a call [@@deriving compare, equal] + type nonrec term = term [@@deriving compare, equal] +end +with type jump := jump + and type 'a call := 'a call + and type term := term = struct + type nonrec jump = jump = {mutable dst: block; mutable retreating: bool} + [@@deriving compare, equal] + + type nonrec 'a call = 'a call = + { callee: 'a + ; typ: Typ.t + ; actuals: Exp.t list + ; areturn: Reg.t option + ; return: jump + ; throw: jump option + ; mutable recursive: bool + ; loc: Loc.t } + [@@deriving compare, equal] + + type nonrec term = term = + | Switch of + {key: Exp.t; tbl: (Exp.t * jump) iarray; els: jump; loc: Loc.t} + | Iswitch of {ptr: Exp.t; tbl: jump iarray; loc: Loc.t} + | Call of Exp.t call + | Return of {exp: Exp.t option; loc: Loc.t} + | Throw of {exc: Exp.t; loc: Loc.t} + | Unreachable + [@@deriving compare, equal] +end + +include Compare + +(* hash *) + +let hash_fold_jump s {dst; retreating} = + let s = [%hash_fold: block] s dst in + let s = [%hash_fold: bool] s retreating in + s + +let hash_fold_term s = function + | Switch {key; tbl; els; loc} -> + let s = [%hash_fold: int] s 1 in + let s = [%hash_fold: Exp.t] s key in + let s = [%hash_fold: (Exp.t * jump) iarray] s tbl in + let s = [%hash_fold: jump] s els in + let s = [%hash_fold: Loc.t] s loc in + s + | Iswitch {ptr; tbl; loc} -> + let s = [%hash_fold: int] s 2 in + let s = [%hash_fold: Exp.t] s ptr in + let s = [%hash_fold: jump iarray] s tbl in + let s = [%hash_fold: Loc.t] s loc in + s + | Call {callee; typ; actuals; areturn; return; throw; recursive; loc} -> + let s = [%hash_fold: int] s 3 in + let s = [%hash_fold: Exp.t] s callee in + let s = [%hash_fold: Typ.t] s typ in + let s = [%hash_fold: Exp.t list] s actuals in + let s = [%hash_fold: Reg.t option] s areturn in + let s = [%hash_fold: jump] s return in + let s = [%hash_fold: jump option] s throw in + let s = [%hash_fold: bool] s recursive in + let s = [%hash_fold: Loc.t] s loc in + s + | Return {exp; loc} -> + let s = [%hash_fold: int] s 4 in + let s = [%hash_fold: Exp.t option] s exp in + let s = [%hash_fold: Loc.t] s loc in + s + | Throw {exc; loc} -> + let s = [%hash_fold: int] s 5 in + let s = [%hash_fold: Exp.t] s exc in + let s = [%hash_fold: Loc.t] s loc in + s + | Unreachable -> [%hash_fold: int] s 6 + +let hash_func = Hash.of_fold hash_fold_func +let hash_block = Hash.of_fold hash_fold_block +let hash_jump = Hash.of_fold hash_fold_jump +let hash_term = Hash.of_fold hash_fold_term + +(* sexp *) + let sexp_cons (hd : Sexp.t) (tl : Sexp.t) = match tl with | List xs -> Sexp.List (hd :: xs) @@ -120,15 +220,13 @@ let sexp_of_func {name; formals; freturn; fthrow; locals; entry; loc} = ; entry: block ; loc: Loc.t }] -(* blocks in a [t] are uniquely identified by [sort_index] *) -let compare_block x y = Int.compare x.sort_index y.sort_index -let equal_block x y = Int.equal x.sort_index y.sort_index - type functions = func Function.Map.t [@@deriving sexp_of] type program = {globals: GlobalDefn.t iarray; functions: functions} [@@deriving sexp_of] +(* pp *) + let pp_inst fs inst = let pf pp = Format.fprintf fs pp in match inst with @@ -237,7 +335,7 @@ and dummy_func = (** Instructions *) module Inst = struct - type t = inst [@@deriving sexp] + type t = inst [@@deriving compare, equal, hash, sexp] let pp = pp_inst let move ~reg_exps ~loc = Move {reg_exps; loc} @@ -295,7 +393,7 @@ end (** Jumps *) module Jump = struct - type t = jump [@@deriving sexp_of] + type t = jump [@@deriving compare, equal, hash, sexp_of] let compare x y = compare_block x.dst y.dst let equal x y = equal_block x.dst y.dst @@ -306,7 +404,7 @@ end (** Basic-Block Terminators *) module Term = struct - type t = term [@@deriving sexp_of] + type t = term [@@deriving compare, equal, hash, sexp_of] let pp = pp_term @@ -371,7 +469,7 @@ end module Block = struct module T = struct - type t = block [@@deriving compare, equal, sexp_of] + type t = block [@@deriving compare, equal, hash, sexp_of] end include T @@ -415,7 +513,7 @@ module FuncQ = HashQueue.Make (Function) (** Functions *) module Func = struct - type t = func [@@deriving sexp_of] + type t = func [@@deriving compare, equal, hash, sexp_of] let is_undefined = function | {entry= {cmnd; term= Unreachable; _}; _} -> IArray.is_empty cmnd diff --git a/sledge/src/llair/llair.mli b/sledge/src/llair/llair.mli index d65cadf11..ac650ad53 100644 --- a/sledge/src/llair/llair.mli +++ b/sledge/src/llair/llair.mli @@ -109,7 +109,7 @@ type program = private ; functions: functions (** (Global) function definitions. *) } module Inst : sig - type t = inst + type t = inst [@@deriving compare, equal, hash] val pp : t pp val move : reg_exps:(Reg.t * Exp.t) iarray -> loc:Loc.t -> inst @@ -128,14 +128,14 @@ module Inst : sig end module Jump : sig - type t = jump [@@deriving compare, equal, sexp_of] + type t = jump [@@deriving compare, equal, hash, sexp_of] val pp : jump pp val mk : string -> jump end module Term : sig - type t = term + type t = term [@@deriving compare, equal, hash] val pp : t pp @@ -167,7 +167,7 @@ module Term : sig end module Block : sig - type t = block [@@deriving compare, equal, sexp_of] + type t = block [@@deriving compare, equal, hash, sexp_of] val pp : t pp val mk : lbl:label -> cmnd:cmnd -> term:term -> block @@ -176,7 +176,7 @@ module Block : sig end module Func : sig - type t = func + type t = func [@@deriving compare, equal, hash] val pp : t pp