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/Asm.v | 15 +---- ia32/Asmgen.v | 48 +++++++------- ia32/Asmgenproof.v | 18 +++++- ia32/Asmgenproof1.v | 179 ++++++++++++++++++++++----------------------------- ia32/Asmgenretaddr.v | 14 +++- 5 files changed, 133 insertions(+), 141 deletions(-) (limited to 'ia32') diff --git a/ia32/Asm.v b/ia32/Asm.v index 2eb6a8d..002119e 100644 --- a/ia32/Asm.v +++ b/ia32/Asm.v @@ -120,6 +120,7 @@ Inductive instruction: Type := | Pfld_m (a: addrmode) (**r [fld] from memory *) | Pfstp_f (rd: freg) (**r [fstp] to XMM register (pseudo) *) | Pfstp_m (a: addrmode) (**r [fstp] to memory *) + | Pxchg_rr (r1: ireg) (r2: ireg) (**r register-register exchange *) (** Moves with conversion *) | Pmovb_mr (a: addrmode) (rs: ireg) (**r [mov] (8-bit int) *) | Pmovw_mr (a: addrmode) (rs: ireg) (**r [mov] (16-bit int) *) @@ -380,18 +381,6 @@ Definition eval_testcond (c: testcond) (rs: regset) : option bool := | Vint n => Some (Int.eq n Int.zero) | _ => None end -(* - | Cond_nep => - match rs PF, rs ZF with - | Vint p, Vint z => Some (Int.eq p Int.one || Int.eq z Int.zero) - | _, _ => None - end - | Cond_enp => - match rs PF, rs ZF with - | Vint p, Vint z => Some (Int.eq p Int.zero && Int.eq z Int.one) - | _, _ => None - end -*) end. (** The semantics is purely small-step and defined as a function @@ -491,6 +480,8 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome Next (nextinstr (rs#rd <- (rs ST0) #ST0 <- Vundef)) m | Pfstp_m a => exec_store Mfloat64 m a rs ST0 + | Pxchg_rr r1 r2 => + Next (nextinstr (rs#r1 <- (rs r2) #r2 <- (rs r1))) m (** Moves with conversion *) | Pmovb_mr a r1 => exec_store Mint8unsigned m a rs r1 diff --git a/ia32/Asmgen.v b/ia32/Asmgen.v index 452f2e7..4c1167b 100644 --- a/ia32/Asmgen.v +++ b/ia32/Asmgen.v @@ -33,8 +33,6 @@ Open Local Scope error_monad_scope. - Argument and result registers are of the correct type. - For two-address instructions, the result and the first argument are in the same register. (True by construction in [RTLgen], and preserved by [Reload].) -- The first argument register is never [ECX] (a.k.a. [IT2]) nor [XMM7] - (a.k.a [FT2]). - The top of the floating-point stack ([ST0], a.k.a. [FP0]) can only appear in [mov] instructions, but never in arithmetic instructions. @@ -64,10 +62,24 @@ Definition mk_shift (shift_instr: ireg -> instruction) (r1 r2: ireg) (k: code) : res code := if ireg_eq r2 ECX then OK (shift_instr r1 :: k) + else if ireg_eq r1 ECX then + OK (Pxchg_rr r2 ECX :: shift_instr r2 :: Pxchg_rr r2 ECX :: k) else - do x <- assertion (negb (ireg_eq r1 ECX)); OK (Pmov_rr ECX r2 :: shift_instr r1 :: k). +Definition mk_mov2 (src1 dst1 src2 dst2: ireg) (k: code) : code := + if ireg_eq src1 dst1 then + Pmov_rr dst2 src2 :: k + else if ireg_eq src2 dst2 then + Pmov_rr dst1 src1 :: k + else if ireg_eq src2 dst1 then + if ireg_eq src1 dst2 then + Pxchg_rr src1 src2 :: k + else + Pmov_rr dst2 src2 :: Pmov_rr dst1 src1 :: k + else + Pmov_rr dst1 src1 :: Pmov_rr dst2 src2 :: k. + Definition mk_div (div_instr: ireg -> instruction) (r1 r2: ireg) (k: code) : res code := if ireg_eq r1 EAX then @@ -76,15 +88,9 @@ Definition mk_div (div_instr: ireg -> instruction) else OK (div_instr r2 :: k) else - do x <- assertion (negb (ireg_eq r1 ECX)); - if ireg_eq r2 EAX then - OK (Pmov_rr ECX EAX :: Pmov_rr EAX r1 :: - div_instr ECX :: - Pmov_rr r1 EAX :: Pmov_rr EAX ECX :: k) - else - OK (Pmovd_fr XMM7 EAX :: Pmov_rr ECX r2 :: Pmov_rr EAX r1 :: - div_instr ECX :: - Pmov_rr r2 ECX :: Pmov_rr r1 EAX :: Pmovd_rf EAX XMM7 :: k). + OK (Pmovd_fr XMM7 EAX :: + mk_mov2 r1 EAX r2 ECX + (div_instr ECX :: Pmov_rr r1 EAX :: Pmovd_rf EAX XMM7 :: k)). Definition mk_mod (div_instr: ireg -> instruction) (r1 r2: ireg) (k: code) : res code := @@ -94,22 +100,16 @@ Definition mk_mod (div_instr: ireg -> instruction) else OK (div_instr r2 :: Pmov_rr EAX EDX :: k) else - do x <- assertion (negb (ireg_eq r1 ECX)); - if ireg_eq r2 EDX then - OK (Pmovd_fr XMM7 EAX :: Pmov_rr ECX EDX :: Pmov_rr EAX r1 :: - div_instr ECX :: - Pmov_rr r1 EDX :: Pmovd_rf EAX XMM7 :: k) - else - OK (Pmovd_fr XMM7 EAX :: Pmov_rr ECX r2 :: Pmov_rr EAX r1 :: - div_instr ECX :: - Pmov_rr r2 ECX :: Pmov_rr r1 EDX :: Pmovd_rf EAX XMM7 :: k). + OK (Pmovd_fr XMM7 EAX :: + mk_mov2 r1 EAX r2 ECX + (div_instr ECX :: Pmov_rr r1 EDX :: Pmovd_rf EAX XMM7 :: k)). Definition mk_shrximm (r: ireg) (n: int) (k: code) : res code := - do x <- assertion (negb (ireg_eq r ECX)); + let tmp := if ireg_eq r ECX then EDX else ECX in let p := Int.sub (Int.shl Int.one n) Int.one in OK (Ptest_rr r r :: - Plea ECX (Addrmode (Some r) None (inl _ p)) :: - Pcmov Cond_l r ECX :: + Plea tmp (Addrmode (Some r) None (inl _ p)) :: + Pcmov Cond_l r tmp :: Psar_ri r n :: k). Definition low_ireg (r: ireg) : bool := diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index 6c68b37..5b98d27 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -332,7 +332,19 @@ Remark mk_shift_label: find_label lbl c = find_label lbl k. Proof. unfold mk_shift; intros. - destruct (ireg_eq r2 ECX); monadInv H; simpl; rewrite H0; auto. + destruct (ireg_eq r2 ECX). monadInv H; simpl; rewrite H0; auto. + destruct (ireg_eq r1 ECX); monadInv H; simpl; rewrite H0; auto. +Qed. + +Remark mk_mov2_label: + forall r1 r2 r3 r4 k, + find_label lbl (mk_mov2 r1 r2 r3 r4 k) = find_label lbl k. +Proof. + intros; unfold mk_mov2. + destruct (ireg_eq r1 r2); auto. + destruct (ireg_eq r3 r4); auto. + destruct (ireg_eq r3 r2); auto. + destruct (ireg_eq r1 r4); auto. Qed. Remark mk_div_label: @@ -343,7 +355,7 @@ Proof. unfold mk_div; intros. destruct (ireg_eq r1 EAX). destruct (ireg_eq r2 EDX); monadInv H; simpl; rewrite H0; auto. - destruct (ireg_eq r2 EAX); monadInv H; simpl; rewrite H0; auto. + monadInv H; simpl. rewrite mk_mov2_label. simpl; rewrite H0; auto. Qed. Remark mk_mod_label: @@ -354,7 +366,7 @@ Proof. unfold mk_mod; intros. destruct (ireg_eq r1 EAX). destruct (ireg_eq r2 EDX); monadInv H; simpl; rewrite H0; auto. - destruct (ireg_eq r2 EDX); monadInv H; simpl; rewrite H0; auto. + monadInv H; simpl. rewrite mk_mov2_label. simpl; rewrite H0; auto. Qed. Remark mk_shrximm_label: diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index d8edac0..27bc901 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. diff --git a/ia32/Asmgenretaddr.v b/ia32/Asmgenretaddr.v index e0787d7..e963c2e 100644 --- a/ia32/Asmgenretaddr.v +++ b/ia32/Asmgenretaddr.v @@ -112,7 +112,7 @@ Ltac IsTail := match goal with | [ |- is_tail _ (_ :: _) ] => constructor; IsTail | [ H: Error _ = OK _ |- _ ] => discriminate - | [ H: OK _ = OK _ |- _ ] => inversion H; subst; IsTail + | [ H: OK _ = OK _ |- _ ] => inv H; IsTail | [ H: bind _ _ = OK _ |- _ ] => monadInv H; IsTail | [ H: (if ?x then _ else _) = OK _ |- _ ] => destruct x; IsTail | [ H: match ?x with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct x; IsTail @@ -131,16 +131,28 @@ Proof. unfold mk_shift; intros; IsTail. Qed. +Lemma mk_mov2_tail: + forall r1 r2 r3 r4 k, is_tail k (mk_mov2 r1 r2 r3 r4 k). +Proof. + unfold mk_mov2; intros. + destruct (ireg_eq r1 r2). IsTail. + destruct (ireg_eq r3 r4). IsTail. + destruct (ireg_eq r3 r2); IsTail. + destruct (ireg_eq r1 r4); IsTail. +Qed. + Lemma mk_div_tail: forall di r1 r2 k c, mk_div di r1 r2 k = OK c -> is_tail k c. Proof. unfold mk_div; intros; IsTail. + eapply is_tail_trans. 2: eapply mk_mov2_tail. IsTail. Qed. Lemma mk_mod_tail: forall di r1 r2 k c, mk_mod di r1 r2 k = OK c -> is_tail k c. Proof. unfold mk_mod; intros; IsTail. + eapply is_tail_trans. 2: eapply mk_mov2_tail. IsTail. Qed. Lemma mk_shrximm_tail: -- cgit v1.2.3