aboutsummaryrefslogtreecommitdiffstats
path: root/powerpc/Asmexpand.ml
diff options
context:
space:
mode:
Diffstat (limited to 'powerpc/Asmexpand.ml')
-rw-r--r--powerpc/Asmexpand.ml107
1 files changed, 83 insertions, 24 deletions
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 49a0d237..ce88778c 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -14,7 +14,7 @@
of the PPC assembly code. *)
open Camlcoq
-open Integers
+open! Integers
open AST
open Asm
open Asmexpandaux
@@ -30,20 +30,22 @@ let eref =
(* Useful constants and helper functions *)
-let _0 = Integers.Int.zero
-let _1 = Integers.Int.one
+let _0 = Int.zero
+let _1 = Int.one
let _2 = coqint_of_camlint 2l
let _4 = coqint_of_camlint 4l
let _6 = coqint_of_camlint 6l
let _8 = coqint_of_camlint 8l
+let _16 = coqint_of_camlint 16l
let _31 = coqint_of_camlint 31l
let _32 = coqint_of_camlint 32l
let _64 = coqint_of_camlint 64l
let _m1 = coqint_of_camlint (-1l)
let _m4 = coqint_of_camlint (-4l)
let _m8 = coqint_of_camlint (-8l)
+let _m16 = coqint_of_camlint (-16l)
-let _0L = Integers.Int64.zero
+let _0L = Int64.zero
let _32L = coqint_of_camlint64 32L
let _64L = coqint_of_camlint64 64L
let _m1L = coqint_of_camlint64 (-1L)
@@ -56,6 +58,15 @@ let emit_loadimm r n =
let emit_addimm rd rs n =
List.iter emit (Asmgen.addimm rd rs n [])
+(* Numbering of bits in the CR register *)
+
+let num_crbit = function
+ | CRbit_0 -> 0
+ | CRbit_1 -> 1
+ | CRbit_2 -> 2
+ | CRbit_3 -> 3
+ | CRbit_6 -> 6
+
(* Handling of annotations *)
let expand_annot_val kind txt targ args res =
@@ -77,8 +88,6 @@ let expand_annot_val kind txt targ args res =
So, use 64-bit accesses only if alignment >= 4.
Note that lfd and stfd cannot trap on ill-formed floats. *)
-
-
let offset_in_range ofs =
Int.eq (Asmgen.high_s ofs) _0
@@ -410,10 +419,21 @@ let expand_builtin_va_start r =
let expand_int64_arith conflict rl fn =
if conflict then (fn GPR0; emit (Pmr(rl, GPR0))) else fn rl
-(* Expansion of integer conditional moves (__builtin_*sel) *)
+(* Expansion of integer conditional moves (__builtin_*sel and Pisel) *)
(* The generated code works equally well with 32-bit integer registers
and with 64-bit integer registers. *)
+let expand_integer_cond_move_1 a2 a3 res =
+ (* GPR0 is -1 (all ones) if condition is true, 0 if it is false *)
+ if res <> a3 then begin
+ emit (Pand_ (res, a2, GPR0));
+ emit (Pandc (GPR0, a3, GPR0))
+ end else begin
+ emit (Pandc (res, a3, GPR0));
+ emit (Pand_ (GPR0, a2, GPR0))
+ end;
+ emit (Por (res, res, GPR0))
+
let expand_integer_cond_move a1 a2 a3 res =
if a2 = a3 then
emit (Pmr (res, a2))
@@ -423,15 +443,37 @@ let expand_integer_cond_move a1 a2 a3 res =
end else begin
(* a1 has type _Bool, hence it is 0 or 1 *)
emit (Psubfic (GPR0, a1, Cint _0));
- (* r0 = -1 (all ones) if a1 is true, r0 = 0 if a1 is false *)
- if res <> a3 then begin
- emit (Pand_ (res, a2, GPR0));
- emit (Pandc (GPR0, a3, GPR0))
- end else begin
- emit (Pandc (res, a3, GPR0));
- emit (Pand_ (GPR0, a2, GPR0))
- end;
- emit (Por (res, res, GPR0))
+ expand_integer_cond_move_1 a2 a3 res
+ end
+
+
+(* Expansion of floating point conditional moves (Pfcmove) *)
+
+let expand_float_cond_move bit a2 a3 res =
+ emit (Pmfcr GPR0);
+ emit (Prlwinm(GPR0, GPR0, Z.of_uint (4 + num_crbit bit), _8));
+ emit (Pstfdu (a3, Cint (_m16), GPR1));
+ emit (Pcfi_adjust _16);
+ emit (Pstfd (a2, Cint (_8), GPR1));
+ emit (Plfdx (res, GPR1, GPR0));
+ emit (Paddi (GPR1, GPR1, (Cint _16)));
+ emit (Pcfi_adjust _m16)
+
+
+
+(* Symmetrically, we emulate the "isel" instruction on PPC processors
+ that do not have it. *)
+
+let expand_isel bit a2 a3 res =
+ if a2 = a3 then
+ emit (Pmr (res, a2))
+ else if eref then
+ emit (Pisel (res, a2, a3, bit))
+ else begin
+ emit (Pmfcr GPR0);
+ emit (Prlwinm(GPR0, GPR0, Z.of_uint (1 + num_crbit bit), _1));
+ emit (Psubfic (GPR0, GPR0, Cint _0));
+ expand_integer_cond_move_1 a2 a3 res
end
(* Convert integer constant into GPR with corresponding number *)
@@ -512,6 +554,26 @@ let expand_builtin_inline name args res =
emit (Plabel lbl2)
| "__builtin_cmpb", [BA(IR a1); BA(IR a2)], BR(IR res) ->
emit (Pcmpb (res,a1,a2))
+ | "__builtin_bswap64", [BA_splitlong(BA(IR ah), BA(IR al))],
+ BR_splitlong(BR(IR rh), BR(IR rl))->
+ assert (not Archi.ppc64);
+ emit (Pstwu(ah, Cint _m8, GPR1));
+ emit (Pcfi_adjust _8);
+ emit (Pstwu(al, Cint _m8, GPR1));
+ emit (Pcfi_adjust _8);
+ emit (Plwbrx(rh, GPR0, GPR1));
+ emit (Paddi(GPR1, GPR1, Cint _8));
+ emit (Pcfi_adjust _m8);
+ emit (Plwbrx(rl, GPR0, GPR1));
+ emit (Paddi(GPR1, GPR1, Cint _8));
+ emit (Pcfi_adjust _m8)
+ | "__builtin_bswap64", [BA(IR a1)], BR(IR res) ->
+ assert (Archi.ppc64);
+ emit (Pstdu(a1, Cint _m8, GPR1));
+ emit (Pcfi_adjust _8);
+ emit (Pldbrx(res, GPR0, GPR1));
+ emit (Paddi(GPR1, GPR1, Cint _8));
+ emit (Pcfi_adjust _m8)
| ("__builtin_bswap" | "__builtin_bswap32"), [BA(IR a1)], BR(IR res) ->
emit (Pstwu(a1, Cint _m8, GPR1));
emit (Pcfi_adjust _8);
@@ -772,13 +834,6 @@ let set_cr6 sg =
(* Expand instructions *)
-let num_crbit = function
- | CRbit_0 -> 0
- | CRbit_1 -> 1
- | CRbit_2 -> 2
- | CRbit_3 -> 3
- | CRbit_6 -> 6
-
let expand_instruction instr =
match instr with
| Pallocframe(sz, ofs,retofs) ->
@@ -797,7 +852,7 @@ let expand_instruction instr =
if variadic then begin
emit (Pmflr GPR0);
emit (Pbl(intern_string "__compcert_va_saveregs",
- {sig_args = []; sig_res = None; sig_cc = cc_default}));
+ {sig_args = []; sig_res = Tvoid; sig_cc = cc_default}));
emit (Pmtlr GPR0)
end;
current_function_stacksize := sz;
@@ -874,6 +929,10 @@ let expand_instruction instr =
emit (Pcfi_adjust _m8);
| Pfxdp(r1, r2) ->
if r1 <> r2 then emit(Pfmr(r1, r2))
+ | Pisel(rd, r1, r2, bit) ->
+ expand_isel bit r1 r2 rd
+ | Pfsel_gen (rd, r1, r2, bit) ->
+ expand_float_cond_move bit r1 r2 rd
| Plmake(r1, rhi, rlo) ->
if r1 = rlo then
emit (Prldimi(r1, rhi, _32L, upper32))