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.

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 ->