Pretty-print bitvector expressions

- Add case distinctions between bitvector types and vectors of other element
  types (e.g. registers) and use the corresponding operations (i.e. "bvslice",
"bvaccess", etc for the former, and "slice", "access", etc for the latter) when
pretty-printing expressions
- Add type annotations to expressions when the type includes bitvectors with
  concretely known length
- Update state.lem to use bitvectors (in the interface, at least; internally,
  bitvectors are still stored as bit lists for now, since that makes it easier
to support storing different registers with different lengths)

This has been tested with the CHERI-MIPS model with some success, but some
things are still missing:
- Bitvector patterns are not handled yet
- Some bitvector length monomorphisation is needed in a few places of the model
- Some type annotations are missing, because the (old) Sail type checker does
  not infer bitvector lengths in some instances where one would hope it to do
that; this should be checked with the new type checker

3 files changed, 76 insertions, 53 deletions

diff --git a/src/gen_lib/prompt.lem b/src/gen_lib/prompt.lem
index 426b0811..70850dc1 100644
--- a/src/gen_lib/prompt.lem
+++ b/src/gen_lib/prompt.lem
@@ -71,12 +71,12 @@ let read_reg_range reg i j =
   read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger j))
 let read_reg_bit reg i =
   read_reg_aux (external_reg_slice reg (natFromInteger i,natFromInteger i)) >>= fun v ->
-  return (extract_only_bit v)
+  return (extract_only_element v)
 let read_reg_field reg regfield =
   read_reg_aux (external_reg_field_whole reg regfield)
 let read_reg_bitfield reg regfield =
   read_reg_aux (external_reg_field_whole reg regfield) >>= fun v ->
-  return (extract_only_bit v)
+  return (extract_only_element v)
 
 val write_reg_aux : reg_name -> vector bitU -> M unit
 let write_reg_aux reg_name v =
diff --git a/src/gen_lib/sail_values.lem b/src/gen_lib/sail_values.lem
index ecfd3ce7..bccdd8f2 100644
--- a/src/gen_lib/sail_values.lem
+++ b/src/gen_lib/sail_values.lem
@@ -218,6 +218,14 @@ instance forall 'a. Show 'a => (Show (bitvector 'a))
   let show = showBitvector
 end
 
+let bvec_to_vec (Bitvector bs start is_inc) =
+  let bits = List.map bool_to_bitU (bitlistFromWord bs) in
+  Vector bits start is_inc
+
+let vec_to_bvec (Vector elems start is_inc) =
+  let word = wordFromBitlist (List.map bitU_to_bool elems) in
+  Bitvector word start is_inc
+
 (*** Vector operations *)
 
 val set_bitvector_start : forall 'a. integer -> bitvector 'a -> bitvector 'a
@@ -265,7 +273,7 @@ let bvupdate_aux (Bitvector bs start is_inc) i j bs' =
   let bits = word_update bs lo hi bs' in
   Bitvector bits start is_inc
 
-val bvupdate : forall 'a. bitvector 'a -> integer -> integer -> bitvector 'a -> bitvector 'a
+val bvupdate : forall 'a 'b. bitvector 'a -> integer -> integer -> bitvector 'b -> bitvector 'a
 let bvupdate v i j (Bitvector bs' _ _) =
   bvupdate_aux v i j bs'
 
@@ -273,25 +281,32 @@ let bvupdate v i j (Bitvector bs' _ _) =
 val getBit' : forall 'a. mword 'a -> nat -> bool
 let getBit' w n = getBit w (naturalFromNat n)
 
-val bvaccess : forall 'a. bitvector 'a -> integer -> bool
-let bvaccess (Bitvector bs start is_inc) n =
+val bvaccess : forall '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))
+  else getBit' bs (natFromInteger (start - n)))
 
-val bvupdate_pos : forall 'a. Size 'a => bitvector 'a -> integer -> bool -> bitvector 'a
+val bvupdate_pos : forall 'a. Size 'a => bitvector 'a -> integer -> bitU -> bitvector 'a
 let bvupdate_pos v n b =
-  bvupdate_aux v n n ((wordFromNatural (if b then 1 else 0)) : mword ty1)
+  bvupdate_aux v n n ((wordFromNatural (if bitU_to_bool b then 1 else 0)) : mword ty1)
 
 (*** Bit vector operations *)
 
+let extract_only_element (Vector elems _ _) = match elems with
+  | [] -> failwith "extract_only_element called for empty vector"
+  | [e] -> e
+  | _ -> failwith "extract_only_element called for vector with more elements"
+end
+
+val extract_only_bit : bitvector ty1 -> bitU
 let extract_only_bit (Bitvector elems _ _) =
-  let l = word_length elems in
-  if l = 1 then
-    msb elems
-  else if l = 0 then
+  (*let l = word_length elems in
+  if l = 1 then*)
+    bool_to_bitU (msb elems)
+  (*else if l = 0 then
     failwith "extract_single_bit called for empty vector"
   else
-    failwith "extract_single_bit called for vector with more bits"
+    failwith "extract_single_bit called for vector with more bits"*)
 
 let pp_bitu_vector (Vector elems start inc) =
   let elems_pp = List.foldl (fun acc elem -> acc ^ showBitU elem) "" elems in
@@ -302,7 +317,7 @@ let most_significant (Bitvector v _ _) =
   if word_length v = 0 then
     failwith "most_significant applied to empty vector"
   else
-    msb v
+    bool_to_bitU (msb v)
 
 let bitwise_not_bitlist = List.map bitwise_not_bit
 
@@ -402,13 +417,14 @@ let to_vec_big = to_vec
 
 let to_vec_inc = to_vec true
 let to_vec_dec = to_vec false
-(* TODO??
+
+(* TODO: Think about undefined bit(vector)s *)
 let to_vec_undef is_inc (len : integer) =
-  Vector (replicate (natFromInteger len) BU) (if is_inc then 0 else len-1) is_inc
+  Bitvector (failwith "undefined bitvector") (if is_inc then 0 else len-1) is_inc
 
 let to_vec_inc_undef = to_vec_undef true
 let to_vec_dec_undef = to_vec_undef false
-*)
+
 let exts (len, vec) = to_vec (bvget_dir vec) (len,signed vec)
 let extz (len, vec) = to_vec (bvget_dir vec) (len,unsigned vec)
 
@@ -737,9 +753,9 @@ let make_bitvector_undef length =
 
 (* let bitwise_not_range_bit n = bitwise_not (to_vec defaultDir n) *)
 
-let mask (n,Vector bits start dir) =
-  let current_size = List.length bits in
-  Vector (drop (current_size - (natFromInteger n)) bits) (if dir then 0 else (n-1)) dir
+let mask (n,bv) =
+  let len = bvlength bv in
+  bvslice_raw bv (len - n) (len - 1)
 
 
 val byte_chunks : forall 'a. nat -> list 'a -> list (list 'a)
@@ -1026,4 +1042,3 @@ let diafp_to_dia reginfo = function
   | DIAFP_concrete v -> DIA_concrete_address (address_of_bitv v)
   | DIAFP_reg r -> DIA_register (regfp_to_reg reginfo r)
 end
-
diff --git a/src/gen_lib/state.lem b/src/gen_lib/state.lem
index 430ee562..709052fe 100644
--- a/src/gen_lib/state.lem
+++ b/src/gen_lib/state.lem
@@ -47,12 +47,12 @@ let set_reg state reg bitv =
   <| state with regstate = Map.insert reg bitv state.regstate |>
 
 
-val read_mem : bool -> read_kind -> vector bitU -> integer -> M (vector bitU)
+val read_mem : forall 'a 'b. Size 'b => bool -> read_kind -> bitvector 'a -> integer -> M (bitvector 'b)
 let read_mem dir read_kind addr sz state =
-  let addr = integer_of_address (address_of_bitv addr) in
+  let addr = unsigned addr in
   let addrs = range addr (addr+sz-1) in
   let memory_value = List.map (fun addr -> Map_extra.find addr state.memstate) addrs in
-  let value = Sail_values.internal_mem_value dir memory_value in
+  let value = vec_to_bvec (Sail_values.internal_mem_value dir memory_value) in
   let is_exclusive = match read_kind with
     | Sail_impl_base.Read_plain -> false
     | Sail_impl_base.Read_reserve -> true
@@ -69,9 +69,9 @@ let read_mem dir read_kind addr sz state =
 (* caps are aligned at 32 bytes *)
 let cap_alignment = (32 : integer)
 
-val read_tag : bool -> read_kind -> vector bitU -> M bitU
+val read_tag : forall 'a. bool -> read_kind -> bitvector 'a -> M bitU
 let read_tag dir read_kind addr state =
-  let addr = (integer_of_address (address_of_bitv addr)) / cap_alignment in
+  let addr = (unsigned addr) / cap_alignment in
   let tag = match (Map.lookup addr state.tagstate) with
     | Just t -> t
     | Nothing -> B0
@@ -96,18 +96,18 @@ let excl_result () state =
     (Left true,  <| state with last_exclusive_operation_was_load = false |>) in
   (Left false, state) :: if state.last_exclusive_operation_was_load then [success] else []
 
-val write_mem_ea : write_kind -> vector bitU -> integer -> M unit
+val write_mem_ea : forall 'a. write_kind -> bitvector 'a -> integer -> M unit
 let write_mem_ea write_kind addr sz state = 
-  let addr = integer_of_address (address_of_bitv addr) in
+  let addr = unsigned addr in
   [(Left (), <| state with write_ea = Just (write_kind,addr,sz) |>)]
 
-val write_mem_val : vector bitU -> M bool
+val write_mem_val : forall 'b. bitvector 'b -> M bool
 let write_mem_val v state =
   let (write_kind,addr,sz) = match state.write_ea with
     | Nothing -> failwith "write ea has not been announced yet"
     | Just write_ea -> write_ea end in
   let addrs = range addr (addr+sz-1) in
-  let v = external_mem_value v in
+  let v = external_mem_value (bvec_to_vec v) in
   let addresses_with_value = List.zip addrs v in
   let memstate = List.foldl (fun mem (addr,v) -> Map.insert addr v mem)
                             state.memstate addresses_with_value in
@@ -122,16 +122,16 @@ let write_tag t state =
   let tagstate = Map.insert taddr t state.tagstate in
   [(Left true,  <| state with tagstate = tagstate |>)]
 
-val read_reg : register -> M (vector bitU)
+val read_reg : forall 'a. Size 'a => register -> M (bitvector 'a)
 let read_reg reg state =
-  let v = Map_extra.find (name_of_reg reg) state.regstate in
+  let v = get_reg state (name_of_reg reg) in
+  [(Left (vec_to_bvec v),state)]
+let read_reg_range reg i j state =
+  let v = slice (get_reg state (name_of_reg reg)) i j in
+  [(Left (vec_to_bvec v),state)]
+let read_reg_bit reg i state =
+  let v = access (get_reg state (name_of_reg reg)) i in
   [(Left v,state)]
-let read_reg_range reg i j =
-  read_reg reg >>= fun rv ->
-  return (slice rv i j)
-let read_reg_bit reg i =
-  read_reg_range reg i i >>= fun v ->
-  return (extract_only_bit v)
 let read_reg_field reg regfield =
   let (i,j) = register_field_indices reg regfield in
   read_reg_range reg i j
@@ -139,25 +139,30 @@ let read_reg_bitfield reg regfield =
   let (i,_) = register_field_indices reg regfield in
   read_reg_bit reg i 
 
-val write_reg : register -> vector bitU -> M unit
+val write_reg : forall 'a. Size 'a => register -> bitvector 'a -> M unit
 let write_reg reg v state =
-  [(Left (),<| state with regstate = Map.insert (name_of_reg reg) v state.regstate |>)]
-let write_reg_range reg i j v =
-  read_reg reg >>= fun current_value ->
-  let new_value = update current_value i j v in
-  write_reg reg new_value
-let write_reg_bit reg i bit =
-  write_reg_range reg i i (Vector [bit] i (is_inc_of_reg reg))
+  [(Left (), set_reg state (name_of_reg reg) (bvec_to_vec v))]
+let write_reg_range reg i j v state =
+  let current_value = get_reg state (name_of_reg reg) in
+  let new_value = update current_value i j (bvec_to_vec v) in
+  [(Left (), set_reg state (name_of_reg reg) new_value)]
+let write_reg_bit reg i bit state =
+  let current_value = get_reg state (name_of_reg reg) in
+  let new_value = update_pos current_value i bit in
+  [(Left (), set_reg state (name_of_reg reg) new_value)]
 let write_reg_field reg regfield =
-  let (i,j) = register_field_indices reg regfield in  
+  let (i,j) = register_field_indices reg regfield in
   write_reg_range reg i j
 let write_reg_bitfield reg regfield =
   let (i,_) = register_field_indices reg regfield in  
   write_reg_bit reg i
-let write_reg_field_range reg regfield i j v =
-  read_reg_field reg regfield >>= fun current_field_value ->
-  let new_field_value = update current_field_value i j v in
-  write_reg_field reg regfield new_field_value
+let write_reg_field_range reg regfield i j v state =
+  let (i0,j0) = register_field_indices reg regfield in
+  let current_value = get_reg state (name_of_reg reg) in
+  let current_field_value = slice current_value i0 j0 in
+  let new_field_value = update current_field_value i j (bvec_to_vec v) in
+  let new_value = update current_value i j new_field_value in
+  [(Left (), set_reg state (name_of_reg reg) new_value)]
 
 
 val barrier : barrier_kind -> M unit
@@ -186,7 +191,8 @@ let rec foreachM_dec (i,stop,by) vars body =
     foreachM_dec (i - by,stop,by) vars body
   else return vars
 
-let write_two_regs r1 r2 vec =
+let write_two_regs r1 r2 bvec state =
+  let vec = bvec_to_vec bvec in
   let is_inc =
     let is_inc_r1 = is_inc_of_reg r1 in
     let is_inc_r2 = is_inc_of_reg r2 in
@@ -205,4 +211,6 @@ let write_two_regs r1 r2 vec =
     if is_inc
     then slice vec (size_r1 - start_vec) (size_vec - start_vec)
     else slice vec (start_vec - size_r1) (start_vec - size_vec) in
-  write_reg r1 r1_v >> write_reg r2 r2_v
+  let state1 = set_reg state (name_of_reg r1) r1_v in
+  let state2 = set_reg state1 (name_of_reg r2) r2_v in
+  [(Left (), state2)]