From 341d1123c475e3fb73032e2f6c6a337c4e2c59c1 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 16 Dec 2020 14:48:50 +0100 Subject: intermediatet commit before builtins --- aarch64/Asmblockprops.v | 104 ++++++++++++++++++++++++------------------------ 1 file changed, 52 insertions(+), 52 deletions(-) (limited to 'aarch64/Asmblockprops.v') diff --git a/aarch64/Asmblockprops.v b/aarch64/Asmblockprops.v index d1015ea9..cef95aad 100644 --- a/aarch64/Asmblockprops.v +++ b/aarch64/Asmblockprops.v @@ -39,7 +39,13 @@ Lemma preg_of_data: Proof. intros. destruct r; reflexivity. Qed. -Hint Resolve preg_of_data: asmgen. + +Lemma dreg_of_data: + forall r, data_preg (dreg_of r) = true. +Proof. + intros. destruct r; reflexivity. +Qed. +Hint Resolve preg_of_data dreg_of_data: asmgen. Lemma data_diff: forall r r', @@ -55,6 +61,12 @@ Proof. intros. apply data_diff; auto with asmgen. Qed. +Lemma preg_of_not_SP: + forall r, preg_of r <> SP. +Proof. + intros. unfold preg_of; destruct r; simpl; try discriminate. +Qed. + (* Lemma preg_of_not_SP: forall r, preg_of r <> SP. @@ -81,73 +93,61 @@ Lemma nextblock_inv1: forall b r rs, data_preg r = true -> (nextblock b rs)#r = rs#r. Proof. intros. apply nextblock_inv. red; intro; subst; discriminate. -Qed. +Qed.*) + +Ltac desif := + repeat match goal with + | [ |- context[ if ?f then _ else _ ] ] => destruct f + end. + +Ltac decomp := + repeat match goal with + | [ |- context[ match (?rs ?r) with | _ => _ end ] ] => destruct (rs r) + end. Ltac Simplif := - ((rewrite nextblock_inv by eauto with asmgen) - || (rewrite nextblock_inv1 by eauto with asmgen) + ((desif) + || (try unfold compare_long) + || (try unfold compare_int) + || (try unfold compare_float) + || (try unfold compare_single) + || decomp || (rewrite Pregmap.gss) - || (rewrite nextblock_pc) || (rewrite Pregmap.gso by eauto with asmgen) ); auto with asmgen. Ltac Simpl := repeat Simplif. +Section EPC. + +Variable lk: aarch64_linker. + (* For Asmblockgenproof0 *) Theorem exec_basic_instr_pc: forall ge b rs1 m1 rs2 m2, - exec_basic_instr ge b rs1 m1 = Next rs2 m2 -> + exec_basic lk ge b rs1 m1 = Next rs2 m2 -> rs2 PC = rs1 PC. Proof. - intros. destruct b; try destruct i; try destruct i. - all: try (inv H; Simpl). - 1-10: unfold parexec_load_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail. - - 1-20: unfold parexec_load_reg, parexec_load_regxs in H1; destruct (Mem.loadv _ _ _); unfold parexec_incorrect_load in *; destruct trap; try discriminate; unfold concrete_default_notrap_load_value in *; inv H1; Simpl; fail. - - { (* PLoadQRRO *) - unfold parexec_load_q_offset in H1. - destruct (gpreg_q_expand _) as [r0 r1] in H1. - destruct (Mem.loadv _ _ _) in H1; try discriminate. - destruct (Mem.loadv _ _ _) in H1; try discriminate. - inv H1. Simpl. } - { (* PLoadORRO *) - unfold parexec_load_o_offset in H1. - destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1. - destruct (Mem.loadv _ _ _) in H1; try discriminate. - destruct (Mem.loadv _ _ _) in H1; try discriminate. - destruct (Mem.loadv _ _ _) in H1; try discriminate. - destruct (Mem.loadv _ _ _) in H1; try discriminate. - inv H1. Simpl. } - 1-8: unfold parexec_store_offset in H1; destruct (eval_offset ofs); try discriminate; destruct (Mem.storev _ _ _); [inv H1; auto | discriminate]; fail. - 1-8: unfold parexec_store_reg in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]; auto; fail. - 1-8: unfold parexec_store_regxs in H1; destruct (Mem.storev _ _ _); [inv H1; Simpl | discriminate]; auto; fail. - - { (* PStoreQRRO *) - unfold parexec_store_q_offset in H1. - destruct (gpreg_q_expand _) as [r0 r1] in H1. - unfold eval_offset in H1; try discriminate. - destruct (Mem.storev _ _ _) in H1; try discriminate. - destruct (Mem.storev _ _ _) in H1; try discriminate. - inv H1. Simpl. reflexivity. } - { (* PStoreORRO *) - unfold parexec_store_o_offset in H1. - destruct (gpreg_o_expand _) as [[[r0 r1] r2] r3] in H1. - unfold eval_offset in H1; try discriminate. - destruct (Mem.storev _ _ _) in H1; try discriminate. - destruct (Mem.storev _ _ _) in H1; try discriminate. - destruct (Mem.storev _ _ _) in H1; try discriminate. - destruct (Mem.storev _ _ _) in H1; try discriminate. - inv H1. Simpl. reflexivity. } - - destruct (Mem.alloc _ _ _). destruct (Mem.store _ _ _ _ _). inv H1. Simpl. discriminate. - - destruct (Mem.loadv _ _ _); try discriminate. destruct (rs1 _); try discriminate. - destruct (Mem.free _ _ _ _). inv H1. Simpl. discriminate. - - destruct rs; try discriminate. inv H1. Simpl. - - destruct rd; try discriminate. inv H1; Simpl. - - reflexivity. + intros. destruct b; try destruct i; try destruct i; try destruct ld; try destruct ld; + try destruct st; try destruct st; try destruct a. + all: try (inv H; simpl in *; auto; Simpl). + all: try (try unfold exec_load_rd_a in H1; try destruct (Mem.loadv _ _ _); inv H1; Simpl). + all: try (try unfold exec_load_double in H0; destruct (Mem.loadv _ _ _); simpl in *; + try destruct (Mem.loadv _ _ _); simpl in *; inv H0; Simpl). + all: try (try unfold exec_store_rs_a in H0; try destruct (Mem.storev _ _ _); inv H0; auto; Simpl). + all: try (try unfold exec_store_double in H1; destruct (Mem.storev _ _ _); simpl in *; + try destruct (Mem.storev _ _ _); simpl in *; inv H1; auto; Simpl). + - (* alloc *) + destruct (Mem.alloc _ _ _); destruct (Mem.store _ _ _); inv H1; auto; Simpl. + - (* free *) + destruct (rs1 SP); try discriminate; destruct (Mem.free _ _ _ _); inv H1; Simpl. Qed. +End EPC. + +(* + (* For PostpassSchedulingproof *) Lemma regset_double_set: -- cgit