diff options
author | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-03 17:14:23 +0100 |
---|---|---|
committer | Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr> | 2021-02-03 17:14:23 +0100 |
commit | 29ba37cc21cedc09b20bbd8adfa0ec52c48365c0 (patch) | |
tree | 673c5cdb7b99756c4c6880e7ef0b14bed7544bc2 /riscV/Asmgen.v | |
parent | 7f8ccba038ce9bf7665341c05b89bb5d9b9b536b (diff) | |
download | compcert-kvx-29ba37cc21cedc09b20bbd8adfa0ec52c48365c0.tar.gz compcert-kvx-29ba37cc21cedc09b20bbd8adfa0ec52c48365c0.zip |
All Ocmp expanded in RTL
Diffstat (limited to 'riscV/Asmgen.v')
-rw-r--r-- | riscV/Asmgen.v | 44 |
1 files changed, 37 insertions, 7 deletions
diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index f702d11a..b3fb2350 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -344,10 +344,10 @@ Definition transl_condimm_int64u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int | _ => loadimm64 X31 n (transl_cond_int64u cmp rd r1 X31 k) end. -Definition transl_cond_op +(* TODO Definition transl_cond_op (cond: condition) (rd: ireg) (args: list mreg) (k: code) := match cond, args with - (* TODO | Ccomp c, a1 :: a2 :: nil => + | 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 => @@ -370,7 +370,7 @@ Definition transl_cond_op 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,10 +386,10 @@ 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]. *) @@ -712,9 +712,9 @@ Definition transl_op do rd <- freg_of res; do rs <- ireg_of a1; OK (Pfcvtslu rd rs :: k) - | Ocmp cmp, _ => + (* TODO | Ocmp cmp, _ => do rd <- ireg_of res; - transl_cond_op cmp rd args k + transl_cond_op cmp rd args k*) | OEseqw optR0, a1 :: a2 :: nil => do rd <- ireg_of res; @@ -795,6 +795,36 @@ Definition transl_op | 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) | _, _ => Error(msg "Asmgen.transl_op") end. |