From 0f5087bea45be49e105727d6cee4194598474fee Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 5 Jul 2011 04:13:33 +0000 Subject: Back from Oregon commit. powerpc/*: better compilation of some comparisons; revised asmgenproof1. common/*: added Mem.storebytes; used to give semantics to memcpy builtin. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1679 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/Asmgenproof1.v | 948 +++++++++++++++++++++++-------------------------- 1 file changed, 441 insertions(+), 507 deletions(-) (limited to 'powerpc/Asmgenproof1.v') diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 55a74be1..42355ad0 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -115,58 +115,90 @@ Qed. (** Characterization of PPC registers that correspond to Mach registers. *) -Definition is_data_reg (r: preg) : Prop := +Definition is_data_reg (r: preg) : bool := match r with - | IR GPR0 => False - | PC => False | LR => False | CTR => False - | CR0_0 => False | CR0_1 => False | CR0_2 => False | CR0_3 => False - | CARRY => False - | _ => True + | IR GPR0 => false + | PC => false | LR => false | CTR => false + | CR0_0 => false | CR0_1 => false | CR0_2 => false | CR0_3 => false + | CARRY => false + | _ => true end. Lemma ireg_of_is_data_reg: - forall (r: mreg), is_data_reg (ireg_of r). + forall (r: mreg), is_data_reg (ireg_of r) = true. Proof. - destruct r; exact I. + destruct r; reflexivity. Qed. Lemma freg_of_is_data_reg: - forall (r: mreg), is_data_reg (ireg_of r). + forall (r: mreg), is_data_reg (ireg_of r) = true. Proof. - destruct r; exact I. + destruct r; reflexivity. Qed. Lemma preg_of_is_data_reg: - forall (r: mreg), is_data_reg (preg_of r). + forall (r: mreg), is_data_reg (preg_of r) = true. Proof. - destruct r; exact I. + destruct r; reflexivity. Qed. -Lemma ireg_of_not_GPR1: - forall r, ireg_of r <> GPR1. +Lemma data_reg_diff: + forall r r', is_data_reg r = true -> is_data_reg r' = false -> r <> r'. Proof. - intro. case r; discriminate. + intros. congruence. Qed. -Lemma ireg_of_not_GPR0: - forall r, ireg_of r <> GPR0. + +Lemma ireg_diff: + forall r r', r <> r' -> IR r <> IR r'. Proof. - intro. case r; discriminate. + intros. congruence. +Qed. + +Lemma diff_ireg: + forall r r', IR r <> IR r' -> r <> r'. +Proof. + intros. congruence. +Qed. + +Hint Resolve ireg_of_is_data_reg freg_of_is_data_reg preg_of_is_data_reg + data_reg_diff ireg_diff diff_ireg: ppcgen. + +Definition is_nontemp_reg (r: preg) : bool := + match r with + | IR GPR0 => false | IR GPR11 => false | IR GPR12 => false + | FR FPR0 => false | FR FPR12 => false | FR FPR13 => false + | PC => false | LR => false | CTR => false + | CR0_0 => false | CR0_1 => false | CR0_2 => false | CR0_3 => false + | CARRY => false + | _ => true + end. + +Remark is_nontemp_is_data: + forall r, is_nontemp_reg r = true -> is_data_reg r = true. +Proof. + destruct r; simpl; try congruence. destruct i; congruence. +Qed. + +Lemma nontemp_reg_diff: + forall r r', is_nontemp_reg r = true -> is_nontemp_reg r' = false -> r <> r'. +Proof. + intros. congruence. Qed. -Hint Resolve ireg_of_not_GPR1 ireg_of_not_GPR0: ppcgen. -Lemma preg_of_not: - forall r1 r2, ~(is_data_reg r2) -> preg_of r1 <> r2. +Hint Resolve is_nontemp_is_data nontemp_reg_diff: ppcgen. + +Lemma ireg_of_not_GPR1: + forall r, ireg_of r <> GPR1. Proof. - intros; red; intro. subst r2. elim H. apply preg_of_is_data_reg. + intro. case r; discriminate. Qed. -Hint Resolve preg_of_not: ppcgen. Lemma preg_of_not_GPR1: forall r, preg_of r <> GPR1. Proof. intro. case r; discriminate. Qed. -Hint Resolve preg_of_not_GPR1: ppcgen. +Hint Resolve ireg_of_not_GPR1 preg_of_not_GPR1: ppcgen. Lemma int_temp_for_diff: forall r, IR(int_temp_for r) <> preg_of r. @@ -229,79 +261,63 @@ Proof. intros. elim H; auto. Qed. -Lemma agree_exten_1: +Lemma agree_exten: forall ms sp rs rs', agree ms sp rs -> - (forall r, is_data_reg r -> rs'#r = rs#r) -> + (forall r, is_data_reg r = true -> rs'#r = rs#r) -> agree ms sp rs'. Proof. - intros. inv H. constructor. - apply H0. exact I. - auto. - intros. rewrite H0. auto. apply preg_of_is_data_reg. -Qed. - -Lemma agree_exten_2: - forall ms sp rs rs', - agree ms sp rs -> - (forall r, - r <> IR GPR0 -> - r <> PC -> r <> LR -> r <> CTR -> - r <> CR0_0 -> r <> CR0_1 -> r <> CR0_2 -> r <> CR0_3 -> - r <> CARRY -> - rs'#r = rs#r) -> - agree ms sp rs'. -Proof. - intros. apply agree_exten_1 with rs. auto. - intros. apply H0; (red; intro; subst r; elim H1). + intros. inv H. constructor; auto. + intros. rewrite H0; auto with ppcgen. Qed. (** Preservation of register agreement under various assignments. *) Lemma agree_set_mreg: - forall ms sp rs r v v', + forall ms sp rs r v rs', agree ms sp rs -> - Val.lessdef v v' -> - agree (Regmap.set r v ms) sp (rs#(preg_of r) <- v'). + Val.lessdef v (rs'#(preg_of r)) -> + (forall r', is_data_reg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') -> + agree (Regmap.set r v ms) sp rs'. Proof. - intros. inv H. constructor. - rewrite Pregmap.gso. auto. apply sym_not_eq. apply preg_of_not_GPR1. - auto. - intros. unfold Regmap.set. case (RegEq.eq r0 r); intro. - subst r0. rewrite Pregmap.gss. auto. - rewrite Pregmap.gso. auto. red; intro. - elim n. apply preg_of_injective; auto. + intros. inv H. constructor; auto with ppcgen. + intros. unfold Regmap.set. destruct (RegEq.eq r0 r). + subst r0. auto. + rewrite H1; auto with ppcgen. red; intros; elim n; apply preg_of_injective; auto. Qed. Hint Resolve agree_set_mreg: ppcgen. Lemma agree_set_mireg: - forall ms sp rs r v, - agree ms sp (rs#(preg_of r) <- v) -> + forall ms sp rs r v (rs': regset), + agree ms sp rs -> + Val.lessdef v (rs'#(ireg_of r)) -> mreg_type r = Tint -> - agree ms sp (rs#(ireg_of r) <- v). + (forall r', is_data_reg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') -> + agree (Regmap.set r v ms) sp rs'. Proof. - intros. unfold preg_of in H. rewrite H0 in H. auto. + intros. eapply agree_set_mreg; eauto. unfold preg_of; rewrite H1; auto. Qed. Hint Resolve agree_set_mireg: ppcgen. Lemma agree_set_mfreg: - forall ms sp rs r v, - agree ms sp (rs#(preg_of r) <- v) -> + forall ms sp rs r v (rs': regset), + agree ms sp rs -> + Val.lessdef v (rs'#(freg_of r)) -> mreg_type r = Tfloat -> - agree ms sp (rs#(freg_of r) <- v). + (forall r', is_data_reg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') -> + agree (Regmap.set r v ms) sp rs'. Proof. - intros. unfold preg_of in H. rewrite H0 in H. auto. + intros. eapply agree_set_mreg; eauto. unfold preg_of; rewrite H1; auto. Qed. -Hint Resolve agree_set_mfreg: ppcgen. Lemma agree_set_other: forall ms sp rs r v, agree ms sp rs -> - ~(is_data_reg r) -> + is_data_reg r = false -> agree ms sp (rs#r <- v). Proof. - intros. apply agree_exten_1 with rs. - auto. intros. apply Pregmap.gso. red; intro; subst r0; contradiction. + intros. apply agree_exten with rs. + auto. intros. apply Pregmap.gso. congruence. Qed. Hint Resolve agree_set_other: ppcgen. @@ -313,24 +329,49 @@ Proof. Qed. Hint Resolve agree_nextinstr: ppcgen. -Lemma agree_set_mireg_twice: - forall ms sp rs r v v' v1, +Lemma agree_undef_regs: + forall rl ms sp rs rs', agree ms sp rs -> - mreg_type r = Tint -> - Val.lessdef v v' -> - agree (Regmap.set r v ms) sp (rs #(ireg_of r) <- v1 #(ireg_of r) <- v'). -Proof. - intros. replace (IR (ireg_of r)) with (preg_of r). inv H. - split. repeat (rewrite Pregmap.gso; auto with ppcgen). auto. - intros. case (mreg_eq r r0); intro. - subst r0. rewrite Regmap.gss. rewrite Pregmap.gss. auto. - assert (preg_of r <> preg_of r0). - red; intro. elim n. apply preg_of_injective. auto. - rewrite Regmap.gso; auto. - repeat (rewrite Pregmap.gso; auto). - unfold preg_of. rewrite H0. auto. + (forall r, is_data_reg r = true -> ~In r (List.map preg_of rl) -> rs'#r = rs#r) -> + agree (undef_regs rl ms) sp rs'. +Proof. + induction rl; simpl; intros. + apply agree_exten with rs; auto. + apply IHrl with (rs#(preg_of a) <- (rs'#(preg_of a))). + apply agree_set_mreg with rs; auto with ppcgen. + intros. unfold Pregmap.set. destruct (PregEq.eq r' (preg_of a)). + congruence. auto. + intros. unfold Pregmap.set. destruct (PregEq.eq r (preg_of a)). + congruence. apply H0; auto. intuition congruence. +Qed. + +Lemma agree_undef_temps: + forall ms sp rs rs', + agree ms sp rs -> + (forall r, is_nontemp_reg r = true -> rs'#r = rs#r) -> + agree (undef_temps ms) sp rs'. +Proof. + unfold undef_temps. intros. apply agree_undef_regs with rs; auto. + simpl. unfold preg_of; simpl. intros. intuition. + apply H0. destruct r; simpl in *; auto. + destruct i; intuition. destruct f; intuition. +Qed. +Hint Resolve agree_undef_temps: ppcgen. + +Lemma agree_set_mreg_undef_temps: + forall ms sp rs r v rs', + agree ms sp rs -> + Val.lessdef v (rs'#(preg_of r)) -> + (forall r', is_nontemp_reg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') -> + agree (Regmap.set r v (undef_temps ms)) sp rs'. +Proof. + intros. apply agree_set_mreg with (rs'#(preg_of r) <- (rs#(preg_of r))). + apply agree_undef_temps with rs; auto. + intros. unfold Pregmap.set. destruct (PregEq.eq r0 (preg_of r)). + congruence. apply H1; auto. + auto. + intros. rewrite Pregmap.gso; auto. Qed. -Hint Resolve agree_set_mireg_twice: ppcgen. Lemma agree_set_twice_mireg: forall ms sp rs r v v1 v', @@ -353,101 +394,6 @@ Proof. red; intros. elim n. apply preg_of_injective; auto. unfold preg_of. rewrite H0. auto. Qed. -Hint Resolve agree_set_twice_mireg: ppcgen. - -Lemma agree_set_commut: - forall ms sp rs r1 r2 v1 v2, - r1 <> r2 -> - agree ms sp ((rs#r2 <- v2)#r1 <- v1) -> - agree ms sp ((rs#r1 <- v1)#r2 <- v2). -Proof. - intros. apply agree_exten_1 with ((rs#r2 <- v2)#r1 <- v1). auto. - intros. - case (preg_eq r r1); intro. - subst r1. rewrite Pregmap.gss. rewrite Pregmap.gso. rewrite Pregmap.gss. - auto. auto. - case (preg_eq r r2); intro. - subst r2. rewrite Pregmap.gss. rewrite Pregmap.gso. rewrite Pregmap.gss. - auto. auto. - repeat (rewrite Pregmap.gso; auto). -Qed. -Hint Resolve agree_set_commut: ppcgen. - -Lemma agree_nextinstr_commut: - forall ms sp rs r v, - agree ms sp (rs#r <- v) -> - r <> PC -> - agree ms sp ((nextinstr rs)#r <- v). -Proof. - intros. unfold nextinstr. apply agree_set_commut. auto. - apply agree_set_other. auto. auto. -Qed. -Hint Resolve agree_nextinstr_commut: ppcgen. - -Lemma agree_set_mireg_exten: - forall ms sp rs r v (rs': regset), - agree ms sp rs -> - mreg_type r = Tint -> - Val.lessdef v rs'#(ireg_of r) -> - (forall r', - r' <> IR GPR0 -> - r' <> PC -> r' <> LR -> r' <> CTR -> - r' <> CR0_0 -> r' <> CR0_1 -> r' <> CR0_2 -> r' <> CR0_3 -> - r' <> CARRY -> - r' <> IR (ireg_of r) -> rs'#r' = rs#r') -> - agree (Regmap.set r v ms) sp rs'. -Proof. - intros. set (v' := rs'#(ireg_of r)). - apply agree_exten_2 with (rs#(ireg_of r) <- v'). - auto with ppcgen. - intros. unfold Pregmap.set. case (PregEq.eq r0 (ireg_of r)); intro. - subst r0. auto. apply H2; auto. -Qed. -Hint Resolve agree_set_mireg_exten: ppcgen. - -Lemma agree_undef_regs: - forall rl ms sp rs rs', - agree ms sp rs -> - (forall r, is_data_reg r -> ~In r (List.map preg_of rl) -> rs'#r = rs#r) -> - agree (undef_regs rl ms) sp rs'. -Proof. - induction rl; simpl; intros. - apply agree_exten_1 with rs; auto. - apply IHrl with (rs#(preg_of a) <- (rs'#(preg_of a))). - apply agree_set_mreg; auto. - intros. unfold Pregmap.set. - destruct (PregEq.eq r (preg_of a)). - congruence. - apply H0. auto. intuition congruence. -Qed. - -Lemma agree_undef_temps: - forall ms sp rs rs', - agree ms sp rs -> - (forall r, - r <> IR GPR0 -> - r <> PC -> r <> LR -> r <> CTR -> - r <> CR0_0 -> r <> CR0_1 -> r <> CR0_2 -> r <> CR0_3 -> - r <> CARRY -> - r <> IR GPR11 -> r <> IR GPR12 -> - r <> FR FPR0 -> r <> FR FPR12 -> r <> FR FPR13 -> - rs'#r = rs#r) -> - agree (undef_temps ms) sp rs'. -Proof. - unfold undef_temps. intros. apply agree_undef_regs with rs; auto. - simpl. unfold preg_of; simpl. intros. - apply H0; (red; intro; subst; simpl in H1; intuition congruence). -Qed. -Hint Resolve agree_undef_temps: ppcgen. - -Lemma agree_undef_temps_2: - forall ms sp rs, - agree ms sp rs -> - agree (undef_temps ms) sp rs. -Proof. - intros. apply agree_undef_temps with rs; auto. -Qed. -Hint Resolve agree_undef_temps_2: ppcgen. (** Useful properties of the PC and GPR0 registers. *) @@ -458,15 +404,6 @@ Proof. Qed. Hint Resolve nextinstr_inv: ppcgen. -Lemma nextinstr_set_preg: - forall rs m v, - (nextinstr (rs#(preg_of m) <- v))#PC = Val.add rs#PC Vone. -Proof. - intros. unfold nextinstr. rewrite Pregmap.gss. - rewrite Pregmap.gso. auto. apply sym_not_eq. auto with ppcgen. -Qed. -Hint Resolve nextinstr_set_preg: ppcgen. - Lemma gpr_or_zero_not_zero: forall rs r, r <> GPR0 -> gpr_or_zero rs r = rs#r. Proof. @@ -622,6 +559,19 @@ Qed. (** * Correctness of PowerPC constructor functions *) +(* +Ltac SIMP := + match goal with + | [ |- nextinstr _ _ = _ ] => rewrite nextinstr_inv; [auto | auto with ppcgen] + | [ |- Pregmap.get ?x (Pregmap.set ?x _ _) = _ ] => rewrite Pregmap.gss; auto + | [ |- Pregmap.set ?x _ _ ?x = _ ] => rewrite Pregmap.gss; auto + | [ |- Pregmap.get _ (Pregmap.set _ _ _) = _ ] => rewrite Pregmap.gso; [auto | auto with ppcgen] + | [ |- Pregmap.set _ _ _ _ = _ ] => rewrite Pregmap.gso; [auto | auto with ppcgen] + end. +*) +Ltac SIMP := + (rewrite nextinstr_inv || rewrite Pregmap.gss || rewrite Pregmap.gso); auto with ppcgen. + (** Properties of comparisons. *) Lemma compare_float_spec: @@ -630,15 +580,13 @@ Lemma compare_float_spec: rs1#CR0_0 = Val.cmpf Clt v1 v2 /\ rs1#CR0_1 = Val.cmpf Cgt v1 v2 /\ rs1#CR0_2 = Val.cmpf Ceq v1 v2 - /\ forall r', r' <> PC -> r' <> CR0_0 -> r' <> CR0_1 -> - r' <> CR0_2 -> r' <> CR0_3 -> rs1#r' = rs#r'. + /\ forall r', r' <> CR0_0 -> r' <> CR0_1 -> r' <> CR0_2 -> r' <> CR0_3 -> r' <> PC -> rs1#r' = rs#r'. Proof. intros. unfold rs1. split. reflexivity. split. reflexivity. split. reflexivity. - intros. rewrite nextinstr_inv; auto. - unfold compare_float. repeat (rewrite Pregmap.gso; auto). + intros. unfold compare_float. repeat SIMP. Qed. Lemma compare_sint_spec: @@ -647,15 +595,13 @@ Lemma compare_sint_spec: rs1#CR0_0 = Val.cmp Clt v1 v2 /\ rs1#CR0_1 = Val.cmp Cgt v1 v2 /\ rs1#CR0_2 = Val.cmp Ceq v1 v2 - /\ forall r', r' <> PC -> r' <> CR0_0 -> r' <> CR0_1 -> - r' <> CR0_2 -> r' <> CR0_3 -> rs1#r' = rs#r'. + /\ forall r', r' <> CR0_0 -> r' <> CR0_1 -> r' <> CR0_2 -> r' <> CR0_3 -> r' <> PC -> rs1#r' = rs#r'. Proof. intros. unfold rs1. split. reflexivity. split. reflexivity. split. reflexivity. - intros. rewrite nextinstr_inv; auto. - unfold compare_sint. repeat (rewrite Pregmap.gso; auto). + intros. unfold compare_sint. repeat SIMP. Qed. Lemma compare_uint_spec: @@ -664,15 +610,13 @@ Lemma compare_uint_spec: rs1#CR0_0 = Val.cmpu Clt v1 v2 /\ rs1#CR0_1 = Val.cmpu Cgt v1 v2 /\ rs1#CR0_2 = Val.cmpu Ceq v1 v2 - /\ forall r', r' <> PC -> r' <> CR0_0 -> r' <> CR0_1 -> - r' <> CR0_2 -> r' <> CR0_3 -> rs1#r' = rs#r'. + /\ forall r', r' <> CR0_0 -> r' <> CR0_1 -> r' <> CR0_2 -> r' <> CR0_3 -> r' <> PC -> rs1#r' = rs#r'. Proof. intros. unfold rs1. split. reflexivity. split. reflexivity. split. reflexivity. - intros. rewrite nextinstr_inv; auto. - unfold compare_uint. repeat (rewrite Pregmap.gso; auto). + intros. unfold compare_uint. repeat SIMP. Qed. (** Loading a constant. *) @@ -689,11 +633,9 @@ Proof. (* addi *) exists (nextinstr (rs#r <- (Vint n))). split. apply exec_straight_one. - simpl. rewrite Int.add_commut. rewrite Int.add_zero. reflexivity. + simpl. rewrite Int.add_zero_l. auto. reflexivity. - split. rewrite nextinstr_inv; auto with ppcgen. - apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + split. repeat SIMP. intros; repeat SIMP. (* addis *) generalize (Int.eq_spec (low_s n) Int.zero); case (Int.eq (low_s n) Int.zero); intro. exists (nextinstr (rs#r <- (Vint n))). @@ -701,19 +643,16 @@ Proof. simpl. rewrite Int.add_commut. rewrite <- H. rewrite low_high_s. reflexivity. reflexivity. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + split. repeat SIMP. intros; repeat SIMP. (* addis + ori *) pose (rs1 := nextinstr (rs#r <- (Vint (Int.shl (high_u n) (Int.repr 16))))). exists (nextinstr (rs1#r <- (Vint n))). split. eapply exec_straight_two. - simpl. rewrite Int.add_commut. rewrite Int.add_zero. reflexivity. + simpl. rewrite Int.add_zero_l. reflexivity. simpl. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. unfold Val.or. rewrite low_high_u. reflexivity. reflexivity. reflexivity. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. - unfold rs1. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. + unfold rs1. split. repeat SIMP. intros; repeat SIMP. Qed. (** Add integer immediate. *) @@ -734,8 +673,7 @@ Proof. split. apply exec_straight_one. simpl. rewrite gpr_or_zero_not_zero; auto. reflexivity. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + split. repeat SIMP. intros. repeat SIMP. (* addis *) generalize (Int.eq_spec (low_s n) Int.zero); case (Int.eq (low_s n) Int.zero); intro. exists (nextinstr (rs#r1 <- (Val.add rs#r2 (Vint n)))). @@ -744,8 +682,7 @@ Proof. generalize (low_high_s n). rewrite H1. rewrite Int.add_zero. intro. rewrite H2. auto. reflexivity. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + split. repeat SIMP. intros; repeat SIMP. (* addis + addi *) pose (rs1 := nextinstr (rs#r1 <- (Val.add rs#r2 (Vint (Int.shl (high_s n) (Int.repr 16)))))). exists (nextinstr (rs1#r1 <- (Val.add rs#r2 (Vint n)))). @@ -755,9 +692,7 @@ Proof. unfold rs1 at 1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. rewrite Val.add_assoc. simpl. rewrite low_high_s. auto. reflexivity. reflexivity. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. - unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + unfold rs1; split. repeat SIMP. intros; repeat SIMP. Qed. (** And integer immediate. *) @@ -770,10 +705,7 @@ Lemma andimm_correct: exec_straight (andimm r1 r2 n k) rs m k rs' m /\ rs'#r1 = v /\ rs'#CR0_2 = Val.cmp Ceq v Vzero - /\ forall r': preg, - r' <> r1 -> r' <> GPR0 -> r' <> PC -> - r' <> CR0_0 -> r' <> CR0_1 -> r' <> CR0_2 -> r' <> CR0_3 -> - rs'#r' = rs#r'. + /\ forall r', is_data_reg r' = true -> r' <> r1 -> rs'#r' = rs#r'. Proof. intros. unfold andimm. case (Int.eq (high_u n) Int.zero). @@ -782,9 +714,9 @@ Proof. generalize (compare_sint_spec (rs#r1 <- v) v Vzero). intros [A [B [C D]]]. split. apply exec_straight_one. reflexivity. reflexivity. - split. rewrite D; try discriminate. apply Pregmap.gss. + split. rewrite D; auto with ppcgen. SIMP. split. auto. - intros. rewrite D; auto. apply Pregmap.gso; auto. + intros. rewrite D; auto with ppcgen. SIMP. (* andis *) generalize (Int.eq_spec (low_u n) Int.zero); case (Int.eq (low_u n) Int.zero); intro. @@ -794,9 +726,9 @@ Proof. split. apply exec_straight_one. simpl. generalize (low_high_u n). rewrite H0. rewrite Int.or_zero. intro. rewrite H1. reflexivity. reflexivity. - split. rewrite D; try discriminate. apply Pregmap.gss. + split. rewrite D; auto with ppcgen. SIMP. split. auto. - intros. rewrite D; auto. apply Pregmap.gso; auto. + intros. rewrite D; auto with ppcgen. SIMP. (* loadimm + and *) generalize (loadimm_correct GPR0 n (Pand_ r1 r2 GPR0 :: k) rs m). intros [rs1 [EX1 [RES1 OTHER1]]]. @@ -807,9 +739,9 @@ Proof. apply exec_straight_one. simpl. rewrite RES1. rewrite (OTHER1 r2). reflexivity. congruence. congruence. reflexivity. - split. rewrite D; try discriminate. apply Pregmap.gss. + split. rewrite D; auto with ppcgen. SIMP. split. auto. - intros. rewrite D; auto. rewrite Pregmap.gso; auto. + intros. rewrite D; auto with ppcgen. SIMP. Qed. (** Or integer immediate. *) @@ -827,8 +759,8 @@ Proof. (* ori *) exists (nextinstr (rs#r1 <- v)). split. apply exec_straight_one. reflexivity. reflexivity. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + split. repeat SIMP. + intros. repeat SIMP. (* oris *) generalize (Int.eq_spec (low_u n) Int.zero); case (Int.eq (low_u n) Int.zero); intro. @@ -836,19 +768,12 @@ Proof. split. apply exec_straight_one. simpl. generalize (low_high_u n). rewrite H. rewrite Int.or_zero. intro. rewrite H0. reflexivity. reflexivity. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + split. repeat SIMP. + intros. repeat SIMP. (* oris + ori *) - pose (rs1 := nextinstr (rs#r1 <- (Val.or rs#r2 (Vint (Int.shl (high_u n) (Int.repr 16)))))). - exists (nextinstr (rs1#r1 <- v)). - split. apply exec_straight_two with rs1 m. - reflexivity. simpl. unfold rs1 at 1. - rewrite nextinstr_inv; auto with ppcgen. - rewrite Pregmap.gss. rewrite Val.or_assoc. simpl. - rewrite low_high_u. reflexivity. reflexivity. reflexivity. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. - unfold rs1. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. + econstructor; split. eapply exec_straight_two; simpl; reflexivity. + split. repeat rewrite nextinstr_inv; auto with ppcgen. repeat rewrite Pregmap.gss. rewrite Val.or_assoc. simpl. rewrite low_high_u. reflexivity. + intros. repeat SIMP. Qed. (** Xor integer immediate. *) @@ -866,8 +791,7 @@ Proof. (* xori *) exists (nextinstr (rs#r1 <- v)). split. apply exec_straight_one. reflexivity. reflexivity. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + split. repeat SIMP. intros. repeat SIMP. (* xoris *) generalize (Int.eq_spec (low_u n) Int.zero); case (Int.eq (low_u n) Int.zero); intro. @@ -875,20 +799,12 @@ Proof. split. apply exec_straight_one. simpl. generalize (low_high_u_xor n). rewrite H. rewrite Int.xor_zero. intro. rewrite H0. reflexivity. reflexivity. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + split. repeat SIMP. intros. repeat SIMP. (* xoris + xori *) - pose (rs1 := nextinstr (rs#r1 <- (Val.xor rs#r2 (Vint (Int.shl (high_u n) (Int.repr 16)))))). - exists (nextinstr (rs1#r1 <- v)). - split. apply exec_straight_two with rs1 m. - reflexivity. simpl. unfold rs1 at 1. - rewrite nextinstr_inv; try discriminate. - rewrite Pregmap.gss. rewrite Val.xor_assoc. simpl. - rewrite low_high_u_xor. reflexivity. reflexivity. reflexivity. - split. rewrite nextinstr_inv; auto with ppcgen. - apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. - unfold rs1. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. + econstructor; split. eapply exec_straight_two; simpl; reflexivity. + split. repeat rewrite nextinstr_inv; auto with ppcgen. repeat rewrite Pregmap.gss. + rewrite Val.xor_assoc. simpl. rewrite low_high_u_xor. reflexivity. + intros. repeat SIMP. Qed. (** Indexed memory loads. *) @@ -906,24 +822,23 @@ Proof. intros. unfold loadind. destruct (Int.eq (high_s ofs) Int.zero). (* one load *) exists (nextinstr (rs#(preg_of dst) <- v)); split. + unfold preg_of. rewrite H0. destruct ty; apply exec_straight_one; auto with ppcgen; simpl. unfold load1. rewrite gpr_or_zero_not_zero; auto. - simpl in *. rewrite H. unfold preg_of; rewrite H0. auto. + simpl in *. rewrite H. auto. unfold load1. rewrite gpr_or_zero_not_zero; auto. - simpl in *. rewrite H. unfold preg_of; rewrite H0. auto. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + simpl in *. rewrite H. auto. + split. repeat SIMP. intros. repeat SIMP. (* loadimm + one load *) exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [A [B C]]]. exists (nextinstr (rs'#(preg_of dst) <- v)); split. eapply exec_straight_trans. eexact A. + unfold preg_of. rewrite H0. destruct ty; apply exec_straight_one; auto with ppcgen; simpl. - unfold load2. rewrite B. rewrite C; auto with ppcgen. simpl in H. rewrite H. - unfold preg_of; rewrite H0. auto. congruence. - unfold load2. rewrite B. rewrite C; auto with ppcgen. simpl in H. rewrite H. - unfold preg_of; rewrite H0. auto. congruence. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. + unfold load2. rewrite B. rewrite C; auto with ppcgen. simpl in H. rewrite H. auto. + unfold load2. rewrite B. rewrite C; auto with ppcgen. simpl in H. rewrite H. auto. + split. repeat SIMP. + intros. repeat SIMP. Qed. (** Indexed memory stores. *) @@ -948,7 +863,7 @@ Proof. intros. apply nextinstr_inv; auto. (* loadimm + one store *) exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [A [B C]]]. - assert (rs' base = rs base). apply C; auto with ppcgen. congruence. + assert (rs' base = rs base). apply C; auto with ppcgen. assert (rs' (preg_of src) = rs (preg_of src)). apply C; auto with ppcgen. exists (nextinstr rs'). split. eapply exec_straight_trans. eexact A. @@ -1035,17 +950,16 @@ Ltac UseTypeInfo := (** Translation of conditions. *) -Lemma transl_cond_correct_aux: - forall cond args k ms sp rs m, +Lemma transl_cond_correct_1: + forall cond args k rs m, map mreg_type args = type_of_condition cond -> - agree ms sp rs -> exists rs', exec_straight (transl_cond cond args k) rs m k rs' m /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) = (if snd (crbit_for_cond cond) then eval_condition_total cond (map rs (map preg_of args)) else Val.notbool (eval_condition_total cond (map rs (map preg_of args)))) - /\ agree ms sp rs'. + /\ forall r, is_data_reg r = true -> rs'#r = rs#r. Proof. intros. destruct cond; simpl in H; TypeInv; simpl; UseTypeInfo. @@ -1056,7 +970,7 @@ Proof. apply exec_straight_one. simpl; reflexivity. reflexivity. split. case c; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto. - apply agree_exten_2 with rs; auto. + auto with ppcgen. (* Ccompu *) destruct (compare_uint_spec rs (rs (ireg_of m0)) (rs (ireg_of m1))) as [A [B [C D]]]. @@ -1064,7 +978,7 @@ Proof. apply exec_straight_one. simpl; reflexivity. reflexivity. split. case c; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto. - apply agree_exten_2 with rs; auto. + auto with ppcgen. (* Ccompimm *) case (Int.eq (high_s i) Int.zero). destruct (compare_sint_spec rs (rs (ireg_of m0)) (Vint i)) @@ -1073,21 +987,20 @@ Proof. apply exec_straight_one. simpl. eauto. reflexivity. split. case c; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto. - apply agree_exten_2 with rs; auto. + auto with ppcgen. generalize (loadimm_correct GPR0 i (Pcmpw (ireg_of m0) GPR0 :: k) rs m). intros [rs1 [EX1 [RES1 OTH1]]]. destruct (compare_sint_spec rs1 (rs (ireg_of m0)) (Vint i)) as [A [B [C D]]]. assert (rs1 (ireg_of m0) = rs (ireg_of m0)). - apply OTH1; auto with ppcgen. decEq. auto with ppcgen. + apply OTH1; auto with ppcgen. exists (nextinstr (compare_sint rs1 (rs1 (ireg_of m0)) (Vint i))). split. eapply exec_straight_trans. eexact EX1. apply exec_straight_one. simpl. rewrite RES1; rewrite H; auto. reflexivity. split. rewrite H. case c; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto. - apply agree_exten_2 with rs; auto. - intros. rewrite H; rewrite D; auto. + intros. rewrite H; rewrite D; auto with ppcgen. (* Ccompuimm *) case (Int.eq (high_u i) Int.zero). destruct (compare_uint_spec rs (rs (ireg_of m0)) (Vint i)) @@ -1096,27 +1009,25 @@ Proof. apply exec_straight_one. simpl. eauto. reflexivity. split. case c; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto. - apply agree_exten_2 with rs; auto. + auto with ppcgen. generalize (loadimm_correct GPR0 i (Pcmplw (ireg_of m0) GPR0 :: k) rs m). intros [rs1 [EX1 [RES1 OTH1]]]. destruct (compare_uint_spec rs1 (rs (ireg_of m0)) (Vint i)) as [A [B [C D]]]. - assert (rs1 (ireg_of m0) = rs (ireg_of m0)). - apply OTH1; auto with ppcgen. decEq. auto with ppcgen. + assert (rs1 (ireg_of m0) = rs (ireg_of m0)). apply OTH1; auto with ppcgen. exists (nextinstr (compare_uint rs1 (rs1 (ireg_of m0)) (Vint i))). split. eapply exec_straight_trans. eexact EX1. apply exec_straight_one. simpl. rewrite RES1; rewrite H; auto. reflexivity. split. rewrite H. case c; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto. - apply agree_exten_2 with rs; auto. - intros. rewrite H; rewrite D; auto. + intros. rewrite H; rewrite D; auto with ppcgen. (* Ccompf *) destruct (floatcomp_correct c (freg_of m0) (freg_of m1) k rs m) as [rs' [EX [RES OTH]]]. exists rs'. split. auto. split. apply RES. - apply agree_exten_2 with rs; auto. + auto with ppcgen. (* Cnotcompf *) destruct (floatcomp_correct c (freg_of m0) (freg_of m1) k rs m) as [rs' [EX [RES OTH]]]. @@ -1126,23 +1037,41 @@ Proof. intros v1 v2; unfold Val.cmpf; destruct v1; destruct v2; auto. apply Val.notbool_idem2. rewrite H. case (snd (crbit_for_fcmp c)); simpl; auto. - apply agree_exten_2 with rs; auto. + auto with ppcgen. (* Cmaskzero *) - destruct (andimm_correct GPR0 (ireg_of m0) i k rs m (ireg_of_not_GPR0 m0)) - as [rs' [A [B [C D]]]]. + destruct (andimm_correct GPR0 (ireg_of m0) i k rs m) + as [rs' [A [B [C D]]]]. auto with ppcgen. exists rs'. split. assumption. split. rewrite C. auto. - apply agree_exten_2 with rs; auto. + auto with ppcgen. (* Cmasknotzero *) - destruct (andimm_correct GPR0 (ireg_of m0) i k rs m (ireg_of_not_GPR0 m0)) - as [rs' [A [B [C D]]]]. + destruct (andimm_correct GPR0 (ireg_of m0) i k rs m) + as [rs' [A [B [C D]]]]. auto with ppcgen. exists rs'. split. assumption. split. rewrite C. rewrite Val.notbool_idem3. reflexivity. - apply agree_exten_2 with rs; auto. + auto with ppcgen. +Qed. + +Lemma transl_cond_correct_2: + forall cond args k rs m b, + map mreg_type args = type_of_condition cond -> + eval_condition cond (map rs (map preg_of args)) m = Some b -> + exists rs', + exec_straight (transl_cond cond args k) rs m k rs' m + /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) = + (if snd (crbit_for_cond cond) + then Val.of_bool b + else Val.notbool (Val.of_bool b)) + /\ forall r, is_data_reg r = true -> rs'#r = rs#r. +Proof. + intros. + assert (eval_condition_total cond rs ## (preg_of ## args) = Val.of_bool b). + apply eval_condition_weaken with m. auto. + rewrite <- H1. eapply transl_cond_correct_1; eauto. Qed. Lemma transl_cond_correct: - forall cond args k ms sp rs m m' b, + forall cond args k ms sp rs m b m', map mreg_type args = type_of_condition cond -> agree ms sp rs -> eval_condition cond (map ms args) m = Some b -> @@ -1156,10 +1085,121 @@ Lemma transl_cond_correct: /\ agree ms sp rs'. Proof. intros. - assert (eval_condition_total cond rs ## (preg_of ## args) = Val.of_bool b). - apply eval_condition_weaken with m'. eapply eval_condition_lessdef; eauto. - eapply preg_vals; eauto. - rewrite <- H3. eapply transl_cond_correct_aux; eauto. + exploit transl_cond_correct_2. eauto. + eapply eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. + intros [rs' [A [B C]]]. + exists rs'; split. eauto. split. auto. apply agree_exten with rs; auto. +Qed. + +(** Translation of condition operators *) + +Remark add_carry_eq0: + forall i, + Vint (Int.add (Int.add (Int.sub Int.zero i) i) + (Int.add_carry Int.zero (Int.xor i Int.mone) Int.one)) = + Val.of_bool (Int.eq i Int.zero). +Proof. + intros. rewrite <- Int.sub_add_l. rewrite Int.add_zero_l. + rewrite Int.sub_idem. rewrite Int.add_zero_l. fold (Int.not i). + predSpec Int.eq Int.eq_spec i Int.zero. + subst i. reflexivity. + unfold Val.of_bool, Vfalse. decEq. + unfold Int.add_carry. rewrite Int.unsigned_zero. rewrite Int.unsigned_one. + apply zlt_true. + generalize (Int.unsigned_range (Int.not i)); intro. + assert (Int.unsigned (Int.not i) <> Int.modulus - 1). + red; intros. + assert (Int.repr (Int.unsigned (Int.not i)) = Int.mone). + rewrite H1. apply Int.mkint_eq. reflexivity. + rewrite Int.repr_unsigned in H2. + assert (Int.not (Int.not i) = Int.zero). + rewrite H2. apply Int.mkint_eq; reflexivity. + rewrite Int.not_involutive in H3. + congruence. + omega. +Qed. + +Remark add_carry_ne0: + forall i, + Vint (Int.add (Int.add i (Int.xor (Int.add i Int.mone) Int.mone)) + (Int.add_carry i Int.mone Int.zero)) = + Val.of_bool (negb (Int.eq i Int.zero)). +Proof. + intros. fold (Int.not (Int.add i Int.mone)). rewrite Int.not_neg. + rewrite (Int.add_commut (Int.neg (Int.add i Int.mone))). + rewrite <- Int.sub_add_opp. rewrite Int.sub_add_r. rewrite Int.sub_idem. + rewrite Int.add_zero_l. rewrite Int.add_neg_zero. rewrite Int.add_zero_l. + unfold Int.add_carry, Int.eq. + rewrite Int.unsigned_zero. rewrite Int.unsigned_mone. + unfold negb, Val.of_bool, Vtrue, Vfalse. + destruct (zeq (Int.unsigned i) 0); decEq. + apply zlt_true. omega. + apply zlt_false. generalize (Int.unsigned_range i). omega. +Qed. + +Lemma transl_cond_op_correct: + forall cond args r k rs m b, + mreg_type r = Tint -> + map mreg_type args = type_of_condition cond -> + eval_condition cond (map rs (map preg_of args)) m = Some b -> + exists rs', + exec_straight (transl_cond_op cond args r k) rs m k rs' m + /\ rs'#(ireg_of r) = Val.of_bool b + /\ forall r', is_data_reg r' = true -> r' <> ireg_of r -> rs'#r' = rs#r'. +Proof. + intros until args. unfold transl_cond_op. + destruct (classify_condition cond args); + intros until b; intros TY1 TY2 EV; simpl in TY2. +(* eq 0 *) + inv TY2. simpl in EV. unfold preg_of in *; rewrite H0 in *. + econstructor; split. + eapply exec_straight_two; simpl; reflexivity. + split. repeat SIMP. destruct (rs (ireg_of r)); inv EV. simpl. + apply add_carry_eq0. + intros; repeat SIMP. +(* ne 0 *) + inv TY2. simpl in EV. unfold preg_of in *; rewrite H0 in *. + econstructor; split. + eapply exec_straight_two; simpl; reflexivity. + split. repeat SIMP. rewrite gpr_or_zero_not_zero; auto with ppcgen. + destruct (rs (ireg_of r)); inv EV. simpl. + apply add_carry_ne0. + intros; repeat SIMP. +(* ge 0 *) + inv TY2. simpl in EV. unfold preg_of in *; rewrite H0 in *. + econstructor; split. + eapply exec_straight_two; simpl; reflexivity. + split. repeat SIMP. rewrite Val.rolm_ge_zero. + destruct (rs (ireg_of r)); simpl; congruence. + intros; repeat SIMP. +(* lt 0 *) + inv TY2. simpl in EV. unfold preg_of in *; rewrite H0 in *. + econstructor; split. + apply exec_straight_one; simpl; reflexivity. + split. repeat SIMP. rewrite Val.rolm_lt_zero. + destruct (rs (ireg_of r)); simpl; congruence. + intros; repeat SIMP. +(* default *) + set (bit := fst (crbit_for_cond c)). + set (isset := snd (crbit_for_cond c)). + set (k1 := + Pmfcrbit (ireg_of r) bit :: + (if isset + then k + else Pxori (ireg_of r) (ireg_of r) (Cint Int.one) :: k)). + generalize (transl_cond_correct_2 c rl k1 rs m b TY2 EV). + fold bit; fold isset. + intros [rs1 [EX1 [RES1 AG1]]]. + destruct isset. + (* bit set *) + econstructor; split. eapply exec_straight_trans. eexact EX1. + unfold k1. apply exec_straight_one; simpl; reflexivity. + split. repeat SIMP. intros; repeat SIMP. + (* bit clear *) + econstructor; split. eapply exec_straight_trans. eexact EX1. + unfold k1. eapply exec_straight_two; simpl; reflexivity. + split. repeat SIMP. rewrite RES1. destruct b; compute; reflexivity. + intros; repeat SIMP. Qed. (** Translation of arithmetic operations. *) @@ -1167,255 +1207,143 @@ Qed. Ltac TranslOpSimpl := econstructor; split; [ apply exec_straight_one; [simpl; eauto | reflexivity] - | auto 7 with ppcgen; fail ]. -(* - match goal with - | H: (Val.lessdef ?v ?v') |- - exists rs' : regset, - exec_straight ?c ?rs ?m ?k rs' ?m /\ - agree (Regmap.set ?res ?v ?ms) ?sp rs' => - - (exists (nextinstr (rs#(ireg_of res) <- v')); - split; - [ apply exec_straight_one; auto; fail - | auto with ppcgen ]) - || - (exists (nextinstr (rs#(freg_of res) <- v')); - split; - [ apply exec_straight_one; auto; fail - | auto with ppcgen ]) - end. -*) + | split; intros; (repeat SIMP; fail) ]. -Lemma transl_op_correct: - forall op args res k ms sp rs m v m', +Lemma transl_op_correct_aux: + forall op args res k (rs: regset) m v, wt_instr (Mop op args res) -> - agree ms sp rs -> - eval_operation ge sp op (map ms args) m = Some v -> - Mem.extends m m' -> + eval_operation ge (rs#GPR1) op (map rs (map preg_of args)) m = Some v -> exists rs', - exec_straight (transl_op op args res k) rs m' k rs' m' - /\ agree (Regmap.set res v (undef_op op ms)) sp rs'. + exec_straight (transl_op op args res k) rs m k rs' m + /\ rs'#(preg_of res) = v + /\ forall r, + match op with Omove => is_data_reg r = true | _ => is_nontemp_reg r = true end -> + r <> preg_of res -> rs'#r = rs#r. Proof. intros. - assert (exists v', Val.lessdef v v' /\ - eval_operation_total ge sp op (map rs (map preg_of args)) = v'). - exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eauto. - intros [v' [A B]]. exists v'; split; auto. - eapply eval_operation_weaken; eauto. - destruct H3 as [v' [LD EQ]]. clear H1 H2. + exploit eval_operation_weaken; eauto. intro EV. inv H. (* Omove *) simpl in *. exists (nextinstr (rs#(preg_of res) <- (rs#(preg_of r1)))). split. unfold preg_of. rewrite <- H2. destruct (mreg_type r1); apply exec_straight_one; auto. - auto with ppcgen. + split. repeat SIMP. intros; repeat SIMP. (* Other instructions *) destruct op; simpl; simpl in H5; injection H5; clear H5; intros; TypeInv; simpl in *; UseTypeInfo; try (TranslOpSimpl). (* Omove again *) congruence. (* Ointconst *) - destruct (loadimm_correct (ireg_of res) i k rs m') - as [rs' [A [B C]]]. - exists rs'. split. auto. - rewrite <- B in LD. eauto with ppcgen. - (* Ofloatconst *) - exists (nextinstr (rs #GPR12 <- Vundef #(freg_of res) <- (Vfloat f))). - split. apply exec_straight_one. reflexivity. reflexivity. - apply agree_nextinstr. apply agree_set_mfreg; auto. apply agree_set_mreg; auto. - eapply agree_undef_temps; eauto. - intros. apply Pregmap.gso; auto. + destruct (loadimm_correct (ireg_of res) i k rs m) as [rs' [A [B C]]]. + exists rs'. split. auto. split. auto. auto with ppcgen. (* Oaddrsymbol *) - change (find_symbol_offset ge i i0) with (symbol_offset ge i i0) in LD. + change (find_symbol_offset ge i i0) with (symbol_offset ge i i0) in *. set (v' := symbol_offset ge i i0) in *. caseEq (symbol_is_small_data i i0); intro SD. (* small data *) - exists (nextinstr (rs#(ireg_of res) <- v')); split. - apply exec_straight_one; auto. simpl. + econstructor; split. apply exec_straight_one; simpl; reflexivity. + split. repeat SIMP. rewrite (small_data_area_addressing _ _ _ SD). unfold v', symbol_offset. destruct (Genv.find_symbol ge i); auto. rewrite Int.add_zero; auto. - eauto with ppcgen. + intros; repeat SIMP. (* not small data *) - pose (rs1 := nextinstr (rs#GPR12 <- (high_half v'))). - exists (nextinstr (rs1#(ireg_of res) <- v')). - split. apply exec_straight_two with rs1 m'. - unfold exec_instr. rewrite gpr_or_zero_zero. - unfold const_high. rewrite Val.add_commut. - rewrite high_half_zero. reflexivity. - simpl. rewrite gpr_or_zero_not_zero. 2: congruence. - unfold rs1 at 1. rewrite nextinstr_inv; auto with ppcgen. - rewrite Pregmap.gss. - fold v'. rewrite Val.add_commut. unfold v'. rewrite low_high_half. - reflexivity. reflexivity. reflexivity. - unfold rs1. apply agree_nextinstr. apply agree_set_mireg; auto. - apply agree_set_mreg; auto. apply agree_nextinstr. - eapply agree_undef_temps; eauto. - intros. apply Pregmap.gso; auto. +Opaque Val.add. + econstructor; split. eapply exec_straight_two; simpl; reflexivity. + split. repeat SIMP. rewrite gpr_or_zero_zero. + rewrite gpr_or_zero_not_zero; auto with ppcgen. repeat SIMP. + rewrite (Val.add_commut Vzero). rewrite high_half_zero. + rewrite Val.add_commut. rewrite low_high_half. auto. + intros; repeat SIMP. (* Oaddrstack *) - assert (GPR1 <> GPR0). discriminate. - generalize (addimm_correct (ireg_of res) GPR1 i k rs m' (ireg_of_not_GPR0 res) H1). - intros [rs' [EX [RES OTH]]]. - exists rs'. split. auto. - apply agree_set_mireg_exten with rs; auto with ppcgen. - rewrite (sp_val ms sp rs) in LD; auto. rewrite RES; auto. + destruct (addimm_correct (ireg_of res) GPR1 i k rs m) as [rs' [EX [RES OTH]]]. + auto with ppcgen. congruence. + exists rs'; auto with ppcgen. (* Ocast8unsigned *) - econstructor; split. - apply exec_straight_one. simpl; reflexivity. reflexivity. - replace (Val.zero_ext 8 (rs (ireg_of m0))) - with (Val.rolm (rs (ireg_of m0)) Int.zero (Int.repr 255)) in LD. - auto with ppcgen. - unfold Val.rolm, Val.zero_ext. destruct (rs (ireg_of m0)); auto. + econstructor; split. apply exec_straight_one; simpl; reflexivity. + split. repeat SIMP. + destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.rolm_zero. rewrite Int.zero_ext_and. auto. compute; auto. + intros; repeat SIMP. (* Ocast16unsigned *) - econstructor; split. - apply exec_straight_one. simpl; reflexivity. reflexivity. - replace (Val.zero_ext 16 (rs (ireg_of m0))) - with (Val.rolm (rs (ireg_of m0)) Int.zero (Int.repr 65535)) in LD. - auto with ppcgen. - unfold Val.rolm, Val.zero_ext. destruct (rs (ireg_of m0)); auto. + econstructor; split. apply exec_straight_one; simpl; reflexivity. + split. repeat SIMP. + destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.rolm_zero. rewrite Int.zero_ext_and. auto. compute; auto. + intros; repeat SIMP. (* Oaddimm *) - generalize (addimm_correct (ireg_of res) (ireg_of m0) i k rs m' - (ireg_of_not_GPR0 res) (ireg_of_not_GPR0 m0)). - intros [rs' [A [B C]]]. - exists rs'. split. auto. - rewrite <- B in LD. eauto with ppcgen. + destruct (addimm_correct (ireg_of res) (ireg_of m0) i k rs m) as [rs' [A [B C]]]; auto with ppcgen. + exists rs'; auto with ppcgen. (* Osubimm *) case (Int.eq (high_s i) Int.zero). + TranslOpSimpl. + destruct (loadimm_correct GPR0 i (Psubfc (ireg_of res) (ireg_of m0) GPR0 :: k) rs m) as [rs1 [EX [RES OTH]]]. econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - auto 7 with ppcgen. - generalize (loadimm_correct GPR0 i (Psubfc (ireg_of res) (ireg_of m0) GPR0 :: k) rs m'). - intros [rs1 [EX [RES OTH]]]. - econstructor; split. - eapply exec_straight_trans. eexact EX. - apply exec_straight_one. simpl; eauto. auto. - rewrite RES. rewrite OTH; auto with ppcgen. - assert (agree (undef_temps ms) sp rs1). eauto with ppcgen. - auto with ppcgen. decEq; auto with ppcgen. + eapply exec_straight_trans. eexact EX. apply exec_straight_one; simpl; reflexivity. + split. repeat SIMP. rewrite RES. rewrite OTH; auto with ppcgen. + intros; repeat SIMP. (* Omulimm *) case (Int.eq (high_s i) Int.zero). + TranslOpSimpl. + destruct (loadimm_correct GPR0 i (Pmullw (ireg_of res) (ireg_of m0) GPR0 :: k) rs m) as [rs1 [EX [RES OTH]]]. econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - auto with ppcgen. - generalize (loadimm_correct GPR0 i (Pmullw (ireg_of res) (ireg_of m0) GPR0 :: k) rs m'). - intros [rs1 [EX [RES OTH]]]. - assert (agree (undef_temps ms) sp rs1). eauto with ppcgen. - econstructor; split. - eapply exec_straight_trans. eexact EX. - apply exec_straight_one. simpl; eauto. auto. - rewrite RES. rewrite OTH; auto with ppcgen. decEq; auto with ppcgen. + eapply exec_straight_trans. eexact EX. apply exec_straight_one; simpl; reflexivity. + split. repeat SIMP. rewrite RES. rewrite OTH; auto with ppcgen. + intros; repeat SIMP. (* Oand *) set (v' := Val.and (rs (ireg_of m0)) (rs (ireg_of m1))) in *. pose (rs1 := rs#(ireg_of res) <- v'). generalize (compare_sint_spec rs1 v' Vzero). intros [A [B [C D]]]. - exists (nextinstr (compare_sint rs1 v' Vzero)). - split. apply exec_straight_one. auto. auto. - apply agree_exten_2 with rs1. unfold rs1; auto with ppcgen. - auto. + econstructor; split. apply exec_straight_one; simpl; reflexivity. + split. rewrite D; auto with ppcgen. unfold rs1. SIMP. + intros. rewrite D; auto with ppcgen. unfold rs1. SIMP. (* Oandimm *) - generalize (andimm_correct (ireg_of res) (ireg_of m0) i k rs m' - (ireg_of_not_GPR0 m0)). - intros [rs' [A [B [C D]]]]. - exists rs'. split. auto. rewrite <- B in LD. eauto with ppcgen. + destruct (andimm_correct (ireg_of res) (ireg_of m0) i k rs m) as [rs' [A [B [C D]]]]; auto with ppcgen. + exists rs'; auto with ppcgen. (* Oorimm *) - generalize (orimm_correct (ireg_of res) (ireg_of m0) i k rs m'). - intros [rs' [A [B C]]]. - exists rs'. split. auto. rewrite <- B in LD. eauto with ppcgen. + destruct (orimm_correct (ireg_of res) (ireg_of m0) i k rs m) as [rs' [A [B C]]]. + exists rs'; auto with ppcgen. (* Oxorimm *) - generalize (xorimm_correct (ireg_of res) (ireg_of m0) i k rs m'). - intros [rs' [A [B C]]]. - exists rs'. split. auto. rewrite <- B in LD. eauto with ppcgen. - (* Oxhrximm *) - pose (rs1 := nextinstr (rs#(ireg_of res) <- (Val.shr (rs (ireg_of m0)) (Vint i)) #CARRY <- (Val.shr_carry (rs (ireg_of m0)) (Vint i)))). - exists (nextinstr (rs1#(ireg_of res) <- (Val.shrx (rs (ireg_of m0)) (Vint i)))). - split. apply exec_straight_two with rs1 m'. - auto. simpl. decEq. decEq. decEq. - unfold rs1. repeat (rewrite nextinstr_inv; try discriminate). - rewrite Pregmap.gss. rewrite Pregmap.gso. rewrite Pregmap.gss. - apply Val.shrx_carry. auto with ppcgen. auto. auto. - apply agree_nextinstr. unfold rs1. apply agree_nextinstr_commut. - apply agree_set_commut. auto with ppcgen. - apply agree_set_other. apply agree_set_mireg_twice; auto with ppcgen. - compute; auto. auto with ppcgen. + destruct (xorimm_correct (ireg_of res) (ireg_of m0) i k rs m) as [rs' [A [B C]]]. + exists rs'; auto with ppcgen. + (* Oshrximm *) + econstructor; split. + eapply exec_straight_two; simpl; reflexivity. + split. repeat SIMP. apply Val.shrx_carry. + intros; repeat SIMP. (* Oroli *) destruct (mreg_eq m0 res). subst m0. TranslOpSimpl. econstructor; split. - eapply exec_straight_three. - simpl. reflexivity. - simpl. reflexivity. - simpl. reflexivity. - auto. auto. auto. - set (rs1 := nextinstr (rs # GPR0 <- (rs (ireg_of m0)))). - set (rs2 := nextinstr (rs1 # GPR0 <- - (Val.or (Val.and (rs1 GPR0) (Vint (Int.not i0))) - (Val.rolm (rs1 (ireg_of m1)) i i0)))). - apply agree_nextinstr. apply agree_set_mireg; auto. apply agree_set_mreg. - apply agree_undef_temps with rs. auto. - intros. unfold rs2. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. - unfold rs1. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. - unfold rs2. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - unfold rs1. repeat rewrite nextinstr_inv; auto with ppcgen. - rewrite Pregmap.gss. rewrite Pregmap.gso; auto with ppcgen. decEq. auto with ppcgen. - (* Ointoffloat *) - econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - apply agree_nextinstr. apply agree_set_mireg; auto. apply agree_set_mreg; auto. - apply agree_undef_temps with rs; auto. intros. - repeat rewrite Pregmap.gso; auto. + eapply exec_straight_three; simpl; reflexivity. + split. repeat SIMP. intros; repeat SIMP. (* Ocmp *) - revert H1 LD; case (classify_condition c args); intros. - (* Optimization: compimm Cge 0 *) - subst n. simpl in *. inv H1. UseTypeInfo. - set (rs1 := nextinstr (rs#(ireg_of res) <- (Val.rolm (rs (ireg_of r)) Int.one Int.one))). - set (rs2 := nextinstr (rs1#(ireg_of res) <- (Val.xor (rs1#(ireg_of res)) (Vint Int.one)))). - exists rs2. - split. apply exec_straight_two with rs1 m'; auto. - rewrite <- Val.rolm_ge_zero in LD. - unfold rs2. apply agree_nextinstr. - unfold rs1. apply agree_nextinstr_commut. fold rs1. - replace (rs1 (ireg_of res)) with (Val.rolm (rs (ireg_of r)) Int.one Int.one). - apply agree_set_mireg_twice; auto with ppcgen. - unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss. auto. - auto with ppcgen. auto with ppcgen. - (* Optimization: compimm Clt 0 *) - subst n. simpl in *. inv H1. UseTypeInfo. - exists (nextinstr (rs#(ireg_of res) <- (Val.rolm (rs (ireg_of r)) Int.one Int.one))). - split. apply exec_straight_one; auto. - rewrite <- Val.rolm_lt_zero in LD. - auto with ppcgen. - (* General case *) - set (bit := fst (crbit_for_cond c0)). - set (isset := snd (crbit_for_cond c0)). - set (k1 := - Pmfcrbit (ireg_of res) bit :: - (if isset - then k - else Pxori (ireg_of res) (ireg_of res) (Cint Int.one) :: k)). - generalize (transl_cond_correct_aux c0 rl k1 ms sp rs m' H1 H0). - fold bit; fold isset. - intros [rs1 [EX1 [RES1 AG1]]]. - set (rs2 := nextinstr (rs1#(ireg_of res) <- (rs1#(reg_of_crbit bit)))). - destruct isset. - exists rs2. - split. apply exec_straight_trans with k1 rs1 m'. assumption. - unfold k1. apply exec_straight_one. - reflexivity. reflexivity. - unfold rs2. rewrite RES1. auto with ppcgen. - econstructor. - split. apply exec_straight_trans with k1 rs1 m'. assumption. - unfold k1. apply exec_straight_two with rs2 m'. - reflexivity. simpl. eauto. auto. auto. - apply agree_nextinstr. - unfold rs2 at 1. rewrite nextinstr_inv. rewrite Pregmap.gss. - rewrite RES1. rewrite <- Val.notbool_xor. - unfold rs2. auto 7 with ppcgen. - apply eval_condition_total_is_bool. - auto with ppcgen. + destruct (eval_condition c rs ## (preg_of ## args) m) as [ b | ] _eqn; try discriminate. + destruct (transl_cond_op_correct c args res k rs m b) as [rs' [A [B C]]]; auto. + exists rs'; intuition auto with ppcgen. + rewrite B. destruct b; inv H0; auto. +Qed. + +Lemma transl_op_correct: + forall op args res k ms sp rs m v m', + wt_instr (Mop op args res) -> + agree ms sp rs -> + eval_operation ge sp op (map ms args) m = Some v -> + Mem.extends m m' -> + exists rs', + exec_straight (transl_op op args res k) rs m' k rs' m' + /\ agree (Regmap.set res v (undef_op op ms)) sp rs'. +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. + unfold undef_op. destruct op; + (apply agree_set_mreg_undef_temps with rs || apply agree_set_mreg with rs); + auto. Qed. Lemma transl_load_store_correct: @@ -1452,10 +1380,10 @@ Proof. set (rs1 := nextinstr (rs#temp <- (Val.add (rs (ireg_of m0)) (Vint (Int.shl (high_s i) (Int.repr 16)))))). exploit (H (Cint (low_s i)) temp rs1 k). simpl. UseTypeInfo. rewrite gpr_or_zero_not_zero; auto. - unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss. - rewrite Val.add_assoc. simpl. rewrite low_high_s. auto. - discriminate. - intros. unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + unfold rs1; repeat SIMP. rewrite Val.add_assoc. +Transparent Val.add. + simpl. rewrite low_high_s. auto. + intros; unfold rs1; repeat SIMP. intros [rs' [EX' AG']]. exists rs'. split. apply exec_straight_step with rs1 m. simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen. auto. @@ -1552,15 +1480,21 @@ Proof. (* mk1 *) intros. exists (nextinstr (rs1#(preg_of dst) <- v')). split. apply exec_straight_one. rewrite H. - unfold load1. rewrite <- H6. rewrite C. auto. - auto with ppcgen. - eauto with ppcgen. + unfold load1. rewrite <- H6. rewrite C. auto. + unfold nextinstr. SIMP. decEq. SIMP. apply sym_not_equal; auto with ppcgen. + apply agree_set_mreg with rs1. + apply agree_undef_temps with rs; auto with ppcgen. + repeat SIMP. + intros; repeat SIMP. (* mk2 *) intros. exists (nextinstr (rs#(preg_of dst) <- v')). split. apply exec_straight_one. rewrite H0. unfold load2. rewrite <- H6. rewrite C. auto. - auto with ppcgen. - eauto with ppcgen. + unfold nextinstr. SIMP. decEq. SIMP. apply sym_not_equal; auto with ppcgen. + apply agree_set_mreg with rs. + apply agree_undef_temps with rs; auto with ppcgen. + repeat SIMP. + intros; repeat SIMP. (* not GPR0 *) congruence. Qed. @@ -1611,9 +1545,9 @@ Proof. intros [rs3 [U V]]. exists rs3; split. apply exec_straight_one. auto. rewrite V; auto with ppcgen. - eapply agree_undef_temps; eauto. intros. - rewrite V; auto. rewrite nextinstr_inv; auto. apply H7; auto. - unfold int_temp_for. destruct (mreg_eq src IT2); auto. + apply agree_undef_temps with rs. auto. + intros. rewrite V; auto with ppcgen. SIMP. apply H7; auto with ppcgen. + unfold int_temp_for. destruct (mreg_eq src IT2); auto with ppcgen. (* mk2 *) intros. exploit (H0 r1 r2 rs (nextinstr rs) m1'). @@ -1622,7 +1556,7 @@ Proof. exists rs3; split. apply exec_straight_one. auto. rewrite V; auto with ppcgen. eapply agree_undef_temps; eauto. intros. - rewrite V; auto. rewrite nextinstr_inv; auto. + rewrite V; auto with ppcgen. unfold int_temp_for. destruct (mreg_eq src IT2); congruence. Qed. -- cgit