4 files changed, 30 insertions, 7 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.
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index c6c88681..e710b5a4 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -521,7 +521,7 @@ Proof.
     unfold transl_cond_float32. exploreInst; try discriminate.
     unfold transl_cond_notfloat32. exploreInst; try discriminate.
   - simpl in TIB. unfold transl_load in TIB. exploreInst; try discriminate.
-    all: monadInv TIB; unfold transl_memory_access in EQ0; unfold transl_memory_access2 in EQ0; exploreInst; try discriminate.
+    all: monadInv TIB; unfold transl_memory_access in EQ0; unfold transl_memory_access2 in EQ0; unfold transl_memory_access2XS in EQ0; exploreInst; try discriminate.
   - simpl in TIB. unfold transl_store in TIB. exploreInst; try discriminate.
     all: monadInv TIB; unfold transl_memory_access in EQ0; unfold transl_memory_access2 in EQ0; exploreInst; try discriminate.
 Qed.
diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index 0cb2d83d..5e44b7a5 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -2168,7 +2168,12 @@ Lemma transl_load_memory_access_ok:
 Proof.
   intros until m. intros ADDR TR ? ?.
   unfold transl_load in TR. destruct addr; try contradiction.
-  - (* Indexed2XS*) monadInv TR.
+  - monadInv TR.
+    destruct chunk;
+    simpl in EQ0;
+    ArgsInv;
+    try discriminate;
+    econstructor; (esplit; eauto).
   - monadInv TR. destruct chunk; ArgsInv; econstructor; (esplit; eauto).
   - monadInv TR. destruct chunk. all: ArgsInv; destruct args; try discriminate; monadInv EQ0; eexists; eexists; split; try split;
     [ instantiate (1 := (PLoadRRO _ x)); simpl; reflexivity
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index d7311272..7a5adf5e 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -1124,9 +1124,8 @@ Definition parexec_load_reg (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem)
   | Some v => Next (rsw#d <- v) mw
   end.
 
-Definition scale_of_chunk (chunk: memory_chunk) :=
-  Vint (Int.repr
-  (match chunk with
+Definition zscale_of_chunk (chunk: memory_chunk) :=
+  match chunk with
   | Mint8signed => 0
   | Mint8unsigned => 0
   | Mint16signed => 1
@@ -1137,7 +1136,8 @@ Definition scale_of_chunk (chunk: memory_chunk) :=
   | Mfloat64 => 3
   | Many32 => 2
   | Many64 => 3
-  end)).
+  end.
+Definition scale_of_chunk chunk := Vint (Int.repr (zscale_of_chunk chunk)).
 
 Definition parexec_load_regxs (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a ro: ireg) :=
   match Mem.loadv chunk mr (Val.addl (rsr a) (Val.shll (rsr ro) (scale_of_chunk chunk))) with