Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Adds Bitvec.modular function #1394

Merged
merged 24 commits into from
Jan 7, 2022
Merged
Changes from 1 commit
Commits
Show all changes
24 commits
Select commit Hold shift + click to select a range
06ee098
Update LLVM backend to work with version 12
bmourad01 Oct 23, 2021
c3f1f26
Merge branch 'BinaryAnalysisPlatform:master' into master
bmourad01 Nov 3, 2021
3b8b06c
Merge branch 'BinaryAnalysisPlatform:master' into master
bmourad01 Nov 4, 2021
53677fc
Merge branch 'BinaryAnalysisPlatform:master' into master
bmourad01 Nov 6, 2021
4695b07
Merge branch 'BinaryAnalysisPlatform:master' into master
bmourad01 Nov 13, 2021
c6c89c1
Merge branch 'BinaryAnalysisPlatform:master' into master
bmourad01 Nov 16, 2021
a1fb592
Merge branch 'BinaryAnalysisPlatform:master' into master
bmourad01 Nov 19, 2021
fa3c6da
Merge branch 'BinaryAnalysisPlatform:master' into master
bmourad01 Nov 20, 2021
d5dc07f
Merge branch 'BinaryAnalysisPlatform:master' into master
bmourad01 Nov 25, 2021
896a34d
Merge branch 'BinaryAnalysisPlatform:master' into master
bmourad01 Dec 1, 2021
3cce21b
Merge branch 'BinaryAnalysisPlatform:master' into master
bmourad01 Dec 2, 2021
96874e4
Merge branch 'BinaryAnalysisPlatform:master' into master
bmourad01 Dec 3, 2021
c25c801
Merge branch 'BinaryAnalysisPlatform:master' into master
bmourad01 Dec 3, 2021
cf3352a
Merge branch 'BinaryAnalysisPlatform:master' into master
bmourad01 Dec 8, 2021
9cc0b14
Merge branch 'BinaryAnalysisPlatform:master' into master
bmourad01 Dec 8, 2021
5a38191
Merge branch 'BinaryAnalysisPlatform:master' into master
bmourad01 Dec 9, 2021
542ba10
Merge branch 'BinaryAnalysisPlatform:master' into master
bmourad01 Dec 9, 2021
14e4b38
Merge branch 'BinaryAnalysisPlatform:master' into master
bmourad01 Jan 5, 2022
2e5ff40
Merge branch 'BinaryAnalysisPlatform:master' into master
bmourad01 Jan 5, 2022
6c98118
Merge branch 'BinaryAnalysisPlatform:master' into master
bmourad01 Jan 5, 2022
a57a83a
Merge branch 'BinaryAnalysisPlatform:master' into master
bmourad01 Jan 6, 2022
baff49c
Adds the `Bitvec.modulus` function
Jan 7, 2022
88cbd5e
Fixes typo in docstring
Jan 7, 2022
f10ddec
Adds since version
Jan 7, 2022
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Adds the Bitvec.modulus function
It's a bit clumsy to construct a Bitvec instance when the bit width is
not statically known, e.g.:

```
let add n x y =
  let module M = Bitvec.Make(struct
    let modulus = Bitvec.modulus n
  end) in
  M.(x + y)
```

Instead, we can create a first-class module more concisely:

```
let add n x y =
  let open (val Bitvec.modular n) in
  x + y
```

Unrelatedly, this also adds the missing `Bitvec.M16` specialization and
its corresponding modulus.
bmourad01 committed Jan 7, 2022
commit baff49cb534ef1191a1e9a259db0644e568a675c
19 changes: 18 additions & 1 deletion lib/bitvec/bitvec.ml
Original file line number Diff line number Diff line change
@@ -71,6 +71,7 @@ let modulus w = {

let m1 = modulus 1
let m8 = modulus 8
let m16 = modulus 16
let m32 = modulus 32
let m64 = modulus 64

@@ -431,7 +432,9 @@ let to_binary = Z.to_bits
let pp ppf x =
Format.fprintf ppf "%s" (to_string x)

module Make(M : Modulus) : S with type 'a m = 'a = struct
module type D = S with type 'a m = 'a

module Make(M : Modulus) : D = struct
type 'a m = 'a
let m = M.modulus

@@ -501,6 +504,10 @@ module M8 = Make(struct
let modulus = m8
end)

module M16 = Make(struct
let modulus = m16
end)

module M32 = Make(struct
let modulus = m32
end)
@@ -509,6 +516,16 @@ module M64 = Make(struct
let modulus = m64
end)

let modular : int -> (module D) = function
| 1 -> (module M1)
| 8 -> (module M8)
| 16 -> (module M16)
| 32 -> (module M32)
| 64 -> (module M64)
| n -> (module Make(struct
let modulus = modulus n
end))

include Syntax
let equal x y = compare x y = 0 [@@inline]
let (<) x y = compare x y < 0 [@@inline]
26 changes: 22 additions & 4 deletions lib/bitvec/bitvec.mli
Original file line number Diff line number Diff line change
@@ -21,6 +21,9 @@ val m1 : modulus
(** [m8 = modulus 8] = $255$ is the modulus of bitvectors with size [8] *)
val m8 : modulus

(** [m16 = modulus 16] = $65535$ is the modulus of bitvectors with size [16] *)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
(** [m16 = modulus 16] = $65535$ is the modulus of bitvectors with size [16] *)
(** [m16 = modulus 16] = $65535$ is the modulus of bitvectors with size [16]
@since 2.5.0 *)

val m16 : modulus

(** [m32 = modulus 32] = $2^32-1$ is the modulus of bitvectors with size [32] *)
val m32 : modulus

@@ -566,14 +569,15 @@ module Make(M : Modulus) : sig
include S with type 'a m = 'a
end

module type D = S with type 'a m = 'a

(** [M1] specializes [Make(struct let modulus = m1 end)]

The specialization relies on a few arithmetic equalities
and on an efficient implementation of the modulo operation
as the [even x] aka [lsb x] operation.
*)
module M1 : S with type 'a m = 'a
module M1 : D

(** [M8] specializes [Make(struct let modulus = m8 end)]

@@ -582,7 +586,17 @@ module M1 : S with type 'a m = 'a
calls to the underlying arbitrary precision arithmetic
library.
*)
module M8 : S with type 'a m = 'a
module M8 : D


(** [M16] specializes [Make(struct let modulus = m16 end)]

This specialization relies on a fact, that 8 bitvectors
always fit into OCaml integer representation, so it avoids
calls to the underlying arbitrary precision arithmetic
library.
*)
module M16 : D


(** [M32] specializes [Make(struct let modulus = m32 end)]
@@ -592,7 +606,7 @@ module M8 : S with type 'a m = 'a
calls to the underlying arbitrary precision arithmetic
library.
*)
module M32 : S with type 'a m = 'a
module M32 : D


(** [M64] specializes [Make(struct let modulus = m64 end)]
@@ -602,4 +616,8 @@ module M32 : S with type 'a m = 'a
will not overflow the OCaml int representation.

*)
module M64 : S with type 'a m = 'a
module M64 : D

(** [modular n] returns a module [M] which implements
all operations in [S] modulo the bitwitdh [n]. *)
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
(** [modular n] returns a module [M] which implements
all operations in [S] modulo the bitwitdh [n]. *)
(** [modular n] returns a module [M], which implements
all operations in [S] modulo the bitwitdh [n].
@since 2.5.0 *)

val modular : int -> (module D)