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.

1 files changed, 9 insertions, 0 deletions

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