aboutsummaryrefslogtreecommitdiffstats
path: root/riscV/Asmgen.v
diff options
context:
space:
mode:
Diffstat (limited to 'riscV/Asmgen.v')
-rw-r--r--riscV/Asmgen.v211
1 files changed, 203 insertions, 8 deletions
diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index b87d2692..252a9270 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -203,8 +203,22 @@ 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.
+
+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 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 transl_cbranch
(cond: condition) (args: list mreg) (lbl: label) (k: code) :=
match cond, args with
@@ -259,7 +273,56 @@ 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 optR0, 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 =>
+ 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 =>
+ 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 =>
+ 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 =>
+ 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 =>
+ 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 =>
+ 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 =>
+ 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 =>
+ 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 =>
+ 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 =>
+ 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 =>
+ 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 =>
+ 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 =>
+ 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 =>
+ 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 =>
+ do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+ OK (apply_bin_r0_r0r0lbl optR0 Pbgeul r1 r2 lbl :: k)
| _, _ =>
Error(msg "Asmgen.transl_cond_branch")
end.
@@ -342,7 +405,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) :=
@@ -364,13 +427,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
@@ -386,14 +449,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
@@ -704,6 +767,138 @@ 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
+ | OEseqw optR0, 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 =>
+ 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 =>
+ 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 =>
+ 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 =>
+ 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 =>
+ 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)
+ | 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 _, a1 :: nil =>
+ do rd <- ireg_of res;
+ OK (Pluiw rd n :: k)
+ | OEaddiwr0 n _, a1 :: nil =>
+ do rd <- ireg_of res;
+ OK (Paddiw rd X0 n :: k)
+ | OEseql optR0, 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 =>
+ 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 =>
+ 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 =>
+ 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 =>
+ 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 =>
+ 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)
+ | 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, a1 :: nil =>
+ do rd <- ireg_of res;
+ OK (Pluil rd n :: k)
+ | OEaddilr0 n, a1 :: nil =>
+ do rd <- ireg_of res;
+ OK (Paddil rd X0 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)
| Obits_of_single, a1 :: nil =>
do rd <- ireg_of res; do rs <- freg_of a1;
generated by cgit (git 2.34.1) at 2024-06-13 12:01:23 +0000