diff options
Diffstat (limited to 'powerpc')
-rw-r--r-- | powerpc/PrintAsm.ml | 22 | ||||
-rw-r--r-- | powerpc/eabi/CPragmas.ml | 168 |
2 files changed, 133 insertions, 57 deletions
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index d9c65314..50a84744 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -175,26 +175,23 @@ let section oc name = (* Names of sections *) -let (text, data, const_data, sdata, float_literal) = +let (text, data, const_data, float_literal) = match target with | MacOS -> (".text", ".data", ".const", - ".data", (* unused *) ".const_data") | Linux -> (".text", ".data", ".rodata", - ".data", (* unused *) ".section .rodata.cst8,\"aM\",@progbits,8") | Diab -> (".text", ".data", - ".data", (* or: .rodata? *) - ".sdata", (* to check *) - ".data") (* or: .rodata? *) + ".text", + ".text") (* Encoding masks for rlwinm instructions *) @@ -496,7 +493,7 @@ let print_function oc name code = Hashtbl.clear current_function_labels; section oc (match CPragmas.section_for_atom name true with - | Some s -> ".section\t" ^ s + | Some s -> s | None -> text); fprintf oc " .align 2\n"; if not (Cil2Csyntax.atom_is_static name) then @@ -713,14 +710,11 @@ let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) = match init_data with [Init_space _] -> false | _ -> true in let sec = match CPragmas.section_for_atom name init with - | Some s -> ".section\t" ^ s + | Some s -> 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 + if Cil2Csyntax.atom_is_readonly name + then const_data + else data in section oc sec; fprintf oc " .align 3\n"; diff --git a/powerpc/eabi/CPragmas.ml b/powerpc/eabi/CPragmas.ml index 9d2eb8a4..d4b79b52 100644 --- a/powerpc/eabi/CPragmas.ml +++ b/powerpc/eabi/CPragmas.ml @@ -22,31 +22,72 @@ open Camlcoq 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 -let use_section_table : (AST.ident, section_info) Hashtbl.t = - Hashtbl.create 51 +(* 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} + ] 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 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 + + +let use_section_table : (AST.ident, section_info) Hashtbl.t = + Hashtbl.create 51 let process_use_section_pragma classname id = try @@ -55,18 +96,42 @@ let process_use_section_pragma classname id = with Not_found -> Cil2Csyntax.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 v = + default_use_section id "CODE" + +let define_stringlit id v = + default_use_section id "STRING" + +let define_variable id v = + let sz = Cil.bitsSizeOf v.vtype / 8 in + let sect = + if Cil2Csyntax.var_is_readonly v then + if sz <= !Clflags.option_small_const then "SCONST" else "CONST" + else + if sz <= !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 *) 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_pragma_section = Str.regexp( + "section[ \t]+" +^ "\\([A-Za-z_][A-Za-z_0-9]*\\)[ \t]+" (* class_name *) +^ "\\(\"[^\"]*\"\\)?[ \t]*" (* istring *) +^ "\\(\"[^\"]*\"\\)?[ \t]*" (* ustring *) +^ "\\(standard\\|near-absolute\\|far-absolute\\|near-data\\|far-data\\|near-code\\|far-code\\)?[ \t]*" (* addressing mode *) +^ "\\([RWXON]*\\)" (* access mode *) +) let re_start_pragma_use_section = Str.regexp "use_section\\b" @@ -101,34 +166,51 @@ let process_pragma (Attr(name, _)) = false let initialize () = - Cil2Csyntax.process_pragma := process_pragma + Cil2Csyntax.process_pragma_hook := process_pragma; + Cil2Csyntax.define_variable_hook := define_variable; + Cil2Csyntax.define_function_hook := define_function; + Cil2Csyntax.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 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 + 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 -> - false - end - | _ -> + 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 (* 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 - + 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 |