Revised handling of #pragma section and small data areas

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

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