From ce1bdcf3da6b5b1d30c344c5f75bcd06c7178d09 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 16 Oct 2020 12:17:21 +0200 Subject: exec_basic_simulation proof OK --- aarch64/Asmgenproof.v | 55 +++++++++++++++++++++------------------------------ 1 file changed, 23 insertions(+), 32 deletions(-) (limited to 'aarch64') diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index f0350628..b26e8d4c 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -1245,45 +1245,36 @@ Proof. destruct st; monadInv TRANSBI; try destruct_ireg_inv; exploit store_preserved; eauto; simpl in *; inv_matchi; find_rwrt_ag. } { (* Pallocframe *) - monadInv TRANSBI. - simpl in *. - inversion MATCHI; subst; - destruct Mem.alloc; - destruct Mem.store in BASIC; - inversion BASIC; subst; clear BASIC. - destruct Mem.store. - (* TODO find a way to complete this proof *) - + eexists; eexists; split; eauto. - repeat (eapply match_internal_nextinstr_set_parallel; [ try congruence | idtac | try reflexivity ]). - pc_not_sp. - -- econstructor; eauto. - all:admit. - -- eapply AG; pc_not_sp. - + repeat (econstructor; eauto). - admit. - - (* TODO *) - all:admit. } + monadInv TRANSBI; + inv_matchi; try pc_not_sp; + destruct sz eqn:EQSZ; + destruct Mem.alloc eqn:EQALLOC; + destruct Mem.store eqn:EQSTORE; inversion BASIC; try pc_not_sp; + eexists; eexists; split; eauto; + repeat (eapply match_internal_nextinstr_set_parallel; [ try (pc_not_sp; congruence) | idtac | try (reflexivity)]); + try (econstructor; eauto); + try (eapply nextinstr_agree_but_pc; eauto); + try (eapply ptrofs_nextinstr_agree; eauto). } { (* Pfreeframe *) - (* TODO seems similar as the above subcase *) - monadInv TRANSBI. - simpl in *. - inversion MATCHI; subst; - destruct Mem.loadv in BASIC; - inversion BASIC; subst; clear BASIC. - destruct Mem.loadv. - (* TODO find a way to complete this proof *) - + eexists; eexists; split; eauto. - repeat (eapply match_internal_nextinstr_set_parallel; [ try congruence | idtac | try reflexivity ]). - all:admit. - + all:admit. } + monadInv TRANSBI; + inv_matchi; try pc_not_sp; + destruct sz eqn:EQSZ; + destruct Mem.loadv eqn:EQLOAD; + destruct (rs1 SP) eqn:EQRS1SP; + try (destruct Mem.free eqn:EQFREE); + inversion BASIC; try pc_not_sp; + eexists; eexists; split; eauto; + repeat (eapply match_internal_nextinstr_set_parallel; [ try (pc_not_sp; congruence) | idtac | try (reflexivity)]); + try (econstructor; eauto); + try (eapply nextinstr_agree_but_pc; eauto); + try (eapply ptrofs_nextinstr_agree; eauto). } 1,2,3,4: (* Ploadsymbol, Pcvtsw2x, Pcvtuw2x, Pcvtx2w *) try (monadInv TRANSBI); try (inv_matchi); try (exploit next_inst_preserved; eauto); rewrite symbol_addresses_preserved; eauto; try (find_rwrt_ag). -Admitted. +Qed. Lemma exec_body_simulation_star': forall b ofs f bb tc bis end_of_body rs_start m_start s_start rs_end m_end -- cgit