aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/Asmgen.v
diff options
context:
space:
mode:
Diffstat (limited to 'riscV/Asmgen.v')
-rw-r--r--riscV/Asmgen.v157
1 files changed, 89 insertions, 68 deletions
diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index 54c7a7c0..88d4f73f 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -205,20 +205,13 @@ Definition transl_cond_single (cmp: comparison) (rd: ireg) (fs1 fs2: freg) :=
| Cge => (Pfles rd fs2 fs1, true)
end.
-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
+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 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
- end.
-
Definition get_opimmR0 (rd: ireg) (opi: opimm) :=
match opi with
| OPimmADD i => Paddiw rd X0 i
@@ -281,54 +274,70 @@ Definition transl_cbranch
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 optR0, a1 :: a2 :: nil =>
+ | CEbeqw optR, 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 =>
+ 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 Pbnew r1 r2 lbl :: k)
- | CEbequw 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 Pbeqw r1 r2 lbl :: k)
- | CEbneuw 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 Pbnew r1 r2 lbl :: k)
- | CEbltw 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 Pbltw r1 r2 lbl :: k)
- | CEbltuw 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 Pbltuw r1 r2 lbl :: k)
- | CEbgew 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 Pbgew r1 r2 lbl :: k)
- | CEbgeuw 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 Pbgeuw r1 r2 lbl :: k)
- | CEbeql 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 Pbeql r1 r2 lbl :: k)
- | CEbnel 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 Pbnel r1 r2 lbl :: k)
- | CEbequl 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 Pbeql r1 r2 lbl :: k)
- | CEbneul 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 Pbnel r1 r2 lbl :: k)
- | CEbltl optR0, a1 :: a2 :: nil =>
+ 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;
- 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 (Pbltl r1' r2' lbl :: k)
+ | CEbltul 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 (Pbltul r1' r2' lbl :: k)
+ | CEbgel 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 (Pbgel r1' r2' lbl :: k)
+ | CEbgeul 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 (Pbgeul r1' r2' lbl :: k)
| _, _ =>
Error(msg "Asmgen.transl_cond_branch")
end.
@@ -779,36 +788,42 @@ Definition transl_op
| OEimmR0 opi, nil =>
do rd <- ireg_of res;
OK (get_opimmR0 rd opi :: k)
- | OEseqw optR0, a1 :: a2 :: nil =>
+ | 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;
@@ -836,36 +851,42 @@ Definition transl_op
do rd <- ireg_of res;
do rs <- ireg_of a1;
OK (Poriw rd rs n :: k)
- | OEseql optR0, a1 :: a2 :: nil =>
+ | 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;
generated by cgit (git 2.34.1) at 2024-05-20 02:16:38 +0000