Refine the type of function results in AST.signature

Before it was "option typ".  Now it is a proper inductive type
that can also express small integer types (8/16-bit unsigned/signed integers).

One benefit is that external functions get more precise types that
control better their return values.  As a consequence,
the CompCert C type preservation property now holds unconditionally,
without extra typing hypotheses on external functions.

13 files changed, 101 insertions, 90 deletions

diff --git a/backend/Allocation.v b/backend/Allocation.v
index 13e14530..08e0a4f4 100644
--- a/backend/Allocation.v
+++ b/backend/Allocation.v
@@ -734,11 +734,11 @@ Function add_equations_args (rl: list reg) (tyl: list typ) (ll: list (rpair loc)
 (** [add_equations_res] is similar but is specialized to the case where
   there is only one pseudo-register. *)
 
-Function add_equations_res (r: reg) (oty: option typ) (p: rpair mreg) (e: eqs) : option eqs :=
-  match p, oty with
+Function add_equations_res (r: reg) (ty: typ) (p: rpair mreg) (e: eqs) : option eqs :=
+  match p, ty with
   | One mr, _ =>
       Some (add_equation (Eq Full r (R mr)) e)
-  | Twolong mr1 mr2, Some Tlong =>
+  | Twolong mr1 mr2, Tlong =>
       if Archi.ptr64 then None else
       Some (add_equation (Eq Low r (R mr2)) (add_equation (Eq High r (R mr1)) e))
   | _, _ =>
@@ -1084,7 +1084,7 @@ Definition transfer_aux (f: RTL.function) (env: regenv)
   | BStailcall sg ros args mv1 ros' =>
       let args' := loc_arguments sg in
       assertion (tailcall_is_possible sg);
-      assertion (opt_typ_eq sg.(sig_res) f.(RTL.fn_sig).(sig_res));
+      assertion (rettype_eq sg.(sig_res) f.(RTL.fn_sig).(sig_res));
       assertion (ros_compatible_tailcall ros');
       do e1 <- add_equation_ros ros ros' empty_eqs;
       do e2 <- add_equations_args args (sig_args sg) args' e1;
@@ -1114,7 +1114,7 @@ Definition transfer_aux (f: RTL.function) (env: regenv)
       track_moves env mv empty_eqs
   | BSreturn (Some arg) mv =>
       let arg' := loc_result (RTL.fn_sig f) in
-      do e1 <- add_equations_res arg (sig_res (RTL.fn_sig f)) arg' empty_eqs;
+      do e1 <- add_equations_res arg (proj_sig_res (RTL.fn_sig f)) arg' empty_eqs;
       track_moves env mv e1
   end.
 
diff --git a/backend/Allocproof.v b/backend/Allocproof.v
index 1804f46b..51755912 100644
--- a/backend/Allocproof.v
+++ b/backend/Allocproof.v
@@ -1301,10 +1301,10 @@ Proof.
 Qed.
 
 Lemma add_equations_res_lessdef:
-  forall r oty l e e' rs ls,
-  add_equations_res r oty l e = Some e' ->
+  forall r ty l e e' rs ls,
+  add_equations_res r ty l e = Some e' ->
   satisf rs ls e' ->
-  Val.has_type rs#r (match oty with Some ty => ty | None => Tint end) ->
+  Val.has_type rs#r ty ->
   Val.lessdef rs#r (Locmap.getpair (map_rpair R l) ls).
 Proof.
   intros. functional inversion H; simpl.
@@ -1892,7 +1892,7 @@ Qed.
 
 Inductive match_stackframes: list RTL.stackframe -> list LTL.stackframe -> signature -> Prop :=
   | match_stackframes_nil: forall sg,
-      sg.(sig_res) = Some Tint ->
+      sg.(sig_res) = Tint ->
       match_stackframes nil nil sg
   | match_stackframes_cons:
       forall res f sp pc rs s tf bb ls ts sg an e env
@@ -2425,13 +2425,13 @@ Proof.
                           (return_regs (parent_locset ts) ls1))
   with (Locmap.getpair (map_rpair R (loc_result (RTL.fn_sig f))) ls1).
   eapply add_equations_res_lessdef; eauto.
-  rewrite H13. apply WTRS.
+  rewrite <- H14. apply WTRS.
   generalize (loc_result_caller_save (RTL.fn_sig f)).
   destruct (loc_result (RTL.fn_sig f)); simpl.
   intros A; rewrite A; auto.
   intros [A B]; rewrite A, B; auto.
   apply return_regs_agree_callee_save.
-  unfold proj_sig_res. rewrite <- H11; rewrite H13. apply WTRS.
+  rewrite <- H11, <- H14. apply WTRS.
 
 (* internal function *)
 - monadInv FUN. simpl in *.
@@ -2463,7 +2463,8 @@ Proof.
   simpl. destruct (loc_result (ef_sig ef)) eqn:RES; simpl.
   rewrite Locmap.gss; auto.
   generalize (loc_result_pair (ef_sig ef)); rewrite RES; intros (A & B & C & D & E).
-  exploit external_call_well_typed; eauto. unfold proj_sig_res; rewrite B. intros WTRES'.
+  assert (WTRES': Val.has_type v' Tlong).
+  { rewrite <- B. eapply external_call_well_typed; eauto. }
   rewrite Locmap.gss. rewrite Locmap.gso by (red; auto). rewrite Locmap.gss.
   rewrite val_longofwords_eq_1 by auto. auto.
   red; intros. rewrite (AG l H0).
diff --git a/backend/Asmexpandaux.ml b/backend/Asmexpandaux.ml
index f5c76925..0530abe4 100644
--- a/backend/Asmexpandaux.ml
+++ b/backend/Asmexpandaux.ml
@@ -96,7 +96,7 @@ let translate_annot sp preg_to_dwarf annot =
   | a::_ -> aux a)
 
 let builtin_nop =
-  let signature ={sig_args = []; sig_res = None; sig_cc = cc_default} in
+  let signature ={sig_args = []; sig_res = Tvoid; sig_cc = cc_default} in
   let name = coqstring_of_camlstring "__builtin_nop" in
   Pbuiltin(EF_builtin(name,signature),[],BR_none)
 
diff --git a/backend/Cminor.v b/backend/Cminor.v
index ca01ad50..91a4c104 100644
--- a/backend/Cminor.v
+++ b/backend/Cminor.v
@@ -676,12 +676,24 @@ Definition outcome_block (out: outcome) : outcome :=
   | out => out
   end.
 
+(*
 Definition outcome_result_value
-    (out: outcome) (retsig: option typ) (vres: val) : Prop :=
+    (out: outcome) (retsig: rettype) (vres: val) : Prop :=
   match out with
   | Out_normal => vres = Vundef
   | Out_return None => vres = Vundef
-  | Out_return (Some v) => retsig <> None /\ vres = v
+  | Out_return (Some v) => retsig <> Tvoid /\ vres = v
+  | Out_tailcall_return v => vres = v
+  | _ => False
+  end.
+*)
+
+Definition outcome_result_value
+    (out: outcome) (vres: val) : Prop :=
+  match out with
+  | Out_normal => vres = Vundef
+  | Out_return None => vres = Vundef
+  | Out_return (Some v) => vres = v
   | Out_tailcall_return v => vres = v
   | _ => False
   end.
@@ -711,7 +723,7 @@ Inductive eval_funcall:
       Mem.alloc m 0 f.(fn_stackspace) = (m1, sp) ->
       set_locals f.(fn_vars) (set_params vargs f.(fn_params)) = e ->
       exec_stmt f (Vptr sp Ptrofs.zero) e m1 f.(fn_body) t e2 m2 out ->
-      outcome_result_value out f.(fn_sig).(sig_res) vres ->
+      outcome_result_value out vres ->
       outcome_free_mem out m2 sp f.(fn_stackspace) m3 ->
       eval_funcall m (Internal f) vargs t m3 vres
   | eval_funcall_external:
@@ -995,7 +1007,7 @@ Proof.
   subst vres. replace k with (call_cont k') by congruence.
   apply star_one. apply step_return_0; auto.
   (* Out_return Some *)
-  destruct H3. subst vres.
+  subst vres.
   replace k with (call_cont k') by congruence.
   apply star_one. eapply step_return_1; eauto.
   (* Out_tailcall_return *)
diff --git a/backend/Cminortyping.v b/backend/Cminortyping.v
index fccbda27..92ec45f2 100644
--- a/backend/Cminortyping.v
+++ b/backend/Cminortyping.v
@@ -130,7 +130,7 @@ Definition opt_set (e: S.typenv) (optid: option ident) (ty: typ) : res S.typenv
   | Some id => S.set e id ty
   end.
 
-Fixpoint type_stmt (tret: option typ) (e: S.typenv) (s: stmt) : res S.typenv :=
+Fixpoint type_stmt (tret: rettype) (e: S.typenv) (s: stmt) : res S.typenv :=
   match s with
   | Sskip => OK e
   | Sassign id a => type_assign e id a
@@ -141,7 +141,7 @@ Fixpoint type_stmt (tret: option typ) (e: S.typenv) (s: stmt) : res S.typenv :=
       do e2 <- type_exprlist e1 args sg.(sig_args);
       opt_set e2 optid (proj_sig_res sg)
   | Stailcall sg fn args =>
-      assertion (opt_typ_eq sg.(sig_res) tret);
+      assertion (rettype_eq sg.(sig_res) tret);
       do e1 <- type_expr e fn Tptr;
       type_exprlist e1 args sg.(sig_args)
   | Sbuiltin optid ef args =>
@@ -163,10 +163,14 @@ Fixpoint type_stmt (tret: option typ) (e: S.typenv) (s: stmt) : res S.typenv :=
   | Sswitch sz a tbl dfl =>
       type_expr e a (if sz then Tlong else Tint)
   | Sreturn opta =>
-      match opta, tret with
-      | None, _ => OK e
-      | Some a, Some t => type_expr e a t
-      | _, _ => Error (msg "inconsistent return")
+      match opta with
+      | None => OK e
+      | Some a => type_expr e a (proj_rettype tret)
+(*
+          if rettype_eq tret Tvoid
+          then Error (msg "inconsistent return")
+          else type_expr e a (proj_rettype tret)
+*)
       end
   | Slabel lbl s1 =>
       type_stmt tret e s1
@@ -186,7 +190,7 @@ Definition type_function (f: function) : res typenv :=
 Section SPEC.
 
 Variable env: ident -> typ.
-Variable tret: option typ.
+Variable tret: rettype.
 
 Inductive wt_expr: expr -> typ -> Prop :=
   | wt_Evar: forall id,
@@ -205,9 +209,9 @@ Inductive wt_expr: expr -> typ -> Prop :=
       wt_expr a1 Tptr ->
       wt_expr (Eload chunk a1) (type_of_chunk chunk).
 
-Definition wt_opt_assign (optid: option ident) (optty: option typ) : Prop :=
+Definition wt_opt_assign (optid: option ident) (ty: rettype) : Prop :=
   match optid with
-  | Some id => match optty with Some ty => ty | None => Tint end = env id
+  | Some id => proj_rettype ty = env id
   | _ => True
   end.
 
@@ -251,8 +255,8 @@ Inductive wt_stmt: stmt -> Prop :=
       wt_stmt (Sswitch sz a tbl dfl)
   | wt_Sreturn_none:
       wt_stmt (Sreturn None)
-  | wt_Sreturn_some: forall a t,
-      tret = Some t -> wt_expr a t ->
+  | wt_Sreturn_some: forall a,
+      wt_expr a (proj_rettype tret) ->
       wt_stmt (Sreturn (Some a))
   | wt_Slabel: forall lbl s1,
       wt_stmt s1 ->
@@ -393,7 +397,7 @@ Proof.
 - constructor; eauto.
 - constructor.
 - constructor; eauto using type_expr_sound with ty.
-- destruct tret, o; try (monadInv T); econstructor; eauto using type_expr_sound with ty.
+- destruct o; try (monadInv T); econstructor; eauto using type_expr_sound with ty.
 - constructor; eauto.
 - constructor.
 Qed.
@@ -414,9 +418,9 @@ Definition wt_env (env: typenv) (e: Cminor.env) : Prop :=
 Definition def_env (f: function) (e: Cminor.env) : Prop :=
   forall id, In id f.(fn_params) \/ In id f.(fn_vars) -> exists v, e!id = Some v.
 
-Inductive wt_cont_call: cont -> option typ -> Prop :=
+Inductive wt_cont_call: cont -> rettype -> Prop :=
   | wt_cont_Kstop:
-      wt_cont_call Kstop (Some Tint)
+      wt_cont_call Kstop Tint
   | wt_cont_Kcall: forall optid f sp e k tret env
         (WT_FN: wt_function env f)
         (WT_CONT: wt_cont env f.(fn_sig).(sig_res) k)
@@ -425,7 +429,7 @@ Inductive wt_cont_call: cont -> option typ -> Prop :=
         (WT_DEST: wt_opt_assign env optid tret),
       wt_cont_call (Kcall optid f sp e k) tret
 
-with wt_cont: typenv -> option typ -> cont -> Prop :=
+with wt_cont: typenv -> rettype -> cont -> Prop :=
   | wt_cont_Kseq: forall env tret s k,
       wt_stmt env tret s ->
       wt_cont env tret k ->
@@ -451,7 +455,7 @@ Inductive wt_state: state -> Prop :=
         (WT_CONT: wt_cont_call k (funsig f).(sig_res)),
       wt_state (Callstate f args k m)
   | wt_return_state: forall v k m tret
-        (WT_RES: Val.has_type v (match tret with None => Tint | Some t => t end))
+        (WT_RES: Val.has_type v (proj_rettype tret))
         (WT_CONT: wt_cont_call k tret),
       wt_state (Returnstate v k m).
 
@@ -651,9 +655,8 @@ Proof.
   rewrite H8; eapply call_cont_wt; eauto.
 - inv WT_STMT. exploit external_call_well_typed; eauto. intros TRES.
   econstructor; eauto using wt_Sskip.
-  unfold proj_sig_res in TRES; red in H5.
-  destruct optid. rewrite H5 in TRES. apply wt_env_assign; auto. assumption.
-  destruct optid. apply def_env_assign; auto. assumption.
+  destruct optid; auto. apply wt_env_assign; auto. rewrite <- H5; auto.
+  destruct optid; auto. apply def_env_assign; auto.
 - inv WT_STMT. econstructor; eauto. econstructor; eauto.
 - inv WT_STMT. destruct b; econstructor; eauto.
 - inv WT_STMT. econstructor; eauto. econstructor; eauto. constructor; auto.
@@ -664,7 +667,7 @@ Proof.
 - econstructor; eauto using wt_Sexit.
 - inv WT_STMT. econstructor; eauto using call_cont_wt. exact I.
 - inv WT_STMT. econstructor; eauto using call_cont_wt.
-  rewrite H2. eapply wt_eval_expr; eauto.
+  eapply wt_eval_expr; eauto.
 - inv WT_STMT. econstructor; eauto.
 - inversion WT_FN; subst.
   assert (WT_CK: wt_cont env (sig_res (fn_sig f)) (call_cont k)).
@@ -675,7 +678,7 @@ Proof.
   constructor; auto.
   apply wt_env_set_locals. apply wt_env_set_params. rewrite H2; auto.
   red; intros. apply def_set_locals. destruct H4; auto. left; apply def_set_params; auto.
-- exploit external_call_well_typed; eauto. unfold proj_sig_res. simpl in *. intros.
+- exploit external_call_well_typed; eauto. intros.
   econstructor; eauto.
 - inv WT_CONT. econstructor; eauto using wt_Sskip.
   red in WT_DEST.
diff --git a/backend/PrintAsmaux.ml b/backend/PrintAsmaux.ml
index 8652b2c5..d82e6f84 100644
--- a/backend/PrintAsmaux.ml
+++ b/backend/PrintAsmaux.ml
@@ -99,7 +99,7 @@ let exists_constants () =
 
 let current_function_stacksize = ref 0l
 let current_function_sig =
-  ref { sig_args = []; sig_res = None; sig_cc = cc_default }
+  ref { sig_args = []; sig_res = Tvoid; sig_cc = cc_default }
 
 (* Functions for printing of symbol names *)
 let elf_symbol oc symb =
@@ -268,8 +268,8 @@ let re_asm_param_2 = Str.regexp "%\\([QR]?\\)\\([0-9]+\\)"
 let print_inline_asm print_preg oc txt sg args res =
   let (operands, ty_operands) =
     match sg.sig_res with
-    | None -> (args, sg.sig_args)
-    | Some tres -> (builtin_arg_of_res res :: args, tres :: sg.sig_args) in
+    | Tvoid -> (args, sg.sig_args)
+    | tres -> (builtin_arg_of_res res :: args, proj_rettype tres :: sg.sig_args) in
   let print_fragment = function
   | Str.Text s ->
       output_string oc s
diff --git a/backend/PrintCminor.ml b/backend/PrintCminor.ml
index 8c255a65..b77c5645 100644
--- a/backend/PrintCminor.ml
+++ b/backend/PrintCminor.ml
@@ -193,9 +193,7 @@ let print_sig p sg =
   List.iter
     (fun t -> fprintf p "%s ->@ " (name_of_type t))
     sg.sig_args;
-  match sg.sig_res with
-  | None -> fprintf p "void"
-  | Some ty -> fprintf p "%s" (name_of_type ty)
+  fprintf p "%s" (name_of_rettype sg.sig_res)
 
 let rec just_skips s =
   match s with
diff --git a/backend/RTLgen.v b/backend/RTLgen.v
index 9d7a8506..f7280c9e 100644
--- a/backend/RTLgen.v
+++ b/backend/RTLgen.v
@@ -410,12 +410,11 @@ Fixpoint convert_builtin_args {A: Type} (al: list (builtin_arg expr)) (rl: list
       a1' :: convert_builtin_args al rl1
   end.
 
-Definition convert_builtin_res (map: mapping) (oty: option typ) (r: builtin_res ident) : mon (builtin_res reg) :=
-  match r, oty with
-  | BR id, _ => do r <- find_var map id; ret (BR r)
-  | BR_none, None => ret BR_none
-  | BR_none, Some _ => do r <- new_reg; ret (BR r)
-  | _, _ => error (Errors.msg "RTLgen: bad builtin_res")
+Definition convert_builtin_res (map: mapping) (ty: rettype) (r: builtin_res ident) : mon (builtin_res reg) :=
+  match r with
+  | BR id => do r <- find_var map id; ret (BR r)
+  | BR_none => if rettype_eq ty Tvoid then ret BR_none else (do r <- new_reg; ret (BR r))
+  | _ => error (Errors.msg "RTLgen: bad builtin_res")
   end.
 
 (** Translation of an expression.  [transl_expr map a rd nd]
@@ -667,10 +666,7 @@ Fixpoint reserve_labels (s: stmt) (ms: labelmap * state)
 (** Translation of a CminorSel function. *)
 
 Definition ret_reg (sig: signature) (rd: reg) : option reg :=
-  match sig.(sig_res) with
-  | None => None
-  | Some ty => Some rd
-  end.
+  if rettype_eq sig.(sig_res) Tvoid then None else Some rd.
 
 Definition transl_fun (f: CminorSel.function) (ngoto: labelmap): mon (node * list reg) :=
   do (rparams, map1) <- add_vars init_mapping f.(CminorSel.fn_params);
diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v
index 17022a7d..72693f63 100644
--- a/backend/RTLgenspec.v
+++ b/backend/RTLgenspec.v
@@ -639,8 +639,8 @@ Lemma new_reg_return_ok:
   map_valid map s1 ->
   return_reg_ok s2 map (ret_reg sig r).
 Proof.
-  intros. unfold ret_reg. destruct (sig_res sig); constructor.
-  eauto with rtlg. eauto with rtlg.
+  intros. unfold ret_reg.
+  destruct (rettype_eq (sig_res sig) Tvoid); constructor; eauto with rtlg.
 Qed.
 
 (** * Relational specification of the translation *)
@@ -1224,9 +1224,9 @@ Lemma convert_builtin_res_charact:
 Proof.
   destruct res; simpl; intros.
 - monadInv TR. constructor.  unfold find_var in EQ. destruct (map_vars map)!x; inv EQ; auto.
-- destruct oty; monadInv TR.
-+ constructor. eauto with rtlg.
+- destruct (rettype_eq oty Tvoid); monadInv TR.
 + constructor.
++ constructor. eauto with rtlg.
 - monadInv TR.
 Qed.
 
@@ -1350,7 +1350,7 @@ Proof.
   intros [C D].
   eapply tr_function_intro; eauto with rtlg.
   eapply transl_stmt_charact; eauto with rtlg.
-  unfold ret_reg. destruct (sig_res (CminorSel.fn_sig f)).
-  constructor. eauto with rtlg. eauto with rtlg.
+  unfold ret_reg. destruct (rettype_eq (sig_res (CminorSel.fn_sig f)) Tvoid).
   constructor.
+  constructor; eauto with rtlg.
 Qed.
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v
index 8336d1bf..5b8646ea 100644
--- a/backend/RTLtyping.v
+++ b/backend/RTLtyping.v
@@ -151,11 +151,12 @@ Inductive wt_instr : instruction -> Prop :=
       list_length_z tbl * 4 <= Int.max_unsigned ->
       wt_instr (Ijumptable arg tbl)
   | wt_Ireturn_none:
-      funct.(fn_sig).(sig_res) = None ->
+      funct.(fn_sig).(sig_res) = Tvoid ->
       wt_instr (Ireturn None)
   | wt_Ireturn_some:
       forall arg ty,
-      funct.(fn_sig).(sig_res) = Some ty ->
+      funct.(fn_sig).(sig_res) <> Tvoid ->
+      env arg = proj_sig_res funct.(fn_sig) ->
       env arg = ty ->
       wt_instr (Ireturn (Some arg)).
 
@@ -298,7 +299,7 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv :=
   | Itailcall sig ros args =>
       do e1 <- type_ros e ros;
       do e2 <- S.set_list e1 args sig.(sig_args);
-      if opt_typ_eq sig.(sig_res) f.(fn_sig).(sig_res) then
+      if rettype_eq sig.(sig_res) f.(fn_sig).(sig_res) then
         if tailcall_is_possible sig
         then OK e2
         else Error(msg "tailcall not possible")
@@ -323,9 +324,9 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv :=
       then OK e1
       else Error(msg "jumptable too big")
   | Ireturn optres =>
-      match optres, f.(fn_sig).(sig_res) with
-      | None, None => OK e
-      | Some r, Some t => S.set e r t
+      match optres, rettype_eq f.(fn_sig).(sig_res) Tvoid with
+      | None, left _ => OK e
+      | Some r, right _ => S.set e r (proj_sig_res f.(fn_sig))
       | _, _ => Error(msg "bad return")
       end
   end.
@@ -468,7 +469,7 @@ Proof.
   destruct l; try discriminate. destruct l; monadInv EQ0. eauto with ty.
   destruct (type_of_operation o) as [targs tres] eqn:TYOP. monadInv EQ0. eauto with ty.
 - (* tailcall *)
-  destruct (opt_typ_eq (sig_res s) (sig_res (fn_sig f))); try discriminate.
+  destruct (rettype_eq (sig_res s) (sig_res (fn_sig f))); try discriminate.
   destruct (tailcall_is_possible s) eqn:TCIP; inv EQ2.
   eauto with ty.
 - (* builtin *)
@@ -477,7 +478,8 @@ Proof.
   destruct (zle (list_length_z l * 4) Int.max_unsigned); inv EQ2.
   eauto with ty.
 - (* return *)
-  simpl in H. destruct o as [r|] eqn: RET; destruct (sig_res (fn_sig f)) as [t|] eqn: RES; try discriminate.
+  simpl in H.
+  destruct o as [r|] eqn: RET; destruct (rettype_eq (sig_res (fn_sig f)) Tvoid); try discriminate.
   eauto with ty.
   inv H; auto with ty.
 Qed.
@@ -519,7 +521,7 @@ Proof.
   eapply S.set_sound; eauto with ty.
   eauto with ty.
 - (* tailcall *)
-  destruct (opt_typ_eq (sig_res s) (sig_res (fn_sig f))); try discriminate.
+  destruct (rettype_eq (sig_res s) (sig_res (fn_sig f))); try discriminate.
   destruct (tailcall_is_possible s) eqn:TCIP; inv EQ2.
   constructor.
   eapply type_ros_sound; eauto with ty.
@@ -543,8 +545,9 @@ Proof.
   eapply check_successors_sound; eauto.
   auto.
 - (* return *)
-  simpl in H. destruct o as [r|] eqn: RET; destruct (sig_res (fn_sig f)) as [t|] eqn: RES; try discriminate.
-  econstructor. eauto. eapply S.set_sound; eauto with ty.
+  simpl in H.
+  destruct o as [r|] eqn: RET; destruct (rettype_eq (sig_res (fn_sig f)) Tvoid); try discriminate.
+  econstructor. auto. eapply S.set_sound; eauto with ty. eauto.
   inv H. constructor. auto.
 Qed.
 
@@ -721,9 +724,9 @@ Proof.
   rewrite check_successor_complete by auto; simpl.
   apply IHtbl0; intros; auto.
 - (* return none *)
-  rewrite H0. exists e; auto.
+  rewrite H0, dec_eq_true. exists e; auto.
 - (* return some *)
-  rewrite H0. apply S.set_complete; auto.
+  rewrite dec_eq_false by auto. apply S.set_complete; auto.
 Qed.
 
 Lemma type_code_complete:
@@ -872,7 +875,7 @@ Qed.
 
 Inductive wt_stackframes: list stackframe -> signature -> Prop :=
   | wt_stackframes_nil: forall sg,
-      sg.(sig_res) = Some Tint ->
+      sg.(sig_res) = Tint ->
       wt_stackframes nil sg
   | wt_stackframes_cons:
       forall s res f sp pc rs env sg,
@@ -964,13 +967,13 @@ Proof.
   econstructor; eauto.
   (* Ireturn *)
   econstructor; eauto.
-  inv WTI; simpl. auto. unfold proj_sig_res; rewrite H2. auto.
+  inv WTI; simpl. auto. rewrite <- H3. auto.
   (* internal function *)
   simpl in *. inv H5.
   econstructor; eauto.
   inv H1. apply wt_init_regs; auto. rewrite wt_params0. auto.
   (* external function *)
-  econstructor; eauto. simpl.
+  econstructor; eauto.
   eapply external_call_well_typed; eauto.
   (* return *)
   inv H1. econstructor; eauto.
diff --git a/backend/SplitLong.vp b/backend/SplitLong.vp
index de954482..694bb0e2 100644
--- a/backend/SplitLong.vp
+++ b/backend/SplitLong.vp
@@ -43,13 +43,13 @@ Class helper_functions := mk_helper_functions {
   i64_smulh: ident;                     (**r signed multiply high *)
 }.
 
-Definition sig_l_l := mksignature (Tlong :: nil) (Some Tlong) cc_default.
-Definition sig_l_f := mksignature (Tlong :: nil) (Some Tfloat) cc_default.
-Definition sig_l_s := mksignature (Tlong :: nil) (Some Tsingle) cc_default.
-Definition sig_f_l := mksignature (Tfloat :: nil) (Some Tlong) cc_default.
-Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) (Some Tlong) cc_default.
-Definition sig_li_l := mksignature (Tlong :: Tint :: nil) (Some Tlong) cc_default.
-Definition sig_ii_l := mksignature (Tint :: Tint :: nil) (Some Tlong) cc_default.
+Definition sig_l_l := mksignature (Tlong :: nil) Tlong cc_default.
+Definition sig_l_f := mksignature (Tlong :: nil) Tfloat cc_default.
+Definition sig_l_s := mksignature (Tlong :: nil) Tsingle cc_default.
+Definition sig_f_l := mksignature (Tfloat :: nil) Tlong cc_default.
+Definition sig_ll_l := mksignature (Tlong :: Tlong :: nil) Tlong cc_default.
+Definition sig_li_l := mksignature (Tlong :: Tint :: nil) Tlong cc_default.
+Definition sig_ii_l := mksignature (Tint :: Tint :: nil) Tlong cc_default.
 
 Section SELECT.
 
diff --git a/backend/Tailcall.v b/backend/Tailcall.v
index 939abeea..b7a62d74 100644
--- a/backend/Tailcall.v
+++ b/backend/Tailcall.v
@@ -82,7 +82,7 @@ Definition transf_instr (f: function) (pc: node) (instr: instruction) :=
   | Icall sig ros args res s =>
       if is_return niter f s res
       && tailcall_is_possible sig
-      && opt_typ_eq sig.(sig_res) f.(fn_sig).(sig_res)
+      && rettype_eq sig.(sig_res) f.(fn_sig).(sig_res)
       then Itailcall sig ros args
       else instr
   | _ => instr
diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v
index 06e314f3..9ec89553 100644
--- a/backend/Tailcallproof.v
+++ b/backend/Tailcallproof.v
@@ -157,12 +157,10 @@ Lemma transf_instr_charact:
   transf_instr_spec f instr (transf_instr f pc instr).
 Proof.
   intros. unfold transf_instr. destruct instr; try constructor.
-  caseEq (is_return niter f n r && tailcall_is_possible s &&
-          opt_typ_eq (sig_res s) (sig_res (fn_sig f))); intros.
-  destruct (andb_prop _ _ H0). destruct (andb_prop _ _ H1).
-  eapply transf_instr_tailcall; eauto.
-  eapply is_return_charact; eauto.
-  constructor.
+  destruct (is_return niter f n r && tailcall_is_possible s &&
+            rettype_eq (sig_res s) (sig_res (fn_sig f))) eqn:B.
+- InvBooleans. eapply transf_instr_tailcall; eauto. eapply is_return_charact; eauto.
+- constructor.
 Qed.
 
 Lemma transf_instr_lookup: