diff --git a/arm/Asm.v b/arm/Asm.v
index 79feee72bbd3dd1d830ac35de5294a68df64423f..a8151a85911020834c3cdd754c1bb675f8adc52b 100644
--- a/arm/Asm.v
+++ b/arm/Asm.v
@@ -152,82 +152,38 @@ Inductive instruction : Type :=
(** The pseudo-instructions are the following:
-- [Plabel]: define a code label at the current program point
-- [Plfi]: load a floating-point constant in a float register.
- Expands to a float load [lfd] from an address in the constant data section
- initialized with the floating-point constant:
+- [Plabel]: define a code label at the current program point.
+- [Ploadsymbol]: load the address of a symbol in an integer register.
+ Expands to a load from an address in the constant data section
+ initialized with the symbol value:
<<
- addis r2, 0, ha16(lbl)
- lfd rdst, lo16(lbl)(r2)
+ ldr rdst, lbl
.const_data
-lbl: .double floatcst
+lbl: .word symbol
.text
>>
Initialized data in the constant data section are not modeled here,
which is why we use a pseudo-instruction for this purpose.
-- [Pfcti]: convert a float to an integer. This requires a transfer
- via memory of a 32-bit integer from a float register to an int register,
- which our memory model cannot express. Expands to:
-<<
- fctiwz f13, rsrc
- stfdu f13, -8(r1)
- lwz rdst, 4(r1)
- addi r1, r1, 8
->>
-- [Pictf]: convert a signed integer to a float. This requires complicated
- bit-level manipulations of IEEE floats through mixed float and integer
- arithmetic over a memory word, which our memory model and axiomatization
- of floats cannot express. Expands to:
-<<
- addis r2, 0, 0x4330
- stwu r2, -8(r1)
- addis r2, rsrc, 0x8000
- stw r2, 4(r1)
- addis r2, 0, ha16(lbl)
- lfd f13, lo16(lbl)(r2)
- lfd rdst, 0(r1)
- addi r1, r1, 8
- fsub rdst, rdst, f13
- .const_data
-lbl: .long 0x43300000, 0x80000000
- .text
->>
- (Don't worry if you do not understand this instruction sequence: intimate
- knowledge of IEEE float arithmetic is necessary.)
-- [Piuctf]: convert an unsigned integer to a float. The expansion is close
- to that [Pictf], and equally obscure.
-<<
- addis r2, 0, 0x4330
- stwu r2, -8(r1)
- stw rsrc, 4(r1)
- addis r2, 0, ha16(lbl)
- lfd f13, lo16(lbl)(r2)
- lfd rdst, 0(r1)
- addi r1, r1, 8
- fsub rdst, rdst, f13
- .const_data
-lbl: .long 0x43300000, 0x00000000
- .text
->>
-- [Pallocframe lo hi]: in the formal semantics, this pseudo-instruction
+- [Pallocframe lo hi pos]: in the formal semantics, this pseudo-instruction
allocates a memory block with bounds [lo] and [hi], stores the value
- of register [r1] (the stack pointer, by convention) at the bottom
- of this block, and sets [r1] to a pointer to the bottom of this
- block. In the printed PowerPC assembly code, this allocation
- is just a store-decrement of register [r1]:
+ of the stack pointer at offset [pos] in this block, and sets the
+ stack pointer to the address of the bottom of this block.
+ In the printed ASM assembly code, this allocation is:
<<
- stwu r1, (lo - hi)(r1)
+ mov r12, sp
+ sub sp, sp, #(hi - lo)
+ str r12, [sp, #pos]
>>
This cannot be expressed in our memory model, which does not reflect
the fact that stack frames are adjacent and allocated/freed
following a stack discipline.
-- [Pfreeframe]: in the formal semantics, this pseudo-instruction
- reads the bottom word of the block pointed by [r1] (the stack pointer),
- frees this block, and sets [r1] to the value of the bottom word.
- In the printed PowerPC assembly code, this freeing
- is just a load of register [r1] relative to [r1] itself:
+- [Pfreeframe pos]: in the formal semantics, this pseudo-instruction
+ reads the word at [pos] of the block pointed by the stack pointer,
+ frees this block, and sets the stack pointer to the value read.
+ In the printed ASM assembly code, this freeing
+ is just a load of register [sp] relative to [sp] itself:
<<
- lwz r1, 0(r1)
+ ldr sp, [sp, #pos]
>>
Again, our memory model cannot comprehend that this operation
frees (logically) the current stack frame.
@@ -239,8 +195,7 @@ Definition program := AST.program fundef unit.
(** * Operational semantics *)
-(** The PowerPC has a great many registers, some general-purpose, some very
- specific. We model only the following registers: *)
+(** We model the following registers of the ARM architecture. *)
Inductive preg: Type :=
| IR: ireg -> preg (**r integer registers *)
@@ -591,7 +546,7 @@ Definition preg_of (r: mreg) :=
(** Extract the values of the arguments of an external call.
We exploit the calling conventions from module [Conventions], except that
- we use PPC registers instead of locations. *)
+ we use ARM registers instead of locations. *)
Inductive extcall_arg (rs: regset) (m: mem): loc -> val -> Prop :=
| extcall_arg_reg: forall r,
@@ -665,9 +620,3 @@ Inductive final_state: state -> int -> Prop :=
Definition exec_program (p: program) (beh: program_behavior) : Prop :=
program_behaves step (initial_state p) final_state (Genv.globalenv p) beh.
-
-
-(** For compatibility with PowerPC *)
-
-Parameter low_half: val -> val.
-Parameter high_half: val -> val.
diff --git a/arm/SelectOp.v b/arm/SelectOp.v
index 49676f839e00a07b175e4be83971aaa58838f9a0..4b5fde7ff9f65593bfc651ef68b3922a1614577e 100644
--- a/arm/SelectOp.v
+++ b/arm/SelectOp.v
@@ -1193,7 +1193,4 @@ Definition addressing (chunk: memory_chunk) (e: expr) :=
(Aindexed Int.zero, e:::Enil)
end.
-(** For compatibility with PowerPC, but unused. *)
-
-Parameter use_fused_mul : unit -> bool.
diff --git a/arm/extractionMachdep.v b/arm/extractionMachdep.v
new file mode 100644
index 0000000000000000000000000000000000000000..f6e17bab714c5530b8cd4f1b05ea16afd966c4d8
--- /dev/null
+++ b/arm/extractionMachdep.v
@@ -0,0 +1,18 @@
+(* *********************************************************************)
+(* *)
+(* 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 INRIA Non-Commercial License Agreement. *)
+(* *)
+(* *********************************************************************)
+
+(* Additional extraction directives specific to the ARM port *)
+
+(* Suppression of stupidly big equality functions *)
+Extract Constant Asm.ireg_eq => "fun (x: ireg) (y: ireg) -> x = y".
+Extract Constant Asm.freg_eq => "fun (x: freg) (y: freg) -> x = y".
+Extract Constant Asm.preg_eq => "fun (x: preg) (y: preg) -> x = y".
diff --git a/arm/linux/CPragmas.ml b/arm/linux/CPragmas.ml
new file mode 100644
index 0000000000000000000000000000000000000000..1602f9f100f9010ae1de8c20db7dbdeda06d6e3d
--- /dev/null
+++ b/arm/linux/CPragmas.ml
@@ -0,0 +1,20 @@
+(* *********************************************************************)
+(* *)
+(* 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. *)
+(* *)
+(* *********************************************************************)
+
+(* Platform-dependent handling of pragmas *)
+
+(* No pragmas supported on ARM/Linux *)
+
+let initialize () = ()
diff --git a/cfrontend/Cil2Csyntax.ml b/cfrontend/Cil2Csyntax.ml
index 16daa1418e193042cbaa2f475490b80597e99b8c..70252354f43a561aa093c0543184214fa71fbf8c 100644
--- a/cfrontend/Cil2Csyntax.ml
+++ b/cfrontend/Cil2Csyntax.ml
@@ -25,12 +25,45 @@ open Csyntax
(* To associate CIL varinfo to the atoms representing global variables *)
-let varinfo_atom : (BinPos.positive, Cil.varinfo) Hashtbl.t =
+let varinfo_atom : (AST.ident, Cil.varinfo) Hashtbl.t =
Hashtbl.create 103
-(* Evaluate compile-time constant expressions. This is a more
- aggressive variant of [Cil.constFold], which does not handle
- floats. *)
+(** Functions used to handle locations *)
+
+let currentLocation = ref Cil.locUnknown
+
+(** Update the current location *)
+let updateLoc loc =
+ currentLocation := loc
+
+(** Convert the current location into a string *)
+let currentLoc() =
+ match !currentLocation with { line=l; file=f } ->
+ f ^ ":" ^ (if l = -1 then "?" else string_of_int l) ^ ": "
+
+(** Exception raised when an error in the C source is encountered,
+ e.g. unsupported C feature *)
+
+exception Error of string
+
+let error msg =
+ raise (Error(currentLoc() ^ msg))
+
+let unsupported msg =
+ error ("Unsupported C feature: " ^ msg)
+
+let internal_error msg =
+ error ("Internal error: " ^ msg ^ "\nPlease report it.")
+
+(** Warning messages *)
+let warning msg =
+ prerr_string (currentLoc());
+ prerr_string "Warning: ";
+ prerr_endline msg
+
+(** Evaluate compile-time constant expressions. This is a more
+ aggressive variant of [Cil.constFold], which does not handle
+ floats. *)
exception NotConst
@@ -168,9 +201,14 @@ and eval_cast ty v =
| TPtr(_, _), CWStr s -> v (* tolerance? *)
| _, _ -> raise NotConst
+(** Handler for #pragma directives --
+ overriden in machine-dependent CPragmas module *)
-(* The parameter to the translation functor: it specifies the
- translation for integer and float types. *)
+let process_pragma = ref (fun (a: Cil.attribute) -> false)
+
+
+(** The parameter to the translation functor: it specifies the
+ translation for integer and float types. *)
module type TypeSpecifierTranslator =
sig
@@ -189,7 +227,6 @@ let const0 = Expr (Econst_int (coqint_of_camlint Int32.zero), constInt32)
(** Global variables *)
-let currentLocation = ref Cil.locUnknown
let stringNum = ref 0 (* number of next global for string literals *)
let stringTable = Hashtbl.create 47
@@ -245,33 +282,6 @@ let rec keepUntil elt' = function
let keepBetween elt elt' l =
keepUntil elt' (keepFrom elt l)
-(** ** Functions used to handle locations *)
-
-(** Update the current location *)
-let updateLoc loc =
- currentLocation := loc
-
-(** Convert the current location into a string *)
-let currentLoc() =
- match !currentLocation with { line=l; file=f } ->
- f ^ ":" ^ (if l = -1 then "?" else string_of_int l) ^ ": "
-
-(** Exception raised when an unsupported feature is encountered *)
-exception Unsupported of string
-let unsupported msg =
- raise (Unsupported(currentLoc() ^ "Unsupported C feature: " ^ msg))
-
-(** Exception raised when an internal error is encountered *)
-exception Internal_error of string
-let internal_error msg =
- raise (Internal_error(currentLoc() ^ "Internal error: " ^ msg))
-
-(** Warning messages *)
-let warning msg =
- prerr_string (currentLoc());
- prerr_string "Warning: ";
- prerr_endline msg
-
(** ** Functions used to handle string literals *)
let name_for_string_literal s =
@@ -1187,9 +1197,10 @@ let rec processGlobals = function
| GAsm (_, loc) ->
updateLoc(loc);
unsupported "inline assembly"
- | GPragma (_, loc) ->
+ | GPragma (Attr(name, _) as attr, loc) ->
updateLoc(loc);
- warning "#pragma directive ignored";
+ if not (!process_pragma attr) then
+ warning ("#pragma `" ^ name ^ "' directive ignored");
processGlobals l
| GText _ -> processGlobals l (* comments are ignored *)
@@ -1251,17 +1262,3 @@ let atom_is_readonly a =
| _ -> false
with Not_found ->
false
-
-let atom_is_small_data a ofs =
- match Configuration.system with
- | "diab" ->
- begin try
- let v = Hashtbl.find varinfo_atom a in
- let sz = Cil.bitsSizeOf v.vtype / 8 in
- let ofs = camlint_of_coqint ofs in
- sz <= 8 && ofs >= 0l && ofs < Int32.of_int sz
- with Not_found ->
- false
- end
- | _ ->
- false
diff --git a/cil/src/frontc/clexer.mll b/cil/src/frontc/clexer.mll
index 08f788193338d934e0b276393a444fa5df05a155..41c8692248a6be66ff39165d0e0841fea0e04413 100644
--- a/cil/src/frontc/clexer.mll
+++ b/cil/src/frontc/clexer.mll
@@ -418,13 +418,15 @@ let hex_escape = '\\' ['x' 'X'] hexdigit+
let oct_escape = '\\' octdigit octdigit? octdigit?
(* Pragmas that are not parsed by CIL. We lex them as PRAGMA_LINE tokens *)
+
let no_parse_pragma =
"warning" | "GCC"
(* Solaris-style pragmas: *)
| "ident" | "section" | "option" | "asm" | "use_section" | "weak"
| "redefine_extname"
| "TCS_align"
-
+ (* Added by XL *)
+ | "global_register"
rule initial =
parse "/*" { let il = comment lexbuf in
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index 08e4a5369f1309674844ee47c55ad4f551dddb86..c6f6e8fe2820347c326e39975b8f89933ac0da3a 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -17,6 +17,7 @@ let linker_options = ref ([]: string list)
let exe_name = ref "a.out"
let option_flonglong = ref false
let option_fmadd = ref false
+let option_dcil = ref false
let option_dclight = ref false
let option_dasm = ref false
let option_E = ref false
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 30d4a6cc29aa1c19f023002858372dd50f686071..b818680481f4bdfe74aebdd4f796c84125297189 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -118,21 +118,26 @@ let compile_c_file sourcename ifile ofile =
cil.Cil.fileName <- sourcename;
(* Cleanup in the CIL.file *)
Rmtmps.removeUnusedTemps ~isRoot:Rmtmps.isExportedRoot cil;
+ (* Save CIL output if requested *)
+ if !option_dcil then begin
+ let ofile = Filename.chop_suffix sourcename ".c" ^ ".cil.c" in
+ let oc = open_out ofile in
+ Cil.dumpFile Cil.defaultCilPrinter oc ofile cil;
+ close_out oc
+ end;
(* Conversion to Csyntax *)
let csyntax =
try
Cil2CsyntaxTranslator.convertFile cil
with
- | Cil2CsyntaxTranslator.Unsupported msg ->
+ | Cil2Csyntax.Error msg ->
eprintf "%s\n" msg;
exit 2
- | Cil2CsyntaxTranslator.Internal_error msg ->
- eprintf "%s\nPlease report it.\n" msg;
- exit 2 in
+ in
(* Save Csyntax if requested *)
if !option_dclight then begin
- let targetname = Filename.chop_suffix sourcename ".c" in
- let oc = open_out (targetname ^ ".light.c") in
+ let ofile = Filename.chop_suffix sourcename ".c" ^ ".light.c" in
+ let oc = open_out ofile in
PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax;
close_out oc
end;
@@ -264,6 +269,7 @@ Preprocessing options:
Compilation options:
-flonglong Treat 'long long' as 'long' and 'long double' as 'double'
-fmadd Use fused multiply-add and multiply-sub instructions
+ -dcil Save CIL-processed source in <file>.cil.c
-dclight Save generated Clight in <file>.light.c
-dasm Save generated assembly in <file>.s
Linking options:
@@ -303,6 +309,10 @@ let rec parse_cmdline i =
option_fmadd := true;
parse_cmdline (i + 1)
end else
+ if s = "-dcil" then begin
+ option_dcil := true;
+ parse_cmdline (i + 1)
+ end else
if s = "-dclight" then begin
option_dclight := true;
parse_cmdline (i + 1)
@@ -348,6 +358,8 @@ let rec parse_cmdline i =
end
let _ =
+ Cil.initCIL();
+ CPragmas.initialize();
parse_cmdline 1;
if not (!option_c || !option_S || !option_E) then begin
linker !exe_name !linker_options
diff --git a/extraction/extraction.v b/extraction/extraction.v
index 86b9b4c8756d642d0fd239f72fa448ba9465e100..77c6c62bbc9cbe9da5704befe3efeec5012f9917 100644
--- a/extraction/extraction.v
+++ b/extraction/extraction.v
@@ -69,20 +69,15 @@ Extract Constant Coloring.graph_coloring => "Coloringaux.graph_coloring".
(* Linearize *)
Extract Constant Linearize.enumerate_aux => "Linearizeaux.enumerate_aux".
-(* Asm *)
-Extract Constant Asm.low_half => "fun _ -> assert false".
-Extract Constant Asm.high_half => "fun _ -> assert false".
-Extract Constant Asm.symbol_is_small_data => "Cil2Csyntax.atom_is_small_data".
-Extract Constant Asm.small_data_area_offset => "fun _ _ _ -> assert false".
-
(* Suppression of stupidly big equality functions *)
Extract Constant Op.eq_operation => "fun (x: operation) (y: operation) -> x = y".
Extract Constant Op.eq_addressing => "fun (x: addressing) (y: addressing) -> x = y".
(*Extract Constant CSE.eq_rhs => "fun (x: rhs) (y: rhs) -> x = y".*)
Extract Constant Machregs.mreg_eq => "fun (x: mreg) (y: mreg) -> x = y".
-Extract Constant Asm.ireg_eq => "fun (x: ireg) (y: ireg) -> x = y".
-Extract Constant Asm.freg_eq => "fun (x: freg) (y: freg) -> x = y".
-Extract Constant Asm.preg_eq => "fun (x: preg) (y: preg) -> x = y".
+
+(* Processor-specific extraction directives *)
+
+Load extractionMachdep.
(* Avoid name clashes *)
Extraction Blacklist List String Int.
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 95074988aeb52ab345e55d059986fe8f47ff017f..539d9894e5f97cd6233166d8cc51ccddf1589ccf 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -192,9 +192,9 @@ let (text, data, const_data, sdata, float_literal) =
| Diab ->
(".text",
".data",
- ".data", (* to check *)
- ".sdata", (* to check *)
- ".data") (* to check *)
+ ".data", (* or: .rodata? *)
+ ".sdata", (* to check *)
+ ".data") (* or: .rodata? *)
(* Encoding masks for rlwinm instructions *)
@@ -480,7 +480,10 @@ let rec labels_of_code = function
let print_function oc name code =
Hashtbl.clear current_function_labels;
- section oc text;
+ section oc
+ (match CPragmas.section_for_atom name true with
+ | Some s -> ".section\t" ^ s
+ | None -> text);
fprintf oc " .align 2\n";
if not (Cil2Csyntax.atom_is_static name) then
fprintf oc " .globl %a\n" symbol name;
@@ -692,13 +695,19 @@ let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) =
match init_data with
| [] -> ()
| _ ->
+ let init =
+ match init_data with [Init_space _] -> false | _ -> true in
let sec =
- if Cil2Csyntax.atom_is_small_data name (coqint_of_camlint 0l) then
- sdata
- else if Cil2Csyntax.atom_is_readonly name then
- const_data
- else
- data in
+ match CPragmas.section_for_atom name init with
+ | Some s -> ".section\t" ^ s
+ | None ->
+ if CPragmas.atom_is_small_data name (coqint_of_camlint 0l) then
+ sdata
+ else if Cil2Csyntax.atom_is_readonly name then
+ const_data
+ else
+ data
+ in
section oc sec;
fprintf oc " .align 3\n";
if not (Cil2Csyntax.atom_is_static name) then
diff --git a/powerpc/eabi/CPragmas.ml b/powerpc/eabi/CPragmas.ml
new file mode 100644
index 0000000000000000000000000000000000000000..9d2eb8a4b953427b9808f08050d11f23c4a4bdae
--- /dev/null
+++ b/powerpc/eabi/CPragmas.ml
@@ -0,0 +1,134 @@
+(* *********************************************************************)
+(* *)
+(* 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. *)
+(* *)
+(* *********************************************************************)
+
+(* Platform-dependent handling of pragmas *)
+
+open Printf
+open Cil
+open Camlcoq
+
+type section_info = {
+ sec_name_init: string;
+ sec_name_uninit: string;
+ sec_near_access: bool
+}
+
+let section_table : (string, section_info) Hashtbl.t =
+ Hashtbl.create 17
+
+let use_section_table : (AST.ident, section_info) Hashtbl.t =
+ Hashtbl.create 51
+
+let process_section_pragma classname istring ustring addrmode accmode =
+ let is_near = (addrmode = "near-absolute") || (addrmode = "near-data") in
+ let is_writable = String.contains accmode 'W'
+ and is_executable = String.contains accmode 'X' in
+ let sec_type =
+ match is_writable, is_executable with
+ | true, true -> 'm' (* text+data *)
+ | true, false -> 'd' (* data *)
+ | false, true -> 'c' (* text *)
+ | false, false -> 'r' (* const *)
+ in
+ let info =
+ { sec_name_init = sprintf "%s,,%c" istring sec_type;
+ sec_name_uninit = sprintf "%s,,%c" ustring sec_type;
+ sec_near_access = is_near } in
+ Hashtbl.add section_table classname info
+
+let process_use_section_pragma classname id =
+ try
+ 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)
+
+(* CIL does not parse the "section" and "use_section" pragmas, which
+ have irregular syntax, so we parse them using regexps *)
+
+let re_start_pragma_section = Str.regexp "section\\b"
+
+let re_pragma_section = Str.regexp
+ "section[ \t]+\
+ \\([A-Za-z_][A-Za-z_0-9]*\\)[ \t]+\
+ \"\\([^\"]*\\)\"[ \t]+\
+ \"\\([^\"]*\\)\"[ \t]+\
+ \\([a-z-]+\\)[ \t]+\
+ \\([A-Z]+\\)"
+
+let re_start_pragma_use_section = Str.regexp "use_section\\b"
+
+let re_pragma_use_section = Str.regexp
+ "use_section[ \t]+\
+ \\([A-Za-z_][A-Za-z_0-9]*\\)[ \t]+\
+ \\(.*\\)$"
+
+let re_split_idents = Str.regexp "[ \t,]+"
+
+let process_pragma (Attr(name, _)) =
+ if Str.string_match re_pragma_section name 0 then begin
+ process_section_pragma
+ (Str.matched_group 1 name) (* classname *)
+ (Str.matched_group 2 name) (* istring *)
+ (Str.matched_group 3 name) (* ustring *)
+ (Str.matched_group 4 name) (* addrmode *)
+ (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"
+ 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";
+ 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"
+ else
+ false
+
+let initialize () =
+ Cil2Csyntax.process_pragma := process_pragma
+
+(* PowerPC-specific: say if an atom is in a small data area *)
+
+let atom_is_small_data a ofs =
+ match Configuration.system with
+ | "diab" ->
+ 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 -> sz <= 8
+ end else
+ false
+ with Not_found ->
+ false
+ end
+ | _ ->
+ false
+
+(* PowerPC-specific: determine section to use for a particular symbol *)
+
+let section_for_atom a init =
+ try
+ let sinfo = Hashtbl.find use_section_table a in
+ Some(if init then sinfo.sec_name_init else sinfo.sec_name_uninit)
+ with Not_found ->
+ None
+
diff --git a/powerpc/extractionMachdep.v b/powerpc/extractionMachdep.v
new file mode 100644
index 0000000000000000000000000000000000000000..46c40caed6b1895f45cd4acdbcccc5a793ffcd9c
--- /dev/null
+++ b/powerpc/extractionMachdep.v
@@ -0,0 +1,24 @@
+(* *********************************************************************)
+(* *)
+(* 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 INRIA Non-Commercial License Agreement. *)
+(* *)
+(* *********************************************************************)
+
+(* Additional extraction directives specific to the PowerPC port *)
+
+(* Asm *)
+Extract Constant Asm.low_half => "fun _ -> assert false".
+Extract Constant Asm.high_half => "fun _ -> assert false".
+Extract Constant Asm.symbol_is_small_data => "CPragmas.atom_is_small_data".
+Extract Constant Asm.small_data_area_offset => "fun _ _ _ -> assert false".
+
+(* Suppression of stupidly big equality functions *)
+Extract Constant Asm.ireg_eq => "fun (x: ireg) (y: ireg) -> x = y".
+Extract Constant Asm.freg_eq => "fun (x: freg) (y: freg) -> x = y".
+Extract Constant Asm.preg_eq => "fun (x: preg) (y: preg) -> x = y".
diff --git a/powerpc/macosx/CPragmas.ml b/powerpc/macosx/CPragmas.ml
new file mode 100644
index 0000000000000000000000000000000000000000..f48064ceaf29145e2b14da030b5da2bfc062245a
--- /dev/null
+++ b/powerpc/macosx/CPragmas.ml
@@ -0,0 +1,28 @@
+(* *********************************************************************)
+(* *)
+(* 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. *)
+(* *)
+(* *********************************************************************)
+
+(* Platform-dependent handling of pragmas *)
+
+(* No pragmas supported on PowerPC/MacOS *)
+
+let initialize () = ()
+
+(* PowerPC-specific: say if an atom is in a small data area *)
+
+let atom_is_small_data a ofs = false
+
+(* PowerPC-specific: determine section to use for a particular symbol *)
+
+let section_for_atom a init = None