From 18312f0470cfb96e44ae1a26a24710cc1df3440d Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Fri, 9 Apr 2021 15:15:57 +0200 Subject: Removing expansions from Asmgen --- riscV/Asmgenproof.v | 162 +--------------------------------------------------- 1 file changed, 3 insertions(+), 159 deletions(-) (limited to 'riscV/Asmgenproof.v') diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v index 509eac94..4af8352c 100644 --- a/riscV/Asmgenproof.v +++ b/riscV/Asmgenproof.v @@ -115,14 +115,6 @@ Qed. Section TRANSL_LABEL. -Remark loadimm32_label: - forall r n k, tail_nolabel k (loadimm32 r n k). -Proof. - intros; unfold loadimm32. destruct (make_immed32 n); TailNoLabel. - unfold load_hilo32. destruct (Int.eq lo Int.zero); TailNoLabel. -Qed. -Hint Resolve loadimm32_label: labels. - Remark opimm32_label: forall op opimm r1 r2 n k, (forall r1 r2 r3, nolabel (op r1 r2 r3)) -> @@ -134,14 +126,6 @@ Proof. Qed. Hint Resolve opimm32_label: labels. -Remark loadimm64_label: - forall r n k, tail_nolabel k (loadimm64 r n k). -Proof. - intros; unfold loadimm64. destruct (make_immed64 n); TailNoLabel. - unfold load_hilo64. destruct (Int64.eq lo Int64.zero); TailNoLabel. -Qed. -Hint Resolve loadimm64_label: labels. - Remark opimm64_label: forall op opimm r1 r2 n k, (forall r1 r2 r3, nolabel (op r1 r2 r3)) -> @@ -161,165 +145,25 @@ Proof. Qed. Hint Resolve addptrofs_label: labels. -Remark transl_cond_float_nolabel: - forall c r1 r2 r3 insn normal, - transl_cond_float c r1 r2 r3 = (insn, normal) -> nolabel insn. -Proof. - unfold transl_cond_float; intros. destruct c; inv H; exact I. -Qed. - -Remark transl_cond_single_nolabel: - forall c r1 r2 r3 insn normal, - transl_cond_single c r1 r2 r3 = (insn, normal) -> nolabel insn. -Proof. - unfold transl_cond_single; intros. destruct c; inv H; exact I. - Qed. - Remark transl_cbranch_label: forall cond args lbl k c, transl_cbranch cond args lbl k = OK c -> tail_nolabel k c. Proof. intros. unfold transl_cbranch in H; destruct cond; TailNoLabel. -- destruct c0; simpl; TailNoLabel. -- destruct c0; simpl; TailNoLabel. -- destruct (Int.eq n Int.zero). - destruct c0; simpl; TailNoLabel. - apply tail_nolabel_trans with (transl_cbranch_int32s c0 x X31 lbl :: k). - auto with labels. destruct c0; simpl; TailNoLabel. -- destruct (Int.eq n Int.zero). - destruct c0; simpl; TailNoLabel. - apply tail_nolabel_trans with (transl_cbranch_int32u c0 x X31 lbl :: k). - auto with labels. destruct c0; simpl; TailNoLabel. -- destruct c0; simpl; TailNoLabel. -- destruct c0; simpl; TailNoLabel. -- destruct (Int64.eq n Int64.zero). - destruct c0; simpl; TailNoLabel. - apply tail_nolabel_trans with (transl_cbranch_int64s c0 x X31 lbl :: k). - auto with labels. destruct c0; simpl; TailNoLabel. -- destruct (Int64.eq n Int64.zero). - destruct c0; simpl; TailNoLabel. - apply tail_nolabel_trans with (transl_cbranch_int64u c0 x X31 lbl :: k). - auto with labels. destruct c0; simpl; TailNoLabel. -- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:F; inv EQ2. - apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. - destruct normal; TailNoLabel. -- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:F; inv EQ2. - apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. - destruct normal; TailNoLabel. -- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:F; inv EQ2. - apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. - destruct normal; TailNoLabel. -- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:F; inv EQ2. - apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. - destruct normal; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. + all: destruct optR as [[]|]; simpl in *; TailNoLabel. Qed. -Remark transl_cond_op_label: - forall cond args r k c, - transl_cond_op cond r args k = OK c -> tail_nolabel k c. -Proof. - intros. unfold transl_cond_op in H; destruct cond; TailNoLabel. -- destruct c0; simpl; TailNoLabel. -- destruct c0; simpl; TailNoLabel. -- unfold transl_condimm_int32s. - destruct (Int.eq n Int.zero). -+ destruct c0; simpl; TailNoLabel. -+ destruct c0; simpl. -* eapply tail_nolabel_trans; [apply opimm32_label; intros; exact I | TailNoLabel]. -* eapply tail_nolabel_trans; [apply opimm32_label; intros; exact I | TailNoLabel]. -* apply opimm32_label; intros; exact I. -* destruct (Int.eq n (Int.repr Int.max_signed)). apply loadimm32_label. apply opimm32_label; intros; exact I. -* eapply tail_nolabel_trans. apply loadimm32_label. TailNoLabel. -* eapply tail_nolabel_trans. apply loadimm32_label. TailNoLabel. -- unfold transl_condimm_int32u. - destruct (Int.eq n Int.zero). -+ destruct c0; simpl; TailNoLabel. -+ destruct c0; simpl; - try (eapply tail_nolabel_trans; [apply loadimm32_label | TailNoLabel]). - apply opimm32_label; intros; exact I. -- destruct c0; simpl; TailNoLabel. - - destruct c0; simpl; TailNoLabel. -- unfold transl_condimm_int64s. - destruct (Int64.eq n Int64.zero). -+ destruct c0; simpl; TailNoLabel. -+ destruct c0; simpl. -* eapply tail_nolabel_trans; [apply opimm64_label; intros; exact I | TailNoLabel]. -* eapply tail_nolabel_trans; [apply opimm64_label; intros; exact I | TailNoLabel]. -* apply opimm64_label; intros; exact I. -* destruct (Int64.eq n (Int64.repr Int64.max_signed)). apply loadimm32_label. apply opimm64_label; intros; exact I. -* eapply tail_nolabel_trans. apply loadimm64_label. TailNoLabel. -* eapply tail_nolabel_trans. apply loadimm64_label. TailNoLabel. -- unfold transl_condimm_int64u. - destruct (Int64.eq n Int64.zero). -+ destruct c0; simpl; TailNoLabel. -+ destruct c0; simpl; - try (eapply tail_nolabel_trans; [apply loadimm64_label | TailNoLabel]). - apply opimm64_label; intros; exact I. -- destruct (transl_cond_float c0 r x x0) as [insn normal] eqn:F; inv EQ2. - apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. - destruct normal; TailNoLabel. -- destruct (transl_cond_float c0 r x x0) as [insn normal] eqn:F; inv EQ2. - apply tail_nolabel_cons. eapply transl_cond_float_nolabel; eauto. - destruct normal; TailNoLabel. -- destruct (transl_cond_single c0 r x x0) as [insn normal] eqn:F; inv EQ2. - apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. - destruct normal; TailNoLabel. -- destruct (transl_cond_single c0 r x x0) as [insn normal] eqn:F; inv EQ2. - apply tail_nolabel_cons. eapply transl_cond_single_nolabel; eauto. - destruct normal; TailNoLabel. - Qed. - Remark transl_op_label: forall op args r k c, transl_op op args r k = OK c -> tail_nolabel k c. Proof. Opaque Int.eq. - unfold transl_op; intros; destruct op; TailNoLabel. + unfold transl_op; intros; destruct op; TailNoLabel; + try (destruct optR as [[]|]; simpl in *; TailNoLabel). - destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel. -- destruct (Float.eq_dec n Float.zero); TailNoLabel. -- destruct (Float32.eq_dec n Float32.zero); TailNoLabel. - destruct (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)). + eapply tail_nolabel_trans; [|apply addptrofs_label]. TailNoLabel. + TailNoLabel. -- apply opimm32_label; intros; exact I. -- apply opimm32_label; intros; exact I. -- apply opimm32_label; intros; exact I. -- apply opimm32_label; intros; exact I. -- destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel. -- apply opimm64_label; intros; exact I. -- apply opimm64_label; intros; exact I. -- apply opimm64_label; intros; exact I. -- apply opimm64_label; intros; exact I. -- destruct (Int.eq n Int.zero); try destruct (Int.eq n Int.one); TailNoLabel. -- eapply transl_cond_op_label; eauto. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. -- destruct optR as [[]|]; simpl in *; TailNoLabel. Qed. Remark indexed_memory_access_label: -- cgit