diff options
Diffstat (limited to 'backend/PPCgenproof1.v')
| -rw-r--r-- | backend/PPCgenproof1.v | 1566 |
1 files changed, 1566 insertions, 0 deletions
diff --git a/backend/PPCgenproof1.v b/backend/PPCgenproof1.v new file mode 100644 index 0000000..30eb336 --- /dev/null +++ b/backend/PPCgenproof1.v @@ -0,0 +1,1566 @@ +(** 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 Machtyping. +Require Import PPC. +Require Import PPCgen. + +(** * Properties of low half/high half decomposition *) + +Lemma high_half_signed_zero: + forall v, Val.add (high_half_signed v) Vzero = high_half_signed v. +Proof. + intros. generalize (high_half_signed_type v). + rewrite Val.add_commut. + case (high_half_signed v); simpl; intros; try contradiction. + auto. + rewrite Int.add_commut; rewrite Int.add_zero; auto. + rewrite Int.add_zero; auto. +Qed. + +Lemma high_half_unsigned_zero: + forall v, Val.add (high_half_unsigned v) Vzero = high_half_unsigned v. +Proof. + intros. generalize (high_half_unsigned_type v). + rewrite Val.add_commut. + case (high_half_unsigned 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.cast16signed. + 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 GPR2 => 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_GPR2: + forall r, ireg_of r <> GPR2. +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_GPR2 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 GPR2 -> 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 GPR2 -> 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. + +(** * 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_refl: + forall c rs m, + exec_straight c rs m c rs m + | 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. auto. + intro. apply exec_straight_step with rs2 m2; auto. +Qed. + +Lemma 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. +Proof. + intros. apply exec_straight_step with rs2 m2. auto. auto. + apply exec_straight_refl. +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 <> GPR2 -> + 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' <> GPR2 -> r' <> PC -> rs'#r' = rs#r'. +Proof. + intros. unfold addimm_2. + generalize (loadimm_correct GPR2 n (Padd r1 r2 GPR2 :: 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 <> GPR2 -> + 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' <> GPR2 -> 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 <> GPR2 -> + 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' <> GPR2 -> 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 GPR2 n (Pand_ r1 r2 GPR2 :: 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 <> GPR2 -> 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#GPR2 <- (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 <> GPR2 -> 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#GPR2 <- (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 GPR2 i (Pcmpw (ireg_of m0) GPR2 :: 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 GPR2 i (Pcmplw (ireg_of m0) GPR2 :: 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 GPR2 (ireg_of m0) i k rs m (ireg_of_not_GPR2 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 GPR2 (ireg_of m0) i k rs m (ireg_of_not_GPR2 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) = 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) = 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. + (* Oundef *) + simpl. exists (nextinstr (rs#(preg_of res) <- Vundef)). + split. caseEq (mreg_type res); intro. + apply exec_straight_one. simpl. + unfold preg_of; rewrite H1. reflexivity. + auto with ppcgen. + apply exec_straight_one. simpl. + unfold preg_of; rewrite H1. reflexivity. + auto with ppcgen. + auto with ppcgen. + (* Other instructions *) + clear H1; clear H2; clear H3. + destruct op; simpl in H6; injection H6; clear H6; 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) #GPR2 <- Vundef)). + split. apply exec_straight_one. reflexivity. reflexivity. + auto with ppcgen. + (* Oaddrsymbol *) + set (v := find_symbol_offset ge i i0). + pose (rs1 := nextinstr (rs#(ireg_of res) <- (high_half_unsigned 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_unsigned_zero. reflexivity. + simpl. unfold rs1 at 1. rewrite nextinstr_inv; auto with ppcgen. + rewrite Pregmap.gss. + fold v. rewrite Val.or_commut. rewrite low_high_half_unsigned. + reflexivity. reflexivity. reflexivity. + unfold rs1. auto with ppcgen. + (* Oaddrstack *) + assert (GPR1 <> GPR2). 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. + (* Oundef again *) + congruence. + (* Oaddimm *) + generalize (addimm_correct (ireg_of res) (ireg_of m0) i k rs m + (ireg_of_not_GPR2 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 GPR2 i (Psubfc (ireg_of res) (ireg_of m0) GPR2 :: 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_GPR2 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 GPR2 i (Pmullw (ireg_of res) (ireg_of m0) GPR2 :: 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_GPR2 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_GPR2 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. + (* Ofloatofint *) + exists (nextinstr (rs#(freg_of res) <- (Val.floatofint (ms m0)) #GPR2 <- 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)) #GPR2 <- 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#GPR2 <- (ms t))). + set (rs2 := nextinstr (rs1#GPR2 <- (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#GPR2 (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: GPR2 <> 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)) GPR2 :: 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#GPR2). 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#GPR2 <- (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#GPR2 (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: GPR2 <> 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#GPR2 <- (const_high ge (Csymbol_high_signed i i0)))). + assert (ADDR: eval_addressing_total ge sp (Aglobal i i0) ms##nil = + Val.add rs1#GPR2 (const_low ge (Csymbol_low_signed 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. apply low_high_half_signed. + discriminate. + assert (AG: agree ms sp rs1). unfold rs1; auto with ppcgen. + assert (NOT0: GPR2 <> 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_signed_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 GPR2 r (Csymbol_high_signed i i0) + :: mk1 (Csymbol_low_signed i i0) GPR2 :: k) rs1 m k rs' m' + /\ agree ms' sp rs'). + intros. + set (rs2 := nextinstr (rs1#GPR2 <- (Val.add (ms t) (const_high ge (Csymbol_high_signed i i0))))). + assert (ADDR: eval_addressing_total ge sp (Abased i i0) ms##(t::nil) = + Val.add rs2#GPR2 (const_low ge (Csymbol_low_signed 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_signed v)). + rewrite low_high_half_signed. apply Val.add_commut. + discriminate. + assert (AG: agree ms sp rs2). unfold rs2; auto with ppcgen. + assert (NOT0: GPR2 <> 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#GPR2 <- (ms t))). + assert (R1: GPR2 <> GPR0). discriminate. + assert (R2: ms t = rs1 GPR2). + unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss; auto. + discriminate. + assert (R3: agree ms sp rs1). unfold rs1; auto with ppcgen. + generalize (COMMON rs1 GPR2 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#GPR2 <- (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#GPR2 (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: GPR2 <> 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. + +End STRAIGHTLINE. + |