Revert "implemented -fno-postpass normally"

This reverts commit fdb8d0c7b5a8be87a64cb995f3abf5bc60f07bfd.

3 files changed, 18 insertions, 45 deletions

diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v
index 46714496..58e80be1 100644
--- a/mppa_k1c/Asmgen.v
+++ b/mppa_k1c/Asmgen.v
@@ -19,16 +19,13 @@ Require Import Integers.
 Require Import Mach Asm Asmblock Asmblockgen Machblockgen.
 Require Import PostpassScheduling.
 Require Import Errors.
-Require Import Compopts.
 
 Local Open Scope error_monad_scope.
 
 Definition transf_program (p: Mach.program) : res Asm.program :=
   let mbp := Machblockgen.transf_program p in
   do abp <- Asmblockgen.transf_program mbp;
-    do abp' <- if Compopts.optim_postpass tt
-               then PostpassScheduling.transf_program abp
-               else OK abp;
+  do abp' <- PostpassScheduling.transf_program abp;
   OK (Asm.transf_program abp').
 
 Definition transf_function (f: Mach.function) : res Asm.function :=
diff --git a/mppa_k1c/Asmgenproof.v b/mppa_k1c/Asmgenproof.v
index 918403cd..588019a2 100644
--- a/mppa_k1c/Asmgenproof.v
+++ b/mppa_k1c/Asmgenproof.v
@@ -17,18 +17,15 @@ 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 PostpassSchedulingproof.
-Require Import Compopts.
 
 Local Open Scope linking_scope.
 
 Definition block_passes :=
       mkpass Machblockgenproof.match_prog
   ::: mkpass Asmblockgenproof.match_prog
-  ::: if Compopts.optim_postpass tt
-      then mkpass PostpassSchedulingproof.match_prog
-           ::: mkpass Asm.match_prog
-           ::: pass_nil _
-      else mkpass Asm.match_prog ::: pass_nil _.
+  ::: mkpass PostpassSchedulingproof.match_prog
+  ::: mkpass Asm.match_prog
+  ::: pass_nil _.
 
 Definition match_prog := pass_match (compose_passes block_passes).
 
@@ -39,16 +36,11 @@ Proof.
   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. inversion H2. remember (Machblockgen.transf_program p) as mbp.
-  unfold match_prog. simpl.
-  destruct (optim_postpass tt); 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.
-  - exists mbp; split. apply Machblockgenproof.transf_program_match; auto.
-    exists x0; split. apply Asmblockgenproof.transf_program_match; auto.
-    congruence.
-    exists tp; split. apply Asm.transf_program_match; auto. auto.
+  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.
 
 (** Return Address Offset *)
@@ -157,25 +149,15 @@ Let tge := Genv.globalenv tprog.
 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.
-  destruct (optim_postpass tt) in *.
-  - inv H. inv H1. inv H. inv H2. inv H. inv H3. inv H. inv H4.
-    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.
-  - inv H. inv H1. inv H. inv H2. inv H. inv H3.
-    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.
-    apply Asm.transf_program_correct ; eauto.
+  unfold match_prog in TRANSF. simpl in TRANSF.
+  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.
 
 End PRESERVATION.
diff --git a/mppa_k1c/SelectOp.v b/mppa_k1c/SelectOp.v
index 66615f1d..edb07e5f 100644
--- a/mppa_k1c/SelectOp.v
+++ b/mppa_k1c/SelectOp.v
@@ -123,8 +123,6 @@ Nondetfunction add (e1: expr) (e2: expr) :=
       addimm n1 (Eop Oadd (t1:::t2:::Enil))
   | t1, Eop (Oaddimm n2) (t2:::Enil) =>
       addimm n2 (Eop Oadd (t1:::t2:::Enil))
-  | t1, (Eop Omul (t2:::t3:::Enil)) =>
-      Eop Omadd (t1:::t2:::t3:::Enil)
   | _, _ => Eop Oadd (e1:::e2:::Enil)
   end.
 >>
@@ -138,7 +136,6 @@ Inductive add_cases: forall (e1: expr) (e2: expr), Type :=
   | add_case5: forall n1 n2 t2, add_cases (Eop (Oaddrstack n1) Enil) (Eop (Oaddimm n2) (t2:::Enil))
   | add_case6: forall n1 t1 t2, add_cases (Eop (Oaddimm n1) (t1:::Enil)) (t2)
   | add_case7: forall t1 n2 t2, add_cases (t1) (Eop (Oaddimm n2) (t2:::Enil))
-  | add_case8: forall t1 t2 t3, add_cases (t1) ((Eop Omul (t2:::t3:::Enil)))
   | add_default: forall (e1: expr) (e2: expr), add_cases e1 e2.
 
 Definition add_match (e1: expr) (e2: expr) :=
@@ -150,7 +147,6 @@ Definition add_match (e1: expr) (e2: expr) :=
   | Eop (Oaddrstack n1) Enil, Eop (Oaddimm n2) (t2:::Enil) => add_case5 n1 n2 t2
   | Eop (Oaddimm n1) (t1:::Enil), t2 => add_case6 n1 t1 t2
   | t1, Eop (Oaddimm n2) (t2:::Enil) => add_case7 t1 n2 t2
-  | t1, (Eop Omul (t2:::t3:::Enil)) => add_case8 t1 t2 t3
   | e1, e2 => add_default e1 e2
   end.
 
@@ -170,8 +166,6 @@ Definition add (e1: expr) (e2: expr) :=
       addimm n1 (Eop Oadd (t1:::t2:::Enil))
   | add_case7 t1 n2 t2 => (* t1, Eop (Oaddimm n2) (t2:::Enil) *) 
       addimm n2 (Eop Oadd (t1:::t2:::Enil))
-  | add_case8 t1 t2 t3 => (* t1, (Eop Omul (t2:::t3:::Enil)) *) 
-      Eop Omadd (t1:::t2:::t3:::Enil)
   | add_default e1 e2 =>
       Eop Oadd (e1:::e2:::Enil)
   end.