diff options
Diffstat (limited to 'driver')
-rw-r--r-- | driver/Configuration.ml | 2 | ||||
-rw-r--r-- | driver/Configuration.mli | 3 | ||||
-rw-r--r-- | driver/Driver.ml | 46 | ||||
-rw-r--r-- | driver/Linker.ml | 17 |
4 files changed, 50 insertions, 18 deletions
diff --git a/driver/Configuration.ml b/driver/Configuration.ml index 58583330..48f8abde 100644 --- a/driver/Configuration.ml +++ b/driver/Configuration.ml @@ -184,3 +184,5 @@ let response_file_style = | v -> bad_config "response_file_style" [v] let gnu_toolchain = system <> "diab" + +let elf_target = system <> "macosx" && system <> "cygwin" diff --git a/driver/Configuration.mli b/driver/Configuration.mli index f0bb8f83..b918c169 100644 --- a/driver/Configuration.mli +++ b/driver/Configuration.mli @@ -77,3 +77,6 @@ val response_file_style: response_file_style val gnu_toolchain: bool (** Does the targeted system use the gnu toolchain *) + +val elf_target: bool + (** Is the target binary format ELF? *) diff --git a/driver/Driver.ml b/driver/Driver.ml index dfbac67f..4f27cb56 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -28,6 +28,9 @@ let sdump_folder = ref "" let jdump_magic_number = "CompCertJDUMP" ^ Version.version +let nolink () = + !option_c || !option_S || !option_E || !option_interp + let dump_jasm asm sourcename destfile = let oc = open_out_bin destfile in let pp = Format.formatter_of_out_channel oc in @@ -55,6 +58,11 @@ let dump_jasm asm sourcename destfile = Format.pp_print_flush pp (); close_out oc +let object_filename sourcename suff = + if nolink () then + output_filename ~final: !option_c sourcename suff ".o" + else + Filename.temp_file "compcert" ".o" (* From CompCert C AST to asm *) @@ -132,7 +140,7 @@ let process_c_file sourcename = compile_c_file sourcename preproname asmname; if not !option_dprepro then safe_remove preproname; - let objname = output_filename ~final: !option_c sourcename ".c" ".o" in + let objname = object_filename sourcename ".c" in assemble asmname objname; if not !option_dasm then safe_remove asmname; objname @@ -158,7 +166,7 @@ let process_i_file sourcename = then output_filename sourcename ".c" ".s" else Filename.temp_file "compcert" ".s" in compile_c_file sourcename sourcename asmname; - let objname = output_filename ~final: !option_c sourcename ".c" ".o" in + let objname = object_filename sourcename ".c" in assemble asmname objname; if not !option_dasm then safe_remove asmname; objname @@ -169,7 +177,7 @@ let process_i_file sourcename = let process_s_file sourcename = ensure_inputfile_exists sourcename; - let objname = output_filename ~final: !option_c sourcename ".s" ".o" in + let objname = object_filename sourcename ".s" in assemble sourcename objname; objname @@ -181,7 +189,7 @@ let process_S_file sourcename = end else begin let preproname = Filename.temp_file "compcert" ".s" in preprocess sourcename preproname; - let objname = output_filename ~final: !option_c sourcename ".S" ".o" in + let objname = object_filename sourcename ".S" in assemble preproname objname; safe_remove preproname; objname @@ -205,7 +213,8 @@ let version_string = else "The CompCert C verified compiler, version "^ Version.version ^ "\n" -let target_help = if Configuration.arch = "arm" then +let target_help = + if Configuration.arch = "arm" && Configuration.model <> "armv6" then {|Target processor options: -mthumb Use Thumb2 instruction encoding -marm Use classic ARM instruction encoding @@ -255,6 +264,7 @@ Processing options: (<n>=0: none, <n>=1: limited, <n>=2: full; default is full) -fcse Perform common subexpression elimination [on] -fredundancy Perform redundancy elimination [on] + -finline Perform inlining of functions [on] Code generation options: (use -fno-<opt> to turn off -f<opt>) -ffpu Use FP registers for some integer operations [on] -fsmall-data <n> Set maximal size <n> for allocation in small data area @@ -309,6 +319,14 @@ let enforce_buildnr nr = Please use matching builds of QSK and CompCert.\n" build nr; exit 2 end +let dump_mnemonics destfile = + let oc = open_out_bin destfile in + let pp = Format.formatter_of_out_channel oc in + AsmToJSON.pp_mnemonics pp; + Format.pp_print_flush pp (); + close_out oc; + exit 0 + let language_support_options = [ option_fbitfields; option_flongdouble; option_fstruct_passing; option_fvararg_calls; option_funprototyped; @@ -336,10 +354,12 @@ let cmdline_actions = (* Getting version info *) Exact "-version", Unit print_version_and_exit; Exact "--version", Unit print_version_and_exit;] @ -(* Enforcing CompCert build numbers for QSKs *) +(* Enforcing CompCert build numbers for QSKs and mnemonics dump *) (if Version.buildnr <> "" then [ Exact "-qsk-enforce-build", Integer enforce_buildnr; - Exact "--qsk-enforce-build", Integer enforce_buildnr; ] + Exact "--qsk-enforce-build", Integer enforce_buildnr; + Exact "-dump-mnemonics", String dump_mnemonics; + ] else []) @ (* Processing options *) [ Exact "-c", Set option_c; @@ -371,8 +391,11 @@ let cmdline_actions = Exact "-conf", Ignore; (* Ignore option since it is already handled *) Exact "-target", Ignore;] @ (* Ignore option since it is already handled *) (if Configuration.arch = "arm" then - [ Exact "-mthumb", Set option_mthumb; - Exact "-marm", Unset option_mthumb; ] + if Configuration.model = "armv6" then + [ Exact "-marm", Ignore ] (* Thumb needs ARMv6T2 or ARMv7 *) + else + [ Exact "-mthumb", Set option_mthumb; + Exact "-marm", Unset option_mthumb; ] else []) @ (* Assembling options *) assembler_actions @ @@ -493,8 +516,7 @@ let _ = CPragmas.initialize(); parse_cmdline cmdline_actions; DebugInit.init (); (* Initialize the debug functions *) - let nolink = !option_c || !option_S || !option_E || !option_interp in - if nolink && !option_o <> None && !num_source_files >= 2 then begin + if nolink () && !option_o <> None && !num_source_files >= 2 then begin eprintf "Ambiguous '-o' option (multiple source files)\n"; exit 2 end; @@ -504,7 +526,7 @@ let _ = exit 2 end; let linker_args = time "Total compilation time" perform_actions () in - if (not nolink) && linker_args <> [] then begin + if not (nolink ()) && linker_args <> [] then begin linker (output_filename_default "a.out") linker_args end; if Cerrors.check_errors () then exit 2 diff --git a/driver/Linker.ml b/driver/Linker.ml index 54566efb..37a5cde0 100644 --- a/driver/Linker.ml +++ b/driver/Linker.ml @@ -35,9 +35,7 @@ let linker exe_name files = let gnu_linker_help = -{| -nostartfiles Do not use the standard system startup files when - linking - -nodefaultlibs Do not use the standard system libraries when +{| -nodefaultlibs Do not use the standard system libraries when linking -nostdlib Do not use the standard system startup files or libraries when linking @@ -47,6 +45,8 @@ let linker_help = {|Linking options: -l<lib> Link library <lib> -L<dir> Add <dir> to search path for libraries + -nostartfiles Do not use the standard system startup files when + linking |} ^ (if Configuration.gnu_toolchain then gnu_linker_help else "") ^ {| -s Remove all symbol table and relocation information from the @@ -62,10 +62,15 @@ let linker_help = let linker_actions = [ Prefix "-l", Self push_linker_arg; - Prefix "-L", Self push_linker_arg; ] @ + Prefix "-L", Self push_linker_arg; + Exact "-nostartfiles", Self (fun s -> + if Configuration.gnu_toolchain then + push_linker_arg s + else + push_linker_arg "-Ws") + ] @ (if Configuration.gnu_toolchain then - [ Exact "-nostartfiles", Self push_linker_arg; - Exact "-nodefaultlibs", Self push_linker_arg; + [ Exact "-nodefaultlibs", Self push_linker_arg; Exact "-nostdlib", Self push_linker_arg;] else []) @ [ Exact "-s", Self push_linker_arg; |