Checkpoint work-in-progress mips sequential interpreter using ocaml shallow embedding.

7 files changed, 887 insertions, 252 deletions

diff --git a/mips/mips_extras_ml.ml b/mips/mips_extras_ml.ml
new file mode 100644
index 00000000..1565c7c6
--- /dev/null
+++ b/mips/mips_extras_ml.ml
@@ -0,0 +1,53 @@
+open Sail_values
+open Big_int_Z
+open Printf
+
+let big_int_to_hex i = Uint64.to_string_hex (Uint64.of_string (string_of_big_int i))
+
+module Mem = struct
+  include Map.Make(struct
+      type t = big_int
+      let compare = compare_big_int
+    end)
+end
+
+let mips_mem = (ref Mem.empty : (int Mem.t) ref);;
+
+let _MEMea (addr, size) = ()
+let _MEMea_conditional = _MEMea
+
+let _MEMval (addr, size, data) =
+  (* assumes data is decreasing vector to be stored in big-endian byte order in mem *)
+  let s = int_of_big_int size in
+  let a = unsigned_big(addr) in
+  for i = 0 to (s - 1) do
+    let bit_idx = i * 8 in
+    let byte = unsigned_int(slice_raw (data, big_int_of_int bit_idx, big_int_of_int (bit_idx + 7))) in
+    let byte_addr = add_int_big_int i a in
+    begin
+      (*printf "MEM [%s] <- %x\n" (big_int_to_hex byte_addr) byte;*)
+      mips_mem := Mem.add byte_addr byte !mips_mem;
+    end
+  done
+  
+let _MEMval_conditional (addr, size, data) =
+    let _ = _MEMval (addr, size, data) in
+    Vone
+
+let _MEMr (addr, size) = begin
+  let s = int_of_big_int size in
+  let a = unsigned_big(addr) in
+  let ret = ref (to_vec_dec_int (0, 0)) in
+  for i = 0 to (s - 1) do
+    let byte_addr = add_int_big_int i a in
+    let byte = Mem.find byte_addr !mips_mem in
+    let byte_vec = to_vec_dec_int (8, byte) in
+    ret := vector_concat (!ret) byte_vec;
+    (*printf "MEM [%s] -> %x %s %s\n" (big_int_to_hex byte_addr) byte (string_of_value byte_vec) (string_of_value !ret);*)
+  done;
+  ret := set_start_to_length (!ret);
+  !ret;
+end
+let _MEMr_reserve = _MEMr
+
+let _MEM_sync _ = ()
diff --git a/mips/mips_prelude.sail b/mips/mips_prelude.sail
index d2a0fc6f..3643d211 100644
--- a/mips/mips_prelude.sail
+++ b/mips/mips_prelude.sail
@@ -475,7 +475,7 @@ function AccessLevel getAccessLevel() =
 function unit checkCP0Access () =
   {
     let accessLevel = getAccessLevel() in
-    if ((accessLevel != Kernel) & (~((CP0Status.CU)[28]))) then
+    if ((accessLevel != Kernel) & (~(CP0Status[28] (*CU0*)))) then
       {
         (CP0Cause.CE) := 0b00;
         SignalException(CpU);
diff --git a/mips/run_embed.ml b/mips/run_embed.ml
new file mode 100644
index 00000000..b65f74d9
--- /dev/null
+++ b/mips/run_embed.ml
@@ -0,0 +1,437 @@
+(**************************************************************************)
+(*     Sail                                                               *)
+(*                                                                        *)
+(*  Copyright (c) 2013-2017                                               *)
+(*    Kathyrn Gray                                                        *)
+(*    Shaked Flur                                                         *)
+(*    Stephen Kell                                                        *)
+(*    Gabriel Kerneis                                                     *)
+(*    Robert Norton-Wright                                                *)
+(*    Christopher Pulte                                                   *)
+(*    Peter Sewell                                                        *)
+(*                                                                        *)
+(*  All rights reserved.                                                  *)
+(*                                                                        *)
+(*  This software was developed by the University of Cambridge Computer   *)
+(*  Laboratory as part of the Rigorous Engineering of Mainstream Systems  *)
+(*  (REMS) project, funded by EPSRC grant EP/K008528/1.                   *)
+(*                                                                        *)
+(*  Redistribution and use in source and binary forms, with or without    *)
+(*  modification, are permitted provided that the following conditions    *)
+(*  are met:                                                              *)
+(*  1. Redistributions of source code must retain the above copyright     *)
+(*     notice, this list of conditions and the following disclaimer.      *)
+(*  2. Redistributions in binary form must reproduce the above copyright  *)
+(*     notice, this list of conditions and the following disclaimer in    *)
+(*     the documentation and/or other materials provided with the         *)
+(*     distribution.                                                      *)
+(*                                                                        *)
+(*  THIS SOFTWARE IS PROVIDED BY THE AUTHOR AND CONTRIBUTORS ``AS IS''    *)
+(*  AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED     *)
+(*  TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A       *)
+(*  PARTICULAR PURPOSE ARE DISCLAIMED.  IN NO EVENT SHALL THE AUTHOR OR   *)
+(*  CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,          *)
+(*  SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT      *)
+(*  LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF      *)
+(*  USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND   *)
+(*  ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,    *)
+(*  OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT    *)
+(*  OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF    *)
+(*  SUCH DAMAGE.                                                          *)
+(**************************************************************************)
+
+open Printf ;;
+open Big_int_Z ;;
+open Sail_values;;
+open Mips_extras_ml;;
+(* The linksem ELF interface *)
+open Sail_interface ;;
+
+module Mips_model=Mips_notlb_embed;;
+
+let interact_print = ref true
+let result_print = ref true
+let error_print = ref true
+let interactf : ('a, out_channel, unit) format -> 'a =
+  function f -> if !interact_print then printf f else ifprintf stderr f
+let errorf : ('a, out_channel, unit) format -> 'a =
+  function f -> if !error_print then printf f else ifprintf stderr f
+let resultf : ('a, out_channel, unit) format -> 'a =
+  function f -> if !result_print then printf f else ifprintf stderr f
+
+let rec foldli f acc ?(i=0) = function
+  | [] -> acc
+  | x::xs -> foldli f (f i acc x) ~i:(i+1) xs;;
+
+let hex_to_big_int s = big_int_of_int64 (Int64.of_string s) ;;
+let big_int_to_hex i = Uint64.to_string_hex (Uint64.of_string (string_of_big_int i))
+let input_buf = (ref [] : int list ref);;
+
+let add_mem byte addr mem = begin
+  assert(byte >= 0 && byte < 256);
+  (*printf "MEM [%s] <- %x\n" (big_int_to_hex addr) byte;*)
+  mem := Mem.add addr byte !mem
+end
+(*  
+let rec load_memory_segment (segment: Elf_interpreted_segment.elf64_interpreted_segment) mem =
+  let (Byte_sequence.Sequence bytes) = segment.Elf_interpreted_segment.elf64_segment_body in
+  let addr = segment.Elf_interpreted_segment.elf64_segment_paddr in
+  load_memory_segment' bytes addr mem
+
+let rec load_memory_segments segments =
+  begin match segments with
+    | [] -> ()
+    | segment::segments' ->
+      let (x,w,r) = segment.Elf_interpreted_segment.elf64_segment_flags in
+      begin
+        load_memory_segment segment mips_mem;
+        load_memory_segments segments'
+      end    
+  end
+
+let initial_system_state_of_elf_file name = 
+
+  (* call ELF analyser on file *)
+  match Sail_interface.populate_and_obtain_global_symbol_init_info name with
+  | Error.Fail s -> failwith ("populate_and_obtain_global_symbol_init_info: " ^ s)
+  | Error.Success 
+      (_, (elf_epi: Sail_interface.executable_process_image),
+       (symbol_map: Elf_file.global_symbol_init_info))
+    ->
+    let (segments, e_entry, e_machine) =
+      begin match elf_epi with
+        | ELF_Class_32 _ -> failwith "cannot handle ELF_Class_32"
+        | ELF_Class_64 (segments,e_entry,e_machine) ->
+          (* remove all the auto generated segments (they contain only 0s) *)
+          let segments =
+            Lem_list.mapMaybe
+              (fun (seg, prov) -> if prov = Elf_file.FromELF then Some seg else None)
+              segments
+          in
+          (segments,e_entry,e_machine)
+      end
+    in
+    (* construct program memory and start address *)
+    begin
+      load_memory_segments segments;
+      (*
+      debugf "prog_mem\n";
+      Mem.iter (fun k v -> debugf "%s\n" (Mem.to_string k v)) !prog_mem;
+      debugf "data_mem\n";
+      Mem.iter (fun k v -> debugf "%s\n" (Mem.to_string k v)) !data_mem;
+      *)
+      let (isa_defs, isa_memory_access, isa_externs, isa_model, model_reg_d, startaddr,
+           initial_stack_data, initial_register_abi_data, register_data_all) =
+        match Nat_big_num.to_int e_machine with
+        | 8 (* EM_MIPS *) ->
+          let startaddr =
+            let e_entry = Uint64.of_string (Nat_big_num.to_string e_entry) in
+            match Abi_mips64.abi_mips64_compute_program_entry_point segments e_entry with
+            | Error.Fail s -> failwith "Failed computing entry point"
+            | Error.Success s -> s
+          in
+          let (initial_stack_data, initial_register_abi_data) =
+            initial_stack_and_reg_data_of_MIPS_elf_file e_entry !data_mem in
+          
+          (Mips.defs,
+           (Mips_extras.read_memory_functions,
+            Mips_extras.memory_writes,
+            Mips_extras.memory_eas,
+            Mips_extras.memory_vals,
+            Mips_extras.barrier_functions),
+           [],
+           MIPS,
+           D_decreasing,
+           startaddr,
+           initial_stack_data,
+           initial_register_abi_data,
+           mips_register_data_all)
+
+        | _ -> failwith (Printf.sprintf "Sail sequential interpreter can't handle the e_machine value %s, only EM_MIPS is supported." (Nat_big_num.to_string e_machine))
+      in
+      
+      (* pull the object symbols from the symbol table *)
+      let symbol_table : (string * Nat_big_num.num * int * word8 list (*their bytes*)) list =
+        let rec convert_symbol_table symbol_map =
+          begin match symbol_map with
+          | [] -> []
+          | ((name: string),
+             ((typ: Nat_big_num.num),
+              (size: Nat_big_num.num (*number of bytes*)),
+              (address: Nat_big_num.num),
+              (mb: Byte_sequence.byte_sequence option (*present iff type=stt_object*)),
+              (binding: Nat_big_num.num)))
+	    (*              (mb: Byte_sequence_wrapper.t option (*present iff type=stt_object*)) )) *)
+            ::symbol_map' ->
+            if Nat_big_num.equal typ Elf_symbol_table.stt_object && not (Nat_big_num.equal size (Nat_big_num.of_int 0))
+            then
+              (,
+                (* an object symbol - map *)
+                (*Printf.printf "*** size %d ***\n" (Nat_big_num.to_int size);*)
+                let bytes =
+                  (match mb with
+                   | None -> raise (Failure "this cannot happen")
+                   | Some (Sequence bytes) ->
+                     List.map (fun (c:char) -> Char.code c) bytes) in
+                 (name, address, List.length bytes, bytes):: convert_symbol_table symbol_map'
+              )
+              else
+                (* not an object symbol or of zero size - ignore *)
+                convert_symbol_table symbol_map'
+          end
+        in
+        (List.map (fun (n,a,bs) -> (n,a,List.length bs,bs)) initial_stack_data) @ convert_symbol_table symbol_map
+      in
+
+      (* invert the symbol table to use for pp *)
+      let symbol_table_pp : ((Sail_impl_base.address * int) * string) list =
+        (* map symbol to (bindings, footprint),
+           if a symbol appears more then onece keep the one with higher
+           precedence (stb_global > stb_weak > stb_local) *)
+        let map =
+          List.fold_left
+            (fun map (name, (typ, size, address, mb, binding)) ->
+               if String.length name <> 0 &&
+                  (if String.length name = 1 then Char.code (String.get name 0) <> 0 else true) &&
+                  not (Nat_big_num.equal address (Nat_big_num.of_int 0))
+               then
+                 try
+                   let (binding', _) = StringMap.find name map in
+                   if  Nat_big_num.equal binding' Elf_symbol_table.stb_local ||
+                       Nat_big_num.equal binding Elf_symbol_table.stb_global
+                   then
+                     StringMap.add name (binding,
+                                         (Sail_impl_base.address_of_integer address, Nat_big_num.to_int size)) map
+                   else map
+                 with Not_found ->
+                   StringMap.add name (binding,
+                                       (Sail_impl_base.address_of_integer address, Nat_big_num.to_int size)) map
+                     
+               else map
+            )
+            StringMap.empty
+            symbol_map
+        in
+
+        List.map (fun (name, (binding, fp)) -> (fp, name)) (StringMap.bindings map)
+      in
+
+
+      (* Now we examine the rest of the data memory,
+         removing the footprint of the symbols and chunking it into aligned chunks *)
+      
+      let rec remove_symbols_from_data_memory data_mem symbols =
+        match symbols with
+        | [] -> data_mem
+        | (name,address,size,bs)::symbols' ->
+          let data_mem' =
+            Mem.filter
+              (fun a v ->
+                 not (Nat_big_num.greater_equal a address &&
+                      Nat_big_num.less a (Nat_big_num.add (Nat_big_num.of_int (List.length bs)) address)))
+              data_mem in
+          remove_symbols_from_data_memory data_mem' symbols' in
+
+      let trimmed_data_memory : (Nat_big_num.num * memory_byte) list =
+        Mem.bindings (remove_symbols_from_data_memory !data_mem symbol_table) in
+
+      (* make sure that's ordered increasingly.... *)
+      let trimmed_data_memory =
+        List.sort (fun (a,b) (a',b') -> Nat_big_num.compare a a') trimmed_data_memory in
+
+      let aligned a n =  (* a mod n = 0 *)
+        let n_big = Nat_big_num.of_int n in
+        Nat_big_num.equal (Nat_big_num.modulus a n_big) ((Nat_big_num.of_int 0)) in
+
+      let isplus a' a n =   (* a' = a+n *)
+        Nat_big_num.equal a' (Nat_big_num.add (Nat_big_num.of_int n) a) in
+
+
+      let initial_register_state =
+        fun rbn ->
+          try
+            List.assoc rbn initial_register_abi_data
+          with
+            Not_found ->
+              (register_state_zero register_data_all) rbn
+      in
+
+      begin
+        (initial_reg_file register_data_all initial_register_state);
+        
+        (* construct initial system state *)
+        let initial_system_state =
+          (isa_defs,
+	   isa_memory_access,
+	   isa_externs,
+           isa_model,
+           model_reg_d,
+           startaddr,
+           (Sail_impl_base.address_of_integer startaddr))
+        in
+        
+        (initial_system_state, symbol_table_pp)
+      end
+    end
+ *)
+
+let max_cut_off = ref false
+let max_instr = ref 0
+let raw_file = ref ""
+let raw_at   = ref 0
+let elf_file = ref ""
+
+let args = [
+  ("--file", Arg.Set_string elf_file, "filename of elf binary to load in memory");
+  ("--max_instruction", Arg.Int (fun i -> max_cut_off := true; max_instr := i), "only run i instructions, then stop");
+  ("--raw", Arg.Set_string raw_file, "filename of raw file to load in memory");
+  ("--at", Arg.Set_int raw_at, "address to load raw file in memory");
+]
+
+let time_it action arg =
+  let start_time = Sys.time () in
+  let ret = action arg in
+  let finish_time = Sys.time () in
+  (finish_time -. start_time, ret)
+
+let rec debug_print_gprs start stop =
+  resultf "DEBUG MIPS REG %.2d %s\n" start (big_int_to_hex (unsigned_big(vector_access Mips_model._GPR (big_int_of_int start))));
+  if start < stop
+  then debug_print_gprs (start + 1) stop
+  else ()
+
+let get_opcode pc_a = _MEMr (to_vec_dec_big (big_int_of_int 64, pc_a), big_int_of_int 4)
+
+let rec fde_loop count =
+  if !max_cut_off && count = !max_instr
+  then begin
+      resultf "\nEnding evaluation due to reaching cut off point of %d instructions\n" count;
+      count
+    end
+  else begin
+    let pc_vaddr = unsigned_big(Mips_model._PC) in
+    interactf "\n**** instruction %d from address %s ****\n"
+      count (big_int_to_hex pc_vaddr);
+    let m_paddr = Some pc_vaddr in (* XXX should be address translate *)
+    match m_paddr with
+      | Some pc ->
+          let inBranchDelay = Some(unsigned_int(Mips_model._inBranchDelay)) in
+          (match inBranchDelay with
+          | Some 0 -> 
+            let npc_addr = add_int_big_int 4 pc_vaddr in
+            let npc_vec = to_vec_dec_big (big_int_of_int 64, npc_addr) in
+            set_register Mips_model._nextPC npc_vec;
+          | Some 1 ->
+            set_register Mips_model._nextPC Mips_model._delayedPC;
+          | _ -> failwith "invalid value of inBranchDelay");
+          let opcode = get_opcode pc in
+          let _ = resultf "decode: 0x%x\n" (unsigned_int(opcode)) in
+          let instruction = Mips_model._decode opcode in
+          let i = match instruction with
+            | Some (i) -> i
+            | _ ->  begin
+                errorf "\n**** Decode error ****\n"; 
+                exit 1;
+              end
+          in
+          if (i == Mips_model.HCF)
+          then 
+            begin
+              debug_print_gprs 0 31;
+              resultf "\nSUCCESS program terminated after %d instructions\n" count;
+              count
+            end 
+          else
+            begin
+              Mips_model._execute(i);
+
+                (*
+                (try
+                  let (pending, _, _)  = (Unix.select [(Unix.stdin)] [] [] 0.0) in
+                  (if (pending != []) then
+                    let char = (input_byte stdin) in (
+                    errorf "Input %x\n" char;
+                    input_buf := (!input_buf) @ [char]));
+                with
+                | _ -> ());
+
+                let uart_rvalid = option_int_of_reg "UART_RVALID" in
+                (match uart_rvalid with
+                | Some 0 ->
+                  (match !input_buf with
+                  | x :: xs -> (
+                      reg := Reg.add "UART_RDATA" (register_value_of_integer 8 7 Sail_impl_base.D_decreasing (Nat_big_num.of_int x)) !reg;
+                      reg := Reg.add "UART_RVALID" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing (Nat_big_num.of_int 1)) !reg;
+                      input_buf := xs;
+                    )
+                  | [] -> ())
+                | _-> ());
+
+                let uart_written = option_int_of_reg "UART_WRITTEN" in
+                (match uart_written with 
+                | Some 1 ->
+                  (let uart_data = option_int_of_reg "UART_WDATA" in
+                  match uart_data with
+                  | Some b -> (printf "%c" (Char.chr b); printf "%!")
+                  | None   -> (errorf "UART_WDATA was undef" ; exit 1))
+                | _      -> ());
+                reg := Reg.add "UART_WRITTEN" (register_value_of_integer 1 0 Sail_impl_base.D_decreasing Nat_big_num.zero) !reg;*)
+                set_register Mips_model._inBranchDelay Mips_model._branchPending;
+                set_register Mips_model._branchPending (to_vec_dec_int (1, 0));
+                set_register Mips_model._PC Mips_model._nextPC;
+                fde_loop (count + 1)
+            end
+      | None -> begin (* Exception during PC translation *)
+          set_register Mips_model._inBranchDelay Mips_model._branchPending;
+          set_register Mips_model._branchPending (to_vec_dec_int (1, 0));
+          set_register Mips_model._PC Mips_model._nextPC;
+          fde_loop (count + 1)
+        end
+  end
+
+let rec load_raw_file' mem addr chan =
+  let byte = input_byte chan in
+  (add_mem byte addr mem;
+  load_raw_file' mem (Big_int_Z.add_int_big_int 1 addr) chan)
+
+let rec load_raw_file mem addr chan =
+  try 
+    load_raw_file' mem addr chan
+   with
+  | End_of_file -> ()
+
+
+let run () =
+  Arg.parse args (fun _ -> raise (Arg.Bad "anonymous parameter")) "" ;
+  (*if !elf_file = "" then begin
+    Arg.usage args "";
+    exit 1;
+  end;*)
+(*
+  let ((isa_defs,
+       (isa_m0, isa_m1, isa_m2, isa_m3,isa_m4),
+        isa_externs,
+        isa_model,
+        model_reg_d,
+        startaddr,
+        startaddr_internal), pp_symbol_map) = initial_system_state_of_elf_file !file in
+ *)
+  if String.length(!raw_file) != 0 then
+    load_raw_file mips_mem (big_int_of_int !raw_at) (open_in_bin !raw_file);
+  set_register_field_bit Mips_model._CP0Status "BEV" Vone;
+  printf "CP0Status: %s\n" (string_of_value Mips_model._CP0Status);
+  let start_addr = (to_vec_dec_big (big_int_of_int 64, hex_to_big_int "0x40000000")) in
+  set_register Mips_model._PC start_addr;
+  let name = Filename.basename !raw_file in
+  let (t, count) = time_it fde_loop 0 in
+  resultf "Execution time for file %s: %f seconds %f IPS \n" name t (float(count) /. t);;
+
+(* Turn off line-buffering of standard input to allow responsive console input 
+if Unix.isatty (Unix.stdin) then begin
+  let tattrs = Unix.tcgetattr (Unix.stdin) in
+  Unix.tcsetattr (Unix.stdin) (Unix.TCSANOW) ({tattrs with c_icanon=false})
+end ;;
+*)
+
+run () ;;
+
diff --git a/src/Makefile b/src/Makefile
index 9b8b727d..acdd0075 100644
--- a/src/Makefile
+++ b/src/Makefile
@@ -82,6 +82,7 @@ MIPS_NOTLB_SAILS:=$(MIPS_NOTLB_SAILS_PRE) $(BITBUCKET_ROOT)/sail/etc/regfp.sail
 CHERI_SAIL_DIR:=$(BITBUCKET_ROOT)/sail/cheri
 
 CHERI_NOTLB_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb_stub.sail $(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_256.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
+
 CHERI_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_types.sail $(CHERI_SAIL_DIR)/cheri_prelude_256.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
 
 CHERI128_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sail $(CHERI_SAIL_DIR)/cheri_types.sail  $(CHERI_SAIL_DIR)/cheri_prelude_128.sail $(CHERI_SAIL_DIR)/cheri_prelude_common.sail $(MIPS_SAIL_DIR)/mips_insts.sail $(CHERI_SAIL_DIR)/cheri_insts.sail $(MIPS_SAIL_DIR)/mips_ri.sail $(MIPS_SAIL_DIR)/mips_epilogue.sail
@@ -89,20 +90,28 @@ CHERI128_SAILS:=$(MIPS_SAIL_DIR)/mips_prelude.sail $(MIPS_SAIL_DIR)/mips_tlb.sai
 elf:
 	make -C $(ELFDIR)
 
+CP_TO_BUILD=mkdir -p _build; cp $< $@
+
 _build/mips_extras.lem: ../mips/mips_extras.lem
-	mkdir -p _build
-	cp $< $@
+	$(CP_TO_BUILD)
+
+_build/mips_extras_ml.ml: ../mips/mips_extras_ml.ml
+	$(CP_TO_BUILD)
+
+_build/sail_values.ml: gen_lib/sail_values.ml
+	$(CP_TO_BUILD)
 
 _build/run_with_elf.ml: lem_interp/run_with_elf.ml
-	mkdir -p _build
-	cp $< $@
+	$(CP_TO_BUILD)
+
 _build/run_with_elf_cheri.ml: lem_interp/run_with_elf_cheri.ml
-	mkdir -p _build
-	cp $< $@
+	$(CP_TO_BUILD)
 
 _build/run_with_elf_cheri128.ml: lem_interp/run_with_elf_cheri128.ml
-	mkdir -p _build
-	cp $< $@
+	$(CP_TO_BUILD)
+
+_build/run_embed.ml: ../mips/run_embed.ml
+	$(CP_TO_BUILD)
 
 _build/mips.lem: $(MIPS_SAILS) ./sail.native
 	mkdir -p _build
@@ -119,6 +128,11 @@ _build/mips_notlb.lem: $(MIPS_NOTLB_SAILS) ./sail.native
 	cd _build ; \
 	../sail.native -lem_ast -o mips_notlb $(MIPS_NOTLB_SAILS)
 
+_build/mips_notlb_embed.ml: $(MIPS_NOTLB_SAILS_PRE) ./sail.native
+	mkdir -p _build
+	cd _build ; \
+	../sail.native -ocaml -lem -lem_ast -ocaml_lib Mips_extras_ml -o mips_notlb_embed $(MIPS_NOTLB_SAILS_PRE)
+
 _build/cheri.lem: $(CHERI_SAILS) ./sail.native
 	mkdir -p _build
 	cd _build ;\
@@ -161,6 +175,12 @@ count: _build/cheri_trimmed.sail _build/mips_trimmed.sail
 run_mips.native: _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml interpreter
 	env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(LEMLIBOCAML)/dependencies/zarith -I _build/lem_interp/ -I $(ELFDIR)/src  -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(LEMLIBOCAML)/dependencies/zarith/zarith.cmxa $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa  _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/mips.ml _build/mips_extras.ml _build/run_with_elf.ml  -o run_mips.native
 
+run_mips_embed.native: _build/mips_notlb_embed.ml _build/mips_extras_ml.ml _build/sail_values.ml _build/run_embed.ml
+	env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(LEMLIBOCAML)/dependencies/zarith -I _build/lem_interp/ -I $(ELFDIR)/src  -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(LEMLIBOCAML)/dependencies/zarith/zarith.cmxa $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa  _build/pprint/src/PPrintLib.cmxa _build/sail_values.ml _build/mips_extras_ml.ml _build/mips_notlb_embed.ml _build/run_embed.ml -o run_mips_embed.native
+
+run_mips_embed.bytes: _build/mips_notlb_embed.ml _build/mips_extras_ml.ml _build/sail_values.ml _build/run_embed.ml
+	env OCAMLRUNPARAM=l=100M ocamlfind ocamlc -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(LEMLIBOCAML)/dependencies/zarith -I _build/lem_interp/ -I $(ELFDIR)/src  -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(LEMLIBOCAML)/dependencies/zarith/zarith.cma $(LEMLIBOCAML)/extract.cma $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cma $(ELFDIR)/src/linksem.cma  _build/sail_values.ml _build/mips_extras_ml.ml _build/mips_notlb_embed.ml _build/run_embed.ml -o run_mips_embed.bytes
+
 run_cheri.native:  _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml interpreter
 	env OCAMLRUNPARAM=l=100M ocamlfind ocamlopt -g -package num -package str -package unix -I $(ELFDIR)/contrib/ocaml-uint/_build/lib -I $(LEMLIBOCAML) -I $(LEMLIBOCAML)/dependencies/zarith -I _build/lem_interp/ -I $(ELFDIR)/src  -I $(ELFDIR)/src/adaptors -I $(ELFDIR)/src/abis/mips64 -I _build -linkpkg $(LEMLIBOCAML)/dependencies/zarith/zarith.cmxa $(LEMLIBOCAML)/extract.cmxa $(ELFDIR)/contrib/ocaml-uint/_build/lib/uint.cmxa $(ELFDIR)/src/linksem.cmxa  _build/pprint/src/PPrintLib.cmxa _build/lem_interp/extract.cmxa _build/cheri.ml _build/mips_extras.ml _build/run_with_elf_cheri.ml  -o run_cheri.native
 
diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml
index 0072d5b6..d6443a16 100644
--- a/src/gen_lib/sail_values.ml
+++ b/src/gen_lib/sail_values.ml
@@ -4,18 +4,34 @@ open Big_int_Z
 type vbit = Vone | Vzero | Vundef
 type number = Big_int_Z.big_int
 type _bool = vbit
+type _string = string
+type _nat = number
+
 type value =
   | Vvector of vbit array * int * bool
   | VvectorR of value array * int * bool
   | Vregister of vbit array ref * int * bool * (string * (int * int)) list
   | Vbit of vbit (*Mostly for Vundef in place of undefined register place holders*)
 
+let string_of_bit = function 
+  | Vone   -> "1"
+  | Vzero  -> "0"
+  | Vundef -> "u"
+
+let string_of_bit_array a = Array.fold_left (^) "" (Array.map string_of_bit a) 
+
+let string_of_value = function
+  | Vvector(bits, start, inc)  -> (string_of_int start) ^ (if inc then "inc" else "dec") ^ (string_of_bit_array bits)
+  | VvectorR(values, start, inc) -> ""
+  | Vregister(bits, start, inc, fields) -> (string_of_int start) ^ (if inc then "inc" else "dec") ^ (string_of_bit_array !bits)
+  | Vbit(b) -> string_of_bit b
+
 let to_bool = function
   | Vzero -> false
   | Vone  -> true
   | Vundef -> assert false
 
-let is_one_big i =
+let is_one i =
   if eq_big_int i unit_big_int
   then Vone
   else Vzero
@@ -24,7 +40,7 @@ let is_one_big i =
 let exit _ = failwith "called exit"
 
 
-let is_one i =
+let is_one_int i =
   if i = 1 then Vone else Vzero
 
 let get_barray  = function
@@ -56,7 +72,7 @@ let length = function
   | VvectorR(array,_,_) -> Array.length array
   | _ -> assert false
   
-let set_start_to_length v = set_start (length v) v
+let set_start_to_length v = set_start ((length v)-1) v (* XXX should take account of direction? *)
 
 let length_big v = big_int_of_int (length v)
 
@@ -64,16 +80,19 @@ let read_register = function
   | Vregister(a,start,inc,_) -> Vvector(!a,start,inc)
   | v -> v
 
-let vector_access v n = match v with
+let vector_access_int v n = 
+  match v with
   | VvectorR(array,start,is_inc) ->
     if is_inc
     then (array.(n-start))
     else (array.(start-n))
   | _ -> assert false
 
-let vector_access_big v n = vector_access v (int_of_big_int n)
-      
-let bit_vector_access v n = match v with
+let vector_access_big v n = vector_access_int v (int_of_big_int n)
+
+let vector_access = vector_access_big
+
+let bit_vector_access_int v n = match v with
   | Vvector(array,start,is_inc) ->
     if is_inc
     then array.(n-start)
@@ -84,9 +103,10 @@ let bit_vector_access v n = match v with
     else !array.(start-n)
   | _ -> assert false
 
-let bit_vector_access_big v n = bit_vector_access v (int_of_big_int n)
+let bit_vector_access_big v n = bit_vector_access_int v (int_of_big_int n)
+let bit_vector_access = bit_vector_access_big
 
-let vector_subrange v n m =
+let vector_subrange_int v n m =
   let builder array length offset default =
     let new_array = Array.make length default in
     begin
@@ -108,7 +128,8 @@ let vector_subrange v n m =
     Vvector(builder !array length offset Vzero,n,is_inc)
   | _ -> v
 
-let vector_subrange_big v n m = vector_subrange v (int_of_big_int n) (int_of_big_int m)
+let vector_subrange_big v n m = vector_subrange_int v (int_of_big_int n) (int_of_big_int m)
+let vector_subrange = vector_subrange_big
 
 let get_register_field_vec reg field =
   match reg with
@@ -117,7 +138,7 @@ let get_register_field_vec reg field =
      | (i,j) ->
        if i = j
        then Vbit Vundef
-       else vector_subrange reg i j)
+       else vector_subrange_int reg i j)
   | _ -> Vbit Vundef
 
 let get_register_field_bit reg field =
@@ -126,7 +147,7 @@ let get_register_field_bit reg field =
     (match List.assoc field fields with
      | (i,j) ->
        if i = j
-       then bit_vector_access reg i
+       then bit_vector_access_int reg i
        else Vundef)
   | _ -> Vundef
 
@@ -137,7 +158,7 @@ let set_register register value = match register,value with
     a := new_v
   | _ -> ()
 
-let set_vector_subrange_vec v n m new_v =
+let set_vector_subrange_vec_int v n m new_v =
   let walker array length offset new_values =
     begin
       for x = 0 to length-1
@@ -152,9 +173,10 @@ let set_vector_subrange_vec v n m new_v =
   | _ -> ()
 
 let set_vector_subrange_vec_big v n m new_v =
-  set_vector_subrange_vec v (int_of_big_int n) (int_of_big_int m) new_v
+  set_vector_subrange_vec_int v (int_of_big_int n) (int_of_big_int m) new_v
+let set_vector_subrange_vec = set_vector_subrange_vec_big (* or maybe _int *)
 
-let set_vector_subrange_bit v n m new_v =
+let set_vector_subrange_bit_int v n m new_v =
   let walker array length offset new_values =
     begin
       for x = 0 to length-1
@@ -172,7 +194,9 @@ let set_vector_subrange_bit v n m new_v =
   | _ -> ()
 
 let set_vector_subrange_bit_big v n m new_v =
-  set_vector_subrange_bit v (int_of_big_int n) (int_of_big_int m) new_v
+  set_vector_subrange_bit_int v (int_of_big_int n) (int_of_big_int m) new_v
+let set_vector_subrange_bit = set_vector_subrange_bit_int
+
 
 let set_register_field_v reg field new_v =
   match reg with
@@ -199,8 +223,8 @@ let set_two_reg r1 r2 vec =
   let dir = get_ord r1 in
   let start = get_start vec in
   let vsize = length vec in
-  let r1_v = vector_subrange vec start ((if dir then size - start else start - size) - 1) in
-  let r2_v = vector_subrange vec (if dir then size - start else start - size)
+  let r1_v = vector_subrange_int vec start ((if dir then size - start else start - size) - 1) in
+  let r2_v = vector_subrange_int vec (if dir then size - start else start - size)
       (if dir then vsize - start else start - vsize) in
   begin set_register r1 r1_v; set_register r2 r2_v end
   
@@ -248,7 +272,7 @@ let vector_concat l r =
 let has_undef = function
   | Vvector(array,_,_) ->
     let rec foreach i =
-      if i <= Array.length array
+      if i < Array.length array
       then
         if array.(i) = Vundef then true
         else foreach (i+1)
@@ -257,7 +281,7 @@ let has_undef = function
   | Vregister(array,_,_,_) ->
     let array = !array in
     let rec foreach i =
-      if i <= Array.length array
+      if i < Array.length array
       then
         if array.(i) = Vundef then true
         else foreach (i+1)
@@ -298,7 +322,7 @@ let bitwise_binop op (l,r) =
   let bop l arrayl arrayr =
     let array = Array.make l Vzero in
     begin
-      for i = 0 to l do
+      for i = 0 to (l-1) do
         array.(i) <- bitwise_binop_bit op (arrayl.(i), arrayr.(i))
       done;
       array
@@ -323,66 +347,62 @@ let rec power_int base raiseto =
   then 1
   else base * (power_int base (raiseto - 1))
 
-let unsigned = function
+let int_of_bit_array array = 
+  let acc = ref 0 in
+  let len = Array.length array in
+  begin 
+    for i = len - 1 downto 0 do
+      match array.(len - i - 1) with
+      | Vone -> acc := !acc + (power_int 2 i)
+      | _ -> ()
+    done;
+    !acc
+  end
+
+let unsigned_int = function
   | (Vvector(array,_,_) as v) ->
     if has_undef v
     then assert false
-    else
-      let acc = ref 0 in
-      begin for i = (Array.length array) - 1 downto 0 do
-          match array.(i) with
-          | Vone -> acc := !acc + (power_int 2 i)
-          | _ -> ()
-        done;
-        !acc
-      end
+    else int_of_bit_array array
   | (Vregister(array,_,_,_) as v)->
     let array = !array in
     if has_undef v
     then assert false
-    else
-      let acc = ref 0 in
-      begin for i = (Array.length array) - 1 downto 0 do
-          match array.(i) with
-          | Vone -> acc := !acc + (power_int 2 i)
-          | _ -> ()
-        done;
-        !acc
-      end
+    else int_of_bit_array array
   | _ -> assert false
 
+let big_int_of_bit_array array = 
+  let acc = ref zero_big_int in
+  let len = Array.length array in
+  begin 
+    for i = len - 1 downto 0 do
+      match array.(len-i-1) with
+      | Vone -> acc := add_big_int !acc (power_int_positive_int 2 i)
+      | _ -> ()
+    done;
+    !acc
+  end
+
 let unsigned_big = function
   | (Vvector(array,_,_) as v) ->
     if has_undef v
     then assert false
     else
-      let acc = ref zero_big_int in
-      begin for i = (Array.length array) - 1 downto 0 do
-          match array.(i) with
-          | Vone -> acc := add_big_int !acc (power_int_positive_int 2 i)
-          | _ -> ()
-        done;
-        !acc
-      end
+      big_int_of_bit_array array
   | (Vregister(array,_,_,_) as v)->
     let array = !array in
     if has_undef v
     then assert false
     else
-      let acc = ref zero_big_int in
-      begin for i = (Array.length array) - 1 downto 0 do
-          match array.(i) with
-          | Vone -> acc := add_big_int !acc (power_int_positive_int 2 i)
-          | _ -> ()
-        done;
-        !acc
-      end
+      big_int_of_bit_array array
   | _ -> assert false
 
-let signed v =
+let unsigned = unsigned_big
+
+let signed_int v =
   match most_significant v with
-  | Vone -> -(1 + (unsigned (bitwise_not v)))
-  | Vzero -> unsigned v
+  | Vone -> -(1 + (unsigned_int (bitwise_not v)))
+  | Vzero -> unsigned_int v
   | _ -> assert false
 
 let signed_big v =
@@ -391,8 +411,11 @@ let signed_big v =
   | Vzero -> unsigned_big v
   | _ -> assert false
 
-let to_num sign = if sign then signed else unsigned
+let signed = signed_big
+
+let to_num_int sign = if sign then signed_int else unsigned_int
 let to_num_big sign = if sign then signed_big else unsigned_big
+let to_num = to_num_big
 
 let two_big_int = big_int_of_int 2
 let max_64u = pred_big_int (power_big two_big_int (big_int_of_int 64))
@@ -430,13 +453,13 @@ let rec divide_by_2_big array i n =
     then begin array.(i) <- Vone; divide_by_2_big array (i-1) quo end
     else divide_by_2_big array (i-1) quo
 
-let rec divide_by_2 array i n =
+let rec divide_by_2_int array i n =
   if i < 0 || n = 0
   then array
   else let (quo,modu) = n/2, n mod 2 in
-    if modu = 0
-    then begin array.(i) <- Vone; divide_by_2 array (i-1) quo end
-    else divide_by_2 array (i-1) quo
+    if modu = 1
+    then begin array.(i) <- Vone; divide_by_2_int array (i-1) quo end
+    else divide_by_2_int array (i-1) quo
 
 let rec add_one_bit array co i =
   if i < 0
@@ -448,16 +471,16 @@ let rec add_one_bit array co i =
     | Vone, true  -> add_one_bit array true (i-1)
     | Vundef,_ -> assert false
 
-let to_vec ord len n =
+let to_vec_int ord len n =
   let array = Array.make len Vzero in
   let start = if ord then 0 else len-1 in
   if n = 0
   then Vvector(array, start, ord)
   else if n >= 0 
-  then Vvector(divide_by_2 array (len -1) n, start, ord)
+  then Vvector(divide_by_2_int array (len -1) n, start, ord)
   else
     let abs_n = abs n in
-    let abs_array = divide_by_2 array (len-1) abs_n in
+    let abs_array = divide_by_2_int array (len-1) abs_n in
     let v_abs = bitwise_not (Vvector(abs_array,start,ord)) in
     match v_abs with
     | Vvector(array,start,ord) -> Vvector(add_one_bit array false (len-1),start,ord)
@@ -479,13 +502,16 @@ let to_vec_big ord len n =
     | Vvector(array,start,ord) -> Vvector(add_one_bit array false (len-1),start,ord)
     | _ -> assert false
 
-let to_vec_inc (len,n) = to_vec true len n
-let to_vec_dec (len,n) = to_vec false len n
+let to_vec_inc_int (len,n) = to_vec_int true len n
+let to_vec_dec_int (len,n) = to_vec_int false len n
 
 let to_vec_inc_big (len,n) = to_vec_big true len n
 let to_vec_dec_big (len,n) = to_vec_big false len n
 
-let to_vec_undef ord len = 
+let to_vec_inc = to_vec_inc_big
+let to_vec_dec = to_vec_dec_big
+
+let to_vec_undef_int ord len = 
   let array = Array.make len Vundef in
   let start = if ord then 0 else len-1 in
   Vvector(array, start, ord)
@@ -496,18 +522,24 @@ let to_vec_undef_big ord len =
   let start = if ord then 0 else len-1 in
   Vvector(array, start, ord)
 
-let to_vec_inc_undef len = to_vec_undef true len
-let to_vec_dec_undef len = to_vec_undef false len
+let to_vec_inc_undef_int len = to_vec_undef_int true len
+let to_vec_dec_undef_int len = to_vec_undef_int false len
 
 let to_vec_inc_undef_big len = to_vec_undef_big true len
 let to_vec_dec_undef_big len = to_vec_undef_big false len
 
-let exts (len, vec) = to_vec (get_ord vec) len (signed vec)
-let extz (len, vec) = to_vec (get_ord vec) len (unsigned vec)
+let to_vec_inc_undef = to_vec_inc_undef_big
+let to_vec_dec_undef = to_vec_dec_undef_big
+
+let exts_int (len, vec) = to_vec_int (get_ord vec) len (signed_int vec)
+let extz_int (len, vec) = to_vec_int (get_ord vec) len (unsigned_int vec)
 
 let exts_big (len,vec) = to_vec_big (get_ord vec) len (signed_big vec)
 let extz_big (len,vec) = to_vec_big (get_ord vec) len (unsigned_big vec)
 
+let exts = exts_big
+let extz = extz_big
+
 let arith_op op (l,r) = op l r
 let add_big = arith_op add_big_int
 let add_signed_big = arith_op add_big_int
@@ -517,13 +549,21 @@ let modulo_big = arith_op mod_big_int
 let quot_big = arith_op div_big_int
 let power_big = arith_op power_big
 
-let add = arith_op (+)
-let add_signed = arith_op (+)
-let minus = arith_op (-)
-let multiply = arith_op ( * )
-let modulo = arith_op (mod)
-let quot = arith_op (/)
-let power = arith_op power_int
+let add_int = arith_op (+)
+let add_signed_int = arith_op (+)
+let minus_int = arith_op (-)
+let multiply_int = arith_op ( * )
+let modulo_int = arith_op (mod)
+let quot_int = arith_op (/)
+let power_int = arith_op power_int
+
+let add        = add_big
+let add_signed = add_signed_big
+let minus      = minus_big
+let multiply   = multiply_big
+let modulo     = modulo_big
+let quot       = quot_big
+let power      = power_big
 
 let arith_op_vec_big op sign size (l,r) =
   let ord = get_ord l in
@@ -537,65 +577,83 @@ let minus_vec_big = arith_op_vec_big sub_big_int false unit_big_int
 let multiply_vec_big = arith_op_vec_big mult_big_int false two_big_int
 let multiply_vec_signed_big = arith_op_vec_big mult_big_int true two_big_int
 
-let arith_op_vec op sign size (l,r) =
+let arith_op_vec_int op sign size (l,r) =
   let ord = get_ord l in
-  let (l',r') = to_num sign l, to_num sign r in
+  let (l',r') = to_num_int sign l, to_num_int sign r in
   let n = arith_op op (l',r') in
-  to_vec ord (size * (length l)) n
+  to_vec_int ord (size * (length l)) n
 
-let add_vec = arith_op_vec (+) false 1
-let add_vec_signed = arith_op_vec (+) true 1
-let minus_vec = arith_op_vec (-) false 1
-let multiply_vec = arith_op_vec ( * ) false 2
-let multiply_vec_signed = arith_op_vec ( * ) true 2
+let add_vec_int = arith_op_vec_int (+) false 1
+let add_vec_signed_int = arith_op_vec_int (+) true 1
+let minus_vec_int = arith_op_vec_int (-) false 1
+let multiply_vec_int = arith_op_vec_int ( * ) false 2
+let multiply_vec_signed_int = arith_op_vec_int ( * ) true 2
 
-let arith_op_vec_range op sign size (l,r) =
+let add_vec             = add_vec_big            
+let add_vec_signed      = add_vec_signed_big     
+let minus_vec           = minus_vec_big          
+let multiply_vec        = multiply_vec_big       
+let multiply_vec_signed = multiply_vec_signed_big
+
+
+let arith_op_vec_range_int op sign size (l,r) =
   let ord = get_ord l in
-  arith_op_vec op sign size (l, to_vec ord (length l) r)
+  arith_op_vec_int op sign size (l, to_vec_int ord (length l) r)
 
-let add_vec_range = arith_op_vec_range (+) false 1
-let add_vec_range_signed = arith_op_vec_range (+) true 1
-let minus_vec_range = arith_op_vec_range (-) false 1
-let mult_vec_range = arith_op_vec_range ( * ) false 2
-let mult_vec_range_signed = arith_op_vec_range ( * ) true 2
+let add_vec_range_int = arith_op_vec_range_int (+) false 1
+let add_vec_range_signed_int = arith_op_vec_range_int (+) true 1
+let minus_vec_range_int = arith_op_vec_range_int (-) false 1
+let mult_vec_range_int = arith_op_vec_range_int ( * ) false 2
+let mult_vec_range_signed_int = arith_op_vec_range_int ( * ) true 2
 
 let arith_op_vec_range_big op sign size (l,r) =
   let ord = get_ord l in
   arith_op_vec_big op sign size (l, to_vec_big ord (length_big l) r)
 
-let add_vec_range_big = arith_op_vec_range_big add_big_int false unit_big_int
-let add_vec_range_signed_big = arith_op_vec_range_big add_big_int true unit_big_int
-let minus_vec_range_big = arith_op_vec_range_big sub_big_int false unit_big_int
-let mult_vec_range_big = arith_op_vec_range_big mult_big_int false two_big_int
+let add_vec_range_big         = arith_op_vec_range_big add_big_int false unit_big_int
+let add_vec_range_signed_big  = arith_op_vec_range_big add_big_int true unit_big_int
+let minus_vec_range_big       = arith_op_vec_range_big sub_big_int false unit_big_int
+let mult_vec_range_big        = arith_op_vec_range_big mult_big_int false two_big_int
 let mult_vec_range_signed_big = arith_op_vec_range_big mult_big_int true two_big_int
 
+let add_vec_range         = add_vec_range_big        
+let add_vec_range_signed  = add_vec_range_signed_big 
+let minus_vec_range       = minus_vec_range_big      
+let mult_vec_range        = mult_vec_range_big       
+let mult_vec_range_signed = mult_vec_range_signed_big
 
-let arith_op_range_vec op sign size (l,r) =
+let arith_op_range_vec_int op sign size (l,r) =
   let ord = get_ord r in
-  arith_op_vec op sign size ((to_vec ord (length r) l), r)
+  arith_op_vec_int op sign size ((to_vec_int ord (length r) l), r)
 
-let add_range_vec = arith_op_range_vec (+) false 1
-let add_range_vec_signed = arith_op_range_vec (+) true 1
-let minus_range_vec = arith_op_range_vec (-) false 1
-let mult_range_vec = arith_op_range_vec ( * ) false 2
-let mult_range_vec_signed = arith_op_range_vec ( * ) true 2
+let add_range_vec_int = arith_op_range_vec_int (+) false 1
+let add_range_vec_signed_int = arith_op_range_vec_int (+) true 1
+let minus_range_vec_int = arith_op_range_vec_int (-) false 1
+let mult_range_vec_int = arith_op_range_vec_int ( * ) false 2
+let mult_range_vec_signed_int = arith_op_range_vec_int ( * ) true 2
 
 let arith_op_range_vec_big op sign size (l,r) =
   let ord = get_ord r in
   arith_op_vec_big op sign size ((to_vec_big ord (length_big r) l), r)
 
-let add_range_vec_big = arith_op_range_vec_big add_big_int false unit_big_int
-let add_range_vec_signed_big = arith_op_range_vec_big add_big_int true unit_big_int
-let minus_range_vec_big = arith_op_range_vec_big sub_big_int false unit_big_int
-let mult_range_vec_big = arith_op_range_vec_big mult_big_int false two_big_int
+let add_range_vec_big         = arith_op_range_vec_big add_big_int false unit_big_int
+let add_range_vec_signed_big  = arith_op_range_vec_big add_big_int true unit_big_int
+let minus_range_vec_big       = arith_op_range_vec_big sub_big_int false unit_big_int
+let mult_range_vec_big        = arith_op_range_vec_big mult_big_int false two_big_int
 let mult_range_vec_signed_big = arith_op_range_vec_big mult_big_int true two_big_int
 
+let add_range_vec         = add_range_vec_big         
+let add_range_vec_signed  = add_range_vec_signed_big  
+let minus_range_vec       = minus_range_vec_big       
+let mult_range_vec        = mult_range_vec_big        
+let mult_range_vec_signed = mult_range_vec_signed_big 
+
 
-let arith_op_range_vec_range op sign (l,r) = arith_op op (l, to_num sign r)
+let arith_op_range_vec_range_int op sign (l,r) = arith_op op (l, to_num_int sign r)
 
-let add_range_vec_range = arith_op_range_vec_range (+) false
-let add_range_vec_range_signed = arith_op_range_vec_range (+) true
-let minus_range_vec_range = arith_op_range_vec_range (-) false
+let add_range_vec_range_int = arith_op_range_vec_range_int (+) false
+let add_range_vec_range_signed_int = arith_op_range_vec_range_int (+) true
+let minus_range_vec_range_int = arith_op_range_vec_range_int (-) false
 
 let arith_op_range_vec_range_big op sign (l,r) = arith_op op (l, to_num_big sign r)
 
@@ -603,11 +661,15 @@ let add_range_vec_range_big = arith_op_range_vec_range_big add_big_int false
 let add_range_vec_range_signed_big = arith_op_range_vec_range_big add_big_int true
 let minus_range_vec_range_big = arith_op_range_vec_range_big sub_big_int false
 
-let arith_op_vec_range_range op sign (l,r) = arith_op op (to_num sign l,r)
+let add_range_vec_range        = add_range_vec_range_big       
+let add_range_vec_range_signed = add_range_vec_range_signed_big 
+let minus_range_vec_range      = minus_range_vec_range_big     
 
-let add_vec_range_range = arith_op_vec_range_range (+) false
-let add_vec_range_range_signed = arith_op_vec_range_range (+) true
-let minus_vec_range_range = arith_op_vec_range_range (-) false
+let arith_op_vec_range_range_int op sign (l,r) = arith_op op (to_num_int sign l,r)
+
+let add_vec_range_range_int = arith_op_vec_range_range_int (+) false
+let add_vec_range_range_signed_int = arith_op_vec_range_range_int (+) true
+let minus_vec_range_range_int = arith_op_vec_range_range_int (-) false
 
 let arith_op_vec_range_range_big op sign (l,r) = arith_op op (to_num_big sign l,r)
 
@@ -615,12 +677,17 @@ let add_vec_range_range_big = arith_op_vec_range_range_big add_big_int false
 let add_vec_range_range_signed_big = arith_op_vec_range_range_big add_big_int true
 let minus_vec_range_range_big = arith_op_vec_range_range_big sub_big_int false
 
-let arith_op_vec_vec_range op sign (l,r) = 
-  let (l',r') = (to_num sign l,to_num sign r) in
+let add_vec_range_range        = add_vec_range_range_big        
+let add_vec_range_range_signed = add_vec_range_range_signed_big 
+let minus_vec_range_range      = minus_vec_range_range_big      
+
+
+let arith_op_vec_vec_range_int op sign (l,r) = 
+  let (l',r') = (to_num_int sign l,to_num_int sign r) in
   arith_op op (l',r')
 
-let add_vec_vec_range = arith_op_vec_vec_range (+) false
-let add_vec_vec_range_signed = arith_op_vec_vec_range (+) true
+let add_vec_vec_range_int        = arith_op_vec_vec_range_int (+) false
+let add_vec_vec_range_signed_int = arith_op_vec_vec_range_int (+) true
 
 let arith_op_vec_vec_range_big op sign (l,r) = 
   let (l',r') = (to_num_big sign l,to_num_big sign r) in
@@ -629,15 +696,18 @@ let arith_op_vec_vec_range_big op sign (l,r) =
 let add_vec_vec_range_big = arith_op_vec_vec_range_big add_big_int false
 let add_vec_vec_range_signed_big = arith_op_vec_vec_range_big add_big_int true
 
-let arith_op_vec_bit op sign (l,r) =
+let add_vec_vec_range        = add_vec_vec_range_big       
+let add_vec_vec_range_signed = add_vec_vec_range_signed_big
+
+let arith_op_vec_bit_int op sign (l,r) =
   let ord = get_ord l in
-  let l' = to_num sign l in
+  let l' = to_num_int sign l in
   let n = arith_op op (l', match r with | Vone -> 1 | _ -> 0) in
-  to_vec ord (length l) n
+  to_vec_int ord (length l) n
     
-let add_vec_bit = arith_op_vec_bit (+) false
-let add_vec_bit_signed = arith_op_vec_bit (+) true 
-let minus_vec_bit = arith_op_vec_bit (-) true
+let add_vec_bit_int = arith_op_vec_bit_int (+) false
+let add_vec_bit_signed_int = arith_op_vec_bit_int (+) true 
+let minus_vec_bit_int = arith_op_vec_bit_int (-) true
 
 let arith_op_vec_bit_big op sign (l,r) =
   let ord = get_ord l in
@@ -649,16 +719,21 @@ let add_vec_bit_big = arith_op_vec_bit_big add_big_int false
 let add_vec_bit_signed_big = arith_op_vec_bit_big add_big_int true
 let minus_vec_bit_big = arith_op_vec_bit_big sub_big_int true
 
-let rec arith_op_overflow_vec op sign size (l,r) =
+let add_vec_bit        = add_vec_bit_big       
+let add_vec_bit_signed = add_vec_bit_signed_big
+let minus_vec_bit      = minus_vec_bit_big     
+
+
+let rec arith_op_overflow_vec_int op sign size (l,r) =
   let ord = get_ord l in
   let len = length l in
   let act_size = len * size in
-  let (l_sign,r_sign) = (to_num sign l,to_num sign r) in
-  let (l_unsign,r_unsign) = (to_num false l,to_num false r) in
+  let (l_sign,r_sign) = (to_num_int sign l,to_num_int sign r) in
+  let (l_unsign,r_unsign) = (to_num_int false l,to_num_int false r) in
   let n = arith_op op (l_sign,r_sign) in
   let n_unsign = arith_op op (l_unsign,r_unsign) in
-  let correct_size_num = to_vec ord act_size n in
-  let one_more_size_u = to_vec ord (act_size +1) n_unsign in
+  let correct_size_num = to_vec_int ord act_size n in
+  let one_more_size_u = to_vec_int ord (act_size +1) n_unsign in
   let overflow = if (n <= (int_of_big_int (get_max_representable_in sign len))) &&
                     (n >= (int_of_big_int (get_min_representable_in sign len)))
     then Vzero
@@ -666,12 +741,12 @@ let rec arith_op_overflow_vec op sign size (l,r) =
   let c_out = most_significant one_more_size_u in
   (correct_size_num,overflow,c_out)
 
-let add_overflow_vec = arith_op_overflow_vec (+) false 1
-let add_overflow_vec_signed = arith_op_overflow_vec (+) true 1
-let minus_overflow_vec = arith_op_overflow_vec (-) false 1
-let minus_overflow_vec_signed = arith_op_overflow_vec (-) true 1
-let mult_overflow_vec = arith_op_overflow_vec ( * ) false 2
-let mult_overflow_vec_signed = arith_op_overflow_vec ( * ) true 2
+let add_overflow_vec_int = arith_op_overflow_vec_int (+) false 1
+let add_overflow_vec_signed_int = arith_op_overflow_vec_int (+) true 1
+let minus_overflow_vec_int = arith_op_overflow_vec_int (-) false 1
+let minus_overflow_vec_signed_int = arith_op_overflow_vec_int (-) true 1
+let mult_overflow_vec_int = arith_op_overflow_vec_int ( * ) false 2
+let mult_overflow_vec_signed_int = arith_op_overflow_vec_int ( * ) true 2
 
 let rec arith_op_overflow_vec_big op sign size (l,r) =
   let ord = get_ord l in
@@ -697,18 +772,25 @@ let minus_overflow_vec_signed_big = arith_op_overflow_vec_big sub_big_int true u
 let mult_overflow_vec_big = arith_op_overflow_vec_big mult_big_int false two_big_int
 let mult_overflow_vec_signed_big = arith_op_overflow_vec_big mult_big_int true two_big_int
 
-let rec arith_op_overflow_vec_bit op sign (l,r_bit) =
+let add_overflow_vec          = add_overflow_vec_big          
+let add_overflow_vec_signed   = add_overflow_vec_signed_big   
+let minus_overflow_vec        = minus_overflow_vec_big        
+let minus_overflow_vec_signed = minus_overflow_vec_signed_big 
+let mult_overflow_vec         = mult_overflow_vec_big         
+let mult_overflow_vec_signed  = mult_overflow_vec_signed_big  
+
+let rec arith_op_overflow_vec_bit_int op sign (l,r_bit) =
   let ord = get_ord l in
   let act_size = length l in
-  let l' = to_num sign l in
-  let l_u = to_num false l in
+  let l' = to_num_int sign l in
+  let l_u = to_num_int false l in
   let (n,nu,changed) = match r_bit with
     | Vone -> (arith_op op (l',1), arith_op op (l_u,1), true)
     | Vzero -> (l',l_u,false)
     | _ -> assert false
   in
-  let correct_size_num = to_vec ord act_size n in
-  let one_larger = to_vec ord (1+ act_size) nu in
+  let correct_size_num = to_vec_int ord act_size n in
+  let one_larger = to_vec_int ord (1+ act_size) nu in
   let overflow =
     if changed 
     then if (n <= (int_of_big_int (get_max_representable_in sign act_size))) &&
@@ -718,9 +800,9 @@ let rec arith_op_overflow_vec_bit op sign (l,r_bit) =
     else Vone in
         (correct_size_num,overflow,most_significant one_larger)
 
-let add_overflow_vec_bit_signed = arith_op_overflow_vec_bit (+) true 
-let minus_overflow_vec_bit = arith_op_overflow_vec_bit (-) false 
-let minus_overflow_vec_bit_signed = arith_op_overflow_vec_bit (-) true
+let add_overflow_vec_bit_signed_int = arith_op_overflow_vec_bit_int (+) true 
+let minus_overflow_vec_bit_int = arith_op_overflow_vec_bit_int (-) false 
+let minus_overflow_vec_bit_signed_int = arith_op_overflow_vec_bit_int (-) true
 
 let rec arith_op_overflow_vec_bit_big op sign (l,r_bit) =
   let ord = get_ord l in
@@ -747,8 +829,11 @@ let add_overflow_vec_bit_signed_big = arith_op_overflow_vec_bit_big add_big_int
 let minus_overflow_vec_bit_big = arith_op_overflow_vec_bit_big sub_big_int false 
 let minus_overflow_vec_bit_signed_big = arith_op_overflow_vec_bit_big sub_big_int true
 
+let add_overflow_vec_bit_signed   = add_overflow_vec_bit_signed_big   
+let minus_overflow_vec_bit        = minus_overflow_vec_bit_big        
+let minus_overflow_vec_bit_signed = minus_overflow_vec_bit_signed_big 
 
-let shift_op_vec op (l,r) =
+let shift_op_vec_int op (l,r) =
   match l with
   | Vvector(_,start,ord) | Vregister(_,start,ord,_) ->
     let array = match l with | Vvector(array,_,_) -> array | Vregister(array,_,_,_) -> !array | _ -> assert false in
@@ -756,49 +841,46 @@ let shift_op_vec op (l,r) =
     (match op with
      | "<<" ->
        let right_vec = Vvector(Array.make r Vzero,0,true) in
-       let left_vec = vector_subrange l r (if ord then len + start else start - len) in
+       let left_vec = vector_subrange_int l r (if ord then len + start else start - len) in
        vector_concat left_vec right_vec
      | ">>" ->
-       let right_vec = vector_subrange l start r in
+       let right_vec = vector_subrange_int l start r in
        let left_vec = Vvector(Array.make r Vzero,0,true) in
        vector_concat left_vec right_vec 
      | "<<<" ->
-       let left_vec = vector_subrange l r (if ord then len + start else start - len) in
-       let right_vec = vector_subrange l start r in
+       let left_vec = vector_subrange_int l r (if ord then len + start else start - len) in
+       let right_vec = vector_subrange_int l start r in
        vector_concat left_vec right_vec
      | _ -> assert false)
   | _ -> assert false
 
-let bitwise_leftshift = shift_op_vec "<<"
-let bitwise_rightshift = shift_op_vec ">>"
-let bitwise_rotate = shift_op_vec "<<<"
-
-let shift_op_vec_big op (l,r) = shift_op_vec op (l, int_of_big_int r)
+let shift_op_vec_big op (l,r) = shift_op_vec_int op (l, int_of_big_int r)
 let bitwise_leftshift_big = shift_op_vec_big "<<"
 let bitwise_rightshift_big = shift_op_vec_big ">>"
 let bitwise_rotate_big = shift_op_vec_big "<<<"
-    
+
+let bitwise_leftshift = bitwise_leftshift_big
+let bitwise_rightshift = bitwise_rightshift_big
+let bitwise_rotate = bitwise_rotate_big
+
 let rec arith_op_no0_big op (l,r) = 
   if eq_big_int r zero_big_int
   then None
   else Some (op l r)
 
-let modulo_big = arith_op_no0_big mod_big_int
-let quot_big = arith_op_no0_big div_big_int
+let modulo_no0_big = arith_op_no0_big mod_big_int
+let quot_no0_big = arith_op_no0_big div_big_int
 
-let rec arith_op_no0 op (l,r) = 
+let rec arith_op_no0_int op (l,r) = 
   if r = 0
   then None
   else Some (op l r)
 
-let modulo = arith_op (mod)
-let quot = arith_op (/)
-
-let rec arith_op_vec_no0 op sign size (l,r) =
+let rec arith_op_vec_no0_int op sign size (l,r) =
   let ord = get_ord l in
   let act_size = ((length l) * size) in
-  let (l',r') = (to_num sign l,to_num sign r) in
-  let n = arith_op_no0 op (l',r') in
+  let (l',r') = (to_num_int sign l,to_num_int sign r) in
+  let n = arith_op_no0_int op (l',r') in
   let representable,n' = 
     match n with 
     | Some n' ->  
@@ -806,16 +888,16 @@ let rec arith_op_vec_no0 op sign size (l,r) =
        (n' >= (int_of_big_int (get_min_representable_in sign act_size)))), n'
     | _ -> false,0 in
   if representable 
-  then to_vec ord act_size n'
+  then to_vec_int ord act_size n'
   else
     match l with
     | Vvector(_, start, _) | Vregister(_, start, _, _) ->
       Vvector((Array.make act_size Vundef), start, ord)
     | _ -> assert false
 
-let mod_vec = arith_op_vec_no0 (mod) false 1
-let quot_vec = arith_op_vec_no0 (/) false 1
-let quot_vec_signed = arith_op_vec_no0 (/) true 1
+let mod_vec_int = arith_op_vec_no0_int (mod) false 1
+let quot_vec_int = arith_op_vec_no0_int (/) false 1
+let quot_vec_signed_int = arith_op_vec_no0_int (/) true 1
 
 let rec arith_op_vec_no0_big op sign size (l,r) =
   let ord = get_ord l in
@@ -840,14 +922,18 @@ let mod_vec_big = arith_op_vec_no0_big mod_big_int false unit_big_int
 let quot_vec_big = arith_op_vec_no0_big div_big_int false unit_big_int
 let quot_vec_signed_big = arith_op_vec_no0_big div_big_int true unit_big_int
 
-let arith_op_overflow_no0_vec op sign size (l,r) =
+let mod_vec         = mod_vec_big         
+let quot_vec        = quot_vec_big        
+let quot_vec_signed = quot_vec_signed_big 
+
+let arith_op_overflow_no0_vec_int op sign size (l,r) =
   let ord = get_ord l in
   let rep_size = (length r) * size in
   let act_size = (length l) * size in
-  let (l',r') = ((to_num sign l),(to_num sign r)) in
-  let (l_u,r_u) = (to_num false l,to_num false r) in
-  let n = arith_op_no0 op (l',r') in
-  let n_u = arith_op_no0 op (l_u,r_u) in
+  let (l',r') = ((to_num_int sign l),(to_num_int sign r)) in
+  let (l_u,r_u) = (to_num_int false l,to_num_int false r) in
+  let n = arith_op_no0_int op (l',r') in
+  let n_u = arith_op_no0_int op (l_u,r_u) in
   let representable,n',n_u' = 
     match n, n_u with 
     | Some n',Some n_u' ->  
@@ -856,7 +942,7 @@ let arith_op_overflow_no0_vec op sign size (l,r) =
     | _ -> true,0,0 in
   let (correct_size_num,one_more) = 
     if representable then
-      (to_vec ord act_size n',to_vec ord (1+act_size) n_u')
+      (to_vec_int ord act_size n',to_vec_int ord (1+act_size) n_u')
     else match l with 
       | Vvector(_, start, _) | Vregister(_, start, _, _) ->
         Vvector((Array.make act_size Vundef), start, ord),
@@ -865,8 +951,8 @@ let arith_op_overflow_no0_vec op sign size (l,r) =
   let overflow = if representable then Vzero else Vone in
   (correct_size_num,overflow,most_significant one_more)
 
-let quot_overflow_vec = arith_op_overflow_no0_vec (/) false 1
-let quot_overflow_vec_signed = arith_op_overflow_no0_vec (/) true 1
+let quot_overflow_vec_int = arith_op_overflow_no0_vec_int (/) false 1
+let quot_overflow_vec_signed_int = arith_op_overflow_no0_vec_int (/) true 1
 
 let arith_op_overflow_no0_vec_big op sign size (l,r) =
   let ord = get_ord l in
@@ -896,11 +982,15 @@ let arith_op_overflow_no0_vec_big op sign size (l,r) =
 let quot_overflow_vec_big = arith_op_overflow_no0_vec_big div_big_int false unit_big_int 
 let quot_overflow_vec_signed_big = arith_op_overflow_no0_vec_big div_big_int true unit_big_int 
 
-let arith_op_vec_range_no0 op sign size (l,r) =
+let quot_overflow_vec        = quot_overflow_vec_big        
+let quot_overflow_vec_signed = quot_overflow_vec_signed_big 
+
+
+let arith_op_vec_range_no0_int op sign size (l,r) =
   let ord = get_ord l in
-  arith_op_vec_no0 op sign size (l,(to_vec ord (length l) r))
+  arith_op_vec_no0_int op sign size (l,(to_vec_int ord (length l) r))
 
-let mod_vec_range = arith_op_vec_range_no0 (mod) false 1
+let mod_vec_range_int = arith_op_vec_range_no0_int (mod) false 1
 
 let arith_op_vec_range_no0_big op sign size (l,r) =
   let ord = get_ord l in
@@ -908,13 +998,17 @@ let arith_op_vec_range_no0_big op sign size (l,r) =
 
 let mod_vec_range_big = arith_op_vec_range_no0_big mod_big_int false unit_big_int
 
+let mod_vec_range = mod_vec_range_big
+
 (*Need to have a default top level direction reference I think*)
-let duplicate (bit,length) =
+let duplicate_int (bit,length) =
   Vvector((Array.make length bit), 0, true)
 
 let duplicate_big (bit,length) =
   Vvector((Array.make (int_of_big_int length) bit), 0, true)
 
+let duplicate = duplicate_big
+
 let compare_op op (l,r) =
   if (op l r)
   then Vone
@@ -924,27 +1018,32 @@ let lt_big = compare_op lt_big_int
 let gt_big = compare_op gt_big_int
 let lteq_big = compare_op le_big_int
 let gteq_big = compare_op ge_big_int
-let lt : (int* int) -> vbit = compare_op (<)
-let gt : (int * int) -> vbit = compare_op (>)
-let lteq : (int * int) -> vbit = compare_op (<=)
-let gteq : (int*int) -> vbit = compare_op (>=)
-
-let compare_op_vec op sign (l,r) = 
-  let (l',r') = (to_num sign l, to_num sign r) in
+let lt_int : (int* int) -> vbit = compare_op (<)
+let gt_int : (int * int) -> vbit = compare_op (>)
+let lteq_int : (int * int) -> vbit = compare_op (<=)
+let gteq_int : (int*int) -> vbit = compare_op (>=)
+
+let lt = lt_big
+let gt = gt_big
+let lteq = lteq_big
+let gteq = gteq_big
+
+let compare_op_vec_int op sign (l,r) = 
+  let (l',r') = (to_num_int sign l, to_num_int 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_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_int = compare_op_vec_int (<) true
+let gt_vec_int = compare_op_vec_int (>) true
+let lteq_vec_int = compare_op_vec_int (<=) true
+let gteq_vec_int = compare_op_vec_int (>=) true
+let lt_vec_signed_int = compare_op_vec_int (<) true
+let gt_vec_signed_int = compare_op_vec_int (>) true
+let lteq_vec_signed_int = compare_op_vec_int (<=) true
+let gteq_vec_signed_int = compare_op_vec_int (>=) true
+let lt_vec_unsigned_int = compare_op_vec_int (<) false
+let gt_vec_unsigned_int = compare_op_vec_int (>) false
+let lteq_vec_unsigned_int = compare_op_vec_int (<=) false
+let gteq_vec_unsigned_int = compare_op_vec_int (>=) false
 
 let compare_op_vec_big op sign (l,r) = 
   let (l',r') = (to_num_big sign l, to_num_big sign r) in
@@ -963,14 +1062,26 @@ let gt_vec_unsigned_big = compare_op_vec_big gt_big_int false
 let lteq_vec_unsigned_big = compare_op_vec_big le_big_int false
 let gteq_vec_unsigned_big = compare_op_vec_big ge_big_int false
 
-
-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            = lt_vec_big            
+let gt_vec            = gt_vec_big            
+let lteq_vec          = lteq_vec_big          
+let gteq_vec          = gteq_vec_big          
+let lt_vec_signed     = lt_vec_signed_big     
+let gt_vec_signed     = gt_vec_signed_big     
+let lteq_vec_signed   = lteq_vec_signed_big   
+let gteq_vec_signed   = gteq_vec_signed_big   
+let lt_vec_unsigned   = lt_vec_unsigned_big   
+let gt_vec_unsigned   = gt_vec_unsigned_big   
+let lteq_vec_unsigned = lteq_vec_unsigned_big 
+let gteq_vec_unsigned = gteq_vec_unsigned_big 
+
+let compare_op_vec_range_int op sign (l,r) = 
+  compare_op op ((to_num_int sign l),r)
+
+let lt_vec_range_int = compare_op_vec_range_int (<) true
+let gt_vec_range_int = compare_op_vec_range_int (>) true
+let lteq_vec_range_int = compare_op_vec_range_int (<=) true
+let gteq_vec_range_int = compare_op_vec_range_int (>=) true
 
 let compare_op_vec_range_big op sign (l,r) = 
   compare_op op ((to_num_big sign l),r)
@@ -980,13 +1091,18 @@ let gt_vec_range_big = compare_op_vec_range_big gt_big_int true
 let lteq_vec_range_big = compare_op_vec_range_big le_big_int true
 let gteq_vec_range_big = compare_op_vec_range_big ge_big_int true
 
-let compare_op_range_vec op sign (l,r) =
-  compare_op op (l, (to_num sign r))
+let lt_vec_range   = lt_vec_range_big   
+let gt_vec_range   = gt_vec_range_big   
+let lteq_vec_range = lteq_vec_range_big 
+let gteq_vec_range = gteq_vec_range_big 
+
+let compare_op_range_vec_int op sign (l,r) =
+  compare_op op (l, (to_num_int 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_int = compare_op_range_vec_int (<) true
+let gt_range_vec_int = compare_op_range_vec_int (>) true
+let lteq_range_vec_int = compare_op_range_vec_int (<=) true
+let gteq_range_vec_int = compare_op_range_vec_int (>=) true
 
 let compare_op_range_vec_big op sign (l,r) =
   compare_op op (l, (to_num_big sign r))
@@ -996,12 +1112,16 @@ let gt_range_vec_big = compare_op_range_vec_big gt_big_int true
 let lteq_range_vec_big = compare_op_range_vec_big le_big_int true
 let gteq_range_vec_big = compare_op_range_vec_big ge_big_int true
 
+let lt_range_vec   = lt_range_vec_big   
+let gt_range_vec   = gt_range_vec_big   
+let lteq_range_vec = lteq_range_vec_big 
+let gteq_range_vec = gteq_range_vec_big 
 
 let eq (l,r) = if l == r then Vone else Vzero
-let eq_vec_vec (l,r) = eq (to_num true l, to_num true r)
+let eq_vec_vec (l,r) = eq (to_num_big true l, to_num_big true r)
 let eq_vec (l,r) = eq_vec_vec(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)
+let eq_vec_range (l,r) = eq (to_num_big false l,r)
+let eq_range_vec (l,r) = eq (l, to_num_big false r)
 let eq_range = eq
 let eq_bit = bitwise_binop_bit (=)
 
@@ -1009,23 +1129,28 @@ let neq (l,r) = bitwise_not_bit (eq (l,r))
 let neq_vec (l,r) = bitwise_not_bit (eq_vec_vec(l,r))
 let neq_bit (l,r) = bitwise_not_bit (eq_bit(l,r))
 
-let mask (n,v) = match v with
+let mask (n,v) = 
+  let n' = int_of_big_int n in
+  match v with
   | Vvector (bits,start,dir) ->
      let current_size = Array.length bits in 
-     let to_drop = (current_size - n) in
-     let bits' = Array.sub bits to_drop n in
-     Vvector (bits',(if dir then 0 else n-1), dir)
+     let to_drop = (current_size - n') in
+     let bits' = Array.sub bits to_drop n' in
+     Vvector (bits',(if dir then 0 else n'-1), dir)
   | VvectorR (bits,start,dir) ->
      let current_size = Array.length bits in 
-     let to_drop = (current_size - n) in
-     let bits' = Array.sub bits to_drop n in
-     VvectorR (bits',(if dir then 0 else n-1), dir)
+     let to_drop = (current_size - n') in
+     let bits' = Array.sub bits to_drop n' in
+     VvectorR (bits',(if dir then 0 else n'-1), dir)
   | Vregister _ -> failwith "mask not implemented for Vregister"
   | Vbit _ -> failwith "mask called for bit"
 
-let slice_raw (v, i, j) = match v with
+let slice_raw (v, i, j) = 
+  let i' = int_of_big_int i in
+  let j' = int_of_big_int j in
+  match v with
   | Vvector (bs, start, is_inc) ->
-     let bits = Array.sub bs i j in
+     let bits = Array.sub bs i' (j'-i'+1) in
      let len = Array.length bits in
      Vvector (bits, (if is_inc then 0 else len - 1), is_inc)
   | _ -> failwith "slice_raw only implemented for VVector"
diff --git a/src/pretty_print.ml b/src/pretty_print.ml
index 83b0cabf..b7b88bb1 100644
--- a/src/pretty_print.ml
+++ b/src/pretty_print.ml
@@ -1533,9 +1533,7 @@ let is_number char =
 let doc_id_ocaml (Id_aux(i,_)) =
   match i with
   | Id("bit") -> string "vbit"
-  | Id i -> string (if i.[0] = '\'' || is_number(i.[0])
-                    then "_" ^ i
-                    else  "_" ^ (String.uncapitalize i))
+  | Id i -> string ("_" ^ i)
   | DeIid x ->
       (* add an extra space through empty to avoid a closing-comment
        * token in case of x ending with star. *)
@@ -1544,7 +1542,7 @@ let doc_id_ocaml (Id_aux(i,_)) =
 let doc_id_ocaml_type (Id_aux(i,_)) =
   match i with
   | Id("bit") -> string "vbit"
-  | Id i -> string ("_" ^ (String.uncapitalize i))
+  | Id i -> string ("_" ^ i)
   | DeIid x ->
       (* add an extra space through empty to avoid a closing-comment
        * token in case of x ending with star. *)
@@ -1607,7 +1605,7 @@ let doc_lit_ocaml in_pat (L_aux(l,_)) =
   | L_one   -> "Vone"
   | L_true  -> "Vone"
   | L_false -> "Vzero"
-  | L_num i -> string_of_int i
+  | L_num i -> "(big_int_of_int " ^ (string_of_int i) ^ ")"
   | L_hex n -> "(num_to_vec " ^ ("0x" ^ n) ^ ")" (*shouldn't happen*)
   | L_bin n -> "(num_to_vec " ^ ("0b" ^ n) ^ ")" (*shouldn't happen*)
   | L_undef -> "Vundef"
@@ -1875,7 +1873,7 @@ let doc_exp_ocaml, doc_let_ocaml =
   | E_list exps ->
       brackets (separate_map semi exp exps)
   | E_case(e,pexps) ->
-      let opening = separate space [string "("; string "match"; top_exp true e; string "with"] in
+      let opening = separate space [string "("; string "match"; top_exp false e; string "with"] in
       let cases = separate_map (break 1) doc_case pexps in
       surround 2 1 opening cases rparen
   | E_exit e ->
@@ -1937,10 +1935,10 @@ let doc_exp_ocaml, doc_let_ocaml =
          let t_act = match t.t with | Tapp("reg",[TA_typ t]) | Tabbrev(_,{t=Tapp("reg",[TA_typ t])}) -> t | _ -> t in
          (match t_act.t with
           | Tid "bit" | Tabbrev(_,{t=Tid "bit"}) ->
-            parens ((string "get_barray") ^^ space ^^ doc_lexp_ocaml false v) ^^ dot ^^ parens (top_exp false e)
-          | _ -> parens ((string "get_varray") ^^ space ^^ doc_lexp_ocaml false v) ^^ dot ^^ parens (top_exp false e))
+            parens ((string "get_barray") ^^ space ^^ doc_lexp_ocaml false v) ^^ dot ^^ parens ((string "int_of_big_int") ^^ space ^^ (top_exp false e))
+          | _ -> parens ((string "get_varray") ^^ space ^^ doc_lexp_ocaml false v) ^^ dot ^^ parens ((string "int_of_big_int") ^^ space ^^ (top_exp false e)))
        | _ ->
-         parens ((string "get_varray") ^^ space ^^ doc_lexp_ocaml false v) ^^ dot ^^ parens (top_exp false e))
+         parens ((string "get_varray") ^^ space ^^ doc_lexp_ocaml false v) ^^ dot ^^ parens ((string "int_of_big_int") ^^ space ^^ (top_exp false e)))
     | _ -> empty
 
   and doc_lexp_rwrite ((LEXP_aux(lexp,(l,annot))) as le) e_new_v =
@@ -1961,7 +1959,7 @@ let doc_exp_ocaml, doc_let_ocaml =
     | LEXP_vector(v,e) ->
       doc_op (string "<-")
         (group (parens ((string (if is_bit then "get_barray" else "get_varray")) ^^ space ^^ doc_lexp_ocaml false v)) ^^
-         dot ^^ parens (exp e))
+         dot ^^ parens ((string "int_of_big_int") ^^ space ^^ (exp e)))
         (exp e_new_v)
     | LEXP_vector_range(v,e1,e2) ->
       parens ((string (if is_bitv then "set_vector_subrange_bit" else "set_vector_subrange_vec")) ^^ space ^^
@@ -1981,7 +1979,7 @@ let doc_exp_ocaml, doc_let_ocaml =
             then
               doc_op (string "<-")
                 (group (parens ((string (if is_bit then "get_barray" else "get_varray")) ^^ space ^^ string reg)) ^^
-                 dot ^^ parens (doc_int start))
+                 dot ^^ parens ((string "int_of_big_int") ^^ space ^^ (doc_int start)))
                 (exp e_new_v)
             else
               parens ((string (if is_bitv then "set_vector_subrange_bit" else "set_vector_subrange_vec")) ^^ space ^^
@@ -2035,7 +2033,7 @@ let doc_typdef_ocaml (TD_aux(td,_)) = match td with
     match n1,n2 with
     | Nexp_aux(Nexp_constant i1,_),Nexp_aux(Nexp_constant i2,_) ->
       let dir = i1 < i2 in
-      let size = if dir then i2-i1 +1 else i1-i2 in
+      let size = if dir then i2-i1 +1 else i1-i2+1  in
       doc_op equals
         ((string "let") ^^ space ^^ doc_id_ocaml id ^^ space ^^ (string "init_val"))
         (separate space [string "Vregister";
@@ -2184,6 +2182,8 @@ let doc_def_ocaml def = group (match def with
   | DEF_val lbind -> doc_let_ocaml lbind
   | DEF_reg_dec dec -> doc_dec_ocaml dec
   | DEF_scattered sdef -> empty (*shoulnd't still be here*)
+  | DEF_kind _ -> failwith "unhandled DEF_kind"
+  | DEF_comm _ -> failwith "unhandled DEF_comm"
   ) ^^ hardline
 
 let doc_defs_ocaml (Defs(defs)) =
diff --git a/src/rewriter.ml b/src/rewriter.ml
index bd0670f4..d26879e9 100644
--- a/src/rewriter.ml
+++ b/src/rewriter.ml
@@ -1350,8 +1350,8 @@ let rewrite_defs_ocaml defs =
   let defs_sorted = top_sort_defs defs in
   let defs_vec_concat_removed = rewrite_defs_remove_vector_concat defs_sorted in
   let defs_lifted_assign = rewrite_defs_exp_lift_assign defs_vec_concat_removed in
-  let defs_separate_nums = rewrite_defs_separate_numbs defs_lifted_assign in
-  defs_separate_nums
+(*  let defs_separate_nums = rewrite_defs_separate_numbs defs_lifted_assign in *)
+  defs_lifted_assign
 
 let rewrite_defs_remove_blocks =
   let letbind_wild v body =