diff options
| -rw-r--r-- | mips/mips_extras_ml.ml | 63 | ||||
| -rw-r--r-- | mips/run_embed.ml | 28 | ||||
| -rw-r--r-- | src/gen_lib/sail_values.ml | 4 |
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) = |