translate load.xs

1 files changed, 19 insertions, 1 deletions

diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index c2a0a315..7c8a08f6 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -846,6 +846,19 @@ Definition transl_memory_access2
   | _, _ => Error (msg "Asmblockgen.transl_memory_access2")
   end.
 
+Definition transl_memory_access2XS
+     (chunk: memory_chunk)
+     (mk_instr: ireg -> ireg -> basic)
+     (addr: addressing) (args: list mreg) (k: bcode) : res bcode :=
+  match addr, args with
+  | (Aindexed2XS scale), (a1 :: a2 :: nil) =>
+      assertion (Z.eqb (zscale_of_chunk chunk) scale);
+      do rs1 <- ireg_of a1;
+      do rs2 <- ireg_of a2;
+      OK (mk_instr rs1 rs2 ::i k)
+  | _, _ => Error (msg "Asmblockgen.transl_memory_access2XS")
+  end.
+
 Definition transl_memory_access
      (mk_instr: ireg -> offset -> basic)
      (addr: addressing) (args: list mreg) (k: bcode) : res bcode :=
@@ -885,10 +898,15 @@ Definition transl_load_rrr (chunk: memory_chunk) (addr: addressing)
   do r <- ireg_of dst;
   transl_memory_access2 (PLoadRRR (chunk2load chunk) r) addr args k.
 
+Definition transl_load_rrrXS (chunk: memory_chunk) (addr: addressing)
+           (args: list mreg) (dst: mreg) (k: bcode) : res bcode :=
+  do r <- ireg_of dst;
+  transl_memory_access2XS chunk (PLoadRRR (chunk2load chunk) r) addr args k.
+
 Definition transl_load (chunk: memory_chunk) (addr: addressing)
            (args: list mreg) (dst: mreg) (k: bcode) : res bcode :=
   match addr with
-  | Aindexed2XS _ => Error (msg "transl_load Aindexed2XS")
+  | Aindexed2XS _ => transl_load_rrrXS chunk addr args dst k
   | Aindexed2 => transl_load_rrr chunk addr args dst k
   | _ => transl_load_rro chunk addr args dst k
   end.