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

5 files changed, 239 insertions, 153 deletions

diff --git a/cfrontend/Cil2Csyntax.ml b/cfrontend/Cil2Csyntax.ml
index e5690aac..822f6cb0 100644
--- a/cfrontend/Cil2Csyntax.ml
+++ b/cfrontend/Cil2Csyntax.ml
@@ -201,11 +201,12 @@ and eval_cast ty v =
   | TPtr(_, _), CWStr s -> v  (* tolerance? *)
   | _, _ -> raise NotConst
 
-(** Handler for #pragma directives -- 
-    overriden in machine-dependent CPragmas module *)
-
-let process_pragma = ref (fun (a: Cil.attribute) -> false)
+(** Hooks -- overriden in machine-dependent CPragmas module *)
 
+let process_pragma_hook = ref (fun (a: Cil.attribute) -> false)
+let define_variable_hook = ref (fun (id: ident) (v: Cil.varinfo) -> ())
+let define_function_hook = ref (fun (id: ident) (v: Cil.varinfo) -> ())
+let define_stringlit_hook = ref (fun (id: ident) (v: Cil.varinfo) -> ())
 
 (** The parameter to the translation functor: it specifies the
     translation for integer and float types. *)
@@ -296,6 +297,7 @@ let name_for_string_literal s =
     v.vstorage <- Static;
     v.vreferenced <- true;
     Hashtbl.add varinfo_atom id v;
+    !define_stringlit_hook id v;
     Hashtbl.add stringTable s id;
     id
 
@@ -1012,6 +1014,7 @@ let convertGFun fdec =
   current_function := None;
   let id = intern_string v.vname in
   Hashtbl.add varinfo_atom id v;
+  !define_function_hook id v;
   Datatypes.Coq_pair
     (id,
      Internal { fn_return=ret; fn_params=args; fn_vars=varList; fn_body=s })
@@ -1144,6 +1147,7 @@ let convertGVar v i =
   updateLoc(v.vdecl);
   let id = intern_string v.vname in
   Hashtbl.add varinfo_atom id v;
+  !define_variable_hook id v;
   Datatypes.Coq_pair (Datatypes.Coq_pair(id, convertInitInfo v.vtype i),
                       convertTyp v.vtype)
 
@@ -1214,7 +1218,7 @@ let rec processGlobals = function
               unsupported "inline assembly"
 	  | GPragma (Attr(name, _) as attr, loc) ->
 	      updateLoc(loc);
-              if not (!process_pragma attr) then
+              if not (!process_pragma_hook attr) then
                 warning ("#pragma `" ^ name ^ "' directive ignored");
               processGlobals l
 	  | GText _ -> processGlobals l (* comments are ignored *)
@@ -1264,16 +1268,16 @@ let atom_is_static a =
   with Not_found ->
     false
 
+let var_is_readonly v =
+  let a = typeAttrs v.vtype in
+  if hasAttribute "volatile" a then false else
+  if hasAttribute "const" a then true else
+  match Cil.unrollType v.vtype with
+  | TArray(ty, _, _) ->
+      let a' = typeAttrs ty in
+      hasAttribute "const" a' && not (hasAttribute "volatile" a')
+  | _ -> false
+
 let atom_is_readonly a =
-  try
-    let v = Hashtbl.find varinfo_atom a in
-    let a = typeAttrs v.vtype in
-    if hasAttribute "volatile" a then false else
-    if hasAttribute "const" a then true else
-    match Cil.unrollType v.vtype with
-    | TArray(ty, _, _) ->
-        let a' = typeAttrs ty in
-        hasAttribute "const" a' && not (hasAttribute "volatile" a')
-    | _ -> false
-  with Not_found ->
-    false
+  try var_is_readonly (Hashtbl.find varinfo_atom a)
+  with Not_found -> false
diff --git a/driver/Clflags.ml b/driver/Clflags.ml
index c6f6e8fe..ddcfaac4 100644
--- a/driver/Clflags.ml
+++ b/driver/Clflags.ml
@@ -24,3 +24,9 @@ let option_E = ref false
 let option_S = ref false
 let option_c = ref false
 let option_v = ref false
+let option_small_data = 
+  ref (if Configuration.arch = "powerpc"
+       && Configuration.variant = "eabi"
+       && Configuration.system = "diab"
+       then 8 else 0)
+let option_small_const = ref (!option_small_data)
diff --git a/driver/Driver.ml b/driver/Driver.ml
index b8186804..aed02219 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -247,10 +247,6 @@ let process_cminor_file sourcename =
 
 (* Command-line parsing *)
 
-let starts_with s1 s2 =
-  String.length s1 >= String.length s2 &&
-  String.sub s1 0 (String.length s2) = s2
-
 let usage_string =
 "ccomp [options] <source files>
 Recognized source files:
@@ -269,6 +265,8 @@ Preprocessing options:
 Compilation options:
   -flonglong     Treat 'long long' as 'long' and 'long double' as 'double'
   -fmadd         Use fused multiply-add and multiply-sub instructions
+  -fsmall-data <n>  Set maximal size <n> for allocation in small data area
+  -fsmall-const <n>  Set maximal size <n> for allocation in small constant area
   -dcil          Save CIL-processed source in <file>.cil.c
   -dclight       Save generated Clight in <file>.light.c
   -dasm          Save generated assembly in <file>.s
@@ -281,86 +279,88 @@ General options:
   -v             Print external commands before invoking them
 "
 
-let rec parse_cmdline i =
-  if i < Array.length Sys.argv then begin
-    let s = Sys.argv.(i) in
-    if starts_with s "-I" || starts_with s "-D" || starts_with s "-U"
-    then begin
-      prepro_options := s :: !prepro_options;
-      parse_cmdline (i + 1)
-    end else 
-    if starts_with s "-l" || starts_with s "-L" then begin
-      linker_options := s :: !linker_options;
-      parse_cmdline (i + 1)
-    end else
-    if s = "-o" && i + 1 < Array.length Sys.argv then begin
-      exe_name := Sys.argv.(i + 1);
-      parse_cmdline (i + 2)
-    end else
-    if s = "-stdlib" && i + 1 < Array.length Sys.argv then begin
-      stdlib_path := Sys.argv.(i + 1);
-      parse_cmdline (i + 2)
-    end else
-    if s = "-flonglong" then begin
-      option_flonglong := true;
-      parse_cmdline (i + 1)
-    end else
-    if s = "-fmadd" then begin
-      option_fmadd := true;
-      parse_cmdline (i + 1)
-    end else
-    if s = "-dcil" then begin
-      option_dcil := true;
-      parse_cmdline (i + 1)
-    end else
-    if s = "-dclight" then begin
-      option_dclight := true;
-      parse_cmdline (i + 1)
-    end else
-    if s = "-dasm" then begin
-      option_dasm := true;
-      parse_cmdline (i + 1)
-    end else
-    if s = "-E" then begin
-      option_E := true;
-      parse_cmdline (i + 1)
-    end else
-    if s = "-S" then begin
-      option_S := true;
-      parse_cmdline (i + 1)
-    end else
-    if s = "-c" then begin
-      option_c := true;
-      parse_cmdline (i + 1)
-    end else
-    if s = "-v" then begin
-      option_v := true;
-      parse_cmdline (i + 1)
-    end else
-    if Filename.check_suffix s ".c" then begin
+type action =
+  | Set of bool ref
+  | Self of (string -> unit)
+  | String of (string -> unit)
+  | Integer of (int -> unit)
+
+let rec find_action s = function
+  | [] -> None
+  | (re, act) :: rem ->
+      if Str.string_match re s 0 then Some act else find_action s rem
+
+let parse_cmdline spec usage =
+  let acts = List.map (fun (pat, act) -> (Str.regexp pat, act)) spec in
+  let error () =
+    eprintf "Usage: %s" usage;
+    exit 2 in
+  let rec parse i =
+    if i < Array.length Sys.argv then begin
+      let s = Sys.argv.(i) in
+      match find_action s acts with
+      | None ->
+          if s <> "-help" && s <> "--help" 
+          then eprintf "Unknown argument `%s'\n" s;
+          error ()
+      | Some(Set r) ->
+          r := true; parse (i+1)
+      | Some(Self fn) ->
+          fn s; parse (i+1)
+      | Some(String fn) ->
+          if i + 1 < Array.length Sys.argv then begin
+            fn Sys.argv.(i+1); parse (i+2)
+          end else begin
+            eprintf "Option `%s' expects an argument\n" s; error()
+          end
+      | Some(Integer fn) ->
+          if i + 1 < Array.length Sys.argv then begin
+            let n =
+              try
+                int_of_string Sys.argv.(i+1)
+              with Failure _ ->
+                eprintf "Argument to option `%s' must be an integer\n" s;
+                error()
+            in
+            fn n; parse (i+2)
+          end else begin
+            eprintf "Option `%s' expects an argument\n" s; error()
+          end
+    end
+  in parse 1
+
+let cmdline_actions = [
+  "-[IDU].", Self(fun s -> prepro_options := s :: !prepro_options);
+  "-[lL].", Self(fun s -> linker_options := s :: !linker_options);
+  "-o$", String(fun s -> exe_name := s);
+  "-stdlib$", String(fun s -> stdlib_path := s);
+  "-flonglong$", Set option_flonglong;
+  "-fmadd$", Set option_fmadd;
+  "-fsmall-data$", Integer(fun n -> option_small_data := n);
+  "-fsmall-const$", Integer(fun n -> option_small_const := n);
+  "-dcil$", Set option_dcil;
+  "-dclight$", Set option_dclight;
+  "-dasm$", Set option_dasm;
+  "-E$", Set option_E;
+  "-S$", Set option_S;
+  "-c$", Set option_c;
+  "-v$", Set option_v;
+  ".*\\.c$", Self (fun s ->
       let objfile = process_c_file s in
-      linker_options := objfile :: !linker_options;
-      parse_cmdline (i + 1)
-    end else
-    if Filename.check_suffix s ".cm" then begin
+      linker_options := objfile :: !linker_options);
+  ".*\\.cm$", Self (fun s ->
       let objfile = process_cminor_file s in
-      linker_options := objfile :: !linker_options;
-      parse_cmdline (i + 1)
-    end else
-    if Filename.check_suffix s ".o" || Filename.check_suffix s ".a" then begin
-      linker_options := s :: !linker_options;
-      parse_cmdline (i + 1)
-    end else begin
-      eprintf "Unknown argument `%s'\n" s;
-      eprintf "Usage: %s" usage_string;
-      exit 2
-    end
-  end
+      linker_options := objfile :: !linker_options);
+  ".*\\.[oa]$", Self (fun s ->
+      linker_options := s :: !linker_options)
+]
 
 let _ =
   Cil.initCIL();
   CPragmas.initialize();
-  parse_cmdline 1;
-  if not (!option_c || !option_S || !option_E) then begin
+  parse_cmdline cmdline_actions usage_string;
+  if !linker_options <> [] 
+  && not (!option_c || !option_S || !option_E)
+  then begin
     linker !exe_name !linker_options
   end
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