diff options
Diffstat (limited to 'riscV/Asmgen.v')
| -rw-r--r-- | riscV/Asmgen.v | 342 |
1 files changed, 317 insertions, 25 deletions
diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index a704ed74..3e84e950 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -25,6 +25,8 @@ Require Import Op Locations Mach Asm. Local Open Scope string_scope. Local Open Scope error_monad_scope. +Definition time {A B: Type} (name: string) (f: A -> B) : A -> B := f. + (** The code generation functions take advantage of several characteristics of the [Mach] code generated by earlier passes of the compiler, mostly that argument and result registers are of the correct @@ -201,8 +203,23 @@ 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. + +(** 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 @@ -257,7 +274,72 @@ 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 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 (Pbeqw r1' r2' lbl :: k) + | CEbnew 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 (Pbnew r1' r2' lbl :: k) + | CEbequw 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 (Pbeqw r1' r2' lbl :: k) + | CEbneuw 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 (Pbnew r1' r2' lbl :: k) + | CEbltw 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 (Pbltw r1' r2' lbl :: k) + | CEbltuw 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 (Pbltuw r1' r2' lbl :: k) + | CEbgew 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 (Pbgew r1' r2' lbl :: k) + | CEbgeuw 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 (Pbgeuw r1' r2' lbl :: k) + | CEbeql 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 (Pbeql r1' r2' lbl :: k) + | CEbnel 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 (Pbnel r1' r2' lbl :: k) + | CEbequl 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 (Pbeql r1' r2' lbl :: k) + | CEbneul 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 (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. @@ -340,7 +422,7 @@ 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. Definition transl_cond_op (cond: condition) (rd: ireg) (args: list mreg) (k: code) := @@ -362,13 +444,13 @@ Definition transl_cond_op 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) + 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) + 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 @@ -384,14 +466,14 @@ Definition transl_cond_op | 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) + 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]. *) - + Definition transl_op (op: operation) (args: list mreg) (res: mreg) (k: code) := match op, args with @@ -503,11 +585,16 @@ Definition transl_op 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 - Psraiw X31 rs (Int.repr 31) :: - Psrliw X31 X31 (Int.sub Int.iwordsize n) :: - Paddw X31 rs X31 :: - Psraiw rd X31 n :: k) + 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 => @@ -592,11 +679,16 @@ Definition transl_op 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 - Psrail X31 rs (Int.repr 63) :: - Psrlil X31 X31 (Int.sub Int64.iwordsize' n) :: - Paddl X31 rs X31 :: - Psrail rd X31 n :: k) + 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; @@ -692,11 +784,206 @@ 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 + 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; + 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; + 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; + 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; + 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; + 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; + 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; + OK (Psltiw rd rs n :: k) + | OEsltiuw n, a1 :: nil => + do rd <- ireg_of res; + do rs <- ireg_of a1; + OK (Psltiuw rd rs n :: k) + | OExoriw n, a1 :: nil => + do rd <- ireg_of res; + do rs <- ireg_of a1; + OK (Pxoriw rd rs n :: k) + | OEluiw n, nil => + do rd <- ireg_of res; + OK (Pluiw rd n :: k) + | 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; + 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; + 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; + 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; + 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; + 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; + 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; + 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; + OK (Psltil rd rs n :: k) + | OEsltiul n, a1 :: nil => + do rd <- ireg_of res; + do rs <- ireg_of a1; + OK (Psltiul rd rs n :: k) + | OExoril n, a1 :: nil => + do rd <- ireg_of res; + do rs <- ireg_of a1; + OK (Pxoril rd rs n :: k) + | OEluil n, nil => + do rd <- ireg_of res; + OK (Pluil rd n :: k) + | OEaddil optR n, nil => + do rd <- ireg_of res; + 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) + | OEfeqd, f1 :: f2 :: nil => + do rd <- ireg_of res; + do r1 <- freg_of f1; + do r2 <- freg_of f2; + OK (Pfeqd rd r1 r2 :: k) + | OEfltd, f1 :: f2 :: nil => + do rd <- ireg_of res; + do r1 <- freg_of f1; + do r2 <- freg_of f2; + OK (Pfltd rd r1 r2 :: k) + | OEfled, f1 :: f2 :: nil => + do rd <- ireg_of res; + do r1 <- freg_of f1; + do r2 <- freg_of f2; + OK (Pfled rd r1 r2 :: k) + | OEfeqs, f1 :: f2 :: nil => + do rd <- ireg_of res; + do r1 <- freg_of f1; + do r2 <- freg_of f2; + OK (Pfeqs rd r1 r2 :: k) + | OEflts, f1 :: f2 :: nil => + do rd <- ireg_of res; + do r1 <- freg_of f1; + do r2 <- freg_of f2; + OK (Pflts rd r1 r2 :: k) + | OEfles, f1 :: f2 :: nil => + do rd <- ireg_of res; + 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; + OK (Pfmvxs rd rs :: k) + | Obits_of_float, a1 :: nil => + do rd <- ireg_of res; do rs <- freg_of a1; + OK (Pfmvxd rd rs :: k) + | Osingle_of_bits, a1 :: nil => + do rd <- freg_of res; do rs <- ireg_of a1; + OK (Pfmvsx rd rs :: k) + | Ofloat_of_bits, a1 :: nil => + do rd <- freg_of res; do rs <- ireg_of a1; + OK (Pfmvdx rd rs :: 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. @@ -770,9 +1057,13 @@ Definition transl_memory_access Error(msg "Asmgen.transl_memory_access") end. -Definition transl_load (chunk: memory_chunk) (addr: addressing) +Definition transl_load (trap : trapping_mode) + (chunk: memory_chunk) (addr: addressing) (args: list mreg) (dst: mreg) (k: code) := - match chunk with + match trap with + | NOTRAP => Error (msg "Asmgen.transl_load non-trapping loads unsupported on Arm") + | TRAP => + match chunk with | Mint8signed => do r <- ireg_of dst; transl_memory_access (Plb r) addr args k @@ -799,6 +1090,7 @@ Definition transl_load (chunk: memory_chunk) (addr: addressing) transl_memory_access (Pfld r) addr args k | _ => Error (msg "Asmgen.transl_load") + end end. Definition transl_store (chunk: memory_chunk) (addr: addressing) @@ -848,8 +1140,8 @@ Definition transl_instr (f: Mach.function) (i: Mach.instruction) else loadind_ptr SP f.(fn_link_ofs) X30 c) | Mop op args res => transl_op op args res k - | Mload chunk addr args dst => - transl_load chunk addr args dst k + | Mload trap chunk addr args dst => + transl_load trap chunk addr args dst k | Mstore chunk addr args src => transl_store chunk addr args src k | Mcall sig (inl r) => |