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 --- exportclight/Clightdefs.v | 53 +++++ exportclight/Clightgen.ml | 282 ++++++++++++++++++++++++ exportclight/ExportClight.ml | 503 +++++++++++++++++++++++++++++++++++++++++++ exportclight/README | 34 +++ 4 files changed, 872 insertions(+) create mode 100644 exportclight/Clightdefs.v create mode 100644 exportclight/Clightgen.ml create mode 100644 exportclight/ExportClight.ml create mode 100644 exportclight/README (limited to 'exportclight') diff --git a/exportclight/Clightdefs.v b/exportclight/Clightdefs.v new file mode 100644 index 0000000..4c3c942 --- /dev/null +++ b/exportclight/Clightdefs.v @@ -0,0 +1,53 @@ +(* *********************************************************************) +(* *) +(* 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 General Public License as published by *) +(* the Free Software Foundation, either version 2 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. *) +(* *) +(* *********************************************************************) + +(** All imports and definitions used by .v Clight files generated by clightgen *) + +Require Export List. +Require Export ZArith. +Require Export Integers. +Require Export Floats. +Require Export AST. +Require Export Ctypes. +Require Export Cop. +Require Export Clight. + +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 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 |}. + +Definition tvolatile (ty: type) := + match ty with + | Tvoid => Tvoid + | Tint sz si a => Tint sz si volatile_attr + | Tfloat sz a => Tfloat sz volatile_attr + | Tpointer elt a => Tpointer elt volatile_attr + | Tarray elt sz a => Tarray elt sz volatile_attr + | Tfunction args res => Tfunction args res + | Tstruct id fld a => Tstruct id fld volatile_attr + | Tunion id fld a => Tunion id fld volatile_attr + | Tcomp_ptr id a => Tcomp_ptr id volatile_attr + end. diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml new file mode 100644 index 0000000..1805573 --- /dev/null +++ b/exportclight/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/exportclight/ExportClight.ml b/exportclight/ExportClight.ml new file mode 100644 index 0000000..452693c --- /dev/null +++ b/exportclight/ExportClight.ml @@ -0,0 +1,503 @@ +(* *********************************************************************) +(* *) +(* 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 General Public License as published by *) +(* the Free Software Foundation, either version 2 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. *) +(* *) +(* *********************************************************************) + +(** Export Clight as a Coq file *) + +open Format +open Camlcoq +open Datatypes +open Values +open AST +open Ctypes +open Cop +open Clight + +(* Options, lists, pairs *) + +let print_option fn p = function + | None -> fprintf p "None" + | Some x -> fprintf p "(Some %a)" fn x + +let print_pair fn1 fn2 p (x1, x2) = + fprintf p "@[(%a,@ %a)@]" fn1 x1 fn2 x2 + +let print_list fn p l = + match l with + | [] -> + fprintf p "nil" + | hd :: tl -> + fprintf p "@[("; + let rec plist = function + | [] -> fprintf p "nil" + | hd :: tl -> fprintf p "%a ::@ " fn hd; plist tl + in plist l; + fprintf p ")@]" + +(* Identifiers *) + +exception Not_an_identifier + +let sanitize s = + let s' = String.create (String.length s) in + for i = 0 to String.length s - 1 do + s'.[i] <- + match s.[i] with + | 'A'..'Z' | 'a'..'z' | '0'..'9' | '_' as c -> c + | ' ' | '$' -> '_' + | _ -> raise Not_an_identifier + done; + s' + +let ident p id = + try + let s = Hashtbl.find string_of_atom id in + fprintf p "_%s" (sanitize s) + with Not_found | Not_an_identifier -> + fprintf p "%ld%%positive" (camlint_of_positive id) + +let define_idents p = + Hashtbl.iter + (fun id name -> + try + fprintf p "Definition _%s : ident := %ld%%positive.@ " + (sanitize name) (camlint_of_positive id) + with Not_an_identifier -> + ()) + string_of_atom; + fprintf p "@ " + +(* Numbers *) + +let coqint p n = + let n = camlint_of_coqint n in + if n >= 0l + then fprintf p "(Int.repr %ld)" n + else fprintf p "(Int.repr (%ld))" n + +let coqfloat p n = + let n = camlint64_of_coqint(Floats.Float.bits_of_double n) in + if n >= 0L + then fprintf p "(Float.double_of_bits (Int64.repr %Ld))" n + else fprintf p "(Float.double_of_bits (Int64.repr (%Ld)))" n + +(* Types *) + +let use_struct_names = ref true + +let rec typ p t = + let a = attr_of_type t in + if a (*.attr_volatile*) + then fprintf p "(tvolatile %a)" rtyp t + else rtyp p t + +and rtyp p = function + | Tvoid -> fprintf p "tvoid" + | Tint(sz, sg, _) -> + fprintf p "%s" ( + match sz, sg with + | I8, Signed -> "tschar" + | I8, Unsigned -> "tuchar" + | I16, Signed -> "tshort" + | I16, Unsigned -> "tushort" + | I32, Signed -> "tint" + | I32, Unsigned -> "tuint" + | IBool, _ -> "tbool") + | Tfloat(sz, _) -> + fprintf p "%s" ( + match sz with + | F32 -> "tfloat" + | F64 -> "tdouble") + | Tpointer(t, _) -> + fprintf p "(tptr %a)" typ t + | Tarray(t, sz, _) -> + fprintf p "(tarray %a %ld)" typ t (camlint_of_z sz) + | Tfunction(targs, tres) -> + fprintf p "@[(Tfunction@ %a@ %a)@]" typlist targs typ tres + | Tstruct(id, flds, _) -> + if !use_struct_names + then fprintf p "t%a" ident id + else fprintf p "@[(Tstruct %a@ %a@ noattr)@]" ident id fieldlist flds + | Tunion(id, flds, _) -> + if !use_struct_names + then fprintf p "t%a" ident id + else fprintf p "@[(Tunion %a@ %a@ noattr)@]" ident id fieldlist flds + | Tcomp_ptr(id, _) -> + fprintf p "(Tcomp_ptr %a noattr)" ident id + +and typlist p = function + | Tnil -> + fprintf p "Tnil" + | Tcons(t, tl) -> + fprintf p "@[(Tcons@ %a@ %a)@]" typ t typlist tl + +and fieldlist p = function + | Fnil -> + fprintf p "Fnil" + | Fcons(id, t, fl) -> + fprintf p "@[(Fcons %a@ %a@ %a)@]" ident id typ t fieldlist fl + +(* External functions *) + +let asttype p t = + fprintf p "%s" (match t with AST.Tint -> "AST.Tint" | AST.Tfloat -> "AST.Tfloat") + +let name_of_chunk = function + | Mint8signed -> "Mint8signed" + | Mint8unsigned -> "Mint8unsigned" + | Mint16signed -> "Mint16signed" + | Mint16unsigned -> "Mint16unsigned" + | Mint32 -> "Mint32" + | Mfloat32 -> "Mfloat32" + | Mfloat64 -> "Mfloat64" + | Mfloat64al32 -> "Mfloat64al32" + +let signatur p sg = + fprintf p "@[(mksignature@ %a@ %a)@]" (print_list asttype) sg.sig_args (print_option asttype) sg.sig_res + +let assertions = ref ([]: (ident * typ list) list) + +let external_function p = function + | EF_external(name, sg) -> + fprintf p "@[(EF_external %a@ %a)@]" ident name signatur sg + | EF_builtin(name, sg) -> + fprintf p "@[(EF_builtin %a@ %a)@]" ident name signatur sg + | EF_vload chunk -> + fprintf p "(EF_vload %s)" (name_of_chunk chunk) + | EF_vstore chunk -> + fprintf p "(EF_vstore %s)" (name_of_chunk chunk) + | EF_vload_global(chunk, id, ofs) -> + fprintf p "(EF_vload_global %s %a %a)" (name_of_chunk chunk) ident id coqint ofs + | EF_vstore_global(chunk, id, ofs) -> + fprintf p "(EF_vstore_global %s %a %a)" (name_of_chunk chunk) ident id coqint ofs + | EF_malloc -> fprintf p "EF_malloc" + | EF_free -> fprintf p "EF_free" + | EF_memcpy(sz, al) -> + fprintf p "(EF_memcpy %ld %ld)" (camlint_of_z sz) (camlint_of_z al) + | EF_annot(text, targs) -> + assertions := (text, targs) :: !assertions; + fprintf p "(EF_annot %ld%%positive %a)" (camlint_of_positive text) (print_list asttype) targs + | EF_annot_val(text, targ) -> + assertions := (text, [targ]) :: !assertions; + fprintf p "(EF_annot_val %ld%%positive %a)" (camlint_of_positive text) asttype targ + | EF_inline_asm(text) -> + fprintf p "(EF_inline_asm %ld%%positive)" (camlint_of_positive text) + +(* Expressions *) + +let name_unop = function + | Onotbool -> "Onotbool" + | Onotint -> "Onotint" + | Oneg -> "Oneg" + +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" + | One -> "One" + | Olt -> "Olt" + | Ogt -> "Ogt" + | Ole -> "Ole" + | Oge -> "Oge" + +let rec expr p = function + | Evar(id, t) -> + fprintf p "(Evar %a %a)" ident id typ t + | Etempvar(id, t) -> + fprintf p "(Etempvar %a %a)" ident id typ t + | Ederef(a1, t) -> + fprintf p "@[(Ederef@ %a@ %a)@]" expr a1 typ t + | Efield(a1, f, t) -> + fprintf p "@[(Efield@ %a@ %a@ %a)@]" expr a1 ident f typ t + | Econst_int(n, t) -> + fprintf p "(Econst_int %a %a)" coqint n typ t + | Econst_float(n, t) -> + fprintf p "(Econst_float %a %a)" coqfloat n typ t + | Eunop(op, a1, t) -> + fprintf p "@[(Eunop %s@ %a@ %a)@]" + (name_unop op) expr a1 typ t + | Eaddrof(a1, t) -> + fprintf p "@[(Eaddrof@ %a@ %a)@]" 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 + +(* Statements *) + +let rec stmt p = function + | Sskip -> + fprintf p "Sskip" + | Sassign(e1, e2) -> + fprintf p "@[(Sassign@ %a@ %a)@]" expr e1 expr e2 + | Sset(id, e2) -> + fprintf p "@[(Sset %a@ %a)@]" ident id expr e2 + | Scall(optid, e1, el) -> + fprintf p "@[(Scall %a@ %a@ %a)@]" + (print_option ident) optid expr e1 (print_list expr) el + | Sbuiltin(optid, ef, tyl, el) -> + fprintf p "@[(Sbuiltin %a@ %a@ %a@ %a)@]" + (print_option ident) optid + external_function ef + typlist tyl + (print_list expr) el + | Ssequence(Sskip, s2) -> + stmt p s2 + | Ssequence(s1, Sskip) -> + stmt p s1 + | Ssequence(s1, s2) -> + fprintf p "@[(Ssequence@ %a@ %a)@]" stmt s1 stmt s2 + | Sifthenelse(e, s1, s2) -> + fprintf p "@[(Sifthenelse %a@ %a@ %a)@]" expr e stmt s1 stmt s2 + | Sloop (Ssequence (Sifthenelse(e, Sskip, Sbreak), s), Sskip) -> + fprintf p "@[(Swhile@ %a@ %a)@]" expr e stmt s + | Sloop (Ssequence (Ssequence(Sskip, Sifthenelse(e, Sskip, Sbreak)), s), Sskip) -> + fprintf p "@[(Swhile@ %a@ %a)@]" expr e stmt s + | Sloop(s1, s2) -> + fprintf p "@[(Sloop@ %a@ %a)@]" stmt s1 stmt s2 + | Sbreak -> + fprintf p "Sbreak" + | Scontinue -> + fprintf p "Scontinue" + | Sswitch(e, cases) -> + fprintf p "@[(Sswitch %a@ %a)@]" expr e lblstmts cases + | Sreturn e -> + fprintf p "@[(Sreturn %a)@]" (print_option expr) e + | Slabel(lbl, s1) -> + fprintf p "@[(Slabel %a@ %a)@]" ident lbl stmt s1 + | Sgoto lbl -> + fprintf p "(Sgoto %a)" ident lbl + +and lblstmts p = function + | LSdefault s -> + fprintf p "@[(LSdefault@ %a)@]" stmt s + | LScase(lbl, s, ls) -> + fprintf p "@[(LScase %a@ %a@ %a)@]" coqint lbl stmt s lblstmts ls + +let print_function p (id, f) = + fprintf p "Definition f_%s := {|@ " (extern_atom id); + fprintf p " fn_return := %a;@ " typ f.fn_return; + 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_temps := %a;@ " (print_list (print_pair ident typ)) f.fn_temps; + fprintf p " fn_body :=@ "; + stmt p f.fn_body; + fprintf p "@ |}.@ @ " + +let init_data p = function + | Init_int8 n -> fprintf p "Init_int8 %a" coqint n + | Init_int16 n -> fprintf p "Init_int16 %a" coqint n + | Init_int32 n -> fprintf p "Init_int32 %a" coqint n + | Init_float32 n -> fprintf p "Init_float32 %a" coqfloat n + | Init_float64 n -> fprintf p "Init_float64 %a" coqfloat n + | Init_space n -> fprintf p "Init_space %ld" (camlint_of_z n) + | Init_addrof(id,ofs) -> fprintf p "Init_addrof %a %a" ident id coqint ofs + +let print_variable p (id, v) = + fprintf p "Definition v_%s := {|@ " (extern_atom id); + fprintf p " gvar_info := %a;@ " typ v.gvar_info; + fprintf p " gvar_init := %a;@ " (print_list init_data) v.gvar_init; + fprintf p " gvar_readonly := %B;@ " v.gvar_readonly; + fprintf p " gvar_volatile := %B@ " v.gvar_volatile; + fprintf p "|}.@ @ " + +let print_globdef p (id, gd) = + match gd with + | Gfun(Internal f) -> print_function p (id, f) + | Gfun(External _) -> () + | Gvar v -> print_variable p (id, v) + +let print_ident_globdef p = function + | (id, Gfun(Internal f)) -> + fprintf p "(%a, Gfun(Internal f_%s))" ident id (extern_atom id) + | (id, Gfun(External(ef, targs, tres))) -> + fprintf p "@[(%a,@ @[Gfun(External %a@ %a@ %a))@]@]" + ident id external_function ef typlist targs typ tres + | (id, Gvar v) -> + fprintf p "(%a, Gvar v_%s)" ident id (extern_atom id) + +(* Collecting the names and fields of structs and unions *) + +module TypeSet = Set.Make(struct + type t = coq_type + let compare = Pervasives.compare +end) + +let struct_unions = ref TypeSet.empty + +let register_struct_union ty = + struct_unions := TypeSet.add ty !struct_unions + +let rec collect_type = function + | Tvoid -> () + | Tint _ -> () + | Tfloat _ -> () + | Tpointer(t, _) -> collect_type t + | Tarray(t, _, _) -> collect_type t + | Tfunction(args, res) -> collect_type_list args; collect_type res + | Tstruct(id, fld, _) -> + register_struct_union (Tstruct(id, fld, noattr)) (*; collect_fields fld*) + | Tunion(id, fld, _) -> + register_struct_union (Tunion(id, fld, noattr)) (*; collect_fields fld*) + | Tcomp_ptr _ -> () + +and collect_type_list = function + | Tnil -> () + | Tcons(hd, tl) -> collect_type hd; collect_type_list tl + +and collect_fields = function + | Fnil -> () + | Fcons(id, hd, tl) -> collect_type hd; collect_fields tl + +let rec collect_expr e = + collect_type (typeof e); + match e with + | Econst_int _ -> () + | Econst_float _ -> () + | Evar _ -> () + | Etempvar _ -> () + | Ederef(r, _) -> collect_expr r + | Efield(l, _, _) -> collect_expr l + | Eaddrof(l, _) -> collect_expr l + | Eunop(_, r, _) -> collect_expr r + | Ebinop(_, r1, r2, _) -> collect_expr r1; collect_expr r2 + | Ecast(r, _) -> collect_expr r + +let rec collect_exprlist = function + | [] -> () + | r1 :: rl -> collect_expr r1; collect_exprlist rl + +let rec collect_stmt = function + | Sskip -> () + | Sassign(e1, e2) -> collect_expr e1; collect_expr e2 + | Sset(id, e2) -> collect_expr e2 + | Scall(optid, e1, el) -> collect_expr e1; collect_exprlist el + | Sbuiltin(optid, ef, tyl, el) -> collect_exprlist el + | Ssequence(s1, s2) -> collect_stmt s1; collect_stmt s2 + | Sifthenelse(e, s1, s2) -> collect_expr e; collect_stmt s1; collect_stmt s2 + | Sloop(s1, s2) -> collect_stmt s1; collect_stmt s2 + | Sbreak -> () + | Scontinue -> () + | Sswitch(e, cases) -> collect_expr e; collect_cases cases + | Sreturn None -> () + | Sreturn (Some e) -> collect_expr e + | Slabel(lbl, s) -> collect_stmt s + | Sgoto lbl -> () + +and collect_cases = function + | LSdefault s -> collect_stmt s + | LScase(lbl, s, rem) -> collect_stmt s; collect_cases rem + +let collect_function f = + collect_type f.fn_return; + List.iter (fun (id, ty) -> collect_type ty) f.fn_params; + List.iter (fun (id, ty) -> collect_type ty) f.fn_vars; + List.iter (fun (id, ty) -> collect_type ty) f.fn_temps; + collect_stmt f.fn_body + +let collect_globdef (id, gd) = + match gd with + | Gfun(External(_, args, res)) -> collect_type_list args; collect_type res + | Gfun(Internal f) -> collect_function f + | Gvar v -> collect_type v.gvar_info + +let define_struct p ty = + match ty with + | Tstruct(id, _, _) | Tunion(id, _, _) -> + fprintf p "@[Definition t%a :=@ %a.@]@ " ident id typ ty + | _ -> assert false + +let define_structs p prog = + struct_unions := TypeSet.empty; + List.iter collect_globdef prog.prog_defs; + use_struct_names := false; + TypeSet.iter (define_struct p) !struct_unions; + use_struct_names := true; + fprintf p "@ " + +(* Assertion processing *) + +let re_annot_param = Str.regexp "%%\\|%[1-9][0-9]*" + +type fragment = Text of string | Param of int + +let print_assertion p (txt, targs) = + let frags = + List.map + (function + | Str.Text s -> Text s + | Str.Delim "%%" -> Text "%" + | Str.Delim s -> Param(int_of_string(String.sub s 1 (String.length s - 1)))) + (Str.full_split re_annot_param (extern_atom txt)) in + let max_param = ref 0 in + List.iter + (function + | Text _ -> () + | Param n -> max_param := max n !max_param) + frags; + fprintf p " | %ld%%positive, " (camlint_of_positive txt); + for i = 1 to !max_param do + fprintf p "_x%d :: " i + done; + fprintf p "nil =>@ "; + fprintf p " "; + List.iter + (function + | Text s -> fprintf p "%s" s + | Param n -> fprintf p "_x%d" n) + frags; + fprintf p "@ " + +let print_assertions p = + if !assertions <> [] then begin + fprintf p "Definition assertions (id: ident) args : Prop :=@ "; + fprintf p " match id, args with@ "; + List.iter (print_assertion p) !assertions; + fprintf p " | _, _ => False@ "; + fprintf p " end.@ @ " + end + +(* The prologue *) + +let prologue = "\ +Require Import Clightdefs. + +Local Open Scope Z_scope. + +" + +(* All together *) + +let print_program p prog = + fprintf p "@["; + fprintf p "%s" prologue; + define_idents p; + define_structs p prog; + List.iter (print_globdef p) prog.prog_defs; + fprintf p "Definition prog : Clight.program := {|@ "; + fprintf p "prog_defs :=@ %a;@ " (print_list print_ident_globdef) prog.prog_defs; + fprintf p "prog_main := %a@ " ident prog.prog_main; + fprintf p "|}.@ "; + print_assertions p; + fprintf p "@]@." + diff --git a/exportclight/README b/exportclight/README new file mode 100644 index 0000000..3fd8c0a --- /dev/null +++ b/exportclight/README @@ -0,0 +1,34 @@ + The clightgen tool + ------------------ + +OVERVIEW + +"clightgen" is an experimental tool that transforms C source files +into Clight abstract syntax, pretty-printed in Coq format in .v files. +These generated .v files can be loaded in a Coq session for +interactive verification, typically. + + +HOW TO BUILD + +Change to the top-level CompCert directory and issue + + make clightgen + + +USAGE + + clightgen [options] + +For each source file "src.c", its Clight abstract syntax is generated +in "src.v". + +The options recognized are a subset of those of the CompCert compiler ccomp +(see http://compcert.inria.fr/man/manual003.html for full documentation): + + -I search for include files + -D define preprocessor macro + -U undefine preprocessor macro + -Wp, pass options to C preprocessor + -f activate emulation of the given C feature + -- cgit v1.2.3