From 9b8f0f6c4683dd00ee0e3422b84c9cc34510011e Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 1 Jul 2012 07:40:04 +0000 Subject: Added option -falign-functions git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1945 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- Changelog | 4 +++- arm/PrintAsm.ml | 4 +++- driver/Clflags.ml | 1 + driver/Driver.ml | 2 ++ ia32/PrintAsm.ml | 4 +++- powerpc/PrintAsm.ml | 11 +++++++---- 6 files changed, 19 insertions(+), 7 deletions(-) diff --git a/Changelog b/Changelog index f07154c4..f585848c 100644 --- a/Changelog +++ b/Changelog @@ -37,12 +37,14 @@ New tool: produced by CompCert. Other changes: -- Elimination of "static" functions and global variables that are unused. +- Elimination of "static" functions and "static" global variables that + are not referenced in the generated code. - The memory model was enriched with "max" permissions in addition to "current" permissions, to better reason over "const" blocks and already-deallocated blocks. - More efficient implementation of the memory model, resulting in faster interpretation of source files by "ccomp -interp". +- Added option "-falign-functions" to control alignment of function code. Release 1.10, 2012-03-13 diff --git a/arm/PrintAsm.ml b/arm/PrintAsm.ml index 161c7600..86fdf0ed 100644 --- a/arm/PrintAsm.ml +++ b/arm/PrintAsm.ml @@ -680,7 +680,9 @@ let print_function oc name fn = | t :: _ -> t | _ -> Section_text in section oc text; - fprintf oc " .align 2\n"; + let alignment = + match !Clflags.option_falignfunctions with Some n -> log2 n | None -> 2 in + fprintf oc " .align %d\n" alignment; if not (C2C.atom_is_static name) then fprintf oc " .global %a\n" print_symb name; fprintf oc "%a:\n" print_symb name; diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 2be48de7..47336b5b 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -24,6 +24,7 @@ let option_fvararg_calls = ref true let option_fpacked_structs = ref false let option_fsse = ref true let option_ffloatconstprop = ref 2 +let option_falignfunctions = ref (None: int option) let option_dparse = ref false let option_dcmedium = ref false let option_dclight = ref false diff --git a/driver/Driver.ml b/driver/Driver.ml index 3d0cc162..881a895a 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -373,6 +373,7 @@ Code generation options: (use -fno- to turn off -f) : -fsmall-const Set maximal size for allocation in small constant area -ffloat-const-prop Control constant propagation of floats (=0: none, =1: limited, =2: full; default is full) + -falign_functions Set alignment (in bytes) of function entry points -Wa, Pass option to the assembler Tracing options: -dparse Save C file after parsing and elaboration in .parse.c @@ -467,6 +468,7 @@ let cmdline_actions = "-fsmall-data$", Integer(fun n -> option_small_data := n); "-fsmall-const$", Integer(fun n -> option_small_const := n); "-ffloat-const-prop$", Integer(fun n -> option_ffloatconstprop := n); + "-falign-functions$", Integer(fun n -> option_falignfunctions := Some n); "-fall$", Self (fun _ -> List.iter (fun r -> r := true) language_support_options); "-fnone$", Self (fun _ -> diff --git a/ia32/PrintAsm.ml b/ia32/PrintAsm.ml index ccc3c0f5..096e1e31 100644 --- a/ia32/PrintAsm.ml +++ b/ia32/PrintAsm.ml @@ -737,7 +737,9 @@ let print_function oc name code = | [t;l;j] -> (t, l, j) | _ -> (Section_text, Section_literal, Section_jumptable) in section oc text; - print_align oc 16; + let alignment = + match !Clflags.option_falignfunctions with Some n -> n | None -> 16 in + print_align oc alignment; if not (C2C.atom_is_static name) then fprintf oc " .globl %a\n" symbol name; fprintf oc "%a:\n" symbol name; diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index 65d6ce0f..0b94aaa4 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -875,7 +875,9 @@ let print_function oc name code = | [t;l;j] -> (t, l, j) | _ -> (Section_text, Section_literal, Section_jumptable) in section oc text; - fprintf oc " .align 2\n"; + let alignment = + match !Clflags.option_falignfunctions with Some n -> log2 n | None -> 2 in + fprintf oc " .align %d\n" alignment; if not (C2C.atom_is_static name) then fprintf oc " .globl %a\n" symbol name; fprintf oc "%a:\n" symbol name; @@ -1070,11 +1072,12 @@ let print_init oc = function | Init_int32 n -> fprintf oc " .long %ld\n" (camlint_of_coqint n) | Init_float32 n -> - fprintf oc " .long %ld %s %.18g\n" (camlint_of_coqint (Floats.Float.bits_of_single n)) - comment (camlfloat_of_coqfloat n) + fprintf oc " .long 0x%lx %s %.18g\n" + (camlint_of_coqint (Floats.Float.bits_of_single n)) + comment (camlfloat_of_coqfloat n) | Init_float64 n -> let b = camlint64_of_coqint (Floats.Float.bits_of_double n) in - fprintf oc " .long %Ld, %Ld %s %.18g\n" + fprintf oc " .long 0x%Lx, 0x%Lx %s %.18g\n" (Int64.shift_right_logical b 32) (Int64.logand b 0xFFFFFFFFL) comment (camlfloat_of_coqfloat n) -- cgit