From 2dd28164e40241a2117142fbb197c967740f196d Mon Sep 17 00:00:00 2001
From: Robert Norton
Date: Mon, 17 Jun 2019 14:25:01 +0100
Subject: 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.

---
 src/sail_lib.ml | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'src')

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
-- 
cgit v1.2.3