From 84cb4939653e5355c2039ed62a140aa392e21162 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 10 Feb 2021 10:34:38 +0100 Subject: [Admitted checker] Checker expansion for reg Ocmp (without scratch) --- riscV/Asmgen.v | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) (limited to 'riscV/Asmgen.v') diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index 4b27ee81..7f63bfee 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -105,8 +105,8 @@ Definition addimm32 := opimm32 Paddw Paddiw. Definition andimm32 := opimm32 Pandw Pandiw. Definition orimm32 := opimm32 Porw Poriw. Definition xorimm32 := opimm32 Pxorw Pxoriw. -(* TODO REMOVE Definition sltimm32 := opimm32 Psltw Psltiw.*) -(* TODO REMOVE Definition sltuimm32 := opimm32 Psltuw Psltiuw.*) +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 +132,8 @@ Definition addimm64 := opimm64 Paddl Paddil. Definition andimm64 := opimm64 Pandl Pandil. Definition orimm64 := opimm64 Porl Poril. Definition xorimm64 := opimm64 Pxorl Pxoril. -(* TODO REMOVE Definition sltimm64 := opimm64 Psltl Psltil.*) -(* TODO REMOVE Definition sltuimm64 := opimm64 Psltul Psltiul.*) +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,7 +145,7 @@ Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) := (** Translation of conditional branches. *) -(* TODO REMOVE Definition transl_cbranch_int32s (cmp: comparison) (r1 r2: ireg0) (lbl: label) := +Definition transl_cbranch_int32s (cmp: comparison) (r1 r2: ireg0) (lbl: label) := match cmp with | Ceq => Pbeqw r1 r2 lbl | Cne => Pbnew r1 r2 lbl @@ -203,7 +203,7 @@ Definition transl_cond_single (cmp: comparison) (rd: ireg) (fs1 fs2: freg) := | Cle => (Pfles rd fs1 fs2, true) | Cgt => (Pflts rd fs2 fs1, true) | Cge => (Pfles rd fs2 fs1, true) - end.*) + end. Definition apply_bin_r0_r0r0lbl (optR0: option bool) (sem: ireg0 -> ireg0 -> label -> instruction) (r1 r2: ireg0) (lbl: label) := match optR0 with @@ -222,7 +222,7 @@ 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 -(* TODO REMOVE | Ccomp c, a1 :: a2 :: nil => +| 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 => @@ -273,7 +273,7 @@ Definition transl_cbranch | 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)*) + 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; @@ -319,7 +319,7 @@ Definition transl_cbranch [rd] target register to 0 or 1 depending on the truth value of the condition. *) -(* TODO REMOVE Definition transl_cond_int32s (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) := +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 @@ -393,9 +393,9 @@ Definition transl_condimm_int64u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int match cmp with | Clt => sltuimm64 rd r1 n k | _ => loadimm64 X31 n (transl_cond_int64u cmp rd r1 X31 k) - end. *) + end. -(* TODO REMOVE Definition transl_cond_op +Definition transl_cond_op (cond: condition) (rd: ireg) (args: list mreg) (k: code) := match cond, args with | Ccomp c, a1 :: a2 :: nil => @@ -440,7 +440,7 @@ Definition transl_condimm_int64u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k) | _, _ => Error(msg "Asmgen.transl_cond_op") - end.*) + end. (** Translation of the arithmetic operation [r <- op(args)]. The corresponding instructions are prepended to [k]. *) @@ -755,9 +755,9 @@ Definition transl_op | Osingleoflongu, a1 :: nil => do rd <- freg_of res; do rs <- ireg_of a1; OK (Pfcvtslu rd rs :: k) - (* TODO REMOVE | Ocmp cmp, _ => + | Ocmp cmp, _ => do rd <- ireg_of res; - transl_cond_op cmp rd args k *) + transl_cond_op cmp rd args k | OEseqw optR0, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; -- cgit