Fusion de la branche "traces":

- Ajout de traces d'evenements d'E/S dans les semantiques
- Ajout constructions switch et allocation dynamique
- Initialisation des variables globales
- Portage Coq 8.1 beta
Debut d'integration du front-end C:
- Traduction Clight -> Csharpminor dans cfrontend/
- Modifications de Csharpminor et Globalenvs en consequence.


git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@72 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e

1 files changed, 598 insertions, 0 deletions

diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
new file mode 100644
index 00000000..58c0bb8f
--- /dev/null
+++ b/cfrontend/Cshmgen.v
@@ -0,0 +1,598 @@
+Require Import Coqlib.
+Require Import Integers.
+Require Import Floats.
+Require Import AST.
+Require Import Csyntax.
+Require Import Csharpminor.
+
+(** The error monad *)
+
+Definition bind (A B: Set) (f: option A) (g: A -> option B) :=
+  match f with None => None | Some x => g x end.
+
+Implicit Arguments bind [A B].
+
+Notation "'do' X <- A ; B" := (bind A (fun X => B))
+   (at level 200, X ident, A at level 100, B at level 200).
+
+(** ** Operations on C types *)
+
+Definition signature_of_function (f: Csyntax.function) : signature :=
+  mksignature 
+   (typlist_of_typelist (type_of_params (Csyntax.fn_params f)))
+   (opttyp_of_type (Csyntax.fn_return f)).
+
+Definition chunk_of_type (ty: type): option memory_chunk :=
+  match access_mode ty with
+  | By_value chunk => Some chunk
+  | _ => None
+  end.
+
+Definition var_kind_of_type (ty: type): option var_kind :=
+  match ty with
+  | Tint I8 Signed => Some(Vscalar Mint8signed)
+  | Tint I8 Unsigned => Some(Vscalar Mint8unsigned)
+  | Tint I16 Signed => Some(Vscalar Mint16signed)
+  | Tint I16 Unsigned => Some(Vscalar Mint16unsigned)
+  | Tint I32 _ => Some(Vscalar Mint32)
+  | Tfloat F32 => Some(Vscalar Mfloat32)
+  | Tfloat F64 => Some(Vscalar Mfloat64)
+  | Tvoid => None
+  | Tpointer _ => Some(Vscalar Mint32)
+  | Tarray _ _ => Some(Varray (Csyntax.sizeof ty))
+  | Tfunction _ _ => None
+  | Tstruct fList => Some(Varray (Csyntax.sizeof ty))
+  | Tunion fList => Some(Varray (Csyntax.sizeof ty))
+end.
+  
+(** ** Csharpminor constructors *)
+
+(* The following functions build Csharpminor expressions that compute
+   the value of a C operation.  Most construction functions take
+   as arguments
+   - Csharpminor subexpressions that compute the values of the
+     arguments of the operation;
+   - The C types of the arguments of the operation.  These types
+     are used to insert the necessary numeric conversions and to
+     resolve operation overloading.
+   Most of these functions return an [option expr], with [None] 
+   denoting a case where the operation is not defined at the given types.
+*)
+
+Definition make_intconst (n: int) :=  Eop (Ointconst n) Enil.
+
+Definition make_floatconst (f: float) :=  Eop (Ofloatconst f) Enil.
+
+Definition make_unop (op: operation) (e: expr) :=  Eop op (Econs e Enil).
+
+Definition make_binop (op: operation) (e1 e2: expr) :=
+    Eop op (Econs e1 (Econs e2 Enil)).
+
+Definition make_floatofint (e: expr) (sg: signedness) :=
+  match sg with
+  | Signed => make_unop Ofloatofint e
+  | Unsigned => make_unop Ofloatofintu e
+  end.
+
+(* [make_boolean e ty] returns a Csharpminor expression that evaluates
+   to the boolean value of [e].  Recall that:
+     - in Csharpminor, [false] is the integer 0,
+       [true] any non-zero integer or any pointer
+     - in C, [false] is the integer 0, the null pointer, the float 0.0
+       [true] is any non-zero integer, non-null pointer, non-null float.
+*)
+Definition make_boolean (e: expr) (ty: type) :=
+  match ty with
+  | Tfloat _ => make_binop (Ocmpf Cne) e (make_floatconst Float.zero)
+  | _ => e
+  end.
+
+Definition make_neg (e: expr) (ty: type) :=
+  match ty with
+  | Tint _ _ => Some (make_binop Osub (make_intconst Int.zero) e)
+  | Tfloat _ => Some (make_unop Onegf e)
+  | _ => None
+  end.
+
+Definition make_notbool (e: expr) (ty: type) :=
+  make_binop (Ocmp Ceq) (make_boolean e ty) (make_intconst Int.zero).
+
+Definition make_notint (e: expr) (ty: type) :=
+  make_unop Onotint e.
+
+Definition make_add (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+  match classify_add ty1 ty2 with
+  | add_case_ii => Some (make_binop Oadd e1 e2)
+  | add_case_ff => Some (make_binop Oaddf e1 e2)
+  | add_case_pi ty =>
+      let n := make_intconst (Int.repr (Csyntax.sizeof ty)) in
+      Some (make_binop Oadd e1 (make_binop Omul n e2))
+  | add_default => None
+  end.
+
+Definition make_sub (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+  match classify_sub ty1 ty2 with
+  | sub_case_ii => Some (make_binop Osub e1 e2)
+  | sub_case_ff => Some (make_binop Osubf e1 e2)
+  | sub_case_pi ty =>
+      let n := make_intconst (Int.repr (Csyntax.sizeof ty)) in
+      Some (make_binop Osub e1 (make_binop Omul n e2))
+  | sub_case_pp ty =>
+      let n := make_intconst (Int.repr (Csyntax.sizeof ty)) in
+      Some (make_binop Odivu (make_binop Osub e1 e2) n)
+  | sub_default => None
+  end.
+
+Definition make_mul (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+  match classify_mul ty1 ty2 with
+  | mul_case_ii => Some (make_binop Omul e1 e2)
+  | mul_case_ff => Some (make_binop Omulf e1 e2)
+  | mul_default => None
+  end.
+
+Definition make_div (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+  match classify_div ty1 ty2 with
+  | div_case_I32unsi => Some (make_binop Odivu e1 e2)
+  | div_case_ii => Some (make_binop Odiv e1 e2)
+  | div_case_ff => Some (make_binop Odivf e1 e2)
+  | div_default => None
+  end.
+
+Definition make_mod (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+  match classify_mod ty1 ty2 with
+  | mod_case_I32unsi => Some (make_binop Omodu e1 e2)
+  | mod_case_ii=> Some (make_binop Omod e1 e2)
+  | mod_default => None
+  end.
+
+Definition make_and (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+  Some(make_binop Oand e1 e2).
+
+Definition make_or (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+  Some(make_binop Oor e1 e2).
+
+Definition make_xor (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+  Some(make_binop Oxor e1 e2).
+
+Definition make_shl (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+  Some(make_binop Oshl e1 e2).
+
+Definition make_shr (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+  match classify_shr ty1 ty2 with
+  | shr_case_I32unsi => Some (make_binop Oshru e1 e2)
+  | shr_case_ii=> Some (make_binop Oshr e1 e2)
+  | shr_default => None
+  end.
+
+Definition make_cmp (c: comparison) (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+  match classify_cmp ty1 ty2 with
+  | cmp_case_I32unsi => Some (make_binop (Ocmpu c) e1 e2)
+  | cmp_case_ii => Some (make_binop (Ocmp c) e1 e2)
+  | cmp_case_ff => Some (make_binop (Ocmpf c) e1 e2)
+  | cmp_case_pi => Some (make_binop (Ocmp c) e1 e2)
+  | cmp_case_pp => Some (make_binop (Ocmp c) e1 e2)
+  | cmp_default => None
+  end.
+
+Definition make_andbool (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+  Econdition
+    (make_boolean e1 ty1)
+    (Econdition
+       (make_boolean e2 ty2)
+       (make_intconst Int.one)
+       (make_intconst Int.zero))
+    (make_intconst Int.zero).
+
+Definition make_orbool (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
+  Econdition
+    (make_boolean e1 ty1)
+    (make_intconst Int.one)
+    (Econdition
+       (make_boolean e2 ty2)
+       (make_intconst Int.one)
+       (make_intconst Int.zero)).
+
+(* [make_cast from to e] applies to [e] the numeric conversions needed
+   to transform a result of type [from] to a result of type [to].
+   It is decomposed in two functions:
+   - [make_cast1]  converts between int/pointer and float if necessary
+   - [make_cast2]  converts to a "smaller" int or float type if necessary.
+*)
+
+Definition make_cast1 (from to: type) (e: expr) :=
+  match from, to with
+  | Tint _ uns, Tfloat _ => make_floatofint e uns
+  | Tfloat _, Tint _ _ => make_unop Ointoffloat e
+  | _, _ => e
+  end.
+
+Definition make_cast2 (from to: type) (e: expr) :=
+  match to with
+  | Tint I8 Signed => make_unop Ocast8signed e  
+  | Tint I8 Unsigned => make_unop Ocast8unsigned e  
+  | Tint I16 Signed => make_unop Ocast16signed e  
+  | Tint I16 Unsigned => make_unop Ocast16unsigned e  
+  | Tfloat F32 => make_unop Osingleoffloat e
+  | _ => e
+  end.
+
+Definition make_cast (from to: type) (e: expr) :=
+  make_cast2 from to (make_cast1 from to e).
+
+(* [make_load addr ty_res] loads a value of type [ty_res] from
+   the memory location denoted by the Csharpminor expression [addr].
+   If [ty_res] is an array or function type, returns [addr] instead,
+   as consistent with C semantics.
+*)
+
+Definition make_load (addr: expr) (ty_res: type) :=
+  match (access_mode ty_res) with
+  | By_value chunk => Some (Eload chunk addr)
+  | By_reference => Some addr
+  | By_nothing => None
+  end.
+
+(* [make_store addr ty_res rhs ty_rhs] stores the value of the
+   Csharpminor expression [rhs] into the memory location denoted by the
+   Csharpminor expression [addr].  
+   [ty] is the type of the memory location. *)
+
+Definition make_store (addr: expr) (ty: type) (rhs: expr) :=
+  match access_mode ty with
+  | By_value chunk => Some (Sstore chunk addr rhs)
+  | _ => None
+  end.
+
+(** ** Reading and writing variables *)
+
+(* [var_get id ty] builds Csharpminor code that evaluates to the
+   value of C variable [id] with type [ty].  Note that 
+   C variables of array or function type evaluate to the address
+   of the corresponding CabsCoq memory block, while variables of other types
+   evaluate to the contents of the corresponding C memory block.
+*)
+
+Definition var_get (id: ident) (ty: type) :=
+  match access_mode ty with
+  | By_value chunk => Some (Evar id)
+  | By_reference => Some (Eaddrof id)
+  | _ => None
+  end.
+
+(* [var_set id ty rhs] stores the value of the Csharpminor
+   expression [rhs] into the CabsCoq variable [id] of type [ty].
+*)
+
+Definition var_set (id: ident) (ty: type) (rhs: expr) :=
+  match access_mode ty with
+  | By_value chunk => Some (Sassign id rhs)
+  | _ => None
+  end.
+
+(** ** Translation of operators *)
+
+Definition transl_unop (op: unary_operation) (a: expr) (ta: type) : option expr :=
+  match op with
+  | Csyntax.Onotbool => Some(make_notbool a ta)
+  | Csyntax.Onotint => Some(make_notint a ta)
+  | Csyntax.Oneg => make_neg a ta
+  end.
+
+Definition transl_binop (op: binary_operation) (a: expr) (ta: type)
+                                  (b: expr) (tb: type) : option expr :=
+  match op with
+  | Csyntax.Oadd => make_add a ta b tb
+  | Csyntax.Osub => make_sub a ta b tb
+  | Csyntax.Omul => make_mul a ta b tb
+  | Csyntax.Odiv => make_div a ta b tb
+  | Csyntax.Omod => make_mod a ta b tb
+  | Csyntax.Oand => make_and a ta b tb
+  | Csyntax.Oor  => make_or a ta b tb
+  | Csyntax.Oxor => make_xor a ta b tb
+  | Csyntax.Oshl => make_shl a ta b tb
+  | Csyntax.Oshr => make_shr a ta b tb
+  | Csyntax.Oeq => make_cmp Ceq a ta b tb
+  | Csyntax.One => make_cmp Cne a ta b tb
+  | Csyntax.Olt => make_cmp Clt a ta b tb
+  | Csyntax.Ogt => make_cmp Cgt a ta b tb
+  | Csyntax.Ole => make_cmp Cle a ta b tb
+  | Csyntax.Oge => make_cmp Cge a ta b tb
+  end.
+
+(** ** Translation of expressions *)
+
+(* [transl_expr a] returns the Csharpminor code that computes the value
+   of expression [a]. The result is an option type to enable error reporting.
+
+   Most cases are self-explanatory.  We outline the non-obvious cases:
+
+   a && b    --->    a ? (b ? 1 : 0) : 0
+
+   a || b    --->    a ? 1 : (b ? 1 : 0)
+*)
+
+Fixpoint transl_expr (a: Csyntax.expr) {struct a} : option expr :=
+  match a with
+  | Expr (Csyntax.Econst_int n) _ =>
+      Some(make_intconst n)
+  | Expr (Csyntax.Econst_float n) _ =>
+      Some(make_floatconst n)
+  | Expr (Csyntax.Evar id) ty =>
+      var_get id ty
+  | Expr (Csyntax.Ederef b) _ =>
+      do tb <- transl_expr b;
+      make_load tb (typeof a)
+  | Expr (Csyntax.Eaddrof b) _ =>
+      transl_lvalue b
+  | Expr (Csyntax.Eunop op b) _ =>
+      do tb <- transl_expr b;
+      transl_unop op tb (typeof b)
+  | Expr (Csyntax.Ebinop op b c) _ =>
+      do tb <- transl_expr b;
+      do tc <- transl_expr c;
+      transl_binop op tb (typeof b) tc (typeof c)
+  | Expr (Csyntax.Ecast ty b) _ =>
+      do tb <- transl_expr b;
+      Some (make_cast (typeof b) ty tb)
+  | Expr (Csyntax.Eindex b c) ty =>
+      do tb <- transl_expr b;
+      do tc <- transl_expr c;
+      do ts <- make_add tb (typeof b) tc (typeof c);
+      make_load ts ty
+  | Expr (Csyntax.Ecall b cl) _ =>
+      match (classify_fun (typeof b)) with
+      | fun_case_f args res =>
+          do tb <- transl_expr b;
+          do tcl <- transl_exprlist cl;
+          Some(Ecall (signature_of_type args res) tb tcl)
+      | _ => None
+      end 
+  | Expr (Csyntax.Eandbool b c) _ =>
+      do tb <- transl_expr b;
+      do tc <- transl_expr c;
+      Some(make_andbool tb (typeof b) tc (typeof c))
+  | Expr (Csyntax.Eorbool b c) _ =>
+      do tb <- transl_expr b;
+      do tc <- transl_expr c;
+      Some(make_orbool tb (typeof b) tc (typeof c))
+  | Expr (Csyntax.Esizeof ty) _ =>
+      Some(make_intconst (Int.repr (Csyntax.sizeof ty)))
+  | Expr (Csyntax.Efield b i) ty => 
+      match typeof b with
+      | Tstruct fld =>
+          do tb <- transl_lvalue b;
+          do ofs <- field_offset i fld;
+          make_load
+            (make_binop Oadd tb (make_intconst (Int.repr ofs)))
+            ty
+      | Tunion fld =>
+          do tb <- transl_lvalue b;
+          make_load tb ty
+      | _ => None
+      end
+  end
+
+(* [transl_lvalue a] returns the Csharpminor code that evaluates
+   [a] as a lvalue, that is, code that returns the memory address
+   where the value of [a] is stored.
+*)
+
+with transl_lvalue (a: Csyntax.expr) {struct a} : option expr :=
+  match a with
+  | Expr (Csyntax.Evar id) _ =>
+      Some (Eaddrof id)
+  | Expr (Csyntax.Ederef b) _ =>
+      transl_expr b
+  | Expr (Csyntax.Eindex b c) _ =>
+      do tb <- transl_expr b;
+      do tc <- transl_expr c;
+      make_add tb (typeof b) tc (typeof c)
+  | Expr (Csyntax.Efield b i) ty => 
+      match typeof b with
+      | Tstruct fld =>
+          do tb <- transl_lvalue b;
+          do ofs <- field_offset i fld;
+          Some (make_binop Oadd tb (make_intconst (Int.repr ofs)))
+      | Tunion fld =>
+          transl_lvalue b
+      | _ => None
+      end
+  | _ => None
+  end
+
+(* [transl_exprlist al] returns a list of Csharpminor expressions
+   that compute the values of the list [al] of Csyntax expressions.
+   Used for function applications. *)
+
+with transl_exprlist (al: Csyntax.exprlist): option exprlist :=
+  match al with
+  | Csyntax.Enil => Some Enil
+  | Csyntax.Econs a1 a2 =>
+      do ta1 <- transl_expr a1;
+      do ta2 <- transl_exprlist a2;
+      Some (Econs ta1 ta2)
+  end.
+
+(** ** Translation of statements *)
+
+(** Determine if a C expression is a variable *)
+
+Definition is_variable (e: Csyntax.expr) : option ident :=
+  match e with
+  | Expr (Csyntax.Evar id) _ => Some id
+  | _ => None
+  end.
+
+(* [exit_if_false e] return the statement that tests the boolean
+   value of the CabsCoq expression [e] and performs an [exit 0] if [e]
+   evaluates to false.
+*)
+Definition exit_if_false (e: Csyntax.expr) : option stmt :=
+  do te <- transl_expr e;
+  Some(Sifthenelse
+        (make_notbool te (typeof e))
+        (Sexit 0%nat)
+        Sskip).
+
+(* [transl_statement nbrk ncnt s] returns a Csharpminor statement
+   that performs the same computations as the CabsCoq statement [s].
+
+   If the statement [s] terminates prematurely on a [break] construct,
+   the generated Csharpminor statement terminates prematurely on an
+   [exit nbrk] construct.
+
+   If the statement [s] terminates prematurely on a [continue]
+   construct, the generated Csharpminor statement terminates
+   prematurely on an [exit ncnt] construct.
+
+   Immediately within a loop, [nbrk = 1] and [ncnt = 0], but this 
+   changes when we're inside a [switch] construct.
+
+   The general translation for loops is as follows:
+
+while (e1) s;       --->     block {
+                               loop {
+                                 if (!e1) exit 0;
+                                 block { s }
+                                 // continue in s branches here
+                               }
+                             }
+                             // break in s branches here
+
+do s; while (e1);   --->     block {
+                               loop {
+                                 block { s }
+                                 // continue in s branches here
+                                 if (!e1) exit 0;
+                               }
+                             }
+                             // break in s branches here
+
+for (e1;e2;e3) s;   --->     e1;
+                             block {
+                               loop {
+                                 if (!e2) exit 0;
+                                 block { s }
+                                 // continue in s branches here
+                                 e3;
+                               }
+                             }
+                             // break in s branches here
+
+switch (e) {        --->    block { block { block { block {
+  case N1: s1;                switch (e) { N1: exit 0; N2: exit 1; default: exit 2; }
+  case N2: s2;                } ; s1  // with break -> exit 2  and continue -> exit 3
+  default: s;                 } ; s2  // with break -> exit 1  and continue -> exit 2
+}                             } ; s   // with break -> exit 0  and continue -> exit 1
+                              }
+*)
+
+Fixpoint switch_table (sl: labeled_statements) (k: nat) {struct sl} : list (int * nat) :=
+  match sl with
+  | LSdefault _ => nil
+  | LScase ni _ rem => (ni, k) :: switch_table rem (k+1)
+  end.
+
+Fixpoint transl_statement (nbrk ncnt: nat) (s: Csyntax.statement) {struct s} : option stmt :=
+  match s with
+  | Csyntax.Sskip =>
+      Some Sskip
+  | Csyntax.Sexpr e =>
+      do te <- transl_expr e;
+      Some (Sexpr te)
+  | Csyntax.Sassign b c =>
+      match (is_variable b) with
+      | Some id =>
+          do tc <- transl_expr c;
+          var_set id (typeof b) tc
+      | None =>
+          do tb <- transl_lvalue b;
+          do tc <- transl_expr c;
+          make_store tb (typeof b) tc
+      end 
+  | Csyntax.Ssequence s1 s2 =>
+      do ts1 <- transl_statement nbrk ncnt s1;
+      do ts2 <- transl_statement nbrk ncnt s2;
+      Some (Sseq ts1 ts2)
+  | Csyntax.Sifthenelse e s1 s2 =>
+      do te <- transl_expr e;
+      do ts1 <- transl_statement nbrk ncnt s1;
+      do ts2 <- transl_statement nbrk ncnt s2;
+      Some (Sifthenelse (make_boolean te (typeof e)) ts1 ts2)
+  | Csyntax.Swhile e s1 =>
+      do te <- exit_if_false e;
+      do ts1 <- transl_statement 1%nat 0%nat s1;
+      Some (Sblock (Sloop (Sseq te (Sblock ts1))))
+  | Csyntax.Sdowhile e s1 =>
+      do te <- exit_if_false e;
+      do ts1 <- transl_statement 1%nat 0%nat s1;
+      Some (Sblock (Sloop (Sseq (Sblock ts1) te)))
+  | Csyntax.Sfor e1 e2 e3 s1 =>
+      do te1 <- transl_statement nbrk ncnt e1;
+      do te2 <- exit_if_false e2;
+      do te3 <- transl_statement nbrk ncnt e3;
+      do ts1 <- transl_statement 1%nat 0%nat s1;
+      Some (Sseq te1 (Sblock (Sloop (Sseq te2 (Sseq (Sblock ts1) te3)))))
+  | Csyntax.Sbreak =>
+      Some (Sexit nbrk)
+  | Csyntax.Scontinue =>
+      Some (Sexit ncnt)
+  | Csyntax.Sreturn (Some e) =>
+      do te <- transl_expr e;
+      Some (Sreturn (Some te))
+  | Csyntax.Sreturn None =>
+      Some (Sreturn None)
+  | Csyntax.Sswitch e sl =>
+      let cases := switch_table sl 0 in
+      let ncases := List.length cases in
+      do te <- transl_expr e;
+      transl_lblstmts ncases (ncnt + ncases + 1)%nat sl (Sblock (Sswitch te cases ncases))
+  end
+
+with transl_lblstmts (nbrk ncnt: nat) (sl: labeled_statements) (body: stmt)
+                     {struct sl}: option stmt :=
+  match sl with
+  | LSdefault s =>
+      do ts <- transl_statement nbrk ncnt s;
+      Some (Sblock (Sseq body ts))
+  | LScase _ s rem =>
+      do ts <- transl_statement nbrk ncnt s;
+      transl_lblstmts (pred nbrk) (pred ncnt) rem (Sblock (Sseq body ts))
+  end.
+
+(*** Translation of functions *)
+
+Definition transl_params := transf_partial_program chunk_of_type.
+Definition transl_vars := transf_partial_program var_kind_of_type.
+
+Definition transl_function (f: Csyntax.function) : option function :=
+  do tparams <- transl_params (Csyntax.fn_params f);
+  do tvars <- transl_vars (Csyntax.fn_vars f);
+  do tbody <- transl_statement 1%nat 0%nat (Csyntax.fn_body f);
+  Some (mkfunction (signature_of_function f) tparams tvars tbody).
+
+Definition transl_fundef (f: Csyntax.fundef) : option fundef :=
+  match f with
+  | Csyntax.Internal g => 
+      do tg <- transl_function g; Some(AST.Internal tg)
+  | Csyntax.External id args res =>
+      Some(AST.External (external_function id args res))
+  end.
+
+(** ** Translation of programs *)
+
+Fixpoint transl_global_vars
+      (vl: list (ident * type * list init_data)) :
+      option (list (ident * var_kind * list init_data)) :=
+  match vl with
+  | nil => Some nil
+  | (id, ty, init) :: rem =>
+      do vk <- var_kind_of_type ty;
+      do trem <- transl_global_vars rem;
+      Some ((id, vk, init) :: trem)
+  end.
+
+Definition transl_program (p: Csyntax.program) : option program :=
+  do tfun <- transf_partial_program transl_fundef (Csyntax.prog_funct p);
+  do tvars <- transl_global_vars (Csyntax.prog_defs p);
+  Some (mkprogram tfun (Csyntax.prog_main p) tvars).