Implement count_leading_zeros in Lem

5 files changed, 27 insertions, 0 deletions

diff --git a/src/gen_lib/sail2_operators_bitlists.lem b/src/gen_lib/sail2_operators_bitlists.lem
index 8b75fa38..c9892e4c 100644
--- a/src/gen_lib/sail2_operators_bitlists.lem
+++ b/src/gen_lib/sail2_operators_bitlists.lem
@@ -304,3 +304,5 @@ val eq_vec    : list bitU -> list bitU -> bool
 val neq_vec   : list bitU -> list bitU -> bool
 let eq_vec    = eq_bv
 let neq_vec   = neq_bv
+
+let inline count_leading_zeros v = count_leading_zero_bits v
diff --git a/src/gen_lib/sail2_operators_mwords.lem b/src/gen_lib/sail2_operators_mwords.lem
index 181fa149..c8524e16 100644
--- a/src/gen_lib/sail2_operators_mwords.lem
+++ b/src/gen_lib/sail2_operators_mwords.lem
@@ -329,3 +329,6 @@ val eq_vec    : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
 val neq_vec   : forall 'a. Size 'a => mword 'a -> mword 'a -> bool
 let inline eq_vec    = eq_mword
 let inline neq_vec   = neq_mword
+
+val count_leading_zeros : forall 'a. Size 'a => mword 'a -> integer
+let count_leading_zeros v = count_leading_zeros_bv v
diff --git a/src/gen_lib/sail2_values.lem b/src/gen_lib/sail2_values.lem
index 9de28cca..f657803f 100644
--- a/src/gen_lib/sail2_values.lem
+++ b/src/gen_lib/sail2_values.lem
@@ -656,6 +656,16 @@ let int_of_bit b =
   | _ -> failwith "int_of_bit saw unknown"
   end
 
+val count_leading_zero_bits : list bitU -> integer
+let rec count_leading_zero_bits v =
+  match v with
+  | B0 :: v' -> count_leading_zero_bits v' + 1
+  | _ -> 0
+  end
+
+val count_leading_zeros_bv : forall 'a. Bitvector 'a => 'a -> integer
+let count_leading_zeros_bv v = count_leading_zero_bits (bits_of v)
+
 val decimal_string_of_bv : forall 'a. Bitvector 'a => 'a -> string
 let decimal_string_of_bv bv =
   let place_values =
diff --git a/test/builtins/count_leading_zeros.sail b/test/builtins/count_leading_zeros.sail
new file mode 100644
index 00000000..6d6d0901
--- /dev/null
+++ b/test/builtins/count_leading_zeros.sail
@@ -0,0 +1,11 @@
+default Order dec
+
+$include <vector_dec.sail>
+
+val main : unit -> unit effect {escape}
+
+function main () = {
+  foreach (i from 0 to 32 by 1 in inc) {
+    assert(count_leading_zeros(sail_shiftright(0xDEADBEEF, i)) == i);
+  }
+}
diff --git a/test/builtins/run_tests.py b/test/builtins/run_tests.py
index ba13d5b9..a677ccfe 100755
--- a/test/builtins/run_tests.py
+++ b/test/builtins/run_tests.py
@@ -68,6 +68,7 @@ def test_lem_builtins(name):
                 step('mkdir -p _lbuild_{}'.format(basename))
                 step('mv {}.lem _lbuild_{}'.format(basename, basename))
                 step('mv {}_types.lem _lbuild_{}'.format(basename, basename))
+                step('cp $SAIL_DIR/src/lem_interp/sail2_instr_kinds.lem _lbuild_{}'.format(basename))
                 step('cp myocamlbuild.ml _lbuild_{}'.format(basename))
                 os.chdir('_lbuild_{}'.format(basename))
                 step('ln -s $SAIL_DIR/src/gen_lib/ gen_lib')