From 91a07b5ef9935780942a53108ac80ef354a76248 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Sat, 19 Dec 2020 18:40:04 +0100 Subject: Cleanup --- aarch64/Asmblockgenproof0.v | 56 ++++++++++++++++++++++----------------------- 1 file changed, 28 insertions(+), 28 deletions(-) (limited to 'aarch64/Asmblockgenproof0.v') diff --git a/aarch64/Asmblockgenproof0.v b/aarch64/Asmblockgenproof0.v index a47654b8..4217f526 100644 --- a/aarch64/Asmblockgenproof0.v +++ b/aarch64/Asmblockgenproof0.v @@ -200,9 +200,9 @@ Lemma agree_set_pair: agree (Mach.set_pair p v ms) sp (set_pair (map_rpair preg_of p) v' rs). Proof. intros. destruct p; simpl. -- apply agree_set_mreg_parallel; auto. -- apply agree_set_mreg_parallel. apply agree_set_mreg_parallel; auto. - apply Val.hiword_lessdef; auto. apply Val.loword_lessdef; auto. + - apply agree_set_mreg_parallel; auto. + - apply agree_set_mreg_parallel. apply agree_set_mreg_parallel; auto. + apply Val.hiword_lessdef; auto. apply Val.loword_lessdef; auto. Qed. Lemma agree_set_res: @@ -212,12 +212,12 @@ Lemma agree_set_res: agree (Mach.set_res res v ms) sp (set_res (map_builtin_res DR (map_builtin_res dreg_of res)) v' rs). Proof. induction res; simpl; intros. -- eapply agree_set_mreg; eauto. rewrite Pregmap.gss. auto. - intros. apply Pregmap.gso; auto. -- auto. -- apply IHres2. apply IHres1. auto. - apply Val.hiword_lessdef; auto. - apply Val.loword_lessdef; auto. + - eapply agree_set_mreg; eauto. rewrite Pregmap.gss. auto. + intros. apply Pregmap.gso; auto. + - auto. + - apply IHres2. apply IHres1. auto. + apply Val.hiword_lessdef; auto. + apply Val.loword_lessdef; auto. Qed. Lemma agree_undef_regs: @@ -257,15 +257,15 @@ Lemma agree_undef_caller_save_regs: agree (Mach.undef_caller_save_regs ms) sp (undef_caller_save_regs rs). Proof. intros. destruct H. unfold Mach.undef_caller_save_regs, undef_caller_save_regs; split. -- unfold proj_sumbool; rewrite dec_eq_true. auto. -- auto. -- intros. unfold proj_sumbool. rewrite dec_eq_false by (apply preg_of_not_SP). - destruct (List.in_dec preg_eq (preg_of r) (List.map preg_of (List.filter is_callee_save all_mregs))); simpl. -+ apply list_in_map_inv in i. destruct i as (mr & A & B). - assert (r = mr) by (apply preg_of_injective; auto). subst mr; clear A. - apply List.filter_In in B. destruct B as [C D]. rewrite D. auto. -+ destruct (is_callee_save r) eqn:CS; auto. - elim n. apply List.in_map. apply List.filter_In. auto using all_mregs_complete. + - unfold proj_sumbool; rewrite dec_eq_true. auto. + - auto. + - intros. unfold proj_sumbool. rewrite dec_eq_false by (apply preg_of_not_SP). + destruct (List.in_dec preg_eq (preg_of r) (List.map preg_of (List.filter is_callee_save all_mregs))); simpl. + + apply list_in_map_inv in i. destruct i as (mr & A & B). + assert (r = mr) by (apply preg_of_injective; auto). subst mr; clear A. + apply List.filter_In in B. destruct B as [C D]. rewrite D. auto. + + destruct (is_callee_save r) eqn:CS; auto. + elim n. apply List.in_map. apply List.filter_In. auto using all_mregs_complete. Qed. Lemma agree_change_sp: @@ -327,10 +327,10 @@ Lemma extcall_arg_pair_match: exists v', extcall_arg_pair rs m' p v' /\ Val.lessdef v v'. Proof. intros. inv H1. -- exploit extcall_arg_match; eauto. intros (v' & A & B). exists v'; split; auto. constructor; auto. -- exploit extcall_arg_match. eauto. eauto. eexact H2. intros (v1 & A1 & B1). - exploit extcall_arg_match. eauto. eauto. eexact H3. intros (v2 & A2 & B2). - exists (Val.longofwords v1 v2); split. constructor; auto. apply Val.longofwords_lessdef; auto. + - exploit extcall_arg_match; eauto. intros (v' & A & B). exists v'; split; auto. constructor; auto. + - exploit extcall_arg_match. eauto. eauto. eexact H2. intros (v1 & A1 & B1). + exploit extcall_arg_match. eauto. eauto. eexact H3. intros (v2 & A2 & B2). + exists (Val.longofwords v1 v2); split. constructor; auto. apply Val.longofwords_lessdef; auto. Qed. Lemma extcall_args_match: @@ -362,9 +362,9 @@ Lemma set_res_other: set_res (map_builtin_res DR (map_builtin_res dreg_of res)) v rs r = rs r. Proof. induction res; simpl; intros. -- apply Pregmap.gso. red; intros; subst r. rewrite dreg_of_data in H; discriminate. -- auto. -- rewrite IHres2, IHres1; auto. + - apply Pregmap.gso. red; intros; subst r. rewrite dreg_of_data in H; discriminate. + - auto. + - rewrite IHres2, IHres1; auto. Qed. Lemma undef_regs_other: @@ -720,8 +720,8 @@ Lemma exec_straight_opt_step: exec_straight (i :: c) rs1 m1 c' rs3 m3. Proof. intros. inv H0. -- apply exec_straight_one; auto. -- eapply exec_straight_step; eauto. + - apply exec_straight_one; auto. + - eapply exec_straight_step; eauto. Qed. Lemma exec_straight_opt_step_opt: @@ -882,4 +882,4 @@ Proof. intros. inv H0. auto. exploit parent_ra_def; eauto. tauto. Qed. -End MATCH_STACK. \ No newline at end of file +End MATCH_STACK. -- cgit