Attempt multi-byte memory read and write

Test seems to fail for some reason, probably endianess and off-by-one
bugs all over the place. Needs debugging code to monitor memory
updates and display bitvectors in a compact way.

2 files changed, 35 insertions, 2 deletions

diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index f0e45646..3f39d543 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -93,6 +93,8 @@ let slice v = function
   | Some (n, m) -> slice_vector v n m
 ;;
 
+let vconcat v v' = vec_concat (V_tuple [v; v']) ;;
+
 let perform_action ((reg, mem) as env) = function
  | Read_reg ((Reg (id, _) | SubReg (id, _, _)), sub) ->
      slice (Reg.find id reg) sub, env
@@ -109,6 +111,29 @@ let perform_action ((reg, mem) as env) = function
      V_lit L_unit, (Reg.add id new_val reg, mem)
  | Write_mem (id, V_lit(L_num n), None, value) ->
      V_lit L_unit, (reg, Mem.add (id, n) value mem)
+ (* multi-byte accesses to memory *)
+ (* XXX this doesn't deal with endianess at all, and it seems broken in tests *)
+ | Read_mem (id, V_tuple [V_lit(L_num n); V_lit(L_num size)], sub) ->
+     let rec fetch k acc =
+       if eq_big_int k size then slice acc sub else
+         let slice = Mem.find (id, add_big_int n k) mem in
+         fetch (succ_big_int k) (vconcat acc slice)
+     in
+     fetch zero_big_int (V_vector (zero_big_int, true, [])), env
+ (* XXX no support for multi-byte slice write at the moment - not hard to add,
+  * but we need a function basic read/write first since slice access involves
+  * read, fupdate, write. *)
+ | Write_mem (id, V_tuple [V_lit(L_num n); V_lit(L_num size)], None, value) ->
+     (* assumes smallest unit of memory is 8 bit *)
+     let byte_size = 8 in
+     let rec update k mem =
+       if eq_big_int k size then mem else
+         let slice = slice_vector value
+           (mult_int_big_int byte_size k)
+           (mult_int_big_int byte_size (succ_big_int k)) in
+         let mem' = Mem.add (id, add_big_int n k) slice mem in
+         update (succ_big_int k) mem'
+     in V_lit L_unit, (reg, update zero_big_int mem)
  (* This case probably never happens in the POWER spec anyway *)
  | Write_mem (id, V_lit(L_num n), Some (start, stop), value) ->
      (* XXX if updating a single element, wrap value into a vector -
diff --git a/src/test/test3.sail b/src/test/test3.sail
index e6bf4cdd..0ffab6ae 100644
--- a/src/test/test3.sail
+++ b/src/test/test3.sail
@@ -4,10 +4,16 @@ register nat dummy_reg
    memory-writing functions are figured out syntactically. *)
 val  nat -> nat effect { wmem , rmem }  MEM
 val  nat -> nat effect { wmem , rmem }  MEM_GPU
-val ( nat * nat ) -> nat effect { wmem , rmem }  MEM_SIZE
+val ( nat * nat ) -> (bit[8]) effect { wmem , rmem }  MEM_SIZE
 
 val  nat -> (bit[8]) effect { wmem , rmem }  MEM_WORD
 
+(* XXX types are wrong *)
+val extern forall Type 'a . 'a -> nat effect pure to_num_inc = "to_num_inc"
+val extern forall Type 'a . 'a -> nat effect pure to_num_dec = "to_num_dec"
+val extern forall Type 'a . nat -> 'a effect pure to_vec_inc = "to_vec_inc"
+val extern forall Type 'a . nat -> 'a effect pure to_vec_dec = "to_vec_dec"
+
 function unit ignore(x) = ()
 
 (* extern functions *)
@@ -43,8 +49,10 @@ function nat main _ = {
   ignore(MEM(1));
   MEM_GPU(0) := 3;
   ignore(MEM_GPU(0));
-  MEM_SIZE(0,1) := 4;
+  MEM_SIZE(0,1) := 0b11110000;
   ignore(MEM_SIZE(0,1));
+  MEM_SIZE(0,2) := 0b1111000010100000;
+  ignore(MEM_SIZE(0,2));
 
   (* extern calls *)
   ignore(3 + 39);