Merge remote-tracking branch 'origin/sail2' into separate_bv

4 files changed, 26 insertions, 7 deletions

diff --git a/src/gen_lib/sail2_operators.lem b/src/gen_lib/sail2_operators.lem
index 547160d3..43a9812e 100644
--- a/src/gen_lib/sail2_operators.lem
+++ b/src/gen_lib/sail2_operators.lem
@@ -163,9 +163,9 @@ let arith_op_bv_no0 op sign size l r =
   Maybe.bind (int_of_bv sign r) (fun r' ->
   if r' = 0 then Nothing else Just (of_int (length l * size) (op l' r'))))
 
-let mod_bv = arith_op_bv_no0 hardware_mod false 1
-let quot_bv = arith_op_bv_no0 hardware_quot false 1
-let quots_bv = arith_op_bv_no0 hardware_quot true 1
+let mod_bv = arith_op_bv_no0 tmod_int false 1
+let quot_bv = arith_op_bv_no0 tdiv_int false 1
+let quots_bv = arith_op_bv_no0 tdiv_int true 1
 
 let mod_mword = Machine_word.modulo
 let quot_mword = Machine_word.unsignedDivide
@@ -174,8 +174,8 @@ let quots_mword = Machine_word.signedDivide
 let arith_op_bv_int_no0 op sign size l r =
   arith_op_bv_no0 op sign size l (of_int (length l) r)
 
-let quot_bv_int = arith_op_bv_int_no0 hardware_quot false 1
-let mod_bv_int = arith_op_bv_int_no0 hardware_mod false 1
+let quot_bv_int = arith_op_bv_int_no0 tdiv_int false 1
+let mod_bv_int = arith_op_bv_int_no0 tmod_int false 1
 
 let mod_mword_int l r = Machine_word.modulo l (wordFromInteger r)
 let quot_mword_int l r = Machine_word.unsignedDivide l (wordFromInteger r)
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 5e6537a8..f657803f 100644
--- a/src/gen_lib/sail2_values.lem
+++ b/src/gen_lib/sail2_values.lem
@@ -104,21 +104,25 @@ let upper n = n
 
 (* Modulus operation corresponding to quot below -- result
    has sign of dividend. *)
-let hardware_mod (a: integer) (b:integer) : integer =
+let tmod_int (a: integer) (b:integer) : integer =
   let m = (abs a) mod (abs b) in
   if a < 0 then ~m else m
 
+let hardware_mod = tmod_int
+
 (* There are different possible answers for integer divide regarding
 rounding behaviour on negative operands. Positive operands always
 round down so derive the one we want (trucation towards zero) from
 that *)
-let hardware_quot (a:integer) (b:integer) : integer =
+let tdiv_int (a:integer) (b:integer) : integer =
   let q = (abs a) / (abs b) in
   if ((a<0) = (b<0)) then
     q  (* same sign -- result positive *)
   else
     ~q (* different sign -- result negative *)
 
+let hardware_quot = tdiv_int
+
 let max_64u = (integerPow 2 64) - 1
 let max_64  = (integerPow 2 63) - 1
 let min_64  = 0 - (integerPow 2 63)
@@ -652,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 =