Added a simple postpass oracle that splits a bblock into single instruction bundles

1 files changed, 7 insertions, 3 deletions

diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v
index 8eb0b693..588019a2 100644
--- a/mppa_k1c/Asmgenproof.v
+++ b/mppa_k1c/Asmgenproof.v
@@ -16,13 +16,14 @@ Require Import Coqlib Errors.
 Require Import Integers Floats AST Linking.
 Require Import Values Memory Events Globalenvs Smallstep.
 Require Import Op Locations Mach Conventions Asm Asmgen Machblockgen Asmblockgen.
-Require Import Machblockgenproof Asmblockgenproof.
+Require Import Machblockgenproof Asmblockgenproof PostpassSchedulingproof.
 
 Local Open Scope linking_scope.
 
 Definition block_passes :=
       mkpass Machblockgenproof.match_prog
   ::: mkpass Asmblockgenproof.match_prog
+  ::: mkpass PostpassSchedulingproof.match_prog
   ::: mkpass Asm.match_prog
   ::: pass_nil _.
 
@@ -33,10 +34,12 @@ Lemma transf_program_match:
 Proof.
   intros p tp H.
   unfold Asmgen.transf_program in H. apply bind_inversion in H. destruct H.
-  inversion_clear H. inversion H1. remember (Machblockgen.transf_program p) as mbp.
+  inversion_clear H. apply bind_inversion in H1. destruct H1.
+  inversion_clear H. inversion H2. remember (Machblockgen.transf_program p) as mbp.
   unfold match_prog; simpl.
   exists mbp; split. apply Machblockgenproof.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 Asm.transf_program_match; auto. auto.
 Qed.
 
@@ -147,12 +150,13 @@ 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 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.
   unfold Machblockgenproof.inv_trans_rao. 
   intros X; apply X.
   eapply compose_forward_simulations. apply Asmblockgenproof.transf_program_correct; eauto.
+  eapply compose_forward_simulations. apply PostpassSchedulingproof.transf_program_correct; eauto.
   apply Asm.transf_program_correct. eauto.
 Qed.