diff options
Diffstat (limited to 'export/ExportDriver.ml')
| -rw-r--r-- | export/ExportDriver.ml | 219 |
1 files changed, 219 insertions, 0 deletions
diff --git a/export/ExportDriver.ml b/export/ExportDriver.ml new file mode 100644 index 00000000..d7980994 --- /dev/null +++ b/export/ExportDriver.ml @@ -0,0 +1,219 @@ +(* *********************************************************************) +(* *) +(* 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 Lesser General Public License as *) +(* published by the Free Software Foundation, either version 2.1 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. *) +(* *) +(* *********************************************************************) + +open Printf +open Commandline +open Clflags +open CommonOptions +open Driveraux +open Frontend +open Diagnostics + +let tool_name = "CompCert AST generator" + +(* Specific options *) + +type export_mode = Mode_Csyntax | Mode_Clight +let option_mode = ref Mode_Clight +let option_normalize = ref false + +(* Export the CompCert Csyntax AST *) + +let export_csyntax sourcename csyntax ofile = + let oc = open_out ofile in + ExportCsyntax.print_program (Format.formatter_of_out_channel oc) + csyntax sourcename; + close_out oc + +(* Transform the CompCert Csyntax AST into Clight and export it *) + +let export_clight sourcename csyntax ofile = + let loc = file_loc sourcename in + let clight = + match SimplExpr.transl_program csyntax with + | Errors.OK p -> + begin match SimplLocals.transf_program p with + | Errors.OK p' -> + if !option_normalize + then Clightnorm.norm_program p' + else p' + | Errors.Error msg -> + fatal_error loc "%a" print_error msg + end + | Errors.Error msg -> + fatal_error loc "%a" print_error msg in + (* Dump Clight in C syntax if requested *) + PrintClight.print_if_2 clight; + (* Print Clight in Coq syntax *) + let oc = open_out ofile in + ExportClight.print_program (Format.formatter_of_out_channel oc) + clight sourcename !option_normalize; + close_out oc + +(* From C source to exported AST *) + +let compile_c_file sourcename ifile ofile = + let set_dest dst opt ext = + dst := if !opt then Some (output_filename sourcename ".c" ext) + else None in + set_dest Cprint.destination option_dparse ".parsed.c"; + set_dest PrintCsyntax.destination option_dcmedium ".compcert.c"; + set_dest PrintClight.destination option_dclight ".light.c"; + let cs = parse_c_file sourcename ifile in + match !option_mode with + | Mode_Csyntax -> export_csyntax sourcename cs ofile + | Mode_Clight -> export_clight sourcename cs ofile + +let output_filename sourcename suff = + let prefixname = Filename.chop_suffix sourcename suff in + output_filename_default (prefixname ^ ".v") + +(* Processing of a .c file *) + +let process_c_file sourcename = + ensure_inputfile_exists sourcename; + let ofile = output_filename sourcename ".c" in + if !option_E then begin + preprocess sourcename "-" + end else begin + let preproname = if !option_dprepro then + Driveraux.output_filename sourcename ".c" ".i" + else + Driveraux.tmp_file ".i" in + preprocess sourcename preproname; + compile_c_file sourcename preproname ofile + end + +(* Processing of a .i file *) + +let process_i_file sourcename = + ensure_inputfile_exists sourcename; + let ofile = output_filename sourcename ".i" in + compile_c_file sourcename sourcename ofile + +let usage_string = + version_string tool_name ^ +{|Usage: clightgen <mode> [options] <source files> +Recognized source files: + .c C source file + .i or .p C source file that should not be preprocessed +Processing options: + -clight Produce Clight AST [default] + -csyntax Produce Csyntax AST + -normalize Normalize the generated Clight code w.r.t. loads in expressions + -canonical-idents Use canonical numbers to represent identifiers (default) + -short-idents Use small, non-canonical numbers to represent identifiers + -E Preprocess only, send result to standard output + -o <file> Generate output in <file> +|} ^ +prepro_help ^ +language_support_help ^ +{|Tracing options: + -dprepro Save C file after preprocessing in <file>.i + -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 + -dall Save all generated intermediate files in <file>.<ext> +|} ^ + general_help ^ + warning_help + + +let print_usage_and_exit () = + printf "%s" usage_string; exit 0 + +let set_all opts () = List.iter (fun r -> r := true) opts +let unset_all opts () = List.iter (fun r -> r := false) opts + +let actions : ((string -> unit) * string) list ref = ref [] +let push_action fn arg = + actions := (fn, arg) :: !actions + +let perform_actions () = + let rec perform = function + | [] -> () + | (fn,arg) :: rem -> fn arg; perform rem + in perform (List.rev !actions) + +let num_input_files = ref 0 + +let cmdline_actions = + [ +(* Getting help *) + Exact "-help", Unit print_usage_and_exit; + Exact "--help", Unit print_usage_and_exit;] + (* Getting version info *) + @ version_options tool_name @ +(* Processing options *) + [ + Exact "-csyntax", Unit (fun () -> option_mode := Mode_Csyntax); + Exact "-clight", Unit (fun () -> option_mode := Mode_Clight); + Exact "-E", Set option_E; + Exact "-normalize", Set option_normalize; + Exact "-canonical-idents", Set Camlcoq.use_canonical_atoms; + Exact "-short-idents", Unset Camlcoq.use_canonical_atoms; + 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 @ +(* Tracing options *) + [ Exact "-dprepro", Set option_dprepro; + Exact "-dparse", Set option_dparse; + Exact "-dc", Set option_dcmedium; + Exact "-dclight", Set option_dclight; + Exact "-dall", Self (fun _ -> + option_dprepro := true; + option_dparse := true; + option_dcmedium := true; + option_dclight := true;); + ] + @ general_options +(* Diagnostic options *) + @ warning_options + @ language_support_options @ +(* Catch options that are not handled *) + [Prefix "-", Self (fun s -> + fatal_error no_loc "Unknown option `%s'" s); +(* File arguments *) + Suffix ".c", Self (fun s -> + incr num_input_files; push_action process_c_file s); + Suffix ".i", Self (fun s -> + incr num_input_files; push_action process_i_file s); + Suffix ".p", Self (fun s -> + incr num_input_files; push_action process_i_file s); + ] + +let _ = +try + Gc.set { (Gc.get()) with + Gc.minor_heap_size = 524288; (* 512k *) + Gc.major_heap_increment = 4194304 (* 4M *) + }; + Printexc.record_backtrace true; + Camlcoq.use_canonical_atoms := true; + Frontend.init (); + parse_cmdline cmdline_actions; + if !option_o <> None && !num_input_files >= 2 then + fatal_error no_loc "Ambiguous '-o' option (multiple source files)"; + if !num_input_files = 0 then + fatal_error no_loc "no input file"; + perform_actions () +with + | Sys_error msg + | CmdError msg -> error no_loc "%s" msg; exit 2 + | Abort -> exit 2 + | e -> crash e |