From 913c1bcc4b2204afd447edd723e06b905fd1f47f Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 8 May 2010 14:32:58 +0000 Subject: Cleaned up handling of linker sections. Minor updates on ARM code generator. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1339 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Sections.ml | 211 ++++++++++++++++++++++++++++++++++++++++++++++++++++ common/Sections.mli | 43 +++++++++++ 2 files changed, 254 insertions(+) create mode 100644 common/Sections.ml create mode 100644 common/Sections.mli (limited to 'common') 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 -- cgit v1.2.3