From 83ca03c1b1f87dc74e0b97c3728c3d8d0c1aad44 Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Sat, 10 Apr 2010 15:25:00 +0000
Subject: [PATCH] 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
---
cfrontend/C2Clight.ml | 7 +++++++
powerpc/CBuiltins.ml | 2 ++
powerpc/PrintAsm.ml | 26 +++++++++++++++++++++++---
3 files changed, 32 insertions(+), 3 deletions(-)
diff --git a/cfrontend/C2Clight.ml b/cfrontend/C2Clight.ml
index b12d60bb4..100c72b11 100644
--- a/cfrontend/C2Clight.ml
+++ b/cfrontend/C2Clight.ml
@@ -791,6 +791,13 @@ let atom_sizeof a =
with Not_found ->
None
+let atom_alignof a =
+ try
+ let (env, (sto, id, ty, init)) = Hashtbl.find decl_atom a in
+ Cutil.alignof env ty
+ with Not_found ->
+ None
+
(** ** The builtin environment *)
open Cparser.Builtins
diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml
index 65cd5b4fb..da64b5653 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 31143fbbb..f528335a6 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;
--
GitLab