diff options
| -rw-r--r-- | src/lem_interp/run_interp.ml | 10 | ||||
| -rw-r--r-- | src/test/test3.sail | 11 |
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); |