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 --- Makefile.extr | 2 +- driver/Clflags.ml | 2 + driver/Driver.ml | 380 +++++++++++++--------------------------------- driver/Driveraux.ml | 110 ++++++++++++++ driver/Driveraux.mli | 43 ++++++ driver/Frontend.ml | 163 ++++++++++++++++++++ driver/Frontend.mli | 23 +++ driver/Sysaux.ml | 85 ----------- driver/Sysaux.mli | 34 ----- exportclight/Clightgen.ml | 189 ++++------------------- 10 files changed, 475 insertions(+), 556 deletions(-) create mode 100644 driver/Driveraux.ml create mode 100644 driver/Driveraux.mli create mode 100644 driver/Frontend.ml create mode 100644 driver/Frontend.mli delete mode 100644 driver/Sysaux.ml delete mode 100644 driver/Sysaux.mli diff --git a/Makefile.extr b/Makefile.extr index 30b439ca..faec34a6 100644 --- a/Makefile.extr +++ b/Makefile.extr @@ -38,7 +38,7 @@ INCLUDES=$(patsubst %,-I %, $(DIRS)) # warning 3 = deprecated feature. Turned off for OCaml 4.02 (bytes vs strings) # warning 20 = unused function argument. There are some in extracted code -WARNINGS=-w +a-3-4-9-27-29 -strict-sequence -safe-string -warn-error +a #Deprication returns with ocaml 4.03 +WARNINGS=-w +a-3-4-9-27 -strict-sequence -safe-string -warn-error +a #Deprication returns with ocaml 4.03 extraction/%.cmx: WARNINGS +=-w -20-27-32..34-39-41-44..45 extraction/%.cmo: WARNINGS +=-w -20-27-32..34-39-41-44..45 cparser/pre_parser.cmx: WARNINGS += -w -41 diff --git a/driver/Clflags.ml b/driver/Clflags.ml index 394dc448..6a695aa4 100644 --- a/driver/Clflags.ml +++ b/driver/Clflags.ml @@ -61,3 +61,5 @@ let option_small_data = let option_small_const = ref (!option_small_data) let option_timings = ref false let option_rename_static = ref false +let stdlib_path = ref Configuration.stdlib_path +let use_standard_headers = ref Configuration.has_standard_headers diff --git a/driver/Driver.ml b/driver/Driver.ml index 0cacae13..db281d2d 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -12,95 +12,16 @@ open Printf open Commandline -open Camlcoq open Clflags open Timing -open Sysaux - -(* Location of the compatibility library *) - -let stdlib_path = ref Configuration.stdlib_path - -(* Use standard headers *) -let use_standard_headers = ref Configuration.has_standard_headers +open Driveraux +open Frontend let dump_options = ref false (* Optional sdump suffix *) let sdump_suffix = ref ".json" -(* Printing of error messages *) - -let print_error oc msg = - let print_one_error = function - | Errors.MSG s -> output_string oc (camlstring_of_coqstring s) - | Errors.CTX i -> output_string oc (extern_atom i) - | Errors.POS i -> fprintf oc "%ld" (P.to_int32 i) - in - List.iter print_one_error msg; - output_char oc '\n' - -(* 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 !use_standard_headers - then ["-I" ^ Filename.concat !stdlib_path "include" ] - else []); - List.rev !prepro_options; - [ifile] - ] in - let exc = command ?stdout:output cmd in - if exc <> 0 then begin - if ofile <> "-" then safe_remove ofile; - command_error "preprocessor" exc; - eprintf "Error during preprocessing.\n"; - exit 2 - end - -(* From preprocessed C to Csyntax *) - -let parse_c_file sourcename ifile = - Debug.init_compile_unit sourcename; - 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 - (* Dump Asm code in asm format for the validator *) let jdump_magic_number = "CompCertJDUMP" ^ Version.version @@ -366,13 +287,6 @@ let perform_actions () = | (fn, arg) :: rem -> let res = fn arg in res :: perform rem in perform (List.rev !actions) -(* Command-line parsing *) - -let explode_comma_option s = - match Str.split (Str.regexp ",") s with - | [] -> assert false - | _ :: tl -> tl - let version_string = if Version.buildnr <> "" && Version.tag <> "" then sprintf "The CompCert verified compiler, %s, Build: %s, Tag: %s\n" Version.version Version.buildnr Version.tag @@ -381,137 +295,105 @@ let version_string = let usage_string = version_string ^ - "Usage: ccomp [options] -Recognized source files: - .c C source file - .i or .p C source file that should not be preprocessed - .cm Cminor source file - .s Assembly file - .S Assembly file that must be preprocessed - .o Object file - .a Library file -Processing options: - -c Compile to object file only (no linking), result in .o - -E Preprocess only, send result to standard output - -S Compile to assembler only, save result in .s - -o Generate output in -Preprocessing options: - -I Add to search path for #include files - -include Process as if #include \"\" appears at the first - line of the primary source file. - -D= Define preprocessor symbol - -U Undefine preprocessor symbol - -Wp, Pass option to the preprocessor - -Xpreprocessor Pass option to the preprocessor - -M (GCC only) Ouput a rule suitable for make describing the - dependencies of the main source file - -MM (GCC only) Like -M but do not mention system header files - -MF (GCC only) Specifies file as output file for -M or -MM - -MG (GCC only) Assumes missing header files are generated for -M - -MP (GCC only) Add a phony target for each dependency other than - the main file - -MT (GCC only) Change the target of the rule emitted by dependency - generation - -MQ (GCC only) Like -MT but quotes - -nostdinc (GCC only) Do not search the standard system directories for - header files - -imacros (GCC only) Like -include but throws output produced by - preprocessing of away - -idirafter (GCC only) Search for header files after all directories - specified with -I and the standard system directories - -isystem (GCC only) Search for header files after all directories - specified by -I but before the standard system directories - -iquote (GCC only) Like -isystem but only for headers included with - quotes - -P (GCC only) Do not generate linemarkers - -C (GCC only) Do not discard comments - -CC (GCC only) Do not discard comments, including during macro - expansion -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 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 -Debugging options: - -g Generate debugging information - -gdwarf- (GCC only) Generate debug information in DWARF v2 or DWARF v3 - -gdepth Control generation of debugging information - (=0: none, =1: only-globals, =2: globals + locals - without locations, =3: full;) - -frename-static Rename static functions and declarations -Optimization options: (use -fno- to turn off -f) - -O Optimize the compiled code [on by default] - -O0 Do not optimize the compiled code - -O1 -O2 -O3 Synonymous for -O - -Os Optimize for code size in preference to code speed - -ftailcalls Optimize function calls in tail position [on] - -fconst-prop Perform global constant propagation [on] - -ffloat-const-prop Control constant propagation of floats - (=0: none, =1: limited, =2: full; default is full) - -fcse Perform common subexpression elimination [on] - -fredundancy Perform redundancy elimination [on] -Code generation options: (use -fno- to turn off -f) - -ffpu Use FP registers for some integer operations [on] - -fsmall-data Set maximal size for allocation in small data area - -fsmall-const Set maximal size for allocation in small constant area - -falign-functions Set alignment (in bytes) of function entry points - -falign-branch-targets Set alignment (in bytes) of branch targets - -falign-cond-branches Set alignment (in bytes) of conditional branches -Target processor options: - -mthumb (ARM only) Use Thumb2 instruction encoding - -marm (ARM only) Use classic ARM instruction encoding -Assembling options: - -Wa, Pass option to the assembler - -Xassembler Pass as an option to the assembler -Linking options: - -l Link library - -L Add to search path for libraries - -nostartfiles (GCC only) Do not use the standard system startup files when - linking - -nodefaultlibs (GCC only) Do not use the standard system libraries when - linking - -nostdlib (GCC only) Do not use the standard system startup files or - libraries when linking - -s Remove all symbol table and relocation information from the - executable - -static Prevent linking with the shared libraries - -T Use as linker command file - -Wl, Pass option to the linker - -WUl, (GCC only) Pass option to the gcc used for linking - -Xlinker Pass as an option to the linker - -u Pretend the symbol is undefined to force linking of - library modules to define it. -Tracing options: - -dprepro Save C file after preprocessing in .i - -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 - -dcminor Save generated Cminor in .cm - -drtl Save RTL at various optimization points in .rtl. - -dltl Save LTL after register allocation in .ltl - -dmach Save generated Mach code in .mach - -dasm Save generated assembly in .s - -sdump Save info for post-linking validation in .json - -doptions Save the compiler configurations in .opt.json -General options: - -stdlib 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 -Interpreter mode: - -interp Execute given .c files using the reference interpreter - -quiet Suppress diagnostic messages for the interpreter - -trace Have the interpreter produce a detailed trace of reductions - -random Randomize execution order - -all Simulate all possible execution orders -" + "Usage: ccomp [options] \n\ +Recognized source files:\n\ +\ .c C source file\n\ +\ .i or .p C source file that should not be preprocessed\n\ +\ .cm Cminor source file\n\ +\ .s Assembly file\n\ +\ .S Assembly file that must be preprocessed\n\ +\ .o Object file\n\ +\ .a Library file\n\ +Processing options:\n\ +\ -c Compile to object file only (no linking), result in .o\n\ +\ -E Preprocess only, send result to standard output\n\ +\ -S Compile to assembler only, save result in .s\n\ +\ -o Generate output in \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 Support calls to variable-argument functions [on]\n\ +\ -funprototyped Support calls to old-style functions without prototypes [on]\n\ +\ -fpacked-structs Emulate packed structs [off]\n\ +\ -finline-asm Support inline 'asm' statements [off]\n\ +\ -fall Activate all language support options above\n\ +\ -fnone Turn off all language support options above\n\ +Debugging options:\n\ +\ -g Generate debugging information\n\ +\ -gdwarf- (GCC only) Generate debug information in DWARF v2 or DWARF v3\n\ +\ -gdepth Control generation of debugging information\n\ +\ (=0: none, =1: only-globals, =2: globals + locals\n\ +\ without locations, =3: full;)\n\ +\ -frename-static Rename static functions and declarations\n\ +Optimization options: (use -fno- to turn off -f)\n\ +\ -O Optimize the compiled code [on by default]\n\ +\ -O0 Do not optimize the compiled code\n\ +\ -O1 -O2 -O3 Synonymous for -O\n\ +\ -Os Optimize for code size in preference to code speed\n\ +\ -ftailcalls Optimize function calls in tail position [on]\n\ +\ -fconst-prop Perform global constant propagation [on]\n\ +\ -ffloat-const-prop Control constant propagation of floats\n\ +\ (=0: none, =1: limited, =2: full; default is full)\n\ +\ -fcse Perform common subexpression elimination [on]\n\ +\ -fredundancy Perform redundancy elimination [on]\n\ +Code generation options: (use -fno- to turn off -f)\n\ +\ -ffpu Use FP registers for some integer operations [on]\n\ +\ -fsmall-data Set maximal size for allocation in small data area\n\ +\ -fsmall-const Set maximal size for allocation in small constant area\n\ +\ -falign-functions Set alignment (in bytes) of function entry points\n\ +\ -falign-branch-targets Set alignment (in bytes) of branch targets\n\ +\ -falign-cond-branches Set alignment (in bytes) of conditional branches\n\ +Target processor options:\n\ +\ -mthumb (ARM only) Use Thumb2 instruction encoding\n\ +\ -marm (ARM only) Use classic ARM instruction encoding\n\ +Assembling options:\n\ +\ -Wa, Pass option to the assembler\n\ +\ -Xassembler Pass as an option to the assembler\n\ +Linking options:\n\ +\ -l Link library \n\ +\ -L Add to search path for libraries\n\ +\ -nostartfiles (GCC only) Do not use the standard system startup files when\n\ +\ linking\n\ +\ -nodefaultlibs (GCC only) Do not use the standard system libraries when\n\ +\ linking\n\ +\ -nostdlib (GCC only) Do not use the standard system startup files or\n\ +\ libraries when linking\n\ +\ -s Remove all symbol table and relocation information from the\n\ +\ executable\n\ +\ -static Prevent linking with the shared libraries\n\ +\ -T Use as linker command file\n\ +\ -Wl, Pass option to the linker\n\ +\ -WUl, (GCC only) Pass option to the gcc used for linking\n\ +\ -Xlinker Pass as an option to the linker\n\ +\ -u Pretend the symbol is undefined to force linking of\n\ +\ library modules to define it.\n\ +Tracing options:\n\ +\ -dprepro Save C file after preprocessing in .i\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\ +\ -dcminor Save generated Cminor in .cm\n\ +\ -drtl Save RTL at various optimization points in .rtl.\n\ +\ -dltl Save LTL after register allocation in .ltl\n\ +\ -dmach Save generated Mach code in .mach\n\ +\ -dasm Save generated assembly in .s\n\ +\ -sdump Save info for post-linking validation in .json\n\ +\ -doptions Save the compiler configurations in .opt.json\n\ +General options:\n\ +\ -stdlib Set the path of the Compcert run-time library\n\ +\ -v Print external commands before invoking them\n\ +\ -timings Show the time spent in various compiler passes\n\ +\ -version Print the version string and exit\n\ +Interpreter mode:\n\ +\ -interp Execute given .c files using the reference interpreter\n\ +\ -quiet Suppress diagnostic messages for the interpreter\n\ +\ -trace Have the interpreter produce a detailed trace of reductions\n\ +\ -random Randomize execution order\n\ +\ -all Simulate all possible execution orders\n" let print_usage_and_exit _ = printf "%s" usage_string; exit 0 @@ -532,35 +414,10 @@ let optimization_options = [ let set_all opts = List.iter (fun r -> r := true) opts let unset_all opts = List.iter (fun r -> r := false) opts -let gnu_option s = - if Configuration.system <> "diab" then - true - else begin - eprintf "ccomp: warning: option %s only supported for gcc backend\n" s; - false - end - let gnu_linker_opt s = if gnu_option s then push_linker_arg s -(* Add gnu preprocessor list *) -let gnu_prepro_opt_key key s = - if gnu_option s then - prepro_options := s::key::!prepro_options - -(* Add gnu preprocessor option *) -let gnu_prepro_opt s = - if gnu_option s then - prepro_options := s::!prepro_options - -(* Add gnu preprocessor option s and the implict -E *) -let gnu_prepro_opt_e s = - if gnu_option s then begin - prepro_options := s :: !prepro_options; - option_E := true - end - let num_source_files = ref 0 let num_input_files = ref 0 @@ -581,38 +438,11 @@ let cmdline_actions = Exact "-S", Set option_S; 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 *) - Exact "-I", String(fun s -> prepro_options := s :: "-I" :: !prepro_options; - assembler_options := s :: "-I" :: !assembler_options); - Prefix "-I", Self(fun s -> prepro_options := s :: !prepro_options; - assembler_options := s :: !assembler_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); - Exact "-Xpreprocessor", String (fun s -> - prepro_options := s :: !prepro_options); - Exact "-include", String (fun s -> prepro_options := s :: "-include" :: !prepro_options); - Exact "-M", Self gnu_prepro_opt_e; - Exact "-MM", Self gnu_prepro_opt_e; - Exact "-MF", String (gnu_prepro_opt_key "-MF"); - Exact "-MG", Self gnu_prepro_opt; - Exact "-MP", Self gnu_prepro_opt; - Exact "-MT", String (gnu_prepro_opt_key "-MT"); - Exact "-MQ", String (gnu_prepro_opt_key "-MQ"); - Exact "-nostdinc", Self (fun s -> gnu_prepro_opt s; use_standard_headers := false); - Exact "-imacros", String (gnu_prepro_opt_key "-imacros"); - Exact "-idirafter", String (gnu_prepro_opt_key "-idirafter"); - Exact "-isystem", String (gnu_prepro_opt_key "-isystem"); - Exact "-iquote", String (gnu_prepro_opt_key "-iquore"); - Exact "-P", Self gnu_prepro_opt; - Exact "-C", Self gnu_prepro_opt; - Exact "-CC", Self gnu_prepro_opt; + option_o := Some s);] + (* Preprocessing 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); (* Debugging options *) Exact "-g", Self (fun s -> option_g := true; diff --git a/driver/Driveraux.ml b/driver/Driveraux.ml new file mode 100644 index 00000000..b5d155d4 --- /dev/null +++ b/driver/Driveraux.ml @@ -0,0 +1,110 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* 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 Printf +open Clflags + +(* Invocation of external tools *) + +let rec waitpid_no_intr pid = + try Unix.waitpid [] pid + with Unix.Unix_error (Unix.EINTR, _, _) -> waitpid_no_intr pid + +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) = + waitpid_no_intr 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 command_error n exc = + eprintf "Error: %s command failed with exit code %d (use -v to see invocation)\n" n exc + +let safe_remove file = + try Sys.remove file with Sys_error _ -> () + + +(* 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 + +(* A variant of [output_filename] where the default output name is fixed *) + +let output_filename_default default_file = + match !option_o with + | Some file -> file + | None -> default_file + +(* All input files should exist *) + +let ensure_inputfile_exists name = + if not (Sys.file_exists name) then begin + eprintf "error: no such file or directory: '%s'\n" name; + exit 2 + end +(* 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' + +let gnu_option s = + if Configuration.system <> "diab" then + true + else begin + eprintf "ccomp: warning: option %s only supported for gcc backend\n" s; + false + end + + +(* Command-line parsing *) +let explode_comma_option s = + match Str.split (Str.regexp ",") s with + | [] -> assert false + | _ :: tl -> tl diff --git a/driver/Driveraux.mli b/driver/Driveraux.mli new file mode 100644 index 00000000..539b1797 --- /dev/null +++ b/driver/Driveraux.mli @@ -0,0 +1,43 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + + +val command: ?stdout:string -> string list -> int + (** Execute the command with the given arguments and an optional file for + the stdout. Returns the exit code. *) + +val command_error: string -> int -> unit + (** Generate an error message for the given command and exit code *) + +val safe_remove: string -> unit + (** Remove the given file if it exists *) + +val output_filename: ?final:bool -> string -> string -> string -> string + (** 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. *) + +val output_filename_default: string -> string + (** Return either the file specified by -o or the given file name *) + +val ensure_inputfile_exists: string -> unit + (** Test whether the given input file exists *) + +val print_error:out_channel -> Errors.errcode list -> unit + (** Printing of error messages *) + +val gnu_option: string -> bool + (** Set the options for gnu systems *) + +val explode_comma_option: string -> string list + (** Split options by whitespace *) diff --git a/driver/Frontend.ml b/driver/Frontend.ml new file mode 100644 index 00000000..44ad1700 --- /dev/null +++ b/driver/Frontend.ml @@ -0,0 +1,163 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* 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 +open Driveraux +open Printf + +(* Common frontend functions between clightgen and ccomp *) + + +(* 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 !Clflags.use_standard_headers + then ["-I" ^ Filename.concat !Clflags.stdlib_path "include" ] + else []); + List.rev !prepro_options; + [ifile] + ] in + let exc = command ?stdout:output cmd in + if exc <> 0 then begin + if ofile <> "-" then safe_remove ofile; + command_error "preprocessor" exc; + eprintf "Error during preprocessing.\n"; + exit 2 + end + +(* From preprocessed C to Csyntax *) + +let parse_c_file sourcename ifile = + Debug.init_compile_unit sourcename; + 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 + +(* Add gnu preprocessor list *) +let gnu_prepro_opt_key key s = + if gnu_option s then + prepro_options := s::key::!prepro_options + +(* Add gnu preprocessor option *) +let gnu_prepro_opt s = + if gnu_option s then + prepro_options := s::!prepro_options + +(* Add gnu preprocessor option s and the implict -E *) +let gnu_prepro_opt_e s = + if gnu_option s then begin + prepro_options := s :: !prepro_options; + option_E := true + end + +let prepro_actions = [ + (* Preprocessing options *) + Exact "-I", String(fun s -> prepro_options := s :: "-I" :: !prepro_options; + assembler_options := s :: "-I" :: !assembler_options); + Prefix "-I", Self(fun s -> prepro_options := s :: !prepro_options; + assembler_options := s :: !assembler_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); + Exact "-Xpreprocessor", String (fun s -> + prepro_options := s :: !prepro_options); + Exact "-include", String (fun s -> prepro_options := s :: "-include" :: !prepro_options); + Exact "-M", Self gnu_prepro_opt_e; + Exact "-MM", Self gnu_prepro_opt_e; + Exact "-MF", String (gnu_prepro_opt_key "-MF"); + Exact "-MG", Self gnu_prepro_opt; + Exact "-MP", Self gnu_prepro_opt; + Exact "-MT", String (gnu_prepro_opt_key "-MT"); + Exact "-MQ", String (gnu_prepro_opt_key "-MQ"); + Exact "-nostdinc", Self (fun s -> gnu_prepro_opt s; use_standard_headers := false); + Exact "-imacros", String (gnu_prepro_opt_key "-imacros"); + Exact "-idirafter", String (gnu_prepro_opt_key "-idirafter"); + Exact "-isystem", String (gnu_prepro_opt_key "-isystem"); + Exact "-iquote", String (gnu_prepro_opt_key "-iquore"); + Exact "-P", Self gnu_prepro_opt; + Exact "-C", Self gnu_prepro_opt; + Exact "-CC", Self gnu_prepro_opt;] + +let prepro_help = "Preprocessing options:\n\ +\ -I Add to search path for #include files\n\ +\ -include Process as if #include \"\" appears at the first\n\ +\ line of the primary source file.\n\ +\ -D= Define preprocessor symbol\n\ +\ -U Undefine preprocessor symbol\n\ +\ -Wp, Pass option to the preprocessor\n\ +\ -Xpreprocessor Pass option to the preprocessor\n\ +\ -M (GCC only) Ouput a rule suitable for make describing the\n\ +\ dependencies of the main source file\n\ +\ -MM (GCC only) Like -M but do not mention system header files\n\ +\ -MF (GCC only) Specifies file as output file for -M or -MM\n\ +\ -MG (GCC only) Assumes missing header files are generated for -M\n\ +\ -MP (GCC only) Add a phony target for each dependency other than\n\ +\ the main file\n\ +\ -MT (GCC only) Change the target of the rule emitted by dependency\n\ +\ generation\n\ +\ -MQ (GCC only) Like -MT but quotes \n\ +\ -nostdinc (GCC only) Do not search the standard system directories for\n\ +\ header files\n\ +\ -imacros (GCC only) Like -include but throws output produced by\n\ +\ preprocessing of away\n\ +\ -idirafter (GCC only) Search for header files after all directories\n\ +\ specified with -I and the standard system directories\n\ +\ -isystem (GCC only) Search for header files after all directories\n\ +\ +\ specified by -I but before the standard system directories\n\ +\ -iquote (GCC only) Like -isystem but only for headers included with\n\ +\ quotes\n\ +\ -P (GCC only) Do not generate linemarkers\n\ +\ -C (GCC only) Do not discard comments\n\ +\ -CC (GCC only) Do not discard comments, including during macro\n\ +\ expansion\n" diff --git a/driver/Frontend.mli b/driver/Frontend.mli new file mode 100644 index 00000000..689f382f --- /dev/null +++ b/driver/Frontend.mli @@ -0,0 +1,23 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Xavier Leroy, INRIA Paris-Rocquencourt *) +(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +val preprocess: string -> string -> unit + (** From C to preprocessed C *) + +val parse_c_file: string -> string -> Csyntax.coq_function Ctypes.program + (** From preprocessed C to Csyntax *) + +val prepro_actions: (Commandline.pattern * Commandline.action) list + (** Commandline optins affecting the frontend *) + +val prepro_help: string diff --git a/driver/Sysaux.ml b/driver/Sysaux.ml deleted file mode 100644 index c9bdd8bf..00000000 --- a/driver/Sysaux.ml +++ /dev/null @@ -1,85 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) -(* *) -(* 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 Printf -open Clflags - -(* Invocation of external tools *) - -let rec waitpid_no_intr pid = - try Unix.waitpid [] pid - with Unix.Unix_error (Unix.EINTR, _, _) -> waitpid_no_intr pid - -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) = - waitpid_no_intr 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 command_error n exc = - eprintf "Error: %s command failed with exit code %d (use -v to see invocation)\n" n exc - -let safe_remove file = - try Sys.remove file with Sys_error _ -> () - - -(* 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 - -(* A variant of [output_filename] where the default output name is fixed *) - -let output_filename_default default_file = - match !option_o with - | Some file -> file - | None -> default_file - -(* All input files should exist *) - -let ensure_inputfile_exists name = - if not (Sys.file_exists name) then begin - eprintf "error: no such file or directory: '%s'\n" name; - exit 2 - end diff --git a/driver/Sysaux.mli b/driver/Sysaux.mli deleted file mode 100644 index c639e780..00000000 --- a/driver/Sysaux.mli +++ /dev/null @@ -1,34 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* Bernhard Schommer, AbsInt Angewandte Informatik GmbH *) -(* *) -(* 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. *) -(* *) -(* *********************************************************************) - - -val command: ?stdout:string -> string list -> int - (** Execute the command with the given arguments and an optional file for - the stdout. Returns the exit code. *) - -val command_error: string -> int -> unit - (** Generate an error message for the given command and exit code *) - -val safe_remove: string -> unit - (** Remove the given file if it exists *) - -val output_filename: ?final:bool -> string -> string -> string -> string - (** 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. *) - -val output_filename_default: string -> string - (** Return either the file specified by -o or the given file name *) - -val ensure_inputfile_exists: string -> unit - (** Test whether the given input file exists *) 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