From 6d2c27127fd67b6ad5499c7d3f4be537333ac356 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Tue, 19 Mar 2019 13:31:57 +0100 Subject: Revert "implemented -fno-postpass normally" This reverts commit fdb8d0c7b5a8be87a64cb995f3abf5bc60f07bfd. --- mppa_k1c/Asmgen.v | 5 +---- mppa_k1c/Asmgenproof.v | 52 +++++++++++++++++--------------------------------- mppa_k1c/SelectOp.v | 6 ------ 3 files changed, 18 insertions(+), 45 deletions(-) (limited to 'mppa_k1c') 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. -- cgit