Moved shared frontend code in own file.

Clightgen and CompCert share the code for preprocessing as well as
parsing C files. The code as well as command line switches is moved
in the new module Frontend.
Bug 18768

1 files changed, 28 insertions, 161 deletions

diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml
index cbc2d8c4..c6ba9649 100644
--- a/exportclight/Clightgen.ml
+++ b/exportclight/Clightgen.ml
@@ -16,127 +16,13 @@
 open Printf
 open Commandline
 open Clflags
+open Driveraux
+open Frontend
 
 (* Location of the compatibility library *)
 
 let stdlib_path = ref Configuration.stdlib_path
 
-(* Invocation of external tools *)
-
-let command ?stdout args =
-  if !option_v then begin
-    eprintf "+ %s" (String.concat " " args);
-    begin match stdout with
-    | None -> ()
-    | Some f -> eprintf " > %s" f
-    end;
-    prerr_endline ""
-  end;
-  let argv = Array.of_list args in
-  assert (Array.length argv > 0);
-  try
-    let fd_out =
-      match stdout with
-      | None -> Unix.stdout
-      | Some f ->
-          Unix.openfile f [Unix.O_WRONLY; Unix.O_CREAT; Unix.O_TRUNC] 0o666 in
-    let pid =
-      Unix.create_process argv.(0) argv Unix.stdin fd_out Unix.stderr in
-    let (_, status) =
-      Unix.waitpid [] pid in
-    if stdout <> None then Unix.close fd_out;
-    match status with
-    | Unix.WEXITED rc -> rc
-    | Unix.WSIGNALED n | Unix.WSTOPPED n ->
-        eprintf "Command '%s' killed on a signal.\n" argv.(0); -1
-  with Unix.Unix_error(err, fn, param) ->
-    eprintf "Error executing '%s': %s: %s %s\n"
-            argv.(0) fn (Unix.error_message err) param;
-    -1
-
-let safe_remove file =
-  try Sys.remove file with Sys_error _ -> ()
-
-(* Printing of error messages *)
-
-let print_error oc msg =
-  let print_one_error = function
-  | Errors.MSG s -> output_string oc (Camlcoq.camlstring_of_coqstring s)
-  | Errors.CTX i -> output_string oc (Camlcoq.extern_atom i)
-  | Errors.POS i -> fprintf oc "%ld" (Camlcoq.P.to_int32 i)
-  in
-    List.iter print_one_error msg;
-    output_char oc '\n'
-
-(* Determine names for output files.  We use -o option if specified
-   and if this is the final destination file (not a dump file).
-   Otherwise, we generate a file in the current directory. *)
-
-let output_filename ?(final = false) source_file source_suffix output_suffix =
-  match !option_o with
-  | Some file when final -> file
-  | _ ->
-    Filename.basename (Filename.chop_suffix source_file source_suffix)
-    ^ output_suffix
-
-(* From C to preprocessed C *)
-
-let preprocess ifile ofile =
-  let output =
-    if ofile = "-" then None else Some ofile in
-  let cmd = List.concat [
-    Configuration.prepro;
-    ["-D__COMPCERT__"];
-    (if Configuration.has_runtime_lib
-     then ["-I" ^ !stdlib_path]
-     else []);
-    List.rev !prepro_options;
-    [ifile]
-  ] in
-  if command ?stdout:output cmd <> 0 then begin
-    if ofile <> "-" then safe_remove ofile;
-    eprintf "Error during preprocessing.\n";
-    exit 2
-  end
-
-(* From preprocessed C to Csyntax *)
-
-let parse_c_file sourcename ifile =
-  Sections.initialize();
-  (* Simplification options *)
-  let simplifs =
-    "b" (* blocks: mandatory *)
-  ^ (if !option_fstruct_passing then "s" else "")
-  ^ (if !option_fbitfields then "f" else "")
-  ^ (if !option_fpacked_structs then "p" else "")
-  in
-  (* Parsing and production of a simplified C AST *)
-  let ast =
-    match Parse.preprocessed_file simplifs sourcename ifile with
-    | None -> exit 2
-    | Some p -> p in
-  (* Save C AST if requested *)
-  if !option_dparse then begin
-    let ofile = output_filename sourcename ".c" ".parsed.c" in
-    let oc = open_out ofile in
-    Cprint.program (Format.formatter_of_out_channel oc) ast;
-    close_out oc
-  end;
-  (* Conversion to Csyntax *)
-  let csyntax =
-    match Timing.time "CompCert C generation" C2C.convertProgram ast with
-    | None -> exit 2
-    | Some p -> p in
-  flush stderr;
-  (* Save CompCert C AST if requested *)
-  if !option_dcmedium then begin
-    let ofile = output_filename sourcename ".c" ".compcert.c" in
-    let oc = open_out ofile in
-    PrintCsyntax.print_program (Format.formatter_of_out_channel oc) csyntax;
-    close_out oc
-  end;
-  csyntax
-
 (* From CompCert C AST to Clight *)
 
 let compile_c_ast sourcename csyntax ofile =
@@ -181,42 +67,30 @@ let process_c_file sourcename =
     compile_c_file sourcename preproname (prefixname ^ ".v")
   end
 
-(* Command-line parsing *)
-
-let explode_comma_option s =
-  match Str.split (Str.regexp ",") s with
-  | [] -> assert false
-  | hd :: tl -> tl
-
 let usage_string =
-"The CompCert Clight generator
-Usage: clightgen [options] <source files>
-Recognized source files:
-  .c             C source file
-Processing options:
-  -E             Preprocess only, send result to standard output
-Preprocessing options:
-  -I<dir>        Add <dir> to search path for #include files
-  -D<symb>=<val> Define preprocessor symbol
-  -U<symb>       Undefine preprocessor symbol
-  -Wp,<opt>      Pass option <opt> to the preprocessor
-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]
-  -fpacked-structs  Emulate packed structs [off]
-  -fall          Activate all language support options above
-  -fnone         Turn off all language support options above
-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:
-  -v             Print external commands before invoking them
-"
+"The CompCert Clight generator\n\
+Usage: clightgen [options] <source files>\n\
+Recognized source files:\n\
+\  .c             C source file\n\
+Processing options:\n\
+\  -E             Preprocess only, send result to standard output\n"^
+prepro_help ^
+"Language support options (use -fno-<opt> to turn off -f<opt>) :\n\
+\  -fbitfields    Emulate bit fields in structs [off]\n\
+\  -flongdouble   Treat 'long double' as 'double' [off]\n\
+\  -fstruct-passing  Support passing structs and unions by value as function\n\
+\                    results or function arguments [off]\n\
+\  -fstruct-return   Like -fstruct-passing (deprecated)\n\
+\  -fvararg-calls Emulate calls to variable-argument functions [on]\n\
+\  -fpacked-structs  Emulate packed structs [off]\n\
+\  -fall          Activate all language support options above\n\
+\  -fnone         Turn off all language support options above\n\
+Tracing options:\n\
+\  -dparse        Save C file after parsing and elaboration in <file>.parsed.c\n\
+\  -dc            Save generated Compcert C in <file>.compcert.c\n\
+\  -dclight       Save generated Clight in <file>.light.c\n\
+General options:\n\
+\  -v             Print external commands before invoking them\n"
 
 let print_usage_and_exit _ =
   printf "%s" usage_string; exit 0
@@ -238,18 +112,11 @@ let cmdline_actions =
   Exact "-help", Self print_usage_and_exit;
   Exact "--help", Self print_usage_and_exit;
 (* Processing options *)
-  Exact "-E", Set option_E;
+  Exact "-E", Set option_E;]
 (* 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);
+  @ prepro_actions @
 (* Language support options -- more below *)
-  Exact "-fall", Self (fun _ -> set_all language_support_options);
+  [Exact "-fall", Self (fun _ -> set_all language_support_options);
   Exact "-fnone", Self (fun _ -> unset_all language_support_options);
 (* Tracing options *)
   Exact "-dparse", Set option_dparse;