diff options
Diffstat (limited to 'src/lem_interp')
| -rw-r--r-- | src/lem_interp/interp.lem | 2 | ||||
| -rw-r--r-- | src/lem_interp/run_interp.ml | 33 |
2 files changed, 28 insertions, 7 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index 0a112962..e08e4053 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -73,6 +73,7 @@ type value = | V_ctor of id * t * value | V_unknown (* Distinct from undefined, used by memory system *) | V_register of reg_form (* Value to store register access, when not actively reading or writing *) + | V_register_alias of (alias_spec tannot) * tannot (* Same as above, but to a concatenation of two registers *) let rec id_value_eq (i, v) (i', v') = i = i' && value_eq v v' and value_eq left right = @@ -172,6 +173,7 @@ let rec to_registers (Defs defs) = | def::defs -> match def with | DEF_reg_dec (DEC_aux (DEC_reg typ id) (l,tannot)) -> (id, V_register(Reg id tannot)) :: (to_registers (Defs defs)) + | DEF_reg_dec (DEC_aux (DEC_alias id aspec) (l,tannot)) -> (id, V_register_alias aspec tannot) :: (to_registers (Defs defs)) | _ -> to_registers (Defs defs) end end diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml index 2f8c5e97..d449f53c 100644 --- a/src/lem_interp/run_interp.ml +++ b/src/lem_interp/run_interp.ml @@ -153,7 +153,7 @@ module Reg = struct (* eprintf "%s -> %s\n" (id_to_string id) (val_to_string v);*) v end ;; - +(* Old Mem, that used the id to map as well as the int... which seems wrong module Mem = struct include Map.Make(struct type t = (id * big_int) @@ -174,8 +174,27 @@ module Mem = struct *) let to_string (n, idx) v = sprintf "%s[%s] -> %s" (id_to_string n) (string_of_big_int idx) (val_to_string v) +end ;;*) + +module Mem = struct + include Map.Make(struct + type t = big_int + let compare v1 v2 = compare_big_int v1 v2 + end) + (* debugging memory accesses + let add idx v m = + eprintf "[%s] <- %s\n" (string_of_big_int idx) (val_to_string v); + add idx v m + let find idx m = + let v = find idx m in + eprintf "[%s] -> %s\n" (string_of_big_int idx) (val_to_string v); + v + *) + let to_string idx v = + sprintf "[%s] -> %s" (string_of_big_int idx) (val_to_string v) end ;; + let vconcat v v' = vec_concat (V_tuple [v; v']) ;; let slice v = function @@ -213,14 +232,14 @@ let rec perform_action ((reg, mem) as env) = function | BF_concat _ -> failwith "unimplemented: non-contiguous register write") (* memory *) | Read_mem (id, V_lit(L_aux((L_num n),_)), sub) -> - slice (Mem.find (id, n) mem) sub, env + slice (Mem.find n mem) sub, env | Write_mem (id, V_lit(L_aux(L_num n,_)), None, value) -> - unit_lit, (reg, Mem.add (id, n) value mem) + unit_lit, (reg, Mem.add n value mem) (* multi-byte accesses to memory *) | Read_mem (id, V_tuple [V_lit(L_aux(L_num n,_)); V_lit(L_aux(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 + let slice = Mem.find (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 @@ -235,14 +254,14 @@ let rec perform_action ((reg, mem) as env) = function let n1 = mult_int_big_int byte_size k in let n2 = sub_big_int (mult_int_big_int byte_size (succ_big_int k)) (big_int_of_int 1) in let slice = slice_vector value n1 n2 in - let mem' = Mem.add (id, add_big_int n k) slice mem in + let mem' = Mem.add (add_big_int n k) slice mem in update (succ_big_int k) mem' in unit_lit, (reg, update zero_big_int mem) (* This case probably never happens in the POWER spec anyway *) | Write_mem (id, V_lit(L_aux(L_num n,_)), Some (start, stop), (V_vector _ as value)) -> - let old_val = Mem.find (id, n) mem in + let old_val = Mem.find n mem in let new_val = fupdate_vector_slice old_val value start stop in - unit_lit, (reg, Mem.add (id, n) new_val mem) + unit_lit, (reg, Mem.add n new_val mem) (* special case for slices of size 1: wrap value in a vector *) | Write_reg ((Reg (_, _) as r), (Some (start, stop) as slice), value) when eq_big_int start stop -> perform_action env (Write_reg (r, slice, V_vector(zero_big_int, true, [value]))) |