From be0b1872bf2ad36df9b0c7a0ffa63b9e77fa769b Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Tue, 18 Feb 2020 16:57:17 +0100 Subject: 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. --- backend/Cminortyping.v | 45 ++++++++++++++++++++++++--------------------- 1 file changed, 24 insertions(+), 21 deletions(-) (limited to 'backend/Cminortyping.v') 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. -- cgit