From 255cee09b71255051c2b40eae0c88bffce1f6f32 Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 20 Apr 2013 07:54:52 +0000 Subject: Big merge of the newregalloc-int64 branch. Lots of changes in two directions: 1- new register allocator (+ live range splitting, spilling&reloading, etc) based on a posteriori validation using the Rideau-Leroy algorithm 2- support for 64-bit integer arithmetic (type "long long"). git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2200 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/Asmgenproof1.v | 45 +++++++++++++++++++++------------------------ 1 file changed, 21 insertions(+), 24 deletions(-) (limited to 'powerpc/Asmgenproof1.v') diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 0e6d3e1..cd961c9 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -546,7 +546,8 @@ Ltac ArgsInv := | [ H: Error _ = OK _ |- _ ] => discriminate | [ H: match ?args with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct args | [ H: bind _ _ = OK _ |- _ ] => monadInv H - | [ H: assertion _ = OK _ |- _ ] => monadInv H + | [ H: match _ with left _ => _ | right _ => assertion_failed end = OK _ |- _ ] => monadInv H; ArgsInv + | [ H: match _ with true => _ | false => assertion_failed end = OK _ |- _ ] => monadInv H; ArgsInv end); subst; repeat (match goal with @@ -810,9 +811,7 @@ Lemma transl_op_correct_aux: exists rs', exec_straight ge fn c rs m k rs' m /\ rs'#(preg_of res) = v - /\ forall r, - match op with Omove => data_preg r = true | _ => nontemp_preg r = true end -> - r <> preg_of res -> rs'#r = rs#r. + /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs' r = rs r. Proof. Opaque Int.eq. intros. unfold transl_op in H; destruct op; ArgsInv; simpl in H0; try (inv H0); try TranslOpSimpl. @@ -839,7 +838,7 @@ Opaque Val.add. rewrite gpr_or_zero_not_zero; eauto with asmgen. Simpl. rewrite (Val.add_commut Vzero). rewrite high_half_zero. rewrite Val.add_commut. rewrite low_high_half. auto. - intros; Simpl. + intros; Simpl. (* Oaddrstack *) destruct (addimm_correct x GPR1 i k rs m) as [rs' [EX [RES OTH]]]; eauto with asmgen. exists rs'; auto with asmgen. @@ -879,12 +878,11 @@ Opaque Val.add. intros. rewrite D; auto with asmgen. unfold rs1; Simpl. (* Oandimm *) destruct (andimm_correct x0 x i k rs m) as [rs' [A [B C]]]; eauto with asmgen. - exists rs'; auto with asmgen. (* Oorimm *) - destruct (orimm_correct x0 x i k rs m) as [rs' [A [B C]]]. + destruct (orimm_correct x0 x i k rs m) as [rs' [A [B C]]]. exists rs'; auto with asmgen. (* Oxorimm *) - destruct (xorimm_correct x0 x i k rs m) as [rs' [A [B C]]]. + destruct (xorimm_correct x0 x i k rs m) as [rs' [A [B C]]]. exists rs'; auto with asmgen. (* Onor *) replace (Val.notint (rs x)) @@ -898,7 +896,6 @@ Opaque Val.add. intros; Simpl. (* Orolm *) destruct (rolm_correct x0 x i i0 k rs m) as [rs' [A [B C]]]; eauto with asmgen. - exists rs'; auto with asmgen. (* Ointoffloat *) replace v with (Val.maketotal (Val.intoffloat (rs x))). TranslOpSimpl. @@ -916,19 +913,17 @@ Lemma transl_op_correct: Mem.extends m m' -> exists rs', exec_straight ge fn c rs m' k rs' m' - /\ agree (Regmap.set res v (undef_op op ms)) sp rs' - /\ forall r, op = Omove -> data_preg r = true -> r <> preg_of res -> rs'#r = rs#r. + /\ agree (Regmap.set res v (Mach.undef_regs (destroyed_by_op op) ms)) sp rs' + /\ forall r, data_preg r = true -> r <> preg_of res -> preg_notin r (destroyed_by_op op) -> rs' r = rs r. Proof. intros. exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eauto. intros [v' [A B]]. rewrite (sp_val _ _ _ H0) in A. exploit transl_op_correct_aux; eauto. intros [rs' [P [Q R]]]. rewrite <- Q in B. - exists rs'; split. eexact P. - split. unfold undef_op. destruct op; - (apply agree_set_undef_mreg with rs || apply agree_set_mreg with rs); + exists rs'; split. eexact P. + split. apply agree_set_undef_mreg with rs; auto. auto. - intros. subst op. auto. Qed. (** Translation of memory accesses *) @@ -1100,17 +1095,18 @@ Lemma transl_store_correct: Mem.storev chunk m a (rs (preg_of src)) = Some m' -> exists rs', exec_straight ge fn c rs m k rs' m' - /\ forall r, r <> PC -> r <> GPR11 -> r <> GPR12 -> r <> FPR13 -> rs' r = rs r. + /\ forall r, r <> PC -> preg_notin r (destroyed_by_store chunk addr) -> rs' r = rs r. Proof. +Local Transparent destroyed_by_store. intros. assert (TEMP0: int_temp_for src = GPR11 \/ int_temp_for src = GPR12). - unfold int_temp_for. destruct (mreg_eq src IT2); auto. + unfold int_temp_for. destruct (mreg_eq src R12); auto. assert (TEMP1: int_temp_for src <> GPR0). destruct TEMP0; congruence. assert (TEMP2: IR (int_temp_for src) <> preg_of src). - unfold int_temp_for. destruct (mreg_eq src IT2). + unfold int_temp_for. destruct (mreg_eq src R12). subst src; simpl; congruence. - change (IR GPR12) with (preg_of IT2). red; intros; elim n. + change (IR GPR12) with (preg_of R12). red; intros; elim n. eapply preg_of_injective; eauto. assert (BASE: forall mk1 mk2 chunk', transl_memory_access mk1 mk2 addr args (int_temp_for src) k = OK c -> @@ -1123,15 +1119,15 @@ Proof. store2 chunk' (preg_of src) r1 r2 rs1 m) -> exists rs', exec_straight ge fn c rs m k rs' m' - /\ forall r, r <> PC -> r <> GPR11 -> r <> GPR12 -> r <> FPR13 -> rs' r = rs r). + /\ forall r, r <> PC -> r <> GPR11 /\ r <> GPR12 -> rs' r = rs r). { intros. eapply transl_memory_access_correct; eauto. intros. econstructor; split. apply exec_straight_one. rewrite H4. unfold store1. rewrite H6. rewrite H7; auto with asmgen. rewrite H3. eauto. auto. - intros; Simpl. apply H7; auto. destruct TEMP0; congruence. + intros; Simpl. apply H7; auto. destruct TEMP0; destruct H9; congruence. intros. econstructor; split. apply exec_straight_one. rewrite H5. unfold store2. rewrite H6. rewrite H7; auto with asmgen. rewrite H3. eauto. auto. - intros; Simpl. apply H7; auto. destruct TEMP0; congruence. + intros; Simpl. apply H7; auto. destruct TEMP0; destruct H9; congruence. } destruct chunk; monadInv H. - (* Mint8signed *) @@ -1153,10 +1149,11 @@ Proof. eapply transl_memory_access_correct. eauto. eauto. eauto. intros. econstructor; split. apply exec_straight_one. simpl. unfold store1. rewrite H. rewrite H2; auto with asmgen. rewrite H1. eauto. auto. - intros. Simpl. apply H2; auto with asmgen. destruct TEMP0; congruence. +Local Transparent destroyed_by_store. + simpl; intros. destruct H4 as [A [B C]]. Simpl. apply H2; auto with asmgen. destruct TEMP0; congruence. intros. econstructor; split. apply exec_straight_one. simpl. unfold store2. rewrite H. rewrite H2; auto with asmgen. rewrite H1. eauto. auto. - intros. Simpl. apply H2; auto with asmgen. destruct TEMP0; congruence. + simpl; intros. destruct H4 as [A [B C]]. Simpl. apply H2; auto with asmgen. destruct TEMP0; congruence. - (* Mfloat64 *) apply Mem.storev_float64al32 in H1. eapply BASE; eauto; erewrite freg_of_eq by eauto; auto. - (* Mfloat64al32 *) -- cgit v1.2.3