PowerPC/EABI port: preliminary support for #pragma section and

  #pragma use_section.
Some clean-ups in Cil2Csyntax.
Separate mach-dep parts of extraction/extraction.v into
   <arch>/extractionMachdep.v


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1167 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

4 files changed, 205 insertions, 10 deletions

diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 9507498..539d989 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -192,9 +192,9 @@ let (text, data, const_data, sdata, float_literal) =
   | Diab ->
       (".text",
        ".data",
-       ".data",  (* to check *)
-       ".sdata", (* to check *)
-       ".data")  (* to check *)
+       ".data", (* or: .rodata? *)
+       ".sdata",  (* to check *)
+       ".data")  (* or: .rodata? *)
 
 (* Encoding masks for rlwinm instructions *)
 
@@ -480,7 +480,10 @@ let rec labels_of_code = function
 
 let print_function oc name code =
   Hashtbl.clear current_function_labels;
-  section oc text;
+  section oc
+    (match CPragmas.section_for_atom name true with
+     | Some s -> ".section\t" ^ s
+     | None -> text);
   fprintf oc "	.align 2\n";
   if not (Cil2Csyntax.atom_is_static name) then
     fprintf oc "	.globl %a\n" symbol name;
@@ -692,13 +695,19 @@ let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) =
   match init_data with
   | [] -> ()
   | _  ->
+      let init =
+        match init_data with [Init_space _] -> false | _ -> true in
       let sec =
-        if Cil2Csyntax.atom_is_small_data name (coqint_of_camlint 0l) then
-          sdata
-        else if Cil2Csyntax.atom_is_readonly name then
-          const_data
-        else
-          data in
+        match CPragmas.section_for_atom name init with
+        | Some s -> ".section\t" ^ 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
+      in
       section oc sec;
       fprintf oc "	.align	3\n";
       if not (Cil2Csyntax.atom_is_static name) then
diff --git a/powerpc/eabi/CPragmas.ml b/powerpc/eabi/CPragmas.ml
new file mode 100644
index 0000000..9d2eb8a
--- /dev/null
+++ b/powerpc/eabi/CPragmas.ml
@@ -0,0 +1,134 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* Platform-dependent handling of pragmas *)
+
+open Printf
+open Cil
+open Camlcoq
+
+type section_info = {
+  sec_name_init: string;
+  sec_name_uninit: string;
+  sec_near_access: bool
+}
+
+let section_table : (string, section_info) Hashtbl.t =
+  Hashtbl.create 17
+
+let use_section_table : (AST.ident, section_info) Hashtbl.t =
+  Hashtbl.create 51
+
+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 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 ->
+    Cil2Csyntax.error (sprintf "unknown section name `%s'" classname)
+
+(* 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_start_pragma_use_section = Str.regexp "use_section\\b"
+
+let re_pragma_use_section = Str.regexp
+  "use_section[ \t]+\
+   \\([A-Za-z_][A-Za-z_0-9]*\\)[ \t]+\
+   \\(.*\\)$"
+
+let re_split_idents = Str.regexp "[ \t,]+"
+
+let process_pragma (Attr(name, _)) =
+  if Str.string_match re_pragma_section name 0 then begin
+    process_section_pragma
+      (Str.matched_group 1 name) (* classname *)
+      (Str.matched_group 2 name) (* istring *)
+      (Str.matched_group 3 name) (* ustring *)
+      (Str.matched_group 4 name) (* addrmode *)
+      (Str.matched_group 5 name); (* accmode *)
+    true
+  end else if Str.string_match re_start_pragma_section name 0 then
+    Cil2Csyntax.error "ill-formed `section' pragma"
+ else if Str.string_match re_pragma_use_section name 0 then begin
+    let classname = Str.matched_group 1 name
+    and idents = Str.matched_group 2 name in
+    let identlist = Str.split re_split_idents idents in
+    if identlist = [] then Cil2Csyntax.warning "vacuous `use_section' pragma";
+    List.iter (process_use_section_pragma classname) identlist;
+    true
+  end else if Str.string_match re_start_pragma_use_section name 0 then
+    Cil2Csyntax.error "ill-formed `use_section' pragma"
+  else
+    false
+
+let initialize () =
+  Cil2Csyntax.process_pragma := process_pragma
+
+(* 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
+      with Not_found ->
+        false
+      end
+  | _ ->
+      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
+    Some(if init then sinfo.sec_name_init else sinfo.sec_name_uninit)
+  with Not_found ->
+    None
+  
diff --git a/powerpc/extractionMachdep.v b/powerpc/extractionMachdep.v
new file mode 100644
index 0000000..46c40ca
--- /dev/null
+++ b/powerpc/extractionMachdep.v
@@ -0,0 +1,24 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* Additional extraction directives specific to the PowerPC port *)
+
+(* 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.small_data_area_offset => "fun _ _ _ -> assert false".
+
+(* Suppression of stupidly big equality functions *)
+Extract Constant Asm.ireg_eq => "fun (x: ireg) (y: ireg) -> x = y".
+Extract Constant Asm.freg_eq => "fun (x: freg) (y: freg) -> x = y".
+Extract Constant Asm.preg_eq => "fun (x: preg) (y: preg) -> x = y".
diff --git a/powerpc/macosx/CPragmas.ml b/powerpc/macosx/CPragmas.ml
new file mode 100644
index 0000000..f48064c
--- /dev/null
+++ b/powerpc/macosx/CPragmas.ml
@@ -0,0 +1,28 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* Platform-dependent handling of pragmas *)
+
+(* No pragmas supported on PowerPC/MacOS *)
+
+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