Asmcondexp branche useful to benchmark expansions

1 files changed, 247 insertions, 0 deletions

diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index 957166b6..4f9d008b 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -105,6 +105,8 @@ Definition addimm32 := opimm32 Paddw Paddiw.
 Definition andimm32 := opimm32 Pandw Pandiw.
 Definition orimm32  := opimm32 Porw  Poriw.
 Definition xorimm32 := opimm32 Pxorw Pxoriw.
+Definition sltimm32 := opimm32 Psltw Psltiw.
+Definition sltuimm32 := opimm32 Psltuw Psltiuw.
   
 Definition load_hilo64 (r: ireg) (hi lo: int64) k :=
   if Int64.eq lo Int64.zero then Pluil r hi :: k
@@ -130,6 +132,8 @@ Definition addimm64 := opimm64 Paddl Paddil.
 Definition andimm64 := opimm64 Pandl Pandil.
 Definition orimm64  := opimm64 Porl  Poril.
 Definition xorimm64 := opimm64 Pxorl  Pxoril.
+Definition sltimm64 := opimm64 Psltl Psltil.
+Definition sltuimm64 := opimm64 Psltul Psltiul.
 
 Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) :=
   if Ptrofs.eq_dec n Ptrofs.zero then
@@ -141,6 +145,66 @@ Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) :=
   
 (** Translation of conditional branches. *)
 
+Definition transl_cbranch_int32s (cmp: comparison) (r1 r2: ireg0) (lbl: label) :=
+  match cmp with
+  | Ceq => Pbeqw r1 r2 lbl
+  | Cne => Pbnew r1 r2 lbl
+  | Clt => Pbltw r1 r2 lbl
+  | Cle => Pbgew r2 r1 lbl
+  | Cgt => Pbltw r2 r1 lbl
+  | Cge => Pbgew r1 r2 lbl
+  end.
+
+Definition transl_cbranch_int32u (cmp: comparison) (r1 r2: ireg0) (lbl: label) :=
+  match cmp with
+  | Ceq => Pbeqw  r1 r2 lbl
+  | Cne => Pbnew  r1 r2 lbl
+  | Clt => Pbltuw r1 r2 lbl
+  | Cle => Pbgeuw r2 r1 lbl
+  | Cgt => Pbltuw r2 r1 lbl
+  | Cge => Pbgeuw r1 r2 lbl
+  end.
+
+Definition transl_cbranch_int64s (cmp: comparison) (r1 r2: ireg0) (lbl: label) :=
+  match cmp with
+  | Ceq => Pbeql r1 r2 lbl
+  | Cne => Pbnel r1 r2 lbl
+  | Clt => Pbltl r1 r2 lbl
+  | Cle => Pbgel r2 r1 lbl
+  | Cgt => Pbltl r2 r1 lbl
+  | Cge => Pbgel r1 r2 lbl
+  end.
+
+Definition transl_cbranch_int64u (cmp: comparison) (r1 r2: ireg0) (lbl: label) :=
+  match cmp with
+  | Ceq => Pbeql  r1 r2 lbl
+  | Cne => Pbnel  r1 r2 lbl
+  | Clt => Pbltul r1 r2 lbl
+  | Cle => Pbgeul r2 r1 lbl
+  | Cgt => Pbltul r2 r1 lbl
+  | Cge => Pbgeul r1 r2 lbl
+  end.
+
+Definition transl_cond_float (cmp: comparison) (rd: ireg) (fs1 fs2: freg) :=
+  match cmp with
+  | Ceq => (Pfeqd rd fs1 fs2, true)
+  | Cne => (Pfeqd rd fs1 fs2, false)
+  | Clt => (Pfltd rd fs1 fs2, true)
+  | Cle => (Pfled rd fs1 fs2, true)
+  | Cgt => (Pfltd rd fs2 fs1, true)
+  | Cge => (Pfled rd fs2 fs1, true)
+  end.
+  
+Definition transl_cond_single (cmp: comparison) (rd: ireg) (fs1 fs2: freg) :=
+  match cmp with
+  | Ceq => (Pfeqs rd fs1 fs2, true)
+  | Cne => (Pfeqs rd fs1 fs2, false)
+  | Clt => (Pflts rd fs1 fs2, true)
+  | 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
@@ -158,6 +222,59 @@ Definition apply_bin_r0_r0r0 (optR0: option bool) (sem: ireg0 -> ireg0 -> instru
 Definition transl_cbranch
            (cond: condition) (args: list mreg) (lbl: label) (k: code) :=
   match cond, args with
+  | Ccomp c, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (transl_cbranch_int32s c r1 r2 lbl :: k)
+  | Ccompu c, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (transl_cbranch_int32u c r1 r2 lbl :: k)
+  | Ccompimm c n, a1 :: nil =>
+      do r1 <- ireg_of a1;
+      OK (if Int.eq n Int.zero then
+            transl_cbranch_int32s c r1 X0 lbl :: k
+          else
+            loadimm32 X31 n (transl_cbranch_int32s c r1 X31 lbl :: k))
+  | Ccompuimm c n, a1 :: nil =>
+      do r1 <- ireg_of a1;
+      OK (if Int.eq n Int.zero then
+            transl_cbranch_int32u c r1 X0 lbl :: k
+          else
+            loadimm32 X31 n (transl_cbranch_int32u c r1 X31 lbl :: k))
+  | Ccompl c, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (transl_cbranch_int64s c r1 r2 lbl :: k)
+  | Ccomplu c, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (transl_cbranch_int64u c r1 r2 lbl :: k)
+  | Ccomplimm c n, a1 :: nil =>
+      do r1 <- ireg_of a1;
+      OK (if Int64.eq n Int64.zero then
+            transl_cbranch_int64s c r1 X0 lbl :: k
+          else
+            loadimm64 X31 n (transl_cbranch_int64s c r1 X31 lbl :: k))
+  | Ccompluimm c n, a1 :: nil =>
+      do r1 <- ireg_of a1;
+      OK (if Int64.eq n Int64.zero then
+            transl_cbranch_int64u c r1 X0 lbl :: k
+          else
+            loadimm64 X31 n (transl_cbranch_int64u c r1 X31 lbl :: k))
+  | Ccompf c, f1 :: f2 :: nil =>
+      do r1 <- freg_of f1; do r2 <- freg_of f2;
+      let (insn, normal) := transl_cond_float c X31 r1 r2 in
+      OK (insn :: (if normal then Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) :: k)
+  | Cnotcompf c, f1 :: f2 :: nil =>
+      do r1 <- freg_of f1; do r2 <- freg_of f2;
+      let (insn, normal) := transl_cond_float c X31 r1 r2 in
+      OK (insn :: (if normal then Pbeqw X31 X0 lbl else Pbnew X31 X0 lbl) :: k)
+  | Ccompfs 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 Pbnew X31 X0 lbl else Pbeqw X31 X0 lbl) :: k)
+  | 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)
+
   | 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)
@@ -210,6 +327,133 @@ Definition transl_cbranch
       Error(msg "Asmgen.transl_cond_branch")
   end.
 
+(** Translation of a condition operator.  The generated code sets the
+  [rd] target register to 0 or 1 depending on the truth value of the
+  condition. *)
+
+Definition transl_cond_int32s (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) :=
+  match cmp with
+  | Ceq => Pseqw rd r1 r2 :: k
+  | Cne => Psnew rd r1 r2 :: k
+  | Clt => Psltw rd r1 r2 :: k
+  | Cle => Psltw rd r2 r1 :: Pxoriw rd rd Int.one :: k
+  | Cgt => Psltw rd r2 r1 :: k
+  | Cge => Psltw rd r1 r2 :: Pxoriw rd rd Int.one :: k
+  end.
+
+Definition transl_cond_int32u (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) :=
+  match cmp with
+  | Ceq => Pseqw rd r1 r2 :: k
+  | Cne => Psnew rd r1 r2 :: k
+  | Clt => Psltuw rd r1 r2 :: k
+  | Cle => Psltuw rd r2 r1 :: Pxoriw rd rd Int.one :: k
+  | Cgt => Psltuw rd r2 r1 :: k
+  | Cge => Psltuw rd r1 r2 :: Pxoriw rd rd Int.one :: k
+  end.
+
+Definition transl_cond_int64s (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) :=
+  match cmp with
+  | Ceq => Pseql rd r1 r2 :: k
+  | Cne => Psnel rd r1 r2 :: k
+  | Clt => Psltl rd r1 r2 :: k
+  | Cle => Psltl rd r2 r1 :: Pxoriw rd rd Int.one :: k
+  | Cgt => Psltl rd r2 r1 :: k
+  | Cge => Psltl rd r1 r2 :: Pxoriw rd rd Int.one :: k
+  end.
+
+Definition transl_cond_int64u (cmp: comparison) (rd: ireg) (r1 r2: ireg0) (k: code) :=
+  match cmp with
+  | Ceq => Pseql rd r1 r2 :: k
+  | Cne => Psnel rd r1 r2 :: k
+  | Clt => Psltul rd r1 r2 :: k
+  | Cle => Psltul rd r2 r1 :: Pxoriw rd rd Int.one :: k
+  | Cgt => Psltul rd r2 r1 :: k
+  | Cge => Psltul rd r1 r2 :: Pxoriw rd rd Int.one :: k
+  end.
+
+Definition transl_condimm_int32s (cmp: comparison) (rd: ireg) (r1: ireg) (n: int) (k: code) :=
+  if Int.eq n Int.zero then transl_cond_int32s cmp rd r1 X0 k else
+  match cmp with
+  | Ceq | Cne => xorimm32 rd r1 n (transl_cond_int32s cmp rd rd X0 k)
+  | Clt => sltimm32 rd r1 n k
+  | Cle => if Int.eq n (Int.repr Int.max_signed)
+           then loadimm32 rd Int.one k
+           else sltimm32 rd r1 (Int.add n Int.one) k
+  | _   => loadimm32 X31 n (transl_cond_int32s cmp rd r1 X31 k)
+  end.
+
+Definition transl_condimm_int32u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int) (k: code) :=
+  if Int.eq n Int.zero then transl_cond_int32u cmp rd r1 X0 k else
+  match cmp with
+  | Clt => sltuimm32 rd r1 n k
+  | _   => loadimm32 X31 n (transl_cond_int32u cmp rd r1 X31 k)
+  end.
+
+Definition transl_condimm_int64s (cmp: comparison) (rd: ireg) (r1: ireg) (n: int64) (k: code) :=
+  if Int64.eq n Int64.zero then transl_cond_int64s cmp rd r1 X0 k else
+  match cmp with
+  | Ceq | Cne => xorimm64 rd r1 n (transl_cond_int64s cmp rd rd X0 k)
+  | Clt => sltimm64 rd r1 n k
+  | Cle => if Int64.eq n (Int64.repr Int64.max_signed)
+           then loadimm32 rd Int.one k
+           else sltimm64 rd r1 (Int64.add n Int64.one) k
+  | _   => loadimm64 X31 n (transl_cond_int64s cmp rd r1 X31 k)
+  end.
+
+Definition transl_condimm_int64u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int64) (k: code) :=
+  if Int64.eq n Int64.zero then transl_cond_int64u cmp rd r1 X0 k else
+  match cmp with
+  | Clt => sltuimm64 rd r1 n k
+  | _   => loadimm64 X31 n (transl_cond_int64u cmp rd r1 X31 k)
+   end.
+
+Definition transl_cond_op
+           (cond: condition) (rd: ireg) (args: list mreg) (k: code) :=
+  match cond, args with
+  | 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 =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (transl_cond_int32u c rd r1 r2 k)
+  | Ccompimm c n, a1 :: nil =>
+      do r1 <- ireg_of a1;
+      OK (transl_condimm_int32s c rd r1 n k)
+  | Ccompuimm c n, a1 :: nil =>
+      do r1 <- ireg_of a1;
+      OK (transl_condimm_int32u c rd r1 n k)
+  | Ccompl c, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      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)
+  | 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)
+  | 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
+      OK (insn :: if normal then k else Pxoriw rd rd Int.one :: k)
+  | Cnotcompf 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
+      OK (insn :: if normal then Pxoriw rd rd Int.one :: k else k)
+  | Ccompfs 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 k else Pxoriw rd rd Int.one :: k)
+  | 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)
+  | _, _ =>
+      Error(msg "Asmgen.transl_cond_op")
+   end.
+
 (** Translation of the arithmetic operation [r <- op(args)].
   The corresponding instructions are prepended to [k]. *)
   
@@ -523,6 +767,9 @@ 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;