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

9 files changed, 335 insertions, 155 deletions

diff --git a/isabelle-lib/Makefile b/isabelle-lib/Makefile
index bd4066cd..11cdbc27 100644
--- a/isabelle-lib/Makefile
+++ b/isabelle-lib/Makefile
@@ -37,5 +37,5 @@ prompt.lem: ../src/gen_lib/prompt.lem
 	cp $< .
 
 clean:
-	rm $(THYS) $(LEMS)
-	rm *Auxiliary.thy
+	-rm $(THYS) $(LEMS)
+	-rm *Auxiliary.thy
diff --git a/mips/mips_extras_embed_sequential.lem b/mips/mips_extras_embed_sequential.lem
index 73dc42ed..708c1f63 100644
--- a/mips/mips_extras_embed_sequential.lem
+++ b/mips/mips_extras_embed_sequential.lem
@@ -4,10 +4,10 @@ open import Sail_impl_base
 open import Sail_values
 open import State
 
-val MEMr             : (vector bitU * integer) -> M (vector bitU)
-val MEMr_reserve     : (vector bitU * integer) -> M (vector bitU)
-val MEMr_tag         : (vector bitU * integer) -> M (bitU * vector bitU)
-val MEMr_tag_reserve : (vector bitU * integer) -> M (bitU * vector bitU)
+val MEMr             : forall 'a 'b. Size 'b => (bitvector 'a * integer) -> M (bitvector 'b)
+val MEMr_reserve     : forall 'a 'b. Size 'b => (bitvector 'a * integer) -> M (bitvector 'b)
+val MEMr_tag         : forall 'a 'b. Size 'b => (bitvector 'a * integer) -> M (bitU * bitvector 'b)
+val MEMr_tag_reserve : forall 'a 'b. Size 'b => (bitvector 'a * integer) -> M (bitU * bitvector 'b)
 
 let MEMr (addr,size)             = read_mem false Read_plain addr size
 let MEMr_reserve (addr,size)     = read_mem false Read_reserve addr size
@@ -23,10 +23,10 @@ let MEMr_tag_reserve (addr,size) =
   return (t, v)
 
 
-val MEMea                 : (vector bitU * integer) -> M unit
-val MEMea_conditional     : (vector bitU * integer) -> M unit
-val MEMea_tag             : (vector bitU * integer) -> M unit
-val MEMea_tag_conditional : (vector bitU * integer) -> M unit
+val MEMea                 : forall 'a. (bitvector 'a * integer) -> M unit
+val MEMea_conditional     : forall 'a. (bitvector 'a * integer) -> M unit
+val MEMea_tag             : forall 'a. (bitvector 'a * integer) -> M unit
+val MEMea_tag_conditional : forall 'a. (bitvector 'a * integer) -> M unit
 
 let MEMea (addr,size)                 = write_mem_ea Write_plain addr size
 let MEMea_conditional (addr,size)     = write_mem_ea Write_conditional addr size
@@ -35,10 +35,10 @@ let MEMea_tag (addr,size)             = write_mem_ea Write_plain addr size
 let MEMea_tag_conditional (addr,size) = write_mem_ea Write_conditional addr size
 
 
-val MEMval                 : (vector bitU * integer * vector bitU) -> M unit
-val MEMval_conditional     : (vector bitU * integer * vector bitU) -> M bitU
-val MEMval_tag             : (vector bitU * integer * bitU * vector bitU) -> M unit
-val MEMval_tag_conditional : (vector bitU * integer * bitU * vector bitU) -> M bitU
+val MEMval                 : forall 'a 'b. (bitvector 'a * integer * bitvector 'b) -> M unit
+val MEMval_conditional     : forall 'a 'b. (bitvector 'a * integer * bitvector 'b) -> M bitU
+val MEMval_tag             : forall 'a 'b. (bitvector 'a * integer * bitU * bitvector 'b) -> M unit
+val MEMval_tag_conditional : forall 'a 'b. (bitvector 'a * integer * bitU * bitvector 'b) -> M bitU
 
 let MEMval (_,_,v)                   = write_mem_val v >>= fun _ -> return ()
 let MEMval_conditional (_,_,v)       = write_mem_val v >>= fun b -> return (if b then B1 else B0)
@@ -50,7 +50,9 @@ val MEM_sync  : unit -> M unit
 let MEM_sync () = barrier Barrier_MIPS_SYNC
 
 
+(* TODO: Consider moving this to sail_values.lem (after fixing and implementing
+   a default index ordering) *)
 let duplicate (bit,len) =
-  let bits = repeat [bit] len in
+  let bits = repeat [bitU_to_bool bit] len in
   let start = len - 1 in
-  Vector bits start false
+  Bitvector (wordFromBitlist bits) start false
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)]
diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index 65c679ff..5f2e9888 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -118,18 +118,24 @@ let doc_id_lem_ctor (Id_aux(i,_)) =
       * token in case of x ending with star. *)
      separate space [colon; string (String.capitalize x); empty]
 
+let effectful_set =
+  List.exists
+    (fun (BE_aux (eff,_)) ->
+      match eff with
+      | BE_rreg | BE_wreg | BE_rmem | BE_rmemt | BE_wmem | BE_eamem
+      | BE_exmem | BE_wmv | BE_wmvt | BE_barr | BE_depend | BE_nondet
+      | BE_escape -> true
+      | _ -> false)
+
 let effectful (Effect_aux (eff,_)) =
   match eff with
   | Effect_var _ -> failwith "effectful: Effect_var not supported"
-  | Effect_set effs ->
-     List.exists
-       (fun (BE_aux (eff,_)) ->
-         match eff with
-         | BE_rreg | BE_wreg | BE_rmem | BE_rmemt | BE_wmem | BE_eamem
-         | BE_exmem | BE_wmv | BE_wmvt | BE_barr | BE_depend | BE_nondet
-         | BE_escape -> true
-         | _ -> false)
-       effs
+  | Effect_set effs -> effectful_set effs
+
+let effectful_t eff =
+  match eff.effect with
+  | Eset effs -> effectful_set effs
+  | _ -> false
 
 let rec is_number {t=t} =
   match t with
@@ -166,9 +172,20 @@ let doc_typ_lem, doc_atomic_typ_lem =
           Typ_arg_aux (Typ_arg_order ord, _);
           Typ_arg_aux (Typ_arg_typ elem_typ, _)]) ->
          let tpp = match elem_typ with
-           | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) -> string "bitvector" ^^ space ^^ doc_nexp m
+           | Typ_aux (Typ_id (Id_aux (Id "bit",_)),_) ->
+               let len = match m with
+                 | (Nexp_aux(Nexp_constant i,_)) -> string "ty" ^^ doc_int i
+                 | _ -> doc_nexp m in
+               string "bitvector" ^^ space ^^ len
            | _ -> string "vector" ^^ space ^^ typ regtypes elem_typ in
          if atyp_needed then parens tpp else tpp
+      | Typ_app(Id_aux (Id "register", _), [Typ_arg_aux (Typ_arg_typ etyp, _)]) ->
+         (* TODO: Better distinguish register names and contents?
+            The former are represented in the Lem library using a type
+            "register" (without parameters), the latter just using the content
+            type (e.g. "bitvector ty64").  We assume the latter is meant here
+            and drop the "register" keyword. *)
+         fn_typ regtypes atyp_needed etyp
       | Typ_app(Id_aux (Id "range", _),_) ->
          (string "integer")
       | Typ_app(Id_aux (Id "implicit", _),_) ->
@@ -195,12 +212,17 @@ let doc_typ_lem, doc_atomic_typ_lem =
          let tpp = typ regtypes ty in
          if atyp_needed then parens tpp else tpp
     and doc_typ_arg_lem regtypes (Typ_arg_aux(t,_)) = match t with
-      | Typ_arg_typ t -> app_typ regtypes false t
+      | Typ_arg_typ t -> app_typ regtypes true t
       | Typ_arg_nexp n -> empty
       | Typ_arg_order o -> empty
       | Typ_arg_effect e -> empty
   in typ', atomic_typ
 
+let doc_tannot_lem regtypes eff t =
+  let ta = doc_typ_lem regtypes (t_to_typ (normalize_t t)) in
+  if eff then string " : M " ^^ parens ta
+  else string " : " ^^ ta
+
 (* doc_lit_lem gets as an additional parameter the type information from the
  * expression around it: that's a hack, but how else can we distinguish between
  * undefined values of different types ? *)
@@ -276,6 +298,44 @@ let rec doc_pat_lem regtypes apat_needed (P_aux (p,(l,annot)) as pa) = match p w
       | _ -> parens (separate_map comma_sp (doc_pat_lem regtypes false) pats))
      | P_list pats -> brackets (separate_map semi (doc_pat_lem regtypes false) pats) (*Never seen but easy in lem*)
 
+let rec contains_bitvector_type t = match t.t with
+  | Ttup ts -> List.exists contains_bitvector_type ts
+  | Tapp (_, targs) -> is_bit_vector t || List.exists contains_bitvector_type_arg targs
+  | Tabbrev (_,t') -> contains_bitvector_type t'
+  | Tfn (t1,t2,_,_) -> contains_bitvector_type t1 || contains_bitvector_type t2
+  | _ -> false
+and contains_bitvector_type_arg targ = match targ with
+  | TA_typ t -> contains_bitvector_type t
+  | _ -> false
+
+let const_nexp nexp = match nexp.nexp with
+  | Nconst _ -> true
+  | _ -> false
+
+(* Check for variables in types that would be pretty-printed.
+   In particular, in case of vector types, only the element type and the
+   length argument are checked for variables, and the latter only if it is
+   a bitvector; for other types of vectors, the length is not pretty-printed
+   in the type, and the start index is never pretty-printed in vector types. *)
+let rec contains_t_pp_var t = match t.t with
+  | Tvar _ -> true
+  | Tfn (t1,t2,_,_) -> contains_t_pp_var t1 || contains_t_pp_var t2
+  | Ttup ts -> List.exists contains_t_pp_var ts
+  | Tapp ("vector",[_;TA_nexp m;_;TA_typ t']) ->
+      if is_bit_vector t then not (const_nexp (normalize_nexp m))
+      else contains_t_pp_var t'
+  | Tapp (c,targs) -> List.exists contains_t_arg_pp_var targs
+  | Tabbrev (_,t') -> contains_t_pp_var t'
+  | Toptions (t1,t2o) ->
+      contains_t_pp_var t1 ||
+      (match t2o with Some t2 -> contains_t_pp_var t2 | _ -> false)
+  | Tuvar _ -> true
+  | Tid _ -> false
+and contains_t_arg_pp_var targ = match targ with
+  | TA_typ t -> contains_t_pp_var t
+  | TA_nexp nexp -> not (const_nexp (normalize_nexp nexp))
+  | _ -> false
+
 let prefix_recordtype = true
 let report = Reporting_basic.err_unreachable
 let doc_exp_lem, doc_let_lem =
@@ -342,8 +402,15 @@ let doc_exp_lem, doc_let_lem =
         | _ ->
            (prefix 2 1) (string "write_reg") (doc_lexp_deref_lem regtypes le ^/^ expY e))
     | E_vector_append(l,r) ->
+       let (Base((_,t),_,_,_,_,_)) = annot in
+       let (call,ta,aexp_needed) =
+         if is_bit_vector t then
+           if not (contains_t_pp_var t)
+           then ("bitvector_concat", doc_tannot_lem regtypes false t, true)
+           else ("bitvector_concat", empty, aexp_needed)
+         else ("vector_concat",empty,aexp_needed) in
        let epp =
-         align (group (separate space [expY l;string "^^"] ^/^ expY r)) in
+         align (group (separate space [string call;expY l;expY r])) ^^ ta in
        if aexp_needed then parens epp else epp
     | E_cons(l,r) -> doc_op (group (colon^^colon)) (expY l) (expY r)
     | E_if(c,t,e) ->
@@ -388,7 +455,15 @@ let doc_exp_lem, doc_let_lem =
           if aexp_needed then parens (align epp) else epp
        | Id_aux (Id "slice_raw",_) ->
           let [e1;e2;e3] = args in
-          let epp = separate space [string "slice_raw";expY e1;expY e2;expY e3] in
+          let (E_aux (_,(_,Base((_,t1),_,_,_,_,_)))) = e1 in
+          let call = if is_bit_vector t1 then "bvslice_raw" else "slice_raw" in
+          let epp = separate space [string call;expY e1;expY e2;expY e3] in
+          if aexp_needed then parens (align epp) else epp
+       | Id_aux (Id "length",_) ->
+          let [arg] = args in
+          let (E_aux (_,(_,Base((_,targ),_,_,_,_,_)))) = arg in
+          let call = if is_bit_vector targ then "bvlength" else "length" in
+          let epp = separate space [string call;expY arg] in
           if aexp_needed then parens (align epp) else epp
        | _ ->
           begin match annot with
@@ -398,10 +473,13 @@ let doc_exp_lem, doc_let_lem =
              if aexp_needed then parens (align epp) else epp
           | Base (_,Constructor _,_,_,_,_) ->
              let argpp a_needed arg =
-               let (E_aux (_,(_,Base((_,{t=t}),_,_,_,_,_)))) = arg in
-               match t with
-               | Tapp("vector",_) ->
-                  let epp = concat [string "reset_vector_start";space;expY arg] in
+               let (E_aux (_,(_,Base((_,t),_,_,_,_,_)))) = arg in
+               match t.t with
+               | Tapp("vector",[_;_;_;_]) ->
+                  let call =
+                    if is_bit_vector t then "reset_bitvector_start"
+                    else "reset_vector_start" in
+                  let epp = concat [string call;space;expY arg] in
                   if a_needed then parens epp else epp
                | _ -> expV a_needed arg in
              let epp =
@@ -417,17 +495,25 @@ let doc_exp_lem, doc_let_lem =
                | Base(_,External (Some n),_,_,_,_) -> string n
                | _ -> doc_id_lem f in
              let argpp a_needed arg =
-               let (E_aux (_,(_,Base((_,{t=t}),_,_,_,_,_)))) = arg in
-               match t with
-               | Tapp("vector",_) ->
-                  let epp = concat [string "reset_vector_start";space;expY arg] in
+               let (E_aux (_,(_,Base((_,t),_,_,_,_,_)))) = arg in
+               match t.t with
+               | Tapp("vector",[_;_;_;_]) ->
+                  let call =
+                    if is_bit_vector t then "reset_bitvector_start"
+                    else "reset_vector_start" in
+                  let epp = concat [string call;space;expY arg] in
                   if a_needed then parens epp else epp
                | _ -> expV a_needed arg in
              let argspp = match args with
                | [arg] -> argpp true arg
                | args -> parens (align (separate_map (comma ^^ break 0) (argpp false) args)) in
              let epp = align (call ^//^ argspp) in
-             if aexp_needed then parens (align epp) else epp
+             let (taepp,aexp_needed) =
+               let (Base ((_,t),_,_,eff,_,_)) = annot in
+               if contains_bitvector_type t && not (contains_t_pp_var t)
+               then (align epp ^^ (doc_tannot_lem regtypes (effectful_t eff) t), true)
+               else (epp, aexp_needed) in
+             if aexp_needed then parens (align taepp) else taepp
           end
        end
     | E_vector_access (v,e) ->
@@ -436,27 +522,40 @@ let doc_exp_lem, doc_let_lem =
          if has_rreg_effect eff then
            separate space [string "read_reg_bit";expY v;expY e]
          else
-           separate space [string "access";expY v;expY e] in
+           let (E_aux (_,(_,Base ((_,tv),_,_,_,_,_)))) = v in
+           let call = if is_bit_vector tv then "bvaccess" else "access" in
+           separate space [string call;expY v;expY e] in
        if aexp_needed then parens (align epp) else epp
     | E_vector_subrange (v,e1,e2) ->
-       let (Base (_,_,_,_,eff,_)) = annot in
-       let epp =
+       let (Base ((_,t),_,_,_,eff,_)) = annot in
+       let (epp,aexp_needed) =
          if has_rreg_effect eff then
-           align (string "read_reg_range" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2)
+           let epp = align (string "read_reg_range" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2) in
+           if contains_bitvector_type t && not (contains_t_pp_var t)
+           then (epp ^^ doc_tannot_lem regtypes true t, true)
+           else (epp, aexp_needed)
          else
-           align (string "slice" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2) in
+           if is_bit_vector t then
+             let bepp = string "bvslice" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2 in
+             if not (contains_t_pp_var t)
+             then (bepp ^^ doc_tannot_lem regtypes false t, true)
+             else (bepp, aexp_needed)
+           else (string "slice" ^^ space ^^ expY v ^//^ expY e1 ^//^ expY e2, aexp_needed) in
        if aexp_needed then parens (align epp) else epp
     | E_field((E_aux(_,(l,fannot)) as fexp),id) ->
-       let (Base ((_,{t = t}),_,_,_,_,_)) = fannot in
-       (match t with
+       let (Base ((_,{t = ft}),_,_,_,_,_)) = fannot in
+       (match ft with
         | Tabbrev({t = Tid regtyp},{t=Tapp("register",_)}) ->
-           let field_f = match annot with
-             | Base((_,{t = Tid "bit"}),_,_,_,_,_)
-               | Base((_,{t = Tabbrev(_,{t=Tid "bit"})}),_,_,_,_,_) ->
-                string "read_reg_bitfield"
+           let (Base((_,t),_,_,_,_,_)) = annot in
+           let field_f = match t.t with
+             | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) -> string "read_reg_bitfield"
              | _ -> string "read_reg_field" in
+           let (ta,aexp_needed) =
+             if contains_bitvector_type t && not (contains_t_pp_var t)
+             then (doc_tannot_lem regtypes true t, true)
+             else (empty, aexp_needed) in
            let epp = field_f ^^ space ^^ (expY fexp) ^^ space ^^ string_lit (doc_id_lem id) in
-           if aexp_needed then parens (align epp) else epp
+           if aexp_needed then parens (align epp ^^ ta) else (epp ^^ ta)
         | Tid recordtyp
           | Tabbrev ({t = Tid recordtyp},_) ->
            let fname =
@@ -470,57 +569,73 @@ let doc_exp_lem, doc_let_lem =
     | E_block exps -> raise (report l "Blocks should have been removed till now.")
     | E_nondet exps -> raise (report l "Nondet blocks not supported.")
     | E_id id ->
+       let (Base((_,t),_,_,_,_,_)) = annot in
        (match annot with
         | Base((_, ({t = Tapp("register",_)} | {t=Tabbrev(_,{t=Tapp("register",_)})})),
                External _,_,eff,_,_) ->
            if has_rreg_effect eff then
-             separate space [string "read_reg";doc_id_lem id]
+             let epp = separate space [string "read_reg";doc_id_lem id] in
+             if contains_bitvector_type t && not (contains_t_pp_var t)
+             then parens (epp ^^ doc_tannot_lem regtypes true t)
+             else epp
            else
              doc_id_lem id
         | Base(_,(Constructor i |Enum i),_,_,_,_) -> doc_id_lem_ctor id
         | Base((_,t),Alias alias_info,_,eff,_,_) ->
            (match alias_info with
             | Alias_field(reg,field) ->
-               let epp = match t.t with
-                 | Tid "bit" | Tabbrev (_,{t=Tid "bit"}) ->
-                    (separate space)
-                      [string "read_reg_bitfield"; string reg;string_lit(string field)]
-                 | _ ->
-                    (separate space)
-                      [string "read_reg_field"; string reg; string_lit(string field)] in
-               if aexp_needed then parens (align epp) else epp
+                let call = match t.t with
+                  | Tid "bit" | Tabbrev (_,{t=Tid "bit"}) -> "read_reg_bitfield"
+                  | _ -> "read_reg_field" in
+                let ta =
+                  if contains_bitvector_type t && not (contains_t_pp_var t)
+                  then doc_tannot_lem regtypes true t else empty in
+                let epp = separate space [string call;string reg;string_lit(string field)] ^^ ta in
+                if aexp_needed then parens (align epp) else epp
             | Alias_pair(reg1,reg2) ->
-               let epp =
-                 if has_rreg_effect eff then
-                   separate space [string "read_two_regs";string reg1;string reg2]
-                 else
-                   separate space [string "RegisterPair";string reg1;string reg2] in
-               if aexp_needed then parens (align epp) else epp
+                let (call,ta) =
+                  if has_rreg_effect eff then
+                    let ta =
+                      if contains_bitvector_type t && not (contains_t_pp_var t)
+                      then doc_tannot_lem regtypes true t else empty in
+                    ("read_two_regs", ta)
+                  else
+                    ("RegisterPair", empty) in
+                let epp = separate space [string call;string reg1;string reg2] ^^ ta in
+                if aexp_needed then parens (align epp) else epp
             | Alias_extract(reg,start,stop) ->
-               let epp =
-                 if start = stop then
-                   (separate space)
-                     [string "access";doc_int start;
-                      parens (string "read_reg" ^^ space ^^ string reg)]
-                 else
-                   (separate space)
-                     [string "slice"; doc_int start; doc_int stop;
-                      parens (string "read_reg" ^^ space ^^ string reg)] in
-               if aexp_needed then parens (align epp) else epp
+                let epp =
+                  if start = stop then
+                    separate space [string "read_reg_bit";string reg;doc_int start]
+                  else
+                    let ta =
+                      if contains_bitvector_type t && not (contains_t_pp_var t)
+                      then doc_tannot_lem regtypes true t else empty in
+                    separate space [string "read_reg_range";string reg;doc_int start;doc_int stop] ^^ ta in
+                if aexp_needed then parens (align epp) else epp
            )
         | _ -> doc_id_lem id)
     | E_lit lit -> doc_lit_lem false lit annot
     | E_cast(Typ_aux (typ,_),e) ->
        (match annot with
-        | Base(_,External _,_,_,_,_) -> string "read_reg" ^^ space ^^ expY e
-        | _ ->
+        | Base((_,t),External _,_,_,_,_) ->
+           let epp = string "read_reg" ^^ space ^^ expY e in
+           if contains_bitvector_type t && not (contains_t_pp_var t)
+           then parens (epp ^^ doc_tannot_lem regtypes true t) else epp
+        | Base((_,t),_,_,_,_,_) ->
            (match typ with
             | Typ_app (Id_aux (Id "vector",_), [Typ_arg_aux (Typ_arg_nexp(Nexp_aux (Nexp_constant i,_)),_);_;_;_]) ->
-               let epp = (concat [string "set_vector_start";space;string (string_of_int i)]) ^//^
+               let call =
+                 if is_bit_vector t then "set_bitvector_start"
+                 else "set_vector_start" in
+               let epp = (concat [string call;space;string (string_of_int i)]) ^//^
                            expY e in
                if aexp_needed then parens epp else epp
             | Typ_var (Kid_aux (Var "length",_)) ->
-               let epp = (string "set_vector_start_to_length") ^//^ expY e in
+               let call =
+                 if is_bit_vector t then "set_bitvector_start_to_length"
+                 else "set_vector_start_to_length" in
+               let epp = (string call) ^//^ expY e in
                if aexp_needed then parens epp else epp
             | _ -> 
                expV aexp_needed e)) (*(parens (doc_op colon (group (expY e)) (doc_typ_lem typ)))) *)
@@ -549,8 +664,8 @@ let doc_exp_lem, doc_let_lem =
        (match annot with
         | Base((_,t),_,_,_,_,_) ->
            match t.t with
-           | Tapp("vector", [TA_nexp start; _; TA_ord order; _])
-             | Tabbrev(_,{t= Tapp("vector", [TA_nexp start; _; TA_ord order; _])}) ->
+           | Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; TA_typ etyp])
+             | Tabbrev(_,{t= Tapp("vector", [TA_nexp start; TA_nexp len; TA_ord order; TA_typ etyp])}) ->
               let dir,dir_out = match order.order with
                 | Oinc -> true,"true"
                 | _ -> false, "false" in
@@ -572,6 +687,13 @@ let doc_exp_lem, doc_let_lem =
                    align (group expspp) in
               let epp =
                 group (separate space [string "Vector"; brackets expspp;string start;string dir_out]) in
+              let (epp,aexp_needed) =
+                if etyp.t = Tid "bit" then
+                  let bepp = string "vec_to_bvec" ^^ space ^^ parens (align epp) in
+                  if contains_t_pp_var t
+                  then (bepp, aexp_needed)
+                  else (bepp ^^ doc_tannot_lem regtypes false t, true)
+                else (epp,aexp_needed) in
               if aexp_needed then parens (align epp) else epp
        )
     | E_vector_indexed (iexps, (Def_val_aux (default,(dl,dannot)))) ->
@@ -627,12 +749,20 @@ let doc_exp_lem, doc_let_lem =
        let epp =
          align (group (call ^//^ brackets expspp ^/^
                          separate space [default_string;string start;string size;string dir_out])) in
-       if aexp_needed then parens (align epp) else epp
+       let (bepp, aexp_needed) =
+         if is_bit_vector t
+         then (string "vec_to_bvec" ^^ space ^^ parens (epp) ^^ doc_tannot_lem regtypes false t, true)
+         else (epp, aexp_needed) in
+       if aexp_needed then parens (align bepp) else bepp
     | E_vector_update(v,e1,e2) ->
-       let epp = separate space [string "update_pos";expY v;expY e1;expY e2] in
+       let (Base((_,t),_,_,_,_,_)) = annot in
+       let call = if is_bit_vector t then "bvupdate_pos" else "update_pos" in
+       let epp = separate space [string call;expY v;expY e1;expY e2] in
        if aexp_needed then parens (align epp) else epp
     | E_vector_update_subrange(v,e1,e2,e3) ->
-       let epp = align (string "update" ^//^
+       let (Base((_,t),_,_,_,_,_)) = annot in
+       let call = if is_bit_vector t then "bvupdate" else "update" in
+       let epp = align (string call ^//^
                           group (group (expY v) ^/^ group (expY e1) ^/^ group (expY e2)) ^/^
                             group (expY e3)) in
        if aexp_needed then parens (align epp) else epp
@@ -670,9 +800,13 @@ let doc_exp_lem, doc_let_lem =
        (match annot with
         | Base((_,t),External(Some name),_,_,_,_) ->
            let argpp arg =
-             let (E_aux (_,(_,Base((_,{t=t}),_,_,_,_,_)))) = arg in
-             match t with
-             | Tapp("vector",_) -> parens (concat [string "reset_vector_start";space;expY arg])
+             let (E_aux (_,(_,Base((_,t),_,_,_,_,_)))) = arg in
+             match t.t with
+             | Tapp("vector",_) ->
+                 let call =
+                   if is_bit_vector t then "reset_bitvector_start"
+                   else "reset_vector_start" in
+                 parens (concat [string call;space;expY arg])
              | _ -> expY arg in
            let epp =
              let aux name = align (argpp e1 ^^ space ^^ string name ^//^ argpp e2) in
@@ -740,6 +874,10 @@ let doc_exp_lem, doc_let_lem =
 
                 | _ ->
                    string name ^//^ parens (expN e1 ^^ comma ^/^ expN e2)) in
+           let (epp,aexp_needed) =
+             if contains_bitvector_type t && not (contains_t_pp_var t)
+             then (parens epp ^^ doc_tannot_lem regtypes false t, true)
+             else (epp, aexp_needed) in
            if aexp_needed then parens (align epp) else epp
         | _ ->
            let epp =
diff --git a/src/pretty_print_ocaml.ml b/src/pretty_print_ocaml.ml
index 3772f549..adca6b12 100644
--- a/src/pretty_print_ocaml.ml
+++ b/src/pretty_print_ocaml.ml
@@ -338,10 +338,7 @@ let doc_exp_ocaml, doc_let_ocaml =
             | Typ_var (Kid_aux (Var "length",_)) ->
                parens ((string "set_start_to_length") ^//^ exp e)
             | _ -> 
-               parens (doc_op colon (group (exp e)) (doc_typ_ocaml typ)))
-
-
-)
+               parens (doc_op colon (group (exp e)) (doc_typ_ocaml typ))))
     | E_tuple exps ->
       parens (separate_map comma exp exps)
     | E_record(FES_aux(FES_Fexps(fexps,_),_)) ->
@@ -753,4 +750,3 @@ let pp_defs_ocaml f d top_line opens =
   print f (string "(*" ^^ (string top_line) ^^ string "*)" ^/^
            (separate_map hardline (fun lib -> (string "open") ^^ space ^^ (string lib)) opens) ^/^
            (doc_defs_ocaml d))
-
diff --git a/src/type_internal.ml b/src/type_internal.ml
index 2932cf33..3df352ae 100644
--- a/src/type_internal.ml
+++ b/src/type_internal.ml
@@ -560,15 +560,6 @@ let rec pow_i i n =
   | n -> mult_int_big_int i (pow_i i (n-1))
 let two_pow = pow_i 2
 
-let is_bit_vector t = match t.t with
-  | Tapp("vector", [_;_;_; TA_typ t])
-  | Tabbrev(_,{t=Tapp("vector",[_;_;_; TA_typ t])})
-  | Tapp("reg", [TA_typ {t=Tapp("vector",[_;_;_; TA_typ t])}])->
-    (match t.t with
-     | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) | Tapp("reg",[TA_typ {t=Tid "bit"}]) -> true
-     | _ -> false)
-  | _ -> false
-
 (* predicate to determine if pushing a constant in for addition or multiplication could change the form *)
 let rec contains_const n =
   match n.nexp with
@@ -929,8 +920,37 @@ let rec normalize_n_rec recur_ok n =
     
 let normalize_nexp = normalize_n_rec true
 
+let rec normalize_t t = match t.t with
+  | Tfn (t1,t2,i,eff) -> {t = Tfn (normalize_t t1,normalize_t t2,i,eff)}
+  | Ttup ts -> {t = Ttup (List.map normalize_t ts)}
+  | Tapp (c,args) -> {t = Tapp (c, List.map normalize_t_arg args)}
+  | Tabbrev (_,t') -> t'
+  | _ -> t
+and normalize_t_arg targ = match targ with
+  | TA_typ t -> TA_typ (normalize_t t)
+  | TA_nexp nexp -> TA_nexp (normalize_nexp nexp)
+  | _ -> targ
+
 let int_to_nexp = mk_c_int
 
+let rec is_bit_vector t = match t.t with
+  | Tapp("vector", [_;_;_; TA_typ t]) ->
+    (match t.t with
+     | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) | Tapp("register",[TA_typ {t=Tid "bit"}]) -> true
+     | _ -> false)
+  | Tapp("register", [TA_typ t']) -> is_bit_vector t'
+  | Tabbrev(_,t') -> is_bit_vector t'
+  | _ -> false
+
+let rec has_const_vector_length t = match t.t with
+  | Tapp("vector", [_;TA_nexp m;_;_]) ->
+    (match (normalize_nexp m).nexp with
+      | Nconst i -> Some i
+      | _ -> None)
+  | Tapp("register", [TA_typ t']) -> has_const_vector_length t'
+  | Tabbrev(_,t') -> has_const_vector_length t'
+  | _ -> None
+
 let v_count = ref 0
 let t_count = ref 0
 let tuvars = ref []
diff --git a/src/type_internal.mli b/src/type_internal.mli
index ee2e3988..f4924a63 100644
--- a/src/type_internal.mli
+++ b/src/type_internal.mli
@@ -313,6 +313,7 @@ val get_abbrev : def_envs -> t -> (t * nexp_range list)
 
 val is_enum_typ : def_envs -> t -> int option
 val is_bit_vector : t -> bool
+val has_const_vector_length : t -> big_int option
 
 val extract_bounds : def_envs -> string -> t -> bounds_env
 val merge_bounds : bounds_env -> bounds_env -> bounds_env
@@ -324,6 +325,7 @@ val merge_option_maps : nexp_map option -> nexp_map option -> nexp_map option
 
 val expand_nexp : nexp -> nexp list
 val normalize_nexp : nexp -> nexp
+val normalize_t : t -> t
 val get_index : nexp -> int (*expose nindex through this for debugging purposes*)
 val get_all_nvar : nexp -> string list (*Pull out all of the contained nvar and nuvars in nexp*)
 
@@ -387,4 +389,3 @@ val tannot_merge : constraint_origin -> def_envs -> bool -> tannot -> tannot ->
 val initial_typ_env : tannot Envmap.t
 
 val initial_typ_env_list : (string * ((string * tannot) list)) list 
-