From 3e47c1b17e8ff03400106a80117eb86d7e7f9da6 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 2 Feb 2021 13:30:57 +0100 Subject: Expansion of Ccompimm in RTL [Admitted checker] --- riscV/Asmgen.v | 40 ++++++++++++++++++++++++++++++++++++++-- 1 file changed, 38 insertions(+), 2 deletions(-) (limited to 'riscV/Asmgen.v') diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index b431d63d..8d1e3a5c 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -393,7 +393,14 @@ Definition transl_cond_op (** Translation of the arithmetic operation [r <- op(args)]. The corresponding instructions are prepended to [k]. *) - + +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_op (op: operation) (args: list mreg) (res: mreg) (k: code) := match op, args with @@ -708,7 +715,36 @@ Definition transl_op | 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) + | 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) + | OEsltiw n, a1 :: nil => + do rd <- ireg_of res; + do rs <- ireg_of a1; + OK (Psltiw 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, nil => + do rd <- ireg_of res; + OK (Pluiw rd n :: k) + | OEaddiwr0 n, nil => + do rd <- ireg_of res; + OK (Paddiw rd X0 n :: k) | _, _ => Error(msg "Asmgen.transl_op") end. -- cgit