Skip to content

Commit

Permalink
Remove IntDomain.BigInt
Browse files Browse the repository at this point in the history
  • Loading branch information
karoliineh committed Jan 22, 2024
1 parent a8d74cd commit bc267c8
Show file tree
Hide file tree
Showing 2 changed files with 17 additions and 13 deletions.
21 changes: 8 additions & 13 deletions src/cdomain/value/cdomains/intDomain.ml
Original file line number Diff line number Diff line change
Expand Up @@ -1773,13 +1773,8 @@ struct
include (Lattice.Reverse (Base) : Lattice.S with type t := Base.t)
end

module BigInt = struct
include IntOps.BigIntOps
let arbitrary () = QCheck.map ~rev:Z.to_int64 Z.of_int64 QCheck.int64
end

module BISet = struct
include SetDomain.Make (BigInt)
include SetDomain.Make (IntOps.BigIntOps)
let is_singleton s = cardinal s = 1
end

Expand Down Expand Up @@ -2062,7 +2057,7 @@ struct
let of_bool = of_bool_cmp
let to_bool x =
match x with
| `Definite x -> Some (BigInt.to_bool x)
| `Definite x -> Some (IntOps.BigIntOps.to_bool x)
| `Excluded (s,r) when S.mem Z.zero s -> Some true
| _ -> None
let top_bool = `Excluded (S.empty (), R.of_interval range_ikind (0L, 1L))
Expand Down Expand Up @@ -2257,14 +2252,14 @@ struct
| _, Some false ->
of_bool ik false
| _, _ ->
lift2 BigInt.logand ik x y
lift2 IntOps.BigIntOps.logand ik x y
let logor ik x y =
match to_bool x, to_bool y with
| Some true, _
| _, Some true ->
of_bool ik true
| _, _ ->
lift2 BigInt.logor ik x y
lift2 IntOps.BigIntOps.logor ik x y
let lognot ik = eq ik (of_int ik Z.zero)

let invariant_ikind e ik (x:t) =
Expand Down Expand Up @@ -2297,12 +2292,12 @@ struct
let definite x = of_int ik x in
let shrink = function
| `Excluded (s, _) -> GobQCheck.shrink (S.arbitrary ()) s >|= excluded (* S TODO: possibly shrink excluded to definite *)
| `Definite x -> (return `Bot) <+> (GobQCheck.shrink (BigInt.arbitrary ()) x >|= definite)
| `Definite x -> (return `Bot) <+> (GobQCheck.shrink (IntOps.BigIntOps.arbitrary ()) x >|= definite)
| `Bot -> empty
in
QCheck.frequency ~shrink ~print:show [
20, QCheck.map excluded (S.arbitrary ());
10, QCheck.map definite (BigInt.arbitrary ());
10, QCheck.map definite (IntOps.BigIntOps.arbitrary ());
1, QCheck.always `Bot
] (* S TODO: decide frequencies *)

Expand Down Expand Up @@ -2630,8 +2625,8 @@ module Enums : S with type int_t = Z.t = struct
| Some b -> of_bool ik (not b)
| None -> top_bool

let logand = lift2 BigInt.logand
let logor = lift2 BigInt.logor
let logand = lift2 IntOps.BigIntOps.logand
let logor = lift2 IntOps.BigIntOps.logor
let maximal = function
| Inc xs when not (BISet.is_empty xs) -> Some (BISet.max_elt xs)
| Exc (excl,r) ->
Expand Down
9 changes: 9 additions & 0 deletions src/common/util/intOps.ml
Original file line number Diff line number Diff line change
Expand Up @@ -55,6 +55,8 @@ sig
val to_string : t -> string
val of_bigint : Z.t -> t
val to_bigint : t -> Z.t

val arbitrary : unit -> t QCheck.arbitrary
end

module type IntOps =
Expand Down Expand Up @@ -115,6 +117,8 @@ struct
let to_string = string_of_int
let of_bigint = Z.to_int
let to_bigint = Z.of_int

let arbitrary () = QCheck.int
end

module Int32OpsBase : IntOpsBase with type t = int32 =
Expand Down Expand Up @@ -161,6 +165,8 @@ struct
let to_string = Int32.to_string
let of_bigint = Z.to_int32
let to_bigint = Z.of_int32

let arbitrary () = QCheck.int32
end

module Int64OpsBase : IntOpsBase with type t = int64 =
Expand Down Expand Up @@ -207,6 +213,8 @@ struct
let to_string = Int64.to_string
let of_bigint = Z.to_int64
let to_bigint = Z.of_int64

let arbitrary () = QCheck.int64
end

module BigIntOpsBase : IntOpsBase with type t = Z.t =
Expand Down Expand Up @@ -252,6 +260,7 @@ struct
let bitor = Z.logor
let bitxor = Z.logxor

let arbitrary () = QCheck.map ~rev:Z.to_int64 Z.of_int64 QCheck.int64
end


Expand Down

0 comments on commit bc267c8

Please sign in to comment.