Added definition of PLoadRRR and PStoreRRR - no Asmblockgen generation yet

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