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

2 files changed, 254 insertions, 0 deletions

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