cond and branches expanded

1 files changed, 65 insertions, 23 deletions

diff --git a/riscV/Asmgen.v b/riscV/Asmgen.v
index b3fb2350..4b27ee81 100644
--- a/riscV/Asmgen.v
+++ b/riscV/Asmgen.v
@@ -105,8 +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.
+(* TODO REMOVE Definition sltimm32 := opimm32 Psltw Psltiw.*)
+(* TODO REMOVE 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
@@ -132,8 +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.
+(* TODO REMOVE Definition sltimm64 := opimm64 Psltl Psltil.*)
+(* TODO REMOVE Definition sltuimm64 := opimm64 Psltul Psltiul.*)
 
 Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) :=
   if Ptrofs.eq_dec n Ptrofs.zero then
@@ -145,7 +145,7 @@ Definition addptrofs (rd rs: ireg) (n: ptrofs) (k: code) :=
   
 (** Translation of conditional branches. *)
 
-Definition transl_cbranch_int32s (cmp: comparison) (r1 r2: ireg0) (lbl: label) :=
+(* TODO REMOVE Definition transl_cbranch_int32s (cmp: comparison) (r1 r2: ireg0) (lbl: label) :=
   match cmp with
   | Ceq => Pbeqw r1 r2 lbl
   | Cne => Pbnew r1 r2 lbl
@@ -203,12 +203,26 @@ Definition transl_cond_single (cmp: comparison) (rd: ireg) (fs1 fs2: freg) :=
   | 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
+  | Some true => sem X0 r1 lbl
+  | Some false => sem r1 X0 lbl
+  end. 
+
+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_cbranch
            (cond: condition) (args: list mreg) (lbl: label) (k: code) :=
   match cond, args with
-  | Ccomp c, a1 :: a2 :: nil =>
+(* TODO REMOVE | 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 =>
@@ -259,7 +273,44 @@ Definition transl_cbranch
   | 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)
+   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)
+  | CEbnew optR0, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0lbl optR0 Pbnew r1 r2 lbl :: k)
+  | CEbltw optR0, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0lbl optR0 Pbltw r1 r2 lbl :: k)
+  | CEbltuw optR0, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0lbl optR0 Pbltuw r1 r2 lbl :: k)
+  | CEbgew optR0, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0lbl optR0 Pbgew r1 r2 lbl :: k)
+  | CEbgeuw optR0, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0lbl optR0 Pbgeuw r1 r2 lbl :: k)
+  | CEbeql optR0, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0lbl optR0 Pbeql r1 r2 lbl :: k)
+  | CEbnel optR0, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0lbl optR0 Pbnel r1 r2 lbl :: k)
+  | CEbltl optR0, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0lbl optR0 Pbltl r1 r2 lbl :: k)
+  | CEbltul optR0, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0lbl optR0 Pbltul r1 r2 lbl :: k)
+  | CEbgel optR0, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0lbl optR0 Pbgel r1 r2 lbl :: k)
+  | CEbgeul optR0, a1 :: a2 :: nil =>
+      do r1 <- ireg_of a1; do r2 <- ireg_of a2;
+      OK (apply_bin_r0_r0r0lbl optR0 Pbgeul r1 r2 lbl :: k)
   | _, _ =>
       Error(msg "Asmgen.transl_cond_branch")
   end.
@@ -268,7 +319,7 @@ Definition transl_cbranch
   [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) :=
+(* TODO REMOVE 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
@@ -342,9 +393,9 @@ Definition transl_condimm_int64u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int
   match cmp with
   | Clt => sltuimm64 rd r1 n k
   | _   => loadimm64 X31 n (transl_cond_int64u cmp rd r1 X31 k)
-  end.
+   end. *)
 
-(* TODO Definition transl_cond_op
+(* TODO REMOVE Definition transl_cond_op
            (cond: condition) (rd: ireg) (args: list mreg) (k: code) :=
   match cond, args with
   | Ccomp c, a1 :: a2 :: nil =>
@@ -389,18 +440,11 @@ Definition transl_condimm_int64u (cmp: comparison) (rd: ireg) (r1: ireg) (n: int
      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]. *)
   
-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
@@ -711,11 +755,9 @@ Definition transl_op
   | Osingleoflongu, a1 :: nil =>
       do rd <- freg_of res; do rs <- ireg_of a1;
       OK (Pfcvtslu rd rs :: k)
-
-      (* TODO | Ocmp cmp, _ =>
+  (* TODO REMOVE | 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;
       do rs1 <- ireg_of a1;