From 7f248d6bc8cea128c49b77818a04af0d85b927db Mon Sep 17 00:00:00 2001 From: Arthur Carcano Date: Tue, 27 Feb 2024 18:40:06 +0100 Subject: [PATCH] Add dichotomic symbolic ctz --- src/int32.ml | 5 ++++- src/int32.mli | 2 +- src/int64.ml | 5 ++++- src/int64.mli | 2 +- src/interpret.ml | 34 ++++++++++++++++++++++++++++++++-- src/symbolic_value.ml | 8 ++------ src/value_intf.ml | 2 +- test/sym/clz_32.wat | 13 +++++++++++++ test/sym/clz_64.wat | 13 +++++++++++++ 9 files changed, 71 insertions(+), 13 deletions(-) diff --git a/src/int32.ml b/src/int32.ml index 1aa9a6841..9954cea41 100644 --- a/src/int32.ml +++ b/src/int32.ml @@ -6,7 +6,10 @@ let clz = Some (fun n -> Stdlib.Int32.of_int (Ocaml_intrinsics.Int32.count_leading_zeros n)) -let ctz n = Stdlib.Int32.of_int (Ocaml_intrinsics.Int32.count_trailing_zeros n) +let ctz = + Some + (fun n -> + Stdlib.Int32.of_int (Ocaml_intrinsics.Int32.count_trailing_zeros n) ) (* Taken from Base https://github.com/janestreet/base *) let popcnt = diff --git a/src/int32.mli b/src/int32.mli index b786366d4..66e1acc94 100644 --- a/src/int32.mli +++ b/src/int32.mli @@ -36,7 +36,7 @@ val unsigned_to_int : t -> int option val clz : (t -> t) option -val ctz : t -> t +val ctz : (t -> t) option val popcnt : t -> t diff --git a/src/int64.ml b/src/int64.ml index 96da45ac1..bd10c431f 100644 --- a/src/int64.ml +++ b/src/int64.ml @@ -6,7 +6,10 @@ let clz = Some (fun n -> Stdlib.Int64.of_int (Ocaml_intrinsics.Int64.count_leading_zeros n)) -let ctz n = Stdlib.Int64.of_int (Ocaml_intrinsics.Int64.count_trailing_zeros n) +let ctz = + Some + (fun n -> + Stdlib.Int64.of_int (Ocaml_intrinsics.Int64.count_trailing_zeros n) ) (* Taken from Base: https://github.com/janestreet/base *) let popcnt = diff --git a/src/int64.mli b/src/int64.mli index b4d833d5f..88cecfeb4 100644 --- a/src/int64.mli +++ b/src/int64.mli @@ -36,7 +36,7 @@ val abs : t -> t val clz : (t -> t) option -val ctz : t -> t +val ctz : (t -> t) option val popcnt : t -> t diff --git a/src/interpret.ml b/src/interpret.ml index 601240ea9..c3c38be3e 100644 --- a/src/interpret.ml +++ b/src/interpret.ml @@ -126,6 +126,32 @@ module Make (P : Interpret_intf.P) : let> cond = I64.(eqz n) in if cond then return @@ const_i64 64L else aux 0 64 + let ctz_impl_32 n = + let rec aux (lb : int) ub = + if ub = lb + 1 then return (const_i32 (Int32.of_int lb)) + else begin + let mid = (lb + ub) / 2 in + let two_pow_mid = Int32.shl 1l (Int32.of_int mid) in + let> cond = I32.(eqz @@ rem n (const_i32 two_pow_mid)) in + if cond then aux mid ub else aux lb mid + end + in + let> cond = I32.(eqz n) in + if cond then return @@ const_i32 32l else aux 0 32 + + let ctz_impl_64 n = + let rec aux (lb : int) ub = + if ub = lb + 1 then return (const_i64 (Int64.of_int lb)) + else begin + let mid = (lb + ub) / 2 in + let two_pow_mid = Int64.shl 1L (Int64.of_int mid) in + let> cond = I64.(eqz @@ rem n (const_i64 two_pow_mid)) in + if cond then aux mid ub else aux lb mid + end + in + let> cond = I64.(eqz n) in + if cond then return @@ const_i64 64L else aux 0 64 + let with_choosing_default_impl f ch_f = match f with | Some f -> fun n -> Choice.return (f n) @@ -141,7 +167,9 @@ module Make (P : Interpret_intf.P) : | Clz -> let clz = with_choosing_default_impl clz clz_impl_32 in clz n - | Ctz -> Choice.return @@ ctz n + | Ctz -> + let ctz = with_choosing_default_impl ctz ctz_impl_32 in + ctz n | Popcnt -> Choice.return @@ popcnt n in Stack.push_i32 stack res @@ -153,7 +181,9 @@ module Make (P : Interpret_intf.P) : | Clz -> let clz = with_choosing_default_impl clz clz_impl_64 in clz n - | Ctz -> Choice.return @@ ctz n + | Ctz -> + let ctz = with_choosing_default_impl ctz ctz_impl_64 in + ctz n | Popcnt -> Choice.return @@ popcnt n in Stack.push_i64 stack res diff --git a/src/symbolic_value.ml b/src/symbolic_value.ml index e789a04f8..3fc3805a6 100644 --- a/src/symbolic_value.ml +++ b/src/symbolic_value.ml @@ -167,9 +167,7 @@ module I32 = struct let clz = None - let ctz _ = - (* TODO *) - assert false + let ctz = None let popcnt _ = (* TODO *) @@ -283,9 +281,7 @@ module I64 = struct let clz = None - let ctz _ = - (* TODO *) - assert false + let ctz = None let popcnt _ = (* TODO *) diff --git a/src/value_intf.ml b/src/value_intf.ml index 215a715eb..1c0b816b3 100644 --- a/src/value_intf.ml +++ b/src/value_intf.ml @@ -19,7 +19,7 @@ module type Iop = sig val clz : (num -> num) option - val ctz : num -> num + val ctz : (num -> num) option val popcnt : num -> num diff --git a/test/sym/clz_32.wat b/test/sym/clz_32.wat index 6dd88bfe2..acee1ef6d 100644 --- a/test/sym/clz_32.wat +++ b/test/sym/clz_32.wat @@ -44,6 +44,19 @@ (call $countLeadingZeros (local.get $n)) (i32.clz (local.get $n)) )) + + (call $assert (i32.eq + (i32.ctz (local.get $n)) + ;; Implem of ctz using clz + ;; from hacker's delight p107 + (i32.sub + (i32.const 32) + (i32.clz ( i32.and + (i32.xor (local.get $n) (i32.const -1)) + (i32.sub (local.get $n) (i32.const 1)) + )) + ) + )) ) diff --git a/test/sym/clz_64.wat b/test/sym/clz_64.wat index 98f954f9c..0430d61de 100644 --- a/test/sym/clz_64.wat +++ b/test/sym/clz_64.wat @@ -44,6 +44,19 @@ (call $countLeadingZeros (local.get $n)) (i64.clz (local.get $n)) )) + + (call $assert (i64.eq + (i64.ctz (local.get $n)) + ;; Implem of ctz using clz + ;; from hacker's delight p107 + (i64.sub + (i64.const 64) + (i64.clz ( i64.and + (i64.xor (local.get $n) (i64.const -1)) + (i64.sub (local.get $n) (i64.const 1)) + )) + ) + )) )