Refactor clightgen

Split reusable parts of ExportClight.ml off, into
ExportBase.ml and ExportCtypes.ml.

Rename exportclight/ directory to export/

7 files changed, 1350 insertions, 0 deletions

diff --git a/export/Clightdefs.v b/export/Clightdefs.v
new file mode 100644
index 00000000..708be1cb
--- /dev/null
+++ b/export/Clightdefs.v
@@ -0,0 +1,304 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.                            *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** All imports and definitions used by .v Clight 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.
+
+(** ** 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) : Clight.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 |}.
+
+(** ** 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.
+
+(** 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) : clight_scope.
+
+End ClightNotations.
diff --git a/export/Clightgen.ml b/export/Clightgen.ml
new file mode 100644
index 00000000..44c76cc6
--- /dev/null
+++ b/export/Clightgen.ml
@@ -0,0 +1,201 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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] <source files>
+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 <file>      Generate output in <file>
+|} ^
+prepro_help ^
+language_support_help ^
+{|Tracing options:
+  -dprepro       Save C file after preprocessing in <file>.i
+  -dparse        Save C file after parsing and elaboration in <file>.parsed.c
+  -dc            Save generated Compcert C in <file>.compcert.c
+  -dclight       Save generated Clight in <file>.light.c
+  -dall          Save all generated intermediate files in <file>.<ext>
+|} ^
+  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/Clightnorm.ml b/export/Clightnorm.ml
new file mode 100644
index 00000000..88d44c08
--- /dev/null
+++ b/export/Clightnorm.ml
@@ -0,0 +1,178 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.                            *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Clight-to-Clight rewriting to name memory loads *)
+
+(* The effect of this rewriting is to ensure that Clight expressions
+  whose evaluation involves a memory load (i.e. a lvalue-to-rvalue
+  conversion with By_value access mode) are always bound to a temporary
+  and never occur deep inside another expression.  For example,
+
+      tmp = *(x + 0) + *(x + 1)
+
+  in the original Clight is rewritten to
+
+      tmp1 = *(x + 0)
+      tmp2 = *(x + 1)
+      tmp = tmp1 + tmp2
+*)
+
+open Camlcoq
+open Ctypes
+open Clight
+
+let gen_next : AST.ident ref = ref P.one
+let gen_trail : (AST.ident * coq_type) list ref = ref []
+
+let gensym ty =
+  let id = !gen_next in
+  gen_next := P.succ id;
+  gen_trail := (id, ty) :: !gen_trail;
+  id
+
+let is_lvalue = function
+  | Evar _ | Ederef _ | Efield _ -> true
+  | _ -> false
+
+let accesses_memory e =
+  is_lvalue e &&
+  match access_mode (typeof e) with By_value _ -> true | _ -> false
+
+(** Normalization of an expression.  Return a normalized expression
+  and a list of statements to be executed before evaluating the expression. *)
+
+let rec norm_expr e =
+  let (sl, e') = norm_expr_1 e in
+  if accesses_memory e then begin
+    let ty = typeof e in
+    let id = gensym ty in
+    (sl @ [Sset(id, e')], Etempvar(id, ty))
+  end else
+    (sl, e')
+
+and norm_expr_1 e =
+  match e with
+  | Econst_int _ | Econst_float _ | Econst_single _ | Econst_long _ -> ([], e)
+  | Evar _ | Etempvar _ -> ([], e)
+  | Ederef(e1, t) ->
+      let (sl, e1') = norm_expr e1 in (sl, Ederef(e1', t))
+  | Eaddrof(e1, t) ->
+      let (sl, e1') = norm_expr_lvalue e1 in (sl, Eaddrof(e1', t))
+  | Eunop(op, e1, t) ->
+      let (sl, e1') = norm_expr e1 in (sl, Eunop(op, e1', t))
+  | Ebinop(op, e1, e2, t) ->
+      let (sl1, e1') = norm_expr e1 in
+      let (sl2, e2') = norm_expr e2 in
+      (sl1 @ sl2, Ebinop(op, e1', e2', t))
+  | Ecast(e1, t) ->
+      let (sl, e1') = norm_expr e1 in (sl, Ecast(e1', t))
+  | Efield(e1, id, t) ->
+      let (sl, e1') = norm_expr e1 in (sl, Efield(e1', id, t))
+  | Esizeof _ | Ealignof _ -> ([], e)
+
+(** An expression in l-value position has no memory dereference at top level,
+  by definition of l-values.  Hence, use the [norm_expr_1] variant.. *)
+and norm_expr_lvalue e = norm_expr_1 e
+
+(** In a [Sset id e] statement, the [e] expression can contain a memory
+  dereference at top level.  Hence, use the [norm_expr_1] variant. *)
+let norm_expr_set_top = norm_expr_1
+
+let rec norm_expr_list el =
+  match el with
+  | [] -> ([], [])
+  | e1 :: el ->
+      let (sl1, e1') = norm_expr e1 in
+      let (sl2, el') = norm_expr_list el in
+      (sl1 @ sl2, e1' :: el')
+
+let rec add_sequence sl s =
+  match sl with
+  | [] -> s
+  | s1 :: sl -> Ssequence(s1, add_sequence sl s)
+
+let rec norm_stmt s =
+  match s with
+  | Sskip -> s
+  | Sassign(e1, e2) ->
+      let (sl1, e1') = norm_expr_lvalue e1 in
+      let (sl2, e2') = norm_expr e2 in
+      add_sequence (sl1 @ sl2) (Sassign(e1', e2'))
+  | Sset(id, e) ->
+      let (sl, e') = norm_expr_set_top e in
+      add_sequence sl (Sset(id, e'))
+  | Scall(optid, e, el) ->
+      let (sl1, e') = norm_expr e in
+      let (sl2, el') = norm_expr_list el in
+      add_sequence (sl1 @ sl2) (Scall(optid, e', el'))  
+  | Sbuiltin(optid, ef, tyl, el) ->
+      let (sl, el') = norm_expr_list el in
+      add_sequence sl (Sbuiltin(optid, ef, tyl, el'))
+  | Ssequence(s1, s2) ->
+      Ssequence(norm_stmt s1, norm_stmt s2)
+  | Sifthenelse(e, s1, s2) ->
+      let (sl, e') = norm_expr e in
+      add_sequence sl (Sifthenelse(e', norm_stmt s1, norm_stmt s2))
+  | Sloop(s1, s2) ->
+      Sloop(norm_stmt s1, norm_stmt s2)
+  | Sbreak | Scontinue | Sreturn None -> s
+  | Sreturn (Some e) ->
+      let (sl, e') = norm_expr e in
+      add_sequence sl (Sreturn(Some e'))
+  | Sswitch(e, ls) ->
+      let (sl, e') = norm_expr e in
+      add_sequence sl (Sswitch(e', norm_lbl_stmt ls))
+  | Slabel(lbl, s1) ->
+      Slabel(lbl, norm_stmt s1)
+  | Sgoto lbl -> s
+
+and norm_lbl_stmt ls =
+  match ls with
+  | LSnil -> LSnil
+  | LScons(n, s, ls) -> LScons(n, norm_stmt s, norm_lbl_stmt ls)
+
+(* In "canonical atoms" mode, temporaries are between 2^7 and 2^12 - 1.
+   Below 2^7 are single-letter identifiers and above 2^12 are all
+   other identifiers. *)
+
+let first_temp = P.of_int 128
+let last_temp  = P.of_int 4095
+
+let next_var curr (v, _) =
+  if P.lt v curr
+  || !use_canonical_atoms && (P.lt v first_temp || P.gt v last_temp)
+  then curr
+  else P.succ v
+
+let next_var_list vars start = List.fold_left next_var start vars
+
+let norm_function f =
+  gen_next := next_var_list f.fn_params
+                (next_var_list f.fn_vars
+                   (next_var_list f.fn_temps
+                     (Camlcoq.first_unused_ident ())));
+  gen_trail := [];
+  let s' = norm_stmt f.fn_body in
+  let new_temps = !gen_trail in
+  { f with fn_body = s'; fn_temps = f.fn_temps @ new_temps }
+
+let norm_fundef = function
+  | Internal f -> Internal (norm_function f)
+  | External _ as fd -> fd
+
+let norm_program p =
+  let p1 = AST.transform_program norm_fundef (program_of_program p) in
+  { p with prog_defs = p1.AST.prog_defs }
diff --git a/export/ExportBase.ml b/export/ExportBase.ml
new file mode 100644
index 00000000..b7d0170d
--- /dev/null
+++ b/export/ExportBase.ml
@@ -0,0 +1,261 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 Format
+open Camlcoq
+open AST
+
+(* 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 ")@]"
+
+(* 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 coqptrofs p n =
+  let s = Z.to_string n in
+  if Z.ge n Z.zero
+  then fprintf p "(Ptrofs.repr %s)" s
+  else fprintf p "(Ptrofs.repr (%s))" s
+
+let coqint64 p n =
+  let n = camlint64_of_coqint n in
+  if n >= 0L
+  then fprintf p "(Int64.repr %Ld)" n
+  else fprintf p "(Int64.repr (%Ld))" n
+
+let coqfloat p n =
+  fprintf p "(Float.of_bits %a)" coqint64 (Floats.Float.to_bits n)
+
+let coqsingle p n =
+  fprintf p "(Float32.of_bits %a)" coqint (Floats.Float32.to_bits n)
+
+let positive p n =
+  fprintf p "%s%%positive" (Z.to_string (Z.Zpos n))
+
+let coqN p n =
+  fprintf p "%s%%N" (Z.to_string (Z.of_N n))
+
+let coqZ p n =
+  if Z.ge n Z.zero
+  then fprintf p "%s" (Z.to_string n)
+  else fprintf p "(%s)" (Z.to_string n)
+
+(* Coq strings *)
+
+let coqstring p s =
+  fprintf p "\"%s\"" (camlstring_of_coqstring s)
+
+(* Identifiers *)
+
+exception Not_an_identifier
+
+let sanitize_char = function
+  | 'A'..'Z' | 'a'..'z' | '0'..'9' | '_' as c -> c
+  | ' ' | '$' -> '_'
+  | _ -> raise Not_an_identifier
+
+let sanitize s =
+  if s <> ""
+  then "_" ^ String.map sanitize_char s
+  else "empty_ident"
+
+let temp_names : (ident, string) Hashtbl.t = Hashtbl.create 17
+
+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 ->
+  try
+    let s = Hashtbl.find temp_names id in
+    fprintf p "%s" s
+  with Not_found ->
+    positive p id
+
+let iter_hashtbl_sorted (h: ('a, string) Hashtbl.t) (f: 'a * string -> unit) =
+  List.iter f
+    (List.fast_sort (fun (k1, d1) (k2, d2) -> String.compare d1 d2)
+      (Hashtbl.fold (fun k d accu -> (k, d) :: accu) h []))
+
+let define_idents p =
+  iter_hashtbl_sorted
+    string_of_atom
+    (fun (id, name) ->
+      try
+        if !use_canonical_atoms && id = pos_of_string name then
+          fprintf p "Definition %s : ident := $\"%s\".@ "
+                    (sanitize name) name
+        else
+          fprintf p "Definition %s : ident := %a.@ "
+                    (sanitize name) positive id
+      with Not_an_identifier ->
+        ());
+  iter_hashtbl_sorted
+    temp_names
+    (fun (id, name) ->
+      fprintf p "Definition %s : ident := %a.@ "
+                name positive id);
+  fprintf p "@ "
+
+let name_temporary t =
+  if not (Hashtbl.mem string_of_atom t) && not (Hashtbl.mem temp_names t)
+  then begin
+    let t0 = first_unused_ident () in
+    let d = Z.succ (Z.sub (Z.Zpos t) (Z.Zpos t0)) in
+    Hashtbl.add temp_names t ("_t'" ^ Z.to_string d)
+  end
+
+let name_opt_temporary = function
+  | None -> ()
+  | Some id -> name_temporary id
+
+(* External functions *)
+
+let asttype p t =
+  fprintf p "%s"
+     (match t with
+      | AST.Tint -> "AST.Tint"
+      | AST.Tfloat -> "AST.Tfloat"
+      | AST.Tlong -> "AST.Tlong"
+      | AST.Tsingle -> "AST.Tsingle"
+      | AST.Tany32 -> "AST.Tany32"
+      | AST.Tany64 -> "AST.Tany64")
+
+let astrettype p = function
+  | AST.Tret t -> asttype p t
+  | AST.Tvoid -> fprintf p "AST.Tvoid"
+  | AST.Tint8signed -> fprintf p "AST.Tint8signed"
+  | AST.Tint8unsigned -> fprintf p "AST.Tint8unsigned"
+  | AST.Tint16signed -> fprintf p "AST.Tint16signed"
+  | AST.Tint16unsigned -> fprintf p "AST.Tint16unsigned"
+
+let name_of_chunk = function
+  | Mint8signed -> "Mint8signed"
+  | Mint8unsigned -> "Mint8unsigned"
+  | Mint16signed -> "Mint16signed"
+  | Mint16unsigned -> "Mint16unsigned"
+  | Mint32 -> "Mint32"
+  | Mint64 -> "Mint64"
+  | Mfloat32 -> "Mfloat32"
+  | Mfloat64 -> "Mfloat64"
+  | Many32 -> "Many32"
+  | Many64 -> "Many64"
+
+let callconv p cc =
+  if cc = cc_default
+  then fprintf p "cc_default"
+  else fprintf p "{|cc_vararg:=%a; cc_unproto:=%b; cc_structret:=%b|}"
+                  (print_option coqZ) cc.cc_vararg cc.cc_unproto cc.cc_structret
+
+let signatur p sg =
+  fprintf p "@[<hov 2>(mksignature@ %a@ %a@ %a)@]"
+     (print_list asttype) sg.sig_args
+     astrettype sg.sig_res
+     callconv sg.sig_cc
+
+let external_function p = function
+  | EF_external(name, sg) ->
+      fprintf p "@[<hov 2>(EF_external %a@ %a)@]" coqstring name signatur sg
+  | EF_builtin(name, sg) ->
+      fprintf p "@[<hov 2>(EF_builtin %a@ %a)@]" coqstring name signatur sg
+  | EF_runtime(name, sg) ->
+      fprintf p "@[<hov 2>(EF_runtime %a@ %a)@]" coqstring 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_malloc -> fprintf p "EF_malloc"
+  | EF_free -> fprintf p "EF_free"
+  | EF_memcpy(sz, al) ->
+      fprintf p "(EF_memcpy %ld %ld)" (Z.to_int32 sz) (Z.to_int32 al)
+  | EF_annot(kind, text, targs) ->
+      fprintf p "(EF_annot %a %a %a)"
+                positive kind coqstring text (print_list asttype) targs
+  | EF_annot_val(kind, text, targ) ->
+      fprintf p "(EF_annot_val %a %a %a)"
+                positive kind coqstring text asttype targ
+  | EF_debug(kind, text, targs) ->
+      fprintf p "(EF_debug %a %a %a)"
+                positive kind positive text (print_list asttype) targs
+  | EF_inline_asm(text, sg, clob) ->
+      fprintf p "@[<hov 2>(EF_inline_asm %a@ %a@ %a)@]"
+              coqstring text
+              signatur sg
+              (print_list coqstring) clob
+
+(* Variables *)
+
+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_int64 n -> fprintf p "Init_int64 %a" coqint64 n
+  | Init_float32 n -> fprintf p "Init_float32 %a" coqsingle n
+  | Init_float64 n -> fprintf p "Init_float64 %a" coqfloat n
+  | Init_space n -> fprintf p "Init_space %a" coqZ n
+  | Init_addrof(id,ofs) -> fprintf p "Init_addrof %a %a" ident id coqptrofs ofs
+
+let print_variable print_info p (id, v) =
+  fprintf p "Definition v%s := {|@ " (sanitize (extern_atom id));
+  fprintf p "  gvar_info := %a;@ " print_info 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 "|}.@ @ "
+
+(* Information about this run of clightgen *)
+
+let print_clightgen_info ~sourcefile ?normalized p =
+  fprintf p "@[<v 2>Module Info.";
+  fprintf p "@ Definition version := %S." Version.version;
+  fprintf p "@ Definition build_number := %S." Version.buildnr;
+  fprintf p "@ Definition build_tag := %S." Version.tag;
+  fprintf p "@ Definition build_branch := %S." Version.branch;
+  fprintf p "@ Definition arch := %S." Configuration.arch;
+  fprintf p "@ Definition model := %S." Configuration.model;
+  fprintf p "@ Definition abi := %S." Configuration.abi;
+  fprintf p "@ Definition bitsize := %d." (if Archi.ptr64 then 64 else 32);
+  fprintf p "@ Definition big_endian := %B." Archi.big_endian;
+  fprintf p "@ Definition source_file := %S." sourcefile;
+  begin match normalized with
+  | None -> ()
+  | Some b -> fprintf p "@ Definition normalized := %B." b
+  end;
+  fprintf p "@]@ End Info.@ @ "  
+  
diff --git a/export/ExportClight.ml b/export/ExportClight.ml
new file mode 100644
index 00000000..421db5ed
--- /dev/null
+++ b/export/ExportClight.ml
@@ -0,0 +1,251 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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.                            *)
+(*                                                                     *)
+(* *********************************************************************)
+
+(** Export Clight as a Coq file *)
+
+open Format
+open Camlcoq
+open AST
+open! Ctypes
+open Cop
+open Clight
+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 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
+  | Econst_long(n, t) ->
+      fprintf p "(Econst_long %a %a)" coqint64 n typ t
+  | Econst_single(n, t) ->
+      fprintf p "(Econst_single %a %a)" coqsingle 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
+  | Esizeof(t1, t) ->
+      fprintf p "(Esizeof %a %a)" typ t1 typ t
+  | Ealignof(t1, t) ->
+      fprintf p "(Ealignof %a %a)" typ t1 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
+  | LSnil ->
+      (fprintf p "LSnil")
+  | LScons(lbl, s, ls) ->
+      fprintf p "@[<hv 2>(LScons %a@ %a@ %a)@]"
+              (print_option coqZ) lbl stmt s lblstmts 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_temps := %a;@ " (print_list (print_pair ident typ)) f.fn_temps;
+  fprintf p "  fn_body :=@ ";
+  stmt 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 "@[<hov 2>(%a,@ @[<hov 2>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 AST Ctypes Cop Clight Clightdefs.\n\
+Import Clightdefs.ClightNotations.\n\
+Local Open Scope Z_scope.\n\
+Local Open Scope string_scope.\n\
+Local Open Scope clight_scope.\n"
+
+(* Naming the compiler-generated temporaries occurring in the program *)
+
+let rec name_expr = function
+  | Evar(id, t) -> ()
+  | Etempvar(id, t) -> name_temporary id
+  | Ederef(a1, t) -> name_expr a1
+  | Efield(a1, f, t) -> name_expr a1
+  | Econst_int(n, t) -> ()
+  | Econst_float(n, t) -> ()
+  | Econst_long(n, t) -> ()
+  | Econst_single(n, t) -> ()
+  | Eunop(op, a1, t) -> name_expr a1
+  | Eaddrof(a1, t) -> name_expr a1
+  | Ebinop(op, a1, a2, t) -> name_expr a1; name_expr a2
+  | Ecast(a1, t) -> name_expr a1
+  | Esizeof(t1, t) -> ()
+  | Ealignof(t1, t) -> ()
+
+let rec name_stmt = function
+  | Sskip -> ()
+  | Sassign(e1, e2) -> name_expr e1; name_expr e2
+  | Sset(id, e2) -> name_temporary id; name_expr e2
+  | Scall(optid, e1, el) ->
+      name_opt_temporary optid; name_expr e1; List.iter name_expr el
+  | Sbuiltin(optid, ef, tyl, el) ->
+      name_opt_temporary optid; List.iter name_expr el
+  | Ssequence(s1, s2) -> name_stmt s1; name_stmt s2
+  | Sifthenelse(e, s1, s2) -> name_expr e; name_stmt s1; name_stmt s2
+  | Sloop(s1, s2) -> name_stmt s1; name_stmt s2
+  | Sbreak -> ()
+  | Scontinue -> ()
+  | Sswitch(e, cases) -> name_expr e; name_lblstmts cases
+  | Sreturn (Some e) -> name_expr e
+  | Sreturn None -> ()
+  | Slabel(lbl, s1) -> name_stmt s1
+  | Sgoto lbl -> ()
+
+and name_lblstmts = function
+  | LSnil -> ()
+  | LScons(lbl, s, ls) -> name_stmt s; name_lblstmts ls
+
+let name_function f =
+  List.iter (fun (id, ty) -> name_temporary id) f.fn_temps;
+  name_stmt f.fn_body
+
+let name_globdef (id, g) =
+  match g with
+  | Gfun(Ctypes.Internal f) -> name_function f
+  | _ -> ()
+
+let name_program p =
+  List.iter name_globdef p.Ctypes.prog_defs
+
+(* All together *)
+
+let print_program p prog sourcefile normalized =
+  Hashtbl.clear temp_names;
+  name_program prog;
+  fprintf p "@[<v 0>";
+  fprintf p "%s" prologue;
+  print_clightgen_info ~sourcefile ~normalized 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 : Clight.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
new file mode 100644
index 00000000..428a1459
--- /dev/null
+++ b/export/ExportCtypes.ml
@@ -0,0 +1,122 @@
+(* *********************************************************************)
+(*                                                                     *)
+(*              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 Format
+open Camlcoq
+open Ctypes
+open ExportBase
+
+(* Raw attributes *)
+
+let attribute p a =
+  if a = noattr then
+    fprintf p "noattr"
+  else
+    fprintf p "{| attr_volatile := %B; attr_alignas := %a |}"
+              a.attr_volatile
+              (print_option coqN) a.attr_alignas
+
+(* Raw int size and signedness *)
+
+let intsize p sz =
+  fprintf p "%s"
+    (match sz with 
+     | I8 -> "I8"
+     | I16 -> "I16"
+     | I32 -> "I32"
+     | IBool -> "IBool")
+
+let signedness p sg =
+  fprintf p "%s"
+    (match sg with
+      | Signed -> "Signed"
+      | Unsigned -> "Unsigned")
+
+(* Types *)
+
+let rec typ p t =
+  match attr_of_type t with
+  | { attr_volatile = false; attr_alignas = None} ->
+        rtyp p t
+  | { attr_volatile = true; attr_alignas = None} ->
+        fprintf p "(tvolatile %a)" rtyp t
+  | { attr_volatile = false; attr_alignas = Some n} ->
+        fprintf p "(talignas %a %a)" coqN n rtyp t
+  | { attr_volatile = true; attr_alignas = Some n} ->
+        fprintf p "(tvolatile_alignas %a %a)" coqN n rtyp t
+
+and rtyp p = function
+  | Tvoid -> fprintf p "tvoid"
+  | Ctypes.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")
+  | Ctypes.Tlong(sg, _) ->
+      fprintf p "%s" (
+        match sg with
+        | Signed -> "tlong"
+        | Unsigned -> "tulong")
+  | Ctypes.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 (Z.to_int32 sz)
+  | Tfunction(targs, tres, cc) ->
+      fprintf p "@[<hov 2>(Tfunction@ %a@ %a@ %a)@]"
+                typlist targs typ tres callconv cc
+  | Tstruct(id, _) ->
+      fprintf p "(Tstruct %a noattr)" ident id
+  | Tunion(id, _) ->
+      fprintf p "(Tunion %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
+
+(* Composite definitions *)
+
+let print_member p = function
+  | Member_plain (id, ty) ->
+      fprintf p "@[<hov 2>Member_plain@ %a@ %a@]"
+              ident id typ ty
+  | Member_bitfield (id, sz, sg, a, width, pad) ->
+      fprintf p "@[<hov 2>Member_bitfield@ %a@ %a@ %a@ %a@ %a@ %B@]"
+              ident id
+              intsize sz
+              signedness sg
+              attribute a
+              coqZ width
+              pad
+
+let print_composite_definition p (Composite(id, su, m, a)) =
+  fprintf p "@[<hv 2>Composite %a %s@ %a@ %a@]"
+    ident id
+    (match su with Struct -> "Struct" | Union -> "Union")
+    (print_list print_member) m
+    attribute a
+
diff --git a/export/README.md b/export/README.md
new file mode 100644
index 00000000..85e0790b
--- /dev/null
+++ b/export/README.md
@@ -0,0 +1,33 @@
+# 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 [user's manual](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
+```