From 578cc2a54897e0c89425a56df7a173bebeee2382 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 5 Jan 2013 09:59:26 +0000 Subject: Put clighgen files in exportclight/ Short doc in exportclight/README git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2089 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- driver/Clightgen.ml | 282 ---------------------------------------------------- 1 file changed, 282 deletions(-) delete mode 100644 driver/Clightgen.ml (limited to 'driver') diff --git a/driver/Clightgen.ml b/driver/Clightgen.ml deleted file mode 100644 index 1805573..0000000 --- a/driver/Clightgen.ml +++ /dev/null @@ -1,282 +0,0 @@ -(* *********************************************************************) -(* *) -(* 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 INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -open Printf -open Clflags - -(* Location of the compatibility library *) - -let stdlib_path = ref( - try - Sys.getenv "COMPCERT_LIBRARY" - with Not_found -> - Configuration.stdlib_path) - -let command cmd = - if !option_v then begin - prerr_string "+ "; prerr_string cmd; prerr_endline "" - end; - Sys.command cmd - -let quote_options opts = - String.concat " " (List.rev_map Filename.quote opts) - -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.camlint_of_positive 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 "" else sprintf "> %s" ofile in - let cmd = - sprintf "%s -D__COMPCERT__ %s %s %s %s" - Configuration.prepro - (if Configuration.has_runtime_lib - then sprintf "-I%s" !stdlib_path - else "") - (quote_options !prepro_options) - ifile output in - if command 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_return 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 - (* Remove preprocessed file (always a temp file) *) - safe_remove ifile; - (* Save C AST if requested *) - if !option_dparse then begin - let ofile = Filename.chop_suffix 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 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 = Filename.chop_suffix 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 = - let clight = - match SimplExpr.transl_program csyntax with - | Errors.OK p -> - begin match SimplLocals.transf_program p with - | Errors.OK p' -> p' - | Errors.Error msg -> - print_error stderr msg; - exit 2 - end - | Errors.Error msg -> - print_error stderr msg; - exit 2 in - (* Dump Clight in C syntax if requested *) - if !option_dclight then begin - let ofile = Filename.chop_suffix sourcename ".c" ^ ".light.c" in - let oc = open_out ofile in - PrintClight.print_program (Format.formatter_of_out_channel oc) clight; - close_out oc - end; - (* Print Clight in Coq syntax *) - let oc = open_out ofile in - ExportClight.print_program (Format.formatter_of_out_channel oc) clight; - close_out oc - -(* From C source to Clight *) - -let compile_c_file sourcename ifile ofile = - compile_c_ast sourcename (parse_c_file sourcename ifile) ofile - -(* Processing of a .c file *) - -let process_c_file sourcename = - let prefixname = Filename.chop_suffix sourcename ".c" in - if !option_E then begin - preprocess sourcename "-" - end else begin - let preproname = Filename.temp_file "compcert" ".i" in - preprocess sourcename preproname; - 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 - -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 error () = - eprintf "%s" usage; - exit 2 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; - error () - | 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; error() - 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; - error() - in - fn n; parse (i+2) - end else begin - eprintf "Option `%s' expects an argument\n" s; error() - end - end - in parse 1 - -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] - -flonglong Partial emulation of 'long long' types [on] - -flongdouble Treat 'long double' as 'double' [off] - -fstruct-return Emulate returning structs and unions by value [off] - -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 .parse.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 -" - -let language_support_options = [ - option_fbitfields; option_flonglong; option_flongdouble; - option_fstruct_return; option_fvararg_calls; option_fpacked_structs -] - -let cmdline_actions = - let f_opt name ref = - ["-f" ^ name ^ "$", Set ref; "-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); - "-dparse$", Set option_dparse; - "-dc$", Set option_dcmedium; - "-dclight$", Set option_dclight; - "-E$", Set option_E; - ".*\\.c$", Self (fun s -> process_c_file s); - "-Wp,", Self (fun s -> - prepro_options := List.rev_append (explode_comma_option s) !prepro_options); - "-fall$", Self (fun _ -> - List.iter (fun r -> r := true) language_support_options); - "-fnone$", Self (fun _ -> - List.iter (fun r -> r := false) language_support_options); - ] - @ f_opt "longlong" option_flonglong - @ f_opt "longdouble" option_flongdouble - @ f_opt "struct-return" option_fstruct_return - @ f_opt "bitfields" option_fbitfields - @ f_opt "vararg-calls" option_fvararg_calls - @ f_opt "packed-structs" option_fpacked_structs - -let _ = - Gc.set { (Gc.get()) with Gc.minor_heap_size = 524288 }; - Machine.config := - begin match Configuration.arch with - | "powerpc" -> Machine.ppc_32_bigendian - | "arm" -> Machine.arm_littleendian - | "ia32" -> Machine.x86_32 - | _ -> assert false - end; - Builtins.set C2C.builtins_generic; - CPragmas.initialize(); - parse_cmdline cmdline_actions usage_string -- cgit v1.2.3