diff options
Diffstat (limited to 'powerpc/Asmgen.v')
-rw-r--r-- | powerpc/Asmgen.v | 19 |
1 files changed, 18 insertions, 1 deletions
diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index 62efc17f..a686414a 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -416,6 +416,16 @@ Definition transl_select_op let r2' := if snd p then r2 else r1 in transl_cond cond args (Pisel rd r1' r2' (fst p) :: k)). +Definition transl_fselect_op + (cond: condition) (args: list mreg) (r1 r2 rd: freg) (k: code) := + if freg_eq r1 r2 then + OK (Pfmr rd r1 :: k) + else + (let p := crbit_for_cond cond in + let r1' := if snd p then r1 else r2 in + let r2' := if snd p then r2 else r1 in + transl_cond cond args (Pfsel_gen rd r1' r2' (fst p) :: k)). + (** Translation of the arithmetic operation [r <- op(args)]. The corresponding instructions are prepended to [k]. *) @@ -623,9 +633,16 @@ Definition transl_op | Ocmp cmp, _ => transl_cond_op cmp args res k | Osel cmp ty, a1 :: a2 :: args => - assertion (typ_eq ty Tint || typ_eq ty Tlong); + match preg_of res with + | IR r1 => do r1 <- ireg_of a1; do r2 <- ireg_of a2; do r <- ireg_of res; transl_select_op cmp args r1 r2 r k + | FR r => + do r1 <- freg_of a1; do r2 <- freg_of a2; do r <- freg_of res; + transl_fselect_op cmp args r1 r2 r k + | _ => + Error (msg "Asmgen.Osel") + end (*c PPC64 operations *) | Olongconst n, nil => do r <- ireg_of res; OK (loadimm64 r n k) |