diff options
| -rw-r--r-- | driver/CommonOptions.ml | 89 | ||||
| -rw-r--r-- | driver/Driver.ml | 77 | ||||
| -rw-r--r-- | exportclight/Clightgen.ml | 85 |
3 files changed, 120 insertions, 131 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 diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml index f927e5ab..2878cb17 100644 --- a/exportclight/Clightgen.ml +++ b/exportclight/Clightgen.ml @@ -16,12 +16,11 @@ open Printf open Commandline open Clflags +open CommonOptions open Driveraux open Frontend -(* Location of the compatibility library *) - -let stdlib_path = ref Configuration.stdlib_path +let tool_name = "Clight generator" (* clightgen-specific options *) @@ -86,14 +85,8 @@ let process_i_file sourcename = let ofile = output_filename sourcename ".i" in compile_c_file sourcename sourcename ofile -let version_string = - if Version.buildnr <> "" && Version.tag <> "" then - sprintf "The CompCert Clight generator, %s, Build: %s, Tag: %s\n" Version.version Version.buildnr Version.tag - else - "The CompCert Clight generator, version "^ Version.version ^ "\n" - let usage_string = - version_string ^ + version_string tool_name^ {|Usage: clightgen [options] <source files> Recognized source files: .c C source file @@ -104,44 +97,18 @@ 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 Emulate 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 -Tracing options: +language_support_help ^ +{|Tracing options: -dparse Save C file after parsing and elaboration in <file>.parsed.c -dc Save generated Compcert C in <file>.compcert.c -dclight Save generated Clight in <file>.light.c -General options: - -stdlib <dir> Set the path of the Compcert run-time library - -v Print external commands before invoking them - -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 let print_usage_and_exit () = printf "%s" usage_string; exit 0 -let print_version_and_exit () = - printf "%s" version_string; 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 set_all opts () = List.iter (fun r -> r := true) opts let unset_all opts () = List.iter (fun r -> r := false) opts @@ -158,52 +125,30 @@ let perform_actions () = let num_input_files = ref 0 let cmdline_actions = - let f_opt name ref = - [Exact("-f" ^ name), Set ref; Exact("-fno-" ^ name), Unset ref] in [ (* Getting help *) 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; + Exact "--help", Unit print_usage_and_exit;] + (* Getting version info *) + @ version_options tool_name @ (* Processing options *) - Exact "-E", Set option_E; + [ Exact "-E", Set option_E; Exact "-normalize", Set option_normalize; Exact "-o", String(fun s -> option_o := Some s); Prefix "-o", Self (fun s -> let s = String.sub s 2 ((String.length s) - 2) in 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); (* Tracing options *) - Exact "-dparse", Set option_dparse; + [ Exact "-dparse", Set option_dparse; Exact "-dc", Set option_dcmedium; - Exact "-dclight", Set option_dclight; -(* General options *) - Exact "-v", Set option_v; - Exact "-stdlib", String(fun s -> stdlib_path := s); - Exact "-stdlib", String(fun s -> stdlib_path := s); - Exact "-conf", Ignore; (* Ignore option since it is already handled *) - Exact "-target", Ignore; (* Ignore option since it is already handled *) - ] + Exact "-dclight", Set option_dclight;] + @ general_options (* Diagnostic options *) @ Cerrors.warning_options -(* -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 - @ [ + @ language_support_options @ (* Catch options that are not handled *) - Prefix "-", Self (fun s -> + [Prefix "-", Self (fun s -> eprintf "Unknown option `%s'\n" s; exit 2); (* File arguments *) Suffix ".c", Self (fun s -> |