diff options
Diffstat (limited to 'riscV/Asmgen.v')
| -rw-r--r-- | riscV/Asmgen.v | 58 |
1 files changed, 45 insertions, 13 deletions
diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index 88d4f73f..ff5d1a6e 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -204,19 +204,23 @@ Definition transl_cond_single (cmp: comparison) (rd: ireg) (fs1 fs2: freg) := | 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) + | Some SP_S => (X SP, r1) end. -Definition get_opimmR0 (rd: ireg) (opi: opimm) := - match opi with - | OPimmADD i => Paddiw rd X0 i - | OPimmADDL i => Paddil rd X0 i - end. +Definition get_oreg (optR: option oreg) (r: ireg0) := + match optR with + | Some SP_S => X SP + | Some X0_L | Some X0_R => X0 + | _ => r + end. Definition transl_cbranch (cond: condition) (args: list mreg) (lbl: label) (k: code) := @@ -785,9 +789,8 @@ Definition transl_op | Ocmp cmp, _ => do rd <- ireg_of res; transl_cond_op cmp rd args k - | OEimmR0 opi, nil => - do rd <- ireg_of res; - OK (get_opimmR0 rd opi :: k) + + (* Instructions expanded in RTL *) | OEseqw optR, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; @@ -839,10 +842,21 @@ Definition transl_op | OEluiw n, nil => do rd <- ireg_of res; OK (Pluiw rd n :: k) - | OEaddiw n, a1 :: nil => + | OEaddiw optR n, nil => do rd <- ireg_of res; - do rs <- ireg_of a1; + let rs := get_oreg optR X0 in OK (Paddiw rd rs n :: k) + | OEaddiw (Some SP_S) n, a1 :: nil => + do rd <- ireg_of res; + do rs <- ireg_of a1; + if Int.eq n Int.zero then + OK (Paddw rd SP rs :: k) + else Error (msg "Asmgen.transl_op") + | 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; @@ -902,10 +916,21 @@ Definition transl_op | OEluil n, nil => do rd <- ireg_of res; OK (Pluil rd n :: k) - | OEaddil n, a1 :: nil => + | OEaddil optR n, nil => do rd <- ireg_of res; - do rs <- ireg_of a1; + let rs := get_oreg optR X0 in OK (Paddil rd rs n :: k) + | OEaddil (Some SP_S) n, a1 :: nil => + do rd <- ireg_of res; + do rs <- ireg_of a1; + if Int64.eq n Int64.zero then + OK (Paddl rd SP rs :: k) + else Error (msg "Asmgen.transl_op") + | 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; @@ -947,6 +972,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; |