Skip to content

Commit

Permalink
Use deriving where possible
Browse files Browse the repository at this point in the history
  • Loading branch information
sim642 committed Mar 20, 2024
1 parent be3ee1d commit da91765
Showing 6 changed files with 10 additions and 57 deletions.
23 changes: 2 additions & 21 deletions src/cdomains/pthreadDomain.ml
Original file line number Diff line number Diff line change
@@ -25,8 +25,7 @@ end
module D = struct
include Printable.StdLeaf

type domain = { tid : Tid.t; pred : Pred.t; ctx : Ctx.t } [@@deriving to_yojson]
type t = domain
type t = { tid : Tid.t; pred : Pred.t; ctx : Ctx.t } [@@deriving eq, ord, hash, to_yojson]

(** printing *)
let show x =
@@ -36,28 +35,10 @@ module D = struct
(Pred.show x.pred)
(Ctx.show x.ctx)

include Printable.SimpleShow(struct type t = domain let show = show end)
include Printable.SimpleShow(struct type nonrec t = t let show = show end) (* TODO: overrides derived to_yojson *)

let name () = "pthread state"

(** let equal = Util.equals *)
let equal x y =
Tid.equal x.tid y.tid && Pred.equal x.pred y.pred && Ctx.equal x.ctx y.ctx


(** compare all fields with correspoding compare operators *)
let compare x y =
List.fold_left
(fun acc v -> if acc = 0 && v <> 0 then v else acc)
0
[ Tid.compare x.tid y.tid
; Pred.compare x.pred y.pred
; Ctx.compare x.ctx y.ctx
]


(** let hash = Hashtbl.hash *)
let hash x = Hashtbl.hash (Tid.hash x.tid, Pred.hash x.pred, Ctx.hash x.ctx)
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
20 changes: 4 additions & 16 deletions src/common/util/intOps.ml
Original file line number Diff line number Diff line change
@@ -83,7 +83,7 @@ end
* -------------------------------------------------------------- *)
module NIntOpsBase : IntOpsBase with type t = int =
struct
type t = int [@@deriving hash]
type t = int [@@deriving eq, ord, hash]
let name () = "int"
let zero = 0
let one = 1
@@ -108,9 +108,6 @@ struct
let logxor = (lxor)
let lognot = (lnot)


let compare = compare
let equal = Int.equal
let top_range a b = (a = min_int) && (b = max_int)
let max = Int.max
let min = Int.min
@@ -129,7 +126,7 @@ end

module Int32OpsBase : IntOpsBase with type t = int32 =
struct
type t = int32 [@@deriving hash]
type t = int32 [@@deriving eq, ord, hash]
let name () = "int32"
let zero = 0l
let one = 1l
@@ -155,9 +152,6 @@ struct

let lognot = Int32.lognot (* Int32 calls bitwise operations 'log' *)

let compare = Int32.compare
let equal = Int32.equal

let top_range a b =
(0 = compare a Int32.min_int) && (0 = compare b Int32.max_int)
let max = Int32.max
@@ -177,7 +171,7 @@ end

module Int64OpsBase : IntOpsBase with type t = int64 =
struct
type t = int64 [@@deriving hash]
type t = int64 [@@deriving eq, ord, hash]
let name () = "int64"
let zero = 0L
let one = 1L
@@ -203,9 +197,6 @@ struct

let lognot = Int64.lognot (* Int64 calls bitwise operations 'log' *)

let compare = Int64.compare
let equal = Int64.equal

let top_range a b =
(0 = compare a Int64.min_int) && (0 = compare b Int64.max_int)
let max = Int64.max
@@ -225,7 +216,7 @@ end

module BigIntOpsBase : IntOpsBase with type t = Z.t =
struct
type t = Z.t
type t = Z.t [@@deriving eq, ord, hash]
let name () = "Z"
let zero = Z.zero
let one = Z.one
@@ -241,9 +232,6 @@ struct
let rem = Z.rem

let gcd = Z.gcd
let compare = Z.compare
let equal = Z.equal
let hash = Z.hash

let top_range _ _ = false

3 changes: 1 addition & 2 deletions src/domain/mapDomain.ml
Original file line number Diff line number Diff line change
@@ -110,8 +110,7 @@ struct

module Group =
struct
type t = D.group
let compare = D.compare_group
type t = D.group [@@deriving ord]
end

module GroupMap = Map.Make (Group)
3 changes: 1 addition & 2 deletions src/incremental/compareCIL.ml
Original file line number Diff line number Diff line change
@@ -29,8 +29,7 @@ let get_varinfo gc = match gc.decls, gc.def with

module GlobalColMap = Map.Make(
struct
type t = global_col
let compare = compare_global_col
type t = global_col [@@deriving ord]
end)

let name_of_global g = match g with
4 changes: 1 addition & 3 deletions src/util/std/gobFpath.ml
Original file line number Diff line number Diff line change
@@ -1,7 +1,5 @@
type t = Fpath.t [@@deriving show]
type t = Fpath.t [@@deriving eq, ord, show]

let equal = Fpath.equal
let compare = Fpath.compare
let hash p = Hashtbl.hash (Fpath.to_string p)

let pretty () p = GoblintCil.Pretty.text (Fpath.to_string p)
14 changes: 1 addition & 13 deletions src/witness/argTools.ml
Original file line number Diff line number Diff line change
@@ -62,19 +62,7 @@ struct

module Node =
struct
type t = MyCFG.node * Spec.C.t * int

let equal (n1, c1, i1) (n2, c2, i2) =
EQSys.LVar.equal (n1, c1) (n2, c2) && i1 = i2

let compare (n1, c1, i1) (n2, c2, i2) =
let r = EQSys.LVar.compare (n1, c1) (n2, c2) in
if r <> 0 then
r
else
Int.compare i1 i2

let hash (n, c, i) = 31 * EQSys.LVar.hash (n, c) + i
type t = Node.t * Spec.C.t * int [@@deriving eq, ord, hash]

let cfgnode (n, c, i) = n
let context_id (n, c, i) = Spec.C.tag c

0 comments on commit da91765

Please sign in to comment.