diff options
Diffstat (limited to 'backend/PPCgenproof1.v')
| -rw-r--r-- | backend/PPCgenproof1.v | 1686 |
1 files changed, 0 insertions, 1686 deletions
diff --git a/backend/PPCgenproof1.v b/backend/PPCgenproof1.v deleted file mode 100644 index dd142c5b..00000000 --- a/backend/PPCgenproof1.v +++ /dev/null @@ -1,1686 +0,0 @@ -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, INRIA Paris-Rocquencourt *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Correctness proof for PPC generation: auxiliary results. *) - -Require Import Coqlib. -Require Import Maps. -Require Import AST. -Require Import Integers. -Require Import Floats. -Require Import Values. -Require Import Mem. -Require Import Globalenvs. -Require Import Op. -Require Import Locations. -Require Import Mach. -Require Import Machconcr. -Require Import Machtyping. -Require Import PPC. -Require Import PPCgen. -Require Conventions. - -(** * Properties of low half/high half decomposition *) - -Lemma high_half_zero: - forall v, Val.add (high_half v) Vzero = high_half v. -Proof. - intros. generalize (high_half_type v). - rewrite Val.add_commut. - case (high_half v); simpl; intros; try contradiction. - auto. - rewrite Int.add_commut; rewrite Int.add_zero; auto. - rewrite Int.add_zero; auto. -Qed. - -Lemma low_high_u: - forall n, Int.or (Int.shl (high_u n) (Int.repr 16)) (low_u n) = n. -Proof. - intros. unfold high_u, low_u. - rewrite Int.shl_rolm. rewrite Int.shru_rolm. - rewrite Int.rolm_rolm. - change (Int.modu (Int.add (Int.sub (Int.repr (Z_of_nat wordsize)) (Int.repr 16)) - (Int.repr 16)) - (Int.repr (Z_of_nat wordsize))) - with (Int.zero). - rewrite Int.rolm_zero. rewrite <- Int.and_or_distrib. - exact (Int.and_mone n). - reflexivity. reflexivity. -Qed. - -Lemma low_high_u_xor: - forall n, Int.xor (Int.shl (high_u n) (Int.repr 16)) (low_u n) = n. -Proof. - intros. unfold high_u, low_u. - rewrite Int.shl_rolm. rewrite Int.shru_rolm. - rewrite Int.rolm_rolm. - change (Int.modu (Int.add (Int.sub (Int.repr (Z_of_nat wordsize)) (Int.repr 16)) - (Int.repr 16)) - (Int.repr (Z_of_nat wordsize))) - with (Int.zero). - rewrite Int.rolm_zero. rewrite <- Int.and_xor_distrib. - exact (Int.and_mone n). - reflexivity. reflexivity. -Qed. - -Lemma low_high_s: - forall n, Int.add (Int.shl (high_s n) (Int.repr 16)) (low_s n) = n. -Proof. - intros. rewrite Int.shl_mul_two_p. - unfold high_s. - rewrite <- (Int.divu_pow2 (Int.sub n (low_s n)) (Int.repr 65536) (Int.repr 16)). - change (two_p (Int.unsigned (Int.repr 16))) with 65536. - - assert (forall x y, y > 0 -> (x - x mod y) mod y = 0). - intros. apply Zmod_unique with (x / y). - generalize (Z_div_mod_eq x y H). intro. rewrite Zmult_comm. omega. - omega. - - assert (Int.modu (Int.sub n (low_s n)) (Int.repr 65536) = Int.zero). - unfold Int.modu, Int.zero. decEq. - change (Int.unsigned (Int.repr 65536)) with 65536. - unfold Int.sub. - assert (forall a b, Int.eqm a b -> b mod 65536 = 0 -> a mod 65536 = 0). - intros a b [k EQ] H1. rewrite EQ. - change modulus with (65536 * 65536). - rewrite Zmult_assoc. rewrite Zplus_comm. rewrite Z_mod_plus. auto. - omega. - eapply H0. apply Int.eqm_sym. apply Int.eqm_unsigned_repr. - unfold low_s. unfold Int.sign_ext. - change (two_p 16) with 65536. change (two_p (16-1)) with 32768. - set (N := Int.unsigned n). - case (zlt (N mod 65536) 32768); intro. - apply H0 with (N - N mod 65536). auto with ints. - apply H. omega. - apply H0 with (N - (N mod 65536 - 65536)). auto with ints. - replace (N - (N mod 65536 - 65536)) - with ((N - N mod 65536) + 1 * 65536). - rewrite Z_mod_plus. apply H. omega. omega. ring. - - assert (Int.repr 65536 <> Int.zero). compute. congruence. - generalize (Int.modu_divu_Euclid (Int.sub n (low_s n)) (Int.repr 65536) H1). - rewrite H0. rewrite Int.add_zero. intro. rewrite <- H2. - rewrite Int.sub_add_opp. rewrite Int.add_assoc. - replace (Int.add (Int.neg (low_s n)) (low_s n)) with Int.zero. - apply Int.add_zero. symmetry. rewrite Int.add_commut. - rewrite <- Int.sub_add_opp. apply Int.sub_idem. - - reflexivity. -Qed. - -(** * Correspondence between Mach registers and PPC registers *) - -Hint Extern 2 (_ <> _) => discriminate: ppcgen. - -(** Mapping from Mach registers to PPC registers. *) - -Definition preg_of (r: mreg) := - match mreg_type r with - | Tint => IR (ireg_of r) - | Tfloat => FR (freg_of r) - end. - -Lemma preg_of_injective: - forall r1 r2, preg_of r1 = preg_of r2 -> r1 = r2. -Proof. - destruct r1; destruct r2; simpl; intros; reflexivity || discriminate. -Qed. - -(** Characterization of PPC registers that correspond to Mach registers. *) - -Definition is_data_reg (r: preg) : Prop := - match r with - | IR GPR12 => 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. - -Lemma ireg_of_is_data_reg: - forall (r: mreg), is_data_reg (ireg_of r). -Proof. - destruct r; exact I. -Qed. - -Lemma freg_of_is_data_reg: - forall (r: mreg), is_data_reg (ireg_of r). -Proof. - destruct r; exact I. -Qed. - -Lemma preg_of_is_data_reg: - forall (r: mreg), is_data_reg (preg_of r). -Proof. - destruct r; exact I. -Qed. - -Lemma ireg_of_not_GPR1: - forall r, ireg_of r <> GPR1. -Proof. - intro. case r; discriminate. -Qed. -Lemma ireg_of_not_GPR12: - forall r, ireg_of r <> GPR12. -Proof. - intro. case r; discriminate. -Qed. -Lemma freg_of_not_FPR13: - forall r, freg_of r <> FPR13. -Proof. - intro. case r; discriminate. -Qed. -Hint Resolve ireg_of_not_GPR1 ireg_of_not_GPR12 freg_of_not_FPR13: ppcgen. - -Lemma preg_of_not: - forall r1 r2, ~(is_data_reg r2) -> preg_of r1 <> r2. -Proof. - intros; red; intro. subst r2. elim H. apply preg_of_is_data_reg. -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. - -(** Agreement between Mach register sets and PPC register sets. *) - -Definition agree (ms: Mach.regset) (sp: val) (rs: PPC.regset) := - rs#GPR1 = sp /\ forall r: mreg, ms r = rs#(preg_of r). - -Lemma preg_val: - forall ms sp rs r, - agree ms sp rs -> ms r = rs#(preg_of r). -Proof. - intros. elim H. auto. -Qed. - -Lemma ireg_val: - forall ms sp rs r, - agree ms sp rs -> - mreg_type r = Tint -> - ms r = rs#(ireg_of r). -Proof. - intros. elim H; intros. - generalize (H2 r). unfold preg_of. rewrite H0. auto. -Qed. - -Lemma freg_val: - forall ms sp rs r, - agree ms sp rs -> - mreg_type r = Tfloat -> - ms r = rs#(freg_of r). -Proof. - intros. elim H; intros. - generalize (H2 r). unfold preg_of. rewrite H0. auto. -Qed. - -Lemma sp_val: - forall ms sp rs, - agree ms sp rs -> - sp = rs#GPR1. -Proof. - intros. elim H; auto. -Qed. - -Lemma agree_exten_1: - forall ms sp rs rs', - agree ms sp rs -> - (forall r, is_data_reg r -> rs'#r = rs#r) -> - agree ms sp rs'. -Proof. - unfold agree; intros. elim H; intros. - split. rewrite H0. auto. exact I. - 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 GPR12 -> r <> FR FPR13 -> - 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). -Qed. - -(** Preservation of register agreement under various assignments. *) - -Lemma agree_set_mreg: - forall ms sp rs r v, - agree ms sp rs -> - agree (Regmap.set r v ms) sp (rs#(preg_of r) <- v). -Proof. - unfold agree; intros. elim H; intros; clear H. - split. rewrite Pregmap.gso. auto. apply sym_not_eq. apply preg_of_not_GPR1. - 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. -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) -> - mreg_type r = Tint -> - agree ms sp (rs#(ireg_of r) <- v). -Proof. - intros. unfold preg_of in H. rewrite H0 in H. 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) -> - mreg_type r = Tfloat -> - agree ms sp (rs#(freg_of r) <- v). -Proof. - intros. unfold preg_of in H. rewrite H0 in H. 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) -> - agree ms sp (rs#r <- v). -Proof. - intros. apply agree_exten_1 with rs. - auto. intros. apply Pregmap.gso. red; intro; subst r0; contradiction. -Qed. -Hint Resolve agree_set_other: ppcgen. - -Lemma agree_nextinstr: - forall ms sp rs, - agree ms sp rs -> agree ms sp (nextinstr rs). -Proof. - intros. unfold nextinstr. apply agree_set_other. auto. auto. -Qed. -Hint Resolve agree_nextinstr: ppcgen. - -Lemma agree_set_mireg_twice: - forall ms sp rs r v v', - agree ms sp rs -> - mreg_type r = Tint -> - agree (Regmap.set r v ms) sp (rs #(ireg_of r) <- v' #(ireg_of r) <- v). -Proof. - intros. replace (IR (ireg_of r)) with (preg_of r). elim H; intros. - split. repeat (rewrite Pregmap.gso; auto with ppcgen). - 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. -Qed. -Hint Resolve agree_set_mireg_twice: ppcgen. - -Lemma agree_set_twice_mireg: - forall ms sp rs r v v', - agree (Regmap.set r v' ms) sp rs -> - mreg_type r = Tint -> - agree (Regmap.set r v ms) sp (rs#(ireg_of r) <- v). -Proof. - intros. elim H; intros. - split. rewrite Pregmap.gso. auto. - generalize (ireg_of_not_GPR1 r); congruence. - intros. generalize (H2 r0). - case (mreg_eq r0 r); intro. - subst r0. repeat rewrite Regmap.gss. unfold preg_of; rewrite H0. - rewrite Pregmap.gss. auto. - repeat rewrite Regmap.gso; auto. - rewrite Pregmap.gso. auto. - replace (IR (ireg_of r)) with (preg_of r). - 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 -> - rs'#(ireg_of r) = v -> - (forall r', - r' <> IR GPR12 -> r' <> FR FPR13 -> - 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. 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. - -(** Useful properties of the PC and GPR0 registers. *) - -Lemma nextinstr_inv: - forall r rs, r <> PC -> (nextinstr rs)#r = rs#r. -Proof. - intros. unfold nextinstr. apply Pregmap.gso. auto. -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. - intros. unfold gpr_or_zero. case (ireg_eq r GPR0); tauto. -Qed. -Lemma gpr_or_zero_zero: - forall rs, gpr_or_zero rs GPR0 = Vzero. -Proof. - intros. reflexivity. -Qed. -Hint Resolve gpr_or_zero_not_zero gpr_or_zero_zero: ppcgen. - -(** Connection between Mach and PPC calling conventions for external - functions. *) - -Lemma loc_external_result_match: - forall sg, - PPC.loc_external_result sg = preg_of (Conventions.loc_result sg). -Proof. - intros. destruct sg as [sargs sres]. - destruct sres. destruct t; reflexivity. reflexivity. -Qed. - -Lemma extcall_args_match: - forall ms m sp rs, - agree ms sp rs -> - forall tyl iregl fregl ofs args, - (forall r, In r iregl -> mreg_type r = Tint) -> - (forall r, In r fregl -> mreg_type r = Tfloat) -> - Machconcr.extcall_args ms m sp (Conventions.loc_arguments_rec tyl iregl fregl ofs) args -> - PPC.extcall_args rs m tyl (List.map ireg_of iregl) (List.map freg_of fregl) (Stacking.fe_ofs_arg + 4 * ofs) args. -Proof. - induction tyl; intros. - inversion H2; constructor. - destruct a. - (* integer case *) - destruct iregl as [ | ir1 irl]. - (* stack *) - inversion H2; subst; clear H2. inversion H8; subst; clear H8. - constructor. replace (rs GPR1) with sp. assumption. - eapply sp_val; eauto. - change (@nil ireg) with (ireg_of ## nil). - replace (Stacking.fe_ofs_arg + 4 * ofs + 4) with (Stacking.fe_ofs_arg + 4 * (ofs + 1)) by omega. - apply IHtyl; auto. - (* register *) - inversion H2; subst; clear H2. inversion H8; subst; clear H8. - simpl map. econstructor. eapply ireg_val; eauto. - apply H0; simpl; auto. - replace (4 * ofs + 4) with (4 * (ofs + 1)) by omega. - apply IHtyl; auto. - intros; apply H0; simpl; auto. - (* float case *) - destruct fregl as [ | fr1 frl]. - (* stack *) - inversion H2; subst; clear H2. inversion H8; subst; clear H8. - constructor. replace (rs GPR1) with sp. assumption. - eapply sp_val; eauto. - change (@nil freg) with (freg_of ## nil). - replace (Stacking.fe_ofs_arg + 4 * ofs + 8) with (Stacking.fe_ofs_arg + 4 * (ofs + 2)) by omega. - apply IHtyl; auto. - (* register *) - inversion H2; subst; clear H2. inversion H8; subst; clear H8. - simpl map. econstructor. eapply freg_val; eauto. - apply H1; simpl; auto. - rewrite list_map_drop2. - apply IHtyl; auto. - intros; apply H0. apply list_drop2_incl. auto. - intros; apply H1; simpl; auto. -Qed. - -Ltac ElimOrEq := - match goal with - | |- (?x = ?y) \/ _ -> _ => - let H := fresh in - (intro H; elim H; clear H; - [intro H; rewrite <- H; clear H | ElimOrEq]) - | |- False -> _ => - let H := fresh in (intro H; contradiction) - end. - -Lemma extcall_arguments_match: - forall ms m sp rs sg args, - agree ms sp rs -> - Machconcr.extcall_arguments ms m sp sg args -> - PPC.extcall_arguments rs m sg args. -Proof. - unfold Machconcr.extcall_arguments, PPC.extcall_arguments; intros. - change (extcall_args rs m sg.(sig_args) - (List.map ireg_of Conventions.int_param_regs) - (List.map freg_of Conventions.float_param_regs) - (Stacking.fe_ofs_arg + 4 * 8) args). - eapply extcall_args_match; eauto. - intro; simpl; ElimOrEq; reflexivity. - intro; simpl; ElimOrEq; reflexivity. -Qed. - -(** * Execution of straight-line code *) - -Section STRAIGHTLINE. - -Variable ge: genv. -Variable fn: code. - -(** Straight-line code is composed of PPC instructions that execute - in sequence (no branches, no function calls and returns). - The following inductive predicate relates the machine states - before and after executing a straight-line sequence of instructions. - Instructions are taken from the first list instead of being fetched - from memory. *) - -Inductive exec_straight: code -> regset -> mem -> - code -> regset -> mem -> Prop := - | exec_straight_one: - forall i1 c rs1 m1 rs2 m2, - exec_instr ge fn i1 rs1 m1 = OK rs2 m2 -> - rs2#PC = Val.add rs1#PC Vone -> - exec_straight (i1 :: c) rs1 m1 c rs2 m2 - | exec_straight_step: - forall i c rs1 m1 rs2 m2 c' rs3 m3, - exec_instr ge fn i rs1 m1 = OK rs2 m2 -> - rs2#PC = Val.add rs1#PC Vone -> - exec_straight c rs2 m2 c' rs3 m3 -> - exec_straight (i :: c) rs1 m1 c' rs3 m3. - -Lemma exec_straight_trans: - forall c1 rs1 m1 c2 rs2 m2 c3 rs3 m3, - exec_straight c1 rs1 m1 c2 rs2 m2 -> - exec_straight c2 rs2 m2 c3 rs3 m3 -> - exec_straight c1 rs1 m1 c3 rs3 m3. -Proof. - induction 1; intros. - apply exec_straight_step with rs2 m2; auto. - apply exec_straight_step with rs2 m2; auto. -Qed. - -Lemma exec_straight_two: - forall i1 i2 c rs1 m1 rs2 m2 rs3 m3, - exec_instr ge fn i1 rs1 m1 = OK rs2 m2 -> - exec_instr ge fn i2 rs2 m2 = OK rs3 m3 -> - rs2#PC = Val.add rs1#PC Vone -> - rs3#PC = Val.add rs2#PC Vone -> - exec_straight (i1 :: i2 :: c) rs1 m1 c rs3 m3. -Proof. - intros. apply exec_straight_step with rs2 m2; auto. - apply exec_straight_one; auto. -Qed. - -Lemma exec_straight_three: - forall i1 i2 i3 c rs1 m1 rs2 m2 rs3 m3 rs4 m4, - exec_instr ge fn i1 rs1 m1 = OK rs2 m2 -> - exec_instr ge fn i2 rs2 m2 = OK rs3 m3 -> - exec_instr ge fn i3 rs3 m3 = OK rs4 m4 -> - rs2#PC = Val.add rs1#PC Vone -> - rs3#PC = Val.add rs2#PC Vone -> - rs4#PC = Val.add rs3#PC Vone -> - exec_straight (i1 :: i2 :: i3 :: c) rs1 m1 c rs4 m4. -Proof. - intros. apply exec_straight_step with rs2 m2; auto. - eapply exec_straight_two; eauto. -Qed. - -(** * Correctness of PowerPC constructor functions *) - -(** Properties of comparisons. *) - -Lemma compare_float_spec: - forall rs v1 v2, - let rs1 := nextinstr (compare_float rs v1 v2) in - 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'. -Proof. - intros. unfold rs1. - split. reflexivity. - split. reflexivity. - split. reflexivity. - intros. rewrite nextinstr_inv; auto. - unfold compare_float. repeat (rewrite Pregmap.gso; auto). -Qed. - -Lemma compare_sint_spec: - forall rs v1 v2, - let rs1 := nextinstr (compare_sint rs v1 v2) in - 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'. -Proof. - intros. unfold rs1. - split. reflexivity. - split. reflexivity. - split. reflexivity. - intros. rewrite nextinstr_inv; auto. - unfold compare_sint. repeat (rewrite Pregmap.gso; auto). -Qed. - -Lemma compare_uint_spec: - forall rs v1 v2, - let rs1 := nextinstr (compare_uint rs v1 v2) in - 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'. -Proof. - intros. unfold rs1. - split. reflexivity. - split. reflexivity. - split. reflexivity. - intros. rewrite nextinstr_inv; auto. - unfold compare_uint. repeat (rewrite Pregmap.gso; auto). -Qed. - -(** Loading a constant. *) - -Lemma loadimm_correct: - forall r n k rs m, - exists rs', - exec_straight (loadimm r n k) rs m k rs' m - /\ rs'#r = Vint n - /\ forall r': preg, r' <> r -> r' <> PC -> rs'#r' = rs#r'. -Proof. - intros. unfold loadimm. - case (Int.eq (high_s n) Int.zero). - (* addi *) - exists (nextinstr (rs#r <- (Vint n))). - split. apply exec_straight_one. - simpl. rewrite Int.add_commut. rewrite Int.add_zero. reflexivity. - reflexivity. - split. rewrite nextinstr_inv; auto with ppcgen. - apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. - (* 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))). - split. apply exec_straight_one. - 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. - (* 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 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. -Qed. - -(** Add integer immediate. *) - -Lemma addimm_1_correct: - forall r1 r2 n k rs m, - r1 <> GPR0 -> - r2 <> GPR0 -> - exists rs', - exec_straight (addimm_1 r1 r2 n k) rs m k rs' m - /\ rs'#r1 = Val.add rs#r2 (Vint n) - /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'. -Proof. - intros. unfold addimm_1. - (* addi *) - case (Int.eq (high_s n) Int.zero). - exists (nextinstr (rs#r1 <- (Val.add rs#r2 (Vint n)))). - 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. - (* 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)))). - split. apply exec_straight_one. - simpl. rewrite gpr_or_zero_not_zero; auto. - 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. - (* 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)))). - split. apply exec_straight_two with rs1 m. - simpl. rewrite gpr_or_zero_not_zero; auto. - simpl. rewrite gpr_or_zero_not_zero; auto. - 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. -Qed. - -Lemma addimm_2_correct: - forall r1 r2 n k rs m, - r2 <> GPR12 -> - exists rs', - exec_straight (addimm_2 r1 r2 n k) rs m k rs' m - /\ rs'#r1 = Val.add rs#r2 (Vint n) - /\ forall r': preg, r' <> r1 -> r' <> GPR12 -> r' <> PC -> rs'#r' = rs#r'. -Proof. - intros. unfold addimm_2. - generalize (loadimm_correct GPR12 n (Padd r1 r2 GPR12 :: k) rs m). - intros [rs1 [EX [RES OTHER]]]. - exists (nextinstr (rs1#r1 <- (Val.add rs#r2 (Vint n)))). - split. eapply exec_straight_trans. eexact EX. - apply exec_straight_one. simpl. rewrite RES. rewrite OTHER. - auto. congruence. discriminate. - reflexivity. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. -Qed. - -Lemma addimm_correct: - forall r1 r2 n k rs m, - r2 <> GPR12 -> - exists rs', - exec_straight (addimm r1 r2 n k) rs m k rs' m - /\ rs'#r1 = Val.add rs#r2 (Vint n) - /\ forall r': preg, r' <> r1 -> r' <> GPR12 -> r' <> PC -> rs'#r' = rs#r'. -Proof. - intros. unfold addimm. - case (ireg_eq r1 GPR0); intro. - apply addimm_2_correct; auto. - case (ireg_eq r2 GPR0); intro. - apply addimm_2_correct; auto. - generalize (addimm_1_correct r1 r2 n k rs m n0 n1). - intros [rs' [EX [RES OTH]]]. exists rs'. intuition. -Qed. - -(** And integer immediate. *) - -Lemma andimm_correct: - forall r1 r2 n k (rs : regset) m, - r2 <> GPR12 -> - let v := Val.and rs#r2 (Vint n) in - exists rs', - 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' <> GPR12 -> r' <> PC -> - r' <> CR0_0 -> r' <> CR0_1 -> r' <> CR0_2 -> r' <> CR0_3 -> - rs'#r' = rs#r'. -Proof. - intros. unfold andimm. - case (Int.eq (high_u n) Int.zero). - (* andi *) - exists (nextinstr (compare_sint (rs#r1 <- v) v Vzero)). - 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. auto. - intros. rewrite D; auto. apply Pregmap.gso; auto. - (* andis *) - generalize (Int.eq_spec (low_u n) Int.zero); - case (Int.eq (low_u n) Int.zero); intro. - exists (nextinstr (compare_sint (rs#r1 <- v) v Vzero)). - generalize (compare_sint_spec (rs#r1 <- v) v Vzero). - intros [A [B [C D]]]. - 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. auto. - intros. rewrite D; auto. apply Pregmap.gso; auto. - (* loadimm + and *) - generalize (loadimm_correct GPR12 n (Pand_ r1 r2 GPR12 :: k) rs m). - intros [rs1 [EX1 [RES1 OTHER1]]]. - exists (nextinstr (compare_sint (rs1#r1 <- v) v Vzero)). - generalize (compare_sint_spec (rs1#r1 <- v) v Vzero). - intros [A [B [C D]]]. - split. eapply exec_straight_trans. eexact EX1. - apply exec_straight_one. simpl. rewrite RES1. - rewrite (OTHER1 r2). reflexivity. congruence. congruence. - reflexivity. - split. rewrite D; try discriminate. apply Pregmap.gss. - split. auto. - intros. rewrite D; auto. rewrite Pregmap.gso; auto. -Qed. - -(** Or integer immediate. *) - -Lemma orimm_correct: - forall r1 (r2: ireg) n k (rs : regset) m, - let v := Val.or rs#r2 (Vint n) in - exists rs', - exec_straight (orimm r1 r2 n k) rs m k rs' m - /\ rs'#r1 = v - /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'. -Proof. - intros. unfold orimm. - case (Int.eq (high_u n) Int.zero). - (* 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. - (* oris *) - generalize (Int.eq_spec (low_u n) Int.zero); - case (Int.eq (low_u n) Int.zero); intro. - exists (nextinstr (rs#r1 <- v)). - 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. - (* 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. -Qed. - -(** Xor integer immediate. *) - -Lemma xorimm_correct: - forall r1 (r2: ireg) n k (rs : regset) m, - let v := Val.xor rs#r2 (Vint n) in - exists rs', - exec_straight (xorimm r1 r2 n k) rs m k rs' m - /\ rs'#r1 = v - /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'. -Proof. - intros. unfold xorimm. - case (Int.eq (high_u n) Int.zero). - (* 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. - (* xoris *) - generalize (Int.eq_spec (low_u n) Int.zero); - case (Int.eq (low_u n) Int.zero); intro. - exists (nextinstr (rs#r1 <- v)). - 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. - (* 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. -Qed. - -(** Indexed memory loads. *) - -Lemma loadind_aux_correct: - forall (base: ireg) ofs ty dst (rs: regset) m v, - Mem.loadv (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) = Some v -> - mreg_type dst = ty -> - base <> GPR0 -> - exec_instr ge fn (loadind_aux base ofs ty dst) rs m = - OK (nextinstr (rs#(preg_of dst) <- v)) m. -Proof. - intros. unfold loadind_aux. unfold preg_of. rewrite H0. destruct ty. - simpl. unfold load1. rewrite gpr_or_zero_not_zero; auto. - unfold const_low. simpl in H. rewrite H. auto. - simpl. unfold load1. rewrite gpr_or_zero_not_zero; auto. - unfold const_low. simpl in H. rewrite H. auto. -Qed. - -Lemma loadind_correct: - forall (base: ireg) ofs ty dst k (rs: regset) m v, - Mem.loadv (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) = Some v -> - mreg_type dst = ty -> - base <> GPR0 -> - exists rs', - exec_straight (loadind base ofs ty dst k) rs m k rs' m - /\ rs'#(preg_of dst) = v - /\ forall r, r <> PC -> r <> GPR12 -> r <> preg_of dst -> rs'#r = rs#r. -Proof. - intros. unfold loadind. - assert (preg_of dst <> PC). - unfold preg_of. case (mreg_type dst); discriminate. - (* short offset *) - case (Int.eq (high_s ofs) Int.zero). - exists (nextinstr (rs#(preg_of dst) <- v)). - split. apply exec_straight_one. apply loadind_aux_correct; auto. - unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso. auto. auto. - split. rewrite nextinstr_inv; auto. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. - (* long offset *) - pose (rs1 := nextinstr (rs#GPR12 <- (Val.add rs#base (Vint (Int.shl (high_s ofs) (Int.repr 16)))))). - exists (nextinstr (rs1#(preg_of dst) <- v)). - split. apply exec_straight_two with rs1 m. - simpl. rewrite gpr_or_zero_not_zero; auto. - apply loadind_aux_correct. - unfold rs1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - rewrite Val.add_assoc. simpl. rewrite low_high_s. assumption. - auto. discriminate. reflexivity. - unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso. auto. auto. - split. rewrite nextinstr_inv; auto. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. - unfold rs1. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. -Qed. - -(** Indexed memory stores. *) - -Lemma storeind_aux_correct: - forall (base: ireg) ofs ty src (rs: regset) m m', - Mem.storev (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) (rs#(preg_of src)) = Some m' -> - mreg_type src = ty -> - base <> GPR0 -> - exec_instr ge fn (storeind_aux src base ofs ty) rs m = - OK (nextinstr rs) m'. -Proof. - intros. unfold storeind_aux. unfold preg_of in H. rewrite H0 in H. destruct ty. - simpl. unfold store1. rewrite gpr_or_zero_not_zero; auto. - unfold const_low. simpl in H. rewrite H. auto. - simpl. unfold store1. rewrite gpr_or_zero_not_zero; auto. - unfold const_low. simpl in H. rewrite H. auto. -Qed. - -Lemma storeind_correct: - forall (base: ireg) ofs ty src k (rs: regset) m m', - Mem.storev (chunk_of_type ty) m (Val.add rs#base (Vint ofs)) (rs#(preg_of src)) = Some m' -> - mreg_type src = ty -> - base <> GPR0 -> - exists rs', - exec_straight (storeind src base ofs ty k) rs m k rs' m' - /\ forall r, r <> PC -> r <> GPR12 -> rs'#r = rs#r. -Proof. - intros. unfold storeind. - (* short offset *) - case (Int.eq (high_s ofs) Int.zero). - exists (nextinstr rs). - split. apply exec_straight_one. apply storeind_aux_correct; auto. - reflexivity. - intros. rewrite nextinstr_inv; auto. - (* long offset *) - pose (rs1 := nextinstr (rs#GPR12 <- (Val.add rs#base (Vint (Int.shl (high_s ofs) (Int.repr 16)))))). - exists (nextinstr rs1). - split. apply exec_straight_two with rs1 m. - simpl. rewrite gpr_or_zero_not_zero; auto. - apply storeind_aux_correct; auto with ppcgen. - unfold rs1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - rewrite nextinstr_inv; auto with ppcgen. - rewrite Pregmap.gso; auto with ppcgen. - rewrite Val.add_assoc. simpl. rewrite low_high_s. assumption. - reflexivity. reflexivity. - intros. rewrite nextinstr_inv; auto. - unfold rs1. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. -Qed. - -(** Float comparisons. *) - -Lemma floatcomp_correct: - forall cmp (r1 r2: freg) k rs m, - exists rs', - exec_straight (floatcomp cmp r1 r2 k) rs m k rs' m - /\ rs'#(reg_of_crbit (fst (crbit_for_fcmp cmp))) = - (if snd (crbit_for_fcmp cmp) - then Val.cmpf cmp rs#r1 rs#r2 - else Val.notbool (Val.cmpf cmp rs#r1 rs#r2)) - /\ forall r', - r' <> PC -> r' <> CR0_0 -> r' <> CR0_1 -> - r' <> CR0_2 -> r' <> CR0_3 -> rs'#r' = rs#r'. -Proof. - intros. - generalize (compare_float_spec rs rs#r1 rs#r2). - intros [A [B [C D]]]. - set (rs1 := nextinstr (compare_float rs rs#r1 rs#r2)) in *. - assert ((cmp = Ceq \/ cmp = Cne \/ cmp = Clt \/ cmp = Cgt) - \/ (cmp = Cle \/ cmp = Cge)). - case cmp; tauto. - unfold floatcomp. elim H; intro; clear H. - exists rs1. - split. generalize H0; intros [EQ|[EQ|[EQ|EQ]]]; subst cmp; - apply exec_straight_one; reflexivity. - split. - generalize H0; intros [EQ|[EQ|[EQ|EQ]]]; subst cmp; simpl; auto. - rewrite Val.negate_cmpf_eq. auto. - auto. - (* two instrs *) - exists (nextinstr (rs1#CR0_3 <- (Val.cmpf cmp rs#r1 rs#r2))). - split. elim H0; intro; subst cmp. - apply exec_straight_two with rs1 m. - reflexivity. simpl. - rewrite C; rewrite A. rewrite Val.or_commut. rewrite <- Val.cmpf_le. - reflexivity. reflexivity. reflexivity. - apply exec_straight_two with rs1 m. - reflexivity. simpl. - rewrite C; rewrite B. rewrite Val.or_commut. rewrite <- Val.cmpf_ge. - reflexivity. reflexivity. reflexivity. - split. elim H0; intro; subst cmp; simpl. - reflexivity. - reflexivity. - intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. -Qed. - -Ltac TypeInv := - match goal with - | H: (List.map ?f ?x = nil) |- _ => - destruct x; [clear H | simpl in H; discriminate] - | H: (List.map ?f ?x = ?hd :: ?tl) |- _ => - destruct x; simpl in H; - [ discriminate | - injection H; clear H; let T := fresh "T" in ( - intros H T; TypeInv) ] - | _ => idtac - end. - -(** Translation of conditions. *) - -Lemma transl_cond_correct_aux: - forall cond args k ms sp 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 ms args) - else Val.notbool (eval_condition_total cond (map ms args))) - /\ agree ms sp rs'. -Proof. - intros. destruct cond; simpl in H; TypeInv. - (* Ccomp *) - simpl. - generalize (compare_sint_spec rs ms#m0 ms#m1). - intros [A [B [C D]]]. - exists (nextinstr (compare_sint rs ms#m0 ms#m1)). - split. apply exec_straight_one. simpl. - repeat (rewrite <- (ireg_val ms sp rs); auto). - reflexivity. - split. - case c; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto. - apply agree_exten_2 with rs; auto. - (* Ccompu *) - simpl. - generalize (compare_uint_spec rs ms#m0 ms#m1). - intros [A [B [C D]]]. - exists (nextinstr (compare_uint rs ms#m0 ms#m1)). - split. apply exec_straight_one. simpl. - repeat (rewrite <- (ireg_val ms sp rs); auto). - reflexivity. - split. - case c; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto. - apply agree_exten_2 with rs; auto. - (* Ccompimm *) - simpl. - case (Int.eq (high_s i) Int.zero). - generalize (compare_sint_spec rs ms#m0 (Vint i)). - intros [A [B [C D]]]. - exists (nextinstr (compare_sint rs ms#m0 (Vint i))). - split. apply exec_straight_one. simpl. - repeat (rewrite <- (ireg_val ms sp rs); auto). - reflexivity. - split. - case c; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto. - apply agree_exten_2 with rs; auto. - generalize (loadimm_correct GPR12 i (Pcmpw (ireg_of m0) GPR12 :: k) rs m). - intros [rs1 [EX1 [RES1 OTH1]]]. - assert (agree ms sp rs1). apply agree_exten_2 with rs; auto. - generalize (compare_sint_spec rs1 ms#m0 (Vint i)). - intros [A [B [C D]]]. - exists (nextinstr (compare_sint rs1 ms#m0 (Vint i))). - split. eapply exec_straight_trans. eexact EX1. - apply exec_straight_one. simpl. - repeat (rewrite <- (ireg_val ms sp rs1); auto). rewrite RES1. - reflexivity. reflexivity. - split. - case c; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto. - apply agree_exten_2 with rs1; auto. - (* Ccompuimm *) - simpl. - case (Int.eq (high_u i) Int.zero). - generalize (compare_uint_spec rs ms#m0 (Vint i)). - intros [A [B [C D]]]. - exists (nextinstr (compare_uint rs ms#m0 (Vint i))). - split. apply exec_straight_one. simpl. - repeat (rewrite <- (ireg_val ms sp rs); auto). - reflexivity. - split. - case c; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto. - apply agree_exten_2 with rs; auto. - generalize (loadimm_correct GPR12 i (Pcmplw (ireg_of m0) GPR12 :: k) rs m). - intros [rs1 [EX1 [RES1 OTH1]]]. - assert (agree ms sp rs1). apply agree_exten_2 with rs; auto. - generalize (compare_uint_spec rs1 ms#m0 (Vint i)). - intros [A [B [C D]]]. - exists (nextinstr (compare_uint rs1 ms#m0 (Vint i))). - split. eapply exec_straight_trans. eexact EX1. - apply exec_straight_one. simpl. - repeat (rewrite <- (ireg_val ms sp rs1); auto). rewrite RES1. - reflexivity. reflexivity. - split. - case c; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto. - apply agree_exten_2 with rs1; auto. - (* Ccompf *) - simpl. - generalize (floatcomp_correct c (freg_of m0) (freg_of m1) k rs m). - intros [rs' [EX [RES OTH]]]. - exists rs'. split. auto. - split. rewrite RES. repeat (rewrite <- (freg_val ms sp rs); auto). - apply agree_exten_2 with rs; auto. - (* Cnotcompf *) - simpl. - generalize (floatcomp_correct c (freg_of m0) (freg_of m1) k rs m). - intros [rs' [EX [RES OTH]]]. - exists rs'. split. auto. - split. rewrite RES. repeat (rewrite <- (freg_val ms sp rs); auto). - assert (forall v1 v2, Val.notbool (Val.notbool (Val.cmpf c v1 v2)) = Val.cmpf c v1 v2). - intros v1 v2; unfold Val.cmpf; destruct v1; destruct v2; auto. - apply Val.notbool_idem2. - rewrite H. - generalize RES. case (snd (crbit_for_fcmp c)); simpl; auto. - apply agree_exten_2 with rs; auto. - (* Cmaskzero *) - simpl. - generalize (andimm_correct GPR12 (ireg_of m0) i k rs m (ireg_of_not_GPR12 m0)). - intros [rs' [A [B [C D]]]]. - exists rs'. split. assumption. - split. rewrite C. rewrite <- (ireg_val ms sp rs); auto. - apply agree_exten_2 with rs; auto. - (* Cmasknotzero *) - simpl. - generalize (andimm_correct GPR12 (ireg_of m0) i k rs m (ireg_of_not_GPR12 m0)). - intros [rs' [A [B [C D]]]]. - exists rs'. split. assumption. - split. rewrite C. rewrite <- (ireg_val ms sp rs); auto. - rewrite Val.notbool_idem3. reflexivity. - apply agree_exten_2 with rs; auto. -Qed. - -Lemma transl_cond_correct: - forall cond args k ms sp rs m b, - map mreg_type args = type_of_condition cond -> - agree ms sp rs -> - eval_condition cond (map ms 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)) - /\ agree ms sp rs'. -Proof. - intros. rewrite <- (eval_condition_weaken _ _ _ H1). - apply transl_cond_correct_aux; auto. -Qed. - -(** Translation of arithmetic operations. *) - -Ltac TranslOpSimpl := - match goal with - | |- 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; - [ repeat (rewrite (ireg_val ms sp rs); auto); reflexivity - | reflexivity ] - | auto with ppcgen ]) - || - (exists (nextinstr (rs#(freg_of res) <- v)); - split; - [ apply exec_straight_one; - [ repeat (rewrite (freg_val ms sp rs); auto); reflexivity - | reflexivity ] - | auto with ppcgen ]) - end. - -Lemma transl_op_correct: - forall op args res k ms sp rs m v, - wt_instr (Mop op args res) -> - agree ms sp rs -> - eval_operation ge sp op (map ms args) m = Some v -> - exists rs', - exec_straight (transl_op op args res k) rs m k rs' m - /\ agree (Regmap.set res v ms) sp rs'. -Proof. - intros. rewrite <- (eval_operation_weaken _ _ _ _ _ H1). clear H1; clear v. - inversion H. - (* Omove *) - simpl. exists (nextinstr (rs#(preg_of res) <- (ms r1))). - split. caseEq (mreg_type r1); intro. - apply exec_straight_one. simpl. rewrite (ireg_val ms sp rs); auto. - simpl. unfold preg_of. rewrite <- H2. rewrite H5. reflexivity. - auto with ppcgen. - apply exec_straight_one. simpl. rewrite (freg_val ms sp rs); auto. - simpl. unfold preg_of. rewrite <- H2. rewrite H5. reflexivity. - auto with ppcgen. - auto with ppcgen. - (* Other instructions *) - clear H1; clear H2; clear H4. - destruct op; simpl in H5; injection H5; clear H5; intros; - TypeInv; simpl; try (TranslOpSimpl). - (* Omove again *) - congruence. - (* Ointconst *) - generalize (loadimm_correct (ireg_of res) i k rs m). - intros [rs' [A [B C]]]. - exists rs'. split. auto. - apply agree_set_mireg_exten with rs; auto. - (* Ofloatconst *) - exists (nextinstr (rs#(freg_of res) <- (Vfloat f) #GPR12 <- Vundef)). - split. apply exec_straight_one. reflexivity. reflexivity. - auto with ppcgen. - (* Oaddrsymbol *) - change (find_symbol_offset ge i i0) with (symbol_offset ge i i0). - set (v := symbol_offset ge i i0). - 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. apply agree_nextinstr. - apply agree_set_other. auto. simpl. tauto. - (* Oaddrstack *) - assert (GPR1 <> GPR12). discriminate. - generalize (addimm_correct (ireg_of res) GPR1 i k rs m H2). - intros [rs' [EX [RES OTH]]]. - exists rs'. split. auto. - apply agree_set_mireg_exten with rs; auto. - rewrite (sp_val ms sp rs). auto. auto. - (* Ocast8unsigned *) - exists (nextinstr (rs#(ireg_of res) <- (Val.rolm (ms m0) Int.zero (Int.repr 255)))). - split. apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs)); auto. reflexivity. - replace (Val.zero_ext 8 (ms m0)) - with (Val.rolm (ms m0) Int.zero (Int.repr 255)). - auto with ppcgen. - unfold Val.rolm, Val.zero_ext. destruct (ms m0); auto. - rewrite Int.rolm_zero. rewrite Int.zero_ext_and. auto. compute; auto. - (* Ocast16unsigned *) - exists (nextinstr (rs#(ireg_of res) <- (Val.rolm (ms m0) Int.zero (Int.repr 65535)))). - split. apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs)); auto. reflexivity. - replace (Val.zero_ext 16 (ms m0)) - with (Val.rolm (ms m0) Int.zero (Int.repr 65535)). - auto with ppcgen. - unfold Val.rolm, Val.zero_ext. destruct (ms m0); auto. - rewrite Int.rolm_zero. rewrite Int.zero_ext_and. auto. compute; auto. - (* Oaddimm *) - generalize (addimm_correct (ireg_of res) (ireg_of m0) i k rs m - (ireg_of_not_GPR12 m0)). - intros [rs' [A [B C]]]. - exists rs'. split. auto. - apply agree_set_mireg_exten with rs; auto. - rewrite (ireg_val ms sp rs); auto. - (* Osub *) - exists (nextinstr (rs#(ireg_of res) <- (Val.sub (ms m0) (ms m1)) #CARRY <- Vundef)). - split. apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs); auto). - simpl. reflexivity. auto with ppcgen. - (* Osubimm *) - case (Int.eq (high_s i) Int.zero). - exists (nextinstr (rs#(ireg_of res) <- (Val.sub (Vint i) (ms m0)) #CARRY <- Vundef)). - split. apply exec_straight_one. rewrite (ireg_val ms sp rs); auto. - reflexivity. simpl. auto with ppcgen. - generalize (loadimm_correct GPR12 i (Psubfc (ireg_of res) (ireg_of m0) GPR12 :: k) rs m). - intros [rs1 [EX [RES OTH]]]. - assert (agree ms sp rs1). apply agree_exten_2 with rs; auto. - exists (nextinstr (rs1#(ireg_of res) <- (Val.sub (Vint i) (ms m0)) #CARRY <- Vundef)). - split. eapply exec_straight_trans. eexact EX. - apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs); auto). - simpl. rewrite RES. rewrite OTH. reflexivity. - generalize (ireg_of_not_GPR12 m0); congruence. - discriminate. - reflexivity. simpl; auto with ppcgen. - (* Omulimm *) - case (Int.eq (high_s i) Int.zero). - exists (nextinstr (rs#(ireg_of res) <- (Val.mul (ms m0) (Vint i)))). - split. apply exec_straight_one. rewrite (ireg_val ms sp rs); auto. - reflexivity. auto with ppcgen. - generalize (loadimm_correct GPR12 i (Pmullw (ireg_of res) (ireg_of m0) GPR12 :: k) rs m). - intros [rs1 [EX [RES OTH]]]. - assert (agree ms sp rs1). apply agree_exten_2 with rs; auto. - exists (nextinstr (rs1#(ireg_of res) <- (Val.mul (ms m0) (Vint i)))). - split. eapply exec_straight_trans. eexact EX. - apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs); auto). - simpl. rewrite RES. rewrite OTH. reflexivity. - generalize (ireg_of_not_GPR12 m0); congruence. - discriminate. - reflexivity. simpl; auto with ppcgen. - (* Oand *) - pose (v := Val.and (ms m0) (ms m1)). - 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. - unfold rs1, v. repeat (rewrite (ireg_val ms sp rs); auto). - reflexivity. - apply agree_exten_2 with rs1. unfold rs1, v; auto with ppcgen. - auto. - (* Oandimm *) - generalize (andimm_correct (ireg_of res) (ireg_of m0) i k rs m - (ireg_of_not_GPR12 m0)). - intros [rs' [A [B [C D]]]]. - exists rs'. split. auto. apply agree_set_mireg_exten with rs; auto. - rewrite (ireg_val ms sp rs); auto. - (* Oorimm *) - generalize (orimm_correct (ireg_of res) (ireg_of m0) i k rs m). - intros [rs' [A [B C]]]. - exists rs'. split. auto. apply agree_set_mireg_exten with rs; auto. - rewrite (ireg_val ms sp rs); auto. - (* Oxorimm *) - generalize (xorimm_correct (ireg_of res) (ireg_of m0) i k rs m). - intros [rs' [A [B C]]]. - exists rs'. split. auto. apply agree_set_mireg_exten with rs; auto. - rewrite (ireg_val ms sp rs); auto. - (* Oshr *) - exists (nextinstr (rs#(ireg_of res) <- (Val.shr (ms m0) (ms m1)) #CARRY <- (Val.shr_carry (ms m0) (ms m1)))). - split. apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs); auto). - reflexivity. auto with ppcgen. - (* Oshrimm *) - exists (nextinstr (rs#(ireg_of res) <- (Val.shr (ms m0) (Vint i)) #CARRY <- (Val.shr_carry (ms m0) (Vint i)))). - split. apply exec_straight_one. repeat (rewrite (ireg_val ms sp rs); auto). - reflexivity. auto with ppcgen. - (* Oxhrximm *) - pose (rs1 := nextinstr (rs#(ireg_of res) <- (Val.shr (ms m0) (Vint i)) #CARRY <- (Val.shr_carry (ms m0) (Vint i)))). - exists (nextinstr (rs1#(ireg_of res) <- (Val.shrx (ms m0) (Vint i)))). - split. apply exec_straight_two with rs1 m. - unfold rs1; rewrite (ireg_val ms sp rs); auto. - simpl; unfold rs1; repeat rewrite <- (ireg_val ms sp rs); auto. - repeat (rewrite nextinstr_inv; try discriminate). - repeat rewrite Pregmap.gss. decEq. decEq. - apply (f_equal3 (@Pregmap.set val)); auto. - rewrite Pregmap.gso. rewrite Pregmap.gss. apply Val.shrx_carry. - discriminate. reflexivity. reflexivity. - apply agree_exten_2 with (rs#(ireg_of res) <- (Val.shrx (ms m0) (Vint i))). - auto with ppcgen. - intros. rewrite nextinstr_inv; auto. - case (preg_eq (ireg_of res) r); intro. - subst r. repeat rewrite Pregmap.gss. auto. - repeat rewrite Pregmap.gso; auto. - unfold rs1. rewrite nextinstr_inv; auto. - repeat rewrite Pregmap.gso; auto. - (* Ointoffloat *) - exists (nextinstr (rs#(ireg_of res) <- (Val.intoffloat (ms m0)) #FPR13 <- Vundef)). - split. apply exec_straight_one. - repeat (rewrite (freg_val ms sp rs); auto). - reflexivity. auto with ppcgen. - (* Ointuoffloat *) - exists (nextinstr (rs#(ireg_of res) <- (Val.intuoffloat (ms m0)) #FPR13 <- Vundef)). - split. apply exec_straight_one. - repeat (rewrite (freg_val ms sp rs); auto). - reflexivity. auto with ppcgen. - (* Ofloatofint *) - exists (nextinstr (rs#(freg_of res) <- (Val.floatofint (ms m0)) #GPR12 <- Vundef #FPR13 <- Vundef)). - split. apply exec_straight_one. - repeat (rewrite (ireg_val ms sp rs); auto). - reflexivity. auto 10 with ppcgen. - (* Ofloatofintu *) - exists (nextinstr (rs#(freg_of res) <- (Val.floatofintu (ms m0)) #GPR12 <- Vundef #FPR13 <- Vundef)). - split. apply exec_straight_one. - repeat (rewrite (ireg_val ms sp rs); auto). - reflexivity. auto 10 with ppcgen. - (* Ocmp *) - set (bit := fst (crbit_for_cond c)). - set (isset := snd (crbit_for_cond c)). - 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 c args k1 ms sp rs m H2 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. - exists (nextinstr (rs2#(ireg_of res) <- (eval_condition_total c ms##args))). - split. apply exec_straight_trans with k1 rs1 m. assumption. - unfold k1. apply exec_straight_two with rs2 m. - reflexivity. simpl. - replace (Val.xor (rs2 (ireg_of res)) (Vint Int.one)) - with (eval_condition_total c ms##args). - reflexivity. - unfold rs2. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - rewrite RES1. apply Val.notbool_xor. apply eval_condition_total_is_bool. - reflexivity. reflexivity. - unfold rs2. auto with ppcgen. -Qed. - -Lemma transl_load_store_correct: - forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction) - addr args k ms sp rs m ms' m', - (forall cst (r1: ireg) (rs1: regset) k, - eval_addressing_total ge sp addr (map ms args) = Val.add rs1#r1 (const_low ge cst) -> - agree ms sp rs1 -> - r1 <> GPR0 -> - exists rs', - exec_straight (mk1 cst r1 :: k) rs1 m k rs' m' /\ - agree ms' sp rs') -> - (forall (r1 r2: ireg) (rs1: regset) k, - eval_addressing_total ge sp addr (map ms args) = Val.add rs1#r1 rs1#r2 -> - agree ms sp rs1 -> - exists rs', - exec_straight (mk2 r1 r2 :: k) rs1 m k rs' m' /\ - agree ms' sp rs') -> - agree ms sp rs -> - map mreg_type args = type_of_addressing addr -> - exists rs', - exec_straight (transl_load_store mk1 mk2 addr args k) rs m - k rs' m' - /\ agree ms' sp rs'. -Proof. - intros. destruct addr; simpl in H2; TypeInv; simpl. - (* Aindexed *) - case (ireg_eq (ireg_of t) GPR0); intro. - (* Aindexed from GPR0 *) - set (rs1 := nextinstr (rs#GPR12 <- (ms t))). - set (rs2 := nextinstr (rs1#GPR12 <- (Val.add (ms t) (Vint (Int.shl (high_s i) (Int.repr 16)))))). - assert (ADDR: eval_addressing_total ge sp (Aindexed i) ms##(t :: nil) = - Val.add rs2#GPR12 (const_low ge (Cint (low_s i)))). - simpl. unfold rs2. rewrite nextinstr_inv. rewrite Pregmap.gss. - rewrite Val.add_assoc. simpl. rewrite low_high_s. auto. - discriminate. - assert (AG: agree ms sp rs2). unfold rs2, rs1; auto 6 with ppcgen. - assert (NOT0: GPR12 <> GPR0). discriminate. - generalize (H _ _ _ k ADDR AG NOT0). - intros [rs' [EX' AG']]. - exists rs'. split. - apply exec_straight_trans with (mk1 (Cint (low_s i)) GPR12 :: k) rs2 m. - apply exec_straight_two with rs1 m. - unfold rs1. rewrite (ireg_val ms sp rs); auto. - unfold rs2. replace (ms t) with (rs1#GPR12). auto. - unfold rs1. rewrite nextinstr_inv. apply Pregmap.gss. discriminate. - reflexivity. reflexivity. - assumption. assumption. - (* Aindexed short *) - case (Int.eq (high_s i) Int.zero). - assert (ADDR: eval_addressing_total ge sp (Aindexed i) ms##(t :: nil) = - Val.add rs#(ireg_of t) (const_low ge (Cint i))). - simpl. rewrite (ireg_val ms sp rs); auto. - generalize (H _ _ _ k ADDR H1 n). intros [rs' [EX' AG']]. - exists rs'. split. auto. auto. - (* Aindexed long *) - set (rs1 := nextinstr (rs#GPR12 <- (Val.add (ms t) (Vint (Int.shl (high_s i) (Int.repr 16)))))). - assert (ADDR: eval_addressing_total ge sp (Aindexed i) ms##(t :: nil) = - Val.add rs1#GPR12 (const_low ge (Cint (low_s i)))). - simpl. unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss. - rewrite Val.add_assoc. simpl. rewrite low_high_s. auto. - discriminate. - assert (AG: agree ms sp rs1). unfold rs1; auto with ppcgen. - assert (NOT0: GPR12 <> GPR0). discriminate. - generalize (H _ _ _ k ADDR AG NOT0). intros [rs' [EX' AG']]. - exists rs'. split. apply exec_straight_step with rs1 m. - simpl. rewrite gpr_or_zero_not_zero; auto. - rewrite <- (ireg_val ms sp rs); auto. reflexivity. - assumption. assumption. - (* Aindexed2 *) - apply H0. - simpl. repeat (rewrite (ireg_val ms sp rs); auto). auto. - (* Aglobal *) - set (rs1 := nextinstr (rs#GPR12 <- (const_high ge (Csymbol_high i i0)))). - assert (ADDR: eval_addressing_total ge sp (Aglobal i i0) ms##nil = - Val.add rs1#GPR12 (const_low ge (Csymbol_low i i0))). - simpl. unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss. - unfold const_high, const_low. - set (v := symbol_offset ge i i0). - symmetry. rewrite Val.add_commut. unfold v. apply low_high_half. - discriminate. - assert (AG: agree ms sp rs1). unfold rs1; auto with ppcgen. - assert (NOT0: GPR12 <> GPR0). discriminate. - generalize (H _ _ _ k ADDR AG NOT0). intros [rs' [EX' AG']]. - exists rs'. split. apply exec_straight_step with rs1 m. - unfold exec_instr. rewrite gpr_or_zero_zero. - rewrite Val.add_commut. unfold const_high. - rewrite high_half_zero. - reflexivity. reflexivity. - assumption. assumption. - (* Abased *) - assert (COMMON: - forall (rs1: regset) r, - r <> GPR0 -> - ms t = rs1#r -> - agree ms sp rs1 -> - exists rs', - exec_straight - (Paddis GPR12 r (Csymbol_high i i0) - :: mk1 (Csymbol_low i i0) GPR12 :: k) rs1 m k rs' m' - /\ agree ms' sp rs'). - intros. - set (rs2 := nextinstr (rs1#GPR12 <- (Val.add (ms t) (const_high ge (Csymbol_high i i0))))). - assert (ADDR: eval_addressing_total ge sp (Abased i i0) ms##(t::nil) = - Val.add rs2#GPR12 (const_low ge (Csymbol_low i i0))). - simpl. unfold rs2. rewrite nextinstr_inv. rewrite Pregmap.gss. - unfold const_high. - set (v := symbol_offset ge i i0). - rewrite Val.add_assoc. - rewrite (Val.add_commut (high_half v)). - unfold v. rewrite low_high_half. apply Val.add_commut. - discriminate. - assert (AG: agree ms sp rs2). unfold rs2; auto with ppcgen. - assert (NOT0: GPR12 <> GPR0). discriminate. - generalize (H _ _ _ k ADDR AG NOT0). intros [rs' [EX' AG']]. - exists rs'. split. apply exec_straight_step with rs2 m. - unfold exec_instr. rewrite gpr_or_zero_not_zero; auto. - rewrite <- H3. reflexivity. reflexivity. - assumption. assumption. - case (ireg_eq (ireg_of t) GPR0); intro. - set (rs1 := nextinstr (rs#GPR12 <- (ms t))). - assert (R1: GPR12 <> GPR0). discriminate. - assert (R2: ms t = rs1 GPR12). - unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss; auto. - discriminate. - assert (R3: agree ms sp rs1). unfold rs1; auto with ppcgen. - generalize (COMMON rs1 GPR12 R1 R2 R3). intros [rs' [EX' AG']]. - exists rs'. split. - apply exec_straight_step with rs1 m. - unfold rs1. rewrite (ireg_val ms sp rs); auto. reflexivity. - assumption. assumption. - apply COMMON; auto. eapply ireg_val; eauto. - (* Ainstack *) - case (Int.eq (high_s i) Int.zero). - apply H. simpl. rewrite (sp_val ms sp rs); auto. auto. - discriminate. - set (rs1 := nextinstr (rs#GPR12 <- (Val.add sp (Vint (Int.shl (high_s i) (Int.repr 16)))))). - assert (ADDR: eval_addressing_total ge sp (Ainstack i) ms##nil = - Val.add rs1#GPR12 (const_low ge (Cint (low_s i)))). - simpl. unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss. - rewrite Val.add_assoc. decEq. simpl. rewrite low_high_s. auto. - discriminate. - assert (AG: agree ms sp rs1). unfold rs1; auto with ppcgen. - assert (NOT0: GPR12 <> GPR0). discriminate. - generalize (H _ _ _ k ADDR AG NOT0). intros [rs' [EX' AG']]. - exists rs'. split. apply exec_straight_step with rs1 m. - simpl. rewrite gpr_or_zero_not_zero. - unfold rs1. rewrite (sp_val ms sp rs). reflexivity. - auto. discriminate. reflexivity. assumption. assumption. -Qed. - -(** Translation of memory loads. *) - -Lemma transl_load_correct: - forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction) - chunk addr args k ms sp rs m dst a v, - (forall cst (r1: ireg) (rs1: regset), - exec_instr ge fn (mk1 cst r1) rs1 m = - load1 ge chunk (preg_of dst) cst r1 rs1 m) -> - (forall (r1 r2: ireg) (rs1: regset), - exec_instr ge fn (mk2 r1 r2) rs1 m = - load2 chunk (preg_of dst) r1 r2 rs1 m) -> - agree ms sp rs -> - map mreg_type args = type_of_addressing addr -> - eval_addressing ge sp addr (map ms args) = Some a -> - Mem.loadv chunk m a = Some v -> - exists rs', - exec_straight (transl_load_store mk1 mk2 addr args k) rs m - k rs' m - /\ agree (Regmap.set dst v ms) sp rs'. -Proof. - intros. apply transl_load_store_correct with ms. - intros. exists (nextinstr (rs1#(preg_of dst) <- v)). - split. apply exec_straight_one. rewrite H. - unfold load1. rewrite gpr_or_zero_not_zero; auto. - rewrite <- (eval_addressing_weaken _ _ _ _ H3) in H4. - rewrite H5 in H4. rewrite H4. auto. - auto with ppcgen. auto with ppcgen. - intros. exists (nextinstr (rs1#(preg_of dst) <- v)). - split. apply exec_straight_one. rewrite H0. - unfold load2. - rewrite <- (eval_addressing_weaken _ _ _ _ H3) in H4. - rewrite H5 in H4. rewrite H4. auto. - auto with ppcgen. auto with ppcgen. - auto. auto. -Qed. - -(** Translation of memory stores. *) - -Lemma transl_store_correct: - forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction) - chunk addr args k ms sp rs m src a m', - (forall cst (r1: ireg) (rs1: regset), - exec_instr ge fn (mk1 cst r1) rs1 m = - store1 ge chunk (preg_of src) cst r1 rs1 m) -> - (forall (r1 r2: ireg) (rs1: regset), - exec_instr ge fn (mk2 r1 r2) rs1 m = - store2 chunk (preg_of src) r1 r2 rs1 m) -> - agree ms sp rs -> - map mreg_type args = type_of_addressing addr -> - eval_addressing ge sp addr (map ms args) = Some a -> - Mem.storev chunk m a (ms src) = Some m' -> - exists rs', - exec_straight (transl_load_store mk1 mk2 addr args k) rs m - k rs' m' - /\ agree ms sp rs'. -Proof. - intros. apply transl_load_store_correct with ms. - intros. exists (nextinstr rs1). - split. apply exec_straight_one. rewrite H. - unfold store1. rewrite gpr_or_zero_not_zero; auto. - rewrite <- (eval_addressing_weaken _ _ _ _ H3) in H4. - rewrite H5 in H4. elim H6; intros. rewrite H9 in H4. - rewrite H4. auto. - auto with ppcgen. auto with ppcgen. - intros. exists (nextinstr rs1). - split. apply exec_straight_one. rewrite H0. - unfold store2. - rewrite <- (eval_addressing_weaken _ _ _ _ H3) in H4. - rewrite H5 in H4. elim H6; intros. rewrite H8 in H4. - rewrite H4. auto. - auto with ppcgen. auto with ppcgen. - auto. auto. -Qed. - -(** Translation of allocations *) - -Lemma transl_alloc_correct: - forall ms sp rs sz m m' blk k, - agree ms sp rs -> - ms Conventions.loc_alloc_argument = Vint sz -> - Mem.alloc m 0 (Int.signed sz) = (m', blk) -> - let ms' := Regmap.set Conventions.loc_alloc_result (Vptr blk Int.zero) ms in - exists rs', - exec_straight (Pallocblock :: k) rs m k rs' m' - /\ agree ms' sp rs'. -Proof. - intros. - pose (rs' := nextinstr (rs#GPR3 <- (Vptr blk Int.zero) #LR <- (Val.add rs#PC Vone))). - exists rs'; split. - apply exec_straight_one. unfold exec_instr. - generalize (preg_val _ _ _ Conventions.loc_alloc_argument H). - unfold preg_of; intro. simpl in H2. rewrite <- H2. rewrite H0. - rewrite H1. reflexivity. - reflexivity. - unfold ms', rs'. apply agree_nextinstr. apply agree_set_other. - change (IR GPR3) with (preg_of Conventions.loc_alloc_result). - apply agree_set_mreg. auto. - simpl. tauto. -Qed. - -End STRAIGHTLINE. - |