PowerPC:

- added __builtin_trap()
- generate .size and .type directives
- use natural alignment for variables


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

2 files changed, 25 insertions, 3 deletions

diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml
index 65cd5b4..da64b56 100644
--- a/powerpc/CBuiltins.ml
+++ b/powerpc/CBuiltins.ml
@@ -64,6 +64,8 @@ let builtins = {
     "__builtin_sync",
       (TVoid [], [], false);
     "__builtin_isync",
+      (TVoid [], [], false);
+    "__builtin_trap",
       (TVoid [], [], false)
   ]
 }
diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml
index 31143fb..f528335 100644
--- a/powerpc/PrintAsm.ml
+++ b/powerpc/PrintAsm.ml
@@ -219,6 +219,12 @@ let rolm_mask n =
   assert (!count = 2 || (!count = 0 && !last));
   (!mb, !me-1)
 
+(* Base-2 log of a Caml integer *)
+
+let rec log2 n =
+  assert (n > 0);
+  if n = 1 then 0 else 1 + log2 (n lsr 1)
+
 (* Built-in functions *)
 
 let re_builtin_function = Str.regexp "__builtin_"
@@ -310,6 +316,8 @@ let print_builtin_function oc s =
       fprintf oc "	sync\n"
   | "__builtin_isync" ->
       fprintf oc "	isync\n"
+  | "__builtin_trap" ->
+      fprintf oc "	trap\n"
   (* Catch-all *)
   | s ->
       invalid_arg ("unrecognized builtin function " ^ s)
@@ -610,7 +618,11 @@ let print_function oc name code =
   if not (C2Clight.atom_is_static name) then
     fprintf oc "	.globl %a\n" symbol name;
   fprintf oc "%a:\n" symbol name;
-  List.iter (print_instruction oc (labels_of_code Labelset.empty code)) code
+  List.iter (print_instruction oc (labels_of_code Labelset.empty code)) 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
 
 (* Generation of stub functions *)
 
@@ -816,13 +828,21 @@ let print_var oc (Coq_pair(Coq_pair(name, init_data), _)) =
             if C2Clight.atom_is_readonly name
             then const_data
             else data
+      and align =
+        match C2Clight.atom_alignof name with
+        | Some a -> log2 a
+        | None -> 3 (* 8-alignment is a safe default *)
       in
       section oc sec;
-      fprintf oc "	.align	3\n";
+      fprintf oc "	.align	%d\n" align;
       if not (C2Clight.atom_is_static name) then
         fprintf oc "	.globl	%a\n" symbol name;
       fprintf oc "%a:\n" symbol name;
-      print_init_data oc name init_data
+      print_init_data oc name init_data;
+      if target <> MacOS then begin
+        fprintf oc "	.type	%a, @object\n" symbol name;
+        fprintf oc "	.size	%a, . - %a\n" symbol name symbol name
+      end
 
 let print_program oc p =
   stubbed_functions := IdentSet.empty;