it compiles

10 files changed, 164 insertions, 33 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 0e217d36..d73d00c7 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -475,6 +475,15 @@ Definition basic_to_instruction (b: basic) :=
   | PStoreRRR Asmvliw.Pfss rd ra ro => Pfss rd ra (AReg ro)

   | PStoreRRR Asmvliw.Pfsd rd ra ro => Pfsd rd ra (AReg ro)

 

+  | PStoreRRRXS Asmvliw.Psb rd ra ro  => Psb rd ra (ARegXS ro)

+  | PStoreRRRXS Asmvliw.Psh rd ra ro => Psh rd ra (ARegXS ro)

+  | PStoreRRRXS Asmvliw.Psw rd ra ro => Psw rd ra (ARegXS ro)

+  | PStoreRRRXS Asmvliw.Psw_a rd ra ro => Psw_a rd ra (ARegXS ro)

+  | PStoreRRRXS Asmvliw.Psd rd ra ro => Psd rd ra (ARegXS ro)

+  | PStoreRRRXS Asmvliw.Psd_a rd ra ro => Psd_a rd ra (ARegXS ro)

+  | PStoreRRRXS Asmvliw.Pfss rd ra ro => Pfss rd ra (ARegXS ro)

+  | PStoreRRRXS Asmvliw.Pfsd rd ra ro => Pfsd rd ra (ARegXS ro)

+

   end.

 

 Section RELSEM.

diff --git a/mppa_k1c/Asmblock.v b/mppa_k1c/Asmblock.v
index 3aec4e11..1988813f 100644
--- a/mppa_k1c/Asmblock.v
+++ b/mppa_k1c/Asmblock.v
@@ -274,6 +274,8 @@ Definition exec_store_offset (chunk: memory_chunk) (rs: regset) (m: mem) (s a: i
 
 Definition exec_store_reg (chunk: memory_chunk) (rs: regset) (m: mem) (s a ro: ireg) := parexec_store_reg chunk rs rs m m s a ro.
 
+Definition exec_store_regxs (chunk: memory_chunk) (rs: regset) (m: mem) (s a ro: ireg) := parexec_store_regxs chunk rs rs m m s a ro.
+
 (** * basic instructions *)
 
 Definition exec_basic_instr (bi: basic) (rs: regset) (m: mem) : outcome := parexec_basic_instr ge bi rs rs m m.
diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 32a5fa04..f6573838 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -83,6 +83,7 @@ Coercion OLoadRRO: load_name >-> Funclass.
 Inductive store_op :=
   | OStoreRRO (n: store_name) (ofs: offset)
   | OStoreRRR (n: store_name)
+  | OStoreRRRXS (n: store_name)
 .
 
 Coercion OStoreRRO: store_name >-> Funclass.
@@ -177,10 +178,17 @@ Definition exec_store_deps_reg (chunk: memory_chunk) (m: mem) (vs va vo: val) :=
   | Some m' => Some (Memstate m')
   end.
 
+Definition exec_store_deps_regxs (chunk: memory_chunk) (m: mem) (vs va vo: val) :=
+  match Mem.storev chunk m (Val.addl va (Val.shll vo (scale_of_chunk chunk))) vs with
+  | None => None
+  | Some m' => Some (Memstate m')
+  end.
+
 Definition store_eval (so: store_op) (l: list value) :=
   match so, l with
   | OStoreRRO n ofs, [Val vs; Val va; Memstate m] => exec_store_deps_offset (store_chunk n) m vs va ofs
   | OStoreRRR n, [Val vs; Val va; Val vo; Memstate m] => exec_store_deps_reg (store_chunk n) m vs va vo
+  | OStoreRRRXS n, [Val vs; Val va; Val vo; Memstate m] => exec_store_deps_regxs (store_chunk n) m vs va vo
   | _, _ => None
   end.
 
@@ -385,6 +393,8 @@ Definition store_op_eq (o1 o2: store_op): ?? bool :=
      match o2 with OStoreRRO n2 ofs2 => iandb (phys_eq n1 n2) (phys_eq ofs1 ofs2) | _ => RET false end
   | OStoreRRR n1 =>
      match o2 with OStoreRRR n2 => phys_eq n1 n2 | _ => RET false end
+  | OStoreRRRXS n1 =>
+     match o2 with OStoreRRRXS n2 => phys_eq n1 n2 | _ => RET false end
   end.
 
 Lemma store_op_eq_correct o1 o2:
@@ -393,6 +403,7 @@ Proof.
   destruct o1, o2; wlp_simplify; try discriminate.
   - congruence.
   - congruence.
+  - congruence.
 Qed.
 Hint Resolve store_op_eq_correct: wlp.
 Opaque store_op_eq_correct.
@@ -626,6 +637,7 @@ Definition trans_basic (b: basic) : inst :=
   | PLoadRRRXS n d a ro =>  [(#d, Op (Load (OLoadRRRXS n)) (PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))]
   | PStoreRRO n s a ofs => [(pmem, Op (Store (OStoreRRO n ofs)) (PReg (#s) @ PReg (#a) @ PReg pmem @ Enil))]
   | PStoreRRR n s a ro => [(pmem, Op (Store (OStoreRRR n)) (PReg (#s) @ PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))]
+  | PStoreRRRXS n s a ro => [(pmem, Op (Store (OStoreRRRXS n)) (PReg (#s) @ PReg (#a) @ PReg (#ro) @ PReg pmem @ Enil))]
   | Pallocframe sz pos => [(#FP, PReg (#SP)); (#SP, Op (Allocframe2 sz pos) (PReg (#SP) @ PReg pmem @ Enil)); (#RTMP, Op (Constant Vundef) Enil);
                            (pmem, Op (Allocframe sz pos) (Old (PReg (#SP)) @ PReg pmem @ Enil))]
   | Pfreeframe sz pos => [(pmem, Op (Freeframe sz pos) (PReg (#SP) @ PReg pmem @ Enil));
@@ -864,6 +876,13 @@ Proof.
       eexists; split; try split; Simpl;
       intros rr; destruct rr; Simpl.
 
+    (* Store Reg XS *)
+    + destruct i; simpl store_chunk. all:
+      unfold parexec_store_regxs; simpl; unfold exec_store_deps_regxs; rewrite H, H0; rewrite (H0 ra); rewrite (H0 rofs);
+      destruct (Mem.storev _ _ _ _) eqn:MEML; simpl; auto;
+      eexists; split; try split; Simpl;
+      intros rr; destruct rr; Simpl.
+
 (* Allocframe *)
   - destruct (Mem.alloc _ _ _) eqn:MEMAL. destruct (Mem.store _ _ _ _) eqn:MEMS.
     * eexists; repeat split.
@@ -1446,6 +1465,7 @@ Definition string_of_store (op: store_op) : pstring :=
   match op with
   | OStoreRRO n _ => string_of_store_name n
   | OStoreRRR n => string_of_store_name n
+  | OStoreRRRXS n => string_of_store_name n
   end.
 
 Definition string_of_control (op: control_op) : pstring :=
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index a74aa9f6..ea99c098 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -807,31 +807,31 @@ end.
 
 Definition loadind (base: ireg) (ofs: ptrofs) (ty: typ) (dst: mreg) (k: bcode) :=
   match ty, preg_of dst with
-  | Tint,    IR rd => OK (indexed_memory_access (Plw rd) base ofs ::i k)
-  | Tlong,   IR rd => OK (indexed_memory_access (Pld rd) base ofs ::i k)
-  | Tsingle, IR rd => OK (indexed_memory_access (Pfls rd) base ofs ::i k)
-  | Tfloat,  IR rd => OK (indexed_memory_access (Pfld rd) base ofs ::i k)
-  | Tany32,  IR rd => OK (indexed_memory_access (Plw_a rd) base ofs ::i k)
-  | Tany64,  IR rd => OK (indexed_memory_access (Pld_a rd) base ofs ::i k)
+  | Tint,    IR rd => OK (indexed_memory_access (PLoadRRO Plw rd) base ofs ::i k)
+  | Tlong,   IR rd => OK (indexed_memory_access (PLoadRRO Pld rd) base ofs ::i k)
+  | Tsingle, IR rd => OK (indexed_memory_access (PLoadRRO Pfls rd) base ofs ::i k)
+  | Tfloat,  IR rd => OK (indexed_memory_access (PLoadRRO Pfld rd) base ofs ::i k)
+  | Tany32,  IR rd => OK (indexed_memory_access (PLoadRRO Plw_a rd) base ofs ::i k)
+  | Tany64,  IR rd => OK (indexed_memory_access (PLoadRRO Pld_a rd) base ofs ::i k)
   | _, _           => Error (msg "Asmblockgen.loadind")
   end.
 
 Definition storeind (src: mreg) (base: ireg) (ofs: ptrofs) (ty: typ) (k: bcode) :=
   match ty, preg_of src with
-  | Tint,    IR rd => OK (indexed_memory_access (Psw rd) base ofs ::i k)
-  | Tlong,   IR rd => OK (indexed_memory_access (Psd rd) base ofs ::i k)
-  | Tsingle, IR rd => OK (indexed_memory_access (Pfss rd) base ofs ::i k)
-  | Tfloat,  IR rd => OK (indexed_memory_access (Pfsd rd) base ofs ::i k)
-  | Tany32,  IR rd => OK (indexed_memory_access (Psw_a rd) base ofs ::i k)
-  | Tany64,  IR rd => OK (indexed_memory_access (Psd_a rd) base ofs ::i k)
+  | Tint,    IR rd => OK (indexed_memory_access (PStoreRRO Psw rd) base ofs ::i k)
+  | Tlong,   IR rd => OK (indexed_memory_access (PStoreRRO Psd rd) base ofs ::i k)
+  | Tsingle, IR rd => OK (indexed_memory_access (PStoreRRO Pfss rd) base ofs ::i k)
+  | Tfloat,  IR rd => OK (indexed_memory_access (PStoreRRO Pfsd rd) base ofs ::i k)
+  | Tany32,  IR rd => OK (indexed_memory_access (PStoreRRO Psw_a rd) base ofs ::i k)
+  | Tany64,  IR rd => OK (indexed_memory_access (PStoreRRO Psd_a rd) base ofs ::i k)
   | _, _           => Error (msg "Asmblockgen.storeind")
   end.
 
 Definition loadind_ptr (base: ireg) (ofs: ptrofs) (dst: ireg) :=
-  indexed_memory_access (Pld dst) base ofs.
+  indexed_memory_access (PLoadRRO Pld dst) base ofs.
 
 Definition storeind_ptr (src: ireg) (base: ireg) (ofs: ptrofs) :=
-  indexed_memory_access (Psd src) base ofs.
+  indexed_memory_access (PStoreRRO Psd src) base ofs.
 
 (** Translation of memory accesses: loads, and stores. *)
 
@@ -901,7 +901,7 @@ Definition transl_load_rrr (chunk: memory_chunk) (addr: addressing)
 Definition transl_load_rrrXS (chunk: memory_chunk) (scale : Z)
            (args: list mreg) (dst: mreg) (k: bcode) : res bcode :=
   do r <- ireg_of dst;
-  transl_memory_access2XS chunk (PLoadRRR (chunk2load chunk) r) scale args k.
+  transl_memory_access2XS chunk (PLoadRRRXS (chunk2load chunk) r) scale args k.
 
 Definition transl_load (chunk: memory_chunk) (addr: addressing)
            (args: list mreg) (dst: mreg) (k: bcode) : res bcode :=
@@ -933,10 +933,16 @@ Definition transl_store_rrr (chunk: memory_chunk) (addr: addressing)
   do r <- ireg_of src;
   transl_memory_access2 (PStoreRRR (chunk2store chunk) r) addr args k.
 
+Definition transl_store_rrrxs (chunk: memory_chunk) (scale: Z)
+           (args: list mreg) (src: mreg) (k: bcode) : res bcode :=
+  do r <- ireg_of src;
+  transl_memory_access2XS chunk (PStoreRRRXS (chunk2store chunk) r) scale args k.
+
 Definition transl_store (chunk: memory_chunk) (addr: addressing)
            (args: list mreg) (src: mreg) (k: bcode) : res bcode :=
   match addr with
   | Aindexed2 => transl_store_rrr chunk addr args src k
+  | Aindexed2XS scale => transl_store_rrrxs chunk scale args src k
   | _ => transl_store_rro chunk addr args src k
   end.
 
diff --git a/mppa_k1c/Asmblockgenproof.v b/mppa_k1c/Asmblockgenproof.v
index e710b5a4..0233a3dc 100644
--- a/mppa_k1c/Asmblockgenproof.v
+++ b/mppa_k1c/Asmblockgenproof.v
@@ -523,7 +523,7 @@ Proof.
   - 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; 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.

+    all: monadInv TIB; unfold transl_memory_access in EQ0; unfold transl_memory_access2 in EQ0; unfold transl_memory_access2XS in EQ0; exploreInst; try discriminate. 

 Qed.

 

 Lemma transl_basic_code_nonil:

diff --git a/mppa_k1c/Asmblockgenproof1.v b/mppa_k1c/Asmblockgenproof1.v
index c9d72c4d..82f3b0fc 100644
--- a/mppa_k1c/Asmblockgenproof1.v
+++ b/mppa_k1c/Asmblockgenproof1.v
@@ -2254,15 +2254,15 @@ Lemma transl_load_memory_access2XS_ok:
       args = mr0 :: mro :: nil
    /\ preg_of dst = IR rd
    /\ preg_of mro = IR ro
-   /\ transl_memory_access2XS chunk mk_instr (Aindexed2XS scale) args k = OK c
+   /\ transl_memory_access2XS chunk mk_instr scale args k = OK c
    /\ forall base rs,
-      exec_basic_instr ge (mk_instr base ro) rs m = exec_load_reg chunk rs m rd base ro.
+      exec_basic_instr ge (mk_instr base ro) rs m = exec_load_regxs chunk rs m rd base ro.
 Proof.
   intros until m. intros TR ? ?.
   unfold transl_load in TR. subst. monadInv TR. destruct chunk. all:
   unfold transl_memory_access2XS in EQ0; repeat (destruct args; try discriminate); monadInv EQ0; ArgsInv; repeat eexists;
   [ unfold ireg_of in EQ0; destruct (preg_of m1); eauto; try discriminate; monadInv EQ0; reflexivity
-  | rewrite EQ1; rewrite EQ0; simpl; instantiate (1 := (PLoadRRR _ x)); simpl; rewrite Heqb; reflexivity
+  | rewrite EQ1; rewrite EQ0; simpl; instantiate (1 := (PLoadRRRXS _ x)); simpl; rewrite Heqb; eauto
   | eauto].
 Qed.
 
@@ -2316,6 +2316,33 @@ Proof.
   auto.
 Qed.
 
+Lemma transl_store_access2XS_correct:
+  forall chunk (mk_instr: ireg -> ireg -> basic) scale args k c r1 (rs: regset) m v mr1 mro ro m',
+  args = mr1 :: mro :: nil ->
+  ireg_of mro = OK ro ->
+  (forall base rs,
+     exec_basic_instr ge (mk_instr base ro) rs m = exec_store_regxs chunk rs m r1 base ro) ->
+  transl_memory_access2XS chunk mk_instr scale args k = OK c ->
+  eval_addressing ge rs#SP (Aindexed2XS scale) (map rs (map preg_of args)) = Some v ->
+  Mem.storev chunk m v rs#r1 = Some m' ->
+  r1 <> RTMP ->
+  exists rs',
+     exec_straight ge (basics_to_code c) rs m (basics_to_code k) rs' m'
+  /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
+Proof.
+  intros until m'; intros ARGS IREG INSTR TR EV STORE NOT31. 
+  exploit transl_memory_access2XS_correct; eauto.
+  intros (base & ro2 & mr2 & mro2 & rs' & ARGSS & IREGG & A & B & C & D). rewrite ARGSS in ARGS. inversion ARGS. subst mro2 mr2. clear ARGS.
+  econstructor; split.
+  eapply exec_straight_opt_right. eexact A. apply exec_straight_one. assert (ro = ro2) by congruence. subst ro2.
+  rewrite INSTR. unfold exec_store_regxs. unfold parexec_store_regxs.
+  unfold scale_of_chunk.
+  subst scale.
+  rewrite B. rewrite C; try discriminate. rewrite STORE. auto.
+  intro. inv H. contradiction.
+  auto.
+Qed.
+
 Lemma transl_store_access_correct:
   forall chunk (mk_instr: ireg -> offset -> basic) addr args k c r1 (rs: regset) m v m',
   (forall base ofs rs,
@@ -2355,7 +2382,7 @@ Qed.
 
 Lemma transl_store_memory_access_ok:
   forall addr chunk args src k c rs a m m',
-  addr <> Aindexed2 ->
+  (match addr with Aindexed2XS _ | Aindexed2 => False | _ => True end) ->
   transl_store chunk addr args src k = OK c ->
   eval_addressing ge (rs (IR SP)) addr (map rs (map preg_of args)) = Some a ->
   Mem.storev chunk m a (rs (preg_of src)) = Some m' ->
@@ -2368,7 +2395,6 @@ Lemma transl_store_memory_access_ok:
 Proof.
   intros until m'. intros ? TR ? ?.
   unfold transl_store in TR. destruct addr; try contradiction.
-  - (* Aindex2XS *) discriminate.
   - monadInv TR. destruct chunk. all:
     ArgsInv; eexists; eexists; eexists; split; try split; [
       repeat (destruct args; try discriminate); eassumption
@@ -2403,6 +2429,20 @@ Proof.
   erewrite <- Mem.store_signed_unsigned_16. reflexivity.
 Qed.
 
+Remark exec_store_regxs_8_sign rs m x base ofs:
+  exec_store_regxs Mint8unsigned rs m x base ofs = exec_store_regxs Mint8signed rs m x base ofs.
+Proof.
+  unfold exec_store_regxs. unfold parexec_store_regxs. unfold Mem.storev. destruct (Val.addl _ _); auto.
+  erewrite <- Mem.store_signed_unsigned_8. reflexivity.
+Qed.
+
+Remark exec_store_regxs_16_sign rs m x base ofs:
+  exec_store_regxs Mint16unsigned rs m x base ofs = exec_store_regxs Mint16signed rs m x base ofs.
+Proof.
+  unfold exec_store_regxs. unfold parexec_store_regxs. unfold Mem.storev. destruct (Val.addl _ _); auto.
+  erewrite <- Mem.store_signed_unsigned_16. reflexivity.
+Qed.
+
 Lemma transl_store_memory_access2_ok:
   forall addr chunk args src k c rs a m m',
   addr = Aindexed2 ->
@@ -2428,6 +2468,30 @@ Proof.
   - simpl. intros. eapply exec_store_reg_16_sign.
 Qed.
 
+Lemma transl_store_memory_access2XS_ok:
+  forall scale chunk args src k c rs a m m',
+  transl_store chunk (Aindexed2XS scale) args src k = OK c ->
+  eval_addressing ge (rs (IR SP)) (Aindexed2XS scale) (map rs (map preg_of args)) = Some a ->
+  Mem.storev chunk m a (rs (preg_of src)) = Some m' ->
+  exists mk_instr chunk' rr mr0 mro ro,
+     args = mr0 :: mro :: nil
+  /\ preg_of mro = IR ro
+  /\ preg_of src = IR rr
+  /\ transl_memory_access2XS chunk' mk_instr scale args k = OK c
+  /\ (forall base rs,
+       exec_basic_instr ge (mk_instr base ro) rs m = exec_store_regxs chunk' rs m rr base ro)
+  /\ Mem.storev chunk m a rs#(preg_of src) = Mem.storev chunk' m a rs#(preg_of src).
+Proof.
+  intros until m'. intros TR ? ?.
+  unfold transl_store in TR. monadInv TR. destruct chunk. all:
+  unfold transl_memory_access2XS in EQ0; repeat (destruct args; try discriminate); monadInv EQ0; ArgsInv; repeat eexists;
+  [ ArgsInv; reflexivity
+  | rewrite EQ1; rewrite EQ0; instantiate (1 := (PStoreRRRXS _ x)); simpl; rewrite Heqb; eauto
+  | eauto ].
+  - simpl. intros. eapply exec_store_regxs_8_sign.
+  - simpl. intros. eapply exec_store_regxs_16_sign.
+Qed.
+
 Lemma transl_store_correct:
   forall chunk addr args src k c (rs: regset) m a m',
   transl_store chunk addr args src k = OK c ->
@@ -2438,15 +2502,30 @@ Lemma transl_store_correct:
   /\ forall r, r <> PC -> r <> RTMP -> rs'#r = rs#r.
 Proof.
   intros until m'; intros TR EV STORE. destruct addr.
-  1: (* AIndexed2XS *) discriminate.
-  2-4: exploit transl_store_memory_access_ok; eauto; try discriminate; intro A;
+  - exploit transl_store_memory_access2XS_ok; eauto. intros (mk_instr & chunk' & rr & mr0 & mro & ro & argsEq & roEq & srcEq & A & B & C).
+    eapply transl_store_access2XS_correct; eauto with asmgen. unfold ireg_of. rewrite roEq. reflexivity. congruence.
+    destruct rr; try discriminate. destruct src; simpl in srcEq; try discriminate.
+  - exploit transl_store_memory_access2_ok; eauto. intros (mk_instr & chunk' & rr & mr0 & mro & ro & argsEq & roEq & srcEq & A & B & C).
+    eapply transl_store_access2_correct; eauto with asmgen. unfold ireg_of. rewrite roEq. reflexivity. congruence.
+    destruct rr; try discriminate. destruct src; simpl in srcEq; try discriminate.
+  - exploit transl_store_memory_access_ok; eauto; try discriminate; try (simpl; reflexivity).
+    intro A;
+    destruct A as (mk_instr & chunk' & rr & rrEq & B & C & D);
+    rewrite D in STORE; clear D; 
+    eapply transl_store_access_correct; eauto with asmgen; try congruence;
+    destruct rr; try discriminate; destruct src; try discriminate.
+  - exploit transl_store_memory_access_ok; eauto; try discriminate; try (simpl; reflexivity).
+    intro A;
+    destruct A as (mk_instr & chunk' & rr & rrEq & B & C & D);
+    rewrite D in STORE; clear D; 
+    eapply transl_store_access_correct; eauto with asmgen; try congruence;
+    destruct rr; try discriminate; destruct src; try discriminate.
+  - exploit transl_store_memory_access_ok; eauto; try discriminate; try (simpl; reflexivity).
+    intro A;
     destruct A as (mk_instr & chunk' & rr & rrEq & B & C & D);
     rewrite D in STORE; clear D; 
     eapply transl_store_access_correct; eauto with asmgen; try congruence;
     destruct rr; try discriminate; destruct src; try discriminate.
-  - exploit transl_store_memory_access2_ok; eauto. intros (mk_instr & chunk' & rr & mr0 & mro & ro & argsEq & roEq & srcEq & A & B & C).
-    eapply transl_store_access2_correct; eauto with asmgen. unfold ireg_of. rewrite roEq. reflexivity. congruence.
-    destruct rr; try discriminate. destruct src; simpl in srcEq; try discriminate.
 Qed.
 
 Lemma make_epilogue_correct:
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index 7a5adf5e..629d1449 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -273,9 +273,6 @@ Inductive ld_instruction : Type :=
   | PLoadRRRXS (i: load_name) (rd: ireg) (ra: ireg) (rofs: ireg)
 .
 
-Coercion PLoadRRO:       load_name        >-> Funclass.
-Coercion PLoadRRR:       load_name        >-> Funclass.
-
 (** Stores **)
 Inductive store_name : Type :=
   | Psb                                             (**r store byte *)
@@ -291,11 +288,9 @@ Inductive store_name : Type :=
 Inductive st_instruction : Type :=
   | PStoreRRO  (i: store_name) (rs: ireg) (ra: ireg) (ofs: offset)
   | PStoreRRR  (i: store_name) (rs: ireg) (ra: ireg) (rofs: ireg)
+  | PStoreRRRXS(i: store_name) (rs: ireg) (ra: ireg) (rofs: ireg)
 .
 
-Coercion PStoreRRO:       store_name        >-> Funclass.
-Coercion PStoreRRR:       store_name        >-> Funclass.
-
 (** Arithmetic instructions **)
 Inductive arith_name_r : Type :=
   | Ploadsymbol (id: ident) (ofs: ptrofs)           (**r load the address of a symbol *)
@@ -1160,6 +1155,12 @@ Definition parexec_store_reg (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem
   | Some m' => Next rsw m'
   end.
 
+Definition parexec_store_regxs (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (s a ro: ireg) :=
+  match Mem.storev chunk mr (Val.addl (rsr a) (Val.shll (rsr ro) (scale_of_chunk chunk))) (rsr s) with
+  | None => Stuck
+  | Some m' => Next rsw m'
+  end.
+
 Definition load_chunk n :=
   match n with
   | Plb => Mint8signed
@@ -1198,6 +1199,7 @@ Definition parexec_basic_instr (bi: basic) (rsr rsw: regset) (mr mw: mem) :=
 
   | PStoreRRO n s a ofs => parexec_store_offset (store_chunk n) rsr rsw mr mw s a ofs
   | PStoreRRR n s a ro => parexec_store_reg (store_chunk n) rsr rsw mr mw s a ro
+  | PStoreRRRXS n s a ro => parexec_store_regxs (store_chunk n) rsr rsw mr mw s a ro
 
   | Pallocframe sz pos =>
       let (mw, stk) := Mem.alloc mr 0 sz in
diff --git a/mppa_k1c/PostpassSchedulingOracle.ml b/mppa_k1c/PostpassSchedulingOracle.ml
index ef5e325a..e6643736 100644
--- a/mppa_k1c/PostpassSchedulingOracle.ml
+++ b/mppa_k1c/PostpassSchedulingOracle.ml
@@ -224,7 +224,7 @@ let load_rec i = match i with
 let store_rec i = match i with
   | PStoreRRO (i, rs1, rs2, imm) -> { inst = store_str i; write_locs = [Mem]; read_locs = [Reg (IR rs1); Reg (IR rs2)]; imm = (Some (Off imm))
                                       ; is_control = false}
-  | PStoreRRR (i, rs1, rs2, rs3) -> { inst = store_str i; write_locs = [Mem]; read_locs = [Reg (IR rs1); Reg (IR rs2); Reg (IR rs3)]; imm = None
+  | PStoreRRR (i, rs1, rs2, rs3)  | PStoreRRRXS (i, rs1, rs2, rs3) -> { inst = store_str i; write_locs = [Mem]; read_locs = [Reg (IR rs1); Reg (IR rs2); Reg (IR rs3)]; imm = None
                                       ; is_control = false}
 
 let get_rec (rd:gpreg) rs = { inst = get_str; write_locs = [Reg (IR rd)]; read_locs = [Reg rs]; imm = None; is_control = false }
diff --git a/mppa_k1c/PostpassSchedulingproof.v b/mppa_k1c/PostpassSchedulingproof.v
index 3f3cb19c..43c8acb8 100644
--- a/mppa_k1c/PostpassSchedulingproof.v
+++ b/mppa_k1c/PostpassSchedulingproof.v
@@ -151,6 +151,17 @@ Proof.
   - discriminate.
 Qed.
 
+Lemma exec_store_regxs_pc_var:
+  forall t rs m rd ra ro rs' m' v,
+  exec_store_regxs t rs m rd ra ro = Next rs' m' ->
+  exec_store_regxs t rs # PC <- v m rd ra ro = Next rs' # PC <- v m'.
+Proof.
+  intros. unfold exec_store_regxs in *. unfold parexec_store_regxs in *. rewrite Pregmap.gso; try discriminate.
+  destruct (Mem.storev _ _ _).
+  - inv H. apply next_eq; auto.
+  - discriminate.
+Qed.
+
 Lemma exec_basic_instr_pc_var:
   forall ge i rs m rs' m' v,
   exec_basic_instr ge i rs m = Next rs' m' ->
@@ -170,6 +181,7 @@ Proof.
   - destruct i.
     + exploreInst; apply exec_store_offset_pc_var; auto.
     + exploreInst; apply exec_store_reg_pc_var; auto.
+    + exploreInst; apply exec_store_regxs_pc_var; auto.
   - destruct (Mem.alloc _ _ _) as (m1 & stk). repeat (rewrite Pregmap.gso; try discriminate).
     destruct (Mem.storev _ _ _ _); try discriminate.
     inv H. apply next_eq; auto. apply functional_extensionality. intros.
diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v
index ab0d2964..0a83a903 100644
--- a/mppa_k1c/lib/Asmblockgenproof0.v
+++ b/mppa_k1c/lib/Asmblockgenproof0.v
@@ -949,6 +949,7 @@ Proof.
   1-10: try (unfold parexec_load_regxs in H1; destruct (Mem.loadv _ _ _); [inv H1; Simpl | discriminate]).
   1-10: try (unfold parexec_store_offset in H1; destruct (eval_offset ge ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]).
   1-10: try (unfold parexec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]); auto.
+  1-10: try (unfold parexec_store_regxs in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]); auto.
   - destruct (Mem.alloc _ _ _). destruct (Mem.store _ _ _ _ _). inv H1. Simpl. discriminate.
   - destruct (Mem.loadv _ _ _); try discriminate. destruct (rs1 _); try discriminate.
     destruct (Mem.free _ _ _ _). inv H1. Simpl. discriminate.