Some more refactoring of Sail library

- Remove start indices and indexing order from bitvector types. Instead add
  them as arguments to functions accessing/updating bitvectors. These arguments
are effectively implicit, thanks to wrappers in prelude_wrappers.sail and a
"sizeof" rewriting pass.

- Add a typeclass for bitvectors with a few basic functions (converting to/from
  bitlists, converting to an integer, getting and setting bits). Make both
monads use this interface, so that they work with both the bitlist and the
machine word representation of bitvectors.

1 files changed, 31 insertions, 29 deletions

diff --git a/src/gen_lib/sail_operators.lem b/src/gen_lib/sail_operators.lem
index a760fb42..7b117726 100644
--- a/src/gen_lib/sail_operators.lem
+++ b/src/gen_lib/sail_operators.lem
@@ -18,14 +18,15 @@ let inline (^^^) = bitvector_concat
 let bitvector_subrange_inc = vector_subrange_inc
 let bitvector_subrange_dec = vector_subrange_dec
 
-let vector_subrange_bl (v, i, j) =
+let vector_subrange_bl (start, v, i, j) =
   let v' = slice v i j in
   get_elems v'
+let vector_subrange_bl_dec = vector_subrange_bl
 
 let bitvector_access_inc = vector_access_inc
 let bitvector_access_dec = vector_access_dec
 let bitvector_update_pos_dec = update_pos
-let bitvector_update_dec = vector_update_dec
+let bitvector_update_subrange_dec = vector_update_dec
 
 let extract_only_bit = extract_only_element
 
@@ -60,7 +61,7 @@ let bitwise_and = bitwise_binop (&&)
 let bitwise_or = bitwise_binop (||)
 let bitwise_xor = bitwise_binop xor
 
-let unsigned (Vector bs _ _) : integer =
+(*let unsigned (Vector bs _ _) : integer =
   let (sum,_) =
     List.foldr
       (fun b (acc,exp) ->
@@ -70,7 +71,7 @@ let unsigned (Vector bs _ _) : integer =
         | BU -> failwith "unsigned: vector has undefined bits"
         end)
       (0,0) bs in
-  sum
+  sum*)
 
 let unsigned_big = unsigned
 
@@ -155,7 +156,7 @@ let add_one_bit_ignore_overflow bits =
   List.reverse (add_one_bit_ignore_overflow_aux (List.reverse bits))
   
 
-let to_vec is_inc ((len : integer),(n : integer)) =
+let to_norm_vec is_inc ((len : integer),(n : integer)) =
   let start = if is_inc then 0 else len - 1 in
   let bits = to_bin (naturalFromInteger (abs n)) in
   let len_bits = integerFromNat (List.length bits) in
@@ -168,12 +169,12 @@ let to_vec is_inc ((len : integer),(n : integer)) =
   else Vector (add_one_bit_ignore_overflow (bitwise_not_bitlist bits'))
               start is_inc
 
-let to_vec_big = to_vec
+let to_vec_big = to_norm_vec
 
-let to_vec_inc (start, len, n) = set_vector_start (start, to_vec true (len, n))
-let to_vec_norm_inc (len, n) = to_vec true (len, n)
-let to_vec_dec (start, len, n) = set_vector_start (start, to_vec false (len, n))
-let to_vec_norm_dec (len, n) = to_vec false (len, n)
+let to_vec_inc (start, len, n) = set_vector_start (start, to_norm_vec true (len, n))
+let to_vec_norm_inc (len, n) = to_norm_vec true (len, n)
+let to_vec_dec (start, len, n) = set_vector_start (start, to_norm_vec false (len, n))
+let to_vec_norm_dec (len, n) = to_norm_vec false (len, n)
 
 let cast_0_vec = to_vec_dec
 let cast_1_vec = to_vec_dec
@@ -185,8 +186,8 @@ let to_vec_undef is_inc (len : integer) =
 let to_vec_inc_undef = to_vec_undef true
 let to_vec_dec_undef = to_vec_undef false
 
-let exts (start, len, vec) = set_vector_start (start, to_vec (get_dir vec) (len,signed vec))
-let extz (start, len, vec) = set_vector_start (start, to_vec (get_dir vec) (len,unsigned vec))
+let exts (start, len, vec) = set_vector_start (start, to_norm_vec (get_dir vec) (len,signed vec))
+let extz (start, len, vec) = set_vector_start (start, to_norm_vec (get_dir vec) (len,unsigned vec))
 
 let exts_big (start, len, vec) = set_vector_start (start, to_vec_big (get_dir vec) (len, signed_big vec))
 let extz_big (start, len, vec) = set_vector_start (start, to_vec_big (get_dir vec) (len, unsigned_big vec))
@@ -212,7 +213,7 @@ let mult_int = mult
 let arith_op_vec op sign (size : integer) (Vector _ _ is_inc as l) r =
   let (l',r') = (to_num sign l, to_num sign r) in
   let n = op l' r' in
-  to_vec is_inc (size * (length l),n)
+  to_norm_vec is_inc (size * (length l),n)
 
 
 (* add_vec
@@ -234,7 +235,7 @@ let add_vec (l, r) = add_VVV l r
 let sub_vec (l, r) = minus_VVV l r
 
 let arith_op_vec_range op sign size (Vector _ _ is_inc as l) r =
-  arith_op_vec op sign size l (to_vec is_inc (length l,r))
+  arith_op_vec op sign size l (to_norm_vec is_inc (length l,r))
 
 (* add_vec_range
  * add_vec_range_signed
@@ -252,7 +253,7 @@ let add_vec_int (l, r) = add_VIV l r
 let sub_vec_int (l, r) = minus_VIV l r
 
 let arith_op_range_vec op sign size l (Vector _ _ is_inc as r) =
-  arith_op_vec op sign size (to_vec is_inc (length r, l)) r
+  arith_op_vec op sign size (to_norm_vec is_inc (length r, l)) r
 
 (* add_range_vec
  * add_range_vec_signed
@@ -301,7 +302,7 @@ let addS_VVI = arith_op_vec_vec_range integerAdd true
 let arith_op_vec_bit op sign (size : integer) (Vector _ _ is_inc as l)r =
   let l' = to_num sign l in
   let n = op l' (match r with | B1 -> (1 : integer) | _ -> 0 end) in
-  to_vec is_inc (length l * size,n)
+  to_norm_vec is_inc (length l * size,n)
 
 (* add_vec_bit
  * add_vec_bit_signed
@@ -318,8 +319,8 @@ let rec arith_op_overflow_vec (op : integer -> integer -> integer) sign size (Ve
   let (l_unsign,r_unsign) = (to_num false l,to_num false r) in
   let n = op l_sign r_sign in
   let n_unsign = op l_unsign r_unsign in
-  let correct_size_num = to_vec is_inc (act_size,n) in
-  let one_more_size_u = to_vec is_inc (act_size + 1,n_unsign) in
+  let correct_size_num = to_norm_vec is_inc (act_size,n) in
+  let one_more_size_u = to_norm_vec is_inc (act_size + 1,n_unsign) in
   let overflow =
     if n <= get_max_representable_in sign len &&
          n >= get_min_representable_in sign len
@@ -352,8 +353,8 @@ let rec arith_op_overflow_vec_bit (op : integer -> integer -> integer) sign (siz
     | BU -> failwith "arith_op_overflow_vec_bit applied to undefined bit"
     end in
 (*    | _ -> assert false *)
-  let correct_size_num = to_vec is_inc (act_size,n) in
-  let one_larger = to_vec is_inc (act_size + 1,nu) in
+  let correct_size_num = to_norm_vec is_inc (act_size,n) in
+  let one_larger = to_norm_vec is_inc (act_size + 1,nu) in
   let overflow =
     if changed
     then
@@ -406,7 +407,7 @@ let rec arith_op_vec_no0 (op : integer -> integer -> integer) sign size ((Vector
     | _ -> (false,0)
     end in
   if representable
-  then to_vec is_inc (act_size,n')
+  then to_norm_vec is_inc (act_size,n')
   else Vector (List.replicate (natFromInteger act_size) BU) start is_inc
 
 let mod_VVV = arith_op_vec_no0 hardware_mod false 1
@@ -429,7 +430,7 @@ let arith_op_overflow_no0_vec op sign size ((Vector _ start is_inc) as l) r =
     end in
   let (correct_size_num,one_more) =
     if representable then
-      (to_vec is_inc (act_size,n'),to_vec is_inc (act_size + 1,n_u'))
+      (to_norm_vec is_inc (act_size,n'),to_norm_vec is_inc (act_size + 1,n_u'))
     else
       (Vector (List.replicate (natFromInteger act_size) BU) start is_inc,
        Vector (List.replicate (natFromInteger (act_size + 1)) BU) start is_inc) in
@@ -440,7 +441,7 @@ let quotO_VVV = arith_op_overflow_no0_vec hardware_quot false 1
 let quotSO_VVV = arith_op_overflow_no0_vec hardware_quot true 1
 
 let arith_op_vec_range_no0 op sign size (Vector _ _ is_inc as l) r =
-  arith_op_vec_no0 op sign size l (to_vec is_inc (length l,r))
+  arith_op_vec_no0 op sign size l (to_norm_vec is_inc (length l,r))
 
 let mod_VIV = arith_op_vec_range_no0 hardware_mod false 1
 
@@ -514,7 +515,8 @@ let eq_vec_vec (l,r) = eq (to_num true l, to_num true r)
 let neq (l,r) = not (eq (l,r))
 let neq_bit (l,r) = not (eq_bit (l,r))
 let neq_range (l,r) = not (eq_range (l,r))
-let neq_vec (l,r) = not (eq_vec_vec (l,r))
+let neq_vec (l,r) = not (eq_vec (l,r))
+let neq_vec_vec (l,r) = not (eq_vec_vec (l,r))
 let neq_vec_range (l,r) = not (eq_vec_range (l,r))
 let neq_range_vec (l,r) = not (eq_range_vec (l,r))
 
@@ -532,20 +534,20 @@ let make_bitvector_undef length =
 
 (* let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n) *)
 
-let mask' (start, n, Vector bits _ dir) =
+let mask (start, n, Vector bits _ dir) =
   let current_size = List.length bits in
   Vector (drop (current_size - (natFromInteger n)) bits) start dir
 
 
 (* Register operations *)
 
-let update_reg_range i j reg_val new_val = update reg_val i j new_val
-let update_reg_bit i reg_val bit = update_pos reg_val i bit
+(*let update_reg_range i j reg_val new_val = update reg_val i j new_val
+let update_reg_pos i reg_val bit = update_pos reg_val i bit
 let update_reg_field_range regfield i j reg_val new_val =
   let current_field_value = regfield.get_field reg_val in
   let new_field_value = update current_field_value i j new_val in
   regfield.set_field reg_val new_field_value
-let write_reg_field_bit regfield i reg_val bit =
+(*let write_reg_field_pos regfield i reg_val bit =
   let current_field_value = regfield.get_field reg_val in
   let new_field_value = update_pos current_field_value i bit in
-  regfield.set_field reg_val new_field_value
+  regfield.set_field reg_val new_field_value*)*)