Add dichotomic symbolic ctz

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 =

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
 

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 =

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
 

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

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 *)

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
 

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))
+        ))
+        )
+    ))
   )
 
 

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))
+        ))
+        )
+    ))
   )