replace memory representation with map of 1MB pages rather than map of bytes. This makes loading binaries much quicker but doesn't seem to make a big difference to execution speed.

3 files changed, 62 insertions, 33 deletions

diff --git a/mips/mips_extras_ml.ml b/mips/mips_extras_ml.ml
index 96c55909..da1aa0ad 100644
--- a/mips/mips_extras_ml.ml
+++ b/mips/mips_extras_ml.ml
@@ -11,9 +11,50 @@ module Mem = struct
     end)
 end
 
-let mips_mem = (ref Mem.empty : (int Mem.t) ref);;
+let mem_pages = (ref Mem.empty : (Bytes.t Mem.t) ref);;
 let tag_mem = (ref Mem.empty : (bool Mem.t) ref);;
 
+let page_shift_bits = 20 (* 1M page *)
+let page_size_bytes = 1 lsl page_shift_bits;; 
+
+
+let page_no_of_addr a = shift_right_big_int a page_shift_bits;;
+let bottom_addr_of_page p = shift_left_big_int p page_shift_bits
+let top_addr_of_page p = shift_left_big_int (succ_big_int p) page_shift_bits
+let get_page p =
+  try
+    Mem.find p !mem_pages
+  with Not_found -> 
+    let new_page = Bytes.create page_size_bytes in
+    mem_pages := Mem.add p new_page !mem_pages;
+    new_page
+  
+let rec add_mem_bytes addr buf off len =
+  let page_no = page_no_of_addr addr in
+  let page_bot = bottom_addr_of_page page_no in
+  let page_top = top_addr_of_page page_no in
+  let page_off = int_of_big_int (sub_big_int addr page_bot) in
+  let page = get_page page_no in
+  let bytes_left_in_page = sub_big_int page_top addr in
+  let to_copy = min_int (int_of_big_int bytes_left_in_page) len in
+  Bytes.blit buf off page page_off to_copy;
+  if (to_copy < len) then
+    add_mem_bytes page_top buf (off + to_copy) (len - to_copy)
+
+let rec read_mem_bytes addr len = 
+  let page_no = page_no_of_addr addr in
+  let page_bot = bottom_addr_of_page page_no in
+  let page_top = top_addr_of_page page_no in
+  let page_off = int_of_big_int (sub_big_int addr page_bot) in
+  let page = get_page page_no in
+  let bytes_left_in_page = sub_big_int page_top addr in
+  let to_get = min_int (int_of_big_int bytes_left_in_page) len in
+  let bytes = Bytes.sub page page_off to_get in
+  if to_get >= len then
+    bytes
+  else
+    Bytes.cat bytes (read_mem_bytes page_top (len - to_get))
+
 let _MEMea (addr, size) = ()
 let _MEMea_conditional = _MEMea
 let _MEMea_tag  = _MEMea
@@ -23,15 +64,13 @@ let _MEMval (addr, size, data) =
   (* assumes data is decreasing vector to be stored in little-endian byte order in mem *)
   let s = int_of_big_int size in
   let a = unsigned_big(addr) in
+  let buf = Bytes.create s 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 (s-1-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
+    Bytes.set buf (s-1-i) (char_of_int byte);
+  done;
+  add_mem_bytes a buf 0 s
 
 let _MEMval_tag (addr, size, data) =
   let tag = bit_vector_access_int data 0 in
@@ -54,15 +93,11 @@ let _MEMval_tag_conditional (addr, size, data) =
 let _MEMr (addr, size) = begin
   let s = int_of_big_int size in
   let a = unsigned_big(addr) in
+  let bytes = read_mem_bytes a s 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_vec = 
-      try
-        let byte = Mem.find byte_addr !mips_mem in
-        to_vec_dec_int (8, byte)
-      with Not_found -> 
-        to_vec_dec_int (8, 0) in (* XXX return 0 for uninitialised memory. Optionally return undef instead. *)
+    let byte = Bytes.get bytes i in
+    let byte_vec = to_vec_dec_int (8, int_of_char byte) in
     ret := vector_concat byte_vec (!ret);
     (*printf "MEM [%s] -> %x %s %s\n" (big_int_to_hex byte_addr) byte (string_of_value byte_vec) (string_of_value !ret);*)
   done;
diff --git a/mips/run_embed.ml b/mips/run_embed.ml
index 7d83355e..a1d9e059 100644
--- a/mips/run_embed.ml
+++ b/mips/run_embed.ml
@@ -64,12 +64,6 @@ let big_int_to_hex64 i = Z.format "%016x" 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 max_cut_off = ref false
 let max_instr = ref 0
 let model_arg = ref "cheri"
@@ -355,17 +349,12 @@ let rec fde_loop (model, count) =
           fde_loop (model, count + 1)
   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 rec load_raw_file buf addr len chan =
+    let to_read = min_int len page_size_bytes in
+    really_input chan buf 0 to_read;
+    add_mem_bytes addr buf 0 to_read;
+    if (len > to_read) then
+      load_raw_file buf (add_int_big_int to_read addr) (len - to_read) chan
 
 let get_model = function
   | "cheri128" -> (module CHERI128_model : ISA_model)
@@ -384,7 +373,10 @@ let anon_raw s =
   raw_list := (!raw_list) @ [(f, big_int_of_string addr)]
 
 let load_raw_arg (f, a) =
-  load_raw_file mips_mem a (open_in_bin f)
+  let buf = Bytes.create page_size_bytes in
+  let chan = open_in_bin f in
+  let len = in_channel_length chan in
+  load_raw_file buf a len chan
 
 let run () =
   (* Turn off line-buffering of standard input to allow responsive console input  *)
diff --git a/src/gen_lib/sail_values.ml b/src/gen_lib/sail_values.ml
index 6f46d7c3..99f037f7 100644
--- a/src/gen_lib/sail_values.ml
+++ b/src/gen_lib/sail_values.ml
@@ -630,7 +630,9 @@ let multiply   = multiply_big
 let modulo     = modulo_big
 let quot       = quot_big
 let power      = power_big
-let min        = min_big
+let min_int    = min (* the built-in version *)
+let min        = min_big (* is overwritten here *)
+let max_int    = max (* likewise *)
 let max        = max_big
 
 let arith_op_vec_big op sign size (l,r) =