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

4 files changed, 872 insertions, 0 deletions

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] <source files>
+Recognized source files:
+  .c             C source file
+Processing options:
+  -E             Preprocess only, send result to standard output
+Preprocessing options:
+  -I<dir>        Add <dir> to search path for #include files
+  -D<symb>=<val> Define preprocessor symbol
+  -U<symb>       Undefine preprocessor symbol
+  -Wp,<opt>      Pass option <opt> to the preprocessor
+Language support options (use -fno-<opt> to turn off -f<opt>) :
+  -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 <file>.parse.c
+  -dc            Save generated Compcert C in <file>.compcert.c
+  -dclight       Save generated Clight in <file>.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 "@[<hov 1>(%a,@ %a)@]" fn1 x1 fn2 x2
+
+let print_list fn p l =
+  match l with
+  | [] ->
+      fprintf p "nil"
+  | hd :: tl ->
+      fprintf p "@[<hov 1>(";
+      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 "@[<hov 2>(Tfunction@ %a@ %a)@]" typlist targs typ tres
+  | Tstruct(id, flds, _) ->
+      if !use_struct_names
+      then fprintf p "t%a" ident id
+      else fprintf p "@[<hov 2>(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 "@[<hov 2>(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 "@[<hov 2>(Tcons@ %a@ %a)@]" typ t typlist tl
+
+and fieldlist p = function
+  | Fnil ->
+      fprintf p "Fnil"
+  | Fcons(id, t, fl) ->
+      fprintf p "@[<hov 2>(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 "@[<hov 2>(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 "@[<hov 2>(EF_external %a@ %a)@]" ident name signatur sg
+  | EF_builtin(name, sg) ->
+      fprintf p "@[<hov 2>(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 "@[<hov 2>(Ederef@ %a@ %a)@]" expr a1 typ t
+  | Efield(a1, f, t) ->
+      fprintf p "@[<hov 2>(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 "@[<hov 2>(Eunop %s@ %a@ %a)@]"
+         (name_unop op) expr a1 typ t
+  | Eaddrof(a1, t) ->
+      fprintf p "@[<hov 2>(Eaddrof@ %a@ %a)@]" expr a1 typ t
+  | Ebinop(op, a1, a2, t) ->
+      fprintf p "@[<hov 2>(Ebinop %s@ %a@ %a@ %a)@]"
+         (name_binop op) expr a1 expr a2 typ t
+  | Ecast(a1, t) ->
+      fprintf p "@[<hov 2>(Ecast@ %a@ %a)@]" expr a1 typ t
+
+(* Statements *)
+
+let rec stmt p = function
+  | Sskip ->
+      fprintf p "Sskip"
+  | Sassign(e1, e2) ->
+      fprintf p "@[<hov 2>(Sassign@ %a@ %a)@]" expr e1 expr e2
+  | Sset(id, e2) ->
+      fprintf p "@[<hov 2>(Sset %a@ %a)@]" ident id expr e2
+  | Scall(optid, e1, el) ->
+      fprintf p "@[<hov 2>(Scall %a@ %a@ %a)@]"
+        (print_option ident) optid expr e1 (print_list expr) el
+  | Sbuiltin(optid, ef, tyl, el) ->
+      fprintf p "@[<hov 2>(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 "@[<hv 2>(Ssequence@ %a@ %a)@]" stmt s1 stmt s2
+  | Sifthenelse(e, s1, s2) ->
+      fprintf p "@[<hv 2>(Sifthenelse %a@ %a@ %a)@]" expr e stmt s1 stmt s2
+  | Sloop (Ssequence (Sifthenelse(e, Sskip, Sbreak), s), Sskip) ->
+      fprintf p "@[<hv 2>(Swhile@ %a@ %a)@]" expr e stmt s
+  | Sloop (Ssequence (Ssequence(Sskip, Sifthenelse(e, Sskip, Sbreak)), s), Sskip) ->
+      fprintf p "@[<hv 2>(Swhile@ %a@ %a)@]" expr e stmt s
+  | Sloop(s1, s2) ->
+      fprintf p "@[<hv 2>(Sloop@ %a@ %a)@]" stmt s1 stmt s2
+  | Sbreak ->
+      fprintf p "Sbreak"
+  | Scontinue ->
+      fprintf p "Scontinue"
+  | Sswitch(e, cases) ->
+      fprintf p "@[<hv 2>(Sswitch %a@ %a)@]" expr e lblstmts cases
+  | Sreturn e ->
+      fprintf p "@[<hv 2>(Sreturn %a)@]" (print_option expr) e
+  | Slabel(lbl, s1) ->
+      fprintf p "@[<hv 2>(Slabel %a@ %a)@]" ident lbl stmt s1
+  | Sgoto lbl ->
+      fprintf p "(Sgoto %a)" ident lbl
+
+and lblstmts p = function
+  | LSdefault s ->
+      fprintf p "@[<hv 2>(LSdefault@ %a)@]" stmt s
+  | LScase(lbl, s, ls) ->
+      fprintf p "@[<hv 2>(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 "@[<hov 2>(%a,@ @[<hov 2>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 "@[<hv 2>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 "@[<v 0>";
+  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] <C source files>
+
+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<dir>     search <dir> for include files
+   -D<symbol>  define preprocessor macro
+   -U<symbol>  undefine preprocessor macro
+   -Wp,<opts>  pass options to C preprocessor
+   -f<feature> activate emulation of the given C feature
+