implemented -fno-postpass normally

3 files changed, 45 insertions, 18 deletions

diff --git a/mppa_k1c/Asmgen.v b/mppa_k1c/Asmgen.v
index 58e80be1..46714496 100644
--- a/mppa_k1c/Asmgen.v
+++ b/mppa_k1c/Asmgen.v
@@ -19,13 +19,16 @@ 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' <- PostpassScheduling.transf_program abp;
+    do abp' <- if Compopts.optim_postpass tt
+               then PostpassScheduling.transf_program abp
+               else OK 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 588019a2..918403cd 100644
--- a/mppa_k1c/Asmgenproof.v
+++ b/mppa_k1c/Asmgenproof.v
@@ -17,15 +17,18 @@ 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
-  ::: mkpass PostpassSchedulingproof.match_prog
-  ::: mkpass Asm.match_prog
-  ::: pass_nil _.
+  ::: if Compopts.optim_postpass tt
+      then mkpass PostpassSchedulingproof.match_prog
+           ::: mkpass Asm.match_prog
+           ::: pass_nil _
+      else mkpass Asm.match_prog ::: pass_nil _.
 
 Definition match_prog := pass_match (compose_passes block_passes).
 
@@ -36,11 +39,16 @@ 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.
-  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.
+  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.
 Qed.
 
 (** Return Address Offset *)
@@ -149,15 +157,25 @@ 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. 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.
+  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.
 Qed.
 
 End PRESERVATION.
diff --git a/mppa_k1c/SelectOp.v b/mppa_k1c/SelectOp.v
index edb07e5f..66615f1d 100644
--- a/mppa_k1c/SelectOp.v
+++ b/mppa_k1c/SelectOp.v
@@ -123,6 +123,8 @@ 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.
 >>
@@ -136,6 +138,7 @@ 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) :=
@@ -147,6 +150,7 @@ 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.
 
@@ -166,6 +170,8 @@ 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.