diff options
Diffstat (limited to 'mppa_k1c/Asmgenproof.v')
| -rw-r--r-- | mppa_k1c/Asmgenproof.v | 52 |
1 files changed, 17 insertions, 35 deletions
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. |