Commit be0b1872 authored by Xavier Leroy's avatar Xavier Leroy Committed by Xavier Leroy
Browse files

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.
parent a9eaf489
......@@ -29,5 +29,5 @@ Definition platform_builtin_table : list (string * platform_builtin) :=
Definition platform_builtin_sig (b: platform_builtin) : signature :=
match b with end.
Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) :=
Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) :=
match b with end.
......@@ -102,10 +102,9 @@ Definition is_float_reg (r: mreg): bool :=
with one integer result. *)
Definition loc_result (s: signature) : rpair mreg :=
match s.(sig_res) with
| None => One R0
| Some (Tint | Tlong | Tany32 | Tany64) => One R0
| Some (Tfloat | Tsingle) => One F0
match proj_sig_res s with
| Tint | Tlong | Tany32 | Tany64 => One R0
| Tfloat | Tsingle => One F0
end.
(** The result registers have types compatible with that given in the signature. *)
......@@ -114,7 +113,7 @@ Lemma loc_result_type:
forall sig,
subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true.
Proof.
intros. unfold proj_sig_res, loc_result. destruct (sig_res sig) as [[]|]; auto.
intros. unfold loc_result. destruct (proj_sig_res sig); auto.
Qed.
(** The result locations are caller-save registers *)
......@@ -124,7 +123,7 @@ Lemma loc_result_caller_save:
forall_rpair (fun r => is_callee_save r = false) (loc_result s).
Proof.
intros.
unfold loc_result. destruct (sig_res s) as [[]|]; simpl; auto.
unfold loc_result. destruct (proj_sig_res s); simpl; auto.
Qed.
(** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *)
......@@ -134,12 +133,12 @@ Lemma loc_result_pair:
match loc_result sg with
| One _ => True
| Twolong r1 r2 =>
r1 <> r2 /\ sg.(sig_res) = Some Tlong
r1 <> r2 /\ proj_sig_res sg = Tlong
/\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true
/\ Archi.ptr64 = false
end.
Proof.
intros; unfold loc_result; destruct (sig_res sg) as [[]|]; exact I.
intros; unfold loc_result; destruct (proj_sig_res sg); exact I.
Qed.
(** The location of the result depends only on the result part of the signature *)
......@@ -147,7 +146,7 @@ Qed.
Lemma loc_result_exten:
forall s1 s2, s1.(sig_res) = s2.(sig_res) -> loc_result s1 = loc_result s2.
Proof.
intros. unfold loc_result. rewrite H; auto.
intros. unfold loc_result, proj_sig_res. rewrite H; auto.
Qed.
(** ** Location of function arguments *)
......
......@@ -29,5 +29,5 @@ Definition platform_builtin_table : list (string * platform_builtin) :=
Definition platform_builtin_sig (b: platform_builtin) : signature :=
match b with end.
Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (proj_sig_res (platform_builtin_sig b)) :=
Definition platform_builtin_sem (b: platform_builtin) : builtin_sem (sig_res (platform_builtin_sig b)) :=
match b with end.
......@@ -104,13 +104,12 @@ Definition is_float_reg (r: mreg): bool :=
representation with a single LDM instruction. *)
Definition loc_result (s: signature) : rpair mreg :=
match s.(sig_res) with
| None => One R0
| Some (Tint | Tany32) => One R0
| Some (Tfloat | Tsingle | Tany64) => One F0
| Some Tlong => if Archi.big_endian
then Twolong R0 R1
else Twolong R1 R0
match proj_sig_res s with
| Tint | Tany32 => One R0
| Tfloat | Tsingle | Tany64 => One F0
| Tlong => if Archi.big_endian
then Twolong R0 R1
else Twolong R1 R0
end.
(** The result registers have types compatible with that given in the signature. *)
......@@ -119,7 +118,7 @@ Lemma loc_result_type:
forall sig,
subtype (proj_sig_res sig) (typ_rpair mreg_type (loc_result sig)) = true.
Proof.
intros. unfold proj_sig_res, loc_result. destruct (sig_res sig) as [[]|]; destruct Archi.big_endian; auto.
intros. unfold loc_result. destruct (proj_sig_res sig); destruct Archi.big_endian; auto.
Qed.
(** The result locations are caller-save registers *)
......@@ -129,7 +128,7 @@ Lemma loc_result_caller_save:
forall_rpair (fun r => is_callee_save r = false) (loc_result s).
Proof.
intros.
unfold loc_result. destruct (sig_res s) as [[]|]; destruct Archi.big_endian; simpl; auto.
unfold loc_result. destruct (proj_sig_res s); destruct Archi.big_endian; simpl; auto.
Qed.
(** If the result is in a pair of registers, those registers are distinct and have type [Tint] at least. *)
......@@ -139,14 +138,13 @@ Lemma loc_result_pair:
match loc_result sg with
| One _ => True
| Twolong r1 r2 =>
r1 <> r2 /\ sg.(sig_res) = Some Tlong
r1 <> r2 /\ proj_sig_res sg = Tlong
/\ subtype Tint (mreg_type r1) = true /\ subtype Tint (mreg_type r2) = true
/\ Archi.ptr64 = false
end.
Proof.
intros; unfold loc_result; destruct (sig_res sg) as [[]|]; destruct Archi.big_endian; auto.
intuition congruence.
intuition congruence.
intros; unfold loc_result; destruct (proj_sig_res sg); auto.
destruct Archi.big_endian; intuition congruence.
Qed.
(** The location of the result depends only on the result part of the signature *)
......@@ -154,7 +152,7 @@ Qed.
Lemma loc_result_exten:
forall s1 s2, s1.(sig_res) = s2.(sig_res) -> loc_result s1 = loc_result s2.
Proof.
intros. unfold loc_result. rewrite H; auto.
intros. unfold loc_result, proj_sig_res. rewrite H; auto.
Qed.
(** ** Location of function arguments *)
......
......@@ -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.
......
......@@ -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).
......
......@@ -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)
......
......@@ -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 *)
......
......@@ -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.
......
......@@ -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
......
......@@ -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
......
......@@ -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);
......
......@@ -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.
......@@ -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,