From 2a0168fea37b68ad14e2cb60bf215111e49d4870 Mon Sep 17 00:00:00 2001 From: xleroy Date: Wed, 23 Jul 2014 08:54:56 +0000 Subject: Merge of "newspilling" branch: - Support single-precision floats as first-class values - Introduce chunks Many32, Many64 and types Tany32, Tany64 to support saving and restoring registers without knowing the exact types (int/single/float) of their contents, just their sizes. - Memory model: generalize the opaque encoding of pointers to apply to any value, not just pointers, if chunks Many32/Many64 are selected. - More properties of FP arithmetic proved. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2537 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/RTLtyping.v | 88 ++++++++++++++++++----------------------------------- 1 file changed, 30 insertions(+), 58 deletions(-) (limited to 'backend/RTLtyping.v') diff --git a/backend/RTLtyping.v b/backend/RTLtyping.v index e8ae7ae0..5042c775 100644 --- a/backend/RTLtyping.v +++ b/backend/RTLtyping.v @@ -36,8 +36,6 @@ 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]. Additionally, we impose that each pseudo-register has the same type throughout the function. This requirement helps with register allocation, @@ -57,11 +55,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. @@ -86,39 +79,39 @@ Inductive wt_instr : instruction -> Prop := forall op args res s, op <> Omove -> map env args = fst (type_of_operation op) -> - env res = normalize (snd (type_of_operation op)) -> + env res = snd (type_of_operation op) -> 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) -> + env dst = type_of_chunk chunk -> 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 -> + env src = type_of_chunk chunk -> 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) -> + map env args = sig.(sig_args) -> + env res = proj_sig_res sig -> 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) -> + map env args = sig.(sig_args) -> sig.(sig_res) = funct.(fn_sig).(sig_res) -> 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)) -> + map env args = (ef_sig ef).(sig_args) -> + env res = proj_sig_res (ef_sig ef) -> valid_successor s -> wt_instr (Ibuiltin ef args res s) | wt_Icond: @@ -139,7 +132,7 @@ Inductive wt_instr : instruction -> Prop := | wt_Ireturn_some: forall arg ty, funct.(fn_sig).(sig_res) = Some ty -> - env arg = normalize ty -> + env arg = ty -> wt_instr (Ireturn (Some arg)). End WT_INSTR. @@ -152,7 +145,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); + map env f.(fn_params) = f.(fn_sig).(sig_args); wt_norepet: list_norepet f.(fn_params); wt_instrs: @@ -231,23 +224,23 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv := 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.set_list e args targs; S.set 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)) + S.set 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) + S.set e1 src (type_of_chunk 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.set_list e1 args sig.(sig_args); + S.set 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.set_list 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,8 +249,8 @@ 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)) + do e1 <- S.set_list e args sig.(sig_args); + S.set e1 res (proj_sig_res sig) | Icond cond args s1 s2 => do x1 <- check_successor s1; do x2 <- check_successor s2; @@ -271,7 +264,7 @@ Definition type_instr (e: S.typenv) (i: instruction) : res S.typenv := | 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.set e r t | _, _ => Error(msg "bad return") end end. @@ -297,7 +290,7 @@ Definition check_params_norepet (params: list reg): res unit := 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.set_list 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); @@ -597,7 +590,7 @@ 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.set_list_complete te f.(fn_params) f.(fn_sig).(sig_args) e1) as (e2 & C & D); 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 +630,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 -> @@ -684,9 +660,8 @@ Proof. intros. inv H. simpl in H0. inv H0. apply wt_regset_assign; auto. rewrite H4; auto. - eapply wt_regset_assign2; auto. - eapply type_of_operation_sound; eauto. - auto. + eapply wt_regset_assign; auto. + rewrite H8. eapply type_of_operation_sound; eauto. Qed. Lemma wt_exec_Iload: @@ -697,8 +672,7 @@ 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. - eapply Mem.load_type; eauto. + eapply wt_regset_assign; eauto. rewrite H8; eapply Mem.load_type; eauto. Qed. Lemma wt_exec_Ibuiltin: @@ -709,8 +683,8 @@ Lemma wt_exec_Ibuiltin: wt_regset env (rs#res <- vres). Proof. intros. inv H. - eapply wt_regset_assign2; eauto. - eapply external_call_well_typed; eauto. + eapply wt_regset_assign; eauto. + rewrite H7; eapply external_call_well_typed; eauto. Qed. Lemma wt_instr_at: @@ -728,7 +702,7 @@ Inductive wt_stackframes: list stackframe -> signature -> Prop := forall s res f sp pc rs env sg, wt_function f env -> wt_regset env rs -> - env res = normalize (proj_sig_res sg) -> + env res = proj_sig_res sg -> wt_stackframes s (fn_sig f) -> wt_stackframes (Stackframe res f sp pc rs :: s) sg. @@ -743,12 +717,12 @@ Inductive wt_state: state -> Prop := forall s f args m, wt_stackframes s (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)) -> + Val.has_type v (proj_sig_res sg) -> wt_state (Returnstate s v m). Remark wt_stackframes_change_sig: @@ -814,15 +788,13 @@ Proof. econstructor; eauto. (* Ireturn *) econstructor; eauto. - inv WTI; simpl. auto. unfold proj_sig_res; rewrite H2. rewrite <- H3. auto. + inv WTI; simpl. auto. unfold proj_sig_res; rewrite H2. 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. - change (Val.has_type res (normalize (proj_sig_res (ef_sig ef)))). - eapply Val.has_subtype. apply normalize_subtype. eapply external_call_well_typed; eauto. (* return *) inv H1. econstructor; eauto. -- cgit