Implement a count_leading_zeros builtin for ocaml and c. This may be a slight performance improvement and keeps compatibility with smt backend that already had a builtin for this because it can't handle the loop in the sail version. Will need implementations for prover backends.

5 files changed, 29 insertions, 0 deletions

diff --git a/lib/sail.c b/lib/sail.c
index e9c6ca37..7fc45714 100644
--- a/lib/sail.c
+++ b/lib/sail.c
@@ -767,6 +767,16 @@ void length_lbits(sail_int *rop, const lbits op)
   mpz_set_ui(*rop, op.len);
 }
 
+void count_leading_zeros(sail_int *rop, const lbits op)
+{
+  if (mpz_cmp_ui(*op.bits, 0) == 0) {
+    mpz_set_ui(*rop, op.len);
+  } else {
+    size_t bits = mpz_sizeinbase(*op.bits, 2);
+    mpz_set_ui(*rop, op.len - bits);
+  }
+}
+
 bool eq_bits(const lbits op1, const lbits op2)
 {
   assert(op1.len == op2.len);
diff --git a/lib/sail.h b/lib/sail.h
index 1a123cf4..eddf6e41 100644
--- a/lib/sail.h
+++ b/lib/sail.h
@@ -262,6 +262,7 @@ fbits fast_sign_extend(const fbits op, const uint64_t n, const uint64_t m);
 fbits fast_sign_extend2(const sbits op, const uint64_t m);
 
 void length_lbits(sail_int *rop, const lbits op);
+void count_leading_zeros(sail_int *rop, const lbits op);
 
 bool eq_bits(const lbits op1, const lbits op2);
 bool EQUAL(lbits)(const lbits op1, const lbits op2);
diff --git a/lib/vector_dec.sail b/lib/vector_dec.sail
index de63c1a1..909f3898 100644
--- a/lib/vector_dec.sail
+++ b/lib/vector_dec.sail
@@ -37,6 +37,8 @@ val vector_length = {
 
 overload length = {bitvector_length, vector_length}
 
+val count_leading_zeros = "count_leading_zeros" : forall 'N , 'N >= 1. bits('N) -> {'n, 0 <= 'n <= 'N . atom('n)}
+
 val "print_bits" : forall 'n. (string, bits('n)) -> unit
 
 val "prerr_bits" : forall 'n. (string, bits('n)) -> unit
diff --git a/src/sail_lib.ml b/src/sail_lib.ml
index 2e00f980..76c2f59b 100644
--- a/src/sail_lib.ml
+++ b/src/sail_lib.ml
@@ -138,6 +138,13 @@ let rec take n xs =
   | n, (x :: xs) -> x :: take (n - 1) xs
   | n, [] -> []
 
+let count_leading_zeros xs =
+  let rec clz = function
+    | [] -> 0
+    | (B1 :: xs') -> clz xs'
+    | (B0 :: xs') -> 1 + clz xs' in
+  Big_int.of_int (clz xs)
+
 let subrange (list, n, m) =
   let n = Big_int.to_int n in
   let m = Big_int.to_int m in
diff --git a/test/builtins/clz.sail b/test/builtins/clz.sail
new file mode 100644
index 00000000..5cf20068
--- /dev/null
+++ b/test/builtins/clz.sail
@@ -0,0 +1,9 @@
+default Order dec
+$include <vector_dec.sail>
+
+function main () : unit -> unit = {
+  assert(count_leading_zeros(0x0) == 4);
+  assert(count_leading_zeros(0x1) == 3);
+  assert(count_leading_zeros(0x4) == 1);
+  assert(count_leading_zeros(0xf) == 0);
+}
\ No newline at end of file