From 5aea6849eed83009e300b04ef17786643ead9cbc Mon Sep 17 00:00:00 2001 From: xleroy Date: Sun, 14 Aug 2011 15:41:26 +0000 Subject: Locations.v: add Loc.diff_dec. ia32: lift restriction that 1st arg of ops cannot be ECX (could be useful for a future, better reloading strategy) git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1711 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- ia32/Asmgenproof1.v | 179 +++++++++++++++++++++++----------------------------- 1 file changed, 78 insertions(+), 101 deletions(-) (limited to 'ia32/Asmgenproof1.v') diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index d8edac08..27bc9013 100644 --- a/ia32/Asmgenproof1.v +++ b/ia32/Asmgenproof1.v @@ -589,13 +589,23 @@ Lemma mk_shift_correct: /\ forall r, nontemp_preg r = true -> r <> r1 -> rs2#r = rs1#r. Proof. unfold mk_shift; intros. - destruct (ireg_eq r2 ECX); monadInv H. + destruct (ireg_eq r2 ECX). (* fast case *) + monadInv H. econstructor. split. apply exec_straight_one. apply H0. auto. split. repeat SRes. intros. repeat SOther. +(* xchg case *) + destruct (ireg_eq r1 ECX); monadInv H. + econstructor. split. eapply exec_straight_three. + simpl; eauto. + apply H0. + simpl; eauto. + auto. auto. auto. + split. repeat SRes. repeat rewrite nextinstr_inv; auto with ppcgen. + rewrite Pregmap.gss. decEq. rewrite Pregmap.gso; auto with ppcgen. apply Pregmap.gss. + intros. destruct (preg_eq r r2). subst. repeat SRes. repeat SOther. (* general case *) - monadInv EQ. econstructor. split. eapply exec_straight_two. simpl; eauto. apply H0. auto. auto. split. repeat SRes. repeat rewrite nextinstr_inv; auto with ppcgen. @@ -603,8 +613,40 @@ Proof. intros. repeat SOther. Qed. -(** Smart constructor for division *) +(** Parallel move 2 *) +Lemma mk_mov2_correct: + forall src1 dst1 src2 dst2 k rs m, + dst1 <> dst2 -> + exists rs', + exec_straight (mk_mov2 src1 dst1 src2 dst2 k) rs m k rs' m + /\ rs'#dst1 = rs#src1 + /\ rs'#dst2 = rs#src2 + /\ forall r, r <> PC -> r <> dst1 -> r <> dst2 -> rs'#r = rs#r. +Proof. + intros. unfold mk_mov2. +(* single moves *) + destruct (ireg_eq src1 dst1). subst. + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split. repeat SRes. split. repeat SRes. intros; repeat SOther. + destruct (ireg_eq src2 dst2). subst. + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split. repeat SRes. split. repeat SRes. intros; repeat SOther. +(* xchg *) + destruct (ireg_eq src2 dst1). destruct (ireg_eq src1 dst2). + subst. econstructor; split. apply exec_straight_one. simpl; eauto. auto. + split. repeat SRes. split. repeat SRes. intros; repeat SOther. +(* move 2; move 1 *) + subst. econstructor; split. eapply exec_straight_two. + simpl; eauto. simpl; eauto. auto. auto. + split. repeat SRes. split. repeat SRes. intros; repeat SOther. +(* move 1; move 2*) + subst. econstructor; split. eapply exec_straight_two. + simpl; eauto. simpl; eauto. auto. auto. + split. repeat SRes. split. repeat SRes. intros; repeat SOther. +Qed. + +(** Smart constructor for division *) Lemma mk_div_correct: forall mkinstr dsem msem r1 r2 k c rs1 m, @@ -629,52 +671,19 @@ Proof. split. repeat SRes. decEq. apply Pregmap.gso. congruence. intros. repeat SOther. (* r1 <> EAX *) - monadInv H. monadInv EQ. destruct (ireg_eq r2 EAX); monadInv EQ0. -(* r1 <> EAX, r1 <> ECX, r2 = EAX *) - set (rs2 := nextinstr (rs1#ECX <- (rs1#EAX))). - set (rs3 := nextinstr (rs2#EAX <- (rs2#r1))). - set (rs4 := nextinstr_nf (rs3#EAX <- (dsem rs3#EAX (rs3#EDX <- Vundef)#ECX) - #EDX <- (msem rs3#EAX (rs3#EDX <- Vundef)#ECX))). - set (rs5 := nextinstr (rs4#r1 <- (rs4#EAX))). - set (rs6 := nextinstr (rs5#EAX <- (rs5#ECX))). - exists rs6. split. apply exec_straight_step with rs2 m; auto. - apply exec_straight_step with rs3 m; auto. - apply exec_straight_step with rs4 m; auto. apply H0. - apply exec_straight_step with rs5 m; auto. - apply exec_straight_one; auto. - split. unfold rs6. SRes. unfold rs5. repeat SRes. - unfold rs4. repeat SRes. decEq. - unfold rs3. repeat SRes. unfold rs2. repeat SRes. - intros. unfold rs6. SOther. - unfold Pregmap.set. destruct (PregEq.eq r EAX). subst r. - unfold rs5. repeat SOther. - unfold rs5. repeat SOther. unfold rs4. repeat SOther. - unfold rs3. repeat SOther. unfold rs2. repeat SOther. -(* r1 <> EAX, r1 <> ECX, r2 <> EAX *) + monadInv H. set (rs2 := nextinstr (rs1#XMM7 <- (rs1#EAX))). - set (rs3 := nextinstr (rs2#ECX <- (rs2#r2))). - set (rs4 := nextinstr (rs3#EAX <- (rs3#r1))). - set (rs5 := nextinstr_nf (rs4#EAX <- (dsem rs4#EAX (rs4#EDX <- Vundef)#ECX) - #EDX <- (msem rs4#EAX (rs4#EDX <- Vundef)#ECX))). - set (rs6 := nextinstr (rs5#r2 <- (rs5#ECX))). - set (rs7 := nextinstr (rs6#r1 <- (rs6#EAX))). - set (rs8 := nextinstr (rs7#EAX <- (rs7#XMM7))). - exists rs8. split. apply exec_straight_step with rs2 m; auto. - apply exec_straight_step with rs3 m; auto. - apply exec_straight_step with rs4 m; auto. - apply exec_straight_step with rs5 m; auto. apply H0. - apply exec_straight_step with rs6 m; auto. - apply exec_straight_step with rs7 m; auto. - apply exec_straight_one; auto. - split. unfold rs8. SRes. unfold rs7. repeat SRes. - unfold rs6. repeat SRes. unfold rs5. repeat SRes. - decEq. unfold rs4. repeat SRes. unfold rs3. repeat SRes. - intros. unfold rs8. SOther. - unfold Pregmap.set. destruct (PregEq.eq r EAX). subst r. auto. - unfold rs7. repeat SOther. unfold rs6. SOther. - unfold Pregmap.set. destruct (PregEq.eq r r2). subst r. auto. - unfold rs5. repeat SOther. unfold rs4. repeat SOther. - unfold rs3. repeat SOther. unfold rs2. repeat SOther. + exploit (mk_mov2_correct r1 EAX r2 ECX). congruence. instantiate (1 := rs2). + intros [rs3 [A [B [C D]]]]. + econstructor; split. + apply exec_straight_step with rs2 m; auto. + eapply exec_straight_trans. eexact A. + eapply exec_straight_three. simpl; eauto. simpl; eauto. simpl; eauto. + auto. auto. auto. + split. repeat SRes. decEq. rewrite B; unfold rs2; SRes. SOther. + intros. destruct (preg_eq r EAX). subst. + repeat SRes. rewrite D; auto with ppcgen. + repeat SOther. rewrite D; auto with ppcgen. unfold rs2; repeat SOther. Qed. (** Smart constructor for modulus *) @@ -703,55 +712,19 @@ Proof. split. repeat SRes. decEq. apply Pregmap.gso. congruence. intros. repeat SOther. (* r1 <> EAX *) - monadInv H. monadInv EQ. destruct (ireg_eq r2 EDX); monadInv EQ0. -(* r1 <> EAX, r1 <> ECX, r2 = EDX *) - set (rs2 := nextinstr (rs1#XMM7 <- (rs1#EAX))). - set (rs3 := nextinstr (rs2#ECX <- (rs2#EDX))). - set (rs4 := nextinstr (rs3#EAX <- (rs3#r1))). - set (rs5 := nextinstr_nf (rs4#EAX <- (dsem rs4#EAX (rs4#EDX <- Vundef)#ECX) - #EDX <- (msem rs4#EAX (rs4#EDX <- Vundef)#ECX))). - set (rs6 := nextinstr (rs5#r1 <- (rs5#EDX))). - set (rs7 := nextinstr (rs6#EAX <- (rs6#XMM7))). - exists rs7. split. apply exec_straight_step with rs2 m; auto. - apply exec_straight_step with rs3 m; auto. - apply exec_straight_step with rs4 m; auto. - apply exec_straight_step with rs5 m; auto. apply H0. - apply exec_straight_step with rs6 m; auto. - apply exec_straight_one; auto. - split. unfold rs7. repeat SRes. unfold rs6. repeat SRes. - unfold rs5. repeat SRes. decEq. - unfold rs4. repeat SRes. unfold rs3. repeat SRes. - intros. unfold rs7. SOther. - unfold Pregmap.set. destruct (PregEq.eq r EAX). subst r. - unfold rs6. repeat SOther. - unfold rs6. repeat SOther. - unfold rs5. repeat SOther. unfold rs4. repeat SOther. - unfold rs3. repeat SOther. unfold rs2. repeat SOther. -(* r1 <> EAX, r1 <> ECX, r2 <> EDX *) + monadInv H. set (rs2 := nextinstr (rs1#XMM7 <- (rs1#EAX))). - set (rs3 := nextinstr (rs2#ECX <- (rs2#r2))). - set (rs4 := nextinstr (rs3#EAX <- (rs3#r1))). - set (rs5 := nextinstr_nf (rs4#EAX <- (dsem rs4#EAX (rs4#EDX <- Vundef)#ECX) - #EDX <- (msem rs4#EAX (rs4#EDX <- Vundef)#ECX))). - set (rs6 := nextinstr (rs5#r2 <- (rs5#ECX))). - set (rs7 := nextinstr (rs6#r1 <- (rs6#EDX))). - set (rs8 := nextinstr (rs7#EAX <- (rs7#XMM7))). - exists rs8. split. apply exec_straight_step with rs2 m; auto. - apply exec_straight_step with rs3 m; auto. - apply exec_straight_step with rs4 m; auto. - apply exec_straight_step with rs5 m; auto. apply H0. - apply exec_straight_step with rs6 m; auto. - apply exec_straight_step with rs7 m; auto. - apply exec_straight_one; auto. - split. unfold rs8. SRes. unfold rs7. repeat SRes. - unfold rs6. repeat SRes. unfold rs5. repeat SRes. - decEq. unfold rs4. repeat SRes. unfold rs3. repeat SRes. - intros. unfold rs8. SOther. - unfold Pregmap.set. destruct (PregEq.eq r EAX). subst r. auto. - unfold rs7. repeat SOther. unfold rs6. SOther. - unfold Pregmap.set. destruct (PregEq.eq r r2). subst r. auto. - unfold rs5. repeat SOther. unfold rs4. repeat SOther. - unfold rs3. repeat SOther. unfold rs2. repeat SOther. + exploit (mk_mov2_correct r1 EAX r2 ECX). congruence. instantiate (1 := rs2). + intros [rs3 [A [B [C D]]]]. + econstructor; split. + apply exec_straight_step with rs2 m; auto. + eapply exec_straight_trans. eexact A. + eapply exec_straight_three. simpl; eauto. simpl; eauto. simpl; eauto. + auto. auto. auto. + split. repeat SRes. decEq. rewrite B; unfold rs2; SRes. SOther. + intros. destruct (preg_eq r EAX). subst. + repeat SRes. rewrite D; auto with ppcgen. + repeat SOther. rewrite D; auto with ppcgen. unfold rs2; repeat SOther. Qed. (** Smart constructor for [shrx] *) @@ -766,15 +739,19 @@ Lemma mk_shrximm_correct: /\ rs2#r1 = Vint (Int.shrx x n) /\ forall r, nontemp_preg r = true -> r <> r1 -> rs2#r = rs1#r. Proof. - unfold mk_shrximm; intros. monadInv H. monadInv EQ. + unfold mk_shrximm; intros. inv H. + set (tmp := if ireg_eq r1 ECX then EDX else ECX). + assert (TMP1: tmp <> r1). unfold tmp; destruct (ireg_eq r1 ECX); congruence. + assert (TMP2: nontemp_preg tmp = false). unfold tmp; destruct (ireg_eq r1 ECX); auto. rewrite Int.shrx_shr; auto. set (tnm1 := Int.sub (Int.shl Int.one n) Int.one). set (x' := Int.add x tnm1). set (rs2 := nextinstr (compare_ints (Vint x) (Vint Int.zero) rs1)). - set (rs3 := nextinstr (rs2#ECX <- (Vint x'))). + set (rs3 := nextinstr (rs2#tmp <- (Vint x'))). set (rs4 := nextinstr (if Int.lt x Int.zero then rs3#r1 <- (Vint x') else rs3)). set (rs5 := nextinstr_nf (rs4#r1 <- (Val.shr rs4#r1 (Vint n)))). assert (rs3#r1 = Vint x). unfold rs3. SRes. SRes. + assert (rs3#tmp = Vint x'). unfold rs3. SRes. SRes. exists rs5. split. apply exec_straight_step with rs2 m. simpl. rewrite H0. simpl. rewrite Int.and_idem. auto. auto. apply exec_straight_step with rs3 m. simpl. @@ -783,7 +760,7 @@ Proof. apply exec_straight_step with rs4 m. simpl. change (rs3 SOF) with (rs2 SOF). unfold rs2. rewrite nextinstr_inv; auto with ppcgen. unfold compare_ints. rewrite Pregmap.gso; auto with ppcgen. rewrite Pregmap.gss. - simpl. unfold rs4. destruct (Int.lt x Int.zero); auto. + simpl. unfold rs4. destruct (Int.lt x Int.zero); auto. rewrite H2; auto. unfold rs4. destruct (Int.lt x Int.zero); auto. apply exec_straight_one. auto. auto. split. unfold rs5. SRes. SRes. unfold rs4. rewrite nextinstr_inv; auto with ppcgen. @@ -791,8 +768,8 @@ Proof. unfold Int.ltu in *. change (Int.unsigned (Int.repr 31)) with 31 in H1. destruct (zlt (Int.unsigned n) 31); try discriminate. change (Int.unsigned Int.iwordsize) with 32. apply zlt_true. omega. - destruct (Int.lt x Int.zero). rewrite Pregmap.gss. unfold Val.shr. rewrite H2. auto. - rewrite H. unfold Val.shr. rewrite H2. auto. + destruct (Int.lt x Int.zero). rewrite Pregmap.gss. unfold Val.shr. rewrite H3. auto. + rewrite H. unfold Val.shr. rewrite H3. auto. intros. unfold rs5. repeat SOther. unfold rs4. SOther. transitivity (rs3#r). destruct (Int.lt x Int.zero). SOther. auto. unfold rs3. repeat SOther. unfold rs2. repeat SOther. -- cgit