From 6bff68d55932bdc4715741a973724317c639b833 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 2 Mar 2021 12:13:19 +0100 Subject: Merge conflicts solved and cleaning in Asmgenproof after expansion --- riscV/Asmgen.v | 253 ---------------- riscV/Asmgenproof.v | 164 ++-------- riscV/Asmgenproof1.v | 834 ++++++--------------------------------------------- riscV/Op.v | 3 +- 4 files changed, 106 insertions(+), 1148 deletions(-) (limited to 'riscV') diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index 252a9270..957166b6 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -105,8 +105,6 @@ Definition addimm32 := opimm32 Paddw Paddiw. Definition andimm32 := opimm32 Pandw Pandiw. Definition orimm32 := opimm32 Porw Poriw. Definition xorimm32 := opimm32 Pxorw Pxoriw. -Definition sltimm32 := opimm32 Psltw Psltiw. -Definition sltuimm32 := opimm32 Psltuw Psltiuw. Definition load_hilo64 (r: ireg) (hi lo: int64) k := if Int64.eq lo Int64.zero then Pluil r hi :: k @@ -132,8 +130,6 @@ Definition addimm64 := opimm64 Paddl Paddil. Definition andimm64 := opimm64 Pandl Pandil. Definition orimm64 := opimm64 Porl Poril. Definition xorimm64 := opimm64 Pxorl Pxoril. -Definition sltimm64 := opimm64 Psltl Psltil. -Definition sltuimm64 := opimm64 Psltul Psltiul. Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) := if Ptrofs.eq_dec n Ptrofs.zero then @@ -145,66 +141,6 @@ Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) := (** Translation of conditional branches. *) -Definition transl_cbranch_int32s (cmp: comparison) (r1 r2: ireg0) (lbl: label) := - match cmp with - | Ceq => Pbeqw r1 r2 lbl - | Cne => Pbnew r1 r2 lbl - | Clt => Pbltw r1 r2 lbl - | Cle => Pbgew r2 r1 lbl - | Cgt => Pbltw r2 r1 lbl - | Cge => Pbgew r1 r2 lbl - end. - -Definition transl_cbranch_int32u (cmp: comparison) (r1 r2: ireg0) (lbl: label) := - match cmp with - | Ceq => Pbeqw r1 r2 lbl - | Cne => Pbnew r1 r2 lbl - | Clt => Pbltuw r1 r2 lbl - | Cle => Pbgeuw r2 r1 lbl - | Cgt => Pbltuw r2 r1 lbl - | Cge => Pbgeuw r1 r2 lbl - end. - -Definition transl_cbranch_int64s (cmp: comparison) (r1 r2: ireg0) (lbl: label) := - match cmp with - | Ceq => Pbeql r1 r2 lbl - | Cne => Pbnel r1 r2 lbl - | Clt => Pbltl r1 r2 lbl - | Cle => Pbgel r2 r1 lbl - | Cgt => Pbltl r2 r1 lbl - | Cge => Pbgel r1 r2 lbl - end. - -Definition transl_cbranch_int64u (cmp: comparison) (r1 r2: ireg0) (lbl: label) := - match cmp with - | Ceq => Pbeql r1 r2 lbl - | Cne => Pbnel r1 r2 lbl - | Clt => Pbltul r1 r2 lbl - | Cle => Pbgeul r2 r1 lbl - | Cgt => Pbltul r2 r1 lbl - | Cge => Pbgeul r1 r2 lbl - end. - -Definition transl_cond_float (cmp: comparison) (rd: ireg) (fs1 fs2: freg) := - match cmp with - | Ceq => (Pfeqd rd fs1 fs2, true) - | Cne => (Pfeqd rd fs1 fs2, false) - | Clt => (Pfltd rd fs1 fs2, true) - | Cle => (Pfled rd fs1 fs2, true) - | Cgt => (Pfltd rd fs2 fs1, true) - | Cge => (Pfled rd fs2 fs1, true) - end. - -Definition transl_cond_single (cmp: comparison) (rd: ireg) (fs1 fs2: freg) := - match cmp with - | Ceq => (Pfeqs rd fs1 fs2, true) - | Cne => (Pfeqs rd fs1 fs2, false) - | Clt => (Pflts rd fs1 fs2, true) - | Cle => (Pfles rd fs1 fs2, true) - | Cgt => (Pflts rd fs2 fs1, true) - | Cge => (Pfles rd fs2 fs1, true) - end. - Definition apply_bin_r0_r0r0lbl (optR0: option bool) (sem: ireg0 -> ireg0 -> label -> instruction) (r1 r2: ireg0) (lbl: label) := match optR0 with | None => sem r1 r2 lbl @@ -222,59 +158,6 @@ Definition apply_bin_r0_r0r0 (optR0: option bool) (sem: ireg0 -> ireg0 -> instru Definition transl_cbranch (cond: condition) (args: list mreg) (lbl: label) (k: code) := match cond, args with - | Ccomp c, a1 :: a2 :: nil => - do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (transl_cbranch_int32s c r1 r2 lbl :: k) - | Ccompu c, a1 :: a2 :: nil => - do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (transl_cbranch_int32u c r1 r2 lbl :: k) - | Ccompimm c n, a1 :: nil => - do r1 <- ireg_of a1; - OK (if Int.eq n Int.zero then - transl_cbranch_int32s c r1 X0 lbl :: k - else - loadimm32 X31 n (transl_cbranch_int32s c r1 X31 lbl :: k)) - | Ccompuimm c n, a1 :: nil => - do r1 <- ireg_of a1; - OK (if Int.eq n Int.zero then - transl_cbranch_int32u c r1 X0 lbl :: k - else - loadimm32 X31 n (transl_cbranch_int32u c r1 X31 lbl :: k)) - | Ccompl c, a1 :: a2 :: nil => - do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (transl_cbranch_int64s c r1 r2 lbl :: k) - | Ccomplu c, a1 :: a2 :: nil => - do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (transl_cbranch_int64u c r1 r2 lbl :: k) - | Ccomplimm c n, a1 :: nil => - do r1 <- ireg_of a1; - OK (if Int64.eq n Int64.zero then - transl_cbranch_int64s c r1 X0 lbl :: k - else - loadimm64 X31 n (transl_cbranch_int64s c r1 X31 lbl :: k)) - | Ccompluimm c n, a1 :: nil => - do r1 <- ireg_of a1; - OK (if Int64.eq n Int64.zero then - transl_cbranch_int64u c r1 X0 lbl :: k - else - loadimm64 X31 n (transl_cbranch_int64u c r1 X31 lbl :: k)) - | Ccompf c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_float c X31 r1 r2 in - OK (insn :: (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) :: k) - | Cnotcompf c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_float c X31 r1 r2 in - OK (insn :: (if normal then Pbeqw X31 X0 lbl else Pbnew X31 X0 lbl) :: k) - | Ccompfs c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_single c X31 r1 r2 in - OK (insn :: (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) :: k) - | Cnotcompfs c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_single c X31 r1 r2 in - OK (insn :: (if normal then Pbeqw X31 X0 lbl else Pbnew X31 X0 lbl) :: k) - | CEbeqw optR0, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; OK (apply_bin_r0_r0r0lbl optR0 Pbeqw r1 r2 lbl :: k) @@ -327,133 +210,6 @@ Definition transl_cbranch Error(msg "Asmgen.transl_cond_branch") end. -(** Translation of a condition operator. The generated code sets the - [rd] target register to 0 or 1 depending on the truth value of the - condition. *) - -Definition transl_cond_int32s (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) := - match cmp with - | Ceq => Pseqw rd r1 r2 :: k - | Cne => Psnew rd r1 r2 :: k - | Clt => Psltw rd r1 r2 :: k - | Cle => Psltw rd r2 r1 :: Pxoriw rd rd Int.one :: k - | Cgt => Psltw rd r2 r1 :: k - | Cge => Psltw rd r1 r2 :: Pxoriw rd rd Int.one :: k - end. - -Definition transl_cond_int32u (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) := - match cmp with - | Ceq => Pseqw rd r1 r2 :: k - | Cne => Psnew rd r1 r2 :: k - | Clt => Psltuw rd r1 r2 :: k - | Cle => Psltuw rd r2 r1 :: Pxoriw rd rd Int.one :: k - | Cgt => Psltuw rd r2 r1 :: k - | Cge => Psltuw rd r1 r2 :: Pxoriw rd rd Int.one :: k - end. - -Definition transl_cond_int64s (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) := - match cmp with - | Ceq => Pseql rd r1 r2 :: k - | Cne => Psnel rd r1 r2 :: k - | Clt => Psltl rd r1 r2 :: k - | Cle => Psltl rd r2 r1 :: Pxoriw rd rd Int.one :: k - | Cgt => Psltl rd r2 r1 :: k - | Cge => Psltl rd r1 r2 :: Pxoriw rd rd Int.one :: k - end. - -Definition transl_cond_int64u (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) := - match cmp with - | Ceq => Pseql rd r1 r2 :: k - | Cne => Psnel rd r1 r2 :: k - | Clt => Psltul rd r1 r2 :: k - | Cle => Psltul rd r2 r1 :: Pxoriw rd rd Int.one :: k - | Cgt => Psltul rd r2 r1 :: k - | Cge => Psltul rd r1 r2 :: Pxoriw rd rd Int.one :: k - end. - -Definition transl_condimm_int32s (cmp: comparison) (rd: ireg) (r1: ireg) (n: int) (k: code) := - if Int.eq n Int.zero then transl_cond_int32s cmp rd r1 X0 k else - match cmp with - | Ceq | Cne => xorimm32 rd r1 n (transl_cond_int32s cmp rd rd X0 k) - | Clt => sltimm32 rd r1 n k - | Cle => if Int.eq n (Int.repr Int.max_signed) - then loadimm32 rd Int.one k - else sltimm32 rd r1 (Int.add n Int.one) k - | _ => loadimm32 X31 n (transl_cond_int32s cmp rd r1 X31 k) - end. - -Definition transl_condimm_int32u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int) (k: code) := - if Int.eq n Int.zero then transl_cond_int32u cmp rd r1 X0 k else - match cmp with - | Clt => sltuimm32 rd r1 n k - | _ => loadimm32 X31 n (transl_cond_int32u cmp rd r1 X31 k) - end. - -Definition transl_condimm_int64s (cmp: comparison) (rd: ireg) (r1: ireg) (n: int64) (k: code) := - if Int64.eq n Int64.zero then transl_cond_int64s cmp rd r1 X0 k else - match cmp with - | Ceq | Cne => xorimm64 rd r1 n (transl_cond_int64s cmp rd rd X0 k) - | Clt => sltimm64 rd r1 n k - | Cle => if Int64.eq n (Int64.repr Int64.max_signed) - then loadimm32 rd Int.one k - else sltimm64 rd r1 (Int64.add n Int64.one) k - | _ => loadimm64 X31 n (transl_cond_int64s cmp rd r1 X31 k) - end. - -Definition transl_condimm_int64u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int64) (k: code) := - if Int64.eq n Int64.zero then transl_cond_int64u cmp rd r1 X0 k else - match cmp with - | Clt => sltuimm64 rd r1 n k - | _ => loadimm64 X31 n (transl_cond_int64u cmp rd r1 X31 k) - end. - -Definition transl_cond_op - (cond: condition) (rd: ireg) (args: list mreg) (k: code) := - match cond, args with - | Ccomp c, a1 :: a2 :: nil => - do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (transl_cond_int32s c rd r1 r2 k) - | Ccompu c, a1 :: a2 :: nil => - do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (transl_cond_int32u c rd r1 r2 k) - | Ccompimm c n, a1 :: nil => - do r1 <- ireg_of a1; - OK (transl_condimm_int32s c rd r1 n k) - | Ccompuimm c n, a1 :: nil => - do r1 <- ireg_of a1; - OK (transl_condimm_int32u c rd r1 n k) - | Ccompl c, a1 :: a2 :: nil => - do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (transl_cond_int64s c rd r1 r2 k) - | Ccomplu c, a1 :: a2 :: nil => - do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (transl_cond_int64u c rd r1 r2 k) - | Ccomplimm c n, a1 :: nil => - do r1 <- ireg_of a1; - OK (transl_condimm_int64s c rd r1 n k) - | Ccompluimm c n, a1 :: nil => - do r1 <- ireg_of a1; - OK (transl_condimm_int64u c rd r1 n k) - | Ccompf c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_float c rd r1 r2 in - OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k) - | Cnotcompf c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_float c rd r1 r2 in - OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k) - | Ccompfs c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_single c rd r1 r2 in - OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k) - | Cnotcompfs c, f1 :: f2 :: nil => - do r1 <- freg_of f1; do r2 <- freg_of f2; - let (insn, normal) := transl_cond_single c rd r1 r2 in - OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k) - | _, _ => - Error(msg "Asmgen.transl_cond_op") - end. - (** Translation of the arithmetic operation [r <- op(args)]. The corresponding instructions are prepended to [k]. *) @@ -767,9 +523,6 @@ Definition transl_op | Osingleoflongu, a1 :: nil => do rd <- freg_of res; do rs <- ireg_of a1; OK (Pfcvtslu rd rs :: k) - | Ocmp cmp, _ => - do rd <- ireg_of res; - transl_cond_op cmp rd args k | OEseqw optR0, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; @@ -912,18 +665,12 @@ Definition transl_op | Ofloat_of_bits, a1 :: nil => do rd <- freg_of res; do rs <- ireg_of a1; OK (Pfmvdx rd rs :: k) - - | Ocmp cmp, _ => - do rd <- ireg_of res; - transl_cond_op cmp rd args k - | Oselectl, b::t::f::nil => do rd <- ireg_of res; do rb <- ireg_of b; do rt <- ireg_of t; do rf <- ireg_of f; OK (Pselectl rd rb rt rf :: k) - | _, _ => Error(msg "Asmgen.transl_op") end. diff --git a/riscV/Asmgenproof.v b/riscV/Asmgenproof.v index 82c1917d..6abad4ed 100644 --- a/riscV/Asmgenproof.v +++ b/riscV/Asmgenproof.v @@ -161,165 +161,37 @@ 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 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. -- destruct optR0 as [[]|]; TailNoLabel. -- destruct optR0 as [[]|]; TailNoLabel. -- destruct optR0 as [[]|]; TailNoLabel. -- destruct optR0 as [[]|]; TailNoLabel. + all: destruct optR0 as [[]|]; 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. -- 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 optR0 as [[]|]; simpl; TailNoLabel. -- destruct optR0 as [[]|]; simpl; TailNoLabel. -- destruct optR0 as [[]|]; simpl; TailNoLabel. -- destruct optR0 as [[]|]; simpl; TailNoLabel. -- destruct optR0 as [[]|]; simpl; TailNoLabel. -- destruct optR0 as [[]|]; simpl; TailNoLabel. -- destruct optR0 as [[]|]; simpl; TailNoLabel. -- destruct optR0 as [[]|]; simpl; TailNoLabel. -- destruct optR0 as [[]|]; simpl; TailNoLabel. -- destruct optR0 as [[]|]; simpl; TailNoLabel. -- destruct optR0 as [[]|]; simpl; TailNoLabel. -- destruct optR0 as [[]|]; simpl; 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. Qed. Remark indexed_memory_access_label: diff --git a/riscV/Asmgenproof1.v b/riscV/Asmgenproof1.v index 1b3a0dbf..f0def29b 100644 --- a/riscV/Asmgenproof1.v +++ b/riscV/Asmgenproof1.v @@ -290,102 +290,6 @@ Proof. rewrite H0 in B. inv B. auto. Qed. -(** Translation of conditional branches *) - -Lemma transl_cbranch_int32s_correct: - forall cmp r1 r2 lbl (rs: regset) m b, - Val.cmp_bool cmp rs##r1 rs##r2 = Some b -> - exec_instr ge fn (transl_cbranch_int32s cmp r1 r2 lbl) rs m = - eval_branch fn lbl rs m (Some b). -Proof. - intros. destruct cmp; simpl; rewrite ? H. -- destruct rs##r1; simpl in H; try discriminate. destruct rs##r2; inv H. - simpl; auto. -- destruct rs##r1; simpl in H; try discriminate. destruct rs##r2; inv H. - simpl; auto. -- auto. -- rewrite <- Val.swap_cmp_bool. simpl. rewrite H; auto. -- rewrite <- Val.swap_cmp_bool. simpl. rewrite H; auto. -- auto. -Qed. - -Lemma transl_cbranch_int32u_correct: - forall cmp r1 r2 lbl (rs: regset) m b, - Val.cmpu_bool (Mem.valid_pointer m) cmp rs##r1 rs##r2 = Some b -> - exec_instr ge fn (transl_cbranch_int32u cmp r1 r2 lbl) rs m = - eval_branch fn lbl rs m (Some b). -Proof. - intros. destruct cmp; simpl; rewrite ? H; auto. -- rewrite <- Val.swap_cmpu_bool. simpl. rewrite H; auto. -- rewrite <- Val.swap_cmpu_bool. simpl. rewrite H; auto. -Qed. - -Lemma transl_cbranch_int64s_correct: - forall cmp r1 r2 lbl (rs: regset) m b, - Val.cmpl_bool cmp rs###r1 rs###r2 = Some b -> - exec_instr ge fn (transl_cbranch_int64s cmp r1 r2 lbl) rs m = - eval_branch fn lbl rs m (Some b). -Proof. - intros. destruct cmp; simpl; rewrite ? H. -- destruct rs###r1; simpl in H; try discriminate. destruct rs###r2; inv H. - simpl; auto. -- destruct rs###r1; simpl in H; try discriminate. destruct rs###r2; inv H. - simpl; auto. -- auto. -- rewrite <- Val.swap_cmpl_bool. simpl. rewrite H; auto. -- rewrite <- Val.swap_cmpl_bool. simpl. rewrite H; auto. -- auto. -Qed. - -Lemma transl_cbranch_int64u_correct: - forall cmp r1 r2 lbl (rs: regset) m b, - Val.cmplu_bool (Mem.valid_pointer m) cmp rs###r1 rs###r2 = Some b -> - exec_instr ge fn (transl_cbranch_int64u cmp r1 r2 lbl) rs m = - eval_branch fn lbl rs m (Some b). -Proof. - intros. destruct cmp; simpl; rewrite ? H; auto. -- rewrite <- Val.swap_cmplu_bool. simpl. rewrite H; auto. -- rewrite <- Val.swap_cmplu_bool. simpl. rewrite H; auto. -Qed. - -Lemma transl_cond_float_correct: - forall (rs: regset) m cmp rd r1 r2 insn normal v, - transl_cond_float cmp rd r1 r2 = (insn, normal) -> - v = (if normal then Val.cmpf cmp rs#r1 rs#r2 else Val.notbool (Val.cmpf cmp rs#r1 rs#r2)) -> - exec_instr ge fn insn rs m = Next (nextinstr (rs#rd <- v)) m. -Proof. - intros. destruct cmp; simpl in H; inv H; auto. -- rewrite Val.negate_cmpf_eq. auto. -- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpf, Val.cmpf_bool. - rewrite <- Float.cmp_swap. auto. -- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpf, Val.cmpf_bool. - rewrite <- Float.cmp_swap. auto. -Qed. - -Lemma transl_cond_single_correct: - forall (rs: regset) m cmp rd r1 r2 insn normal v, - transl_cond_single cmp rd r1 r2 = (insn, normal) -> - v = (if normal then Val.cmpfs cmp rs#r1 rs#r2 else Val.notbool (Val.cmpfs cmp rs#r1 rs#r2)) -> - exec_instr ge fn insn rs m = Next (nextinstr (rs#rd <- v)) m. -Proof. - intros. destruct cmp; simpl in H; inv H; auto. -- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool. - rewrite Float32.cmp_ne_eq. destruct (Float32.cmp Ceq f0 f); auto. -- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool. - rewrite <- Float32.cmp_swap. auto. -- simpl. f_equal. f_equal. f_equal. destruct (rs r2), (rs r1); auto. unfold Val.cmpfs, Val.cmpfs_bool. - rewrite <- Float32.cmp_swap. auto. - Qed. - -(* TODO gourdinl UNUSUED ? Remark branch_on_X31: - forall normal lbl (rs: regset) m b, - rs#X31 = Val.of_bool (eqb normal b) -> - exec_instr ge fn (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) rs m = - eval_branch fn lbl rs m (Some b). -Proof. - intros. destruct normal; simpl; rewrite H; simpl; destruct b; reflexivity. - Qed.*) - Ltac ArgsInv := repeat (match goal with | [ H: Error _ = OK _ |- _ ] => discriminate @@ -417,203 +321,84 @@ Proof. { apply eval_condition_lessdef with (map ms args) m; auto. eapply preg_vals; eauto. } clear EVAL MEXT AG. destruct cond; simpl in TRANSL; ArgsInv. - - exists rs, (transl_cbranch_int32s c0 x x0 lbl). - intuition auto. constructor. apply transl_cbranch_int32s_correct; auto. -- exists rs, (transl_cbranch_int32u c0 x x0 lbl). - intuition auto. constructor. apply transl_cbranch_int32u_correct; auto. -- predSpec Int.eq Int.eq_spec n Int.zero. -+ subst n. exists rs, (transl_cbranch_int32s c0 x X0 lbl). - intuition auto. constructor. apply transl_cbranch_int32s_correct; auto. -+ exploit (loadimm32_correct X31 n); eauto. intros (rs' & A & B & C). - exists rs', (transl_cbranch_int32s c0 x X31 lbl). - split. constructor; eexact A. split; auto. - apply transl_cbranch_int32s_correct; auto. - simpl; rewrite B, C; eauto with asmgen. -- predSpec Int.eq Int.eq_spec n Int.zero. -+ subst n. exists rs, (transl_cbranch_int32u c0 x X0 lbl). - intuition auto. constructor. apply transl_cbranch_int32u_correct; auto. -+ exploit (loadimm32_correct X31 n); eauto. intros (rs' & A & B & C). - exists rs', (transl_cbranch_int32u c0 x X31 lbl). - split. constructor; eexact A. split; auto. - apply transl_cbranch_int32u_correct; auto. - simpl; rewrite B, C; eauto with asmgen. -- exists rs, (transl_cbranch_int64s c0 x x0 lbl). - intuition auto. constructor. apply transl_cbranch_int64s_correct; auto. -- exists rs, (transl_cbranch_int64u c0 x x0 lbl). - intuition auto. constructor. apply transl_cbranch_int64u_correct; auto. -- predSpec Int64.eq Int64.eq_spec n Int64.zero. -+ subst n. exists rs, (transl_cbranch_int64s c0 x X0 lbl). - intuition auto. constructor. apply transl_cbranch_int64s_correct; auto. -+ exploit (loadimm64_correct X31 n); eauto. intros (rs' & A & B & C). - exists rs', (transl_cbranch_int64s c0 x X31 lbl). - split. constructor; eexact A. split; auto. - apply transl_cbranch_int64s_correct; auto. - simpl; rewrite B, C; eauto with asmgen. -- predSpec Int64.eq Int64.eq_spec n Int64.zero. -+ subst n. exists rs, (transl_cbranch_int64u c0 x X0 lbl). - intuition auto. constructor. apply transl_cbranch_int64u_correct; auto. -+ exploit (loadimm64_correct X31 n); eauto. intros (rs' & A & B & C). - exists rs', (transl_cbranch_int64u c0 x X31 lbl). - split. constructor; eexact A. split; auto. - apply transl_cbranch_int64u_correct; auto. - simpl; rewrite B, C; eauto with asmgen. -- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2. - set (v := if normal then Val.cmpf c0 rs#x rs#x0 else Val.notbool (Val.cmpf c0 rs#x rs#x0)). - assert (V: v = Val.of_bool (eqb normal b)). - { unfold v, Val.cmpf. rewrite EVAL'. destruct normal, b; reflexivity. } - econstructor; econstructor. - split. constructor. apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto. - split. rewrite V; destruct normal, b; reflexivity. - intros; Simpl. -- destruct (transl_cond_float c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2. - assert (EVAL'': Val.cmpf_bool c0 (rs x) (rs x0) = Some (negb b)). - { destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; inv EVAL'; auto. } - set (v := if normal then Val.cmpf c0 rs#x rs#x0 else Val.notbool (Val.cmpf c0 rs#x rs#x0)). - assert (V: v = Val.of_bool (xorb normal b)). - { unfold v, Val.cmpf. rewrite EVAL''. destruct normal, b; reflexivity. } - econstructor; econstructor. - split. constructor. apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto. - split. rewrite V; destruct normal, b; reflexivity. - intros; Simpl. -- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2. - set (v := if normal then Val.cmpfs c0 rs#x rs#x0 else Val.notbool (Val.cmpfs c0 rs#x rs#x0)). - assert (V: v = Val.of_bool (eqb normal b)). - { unfold v, Val.cmpfs. rewrite EVAL'. destruct normal, b; reflexivity. } - econstructor; econstructor. - split. constructor. apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto. - split. rewrite V; destruct normal, b; reflexivity. - intros; Simpl. -- destruct (transl_cond_single c0 X31 x x0) as [insn normal] eqn:TC; inv EQ2. - assert (EVAL'': Val.cmpfs_bool c0 (rs x) (rs x0) = Some (negb b)). - { destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; inv EVAL'; auto. } - set (v := if normal then Val.cmpfs c0 rs#x rs#x0 else Val.notbool (Val.cmpfs c0 rs#x rs#x0)). - assert (V: v = Val.of_bool (xorb normal b)). - { unfold v, Val.cmpfs. rewrite EVAL''. destruct normal, b; reflexivity. } - econstructor; econstructor. - split. constructor. apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto. - split. rewrite V; destruct normal, b; reflexivity. - intros; Simpl. - -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; - unfold zero32, Op.zero32 in *; - eexists; eexists; eauto; split; constructor; auto; - simpl in *. - + destruct (rs x); simpl in *; try congruence. - assert (HB: (Int.eq Int.zero i) = b) by congruence. - rewrite HB; destruct b; simpl; auto. - + destruct (rs x); simpl in *; try congruence. - assert (HB: (Int.eq i Int.zero) = b) by congruence. - rewrite HB; destruct b; simpl; auto. - + destruct (rs x); simpl in *; try congruence. - destruct (rs x0); try congruence. - assert (HB: (Int.eq i i0) = b) by congruence. - rewrite HB; destruct b; simpl; auto. -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; - unfold zero32, Op.zero32 in *; - eexists; eexists; eauto; split; constructor; auto; - simpl in *. - + destruct (rs x); simpl in *; try congruence. - assert (HB: negb (Int.eq Int.zero i) = b) by congruence. - rewrite HB; destruct b; simpl; auto. - + destruct (rs x); simpl in *; try congruence. - assert (HB: negb (Int.eq i Int.zero) = b) by congruence. - rewrite HB; destruct b; simpl; auto. - + destruct (rs x); simpl in *; try congruence. - destruct (rs x0); try congruence. - assert (HB: negb (Int.eq i i0) = b) by congruence. - rewrite HB; destruct b; simpl; auto. -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; - unfold zero32, Op.zero32 in *; - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; - unfold zero32, Op.zero32 in *; - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; - unfold zero32, Op.zero32 in *; - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; - unfold zero32, Op.zero32 in *; - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; - unfold zero32, Op.zero32 in *; - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; - unfold zero32, Op.zero32 in *; - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; - unfold zero64, Op.zero64 in *; - eexists; eexists; eauto; split; constructor; - simpl in *; auto. - + destruct (rs x); simpl in *; try congruence. - assert (HB: (Int64.eq Int64.zero i) = b) by congruence. - rewrite HB; destruct b; simpl; auto. - + destruct (rs x); simpl in *; try congruence. - assert (HB: (Int64.eq i Int64.zero) = b) by congruence. - rewrite HB; destruct b; simpl; auto. - + destruct (rs x); simpl in *; try congruence. - destruct (rs x0); try congruence. - assert (HB: (Int64.eq i i0) = b) by congruence. - rewrite HB; destruct b; simpl; auto. -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; - unfold zero64, Op.zero64 in *; - eexists; eexists; eauto; split; constructor; - simpl in *; auto. - + destruct (rs x); simpl in *; try congruence. - assert (HB: negb (Int64.eq Int64.zero i) = b) by congruence. - rewrite HB; destruct b; simpl; auto. - + destruct (rs x); simpl in *; try congruence. - assert (HB: negb (Int64.eq i Int64.zero) = b) by congruence. - rewrite HB; destruct b; simpl; auto. - + destruct (rs x); simpl in *; try congruence. - destruct (rs x0); try congruence. - assert (HB: negb (Int64.eq i i0) = b) by congruence. - rewrite HB; destruct b; simpl; auto. -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; - unfold zero64, Op.zero64 in *; - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; - unfold zero64, Op.zero64 in *; - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; - unfold zero64, Op.zero64 in *; - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; - unfold zero64, Op.zero64 in *; - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; - unfold zero64, Op.zero64 in *; - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. -- destruct optR0 as [[]|]; - unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; - unfold zero64, Op.zero64 in *; - eexists; eexists; eauto; split; constructor; - simpl in *; try rewrite EVAL'; auto. + (* Pbeqw / Cmp *) + { destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero32, Op.zero32 in *; + eexists; eexists; eauto; split; constructor; auto; + simpl in *. + + destruct (rs x); simpl in *; try congruence. + assert (HB: (Int.eq Int.zero i) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + assert (HB: (Int.eq i Int.zero) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + destruct (rs x0); try congruence. + assert (HB: (Int.eq i i0) = b) by congruence. + rewrite HB; destruct b; simpl; auto. } + (* Pbnew / Cmp *) + { destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero32, Op.zero32 in *; + eexists; eexists; eauto; split; constructor; auto; + simpl in *. + + destruct (rs x); simpl in *; try congruence. + assert (HB: negb (Int.eq Int.zero i) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + assert (HB: negb (Int.eq i Int.zero) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + destruct (rs x0); try congruence. + assert (HB: negb (Int.eq i i0) = b) by congruence. + rewrite HB; destruct b; simpl; auto. } + (* Pbeqw, Pbnew, Pbltw, Pbtluw, Pbgew, Pbgeuw / Cmpu *) + 1-6: + destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero32, Op.zero32 in *; + eexists; eexists; eauto; split; constructor; + simpl in *; try rewrite EVAL'; auto. + (* Pbeql / Cmpl *) + { destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero64, Op.zero64 in *; + eexists; eexists; eauto; split; constructor; + simpl in *; auto. + + destruct (rs x); simpl in *; try congruence. + assert (HB: (Int64.eq Int64.zero i) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + assert (HB: (Int64.eq i Int64.zero) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + destruct (rs x0); try congruence. + assert (HB: (Int64.eq i i0) = b) by congruence. + rewrite HB; destruct b; simpl; auto. } + (* Pbnel / Cmpl *) + { destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero64, Op.zero64 in *; + eexists; eexists; eauto; split; constructor; + simpl in *; auto. + + destruct (rs x); simpl in *; try congruence. + assert (HB: negb (Int64.eq Int64.zero i) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + assert (HB: negb (Int64.eq i Int64.zero) = b) by congruence. + rewrite HB; destruct b; simpl; auto. + + destruct (rs x); simpl in *; try congruence. + destruct (rs x0); try congruence. + assert (HB: negb (Int64.eq i i0) = b) by congruence. + rewrite HB; destruct b; simpl; auto. } + (* Pbeql, Pbnel, Pbltl, Pbtlul, Pbgel, Pbgeul / Cmplu *) + 1-6: + destruct optR0 as [[]|]; + unfold apply_bin_r0, apply_bin_r0_r0r0lbl in *; + unfold zero64, Op.zero64 in *; + eexists; eexists; eauto; split; constructor; + simpl in *; try rewrite EVAL'; auto. Qed. Lemma transl_cbranch_correct_true: @@ -647,405 +432,6 @@ Proof. intros; Simpl. Qed. -(** Translation of condition operators *) - -Lemma transl_cond_int32s_correct: - forall cmp rd r1 r2 k rs m, - exists rs', - exec_straight ge fn (transl_cond_int32s cmp rd r1 r2 k) rs m k rs' m - /\ Val.lessdef (Val.cmp cmp rs##r1 rs##r2) rs'#rd - /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. -Proof. - intros. destruct cmp; simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. destruct (rs##r1); auto. destruct (rs##r2); auto. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. destruct (rs##r1); auto. destruct (rs##r2); auto. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. -- econstructor; split. - eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split; intros; Simpl. unfold Val.cmp. rewrite <- Val.swap_cmp_bool. - simpl. rewrite (Val.negate_cmp_bool Clt). - destruct (Val.cmp_bool Clt rs##r2 rs##r1) as [[]|]; auto. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. unfold Val.cmp. rewrite <- Val.swap_cmp_bool. auto. -- econstructor; split. - eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split; intros; Simpl. unfold Val.cmp. rewrite (Val.negate_cmp_bool Clt). - destruct (Val.cmp_bool Clt rs##r1 rs##r2) as [[]|]; auto. -Qed. - -Lemma transl_cond_int32u_correct: - forall cmp rd r1 r2 k rs m, - exists rs', - exec_straight ge fn (transl_cond_int32u cmp rd r1 r2 k) rs m k rs' m - /\ rs'#rd = Val.cmpu (Mem.valid_pointer m) cmp rs##r1 rs##r2 - /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. -Proof. - intros. destruct cmp; simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. -- econstructor; split. - eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split; intros; Simpl. unfold Val.cmpu. rewrite <- Val.swap_cmpu_bool. - simpl. rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Cle). - destruct (Val.cmpu_bool (Mem.valid_pointer m) Cle rs##r1 rs##r2) as [[]|]; auto. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. unfold Val.cmpu. rewrite <- Val.swap_cmpu_bool. auto. -- econstructor; split. - eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split; intros; Simpl. unfold Val.cmpu. rewrite (Val.negate_cmpu_bool (Mem.valid_pointer m) Clt). - destruct (Val.cmpu_bool (Mem.valid_pointer m) Clt rs##r1 rs##r2) as [[]|]; auto. -Qed. - -Lemma transl_cond_int64s_correct: - forall cmp rd r1 r2 k rs m, - exists rs', - exec_straight ge fn (transl_cond_int64s cmp rd r1 r2 k) rs m k rs' m - /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs###r1 rs###r2)) rs'#rd - /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. -Proof. - intros. destruct cmp; simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. destruct (rs###r1); auto. destruct (rs###r2); auto. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. destruct (rs###r1); auto. destruct (rs###r2); auto. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. -- econstructor; split. - eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split; intros; Simpl. unfold Val.cmpl. rewrite <- Val.swap_cmpl_bool. - simpl. rewrite (Val.negate_cmpl_bool Clt). - destruct (Val.cmpl_bool Clt rs###r2 rs###r1) as [[]|]; auto. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. unfold Val.cmpl. rewrite <- Val.swap_cmpl_bool. auto. -- econstructor; split. - eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split; intros; Simpl. unfold Val.cmpl. rewrite (Val.negate_cmpl_bool Clt). - destruct (Val.cmpl_bool Clt rs###r1 rs###r2) as [[]|]; auto. -Qed. - -Lemma transl_cond_int64u_correct: - forall cmp rd r1 r2 k rs m, - exists rs', - exec_straight ge fn (transl_cond_int64u cmp rd r1 r2 k) rs m k rs' m - /\ rs'#rd = Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs###r1 rs###r2) - /\ forall r, r <> PC -> r <> rd -> rs'#r = rs#r. -Proof. - intros. destruct cmp; simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. -- econstructor; split. - eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split; intros; Simpl. unfold Val.cmplu. rewrite <- Val.swap_cmplu_bool. - simpl. rewrite (Val.negate_cmplu_bool (Mem.valid_pointer m) Cle). - destruct (Val.cmplu_bool (Mem.valid_pointer m) Cle rs###r1 rs###r2) as [[]|]; auto. -- econstructor; split. apply exec_straight_one; [simpl; eauto|auto]. - split; intros; Simpl. unfold Val.cmplu. rewrite <- Val.swap_cmplu_bool. auto. -- econstructor; split. - eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split; intros; Simpl. unfold Val.cmplu. rewrite (Val.negate_cmplu_bool (Mem.valid_pointer m) Clt). - destruct (Val.cmplu_bool (Mem.valid_pointer m) Clt rs###r1 rs###r2) as [[]|]; auto. -Qed. - -Lemma transl_condimm_int32s_correct: - forall cmp rd r1 n k rs m, - r1 <> X31 -> - exists rs', - exec_straight ge fn (transl_condimm_int32s cmp rd r1 n k) rs m k rs' m - /\ Val.lessdef (Val.cmp cmp rs#r1 (Vint n)) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r. -Proof. - intros. unfold transl_condimm_int32s. - predSpec Int.eq Int.eq_spec n Int.zero. -- subst n. exploit transl_cond_int32s_correct. intros (rs' & A & B & C). - exists rs'; eauto. -- assert (DFL: - exists rs', - exec_straight ge fn (loadimm32 X31 n (transl_cond_int32s cmp rd r1 X31 k)) rs m k rs' m - /\ Val.lessdef (Val.cmp cmp rs#r1 (Vint n)) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r). - { exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1). - exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2). - exists rs2; split. - eapply exec_straight_trans. eexact A1. eexact A2. - split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. auto. - intros; transitivity (rs1 r); auto. } - destruct cmp. -+ unfold xorimm32. - exploit (opimm32_correct Pxorw Pxoriw Val.xor); eauto. intros (rs1 & A1 & B1 & C1). - exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2). - exists rs2; split. - eapply exec_straight_trans. eexact A1. eexact A2. - split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto. - unfold Val.cmp in B2; simpl in B2; rewrite Int.xor_is_zero in B2. exact B2. - intros; transitivity (rs1 r); auto. -+ unfold xorimm32. - exploit (opimm32_correct Pxorw Pxoriw Val.xor); eauto. intros (rs1 & A1 & B1 & C1). - exploit transl_cond_int32s_correct; eauto. intros (rs2 & A2 & B2 & C2). - exists rs2; split. - eapply exec_straight_trans. eexact A1. eexact A2. - split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto. - unfold Val.cmp in B2; simpl in B2; rewrite Int.xor_is_zero in B2. exact B2. - intros; transitivity (rs1 r); auto. -+ exploit (opimm32_correct Psltw Psltiw (Val.cmp Clt)); eauto. intros (rs1 & A1 & B1 & C1). - exists rs1; split. eexact A1. split; auto. rewrite B1; auto. -+ predSpec Int.eq Int.eq_spec n (Int.repr Int.max_signed). -* subst n. exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1). - exists rs1; split. eexact A1. split; auto. - unfold Val.cmp; destruct (rs#r1); simpl; auto. rewrite B1. - unfold Int.lt. rewrite zlt_false. auto. - change (Int.signed (Int.repr Int.max_signed)) with Int.max_signed. - generalize (Int.signed_range i); omega. -* exploit (opimm32_correct Psltw Psltiw (Val.cmp Clt)); eauto. intros (rs1 & A1 & B1 & C1). - exists rs1; split. eexact A1. split; auto. - rewrite B1. unfold Val.cmp; simpl; destruct (rs#r1); simpl; auto. - unfold Int.lt. replace (Int.signed (Int.add n Int.one)) with (Int.signed n + 1). - destruct (zlt (Int.signed n) (Int.signed i)). - rewrite zlt_false by omega. auto. - rewrite zlt_true by omega. auto. - rewrite Int.add_signed. symmetry; apply Int.signed_repr. - assert (Int.signed n <> Int.max_signed). - { red; intros E. elim H1. rewrite <- (Int.repr_signed n). rewrite E. auto. } - generalize (Int.signed_range n); omega. -+ apply DFL. -+ apply DFL. -Qed. - -Lemma transl_condimm_int32u_correct: - forall cmp rd r1 n k rs m, - r1 <> X31 -> - exists rs', - exec_straight ge fn (transl_condimm_int32u cmp rd r1 n k) rs m k rs' m - /\ Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp rs#r1 (Vint n)) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r. -Proof. - intros. unfold transl_condimm_int32u. - predSpec Int.eq Int.eq_spec n Int.zero. -- subst n. exploit transl_cond_int32u_correct. intros (rs' & A & B & C). - exists rs'; split. eexact A. split; auto. rewrite B; auto. -- assert (DFL: - exists rs', - exec_straight ge fn (loadimm32 X31 n (transl_cond_int32u cmp rd r1 X31 k)) rs m k rs' m - /\ Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp rs#r1 (Vint n)) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r). - { exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1). - exploit transl_cond_int32u_correct; eauto. intros (rs2 & A2 & B2 & C2). - exists rs2; split. - eapply exec_straight_trans. eexact A1. eexact A2. - split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. rewrite B2; auto. - intros; transitivity (rs1 r); auto. } - destruct cmp. -+ apply DFL. -+ apply DFL. -+ exploit (opimm32_correct Psltuw Psltiuw (Val.cmpu (Mem.valid_pointer m) Clt) m); eauto. - intros (rs1 & A1 & B1 & C1). - exists rs1; split. eexact A1. split; auto. rewrite B1; auto. -+ apply DFL. -+ apply DFL. -+ apply DFL. -Qed. - -Lemma transl_condimm_int64s_correct: - forall cmp rd r1 n k rs m, - r1 <> X31 -> - exists rs', - exec_straight ge fn (transl_condimm_int64s cmp rd r1 n k) rs m k rs' m - /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs#r1 (Vlong n))) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r. -Proof. - intros. unfold transl_condimm_int64s. - predSpec Int64.eq Int64.eq_spec n Int64.zero. -- subst n. exploit transl_cond_int64s_correct. intros (rs' & A & B & C). - exists rs'; eauto. -- assert (DFL: - exists rs', - exec_straight ge fn (loadimm64 X31 n (transl_cond_int64s cmp rd r1 X31 k)) rs m k rs' m - /\ Val.lessdef (Val.maketotal (Val.cmpl cmp rs#r1 (Vlong n))) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r). - { exploit loadimm64_correct; eauto. intros (rs1 & A1 & B1 & C1). - exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2). - exists rs2; split. - eapply exec_straight_trans. eexact A1. eexact A2. - split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. auto. - intros; transitivity (rs1 r); auto. } - destruct cmp. -+ unfold xorimm64. - exploit (opimm64_correct Pxorl Pxoril Val.xorl); eauto. intros (rs1 & A1 & B1 & C1). - exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2). - exists rs2; split. - eapply exec_straight_trans. eexact A1. eexact A2. - split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto. - unfold Val.cmpl in B2; simpl in B2; rewrite Int64.xor_is_zero in B2. exact B2. - intros; transitivity (rs1 r); auto. -+ unfold xorimm64. - exploit (opimm64_correct Pxorl Pxoril Val.xorl); eauto. intros (rs1 & A1 & B1 & C1). - exploit transl_cond_int64s_correct; eauto. intros (rs2 & A2 & B2 & C2). - exists rs2; split. - eapply exec_straight_trans. eexact A1. eexact A2. - split. simpl in B2; rewrite B1 in B2; simpl in B2. destruct (rs#r1); auto. - unfold Val.cmpl in B2; simpl in B2; rewrite Int64.xor_is_zero in B2. exact B2. - intros; transitivity (rs1 r); auto. -+ exploit (opimm64_correct Psltl Psltil (fun v1 v2 => Val.maketotal (Val.cmpl Clt v1 v2))); eauto. intros (rs1 & A1 & B1 & C1). - exists rs1; split. eexact A1. split; auto. rewrite B1; auto. -+ predSpec Int64.eq Int64.eq_spec n (Int64.repr Int64.max_signed). -* subst n. exploit loadimm32_correct; eauto. intros (rs1 & A1 & B1 & C1). - exists rs1; split. eexact A1. split; auto. - unfold Val.cmpl; destruct (rs#r1); simpl; auto. rewrite B1. - unfold Int64.lt. rewrite zlt_false. auto. - change (Int64.signed (Int64.repr Int64.max_signed)) with Int64.max_signed. - generalize (Int64.signed_range i); omega. -* exploit (opimm64_correct Psltl Psltil (fun v1 v2 => Val.maketotal (Val.cmpl Clt v1 v2))); eauto. intros (rs1 & A1 & B1 & C1). - exists rs1; split. eexact A1. split; auto. - rewrite B1. unfold Val.cmpl; simpl; destruct (rs#r1); simpl; auto. - unfold Int64.lt. replace (Int64.signed (Int64.add n Int64.one)) with (Int64.signed n + 1). - destruct (zlt (Int64.signed n) (Int64.signed i)). - rewrite zlt_false by omega. auto. - rewrite zlt_true by omega. auto. - rewrite Int64.add_signed. symmetry; apply Int64.signed_repr. - assert (Int64.signed n <> Int64.max_signed). - { red; intros E. elim H1. rewrite <- (Int64.repr_signed n). rewrite E. auto. } - generalize (Int64.signed_range n); omega. -+ apply DFL. -+ apply DFL. -Qed. - -Lemma transl_condimm_int64u_correct: - forall cmp rd r1 n k rs m, - r1 <> X31 -> - exists rs', - exec_straight ge fn (transl_condimm_int64u cmp rd r1 n k) rs m k rs' m - /\ Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 (Vlong n))) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r. -Proof. - intros. unfold transl_condimm_int64u. - predSpec Int64.eq Int64.eq_spec n Int64.zero. -- subst n. exploit transl_cond_int64u_correct. intros (rs' & A & B & C). - exists rs'; split. eexact A. split; auto. rewrite B; auto. -- assert (DFL: - exists rs', - exec_straight ge fn (loadimm64 X31 n (transl_cond_int64u cmp rd r1 X31 k)) rs m k rs' m - /\ Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp rs#r1 (Vlong n))) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r). - { exploit loadimm64_correct; eauto. intros (rs1 & A1 & B1 & C1). - exploit transl_cond_int64u_correct; eauto. intros (rs2 & A2 & B2 & C2). - exists rs2; split. - eapply exec_straight_trans. eexact A1. eexact A2. - split. simpl in B2. rewrite B1, C1 in B2 by auto with asmgen. rewrite B2; auto. - intros; transitivity (rs1 r); auto. } - destruct cmp. -+ apply DFL. -+ apply DFL. -+ exploit (opimm64_correct Psltul Psltiul (fun v1 v2 => Val.maketotal (Val.cmplu (Mem.valid_pointer m) Clt v1 v2)) m); eauto. - intros (rs1 & A1 & B1 & C1). - exists rs1; split. eexact A1. split; auto. rewrite B1; auto. -+ apply DFL. -+ apply DFL. -+ apply DFL. - Qed. - -Lemma transl_cond_op_correct: - forall cond rd args k c rs m, - transl_cond_op cond rd args k = OK c -> - exists rs', - exec_straight ge fn c rs m k rs' m - /\ Val.lessdef (Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m)) rs'#rd - /\ forall r, r <> PC -> r <> rd -> r <> X31 -> rs'#r = rs#r. -Proof. - assert (MKTOT: forall ob, Val.of_optbool ob = Val.maketotal (option_map Val.of_bool ob)). - { destruct ob as [[]|]; reflexivity. } - intros until m; intros TR. - destruct cond; simpl in TR; ArgsInv. -+ (* cmp *) - exploit transl_cond_int32s_correct; eauto. intros (rs' & A & B & C). exists rs'; eauto. -+ (* cmpu *) - exploit transl_cond_int32u_correct; eauto. intros (rs' & A & B & C). - exists rs'; repeat split; eauto. rewrite B; auto. -+ (* cmpimm *) - apply transl_condimm_int32s_correct; eauto with asmgen. -+ (* cmpuimm *) - apply transl_condimm_int32u_correct; eauto with asmgen. -+ (* cmpl *) - exploit transl_cond_int64s_correct; eauto. intros (rs' & A & B & C). - exists rs'; repeat split; eauto. rewrite MKTOT; eauto. -+ (* cmplu *) - exploit transl_cond_int64u_correct; eauto. intros (rs' & A & B & C). - exists rs'; repeat split; eauto. rewrite B, MKTOT; eauto. -+ (* cmplimm *) - exploit transl_condimm_int64s_correct; eauto. instantiate (1 := x); eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; repeat split; eauto. rewrite MKTOT; eauto. -+ (* cmpluimm *) - exploit transl_condimm_int64u_correct; eauto. instantiate (1 := x); eauto with asmgen. - intros (rs' & A & B & C). - exists rs'; repeat split; eauto. rewrite MKTOT; eauto. -+ (* cmpf *) - destruct (transl_cond_float c0 rd x x0) as [insn normal] eqn:TR. - fold (Val.cmpf c0 (rs x) (rs x0)). - set (v := Val.cmpf c0 (rs x) (rs x0)). - destruct normal; inv EQ2. -* econstructor; split. - apply exec_straight_one. eapply transl_cond_float_correct with (v := v); eauto. auto. - split; intros; Simpl. -* econstructor; split. - eapply exec_straight_two. - eapply transl_cond_float_correct with (v := Val.notbool v); eauto. - simpl; reflexivity. - auto. auto. - split; intros; Simpl. unfold v, Val.cmpf. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; auto. -+ (* notcmpf *) - destruct (transl_cond_float c0 rd x x0) as [insn normal] eqn:TR. - rewrite Val.notbool_negb_3. fold (Val.cmpf c0 (rs x) (rs x0)). - set (v := Val.cmpf c0 (rs x) (rs x0)). - destruct normal; inv EQ2. -* econstructor; split. - eapply exec_straight_two. - eapply transl_cond_float_correct with (v := v); eauto. - simpl; reflexivity. - auto. auto. - split; intros; Simpl. unfold v, Val.cmpf. destruct (Val.cmpf_bool c0 (rs x) (rs x0)) as [[]|]; auto. -* econstructor; split. - apply exec_straight_one. eapply transl_cond_float_correct with (v := Val.notbool v); eauto. auto. - split; intros; Simpl. -+ (* cmpfs *) - destruct (transl_cond_single c0 rd x x0) as [insn normal] eqn:TR. - fold (Val.cmpfs c0 (rs x) (rs x0)). - set (v := Val.cmpfs c0 (rs x) (rs x0)). - destruct normal; inv EQ2. -* econstructor; split. - apply exec_straight_one. eapply transl_cond_single_correct with (v := v); eauto. auto. - split; intros; Simpl. -* econstructor; split. - eapply exec_straight_two. - eapply transl_cond_single_correct with (v := Val.notbool v); eauto. - simpl; reflexivity. - auto. auto. - split; intros; Simpl. unfold v, Val.cmpfs. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; auto. -+ (* notcmpfs *) - destruct (transl_cond_single c0 rd x x0) as [insn normal] eqn:TR. - rewrite Val.notbool_negb_3. fold (Val.cmpfs c0 (rs x) (rs x0)). - set (v := Val.cmpfs c0 (rs x) (rs x0)). - destruct normal; inv EQ2. -* econstructor; split. - eapply exec_straight_two. - eapply transl_cond_single_correct with (v := v); eauto. - simpl; reflexivity. - auto. auto. - split; intros; Simpl. unfold v, Val.cmpfs. destruct (Val.cmpfs_bool c0 (rs x) (rs x0)) as [[]|]; auto. -* econstructor; split. - apply exec_straight_one. eapply transl_cond_single_correct with (v := Val.notbool v); eauto. auto. - split; intros; Simpl. - Qed. - (** Some arithmetic properties. *) Remark cast32unsigned_from_cast32signed: @@ -1254,68 +640,22 @@ Opaque Int.eq. eapply exec_straight_step. simpl; reflexivity. auto. apply exec_straight_one. simpl; reflexivity. auto. split; intros; Simpl. } - (* cond *) - { exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). - exists rs'; split. eexact A. eauto with asmgen. } (* Expanded instructions from RTL *) 7,8,15,16: econstructor; split; try apply exec_straight_one; simpl; eauto; split; intros; Simpl; unfold may_undef_int; try destruct is_long; simpl; try rewrite Int.add_commut; try rewrite Int64.add_commut; destruct (rs (preg_of m0)); try discriminate; eauto. - all: destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0; - econstructor; split; try apply exec_straight_one; simpl; eauto; - split; intros; Simpl. - all: destruct (rs x0); auto. - all: destruct (rs x1); auto. - exists rs'; split; eauto. rewrite B; auto with asmgen. -- (* shrxlimm *) - destruct (Val.shrxl (rs x0) (Vint n)) eqn:TOTAL. - { - exploit Val.shrxl_shrl_3; eauto. intros E; subst v. - destruct (Int.eq n Int.zero). -+ econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split; intros; Simpl. -+ destruct (Int.eq n Int.one). - * econstructor; split. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - apply exec_straight_one. simpl; reflexivity. auto. - split; intros; Simpl. - - * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n). - econstructor; split. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - apply exec_straight_one. simpl; reflexivity. auto. - split; intros; Simpl. - } - destruct (Int.eq n Int.zero). -+ econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split; intros; Simpl. -+ destruct (Int.eq n Int.one). - * econstructor; split. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - apply exec_straight_one. simpl; reflexivity. auto. - split; intros; Simpl. - - * change (Int.repr 64) with Int64.iwordsize'. set (n' := Int.sub Int64.iwordsize' n). - econstructor; split. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - eapply exec_straight_step. simpl; reflexivity. auto. - apply exec_straight_one. simpl; reflexivity. auto. - split; intros; Simpl. - -- (* cond *) - exploit transl_cond_op_correct; eauto. intros (rs' & A & B & C). - exists rs'; split. eexact A. eauto with asmgen. -- (* select *) - econstructor; split. apply exec_straight_one. simpl; eauto. auto. + 1-12: + destruct optR0 as [[]|]; unfold apply_bin_r0_r0r0, apply_bin_r0; + econstructor; split; try apply exec_straight_one; simpl; eauto; + split; intros; Simpl; + destruct (rs x0); auto; + destruct (rs x1); auto. + (* select *) + { econstructor; split. apply exec_straight_one. simpl; eauto. auto. split; intros; Simpl. - apply Val.lessdef_normalize. + apply Val.lessdef_normalize. } Qed. (** Memory accesses *) diff --git a/riscV/Op.v b/riscV/Op.v index 4c2390a1..8b4d444d 100644 --- a/riscV/Op.v +++ b/riscV/Op.v @@ -200,8 +200,7 @@ Inductive operation : Type := | OEfled (**r compare less-than/equal *) | OEfeqs (**r compare equal *) | OEflts (**r compare less-than *) - | OEfles. (**r compare less-than/equal *) - | Ocmp (cond: condition) (**r [rd = 1] if condition holds, [rd = 0] otherwise. *) + | OEfles (**r compare less-than/equal *) | Obits_of_single | Obits_of_float | Osingle_of_bits -- cgit