From 5909a0340ad0fe871dede1eaead855fb4b68fb0e Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 8 Aug 2011 06:31:10 +0000 Subject: IA32 port: more faithful treatment of pseudoregister ST0. Related general change: support for destroyed_at_moves. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1700 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- ia32/Asm.v | 4 ++-- ia32/Asmgenproof.v | 6 ++--- ia32/Asmgenproof1.v | 57 +++++++++++++++++++++++++++++++++++--------- ia32/standard/Conventions1.v | 17 +++++++++---- 4 files changed, 63 insertions(+), 21 deletions(-) (limited to 'ia32') diff --git a/ia32/Asm.v b/ia32/Asm.v index 1870d698..2eb6a8d3 100644 --- a/ia32/Asm.v +++ b/ia32/Asm.v @@ -437,7 +437,7 @@ Definition exec_load (chunk: memory_chunk) (m: mem) Definition exec_store (chunk: memory_chunk) (m: mem) (a: addrmode) (rs: regset) (r1: preg) := match Mem.storev chunk m (eval_addrmode a rs) (rs r1) with - | Some m' => Next (nextinstr_nf rs) m' + | Some m' => Next (nextinstr_nf (if preg_eq r1 ST0 then rs#ST0 <- Vundef else rs)) m' | None => Stuck end. @@ -488,7 +488,7 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome | Pfld_m a => exec_load Mfloat64 m a rs ST0 | Pfstp_f rd => - Next (nextinstr (rs#rd <- (rs ST0))) m + Next (nextinstr (rs#rd <- (rs ST0) #ST0 <- Vundef)) m | Pfstp_m a => exec_store Mfloat64 m a rs ST0 (** Moves with conversion *) diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index 45ac48d3..6c68b376 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -758,7 +758,7 @@ Lemma exec_Msetstack_prop: (ms : mreg -> val) (m m' : mem), store_stack m sp ty ofs (ms src) = Some m' -> exec_instr_prop (Machsem.State s fb sp (Msetstack src ofs ty :: c) ms m) E0 - (Machsem.State s fb sp c ms m'). + (Machsem.State s fb sp c (undef_setstack ms) m'). Proof. intros; red; intros; inv MS. unfold store_stack in H. @@ -768,7 +768,7 @@ Proof. left; eapply exec_straight_steps; eauto. intros. simpl in H1. exploit storeind_correct; eauto. intros [rs' [P Q]]. exists rs'; split. eauto. - split. eapply agree_exten; eauto. + split. unfold undef_setstack. eapply agree_undef_move; eauto. simpl; intros. rewrite Q; auto with ppcgen. Qed. @@ -834,7 +834,7 @@ Proof. split. rewrite <- Q in B. unfold undef_op. destruct op; try (eapply agree_set_undef_mreg; eauto). - eapply agree_set_mreg; eauto. + eapply agree_set_undef_move_mreg; eauto. simpl; congruence. Qed. diff --git a/ia32/Asmgenproof1.v b/ia32/Asmgenproof1.v index 3a91ac50..d8edac08 100644 --- a/ia32/Asmgenproof1.v +++ b/ia32/Asmgenproof1.v @@ -232,6 +232,7 @@ Qed. Hint Resolve nontemp_diff: ppcgen. +(* Remark undef_regs_1: forall l ms r, ms r = Vundef -> Mach.undef_regs l ms r = Vundef. Proof. @@ -253,6 +254,7 @@ Proof. induction l; simpl; intros. auto. rewrite IHl. apply Regmap.gso. intuition. intuition. Qed. +*) Lemma agree_exten_temps: forall ms sp rs rs', @@ -263,12 +265,29 @@ Proof. intros. destruct H. split. rewrite H0; auto. auto. intros. unfold undef_temps. - destruct (In_dec mreg_eq r (int_temporaries ++ float_temporaries)). - rewrite undef_regs_2; auto. - rewrite undef_regs_3; auto. rewrite H0; auto. + destruct (In_dec mreg_eq r temporary_regs). + rewrite Mach.undef_regs_same; auto. + rewrite Mach.undef_regs_other; auto. rewrite H0; auto. simpl in n. destruct r; auto; intuition. Qed. +Lemma agree_undef_move: + forall ms sp rs rs', + agree ms sp rs -> + (forall r, important_preg r = true -> r <> ST0 -> rs'#r = rs#r) -> + agree (undef_move ms) sp rs'. +Proof. + intros. destruct H. split. + rewrite H0; auto. congruence. auto. + intros. unfold undef_move. + destruct (In_dec mreg_eq r destroyed_at_move_regs). + rewrite Mach.undef_regs_same; auto. + rewrite Mach.undef_regs_other; auto. + assert (important_preg (preg_of r) = true /\ preg_of r <> ST0). + simpl in n. destruct r; simpl; auto; intuition congruence. + destruct H. rewrite H0; auto. +Qed. + Lemma agree_set_undef_mreg: forall ms sp rs r v rs', agree ms sp rs -> @@ -283,6 +302,20 @@ Proof. intros. rewrite Pregmap.gso; auto. Qed. +Lemma agree_set_undef_move_mreg: + forall ms sp rs r v rs', + agree ms sp rs -> + Val.lessdef v (rs'#(preg_of r)) -> + (forall r', important_preg r' = true /\ r' <> ST0 -> r' <> preg_of r -> rs'#r' = rs#r') -> + agree (Regmap.set r v (undef_move ms)) sp rs'. +Proof. + intros. apply agree_set_mreg with (rs'#(preg_of r) <- (rs#(preg_of r))); auto. + eapply agree_undef_move; eauto. + intros. unfold Pregmap.set. destruct (PregEq.eq r0 (preg_of r)). + congruence. auto. + intros. rewrite Pregmap.gso; auto. +Qed. + (** Useful properties of the PC register. *) Lemma nextinstr_inv: @@ -499,7 +532,7 @@ Lemma mk_mov_correct: exists rs2, exec_straight c rs1 m k rs2 m /\ rs2#rd = rs1#rs - /\ forall r, important_preg r = true -> r <> rd -> rs2#r = rs1#r. + /\ forall r, important_preg r = true -> r <> ST0 -> r <> rd -> rs2#r = rs1#r. Proof. unfold mk_mov; intros. destruct rd; try (monadInv H); destruct rs; monadInv H. @@ -513,8 +546,10 @@ Proof. intros. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gso. auto. (* getfp0 *) econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gso; auto. + split. rewrite nextinstr_inv; auto with ppcgen. + rewrite Pregmap.gso; auto with ppcgen. + apply Pregmap.gss. + intros. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gso; auto. rewrite Pregmap.gso; auto. (* setfp0 *) econstructor. split. apply exec_straight_one. simpl. eauto. auto. split. auto. @@ -846,7 +881,7 @@ Proof. change (rs2 ECX) with (rs1 r). rewrite H0. eauto. intros. unfold rs2. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gso; auto with ppcgen. auto. auto. - intros. repeat SOther. unfold rs2. repeat SOther. + intros. rewrite dec_eq_false. repeat SOther. unfold rs2. repeat SOther. congruence. Qed. (** Accessing slots in the stack frame *) @@ -887,7 +922,7 @@ Lemma storeind_correct: Mem.storev (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) (rs#(preg_of src)) = Some m' -> exists rs', exec_straight c rs m k rs' m' - /\ forall r, important_preg r = true -> rs'#r = rs#r. + /\ forall r, important_preg r = true -> r <> ST0 -> rs'#r = rs#r. Proof. unfold storeind; intros. set (addr := Addrmode (Some base) None (inl (ident * int) ofs)) in *. @@ -907,7 +942,7 @@ Proof. intros. apply nextinstr_nf_inv1; auto. econstructor; split. apply exec_straight_one. simpl. unfold exec_store. rewrite H1; rewrite H0. eauto. auto. - intros. apply nextinstr_nf_inv1; auto. + intros. rewrite nextinstr_nf_inv1; auto. rewrite dec_eq_true. apply Pregmap.gso; auto. Qed. (** Translation of addressing modes *) @@ -1463,7 +1498,7 @@ Lemma transl_op_correct: exec_straight c rs m k rs' m /\ rs'#(preg_of res) = v /\ forall r, - match op with Omove => important_preg r = true | _ => nontemp_preg r = true end -> + match op with Omove => important_preg r = true /\ r <> ST0 | _ => nontemp_preg r = true end -> r <> preg_of res -> rs' r = rs r. Proof. intros until v; intros TR EV. @@ -1471,7 +1506,7 @@ Proof. destruct op; simpl in TR; ArgsInv; try (TranslOp; fail). (* move *) exploit mk_mov_correct; eauto. intros [rs2 [A [B C]]]. - exists rs2. split. eauto. split. simpl. auto. auto. + exists rs2. split. eauto. split. simpl. auto. intros. destruct H; auto. (* cast8signed *) eapply mk_intconv_correct; eauto. (* cast8unsigned *) diff --git a/ia32/standard/Conventions1.v b/ia32/standard/Conventions1.v index 781617e7..49f5da92 100644 --- a/ia32/standard/Conventions1.v +++ b/ia32/standard/Conventions1.v @@ -42,15 +42,22 @@ Definition float_callee_save_regs : list mreg := nil. Definition destroyed_at_call_regs := int_caller_save_regs ++ float_caller_save_regs. -Definition destroyed_at_call := - List.map R destroyed_at_call_regs. +Definition destroyed_at_call := List.map R destroyed_at_call_regs. Definition int_temporaries := IT1 :: IT2 :: nil. -Definition float_temporaries := FT1 :: FT2 :: FP0 :: nil. +Definition float_temporaries := FT1 :: FT2 :: nil. + +(** [FP0] is not used for reloading, hence it is not in [float_temporaries], + however it is not allocatable, hence it is in [temporaries]. *) -Definition temporaries := - R IT1 :: R IT2 :: R FT1 :: R FT2 :: R FP0 :: nil. +Definition temporary_regs := IT1 :: IT2 :: FT1 :: FT2 :: FP0 :: nil. + +Definition temporaries := List.map R temporary_regs. + +Definition destroyed_at_move_regs := FP0 :: nil. + +Definition destroyed_at_move := List.map R destroyed_at_move_regs. Definition dummy_int_reg := AX. (**r Used in [Coloring]. *) Definition dummy_float_reg := X0. (**r Used in [Coloring]. *) -- cgit