diff options
Diffstat (limited to 'driver/Driver.ml')
| -rw-r--r-- | driver/Driver.ml | 46 |
1 files changed, 34 insertions, 12 deletions
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 |