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

4 files changed, 99 insertions, 204 deletions

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