From 0a450d3e1d8a9e166e198381676b7e51b8b2f7bb Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 26 Apr 2016 14:30:59 +0200 Subject: 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 --- exportclight/Clightgen.ml | 189 +++++++--------------------------------------- 1 file changed, 28 insertions(+), 161 deletions(-) (limited to 'exportclight') 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] -Recognized source files: - .c C source file -Processing options: - -E Preprocess only, send result to standard output -Preprocessing options: - -I Add to search path for #include files - -D= Define preprocessor symbol - -U Undefine preprocessor symbol - -Wp, Pass option to the preprocessor -Language support options (use -fno- to turn off -f) : - -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 .parsed.c - -dc Save generated Compcert C in .compcert.c - -dclight Save generated Clight in .light.c -General options: - -v Print external commands before invoking them -" +"The CompCert Clight generator\n\ +Usage: clightgen [options] \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- to turn off -f) :\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 .parsed.c\n\ +\ -dc Save generated Compcert C in .compcert.c\n\ +\ -dclight Save generated Clight in .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; -- cgit