From 9c7c84cc40eaacc1e2c13091165785cddecba5ad Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 29 Jun 2010 08:27:14 +0000 Subject: Support for inlined built-ins. AST: add ef_inline flag to external functions. Selection: recognize calls to inlined built-ins and inline them as Sbuiltin. CminorSel to Asm: added Sbuiltin/Ibuiltin instruction. PrintAsm: adapted expansion of builtins. C2Clight: adapted detection of builtins. Conventions: refactored in a machine-independent part (backend/Conventions) and a machine-dependent part (ARCH/SYS/Conventions1). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1356 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/PrintAsm.ml | 230 +++++++++++++++++++++++++++------------------------- 1 file changed, 120 insertions(+), 110 deletions(-) (limited to 'powerpc/PrintAsm.ml') diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 62e4536..b3ccb20 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -178,6 +178,11 @@ let creg oc r = | MacOS|Diab -> fprintf oc "cr%d" r | Linux -> fprintf oc "%d" r +let preg oc = function + | IR r -> ireg oc r + | FR r -> freg oc r + | _ -> assert false + (* Names of sections *) let name_of_section_MacOS = function @@ -256,7 +261,90 @@ let rec log2 n = assert (n > 0); if n = 1 then 0 else 1 + log2 (n lsr 1) -(* Built-in functions *) +(* Built-ins. They come in two flavors: + - inlined by the compiler: take their arguments in arbitrary + registers; preserve all registers except GPR12 and FPR13 + - inlined while printing asm code; take their arguments in + locations dictated by the calling conventions; preserve + callee-save regs only. *) + +let print_builtin_inlined oc name args res = + fprintf oc "%s begin builtin %s\n" comment name; + (* Can use as temporaries: GPR12, FPR13 *) + begin match name, args, res with + (* Volatile reads *) + | "__builtin_volatile_read_int8unsigned", [IR addr], IR res -> + fprintf oc " lbz %a, 0(%a)\n" ireg res ireg addr + | "__builtin_volatile_read_int8signed", [IR addr], IR res -> + fprintf oc " lbz %a, 0(%a)\n" ireg res ireg addr; + fprintf oc " extsb %a, %a\n" ireg res ireg res + | "__builtin_volatile_read_int16unsigned", [IR addr], IR res -> + fprintf oc " lhz %a, 0(%a)\n" ireg res ireg addr + | "__builtin_volatile_read_int16signed", [IR addr], IR res -> + fprintf oc " lha %a, 0(%a)\n" ireg res ireg addr + | ("__builtin_volatile_read_int32"|"__builtin_volatile_read_pointer"), [IR addr], IR res -> + fprintf oc " lwz %a, 0(%a)\n" ireg res ireg addr + | "__builtin_volatile_read_float32", [IR addr], FR res -> + fprintf oc " lfs %a, 0(%a)\n" freg res ireg addr + | "__builtin_volatile_read_float64", [IR addr], FR res -> + fprintf oc " lfd %a, 0(%a)\n" freg res ireg addr + (* Volatile writes *) + | ("__builtin_volatile_write_int8unsigned"|"__builtin_volatile_write_int8signed"), [IR addr; IR src], _ -> + fprintf oc " stb %a, 0(%a)\n" ireg src ireg addr + | ("__builtin_volatile_write_int16unsigned"|"__builtin_volatile_write_int16signed"), [IR addr; IR src], _ -> + fprintf oc " sth %a, 0(%a)\n" ireg src ireg addr + | ("__builtin_volatile_write_int32"|"__builtin_volatile_write_pointer"), [IR addr; IR src], _ -> + fprintf oc " stw %a, 0(%a)\n" ireg src ireg addr + | "__builtin_volatile_write_float32", [IR addr; FR src], _ -> + fprintf oc " frsp %a, %a\n" freg FPR13 freg src; + fprintf oc " stfs %a, 0(%a)\n" freg FPR13 ireg addr + | "__builtin_volatile_write_float64", [IR addr; FR src], _ -> + fprintf oc " stfd %a, 0(%a)\n" freg src ireg addr + (* Integer arithmetic *) + | "__builtin_mulhw", [IR a1; IR a2], IR res -> + fprintf oc " mulhw %a, %a, %a\n" ireg res ireg a1 ireg a2 + | "__builtin_mulhwu", [IR a1; IR a2], IR res -> + fprintf oc " mulhwu %a, %a, %a\n" ireg res ireg a1 ireg a2 + | "__builtin_cntlzw", [IR a1], IR res -> + fprintf oc " cntlzw %a, %a\n" ireg res ireg a1 + (* Float arithmetic *) + | "__builtin_fmadd", [FR a1; FR a2; FR a3], FR res -> + fprintf oc " fmadd %a, %a, %a, %a\n" freg res freg a1 freg a2 freg a3 + | "__builtin_fmsub", [FR a1; FR a2; FR a3], FR res -> + fprintf oc " fmsub %a, %a, %a, %a\n" freg res freg a1 freg a2 freg a3 + | "__builtin_fabs", [FR a1], FR res -> + fprintf oc " fabs %a, %a\n" freg res freg a1 + | "__builtin_fsqrt", [FR a1], FR res -> + fprintf oc " fsqrt %a, %a\n" freg res freg a1 + | "__builtin_frsqrte", [FR a1], FR res -> + fprintf oc " frsqrte %a, %a\n" freg res freg a1 + | "__builtin_fres", [FR a1], FR res -> + fprintf oc " fres %a, %a\n" freg res freg a1 + | "__builtin_fsel", [FR a1; FR a2; FR a3], FR res -> + fprintf oc " fsel %a, %a, %a, %a\n" freg res freg a1 freg a2 freg a3 + (* Memory accesses *) + | "__builtin_read_int16_reversed", [IR a1], IR res -> + fprintf oc " lhbrx %a, %a, %a\n" ireg res ireg_or_zero GPR0 ireg a1 + | "__builtin_read_int32_reversed", [IR a1], IR res -> + fprintf oc " lwbrx %a, %a, %a\n" ireg res ireg_or_zero GPR0 ireg a1 + | "__builtin_write_int16_reversed", [IR a1; IR a2], _ -> + fprintf oc " sthbrx %a, %a, %a\n" ireg a2 ireg_or_zero GPR0 ireg a1 + | "__builtin_write_int32_reversed", [IR a1; IR a2], _ -> + fprintf oc " stwbrx %a, %a, %a\n" ireg a2 ireg_or_zero GPR0 ireg a1 + (* Synchronization *) + | "__builtin_eieio", [], _ -> + fprintf oc " eieio\n" + | "__builtin_sync", [], _ -> + fprintf oc " sync\n" + | "__builtin_isync", [], _ -> + fprintf oc " isync\n" + | "__builtin_trap", [], _ -> + fprintf oc " trap\n" + (* Catch-all *) + | _ -> + invalid_arg ("unrecognized builtin " ^ name) + end; + fprintf oc "%s end builtin %s\n" comment name let re_builtin_function = Str.regexp "__builtin_" @@ -264,121 +352,42 @@ let is_builtin_function s = Str.string_match re_builtin_function (extern_atom s) 0 let print_builtin_function oc s = - fprintf oc "%s begin builtin %s\n" comment (extern_atom s); - (* int args: GPR3, GPR4 float args: FPR1, FPR2, FPR3 - int res: GPR3 float res: FPR1 + fprintf oc "%s begin builtin function %s\n" comment (extern_atom s); + (* int args: GPR3, GPR4, GPR5 float args: FPR1, FPR2, FPR3 + int res: GPR3 float res: FPR1 Watch out for MacOSX/EABI incompatibility: functions that take some floats then some ints. There are none here. *) - begin match extern_atom s with - (* Volatile reads *) - | "__builtin_volatile_read_int8unsigned" -> - fprintf oc " lbz %a, 0(%a)\n" ireg GPR3 ireg GPR3 - | "__builtin_volatile_read_int8signed" -> - fprintf oc " lbz %a, 0(%a)\n" ireg GPR3 ireg GPR3; - fprintf oc " extsb %a, %a\n" ireg GPR3 ireg GPR3 - | "__builtin_volatile_read_int16unsigned" -> - fprintf oc " lhz %a, 0(%a)\n" ireg GPR3 ireg GPR3 - | "__builtin_volatile_read_int16signed" -> - fprintf oc " lha %a, 0(%a)\n" ireg GPR3 ireg GPR3 - | "__builtin_volatile_read_int32" - | "__builtin_volatile_read_pointer" -> - fprintf oc " lwz %a, 0(%a)\n" ireg GPR3 ireg GPR3 - | "__builtin_volatile_read_float32" -> - fprintf oc " lfs %a, 0(%a)\n" freg FPR1 ireg GPR3 - | "__builtin_volatile_read_float64" -> - fprintf oc " lfd %a, 0(%a)\n" freg FPR1 ireg GPR3 - (* Volatile writes *) - | "__builtin_volatile_write_int8unsigned" - | "__builtin_volatile_write_int8signed" -> - fprintf oc " stb %a, 0(%a)\n" ireg GPR4 ireg GPR3 - | "__builtin_volatile_write_int16unsigned" - | "__builtin_volatile_write_int16signed" -> - fprintf oc " sth %a, 0(%a)\n" ireg GPR4 ireg GPR3 - | "__builtin_volatile_write_int32" - | "__builtin_volatile_write_pointer" -> - fprintf oc " stw %a, 0(%a)\n" ireg GPR4 ireg GPR3 - | "__builtin_volatile_write_float32" -> - fprintf oc " frsp %a, %a\n" freg FPR1 freg FPR1; - fprintf oc " stfs %a, 0(%a)\n" freg FPR1 ireg GPR3 - | "__builtin_volatile_write_float64" -> - fprintf oc " stfd %a, 0(%a)\n" freg FPR1 ireg GPR3 (* Block copy *) + begin match extern_atom s with | "__builtin_memcpy" -> let lbl1 = new_label() in let lbl2 = new_label() in - fprintf oc " cmplwi %a, %a, 0\n" creg 0 ireg GPR5; - fprintf oc " beq %a, %a\n" creg 0 label lbl1; - fprintf oc " mtctr %a\n" ireg GPR5; - fprintf oc " addi %a, %a, -1\n" ireg GPR3 ireg GPR3; - fprintf oc " addi %a, %a, -1\n" ireg GPR4 ireg GPR4; - fprintf oc "%a: lbzu %a, 1(%a)\n" label lbl2 ireg GPR0 ireg GPR4; - fprintf oc " stbu %a, 1(%a)\n" ireg GPR0 ireg GPR3; - fprintf oc " bdnz %a\n" label lbl2; + fprintf oc " cmplwi %a, %a, 0\n" creg 0 ireg GPR5; + fprintf oc " beq %a, %a\n" creg 0 label lbl1; + fprintf oc " mtctr %a\n" ireg GPR5; + fprintf oc " addi %a, %a, -1\n" ireg GPR3 ireg GPR3; + fprintf oc " addi %a, %a, -1\n" ireg GPR4 ireg GPR4; + fprintf oc "%a: lbzu %a, 1(%a)\n" label lbl2 ireg GPR0 ireg GPR4; + fprintf oc " stbu %a, 1(%a)\n" ireg GPR0 ireg GPR3; + fprintf oc " bdnz %a\n" label lbl2; fprintf oc "%a:\n" label lbl1 | "__builtin_memcpy_words" -> let lbl1 = new_label() in let lbl2 = new_label() in - fprintf oc " rlwinm. %a, %a, 30, 2, 31\n" ireg GPR5 ireg GPR5; - fprintf oc " beq %a, %a\n" creg 0 label lbl1; - fprintf oc " mtctr %a\n" ireg GPR5; - fprintf oc " addi %a, %a, -4\n" ireg GPR3 ireg GPR3; - fprintf oc " addi %a, %a, -4\n" ireg GPR4 ireg GPR4; - fprintf oc "%a: lwzu %a, 4(%a)\n" label lbl2 ireg GPR0 ireg GPR4; - fprintf oc " stwu %a, 4(%a)\n" ireg GPR0 ireg GPR3; - fprintf oc " bdnz %a\n" label lbl2; + fprintf oc " rlwinm. %a, %a, 30, 2, 31\n" ireg GPR5 ireg GPR5; + fprintf oc " beq %a, %a\n" creg 0 label lbl1; + fprintf oc " mtctr %a\n" ireg GPR5; + fprintf oc " addi %a, %a, -4\n" ireg GPR3 ireg GPR3; + fprintf oc " addi %a, %a, -4\n" ireg GPR4 ireg GPR4; + fprintf oc "%a: lwzu %a, 4(%a)\n" label lbl2 ireg GPR0 ireg GPR4; + fprintf oc " stwu %a, 4(%a)\n" ireg GPR0 ireg GPR3; + fprintf oc " bdnz %a\n" label lbl2; fprintf oc "%a:\n" label lbl1 - (* Integer arithmetic *) - | "__builtin_mulhw" -> - fprintf oc " mulhw %a, %a, %a\n" ireg GPR3 ireg GPR3 ireg GPR4 - | "__builtin_mulhwu" -> - fprintf oc " mulhwu %a, %a, %a\n" ireg GPR3 ireg GPR3 ireg GPR4 - | "__builtin_cntlzw" -> - fprintf oc " cntlzw %a, %a\n" ireg GPR3 ireg GPR3 - (* Float arithmetic *) - | "__builtin_fmadd" -> - fprintf oc " fmadd %a, %a, %a, %a\n" - freg FPR1 freg FPR1 freg FPR2 freg FPR3 - | "__builtin_fmsub" -> - fprintf oc " fmsub %a, %a, %a, %a\n" - freg FPR1 freg FPR1 freg FPR2 freg FPR3 - | "__builtin_fabs" -> - fprintf oc " fabs %a, %a\n" freg FPR1 freg FPR1 - | "__builtin_fsqrt" -> - fprintf oc " fsqrt %a, %a\n" freg FPR1 freg FPR1 - | "__builtin_frsqrte" -> - fprintf oc " frsqrte %a, %a\n" freg FPR1 freg FPR1 - | "__builtin_fres" -> - fprintf oc " fres %a, %a\n" freg FPR1 freg FPR1 - | "__builtin_fsel" -> - fprintf oc " fsel %a, %a, %a, %a\n" - freg FPR1 freg FPR1 freg FPR2 freg FPR3 - (* Memory accesses *) - | "__builtin_read_int16_reversed" -> - fprintf oc " lhbrx %a, %a, %a\n" - ireg GPR3 ireg_or_zero GPR0 ireg GPR3 - | "__builtin_read_int32_reversed" -> - fprintf oc " lwbrx %a, %a, %a\n" - ireg GPR3 ireg_or_zero GPR0 ireg GPR3 - | "__builtin_write_int16_reversed" -> - fprintf oc " sthbrx %a, %a, %a\n" - ireg GPR4 ireg_or_zero GPR0 ireg GPR3 - | "__builtin_write_int32_reversed" -> - fprintf oc " stwbrx %a, %a, %a\n" - ireg GPR4 ireg_or_zero GPR0 ireg GPR3 - (* Synchronization *) - | "__builtin_eieio" -> - fprintf oc " eieio\n" - | "__builtin_sync" -> - fprintf oc " sync\n" - | "__builtin_isync" -> - fprintf oc " isync\n" - | "__builtin_trap" -> - fprintf oc " trap\n" (* Catch-all *) | s -> invalid_arg ("unrecognized builtin function " ^ s) end; - fprintf oc "%s end builtin %s\n" comment (extern_atom s) + fprintf oc "%s end builtin function %s\n" comment (extern_atom s) (* Printing of instructions *) @@ -450,10 +459,7 @@ let print_instruction oc labels = function fprintf oc " lwz %a, %a(%a)\n" ireg GPR12 label_low lbl ireg GPR12; fprintf oc " mtctr %a\n" ireg GPR12; fprintf oc " bctr\n"; - fprintf oc "%a:" label lbl; - List.iter - (fun l -> fprintf oc " .long %a\n" label (transl_label l)) - tbl; + jumptables := (lbl, tbl) :: !jumptables; fprintf oc "%s end pseudoinstr btbl\n" comment | Pcmplw(r1, r2) -> fprintf oc " cmplw %a, %a, %a\n" creg 0 ireg r1 ireg r2 @@ -660,6 +666,8 @@ let print_instruction oc labels = function | Plabel lbl -> if Labelset.mem lbl labels then fprintf oc "%a:\n" label (transl_label lbl) + | Pbuiltin(ef, args, res) -> + print_builtin_inlined oc (extern_atom ef.ef_id) args res let print_literal oc (lbl, n) = let nlo = Int64.to_int32 n @@ -814,7 +822,7 @@ let stub_function oc name ef = fprintf oc " .align 2\n"; fprintf oc "L%s$stub:\n" name; if Str.string_match re_variadic_stub name 0 - then variadic_stub oc name (Str.matched_group 1 name) ef.ef_sig.sig_args + then variadic_stub oc name (Str.matched_group 1 name) (ef_sig ef).sig_args else non_variadic_stub oc name let function_needs_stub name = true @@ -839,7 +847,7 @@ let stub_function oc name ef = let name = extern_atom name in (* Only variadic functions need a stub *) if Str.string_match re_variadic_stub name 0 - then variadic_stub oc name (Str.matched_group 1 name) ef.ef_sig.sig_args + then variadic_stub oc name (Str.matched_group 1 name) (ef_sig ef).sig_args let function_needs_stub name = Str.string_match re_variadic_stub (extern_atom name) 0 @@ -858,13 +866,15 @@ let stub_function = let print_fundef oc (Coq_pair(name, defn)) = match defn with - | Internal code -> print_function oc name code - | External ef -> if not(is_builtin_function name) then stub_function oc name ef + | Internal code -> + print_function oc name code + | External ef -> + if not (is_builtin_function name) then stub_function oc name ef let record_extfun (Coq_pair(name, defn)) = match defn with | Internal _ -> () - | External _ -> + | External _ -> if function_needs_stub name && not (is_builtin_function name) then stubbed_functions := IdentSet.add name !stubbed_functions -- cgit v1.2.3