diff options
Diffstat (limited to 'aarch64/Asmgenproof.v')
-rw-r--r-- | aarch64/Asmgenproof.v | 185 |
1 files changed, 75 insertions, 110 deletions
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 173ce8f8..f0350628 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -1027,6 +1027,12 @@ Ltac destruct_ir0_reg := => unfold ir0 in *; destruct r; find_rwrt_ag; eauto end. +Ltac pc_not_sp := + match goal with + | [ |- ?PC <> ?SP ] + => destruct (PregEq.eq SP PC); repeat congruence; discriminate + end. + Ltac update_x_access_x := subst; rewrite !Pregmap.gss; auto. @@ -1143,91 +1149,52 @@ Lemma exec_basic_simulation: Proof. intros. destruct bi. - - (* PArith *) + { (* PArith *) simpl in *; destruct i. - + (* PArithP *) - destruct i; - try (monadInv TRANSBI); - try (destruct_reg_inv); - exploit next_inst_preserved; eauto; - try (destruct_reg_size). - + (* PArithPP *) + 1,2,3,4,5,6: (* PArithP, PArithPP, PArithPPP, PArithRR0R, PArithRR0, PArithARRRR0 *) destruct i; try (destruct sumbool_rec; try congruence); try (monadInv TRANSBI); try (destruct_reg_inv); try (inv_matchi); try (exploit next_inst_preserved; eauto); - try (repeat destruct_reg_size). - + (* PArithPPP *) - destruct i; - try (monadInv TRANSBI); - try (destruct_reg_inv); - try (inv_matchi); - try (exploit next_inst_preserved; eauto); - try (destruct_reg_size). - + (* PArithRR0R *) - destruct i; - try (monadInv TRANSBI); - try (inv_matchi); - try (exploit next_inst_preserved; eauto); - try (destruct_reg_size); - try (destruct_ir0_reg). - + (* PArithRR0 *) - destruct i; - try (monadInv TRANSBI); - try (inv_matchi); - try (exploit next_inst_preserved; eauto); - try (destruct_reg_size); - try (destruct_ir0_reg). - + (* PArithARRRR0 *) - destruct i; - try (monadInv TRANSBI); - try (inv_matchi); - try (exploit next_inst_preserved; eauto); - try (destruct_reg_size); + try (repeat destruct_reg_size); try (destruct_ir0_reg). - + (* PArithComparisonPP *) - destruct i; - try (monadInv TRANSBI); - try (inv_matchi); - try (destruct_reg_inv); - simpl in *; - inversion BASIC; clear BASIC; subst; - eexists; eexists; split; eauto; - unfold compare_long, compare_int, compare_float, compare_single; - try (destruct_reg_size); - try (destruct_reg_size); - try (destruct_reg_size); - repeat (eapply match_internal_nextinstr_set_parallel; [ congruence | idtac | try (rewrite !AG; congruence)]); - try (econstructor; eauto); - try (eapply nextinstr_agree_but_pc; eauto); - try (eapply ptrofs_nextinstr_agree; eauto). - (* TODO find a solution to avoid destructing a lot of subcases *) - (** destruct sz.*) - (*{ [> Vsingle <]*) - (*try (exploit next_inst_preserved; eauto). intros.*) - (*destruct (rs1 x).*) - (*unfold Asm.nextinstr.*) - (*inversion MATCHI.*) - (*}*) - all:admit. - + (* PArithComparisonR0R *) + { (* PArithComparisonPP *) destruct i; try (monadInv TRANSBI); try (inv_matchi); try (destruct_reg_inv); - try (destruct_reg_size); - simpl in *; - inversion BASIC; clear BASIC; subst; - eexists; eexists; split; eauto; - unfold compare_long, compare_int, compare_float, compare_single; - repeat (eapply match_internal_nextinstr_set_parallel; [ congruence | idtac | try (rewrite !AG; congruence)]); - try (econstructor; eauto); - try (destruct_ir0_reg); - try (eapply nextinstr_agree_but_pc; eauto); - try (eapply ptrofs_nextinstr_agree; eauto). - + (* PArithComparisonP *) + simpl in *. + 1,2: (* compare_long *) + inversion BASIC; clear BASIC; subst; + eexists; eexists; split; eauto; + unfold compare_long; + repeat (eapply match_internal_nextinstr_set_parallel; [ congruence | idtac | try (rewrite !AG; congruence)]); + try (econstructor; eauto); + try (eapply nextinstr_agree_but_pc; eauto); + try (eapply ptrofs_nextinstr_agree; eauto). + + destruct sz. + - (* compare_single *) + unfold compare_single in BASIC. + destruct (rs1 x), (rs1 x0); + inversion BASIC; + eexists; eexists; split; eauto; + repeat (eapply match_internal_nextinstr_set_parallel; [ congruence | idtac | try (rewrite !AG; congruence)]); + try (econstructor; eauto); + try (eapply nextinstr_agree_but_pc; eauto); + try (eapply ptrofs_nextinstr_agree; eauto). + - (* compare_float *) + unfold compare_float in BASIC. + destruct (rs1 x), (rs1 x0); + inversion BASIC; + eexists; eexists; split; eauto; + repeat (eapply match_internal_nextinstr_set_parallel; [ congruence | idtac | try (rewrite !AG; congruence)]); + try (econstructor; eauto); + try (eapply nextinstr_agree_but_pc; eauto); + try (eapply ptrofs_nextinstr_agree; eauto). } + 1,2: (* PArithComparisonR0R, PArithComparisonP *) destruct i; try (monadInv TRANSBI); try (inv_matchi); @@ -1240,22 +1207,23 @@ Proof. try (destruct_reg_size); repeat (eapply match_internal_nextinstr_set_parallel; [ congruence | idtac | try (rewrite !AG; congruence)]); try (econstructor; eauto); + try (destruct_ir0_reg); try (eapply nextinstr_agree_but_pc; eauto); try (eapply ptrofs_nextinstr_agree; eauto). - + (* Pcset *) + { (* Pcset *) try (monadInv TRANSBI); - try (inv_matchi); + try (inv_matchi). try (exploit next_inst_preserved; eauto); - simpl in *; intros; + try (simpl in *; intros; unfold if_opt_bool_val in *; unfold eval_testcond in *; - rewrite <- !AG; try congruence; eauto. - + (* Pfmovi *) + rewrite <- !AG; try congruence; eauto). } + { (* Pfmovi *) try (monadInv TRANSBI); try (inv_matchi); try (destruct_reg_size); try (destruct_ir0_reg); - try (exploit next_inst_preserved; eauto). - + (* Pcsel *) + try (exploit next_inst_preserved; eauto). } + { (* Pcsel *) try (destruct_reg_inv); try (monadInv TRANSBI); try (destruct_reg_inv); @@ -1263,20 +1231,20 @@ Proof. try (exploit next_inst_preserved; eauto); simpl in *; intros; unfold if_opt_bool_val in *; unfold eval_testcond in *; - rewrite <- !AG; try congruence; eauto. - + (* Pfnmul *) + rewrite <- !AG; try congruence; eauto. } + { (* Pfnmul *) try (monadInv TRANSBI); try (inv_matchi); try (destruct_reg_size); try (exploit next_inst_preserved; eauto); - try (find_rwrt_ag). - - (* PLoad *) + try (find_rwrt_ag). } } + { (* PLoad *) destruct ld; monadInv TRANSBI; try destruct_ireg_inv; exploit load_preserved; eauto; - intros; simpl in *; destruct sz; eauto. - - (* PStore *) + intros; simpl in *; destruct sz; eauto. } + { (* PStore *) destruct st; monadInv TRANSBI; try destruct_ireg_inv; exploit store_preserved; eauto; - simpl in *; inv_matchi; find_rwrt_ag. - - (* Pallocframe *) + simpl in *; inv_matchi; find_rwrt_ag. } + { (* Pallocframe *) monadInv TRANSBI. simpl in *. inversion MATCHI; subst; @@ -1287,36 +1255,33 @@ Proof. (* TODO find a way to complete this proof *) + eexists; eexists; split; eauto. repeat (eapply match_internal_nextinstr_set_parallel; [ try congruence | idtac | try reflexivity ]). - destruct (PregEq.eq SP PC); try (repeat congruence); discriminate. - -- admit. - -- eapply AG; destruct (PregEq.eq SP PC); try (repeat congruence); discriminate. + pc_not_sp. + -- econstructor; eauto. + all:admit. + -- eapply AG; pc_not_sp. + repeat (econstructor; eauto). admit. (* TODO *) - all:admit. - - (* Pfreeframe *) + all:admit. } + { (* Pfreeframe *) (* TODO seems similar as the above subcase *) - all:admit. - - (* Ploadsymbol *) - try (monadInv TRANSBI); - try (inv_matchi); - try (exploit next_inst_preserved; eauto); - rewrite symbol_addresses_preserved; eauto. - - (* Pcvtsw2x *) - try (monadInv TRANSBI); - try (inv_matchi); - try (exploit next_inst_preserved; eauto); - try (find_rwrt_ag). - - (* Pcvtuw2x *) - try (monadInv TRANSBI); - try (inv_matchi); - try (exploit next_inst_preserved; eauto); - try (find_rwrt_ag). - - (* Pcvtx2w *) + 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. } + 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. |