diff options
| -rw-r--r-- | .depend | 6 | ||||
| -rw-r--r-- | backend/Locations.v | 9 | ||||
| -rw-r--r-- | ia32/Asm.v | 15 | ||||
| -rw-r--r-- | ia32/Asmgen.v | 48 | ||||
| -rw-r--r-- | ia32/Asmgenproof.v | 18 | ||||
| -rw-r--r-- | ia32/Asmgenproof1.v | 179 | ||||
| -rw-r--r-- | ia32/Asmgenretaddr.v | 14 |
7 files changed, 145 insertions, 144 deletions
@@ -85,9 +85,9 @@ backend/Stackingtyping.vo backend/Stackingtyping.glob: backend/Stackingtyping.v backend/Machsem.vo backend/Machsem.glob: backend/Machsem.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo $(ARCH)/$(VARIANT)/Stacklayout.vo $(ARCH)/Asmgenretaddr.vo $(ARCH)/Asm.vo $(ARCH)/Asm.glob: $(ARCH)/Asm.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo backend/Locations.vo $(ARCH)/$(VARIANT)/Stacklayout.vo backend/Conventions.vo $(ARCH)/Asmgen.vo $(ARCH)/Asmgen.glob: $(ARCH)/Asmgen.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo -$(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenretaddr.glob: $(ARCH)/Asmgenretaddr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo -$(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob: $(ARCH)/Asmgenproof1.v lib/Coqlib.vo lib/Maps.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machsem.vo backend/Machtyping.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo -$(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob: $(ARCH)/Asmgenproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Conventions.vo backend/Mach.vo backend/Machsem.vo backend/Machtyping.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo $(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenproof1.vo +$(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenretaddr.glob: $(ARCH)/Asmgenretaddr.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo +$(ARCH)/Asmgenproof1.vo $(ARCH)/Asmgenproof1.glob: $(ARCH)/Asmgenproof1.v lib/Coqlib.vo lib/Maps.vo common/AST.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Globalenvs.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machsem.vo backend/Machtyping.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo backend/Conventions.vo +$(ARCH)/Asmgenproof.vo $(ARCH)/Asmgenproof.glob: $(ARCH)/Asmgenproof.v lib/Coqlib.vo lib/Maps.vo common/Errors.vo common/AST.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo $(ARCH)/Op.vo backend/Locations.vo backend/Mach.vo backend/Machsem.vo backend/Machtyping.vo backend/Conventions.vo $(ARCH)/Asm.vo $(ARCH)/Asmgen.vo $(ARCH)/Asmgenretaddr.vo $(ARCH)/Asmgenproof1.vo cfrontend/Csyntax.vo cfrontend/Csyntax.glob: cfrontend/Csyntax.v lib/Coqlib.vo common/Errors.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo cfrontend/Csem.vo cfrontend/Csem.glob: cfrontend/Csem.v lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo cfrontend/Csyntax.vo common/Smallstep.vo cfrontend/Cstrategy.vo cfrontend/Cstrategy.glob: cfrontend/Cstrategy.v lib/Axioms.vo lib/Coqlib.vo common/Errors.vo lib/Maps.vo lib/Integers.vo lib/Floats.vo common/Values.vo common/AST.vo common/Memory.vo common/Events.vo common/Globalenvs.vo common/Smallstep.vo cfrontend/Csyntax.vo cfrontend/Csem.vo diff --git a/backend/Locations.v b/backend/Locations.v index 1270e1d..8a0b5ea 100644 --- a/backend/Locations.v +++ b/backend/Locations.v @@ -280,6 +280,15 @@ Module Loc. apply overlap_aux_false_1. exact H0. Qed. + Definition diff_dec (l1 l2: loc) : { Loc.diff l1 l2 } + {~Loc.diff l1 l2}. + Proof. + intros. case (eq l1 l2); intros. + right. rewrite e. apply same_not_diff. + case_eq (overlap l1 l2); intros. + right. apply overlap_not_diff; auto. + left. apply non_overlap_diff; auto. + Qed. + (** We now redefine some standard notions over lists, using the [Loc.diff] predicate instead of standard disequality [<>]. @@ -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: |