diff options
| -rw-r--r-- | Changelog | 4 | ||||
| -rw-r--r-- | arm/PrintAsm.ml | 4 | ||||
| -rw-r--r-- | driver/Clflags.ml | 1 | ||||
| -rw-r--r-- | driver/Driver.ml | 2 | ||||
| -rw-r--r-- | ia32/PrintAsm.ml | 4 | ||||
| -rw-r--r-- | powerpc/PrintAsm.ml | 11 |
6 files changed, 19 insertions, 7 deletions
@@ -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 161c760..86fdf0e 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 2be48de..47336b5 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 3d0cc16..881a895 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -373,6 +373,7 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>) : -fsmall-const <n> Set maximal size <n> for allocation in small constant area -ffloat-const-prop <n> Control constant propagation of floats (<n>=0: none, <n>=1: limited, <n>=2: full; default is full) + -falign_functions <n> Set alignment (in bytes) of function entry points -Wa,<opt> Pass option <opt> to the assembler Tracing options: -dparse Save C file after parsing and elaboration in <file>.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 ccc3c0f..096e1e3 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 65d6ce0..0b94aaa 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) |