Write slice to memory

I'm not sure whether this is useful at all. It is currently a bit
broken when subrange is not in the "correct" order. Presumably the
typechecker should catch this? I'm not quite sure what the intended
semantics should be. Probably the same bug occurs with register slices
too.

2 files changed, 20 insertions, 1 deletions

diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml
index 6ded3294..f0e45646 100644
--- a/src/lem_interp/run_interp.ml
+++ b/src/lem_interp/run_interp.ml
@@ -109,8 +109,16 @@ 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)
+ (* 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 -
+      * should the typechecker do that coercion for us automatically? *)
+     let value = if eq_big_int start stop then V_vector (zero_big_int, true, [value]) else value in
+     let old_val = Mem.find (id, n) mem in
+     let new_val = fupdate_vector_slice old_val value start stop in
+     V_lit L_unit, (reg, Mem.add (id, n) new_val mem)
  | Call_extern (name, arg) -> eval_external name arg, env
- | _ -> failwith "partial write not implemented" (* XXX *)
+ | _ -> assert false
 ;;
 
 
diff --git a/src/test/test3.sail b/src/test/test3.sail
index 154ce5b6..e6bf4cdd 100644
--- a/src/test/test3.sail
+++ b/src/test/test3.sail
@@ -6,6 +6,8 @@ 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 -> (bit[8]) effect { wmem , rmem }  MEM_WORD
+
 function unit ignore(x) = ()
 
 (* extern functions *)
@@ -24,6 +26,15 @@ function nat main _ = {
   (* register read, thanks to register declaration *)
   ignore(dummy_reg);
 
+
+  MEM_WORD(0) := 0b10101010;
+  (MEM_WORD(0))[3..4] := 0b10;
+  (* XXX this one is broken - I don't what it should do,
+  or even if we should accept it, but the current result
+  is to eat up one bit, ending up with a 7-bit word. *)
+  (MEM_WORD(0))[4..3] := 0b10;
+  ignore(MEM_WORD(0));
+
   (* infix call *)
   ignore(7 * 9);