MPPA - added Oaddrsymbol -> now able to run the matrix mult test

3 files changed, 17 insertions, 15 deletions

diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v
index d17ba14b..675cb065 100644
--- a/mppa_k1c/Asmgen.v
+++ b/mppa_k1c/Asmgen.v
@@ -262,12 +262,12 @@ Definition transl_op
       OK (if Float32.eq_dec f Float32.zero
           then Pfcvtsw rd GPR0 :: k
           else Ploadsi rd f :: k)
-  | Oaddrsymbol s ofs, nil =>
+*)| Oaddrsymbol s ofs, nil =>
       do rd <- ireg_of res;
       OK (if Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)
           then Ploadsymbol rd s Ptrofs.zero :: addptrofs rd rd ofs k
           else Ploadsymbol rd s ofs :: k)
-*)| Oaddrstack n, nil =>
+  | Oaddrstack n, nil =>
       do rd <- ireg_of res;
       OK (addptrofs rd SP n k)
 
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v
index 4150cba8..2003239e 100644
--- a/mppa_k1c/Asmgenproof.v
+++ b/mppa_k1c/Asmgenproof.v
@@ -317,6 +317,8 @@ Opaque Int.eq.
   unfold transl_op; intros; destruct op; TailNoLabel.
 (* Omove *)
 - destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel.
+(* Oaddrsymbol *)
+- destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)); TailNoLabel.
 (* Oaddimm32 *)
 - apply opimm32_label; intros; exact I.
 (* Oandimm32 *)
diff --git a/mppa_k1c/Asmgenproof1.v b/mppa_k1c/Asmgenproof1.v
index 77643b8b..3085072e 100644
--- a/mppa_k1c/Asmgenproof1.v
+++ b/mppa_k1c/Asmgenproof1.v
@@ -1198,6 +1198,19 @@ Opaque Int.eq.
   unfold transl_op in TR; destruct op; ArgsInv; simpl in EV; SimplEval EV; try TranslOpSimpl.
 - (* Omove *)
   destruct (preg_of res), (preg_of m0); inv TR; TranslOpSimpl.
+- (* Oaddrsymbol *)
+  destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)).
++ set (rs1 := nextinstr (rs#x <- (Genv.symbol_address ge id Ptrofs.zero))).
+  exploit (addptrofs_correct x x ofs k rs1 m); eauto with asmgen. 
+  intros (rs2 & A & B & C).
+  exists rs2; split. 
+  apply exec_straight_step with rs1 m; auto.
+  split. replace ofs with (Ptrofs.add Ptrofs.zero ofs) by (apply Ptrofs.add_zero_l). 
+  rewrite Genv.shift_symbol_address.
+  replace (rs1 x) with (Genv.symbol_address ge id Ptrofs.zero) in B by (unfold rs1; Simpl).
+  exact B.
+  intros. rewrite C by eauto with asmgen. unfold rs1; Simpl.  
++ TranslOpSimpl.
 - (* Oaddrstack *)
   exploit addptrofs_correct. instantiate (1 := GPR12); auto with asmgen. intros (rs' & A & B & C).
   exists rs'; split; eauto. auto with asmgen.
@@ -1229,19 +1242,6 @@ Opaque Int.eq.
 + econstructor; split. 
   apply exec_straight_one. simpl; eauto. auto.
   split; intros; Simpl. 
-- (* addrsymbol *)
-  destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)).
-+ set (rs1 := nextinstr (rs#x <- (Genv.symbol_address ge id Ptrofs.zero))).
-  exploit (addptrofs_correct x x ofs k rs1 m); eauto with asmgen. 
-  intros (rs2 & A & B & C).
-  exists rs2; split. 
-  apply exec_straight_step with rs1 m; auto.
-  split. replace ofs with (Ptrofs.add Ptrofs.zero ofs) by (apply Ptrofs.add_zero_l). 
-  rewrite Genv.shift_symbol_address.
-  replace (rs1 x) with (Genv.symbol_address ge id Ptrofs.zero) in B by (unfold rs1; Simpl).
-  exact B.
-  intros. rewrite C by eauto with asmgen. unfold rs1; Simpl.  
-+ TranslOpSimpl.
 - (* stackoffset *)
   exploit addptrofs_correct. instantiate (1 := X2); auto with asmgen. intros (rs' & A & B & C).
   exists rs'; split; eauto. auto with asmgen.