Removing the PseudoAsm IR

1 files changed, 11 insertions, 21 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 793d94f9..690a54a2 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -18,7 +18,7 @@
 Require Import Coqlib Errors.
 Require Import Integers Floats AST Linking.
 Require Import Values Memory Events Globalenvs Smallstep.
-Require Import Op Locations Machblock Conventions PseudoAsmblock PseudoAsmblockproof Asm Asmblock.
+Require Import Op Locations Machblock Conventions Asm Asmblock.
 Require Machblockgenproof Asmblockgenproof PostpassSchedulingproof.
 Require Import Asmgen.
 Require Import Axioms.
@@ -2281,7 +2281,6 @@ Local Open Scope linking_scope.
 
 Definition block_passes :=
       mkpass Machblockgenproof.match_prog
-  ::: mkpass PseudoAsmblockproof.match_prog
   ::: mkpass Asmblockgenproof.match_prog
   ::: mkpass PostpassSchedulingproof.match_prog
   ::: mkpass Asmblock_PRESERVATION.match_prog
@@ -2295,27 +2294,27 @@ Proof.
   intros p tp H.
   unfold Asmgen.transf_program in H. apply bind_inversion in H. destruct H.
   inversion_clear H. apply bind_inversion in H1. destruct H1.
-  inversion_clear H. apply bind_inversion in H2. destruct H2. inversion_clear H.
+  inversion_clear H.
   unfold Compopts.time in *. remember (Machblockgen.transf_program p) as mbp.
   unfold match_prog; simpl.
   exists mbp; split. apply Machblockgenproof.transf_program_match; auto.
-  exists x; split. apply PseudoAsmblockproof.transf_program_match; auto.
-  exists x0; split. apply Asmblockgenproof.transf_program_match; auto.
-  exists x1; split. apply PostpassSchedulingproof.transf_program_match; auto.
+  exists x; split. apply Asmblockgenproof.transf_program_match; auto.
+  exists x0; split. apply PostpassSchedulingproof.transf_program_match; auto.
   exists tp; split. apply Asmblock_PRESERVATION.transf_program_match; auto. auto.
 Qed.
 
 (** Return Address Offset *)
 
 Definition return_address_offset: Mach.function -> Mach.code -> ptrofs -> Prop :=
-  Machblockgenproof.Mach_return_address_offset (PseudoAsmblockproof.rao Asmblockgenproof.next).
+  Machblockgenproof.Mach_return_address_offset (Asmblockgenproof.return_address_offset).
 
 Lemma return_address_exists:
   forall f sg ros c, is_tail (Mach.Mcall sg ros :: c) f.(Mach.fn_code) ->
   exists ra, return_address_offset f c ra.
 Proof.
-  intros; eapply Machblockgenproof.Mach_return_address_exists; eauto.
-Admitted.
+  intros; unfold return_address_offset; eapply Machblockgenproof.Mach_return_address_exists; eauto.
+  intros; eapply Asmblockgenproof.return_address_exists; eauto.
+Qed.
 
 Section PRESERVATION.
 
@@ -2329,28 +2328,19 @@ Theorem transf_program_correct:
   forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog).
 Proof.
   unfold match_prog in TRANSF. simpl in TRANSF.
-  inv TRANSF. inv H. inv H1. inv H. inv H2. inv H. inv H3. inv H. inv H4. inv H.
+  inv TRANSF. inv H. inv H1. inv H. inv H2. inv H. inv H3. inv H.
   eapply compose_forward_simulations.
   { exploit Machblockgenproof.transf_program_correct; eauto. }
   
   eapply compose_forward_simulations.
-  + apply PseudoAsmblockproof.transf_program_correct; eauto.
-    - intros; apply Asmblockgenproof.next_progress.
-    - intros. eapply Asmblockgenproof.functions_bound_max_pos; eauto.
-    { intros.
-      unfold Genv.symbol_address.
-      erewrite <- PostpassSchedulingproof.symbols_preserved; eauto.
-      erewrite Asmblock_PRESERVATION.symbol_high_low; eauto.
-      reflexivity.
-     }
-  + eapply compose_forward_simulations. apply Asmblockgenproof.transf_program_correct; eauto.
+  + apply Asmblockgenproof.transf_program_correct; eauto.
     { intros.
       unfold Genv.symbol_address.
       erewrite <- PostpassSchedulingproof.symbols_preserved; eauto.
       erewrite Asmblock_PRESERVATION.symbol_high_low; eauto.
       reflexivity.
     }
-    eapply compose_forward_simulations.
+  + eapply compose_forward_simulations.
     - apply PostpassSchedulingproof.transf_program_correct; eauto.
     - apply Asmblock_PRESERVATION.transf_program_correct; eauto.
 Qed.