From 8539759095f95f2fbb680efc7633d868099114c8 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 29 Dec 2012 16:55:38 +0000 Subject: Merge of the clightgen branch: - Alternate semantics for Clight where function parameters are temporaries, not variables - New pass SimplLocals that turns non-addressed local variables into temporaries - Simplified Csharpminor, Cshmgen and Cminorgen accordingly - SimplExpr starts its temporaries above variable names, therefoe Cminorgen no longer needs to encode variable names and temps names. - Simplified Cminor parser & printer, as well as Errors, accordingly. - New tool clightgen to produce Clight AST in Coq-parsable .v files. - Removed side condition "return type is void" on rules skip_seq in the semantics of CompCert C, Clight, C#minor, Cminor. - Adapted RTLgenproof accordingly (now uses a memory extension). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2083 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- driver/Clightgen.ml | 282 ++++++++++++++++++++++++++++++++++++++++++++++++++++ driver/Compiler.v | 13 ++- driver/Driver.ml | 10 +- 3 files changed, 292 insertions(+), 13 deletions(-) create mode 100644 driver/Clightgen.ml (limited to 'driver') diff --git a/driver/Clightgen.ml b/driver/Clightgen.ml new file mode 100644 index 0000000..1805573 --- /dev/null +++ b/driver/Clightgen.ml @@ -0,0 +1,282 @@ +(* *********************************************************************) +(* *) +(* 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 diff --git a/driver/Compiler.v b/driver/Compiler.v index e6e8cc2..37f7bc2 100644 --- a/driver/Compiler.v +++ b/driver/Compiler.v @@ -39,6 +39,7 @@ Require Asm. (** Translation passes. *) Require Initializers. Require SimplExpr. +Require SimplLocals. Require Cshmgen. Require Cminorgen. Require Selection. @@ -64,6 +65,7 @@ Require Lineartyping. Require Machtyping. (** Proofs of semantic preservation and typing preservation. *) Require SimplExprproof. +Require SimplLocalsproof. Require Cshmgenproof. Require Cminorgenproof. Require Selectionproof. @@ -161,6 +163,7 @@ Definition transf_cminor_program (p: Cminor.program) : res Asm.program := Definition transf_clight_program (p: Clight.program) : res Asm.program := OK p @@ print print_Clight + @@@ SimplLocals.transf_program @@@ Cshmgen.transl_program @@@ Cminorgen.transl_program @@@ transf_cminor_program. @@ -288,16 +291,18 @@ Qed. Theorem transf_clight_program_correct: forall p tp, transf_clight_program p = OK tp -> - forward_simulation (Clight.semantics p) (Asm.semantics tp) - * backward_simulation (Clight.semantics p) (Asm.semantics tp). + forward_simulation (Clight.semantics1 p) (Asm.semantics tp) + * backward_simulation (Clight.semantics1 p) (Asm.semantics tp). Proof. intros. - assert (F: forward_simulation (Clight.semantics p) (Asm.semantics tp)). + assert (F: forward_simulation (Clight.semantics1 p) (Asm.semantics tp)). revert H; unfold transf_clight_program; simpl. rewrite print_identity. - caseEq (Cshmgen.transl_program p); simpl; try congruence; intros p1 EQ1. + caseEq (SimplLocals.transf_program p); simpl; try congruence; intros p0 EQ0. + caseEq (Cshmgen.transl_program p0); simpl; try congruence; intros p1 EQ1. caseEq (Cminorgen.transl_program p1); simpl; try congruence; intros p2 EQ2. intros EQ3. + eapply compose_forward_simulation. apply SimplLocalsproof.transf_program_correct. eauto. eapply compose_forward_simulation. apply Cshmgenproof.transl_program_correct. eauto. eapply compose_forward_simulation. apply Cminorgenproof.transl_program_correct. eauto. exact (fst (transf_cminor_program_correct _ _ EQ3)). diff --git a/driver/Driver.ml b/driver/Driver.ml index 7fe3f64..ca703fd 100644 --- a/driver/Driver.ml +++ b/driver/Driver.ml @@ -35,19 +35,11 @@ let safe_remove file = (* Printing of error messages *) -(* Locally named idents are encoded as in Cminorgen. - This function should live somewhere more central. *) -let ident_name id = - match id with - | BinPos.Coq_xO n -> Camlcoq.extern_atom n - | BinPos.Coq_xI n -> Printf.sprintf "$%ld" (Camlcoq.camlint_of_positive n) - | BinPos.Coq_xH -> "$0" - 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.CTXL i -> output_string oc (ident_name i) + | Errors.POS i -> fprintf oc "%ld" (Camlcoq.camlint_of_positive i) in List.iter print_one_error msg; output_char oc '\n' -- cgit v1.2.3