From 83b556a101b7ed490acf9e127c5b4b9db40e1019 Mon Sep 17 00:00:00 2001 From: Léo Gourdin Date: Tue, 30 Mar 2021 11:25:28 +0200 Subject: Now a more general way to perform imm operations --- riscV/Asmgen.v | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) (limited to 'riscV/Asmgen.v') diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v index d4c6b73a..54c7a7c0 100644 --- a/riscV/Asmgen.v +++ b/riscV/Asmgen.v @@ -219,6 +219,12 @@ Definition apply_bin_r0_r0r0 (optR0: option bool) (sem: ireg0 -> ireg0 -> instru | Some false => sem r1 X0 end. +Definition get_opimmR0 (rd: ireg) (opi: opimm) := + match opi with + | OPimmADD i => Paddiw rd X0 i + | OPimmADDL i => Paddil rd X0 i + end. + Definition transl_cbranch (cond: condition) (args: list mreg) (lbl: label) (k: code) := match cond, args with @@ -770,6 +776,9 @@ Definition transl_op | Ocmp cmp, _ => do rd <- ireg_of res; transl_cond_op cmp rd args k + | OEimmR0 opi, nil => + do rd <- ireg_of res; + OK (get_opimmR0 rd opi :: k) | OEseqw optR0, a1 :: a2 :: nil => do rd <- ireg_of res; do rs1 <- ireg_of a1; @@ -819,9 +828,6 @@ Definition transl_op do rd <- ireg_of res; do rs <- ireg_of a1; OK (Paddiw rd rs n :: k) - | OEaddiwr0 n, nil => - do rd <- ireg_of res; - OK (Paddiw rd X0 n :: k) | OEandiw n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; @@ -879,9 +885,6 @@ Definition transl_op do rd <- ireg_of res; do rs <- ireg_of a1; OK (Paddil rd rs n :: k) - | OEaddilr0 n, nil => - do rd <- ireg_of res; - OK (Paddil rd X0 n :: k) | OEandil n, a1 :: nil => do rd <- ireg_of res; do rs <- ireg_of a1; -- cgit