diff options
Diffstat (limited to 'driver')
-rw-r--r-- | driver/CommonOptions.ml | 89 | ||||
-rw-r--r-- | driver/Driver.ml | 77 |
2 files changed, 105 insertions, 61 deletions
diff --git a/driver/CommonOptions.ml b/driver/CommonOptions.ml new file mode 100644 index 00000000..58dd4007 --- /dev/null +++ b/driver/CommonOptions.ml @@ -0,0 +1,89 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* *) +(* Copyright Institut National de Recherche en Informatique et en *) +(* Automatique. All rights reserved. This file is distributed *) +(* under the terms of the INRIA Non-Commercial License Agreement. *) +(* *) +(* *********************************************************************) + +open Clflags +open Commandline + +(* The version string for [tool_name] *) +let version_string tool_name= + if Version.buildnr <> "" && Version.tag <> "" then + Printf.sprintf "The CompCert %s, %s, Build: %s, Tag: %s\n" tool_name Version.version Version.buildnr Version.tag + else + Printf.sprintf "The CompCert %s, version %s\n" tool_name Version.version + +(* Print the version string and exit the program *) +let print_version_and_exit tool_name () = + Printf.printf "%s" (version_string tool_name); exit 0 + +let version_options tool_name = + [ Exact "-version", Unit (print_version_and_exit tool_name); + Exact "--version", Unit (print_version_and_exit tool_name);] + +(* Language support options *) + +let all_language_support_options = [ + option_fbitfields; option_flongdouble; + option_fstruct_passing; option_fvararg_calls; option_funprototyped; + option_fpacked_structs; option_finline_asm +] + +let f_opt name ref = + [Exact("-f" ^ name), Set ref; Exact("-fno-" ^ name), Unset ref] +let set_all opts () = List.iter (fun r -> r := true) opts +let unset_all opts () = List.iter (fun r -> r := false) opts + +let language_support_options = + [ Exact "-fall", Unit (set_all all_language_support_options); + Exact "-fnone", Unit (unset_all all_language_support_options);] + @ f_opt "longdouble" option_flongdouble + @ f_opt "struct-return" option_fstruct_passing + @ f_opt "struct-passing" option_fstruct_passing + @ f_opt "bitfields" option_fbitfields + @ f_opt "vararg-calls" option_fvararg_calls + @ f_opt "unprototyped" option_funprototyped + @ f_opt "packed-structs" option_fpacked_structs + @ f_opt "inline-asm" option_finline_asm + +let language_support_help = + {|Language support options (use -fno-<opt> to turn off -f<opt>) : + -fbitfields Emulate bit fields in structs [off] + -flongdouble Treat 'long double' as 'double' [off] + -fstruct-passing Support passing structs and unions by value as function + results or function arguments [off] + -fstruct-return Like -fstruct-passing (deprecated) + -fvararg-calls Support calls to variable-argument functions [on] + -funprototyped Support calls to old-style functions without prototypes [on] + -fpacked-structs Emulate packed structs [off] + -finline-asm Support inline 'asm' statements [off] + -fall Activate all language support options above + -fnone Turn off all language support options above +|} + +(* General options *) + +let general_help = + {|General options: + -stdlib <dir> Set the path of the Compcert run-time library + -v Print external commands before invoking them + -timings Show the time spent in various compiler passes + -version Print the version string and exit + -target <value> Generate code for the given target + -conf <file> Read configuration from file + @<file> Read command line options from <file> +|} + +let general_options = + [ Exact "-conf", Ignore; (* Ignore option since it is already handled *) + Exact "-target", Ignore;(* Ignore option since it is already handled *) + Exact "-v", Set option_v; + Exact "-stdlib", String(fun s -> stdlib_path := s); + Exact "-timings", Set option_timings;] diff --git a/driver/Driver.ml b/driver/Driver.ml index d891cab7..063e49d2 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -13,12 +13,16 @@ open Printf open Commandline open Clflags +open CommonOptions open Timing open Driveraux open Frontend open Assembler open Linker +(* Name used for version string etc. *) +let tool_name = "C verified compiler" + (* Optional sdump suffix *) let sdump_suffix = ref ".json" @@ -144,12 +148,6 @@ let process_h_file sourcename = exit 2 end -let version_string = - if Version.buildnr <> "" && Version.tag <> "" then - sprintf "The CompCert C verified compiler, %s, Build: %s, Tag: %s\n" Version.version Version.buildnr Version.tag - else - "The CompCert C verified compiler, version "^ Version.version ^ "\n" - let target_help = if Configuration.arch = "arm" && Configuration.model <> "armv6" then {|Target processor options: @@ -167,7 +165,7 @@ let toolchain_help = "" let usage_string = - version_string ^ + version_string tool_name ^ {|Usage: ccomp [options] <source files> Recognized source files: .c C source file @@ -183,19 +181,7 @@ Processing options: -o <file> Generate output in <file> |} ^ prepro_help ^ -{|Language support options (use -fno-<opt> to turn off -f<opt>) : - -fbitfields Emulate bit fields in structs [off] - -flongdouble Treat 'long double' as 'double' [off] - -fstruct-passing Support passing structs and unions by value as function - results or function arguments [off] - -fstruct-return Like -fstruct-passing (deprecated) - -fvararg-calls Support calls to variable-argument functions [on] - -funprototyped Support calls to old-style functions without prototypes [on] - -fpacked-structs Emulate packed structs [off] - -finline-asm Support inline 'asm' statements [off] - -fall Activate all language support options above - -fnone Turn off all language support options above -|}^ + language_support_help ^ DebugInit.debugging_help ^ {|Optimization options: (use -fno-<opt> to turn off -f<opt>) -O Optimize the compiled code [on by default] @@ -235,15 +221,8 @@ Code generation options: (use -fno-<opt> to turn off -f<opt>) -dasm Save generated assembly in <file>.s -dall Save all generated intermediate files in <file>.<ext> -sdump Save info for post-linking validation in <file>.json -General options: - -stdlib <dir> Set the path of the Compcert run-time library - -v Print external commands before invoking them - -timings Show the time spent in various compiler passes - -version Print the version string and exit - -target <value> Generate code for the given target - -conf <file> Read configuration from file - @<file> Read command line options from <file> |} ^ + general_help ^ Cerrors.warning_help ^ {|Interpreter mode: -interp Execute given .c files using the reference interpreter @@ -256,9 +235,6 @@ General options: let print_usage_and_exit () = printf "%s" usage_string; exit 0 -let print_version_and_exit () = - printf "%s" version_string; exit 0 - let enforce_buildnr nr = let build = int_of_string Version.buildnr in if nr != build then begin @@ -274,12 +250,6 @@ let dump_mnemonics destfile = close_out oc; exit 0 -let language_support_options = [ - option_fbitfields; option_flongdouble; - option_fstruct_passing; option_fvararg_calls; option_funprototyped; - option_fpacked_structs; option_finline_asm -] - let optimization_options = [ option_ftailcalls; option_fconstprop; option_fcse; option_fredundancy; option_finline_functions_called_once; ] @@ -297,10 +267,9 @@ let cmdline_actions = [ (* Getting help *) Exact "-help", Unit print_usage_and_exit; - Exact "--help", Unit print_usage_and_exit; + Exact "--help", Unit print_usage_and_exit;] (* Getting version info *) - Exact "-version", Unit print_version_and_exit; - Exact "--version", Unit print_version_and_exit;] @ + @ version_options tool_name @ (* Enforcing CompCert build numbers for QSKs and mnemonics dump *) (if Version.buildnr <> "" then [ Exact "-qsk-enforce-build", Integer enforce_buildnr; @@ -317,10 +286,9 @@ let cmdline_actions = option_o := Some s);] (* Preprocessing options *) @ prepro_actions @ -(* Language support options -- more below *) - [ Exact "-fall", Unit (set_all language_support_options); - Exact "-fnone", Unit (unset_all language_support_options);] - (* Debugging options *) + (* Language support options *) + language_support_options + (* Debugging options *) @ DebugInit.debugging_actions @ (* Code generation options -- more below *) [ @@ -333,10 +301,8 @@ let cmdline_actions = Exact "-ffloat-const-prop", Integer(fun n -> option_ffloatconstprop := n); Exact "-falign-functions", Integer(fun n -> option_falignfunctions := Some n); Exact "-falign-branch-targets", Integer(fun n -> option_falignbranchtargets := n); - Exact "-falign-cond-branches", Integer(fun n -> option_faligncondbranchs := n); + Exact "-falign-cond-branches", Integer(fun n -> option_faligncondbranchs := n);] @ (* Target processor options *) - 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 if Configuration.model = "armv6" then [ Exact "-marm", Ignore ] (* Thumb needs ARMv6T2 or ARMv7 *) @@ -379,11 +345,9 @@ let cmdline_actions = option_dasm := true); Exact "-sdump", Set option_sdump; Exact "-sdump-suffix", String (fun s -> option_sdump := true; sdump_suffix:= s); - Exact "-sdump-folder", String (fun s -> AsmToJSON.sdump_folder := s); + Exact "-sdump-folder", String (fun s -> AsmToJSON.sdump_folder := s);] @ (* General options *) - Exact "-v", Set option_v; - Exact "-stdlib", String(fun s -> stdlib_path := s); - Exact "-timings", Set option_timings;] @ + general_options @ (* Diagnostic options *) Cerrors.warning_options @ (* Interpreter mode *) @@ -393,17 +357,8 @@ let cmdline_actions = Exact "-random", Unit (fun () -> Interp.mode := Interp.Random); Exact "-all", Unit (fun () -> Interp.mode := Interp.All) ] -(* -f options: come in -f and -fno- variants *) -(* Language support options *) - @ f_opt "longdouble" option_flongdouble - @ f_opt "struct-return" option_fstruct_passing - @ f_opt "struct-passing" option_fstruct_passing - @ f_opt "bitfields" option_fbitfields - @ f_opt "vararg-calls" option_fvararg_calls - @ f_opt "unprototyped" option_funprototyped - @ f_opt "packed-structs" option_fpacked_structs - @ f_opt "inline-asm" option_finline_asm (* Optimization options *) +(* -f options: come in -f and -fno- variants *) @ f_opt "tailcalls" option_ftailcalls @ f_opt "const-prop" option_fconstprop @ f_opt "cse" option_fcse |