diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/lem_interp/interp.lem | 22 | ||||
| -rw-r--r-- | src/lem_interp/run_interp.ml | 20 | ||||
| -rw-r--r-- | src/test/power.sail | 12 |
3 files changed, 28 insertions, 26 deletions
diff --git a/src/lem_interp/interp.lem b/src/lem_interp/interp.lem index a57c71a4..854ed202 100644 --- a/src/lem_interp/interp.lem +++ b/src/lem_interp/interp.lem @@ -282,27 +282,19 @@ let access_vector v n = else list_nth vs (m - n) end -val from_n_to_n :forall 'a. natural -> natural -> natural -> list 'a -> list 'a -let rec from_n_to_n from to_ acc ls = - match ls with - | [] -> [] - | l::ls -> - if from > acc - then from_n_to_n from to_ acc ls - else if from = to_ - then [l] - else l::(from_n_to_n from to_ acc ls) -end - -(*Needs debugging*) +val from_n_to_n :forall 'a. natural -> natural -> list 'a -> list 'a +let from_n_to_n from to_ ls = + let from = natFromNatural from in + let to_ = natFromNatural to_ in + take (to_ - from + 1) (drop from ls) val slice_vector : value -> natural -> natural -> value let slice_vector v n1 n2 = match v with | V_vector m inc vs -> if inc - then V_vector n1 inc (from_n_to_n (n1 - m) (n2 - m) 0 vs) - else V_vector n1 inc (from_n_to_n (m - n1) (m - n2) 0 vs) + then V_vector n1 inc (from_n_to_n (n1 - m) (n2 - m) vs) + else V_vector n1 inc (from_n_to_n (m - n1) (m - n2) vs) end val update_field_list : list (id * value) -> list (id * value) -> list (id * value) diff --git a/src/lem_interp/run_interp.ml b/src/lem_interp/run_interp.ml index 3a0219d6..19c27b56 100644 --- a/src/lem_interp/run_interp.ml +++ b/src/lem_interp/run_interp.ml @@ -109,6 +109,14 @@ module Mem = struct | 0 -> compare_big_int v1 v2 | n -> n end) + (* debugging memory accesses *) + let add (n, idx) v m = + eprintf "%s[%s] <- %s\n" (id_to_string n) (string_of_big_int idx) (val_to_string v); + add (n, idx) v m + let find (n, idx) m = + let v = find (n, idx) m in + eprintf "%s[%s] -> %s\n" (id_to_string n) (string_of_big_int idx) (val_to_string v); + v end ;; let slice v = function @@ -135,7 +143,7 @@ let perform_action ((reg, mem) as env) = function | Write_mem (id, V_lit(L_aux(L_num n,_)), None, value) -> V_lit (L_aux(L_unit, Interp_ast.Unknown)), (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 *) + (* XXX this doesn't deal with endianess at all *) | 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 @@ -146,14 +154,16 @@ let perform_action ((reg, mem) as env) = function (* 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_aux(L_num n,_)); V_lit(L_aux(L_num size,_))], None, value) -> + | Write_mem (id, V_tuple [V_lit(L_aux(L_num n,_)); V_lit(L_aux(L_num size,_))], None, V_vector (m, inc, vs)) -> + (* normalize input vector so that it is indexed from 0 - for slices *) + let value = V_vector (zero_big_int, inc, vs) in (* 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 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 update (succ_big_int k) mem' in V_lit (L_aux(L_unit, Interp_ast.Unknown)), (reg, update zero_big_int mem) diff --git a/src/test/power.sail b/src/test/power.sail index 9c07a39f..7e78f2cd 100644 --- a/src/test/power.sail +++ b/src/test/power.sail @@ -17,13 +17,13 @@ val extern bit -> bool effect pure is_one = "is_one" (* XXX sign extension *) function forall Type 'a . 'a exts ( x ) = x -register (bit[32]) NIA (* next instruction address *) -register (bit[32]) CIA (* current instruction address *) +register (bit[64]) NIA (* next instruction address *) +register (bit[64]) CIA (* current instruction address *) -(* XXX check me *) -register (bit[32]) CR -register (bit[32]) CTR -register (bit[32]) LR +(* XXX endianess; also, bit[64] translates to 0:64, not 0:63??? *) +register (bit[32 : 63]) CR +register (bit[64]) CTR +register (bit[64]) LR register bool mode64bit |