1 files changed, 46 insertions, 43 deletions

diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index eb5cdef5..f994ae22 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -258,12 +258,13 @@ let adjust_dec = reset_bitvector_start
 
 let inline (^^^) = bitvector_concat
 
-val bvslice : forall 'a 'b. bitvector 'a -> integer -> integer -> bitvector 'b
+val bvslice : forall 'a 'b. Size 'a => bitvector 'a -> integer -> integer -> bitvector 'b
 let bvslice (Bitvector bs start is_inc) i j =
   let iN = natFromInteger i in
   let jN = natFromInteger j in
   let startN = natFromInteger start in
-  let (lo,hi) = if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN) in
+  let top = word_length bs - 1 in
+  let (hi,lo) = if is_inc then (top+startN-iN,top+startN-jN) else (top-startN+iN,top-startN+jN) in
   let subvector_bits = word_extract lo hi bs in
   Bitvector subvector_bits i is_inc
 
@@ -286,23 +287,25 @@ let bvslice_raw (Bitvector bs start is_inc) i j =
   let len = integerFromNat (word_length bits) in
   Bitvector bits (if is_inc then 0 else len - 1) is_inc
 
-val bvupdate_aux : forall 'a 'b. bitvector 'a -> integer -> integer -> mword 'b -> bitvector 'a
+val bvupdate_aux : forall 'a 'b. Size 'a => bitvector 'a -> integer -> integer -> mword 'b -> bitvector 'a
 let bvupdate_aux (Bitvector bs start is_inc) i j bs' =
   let iN = natFromInteger i in
   let jN = natFromInteger j in
   let startN = natFromInteger start in
-  let (lo,hi) = if is_inc then (iN-startN,jN-startN) else (startN-iN,startN-jN) in
+  let top = word_length bs - 1 in
+  let (hi,lo) = if is_inc then (top+startN-iN,top+startN-jN) else (top-startN+iN,top-startN+jN) in
   let bits = word_update bs lo hi bs' in
   Bitvector bits start is_inc
 
-val bvupdate : forall 'a 'b. bitvector 'a -> integer -> integer -> bitvector 'b -> bitvector 'a
+val bvupdate : forall 'a 'b. Size 'a => bitvector 'a -> integer -> integer -> bitvector 'b -> bitvector 'a
 let bvupdate v i j (Bitvector bs' _ _) =
   bvupdate_aux v i j bs'
 
-val bvaccess : forall 'a. bitvector 'a -> integer -> bitU
+val bvaccess : forall 'a. Size 'a => bitvector 'a -> integer -> bitU
 let bvaccess (Bitvector bs start is_inc) n = bool_to_bitU (
-  if is_inc then getBit bs (natFromInteger (n - start))
-  else getBit bs (natFromInteger (start - n)))
+  let top = integerFromNat (word_length bs) - 1 in
+  if is_inc then getBit bs (natFromInteger (top + start - n))
+  else getBit bs (natFromInteger (top + n - start)))
 
 val bvupdate_pos : forall 'a. Size 'a => bitvector 'a -> integer -> bitU -> bitvector 'a
 let bvupdate_pos v n b =
@@ -353,9 +356,9 @@ let bitwise_not (Bitvector bs start is_inc) =
 let bitwise_binop op (Bitvector bsl start is_inc, Bitvector bsr _ _) =
   Bitvector (op bsl bsr) start is_inc
 
-let bitwise_and = bitwise_binop lAnd
-let bitwise_or = bitwise_binop lOr
-let bitwise_xor = bitwise_binop lXor
+let bitwise_and x = bitwise_binop lAnd x
+let bitwise_or x = bitwise_binop lOr x
+let bitwise_xor x = bitwise_binop lXor x
 
 let unsigned (Bitvector bs _ _) : integer = unsignedIntegerFromWord bs
 let unsigned_big = unsigned
@@ -549,9 +552,9 @@ let arith_op_range_vec_range op sign l r = op l (to_num sign r)
  * add_range_vec_range_signed
  * minus_range_vec_range
  *)
-let add_IVI = arith_op_range_vec_range integerAdd false
-let addS_IVI = arith_op_range_vec_range integerAdd true
-let minus_IVI = arith_op_range_vec_range integerMinus false
+let add_IVI x y = arith_op_range_vec_range integerAdd false x y
+let addS_IVI x y = arith_op_range_vec_range integerAdd true x y
+let minus_IVI x y = arith_op_range_vec_range integerMinus false x y
 
 let arith_op_vec_range_range op sign l r = op (to_num sign l) r
 
@@ -559,9 +562,9 @@ let arith_op_vec_range_range op sign l r = op (to_num sign l) r
  * add_vec_range_range_signed
  * minus_vec_range_range
  *)
-let add_VII = arith_op_vec_range_range integerAdd false
-let addS_VII = arith_op_vec_range_range integerAdd true
-let minus_VII = arith_op_vec_range_range integerMinus false
+let add_VII x y = arith_op_vec_range_range integerAdd false x y
+let addS_VII x y = arith_op_vec_range_range integerAdd true x y
+let minus_VII x y = arith_op_vec_range_range integerMinus false x y
 
 
 
@@ -572,8 +575,8 @@ let arith_op_vec_vec_range op sign l r =
 (* add_vec_vec_range
  * add_vec_vec_range_signed
  *)
-let add_VVI = arith_op_vec_vec_range integerAdd false
-let addS_VVI = arith_op_vec_vec_range integerAdd true
+let add_VVI x y = arith_op_vec_vec_range integerAdd false x y
+let addS_VVI x y = arith_op_vec_vec_range integerAdd true x y
 
 let arith_op_vec_bit op sign (size : integer) (Bitvector _ _ is_inc as l) r =
   let l' = to_num sign l in
@@ -664,9 +667,9 @@ let shift_op_vec op (Bitvector bs start is_inc,(n : integer)) =
      Bitvector (rotateLeft n bs) start is_inc
   end
 
-let bitwise_leftshift = shift_op_vec LL_shift (*"<<"*)
-let bitwise_rightshift = shift_op_vec RR_shift (*">>"*)
-let bitwise_rotate = shift_op_vec LLL_shift (*"<<<"*)
+let bitwise_leftshift x = shift_op_vec LL_shift x (*"<<"*)
+let bitwise_rightshift x = shift_op_vec RR_shift x (*">>"*)
+let bitwise_rotate x = shift_op_vec LLL_shift x (*"<<<"*)
 
 let shiftl = bitwise_leftshift
 
@@ -747,44 +750,44 @@ let compare_op_vec op sign (l,r) =
   let (l',r') = (to_num sign l, to_num sign r) in
   compare_op op (l',r')
 
-let lt_vec = compare_op_vec (<) true
-let gt_vec = compare_op_vec (>) true
-let lteq_vec = compare_op_vec (<=) true
-let gteq_vec = compare_op_vec (>=) true
+let lt_vec x = compare_op_vec (<) true x
+let gt_vec x = compare_op_vec (>) true x
+let lteq_vec x = compare_op_vec (<=) true x
+let gteq_vec x = compare_op_vec (>=) true x
 
-let lt_vec_signed = compare_op_vec (<) true
-let gt_vec_signed = compare_op_vec (>) true
-let lteq_vec_signed = compare_op_vec (<=) true
-let gteq_vec_signed = compare_op_vec (>=) true
-let lt_vec_unsigned = compare_op_vec (<) false
-let gt_vec_unsigned = compare_op_vec (>) false
-let lteq_vec_unsigned = compare_op_vec (<=) false
-let gteq_vec_unsigned = compare_op_vec (>=) false
+let lt_vec_signed x = compare_op_vec (<) true x
+let gt_vec_signed x = compare_op_vec (>) true x
+let lteq_vec_signed x = compare_op_vec (<=) true x
+let gteq_vec_signed x = compare_op_vec (>=) true x
+let lt_vec_unsigned x = compare_op_vec (<) false x
+let gt_vec_unsigned x = compare_op_vec (>) false x
+let lteq_vec_unsigned x = compare_op_vec (<=) false x
+let gteq_vec_unsigned x = compare_op_vec (>=) false x
 
 let lt_svec = lt_vec_signed
 
 let compare_op_vec_range op sign (l,r) =
   compare_op op ((to_num sign l),r)
 
-let lt_vec_range = compare_op_vec_range (<) true
-let gt_vec_range = compare_op_vec_range (>) true
-let lteq_vec_range = compare_op_vec_range (<=) true
-let gteq_vec_range = compare_op_vec_range (>=) true
+let lt_vec_range x = compare_op_vec_range (<) true x
+let gt_vec_range x = compare_op_vec_range (>) true x
+let lteq_vec_range x = compare_op_vec_range (<=) true x
+let gteq_vec_range x = compare_op_vec_range (>=) true x
 
 let compare_op_range_vec op sign (l,r) =
   compare_op op (l, (to_num sign r))
 
-let lt_range_vec = compare_op_range_vec (<) true
-let gt_range_vec = compare_op_range_vec (>) true
-let lteq_range_vec = compare_op_range_vec (<=) true
-let gteq_range_vec = compare_op_range_vec (>=) true
+let lt_range_vec x = compare_op_range_vec (<) true x
+let gt_range_vec x = compare_op_range_vec (>) true x
+let lteq_range_vec x = compare_op_range_vec (<=) true x
+let gteq_range_vec x = compare_op_range_vec (>=) true x
 
 val eq : forall 'a. Eq 'a => 'a * 'a -> bool
 let eq (l,r) = (l = r)
 let eq_range (l,r) = (l = r)
 
 val eq_vec : forall 'a. bitvector 'a * bitvector 'a -> bool
-let eq_vec (l,r) = (l = r)
+let eq_vec (Bitvector l _ _,Bitvector r _ _) = (l = r)
 let eq_bit (l,r) = (l = r)
 let eq_vec_range (l,r) = eq (to_num false l,r)
 let eq_range_vec (l,r) = eq (l, to_num false r)