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

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);
+    }
+}