From dffc9885e54f9c68af23ec79023dfe8516a4cc32 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 16 Sep 2021 14:54:22 +0200 Subject: Add support to clightgen for generating Csyntax AST as .v files As proposed in #404. This is presented as a new option `-clight` to the existing `clightgen` tool. Revise clightgen testing to test the Csyntax output in addition to the Clight output. --- export/Clightdefs.v | 247 +-------------------------------------------- export/Clightgen.ml | 201 ------------------------------------- export/Csyntaxdefs.v | 65 ++++++++++++ export/Ctypesdefs.v | 260 ++++++++++++++++++++++++++++++++++++++++++++++++ export/ExportBase.ml | 15 ++- export/ExportClight.ml | 2 +- export/ExportCsyntax.ml | 209 ++++++++++++++++++++++++++++++++++++++ export/ExportCtypes.ml | 11 +- export/ExportDriver.ml | 219 ++++++++++++++++++++++++++++++++++++++++ 9 files changed, 781 insertions(+), 448 deletions(-) delete mode 100644 export/Clightgen.ml create mode 100644 export/Csyntaxdefs.v create mode 100644 export/Ctypesdefs.v create mode 100644 export/ExportCsyntax.ml create mode 100644 export/ExportDriver.ml (limited to 'export') diff --git a/export/Clightdefs.v b/export/Clightdefs.v index 708be1cb..dc4e3491 100644 --- a/export/Clightdefs.v +++ b/export/Clightdefs.v @@ -14,50 +14,11 @@ (* *) (* *********************************************************************) -(** All imports and definitions used by .v Clight files generated by clightgen *) +(** Definitions used by .v files generated by clightgen *) -From Coq Require Import Ascii String List ZArith. -From compcert Require Import Integers Floats Maps Errors AST Ctypes Cop Clight. - -(** ** Short names for types *) - -Definition tvoid := Tvoid. -Definition tschar := Tint I8 Signed noattr. -Definition tuchar := Tint I8 Unsigned noattr. -Definition tshort := Tint I16 Signed noattr. -Definition tushort := Tint I16 Unsigned noattr. -Definition tint := Tint I32 Signed noattr. -Definition tuint := Tint I32 Unsigned noattr. -Definition tbool := Tint IBool Unsigned noattr. -Definition tlong := Tlong Signed noattr. -Definition tulong := Tlong Unsigned noattr. -Definition tfloat := Tfloat F32 noattr. -Definition tdouble := Tfloat F64 noattr. -Definition tptr (t: type) := Tpointer t noattr. -Definition tarray (t: type) (sz: Z) := Tarray t sz noattr. - -Definition volatile_attr := {| attr_volatile := true; attr_alignas := None |}. - -Definition tattr (a: attr) (ty: type) := - match ty with - | Tvoid => Tvoid - | Tint sz si _ => Tint sz si a - | Tlong si _ => Tlong si a - | Tfloat sz _ => Tfloat sz a - | Tpointer elt _ => Tpointer elt a - | Tarray elt sz _ => Tarray elt sz a - | Tfunction args res cc => Tfunction args res cc - | Tstruct id _ => Tstruct id a - | Tunion id _ => Tunion id a - end. - -Definition tvolatile (ty: type) := tattr volatile_attr ty. - -Definition talignas (n: N) (ty: type) := - tattr {| attr_volatile := false; attr_alignas := Some n |} ty. - -Definition tvolatile_alignas (n: N) (ty: type) := - tattr {| attr_volatile := true; attr_alignas := Some n |} ty. +From Coq Require Import List. +From compcert Require Import Maps Errors AST Ctypes Clight. +From compcert Require Export Ctypesdefs. (** ** Constructor for programs and compilation units *) @@ -86,206 +47,6 @@ Definition mkprogram (types: list composite_definition) prog_comp_env := ce; prog_comp_env_eq := EQ |}. -(** ** Encoding character strings as positive numbers *) - -(** The following encoding of character strings as positive numbers - must be kept consistent with the OCaml function [Camlcoq.pos_of_string]. *) - -Definition append_bit_pos (b: bool) (p: positive) : positive := - if b then xI p else xO p. - -Definition append_char_pos_default (c: ascii) (p: positive) : positive := - let '(Ascii b7 b6 b5 b4 b3 b2 b1 b0) := c in - xI (xI (xI (xI (xI (xI - (append_bit_pos b0 (append_bit_pos b1 - (append_bit_pos b2 (append_bit_pos b3 - (append_bit_pos b4 (append_bit_pos b5 - (append_bit_pos b6 (append_bit_pos b7 p))))))))))))). - -Definition append_char_pos (c: ascii) (p: positive) : positive := - match c with - | "0"%char => xO (xO (xO (xO (xO (xO p))))) - | "1"%char => xI (xO (xO (xO (xO (xO p))))) - | "2"%char => xO (xI (xO (xO (xO (xO p))))) - | "3"%char => xI (xI (xO (xO (xO (xO p))))) - | "4"%char => xO (xO (xI (xO (xO (xO p))))) - | "5"%char => xI (xO (xI (xO (xO (xO p))))) - | "6"%char => xO (xI (xI (xO (xO (xO p))))) - | "7"%char => xI (xI (xI (xO (xO (xO p))))) - | "8"%char => xO (xO (xO (xI (xO (xO p))))) - | "9"%char => xI (xO (xO (xI (xO (xO p))))) - | "a"%char => xO (xI (xO (xI (xO (xO p))))) - | "b"%char => xI (xI (xO (xI (xO (xO p))))) - | "c"%char => xO (xO (xI (xI (xO (xO p))))) - | "d"%char => xI (xO (xI (xI (xO (xO p))))) - | "e"%char => xO (xI (xI (xI (xO (xO p))))) - | "f"%char => xI (xI (xI (xI (xO (xO p))))) - | "g"%char => xO (xO (xO (xO (xI (xO p))))) - | "h"%char => xI (xO (xO (xO (xI (xO p))))) - | "i"%char => xO (xI (xO (xO (xI (xO p))))) - | "j"%char => xI (xI (xO (xO (xI (xO p))))) - | "k"%char => xO (xO (xI (xO (xI (xO p))))) - | "l"%char => xI (xO (xI (xO (xI (xO p))))) - | "m"%char => xO (xI (xI (xO (xI (xO p))))) - | "n"%char => xI (xI (xI (xO (xI (xO p))))) - | "o"%char => xO (xO (xO (xI (xI (xO p))))) - | "p"%char => xI (xO (xO (xI (xI (xO p))))) - | "q"%char => xO (xI (xO (xI (xI (xO p))))) - | "r"%char => xI (xI (xO (xI (xI (xO p))))) - | "s"%char => xO (xO (xI (xI (xI (xO p))))) - | "t"%char => xI (xO (xI (xI (xI (xO p))))) - | "u"%char => xO (xI (xI (xI (xI (xO p))))) - | "v"%char => xI (xI (xI (xI (xI (xO p))))) - | "w"%char => xO (xO (xO (xO (xO (xI p))))) - | "x"%char => xI (xO (xO (xO (xO (xI p))))) - | "y"%char => xO (xI (xO (xO (xO (xI p))))) - | "z"%char => xI (xI (xO (xO (xO (xI p))))) - | "A"%char => xO (xO (xI (xO (xO (xI p))))) - | "B"%char => xI (xO (xI (xO (xO (xI p))))) - | "C"%char => xO (xI (xI (xO (xO (xI p))))) - | "D"%char => xI (xI (xI (xO (xO (xI p))))) - | "E"%char => xO (xO (xO (xI (xO (xI p))))) - | "F"%char => xI (xO (xO (xI (xO (xI p))))) - | "G"%char => xO (xI (xO (xI (xO (xI p))))) - | "H"%char => xI (xI (xO (xI (xO (xI p))))) - | "I"%char => xO (xO (xI (xI (xO (xI p))))) - | "J"%char => xI (xO (xI (xI (xO (xI p))))) - | "K"%char => xO (xI (xI (xI (xO (xI p))))) - | "L"%char => xI (xI (xI (xI (xO (xI p))))) - | "M"%char => xO (xO (xO (xO (xI (xI p))))) - | "N"%char => xI (xO (xO (xO (xI (xI p))))) - | "O"%char => xO (xI (xO (xO (xI (xI p))))) - | "P"%char => xI (xI (xO (xO (xI (xI p))))) - | "Q"%char => xO (xO (xI (xO (xI (xI p))))) - | "R"%char => xI (xO (xI (xO (xI (xI p))))) - | "S"%char => xO (xI (xI (xO (xI (xI p))))) - | "T"%char => xI (xI (xI (xO (xI (xI p))))) - | "U"%char => xO (xO (xO (xI (xI (xI p))))) - | "V"%char => xI (xO (xO (xI (xI (xI p))))) - | "W"%char => xO (xI (xO (xI (xI (xI p))))) - | "X"%char => xI (xI (xO (xI (xI (xI p))))) - | "Y"%char => xO (xO (xI (xI (xI (xI p))))) - | "Z"%char => xI (xO (xI (xI (xI (xI p))))) - | "_"%char => xO (xI (xI (xI (xI (xI p))))) - | _ => append_char_pos_default c p - end. - -Fixpoint ident_of_string (s: string) : ident := - match s with - | EmptyString => xH - | String c s => append_char_pos c (ident_of_string s) - end. - -(** The inverse conversion, from encoded strings to strings *) - -Section DECODE_BITS. - -Variable rec: positive -> string. - -Fixpoint decode_n_bits (n: nat) (l: list bool) (p: positive) : string := - match n with - | O => - match l with - | b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: _ => - String (Ascii b7 b6 b5 b4 b3 b2 b1 b0) (rec p) - | _ => EmptyString - end - | S n => - match p with - | xO q => decode_n_bits n (false :: l) q - | xI q => decode_n_bits n (true :: l) q - | xH => EmptyString - end - end. - -Definition decode_8_bits := Eval compute in (decode_n_bits 8%nat nil). - -End DECODE_BITS. - -Fixpoint string_of_ident (p: positive) : string := - match p with - | xO (xO (xO (xO (xO (xO p))))) => String "0"%char (string_of_ident p) - | xI (xO (xO (xO (xO (xO p))))) => String "1"%char (string_of_ident p) - | xO (xI (xO (xO (xO (xO p))))) => String "2"%char (string_of_ident p) - | xI (xI (xO (xO (xO (xO p))))) => String "3"%char (string_of_ident p) - | xO (xO (xI (xO (xO (xO p))))) => String "4"%char (string_of_ident p) - | xI (xO (xI (xO (xO (xO p))))) => String "5"%char (string_of_ident p) - | xO (xI (xI (xO (xO (xO p))))) => String "6"%char (string_of_ident p) - | xI (xI (xI (xO (xO (xO p))))) => String "7"%char (string_of_ident p) - | xO (xO (xO (xI (xO (xO p))))) => String "8"%char (string_of_ident p) - | xI (xO (xO (xI (xO (xO p))))) => String "9"%char (string_of_ident p) - | xO (xI (xO (xI (xO (xO p))))) => String "a"%char (string_of_ident p) - | xI (xI (xO (xI (xO (xO p))))) => String "b"%char (string_of_ident p) - | xO (xO (xI (xI (xO (xO p))))) => String "c"%char (string_of_ident p) - | xI (xO (xI (xI (xO (xO p))))) => String "d"%char (string_of_ident p) - | xO (xI (xI (xI (xO (xO p))))) => String "e"%char (string_of_ident p) - | xI (xI (xI (xI (xO (xO p))))) => String "f"%char (string_of_ident p) - | xO (xO (xO (xO (xI (xO p))))) => String "g"%char (string_of_ident p) - | xI (xO (xO (xO (xI (xO p))))) => String "h"%char (string_of_ident p) - | xO (xI (xO (xO (xI (xO p))))) => String "i"%char (string_of_ident p) - | xI (xI (xO (xO (xI (xO p))))) => String "j"%char (string_of_ident p) - | xO (xO (xI (xO (xI (xO p))))) => String "k"%char (string_of_ident p) - | xI (xO (xI (xO (xI (xO p))))) => String "l"%char (string_of_ident p) - | xO (xI (xI (xO (xI (xO p))))) => String "m"%char (string_of_ident p) - | xI (xI (xI (xO (xI (xO p))))) => String "n"%char (string_of_ident p) - | xO (xO (xO (xI (xI (xO p))))) => String "o"%char (string_of_ident p) - | xI (xO (xO (xI (xI (xO p))))) => String "p"%char (string_of_ident p) - | xO (xI (xO (xI (xI (xO p))))) => String "q"%char (string_of_ident p) - | xI (xI (xO (xI (xI (xO p))))) => String "r"%char (string_of_ident p) - | xO (xO (xI (xI (xI (xO p))))) => String "s"%char (string_of_ident p) - | xI (xO (xI (xI (xI (xO p))))) => String "t"%char (string_of_ident p) - | xO (xI (xI (xI (xI (xO p))))) => String "u"%char (string_of_ident p) - | xI (xI (xI (xI (xI (xO p))))) => String "v"%char (string_of_ident p) - | xO (xO (xO (xO (xO (xI p))))) => String "w"%char (string_of_ident p) - | xI (xO (xO (xO (xO (xI p))))) => String "x"%char (string_of_ident p) - | xO (xI (xO (xO (xO (xI p))))) => String "y"%char (string_of_ident p) - | xI (xI (xO (xO (xO (xI p))))) => String "z"%char (string_of_ident p) - | xO (xO (xI (xO (xO (xI p))))) => String "A"%char (string_of_ident p) - | xI (xO (xI (xO (xO (xI p))))) => String "B"%char (string_of_ident p) - | xO (xI (xI (xO (xO (xI p))))) => String "C"%char (string_of_ident p) - | xI (xI (xI (xO (xO (xI p))))) => String "D"%char (string_of_ident p) - | xO (xO (xO (xI (xO (xI p))))) => String "E"%char (string_of_ident p) - | xI (xO (xO (xI (xO (xI p))))) => String "F"%char (string_of_ident p) - | xO (xI (xO (xI (xO (xI p))))) => String "G"%char (string_of_ident p) - | xI (xI (xO (xI (xO (xI p))))) => String "H"%char (string_of_ident p) - | xO (xO (xI (xI (xO (xI p))))) => String "I"%char (string_of_ident p) - | xI (xO (xI (xI (xO (xI p))))) => String "J"%char (string_of_ident p) - | xO (xI (xI (xI (xO (xI p))))) => String "K"%char (string_of_ident p) - | xI (xI (xI (xI (xO (xI p))))) => String "L"%char (string_of_ident p) - | xO (xO (xO (xO (xI (xI p))))) => String "M"%char (string_of_ident p) - | xI (xO (xO (xO (xI (xI p))))) => String "N"%char (string_of_ident p) - | xO (xI (xO (xO (xI (xI p))))) => String "O"%char (string_of_ident p) - | xI (xI (xO (xO (xI (xI p))))) => String "P"%char (string_of_ident p) - | xO (xO (xI (xO (xI (xI p))))) => String "Q"%char (string_of_ident p) - | xI (xO (xI (xO (xI (xI p))))) => String "R"%char (string_of_ident p) - | xO (xI (xI (xO (xI (xI p))))) => String "S"%char (string_of_ident p) - | xI (xI (xI (xO (xI (xI p))))) => String "T"%char (string_of_ident p) - | xO (xO (xO (xI (xI (xI p))))) => String "U"%char (string_of_ident p) - | xI (xO (xO (xI (xI (xI p))))) => String "V"%char (string_of_ident p) - | xO (xI (xO (xI (xI (xI p))))) => String "W"%char (string_of_ident p) - | xI (xI (xO (xI (xI (xI p))))) => String "X"%char (string_of_ident p) - | xO (xO (xI (xI (xI (xI p))))) => String "Y"%char (string_of_ident p) - | xI (xO (xI (xI (xI (xI p))))) => String "Z"%char (string_of_ident p) - | xO (xI (xI (xI (xI (xI p))))) => String "_"%char (string_of_ident p) - | xI (xI (xI (xI (xI (xI p))))) => decode_8_bits string_of_ident p - | _ => EmptyString - end. - -Lemma string_of_ident_of_string: - forall s, string_of_ident (ident_of_string s) = s. -Proof. - induction s as [ | c s]; simpl. -- auto. -- rewrite <- IHs at 2. destruct c as [[] [] [] [] [] [] [] []]; reflexivity. -Qed. - -Corollary ident_of_string_injective: - forall s1 s2, ident_of_string s1 = ident_of_string s2 -> s1 = s2. -Proof. - intros. rewrite <- (string_of_ident_of_string s1), <- (string_of_ident_of_string s2). - congruence. -Qed. - (** ** Notations *) Module ClightNotations. diff --git a/export/Clightgen.ml b/export/Clightgen.ml deleted file mode 100644 index 44c76cc6..00000000 --- a/export/Clightgen.ml +++ /dev/null @@ -1,201 +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 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 = "Clight generator" - -(* clightgen-specific options *) - -let option_normalize = ref false - -(* From CompCert C AST to Clight *) - -let compile_c_ast 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 Clight *) - -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"; - compile_c_ast sourcename (parse_c_file sourcename ifile) 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 [options] -Recognized source files: - .c C source file - .i or .p C source file that should not be preprocessed -Processing options: - -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 Generate output in -|} ^ -prepro_help ^ -language_support_help ^ -{|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 - -dall Save all generated intermediate files in . -|} ^ - 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 "-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 diff --git a/export/Csyntaxdefs.v b/export/Csyntaxdefs.v new file mode 100644 index 00000000..84ce9f3a --- /dev/null +++ b/export/Csyntaxdefs.v @@ -0,0 +1,65 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Definitions used by .v files generated by clightgen -csyntax *) + +From Coq Require Import List. +From compcert Require Import Maps Errors AST Ctypes Csyntax. +From compcert Require Export Ctypesdefs. + +(** ** Constructor for programs and compilation units *) + +Definition wf_composites (types: list composite_definition) : Prop := + match build_composite_env types with OK _ => True | Error _ => False end. + +Definition build_composite_env' (types: list composite_definition) + (WF: wf_composites types) + : { ce | build_composite_env types = OK ce }. +Proof. + revert WF. unfold wf_composites. case (build_composite_env types); intros. +- exists c; reflexivity. +- contradiction. +Defined. + +Definition mkprogram (types: list composite_definition) + (defs: list (ident * globdef fundef type)) + (public: list ident) + (main: ident) + (WF: wf_composites types) : Csyntax.program := + let (ce, EQ) := build_composite_env' types WF in + {| prog_defs := defs; + prog_public := public; + prog_main := main; + prog_types := types; + prog_comp_env := ce; + prog_comp_env_eq := EQ |}. + +(** ** Notations *) + +Module CsyntaxNotations. + +(** A convenient notation [$ "ident"] to force evaluation of + [ident_of_string "ident"] *) + +Ltac ident_of_string s := + let x := constr:(ident_of_string s) in + let y := eval compute in x in + exact y. + +Notation "$ s" := (ltac:(ident_of_string s)) + (at level 1, only parsing) : csyntax_scope. + +End CsyntaxNotations. diff --git a/export/Ctypesdefs.v b/export/Ctypesdefs.v new file mode 100644 index 00000000..45695ebb --- /dev/null +++ b/export/Ctypesdefs.v @@ -0,0 +1,260 @@ +(* *********************************************************************) +(* *) +(* 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. *) +(* *) +(* *********************************************************************) + +(** Definitions used by the .v files generated by clightgen *) + +From Coq Require Import Ascii String List ZArith. +From compcert Require Import Maps Errors AST Ctypes. + +(** ** Short names for types *) + +Definition tvoid := Tvoid. +Definition tschar := Tint I8 Signed noattr. +Definition tuchar := Tint I8 Unsigned noattr. +Definition tshort := Tint I16 Signed noattr. +Definition tushort := Tint I16 Unsigned noattr. +Definition tint := Tint I32 Signed noattr. +Definition tuint := Tint I32 Unsigned noattr. +Definition tbool := Tint IBool Unsigned noattr. +Definition tlong := Tlong Signed noattr. +Definition tulong := Tlong Unsigned noattr. +Definition tfloat := Tfloat F32 noattr. +Definition tdouble := Tfloat F64 noattr. +Definition tptr (t: type) := Tpointer t noattr. +Definition tarray (t: type) (sz: Z) := Tarray t sz noattr. + +Definition volatile_attr := {| attr_volatile := true; attr_alignas := None |}. + +Definition tattr (a: attr) (ty: type) := + match ty with + | Tvoid => Tvoid + | Tint sz si _ => Tint sz si a + | Tlong si _ => Tlong si a + | Tfloat sz _ => Tfloat sz a + | Tpointer elt _ => Tpointer elt a + | Tarray elt sz _ => Tarray elt sz a + | Tfunction args res cc => Tfunction args res cc + | Tstruct id _ => Tstruct id a + | Tunion id _ => Tunion id a + end. + +Definition tvolatile (ty: type) := tattr volatile_attr ty. + +Definition talignas (n: N) (ty: type) := + tattr {| attr_volatile := false; attr_alignas := Some n |} ty. + +Definition tvolatile_alignas (n: N) (ty: type) := + tattr {| attr_volatile := true; attr_alignas := Some n |} ty. + +(** ** Encoding character strings as positive numbers *) + +(** The following encoding of character strings as positive numbers + must be kept consistent with the OCaml function [Camlcoq.pos_of_string]. *) + +Definition append_bit_pos (b: bool) (p: positive) : positive := + if b then xI p else xO p. + +Definition append_char_pos_default (c: ascii) (p: positive) : positive := + let '(Ascii b7 b6 b5 b4 b3 b2 b1 b0) := c in + xI (xI (xI (xI (xI (xI + (append_bit_pos b0 (append_bit_pos b1 + (append_bit_pos b2 (append_bit_pos b3 + (append_bit_pos b4 (append_bit_pos b5 + (append_bit_pos b6 (append_bit_pos b7 p))))))))))))). + +Definition append_char_pos (c: ascii) (p: positive) : positive := + match c with + | "0"%char => xO (xO (xO (xO (xO (xO p))))) + | "1"%char => xI (xO (xO (xO (xO (xO p))))) + | "2"%char => xO (xI (xO (xO (xO (xO p))))) + | "3"%char => xI (xI (xO (xO (xO (xO p))))) + | "4"%char => xO (xO (xI (xO (xO (xO p))))) + | "5"%char => xI (xO (xI (xO (xO (xO p))))) + | "6"%char => xO (xI (xI (xO (xO (xO p))))) + | "7"%char => xI (xI (xI (xO (xO (xO p))))) + | "8"%char => xO (xO (xO (xI (xO (xO p))))) + | "9"%char => xI (xO (xO (xI (xO (xO p))))) + | "a"%char => xO (xI (xO (xI (xO (xO p))))) + | "b"%char => xI (xI (xO (xI (xO (xO p))))) + | "c"%char => xO (xO (xI (xI (xO (xO p))))) + | "d"%char => xI (xO (xI (xI (xO (xO p))))) + | "e"%char => xO (xI (xI (xI (xO (xO p))))) + | "f"%char => xI (xI (xI (xI (xO (xO p))))) + | "g"%char => xO (xO (xO (xO (xI (xO p))))) + | "h"%char => xI (xO (xO (xO (xI (xO p))))) + | "i"%char => xO (xI (xO (xO (xI (xO p))))) + | "j"%char => xI (xI (xO (xO (xI (xO p))))) + | "k"%char => xO (xO (xI (xO (xI (xO p))))) + | "l"%char => xI (xO (xI (xO (xI (xO p))))) + | "m"%char => xO (xI (xI (xO (xI (xO p))))) + | "n"%char => xI (xI (xI (xO (xI (xO p))))) + | "o"%char => xO (xO (xO (xI (xI (xO p))))) + | "p"%char => xI (xO (xO (xI (xI (xO p))))) + | "q"%char => xO (xI (xO (xI (xI (xO p))))) + | "r"%char => xI (xI (xO (xI (xI (xO p))))) + | "s"%char => xO (xO (xI (xI (xI (xO p))))) + | "t"%char => xI (xO (xI (xI (xI (xO p))))) + | "u"%char => xO (xI (xI (xI (xI (xO p))))) + | "v"%char => xI (xI (xI (xI (xI (xO p))))) + | "w"%char => xO (xO (xO (xO (xO (xI p))))) + | "x"%char => xI (xO (xO (xO (xO (xI p))))) + | "y"%char => xO (xI (xO (xO (xO (xI p))))) + | "z"%char => xI (xI (xO (xO (xO (xI p))))) + | "A"%char => xO (xO (xI (xO (xO (xI p))))) + | "B"%char => xI (xO (xI (xO (xO (xI p))))) + | "C"%char => xO (xI (xI (xO (xO (xI p))))) + | "D"%char => xI (xI (xI (xO (xO (xI p))))) + | "E"%char => xO (xO (xO (xI (xO (xI p))))) + | "F"%char => xI (xO (xO (xI (xO (xI p))))) + | "G"%char => xO (xI (xO (xI (xO (xI p))))) + | "H"%char => xI (xI (xO (xI (xO (xI p))))) + | "I"%char => xO (xO (xI (xI (xO (xI p))))) + | "J"%char => xI (xO (xI (xI (xO (xI p))))) + | "K"%char => xO (xI (xI (xI (xO (xI p))))) + | "L"%char => xI (xI (xI (xI (xO (xI p))))) + | "M"%char => xO (xO (xO (xO (xI (xI p))))) + | "N"%char => xI (xO (xO (xO (xI (xI p))))) + | "O"%char => xO (xI (xO (xO (xI (xI p))))) + | "P"%char => xI (xI (xO (xO (xI (xI p))))) + | "Q"%char => xO (xO (xI (xO (xI (xI p))))) + | "R"%char => xI (xO (xI (xO (xI (xI p))))) + | "S"%char => xO (xI (xI (xO (xI (xI p))))) + | "T"%char => xI (xI (xI (xO (xI (xI p))))) + | "U"%char => xO (xO (xO (xI (xI (xI p))))) + | "V"%char => xI (xO (xO (xI (xI (xI p))))) + | "W"%char => xO (xI (xO (xI (xI (xI p))))) + | "X"%char => xI (xI (xO (xI (xI (xI p))))) + | "Y"%char => xO (xO (xI (xI (xI (xI p))))) + | "Z"%char => xI (xO (xI (xI (xI (xI p))))) + | "_"%char => xO (xI (xI (xI (xI (xI p))))) + | _ => append_char_pos_default c p + end. + +Fixpoint ident_of_string (s: string) : ident := + match s with + | EmptyString => xH + | String c s => append_char_pos c (ident_of_string s) + end. + +(** The inverse conversion, from encoded strings to strings *) + +Section DECODE_BITS. + +Variable rec: positive -> string. + +Fixpoint decode_n_bits (n: nat) (l: list bool) (p: positive) : string := + match n with + | O => + match l with + | b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: _ => + String (Ascii b7 b6 b5 b4 b3 b2 b1 b0) (rec p) + | _ => EmptyString + end + | S n => + match p with + | xO q => decode_n_bits n (false :: l) q + | xI q => decode_n_bits n (true :: l) q + | xH => EmptyString + end + end. + +Definition decode_8_bits := Eval compute in (decode_n_bits 8%nat nil). + +End DECODE_BITS. + +Fixpoint string_of_ident (p: positive) : string := + match p with + | xO (xO (xO (xO (xO (xO p))))) => String "0"%char (string_of_ident p) + | xI (xO (xO (xO (xO (xO p))))) => String "1"%char (string_of_ident p) + | xO (xI (xO (xO (xO (xO p))))) => String "2"%char (string_of_ident p) + | xI (xI (xO (xO (xO (xO p))))) => String "3"%char (string_of_ident p) + | xO (xO (xI (xO (xO (xO p))))) => String "4"%char (string_of_ident p) + | xI (xO (xI (xO (xO (xO p))))) => String "5"%char (string_of_ident p) + | xO (xI (xI (xO (xO (xO p))))) => String "6"%char (string_of_ident p) + | xI (xI (xI (xO (xO (xO p))))) => String "7"%char (string_of_ident p) + | xO (xO (xO (xI (xO (xO p))))) => String "8"%char (string_of_ident p) + | xI (xO (xO (xI (xO (xO p))))) => String "9"%char (string_of_ident p) + | xO (xI (xO (xI (xO (xO p))))) => String "a"%char (string_of_ident p) + | xI (xI (xO (xI (xO (xO p))))) => String "b"%char (string_of_ident p) + | xO (xO (xI (xI (xO (xO p))))) => String "c"%char (string_of_ident p) + | xI (xO (xI (xI (xO (xO p))))) => String "d"%char (string_of_ident p) + | xO (xI (xI (xI (xO (xO p))))) => String "e"%char (string_of_ident p) + | xI (xI (xI (xI (xO (xO p))))) => String "f"%char (string_of_ident p) + | xO (xO (xO (xO (xI (xO p))))) => String "g"%char (string_of_ident p) + | xI (xO (xO (xO (xI (xO p))))) => String "h"%char (string_of_ident p) + | xO (xI (xO (xO (xI (xO p))))) => String "i"%char (string_of_ident p) + | xI (xI (xO (xO (xI (xO p))))) => String "j"%char (string_of_ident p) + | xO (xO (xI (xO (xI (xO p))))) => String "k"%char (string_of_ident p) + | xI (xO (xI (xO (xI (xO p))))) => String "l"%char (string_of_ident p) + | xO (xI (xI (xO (xI (xO p))))) => String "m"%char (string_of_ident p) + | xI (xI (xI (xO (xI (xO p))))) => String "n"%char (string_of_ident p) + | xO (xO (xO (xI (xI (xO p))))) => String "o"%char (string_of_ident p) + | xI (xO (xO (xI (xI (xO p))))) => String "p"%char (string_of_ident p) + | xO (xI (xO (xI (xI (xO p))))) => String "q"%char (string_of_ident p) + | xI (xI (xO (xI (xI (xO p))))) => String "r"%char (string_of_ident p) + | xO (xO (xI (xI (xI (xO p))))) => String "s"%char (string_of_ident p) + | xI (xO (xI (xI (xI (xO p))))) => String "t"%char (string_of_ident p) + | xO (xI (xI (xI (xI (xO p))))) => String "u"%char (string_of_ident p) + | xI (xI (xI (xI (xI (xO p))))) => String "v"%char (string_of_ident p) + | xO (xO (xO (xO (xO (xI p))))) => String "w"%char (string_of_ident p) + | xI (xO (xO (xO (xO (xI p))))) => String "x"%char (string_of_ident p) + | xO (xI (xO (xO (xO (xI p))))) => String "y"%char (string_of_ident p) + | xI (xI (xO (xO (xO (xI p))))) => String "z"%char (string_of_ident p) + | xO (xO (xI (xO (xO (xI p))))) => String "A"%char (string_of_ident p) + | xI (xO (xI (xO (xO (xI p))))) => String "B"%char (string_of_ident p) + | xO (xI (xI (xO (xO (xI p))))) => String "C"%char (string_of_ident p) + | xI (xI (xI (xO (xO (xI p))))) => String "D"%char (string_of_ident p) + | xO (xO (xO (xI (xO (xI p))))) => String "E"%char (string_of_ident p) + | xI (xO (xO (xI (xO (xI p))))) => String "F"%char (string_of_ident p) + | xO (xI (xO (xI (xO (xI p))))) => String "G"%char (string_of_ident p) + | xI (xI (xO (xI (xO (xI p))))) => String "H"%char (string_of_ident p) + | xO (xO (xI (xI (xO (xI p))))) => String "I"%char (string_of_ident p) + | xI (xO (xI (xI (xO (xI p))))) => String "J"%char (string_of_ident p) + | xO (xI (xI (xI (xO (xI p))))) => String "K"%char (string_of_ident p) + | xI (xI (xI (xI (xO (xI p))))) => String "L"%char (string_of_ident p) + | xO (xO (xO (xO (xI (xI p))))) => String "M"%char (string_of_ident p) + | xI (xO (xO (xO (xI (xI p))))) => String "N"%char (string_of_ident p) + | xO (xI (xO (xO (xI (xI p))))) => String "O"%char (string_of_ident p) + | xI (xI (xO (xO (xI (xI p))))) => String "P"%char (string_of_ident p) + | xO (xO (xI (xO (xI (xI p))))) => String "Q"%char (string_of_ident p) + | xI (xO (xI (xO (xI (xI p))))) => String "R"%char (string_of_ident p) + | xO (xI (xI (xO (xI (xI p))))) => String "S"%char (string_of_ident p) + | xI (xI (xI (xO (xI (xI p))))) => String "T"%char (string_of_ident p) + | xO (xO (xO (xI (xI (xI p))))) => String "U"%char (string_of_ident p) + | xI (xO (xO (xI (xI (xI p))))) => String "V"%char (string_of_ident p) + | xO (xI (xO (xI (xI (xI p))))) => String "W"%char (string_of_ident p) + | xI (xI (xO (xI (xI (xI p))))) => String "X"%char (string_of_ident p) + | xO (xO (xI (xI (xI (xI p))))) => String "Y"%char (string_of_ident p) + | xI (xO (xI (xI (xI (xI p))))) => String "Z"%char (string_of_ident p) + | xO (xI (xI (xI (xI (xI p))))) => String "_"%char (string_of_ident p) + | xI (xI (xI (xI (xI (xI p))))) => decode_8_bits string_of_ident p + | _ => EmptyString + end. + +Lemma string_of_ident_of_string: + forall s, string_of_ident (ident_of_string s) = s. +Proof. + induction s as [ | c s]; simpl. +- auto. +- rewrite <- IHs at 2. destruct c as [[] [] [] [] [] [] [] []]; reflexivity. +Qed. + +Corollary ident_of_string_injective: + forall s1 s2, ident_of_string s1 = ident_of_string s2 -> s1 = s2. +Proof. + intros. rewrite <- (string_of_ident_of_string s1), <- (string_of_ident_of_string s2). + congruence. +Qed. diff --git a/export/ExportBase.ml b/export/ExportBase.ml index b7d0170d..4b93d8a9 100644 --- a/export/ExportBase.ml +++ b/export/ExportBase.ml @@ -17,6 +17,7 @@ open Format open Camlcoq open AST +open Values (* Options, lists, pairs *) @@ -239,9 +240,19 @@ let print_variable print_info p (id, v) = fprintf p " gvar_volatile := %B@ " v.gvar_volatile; fprintf p "|}.@ @ " -(* Information about this run of clightgen *) +(* Values *) -let print_clightgen_info ~sourcefile ?normalized p = +let val_ p = function + | Vundef -> fprintf p "Vundef" + | Vint i -> fprintf p "(Vint %a)" coqint i + | Vlong l -> fprintf p "(Vlong %a)" coqint64 l + | Vfloat f -> fprintf p "(Vfloat %a)" coqfloat f + | Vsingle s -> fprintf p "(Vsingle %a)" coqsingle s + | Vptr(b, o) -> fprintf p "(Vptr %a %a)" positive b coqptrofs o + +(* Information about this run of clightgen or csyntaxgen *) + +let print_gen_info ~sourcefile ?normalized p = fprintf p "@[Module Info."; fprintf p "@ Definition version := %S." Version.version; fprintf p "@ Definition build_number := %S." Version.buildnr; diff --git a/export/ExportClight.ml b/export/ExportClight.ml index 421db5ed..e3b00986 100644 --- a/export/ExportClight.ml +++ b/export/ExportClight.ml @@ -233,7 +233,7 @@ let print_program p prog sourcefile normalized = name_program prog; fprintf p "@["; fprintf p "%s" prologue; - print_clightgen_info ~sourcefile ~normalized p; + print_gen_info ~sourcefile ~normalized p; define_idents p; List.iter (print_globdef p) prog.Ctypes.prog_defs; fprintf p "Definition composites : list composite_definition :=@ "; diff --git a/export/ExportCsyntax.ml b/export/ExportCsyntax.ml new file mode 100644 index 00000000..1d91cba5 --- /dev/null +++ b/export/ExportCsyntax.ml @@ -0,0 +1,209 @@ +(* *********************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Bart Jacobs, KU Leuven *) +(* 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. *) +(* *) +(* The contributions by Bart Jacobs are reused and adapted *) +(* under the terms of a Contributor License Agreement. *) +(* *) +(* *********************************************************************) + +(** Export C syntax as a Coq file *) + +open Format +open Camlcoq +open AST +open! Ctypes +open Cop +open Csyntax +open ExportBase +open ExportCtypes + +(* Expressions *) + +let name_unop = function + | Onotbool -> "Onotbool" + | Onotint -> "Onotint" + | Oneg -> "Oneg" + | Oabsfloat -> "Oabsfloat" + +let name_binop = function + | Oadd -> "Oadd" + | Osub -> "Osub" + | Omul -> "Omul" + | Odiv -> "Odiv" + | Omod -> "Omod" + | Oand -> "Oand" + | Oor -> "Oor" + | Oxor -> "Oxor" + | Oshl -> "Oshl" + | Oshr -> "Oshr" + | Oeq -> "Oeq" + | Cop.One -> "One" + | Olt -> "Olt" + | Ogt -> "Ogt" + | Ole -> "Ole" + | Oge -> "Oge" + +let name_incr_or_decr = function + | Incr -> "Incr" + | Decr -> "Decr" + +let rec expr p = function + | Eval(v, t) -> + fprintf p "(Eval %a %a)" val_ v typ t + | Evar(id, t) -> + fprintf p "(Evar %a %a)" ident id typ t + | Efield(a1, f, t) -> + fprintf p "@[(Efield@ %a@ %a@ %a)@]" expr a1 ident f typ t + | Evalof(l, t) -> + fprintf p "@[(Evalof@ %a@ %a)@]" expr l typ t + | Ederef(a1, t) -> + fprintf p "@[(Ederef@ %a@ %a)@]" expr a1 typ t + | Eaddrof(a1, t) -> + fprintf p "@[(Eaddrof@ %a@ %a)@]" expr a1 typ t + | Eunop(op, a1, t) -> + fprintf p "@[(Eunop %s@ %a@ %a)@]" + (name_unop op) expr a1 typ t + | Ebinop(op, a1, a2, t) -> + fprintf p "@[(Ebinop %s@ %a@ %a@ %a)@]" + (name_binop op) expr a1 expr a2 typ t + | Ecast(a1, t) -> + fprintf p "@[(Ecast@ %a@ %a)@]" expr a1 typ t + | Eseqand(a1, a2, t) -> + fprintf p "@[(Eseqand@ %a@ %a@ %a)@]" expr a1 expr a2 typ t + | Eseqor(a1, a2, t) -> + fprintf p "@[(Eseqor@ %a@ %a@ %a)@]" expr a1 expr a2 typ t + | Econdition(a1, a2, a3, t) -> + fprintf p "@[(Econdition@ %a@ %a@ %a@ %a)@]" expr a1 expr a2 expr a3 typ t + | Esizeof(t1, t) -> + fprintf p "(Esizeof %a %a)" typ t1 typ t + | Ealignof(t1, t) -> + fprintf p "(Ealignof %a %a)" typ t1 typ t + | Eassign(l, r, t) -> + fprintf p "@[(Eassign@ %a@ %a@ %a)@]" expr l expr r typ t + | Eassignop(op, l, r, t', t) -> + fprintf p "@[(Eassignop@ %s@ %a@ %a@ %a %a)@]" (name_binop op) expr l expr r typ t' typ t + | Epostincr(id, l, t) -> + fprintf p "@[(Epostincr@ %s@ %a@ %a)@]" (name_incr_or_decr id) expr l typ t + | Ecomma(a1, a2, t) -> + fprintf p "@[(Ecomma@ %a@ %a@ %a)@]" expr a1 expr a2 typ t + | Ecall(r1, rargs, t) -> + fprintf p "@[(Ecall@ %a@ %a@ %a)@]" expr r1 exprlist rargs typ t + | Ebuiltin(ef, tyargs, rargs, t) -> + fprintf p "@[(Ebuiltin@ %a@ %a@ %a@ %a)@]" external_function ef typlist tyargs exprlist rargs typ t + | Eloc(b, o, bf, t) -> + fprintf p "@[(Eloc@ %a@ %a@ %a@ %a)@]" positive b coqptrofs o bitfield bf typ t + | Eparen(r, t', t) -> + fprintf p "@[(Eparen@ %a@ %a@ %a)@]" expr r typ t' typ t +and exprlist p = function + | Enil -> + fprintf p "Enil" + | Econs(r1, rl) -> + fprintf p "@[(Econs@ %a@ %a)@]" expr r1 exprlist rl + +(* Statements *) + +let rec statement p = function + | Sskip -> + fprintf p "Sskip" + | Sdo(e) -> + fprintf p "@[(Sdo %a)@]" expr e + | Ssequence(s1, s2) -> + fprintf p "@[(Ssequence@ %a@ %a)@]" statement s1 statement s2 + | Sifthenelse(e, s1, s2) -> + fprintf p "@[(Sifthenelse %a@ %a@ %a)@]" expr e statement s1 statement s2 + | Swhile(e, s) -> + fprintf p "@[(Swhile@ %a@ %a)@]" expr e statement s + | Sdowhile(e, s) -> + fprintf p "@[(Sdowhile@ %a@ %a)@]" expr e statement s + | Sfor(s1, e, s2, s3) -> + fprintf p "@[(Sfor@ %a@ %a@ %a@ %a)@]" statement s1 expr e statement s2 statement s3 + | Sbreak -> + fprintf p "Sbreak" + | Scontinue -> + fprintf p "Scontinue" + | Sreturn e -> + fprintf p "@[(Sreturn %a)@]" (print_option expr) e + | Sswitch(e, cases) -> + fprintf p "@[(Sswitch %a@ %a)@]" expr e labeled_statements cases + | Slabel(lbl, s1) -> + fprintf p "@[(Slabel %a@ %a)@]" ident lbl statement s1 + | Sgoto lbl -> + fprintf p "(Sgoto %a)" ident lbl + +and labeled_statements p = function + | LSnil -> + (fprintf p "LSnil") + | LScons(lbl, s, ls) -> + fprintf p "@[(LScons %a@ %a@ %a)@]" + (print_option coqZ) lbl statement s labeled_statements ls + +(* Global definitions *) + +let print_function p (id, f) = + fprintf p "Definition f%s := {|@ " (sanitize (extern_atom id)); + fprintf p " fn_return := %a;@ " typ f.fn_return; + fprintf p " fn_callconv := %a;@ " callconv f.fn_callconv; + fprintf p " fn_params := %a;@ " (print_list (print_pair ident typ)) f.fn_params; + fprintf p " fn_vars := %a;@ " (print_list (print_pair ident typ)) f.fn_vars; + fprintf p " fn_body :=@ "; + statement p f.fn_body; + fprintf p "@ |}.@ @ " + +let print_globdef p (id, gd) = + match gd with + | Gfun(Ctypes.Internal f) -> print_function p (id, f) + | Gfun(Ctypes.External _) -> () + | Gvar v -> print_variable typ p (id, v) + +let print_ident_globdef p = function + | (id, Gfun(Ctypes.Internal f)) -> + fprintf p "(%a, Gfun(Internal f%s))" ident id (sanitize (extern_atom id)) + | (id, Gfun(Ctypes.External(ef, targs, tres, cc))) -> + fprintf p "@[(%a,@ @[Gfun(External %a@ %a@ %a@ %a))@]@]" + ident id external_function ef typlist targs typ tres callconv cc + | (id, Gvar v) -> + fprintf p "(%a, Gvar v%s)" ident id (sanitize (extern_atom id)) + +(* The prologue *) + +let prologue = "\ +From Coq Require Import String List ZArith.\n\ +From compcert Require Import Coqlib Integers Floats Values AST Ctypes Cop Csyntax Csyntaxdefs.\n\ +Import Csyntaxdefs.CsyntaxNotations.\n\ +Local Open Scope Z_scope.\n\ +Local Open Scope string_scope.\n\ +Local Open Scope csyntax_scope.\n" + +(* All together *) + +let print_program p prog sourcefile = + fprintf p "@["; + fprintf p "%s" prologue; + print_gen_info ~sourcefile p; + define_idents p; + List.iter (print_globdef p) prog.Ctypes.prog_defs; + fprintf p "Definition composites : list composite_definition :=@ "; + print_list print_composite_definition p prog.prog_types; + fprintf p ".@ @ "; + fprintf p "Definition global_definitions : list (ident * globdef fundef type) :=@ "; + print_list print_ident_globdef p prog.Ctypes.prog_defs; + fprintf p ".@ @ "; + fprintf p "Definition public_idents : list ident :=@ "; + print_list ident p prog.Ctypes.prog_public; + fprintf p ".@ @ "; + fprintf p "Definition prog : Csyntax.program := @ "; + fprintf p " mkprogram composites global_definitions public_idents %a Logic.I.@ @ " + ident prog.Ctypes.prog_main; + fprintf p "@]@." diff --git a/export/ExportCtypes.ml b/export/ExportCtypes.ml index 428a1459..d0a7f28a 100644 --- a/export/ExportCtypes.ml +++ b/export/ExportCtypes.ml @@ -98,6 +98,16 @@ and typlist p = function | Tcons(t, tl) -> fprintf p "@[(Tcons@ %a@ %a)@]" typ t typlist tl +(* Access modes for members of structs or unions *) + +let bitfield p = function + | Full -> + fprintf p "Full" + | Bits(sz, sg, pos, width) -> + fprintf p "@[(Bits@ %a@ %a@ %a@ %a)@]" + intsize sz signedness sg + coqZ pos coqZ width + (* Composite definitions *) let print_member p = function @@ -119,4 +129,3 @@ let print_composite_definition p (Composite(id, su, m, a)) = (match su with Struct -> "Struct" | Union -> "Union") (print_list print_member) m attribute a - 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 [options] +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 Generate output in +|} ^ +prepro_help ^ +language_support_help ^ +{|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 + -dall Save all generated intermediate files in . +|} ^ + 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 -- cgit