diff options
Diffstat (limited to 'backend/RTLtyping.v')
| -rw-r--r-- | backend/RTLtyping.v | 428 |
1 files changed, 252 insertions, 176 deletions
diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index e8ae7ae..24f8d7b 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -14,7 +14,7 @@ Require Import Coqlib. Require Import Errors. -Require Import Unityping. +Require Import Subtyping. Require Import Maps. Require Import AST. Require Import Op. @@ -36,8 +36,7 @@ Require Import Conventions. is very simple, consisting of the four types [Tint] (for integers and pointers), [Tfloat] (for double-precision floats), [Tlong] (for 64-bit integers) and [Tsingle] (for single-precision floats). - At the RTL level, we simplify things further by equating [Tsingle] - with [Tfloat]. + The only subtlety is that [Tsingle] is a subtype of [Tfloat]. Additionally, we impose that each pseudo-register has the same type throughout the function. This requirement helps with register allocation, @@ -57,11 +56,6 @@ Require Import Conventions. which can work over both integers and floats. *) -Definition normalize (ty: typ) : typ := - match ty with Tsingle => Tfloat | _ => ty end. - -Definition normalize_list (tyl: list typ) : list typ := map normalize tyl. - Definition regenv := reg -> typ. Section WT_INSTR. @@ -79,57 +73,57 @@ Inductive wt_instr : instruction -> Prop := wt_instr (Inop s) | wt_Iopmove: forall r1 r s, - env r = env r1 -> + subtype (env r1) (env r) = true -> valid_successor s -> wt_instr (Iop Omove (r1 :: nil) r s) | wt_Iop: forall op args res s, op <> Omove -> - map env args = fst (type_of_operation op) -> - env res = normalize (snd (type_of_operation op)) -> + subtype_list (map env args) (fst (type_of_operation op)) = true -> + subtype (snd (type_of_operation op)) (env res) = true -> valid_successor s -> wt_instr (Iop op args res s) | wt_Iload: forall chunk addr args dst s, - map env args = type_of_addressing addr -> - env dst = normalize (type_of_chunk chunk) -> + subtype_list (map env args) (type_of_addressing addr) = true -> + subtype (type_of_chunk chunk) (env dst) = true -> valid_successor s -> wt_instr (Iload chunk addr args dst s) | wt_Istore: forall chunk addr args src s, - map env args = type_of_addressing addr -> - env src = type_of_chunk_use chunk -> + subtype_list (map env args) (type_of_addressing addr) = true -> + subtype (env src) (type_of_chunk_use chunk) = true -> valid_successor s -> wt_instr (Istore chunk addr args src s) | wt_Icall: forall sig ros args res s, - match ros with inl r => env r = Tint | inr s => True end -> - map env args = normalize_list sig.(sig_args) -> - env res = normalize (proj_sig_res sig) -> + match ros with inl r => subtype (env r) Tint = true | inr s => True end -> + subtype_list (map env args) sig.(sig_args) = true -> + subtype (proj_sig_res sig) (env res) = true -> valid_successor s -> wt_instr (Icall sig ros args res s) | wt_Itailcall: forall sig ros args, - match ros with inl r => env r = Tint | inr s => True end -> - map env args = normalize_list sig.(sig_args) -> + match ros with inl r => subtype (env r) Tint = true | inr s => True end -> sig.(sig_res) = funct.(fn_sig).(sig_res) -> + subtype_list (map env args) sig.(sig_args) = true -> tailcall_possible sig -> wt_instr (Itailcall sig ros args) | wt_Ibuiltin: forall ef args res s, - map env args = normalize_list (ef_sig ef).(sig_args) -> - env res = normalize (proj_sig_res (ef_sig ef)) -> + subtype_list (map env args) (ef_sig ef).(sig_args) = true -> + subtype (proj_sig_res (ef_sig ef)) (env res) = true -> valid_successor s -> wt_instr (Ibuiltin ef args res s) | wt_Icond: forall cond args s1 s2, - map env args = type_of_condition cond -> + subtype_list (map env args) (type_of_condition cond) = true -> valid_successor s1 -> valid_successor s2 -> wt_instr (Icond cond args s1 s2) | wt_Ijumptable: forall arg tbl, - env arg = Tint -> + subtype (env arg) Tint = true -> (forall s, In s tbl -> valid_successor s) -> list_length_z tbl * 4 <= Int.max_unsigned -> wt_instr (Ijumptable arg tbl) @@ -139,7 +133,7 @@ Inductive wt_instr : instruction -> Prop := | wt_Ireturn_some: forall arg ty, funct.(fn_sig).(sig_res) = Some ty -> - env arg = normalize ty -> + subtype (env arg) ty = true -> wt_instr (Ireturn (Some arg)). End WT_INSTR. @@ -152,7 +146,7 @@ End WT_INSTR. Record wt_function (f: function) (env: regenv): Prop := mk_wt_function { wt_params: - map env f.(fn_params) = normalize_list f.(fn_sig).(sig_args); + subtype_list f.(fn_sig).(sig_args) (map env f.(fn_params)) = true; wt_norepet: list_norepet f.(fn_params); wt_instrs: @@ -174,8 +168,8 @@ Definition wt_program (p: program): Prop := (** * Type inference *) -(** Type inference reuses the generic solver for unification constraints - defined in module [Unityping]. *) +(** Type inference reuses the generic solver for subtyping constraints + defined in module [Subtyping]. *) Module RTLtypes <: TYPE_ALGEBRA. @@ -183,9 +177,122 @@ Definition t := typ. Definition eq := typ_eq. Definition default := Tint. +Definition sub (t1 t2: typ): Prop := subtype t1 t2 = true. + +Lemma sub_refl: forall ty, sub ty ty. +Proof. unfold sub; destruct ty; auto. Qed. + +Lemma sub_trans: forall ty1 ty2 ty3, sub ty1 ty2 -> sub ty2 ty3 -> sub ty1 ty3. +Proof. + unfold sub; intros. destruct ty1; destruct ty2; try discriminate; destruct ty3; auto; discriminate. +Qed. + +Definition sub_dec: forall ty1 ty2, {sub ty1 ty2} + {~sub ty1 ty2}. +Proof. + unfold sub; intros. destruct (subtype ty1 ty2). left; auto. right; congruence. +Defined. + +Definition lub (ty1 ty2: typ) := + match ty1, ty2 with + | Tint, Tint => Tint + | Tlong, Tlong => Tlong + | Tfloat, Tfloat => Tfloat + | Tsingle, Tsingle => Tsingle + | Tfloat, Tsingle => Tfloat + | Tsingle, Tfloat => Tfloat + | _, _ => default + end. + +Lemma lub_left: forall x y z, sub x z -> sub y z -> sub x (lub x y). +Proof. + unfold sub, lub; intros. destruct x; destruct y; auto; destruct z; discriminate. +Qed. + +Lemma lub_right: forall x y z, sub x z -> sub y z -> sub y (lub x y). +Proof. + unfold sub, lub; intros. destruct x; destruct y; auto; destruct z; discriminate. +Qed. + +Lemma lub_min: forall x y z, sub x z -> sub y z -> sub (lub x y) z. +Proof. + unfold sub, lub; intros. destruct x; destruct z; try discriminate; destruct y; auto; discriminate. +Qed. + +Definition glb (ty1 ty2: typ) := + match ty1, ty2 with + | Tint, Tint => Tint + | Tlong, Tlong => Tlong + | Tfloat, Tfloat => Tfloat + | Tsingle, Tsingle => Tsingle + | Tfloat, Tsingle => Tsingle + | Tsingle, Tfloat => Tsingle + | _, _ => default + end. + +Lemma glb_left: forall x y z, sub z x -> sub z y -> sub (glb x y) x. +Proof. + unfold sub, glb; intros. destruct x; destruct y; auto; destruct z; discriminate. +Qed. + +Lemma glb_right: forall x y z, sub z x -> sub z y -> sub (glb x y) y. +Proof. + unfold sub, glb; intros. destruct x; destruct y; auto; destruct z; discriminate. +Qed. + +Lemma glb_max: forall x y z, sub z x -> sub z y -> sub z (glb x y). +Proof. + unfold sub, glb; intros. destruct x; destruct z; try discriminate; destruct y; auto; discriminate. +Qed. + +Definition low_bound (ty: typ) := + match ty with Tfloat => Tsingle | _ => ty end. + +Definition high_bound (ty: typ) := + match ty with Tsingle => Tfloat | _ => ty end. + +Lemma low_bound_sub: forall t, sub (low_bound t) t. +Proof. + unfold sub; destruct t0; auto. +Qed. + +Lemma low_bound_minorant: forall x y, sub x y -> sub (low_bound y) x. +Proof. + unfold sub; intros. destruct x; destruct y; auto; discriminate. +Qed. + +Lemma high_bound_sub: forall t, sub t (high_bound t). +Proof. + unfold sub; destruct t0; auto. +Qed. + +Lemma high_bound_majorant: forall x y, sub x y -> sub y (high_bound x). +Proof. + unfold sub; intros. destruct x; destruct y; auto; discriminate. +Qed. + +Definition weight (t: typ) := + match t with Tfloat => 1%nat | _ => 0%nat end. + +Definition max_weight := 1%nat. + +Lemma weight_range: forall t, (weight t <= max_weight)%nat. +Proof. + unfold max_weight; destruct t0; simpl; omega. +Qed. + +Lemma weight_sub: forall x y, sub x y -> (weight x <= weight y)%nat. +Proof. + unfold sub; intros. destruct x; destruct y; simpl; discriminate || omega. +Qed. + +Lemma weight_sub_strict: forall x y, sub x y -> x <> y -> (weight x < weight y)%nat. +Proof. + unfold sub, subtype; intros. destruct x; destruct y; simpl; congruence || omega. +Qed. + End RTLtypes. -Module S := UniSolver(RTLtypes). +Module S := SubSolver(RTLtypes). Section INFERENCE. @@ -211,7 +318,7 @@ Fixpoint check_successors (sl: list node): res unit := Definition type_ros (e: S.typenv) (ros: reg + ident) : res S.typenv := match ros with - | inl r => S.set e r Tint + | inl r => S.type_use e r Tint | inr s => OK e end. @@ -226,28 +333,28 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv := do x <- check_successor s; if is_move op then match args with - | arg :: nil => do (changed, e') <- S.move e res arg; OK e' + | arg :: nil => do (changed, e') <- S.type_move e arg res; OK e' | _ => Error (msg "ill-formed move") end else (let (targs, tres) := type_of_operation op in - do e1 <- S.set_list e args targs; S.set e1 res (normalize tres)) + do e1 <- S.type_uses e args targs; S.type_def e1 res tres) | Iload chunk addr args dst s => do x <- check_successor s; - do e1 <- S.set_list e args (type_of_addressing addr); - S.set e1 dst (normalize (type_of_chunk chunk)) + do e1 <- S.type_uses e args (type_of_addressing addr); + S.type_def e1 dst (type_of_chunk chunk) | Istore chunk addr args src s => do x <- check_successor s; - do e1 <- S.set_list e args (type_of_addressing addr); - S.set e1 src (type_of_chunk_use chunk) + do e1 <- S.type_uses e args (type_of_addressing addr); + S.type_use e1 src (type_of_chunk_use chunk) | Icall sig ros args res s => do x <- check_successor s; do e1 <- type_ros e ros; - do e2 <- S.set_list e1 args (normalize_list sig.(sig_args)); - S.set e2 res (normalize (proj_sig_res sig)) + do e2 <- S.type_uses e1 args sig.(sig_args); + S.type_def e2 res (proj_sig_res sig) | Itailcall sig ros args => do e1 <- type_ros e ros; - do e2 <- S.set_list e1 args (normalize_list sig.(sig_args)); + do e2 <- S.type_uses e1 args sig.(sig_args); if opt_typ_eq sig.(sig_res) f.(fn_sig).(sig_res) then if tailcall_is_possible sig then OK e2 @@ -256,48 +363,45 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv := | Ibuiltin ef args res s => let sig := ef_sig ef in do x <- check_successor s; - do e1 <- S.set_list e args (normalize_list sig.(sig_args)); - S.set e1 res (normalize (proj_sig_res sig)) - | Icond cond args s1 s2 => + do e1 <- S.type_uses e args sig.(sig_args); + S.type_def e1 res (proj_sig_res sig) + | Icond cond args s1 s2 => do x1 <- check_successor s1; do x2 <- check_successor s2; - S.set_list e args (type_of_condition cond) - | Ijumptable arg tbl => + S.type_uses e args (type_of_condition cond) + | Ijumptable arg tbl => do x <- check_successors tbl; - do e1 <- S.set e arg Tint; - if zle (list_length_z tbl * 4) Int.max_unsigned - then OK e1 - else Error(msg "jumptable too big") + do e1 <- S.type_use e arg Tint; + if zle (list_length_z tbl * 4) Int.max_unsigned 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 (normalize t) + | Some r, Some t => S.type_use e r t | _, _ => Error(msg "bad return") end end. Definition type_code (e: S.typenv): res S.typenv := - PTree.fold (fun re pc i => - match re with - | Error _ => re - | OK e => - match type_instr e i with - | Error msg => Error(MSG "At PC " :: POS pc :: MSG ": " :: msg) - | OK e' => OK e' - end - end) - f.(fn_code) (OK e). + PTree.fold + (fun re pc i => + match re with + | Error _ => re + | OK e => + match type_instr e i with + | Error msg => Error(MSG "At PC " :: POS pc :: MSG ": " :: msg) + | OK e' => OK e' + end + end) + f.(fn_code) (OK e). (** Solve remaining constraints *) -Definition check_params_norepet (params: list reg): res unit := - if list_norepet_dec Reg.eq params - then OK tt - else Error(msg "duplicate parameters"). +Definition check_params_norepet (params: list reg): res unit := + if list_norepet_dec Reg.eq params then OK tt else Error(msg "duplicate parameters"). Definition type_function : res regenv := do e1 <- type_code S.initial; - do e2 <- S.set_list e1 f.(fn_params) (normalize_list f.(fn_sig).(sig_args)); + do e2 <- S.type_defs e1 f.(fn_params) f.(fn_sig).(sig_args); do te <- S.solve e2; do x1 <- check_params_norepet f.(fn_params); do x2 <- check_successor f.(fn_entrypoint); @@ -315,10 +419,10 @@ Hint Resolve type_ros_incr: ty. Lemma type_ros_sound: forall e ros e' te, type_ros e ros = OK e' -> S.satisf te e' -> - match ros with inl r => te r = Tint | inr s => True end. + match ros with inl r => subtype (te r) Tint = true | inr s => True end. Proof. unfold type_ros; intros. destruct ros. - eapply S.set_sound; eauto. + eapply S.type_use_sound; eauto. auto. Qed. @@ -339,6 +443,17 @@ Proof. monadInv H. destruct H0. subst a; eauto with ty. eauto. Qed. +Remark subtype_list_charact: + forall tyl1 tyl2, + subtype_list tyl1 tyl2 = true <-> list_forall2 RTLtypes.sub tyl1 tyl2. +Proof. + unfold RTLtypes.sub; intros; split; intros. + revert tyl1 tyl2 H. induction tyl1; destruct tyl2; simpl; intros; try discriminate. + constructor. + InvBooleans. constructor; auto. + revert tyl1 tyl2 H. induction 1; simpl. auto. rewrite H; rewrite IHlist_forall2; auto. +Qed. + Lemma type_instr_incr: forall e i e' te, type_instr e i = OK e' -> S.satisf te e' -> S.satisf te e. @@ -374,56 +489,56 @@ Proof. + assert (o = Omove) by (unfold is_move in ISMOVE; destruct o; congruence). subst o. destruct l; try discriminate. destruct l; monadInv EQ0. - constructor. eapply S.move_sound; eauto. eauto with ty. + constructor. eapply S.type_move_sound; eauto. eauto with ty. + destruct (type_of_operation o) as [targs tres] eqn:TYOP. monadInv EQ0. apply wt_Iop. unfold is_move in ISMOVE; destruct o; congruence. - rewrite TYOP. eapply S.set_list_sound; eauto with ty. - rewrite TYOP. eapply S.set_sound; eauto with ty. + rewrite TYOP. rewrite subtype_list_charact. eapply S.type_uses_sound; eauto with ty. + rewrite TYOP. eapply S.type_def_sound; eauto with ty. eauto with ty. - (* load *) constructor. - eapply S.set_list_sound; eauto with ty. - eapply S.set_sound; eauto with ty. + rewrite subtype_list_charact. eapply S.type_uses_sound; eauto with ty. + eapply S.type_def_sound; eauto with ty. eauto with ty. - (* store *) constructor. - eapply S.set_list_sound; eauto with ty. - eapply S.set_sound; eauto with ty. + rewrite subtype_list_charact. eapply S.type_uses_sound; eauto with ty. + eapply S.type_use_sound; eauto with ty. eauto with ty. - (* call *) constructor. eapply type_ros_sound; eauto with ty. - eapply S.set_list_sound; eauto with ty. - eapply S.set_sound; eauto with ty. + rewrite subtype_list_charact. eapply S.type_uses_sound; eauto with ty. + eapply S.type_def_sound; eauto with ty. eauto with ty. - (* tailcall *) destruct (opt_typ_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. - eapply S.set_list_sound; eauto with ty. auto. + rewrite subtype_list_charact. eapply S.type_uses_sound; eauto with ty. apply tailcall_is_possible_correct; auto. - (* builtin *) constructor. - eapply S.set_list_sound; eauto with ty. - eapply S.set_sound; eauto with ty. + rewrite subtype_list_charact. eapply S.type_uses_sound; eauto with ty. + eapply S.type_def_sound; eauto with ty. eauto with ty. - (* cond *) constructor. - eapply S.set_list_sound; eauto with ty. + rewrite subtype_list_charact. eapply S.type_uses_sound; eauto with ty. eauto with ty. eauto with ty. - (* jumptable *) destruct (zle (list_length_z l * 4) Int.max_unsigned); inv EQ2. constructor. - eapply S.set_sound; eauto. + eapply S.type_use_sound; eauto. 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. + econstructor. eauto. eapply S.type_use_sound; eauto with ty. inv H. constructor. auto. Qed. @@ -460,7 +575,7 @@ Proof. assert (SAT1: S.satisf env x) by (eauto with ty). constructor. - (* type of parameters *) - eapply S.set_list_sound; eauto. + rewrite subtype_list_charact. eapply S.type_defs_sound; eauto. - (* parameters are unique *) unfold check_params_norepet in EQ2. destruct (list_norepet_dec Reg.eq (fn_params f)); inv EQ2; auto. @@ -475,11 +590,11 @@ Qed. Lemma type_ros_complete: forall te ros e, S.satisf te e -> - match ros with inl r => te r = Tint | inr s => True end -> + match ros with inl r => subtype (te r) Tint = true | inr s => True end -> exists e', type_ros e ros = OK e' /\ S.satisf te e'. Proof. intros; destruct ros; simpl. - eapply S.set_complete; eauto. + eapply S.type_use_complete; eauto. exists e; auto. Qed. @@ -500,60 +615,67 @@ Proof. - (* nop *) econstructor; split. rewrite check_successor_complete; simpl; eauto. auto. - (* move *) - exploit S.move_complete; eauto. intros (changed & e' & A & B). + exploit S.type_move_complete; eauto. intros (changed & e' & A & B). exists e'; split. rewrite check_successor_complete by auto; simpl. rewrite A; auto. auto. - (* other op *) destruct (type_of_operation op) as [targ tres]. simpl in *. - exploit S.set_list_complete. eauto. eauto. intros [e1 [A B]]. - exploit S.set_complete. eexact B. eauto. intros [e2 [C D]]. + rewrite subtype_list_charact in H1. + exploit S.type_uses_complete. eauto. eauto. intros [e1 [A B]]. + exploit S.type_def_complete. eexact B. eauto. intros [e2 [C D]]. exists e2; split; auto. rewrite check_successor_complete by auto; simpl. replace (is_move op) with false. rewrite A; simpl; rewrite C; auto. destruct op; reflexivity || congruence. - (* load *) - exploit S.set_list_complete. eauto. eauto. intros [e1 [A B]]. - exploit S.set_complete. eexact B. eauto. intros [e2 [C D]]. + rewrite subtype_list_charact in H0. + exploit S.type_uses_complete. eauto. eauto. intros [e1 [A B]]. + exploit S.type_def_complete. eexact B. eauto. intros [e2 [C D]]. exists e2; split; auto. rewrite check_successor_complete by auto; simpl. rewrite A; simpl; rewrite C; auto. - (* store *) - exploit S.set_list_complete. eauto. eauto. intros [e1 [A B]]. - exploit S.set_complete. eexact B. eauto. intros [e2 [C D]]. + rewrite subtype_list_charact in H0. + exploit S.type_uses_complete. eauto. eauto. intros [e1 [A B]]. + exploit S.type_use_complete. eexact B. eauto. intros [e2 [C D]]. exists e2; split; auto. rewrite check_successor_complete by auto; simpl. rewrite A; simpl; rewrite C; auto. - (* call *) exploit type_ros_complete. eauto. eauto. intros [e1 [A B]]. - exploit S.set_list_complete. eauto. eauto. intros [e2 [C D]]. - exploit S.set_complete. eexact D. eauto. intros [e3 [E F]]. + rewrite subtype_list_charact in H1. + exploit S.type_uses_complete. eauto. eauto. intros [e2 [C D]]. + exploit S.type_def_complete. eexact D. eauto. intros [e3 [E F]]. exists e3; split; auto. rewrite check_successor_complete by auto; simpl. rewrite A; simpl; rewrite C; simpl; rewrite E; auto. - (* tailcall *) exploit type_ros_complete. eauto. eauto. intros [e1 [A B]]. - exploit S.set_list_complete. eauto. eauto. intros [e2 [C D]]. + rewrite subtype_list_charact in H2. + exploit S.type_uses_complete. eauto. eauto. intros [e2 [C D]]. exists e2; split; auto. rewrite A; simpl; rewrite C; simpl. - rewrite H2; rewrite dec_eq_true. + rewrite H1; rewrite dec_eq_true. replace (tailcall_is_possible sig) with true; auto. revert H3. unfold tailcall_possible, tailcall_is_possible. generalize (loc_arguments sig). induction l; simpl; intros. auto. exploit (H3 a); auto. intros. destruct a; try contradiction. apply IHl. intros; apply H3; auto. - (* builtin *) - exploit S.set_list_complete. eauto. eauto. intros [e1 [A B]]. - exploit S.set_complete. eexact B. eauto. intros [e2 [C D]]. + rewrite subtype_list_charact in H0. + exploit S.type_uses_complete. eauto. eauto. intros [e1 [A B]]. + exploit S.type_def_complete. eexact B. eauto. intros [e2 [C D]]. exists e2; split; auto. rewrite check_successor_complete by auto; simpl. rewrite A; simpl; rewrite C; auto. - (* cond *) - exploit S.set_list_complete. eauto. eauto. intros [e1 [A B]]. + rewrite subtype_list_charact in H0. + exploit S.type_uses_complete. eauto. eauto. intros [e1 [A B]]. exists e1; split; auto. rewrite check_successor_complete by auto; simpl. rewrite check_successor_complete by auto; simpl. auto. - (* jumptbl *) - exploit S.set_complete. eauto. eauto. intros [e1 [A B]]. + exploit S.type_use_complete. eauto. eauto. intros [e1 [A B]]. exists e1; split; auto. replace (check_successors tbl) with (OK tt). simpl. rewrite A; simpl. apply zle_true; auto. @@ -563,7 +685,7 @@ Proof. - (* return none *) rewrite H0. exists e; auto. - (* return some *) - rewrite H0. apply S.set_complete; auto. + rewrite H0. apply S.type_use_complete; auto. Qed. Lemma type_code_complete: @@ -597,7 +719,8 @@ Proof. intros. destruct H. destruct (type_code_complete te S.initial) as (e1 & A & B). auto. apply S.satisf_initial. - destruct (S.set_list_complete te f.(fn_params) (normalize_list f.(fn_sig).(sig_args)) e1) as (e2 & C & D); auto. + destruct (S.type_defs_complete te f.(fn_params) f.(fn_sig).(sig_args) e1) as (e2 & C & D); auto. + rewrite <- subtype_list_charact; auto. destruct (S.solve_complete te e2) as (te' & E); auto. exists te'; unfold type_function. rewrite A; simpl. rewrite C; simpl. rewrite E; simpl. @@ -637,23 +760,6 @@ Proof. apply H. Qed. -Lemma normalize_subtype: - forall ty, subtype ty (normalize ty) = true. -Proof. - intros. destruct ty; reflexivity. -Qed. - -Lemma wt_regset_assign2: - forall env rs v r ty, - wt_regset env rs -> - Val.has_type v ty -> - env r = normalize ty -> - wt_regset env (rs#r <- v). -Proof. - intros. eapply wt_regset_assign; eauto. - rewrite H1. eapply Val.has_subtype; eauto. apply normalize_subtype. -Qed. - Lemma wt_regset_list: forall env rs, wt_regset env rs -> @@ -682,11 +788,11 @@ Lemma wt_exec_Iop: wt_regset env (rs#res <- v). Proof. intros. inv H. - simpl in H0. inv H0. apply wt_regset_assign; auto. - rewrite H4; auto. - eapply wt_regset_assign2; auto. + simpl in H0. inv H0. apply wt_regset_assign; auto. + eapply Val.has_subtype; eauto. + apply wt_regset_assign; auto. + eapply Val.has_subtype; eauto. eapply type_of_operation_sound; eauto. - auto. Qed. Lemma wt_exec_Iload: @@ -697,7 +803,8 @@ Lemma wt_exec_Iload: wt_regset env (rs#dst <- v). Proof. intros. destruct a; simpl in H0; try discriminate. inv H. - eapply wt_regset_assign2; eauto. + apply wt_regset_assign; auto. + eapply Val.has_subtype; eauto. eapply Mem.load_type; eauto. Qed. @@ -709,7 +816,8 @@ Lemma wt_exec_Ibuiltin: wt_regset env (rs#res <- vres). Proof. intros. inv H. - eapply wt_regset_assign2; eauto. + apply wt_regset_assign; auto. + eapply Val.has_subtype; eauto. eapply external_call_well_typed; eauto. Qed. @@ -720,46 +828,36 @@ Proof. intros. inv H. eauto. Qed. -Inductive wt_stackframes: list stackframe -> signature -> Prop := - | wt_stackframes_nil: forall sg, - sg.(sig_res) = Some Tint -> - wt_stackframes nil sg +Inductive wt_stackframes: list stackframe -> option typ -> Prop := + | wt_stackframes_nil: + wt_stackframes nil (Some Tint) | wt_stackframes_cons: - forall s res f sp pc rs env sg, + forall s res f sp pc rs env tyres, wt_function f env -> wt_regset env rs -> - env res = normalize (proj_sig_res sg) -> - wt_stackframes s (fn_sig f) -> - wt_stackframes (Stackframe res f sp pc rs :: s) sg. + subtype (match tyres with None => Tint | Some t => t end) (env res) = true -> + wt_stackframes s (sig_res (fn_sig f)) -> + wt_stackframes (Stackframe res f sp pc rs :: s) tyres. Inductive wt_state: state -> Prop := | wt_state_intro: forall s f sp pc rs m env - (WT_STK: wt_stackframes s (fn_sig f)) + (WT_STK: wt_stackframes s (sig_res (fn_sig f))) (WT_FN: wt_function f env) (WT_RS: wt_regset env rs), wt_state (State s f sp pc rs m) | wt_state_call: forall s f args m, - wt_stackframes s (funsig f) -> + wt_stackframes s (sig_res (funsig f)) -> wt_fundef f -> - Val.has_type_list args (normalize_list (sig_args (funsig f))) -> + Val.has_type_list args (sig_args (funsig f)) -> wt_state (Callstate s f args m) | wt_state_return: - forall s v m sg, - wt_stackframes s sg -> - Val.has_type v (normalize (proj_sig_res sg)) -> + forall s v m tyres, + wt_stackframes s tyres -> + Val.has_type v (match tyres with None => Tint | Some t => t end) -> wt_state (Returnstate s v m). -Remark wt_stackframes_change_sig: - forall s sg1 sg2, - sg1.(sig_res) = sg2.(sig_res) -> wt_stackframes s sg1 -> wt_stackframes s sg2. -Proof. - intros. inv H0. -- constructor; congruence. -- econstructor; eauto. rewrite H3. unfold proj_sig_res. rewrite H. auto. -Qed. - Section SUBJECT_REDUCTION. Variable p: program. @@ -793,7 +891,7 @@ Proof. discriminate. econstructor; eauto. econstructor; eauto. inv WTI; auto. - inv WTI. rewrite <- H8. apply wt_regset_list. auto. + inv WTI. eapply Val.has_subtype_list; eauto. apply wt_regset_list. auto. (* Itailcall *) assert (wt_fundef fd). destruct ros; simpl in H0. @@ -804,8 +902,8 @@ Proof. exact wt_p. exact H0. discriminate. econstructor; eauto. - inv WTI. apply wt_stackframes_change_sig with (fn_sig f); auto. - inv WTI. rewrite <- H7. apply wt_regset_list. auto. + inv WTI. rewrite H7; auto. + inv WTI. eapply Val.has_subtype_list; eauto. apply wt_regset_list. auto. (* Ibuiltin *) econstructor; eauto. eapply wt_exec_Ibuiltin; eauto. (* Icond *) @@ -814,40 +912,18 @@ Proof. econstructor; eauto. (* Ireturn *) econstructor; eauto. - inv WTI; simpl. auto. unfold proj_sig_res; rewrite H2. rewrite <- H3. auto. + inv WTI; simpl. auto. rewrite H2. eapply Val.has_subtype; eauto. (* internal function *) simpl in *. inv H5. econstructor; eauto. - inv H1. apply wt_init_regs; auto. rewrite wt_params0. auto. + inv H1. apply wt_init_regs; auto. eapply Val.has_subtype_list; eauto. (* external function *) econstructor; eauto. simpl. - change (Val.has_type res (normalize (proj_sig_res (ef_sig ef)))). - eapply Val.has_subtype. apply normalize_subtype. + change (Val.has_type res (proj_sig_res (ef_sig ef))). eapply external_call_well_typed; eauto. (* return *) inv H1. econstructor; eauto. - apply wt_regset_assign; auto. rewrite H10; auto. -Qed. - -Lemma wt_initial_state: - forall S, initial_state p S -> wt_state S. -Proof. - intros. inv H. constructor. constructor. rewrite H3; auto. - pattern f. apply Genv.find_funct_ptr_prop with fundef unit p b. - exact wt_p. exact H2. - rewrite H3. constructor. -Qed. - -Lemma wt_instr_inv: - forall s f sp pc rs m i, - wt_state (State s f sp pc rs m) -> - f.(fn_code)!pc = Some i -> - exists env, wt_instr f env i /\ wt_regset env rs. -Proof. - intros. inv H. exists env; split; auto. - inv WT_FN. eauto. + apply wt_regset_assign; auto. eapply Val.has_subtype; eauto. Qed. End SUBJECT_REDUCTION. - - |