Preliminary support for 'aligned' and 'section' attributes, gcc-style. New-style handling of sections for IA32 and ARM. Work in progress, to be tested.

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

6 files changed, 155 insertions, 71 deletions

diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml
index 883ee72..f6bff26 100644
--- a/arm/PrintAsm.ml
+++ b/arm/PrintAsm.ml
@@ -15,6 +15,7 @@
 open Printf
 open Datatypes
 open Camlcoq
+open Sections
 open AST
 open Asm
 
@@ -98,6 +99,24 @@ let condition_name = function
   | CRgt -> "gt"
   | CRle -> "le"
 
+(* Names of sections *)
+
+let name_of_section_ELF = 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 section oc sec =
+  fprintf oc "	%s\n" (name_of_section sec)
+
 (* Record current code position and latest position at which to
    emit float and symbol constants. *)
 
@@ -525,14 +544,16 @@ let print_function oc name code =
   Hashtbl.clear current_function_labels;
   reset_constants();
   currpos := 0;
-  fprintf oc "	.text\n";
+  let (text, _, _) = sections_for_function name in
+  section oc text;
   fprintf oc "	.align 2\n";
   if not (C2C.atom_is_static name) then
     fprintf oc "	.global	%a\n" print_symb name;
-  fprintf oc "	.type	%a, %%function\n" print_symb name;
   fprintf oc "%a:\n" print_symb name;
   print_instructions oc (labels_of_code Labelset.empty code) code;
-  emit_constants oc
+  emit_constants oc;
+  fprintf oc "	.type	%a, %%function\n" print_symb name;
+  fprintf oc "	.size	%a, . - %a\n" symbol name symbol name
 
 (* Generation of stub code for external functions.
    Compcert passes the first two float arguments in F0 and F1,
@@ -566,7 +587,7 @@ let print_external_function oc name sg =
             move_args tys int_regs float_regs
         end
   in
-  fprintf oc "	.text\n";
+  section oc Section_text;
   fprintf oc "	.align 2\n";
   fprintf oc ".L%s$stub:\n" name;
   move_args sg.sig_args [IR0;IR1;IR2;IR3] [FR0;FR1];
@@ -616,15 +637,24 @@ let print_var oc (Coq_pair(name, v)) =
   match v.gvar_init with
   | [] -> ()
   | _  ->
-      if v.gvar_readonly
-      then fprintf oc "	.const\n"
-      else fprintf oc "	.data\n";
-      fprintf oc "	.align	2\n";
+      let init =
+        match v.gvar_init with [Init_space _] -> false | _ -> true in
+      let sec =
+        Sections.section_for_variable name init
+      and align =
+        match C2C.atom_alignof name with
+        | Some a -> log2 a
+        | None -> 3 (* 8-alignment is a safe default *)
+      in
+      section oc sec;
+      fprintf oc "	.align	%d\n" align;
       if not (C2C.atom_is_static name) then
         fprintf oc "	.global	%a\n" print_symb name;
       fprintf oc "	.type	%a, %%object\n" print_symb name;
       fprintf oc "%a:\n" print_symb name;
-      print_init_data oc name v.gvar_init
+      print_init_data oc name v.gvar_init;
+      fprintf oc "	.type	%a, @object\n" print_symb name;
+      fprintf oc "	.size	%a, . - %a\n" print_symb name print_symb name
 
 let print_program oc p =
   extfuns := IdentSet.empty;
diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 966bb76..1a6539a 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -719,7 +719,7 @@ let convertFundef env fd =
       a_env = env;
       a_type = Cutil.fundef_typ fd;
       a_fundef = Some fd };
-  Sections.define_function id';
+  Sections.define_function env id' fd.fd_ret;
   Datatypes.Coq_pair(id',
                      Internal {fn_return = ret; fn_params = params;
                                fn_vars = vars; fn_body = body'})
@@ -776,21 +776,6 @@ let convertInitializer env ty i =
 
 (** Global variable *)
 
-let rec type_is_readonly env t =
-  let a = Cutil.attributes_of_type env t in
-  if List.mem C.AVolatile a then false else
-  if List.mem C.AConst a then true else
-  match Cutil.unroll env t with
-  | C.TArray(t', _, _) -> type_is_readonly env t'
-  | _ -> false
-
-let rec type_is_volatile env t =
-  let a = Cutil.attributes_of_type env t in
-  if List.mem C.AConst a then true else
-  match Cutil.unroll env t with
-  | C.TArray(t', _, _) -> type_is_volatile env t'
-  | _ -> false
-
 let convertGlobvar env (sto, id, ty, optinit) =
   let id' = intern_string id.name in
   let ty' = convertTyp env ty in 
@@ -805,13 +790,14 @@ let convertGlobvar env (sto, id, ty, optinit) =
       a_env = env;
       a_type = ty;
       a_fundef = None };
-  Sections.define_variable id'
-    (match Cutil.sizeof env ty with Some sz -> sz | None -> max_int)
-    (type_is_readonly env ty);
+  Sections.define_variable env id' ty;
+  let a = Cutil.attributes_of_type env ty in
+  let volatile = List.mem C.AVolatile a in
+  let readonly = List.mem C.AConst a && not volatile in
   Datatypes.Coq_pair(id', 
                      {gvar_info = ty'; gvar_init = init';
-                      gvar_readonly = type_is_readonly env ty;
-                      gvar_volatile = type_is_volatile env ty})
+                      gvar_readonly = readonly;
+                      gvar_volatile = volatile})
 
 (** Convert a list of global declarations.
   Result is a pair [(funs, vars)] where [funs] are 
@@ -937,6 +923,7 @@ let atom_is_extern a =
   with Not_found ->
     false
 
+(*
 let atom_is_readonly a =
   try
     let i = Hashtbl.find decl_atom a in type_is_readonly i.a_env i.a_type
@@ -948,10 +935,16 @@ let atom_sizeof a =
     let i = Hashtbl.find decl_atom a in Cutil.sizeof i.a_env i.a_type
   with Not_found ->
     None
+*)
 
 let atom_alignof a =
   try
-    let i = Hashtbl.find decl_atom a in Cutil.alignof i.a_env i.a_type
+    let i = Hashtbl.find decl_atom a in
+    match Cutil.find_custom_attributes
+                  ["aligned"; "__aligned__"]
+                  (Cutil.attributes_of_type i.a_env i.a_type) with
+    | [[C.AInt n]] -> Some(Int64.to_int n)
+    | _            -> Cutil.alignof i.a_env i.a_type
   with Not_found ->
     None
 
diff --git a/common/Sections.ml b/common/Sections.ml
index 9124f85..f37144a 100644
--- a/common/Sections.ml
+++ b/common/Sections.ml
@@ -14,6 +14,7 @@
 (* *********************************************************************)
 
 open Camlcoq
+open Cparser
 
 module StringMap = Map.Make(String)
 
@@ -165,19 +166,50 @@ let default_use_section id name =
     assert ok
   end
 
-let define_function id =
-  default_use_section id "CODE"
+(* Associate an undeclared section to a global symbol, GCC-style *)
+
+let use_gcc_section id name readonly exec =
+  Hashtbl.add section_table_at_def id !current_section_table;
+  let sn = Section_user(name, not readonly, exec) in
+  let si = { sec_name_init = sn; sec_name_uninit = sn;
+             sec_writable = not readonly; sec_executable = exec;
+             sec_near_access = false } in
+  Hashtbl.add use_section_table id si
+
+(* Record sections for a variable definition *)
+
+let define_variable env id ty =
+  let attr = Cutil.attributes_of_type env ty in
+  let readonly = List.mem C.AConst attr && not(List.mem C.AVolatile attr) in
+  (* Check for a GCC-style "section" attribute *)
+  match Cutil.find_custom_attributes ["section"; "__section__"] attr with
+  | [[C.AString name]] ->
+    (* Use gcc-style section *)
+    use_gcc_section id name readonly false
+  | _ ->
+    (* Use default section appropriate for size and const-ness *)
+    let size = match Cutil.sizeof env ty with Some sz -> sz | None -> max_int in
+    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")
+
+(* Record sections for a function definition *)
+
+let define_function env id ty_res =
+  let attr = Cutil.attributes_of_type env ty_res in
+  match Cutil.find_custom_attributes ["section"; "__section__"] attr with
+  | [[C.AString name]] ->
+      use_gcc_section id name true true
+  | _ ->
+      default_use_section id "CODE"
+
+(* Record sections for a string literal *)
 
 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 *)
+(* Determine section to use for a variable *)
 
 let section_for_variable a initialized =
   try
@@ -186,8 +218,7 @@ let section_for_variable a initialized =
   with Not_found ->
     Section_data initialized
 
-(* Determine (text, literal, jumptable) sections to use 
-   for a function definition *)
+(* Determine (text, literal, jumptable) sections to use for a function *)
 
 let sections_for_function a =
   let s_text =
diff --git a/common/Sections.mli b/common/Sections.mli
index 090d4bb..c6a7c96 100644
--- a/common/Sections.mli
+++ b/common/Sections.mli
@@ -34,8 +34,8 @@ val define_section:
          -> ?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_function: Cparser.Env.t -> AST.ident -> Cparser.C.typ -> unit
+val define_variable: Cparser.Env.t -> AST.ident -> Cparser.C.typ -> unit
 val define_stringlit: AST.ident -> unit
 
 val section_for_variable: AST.ident -> bool -> section_name
diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml
index e4de2a3..33aae6a 100644
--- a/ia32/PrintAsm.ml
+++ b/ia32/PrintAsm.ml
@@ -15,6 +15,7 @@
 open Printf
 open Datatypes
 open Camlcoq
+open Sections
 open AST
 open Asm
 
@@ -132,26 +133,46 @@ let section oc name =
 
 (* Names of sections *)
 
-let (text, data, const_data, float_literal, jumptable_literal) =
+let name_of_section_ELF = function
+  | Section_text -> ".text"
+  | Section_data i | Section_small_data i -> if i then ".data" else ".bss"
+  | Section_const | Section_small_const -> ".rodata"
+  | 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_MacOS = function
+  | Section_text -> ".text"
+  | Section_data _ | Section_small_data _ -> ".data"
+  | Section_const  | Section_small_const -> ".const"
+  | Section_string -> ".const"
+  | Section_literal -> ".literal8"
+  | Section_jumptable -> ".const"
+  | Section_user(s, wr, ex) ->
+       sprintf ".section	%s, %s, %s"
+               (if wr then "__DATA" else "__TEXT") s
+               (if ex then "regular, pure_instructions" else "regular")
+
+let name_of_section_Cygwin = function
+  | Section_text -> ".text"
+  | Section_data _ | Section_small_data _ -> ".data"
+  | Section_const  | Section_small_const -> ".section	.rdata,\"dr\""
+  | Section_string -> ".section	.rdata,\"dr\""
+  | Section_literal -> ".section	.rdata,\"dr\""
+  | Section_jumptable -> ".text"
+  | Section_user _ -> assert false
+
+let name_of_section =
   match target with
-  | ELF ->
-      (".text",
-       ".data",
-       ".section	.rodata",
-       ".section	.rodata.cst8,\"a\",@progbits",
-       ".text")
-  | MacOS ->
-      (".text",
-       ".data",
-       ".const",
-       ".const_data",
-       ".text")
-  | Cygwin ->
-      (".text",
-       ".data",
-       ".section	.rdata,\"dr\"",
-       ".section	.rdata,\"dr\"",
-       ".text")
+  | ELF    -> name_of_section_ELF
+  | MacOS  -> name_of_section_MacOS
+  | Cygwin -> name_of_section_Cygwin
+
+let section oc sec =
+  fprintf oc "	%s\n" (name_of_section sec)
 
 (* SP adjustment to allocate or free a stack frame *)
 
@@ -587,6 +608,7 @@ let print_function oc name code =
   Hashtbl.clear current_function_labels;
   float_literals := [];
   jumptables := [];
+  let (text, lit, jmptbl) = sections_for_function name in
   section oc text;
   print_align oc 16;
   if not (C2C.atom_is_static name) then
@@ -598,13 +620,13 @@ let print_function oc name code =
     fprintf oc "	.size	%a, . - %a\n" symbol name symbol name
   end;
   if !float_literals <> [] then begin
-    section oc float_literal;
+    section oc lit;
     print_align oc 8;
     List.iter (print_literal oc) !float_literals;
     float_literals := []
   end;
   if !jumptables <> [] then begin
-    section oc jumptable_literal;
+    section oc jmptbl;
     print_align oc 4;
     List.iter (print_jumptable oc) !jumptables;
     jumptables := []
@@ -645,8 +667,10 @@ let print_var oc (Coq_pair(name, v)) =
   match v.gvar_init with
   | [] -> ()
   | _  ->
+      let init =
+        match v.gvar_init with [Init_space _] -> false | _ -> true in
       let sec =
-        if v.gvar_readonly then const_data else data
+        Sections.section_for_variable name init
       and align =
         match C2C.atom_alignof name with
         | Some a -> a
@@ -668,7 +692,7 @@ let print_program oc p =
   List.iter (print_var oc) p.prog_vars;
   List.iter (print_fundef oc) p.prog_funct;
   if !need_masks then begin
-    section oc float_literal;
+    section oc Section_const;  (* not Section_literal because not 8-bytes *)
     print_align oc 16;
     fprintf oc "%a:	.quad   0x8000000000000000, 0\n"
                raw_symbol "__negd_mask";
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index c0f9294..71d73c0 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -192,9 +192,12 @@ let name_of_section_MacOS = function
   | Section_const -> ".const"
   | Section_small_const -> ".const"
   | Section_string -> ".const"
-  | Section_literal -> ".const_data"
-  | Section_jumptable -> ".text"
-  | Section_user _ -> assert false
+  | Section_literal -> ".literal8"
+  | Section_jumptable -> ".const"
+  | Section_user(s, wr, ex) ->
+       sprintf ".section	%s, %s, %s"
+               (if wr then "__DATA" else "__TEXT") s
+               (if ex then "regular, pure_instructions" else "regular")
 
 let name_of_section_Linux = function
   | Section_text -> ".text"
@@ -479,7 +482,10 @@ let print_instruction oc labels = function
       fprintf oc "	bt	%a, %a\n" crbit bit label (transl_label lbl)
   | Pbtbl(r, tbl) ->
       let lbl = new_label() in
-      fprintf oc "%s begin pseudoinstr btbl(%a, %a)\n" comment ireg r label lbl;
+      fprintf oc "%s begin pseudoinstr btbl(%a)\n comment ireg r;
+      fprintf oc "%s jumptable [ " comment;
+      List.iter (fun l -> fprintf oc "%a " (transl_label l)) tbl;
+      fprintf oc "]\n";
       fprintf oc "	addis	%a, %a, %a\n" ireg GPR12 ireg r label_high lbl;
       fprintf oc "	lwz	%a, %a(%a)\n" ireg GPR12 label_low lbl ireg GPR12;
       fprintf oc "	mtctr	%a\n" ireg GPR12;