summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--arm/CBuiltins.ml27
-rw-r--r--cfrontend/C2Clight.ml123
-rwxr-xr-xconfigure4
-rw-r--r--driver/Driver.ml2
-rw-r--r--powerpc/CBuiltins.ml69
-rw-r--r--powerpc/PrintAsm.ml110
-rw-r--r--powerpc/eabi/CPragmas.ml69
-rw-r--r--test/regression/builtins.c50
-rwxr-xr-xtest/regression/check-pragmas18
9 files changed, 412 insertions, 60 deletions
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 <stdio.h>
+
+#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);
+ }
+}