From a24cfb086163ab359735392340acfe03e133be64 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 8 Mar 2010 13:56:08 +0000 Subject: Handling of volatile accesses through builtin functions. Added support for processor-specific builtin functions. Added some PowerPC instructions as builtins. Updated #pragma section handling. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1285 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/CBuiltins.ml | 27 ++++++++++ cfrontend/C2Clight.ml | 123 +++++++++++++++++++++++++++++++++++------- configure | 4 +- driver/Driver.ml | 2 +- powerpc/CBuiltins.ml | 69 ++++++++++++++++++++++++ powerpc/PrintAsm.ml | 110 +++++++++++++++++++++++++++++++++++-- powerpc/eabi/CPragmas.ml | 69 ++++++++++++------------ test/regression/builtins.c | 50 +++++++++++++++++ test/regression/check-pragmas | 18 +++++++ 9 files changed, 412 insertions(+), 60 deletions(-) create mode 100644 arm/CBuiltins.ml create mode 100644 powerpc/CBuiltins.ml create mode 100644 test/regression/builtins.c create mode 100755 test/regression/check-pragmas diff --git a/arm/CBuiltins.ml b/arm/CBuiltins.ml new file mode 100644 index 0000000..2e49388 --- /dev/null +++ b/arm/CBuiltins.ml @@ -0,0 +1,27 @@ +(* *********************************************************************) +(* *) +(* 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 + +(* No ARM builtins for the moment *) + +let builtins = { + Builtins.typedefs = []; + Builtins.functions = [] +} + diff --git a/cfrontend/C2Clight.ml b/cfrontend/C2Clight.ml index 57ee8fd..fb939a4 100644 --- a/cfrontend/C2Clight.ml +++ b/cfrontend/C2Clight.ml @@ -310,14 +310,12 @@ let rec projFunType env ty = | _ -> None let convertFuncall env lhs fn args = - let lhs' = - match lhs with None -> None | Some e -> Some(convertExpr env e) in match projFunType env fn.etyp with | None -> error "wrong type for function part of a call"; Sskip | Some(res, false) -> (* Non-variadic function *) - Scall(lhs', convertExpr env fn, List.map (convertExpr env) args) + Scall(lhs, convertExpr env fn, List.map (convertExpr env) args) | Some(res, true) -> (* Variadic function: generate a call to a stub function with the appropriate number and types of arguments. Works only if @@ -334,20 +332,66 @@ let convertFuncall env lhs fn args = let tres = convertTyp env res in let (stub_fun_name, stub_fun_typ) = register_stub_function fun_name tres targs in - Scall(lhs', + Scall(lhs, Expr(Evar(intern_string stub_fun_name), stub_fun_typ), List.map (convertExpr env) args) +(* Handling of volatile *) + +let is_volatile_access env e = + List.mem C.AVolatile (Cutil.attributes_of_type env e.etyp) + && Cutil.is_lvalue env e + +let volatile_fun_suffix_type ty = + match ty with + | Tint(I8, Unsigned) -> ("int8unsigned", ty) + | Tint(I8, Signed) -> ("int8signed", ty) + | Tint(I16, Unsigned) -> ("int16unsigned", ty) + | Tint(I16, Signed) -> ("int16signed", ty) + | Tint(I32, _) -> ("int32", ty) + | Tfloat F32 -> ("float32", ty) + | Tfloat F64 -> ("float64", ty) + | Tpointer _ | Tarray _ | Tfunction _ | Tcomp_ptr _ -> + ("pointer", Tpointer Tvoid) + | _ -> + unsupported "operation on volatile struct or union"; ("", Tvoid) + +let volatile_read_fun ty = + let (suffix, ty') = volatile_fun_suffix_type ty in + Expr(Evar(intern_string ("__builtin_volatile_read_" ^ suffix)), + Tfunction(Tcons(Tpointer Tvoid, Tnil), ty')) + +let volatile_write_fun ty = + let (suffix, ty') = volatile_fun_suffix_type ty in + Expr(Evar(intern_string ("__builtin_volatile_write_" ^ suffix)), + Tfunction(Tcons(Tpointer Tvoid, Tcons(ty', Tnil)), Tvoid)) + (* Toplevel expression, argument of an Sdo *) let convertTopExpr env e = match e.edesc with | C.EBinop(C.Oassign, lhs, {edesc = C.ECall(fn, args)}, _) -> - convertFuncall env (Some lhs) fn args + convertFuncall env (Some (convertExpr env lhs)) fn args | C.EBinop(C.Oassign, lhs, rhs, _) -> if Cutil.is_composite_type env lhs.etyp then unsupported "assignment between structs or between unions"; - Sassign(convertExpr env lhs, convertExpr env rhs) + let lhs' = convertExpr env lhs + and rhs' = convertExpr env rhs in + begin match (is_volatile_access env lhs, is_volatile_access env rhs) with + | true, true -> (* should not happen *) + unsupported "volatile-to-volatile assignment"; + Sskip + | false, true -> (* volatile read *) + Scall(Some lhs', + volatile_read_fun (typeof rhs'), + [ Expr (Eaddrof rhs', Tpointer (typeof rhs')) ]) + | true, false -> (* volatile write *) + Scall(None, + volatile_write_fun (typeof lhs'), + [ Expr(Eaddrof lhs', Tpointer (typeof lhs')); rhs' ]) + | false, false -> (* regular assignment *) + Sassign(convertExpr env lhs, convertExpr env rhs) + end | C.ECall(fn, args) -> convertFuncall env None fn args | _ -> @@ -721,15 +765,12 @@ let convertProgram p = (** ** Extracting information about global variables from their atom *) let type_is_readonly env t = - let a = Cutil.attributes_of_type env t in - if List.mem C.AVolatile a then false else - if List.mem C.AConst a then true else - match Cutil.unroll env t with - | C.TArray(ty, _, _) -> - let a' = Cutil.attributes_of_type env ty in - List.mem C.AConst a' && not (List.mem C.AVolatile a') - | _ -> - false + let a1 = Cutil.attributes_of_type env t in + let a = + match Cutil.unroll env t with + | C.TArray(ty, _, _) -> a1 @ Cutil.attributes_of_type env ty + | _ -> a1 in + List.mem C.AConst a && not (List.mem C.AVolatile a) let atom_is_static a = try @@ -745,15 +786,61 @@ let atom_is_readonly a = with Not_found -> false +let atom_sizeof a = + try + let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in + Cutil.sizeof env ty + with Not_found -> + None + (** ** The builtin environment *) -let builtins = { - Builtins.typedefs = [ +open Cparser.Builtins + +let builtins_generic = { + typedefs = [ (* keeps GCC-specific headers happy, harmless for others *) "__builtin_va_list", C.TPtr(C.TVoid [], []) ]; - Builtins.functions = [ + functions = [ + (* The volatile read/volatile write functions *) + "__builtin_volatile_read_int8unsigned", + (TInt(IUChar, []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_read_int8signed", + (TInt(ISChar, []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_read_int16unsigned", + (TInt(IUShort, []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_read_int16signed", + (TInt(IShort, []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_read_int32", + (TInt(IInt, []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_read_float32", + (TFloat(FFloat, []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_read_float64", + (TFloat(FDouble, []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_read_pointer", + (TPtr(TVoid [], []), [TPtr(TVoid [], [])], false); + "__builtin_volatile_write_int8unsigned", + (TVoid [], [TPtr(TVoid [], []); TInt(IUChar, [])], false); + "__builtin_volatile_write_int8signed", + (TVoid [], [TPtr(TVoid [], []); TInt(ISChar, [])], false); + "__builtin_volatile_write_int16unsigned", + (TVoid [], [TPtr(TVoid [], []); TInt(IUShort, [])], false); + "__builtin_volatile_write_int16signed", + (TVoid [], [TPtr(TVoid [], []); TInt(IShort, [])], false); + "__builtin_volatile_write_int32", + (TVoid [], [TPtr(TVoid [], []); TInt(IInt, [])], false); + "__builtin_volatile_write_float32", + (TVoid [], [TPtr(TVoid [], []); TFloat(FFloat, [])], false); + "__builtin_volatile_write_float64", + (TVoid [], [TPtr(TVoid [], []); TFloat(FDouble, [])], false); + "__builtin_volatile_write_pointer", + (TVoid [], [TPtr(TVoid [], []); TPtr(TVoid [], [])], false) ] } +(* Add processor-dependent builtins *) +let builtins = + { typedefs = builtins_generic.typedefs @ CBuiltins.builtins.typedefs; + functions = builtins_generic.functions @ CBuiltins.builtins.functions } diff --git a/configure b/configure index d8c63fe..2ac95e3 100755 --- a/configure +++ b/configure @@ -62,7 +62,7 @@ done # Per-target configuration case "$target" in - ppc-macosx) + powerpc-macosx|ppc-macosx) arch="powerpc" variant="macosx" system="macosx" @@ -71,7 +71,7 @@ case "$target" in casm="gcc -arch ppc -c" clinker="gcc -arch ppc" libmath="";; - ppc-linux) + powerpc-linux|ppc-linux) arch="powerpc" variant="eabi" system="linux" diff --git a/driver/Driver.ml b/driver/Driver.ml index 2cc409f..d7c9364 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -63,7 +63,7 @@ let preprocess ifile ofile = let compile_c_file sourcename ifile ofile = (* Simplification options *) let simplifs = - "bec" (* blocks, impure exprs, implicit casts: mandatory *) + "becv" (* blocks, impure exprs, implicit casts, volatiles: mandatory *) ^ (if !option_fstruct_passing then "s" else "") ^ (if !option_fstruct_assign then "S" else "") ^ (if !option_fbitfields then "f" else "") in diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml new file mode 100644 index 0000000..65cd5b4 --- /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 d69d0af..69cbc17 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 d4b79b5..4bb7786 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 *) diff --git a/test/regression/builtins.c b/test/regression/builtins.c new file mode 100644 index 0000000..b13578a --- /dev/null +++ b/test/regression/builtins.c @@ -0,0 +1,50 @@ +/* Fun with PowerPC builtins */ + +#include + +#ifdef __ppc__ + +int main(int argc, char ** argv) +{ + int x = 0x12345678; + unsigned int y = 0xDEADBEEF; + + printf("mulhw(%x, %x) = %x\n", x, y, __builtin_mulhw(x, y)); + printf("mulhwu(%x, %x) = %x\n", x, y, __builtin_mulhwu(x, y)); + printf("cntlzw(%x) = %d\n", x, __builtin_cntlzw(x)); + + double a = 3.14159; + double b = 2.718; + double c = 1.414; + + printf("fmadd(%f, %f, %f) = %f\n", a, b, c, __builtin_fmadd(a, b, c)); + printf("fmsub(%f, %f, %f) = %f\n", a, b, c, __builtin_fmsub(a, b, c)); + printf("fabs(%f) = %f\n", a, __builtin_fabs(a)); + printf("fabs(%f) = %f\n", -a, __builtin_fabs(-a)); + printf("fsqrt(%f) = %f\n", a, __builtin_fsqrt(a)); + printf("frsqrte(%f) = %f\n", a, __builtin_frsqrte(a)); + printf("fres(%f) = %f\n", a, __builtin_fres(a)); + printf("fsel(%f, %f, %f) = %f\n", a, b, c, __builtin_fsel(a, b, c)); + printf("fsel(%f, %f, %f) = %f\n", -a, b, c, __builtin_fsel(-a, b, c)); + + unsigned short s = 0x1234; + printf ("read_16_rev = %x\n", __builtin_read_int16_reversed(&s)); + printf ("read_32_rev = %x\n", __builtin_read_int32_reversed(&y)); + __builtin_write_int16_reversed(&s, 0x789A); + printf ("after write_16_rev: %x\n", s); + __builtin_write_int32_reversed(&y, 0x12345678); + printf ("after write_32_rev: %x\n", y); + + __builtin_eieio(); + __builtin_sync(); + __builtin_isync(); + + return 0; +} + +#endif + + + + + diff --git a/test/regression/check-pragmas b/test/regression/check-pragmas new file mode 100755 index 0000000..404d687 --- /dev/null +++ b/test/regression/check-pragmas @@ -0,0 +1,18 @@ +#!/usr/bin/perl + +$sect = 'none'; + +while(<>) { + if (/^ (\.(text|data|sdata|sbss|sdata2))/) { + $sect = $1; + } + if (/^ (\.section.*)/) { + $sect = $1; + } + if (/([A-Za-z_][A-Za-z0-9_]*):/) { + printf ("%32s: %s\n", $1, $sect); + } + if (/([A-Za-z_][A-Za-z0-9_]*)\)?\@sda/) { + printf ("%32s: short reference\n", $1); + } +} -- cgit v1.2.3