aboutsummaryrefslogtreecommitdiffstats
path: root/driver
diff options
context:
space:
mode:
authorBernhard Schommer <bernhardschommer@gmail.com>2018-01-29 12:05:37 +0100
committerBernhard Schommer <bernhardschommer@gmail.com>2018-01-29 12:05:37 +0100
commit5920d4c569337b0eb09132f6160d11b9c0c73888 (patch)
treef8ce584755d7b04afe1deff0dba3e99679b5bf4d /driver
parent7d3440a69c3a344613b11e7fe4b5f20a655d177f (diff)
downloadcompcert-kvx-5920d4c569337b0eb09132f6160d11b9c0c73888.tar.gz
compcert-kvx-5920d4c569337b0eb09132f6160d11b9c0c73888.zip
Share code for common options.
In order to avoid more divergence between the command line options of clightgen and ccomp the code for the common options, the language support options, the version string and the general options.
Diffstat (limited to 'driver')
-rw-r--r--driver/CommonOptions.ml89
-rw-r--r--driver/Driver.ml77
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