diff options
Diffstat (limited to 'powerpc')
| -rw-r--r-- | powerpc/CBuiltins.ml | 69 | ||||
| -rw-r--r-- | powerpc/PrintAsm.ml | 110 | ||||
| -rw-r--r-- | powerpc/eabi/CPragmas.ml | 69 |
3 files changed, 209 insertions, 39 deletions
diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml new file mode 100644 index 00000000..65cd5b4f --- /dev/null +++ b/powerpc/CBuiltins.ml @@ -0,0 +1,69 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the GNU General Public License as published by *) +(* the Free Software Foundation, either version 2 of the License, or *) +(* (at your option) any later version. This file is also distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +(* Processor-dependent builtin C functions *) + +open Cparser +open C + +let builtins = { + Builtins.typedefs = []; + Builtins.functions = [ + (* Integer arithmetic *) + "__builtin_mulhw", + (TInt(IInt, []), [TInt(IInt, []); TInt(IInt, [])], false); + "__builtin_mulhwu", + (TInt(IUInt, []), [TInt(IUInt, []); TInt(IUInt, [])], false); + "__builtin_cntlzw", + (TInt(IUInt, []), [TInt(IUInt, [])], false); + (* Float arithmetic *) + "__builtin_fmadd", + (TFloat(FDouble, []), + [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])], + false); + "__builtin_fmsub", + (TFloat(FDouble, []), + [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])], + false); + "__builtin_fabs", + (TFloat(FDouble, []), [TFloat(FDouble, [])], false); + "__builtin_fsqrt", + (TFloat(FDouble, []), [TFloat(FDouble, [])], false); + "__builtin_frsqrte", + (TFloat(FDouble, []), [TFloat(FDouble, [])], false); + "__builtin_fres", + (TFloat(FFloat, []), [TFloat(FFloat, [])], false); + "__builtin_fsel", + (TFloat(FDouble, []), + [TFloat(FDouble, []); TFloat(FDouble, []); TFloat(FDouble, [])], + false); + (* Memory accesses *) + "__builtin_read_int16_reversed", + (TInt(IUShort, []), [TPtr(TInt(IUShort, []), [])], false); + "__builtin_read_int32_reversed", + (TInt(IUInt, []), [TPtr(TInt(IUInt, []), [])], false); + "__builtin_write_int16_reversed", + (TVoid [], [TPtr(TInt(IUShort, []), []); TInt(IUShort, [])], false); + "__builtin_write_int32_reversed", + (TVoid [], [TPtr(TInt(IUInt, []), []); TInt(IUInt, [])], false); + (* Synchronization *) + "__builtin_eieio", + (TVoid [], [], false); + "__builtin_sync", + (TVoid [], [], false); + "__builtin_isync", + (TVoid [], [], false) + ] +} diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index d69d0aff..69cbc173 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -212,6 +212,100 @@ let rolm_mask n = assert (!count = 2 || (!count = 0 && !last)); (!mb, !me-1) +(* Built-in functions *) + +let re_builtin_function = Str.regexp "__builtin_" + +let is_builtin_function s = + Str.string_match re_builtin_function (extern_atom s) 0 + +let print_builtin_function oc s = + (* int args: GPR3, GPR4 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. *) + 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 + (* 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" + (* Catch-all *) + | s -> + invalid_arg ("unrecognized builtin function " ^ s) + (* Printing of instructions *) module Labelset = Set.Make(struct type t = label let compare = compare end) @@ -251,9 +345,17 @@ let print_instruction oc labels = function | Pbf(bit, lbl) -> fprintf oc " bf %a, %a\n" crbit bit label (transl_label lbl) | Pbl s -> - fprintf oc " bl %a\n" symbol s + if not (is_builtin_function s) then + fprintf oc " bl %a\n" symbol s + else + print_builtin_function oc s | Pbs s -> - fprintf oc " b %a\n" symbol s + if not (is_builtin_function s) then + fprintf oc " b %a\n" symbol s + else begin + print_builtin_function oc s; + fprintf oc " blr\n" + end | Pblr -> fprintf oc " blr\n" | Pbt(bit, lbl) -> @@ -653,13 +755,13 @@ let stub_function = let print_fundef oc (Coq_pair(name, defn)) = match defn with | Internal code -> print_function oc name code - | External ef -> stub_function oc name ef + | 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 _ -> - if function_needs_stub name then + if function_needs_stub name && not (is_builtin_function name) then stubbed_functions := IdentSet.add name !stubbed_functions let print_init oc = function diff --git a/powerpc/eabi/CPragmas.ml b/powerpc/eabi/CPragmas.ml index d4b79b52..4bb7786e 100644 --- a/powerpc/eabi/CPragmas.ml +++ b/powerpc/eabi/CPragmas.ml @@ -16,8 +16,8 @@ (* Platform-dependent handling of pragmas *) open Printf -open Cil open Camlcoq +open Cparser type section_info = { sec_name_init: string; @@ -94,7 +94,7 @@ let process_use_section_pragma classname id = let info = Hashtbl.find section_table classname in Hashtbl.add use_section_table (intern_string id) info with Not_found -> - Cil2Csyntax.error (sprintf "unknown section name `%s'" classname) + C2Clight.error (sprintf "unknown section name `%s'" classname) let default_use_section id classname = if not (Hashtbl.mem use_section_table id) then begin @@ -104,23 +104,25 @@ let default_use_section id classname = Hashtbl.add use_section_table id info end -let define_function id v = +let define_function id d = default_use_section id "CODE" -let define_stringlit id v = +let define_stringlit id = default_use_section id "STRING" -let define_variable id v = - let sz = Cil.bitsSizeOf v.vtype / 8 in +let define_variable id d = + let is_small limit = + match C2Clight.atom_sizeof id with + | None -> false + | Some sz -> sz <= limit in let sect = - if Cil2Csyntax.var_is_readonly v then - if sz <= !Clflags.option_small_const then "SCONST" else "CONST" + if C2Clight.atom_is_readonly id then + if is_small !Clflags.option_small_const then "SCONST" else "CONST" else - if sz <= !Clflags.option_small_data then "SDATA" else "DATA" in + if is_small !Clflags.option_small_data then "SDATA" else "DATA" in default_use_section id sect -(* CIL does not parse the "section" and "use_section" pragmas, which - have irregular syntax, so we parse them using regexps *) +(* Parsing of pragmas using regexps *) let re_start_pragma_section = Str.regexp "section\\b" @@ -142,7 +144,7 @@ let re_pragma_use_section = Str.regexp let re_split_idents = Str.regexp "[ \t,]+" -let process_pragma (Attr(name, _)) = +let process_pragma name = if Str.string_match re_pragma_section name 0 then begin process_section_pragma (Str.matched_group 1 name) (* classname *) @@ -152,44 +154,41 @@ let process_pragma (Attr(name, _)) = (Str.matched_group 5 name); (* accmode *) true end else if Str.string_match re_start_pragma_section name 0 then - Cil2Csyntax.error "ill-formed `section' pragma" + (C2Clight.error "ill-formed `section' pragma"; true) else if Str.string_match re_pragma_use_section name 0 then begin let classname = Str.matched_group 1 name and idents = Str.matched_group 2 name in let identlist = Str.split re_split_idents idents in - if identlist = [] then Cil2Csyntax.warning "vacuous `use_section' pragma"; + if identlist = [] then C2Clight.warning "vacuous `use_section' pragma"; List.iter (process_use_section_pragma classname) identlist; true end else if Str.string_match re_start_pragma_use_section name 0 then - Cil2Csyntax.error "ill-formed `use_section' pragma" + (C2Clight.error "ill-formed `use_section' pragma"; true) else false let initialize () = - Cil2Csyntax.process_pragma_hook := process_pragma; - Cil2Csyntax.define_variable_hook := define_variable; - Cil2Csyntax.define_function_hook := define_function; - Cil2Csyntax.define_stringlit_hook := define_stringlit + C2Clight.process_pragma_hook := process_pragma; + C2Clight.define_variable_hook := define_variable; + C2Clight.define_function_hook := define_function; + C2Clight.define_stringlit_hook := define_stringlit (* PowerPC-specific: say if an atom is in a small data area *) let atom_is_small_data a ofs = - begin try - let v = Hashtbl.find Cil2Csyntax.varinfo_atom a in - let sz = Cil.bitsSizeOf v.vtype / 8 in - let ofs = camlint_of_coqint ofs in - if ofs >= 0l && ofs < Int32.of_int sz then begin - try - (Hashtbl.find use_section_table a).sec_near_access - with Not_found -> - if Cil2Csyntax.var_is_readonly v - then sz <= !Clflags.option_small_const - else sz <= !Clflags.option_small_data - end else - false - with Not_found -> - false - end + match C2Clight.atom_sizeof a with + | None -> false + | Some sz -> + let ofs = camlint_of_coqint ofs in + if ofs >= 0l && ofs < Int32.of_int sz then begin + try + (Hashtbl.find use_section_table a).sec_near_access + with Not_found -> + if C2Clight.atom_is_readonly a + then sz <= !Clflags.option_small_const + else sz <= !Clflags.option_small_data + end else + false (* PowerPC-specific: determine section to use for a particular symbol *) |