Revised parsing of command-line arguments (in preparation for adding more).

Honor "ccomp -E foo.h" for GCC compatibility.
Accept .o.ext files as object files for GCC compatibility.
Fixed and improved handling of Cminor source files.

3 files changed, 250 insertions, 118 deletions

diff --git a/driver/Commandline.ml b/driver/Commandline.ml
new file mode 100644
index 00000000..bc095af6
--- /dev/null
+++ b/driver/Commandline.ml
@@ -0,0 +1,105 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* Parsing of command-line flags and arguments *)
+
+open Printf
+
+type pattern =
+  | Exact of string
+  | Prefix of string
+  | Suffix of string
+  | Regexp of Str.regexp
+
+let _Regexp re = Regexp (Str.regexp re)
+
+type action =
+  | Set of bool ref
+  | Unset of bool ref
+  | Self of (string -> unit)
+  | String of (string -> unit)
+  | Integer of (int -> unit)
+
+let match_pattern text = function
+  | Exact s ->
+      text = s
+  | Prefix pref ->
+      let lpref = String.length pref and ltext = String.length text in
+      lpref < ltext && String.sub text 0 lpref = pref
+      (* strict prefix: no match if pref = text. See below. *)
+  | Suffix suff ->
+      let lsuff = String.length suff and ltext = String.length text in
+      lsuff < ltext && String.sub text (ltext - lsuff) lsuff = suff
+      (* strict suffix: no match if suff = text, so that e.g. ".c"
+         causes an error rather than being treated as a C source file. *)
+  | Regexp re ->
+      Str.string_match re text 0
+
+let rec find_action text = function
+  | [] -> None
+  | (pat, act) :: rem ->
+      if match_pattern text pat then Some act else find_action text rem
+
+let parse_array spec usage argv first last =
+  (* Split the spec into Exact patterns (in a hashtable) and other patterns *)
+  let exact_cases = (Hashtbl.create 29 : (string, action) Hashtbl.t) in
+  let rec split_spec = function
+    | [] -> []
+    | (Exact s, act) :: rem -> Hashtbl.add exact_cases s act; split_spec rem
+    | (pat, act) :: rem -> (pat, act) :: split_spec rem in
+  let inexact_cases = split_spec spec in
+  (* Parse the vector of arguments *)
+  let rec parse i =
+    if i <= last then begin
+      let s = argv.(i) in
+      let optact =
+        try Some (Hashtbl.find exact_cases s)
+        with Not_found -> find_action s inexact_cases in
+      match optact with
+      | None ->
+          if s <> "-help" && s <> "--help" 
+          then eprintf "Unknown argument `%s'\n" s
+          else printf "%s" usage;
+          exit 2
+      | Some(Set r) ->
+          r := true; parse (i+1)
+      | Some(Unset r) ->
+          r := false; parse (i+1)
+      | Some(Self fn) ->
+          fn s; parse (i+1)
+      | Some(String fn) ->
+          if i + 1 <= last then begin
+            fn argv.(i+1); parse (i+2)
+          end else begin
+            eprintf "Option `%s' expects an argument\n" s; exit 2
+          end
+      | Some(Integer fn) ->
+          if i + 1 <= last then begin
+            let n =
+              try
+                int_of_string argv.(i+1)
+              with Failure _ ->
+                eprintf "Argument to option `%s' must be an integer\n" s;
+                exit 2
+            in
+            fn n; parse (i+2)
+          end else begin
+            eprintf "Option `%s' expects an argument\n" s; exit 2
+          end
+    end
+  in parse first
+
+let parse_cmdline spec usage =
+  parse_array spec usage Sys.argv 1 (Array.length Sys.argv - 1)
diff --git a/driver/Commandline.mli b/driver/Commandline.mli
new file mode 100644
index 00000000..7a18905f
--- /dev/null
+++ b/driver/Commandline.mli
@@ -0,0 +1,41 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 GNU General Public License as published by  *)
+(*  the Free Software Foundation, either version 2 of the License, or  *)
+(*  (at your option) any later version.  This file is also distributed *)
+(*  under the terms of the INRIA Non-Commercial License Agreement.     *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(* Parsing of command-line flags and arguments *)
+
+(* A command-line specification is a list of pairs (pattern, action).
+   Command-line words are matched against the patterns, and the
+   corresponding actions are invoked. *)
+
+type pattern =
+  | Exact of string             (** exactly this string *)
+  | Prefix of string            (** any string starting with this prefix *)
+  | Suffix of string            (** any string ending with this suffix *)
+  | Regexp of Str.regexp        (** any string matching this anchored regexp *)
+
+val _Regexp: string -> pattern  (** text of an [Str] regexp *)
+
+type action =
+  | Set of bool ref             (** set the given ref to true *)
+  | Unset of bool ref           (** set the given ref to false *)
+  | Self of (string -> unit)    (** call the function with the matched string *)
+  | String of (string -> unit)  (** read next arg as a string, call function *)
+  | Integer of (int -> unit)    (** read next arg as an int, call function *)
+
+val parse_cmdline:
+  (pattern * action) list -> string (* usage string *) -> unit
+
+(* Note on precedence: [Exact] patterns are tried first, then the other
+   patterns are tried in the order in which they appear in the list. *)
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 18005302..602b01be 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -11,6 +11,7 @@
 (* *********************************************************************)
 
 open Printf
+open Commandline
 open Camlcoq
 open Clflags
 open Timing
@@ -89,7 +90,6 @@ let parse_c_file sourcename ifile =
   (* Simplification options *)
   let simplifs =
     "b" (* blocks: mandatory *)
-(*  ^ (if !option_flonglong then "l" else "") *)
   ^ (if !option_fstruct_return then "s" else "")
   ^ (if !option_fbitfields then "f" else "")
   ^ (if !option_fpacked_structs then "p" else "")
@@ -170,6 +170,14 @@ let compile_c_file sourcename ifile ofile =
 (* From Cminor to asm *)
 
 let compile_cminor_file ifile ofile =
+  (* Prepare to dump RTL, Mach, etc, if requested *)
+  let set_dest dst opt ext =
+    dst := if !opt then Some (output_filename ifile ".cm" ext)
+                   else None in
+  set_dest PrintRTL.destination option_drtl ".rtl";
+  set_dest Regalloc.destination_alloctrace option_dalloctrace ".alloctrace";
+  set_dest PrintLTL.destination option_dltl ".ltl";
+  set_dest PrintMach.destination option_dmach ".mach";
   Sections.initialize();
   let ic = open_in ifile in
   let lb = Lexing.from_channel ic in
@@ -292,7 +300,7 @@ let process_cminor_file sourcename =
       then output_filename sourcename ".cm" ".s"
       else Filename.temp_file "compcert" ".s" in
     compile_cminor_file sourcename asmname;
-    let objname = output_filename ~final: !option_c sourcename ".c" ".o" in
+    let objname = output_filename ~final: !option_c sourcename ".cm" ".o" in
     assemble asmname objname;
     if not !option_dasm then safe_remove asmname;
     objname
@@ -318,6 +326,17 @@ let process_S_file sourcename =
     objname
   end
 
+(* Processing of .h files *)
+
+let process_h_file sourcename =
+  if !option_E then begin
+    preprocess sourcename (output_filename_default "-");
+    ""
+  end else begin
+    eprintf "Error: input file %s ignored (not in -E mode)\n" sourcename;
+    exit 2
+  end    
+
 (* Record actions to be performed after parsing the command line *)
 
 let actions : ((string -> string) * string) list ref = ref []
@@ -341,57 +360,6 @@ let explode_comma_option s =
   | [] -> assert false
   | hd :: tl -> tl
 
-type action =
-  | Set of bool ref
-  | Unset of bool ref
-  | Self of (string -> unit)
-  | String of (string -> unit)
-  | Integer of (int -> unit)
-
-let rec find_action s = function
-  | [] -> None
-  | (re, act) :: rem ->
-      if Str.string_match re s 0 then Some act else find_action s rem
-
-let parse_cmdline spec usage =
-  let acts = List.map (fun (pat, act) -> (Str.regexp pat, act)) spec in
-  let rec parse i =
-    if i < Array.length Sys.argv then begin
-      let s = Sys.argv.(i) in
-      match find_action s acts with
-      | None ->
-          if s <> "-help" && s <> "--help" 
-          then eprintf "Unknown argument `%s'\n" s
-          else printf "%s" usage;
-          exit 2
-      | Some(Set r) ->
-          r := true; parse (i+1)
-      | Some(Unset r) ->
-          r := false; parse (i+1)
-      | Some(Self fn) ->
-          fn s; parse (i+1)
-      | Some(String fn) ->
-          if i + 1 < Array.length Sys.argv then begin
-            fn Sys.argv.(i+1); parse (i+2)
-          end else begin
-            eprintf "Option `%s' expects an argument\n" s; exit 2
-          end
-      | Some(Integer fn) ->
-          if i + 1 < Array.length Sys.argv then begin
-            let n =
-              try
-                int_of_string Sys.argv.(i+1)
-              with Failure _ ->
-                eprintf "Argument to option `%s' must be an integer\n" s;
-                exit 2
-            in
-            fn n; parse (i+2)
-          end else begin
-            eprintf "Option `%s' expects an argument\n" s; exit 2
-          end
-    end
-  in parse 1
-
 let usage_string =
 "The CompCert C verified compiler, version " ^ Configuration.version ^ "
 Usage: ccomp [options] <source files>
@@ -478,75 +446,91 @@ let num_source_files = ref 0
 
 let cmdline_actions =
   let f_opt name ref =
-    ["-f" ^ name ^ "$", Set ref; "-fno-" ^ name ^ "$", Unset ref] in
+    [Exact("-f" ^ name), Set ref; Exact("-fno-" ^ name), Unset ref] in
   [
-  "-I$", String(fun s -> prepro_options := s :: "-I" :: !prepro_options);
-  "-D$", String(fun s -> prepro_options := s :: "-D" :: !prepro_options);
-  "-U$", String(fun s -> prepro_options := s :: "-U" :: !prepro_options);
-  "-[IDU].", Self(fun s -> prepro_options := s :: !prepro_options);
-  "-[lL].", Self(fun s -> push_linker_arg s);
-  "-o$", String(fun s -> option_o := Some s);
-  "-E$", Set option_E;
-  "-S$", Set option_S;
-  "-c$", Set option_c;
-  "-v$", Set option_v;
-  "-g$", Self (fun s -> option_g := true; push_linker_arg s);
-  "-stdlib$", String(fun s -> stdlib_path := s);
-  "-dparse$", Set option_dparse;
-  "-dc$", Set option_dcmedium;
-  "-dclight$", Set option_dclight;
-  "-dcminor", Set option_dcminor;
-  "-drtl$", Set option_drtl;
-  "-dltl$", Set option_dltl;
-  "-dalloctrace$", Set option_dalloctrace;
-  "-dmach$", Set option_dmach;
-  "-dasm$", Set option_dasm;
-  "-sdump$", Set option_sdump;
-  "-interp$", Set option_interp;
-  "-quiet$", Self (fun _ -> Interp.trace := 0);
-  "-trace$", Self (fun _ -> Interp.trace := 2);
-  "-random$", Self (fun _ -> Interp.mode := Interp.Random);
-  "-all$", Self (fun _ -> Interp.mode := Interp.All);
-  ".*\\.c$", Self (fun s ->
-      push_action process_c_file s;
-      incr num_source_files);
-  ".*\\.[ip]$", Self (fun s ->
-      push_action process_i_file s;
-      incr num_source_files);
-  ".*\\.cm$", Self (fun s ->
-      push_action process_cminor_file s;
-      incr num_source_files);
-  ".*\\.s$", Self (fun s ->
-      push_action process_s_file s;
-      incr num_source_files);
-  ".*\\.S$", Self (fun s ->
-      push_action process_S_file s;
-      incr num_source_files);
-  ".*\\.[oa]$", Self (fun s ->
-      push_linker_arg s);
-  "-Wp,", Self (fun s ->
-      prepro_options := List.rev_append (explode_comma_option s) !prepro_options);
-  "-Wa,", Self (fun s ->
-      assembler_options := s :: !assembler_options);
-  "-Wl,", Self (fun s ->
-      push_linker_arg s);
-  "-Os$", Set option_Osize;
-  "-O$", Unset option_Osize;
-  "-timings$", Set option_timings;
-  "-mthumb$", Set option_mthumb;
-  "-marm$", Unset option_mthumb;
-  "-fsmall-data$", Integer(fun n -> option_small_data := n);
-  "-fsmall-const$", Integer(fun n -> option_small_const := n);
-  "-ffloat-const-prop$", Integer(fun n -> option_ffloatconstprop := n);
-  "-falign-functions$", Integer(fun n -> option_falignfunctions := Some n);
-  "-falign-branch-targets", Integer(fun n -> option_falignbranchtargets := n);
-  "-falign-cond-branches", Integer(fun n -> option_faligncondbranchs := n);
-  "-fall$", Self (fun _ ->
+(* File arguments *)
+  Suffix ".c", Self (fun s ->
+      push_action process_c_file s; incr num_source_files);
+  Suffix ".i", Self (fun s ->
+      push_action process_i_file s; incr num_source_files);
+  Suffix ".p", Self (fun s ->
+      push_action process_i_file s; incr num_source_files);
+  Suffix ".cm", Self (fun s ->
+      push_action process_cminor_file s; incr num_source_files);
+  Suffix ".s", Self (fun s ->
+      push_action process_s_file s; incr num_source_files);
+  Suffix ".S", Self (fun s ->
+      push_action process_S_file s; incr num_source_files);
+  Suffix ".o", Self push_linker_arg;
+  Suffix ".a", Self push_linker_arg;
+  (* GCC compatibility: .o.ext files are also object files *)
+  _Regexp ".*\\.o\\.", Self push_linker_arg;
+  (* GCC compatibility: .h files can be preprocessed with -E *)
+  Suffix ".h", Self (fun s ->
+      push_action process_h_file s; incr num_source_files);
+(* Processing options *)
+  Exact "-c", Set option_c;
+  Exact "-E", Set option_E;
+  Exact "-S", Set option_S;
+  Exact "-o", String(fun s -> option_o := Some s);
+(* Preprocessing options *)
+  Exact "-I", String(fun s -> prepro_options := s :: "-I" :: !prepro_options);
+  Prefix "-I", Self(fun s -> prepro_options := s :: !prepro_options);
+  Exact "-D", String(fun s -> prepro_options := s :: "-D" :: !prepro_options);
+  Prefix "-D", Self(fun s -> prepro_options := s :: !prepro_options);
+  Exact "-U", String(fun s -> prepro_options := s :: "-U" :: !prepro_options);
+  Prefix "-U", Self(fun s -> prepro_options := s :: !prepro_options);
+  Prefix "-Wp,", Self (fun s ->
+    prepro_options := List.rev_append (explode_comma_option s) !prepro_options);
+(* Language support options -- more below *)
+  Exact "-fall", Self (fun _ ->
               List.iter (fun r -> r := true) language_support_options);
-  "-fnone$", Self (fun _ ->
+  Exact "-fnone", Self (fun _ ->
               List.iter (fun r -> r := false) language_support_options);
+(* Debugging options *)
+  Exact "-g", Self (fun s -> option_g := true; push_linker_arg s);
+(* Code generation options -- more below *)
+  Exact "-Os", Set option_Osize;
+  Exact "-O", Unset option_Osize;
+  Exact "-fsmall-data", Integer(fun n -> option_small_data := n);
+  Exact "-fsmall-const", Integer(fun n -> option_small_const := n);
+  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);
+(* Target processor options *)
+  Exact "-mthumb", Set option_mthumb;
+  Exact "-marm", Unset option_mthumb;
+(* Assembling options *)
+  Prefix "-Wa,", Self (fun s -> assembler_options := s :: !assembler_options);
+(* Linking options *)
+  Prefix "-l", Self push_linker_arg;
+  Prefix "-L", Self push_linker_arg;
+  Prefix "-Wl,", Self push_linker_arg;
+(* Tracing options *)
+  Exact "-dparse", Set option_dparse;
+  Exact "-dc", Set option_dcmedium;
+  Exact "-dclight", Set option_dclight;
+  Exact "-dcminor", Set option_dcminor;
+  Exact "-drtl", Set option_drtl;
+  Exact "-dltl", Set option_dltl;
+  Exact "-dalloctrace", Set option_dalloctrace;
+  Exact "-dmach", Set option_dmach;
+  Exact "-dasm", Set option_dasm;
+  Exact "-sdump", Set option_sdump;
+(* General options *) 
+  Exact "-v", Set option_v;
+  Exact "-stdlib", String(fun s -> stdlib_path := s);
+  Exact "-timings", Set option_timings;
+(* Interpreter mode *)
+  Exact "-interp", Set option_interp;
+  Exact "-quiet", Self (fun _ -> Interp.trace := 0);
+  Exact "-trace", Self (fun _ -> Interp.trace := 2);
+  Exact "-random", Self (fun _ -> Interp.mode := Interp.Random);
+  Exact "-all", Self (fun _ -> Interp.mode := Interp.All)
   ]
-  @ f_opt "tailcalls" option_ftailcalls
+(* -f options: come in -f and -fno- variants *)
+(* Language support options *)
   @ f_opt "longdouble" option_flongdouble
   @ f_opt "struct-return" option_fstruct_return
   @ f_opt "bitfields" option_fbitfields
@@ -554,6 +538,8 @@ let cmdline_actions =
   @ f_opt "unprototyped" option_funprototyped
   @ f_opt "packed-structs" option_fpacked_structs
   @ f_opt "inline-asm" option_finline_asm
+(* Code generation options *)
+  @ f_opt "tailcalls" option_ftailcalls
   @ f_opt "fpu" option_ffpu
   @ f_opt "sse" option_ffpu (* backward compatibility *)