diff options
| author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-06 16:53:46 +0100 |
|---|---|---|
| committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-06 16:53:46 +0100 |
| commit | acb41b1af6e5e4c933e3be1b17f6e5012eca794d (patch) | |
| tree | db57a6b2543871312a952ffa2e462e35aef674e0 /riscV/Asmgenproof.v | |
| parent | 29ba37cc21cedc09b20bbd8adfa0ec52c48365c0 (diff) | |
| download | compcert-kvx-acb41b1af6e5e4c933e3be1b17f6e5012eca794d.tar.gz compcert-kvx-acb41b1af6e5e4c933e3be1b17f6e5012eca794d.zip | |
cond and branches expanded
Diffstat (limited to 'riscV/Asmgenproof.v')
| -rw-r--r-- | riscV/Asmgenproof.v | 28 |
1 files changed, 20 insertions, 8 deletions
diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v index 6bacaa5c..52a3bf27 100644 --- a/riscV/Asmgenproof.v +++ b/riscV/Asmgenproof.v @@ -161,7 +161,7 @@ Proof. Qed. Hint Resolve addptrofs_label: labels. -Remark transl_cond_float_nolabel: +(* TODO REMOVE Remark transl_cond_float_nolabel: forall c r1 r2 r3 insn normal, transl_cond_float c r1 r2 r3 = (insn, normal) -> nolabel insn. Proof. @@ -173,14 +173,14 @@ Remark transl_cond_single_nolabel: transl_cond_single c r1 r2 r3 = (insn, normal) -> nolabel insn. Proof. unfold transl_cond_single; intros. destruct c; inv H; exact I. -Qed. + 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. + (* TODO REMOVE - destruct c0; simpl; TailNoLabel. - destruct c0; simpl; TailNoLabel. - destruct (Int.eq n Int.zero). destruct c0; simpl; TailNoLabel. @@ -211,15 +211,27 @@ Proof. 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 normal; TailNoLabel.*) +- destruct optR0 as [[]|]; TailNoLabel. +- destruct optR0 as [[]|]; TailNoLabel. +- destruct optR0 as [[]|]; TailNoLabel. +- destruct optR0 as [[]|]; TailNoLabel. +- destruct optR0 as [[]|]; TailNoLabel. +- destruct optR0 as [[]|]; TailNoLabel. +- destruct optR0 as [[]|]; TailNoLabel. +- destruct optR0 as [[]|]; TailNoLabel. +- destruct optR0 as [[]|]; TailNoLabel. +- destruct optR0 as [[]|]; TailNoLabel. +- destruct optR0 as [[]|]; TailNoLabel. +- destruct optR0 as [[]|]; TailNoLabel. Qed. -(* TODO Remark transl_cond_op_label: +(* TODO REMOVE 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. - (* TODO - destruct c0; simpl; TailNoLabel. +- destruct c0; simpl; TailNoLabel. - destruct c0; simpl; TailNoLabel. - unfold transl_condimm_int32s. destruct (Int.eq n Int.zero). @@ -254,7 +266,7 @@ Proof. + destruct c0; simpl; TailNoLabel. + destruct c0; simpl; try (eapply tail_nolabel_trans; [apply loadimm64_label | TailNoLabel]). - apply opimm64_label; intros; exact I.*) + 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. @@ -291,7 +303,7 @@ Opaque Int.eq. - 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. -(* TODO - eapply transl_cond_op_label; eauto.*) +(* TODO REMOVE - eapply transl_cond_op_label; eauto.*) - destruct optR0 as [[]|]; simpl; TailNoLabel. - destruct optR0 as [[]|]; simpl; TailNoLabel. - destruct optR0 as [[]|]; simpl; TailNoLabel. |