diff options
Diffstat (limited to 'mppa_k1c')
-rw-r--r-- | mppa_k1c/Asmgen.v | 4 | ||||
-rw-r--r-- | mppa_k1c/Asmgenproof.v | 2 | ||||
-rw-r--r-- | mppa_k1c/Asmgenproof1.v | 26 |
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. |