Merge pull request #93 from AbsInt/separate-compilation

This pull request implements "approach A" to separate compilation in CompCert from the paper

Lightweight verification of separate compilation
by Jeehoon Kang, Yoonseung Kim, Chung-Kil Hur, Derek Dreyer, Viktor Vafeiadis,
POPL 2016, pages 178-190

In a nutshell, semantic preservation is still stated and proved in terms of a whole C program and a whole assembly program. However, the whole C program can be the result of syntactic linking of several C compilation units, each unit being separated compiled by CompCert to produce assembly unit, and these assembly units being linked together to produce the whole assembly program.

This way, the statement of semantic preservation and its proof now take into account the fact that each compilation unit is compiled separately, knowing only a fragment of the whole program (i.e. the current compilation unit) rather than the whole program.

18 files changed, 1093 insertions, 649 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index e4001e6b..418fa702 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -1090,6 +1090,7 @@ let convertFundef loc env fd =
 (** External function declaration *)
 
 let re_builtin = Str.regexp "__builtin_"
+let re_runtime = Str.regexp "__i64_"
 
 let convertFundecl env (sto, id, ty, optinit) =
   let (args, res, cconv) =
@@ -1102,6 +1103,7 @@ let convertFundecl env (sto, id, ty, optinit) =
   let ef =
     if id.name = "malloc" then EF_malloc else
     if id.name = "free" then EF_free else
+    if Str.string_match re_runtime id.name 0 then EF_runtime(id'', sg) else
     if Str.string_match re_builtin id.name 0
     && List.mem_assoc id.name builtins.functions
     then EF_builtin(id'', sg)
diff --git a/cfrontend/Cexec.v b/cfrontend/Cexec.v
index 00d77b00..bf88e033 100644
--- a/cfrontend/Cexec.v
+++ b/cfrontend/Cexec.v
@@ -536,6 +536,7 @@ Definition do_external (ef: external_function):
   match ef with
   | EF_external name sg => do_external_function name sg ge
   | EF_builtin name sg => do_external_function name sg ge
+  | EF_runtime name sg => do_external_function name sg ge
   | EF_vload chunk => do_ef_volatile_load chunk
   | EF_vstore chunk => do_ef_volatile_store chunk
   | EF_malloc => do_ef_malloc
@@ -558,6 +559,8 @@ Proof with try congruence.
   eapply do_external_function_sound; eauto.
 (* EF_builtin *)
   eapply do_external_function_sound; eauto.
+(* EF_runtime *)
+  eapply do_external_function_sound; eauto.
 (* EF_vload *)
   unfold do_ef_volatile_load. destruct vargs... destruct v... destruct vargs...
   mydestr. destruct p as [[w'' t''] v]; mydestr.
@@ -604,6 +607,8 @@ Proof.
   eapply do_external_function_complete; eauto.
 (* EF_builtin *)
   eapply do_external_function_complete; eauto.
+(* EF_runtime *)
+  eapply do_external_function_complete; eauto.
 (* EF_vload *)
   inv H; unfold do_ef_volatile_load.
   exploit do_volatile_load_complete; eauto. intros EQ; rewrite EQ; auto.
diff --git a/cfrontend/Clight.v b/cfrontend/Clight.v
index 086f4654..e6426fb8 100644
--- a/cfrontend/Clight.v
+++ b/cfrontend/Clight.v
@@ -146,9 +146,7 @@ Definition var_names (vars: list(ident * type)) : list ident :=
 (** Functions can either be defined ([Internal]) or declared as
   external functions ([External]). *)
 
-Inductive fundef : Type :=
-  | Internal: function -> fundef
-  | External: external_function -> typelist -> type -> calling_convention -> fundef.
+Definition fundef := Ctypes.fundef function.
 
 (** The type of a function definition. *)
 
@@ -163,45 +161,16 @@ Definition type_of_fundef (f: fundef) : type :=
 
 (** ** Programs *)
 
-(** A program is composed of:
+(** As defined in module [Ctypes], a program, or compilation unit, is
+  composed of:
 - a list of definitions of functions and global variables;
 - the names of functions and global variables that are public (not static);
 - the name of the function that acts as entry point ("main" function).
-- a list of definitions for structure and union names;
-- the corresponding composite environment;
-*)
-
-Record program : Type := {
-  prog_defs: list (ident * globdef fundef type);
-  prog_public: list ident;
-  prog_main: ident;
-  prog_types: list composite_definition;
-  prog_comp_env: composite_env;
-  prog_comp_env_eq: build_composite_env prog_types = OK prog_comp_env
-}.
+- a list of definitions for structure and union names
+- the corresponding composite environment
+- a proof that this environment is consistent with the definitions. *)
 
-Definition program_of_program (p: program) : AST.program fundef type :=
-  {| AST.prog_defs := p.(prog_defs);
-     AST.prog_public := p.(prog_public);
-     AST.prog_main := p.(prog_main) |}.
-
-Coercion program_of_program: program >-> AST.program.
-
-Program Definition make_program (types: list composite_definition)
-                                (defs: list (ident * globdef fundef type))
-                                (public: list ident)
-                                (main: ident): res program :=
-  match build_composite_env types with
-  | OK env =>
-      OK {| prog_defs := defs;
-            prog_public := public;
-            prog_main := main;
-            prog_types := types;
-            prog_comp_env := env;
-            prog_comp_env_eq := _ |}
-  | Error msg =>
-      Error msg
-  end.
+Definition program := Ctypes.program function.
 
 (** * Operational semantics *)
 
@@ -774,4 +743,3 @@ Proof.
   eapply external_call_trace_length; eauto.
   eapply external_call_trace_length; eauto.
 Qed.
-
diff --git a/cfrontend/Cminorgen.v b/cfrontend/Cminorgen.v
index c2b59fbe..b9a28ee1 100644
--- a/cfrontend/Cminorgen.v
+++ b/cfrontend/Cminorgen.v
@@ -12,19 +12,10 @@
 
 (** Translation from Csharpminor to Cminor. *)
 
-Require Import FSets.
-Require FSetAVL.
-Require Import Orders.
-Require Mergesort.
-Require Import Coqlib.
-Require Import Errors.
-Require Import Maps.
-Require Import Ordered.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Csharpminor.
-Require Import Cminor.
+Require Import FSets FSetAVL Orders Mergesort.
+Require Import Coqlib Maps Ordered Errors Integers Floats.
+Require Import AST Linking.
+Require Import Csharpminor Cminor.
 
 Local Open Scope string_scope.
 Local Open Scope error_monad_scope.
diff --git a/cfrontend/Cminorgenproof.v b/cfrontend/Cminorgenproof.v
index 7a5d882e..2f551d68 100644
--- a/cfrontend/Cminorgenproof.v
+++ b/cfrontend/Cminorgenproof.v
@@ -12,61 +12,54 @@
 
 (** Correctness proof for Cminor generation. *)
 
-Require Import Coq.Program.Equality.
-Require Import FSets.
-Require Import Permutation.
-Require Import Coqlib.
+Require Import Coq.Program.Equality FSets Permutation.
+Require Import FSets FSetAVL Orders Mergesort.
+Require Import Coqlib Maps Ordered Errors Integers Floats.
 Require Intv.
-Require Import Errors.
-Require Import Maps.
-Require Import AST.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import Memory.
-Require Import Events.
-Require Import Globalenvs.
-Require Import Smallstep.
-Require Import Switch.
-Require Import Csharpminor.
-Require Import Cminor.
-Require Import Cminorgen.
+Require Import AST Linking.
+Require Import Values Memory Events Globalenvs Smallstep.
+Require Import Csharpminor Switch Cminor Cminorgen.
 
 Open Local Scope error_monad_scope.
 
+Definition match_prog (p: Csharpminor.program) (tp: Cminor.program) :=
+  match_program (fun cu f tf => transl_fundef f = OK tf) eq p tp.
+
+Lemma transf_program_match:
+  forall p tp, transl_program p = OK tp -> match_prog p tp.
+Proof.
+  intros. apply match_transform_partial_program; auto.
+Qed.
+
 Section TRANSLATION.
 
 Variable prog: Csharpminor.program.
 Variable tprog: program.
-Hypothesis TRANSL: transl_program prog = OK tprog.
+Hypothesis TRANSL: match_prog prog tprog.
 Let ge : Csharpminor.genv := Genv.globalenv prog.
 Let tge: genv := Genv.globalenv tprog.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof (Genv.find_symbol_transf_partial transl_fundef _ TRANSL).
+Proof (Genv.find_symbol_transf_partial TRANSL).
 
-Lemma public_preserved:
-  forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s.
-Proof (Genv.public_symbol_transf_partial transl_fundef _ TRANSL).
+Lemma senv_preserved:
+  Senv.equiv ge tge.
+Proof (Genv.senv_transf_partial TRANSL).
 
 Lemma function_ptr_translated:
   forall (b: block) (f: Csharpminor.fundef),
   Genv.find_funct_ptr ge b = Some f ->
   exists tf,
   Genv.find_funct_ptr tge b = Some tf /\ transl_fundef f = OK tf.
-Proof (Genv.find_funct_ptr_transf_partial transl_fundef _ TRANSL).
+Proof (Genv.find_funct_ptr_transf_partial TRANSL).
 
 Lemma functions_translated:
   forall (v: val) (f: Csharpminor.fundef),
   Genv.find_funct ge v = Some f ->
   exists tf,
   Genv.find_funct tge v = Some tf /\ transl_fundef f = OK tf.
-Proof (Genv.find_funct_transf_partial transl_fundef _ TRANSL).
-
-Lemma varinfo_preserved:
-  forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
-Proof (Genv.find_var_info_transf_partial transl_fundef _ TRANSL).
+Proof (Genv.find_funct_transf_partial TRANSL).
 
 Lemma sig_preserved_body:
   forall f tf cenv size,
@@ -2029,8 +2022,7 @@ Proof.
   intros [f' [vres' [tm' [EC [VINJ [MINJ' [UNMAPPED [OUTOFREACH [INCR SEPARATED]]]]]]]]].
   left; econstructor; split.
   apply plus_one. econstructor. eauto.
-  eapply external_call_symbols_preserved; eauto.
-  exact symbols_preserved. exact public_preserved. eexact varinfo_preserved.
+  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   assert (MCS': match_callstack f' m' tm'
                  (Frame cenv tfn e le te sp lo hi :: cs)
                  (Mem.nextblock m') (Mem.nextblock tm')).
@@ -2184,8 +2176,7 @@ Opaque PTree.set.
   intros [f' [vres' [tm' [EC [VINJ [MINJ' [UNMAPPED [OUTOFREACH [INCR SEPARATED]]]]]]]]].
   left; econstructor; split.
   apply plus_one. econstructor.
-  eapply external_call_symbols_preserved; eauto.
-  exact symbols_preserved. exact public_preserved. eexact varinfo_preserved.
+  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   econstructor; eauto.
   apply match_callstack_incr_bound with (Mem.nextblock m) (Mem.nextblock tm).
   eapply match_callstack_external_call; eauto.
@@ -2224,11 +2215,11 @@ Proof.
   exploit function_ptr_translated; eauto. intros [tf [FIND TR]].
   econstructor; split.
   econstructor.
-  apply (Genv.init_mem_transf_partial _ _ TRANSL). eauto.
+  apply (Genv.init_mem_transf_partial TRANSL). eauto.
   simpl. fold tge. rewrite symbols_preserved.
   replace (prog_main tprog) with (prog_main prog). eexact H0.
   symmetry. unfold transl_program in TRANSL.
-  eapply transform_partial_program_main; eauto.
+  eapply match_program_main; eauto. 
   eexact FIND.
   rewrite <- H2. apply sig_preserved; auto.
   eapply match_callstate with (f := Mem.flat_inj (Mem.nextblock m0)) (cs := @nil frame) (cenv := PTree.empty Z).
@@ -2250,7 +2241,7 @@ Theorem transl_program_correct:
   forward_simulation (Csharpminor.semantics prog) (Cminor.semantics tprog).
 Proof.
   eapply forward_simulation_star; eauto.
-  eexact public_preserved.
+  apply senv_preserved.
   eexact transl_initial_states.
   eexact transl_final_states.
   eexact transl_step_correct.
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 825a563c..40b51bd3 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -20,17 +20,9 @@
    Csharpminor's simpler control structures.
 *)
 
-Require Import Coqlib.
-Require Import Maps.
-Require Import Errors.
-Require Import Integers.
-Require Import Floats.
-Require Import AST.
-Require Import Ctypes.
-Require Import Cop.
-Require Import Clight.
-Require Import Cminor.
-Require Import Csharpminor.
+Require Import Coqlib Maps Errors Integers Floats.
+Require Import AST Linking.
+Require Import Ctypes Cop Clight Cminor Csharpminor.
 
 Open Local Scope string_scope.
 Open Local Scope error_monad_scope.
@@ -125,6 +117,18 @@ Definition make_cmp_ne_zero (e: expr) :=
   | _ => Ebinop (Ocmp Cne) e (make_intconst Int.zero)
   end.
 
+(** Variants of [sizeof] and [alignof] that check that the given type is complete. *)
+
+Definition sizeof (ce: composite_env) (t: type) : res Z :=
+  if complete_type ce t
+  then OK (Ctypes.sizeof ce t)
+  else Error (msg "incomplete type").
+
+Definition alignof (ce: composite_env) (t: type) : res Z :=
+  if complete_type ce t
+  then OK (Ctypes.alignof ce t)
+  else Error (msg "incomplete type").
+
 (** [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]. *)
 
@@ -238,16 +242,20 @@ Definition make_binarith (iop iopu fop sop lop lopu: binary_operation)
 Definition make_add (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   match classify_add ty1 ty2 with
   | add_case_pi ty =>
-      let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in
+      do sz <- sizeof ce ty;
+      let n := make_intconst (Int.repr sz) in
       OK (Ebinop Oadd e1 (Ebinop Omul n e2))
   | add_case_ip ty =>
-      let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in
+      do sz <- sizeof ce ty;
+      let n := make_intconst (Int.repr sz) in
       OK (Ebinop Oadd e2 (Ebinop Omul n e1))
   | add_case_pl ty =>
-      let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in
+      do sz <- sizeof ce ty;
+      let n := make_intconst (Int.repr sz) in
       OK (Ebinop Oadd e1 (Ebinop Omul n (Eunop Ointoflong e2)))
   | add_case_lp ty =>
-      let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in
+      do sz <- sizeof ce ty;
+      let n := make_intconst (Int.repr sz) in
       OK (Ebinop Oadd e2 (Ebinop Omul n (Eunop Ointoflong e1)))
   | add_default =>
       make_binarith Oadd Oadd Oaddf Oaddfs Oaddl Oaddl e1 ty1 e2 ty2
@@ -256,13 +264,16 @@ Definition make_add (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2:
 Definition make_sub (ce: composite_env) (e1: expr) (ty1: type) (e2: expr) (ty2: type) :=
   match classify_sub ty1 ty2 with
   | sub_case_pi ty =>
-      let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in
+      do sz <- sizeof ce ty;
+      let n := make_intconst (Int.repr sz) in
       OK (Ebinop Osub e1 (Ebinop Omul n e2))
   | sub_case_pp ty =>
-      let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in
+      do sz <- sizeof ce ty;
+      let n := make_intconst (Int.repr sz) in
       OK (Ebinop Odiv (Ebinop Osub e1 e2) n)
   | sub_case_pl ty =>
-      let n := make_intconst (Int.repr (Ctypes.sizeof ce ty)) in
+      do sz <- sizeof ce ty;
+      let n := make_intconst (Int.repr sz) in
       OK (Ebinop Osub e1 (Ebinop Omul n (Eunop Ointoflong e2)))
   | sub_default =>
       make_binarith Osub Osub Osubf Osubfs Osubl Osubl e1 ty1 e2 ty2
@@ -351,8 +362,9 @@ Definition make_load (addr: expr) (ty_res: type) :=
   by-copy assignment of a value of Clight type [ty]. *)
 
 Definition make_memcpy (ce: composite_env) (dst src: expr) (ty: type) :=
-  Sbuiltin None (EF_memcpy (Ctypes.sizeof ce ty) (Ctypes.alignof_blockcopy ce ty))
-                (dst :: src :: nil).
+  do sz <- sizeof ce ty;
+  OK (Sbuiltin None (EF_memcpy sz (Ctypes.alignof_blockcopy ce ty))
+                    (dst :: src :: nil)).
 
 (** [make_store addr ty rhs] stores the value of the
    Csharpminor expression [rhs] into the memory location denoted by the
@@ -362,7 +374,7 @@ Definition make_memcpy (ce: composite_env) (dst src: expr) (ty: type) :=
 Definition make_store (ce: composite_env) (addr: expr) (ty: type) (rhs: expr) :=
   match access_mode ty with
   | By_value chunk => OK (Sstore chunk addr rhs)
-  | By_copy => OK (make_memcpy ce addr rhs ty)
+  | By_copy => make_memcpy ce addr rhs ty
   | _ => Error (msg "Cshmgen.make_store")
   end.
 
@@ -457,9 +469,9 @@ Fixpoint transl_expr (ce: composite_env) (a: Clight.expr) {struct a} : res expr
       do addr <- make_field_access ce (typeof b) i tb;
       make_load addr ty
   | Clight.Esizeof ty' ty =>
-      OK(make_intconst (Int.repr (sizeof ce ty')))
+      do sz <- sizeof ce ty'; OK(make_intconst (Int.repr sz))
   | Clight.Ealignof ty' ty =>
-      OK(make_intconst (Int.repr (alignof ce ty')))
+      do al <- alignof ce ty'; OK(make_intconst (Int.repr al))
   end
 
 (** [transl_lvalue a] returns the Csharpminor code that evaluates
@@ -621,7 +633,8 @@ with transl_lbl_stmt (ce: composite_env) (tyret: type) (nbrk ncnt: nat)
 
 (*** Translation of functions *)
 
-Definition transl_var (ce: composite_env) (v: ident * type) := (fst v, sizeof ce (snd v)).
+Definition transl_var (ce: composite_env) (v: ident * type) :=
+  do sz <- sizeof ce (snd v); OK (fst v, sz).
 
 Definition signature_of_function (f: Clight.function) :=
   {| sig_args := map typ_of_type (map snd (Clight.fn_params f));
@@ -630,18 +643,19 @@ Definition signature_of_function (f: Clight.function) :=
 
 Definition transl_function (ce: composite_env) (f: Clight.function) : res function :=
   do tbody <- transl_statement ce f.(Clight.fn_return) 1%nat 0%nat (Clight.fn_body f);
+  do tvars <- mmap (transl_var ce) (Clight.fn_vars f);
   OK (mkfunction
        (signature_of_function f)
        (map fst (Clight.fn_params f))
-       (map (transl_var ce) (Clight.fn_vars f))
+       tvars
        (map fst (Clight.fn_temps f))
        tbody).
 
-Definition transl_fundef (ce: composite_env) (f: Clight.fundef) : res fundef :=
+Definition transl_fundef (ce: composite_env) (id: ident) (f: Clight.fundef) : res fundef :=
   match f with
-  | Clight.Internal g =>
+  | Internal g =>
       do tg <- transl_function ce g; OK(AST.Internal tg)
-  | Clight.External ef args res cconv =>
+  | External ef args res cconv =>
       if signature_eq (ef_sig ef) (signature_of_type args res cconv)
       then OK(AST.External ef)
       else Error(msg "Cshmgen.transl_fundef: wrong external signature")
@@ -649,7 +663,7 @@ Definition transl_fundef (ce: composite_env) (f: Clight.fundef) : res fundef :=
 
 (** ** Translation of programs *)
 
-Definition transl_globvar (ty: type) := OK tt.
+Definition transl_globvar (id: ident) (ty: type) := OK tt.
 
 Definition transl_program (p: Clight.program) : res program :=
   transform_partial_program2 (transl_fundef p.(prog_comp_env)) transl_globvar p.
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 4f067fad..8bc97b99 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -12,24 +12,40 @@
 
 (** * Correctness of the translation from Clight to C#minor. *)
 
-Require Import Coqlib.
-Require Import Errors.
-Require Import Maps.
-Require Import Integers.
-Require Import Floats.
-Require Import AST.
-Require Import Values.
-Require Import Events.
-Require Import Memory.
-Require Import Globalenvs.
-Require Import Smallstep.
-Require Import Ctypes.
-Require Import Cop.
-Require Import Clight.
-Require Import Cminor.
-Require Import Csharpminor.
+Require Import Coqlib Errors Maps Integers Floats.
+Require Import AST Linking.
+Require Import Values Events Memory Globalenvs Smallstep.
+Require Import Ctypes Cop Clight Cminor Csharpminor.
 Require Import Cshmgen.
 
+(** * Relational specification of the transformation *)
+
+Inductive match_fundef (p: Clight.program) : Clight.fundef -> Csharpminor.fundef -> Prop :=
+  | match_fundef_internal: forall f tf,
+      transl_function p.(prog_comp_env) f = OK tf ->
+      match_fundef p (Ctypes.Internal f) (AST.Internal tf)
+  | match_fundef_external: forall ef args res cc,
+      ef_sig ef = signature_of_type args res cc ->
+      match_fundef p (Ctypes.External ef args res cc) (AST.External ef).
+
+Definition match_varinfo (v: type) (tv: unit) := True.
+
+Definition match_prog (p: Clight.program) (tp: Csharpminor.program) : Prop :=
+  match_program_gen match_fundef match_varinfo p p tp.
+
+Lemma transf_program_match:
+  forall p tp, transl_program p = OK tp -> match_prog p tp.
+Proof.
+  unfold transl_program; intros.
+  eapply match_transform_partial_program2. 
+  eexact H.
+- intros. destruct f; simpl in H0.
++ monadInv H0. constructor; auto.
++ destruct (signature_eq (ef_sig e) (signature_of_type t t0 c)); inv H0.
+  constructor; auto.
+- intros; red; auto.
+Qed.
+
 (** * Properties of operations over types *)
 
 Remark transl_params_types:
@@ -41,21 +57,20 @@ Qed.
 
 Lemma transl_fundef_sig1:
   forall ce f tf args res cc,
-  transl_fundef ce f = OK tf ->
+  match_fundef ce f tf ->
   classify_fun (type_of_fundef f) = fun_case_f args res cc ->
   funsig tf = signature_of_type args res cc.
 Proof.
-  intros. destruct f; simpl in *.
-  monadInv H. monadInv EQ. simpl. inversion H0.
+  intros. inv H.
+- monadInv H1. simpl. inversion H0.
   unfold signature_of_function, signature_of_type.
   f_equal. apply transl_params_types.
-  destruct (signature_eq (ef_sig e) (signature_of_type t t0 c)); inv H.
-  simpl. congruence.
+- simpl in H0. unfold funsig. congruence.
 Qed.
 
 Lemma transl_fundef_sig2:
   forall ce f tf args res cc,
-  transl_fundef ce f = OK tf ->
+  match_fundef ce f tf ->
   type_of_fundef f = Tfunction args res cc ->
   funsig tf = signature_of_type args res cc.
 Proof.
@@ -63,15 +78,73 @@ Proof.
   rewrite H0; reflexivity.
 Qed.
 
+Lemma transl_sizeof:
+  forall (cunit prog: Clight.program) t sz,
+  linkorder cunit prog ->
+  sizeof cunit.(prog_comp_env) t = OK sz ->
+  sz = Ctypes.sizeof prog.(prog_comp_env) t.
+Proof.
+  intros. destruct H.
+  unfold sizeof in H0. destruct (complete_type (prog_comp_env cunit) t) eqn:C; inv H0.
+  symmetry. apply Ctypes.sizeof_stable; auto.
+Qed.
+
+Lemma transl_alignof:
+  forall (cunit prog: Clight.program) t al,
+  linkorder cunit prog ->
+  alignof cunit.(prog_comp_env) t = OK al ->
+  al = Ctypes.alignof prog.(prog_comp_env) t.
+Proof.
+  intros. destruct H.
+  unfold alignof in H0. destruct (complete_type (prog_comp_env cunit) t) eqn:C; inv H0.
+  symmetry. apply Ctypes.alignof_stable; auto.
+Qed.
+
+Lemma transl_alignof_blockcopy:
+  forall (cunit prog: Clight.program) t sz,
+  linkorder cunit prog ->
+  sizeof cunit.(prog_comp_env) t = OK sz ->
+  sz = Ctypes.sizeof prog.(prog_comp_env) t /\
+  alignof_blockcopy cunit.(prog_comp_env) t = alignof_blockcopy prog.(prog_comp_env) t.
+Proof.
+  intros. destruct H.
+  unfold sizeof in H0. destruct (complete_type (prog_comp_env cunit) t) eqn:C; inv H0.
+  split. 
+- symmetry. apply Ctypes.sizeof_stable; auto.
+- revert C. induction t; simpl; auto;
+  destruct (prog_comp_env cunit)!i as [co|] eqn:X; try discriminate; erewrite H1 by eauto; auto.
+Qed.
+
+Lemma field_offset_stable:
+  forall (cunit prog: Clight.program) id co f,
+  linkorder cunit prog ->
+  cunit.(prog_comp_env)!id = Some co ->
+  prog.(prog_comp_env)!id = Some co /\ 
+  field_offset prog.(prog_comp_env) f (co_members co) = field_offset cunit.(prog_comp_env) f (co_members co).
+Proof.
+  intros. 
+  assert (C: composite_consistent cunit.(prog_comp_env) co).
+  { apply build_composite_env_consistent with cunit.(prog_types) id; auto.
+    apply prog_comp_env_eq. }
+  destruct H as [_ A].
+  split. auto. generalize (co_consistent_complete _ _ C).
+  unfold field_offset. generalize 0. induction (co_members co) as [ | [f1 t1] m]; simpl; intros.
+- auto.
+- InvBooleans.
+  rewrite ! (alignof_stable _ _ A) by auto.
+  rewrite ! (sizeof_stable _ _ A) by auto.
+  destruct (ident_eq f f1); eauto.
+Qed. 
+
 (** * Properties of the translation functions *)
 
 (** Transformation of expressions and statements. *)
 
 Lemma transl_expr_lvalue:
-  forall ge e le m a loc ofs ta,
+  forall ge e le m a loc ofs ce ta,
   Clight.eval_lvalue ge e le m a loc ofs ->
-  transl_expr ge a = OK ta ->
-  (exists tb, transl_lvalue ge a = OK tb /\ make_load tb (typeof a) = OK ta).
+  transl_expr ce a = OK ta ->
+  (exists tb, transl_lvalue ce a = OK tb /\ make_load tb (typeof a) = OK ta).
 Proof.
   intros until ta; intros EVAL TR. inv EVAL; simpl in TR.
   (* var local *)
@@ -140,7 +213,8 @@ Qed.
 
 Section CONSTRUCTORS.
 
-Variable ce: composite_env.
+Variables cunit prog: Clight.program.
+Hypothesis LINK: linkorder cunit prog.
 Variable ge: genv.
 
 Lemma make_intconst_correct:
@@ -487,27 +561,33 @@ End MAKE_BIN.
 
 Hint Extern 2 (@eq (option val) _ _) => (simpl; reflexivity) : cshm.
 
-Lemma make_add_correct: binary_constructor_correct (make_add ce) (sem_add ce).
+Lemma make_add_correct: binary_constructor_correct (make_add cunit.(prog_comp_env)) (sem_add prog.(prog_comp_env)).
 Proof.
   red; unfold make_add, sem_add;
   intros until m; intros SEM MAKE EV1 EV2;
-  destruct (classify_add tya tyb); inv MAKE.
-- destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
-- destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
-- destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
-- destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
+  destruct (classify_add tya tyb); try (monadInv MAKE).
+- rewrite (transl_sizeof _ _ _ _ LINK EQ).
+  destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
+- rewrite (transl_sizeof _ _ _ _ LINK EQ).
+  destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
+- rewrite (transl_sizeof _ _ _ _ LINK EQ).
+  destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
+- rewrite (transl_sizeof _ _ _ _ LINK EQ).
+  destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
 - eapply make_binarith_correct; eauto; intros; auto.
 Qed.
 
-Lemma make_sub_correct: binary_constructor_correct (make_sub ce) (sem_sub ce).
+Lemma make_sub_correct: binary_constructor_correct (make_sub cunit.(prog_comp_env)) (sem_sub prog.(prog_comp_env)).
 Proof.
   red; unfold make_sub, sem_sub;
   intros until m; intros SEM MAKE EV1 EV2;
-  destruct (classify_sub tya tyb); inv MAKE.
-- destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
-- destruct va; try discriminate; destruct vb; inv SEM.
+  destruct (classify_sub tya tyb); try (monadInv MAKE).
+- rewrite (transl_sizeof _ _ _ _ LINK EQ).
+  destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
+- rewrite (transl_sizeof _ _ _ _ LINK EQ).
+  destruct va; try discriminate; destruct vb; inv SEM.
   destruct (eq_block b0 b1); try discriminate.
-  set (sz := sizeof ce ty) in *.
+  set (sz := Ctypes.sizeof (prog_comp_env prog) ty) in *.
   destruct (zlt 0 sz); try discriminate.
   destruct (zle sz Int.max_signed); simpl in H0; inv H0.
   econstructor; eauto with cshm.
@@ -519,7 +599,8 @@ Proof.
   predSpec Int.eq Int.eq_spec (Int.repr sz) Int.mone.
   rewrite H0 in E; rewrite Int.signed_mone in E; omegaContradiction.
   rewrite andb_false_r; auto.
-- destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
+- rewrite (transl_sizeof _ _ _ _ LINK EQ).
+  destruct va; try discriminate; destruct vb; inv SEM; eauto with cshm.
 - eapply make_binarith_correct; eauto; intros; auto.
 Qed.
 
@@ -673,8 +754,8 @@ Qed.
 
 Lemma transl_binop_correct:
   forall op a tya b tyb c va vb v e le m,
-  transl_binop ce op a tya b tyb = OK c ->
-  sem_binary_operation ce op va tya vb tyb m = Some v ->
+  transl_binop cunit.(prog_comp_env) op a tya b tyb = OK c ->
+  sem_binary_operation prog.(prog_comp_env) op va tya vb tyb m = Some v ->
   eval_expr ge e le m a va ->
   eval_expr ge e le m b vb ->
   eval_expr ge e le m c v.
@@ -716,15 +797,18 @@ Proof.
 Qed.
 
 Lemma make_memcpy_correct:
-  forall ce f dst src ty k e le m b ofs v m',
+  forall f dst src ty k e le m b ofs v m' s,
   eval_expr ge e le m dst (Vptr b ofs) ->
   eval_expr ge e le m src v ->
-  assign_loc ce ty m b ofs v m' ->
+  assign_loc prog.(prog_comp_env) ty m b ofs v m' ->
   access_mode ty = By_copy ->
-  step ge (State f (make_memcpy ce dst src ty) k e le m) E0 (State f Sskip k e le m').
+  make_memcpy cunit.(prog_comp_env) dst src ty = OK s ->
+  step ge (State f s k e le m) E0 (State f Sskip k e le m').
 Proof.
   intros. inv H1; try congruence.
-  unfold make_memcpy. change le with (set_optvar None Vundef le) at 2.
+  monadInv H3. 
+  exploit transl_alignof_blockcopy. eexact LINK. eauto. intros [A B]. rewrite A, B.
+  change le with (set_optvar None Vundef le) at 2.
   econstructor.
   econstructor. eauto. econstructor. eauto. constructor.
   econstructor; eauto.
@@ -735,10 +819,10 @@ Qed.
 
 Lemma make_store_correct:
   forall addr ty rhs code e le m b ofs v m' f k,
-  make_store ce addr ty rhs = OK code ->
+  make_store cunit.(prog_comp_env) addr ty rhs = OK code ->
   eval_expr ge e le m addr (Vptr b ofs) ->
   eval_expr ge e le m rhs v ->
-  assign_loc ce ty m b ofs v m' ->
+  assign_loc prog.(prog_comp_env) ty m b ofs v m' ->
   step ge (State f code k e le m) E0 (State f Sskip k e le m').
 Proof.
   unfold make_store. intros until k; intros MKSTORE EV1 EV2 ASSIGN.
@@ -747,8 +831,8 @@ Proof.
   rewrite H in MKSTORE; inv MKSTORE.
   econstructor; eauto.
   (* by copy *)
-  rewrite H in MKSTORE; inv MKSTORE.
-  eapply make_memcpy_correct; eauto.
+  rewrite H in MKSTORE.
+  eapply make_memcpy_correct with (b := b) (v := Vptr b' ofs'); eauto.
 Qed.
 
 End CONSTRUCTORS.
@@ -759,34 +843,30 @@ Section CORRECTNESS.
 
 Variable prog: Clight.program.
 Variable tprog: Csharpminor.program.
-Hypothesis TRANSL: transl_program prog = OK tprog.
+Hypothesis TRANSL: match_prog prog tprog.
 
 Let ge := globalenv prog.
 Let tge := Genv.globalenv tprog.
 
 Lemma symbols_preserved:
   forall s, Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof (Genv.find_symbol_transf_partial2 (transl_fundef ge) transl_globvar _ TRANSL).
+Proof (Genv.find_symbol_match TRANSL).
+
+Lemma senv_preserved:
+  Senv.equiv ge tge.
+Proof (Genv.senv_match TRANSL).
 
-Lemma public_preserved:
-  forall s, Genv.public_symbol tge s = Genv.public_symbol ge s.
-Proof (Genv.public_symbol_transf_partial2 (transl_fundef ge) transl_globvar _ TRANSL).
+Lemma function_ptr_translated:
+  forall v f,
+  Genv.find_funct_ptr ge v = Some f ->
+  exists cu tf, Genv.find_funct_ptr tge v = Some tf /\ match_fundef cu f tf /\ linkorder cu prog.
+Proof (Genv.find_funct_ptr_match TRANSL).
 
 Lemma functions_translated:
   forall v f,
   Genv.find_funct ge v = Some f ->
-  exists tf, Genv.find_funct tge v = Some tf /\ transl_fundef ge f = OK tf.
-Proof (Genv.find_funct_transf_partial2 (transl_fundef ge) transl_globvar _ TRANSL).
-
-Lemma function_ptr_translated:
-  forall b f,
-  Genv.find_funct_ptr ge b = Some f ->
-  exists tf, Genv.find_funct_ptr tge b = Some tf /\ transl_fundef ge f = OK tf.
-Proof (Genv.find_funct_ptr_transf_partial2 (transl_fundef ge) transl_globvar _ TRANSL).
-
-Lemma block_is_volatile_preserved:
-  forall b, Genv.block_is_volatile tge b = Genv.block_is_volatile ge b.
-Proof (Genv.block_is_volatile_transf_partial2 (transl_fundef ge) transl_globvar _ TRANSL).
+  exists cu tf, Genv.find_funct tge v = Some tf /\ match_fundef cu f tf /\ linkorder cu prog.
+Proof (Genv.find_funct_match TRANSL).
 
 (** * Matching between environments *)
 
@@ -797,7 +877,7 @@ Record match_env (e: Clight.env) (te: Csharpminor.env) : Prop :=
   mk_match_env {
     me_local:
       forall id b ty,
-      e!id = Some (b, ty) -> te!id = Some(b, sizeof ge ty);
+      e!id = Some (b, ty) -> te!id = Some(b, Ctypes.sizeof ge ty);
     me_local_inv:
       forall id b sz,
       te!id = Some (b, sz) -> exists ty, e!id = Some(b, ty)
@@ -821,13 +901,13 @@ Proof.
   intros.
   set (R := fun (x: (block * type)) (y: (block * Z)) =>
          match x, y with
-         | (b1, ty), (b2, sz) => b2 = b1 /\ sz = sizeof ge ty
+         | (b1, ty), (b2, sz) => b2 = b1 /\ sz = Ctypes.sizeof ge ty
          end).
   assert (list_forall2
             (fun i_x i_y => fst i_x = fst i_y /\ R (snd i_x) (snd i_y))
             (PTree.elements e) (PTree.elements te)).
   apply PTree.elements_canonical_order.
-  intros id [b ty] GET. exists (b, sizeof ge ty); split. eapply me_local; eauto. red; auto.
+  intros id [b ty] GET. exists (b, Ctypes.sizeof ge ty); split. eapply me_local; eauto. red; auto.
   intros id [b sz] GET. exploit me_local_inv; eauto. intros [ty EQ].
   exploit me_local; eauto. intros EQ1.
   exists (b, ty); split. auto. red; split; congruence.
@@ -863,17 +943,21 @@ Qed.
   local variables and initialization of the parameters. *)
 
 Lemma match_env_alloc_variables:
-  forall e1 m1 vars e2 m2,
-  Clight.alloc_variables ge e1 m1 vars e2 m2 ->
-  forall te1,
+  forall cunit, linkorder cunit prog ->
+  forall e1 m1 vars e2 m2, Clight.alloc_variables ge e1 m1 vars e2 m2 ->
+  forall tvars te1,
+  mmap (transl_var cunit.(prog_comp_env)) vars = OK tvars ->
   match_env e1 te1 ->
   exists te2,
-  Csharpminor.alloc_variables te1 m1 (map (transl_var ge) vars) te2 m2
+  Csharpminor.alloc_variables te1 m1 tvars te2 m2
   /\ match_env e2 te2.
 Proof.
-  induction 1; intros; simpl.
-  exists te1; split. constructor. auto.
-  exploit (IHalloc_variables (PTree.set id (b1, sizeof ge ty) te1)).
+  induction 2; simpl; intros.
+- inv H0. exists te1; split. constructor. auto.
+- monadInv H2. monadInv EQ. simpl in *. 
+  exploit transl_sizeof. eexact H. eauto. intros SZ; rewrite SZ. 
+  exploit (IHalloc_variables x0 (PTree.set id (b1, Ctypes.sizeof ge ty) te1)).
+  auto.
   constructor.
     (* me_local *)
     intros until ty0. repeat rewrite PTree.gsspec.
@@ -903,6 +987,16 @@ Proof.
   destruct a as [id ty]. destruct vals; try discriminate. auto.
 Qed.
 
+Lemma transl_vars_names:
+  forall ce vars tvars,
+  mmap (transl_var ce) vars = OK tvars ->
+  map fst tvars = var_names vars.
+Proof.
+  intros. exploit mmap_inversion; eauto. generalize vars tvars. induction 1; simpl.
+- auto.
+- monadInv H0. simpl; congruence.
+Qed.
+
 (** * Proof of semantic preservation *)
 
 (** ** Semantic preservation for expressions *)
@@ -929,6 +1023,8 @@ Qed.
 
 Section EXPR.
 
+Variable cunit: Clight.program.
+Hypothesis LINK: linkorder cunit prog.
 Variable e: Clight.env.
 Variable le: temp_env.
 Variable m: mem.
@@ -938,11 +1034,11 @@ Hypothesis MENV: match_env e te.
 Lemma transl_expr_lvalue_correct:
   (forall a v,
    Clight.eval_expr ge e le m a v ->
-   forall ta (TR: transl_expr ge a = OK ta) ,
+   forall ta (TR: transl_expr cunit.(prog_comp_env) a = OK ta) ,
    Csharpminor.eval_expr tge te le m ta v)
 /\(forall a b ofs,
    Clight.eval_lvalue ge e le m a b ofs ->
-   forall ta (TR: transl_lvalue ge a = OK ta),
+   forall ta (TR: transl_lvalue cunit.(prog_comp_env) a = OK ta),
    Csharpminor.eval_expr tge te le m ta (Vptr b ofs)).
 Proof.
   apply eval_expr_lvalue_ind; intros; try (monadInv TR).
@@ -965,9 +1061,9 @@ Proof.
 (* cast *)
   eapply make_cast_correct; eauto.
 (* sizeof *)
-  apply make_intconst_correct.
+  rewrite (transl_sizeof _ _ _ _ LINK EQ). apply make_intconst_correct.
 (* alignof *)
-  apply make_intconst_correct.
+  rewrite (transl_alignof _ _ _ _ LINK EQ). apply make_intconst_correct.
 (* rvalue out of lvalue *)
   exploit transl_expr_lvalue; eauto. intros [tb [TRLVAL MKLOAD]].
   eapply make_load_correct; eauto.
@@ -981,11 +1077,13 @@ Proof.
 (* deref *)
   simpl in TR. eauto.
 (* field struct *)
-  change (prog_comp_env prog) with (genv_cenv ge) in EQ0.
-  unfold make_field_access in EQ0; rewrite H1, H2 in EQ0; monadInv EQ0.
+  unfold make_field_access in EQ0. rewrite H1 in EQ0. 
+  destruct (prog_comp_env cunit)!id as [co'|] eqn:CO; monadInv EQ0.
+  exploit field_offset_stable. eexact LINK. eauto. instantiate (1 := i). intros [A B].
+  rewrite <- B in EQ1. 
   eapply eval_Ebinop; eauto.
   apply make_intconst_correct.
-  simpl. congruence.
+  simpl. unfold ge in *; simpl in *. congruence.
 (* field union *)
   unfold make_field_access in EQ0; rewrite H1 in EQ0; monadInv EQ0.
   auto.
@@ -994,21 +1092,21 @@ Qed.
 Lemma transl_expr_correct:
    forall a v,
    Clight.eval_expr ge e le m a v ->
-   forall ta, transl_expr ge a = OK ta ->
+   forall ta, transl_expr cunit.(prog_comp_env) a = OK ta ->
    Csharpminor.eval_expr tge te le m ta v.
 Proof (proj1 transl_expr_lvalue_correct).
 
 Lemma transl_lvalue_correct:
    forall a b ofs,
    Clight.eval_lvalue ge e le m a b ofs ->
-   forall ta, transl_lvalue ge a = OK ta ->
+   forall ta, transl_lvalue cunit.(prog_comp_env) a = OK ta ->
    Csharpminor.eval_expr tge te le m ta (Vptr b ofs).
 Proof (proj2 transl_expr_lvalue_correct).
 
 Lemma transl_arglist_correct:
   forall al tyl vl,
   Clight.eval_exprlist ge e le m al tyl vl ->
-  forall tal, transl_arglist ge al tyl = OK tal ->
+  forall tal, transl_arglist cunit.(prog_comp_env) al tyl = OK tal ->
   Csharpminor.eval_exprlist tge te le m tal vl.
 Proof.
   induction 1; intros.
@@ -1062,71 +1160,75 @@ Proof.
   apply star_refl.
 Qed.
 
-Inductive match_cont: type -> nat -> nat -> Clight.cont -> Csharpminor.cont -> Prop :=
-  | match_Kstop: forall tyret nbrk ncnt,
-      match_cont tyret nbrk ncnt Clight.Kstop Kstop
-  | match_Kseq: forall tyret nbrk ncnt s k ts tk,
-      transl_statement ge tyret nbrk ncnt s = OK ts ->
-      match_cont tyret nbrk ncnt k tk ->
-      match_cont tyret nbrk ncnt
+Inductive match_cont: composite_env -> type -> nat -> nat -> Clight.cont -> Csharpminor.cont -> Prop :=
+  | match_Kstop: forall ce tyret nbrk ncnt,
+      match_cont tyret ce nbrk ncnt Clight.Kstop Kstop
+  | match_Kseq: forall ce tyret nbrk ncnt s k ts tk,
+      transl_statement ce tyret nbrk ncnt s = OK ts ->
+      match_cont ce tyret nbrk ncnt k tk ->
+      match_cont ce tyret nbrk ncnt
                  (Clight.Kseq s k)
                  (Kseq ts tk)
-  | match_Kloop1: forall tyret s1 s2 k ts1 ts2 nbrk ncnt tk,
-      transl_statement ge tyret 1%nat 0%nat s1 = OK ts1 ->
-      transl_statement ge tyret 0%nat (S ncnt) s2 = OK ts2 ->
-      match_cont tyret nbrk ncnt k tk ->
-      match_cont tyret 1%nat 0%nat
+  | match_Kloop1: forall ce tyret s1 s2 k ts1 ts2 nbrk ncnt tk,
+      transl_statement ce tyret 1%nat 0%nat s1 = OK ts1 ->
+      transl_statement ce tyret 0%nat (S ncnt) s2 = OK ts2 ->
+      match_cont ce tyret nbrk ncnt k tk ->
+      match_cont ce tyret 1%nat 0%nat
                  (Clight.Kloop1 s1 s2 k)
                  (Kblock (Kseq ts2 (Kseq (Sloop (Sseq (Sblock ts1) ts2)) (Kblock tk))))
-  | match_Kloop2: forall tyret s1 s2 k ts1 ts2 nbrk ncnt tk,
-      transl_statement ge tyret 1%nat 0%nat s1 = OK ts1 ->
-      transl_statement ge tyret 0%nat (S ncnt) s2 = OK ts2 ->
-      match_cont tyret nbrk ncnt k tk ->
-      match_cont tyret 0%nat (S ncnt)
+  | match_Kloop2: forall ce tyret s1 s2 k ts1 ts2 nbrk ncnt tk,
+      transl_statement ce tyret 1%nat 0%nat s1 = OK ts1 ->
+      transl_statement ce tyret 0%nat (S ncnt) s2 = OK ts2 ->
+      match_cont ce tyret nbrk ncnt k tk ->
+      match_cont ce tyret 0%nat (S ncnt)
                  (Clight.Kloop2 s1 s2 k)
                  (Kseq (Sloop (Sseq (Sblock ts1) ts2)) (Kblock tk))
-  | match_Kswitch: forall tyret nbrk ncnt k tk,
-      match_cont tyret nbrk ncnt k tk ->
-      match_cont tyret 0%nat (S ncnt)
+  | match_Kswitch: forall ce tyret nbrk ncnt k tk,
+      match_cont ce tyret nbrk ncnt k tk ->
+      match_cont ce tyret 0%nat (S ncnt)
                  (Clight.Kswitch k)
                  (Kblock tk)
-  | match_Kcall_some: forall tyret nbrk ncnt nbrk' ncnt' f e k id tf te le tk,
-      transl_function ge f = OK tf ->
+  | match_Kcall: forall ce tyret nbrk ncnt nbrk' ncnt' f e k id tf te le tk cu,
+      linkorder cu prog ->
+      transl_function cu.(prog_comp_env) f = OK tf ->
       match_env e te ->
-      match_cont (Clight.fn_return f) nbrk' ncnt' k tk ->
-      match_cont tyret nbrk ncnt
+      match_cont cu.(prog_comp_env) (Clight.fn_return f) nbrk' ncnt' k tk ->
+      match_cont ce tyret nbrk ncnt
                  (Clight.Kcall id f e le k)
                  (Kcall id tf te le tk).
 
 Inductive match_states: Clight.state -> Csharpminor.state -> Prop :=
   | match_state:
-      forall f nbrk ncnt s k e le m tf ts tk te ts' tk'
-          (TRF: transl_function ge f = OK tf)
-          (TR: transl_statement ge (Clight.fn_return f) nbrk ncnt s = OK ts)
+      forall f nbrk ncnt s k e le m tf ts tk te ts' tk' cu
+          (LINK: linkorder cu prog)
+          (TRF: transl_function cu.(prog_comp_env) f = OK tf)
+          (TR: transl_statement cu.(prog_comp_env) (Clight.fn_return f) nbrk ncnt s = OK ts)
           (MTR: match_transl ts tk ts' tk')
           (MENV: match_env e te)
-          (MK: match_cont (Clight.fn_return f) nbrk ncnt k tk),
+          (MK: match_cont cu.(prog_comp_env) (Clight.fn_return f) nbrk ncnt k tk),
       match_states (Clight.State f s k e le m)
                    (State tf ts' tk' te le m)
   | match_callstate:
-      forall fd args k m tfd tk targs tres cconv
-          (TR: transl_fundef ge fd = OK tfd)
-          (MK: match_cont Tvoid 0%nat 0%nat k tk)
+      forall fd args k m tfd tk targs tres cconv cu ce
+          (LINK: linkorder cu prog)
+          (TR: match_fundef cu fd tfd)
+          (MK: match_cont ce Tvoid 0%nat 0%nat k tk)
           (ISCC: Clight.is_call_cont k)
           (TY: type_of_fundef fd = Tfunction targs tres cconv),
       match_states (Clight.Callstate fd args k m)
                    (Callstate tfd args tk m)
   | match_returnstate:
-      forall res k m tk
-          (MK: match_cont Tvoid 0%nat 0%nat k tk),
+      forall res k m tk ce
+          (MK: match_cont ce Tvoid 0%nat 0%nat k tk),
       match_states (Clight.Returnstate res k m)
                    (Returnstate res tk m).
 
 Remark match_states_skip:
-  forall f e le te nbrk ncnt k tf tk m,
-  transl_function ge f = OK tf ->
+  forall f e le te nbrk ncnt k tf tk m cu,
+  linkorder cu prog ->
+  transl_function cu.(prog_comp_env) f = OK tf ->
   match_env e te ->
-  match_cont (Clight.fn_return f) nbrk ncnt k tk ->
+  match_cont cu.(prog_comp_env) (Clight.fn_return f) nbrk ncnt k tk ->
   match_states (Clight.State f Clight.Sskip k e le m) (State tf Sskip tk te le m).
 Proof.
   intros. econstructor; eauto. simpl; reflexivity. constructor.
@@ -1135,89 +1237,90 @@ Qed.
 (** Commutation between label resolution and compilation *)
 
 Section FIND_LABEL.
+Variable ce: composite_env.
 Variable lbl: label.
 Variable tyret: type.
 
 Lemma transl_find_label:
   forall s nbrk ncnt k ts tk
-  (TR: transl_statement ge tyret nbrk ncnt s = OK ts)
-  (MC: match_cont tyret nbrk ncnt k tk),
+  (TR: transl_statement ce tyret nbrk ncnt s = OK ts)
+  (MC: match_cont ce tyret nbrk ncnt k tk),
   match Clight.find_label lbl s k with
   | None => find_label lbl ts tk = None
   | Some (s', k') =>
       exists ts', exists tk', exists nbrk', exists ncnt',
       find_label lbl ts tk = Some (ts', tk')
-      /\ transl_statement ge tyret nbrk' ncnt' s' = OK ts'
-      /\ match_cont tyret nbrk' ncnt' k' tk'
+      /\ transl_statement ce tyret nbrk' ncnt' s' = OK ts'
+      /\ match_cont ce tyret nbrk' ncnt' k' tk'
   end
 
 with transl_find_label_ls:
   forall ls nbrk ncnt k tls tk
-  (TR: transl_lbl_stmt ge tyret nbrk ncnt ls = OK tls)
-  (MC: match_cont tyret nbrk ncnt k tk),
+  (TR: transl_lbl_stmt ce tyret nbrk ncnt ls = OK tls)
+  (MC: match_cont ce tyret nbrk ncnt k tk),
   match Clight.find_label_ls lbl ls k with
   | None => find_label_ls lbl tls tk = None
   | Some (s', k') =>
       exists ts', exists tk', exists nbrk', exists ncnt',
       find_label_ls lbl tls tk = Some (ts', tk')
-      /\ transl_statement ge tyret nbrk' ncnt' s' = OK ts'
-      /\ match_cont tyret nbrk' ncnt' k' tk'
+      /\ transl_statement ce tyret nbrk' ncnt' s' = OK ts'
+      /\ match_cont ce tyret nbrk' ncnt' k' tk'
   end.
 
 Proof.
-  intro s; case s; intros; try (monadInv TR); simpl.
-(* skip *)
+* intro s; case s; intros; try (monadInv TR); simpl.
+- (* skip *)
   auto.
-(* assign *)
+- (* assign *)
   unfold make_store, make_memcpy in EQ3.
-  destruct (access_mode (typeof e)); inv EQ3; auto.
-(* set *)
+  destruct (access_mode (typeof e)); monadInv EQ3; auto.
+- (* set *)
   auto.
-(* call *)
+- (* call *)
   simpl in TR. destruct (classify_fun (typeof e)); monadInv TR. auto.
-(* builtin *)
+- (* builtin *)
   auto.
-(* seq *)
+- (* seq *)
   exploit (transl_find_label s0 nbrk ncnt (Clight.Kseq s1 k)); eauto. constructor; eauto.
   destruct (Clight.find_label lbl s0 (Clight.Kseq s1 k)) as [[s' k'] | ].
   intros [ts' [tk' [nbrk' [ncnt' [A [B C]]]]]].
   rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto.
   intro. rewrite H. eapply transl_find_label; eauto.
-(* ifthenelse *)
+- (* ifthenelse *)
   exploit (transl_find_label s0); eauto.
   destruct (Clight.find_label lbl s0 k) as [[s' k'] | ].
   intros [ts' [tk' [nbrk' [ncnt' [A [B C]]]]]].
   rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto.
   intro. rewrite H. eapply transl_find_label; eauto.
-(* loop *)
+- (* loop *)
   exploit (transl_find_label s0 1%nat 0%nat (Kloop1 s0 s1 k)); eauto. econstructor; eauto.
   destruct (Clight.find_label lbl s0 (Kloop1 s0 s1 k)) as [[s' k'] | ].
   intros [ts' [tk' [nbrk' [ncnt' [A [B C]]]]]].
   rewrite A. exists ts'; exists tk'; exists nbrk'; exists ncnt'; auto.
   intro. rewrite H.
   eapply transl_find_label; eauto. econstructor; eauto.
-(* break *)
+- (* break *)
   auto.
-(* continue *)
+- (* continue *)
   auto.
-(* return *)
+- (* return *)
   simpl in TR. destruct o; monadInv TR. auto. auto.
-(* switch *)
+- (* switch *)
   assert (exists b, ts = Sblock (Sswitch b x x0)).
   { destruct (classify_switch (typeof e)); inv EQ2; econstructor; eauto. }
   destruct H as [b EQ3]; rewrite EQ3; simpl.
   eapply transl_find_label_ls with (k := Clight.Kswitch k); eauto. econstructor; eauto.
-(* label *)
+- (* label *)
   destruct (ident_eq lbl l).
   exists x; exists tk; exists nbrk; exists ncnt; auto.
   eapply transl_find_label; eauto.
-(* goto *)
+- (* goto *)
   auto.
 
-  intro ls; case ls; intros; monadInv TR; simpl.
-(* nil *)
+* intro ls; case ls; intros; monadInv TR; simpl.
+- (* nil *)
   auto.
-(* cons *)
+- (* cons *)
   exploit (transl_find_label s nbrk ncnt (Clight.Kseq (seq_of_labeled_statement l) k)); eauto.
   econstructor; eauto. apply transl_lbl_stmt_2; eauto.
   destruct (Clight.find_label lbl s (Clight.Kseq (seq_of_labeled_statement l) k)) as [[s' k'] | ].
@@ -1232,9 +1335,9 @@ End FIND_LABEL.
 (** Properties of call continuations *)
 
 Lemma match_cont_call_cont:
-  forall tyret' nbrk' ncnt' tyret nbrk ncnt k tk,
-  match_cont tyret nbrk ncnt k tk ->
-  match_cont tyret' nbrk' ncnt' (Clight.call_cont k) (call_cont tk).
+  forall ce' tyret' nbrk' ncnt' ce tyret nbrk ncnt k tk,
+  match_cont ce tyret nbrk ncnt k tk ->
+  match_cont ce' tyret' nbrk' ncnt' (Clight.call_cont k) (call_cont tk).
 Proof.
   induction 1; simpl; auto.
   constructor.
@@ -1242,10 +1345,10 @@ Proof.
 Qed.
 
 Lemma match_cont_is_call_cont:
-  forall tyret nbrk ncnt k tk tyret' nbrk' ncnt',
-  match_cont tyret nbrk ncnt k tk ->
+  forall ce tyret nbrk ncnt k tk ce' tyret' nbrk' ncnt',
+  match_cont ce tyret nbrk ncnt k tk ->
   Clight.is_call_cont k ->
-  match_cont tyret' nbrk' ncnt' k tk /\ is_call_cont tk.
+  match_cont ce' tyret' nbrk' ncnt' k tk /\ is_call_cont tk.
 Proof.
   intros. inv H; simpl in H0; try contradiction; simpl.
   split; auto; constructor.
@@ -1261,11 +1364,12 @@ Lemma transl_step:
 Proof.
   induction 1; intros T1 MST; inv MST.
 
-(* assign *)
+- (* assign *)
   monadInv TR.
   assert (SAME: ts' = ts /\ tk' = tk).
-    inversion MTR. auto.
-    subst ts. unfold make_store, make_memcpy in EQ3. destruct (access_mode (typeof a1)); congruence.
+  { inversion MTR. auto.
+    subst ts. unfold make_store, make_memcpy in EQ3.
+    destruct (access_mode (typeof a1)); monadInv EQ3; auto. }
   destruct SAME; subst ts' tk'.
   econstructor; split.
   apply plus_one. eapply make_store_correct; eauto.
@@ -1273,62 +1377,61 @@ Proof.
   eapply transl_expr_correct; eauto.
   eapply match_states_skip; eauto.
 
-(* set *)
+- (* set *)
   monadInv TR. inv MTR. econstructor; split.
   apply plus_one. econstructor. eapply transl_expr_correct; eauto.
   eapply match_states_skip; eauto.
 
-(* call *)
+- (* call *)
   revert TR. simpl. case_eq (classify_fun (typeof a)); try congruence.
   intros targs tres cc CF TR. monadInv TR. inv MTR.
-  exploit functions_translated; eauto. intros [tfd [FIND TFD]].
+  exploit functions_translated; eauto. intros (cu' & tfd & FIND & TFD & LINK').
   rewrite H in CF. simpl in CF. inv CF.
   econstructor; split.
   apply plus_one. econstructor; eauto.
-  exploit transl_expr_correct; eauto.
-  exploit transl_arglist_correct; eauto.
+  eapply transl_expr_correct with (cunit := cu); eauto. 
+  eapply transl_arglist_correct with (cunit := cu); eauto.
   erewrite typlist_of_arglist_eq by eauto.
   eapply transl_fundef_sig1; eauto.
   rewrite H3. auto.
   econstructor; eauto.
-  econstructor; eauto.
+  eapply match_Kcall with (ce := prog_comp_env cu') (cu := cu); eauto.
   simpl. auto.
 
-(* builtin *)
+- (* builtin *)
   monadInv TR. inv MTR.
   econstructor; split.
   apply plus_one. econstructor.
   eapply transl_arglist_correct; eauto.
-  eapply external_call_symbols_preserved_gen with (ge1 := ge).
-  exact symbols_preserved. exact public_preserved. exact block_is_volatile_preserved. eauto.
+  eapply external_call_symbols_preserved with (ge1 := ge). apply senv_preserved. eauto.
   eapply match_states_skip; eauto.
 
-(* seq *)
+- (* seq *)
   monadInv TR. inv MTR.
   econstructor; split.
   apply plus_one. constructor.
   econstructor; eauto. constructor.
   econstructor; eauto.
 
-(* skip seq *)
+- (* skip seq *)
   monadInv TR. inv MTR. inv MK.
   econstructor; split.
   apply plus_one. apply step_skip_seq.
   econstructor; eauto. constructor.
 
-(* continue seq *)
+- (* continue seq *)
   monadInv TR. inv MTR. inv MK.
   econstructor; split.
   apply plus_one. constructor.
   econstructor; eauto. simpl. reflexivity. constructor.
 
-(* break seq *)
+- (* break seq *)
   monadInv TR. inv MTR. inv MK.
   econstructor; split.
   apply plus_one. constructor.
   econstructor; eauto. simpl. reflexivity. constructor.
 
-(* ifthenelse *)
+- (* ifthenelse *)
   monadInv TR. inv MTR.
   exploit make_boolean_correct; eauto.
   exploit transl_expr_correct; eauto.
@@ -1337,7 +1440,7 @@ Proof.
   apply plus_one. apply step_ifthenelse with (v := v) (b := b); auto.
   destruct b; econstructor; eauto; constructor.
 
-(* loop *)
+- (* loop *)
   monadInv TR.
   econstructor; split.
   eapply star_plus_trans. eapply match_transl_step; eauto.
@@ -1347,9 +1450,9 @@ Proof.
   reflexivity. reflexivity. traceEq.
   econstructor; eauto. constructor. econstructor; eauto.
 
-(* skip-or-continue loop *)
+- (* skip-or-continue loop *)
   assert ((ts' = Sskip \/ ts' = Sexit ncnt) /\ tk' = tk).
-    destruct H; subst x; monadInv TR; inv MTR; auto.
+  { destruct H; subst x; monadInv TR; inv MTR; auto. }
   destruct H0. inv MK.
   econstructor; split.
   eapply plus_left.
@@ -1357,7 +1460,7 @@ Proof.
   apply star_one. constructor. traceEq.
   econstructor; eauto. constructor. econstructor; eauto.
 
-(* break loop1 *)
+- (* break loop1 *)
   monadInv TR. inv MTR. inv MK.
   econstructor; split.
   eapply plus_left. constructor.
@@ -1367,16 +1470,15 @@ Proof.
   reflexivity. reflexivity. traceEq.
   eapply match_states_skip; eauto.
 
-(* skip loop2 *)
+- (* skip loop2 *)
   monadInv TR. inv MTR. inv MK.
   econstructor; split.
   apply plus_one. constructor.
   econstructor; eauto.
-Local Opaque ge.
-  simpl. rewrite H5; simpl. rewrite H7; simpl. eauto.
+  simpl. rewrite H6; simpl. rewrite H8; simpl. eauto.
   constructor.
 
-(* break loop2 *)
+- (* break loop2 *)
   monadInv TR. inv MTR. inv MK.
   econstructor; split.
   eapply plus_left. constructor.
@@ -1384,32 +1486,32 @@ Local Opaque ge.
   traceEq.
   eapply match_states_skip; eauto.
 
-(* return none *)
+- (* return none *)
   monadInv TR. inv MTR.
   econstructor; split.
   apply plus_one. constructor.
   eapply match_env_free_blocks; eauto.
-  econstructor; eauto.
+  eapply match_returnstate with (ce := prog_comp_env cu); eauto.
   eapply match_cont_call_cont. eauto.
 
-(* return some *)
+- (* return some *)
   monadInv TR. inv MTR.
   econstructor; split.
   apply plus_one. constructor.
   eapply make_cast_correct; eauto. eapply transl_expr_correct; eauto.
   eapply match_env_free_blocks; eauto.
-  econstructor; eauto.
+  eapply match_returnstate with (ce := prog_comp_env cu); eauto.
   eapply match_cont_call_cont. eauto.
 
-(* skip call *)
+- (* skip call *)
   monadInv TR. inv MTR.
   exploit match_cont_is_call_cont; eauto. intros [A B].
   econstructor; split.
   apply plus_one. apply step_skip_call. auto.
   eapply match_env_free_blocks; eauto.
-  constructor. eauto.
+  eapply match_returnstate with (ce := prog_comp_env cu); eauto.
 
-(* switch *)
+- (* switch *)
   monadInv TR.
   assert (E: exists b, ts = Sblock (Sswitch b x x0) /\ Switch.switch_argument b v n).
   { unfold sem_switch_arg in H0.
@@ -1425,7 +1527,7 @@ Local Opaque ge.
   constructor.
   econstructor. eauto.
 
-(* skip or break switch *)
+- (* skip or break switch *)
   assert ((ts' = Sskip \/ ts' = Sexit nbrk) /\ tk' = tk).
     destruct H; subst x; monadInv TR; inv MTR; auto.
   destruct H0. inv MK.
@@ -1433,57 +1535,54 @@ Local Opaque ge.
   apply plus_one. destruct H0; subst ts'. 2:constructor. constructor.
   eapply match_states_skip; eauto.
 
-
-(* continue switch *)
+- (* continue switch *)
   monadInv TR. inv MTR. inv MK.
   econstructor; split.
   apply plus_one. constructor.
   econstructor; eauto. simpl. reflexivity. constructor.
 
-(* label *)
+- (* label *)
   monadInv TR. inv MTR.
   econstructor; split.
   apply plus_one. constructor.
   econstructor; eauto. constructor.
 
-(* goto *)
+- (* goto *)
   monadInv TR. inv MTR.
   generalize TRF. unfold transl_function. intro TRF'. monadInv TRF'.
-  exploit (transl_find_label lbl). eexact EQ. eapply match_cont_call_cont. eauto.
+  exploit (transl_find_label (prog_comp_env cu) lbl). eexact EQ. eapply match_cont_call_cont. eauto.
   rewrite H.
   intros [ts' [tk'' [nbrk' [ncnt' [A [B C]]]]]].
   econstructor; split.
   apply plus_one. constructor. simpl. eexact A.
   econstructor; eauto. constructor.
 
-(* internal function *)
-  inv H. monadInv TR. monadInv EQ.
+- (* internal function *)
+  inv H. inv TR. monadInv H5. 
   exploit match_cont_is_call_cont; eauto. intros [A B].
   exploit match_env_alloc_variables; eauto.
   apply match_env_empty.
   intros [te1 [C D]].
   econstructor; split.
   apply plus_one. eapply step_internal_function.
-  simpl. rewrite list_map_compose. simpl. assumption.
-  simpl. auto.
-  simpl. auto.
-  simpl. eauto.
+  simpl. erewrite transl_vars_names by eauto. assumption.
+  simpl. assumption.
+  simpl. assumption.
+  simpl; eauto. 
   simpl. rewrite create_undef_temps_match. eapply bind_parameter_temps_match; eauto.
   simpl. econstructor; eauto.
-  unfold transl_function. rewrite EQ0; simpl. auto.
+  unfold transl_function. rewrite EQ; simpl. rewrite EQ1; simpl. auto.
   constructor.
 
-(* external function *)
-  simpl in TR.
-  destruct (signature_eq (ef_sig ef) (signature_of_type targs tres cconv)); inv TR.
+- (* external function *)
+  inv TR.
   exploit match_cont_is_call_cont; eauto. intros [A B].
   econstructor; split.
   apply plus_one. constructor. eauto.
-  eapply external_call_symbols_preserved_gen with (ge1 := ge).
-  exact symbols_preserved. exact public_preserved. exact block_is_volatile_preserved. eauto.
-  econstructor; eauto.
+  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
+  eapply match_returnstate with (ce := ce); eauto.
 
-(* returnstate *)
+- (* returnstate *)
   inv MK.
   econstructor; split.
   apply plus_one. constructor.
@@ -1495,17 +1594,14 @@ Lemma transl_initial_states:
   exists R, initial_state tprog R /\ match_states S R.
 Proof.
   intros. inv H.
-  exploit function_ptr_translated; eauto. intros [tf [A B]].
-  assert (C: Genv.find_symbol tge (AST.prog_main tprog) = Some b).
-    rewrite symbols_preserved. replace (AST.prog_main tprog) with (prog_main prog).
-    auto. symmetry. unfold transl_program in TRANSL.
-    change (prog_main prog) with (AST.prog_main (program_of_program prog)).
-    eapply transform_partial_program2_main; eauto.
-  assert (funsig tf = signature_of_type Tnil type_int32s cc_default).
-    eapply transl_fundef_sig2; eauto.
+  exploit function_ptr_translated; eauto. intros (cu & tf & A & B & C).
+  assert (D: Genv.find_symbol tge (AST.prog_main tprog) = Some b).
+  { destruct TRANSL as (P & Q & R). rewrite Q. rewrite symbols_preserved. auto. }
+  assert (E: funsig tf = signature_of_type Tnil type_int32s cc_default).
+  { eapply transl_fundef_sig2; eauto. }
   econstructor; split.
-  econstructor; eauto. eapply Genv.init_mem_transf_partial2; eauto.
-  econstructor; eauto. constructor; auto. exact I.
+  econstructor; eauto. apply (Genv.init_mem_match TRANSL). eauto.
+  econstructor; eauto. instantiate (1 := prog_comp_env cu). constructor; auto. exact I.
 Qed.
 
 Lemma transl_final_states:
@@ -1519,10 +1615,40 @@ Theorem transl_program_correct:
   forward_simulation (Clight.semantics2 prog) (Csharpminor.semantics tprog).
 Proof.
   eapply forward_simulation_plus.
-  eexact public_preserved.
+  apply senv_preserved.
   eexact transl_initial_states.
   eexact transl_final_states.
   eexact transl_step.
 Qed.
 
 End CORRECTNESS.
+
+(** ** Commutation with linking *)
+
+Instance TransfCshmgenLink : TransfLink match_prog.
+Proof.
+  red; intros. destruct (link_linkorder _ _ _ H) as (LO1 & LO2).
+  generalize H. 
+Local Transparent Ctypes.Linker_program.
+  simpl; unfold link_program.
+  destruct (link (program_of_program p1) (program_of_program p2)) as [pp|] eqn:LP; try discriminate.
+  destruct (lift_option (link (prog_types p1) (prog_types p2))) as [[typs EQ]|P]; try discriminate.
+  destruct (link_build_composite_env (prog_types p1) (prog_types p2) typs
+           (prog_comp_env p1) (prog_comp_env p2) (prog_comp_env_eq p1)
+           (prog_comp_env_eq p2) EQ) as (env & P & Q).
+  intros E.
+  eapply Linking.link_match_program; eauto.
+- intros. 
+Local Transparent Linker_fundef Linking.Linker_fundef.
+  inv H3; inv H4; simpl in H2. 
++ discriminate.
++ destruct ef; inv H2. econstructor; split. simpl; eauto. left; constructor; auto.
++ destruct ef; inv H2. econstructor; split. simpl; eauto. right; constructor; auto.
++ destruct (external_function_eq ef ef0 && typelist_eq args args0 &&
+         type_eq res res0 && calling_convention_eq cc cc0) eqn:E'; inv H2.
+  InvBooleans. subst ef0. econstructor; split. 
+  simpl; rewrite dec_eq_true; eauto.
+  left; constructor. congruence.
+- intros. exists tt. auto.
+- replace (program_of_program p) with pp. auto. inv E; destruct pp; auto.
+Qed.
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index 89d0b2bf..fd7a6b96 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -15,14 +15,9 @@
 
 (** Abstract syntax for the Compcert C language *)
 
-Require Import Coqlib.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import AST.
-Require Import Errors.
-Require Import Ctypes.
-Require Import Cop.
+Require Import Coqlib Maps Integers Floats Errors.
+Require Import AST Linking Values.
+Require Import Ctypes Cop.
 
 (** ** Expressions *)
 
@@ -191,9 +186,7 @@ Definition var_names (vars: list(ident * type)) : list ident :=
 (** Functions can either be defined ([Internal]) or declared as
   external functions ([External]). *)
 
-Inductive fundef : Type :=
-  | Internal: function -> fundef
-  | External: external_function -> typelist -> type -> calling_convention -> fundef.
+Definition fundef := Ctypes.fundef function.
 
 (** The type of a function definition. *)
 
@@ -206,50 +199,15 @@ Definition type_of_fundef (f: fundef) : type :=
   | External id args res cc => Tfunction args res cc
   end.
 
-(** ** Programs *)
+(** ** Programs and compilation units *)
 
-(** A "pre-program", as produced by the elaborator is composed of:
+(** As defined in module [Ctypes], a program, or compilation unit, is
+  composed of:
 - a list of definitions of functions and global variables;
 - the names of functions and global variables that are public (not static);
 - the name of the function that acts as entry point ("main" function).
 - a list of definitions for structure and union names
+- the corresponding composite environment
+- a proof that this environment is consistent with the definitions. *)
 
-A program is composed of the same information, plus the corresponding
-composite environment, and a proof that this environment is consistent
-with the composite definitions. *)
-
-Record pre_program : Type := {
-  pprog_defs: list (ident * globdef fundef type);
-  pprog_public: list ident;
-  pprog_main: ident;
-  pprog_types: list composite_definition
-}.
-
-Record program : Type := {
-  prog_defs: list (ident * globdef fundef type);
-  prog_public: list ident;
-  prog_main: ident;
-  prog_types: list composite_definition;
-  prog_comp_env: composite_env;
-  prog_comp_env_eq: build_composite_env prog_types = OK prog_comp_env
-}.
-
-Definition program_of_program (p: program) : AST.program fundef type :=
-  {| AST.prog_defs := p.(prog_defs);
-     AST.prog_public := p.(prog_public);
-     AST.prog_main := p.(prog_main) |}.
-
-Coercion program_of_program: program >-> AST.program.
-
-Program Definition program_of_pre_program (p: pre_program) : res program :=
-  match build_composite_env p.(pprog_types) with
-  | Error e => Error e
-  | OK ce =>
-      OK {| prog_defs := p.(pprog_defs);
-            prog_public := p.(pprog_public);
-            prog_main := p.(pprog_main);
-            prog_types := p.(pprog_types);
-            prog_comp_env := ce;
-            prog_comp_env_eq := _ |}
-  end.
-
+Definition program := Ctypes.program function.
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
index 78345b42..9faa6d40 100644
--- a/cfrontend/Ctypes.v
+++ b/cfrontend/Ctypes.v
@@ -15,10 +15,8 @@
 
 (** Type expressions for the Compcert C and Clight languages *)
 
-Require Import Coqlib.
-Require Import Maps.
-Require Import AST.
-Require Import Errors.
+Require Import Axioms Coqlib Maps Errors.
+Require Import AST Linking.
 Require Archi.
 
 (** * Syntax of types *)
@@ -157,6 +155,20 @@ Definition members : Type := list (ident * type).
 Inductive composite_definition : Type :=
   Composite (id: ident) (su: struct_or_union) (m: members) (a: attr).
 
+Definition name_composite_def (c: composite_definition) : ident :=
+  match c with Composite id su m a => id end.
+
+Definition composite_def_eq (x y: composite_definition): {x=y} + {x<>y}.
+Proof.
+  decide equality.
+- decide equality. decide equality. apply N.eq_dec. apply bool_dec.
+- apply list_eq_dec. decide equality. apply type_eq. apply ident_eq.
+- decide equality.
+- apply ident_eq.
+Defined.
+
+Global Opaque composite_def_eq. 
+
 (** For type-checking, compilation and semantics purposes, the composite
   definitions are collected in the following [composite_env] environment.
   The [composite] record contains additional information compared with
@@ -960,6 +972,29 @@ Record composite_consistent (env: composite_env) (co: composite) : Prop := {
 Definition composite_env_consistent (env: composite_env) : Prop :=
   forall id co, env!id = Some co -> composite_consistent env co.
 
+Lemma composite_consistent_stable:
+  forall (env env': composite_env)
+         (EXTENDS: forall id co, env!id = Some co -> env'!id = Some co)
+         co,
+  composite_consistent env co -> composite_consistent env' co.
+Proof.
+  intros. destruct H as [A B C D]. constructor. 
+  eapply complete_members_stable; eauto.
+  symmetry; rewrite B. f_equal. apply alignof_composite_stable; auto. 
+  symmetry; rewrite C. f_equal. apply sizeof_composite_stable; auto.
+  symmetry; rewrite D. apply rank_members_stable; auto.
+Qed.
+
+Lemma composite_of_def_consistent:
+  forall env id su m a co,
+  composite_of_def env id su m a = OK co ->
+  composite_consistent env co.
+Proof.
+  unfold composite_of_def; intros. 
+  destruct (env!id); try discriminate. destruct (complete_members env m) eqn:C; inv H.
+  constructor; auto.
+Qed. 
+
 Theorem build_composite_env_consistent:
   forall defs env, build_composite_env defs = OK env -> composite_env_consistent env.
 Proof.
@@ -973,28 +1008,15 @@ Proof.
 - destruct d1; monadInv H.
   eapply IHdefs; eauto.
   set (env1 := PTree.set id x env0) in *.
-  unfold composite_of_def in EQ.
-  destruct (env0!id) eqn:E; try discriminate.
-  destruct (complete_members env0 m) eqn:C; inversion EQ; clear EQ.
+  assert (env0!id = None). 
+  { unfold composite_of_def in EQ. destruct (env0!id). discriminate. auto. }
   assert (forall id1 co1, env0!id1 = Some co1 -> env1!id1 = Some co1).
   { intros. unfold env1. rewrite PTree.gso; auto. congruence. }
-  red; intros. unfold env1 in H2; rewrite PTree.gsspec in H2; destruct (peq id0 id).
+  red; intros. apply composite_consistent_stable with env0; auto.
+  unfold env1 in H2; rewrite PTree.gsspec in H2; destruct (peq id0 id).
 + subst id0. inversion H2; clear H2. subst co.
-(*
-  assert (A: alignof_composite env1 m = alignof_composite env0 m)
-  by (apply alignof_composite_stable; assumption).
-*)
-  rewrite <- H1; constructor; simpl.
-* eapply complete_members_stable; eauto.
-* f_equal. symmetry. apply alignof_composite_stable; auto.
-* f_equal. symmetry. apply sizeof_composite_stable; auto.
-* symmetry. apply rank_members_stable; auto.
-+ exploit H0; eauto. intros [P Q R S].
-  constructor; intros.
-* eapply complete_members_stable; eauto.
-* rewrite Q. f_equal. symmetry. apply alignof_composite_stable; auto.
-* rewrite R. f_equal. symmetry. apply sizeof_composite_stable; auto.
-* rewrite S. symmetry; apply rank_members_stable; auto.
+  eapply composite_of_def_consistent; eauto.
++ eapply H0; eauto. 
 Qed.
 
 (** Moreover, every composite definition is reflected in the composite environment. *)
@@ -1018,6 +1040,29 @@ Proof.
   subst x; auto.
 Qed.
 
+Theorem build_composite_env_domain:
+  forall env defs id co,
+  build_composite_env defs = OK env ->
+  env!id = Some co ->
+  In (Composite id (co_su co) (co_members co) (co_attr co)) defs.
+Proof.
+  intros env0 defs0 id co.
+  assert (REC: forall l env env',
+    add_composite_definitions env l = OK env' ->
+    env'!id = Some co ->
+    env!id = Some co \/ In (Composite id (co_su co) (co_members co) (co_attr co)) l).
+  { induction l; simpl; intros. 
+  - inv H; auto.
+  - destruct a; monadInv H. exploit IHl; eauto.
+    unfold composite_of_def in EQ. destruct (env!id0) eqn:E; try discriminate.
+    destruct (complete_members env m) eqn:C; simplify_eq EQ. clear EQ; intros EQ.
+    rewrite PTree.gsspec. intros [A|A]; auto.
+    destruct (peq id id0); auto.
+    inv A. rewrite <- H1; auto.
+  }
+  intros. exploit REC; eauto. rewrite PTree.gempty. intuition congruence.
+Qed.
+
 (** As a corollay, in a consistent environment, the rank of a composite type
   is strictly greater than the ranks of its member types. *)
 
@@ -1054,3 +1099,441 @@ Proof.
   exploit (rank_type_members ce); eauto.
   omega.
 Qed.
+
+(** * Programs and compilation units *)
+
+(** The definitions in this section are parameterized over a type [F] of 
+  internal function definitions, so that they apply both to CompCert C and to Clight. *)
+
+Set Implicit Arguments.
+
+Section PROGRAMS.
+
+Variable F: Type.
+
+(** Functions can either be defined ([Internal]) or declared as
+  external functions ([External]). *)
+
+Inductive fundef : Type :=
+  | Internal: F -> fundef
+  | External: external_function -> typelist -> type -> calling_convention -> fundef.
+
+(** A program, or compilation unit, is composed of:
+- a list of definitions of functions and global variables;
+- the names of functions and global variables that are public (not static);
+- the name of the function that acts as entry point ("main" function).
+- a list of definitions for structure and union names
+- the corresponding composite environment
+- a proof that this environment is consistent with the definitions. *)
+
+Record program : Type := {
+  prog_defs: list (ident * globdef fundef type);
+  prog_public: list ident;
+  prog_main: ident;
+  prog_types: list composite_definition;
+  prog_comp_env: composite_env;
+  prog_comp_env_eq: build_composite_env prog_types = OK prog_comp_env
+}.
+
+Definition program_of_program (p: program) : AST.program fundef type :=
+  {| AST.prog_defs := p.(prog_defs);
+     AST.prog_public := p.(prog_public);
+     AST.prog_main := p.(prog_main) |}.
+
+Coercion program_of_program: program >-> AST.program.
+
+Program Definition make_program (types: list composite_definition)
+                                (defs: list (ident * globdef fundef type))
+                                (public: list ident)
+                                (main: ident) : res program :=
+  match build_composite_env types with
+  | Error e => Error e
+  | OK ce =>
+      OK {| prog_defs := defs;
+            prog_public := public;
+            prog_main := main;
+            prog_types := types;
+            prog_comp_env := ce;
+            prog_comp_env_eq := _ |}
+  end.
+
+End PROGRAMS.
+
+Arguments External {F} _ _ _ _.
+
+Unset Implicit Arguments.
+
+(** * Separate compilation and linking *)
+
+(** ** Linking types *)
+
+Instance Linker_types : Linker type := {
+  link := fun t1 t2 => if type_eq t1 t2 then Some t1 else None;
+  linkorder := fun t1 t2 => t1 = t2
+}.
+Proof.
+  auto.
+  intros; congruence.
+  intros. destruct (type_eq x y); inv H. auto.
+Defined.
+
+Global Opaque Linker_types.
+
+(** ** Linking composite definitions *)
+
+Definition check_compat_composite (l: list composite_definition) (cd: composite_definition) : bool :=
+  List.forallb
+    (fun cd' =>
+      if ident_eq (name_composite_def cd') (name_composite_def cd) then composite_def_eq cd cd' else true)
+    l.
+
+Definition filter_redefs (l1 l2: list composite_definition) :=
+  let names1 := map name_composite_def l1 in
+  List.filter (fun cd => negb (In_dec ident_eq (name_composite_def cd) names1)) l2.
+
+Definition link_composite_defs (l1 l2: list composite_definition): option (list composite_definition) :=
+  if List.forallb (check_compat_composite l2) l1
+  then Some (l1 ++ filter_redefs l1 l2)
+  else None.
+
+Lemma link_composite_def_inv:
+  forall l1 l2 l,
+  link_composite_defs l1 l2 = Some l ->
+     (forall cd1 cd2, In cd1 l1 -> In cd2 l2 -> name_composite_def cd2 = name_composite_def cd1 -> cd2 = cd1)
+  /\ l = l1 ++ filter_redefs l1 l2
+  /\ (forall x, In x l <-> In x l1 \/ In x l2).
+Proof.
+  unfold link_composite_defs; intros.
+  destruct (forallb (check_compat_composite l2) l1) eqn:C; inv H.
+  assert (A: 
+    forall cd1 cd2, In cd1 l1 -> In cd2 l2 -> name_composite_def cd2 = name_composite_def cd1 -> cd2 = cd1).
+  { rewrite forallb_forall in C. intros.
+    apply C in H. unfold check_compat_composite in H. rewrite forallb_forall in H. 
+    apply H in H0. rewrite H1, dec_eq_true in H0. symmetry; eapply proj_sumbool_true; eauto. }
+  split. auto. split. auto. 
+  unfold filter_redefs; intros. 
+  rewrite in_app_iff. rewrite filter_In. intuition auto. 
+  destruct (in_dec ident_eq (name_composite_def x) (map name_composite_def l1)); simpl; auto.
+  exploit list_in_map_inv; eauto. intros (y & P & Q).
+  assert (x = y) by eauto. subst y. auto.
+Qed.
+
+Instance Linker_composite_defs : Linker (list composite_definition) := {
+  link := link_composite_defs;
+  linkorder := @List.incl composite_definition
+}.
+Proof.
+- intros; apply incl_refl.
+- intros; red; intros; eauto.
+- intros. apply link_composite_def_inv in H; destruct H as (A & B & C).
+  split; red; intros; apply C; auto.
+Defined.
+
+(** Connections with [build_composite_env]. *)
+
+Lemma add_composite_definitions_append:
+  forall l1 l2 env env'',
+  add_composite_definitions env (l1 ++ l2) = OK env'' <->
+  exists env', add_composite_definitions env l1 = OK env' /\ add_composite_definitions env' l2 = OK env''.
+Proof.
+  induction l1; simpl; intros.
+- split; intros. exists env; auto. destruct H as (env' & A & B). congruence.
+- destruct a; simpl. destruct (composite_of_def env id su m a); simpl.
+  apply IHl1. 
+  split; intros. discriminate. destruct H as (env' & A & B); discriminate.
+Qed.
+
+Lemma composite_eq:
+  forall su1 m1 a1 sz1 al1 r1 pos1 al2p1 szal1
+         su2 m2 a2 sz2 al2 r2 pos2 al2p2 szal2,
+  su1 = su2 -> m1 = m2 -> a1 = a2 -> sz1 = sz2 -> al1 = al2 -> r1 = r2 ->
+  Build_composite su1 m1 a1 sz1 al1 r1 pos1 al2p1 szal1 = Build_composite su2 m2 a2 sz2 al2 r2 pos2 al2p2 szal2.
+Proof.
+  intros. subst.
+  assert (pos1 = pos2) by apply proof_irr. 
+  assert (al2p1 = al2p2) by apply proof_irr.
+  assert (szal1 = szal2) by apply proof_irr.
+  subst. reflexivity.
+Qed.
+
+Lemma composite_of_def_eq:
+  forall env id co,
+  composite_consistent env co ->
+  env!id = None ->
+  composite_of_def env id (co_su co) (co_members co) (co_attr co) = OK co.
+Proof.
+  intros. destruct H as [A B C D]. unfold composite_of_def. rewrite H0, A.
+  destruct co; simpl in *. f_equal. apply composite_eq; auto. rewrite C, B; auto. 
+Qed.
+
+Lemma composite_consistent_unique:
+  forall env co1 co2,
+  composite_consistent env co1 ->
+  composite_consistent env co2 ->
+  co_su co1 = co_su co2 ->
+  co_members co1 = co_members co2 ->
+  co_attr co1 = co_attr co2 ->
+  co1 = co2.
+Proof.
+  intros. destruct H, H0. destruct co1, co2; simpl in *. apply composite_eq; congruence.
+Qed.
+
+Lemma composite_of_def_stable:
+  forall (env env': composite_env)
+         (EXTENDS: forall id co, env!id = Some co -> env'!id = Some co)
+         id su m a co,
+  env'!id = None ->
+  composite_of_def env id su m a = OK co ->
+  composite_of_def env' id su m a = OK co.
+Proof.
+  intros. 
+  unfold composite_of_def in H0. 
+  destruct (env!id) eqn:E; try discriminate.
+  destruct (complete_members env m) eqn:CM; try discriminate.
+  transitivity (composite_of_def env' id (co_su co) (co_members co) (co_attr co)).
+  inv H0; auto. 
+  apply composite_of_def_eq; auto. 
+  apply composite_consistent_stable with env; auto. 
+  inv H0; constructor; auto.
+Qed.
+
+Lemma link_add_composite_definitions:
+  forall l0 env0,
+  build_composite_env l0 = OK env0 ->
+  forall l env1 env1' env2,
+  add_composite_definitions env1 l = OK env1' ->
+  (forall id co, env1!id = Some co -> env2!id = Some co) ->
+  (forall id co, env0!id = Some co -> env2!id = Some co) ->
+  (forall id, env2!id = if In_dec ident_eq id (map name_composite_def l0) then env0!id else env1!id) ->
+  ((forall cd1 cd2, In cd1 l0 -> In cd2 l -> name_composite_def cd2 = name_composite_def cd1 -> cd2 = cd1)) ->
+  { env2' |
+      add_composite_definitions env2 (filter_redefs l0 l) = OK env2'
+  /\ (forall id co, env1'!id = Some co -> env2'!id = Some co)
+  /\ (forall id co, env0!id = Some co -> env2'!id = Some co) }.
+Proof.
+  induction l; simpl; intros until env2; intros ACD AGREE1 AGREE0 AGREE2 UNIQUE.
+- inv ACD. exists env2; auto.
+- destruct a. destruct (composite_of_def env1 id su m a) as [x|e] eqn:EQ; try discriminate.
+  simpl in ACD.
+  generalize EQ. unfold composite_of_def at 1. 
+  destruct (env1!id) eqn:E1; try congruence.
+  destruct (complete_members env1 m) eqn:CM1; try congruence. 
+  intros EQ1.
+  simpl. destruct (in_dec ident_eq id (map name_composite_def l0)); simpl.
++ eapply IHl; eauto.
+* intros. rewrite PTree.gsspec in H0. destruct (peq id0 id); auto.
+  inv H0.
+  exploit list_in_map_inv; eauto. intros ([id' su' m' a'] & P & Q).
+  assert (X: Composite id su m a = Composite id' su' m' a').
+  { eapply UNIQUE. auto. auto. rewrite <- P; auto. }
+  inv X.
+  exploit build_composite_env_charact; eauto. intros (co' & U & V & W & X). 
+  assert (co' = co).
+  { apply composite_consistent_unique with env2.
+    apply composite_consistent_stable with env0; auto. 
+    eapply build_composite_env_consistent; eauto.
+    apply composite_consistent_stable with env1; auto.
+    inversion EQ1; constructor; auto. 
+    inversion EQ1; auto.
+    inversion EQ1; auto.
+    inversion EQ1; auto. }
+  subst co'. apply AGREE0; auto. 
+* intros. rewrite AGREE2. destruct (in_dec ident_eq id0 (map name_composite_def l0)); auto. 
+  rewrite PTree.gsspec. destruct (peq id0 id); auto. subst id0. contradiction.
++ assert (E2: env2!id = None).
+  { rewrite AGREE2. rewrite pred_dec_false by auto. auto. }
+  assert (E3: composite_of_def env2 id su m a = OK x).
+  { eapply composite_of_def_stable. eexact AGREE1. eauto. eauto. }
+  rewrite E3. simpl. eapply IHl; eauto. 
+* intros until co; rewrite ! PTree.gsspec. destruct (peq id0 id); auto.
+* intros until co; rewrite ! PTree.gsspec. intros. destruct (peq id0 id); auto.
+  subst id0. apply AGREE0 in H0. congruence.
+* intros. rewrite ! PTree.gsspec. destruct (peq id0 id); auto. subst id0. 
+  rewrite pred_dec_false by auto. auto.
+Qed.
+
+Theorem link_build_composite_env:
+  forall l1 l2 l env1 env2,
+  build_composite_env l1 = OK env1 ->
+  build_composite_env l2 = OK env2 ->
+  link l1 l2 = Some l ->
+  { env |
+     build_composite_env l = OK env
+  /\ (forall id co, env1!id = Some co -> env!id = Some co)
+  /\ (forall id co, env2!id = Some co -> env!id = Some co) }.
+Proof.
+  intros. edestruct link_composite_def_inv as (A & B & C); eauto.
+  edestruct link_add_composite_definitions as (env & P & Q & R).
+  eexact H.
+  eexact H0.
+  instantiate (1 := env1). intros. rewrite PTree.gempty in H2; discriminate.
+  auto.
+  intros. destruct (in_dec ident_eq id (map name_composite_def l1)); auto.
+  rewrite PTree.gempty. destruct (env1!id) eqn:E1; auto. 
+  exploit build_composite_env_domain. eexact H. eauto.
+  intros. apply (in_map name_composite_def) in H2. elim n; auto. 
+  auto.
+  exists env; split; auto. subst l. apply add_composite_definitions_append. exists env1; auto. 
+Qed.
+
+(** ** Linking function definitions *)
+
+Definition link_fundef {F: Type} (fd1 fd2: fundef F) :=
+  match fd1, fd2 with
+  | Internal _, Internal _ => None
+  | External ef1 targs1 tres1 cc1, External ef2 targs2 tres2 cc2 =>
+      if external_function_eq ef1 ef2
+      && typelist_eq targs1 targs2
+      && type_eq tres1 tres2
+      && calling_convention_eq cc1 cc2
+      then Some (External ef1 targs1 tres1 cc1)
+      else None
+  | Internal f, External ef targs tres cc =>
+      match ef with EF_external id sg => Some (Internal f) | _ => None end
+  | External ef targs tres cc, Internal f =>
+      match ef with EF_external id sg => Some (Internal f) | _ => None end
+  end.
+
+Inductive linkorder_fundef {F: Type}: fundef F -> fundef F -> Prop :=
+  | linkorder_fundef_refl: forall fd,
+      linkorder_fundef fd fd
+  | linkorder_fundef_ext_int: forall f id sg targs tres cc,
+      linkorder_fundef (External (EF_external id sg) targs tres cc) (Internal f).
+
+Instance Linker_fundef (F: Type): Linker (fundef F) := {
+  link := link_fundef;
+  linkorder := linkorder_fundef
+}.
+Proof.
+- intros; constructor.
+- intros. inv H; inv H0; constructor.
+- intros x y z EQ. destruct x, y; simpl in EQ.
++ discriminate.
++ destruct e; inv EQ. split; constructor.
++ destruct e; inv EQ. split; constructor.
++ destruct (external_function_eq e e0 && typelist_eq t t1 && type_eq t0 t2 && calling_convention_eq c c0) eqn:A; inv EQ.
+  InvBooleans. subst. split; constructor.
+Defined.
+
+Remark link_fundef_either:
+  forall (F: Type) (f1 f2 f: fundef F), link f1 f2 = Some f -> f = f1 \/ f = f2.
+Proof.
+  simpl; intros. unfold link_fundef in H. destruct f1, f2; try discriminate.
+- destruct e; inv H. auto.
+- destruct e; inv H. auto.
+- destruct (external_function_eq e e0 && typelist_eq t t1 && type_eq t0 t2 && calling_convention_eq c c0); inv H; auto.
+Qed.
+
+Global Opaque Linker_fundef.
+
+(** ** Linking programs *)
+
+Definition lift_option {A: Type} (opt: option A) : { x | opt = Some x } + { opt = None }.
+Proof.
+  destruct opt. left; exists a; auto. right; auto. 
+Defined.
+
+Definition link_program {F:Type} (p1 p2: program F): option (program F) :=
+  match link (program_of_program p1) (program_of_program p2) with
+  | None => None
+  | Some p =>
+      match lift_option (link p1.(prog_types) p2.(prog_types)) with
+      | inright _ => None
+      | inleft (exist typs EQ) =>
+          match link_build_composite_env
+                   p1.(prog_types) p2.(prog_types) typs
+                   p1.(prog_comp_env) p2.(prog_comp_env)
+                   p1.(prog_comp_env_eq) p2.(prog_comp_env_eq) EQ with
+          | exist env (conj P Q) =>
+              Some {| prog_defs := p.(AST.prog_defs);
+                      prog_public := p.(AST.prog_public);
+                      prog_main := p.(AST.prog_main);
+                      prog_types := typs;
+                      prog_comp_env := env;
+                      prog_comp_env_eq := P |}
+          end
+      end
+  end.
+
+Definition linkorder_program {F: Type} (p1 p2: program F) : Prop :=
+     linkorder (program_of_program p1) (program_of_program p2)
+  /\ (forall id co, p1.(prog_comp_env)!id = Some co -> p2.(prog_comp_env)!id = Some co).
+
+Instance Linker_program (F: Type): Linker (program F) := {
+  link := link_program;
+  linkorder := linkorder_program
+}.
+Proof.
+- intros; split. apply linkorder_refl. auto. 
+- intros. destruct H, H0. split. eapply linkorder_trans; eauto.
+  intros; auto.
+- intros until z. unfold link_program. 
+  destruct (link (program_of_program x) (program_of_program y)) as [p|] eqn:LP; try discriminate.
+  destruct (lift_option (link (prog_types x) (prog_types y))) as [[typs EQ]|EQ]; try discriminate.
+  destruct (link_build_composite_env (prog_types x) (prog_types y) typs
+       (prog_comp_env x) (prog_comp_env y) (prog_comp_env_eq x)
+       (prog_comp_env_eq y) EQ) as (env & P & Q & R).
+  destruct (link_linkorder _ _ _ LP). 
+  intros X; inv X.
+  split; split; auto.
+Defined.
+
+Global Opaque Linker_program.
+
+(** ** Commutation between linking and program transformations *)
+
+Section LINK_MATCH_PROGRAM.
+
+Context {F G: Type}.
+Variable match_fundef: fundef F -> fundef G -> Prop.
+
+Hypothesis link_match_fundef:
+  forall f1 tf1 f2 tf2 f,
+  link f1 f2 = Some f ->
+  match_fundef f1 tf1 -> match_fundef f2 tf2 ->
+  exists tf, link tf1 tf2 = Some tf /\ match_fundef f tf.
+
+Let match_program (p: program F) (tp: program G) : Prop :=
+    Linking.match_program (fun ctx f tf => match_fundef f tf) eq p tp
+ /\ prog_types tp = prog_types p.
+
+Theorem link_match_program:
+  forall p1 p2 tp1 tp2 p,
+  link p1 p2 = Some p -> match_program p1 tp1 -> match_program p2 tp2 ->
+  exists tp, link tp1 tp2 = Some tp /\ match_program p tp.
+Proof.
+  intros. destruct H0, H1. 
+Local Transparent Linker_program.
+  simpl in H; unfold link_program in H.
+  destruct (link (program_of_program p1) (program_of_program p2)) as [pp|] eqn:LP; try discriminate.
+  assert (A: exists tpp,
+               link (program_of_program tp1) (program_of_program tp2) = Some tpp
+             /\ Linking.match_program (fun ctx f tf => match_fundef f tf) eq pp tpp).
+  { eapply Linking.link_match_program. 
+  - intros. exploit link_match_fundef; eauto. intros (tf & A & B). exists tf; auto.
+  - intros.
+    Local Transparent Linker_types.
+    simpl in *. destruct (type_eq v1 v2); inv H4. subst v tv2. exists tv1; rewrite dec_eq_true; auto.
+  - eauto.
+  - eauto.
+  - eauto.
+  - apply (link_linkorder _ _ _ LP).
+  - apply (link_linkorder _ _ _ LP). }
+  destruct A as (tpp & TLP & MP).
+  simpl; unfold link_program. rewrite TLP.
+  destruct (lift_option (link (prog_types p1) (prog_types p2))) as [[typs EQ]|EQ]; try discriminate.
+  destruct (link_build_composite_env (prog_types p1) (prog_types p2) typs
+           (prog_comp_env p1) (prog_comp_env p2) (prog_comp_env_eq p1)
+           (prog_comp_env_eq p2) EQ) as (env & P & Q). 
+  rewrite <- H2, <- H3 in EQ.
+  destruct (lift_option (link (prog_types tp1) (prog_types tp2))) as [[ttyps EQ']|EQ']; try congruence.
+  assert (ttyps = typs) by congruence. subst ttyps. 
+  destruct (link_build_composite_env (prog_types tp1) (prog_types tp2) typs
+         (prog_comp_env tp1) (prog_comp_env tp2) (prog_comp_env_eq tp1)
+         (prog_comp_env_eq tp2) EQ') as (tenv & R & S).
+  assert (tenv = env) by congruence. subst tenv.
+  econstructor; split; eauto. inv H. split; auto.
+  unfold program_of_program; simpl. destruct pp, tpp; exact MP.
+Qed.
+
+End LINK_MATCH_PROGRAM.
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
index f59fb396..440e4e84 100644
--- a/cfrontend/Ctyping.v
+++ b/cfrontend/Ctyping.v
@@ -15,21 +15,11 @@
 
 (** Typing rules and type-checking for the Compcert C language *)
 
-Require Import Coqlib.
 Require Import String.
-Require Import Maps.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import Memory.
-Require Import Globalenvs.
-Require Import Events.
-Require Import AST.
-Require Import Ctypes.
-Require Import Cop.
-Require Import Csyntax.
-Require Import Csem.
-Require Import Errors.
+Require Import Coqlib Maps Integers Floats Errors.
+Require Import AST Linking.
+Require Import Values Memory Globalenvs Events.
+Require Import Ctypes Cop Csyntax Csem.
 
 Local Open Scope error_monad_scope.
 
@@ -911,8 +901,8 @@ Definition retype_fundef (ce: composite_env) (e: typenv) (fd: fundef) : res fund
 Definition typecheck_program (p: program) : res program :=
   let e := bind_globdef (PTree.empty _) p.(prog_defs) in
   let ce := p.(prog_comp_env) in
-  do defs <- transf_globdefs (retype_fundef ce e) (fun v => OK v) p.(prog_defs);
-  OK {| prog_defs := defs;
+  do tp <- transform_partial_program (retype_fundef ce e) p;
+  OK {| prog_defs := tp.(AST.prog_defs);
         prog_public := p.(prog_public);
         prog_main := p.(prog_main);
         prog_types := p.(prog_types);
@@ -1325,32 +1315,29 @@ Theorem typecheck_program_sound:
   forall p p', typecheck_program p = OK p' -> wt_program p'.
 Proof.
   unfold typecheck_program; intros. monadInv H.
-  rename x into defs.
+  rename x into tp.
   constructor; simpl.
   set (ce := prog_comp_env p) in *.
   set (e := bind_globdef (PTree.empty type) (prog_defs p)) in *.
-  set (e' := bind_globdef (PTree.empty type) defs) in *.
-  assert (MATCH:
-    list_forall2 (match_globdef (fun f tf => retype_fundef ce e f = OK tf) (fun v tv => tv = v)) (prog_defs p) defs).
-  {
-    revert EQ; generalize (prog_defs p) defs.
-    induction l as [ | [id gd] l ]; intros l'; simpl; intros.
-    inv EQ. constructor.
-    destruct gd as [f | v].
-    destruct (retype_fundef ce e f) as [tf|msg] eqn:R; monadInv EQ.
-    constructor; auto. constructor; auto.
-    monadInv EQ. constructor; auto. destruct v; constructor; auto. }
+  set (e' := bind_globdef (PTree.empty type) (AST.prog_defs tp)) in *.
+  assert (M: match_program (fun ctx f tf => retype_fundef ce e f = OK tf) eq p tp)
+  by (eapply match_transform_partial_program; eauto).
+  destruct M as (MATCH & _). simpl in MATCH.
   assert (ENVS: e' = e).
-  { unfold e, e'. revert MATCH; generalize (prog_defs p) defs (PTree.empty type).
+  { unfold e, e'. revert MATCH; generalize (prog_defs p) (AST.prog_defs tp) (PTree.empty type).
     induction l as [ | [id gd] l ]; intros l' t M; inv M.
-    auto. inv H1; simpl; auto. replace (type_of_fundef f2) with (type_of_fundef f1); auto.
-    unfold retype_fundef in H4. destruct f1; monadInv H4; auto. monadInv EQ0; auto.
+    auto.
+    destruct b1 as [id' gd']; destruct H1; simpl in *. inv H0; simpl.
+    replace (type_of_fundef f2) with (type_of_fundef f1); auto.
+    unfold retype_fundef in H2. destruct f1; monadInv H2; auto. monadInv EQ0; auto.
+    inv H1. simpl. auto.
   }
   rewrite ENVS.
-  intros id f. revert MATCH; generalize (prog_defs p) defs. induction 1; simpl; intros.
+  intros id f. revert MATCH; generalize (prog_defs p) (AST.prog_defs tp).
+  induction 1; simpl; intros.
   contradiction.
-  destruct H0; auto. subst b1; inv H. destruct f1; simpl in H2.
-  monadInv H2. eapply retype_function_sound; eauto. congruence.
+  destruct H0; auto. subst b1; inv H. simpl in H1. inv H1. 
+  destruct f1; monadInv H4. eapply retype_function_sound; eauto.
 Qed.
 
 (** * Subject reduction *)
@@ -2122,28 +2109,3 @@ Proof.
 Qed.
 
 End PRESERVATION.
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index e6fcad8c..d5f39d7d 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -649,7 +649,7 @@ Qed.
 Lemma transl_init_single_size:
   forall ty a data,
   transl_init_single ge ty a = OK data ->
-  Genv.init_data_size data = sizeof ge ty.
+  init_data_size data = sizeof ge ty.
 Proof.
   intros. monadInv H. destruct x0.
 - monadInv EQ2.
@@ -666,7 +666,7 @@ Proof.
   inv EQ2; auto.
 Qed.
 
-Notation idlsize := Genv.init_data_list_size.
+Notation idlsize := init_data_list_size.
 
 Remark padding_size:
   forall frm to, frm <= to -> idlsize (tr_padding frm to) = to - frm.
diff --git a/cfrontend/PrintClight.ml b/cfrontend/PrintClight.ml
index 9600b3fa..8a321757 100644
--- a/cfrontend/PrintClight.ml
+++ b/cfrontend/PrintClight.ml
@@ -258,7 +258,7 @@ let print_function p id f =
 
 let print_fundef p id fd =
   match fd with
-  | External(EF_external(_,_), args, res, cconv) ->
+  | External((EF_external _ | EF_runtime _), args, res, cconv) ->
       fprintf p "extern %s;@ @ "
                 (name_cdecl (extern_atom id) (Tfunction(args, res, cconv)))
   | External(_, _, _, _) ->
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index f68f520d..d884100b 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -264,6 +264,8 @@ let rec expr p (prec, e) =
                 (camlstring_of_coqstring txt) exprlist (false, args)
   | Ebuiltin(EF_external(id, sg), _, args, _) ->
       fprintf p "%s@[<hov 1>(%a)@]" (camlstring_of_coqstring id) exprlist (true, args)
+  | Ebuiltin(EF_runtime(id, sg), _, args, _) ->
+      fprintf p "%s@[<hov 1>(%a)@]" (camlstring_of_coqstring id) exprlist (true, args)
   | Ebuiltin(EF_inline_asm(txt, sg, clob), _, args, _) ->
       extended_asm p txt None args clob
   | Ebuiltin(EF_debug(kind,txt,_),_,args,_) ->
@@ -427,7 +429,7 @@ let print_function p id f =
 
 let print_fundef p id fd =
   match fd with
-  | External(EF_external(_,_), args, res, cconv) ->
+  | External((EF_external _ | EF_runtime _), args, res, cconv) ->
       fprintf p "extern %s;@ @ "
                 (name_cdecl (extern_atom id) (Tfunction(args, res, cconv)))
   | External(_, _, _, _) ->
diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v
index a3af8114..bfdd8ab9 100644
--- a/cfrontend/SimplExpr.v
+++ b/cfrontend/SimplExpr.v
@@ -512,9 +512,9 @@ Local Open Scope error_monad_scope.
 
 Definition transl_fundef (fd: Csyntax.fundef) : res fundef :=
   match fd with
-  | Csyntax.Internal f =>
+  | Internal f =>
       do tf <- transl_function f; OK (Internal tf)
-  | Csyntax.External ef targs tres cc =>
+  | External ef targs tres cc =>
       OK (External ef targs tres cc)
   end.
 
@@ -523,6 +523,6 @@ Definition transl_program (p: Csyntax.program) : res program :=
   OK {| prog_defs := AST.prog_defs p1;
         prog_public := AST.prog_public p1;
         prog_main := AST.prog_main p1;
-        prog_types := Csyntax.prog_types p;
-        prog_comp_env := Csyntax.prog_comp_env p;
-        prog_comp_env_eq := Csyntax.prog_comp_env_eq p |}.
+        prog_types := prog_types p;
+        prog_comp_env := prog_comp_env p;
+        prog_comp_env_eq := prog_comp_env_eq p |}.
diff --git a/cfrontend/SimplExprproof.v b/cfrontend/SimplExprproof.v
index 8baa7d46..64e52df8 100644
--- a/cfrontend/SimplExprproof.v
+++ b/cfrontend/SimplExprproof.v
@@ -12,30 +12,34 @@
 
 (** Correctness proof for expression simplification. *)
 
-Require Import Coqlib.
-Require Import Maps.
-Require Import AST.
-Require Import Errors.
-Require Import Integers.
-Require Import Values.
-Require Import Memory.
-Require Import Events.
-Require Import Smallstep.
-Require Import Globalenvs.
-Require Import Ctypes.
-Require Import Cop.
-Require Import Csyntax.
-Require Import Csem.
-Require Import Cstrategy.
-Require Import Clight.
-Require Import SimplExpr.
-Require Import SimplExprspec.
+Require Import Coqlib Maps Errors Integers.
+Require Import AST Linking.
+Require Import Values Memory Events Globalenvs Smallstep.
+Require Import Ctypes Cop Csyntax Csem Cstrategy Clight.
+Require Import SimplExpr SimplExprspec.
+
+(** ** Relational specification of the translation. *)
+
+Definition match_prog (p: Csyntax.program) (tp: Clight.program) :=
+    match_program (fun ctx f tf => tr_fundef f tf) eq p tp
+ /\ prog_types tp = prog_types p.
+
+Lemma transf_program_match:
+  forall p tp, transl_program p = OK tp -> match_prog p tp.
+Proof.
+  unfold transl_program; intros. monadInv H. split; auto.
+  unfold program_of_program; simpl. destruct x; simpl.
+  eapply match_transform_partial_program_contextual. eexact EQ. 
+  intros. apply transl_fundef_spec; auto. 
+Qed.
+
+(** ** Semantic preservation *)
 
 Section PRESERVATION.
 
 Variable prog: Csyntax.program.
 Variable tprog: Clight.program.
-Hypothesis TRANSL: transl_program prog = OK tprog.
+Hypothesis TRANSL: match_prog prog tprog.
 
 Let ge := Csem.globalenv prog.
 Let tge := Clight.globalenv tprog.
@@ -45,22 +49,17 @@ Let tge := Clight.globalenv tprog.
 Lemma comp_env_preserved:
   Clight.genv_cenv tge = Csem.genv_cenv ge.
 Proof.
-  monadInv TRANSL. unfold tge; rewrite <- H0; auto.
+  simpl. destruct TRANSL. generalize (prog_comp_env_eq tprog) (prog_comp_env_eq prog). 
+  congruence.
 Qed.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof.
-  intros. eapply Genv.find_symbol_match. eapply transl_program_spec; eauto.
-  simpl. tauto.
-Qed.
+Proof (Genv.find_symbol_match (proj1 TRANSL)).
 
-Lemma public_preserved:
-  forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s.
-Proof.
-  intros. eapply Genv.public_symbol_match. eapply transl_program_spec; eauto.
-  simpl. tauto.
-Qed.
+Lemma senv_preserved:
+  Senv.equiv ge tge.
+Proof (Genv.senv_match (proj1 TRANSL)).
 
 Lemma function_ptr_translated:
   forall b f,
@@ -68,9 +67,8 @@ Lemma function_ptr_translated:
   exists tf,
   Genv.find_funct_ptr tge b = Some tf /\ tr_fundef f tf.
 Proof.
-  intros. eapply Genv.find_funct_ptr_match.
-  eapply transl_program_spec; eauto.
-  assumption.
+  intros.
+  edestruct (Genv.find_funct_ptr_match (proj1 TRANSL)) as (ctx & tf & A & B & C); eauto.
 Qed.
 
 Lemma functions_translated:
@@ -79,27 +77,8 @@ Lemma functions_translated:
   exists tf,
   Genv.find_funct tge v = Some tf /\ tr_fundef f tf.
 Proof.
-  intros. eapply Genv.find_funct_match.
-  eapply transl_program_spec; eauto.
-  assumption.
-Qed.
-
-Lemma varinfo_preserved:
-  forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
-Proof.
-  intros. destruct (Genv.find_var_info ge b) as [v|] eqn:V.
-- exploit Genv.find_var_info_match. eapply transl_program_spec; eauto. eassumption.
-  intros [tv [A B]]. inv B. assumption.
-- destruct (Genv.find_var_info tge b) as [v'|] eqn:V'; auto.
-  exploit Genv.find_var_info_rev_match. eapply transl_program_spec; eauto. eassumption.
-  simpl. destruct (plt b (Genv.genv_next (Genv.globalenv prog))); try tauto.
-  intros [v [A B]]. inv B. change (Genv.globalenv prog) with (Csem.genv_genv ge) in A. congruence.
-Qed.
-
-Lemma block_is_volatile_preserved:
-  forall b, Genv.block_is_volatile tge b = Genv.block_is_volatile ge b.
-Proof.
-  intros. unfold Genv.block_is_volatile. rewrite varinfo_preserved. auto.
+  intros.
+  edestruct (Genv.find_funct_match (proj1 TRANSL)) as (ctx & tf & A & B & C); eauto.
 Qed.
 
 Lemma type_of_fundef_preserved:
@@ -167,8 +146,7 @@ Proof.
   (* By_value, not volatile *)
   rewrite H1. split; auto. eapply deref_loc_value; eauto.
   (* By_value, volatile *)
-  rewrite H0; rewrite H1. eapply volatile_load_preserved with (ge1 := ge); auto.
-  exact symbols_preserved. exact public_preserved. exact block_is_volatile_preserved.
+  rewrite H0; rewrite H1. eapply volatile_load_preserved with (ge1 := ge); auto. apply senv_preserved.
   (* By reference *)
   rewrite H0. destruct (type_is_volatile ty); split; auto; eapply deref_loc_reference; eauto.
   (* By copy *)
@@ -187,8 +165,7 @@ Proof.
   (* By_value, not volatile *)
   rewrite H1. split; auto. eapply assign_loc_value; eauto.
   (* By_value, volatile *)
-  rewrite H0; rewrite H1. eapply volatile_store_preserved with (ge1 := ge); auto.
-  exact symbols_preserved. exact public_preserved. exact block_is_volatile_preserved.
+  rewrite H0; rewrite H1. eapply volatile_store_preserved with (ge1 := ge); auto. apply senv_preserved.
   (* By copy *)
   rewrite H0. rewrite <- comp_env_preserved in *.
   destruct (type_is_volatile ty); split; auto; eapply assign_loc_copy; eauto.
@@ -1907,8 +1884,7 @@ Proof.
   econstructor; split.
   left. eapply plus_left. constructor.  apply star_one.
   econstructor; eauto.
-  eapply external_call_symbols_preserved; eauto.
-  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
+  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   traceEq.
   econstructor; eauto.
   change sl2 with (nil ++ sl2). apply S. constructor. simpl; auto. auto.
@@ -1918,8 +1894,7 @@ Proof.
   econstructor; split.
   left. eapply plus_left. constructor. apply star_one.
   econstructor; eauto.
-  eapply external_call_symbols_preserved; eauto.
-  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
+  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   traceEq.
   econstructor; eauto.
   change sl2 with (nil ++ sl2). apply S.
@@ -2215,8 +2190,7 @@ Proof.
   inv H5.
   econstructor; split.
   left; apply plus_one. econstructor; eauto.
-  eapply external_call_symbols_preserved; eauto.
-  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
+  eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   constructor; auto.
 
 (* return *)
@@ -2246,15 +2220,14 @@ Lemma transl_initial_states:
   Csem.initial_state prog S ->
   exists S', Clight.initial_state tprog S' /\ match_states S S'.
 Proof.
-  intros. inv H. generalize TRANSL; intros TR; monadInv TR. rewrite H4.
-  exploit transl_program_spec; eauto. intros MP.
+  intros. inv H.
   exploit function_ptr_translated; eauto. intros [tf [FIND TR]].
   econstructor; split.
   econstructor.
-  exploit Genv.init_mem_match; eauto.
-  change (Genv.globalenv tprog) with (genv_genv tge).
-  rewrite symbols_preserved. rewrite <- H4; simpl.
-  rewrite (transform_partial_program_main _ _ EQ). eauto. 
+  eapply (Genv.init_mem_match (proj1 TRANSL)); eauto.
+  replace (prog_main tprog) with (prog_main prog).
+  rewrite symbols_preserved. eauto. 
+  destruct TRANSL. destruct H as (A & B & C). simpl in B. auto. 
   eexact FIND.
   rewrite <- H3. apply type_of_fundef_preserved. auto.
   constructor. auto. constructor.
@@ -2271,7 +2244,7 @@ Theorem transl_program_correct:
   forward_simulation (Cstrategy.semantics prog) (Clight.semantics1 tprog).
 Proof.
   eapply forward_simulation_star_wf with (order := ltof _ measure).
-  eexact public_preserved.
+  eapply senv_preserved.
   eexact transl_initial_states.
   eexact transl_final_states.
   apply well_founded_ltof.
@@ -2279,3 +2252,18 @@ Proof.
 Qed.
 
 End PRESERVATION.
+
+(** ** Commutation with linking *)
+
+Instance TransfSimplExprLink : TransfLink match_prog.
+Proof.
+  red; intros. eapply Ctypes.link_match_program; eauto. 
+- intros.
+Local Transparent Linker_fundef.
+  simpl in *; unfold link_fundef in *. inv H3; inv H4; try discriminate.
+  destruct ef; inv H2. exists (Internal tf); split; auto. constructor; auto.
+  destruct ef; inv H2. exists (Internal tf); split; auto. constructor; auto.
+  destruct (external_function_eq ef ef0 && typelist_eq targs targs0 &&
+            type_eq tres tres0 && calling_convention_eq cconv cconv0); inv H2.
+  exists (External ef targs tres cconv); split; auto. constructor.
+Qed.
diff --git a/cfrontend/SimplExprspec.v b/cfrontend/SimplExprspec.v
index b94465a1..453a4c9a 100644
--- a/cfrontend/SimplExprspec.v
+++ b/cfrontend/SimplExprspec.v
@@ -12,18 +12,9 @@
 
 (** Relational specification of expression simplification. *)
 
-Require Import Coqlib.
-Require Import Errors.
-Require Import Maps.
-Require Import Integers.
-Require Import Floats.
-Require Import Memory.
-Require Import AST.
-Require Import Ctypes.
-Require Import Cop.
-Require Import Csyntax.
-Require Import Clight.
-Require Import SimplExpr.
+Require Import Coqlib Maps Errors Integers Floats.
+Require Import AST Linking Memory.
+Require Import Ctypes Cop Csyntax Clight SimplExpr.
 
 Section SPEC.
 
@@ -1077,8 +1068,7 @@ Opaque transl_expression transl_expr_stmt.
   monadInv TR; constructor; eauto.
 Qed.
 
-(** Relational presentation for the transformation of functions, fundefs, and va
-riables. *)
+(** Relational presentation for the transformation of functions, fundefs, and variables. *)
 
 Inductive tr_function: Csyntax.function -> Clight.function -> Prop :=
   | tr_function_intro: forall f tf,
@@ -1092,9 +1082,9 @@ Inductive tr_function: Csyntax.function -> Clight.function -> Prop :=
 Inductive tr_fundef: Csyntax.fundef -> Clight.fundef -> Prop :=
   | tr_internal: forall f tf,
       tr_function f tf ->
-      tr_fundef (Csyntax.Internal f) (Clight.Internal tf)
+      tr_fundef (Internal f) (Internal tf)
   | tr_external: forall ef targs tres cconv,
-      tr_fundef (Csyntax.External ef targs tres cconv) (External ef targs tres cconv).
+      tr_fundef (External ef targs tres cconv) (External ef targs tres cconv).
 
 Lemma transl_function_spec:
   forall f tf,
@@ -1117,30 +1107,5 @@ Proof.
 + constructor.
 Qed.
 
-Lemma transl_globdefs_spec:
-  forall l l',
-  transf_globdefs transl_fundef (fun v : type => OK v) l = OK l' ->
-  list_forall2 (match_globdef tr_fundef (fun v1 v2 => v1 = v2)) l l'.
-Proof.
-  induction l; simpl; intros.
-- inv H. constructor.
-- destruct a as [id gd]. destruct gd.
-  + destruct (transl_fundef f) as [tf | ?] eqn:E1; Errors.monadInv H.
-    constructor; eauto. constructor. eapply transl_fundef_spec; eauto.
-  + Errors.monadInv H. 
-    constructor; eauto. destruct v; constructor; auto.
-Qed.
-
-Theorem transl_program_spec:
-  forall p tp,
-  transl_program p = OK tp ->
-  match_program tr_fundef (fun v1 v2 => v1 = v2) nil (Csyntax.prog_main p) p tp.
-Proof.
-  unfold transl_program, transform_partial_program; intros. Errors.monadInv H. Errors.monadInv EQ; simpl.
-  split; auto. exists x0; split.
-  eapply transl_globdefs_spec; eauto.
-  rewrite <- app_nil_end; auto.
-Qed.
-
 End SPEC.
 
diff --git a/cfrontend/SimplLocals.v b/cfrontend/SimplLocals.v
index c4b1054d..580f02c2 100644
--- a/cfrontend/SimplLocals.v
+++ b/cfrontend/SimplLocals.v
@@ -15,13 +15,9 @@
 
 Require Import FSets.
 Require FSetAVL.
-Require Import Coqlib.
-Require Import Ordered.
-Require Import Errors.
-Require Import AST.
-Require Import Ctypes.
-Require Import Cop.
-Require Import Clight.
+Require Import Coqlib Ordered Errors.
+Require Import AST Linking.
+Require Import Ctypes Cop Clight.
 Require Compopts.
 
 Open Scope error_monad_scope.
diff --git a/cfrontend/SimplLocalsproof.v b/cfrontend/SimplLocalsproof.v
index a86e3a01..2cd82d8f 100644
--- a/cfrontend/SimplLocalsproof.v
+++ b/cfrontend/SimplLocalsproof.v
@@ -13,80 +13,58 @@
 (** Semantic preservation for the SimplLocals pass. *)
 
 Require Import FSets.
-Require FSetAVL.
-Require Import Coqlib.
-Require Import Errors.
-Require Import Ordered.
-Require Import AST.
-Require Import Maps.
-Require Import Integers.
-Require Import Floats.
-Require Import Values.
-Require Import Memory.
-Require Import Globalenvs.
-Require Import Events.
-Require Import Smallstep.
-Require Import Ctypes.
-Require Import Cop.
-Require Import Clight.
-Require Import SimplLocals.
+Require Import Coqlib Errors Ordered Maps Integers Floats.
+Require Import AST Linking.
+Require Import Values Memory Globalenvs Events Smallstep.
+Require Import Ctypes Cop Clight SimplLocals.
 
 Module VSF := FSetFacts.Facts(VSet).
 Module VSP := FSetProperties.Properties(VSet).
 
+Definition match_prog (p tp: program) : Prop :=
+    match_program (fun ctx f tf => transf_fundef f = OK tf) eq p tp
+ /\ prog_types tp = prog_types p.
+
+Lemma match_transf_program:
+  forall p tp, transf_program p = OK tp -> match_prog p tp.
+Proof.
+  unfold transf_program; intros. monadInv H. 
+  split; auto. apply match_transform_partial_program. rewrite EQ. destruct x; auto.
+Qed.
+
 Section PRESERVATION.
 
 Variable prog: program.
 Variable tprog: program.
-Hypothesis TRANSF: transf_program prog = OK tprog.
+Hypothesis TRANSF: match_prog prog tprog.
 Let ge := globalenv prog.
 Let tge := globalenv tprog.
 
 Lemma comp_env_preserved:
   genv_cenv tge = genv_cenv ge.
 Proof.
-  monadInv TRANSF. unfold tge; rewrite <- H0; auto.
-Qed.
-
-Lemma transf_programs:
-  AST.transform_partial_program transf_fundef (program_of_program prog) = OK (program_of_program tprog).
-Proof.
-  monadInv TRANSF. rewrite EQ. destruct x; reflexivity.
+  unfold tge, ge. destruct prog, tprog; simpl. destruct TRANSF as [_ EQ]. simpl in EQ. congruence.
 Qed.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
-Proof.
-  exact (Genv.find_symbol_transf_partial _ _ transf_programs).
-Qed.
+Proof (Genv.find_symbol_match (proj1 TRANSF)).
 
-Lemma public_preserved:
-  forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s.
-Proof.
-  exact (Genv.public_symbol_transf_partial _ _ transf_programs).
-Qed.
-
-Lemma varinfo_preserved:
-  forall b, Genv.find_var_info tge b = Genv.find_var_info ge b.
-Proof.
-  exact (Genv.find_var_info_transf_partial _ _ transf_programs).
-Qed.
+Lemma senv_preserved:
+  Senv.equiv ge tge.
+Proof (Genv.senv_match (proj1 TRANSF)).
 
 Lemma functions_translated:
   forall (v: val) (f: fundef),
   Genv.find_funct ge v = Some f ->
   exists tf, Genv.find_funct tge v = Some tf /\ transf_fundef f = OK tf.
-Proof.
-  exact (Genv.find_funct_transf_partial _ _ transf_programs).
-Qed.
+Proof (Genv.find_funct_transf_partial (proj1 TRANSF)).
 
 Lemma function_ptr_translated:
   forall (b: block) (f: fundef),
   Genv.find_funct_ptr ge b = Some f ->
   exists tf, Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
-Proof.
-  exact (Genv.find_funct_ptr_transf_partial _ _ transf_programs).
-Qed.
+Proof (Genv.find_funct_ptr_transf_partial (proj1 TRANSF)).
 
 Lemma type_of_fundef_preserved:
   forall fd tfd,
@@ -2073,8 +2051,7 @@ Proof.
   exploit external_call_mem_inject; eauto. apply match_globalenvs_preserves_globals; eauto with compat.
   intros [j' [tvres [tm' [P [Q [R [S [T [U V]]]]]]]]].
   econstructor; split.
-  apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto.
-  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
+  apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   econstructor; eauto with compat.
   eapply match_envs_set_opttemp; eauto.
   eapply match_envs_extcall; eauto.
@@ -2235,8 +2212,7 @@ Proof.
   eapply match_cont_globalenv. eexact (MCONT VSet.empty).
   intros [j' [tvres [tm' [P [Q [R [S [T [U V]]]]]]]]].
   econstructor; split.
-  apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto.
-  exact symbols_preserved. exact public_preserved. exact varinfo_preserved.
+  apply plus_one. econstructor; eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   econstructor; eauto.
   intros. apply match_cont_incr_bounds with (Mem.nextblock m) (Mem.nextblock tm).
   eapply match_cont_extcall; eauto. xomega. xomega.
@@ -2259,10 +2235,10 @@ Proof.
   exploit function_ptr_translated; eauto. intros [tf [A B]].
   econstructor; split.
   econstructor.
-  eapply Genv.init_mem_transf_partial. eexact transf_programs. eauto.
-  change (prog_main tprog) with (AST.prog_main tprog).
-  rewrite (transform_partial_program_main _ _ transf_programs).
+  eapply (Genv.init_mem_transf_partial (proj1 TRANSF)). eauto.
+  replace (prog_main tprog) with (prog_main prog). 
   instantiate (1 := b). rewrite <- H1. apply symbols_preserved.
+  generalize (match_program_main (proj1 TRANSF)). simpl; auto.
   eauto.
   rewrite <- H3; apply type_of_fundef_preserved; auto.
   econstructor; eauto.
@@ -2292,10 +2268,27 @@ Theorem transf_program_correct:
   forward_simulation (semantics1 prog) (semantics2 tprog).
 Proof.
   eapply forward_simulation_plus.
-  eexact public_preserved.
+  apply senv_preserved.
   eexact initial_states_simulation.
   eexact final_states_simulation.
   eexact step_simulation.
 Qed.
 
 End PRESERVATION.
+
+(** ** Commutation with linking *)
+
+Instance TransfSimplLocalsLink : TransfLink match_prog.
+Proof.
+  red; intros. eapply Ctypes.link_match_program; eauto. 
+- intros.
+Local Transparent Linker_fundef.
+  simpl in *; unfold link_fundef in *.
+  destruct f1; monadInv H3; destruct f2; monadInv H4; try discriminate.
+  destruct e; inv H2. exists (Internal x); split; auto. simpl; rewrite EQ; auto.
+  destruct e; inv H2. exists (Internal x); split; auto. simpl; rewrite EQ; auto.
+  destruct (external_function_eq e e0 && typelist_eq t t1 &&
+            type_eq t0 t2 && calling_convention_eq c c0); inv H2.
+  econstructor; split; eauto. 
+Qed.
+