big proofs for so / lo

4 files changed, 306 insertions, 6 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 70d39168..b928a48e 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -113,7 +113,8 @@ Inductive instruction : Type :=
   | Pld_a   (rd: ireg) (ra: ireg) (ofs: addressing)     (**r load any64 *)

   | Pfls    (rd: freg) (ra: ireg) (ofs: addressing)     (**r load float *)

   | Pfld    (rd: freg) (ra: ireg) (ofs: addressing)    (**r load 64-bit float *)

-  | Plq     (rs: gpreg_q) (ra: ireg) (ofs: addressing)  (**r load 64-bit float *)

+  | Plq     (rs: gpreg_q) (ra: ireg) (ofs: addressing)  (**r load 2*64-bit *)

+  | Plo     (rs: gpreg_o) (ra: ireg) (ofs: addressing)  (**r load 4*64-bit *)

 

   (** Stores **)

   | Psb     (rs: ireg) (ra: ireg) (ofs: addressing)     (**r store byte *)

@@ -125,7 +126,8 @@ Inductive instruction : Type :=
   | Pfss    (rs: freg) (ra: ireg) (ofs: addressing)     (**r store float *)

   | Pfsd    (rs: freg) (ra: ireg) (ofs: addressing)    (**r store 64-bit float *)

 

-  | Psq     (rs: gpreg_q) (ra: ireg) (ofs: addressing)  (**r store 64-bit float *)

+  | Psq     (rs: gpreg_q) (ra: ireg) (ofs: addressing)  (**r store 2*64-bit *)

+  | Pso     (rs: gpreg_o) (ra: ireg) (ofs: addressing)  (**r store 2*64-bit *)

 

   (** Arith RR *)

   | Pmv     (rd rs: ireg)                           (**r register move *)

@@ -438,6 +440,7 @@ Definition basic_to_instruction (b: basic) :=
   | PLoadRRO Asmvliw.Pfld rd ra ofs  => Pfld rd ra (AOff ofs)

 

   | PLoadQRRO qrs ra ofs => Plq qrs ra (AOff ofs)

+  | PLoadORRO qrs ra ofs => Plo qrs ra (AOff ofs)

 

   | PLoadRRR Asmvliw.Plb rd ra ro   => Plb rd ra (AReg ro)

   | PLoadRRR Asmvliw.Plbu rd ra ro  => Plbu rd ra (AReg ro)

@@ -490,6 +493,7 @@ Definition basic_to_instruction (b: basic) :=
   | PStoreRRRXS Asmvliw.Pfsd rd ra ro => Pfsd rd ra (ARegXS ro)

 

   | PStoreQRRO qrs ra ofs => Psq qrs ra (AOff ofs)

+  | PStoreORRO qrs ra ofs => Pso qrs ra (AOff ofs)

   end.

 

 Section RELSEM.

diff --git a/mppa_k1c/Asmblockdeps.v b/mppa_k1c/Asmblockdeps.v
index 225c3e98..baaff273 100644
--- a/mppa_k1c/Asmblockdeps.v
+++ b/mppa_k1c/Asmblockdeps.v
@@ -654,17 +654,35 @@ Definition trans_basic (b: basic) : inst :=
   | PLoadQRRO qd a ofs =>
     let (d0, d1) := gpreg_q_expand qd in
     if ireg_eq d0 a
-    then [(#d0, Op Fail Enil);
-            (#d1, Op Fail Enil)]
+    then [(#d0, Op Fail Enil)]
     else
       [(#d0, Op (Load (OLoadRRO Pld_a ofs)) (PReg (#a) @ PReg pmem @ Enil));
        (#d1, Op (Load (OLoadRRO Pld_a (Ptrofs.add ofs (Ptrofs.repr 8)))) (PReg (#a) @ PReg pmem @ Enil))]
+  | PLoadORRO od a ofs =>
+    match gpreg_o_expand od with
+    | (d0, d1, d2, d3) =>
+      if (ireg_eq d0 a) || (ireg_eq d1 a) || (ireg_eq d2 a)
+      then [(#d0, Op Fail Enil)]
+      else
+        [(#d0, Op (Load (OLoadRRO Pld_a ofs)) (PReg (#a) @ PReg pmem @ Enil));
+         (#d1, Op (Load (OLoadRRO Pld_a (Ptrofs.add ofs (Ptrofs.repr 8)))) (PReg (#a) @ PReg pmem @ Enil));
+         (#d2, Op (Load (OLoadRRO Pld_a (Ptrofs.add ofs (Ptrofs.repr 16)))) (PReg (#a) @ PReg pmem @ Enil));
+         (#d3, Op (Load (OLoadRRO Pld_a (Ptrofs.add ofs (Ptrofs.repr 24)))) (PReg (#a) @ PReg pmem @ Enil))]
+    end
   | 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))]
   | PStoreQRRO qs a ofs =>
     let (s0, s1) := gpreg_q_expand qs in 
     [(pmem, Op (Store (OStoreRRO Psd_a ofs)) (PReg (#s0) @ PReg (#a) @ PReg pmem @ Enil));
      (pmem, Op (Store (OStoreRRO Psd_a (Ptrofs.add ofs (Ptrofs.repr 8)))) (PReg (#s1) @ PReg (#a) @ PReg pmem @ Enil))]
+  | PStoreORRO os a ofs =>
+    match gpreg_o_expand os with
+    | (s0, s1, s2, s3) =>
+      [(pmem, Op (Store (OStoreRRO Psd_a ofs)) (PReg (#s0) @ PReg (#a) @ PReg pmem @ Enil));
+       (pmem, Op (Store (OStoreRRO Psd_a (Ptrofs.add ofs (Ptrofs.repr 8)))) (PReg (#s1) @ PReg (#a) @ PReg pmem @ Enil));
+       (pmem, Op (Store (OStoreRRO Psd_a (Ptrofs.add ofs (Ptrofs.repr 16)))) (PReg (#s2) @ PReg (#a) @ PReg pmem @ Enil));
+       (pmem, Op (Store (OStoreRRO Psd_a (Ptrofs.add ofs (Ptrofs.repr 24)))) (PReg (#s3) @ PReg (#a) @ PReg pmem @ Enil))]
+    end
   | 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));
@@ -885,7 +903,9 @@ Proof.
       unfold parexec_load_regxs; simpl; unfold exec_load_deps_regxs; rewrite H, H0; rewrite (H0 rofs);
       destruct (Mem.loadv _ _ _) eqn:MEML; simpl; auto;
       eexists; split; try split; Simpl;
-      intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl.
+        intros rr; destruct rr; Simpl; destruct (ireg_eq g rd); subst; Simpl.
+
+    (* Load Quad word *)
     + unfold parexec_load_q_offset.
       destruct (gpreg_q_expand rd) as [rd0 rd1].
       destruct (ireg_eq rd0 ra) as [ OVERLAP0 | NOOVERLAP0 ].
@@ -935,6 +955,106 @@ Proof.
             constructor.
      ++ rewrite H0. rewrite H. rewrite MEML0. trivial.
                  
+    (* Load Octuple word *)
+    + unfold parexec_load_o_offset.
+      destruct (gpreg_o_expand rd) as [[[rd0 rd1] rd2] rd3].
+      destruct (ireg_eq rd0 ra); simpl; trivial.
+      destruct (ireg_eq rd1 ra); simpl; trivial.
+      destruct (ireg_eq rd2 ra); simpl; trivial.
+      destruct Ge.
+      repeat rewrite H0.
+      destruct (Mem.loadv Many64 mr (Val.offset_ptr (rsr ra) ofs)) as [load0 | ] eqn:MEML0; simpl.
+      { destruct (Mem.loadv Many64 mr
+                            (Val.offset_ptr (rsr ra) (Ptrofs.add ofs (Ptrofs.repr 8)))) as [load1| ] eqn:MEML1.
+        { destruct (Mem.loadv Many64 mr
+                              (Val.offset_ptr (rsr ra) (Ptrofs.add ofs (Ptrofs.repr 16)))) as [load2| ] eqn:MEML2.
+          { destruct (Mem.loadv Many64 mr
+                                (Val.offset_ptr (rsr ra) (Ptrofs.add ofs (Ptrofs.repr 24)))) as [load3| ] eqn:MEML3.
+            { rewrite H.
+              rewrite MEML0.
+              rewrite (assign_diff _ _ (# ra)) by (apply ppos_discr; congruence).
+              rewrite H0.
+              rewrite (assign_diff _ _ pmem) by (apply not_eq_sym; apply ppos_pmem_discr).
+              rewrite H.
+              rewrite MEML1.
+              repeat rewrite (assign_diff _ _ (# ra)) by (apply ppos_discr; congruence).
+              rewrite H0.
+              repeat rewrite (assign_diff _ _ pmem) by (apply not_eq_sym; apply ppos_pmem_discr).
+              rewrite H.
+              rewrite MEML2.
+              repeat rewrite (assign_diff _ _ (# ra)) by (apply ppos_discr; congruence).
+              rewrite H0.
+              repeat rewrite (assign_diff _ _ pmem) by (apply not_eq_sym; apply ppos_pmem_discr).
+              rewrite H.
+              rewrite MEML3.
+              repeat rewrite (assign_diff _ _ (# ra)) by (apply ppos_discr; congruence).
+              econstructor; split; trivial.
+              constructor.
+              { repeat rewrite (assign_diff _ _ pmem) by (apply not_eq_sym; apply ppos_pmem_discr). assumption. }
+              { intro.
+                destruct (preg_eq r rd3).
+                { subst r. rewrite assign_eq. rewrite Pregmap.gss. trivial.
+                }
+                rewrite assign_diff by (apply ppos_discr; congruence).
+                rewrite Pregmap.gso by assumption.
+                destruct (preg_eq r rd2).
+                { subst r. rewrite assign_eq.
+                  rewrite Pregmap.gss. trivial.
+                }
+                rewrite assign_diff by (apply ppos_discr; congruence).
+                rewrite Pregmap.gso by assumption.
+                destruct (preg_eq r rd1).
+                { subst r. rewrite assign_eq.
+                  rewrite Pregmap.gss. trivial.
+                }
+                rewrite assign_diff by (apply ppos_discr; congruence).
+                rewrite Pregmap.gso by assumption.
+                destruct (preg_eq r rd0).
+                { subst r. rewrite assign_eq.
+                  rewrite Pregmap.gss. trivial.
+                }
+                rewrite assign_diff by (apply ppos_discr; congruence).
+                rewrite Pregmap.gso by assumption.
+                auto.
+              }
+            }
+            rewrite H. rewrite MEML0.
+            rewrite assign_diff by (apply ppos_discr; congruence).
+            rewrite H0.
+            rewrite (assign_diff _ _ pmem) by (apply not_eq_sym; apply ppos_pmem_discr).                
+            rewrite H. rewrite MEML1.
+            repeat rewrite assign_diff by (apply ppos_discr; congruence).
+            rewrite H0.
+            repeat rewrite (assign_diff _ _ pmem) by (apply not_eq_sym; apply ppos_pmem_discr).
+            rewrite H. rewrite MEML2.
+            repeat rewrite assign_diff by (apply ppos_discr; congruence).
+            rewrite H0.
+            repeat rewrite (assign_diff _ _ pmem) by (apply not_eq_sym; apply ppos_pmem_discr).
+            rewrite H. rewrite MEML3.
+            constructor.
+          }
+          rewrite H. rewrite MEML0.
+          rewrite assign_diff by (apply ppos_discr; congruence).
+          rewrite H0.
+          rewrite (assign_diff _ _ pmem) by (apply not_eq_sym; apply ppos_pmem_discr).                
+          rewrite H. rewrite MEML1.
+          repeat rewrite assign_diff by (apply ppos_discr; congruence).
+          rewrite H0.
+          repeat rewrite (assign_diff _ _ pmem) by (apply not_eq_sym; apply ppos_pmem_discr).
+          rewrite H. rewrite MEML2.
+          repeat rewrite assign_diff by (apply ppos_discr; congruence).
+          constructor.
+        }
+        rewrite H. rewrite MEML0.
+        rewrite assign_diff by (apply ppos_discr; congruence).
+        rewrite H0.
+        rewrite (assign_diff _ _ pmem) by (apply not_eq_sym; apply ppos_pmem_discr).                
+        rewrite H. rewrite MEML1.
+        repeat rewrite assign_diff by (apply ppos_discr; congruence).
+        constructor.
+      }
+      rewrite H. rewrite MEML0.
+      constructor.
 (* Store *)
   - destruct i.
     (* Store Offset *)
@@ -959,6 +1079,7 @@ Proof.
       eexists; split; try split; Simpl;
       intros rr; destruct rr; Simpl.
 
+    (* Store Quad Word *)
     + unfold parexec_store_q_offset.
       simpl.
       destruct (gpreg_q_expand rs) as [s0 s1].
@@ -989,6 +1110,81 @@ Proof.
            reflexivity.
      ++ rewrite MEML0.
         reflexivity.
+
+    (* Store Ocuple Word *)
+    + unfold parexec_store_o_offset.
+      simpl.
+      destruct (gpreg_o_expand rs) as [[[s0 s1] s2] s3].
+      simpl.
+      destruct Ge.
+      destruct (Mem.storev _ _ _ (rsr s0)) as [store0 | ] eqn:MEML0.
+      { destruct (Mem.storev _ _ _ (rsr s1)) as [store1 | ] eqn:MEML1.
+        { destruct (Mem.storev _ _ _ (rsr s2)) as [store2 | ] eqn:MEML2.
+          { destruct (Mem.storev _ _ _ (rsr s3)) as [store3 | ] eqn:MEML3.
+            { repeat (try rewrite H0; try rewrite H).
+              simpl.
+              rewrite MEML0.
+              repeat rewrite (assign_diff _ _ _) by apply ppos_pmem_discr.
+              repeat (try rewrite H0; try rewrite H).
+              rewrite assign_eq.
+              rewrite MEML1.
+              repeat rewrite (assign_diff _ _ _) by apply ppos_pmem_discr.
+              repeat (try rewrite H0; try rewrite H).
+              rewrite assign_eq.
+              rewrite MEML2.
+              repeat rewrite (assign_diff _ _ _) by apply ppos_pmem_discr.
+              repeat (try rewrite H0; try rewrite H).
+              rewrite assign_eq.
+              rewrite MEML3.
+              econstructor; split; trivial.
+              split.
+              { repeat rewrite assign_eq. trivial. }
+              { intro.
+                repeat rewrite (assign_diff _ _ _) by apply ppos_pmem_discr.
+                trivial. }
+            }
+            {
+              repeat (try rewrite H0; try rewrite H; simpl).
+              rewrite MEML0.
+              repeat rewrite (assign_diff _ _ _) by apply ppos_pmem_discr.
+              repeat (try rewrite H0; try rewrite H; simpl).
+              rewrite MEML1.
+              repeat rewrite (assign_diff _ _ _) by apply ppos_pmem_discr.
+              repeat (try rewrite H0; try rewrite H; simpl).
+              rewrite MEML2.
+              repeat rewrite (assign_diff _ _ _) by apply ppos_pmem_discr.
+              repeat (try rewrite H0; try rewrite H; simpl).
+              rewrite MEML3.
+              trivial.
+            }
+          }
+          {
+              repeat (try rewrite H0; try rewrite H; simpl).
+              rewrite MEML0.
+              repeat rewrite (assign_diff _ _ _) by apply ppos_pmem_discr.
+              repeat (try rewrite H0; try rewrite H; simpl).
+              rewrite MEML1.
+              repeat rewrite (assign_diff _ _ _) by apply ppos_pmem_discr.
+              repeat (try rewrite H0; try rewrite H; simpl).
+              rewrite MEML2.
+              trivial.
+          }
+        }
+        {
+          repeat (try rewrite H0; try rewrite H; simpl).
+          rewrite MEML0.
+          repeat rewrite (assign_diff _ _ _) by apply ppos_pmem_discr.
+          repeat (try rewrite H0; try rewrite H; simpl).
+          rewrite MEML1.
+          trivial.
+        }
+      }
+      {
+        repeat (try rewrite H0; try rewrite H; simpl).
+        rewrite MEML0.
+        trivial.
+      }
+            
   (* Allocframe *)
   - destruct (Mem.alloc _ _ _) eqn:MEMAL. destruct (Mem.store _ _ _ _) eqn:MEMS.
     * eexists; repeat split.
diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v
index 30263b4d..3fbc048c 100644
--- a/mppa_k1c/Asmvliw.v
+++ b/mppa_k1c/Asmvliw.v
@@ -83,7 +83,7 @@ Inductive gpreg_q : Type :=
 | R40R41 | R42R43 | R44R45 | R46R47 | R48R49
 | R50R51 | R52R53 | R54R55 | R56R57 | R58R59
 | R60R61 | R62R63.
-
+                             
 Lemma gpreg_q_eq : forall (x y : gpreg_q), {x=y} + {x<>y}.
 Proof. decide equality. Defined.
 
@@ -123,6 +123,35 @@ Definition gpreg_q_expand (x : gpreg_q) : gpreg * gpreg :=
   | R62R63 => (GPR62, GPR63)
   end.
 
+Inductive gpreg_o : Type :=
+| R0R1R2R3 | R4R5R6R7 | R8R9R10R11 | R12R13R14R15
+| R16R17R18R19 | R20R21R22R23 | R24R25R26R27 | R28R29R30R31
+| R32R33R34R35 | R36R37R38R39 | R40R41R42R43 | R44R45R46R47
+| R48R49R50R51 | R52R53R54R55 | R56R57R58R59 | R60R61R62R63.
+
+Definition gpreg_o_expand (x : gpreg_o) : gpreg * gpreg * gpreg * gpreg :=
+  match x with
+  | R0R1R2R3 => (GPR0, GPR1, GPR2, GPR3)
+  | R4R5R6R7 => (GPR4, GPR5, GPR6, GPR7)
+  | R8R9R10R11 => (GPR8, GPR9, GPR10, GPR11)
+  | R12R13R14R15 => (GPR12, GPR13, GPR14, GPR15)
+  | R16R17R18R19 => (GPR16, GPR17, GPR18, GPR19)
+  | R20R21R22R23 => (GPR20, GPR21, GPR22, GPR23)
+  | R24R25R26R27 => (GPR24, GPR25, GPR26, GPR27)
+  | R28R29R30R31 => (GPR28, GPR29, GPR30, GPR31)
+  | R32R33R34R35 => (GPR32, GPR33, GPR34, GPR35)
+  | R36R37R38R39 => (GPR36, GPR37, GPR38, GPR39)
+  | R40R41R42R43 => (GPR40, GPR41, GPR42, GPR43)
+  | R44R45R46R47 => (GPR44, GPR45, GPR46, GPR47)
+  | R48R49R50R51 => (GPR48, GPR49, GPR50, GPR51)
+  | R52R53R54R55 => (GPR52, GPR53, GPR54, GPR55)
+  | R56R57R58R59 => (GPR56, GPR57, GPR58, GPR59)
+  | R60R61R62R63 => (GPR60, GPR61, GPR62, GPR63)
+  end.
+    
+Lemma gpreg_o_eq : forall (x y : gpreg_o), {x=y} + {x<>y}.
+Proof. decide equality. Defined.
+
 (** We model the following registers of the RISC-V architecture. *)
 
 (** basic register *)
@@ -319,6 +348,7 @@ Inductive ld_instruction : Type :=
   | PLoadRRR   (i: load_name) (rd: ireg) (ra: ireg) (rofs: ireg)
   | PLoadRRRXS (i: load_name) (rd: ireg) (ra: ireg) (rofs: ireg)
   | PLoadQRRO  (rd: gpreg_q) (ra: ireg) (ofs: offset)
+  | PLoadORRO  (rd: gpreg_o) (ra: ireg) (ofs: offset)
 .
 
 (** Stores **)
@@ -338,6 +368,7 @@ Inductive st_instruction : Type :=
   | PStoreRRR  (i: store_name) (rs: ireg) (ra: ireg) (rofs: ireg)
   | PStoreRRRXS(i: store_name) (rs: ireg) (ra: ireg) (rofs: ireg)
   | PStoreQRRO (rs: gpreg_q) (ra: ireg) (ofs: offset)
+  | PStoreORRO (rs: gpreg_o) (ra: ireg) (ofs: offset)
 .
 
 (** Arithmetic instructions **)
@@ -1167,6 +1198,31 @@ Definition parexec_load_q_offset (rsr rsw: regset) (mr mw: mem) (d : gpreg_q) (a
       end
     end.
 
+Definition parexec_load_o_offset (rsr rsw: regset) (mr mw: mem) (d : gpreg_o) (a: ireg) (ofs: offset) :=
+  match gpreg_o_expand d with
+  | (rd0, rd1, rd2, rd3) =>
+  if (ireg_eq rd0 a) || (ireg_eq rd1 a) || (ireg_eq rd2 a)
+  then Stuck
+  else
+    match Mem.loadv Many64 mr (Val.offset_ptr (rsr a) ofs) with
+    | None => Stuck
+    | Some v0 =>
+      match Mem.loadv Many64 mr (Val.offset_ptr (rsr a) (Ptrofs.add ofs (Ptrofs.repr 8))) with
+      | None => Stuck
+      | Some v1 =>
+        match Mem.loadv Many64 mr (Val.offset_ptr (rsr a) (Ptrofs.add ofs (Ptrofs.repr 16))) with
+        | None => Stuck
+        | Some v2 =>
+          match Mem.loadv Many64 mr (Val.offset_ptr (rsr a) (Ptrofs.add ofs (Ptrofs.repr 24))) with
+          | None => Stuck
+          | Some v3 =>
+            Next (rsw#rd0 <- v0 #rd1 <- v1 #rd2 <- v2 #rd3 <- v3) mw
+          end
+        end
+      end
+    end
+  end.
+
 Definition parexec_load_reg (chunk: memory_chunk) (rsr rsw: regset) (mr mw: mem) (d a ro: ireg) :=
   match Mem.loadv chunk mr (Val.addl (rsr a) (rsr ro)) with
   | None => Stuck
@@ -1211,6 +1267,27 @@ Definition parexec_store_q_offset (rsr rsw: regset) (mr mw: mem) (s : gpreg_q) (
     end
   end.
   
+Definition parexec_store_o_offset (rsr rsw: regset) (mr mw: mem) (s : gpreg_o) (a: ireg) (ofs: offset) :=
+  match gpreg_o_expand s with
+  | (s0, s1, s2, s3) =>
+    match Mem.storev Many64 mr (Val.offset_ptr (rsr a) ofs) (rsr s0) with
+    | None => Stuck
+    | Some m1 =>
+      match Mem.storev Many64 m1 (Val.offset_ptr (rsr a) (Ptrofs.add ofs (Ptrofs.repr 8))) (rsr s1) with
+      | None => Stuck
+      | Some m2 =>
+        match Mem.storev Many64 m2 (Val.offset_ptr (rsr a) (Ptrofs.add ofs (Ptrofs.repr 16))) (rsr s2) with
+        | None => Stuck
+        | Some m3 =>
+          match Mem.storev Many64 m3 (Val.offset_ptr (rsr a) (Ptrofs.add ofs (Ptrofs.repr 24))) (rsr s3) with
+          | None => Stuck
+          | Some m4 => Next rsw m4
+          end
+        end
+      end
+    end
+  end.
+  
 
 Definition load_chunk n :=
   match n with
@@ -1249,12 +1326,17 @@ Definition parexec_basic_instr (bi: basic) (rsr rsw: regset) (mr mw: mem) :=
   | PLoadRRRXS n d a ro => parexec_load_regxs (load_chunk n) rsr rsw mr mw d a ro
   | PLoadQRRO d a ofs => 
     parexec_load_q_offset rsr rsw mr mw d a ofs
+  | PLoadORRO d a ofs => 
+    parexec_load_o_offset rsr rsw mr mw d a ofs
 
   | 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
   | PStoreQRRO s a ofs => 
     parexec_store_q_offset rsr rsw mr mw s a ofs
+  | PStoreORRO s a ofs => 
+    parexec_store_o_offset rsr rsw mr mw s a ofs
+
   | Pallocframe sz pos =>
       let (mw, stk) := Mem.alloc mr 0 sz in
       let sp := (Vptr stk Ptrofs.zero) in
diff --git a/mppa_k1c/lib/Asmblockgenproof0.v b/mppa_k1c/lib/Asmblockgenproof0.v
index 9303b780..e8835a82 100644
--- a/mppa_k1c/lib/Asmblockgenproof0.v
+++ b/mppa_k1c/lib/Asmblockgenproof0.v
@@ -957,6 +957,15 @@ Proof.
     destruct (Mem.loadv _ _ _) in H1; try discriminate.
     destruct (Mem.loadv _ _ _) in H1; try discriminate.
     inv H1. Simpl.    
+  - (* PLoadORRO *)
+    unfold  parexec_load_o_offset in H1.
+    destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1.
+    destruct (orb _ _) in H1; try discriminate.
+    destruct (Mem.loadv _ _ _) in H1; try discriminate.
+    destruct (Mem.loadv _ _ _) in H1; try discriminate.
+    destruct (Mem.loadv _ _ _) in H1; try discriminate.
+    destruct (Mem.loadv _ _ _) in H1; try discriminate.
+    inv H1. Simpl.    
   - (* PStoreQRRO *)
     unfold  parexec_store_q_offset in H1.
     destruct (gpreg_q_expand _) as [r0 r1] in H1.
@@ -964,6 +973,15 @@ Proof.
     destruct (Mem.storev _ _ _) in H1; try discriminate.
     destruct (Mem.storev _ _ _) in H1; try discriminate.
     inv H1. Simpl. reflexivity.
+  - (* PStoreORRO *)
+    unfold  parexec_store_o_offset in H1.
+    destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1.
+    unfold eval_offset in H1; try discriminate.
+    destruct (Mem.storev _ _ _) in H1; try discriminate.
+    destruct (Mem.storev _ _ _) in H1; try discriminate.
+    destruct (Mem.storev _ _ _) in H1; try discriminate.
+    destruct (Mem.storev _ _ _) in H1; try discriminate.
+    inv H1. Simpl. reflexivity.
   - 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.