diff options
Diffstat (limited to 'riscV/Asmgen.v')
| -rw-r--r-- | riscV/Asmgen.v | 344 |
1 files changed, 344 insertions, 0 deletions
diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index da6c0101..3e84e950 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -86,6 +86,12 @@ Definition make_immed64 (val: int64) := Definition load_hilo32 (r: ireg) (hi lo: int) k := if Int.eq lo Int.zero then Pluiw r hi :: k else Pluiw r hi :: Paddiw r r lo :: k. + +Definition loadimm32 (r: ireg) (n: int) (k: code) := + match make_immed32 n with + | Imm32_single imm => Paddiw r X0 imm :: k + | Imm32_pair hi lo => load_hilo32 r hi lo k + end. Definition opimm32 (op: ireg -> ireg0 -> ireg0 -> instruction) (opimm: ireg -> ireg0 -> int -> instruction) @@ -96,11 +102,23 @@ Definition opimm32 (op: ireg -> ireg0 -> ireg0 -> instruction) end. 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 else Pluil r hi :: Paddil r r lo :: k. +Definition loadimm64 (r: ireg) (n: int64) (k: code) := + match make_immed64 n with + | Imm64_single imm => Paddil r X0 imm :: k + | Imm64_pair hi lo => load_hilo64 r hi lo k + | Imm64_large imm => Ploadli r imm :: k + end. + Definition opimm64 (op: ireg -> ireg0 -> ireg0 -> instruction) (opimm: ireg -> ireg0 -> int64 -> instruction) (rd rs: ireg) (n: int64) (k: code) := @@ -111,6 +129,11 @@ Definition opimm64 (op: ireg -> ireg0 -> ireg0 -> instruction) end. 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 @@ -120,6 +143,68 @@ Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) := then addimm64 rd rs (Ptrofs.to_int64 n) k else addimm32 rd rs (Ptrofs.to_int n) k. +(** 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. + (** 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) := @@ -138,6 +223,59 @@ Definition get_oreg (optR: option oreg) (r: ireg0) := 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 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 @@ -206,6 +344,133 @@ 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]. *) @@ -218,6 +483,22 @@ Definition transl_op | FR r, FR a => OK (Pfmv r a :: k) | _ , _ => Error(msg "Asmgen.Omove") end + | Ointconst n, nil => + do rd <- ireg_of res; + OK (loadimm32 rd n k) + | Olongconst n, nil => + do rd <- ireg_of res; + OK (loadimm64 rd n k) + | Ofloatconst f, nil => + do rd <- freg_of res; + OK (if Float.eq_dec f Float.zero + then Pfcvtdw rd X0 :: k + else Ploadfi rd f :: k) + | Osingleconst f, nil => + do rd <- freg_of res; + OK (if Float32.eq_dec f Float32.zero + then Pfcvtsw rd X0 :: k + else Ploadsi rd f :: k) | Oaddrsymbol s ofs, nil => do rd <- ireg_of res; OK (if Archi.pic_code tt && negb (Ptrofs.eq ofs Ptrofs.zero) @@ -227,9 +508,18 @@ Definition transl_op do rd <- ireg_of res; OK (addptrofs rd SP n k) + | Ocast8signed, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Pslliw rd rs (Int.repr 24) :: Psraiw rd rd (Int.repr 24) :: k) + | Ocast16signed, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (Pslliw rd rs (Int.repr 16) :: Psraiw rd rd (Int.repr 16) :: k) | Oadd, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Paddw rd rs1 rs2 :: k) + | Oaddimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (addimm32 rd rs n k) | Oneg, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (Psubw rd X0 rs :: k) @@ -260,12 +550,21 @@ Definition transl_op | Oand, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pandw rd rs1 rs2 :: k) + | Oandimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (andimm32 rd rs n k) | Oor, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Porw rd rs1 rs2 :: k) + | Oorimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (orimm32 rd rs n k) | Oxor, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pxorw rd rs1 rs2 :: k) + | Oxorimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (xorimm32 rd rs n k) | Oshl, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Psllw rd rs1 rs2 :: k) @@ -284,6 +583,19 @@ Definition transl_op | Oshruimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (Psrliw rd rs n :: k) + | Oshrximm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (if Int.eq n Int.zero + then Pmv rd rs :: k + else if Int.eq n Int.one + then Psrliw X31 rs (Int.repr 31) :: + Paddw X31 rs X31 :: + Psraiw rd X31 Int.one :: k + else Psraiw X31 rs (Int.repr 31) :: + Psrliw X31 X31 (Int.sub Int.iwordsize n) :: + Paddw X31 rs X31 :: + Psraiw rd X31 n :: k) + (* [Omakelong], [Ohighlong] should not occur *) | Olowlong, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; @@ -292,9 +604,16 @@ Definition transl_op do rd <- ireg_of res; do rs <- ireg_of a1; assertion (ireg_eq rd rs); OK (Pcvtw2l rd :: k) + | Ocast32unsigned, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + assertion (ireg_eq rd rs); + OK (Pcvtw2l rd :: Psllil rd rd (Int.repr 32) :: Psrlil rd rd (Int.repr 32) :: k) | Oaddl, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Paddl rd rs1 rs2 :: k) + | Oaddlimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (addimm64 rd rs n k) | Onegl, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (Psubl rd X0 rs :: k) @@ -325,12 +644,21 @@ Definition transl_op | Oandl, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pandl rd rs1 rs2 :: k) + | Oandlimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (andimm64 rd rs n k) | Oorl, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Porl rd rs1 rs2 :: k) + | Oorlimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (orimm64 rd rs n k) | Oxorl, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pxorl rd rs1 rs2 :: k) + | Oxorlimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (xorimm64 rd rs n k) | Oshll, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2; OK (Pslll rd rs1 rs2 :: k) @@ -349,6 +677,19 @@ Definition transl_op | Oshrluimm n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; OK (Psrlil rd rs n :: k) + | Oshrxlimm n, a1 :: nil => + do rd <- ireg_of res; do rs <- ireg_of a1; + OK (if Int.eq n Int.zero + then Pmv rd rs :: k + else if Int.eq n Int.one + then Psrlil X31 rs (Int.repr 63) :: + Paddl X31 rs X31 :: + Psrail rd X31 Int.one :: k + else Psrail X31 rs (Int.repr 63) :: + Psrlil X31 X31 (Int.sub Int64.iwordsize' n) :: + Paddl X31 rs X31 :: + Psrail rd X31 n :: k) + | Onegf, a1 :: nil => do rd <- freg_of res; do rs <- freg_of a1; OK (Pfnegd rd rs :: k) @@ -443,6 +784,9 @@ 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 (* Instructions expanded in RTL *) | OEseqw optR, a1 :: a2 :: nil => |