diff options
Diffstat (limited to 'riscV/Asmgenproof.v')
| -rw-r--r-- | riscV/Asmgenproof.v | 42 |
1 files changed, 7 insertions, 35 deletions
diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v index 6abad4ed..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)) -> @@ -166,7 +150,7 @@ Remark transl_cbranch_label: transl_cbranch cond args lbl k = OK c -> tail_nolabel k c. Proof. intros. unfold transl_cbranch in H; destruct cond; TailNoLabel. - all: destruct optR0 as [[]|]; TailNoLabel. + all: destruct optR as [[]|]; simpl in *; TailNoLabel. Qed. Remark transl_op_label: @@ -174,24 +158,12 @@ Remark transl_op_label: transl_op op args r k = OK c -> tail_nolabel k c. Proof. Opaque Int.eq. - unfold transl_op; intros; destruct op; 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. } - all: destruct optR0 as [[]|]; simpl; 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 (Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero)). ++ eapply tail_nolabel_trans; [|apply addptrofs_label]. TailNoLabel. ++ TailNoLabel. Qed. Remark indexed_memory_access_label: |