diff options
Diffstat (limited to 'mppa_k1c/Asmblock.v')
-rw-r--r-- | mppa_k1c/Asmblock.v | 52 |
1 files changed, 38 insertions, 14 deletions
diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v index b4cf57ae..3656b91f 100644 --- a/mppa_k1c/Asmblock.v +++ b/mppa_k1c/Asmblock.v @@ -259,9 +259,11 @@ Inductive load_name_rro : Type := Inductive ld_instruction : Type := | PLoadRRO (i: load_name_rro) (rd: ireg) (ra: ireg) (ofs: offset) + | PLoadRRR (i: load_name_rro) (rd: ireg) (ra: ireg) (rofs: ireg) . Coercion PLoadRRO: load_name_rro >-> Funclass. +Coercion PLoadRRR: load_name_rro >-> Funclass. (** Stores **) Inductive store_name_rro : Type := @@ -277,9 +279,11 @@ Inductive store_name_rro : Type := Inductive st_instruction : Type := | PStoreRRO (i: store_name_rro) (rs: ireg) (ra: ireg) (ofs: offset) + | PStoreRRR (i: store_name_rro) (rs: ireg) (ra: ireg) (rofs: ireg) . Coercion PStoreRRO: store_name_rro >-> Funclass. +Coercion PStoreRRR: store_name_rro >-> Funclass. (** Arithmetic instructions **) Inductive arith_name_r : Type := @@ -1259,24 +1263,42 @@ Definition eval_offset (ofs: offset) : res ptrofs := end. Definition exec_load (chunk: memory_chunk) (rs: regset) (m: mem) - (d: ireg) (a: ireg) (ofs: offset) := + (d: ireg) (a: ireg) (ptr: ptrofs) := + match Mem.loadv chunk m (Val.offset_ptr (rs a) ptr) with + | None => Stuck + | Some v => Next (rs#d <- v) m + end +. + +Definition exec_load_offset (chunk: memory_chunk) (rs: regset) (m: mem) (d a: ireg) (ofs: offset) := match (eval_offset ofs) with - | OK ptr => - match Mem.loadv chunk m (Val.offset_ptr (rs a) ptr) with - | None => Stuck - | Some v => Next (rs#d <- v) m - end + | OK ptr => exec_load chunk rs m d a ptr + | _ => Stuck + end. + +Definition exec_load_reg (chunk: memory_chunk) (rs: regset) (m: mem) (d a ro: ireg) := + match (rs ro) with + | Vptr _ ofs => exec_load chunk rs m d a ofs | _ => Stuck end. Definition exec_store (chunk: memory_chunk) (rs: regset) (m: mem) - (s: ireg) (a: ireg) (ofs: offset) := + (s: ireg) (a: ireg) (ptr: ptrofs) := + match Mem.storev chunk m (Val.offset_ptr (rs a) ptr) (rs s) with + | None => Stuck + | Some m' => Next rs m' + end +. + +Definition exec_store_offset (chunk: memory_chunk) (rs: regset) (m: mem) (s a: ireg) (ofs: offset) := match (eval_offset ofs) with - | OK ptr => - match Mem.storev chunk m (Val.offset_ptr (rs a) ptr) (rs s) with - | None => Stuck - | Some m' => Next rs m' - end + | OK ptr => exec_store chunk rs m s a ptr + | _ => Stuck + end. + +Definition exec_store_reg (chunk: memory_chunk) (rs: regset) (m: mem) (s a ro: ireg) := + match (rs ro) with + | Vptr _ ofs => exec_store chunk rs m s a ofs | _ => Stuck end. @@ -1312,9 +1334,11 @@ Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome := match bi with | PArith ai => Next (exec_arith_instr ai rs) m - | PLoadRRO n d a ofs => exec_load (load_chunk n) rs m d a ofs + | PLoadRRO n d a ofs => exec_load_offset (load_chunk n) rs m d a ofs + | PLoadRRR n d a ro => exec_load_reg (load_chunk n) rs m d a ro - | PStoreRRO n s a ofs => exec_store (store_chunk n) rs m s a ofs + | PStoreRRO n s a ofs => exec_store_offset (store_chunk n) rs m s a ofs + | PStoreRRR n s a ro => exec_store_reg (store_chunk n) rs m s a ro | Pallocframe sz pos => let (m1, stk) := Mem.alloc m 0 sz in |