From 7f8ccba038ce9bf7665341c05b89bb5d9b9b536b Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Wed, 3 Feb 2021 12:29:11 +0100 Subject: Ccomp for long --- riscV/Asmgen.v | 47 ++++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 44 insertions(+), 3 deletions(-) (limited to 'riscV/Asmgen.v') diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index 17a2d3bb..f702d11a 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -347,7 +347,7 @@ Definition transl_condimm_int64u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int Definition transl_cond_op (cond: condition) (rd: ireg) (args: list mreg) (k: code) := match cond, args with - | Ccomp c, a1 :: a2 :: nil => + (* TODO | 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 => @@ -364,13 +364,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 @@ -754,6 +754,47 @@ Definition transl_op | OEaddiwr0 n, 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) + | 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, nil => + do rd <- ireg_of res; + OK (Pluil rd n :: k) + | OEaddilr0 n, 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) | _, _ => Error(msg "Asmgen.transl_op") end. -- cgit