diff options
Diffstat (limited to 'riscV/Asmgen.v')
| -rw-r--r-- | riscV/Asmgen.v | 459 |
1 files changed, 386 insertions, 73 deletions
diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index 957166b6..3e84e950 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -105,6 +105,8 @@ 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 @@ -130,6 +132,8 @@ 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 @@ -141,75 +145,332 @@ Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) := (** Translation of conditional branches. *) -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 - | Some true => sem X0 r1 lbl - | Some false => sem r1 X0 lbl - end. +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 apply_bin_r0_r0r0 (optR0: option bool) (sem: ireg0 -> ireg0 -> instruction) (r1 r2: ireg0) := - match optR0 with - | None => sem r1 r2 - | Some true => sem X0 r1 - | Some false => sem r1 X0 +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. + +(** Functions to select a special register according to the op "oreg" argument from RTL *) + +Definition apply_bin_oreg_ireg0 (optR: option oreg) (r1 r2: ireg0): (ireg0 * ireg0) := + match optR with + | None => (r1, r2) + | Some X0_L => (X0, r1) + | Some X0_R => (r1, X0) + end. + +Definition get_oreg (optR: option oreg) (r: ireg0) := + match optR with + | Some X0_L | Some X0_R => X0 + | _ => r + end. + Definition transl_cbranch (cond: condition) (args: list mreg) (lbl: label) (k: code) := match cond, args with - | CEbeqw optR0, a1 :: a2 :: nil => + | Ccomp c, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (apply_bin_r0_r0r0lbl optR0 Pbeqw r1 r2 lbl :: k) - | CEbnew optR0, a1 :: a2 :: nil => + 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 (apply_bin_r0_r0r0lbl optR0 Pbnew r1 r2 lbl :: k) - | CEbequw optR0, a1 :: a2 :: nil => + 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 (apply_bin_r0_r0r0lbl optR0 Pbeqw r1 r2 lbl :: k) - | CEbneuw optR0, a1 :: a2 :: nil => + 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 (apply_bin_r0_r0r0lbl optR0 Pbnew r1 r2 lbl :: k) - | CEbltw optR0, a1 :: a2 :: nil => + 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 optR, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (apply_bin_r0_r0r0lbl optR0 Pbltw r1 r2 lbl :: k) - | CEbltuw optR0, a1 :: a2 :: nil => + let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in + OK (Pbeqw r1' r2' lbl :: k) + | CEbnew optR, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (apply_bin_r0_r0r0lbl optR0 Pbltuw r1 r2 lbl :: k) - | CEbgew optR0, a1 :: a2 :: nil => + let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in + OK (Pbnew r1' r2' lbl :: k) + | CEbequw optR, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (apply_bin_r0_r0r0lbl optR0 Pbgew r1 r2 lbl :: k) - | CEbgeuw optR0, a1 :: a2 :: nil => + let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in + OK (Pbeqw r1' r2' lbl :: k) + | CEbneuw optR, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (apply_bin_r0_r0r0lbl optR0 Pbgeuw r1 r2 lbl :: k) - | CEbeql optR0, a1 :: a2 :: nil => + let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in + OK (Pbnew r1' r2' lbl :: k) + | CEbltw optR, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (apply_bin_r0_r0r0lbl optR0 Pbeql r1 r2 lbl :: k) - | CEbnel optR0, a1 :: a2 :: nil => + let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in + OK (Pbltw r1' r2' lbl :: k) + | CEbltuw optR, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (apply_bin_r0_r0r0lbl optR0 Pbnel r1 r2 lbl :: k) - | CEbequl optR0, a1 :: a2 :: nil => + let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in + OK (Pbltuw r1' r2' lbl :: k) + | CEbgew optR, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (apply_bin_r0_r0r0lbl optR0 Pbeql r1 r2 lbl :: k) - | CEbneul optR0, a1 :: a2 :: nil => + let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in + OK (Pbgew r1' r2' lbl :: k) + | CEbgeuw optR, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (apply_bin_r0_r0r0lbl optR0 Pbnel r1 r2 lbl :: k) - | CEbltl optR0, a1 :: a2 :: nil => + let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in + OK (Pbgeuw r1' r2' lbl :: k) + | CEbeql optR, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (apply_bin_r0_r0r0lbl optR0 Pbltl r1 r2 lbl :: k) - | CEbltul optR0, a1 :: a2 :: nil => + let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in + OK (Pbeql r1' r2' lbl :: k) + | CEbnel optR, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (apply_bin_r0_r0r0lbl optR0 Pbltul r1 r2 lbl :: k) - | CEbgel optR0, a1 :: a2 :: nil => + let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in + OK (Pbnel r1' r2' lbl :: k) + | CEbequl optR, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (apply_bin_r0_r0r0lbl optR0 Pbgel r1 r2 lbl :: k) - | CEbgeul optR0, a1 :: a2 :: nil => + let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in + OK (Pbeql r1' r2' lbl :: k) + | CEbneul optR, a1 :: a2 :: nil => do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (apply_bin_r0_r0r0lbl optR0 Pbgeul r1 r2 lbl :: k) + let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in + OK (Pbnel r1' r2' lbl :: k) + | CEbltl optR, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in + OK (Pbltl r1' r2' lbl :: k) + | CEbltul optR, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in + OK (Pbltul r1' r2' lbl :: k) + | CEbgel optR, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in + OK (Pbgel r1' r2' lbl :: k) + | CEbgeul optR, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + let (r1', r2') := apply_bin_oreg_ireg0 optR r1 r2 in + OK (Pbgeul r1' r2' lbl :: k) | _, _ => 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]. *) @@ -523,36 +784,47 @@ Definition transl_op | Osingleoflongu, a1 :: nil => do rd <- freg_of res; do rs <- ireg_of a1; OK (Pfcvtslu rd rs :: k) - | OEseqw optR0, a1 :: a2 :: nil => + | Ocmp cmp, _ => + do rd <- ireg_of res; + transl_cond_op cmp rd args k + + (* Instructions expanded in RTL *) + | OEseqw optR, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (apply_bin_r0_r0r0 optR0 (Pseqw rd) rs1 rs2 :: k) - | OEsnew optR0, a1 :: a2 :: nil => + let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in + OK (Pseqw rd rs1' rs2' :: k) + | OEsnew optR, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (apply_bin_r0_r0r0 optR0 (Psnew rd) rs1 rs2 :: k) - | OEsequw optR0, a1 :: a2 :: nil => + let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in + OK (Psnew rd rs1' rs2' :: k) + | OEsequw optR, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (apply_bin_r0_r0r0 optR0 (Pseqw rd) rs1 rs2 :: k) - | OEsneuw optR0, a1 :: a2 :: nil => + let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in + OK (Pseqw rd rs1' rs2' :: k) + | OEsneuw optR, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (apply_bin_r0_r0r0 optR0 (Psnew rd) rs1 rs2 :: k) - | OEsltw optR0, a1 :: a2 :: nil => + let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in + OK (Psnew rd rs1' rs2' :: k) + | OEsltw optR, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (apply_bin_r0_r0r0 optR0 (Psltw rd) rs1 rs2 :: k) - | OEsltuw optR0, a1 :: a2 :: nil => + let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in + OK (Psltw rd rs1' rs2' :: k) + | OEsltuw optR, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (apply_bin_r0_r0r0 optR0 (Psltuw rd) rs1 rs2 :: k) + let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in + OK (Psltuw rd rs1' rs2' :: k) | OEsltiw n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; @@ -565,42 +837,62 @@ Definition transl_op do rd <- ireg_of res; do rs <- ireg_of a1; OK (Pxoriw rd rs n :: k) - | OEluiw n _, a1 :: nil => + | OEluiw n, nil => do rd <- ireg_of res; OK (Pluiw rd n :: k) - | OEaddiwr0 n _, a1 :: nil => + | OEaddiw optR n, nil => + do rd <- ireg_of res; + let rs := get_oreg optR X0 in + OK (Paddiw rd rs n :: k) + | OEaddiw optR n, a1 :: nil => + do rd <- ireg_of res; + do rs <- ireg_of a1; + let rs' := get_oreg optR rs in + OK (Paddiw rd rs' n :: k) + | OEandiw n, a1 :: nil => do rd <- ireg_of res; - OK (Paddiw rd X0 n :: k) - | OEseql optR0, a1 :: a2 :: nil => + do rs <- ireg_of a1; + OK (Pandiw rd rs n :: k) + | OEoriw n, a1 :: nil => + do rd <- ireg_of res; + do rs <- ireg_of a1; + OK (Poriw rd rs n :: k) + | OEseql optR, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (apply_bin_r0_r0r0 optR0 (Pseql rd) rs1 rs2 :: k) - | OEsnel optR0, a1 :: a2 :: nil => + let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in + OK (Pseql rd rs1' rs2' :: k) + | OEsnel optR, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (apply_bin_r0_r0r0 optR0 (Psnel rd) rs1 rs2 :: k) - | OEsequl optR0, a1 :: a2 :: nil => + let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in + OK (Psnel rd rs1' rs2' :: k) + | OEsequl optR, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (apply_bin_r0_r0r0 optR0 (Pseql rd) rs1 rs2 :: k) - | OEsneul optR0, a1 :: a2 :: nil => + let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in + OK (Pseql rd rs1' rs2' :: k) + | OEsneul optR, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (apply_bin_r0_r0r0 optR0 (Psnel rd) rs1 rs2 :: k) - | OEsltl optR0, a1 :: a2 :: nil => + let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in + OK (Psnel rd rs1' rs2' :: k) + | OEsltl optR, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (apply_bin_r0_r0r0 optR0 (Psltl rd) rs1 rs2 :: k) - | OEsltul optR0, a1 :: a2 :: nil => + let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in + OK (Psltl rd rs1' rs2' :: k) + | OEsltul optR, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; - OK (apply_bin_r0_r0r0 optR0 (Psltul rd) rs1 rs2 :: k) + let (rs1', rs2') := apply_bin_oreg_ireg0 optR rs1 rs2 in + OK (Psltul rd rs1' rs2' :: k) | OEsltil n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; @@ -613,12 +905,26 @@ Definition transl_op do rd <- ireg_of res; do rs <- ireg_of a1; OK (Pxoril rd rs n :: k) - | OEluil n, a1 :: nil => + | OEluil n, nil => do rd <- ireg_of res; OK (Pluil rd n :: k) - | OEaddilr0 n, a1 :: nil => + | OEaddil optR n, nil => do rd <- ireg_of res; - OK (Paddil rd X0 n :: k) + let rs := get_oreg optR X0 in + OK (Paddil rd rs n :: k) + | OEaddil optR n, a1 :: nil => + do rd <- ireg_of res; + do rs <- ireg_of a1; + let rs' := get_oreg optR rs in + OK (Paddil rd rs' n :: k) + | OEandil n, a1 :: nil => + do rd <- ireg_of res; + do rs <- ireg_of a1; + OK (Pandil rd rs n :: k) + | OEoril n, a1 :: nil => + do rd <- ireg_of res; + do rs <- ireg_of a1; + OK (Poril rd rs n :: k) | OEloadli n, nil => do rd <- ireg_of res; OK (Ploadli rd n :: k) @@ -652,6 +958,13 @@ Definition transl_op do r1 <- freg_of f1; do r2 <- freg_of f2; OK (Pfles rd r1 r2 :: k) + | OEmayundef _, a1 :: a2 :: nil => + do rd <- ireg_of res; + do r2 <- ireg_of a2; + if ireg_eq rd r2 then + OK (Pnop :: k) + else + OK (Pmv rd r2 :: k) | Obits_of_single, a1 :: nil => do rd <- ireg_of res; do rs <- freg_of a1; |