diff options
author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-11-25 16:34:02 +0100 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2020-11-25 16:34:02 +0100 |
commit | fbe134640de11d69cef417e2e59e2e2669ccc7ad (patch) | |
tree | 3b27db2cc29ab938f89926883837fcc835f27ee5 /aarch64 | |
parent | 1975837dbd2b3a924bc77fd4e64cce0a37c21994 (diff) | |
download | compcert-kvx-fbe134640de11d69cef417e2e59e2e2669ccc7ad.tar.gz compcert-kvx-fbe134640de11d69cef417e2e59e2e2669ccc7ad.zip |
Preservation proof with post pass scheduling in Asmgenproof almost done
Diffstat (limited to 'aarch64')
-rw-r--r-- | aarch64/Asmgenproof.v | 17 | ||||
-rw-r--r-- | aarch64/PostpassSchedulingproof.v | 11 |
2 files changed, 14 insertions, 14 deletions
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index c41d0a0b..f441f20e 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -2241,21 +2241,22 @@ Let tge := Genv.globalenv tprog. Theorem transf_program_correct: forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog). Proof. -Admitted. -(* TODO unfold match_prog in TRANSF. simpl in TRANSF. inv TRANSF. inv H. inv H1. inv H. inv H2. inv H. inv H3. inv H. inv H4. inv H. eapply compose_forward_simulations. { exploit Machblockgenproof.transf_program_correct; eauto. } + eapply compose_forward_simulations. + apply PseudoAsmblockproof.transf_program_correct; eauto. - intros; apply Asmblockgenproof.next_progress. - - intros. eapply .functions_bound_max_pos; eauto. - { intros. eapply Asmblock_PRESERVATION.symbol_high_low. eauto. } - + eapply compose_forward_simulations. apply Asmblockgenproof.transf_program_correct; eauto. - { intros; eapply Asmblock_PRESERVATION.symbol_high_low; eauto. } - apply Asmblock_PRESERVATION.transf_program_correct. eauto. -Qed.*) + - intros. eapply Asmblockgenproof.functions_bound_max_pos; eauto. admit. +(* { intros. eapply Asmblock_PRESERVATION.symbol_high_low; eauto. } *) + + eapply compose_forward_simulations. apply Asmblockgenproof.transf_program_correct; eauto. admit. +(* { intros; eapply Asmblock_PRESERVATION.symbol_high_low; eauto. } *) + eapply compose_forward_simulations. + - apply PostpassSchedulingproof.transf_program_correct; eauto. + - apply Asmblock_PRESERVATION.transf_program_correct; eauto. +Admitted. End PRESERVATION. diff --git a/aarch64/PostpassSchedulingproof.v b/aarch64/PostpassSchedulingproof.v index c32579a2..48840602 100644 --- a/aarch64/PostpassSchedulingproof.v +++ b/aarch64/PostpassSchedulingproof.v @@ -24,7 +24,7 @@ Require Import Axioms. Local Open Scope error_monad_scope. -Definition match_prog (p tp: Asmblock.program) := +Definition match_prog (p tp: program) := match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. Lemma transf_program_match: @@ -462,21 +462,20 @@ Proof. + eapply exec_step_external; eauto. Qed. -End PRESERVATION_ASMVLIW. +End PRESERVATION_ASMVLIW.*) Section PRESERVATION. +Variable lk: aarch64_linker. Variables prog tprog: program. Hypothesis TRANSL: match_prog prog tprog. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. Theorem transf_program_correct: - forward_simulation (Asmblock.semantics prog) (Asmvliw.semantics tprog). + forward_simulation (Asmblock.semantics lk prog) (Asmblock.semantics lk tprog). Proof. - eapply compose_forward_simulations. eapply transf_program_correct_Asmblock; eauto. - eapply transf_program_correct_Asmvliw; eauto. Qed. -End PRESERVATION.*) +End PRESERVATION. |