From 0486654fac91947fec93d18a0738dd7aa10bcf96 Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 3 Nov 2009 08:43:54 +0000 Subject: PowerPC/EABI port: preliminary support for #pragma section and #pragma use_section. Some clean-ups in Cil2Csyntax. Separate mach-dep parts of extraction/extraction.v into /extractionMachdep.v git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1167 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- arm/Asm.v | 93 +++++++----------------------- arm/SelectOp.v | 3 - arm/extractionMachdep.v | 18 ++++++ arm/linux/CPragmas.ml | 20 +++++++ cfrontend/Cil2Csyntax.ml | 97 ++++++++++++++++---------------- cil/src/frontc/clexer.mll | 4 +- driver/Clflags.ml | 1 + driver/Driver.ml | 24 ++++++-- extraction/extraction.v | 13 ++--- powerpc/PrintAsm.ml | 29 ++++++---- powerpc/eabi/CPragmas.ml | 134 ++++++++++++++++++++++++++++++++++++++++++++ powerpc/extractionMachdep.v | 24 ++++++++ powerpc/macosx/CPragmas.ml | 28 +++++++++ 13 files changed, 337 insertions(+), 151 deletions(-) create mode 100644 arm/extractionMachdep.v create mode 100644 arm/linux/CPragmas.ml create mode 100644 powerpc/eabi/CPragmas.ml create mode 100644 powerpc/extractionMachdep.v create mode 100644 powerpc/macosx/CPragmas.ml diff --git a/arm/Asm.v b/arm/Asm.v index 79feee7..a8151a8 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 49676f8..4b5fde7 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 0000000..f6e17ba --- /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 0000000..1602f9f --- /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 16daa14..7025235 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 08f7881..41c8692 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 08e4a53..c6f6e8f 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 30d4a6c..b818680 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 .cil.c -dclight Save generated Clight in .light.c -dasm Save generated assembly in .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 86b9b4c..77c6c62 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 9507498..539d989 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 0000000..9d2eb8a --- /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 0000000..46c40ca --- /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 0000000..f48064c --- /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 -- cgit v1.2.3