diff options
Diffstat (limited to 'mppa_k1c/Asmblockgen.v')
-rw-r--r-- | mppa_k1c/Asmblockgen.v | 62 |
1 files changed, 37 insertions, 25 deletions
diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v index edffd879..8c6457a6 100644 --- a/mppa_k1c/Asmblockgen.v +++ b/mppa_k1c/Asmblockgen.v @@ -190,14 +190,29 @@ Definition transl_opt_compluimm loadimm64 RTMP n ::g (transl_compl c Unsigned r1 RTMP lbl k) . -(* match select_compl n c with - | Some Ceq => Pcbu BTdeqz r1 lbl ::g k - | Some Cne => Pcbu BTdnez r1 lbl ::g k - | Some _ => nil (* Never happens *) - | None => loadimm64 RTMP n ::g (transl_compl c Unsigned r1 RTMP lbl k) - end - . - *) +Definition transl_comp_float32 (cmp: comparison) (r1 r2: ireg) (lbl: label) (k: code) := + match ftest_for_cmp cmp with + | Normal ft => Pfcompw ft GPR32 r1 r2 ::g Pcb BTwnez GPR32 lbl ::g k + | Reversed ft => Pfcompw ft GPR32 r2 r1 ::g Pcb BTwnez GPR32 lbl ::g k + end. + +Definition transl_comp_notfloat32 (cmp: comparison) (r1 r2: ireg) (lbl: label) (k: code) := + match notftest_for_cmp cmp with + | Normal ft => Pfcompw ft GPR32 r1 r2 ::g Pcb BTwnez GPR32 lbl ::g k + | Reversed ft => Pfcompw ft GPR32 r2 r1 ::g Pcb BTwnez GPR32 lbl ::g k + end. + +Definition transl_comp_float64 (cmp: comparison) (r1 r2: ireg) (lbl: label) (k: code) := + match ftest_for_cmp cmp with + | Normal ft => Pfcompl ft GPR32 r1 r2 ::g Pcb BTwnez GPR32 lbl ::g k + | Reversed ft => Pfcompl ft GPR32 r2 r1 ::g Pcb BTwnez GPR32 lbl ::g k + end. + +Definition transl_comp_notfloat64 (cmp: comparison) (r1 r2: ireg) (lbl: label) (k: code) := + match notftest_for_cmp cmp with + | Normal ft => Pfcompl ft GPR32 r1 r2 ::g Pcb BTwnez GPR32 lbl ::g k + | Reversed ft => Pfcompl ft GPR32 r2 r1 ::g Pcb BTwnez GPR32 lbl ::g k + end. Definition transl_cbranch (cond: condition) (args: list mreg) (lbl: label) (k: code) : res (list instruction ) := @@ -234,23 +249,19 @@ Definition transl_cbranch else loadimm64 RTMP n ::g (transl_compl c Signed r1 RTMP lbl 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) -*)| _, _ => + | Ccompf c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (transl_comp_float64 c r1 r2 lbl k) + | Cnotcompf c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (transl_comp_notfloat64 c r1 r2 lbl k) + | Ccompfs c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (transl_comp_float32 c r1 r2 lbl k) + | Cnotcompfs c, a1 :: a2 :: nil => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (transl_comp_notfloat32 c r1 r2 lbl k) + | _, _ => Error(msg "Asmgenblock.transl_cbranch") end. @@ -282,6 +293,7 @@ Definition transl_condimm_int64s (cmp: comparison) (rd r1: ireg) (n: int64) (k: Definition transl_condimm_int64u (cmp: comparison) (rd r1: ireg) (n: int64) (k: bcode) := Pcompil (itest_for_cmp cmp Unsigned) rd r1 n ::i k. + Definition transl_cond_float32 (cmp: comparison) (rd r1 r2: ireg) (k: bcode) := match ftest_for_cmp cmp with | Normal ft => Pfcompw ft rd r1 r2 ::i k |