Skip to content

Change implementation of clz and ctz #387

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.

Sign up for GitHub

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

Draft
wants to merge 1 commit into
base: main
Choose a base branch
from
Draft

Change implementation of clz and ctz #387

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
53 changes: 26 additions & 27 deletions src/smtml/mappings.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -303,40 +303,42 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct

module Ixx : sig
val of_int : int -> elt

val shift_left : elt -> int -> elt
end
end

module Bitv_impl (B : Bitv_sig) = struct
open M
include B

(* Stolen from @krtab in OCamlPro/owi#195 *)
let clz n =
let rec loop (lb : int) (ub : int) =
if ub = lb + 1 then v @@ Ixx.of_int (bitwidth - ub)
let clo n =
let rec loop (next : int) expr =
if Prelude.Int.equal next 0 then expr
else
let mid = (lb + ub) / 2 in
let pow_two_mid = v Ixx.(shift_left (of_int 1) mid) in
ite (Bitv.lt_u n pow_two_mid) (loop lb mid) (loop mid ub)
let shift = next in
let shifted = Bitv.lshr n (v @@ Ixx.of_int shift) in
let bit = Bitv.rem_u shifted (v @@ Ixx.of_int 2) in
let expr = Bitv.add bit (Bitv.mul bit expr) in
let next = pred next in
loop next expr
in
ite
(eq n (v @@ Ixx.of_int 0))
(v @@ Ixx.of_int bitwidth)
(loop 0 bitwidth)

(* Stolen from @krtab in OCamlPro/owi #195 *)
let ctz n =
let zero = v (Ixx.of_int 0) in
let rec loop (lb : int) (ub : int) =
if ub = lb + 1 then v (Ixx.of_int lb)
loop bitwidth (v @@ Ixx.of_int 1)

let clz n = clo @@ Bitv.lognot n

let cto n =
let rec loop (next : int) expr =
if Prelude.Int.equal next bitwidth then expr
else
let mid = (lb + ub) / 2 in
let pow_two_mid = v Ixx.(shift_left (of_int 1) mid) in
M.ite (eq (Bitv.rem n pow_two_mid) zero) (loop mid ub) (loop lb mid)
let shift = bitwidth - next - 1 in
let shifted = Bitv.lshr n (v @@ Ixx.of_int shift) in
let bit = Bitv.rem_u shifted (v @@ Ixx.of_int 2) in
let expr = Bitv.add bit (Bitv.mul bit expr) in
let next = succ next in
loop next expr
in
ite (eq n zero) (v @@ Ixx.of_int bitwidth) (loop 0 bitwidth)
loop 0 (v @@ Ixx.of_int 1)

let ctz n = cto @@ Bitv.lognot n

let popcnt n =
let rec loop (next : int) count =
Expand Down Expand Up @@ -422,8 +424,6 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct

module Ixx = struct
let of_int i = i [@@inline]

let shift_left v i = v lsl i [@@inline]
end
end)

Expand Down Expand Up @@ -810,8 +810,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
else (
assert (Z.equal b Z.zero);
Value.False )
| Ty_bitv m ->
Value.Bitv (Bitvector.make (M.Interp.to_bitv v m) m)
| Ty_bitv m -> Value.Bitv (Bitvector.make (M.Interp.to_bitv v m) m)
| Ty_fp 32 ->
let float = M.Interp.to_float v 8 24 in
Value.Num (F32 (Int32.bits_of_float float))
Expand Down
8 changes: 4 additions & 4 deletions test/unit/test_bitvector.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -33,12 +33,12 @@ let test_neg _ =
check (neg bv) (make (z (-5)) 8)

let test_clz _ =
let bv = make (z 1) 8 in
check (clz bv) (make (z 7) 8)
let bv = make (z 2) 8 in
check (clz bv) (make (z 6) 8)

let test_ctz _ =
let bv = make (z 128) 8 in
check (ctz bv) (make (z 7) 8)
let bv = make (z 64) 8 in
check (ctz bv) (make (z 6) 8)

let test_popcnt _ =
let bv = make (z 0b1010_1010) 8 in
Expand Down