diff options
| -rw-r--r-- | arm/PrintAsm.ml | 28 | ||||
| -rw-r--r-- | cfrontend/C2Clight.ml | 27 | ||||
| -rw-r--r-- | common/Sections.ml | 211 | ||||
| -rw-r--r-- | common/Sections.mli | 43 | ||||
| -rw-r--r-- | driver/Driver.ml | 2 | ||||
| -rw-r--r-- | powerpc/PrintAsm.ml | 140 | ||||
| -rw-r--r-- | powerpc/eabi/CPragmas.ml | 154 | ||||
| -rw-r--r-- | powerpc/extractionMachdep.v | 2 | ||||
| -rw-r--r-- | powerpc/macosx/CPragmas.ml | 7 |
9 files changed, 385 insertions, 229 deletions
diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index bb99bb5..f5907f4 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -237,12 +237,13 @@ let print_builtin_function oc s = let lbl1 = new_label() in let lbl2 = new_label() in fprintf oc " cmp %a, #0\n" ireg IR2; - fprintf oc " beq %a\n" label lbl1; - fprintf oc "%a: ldrb %a, [%a], #1\n" label lbl2 ireg IR3 ireg IR1; + fprintf oc " beq .L%d\n" lbl1; + fprintf oc ".L%d: ldrb %a, [%a], #1\n" lbl2 ireg IR3 ireg IR1; fprintf oc " subs %a, %a, #1\n" ireg IR2 ireg IR2; fprintf oc " strb %a, [%a], #1\n" ireg IR3 ireg IR0; - fprintf oc " bne %a\n" label lbl2; - fprintf oc "%a:\n" label lbl1 + fprintf oc " bne .L%d\n" lbl2; + fprintf oc ".L%d:\n" lbl1; + 7 (* let lbl = new_label() in fprintf oc " cmp %a, #0\n" ireg IR2; @@ -255,12 +256,13 @@ let print_builtin_function oc s = let lbl1 = new_label() in let lbl2 = new_label() in fprintf oc " movs %a, %a, lsr #2\n" ireg IR2 ireg IR2; - fprintf oc " beq %a\n" label lbl1; - fprintf oc "%a: ldr %a, [%a], #4\n" label lbl2 ireg IR3 ireg IR1; + fprintf oc " beq .L%d\n" lbl1; + fprintf oc ".L%d: ldr %a, [%a], #4\n" lbl2 ireg IR3 ireg IR1; fprintf oc " subs %a, %a, #1\n" ireg IR2 ireg IR2; fprintf oc " str %a, [%a], #4\n" ireg IR3 ireg IR0; - fprintf oc " bne %a\n" label lbl2; - fprintf oc "%a:\n" label lbl1 + fprintf oc " bne .L%d\n" lbl2; + fprintf oc ".L%d:\n" lbl1; + 7 (* Catch-all *) | s -> invalid_arg ("unrecognized builtin function " ^ s) @@ -496,7 +498,8 @@ let print_function oc name code = currpos := 0; fprintf oc " .text\n"; fprintf oc " .align 2\n"; - fprintf oc " .global %a\n" print_symb name; + if not (C2Clight.atom_is_static name) then + fprintf oc " .global %a\n" print_symb name; fprintf oc " .type %a, %%function\n" print_symb name; fprintf oc "%a:\n" print_symb name; print_instructions oc (labels_of_code Labelset.empty code) code; @@ -584,9 +587,12 @@ let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) = match init_data with | [] -> () | _ -> - fprintf oc " .data\n"; + if C2Clight.atom_is_readonly name + then fprintf oc " .const\n" + else fprintf oc " .data\n"; fprintf oc " .align 2\n"; - fprintf oc " .global %a\n" print_symb name; + if not (C2Clight.atom_is_static name) then + fprintf oc " .global %a\n" print_symb name; fprintf oc " .type %a, %%object\n" print_symb name; fprintf oc "%a:\n" print_symb name; print_init_data oc name init_data diff --git a/cfrontend/C2Clight.ml b/cfrontend/C2Clight.ml index 46242e0..5bdd727 100644 --- a/cfrontend/C2Clight.ml +++ b/cfrontend/C2Clight.ml @@ -16,9 +16,6 @@ let decl_atom : (AST.ident, Env.t * C.decl) Hashtbl.t = Hashtbl.create 103 (** Hooks -- overriden in machine-dependent CPragmas module *) let process_pragma_hook = ref (fun (s: string) -> false) -let define_variable_hook = ref (fun (id: ident) (d: C.decl) -> ()) -let define_function_hook = ref (fun (id: ident) (d: C.decl) -> ()) -let define_stringlit_hook = ref (fun (id: ident) -> ()) (** ** Error handling *) @@ -57,7 +54,7 @@ let name_for_string_literal env s = Env.fresh_ident name, C.TPtr(C.TInt(C.IChar,[C.AConst]),[]), None)); - !define_stringlit_hook id; + Sections.define_stringlit id; Hashtbl.add stringTable s id; id @@ -529,7 +526,7 @@ let convertFundef env fd = let decl = (fd.fd_storage, fd.fd_name, Cutil.fundef_typ fd, None) in Hashtbl.add decl_atom id' (env, decl); - !define_function_hook id' decl; + Sections.define_function id'; Datatypes.Coq_pair(id', Internal {fn_return = ret; fn_params = params; fn_vars = vars; fn_body = body'}) @@ -649,6 +646,14 @@ let convertInit env ty init = (** Global variable *) +let rec 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(t', _, _) -> type_is_readonly env t' + | _ -> false + let convertGlobvar env (sto, id, ty, optinit as decl) = let id' = intern_string id.name in let ty' = convertTyp env ty in @@ -659,7 +664,9 @@ let convertGlobvar env (sto, id, ty, optinit as decl) = | Some i -> convertInit env ty i in Hashtbl.add decl_atom id' (env, decl); - !define_variable_hook id' decl; + Sections.define_variable id' + (match Cutil.sizeof env ty with Some sz -> sz | None -> max_int) + (type_is_readonly env ty); Datatypes.Coq_pair(Datatypes.Coq_pair(id', init'), ty') (** Convert a list of global declarations. @@ -769,14 +776,6 @@ let convertProgram p = (** ** Extracting information about global variables from their atom *) -let rec 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(t', _, _) -> type_is_readonly env t' - | _ -> false - let atom_is_static a = try let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in diff --git a/common/Sections.ml b/common/Sections.ml new file mode 100644 index 0000000..9124f85 --- /dev/null +++ b/common/Sections.ml @@ -0,0 +1,211 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +open Camlcoq + +module StringMap = Map.Make(String) + +(* Handling of linker sections *) + +type section_name = + | Section_text + | Section_data of bool (* true = init data, false = uninit data *) + | Section_small_data of bool + | Section_const + | Section_small_const + | Section_string + | Section_literal + | Section_jumptable + | Section_user of string * bool (*writable*) * bool (*executable*) + +type section_info = { + sec_name_init: section_name; + sec_name_uninit: section_name; + sec_writable: bool; + sec_executable: bool; + sec_near_access: bool +} + +let default_section_info = { + sec_name_init = Section_data true; + sec_name_uninit = Section_data false; + sec_writable = true; + sec_executable = false; + sec_near_access = false +} + +(* Built-in sections *) + +let builtin_sections = [ + "CODE", + {sec_name_init = Section_text; + sec_name_uninit = Section_text; + sec_writable = false; sec_executable = true; + sec_near_access = false}; + "DATA", + {sec_name_init = Section_data true; + sec_name_uninit = Section_data false; + sec_writable = true; sec_executable = false; + sec_near_access = false}; + "SDATA", + {sec_name_init = Section_small_data true; + sec_name_uninit = Section_small_data false; + sec_writable = true; sec_executable = false; + sec_near_access = true}; + "CONST", + {sec_name_init = Section_const; + sec_name_uninit = Section_const; + sec_writable = false; sec_executable = false; + sec_near_access = false}; + "SCONST", + {sec_name_init = Section_small_const; + sec_name_uninit = Section_small_const; + sec_writable = false; sec_executable = false; + sec_near_access = true}; + "STRING", + {sec_name_init = Section_string; + sec_name_uninit = Section_string; + sec_writable = false; sec_executable = false; + sec_near_access = false}; + "LITERAL", + {sec_name_init = Section_literal; + sec_name_uninit = Section_literal; + sec_writable = false; sec_executable = false; + sec_near_access = false}; + "JUMPTABLE", + {sec_name_init = Section_jumptable; + sec_name_uninit = Section_jumptable; + sec_writable = false; sec_executable = false; + sec_near_access = false} +] + +let default_section_table = + List.fold_right + (fun (s, i) t -> StringMap.add s i t) + builtin_sections StringMap.empty + + +(* The current mapping from section names to section info *) + +let current_section_table : (section_info StringMap.t) ref = + ref StringMap.empty + +(* The section to use for each global symbol: either explicitly + assigned using a "use_section" pragma, or inferred at definition + time. *) + +let use_section_table : (AST.ident, section_info) Hashtbl.t = + Hashtbl.create 51 + +(* For each global symbol, the mapping sect name -> sect info + current at the time it was defined *) + +let section_table_at_def : (AST.ident, section_info StringMap.t) Hashtbl.t = + Hashtbl.create 51 + +let initialize () = + current_section_table := default_section_table; + Hashtbl.clear use_section_table; + Hashtbl.clear section_table_at_def + +(* Define or update a given section. *) + +let define_section name ?iname ?uname ?writable ?executable ?near () = + let si = + try StringMap.find name !current_section_table + with Not_found -> default_section_info in + let writable = + match writable with Some b -> b | None -> si.sec_writable + and executable = + match executable with Some b -> b | None -> si.sec_executable + and near = + match near with Some b -> b | None -> si.sec_near_access in + let iname = + match iname with Some s -> Section_user(s, writable, executable) + | None -> si.sec_name_init in + let uname = + match uname with Some s -> Section_user(s, writable, executable) + | None -> si.sec_name_uninit in + let new_si = + { sec_name_init = iname; + sec_name_uninit = uname; + sec_writable = writable; + sec_executable = executable; + sec_near_access = near } in + current_section_table := StringMap.add name new_si !current_section_table + +(* Explicitly associate a section to a global symbol *) + +let use_section_for id name = + try + let si = StringMap.find name !current_section_table in + Hashtbl.add use_section_table id si; + true + with Not_found -> + false + +(* Default association of a section to a global symbol *) + +let default_use_section id name = + Hashtbl.add section_table_at_def id !current_section_table; + if not (Hashtbl.mem use_section_table id) then begin + let ok = use_section_for id name in + assert ok + end + +let define_function id = + default_use_section id "CODE" + +let define_stringlit id = + default_use_section id "STRING" + +let define_variable id size readonly = + default_use_section id + (if readonly + then if size <= !Clflags.option_small_const then "SCONST" else "CONST" + else if size <= !Clflags.option_small_data then "SDATA" else "DATA") + +(* Determine section to use for a variable definition *) + +let section_for_variable a initialized = + try + let si = Hashtbl.find use_section_table a in + if initialized then si.sec_name_init else si.sec_name_uninit + with Not_found -> + Section_data initialized + +(* Determine (text, literal, jumptable) sections to use + for a function definition *) + +let sections_for_function a = + let s_text = + try (Hashtbl.find use_section_table a).sec_name_init + with Not_found -> Section_text in + let s_table = + try Hashtbl.find section_table_at_def a + with Not_found -> default_section_table in + let s_literal = + try (StringMap.find "LITERAL" s_table).sec_name_init + with Not_found -> Section_literal in + let s_jumptable = + try (StringMap.find "JUMPTABLE" s_table).sec_name_init + with Not_found -> Section_jumptable in + (s_text, s_literal, s_jumptable) + +(* Say if an atom is in a small data area *) + +let atom_is_small_data a ofs = + try (Hashtbl.find use_section_table a).sec_near_access + with Not_found -> false diff --git a/common/Sections.mli b/common/Sections.mli new file mode 100644 index 0000000..090d4bb --- /dev/null +++ b/common/Sections.mli @@ -0,0 +1,43 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + + +(* Handling of linker sections *) + +type section_name = + | Section_text + | Section_data of bool (* true = init data, false = uninit data *) + | Section_small_data of bool + | Section_const + | Section_small_const + | Section_string + | Section_literal + | Section_jumptable + | Section_user of string * bool (*writable*) * bool (*executable*) + +val initialize: unit -> unit + +val define_section: + string -> ?iname:string -> ?uname:string + -> ?writable:bool -> ?executable:bool -> ?near:bool -> unit -> unit +val use_section_for: AST.ident -> string -> bool + +val define_function: AST.ident -> unit +val define_variable: AST.ident -> int -> bool -> unit +val define_stringlit: AST.ident -> unit + +val section_for_variable: AST.ident -> bool -> section_name +val sections_for_function: AST.ident -> section_name * section_name * section_name +val atom_is_small_data: AST.ident -> Integers.Int.int -> bool diff --git a/driver/Driver.ml b/driver/Driver.ml index 255b600..2776604 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -61,6 +61,7 @@ let preprocess ifile ofile = (* From preprocessed C to asm *) let compile_c_file sourcename ifile ofile = + Sections.initialize(); (* Simplification options *) let simplifs = "becv" (* blocks, impure exprs, implicit casts, volatiles: mandatory *) @@ -108,6 +109,7 @@ let compile_c_file sourcename ifile ofile = (* From Cminor to asm *) let compile_cminor_file ifile ofile = + Sections.initialize(); let ic = open_in ifile in let lb = Lexing.from_channel ic in try diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 8dab7ae..1fdb1a9 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -15,6 +15,7 @@ open Printf open Datatypes open Camlcoq +open Sections open AST open Asm @@ -177,28 +178,58 @@ let creg oc r = | MacOS|Diab -> fprintf oc "cr%d" r | Linux -> fprintf oc "%d" r -let section oc name = - fprintf oc " %s\n" name - (* Names of sections *) -let (text, data, const_data, float_literal) = +let name_of_section_MacOS = function + | Section_text -> ".text" + | Section_data _ -> ".data" + | Section_small_data _ -> ".data" + | Section_const -> ".const" + | Section_small_const -> ".const" + | Section_string -> ".const" + | Section_literal -> ".const_data" + | Section_jumptable -> ".text" + | Section_user _ -> assert false + +let name_of_section_Linux = function + | Section_text -> ".text" + | Section_data i -> if i then ".data" else ".bss" + | Section_small_data i -> if i then ".sdata" else ".sbss" + | Section_const -> ".rodata" + | Section_small_const -> ".sdata2" + | Section_string -> ".rodata" + | Section_literal -> ".section .rodata.cst8,\"aM\",@progbits,8" + | Section_jumptable -> ".text" + | Section_user(s, wr, ex) -> + sprintf ".section %s,\"a%s%s\",@progbits" + s (if wr then "w" else "") (if ex then "x" else "") + +let name_of_section_Diab = function + | Section_text -> ".text" + | Section_data i -> if i then ".data" else ".bss" + | Section_small_data i -> if i then ".sdata" else ".sbss" + | Section_const -> ".text" + | Section_small_const -> ".sdata2" + | Section_string -> ".text" + | Section_literal -> ".text" + | Section_jumptable -> ".text" + | Section_user(s, wr, ex) -> + sprintf ".section %s,,%c" + s + (match wr, ex with + | true, true -> 'm' (* text+data *) + | true, false -> 'd' (* data *) + | false, true -> 'c' (* text *) + | false, false -> 'r') (* const *) + +let name_of_section = match target with - | MacOS -> - (".text", - ".data", - ".const", - ".const_data") - | Linux -> - (".text", - ".data", - ".rodata", - ".section .rodata.cst8,\"aM\",@progbits,8") - | Diab -> - (".text", - ".data", - ".text", - ".text") + | MacOS -> name_of_section_MacOS + | Linux -> name_of_section_Linux + | Diab -> name_of_section_Diab + +let section oc sec = + fprintf oc " %s\n" (name_of_section sec) (* Encoding masks for rlwinm instructions *) @@ -353,6 +384,9 @@ let print_builtin_function oc s = module Labelset = Set.Make(struct type t = label let compare = compare end) +let float_literals : (int * int64) list ref = ref [] +let jumptables : (int * label list) list ref = ref [] + let print_instruction oc labels = function | Padd(r1, r2, r3) -> fprintf oc " add %a, %a, %a\n" ireg r1 ireg r2 ireg r3 @@ -410,10 +444,7 @@ let print_instruction oc labels = function fprintf oc " lwz %a, %a(%a)\n" ireg GPR12 label_low lbl ireg GPR12; fprintf oc " mtctr %a\n" ireg GPR12; fprintf oc " bctr\n"; - fprintf oc "%a:" label lbl; - List.iter - (fun l -> fprintf oc " .long %a\n" label (transl_label l)) - tbl; + jumptables := (lbl, tbl) :: !jumptables; fprintf oc "%s end pseudoinstr btbl\n" comment | Pcmplw(r1, r2) -> fprintf oc " cmplw %a, %a, %a\n" creg 0 ireg r1 ireg r2 @@ -471,9 +502,7 @@ let print_instruction oc labels = function fprintf oc " lwz %a, 4(%a)\n" ireg r1 ireg GPR1; fprintf oc " addis %a, %a, 0x8000\n" ireg r1 ireg r1; fprintf oc "%a: addi %a, %a, 8\n" label lbl3 ireg GPR1 ireg GPR1; - section oc float_literal; - fprintf oc "%a: .long 0x41e00000, 0x00000000\n" label lbl1; - section oc text; + float_literals := (lbl1, 0x41e00000_00000000L) :: !float_literals; fprintf oc "%s end pseudoinstr fctiu\n" comment | Pfdiv(r1, r2, r3) -> fprintf oc " fdiv %a, %a, %a\n" freg r1 freg r2 freg r3 @@ -503,9 +532,7 @@ let print_instruction oc labels = function fprintf oc " lfd %a, 0(%a)\n" freg r1 ireg GPR1; fprintf oc " addi %a, %a, 8\n" ireg GPR1 ireg GPR1; fprintf oc " fsub %a, %a, %a\n" freg r1 freg r1 freg FPR13; - section oc float_literal; - fprintf oc "%a: .long 0x43300000, 0x80000000\n" label lbl; - section oc text; + float_literals := (lbl, 0x43300000_80000000L) :: !float_literals; fprintf oc "%s end pseudoinstr ictf\n" comment | Piuctf(r1, r2) -> let lbl = new_label() in @@ -518,9 +545,7 @@ let print_instruction oc labels = function fprintf oc " lfd %a, 0(%a)\n" freg r1 ireg GPR1; fprintf oc " addi %a, %a, 8\n" ireg GPR1 ireg GPR1; fprintf oc " fsub %a, %a, %a\n" freg r1 freg r1 freg FPR13; - section oc float_literal; - fprintf oc "%a: .long 0x43300000, 0x00000000\n" label lbl; - section oc text; + float_literals := (lbl, 0x43300000_00000000L) :: !float_literals; fprintf oc "%s end pseudoinstr ictf\n" comment | Plbz(r1, c, r2) -> fprintf oc " lbz %a, %a(%a)\n" ireg r1 constant c ireg r2 @@ -533,14 +558,8 @@ let print_instruction oc labels = function | Plfi(r1, c) -> let lbl = new_label() in fprintf oc " addis %a, 0, %a\n" ireg GPR12 label_high lbl; - fprintf oc " lfd %a, %a(%a)\n" freg r1 label_low lbl ireg GPR12; - section oc float_literal; - let n = Int64.bits_of_float c in - let nlo = Int64.to_int32 n - and nhi = Int64.to_int32(Int64.shift_right_logical n 32) in - fprintf oc "%a: .long 0x%lx, 0x%lx %s %.18g\n" - label lbl nhi nlo comment c; - section oc text + fprintf oc " lfd %a, %a(%a) %s %.18g\n" freg r1 label_low lbl ireg GPR12 comment c; + float_literals := (lbl, Int64.bits_of_float c) :: !float_literals; | Plfs(r1, c, r2) -> fprintf oc " lfs %a, %a(%a)\n" freg r1 constant c ireg r2 | Plfsx(r1, r2, r3) -> @@ -633,6 +652,17 @@ let print_instruction oc labels = function if Labelset.mem lbl labels then fprintf oc "%a:\n" label (transl_label lbl) +let print_literal oc (lbl, n) = + let nlo = Int64.to_int32 n + and nhi = Int64.to_int32(Int64.shift_right_logical n 32) in + fprintf oc "%a: .long 0x%lx, 0x%lx\n" label lbl nhi nlo + +let print_jumptable oc (lbl, tbl) = + fprintf oc "%a:" label lbl; + List.iter + (fun l -> fprintf oc " .long %a\n" label (transl_label l)) + tbl + let rec labels_of_code accu = function | [] -> accu @@ -645,10 +675,10 @@ let rec labels_of_code accu = function let print_function oc name code = Hashtbl.clear current_function_labels; - section oc - (match CPragmas.section_for_atom name true with - | Some s -> s - | None -> text); + float_literals := []; + jumptables := []; + let (text, lit, jmptbl) = sections_for_function name in + section oc text; fprintf oc " .align 2\n"; if not (C2Clight.atom_is_static name) then fprintf oc " .globl %a\n" symbol name; @@ -657,6 +687,16 @@ let print_function oc name code = if target <> MacOS then begin fprintf oc " .type %a, @function\n" symbol name; fprintf oc " .size %a, . - %a\n" symbol name symbol name + end; + if !float_literals <> [] then begin + section oc lit; + List.iter (print_literal oc) !float_literals; + float_literals := [] + end; + if !jumptables <> [] then begin + section oc jmptbl; + List.iter (print_jumptable oc) !jumptables; + jumptables := [] end (* Generation of stub functions *) @@ -761,7 +801,7 @@ let non_variadic_stub oc name = let stub_function oc name ef = let name = extern_atom name in - fprintf oc " .text\n"; + section oc Section_text; fprintf oc " .align 2\n"; fprintf oc "L%s$stub:\n" name; if Str.string_match re_variadic_stub name 0 @@ -777,7 +817,7 @@ end module Stubs_EABI = struct let variadic_stub oc stub_name fun_name args = - fprintf oc " .text\n"; + section oc Section_text; fprintf oc " .align 2\n"; fprintf oc ".L%s$stub:\n" stub_name; (* bit 6 must be set if at least one argument is a float; clear otherwise *) @@ -829,7 +869,6 @@ let print_init oc = function | Init_float32 n -> fprintf oc " .long %ld %s %.18g\n" (Int32.bits_of_float n) comment n | Init_float64 n -> - (* .quad not working on all versions of the MacOSX assembler *) let b = Int64.bits_of_float n in fprintf oc " .long %Ld, %Ld %s %.18g\n" (Int64.shift_right_logical b 32) @@ -857,12 +896,7 @@ let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) = let init = match init_data with [Init_space _] -> false | _ -> true in let sec = - match CPragmas.section_for_atom name init with - | Some s -> s - | None -> - if C2Clight.atom_is_readonly name - then const_data - else data + Sections.section_for_variable name init and align = match C2Clight.atom_alignof name with | Some a -> log2 a diff --git a/powerpc/eabi/CPragmas.ml b/powerpc/eabi/CPragmas.ml index 3104cc8..7dbc215 100644 --- a/powerpc/eabi/CPragmas.ml +++ b/powerpc/eabi/CPragmas.ml @@ -19,111 +19,23 @@ open Printf open Camlcoq open Cparser -type section_info = { - sec_name_init: string; - sec_name_uninit: string; - sec_acc_mode: string; - sec_near_access: bool -} - -let default_section_info = { - sec_name_init = ".data"; - sec_name_uninit = ".data"; (* COMM? *) - sec_acc_mode = "RW"; - sec_near_access = false -} - -let section_table : (string, section_info) Hashtbl.t = - Hashtbl.create 17 - -(* Built-in sections *) - -let _ = - let rodata = - if Configuration.system = "linux" then ".rodata" else ".text" in - List.iter (fun (n, si) -> Hashtbl.add section_table n si) [ - "CODE", {sec_name_init = ".text"; - sec_name_uninit = ".text"; - sec_acc_mode = "RX"; - sec_near_access = false}; - "DATA", {sec_name_init = ".data"; - sec_name_uninit = ".data"; (* COMM? *) - sec_acc_mode = "RW"; - sec_near_access = false}; - "SDATA", {sec_name_init = ".sdata"; - sec_name_uninit = ".sbss"; - sec_acc_mode = "RW"; - sec_near_access = true}; - "CONST", {sec_name_init = rodata; - sec_name_uninit = rodata; - sec_acc_mode = "R"; - sec_near_access = false}; - "SCONST",{sec_name_init = ".sdata2"; - sec_name_uninit = ".sdata2"; - sec_acc_mode = "R"; - sec_near_access = true}; - "STRING",{sec_name_init = rodata; - sec_name_uninit = rodata; - sec_acc_mode = "R"; - sec_near_access = false} - ] - (* #pragma section *) let process_section_pragma classname istring ustring addrmode accmode = - let old_si = - try Hashtbl.find section_table classname - with Not_found -> default_section_info in - let si = - { sec_name_init = - if istring = "" then old_si.sec_name_init else istring; - sec_name_uninit = - if ustring = "" then old_si.sec_name_uninit else ustring; - sec_acc_mode = - if accmode = "" then old_si.sec_acc_mode else accmode; - sec_near_access = - if addrmode = "" - then old_si.sec_near_access - else (addrmode = "near-code") || (addrmode = "near-data") } in - Hashtbl.add section_table classname si + Sections.define_section classname + ?iname: (if istring = "" then None else Some istring) + ?uname: (if ustring = "" then None else Some ustring) + ?writable: (if accmode = "" then None else Some(String.contains accmode 'W')) + ?executable: (if accmode = "" then None else Some(String.contains accmode 'X')) + ?near: (if addrmode = "" then None + else Some(addrmode = "near-code" || addrmode = "near-data")) + () (* #pragma use_section *) -let use_section_table : (AST.ident, section_info) Hashtbl.t = - Hashtbl.create 51 - 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 -> - C2Clight.error (sprintf "unknown section name `%s'" classname) - -let default_use_section id classname = - if not (Hashtbl.mem use_section_table id) then begin - let info = - try Hashtbl.find section_table classname - with Not_found -> assert false in - Hashtbl.add use_section_table id info - end - -let define_function id d = - default_use_section id "CODE" - -let define_stringlit id = - default_use_section id "STRING" - -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 C2Clight.atom_is_readonly id then - if is_small !Clflags.option_small_const then "SCONST" else "CONST" - else - if is_small !Clflags.option_small_data then "SDATA" else "DATA" in - default_use_section id sect + if not (Sections.use_section_for (intern_string id) classname) + then C2Clight.error (sprintf "unknown section name `%s'" classname) (* #pragma reserve_register *) @@ -193,48 +105,4 @@ let process_pragma name = false let initialize () = - 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 = - 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 *) - -let section_for_atom a init = - try - let sinfo = Hashtbl.find use_section_table a in - let sname = - if init then sinfo.sec_name_init else sinfo.sec_name_uninit in - if not (String.contains sname '\"') then - Some sname - else begin - (* The following is Diab-specific... *) - let accmode = sinfo.sec_acc_mode in - let is_writable = String.contains accmode 'W' - and is_executable = String.contains accmode 'X' in - let stype = - match is_writable, is_executable with - | true, true -> 'm' (* text+data *) - | true, false -> 'd' (* data *) - | false, true -> 'c' (* text *) - | false, false -> 'r' (* const *) - in Some(sprintf ".section\t%s,,%c" sname stype) - end - with Not_found -> None + C2Clight.process_pragma_hook := process_pragma diff --git a/powerpc/extractionMachdep.v b/powerpc/extractionMachdep.v index 83fda76..a315e8f 100644 --- a/powerpc/extractionMachdep.v +++ b/powerpc/extractionMachdep.v @@ -18,7 +18,7 @@ Extract Constant SelectOp.use_fused_mul => "(fun () -> !Clflags.option_fmadd)". (* 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.symbol_is_small_data => "Sections.atom_is_small_data". Extract Constant Asm.small_data_area_offset => "fun _ _ _ -> assert false". (* Suppression of stupidly big equality functions *) diff --git a/powerpc/macosx/CPragmas.ml b/powerpc/macosx/CPragmas.ml index f48064c..ede2f38 100644 --- a/powerpc/macosx/CPragmas.ml +++ b/powerpc/macosx/CPragmas.ml @@ -19,10 +19,3 @@ 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 |