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.

1 files changed, 24 insertions, 21 deletions

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.