Merge branch 'mppa-work' into mppa-thread

9 files changed, 232 insertions, 76 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 441c0a14..f2a68156 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -33,6 +33,7 @@ type inline_status =
 
 type atom_info =
   { a_storage: C.storage;              (* storage class *)
+    a_size: int64 option;              (* size in bytes *)
     a_alignment: int option;           (* alignment *)
     a_sections: Sections.section_name list; (* in which section to put it *)
       (* 1 section for data, 3 sections (code/lit/jumptbl) for functions *)
@@ -85,9 +86,14 @@ let atom_sections a =
   with Not_found ->
     []
 
-let atom_is_small_data a ofs =
+let atom_is_small_data a ofs  =
   try
-    (Hashtbl.find decl_atom a).a_access = Sections.Access_near
+    let info = Hashtbl.find decl_atom a in
+    info.a_access = Sections.Access_near
+    && (match info.a_size with
+        | None -> false
+        | Some sz ->
+            let ofs = camlint64_of_ptrofs ofs in 0L <= ofs && ofs < sz)
   with Not_found ->
     false
 
@@ -389,6 +395,7 @@ let name_for_string_literal s =
     Hashtbl.add decl_atom id
       { a_storage = C.Storage_static;
         a_alignment = Some 1;
+        a_size = Some (Int64.of_int (String.length s + 1));
         a_sections = [Sections.for_stringlit()];
         a_access = Sections.Access_default;
         a_inline = No_specifier;
@@ -416,9 +423,12 @@ let name_for_wide_string_literal s =
     incr stringNum;
     let name = Printf.sprintf "__stringlit_%d" !stringNum in
     let id = intern_string name in
+    let wchar_size = Machine.((!config).sizeof_wchar) in
     Hashtbl.add decl_atom id
       { a_storage = C.Storage_static;
-        a_alignment = Some Machine.((!config).sizeof_wchar);
+        a_alignment = Some wchar_size;
+        a_size = Some (Int64.(mul (of_int (List.length s + 1))
+                                  (of_int wchar_size)));
         a_sections = [Sections.for_stringlit()];
         a_access = Sections.Access_default;
         a_inline = No_specifier;
@@ -1261,6 +1271,7 @@ let convertFundef loc env fd =
   Hashtbl.add decl_atom id'
     { a_storage = fd.fd_storage;
       a_alignment = None;
+      a_size = None;
       a_sections = Sections.for_function env id' fd.fd_attrib;
       a_access = Sections.Access_default;
       a_inline = inline;
@@ -1361,6 +1372,7 @@ let convertGlobvar loc env (sto, id, ty, optinit) =
   Hashtbl.add decl_atom id'
     { a_storage = sto;
       a_alignment = Some (Z.to_int al);
+      a_size = Some (Z.to_int64 sz);
       a_sections = [section];
       a_access = access;
       a_inline = No_specifier;
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index aa73abb0..143e87a3 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -140,8 +140,8 @@ Definition classify_cast (tfrom tto: type) : classify_cast_cases :=
   | Tfloat F64 _, Tfloat F32 _ => cast_case_s2f
   | Tfloat F32 _, Tfloat F64 _ => cast_case_f2s
   (* To pointer types *)
-  | Tpointer _ _, Tint _ _ _ =>
-      if Archi.ptr64 then cast_case_i2l Unsigned else cast_case_pointer
+  | Tpointer _ _, Tint _ si _ =>
+      if Archi.ptr64 then cast_case_i2l si else cast_case_pointer
   | Tpointer _ _, Tlong _ _ =>
       if Archi.ptr64 then cast_case_pointer else cast_case_l2i I32 Unsigned
   | Tpointer _ _, (Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _) => cast_case_pointer
diff --git a/cfrontend/Csem.v b/cfrontend/Csem.v
index a76a14ba..6d2b470f 100644
--- a/cfrontend/Csem.v
+++ b/cfrontend/Csem.v
@@ -444,7 +444,7 @@ Lemma red_selection:
 Proof.
   intros. unfold Eselection.
   set (t := typ_of_type ty).
-  set (sg := mksignature (AST.Tint :: t :: t :: nil) (Some t) cc_default).
+  set (sg := mksignature (AST.Tint :: t :: t :: nil) t cc_default).
   assert (LK: lookup_builtin_function "__builtin_sel"%string sg = Some (BI_standard (BI_select t))).
   { unfold sg, t; destruct ty as   [ | ? ? ? | ? | [] ? | ? ? | ? ? ? | ? ? ? | ? ? | ? ? ];
     simpl; unfold Tptr; destruct Archi.ptr64; reflexivity. }
diff --git a/cfrontend/Cshmgen.v b/cfrontend/Cshmgen.v
index 792a73f9..5bd12d00 100644
--- a/cfrontend/Cshmgen.v
+++ b/cfrontend/Cshmgen.v
@@ -23,6 +23,7 @@
 Require Import Coqlib Maps Errors Integers Floats.
 Require Import AST Linking.
 Require Import Ctypes Cop Clight Cminor Csharpminor.
+Require Import Conventions1.
 
 Local Open Scope string_scope.
 Local Open Scope error_monad_scope.
@@ -558,6 +559,34 @@ Fixpoint typlist_of_arglist (al: list Clight.expr) (tyl: typelist)
       typ_of_type (default_argument_conversion (typeof a1)) :: typlist_of_arglist a2 Tnil
   end.
 
+(** Translate a function call.
+    Depending on the ABI, it may be necessary to normalize the value
+    returned by casting it to the return type of the function.
+    For example, in the x86 ABI, a return value of type "char" is
+    returned in register AL, leaving the top 24 bits of EAX
+    unspecified.  Hence, a cast to type "char" is needed to sign- or
+    zero-extend the returned integer before using it. *)
+
+Definition make_normalization (t: type) (a: expr) :=
+  match t with
+  | Tint IBool _ _ => Eunop Ocast8unsigned a
+  | Tint I8 Signed _ => Eunop Ocast8signed a
+  | Tint I8 Unsigned _ => Eunop Ocast8unsigned a
+  | Tint I16 Signed _ => Eunop Ocast16signed a
+  | Tint I16 Unsigned _ => Eunop Ocast16unsigned a
+  | _ => a
+  end.
+
+Definition make_funcall (x: option ident) (tres: type) (sg: signature)
+                      (fn: expr) (args: list expr): stmt :=
+  match x, return_value_needs_normalization sg.(sig_res) with
+  | Some id, true =>
+      Sseq (Scall x sg fn args)
+           (Sset id (make_normalization tres (Evar id)))
+  | _, _ =>
+      Scall x sg fn args
+  end.
+
 (** * Translation of statements *)
 
 (** [transl_statement nbrk ncnt s] returns a Csharpminor statement
@@ -601,10 +630,10 @@ Fixpoint transl_statement (ce: composite_env) (tyret: type) (nbrk ncnt: nat)
       | fun_case_f args res cconv =>
           do tb <- transl_expr ce b;
           do tcl <- transl_arglist ce cl args;
-          OK(Scall x {| sig_args := typlist_of_arglist cl args;
-                        sig_res  := opttyp_of_type res;
-                        sig_cc   := cconv |}
-                   tb tcl)
+          let sg := {| sig_args := typlist_of_arglist cl args;
+                       sig_res  := rettype_of_type res;
+                       sig_cc   := cconv |} in
+          OK (make_funcall x res sg tb tcl)
       | _ => Error(msg "Cshmgen.transl_stmt(call)")
       end
   | Clight.Sbuiltin x ef tyargs bl =>
@@ -667,7 +696,7 @@ Definition transl_var (ce: composite_env) (v: ident * type) :=
 
 Definition signature_of_function (f: Clight.function) :=
   {| sig_args := map typ_of_type (map snd (Clight.fn_params f));
-     sig_res  := opttyp_of_type (Clight.fn_return f);
+     sig_res  := rettype_of_type (Clight.fn_return f);
      sig_cc   := Clight.fn_callconv f |}.
 
 Definition transl_function (ce: composite_env) (f: Clight.function) : res function :=
diff --git a/cfrontend/Cshmgenproof.v b/cfrontend/Cshmgenproof.v
index 09e31cb2..1ceb8e4d 100644
--- a/cfrontend/Cshmgenproof.v
+++ b/cfrontend/Cshmgenproof.v
@@ -15,7 +15,7 @@
 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 Ctypes Ctyping Cop Clight Cminor Csharpminor.
 Require Import Cshmgen.
 
 (** * Relational specification of the transformation *)
@@ -996,6 +996,26 @@ Proof.
   eapply make_memcpy_correct with (b := b) (v := Vptr b' ofs'); eauto.
 Qed.
 
+Lemma make_normalization_correct:
+  forall e le m a v t,
+  eval_expr ge e le m a v ->
+  wt_val v t ->
+  eval_expr ge e le m (make_normalization t a) v.
+Proof.
+  intros. destruct t; simpl; auto. inv H0.
+- destruct i; simpl in H3.
+  + destruct s; econstructor; eauto; simpl; congruence.
+  + destruct s; econstructor; eauto; simpl; congruence.
+  + auto.
+  + econstructor; eauto; simpl; congruence.
+- auto.
+- destruct i.
+  + destruct s; econstructor; eauto. 
+  + destruct s; econstructor; eauto.
+  + auto.
+  + econstructor; eauto.
+Qed.
+
 End CONSTRUCTORS.
 
 (** * Basic preservation invariants *)
@@ -1360,7 +1380,16 @@ Inductive match_cont: composite_env -> type -> nat -> nat -> Clight.cont -> Csha
       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).
+                 (Kcall id tf te le tk)
+  | match_Kcall_normalize: forall ce tyret nbrk ncnt nbrk' ncnt' f e k id a tf te le tk cu,
+      linkorder cu prog ->
+      transl_function cu.(prog_comp_env) f = OK tf ->
+      match_env e te ->
+      match_cont cu.(prog_comp_env) (Clight.fn_return f) nbrk' ncnt' k tk ->
+      (forall v e le m, wt_val v tyret -> le!id = Some v -> eval_expr tge e le m a v) ->
+      match_cont ce tyret nbrk ncnt
+                 (Clight.Kcall (Some id) f e le k)
+                 (Kcall (Some id) tf te le (Kseq (Sset id a) tk)).
 
 Inductive match_states: Clight.state -> Csharpminor.state -> Prop :=
   | match_state:
@@ -1377,14 +1406,15 @@ Inductive match_states: Clight.state -> Csharpminor.state -> Prop :=
       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)
+          (MK: match_cont ce tres 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 ce
-          (MK: match_cont ce Tvoid 0%nat 0%nat k tk),
+      forall res tres k m tk ce
+          (MK: match_cont ce tres 0%nat 0%nat k tk)
+          (WT: wt_val res tres),
       match_states (Clight.Returnstate res k m)
                    (Returnstate res tk m).
 
@@ -1442,7 +1472,9 @@ Proof.
 - (* set *)
   auto.
 - (* call *)
-  simpl in TR. destruct (classify_fun (typeof e)); monadInv TR. auto.
+  simpl in TR. destruct (classify_fun (typeof e)); monadInv TR.
+  unfold make_funcall.
+  destruct o; auto; destruct Conventions1.return_value_needs_normalization; auto.
 - (* builtin *)
   auto.
 - (* seq *)
@@ -1500,24 +1532,26 @@ End FIND_LABEL.
 (** Properties of call continuations *)
 
 Lemma match_cont_call_cont:
-  forall ce' tyret' nbrk' ncnt' ce tyret nbrk ncnt k tk,
+  forall ce' 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).
+  match_cont ce' tyret nbrk' ncnt' (Clight.call_cont k) (call_cont tk).
 Proof.
   induction 1; simpl; auto.
-  constructor.
-  econstructor; eauto.
+- apply match_Kstop.
+- eapply match_Kcall; eauto.
+- eapply match_Kcall_normalize; eauto.
 Qed.
 
 Lemma match_cont_is_call_cont:
-  forall ce tyret nbrk ncnt k tk ce' tyret' nbrk' ncnt',
+  forall ce tyret nbrk ncnt k tk ce' nbrk' ncnt',
   match_cont ce tyret nbrk ncnt k tk ->
   Clight.is_call_cont k ->
-  match_cont ce' 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.
-  split; auto; econstructor; eauto.
+  split; auto; apply match_Kstop.
+  split; auto; eapply match_Kcall; eauto.
+  split; auto; eapply match_Kcall_normalize; eauto.
 Qed.
 
 (** The simulation proof *)
@@ -1549,19 +1583,44 @@ Proof.
 
 - (* call *)
   revert TR. simpl. case_eq (classify_fun (typeof a)); try congruence.
-  intros targs tres cc CF TR. monadInv TR. inv MTR.
+  intros targs tres cc CF TR. monadInv TR.
   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.
-  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.
-  eapply match_Kcall with (ce := prog_comp_env cu') (cu := cu); eauto.
-  simpl. auto.
+  set (sg := {| sig_args := typlist_of_arglist al targs;
+                sig_res := rettype_of_type tres;
+                sig_cc := cc |}) in *.
+  assert (SIG: funsig tfd = sg).
+  { unfold sg; erewrite typlist_of_arglist_eq by eauto.
+    eapply transl_fundef_sig1; eauto. rewrite H3; auto. }
+  assert (EITHER: tk' = tk /\ ts' = Scall optid sg x x0
+               \/ exists id, optid = Some id /\
+                  tk' = tk /\ ts' = Sseq (Scall optid sg x x0)
+                                         (Sset id (make_normalization tres (Evar id)))).
+  { unfold make_funcall in MTR.
+    destruct optid. destruct Conventions1.return_value_needs_normalization.
+    inv MTR. right; exists i; auto.
+    inv MTR; auto.
+    inv MTR; auto. }
+  destruct EITHER as [(EK & ES) | (id & EI & EK & ES)]; rewrite EK, ES.
+  + (* without normalization of return value *)
+    econstructor; split.
+    apply plus_one. eapply step_call; eauto.
+    eapply transl_expr_correct with (cunit := cu); eauto.
+    eapply transl_arglist_correct with (cunit := cu); eauto.
+    econstructor; eauto.
+    eapply match_Kcall with (ce := prog_comp_env cu') (cu := cu); eauto.
+    exact I.
+  + (* with normalization of return value *)
+    subst optid.
+    econstructor; split.
+    eapply plus_two. apply step_seq. eapply step_call; eauto. 
+    eapply transl_expr_correct with (cunit := cu); eauto.
+    eapply transl_arglist_correct with (cunit := cu); eauto.
+    traceEq.
+    econstructor; eauto.
+    eapply match_Kcall_normalize  with (ce := prog_comp_env cu') (cu := cu); eauto.
+    intros. eapply make_normalization_correct; eauto. constructor; eauto.
+    exact I.
 
 - (* builtin *)
   monadInv TR. inv MTR.
@@ -1658,6 +1717,7 @@ Proof.
   eapply match_env_free_blocks; eauto.
   eapply match_returnstate with (ce := prog_comp_env cu); eauto.
   eapply match_cont_call_cont. eauto.
+  constructor.
 
 - (* return some *)
   monadInv TR. inv MTR.
@@ -1667,6 +1727,7 @@ Proof.
   eapply match_env_free_blocks; eauto.
   eapply match_returnstate with (ce := prog_comp_env cu); eauto.
   eapply match_cont_call_cont. eauto.
+  apply wt_val_casted. eapply cast_val_is_casted; eauto.
 
 - (* skip call *)
   monadInv TR. inv MTR.
@@ -1675,6 +1736,7 @@ Proof.
   apply plus_one. apply step_skip_call. auto.
   eapply match_env_free_blocks; eauto.
   eapply match_returnstate with (ce := prog_comp_env cu); eauto.
+  constructor.
 
 - (* switch *)
   monadInv TR.
@@ -1738,20 +1800,33 @@ Proof.
   simpl. econstructor; eauto.
   unfold transl_function. rewrite EQ; simpl. rewrite EQ1; simpl. auto.
   constructor.
+  replace (fn_return f) with tres. eassumption.
+  simpl in TY. unfold type_of_function in TY. congruence. 
 
 - (* external function *)
   inv TR.
   exploit match_cont_is_call_cont; eauto. intros [A B].
   econstructor; split.
-  apply plus_one. constructor. eauto.
+  apply plus_one. constructor.
   eapply external_call_symbols_preserved; eauto. apply senv_preserved.
   eapply match_returnstate with (ce := ce); eauto.
+  apply has_rettype_wt_val. 
+  replace (rettype_of_type tres0) with (sig_res (ef_sig ef)).
+  eapply external_call_well_typed_gen; eauto.
+  rewrite H5. simpl. simpl in TY. congruence.
 
 - (* returnstate *)
   inv MK.
-  econstructor; split.
-  apply plus_one. constructor.
-  econstructor; eauto. simpl; reflexivity. constructor.
+  + (* without normalization *)
+    econstructor; split.
+    apply plus_one. constructor.
+    econstructor; eauto. simpl; reflexivity. constructor.
+  + (* with normalization *)
+    econstructor; split.
+    eapply plus_three. econstructor. econstructor. constructor.
+    simpl. apply H13. eauto. apply PTree.gss.
+    traceEq.
+    simpl. rewrite PTree.set2. econstructor; eauto. simpl; reflexivity. constructor.
 Qed.
 
 Lemma transl_initial_states:
diff --git a/cfrontend/Csyntax.v b/cfrontend/Csyntax.v
index c34a5e13..e3e2c1e9 100644
--- a/cfrontend/Csyntax.v
+++ b/cfrontend/Csyntax.v
@@ -106,7 +106,7 @@ Definition Epreincr (id: incr_or_decr) (l: expr) (ty: type) :=
 
 Definition Eselection (r1 r2 r3: expr) (ty: type) :=
   let t := typ_of_type ty in
-  let sg := mksignature (AST.Tint :: t :: t :: nil) (Some t) cc_default in
+  let sg := mksignature (AST.Tint :: t :: t :: nil) t cc_default in
   Ebuiltin (EF_builtin "__builtin_sel"%string sg)
            (Tcons type_bool (Tcons ty (Tcons ty Tnil)))
            (Econs r1 (Econs r2 (Econs r3 Enil)))
diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v
index bfc5daa9..664a60c5 100644
--- a/cfrontend/Ctypes.v
+++ b/cfrontend/Ctypes.v
@@ -732,8 +732,21 @@ Definition typ_of_type (t: type) : AST.typ :=
   | Tpointer _ _ | Tarray _ _ _ | Tfunction _ _ _ | Tstruct _ _ | Tunion _ _ => AST.Tptr
   end.
 
-Definition opttyp_of_type (t: type) : option AST.typ :=
-  if type_eq t Tvoid then None else Some (typ_of_type t).
+Definition rettype_of_type (t: type) : AST.rettype :=
+  match t with
+  | Tvoid => AST.Tvoid
+  | Tint I32 _ _ => AST.Tint
+  | Tint I8 Signed _ => AST.Tint8signed
+  | Tint I8 Unsigned _ => AST.Tint8unsigned
+  | Tint I16 Signed _ => AST.Tint16signed
+  | Tint I16 Unsigned _ => AST.Tint16unsigned
+  | Tint IBool _ _ => AST.Tint8unsigned
+  | Tlong _ _ => AST.Tlong
+  | Tfloat F32 _ => AST.Tsingle
+  | Tfloat F64 _ => AST.Tfloat
+  | Tpointer _ _ => AST.Tptr
+  | Tarray _ _ _ | Tfunction _ _ _ | Tstruct _ _ | Tunion _ _ => AST.Tvoid
+  end.
 
 Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ :=
   match tl with
@@ -742,7 +755,7 @@ Fixpoint typlist_of_typelist (tl: typelist) : list AST.typ :=
   end.
 
 Definition signature_of_type (args: typelist) (res: type) (cc: calling_convention): signature :=
-  mksignature (typlist_of_typelist args) (opttyp_of_type res) cc.
+  mksignature (typlist_of_typelist args) (rettype_of_type res) cc.
 
 (** * Construction of the composite environment *)
 
diff --git a/cfrontend/Ctyping.v b/cfrontend/Ctyping.v
index b92a9bac..00fcf8ab 100644
--- a/cfrontend/Ctyping.v
+++ b/cfrontend/Ctyping.v
@@ -397,10 +397,10 @@ Inductive wt_rvalue : expr -> Prop :=
       wt_arguments rargs tyargs ->
       (* This typing rule is specialized to the builtin invocations generated
          by C2C, which are either __builtin_sel or builtins returning void. *)
-         (ty = Tvoid /\ sig_res (ef_sig ef) = None)
+         (ty = Tvoid /\ sig_res (ef_sig ef) = AST.Tvoid)
       \/ (tyargs = Tcons type_bool (Tcons ty (Tcons ty Tnil))
           /\ let t := typ_of_type ty in
-             let sg := mksignature (AST.Tint :: t :: t :: nil) (Some t) cc_default in
+             let sg := mksignature (AST.Tint :: t :: t :: nil) t cc_default in
              ef = EF_builtin "__builtin_sel"%string sg) ->
       wt_rvalue (Ebuiltin ef tyargs rargs ty)
   | wt_Eparen: forall r tycast ty,
@@ -521,11 +521,20 @@ Fixpoint bind_globdef (e: typenv) (l: list (ident * globdef fundef type)) : type
   | (id, Gvar v) :: l => bind_globdef (PTree.set id v.(gvar_info) e) l
   end.
 
+Inductive wt_fundef (ce: composite_env) (e: typenv) : fundef -> Prop :=
+  | wt_fundef_internal: forall f,
+      wt_function ce e f ->
+      wt_fundef ce e (Internal f)
+  | wt_fundef_external: forall ef targs tres cc,
+      (ef_sig ef).(sig_res) = rettype_of_type tres ->
+      wt_fundef ce e (External ef targs tres cc).
+
 Inductive wt_program : program -> Prop :=
   | wt_program_intro: forall p,
       let e := bind_globdef (PTree.empty _) p.(prog_defs) in
-      (forall id f, In (id, Gfun (Internal f)) p.(prog_defs) ->
-         wt_function p.(prog_comp_env) e f) ->
+      (forall id fd,
+         In (id, Gfun fd) p.(prog_defs) ->
+         wt_fundef p.(prog_comp_env) e fd) ->
       wt_program p.
 
 Hint Constructors wt_val wt_rvalue wt_lvalue wt_stmt wt_lblstmts: ty.
@@ -745,7 +754,7 @@ Definition ebuiltin (ef: external_function) (tyargs: typelist) (args: exprlist)
   do x1 <- check_rvals args;
   do x2 <- check_arguments args tyargs;
   if type_eq tyres Tvoid
-  && opt_typ_eq (sig_res (ef_sig ef)) None
+  && AST.rettype_eq (sig_res (ef_sig ef)) AST.Tvoid
   then OK (Ebuiltin ef tyargs args tyres)
   else Error (msg "builtin: wrong type decoration").
 
@@ -915,7 +924,8 @@ Definition retype_function (ce: composite_env) (e: typenv) (f: function) : res f
 Definition retype_fundef (ce: composite_env) (e: typenv) (fd: fundef) : res fundef :=
   match fd with
   | Internal f => do f' <- retype_function ce e f; OK (Internal f')
-  | External id args res cc => OK fd
+  | External ef args res cc =>
+      assertion (rettype_eq (ef_sig ef).(sig_res) (rettype_of_type res)); OK fd
   end.
 
 Definition typecheck_program (p: program) : res program :=
@@ -987,6 +997,7 @@ Proof.
           classify_cast (Tint i s a) t2 <> cast_case_default).
   {
     unfold classify_cast. destruct t2; try congruence. destruct f; congruence.
+    destruct Archi.ptr64; congruence.
   }
   destruct i; auto.
 Qed.
@@ -1240,7 +1251,7 @@ Lemma ebuiltin_sound:
 Proof.
   intros. monadInv H.
   destruct (type_eq tyres Tvoid); simpl in EQ2; try discriminate.
-  destruct (opt_typ_eq (sig_res (ef_sig ef)) None); inv EQ2.
+  destruct (rettype_eq (sig_res (ef_sig ef)) AST.Tvoid); inv EQ2.
   econstructor; eauto. eapply check_arguments_sound; eauto.
 Qed.
 
@@ -1372,6 +1383,14 @@ Proof.
   intros. monadInv H. constructor; simpl. eapply retype_stmt_sound; eauto.
 Qed.
 
+Lemma retype_fundef_sound:
+  forall ce e fd fd', retype_fundef ce e fd = OK fd' -> wt_fundef ce e fd'.
+Proof.
+  intros. destruct fd; monadInv H.
+- constructor; eapply retype_function_sound; eauto.
+- constructor; auto.
+Qed.
+
 Theorem typecheck_program_sound:
   forall p p', typecheck_program p = OK p' -> wt_program p'.
 Proof.
@@ -1394,11 +1413,11 @@ Proof.
     inv H1. simpl. auto.
   }
   rewrite ENVS.
-  intros id f. revert MATCH; generalize (prog_defs p) (AST.prog_defs tp).
+  intros id fd. revert MATCH; generalize (prog_defs p) (AST.prog_defs tp).
   induction 1; simpl; intros.
   contradiction.
   destruct H0; auto. subst b1; inv H. simpl in H1. inv H1. 
-  destruct f1; monadInv H4. eapply retype_function_sound; eauto.
+  eapply retype_fundef_sound; eauto.
 Qed.
 
 (** * Subject reduction *)
@@ -1710,6 +1729,26 @@ Proof.
   inv H; auto.
 Qed.
 
+Lemma has_rettype_wt_val:
+  forall v ty,
+  Val.has_rettype v (rettype_of_type ty) -> wt_val v ty.
+Proof.
+  unfold rettype_of_type, Val.has_rettype, Val.has_type; destruct ty; intros.
+- destruct v; contradiction || constructor.
+- destruct i.
+  + destruct s; destruct v; try contradiction; constructor; red; auto.
+  + destruct s; destruct v; try contradiction; constructor; red; auto.
+  + destruct v; try contradiction; constructor; auto.
+  + destruct v; try contradiction; constructor; red; auto.
+- destruct v; try contradiction; constructor; auto.
+- destruct f; destruct v; try contradiction; constructor.
+- unfold Tptr in *; destruct v; destruct Archi.ptr64 eqn:P64; try contradiction; constructor; auto.
+- destruct v; contradiction || constructor.
+- destruct v; contradiction || constructor.
+- destruct v; contradiction || constructor.
+- destruct v; contradiction || constructor.
+Qed.
+
 Lemma wt_rred:
   forall ge tenv a m t a' m',
   rred ge a m t a' m' -> wt_rvalue ge tenv a -> wt_rvalue ge tenv a'.
@@ -1749,7 +1788,7 @@ Proof.
 - (* builtin *) subst. destruct H7 as [(A & B) | (A & B)].
 + subst ty. auto with ty.
 + simpl in B. set (T := typ_of_type ty) in *. 
-  set (sg := mksignature (AST.Tint :: T :: T :: nil) (Some T) cc_default) in *.
+  set (sg := mksignature (AST.Tint :: T :: T :: nil) T cc_default) in *.
   assert (LK: lookup_builtin_function "__builtin_sel"%string sg = Some (BI_standard (BI_select T))).
   { unfold sg, T; destruct ty as   [ | ? ? ? | ? | [] ? | ? ? | ? ? ? | ? ? ? | ? ? | ? ? ];
     simpl; unfold Tptr; destruct Archi.ptr64; reflexivity. }
@@ -1895,12 +1934,6 @@ Hypothesis WTPROG: wt_program prog.
 Let ge := globalenv prog.
 Let gtenv := bind_globdef (PTree.empty _) prog.(prog_defs).
 
-Hypothesis WT_EXTERNAL:
-  forall id ef args res cc vargs m t vres m',
-  In (id, Gfun (External ef args res cc)) prog.(prog_defs) ->
-  external_call ef ge vargs m t vres m' ->
-  wt_val vres res.
-
 Inductive wt_expr_cont: typenv -> function -> cont -> Prop :=
   | wt_Kdo: forall te f k,
       wt_stmt_cont te f k ->
@@ -1999,12 +2032,6 @@ Proof.
   induction 1; simpl; auto; econstructor; eauto.
 Qed.
 
-Definition wt_fundef (fd: fundef) :=
-  match fd with
-  | Internal f => wt_function ge gtenv f
-  | External ef targs tres cc => True
-  end.
-
 Definition fundef_return (fd: fundef) : type :=
   match fd with
   | Internal f => f.(fn_return)
@@ -2012,10 +2039,10 @@ Definition fundef_return (fd: fundef) : type :=
   end.
 
 Lemma wt_find_funct:
-  forall v fd, Genv.find_funct ge v = Some fd -> wt_fundef fd.
+  forall v fd, Genv.find_funct ge v = Some fd -> wt_fundef ge gtenv fd.
 Proof.
   intros. apply Genv.find_funct_prop with (p := prog) (v := v); auto.
-  intros. inv WTPROG. destruct f; simpl; auto. apply H1 with id; auto.
+  intros. inv WTPROG. apply H1 with id; auto.
 Qed.
 
 Inductive wt_state: state -> Prop :=
@@ -2031,7 +2058,7 @@ Inductive wt_state: state -> Prop :=
       wt_state (ExprState f r k e m)
   | wt_call_state: forall b fd vargs k m
         (WTK: wt_call_cont k (fundef_return fd))
-        (WTFD: wt_fundef fd)
+        (WTFD: wt_fundef ge gtenv fd)
         (FIND: Genv.find_funct ge b = Some fd),
       wt_state (Callstate fd vargs k m)
   | wt_return_state: forall v k m ty
@@ -2088,7 +2115,6 @@ Qed.
 
 End WT_FIND_LABEL.
 
-
 Lemma preservation_estep:
   forall S t S', estep ge S t S' -> wt_state S -> wt_state S'.
 Proof.
@@ -2163,9 +2189,10 @@ Proof.
 - inv WTS; eauto with ty.
 - exploit wt_find_label. eexact WTB. eauto. eapply call_cont_wt'; eauto.
   intros [A B]. eauto with ty.
-- simpl in WTFD; inv WTFD. econstructor; eauto. apply wt_call_cont_stmt_cont; auto.
-- exploit (Genv.find_funct_inversion prog); eauto. intros (id & A).
-  econstructor; eauto.
+- inv WTFD. inv H3. econstructor; eauto. apply wt_call_cont_stmt_cont; auto.
+- inv WTFD. econstructor; eauto.
+  apply has_rettype_wt_val. simpl; rewrite <- H1.
+  eapply external_call_well_typed_gen; eauto.
 - inv WTK. eauto with ty.
 Qed.
 
@@ -2180,7 +2207,7 @@ Theorem wt_initial_state:
 Proof.
   intros. inv H. econstructor. constructor.
   apply Genv.find_funct_ptr_prop with (p := prog) (b := b); auto.
-  intros. inv WTPROG. destruct f0; simpl; auto. apply H4 with id; auto.
+  intros. inv WTPROG. apply H4 with id; auto.
   instantiate (1 := (Vptr b Ptrofs.zero)). rewrite Genv.find_funct_find_funct_ptr. auto.
 Qed.
 
diff --git a/cfrontend/PrintCsyntax.ml b/cfrontend/PrintCsyntax.ml
index 1c9729c5..03dc5837 100644
--- a/cfrontend/PrintCsyntax.ml
+++ b/cfrontend/PrintCsyntax.ml
@@ -19,7 +19,7 @@ open Format
 open Camlcoq
 open Values
 open AST
-open Ctypes
+open! Ctypes
 open Cop
 open Csyntax
 
@@ -85,7 +85,7 @@ let name_optid id =
 
 let rec name_cdecl id ty =
   match ty with
-  | Tvoid ->
+  | Ctypes.Tvoid ->
       "void" ^ name_optid id
   | Ctypes.Tint(sz, sg, a) ->
       name_inttype sz sg ^ attributes a ^ name_optid id