From 5020a5a07da3fd690f5d171a48d0c73ef48f9430 Mon Sep 17 00:00:00 2001 From: xleroy Date: Fri, 1 Mar 2013 15:32:13 +0000 Subject: Revised Stacking and Asmgen passes and Mach semantics: - no more prediction of return addresses (Asmgenretaddr is gone) - instead, punch a hole for the retaddr in Mach stack frame and fill this hole with the return address in the Asmgen proof. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2129 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- powerpc/Asmgenproof1.v | 1424 +++++++++++++++++------------------------------- 1 file changed, 489 insertions(+), 935 deletions(-) (limited to 'powerpc/Asmgenproof1.v') diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 56cb224..1e16a0d 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -13,6 +13,7 @@ (** Correctness proof for PPC generation: auxiliary results. *) Require Import Coqlib. +Require Import Errors. Require Import Maps. Require Import AST. Require Import Integers. @@ -23,11 +24,10 @@ Require Import Globalenvs. Require Import Op. Require Import Locations. Require Import Mach. -Require Import Machsem. -Require Import Machtyping. Require Import Asm. Require Import Asmgen. Require Import Conventions. +Require Import Asmgenproof0. (** * Properties of low half/high half decomposition *) @@ -103,308 +103,7 @@ Proof. rewrite Int.sub_idem. apply Int.add_zero. Qed. -(** * Correspondence between Mach registers and PPC registers *) - -Hint Extern 2 (_ <> _) => discriminate: ppcgen. - -(** Mapping from Mach registers to PPC registers. *) - -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) : bool := - match r with - | IR GPR0 => false - | PC => false | LR => false | CTR => false - | CR0_0 => false | CR0_1 => false | CR0_2 => false | CR0_3 => false - | CARRY => false - | _ => true - end. - -Lemma ireg_of_is_data_reg: - forall (r: mreg), is_data_reg (ireg_of r) = true. -Proof. - destruct r; reflexivity. -Qed. - -Lemma freg_of_is_data_reg: - forall (r: mreg), is_data_reg (ireg_of r) = true. -Proof. - destruct r; reflexivity. -Qed. - -Lemma preg_of_is_data_reg: - forall (r: mreg), is_data_reg (preg_of r) = true. -Proof. - destruct r; reflexivity. -Qed. - -Lemma data_reg_diff: - forall r r', is_data_reg r = true -> is_data_reg r' = false -> r <> r'. -Proof. - intros. congruence. -Qed. - -Lemma ireg_diff: - forall r r', r <> r' -> IR r <> IR r'. -Proof. - intros. congruence. -Qed. - -Lemma diff_ireg: - forall r r', IR r <> IR r' -> r <> r'. -Proof. - intros. congruence. -Qed. - -Hint Resolve ireg_of_is_data_reg freg_of_is_data_reg preg_of_is_data_reg - data_reg_diff ireg_diff diff_ireg: ppcgen. - -Definition is_nontemp_reg (r: preg) : bool := - match r with - | IR GPR0 => false | IR GPR11 => false | IR GPR12 => false - | FR FPR0 => false | FR FPR12 => false | FR FPR13 => false - | PC => false | LR => false | CTR => false - | CR0_0 => false | CR0_1 => false | CR0_2 => false | CR0_3 => false - | CARRY => false - | _ => true - end. - -Remark is_nontemp_is_data: - forall r, is_nontemp_reg r = true -> is_data_reg r = true. -Proof. - destruct r; simpl; try congruence. destruct i; congruence. -Qed. - -Lemma nontemp_reg_diff: - forall r r', is_nontemp_reg r = true -> is_nontemp_reg r' = false -> r <> r'. -Proof. - intros. congruence. -Qed. - -Hint Resolve is_nontemp_is_data nontemp_reg_diff: ppcgen. - -Lemma ireg_of_not_GPR1: - forall r, ireg_of r <> GPR1. -Proof. - intro. case r; discriminate. -Qed. - -Lemma preg_of_not_GPR1: - forall r, preg_of r <> GPR1. -Proof. - intro. case r; discriminate. -Qed. -Hint Resolve ireg_of_not_GPR1 preg_of_not_GPR1: ppcgen. - -Lemma int_temp_for_diff: - forall r, IR(int_temp_for r) <> preg_of r. -Proof. - intros. unfold int_temp_for. destruct (mreg_eq r IT2). - subst r. compute. congruence. - change (IR GPR12) with (preg_of IT2). red; intros; elim n. - apply preg_of_injective; auto. -Qed. - -(** Agreement between Mach register sets and PPC register sets. *) - -Record agree (ms: Mach.regset) (sp: val) (rs: Asm.regset) : Prop := mkagree { - agree_sp: rs#GPR1 = sp; - agree_sp_def: sp <> Vundef; - agree_mregs: forall r: mreg, Val.lessdef (ms r) (rs#(preg_of r)) -}. - -Lemma preg_val: - forall ms sp rs r, - agree ms sp rs -> Val.lessdef (ms r) rs#(preg_of r). -Proof. - intros. eapply agree_mregs; eauto. -Qed. - -Lemma preg_vals: - forall ms sp rs rl, - agree ms sp rs -> Val.lessdef_list (List.map ms rl) (List.map rs (List.map preg_of rl)). -Proof. - induction rl; intros; simpl. - constructor. - constructor. eapply preg_val; eauto. eauto. -Qed. - -Lemma ireg_val: - forall ms sp rs r, - agree ms sp rs -> - mreg_type r = Tint -> - Val.lessdef (ms r) rs#(ireg_of r). -Proof. - intros. replace (IR (ireg_of r)) with (preg_of r). eapply preg_val; eauto. - unfold preg_of. rewrite H0. auto. -Qed. - -Lemma freg_val: - forall ms sp rs r, - agree ms sp rs -> - mreg_type r = Tfloat -> - Val.lessdef (ms r) rs#(freg_of r). -Proof. - intros. replace (FR (freg_of r)) with (preg_of r). eapply preg_val; eauto. - 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: - forall ms sp rs rs', - agree ms sp rs -> - (forall r, is_data_reg r = true -> rs'#r = rs#r) -> - agree ms sp rs'. -Proof. - intros. inv H. constructor; auto. - intros. rewrite H0; auto with ppcgen. -Qed. - -(** Preservation of register agreement under various assignments. *) - -Lemma agree_set_mreg: - forall ms sp rs r v rs', - agree ms sp rs -> - Val.lessdef v (rs'#(preg_of r)) -> - (forall r', is_data_reg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') -> - agree (Regmap.set r v ms) sp rs'. -Proof. - intros. inv H. constructor; auto with ppcgen. - intros. unfold Regmap.set. destruct (RegEq.eq r0 r). - subst r0. auto. - rewrite H1; auto with ppcgen. red; intros; elim n; apply preg_of_injective; auto. -Qed. -Hint Resolve agree_set_mreg: ppcgen. - -Lemma agree_set_mireg: - forall ms sp rs r v (rs': regset), - agree ms sp rs -> - Val.lessdef v (rs'#(ireg_of r)) -> - mreg_type r = Tint -> - (forall r', is_data_reg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') -> - agree (Regmap.set r v ms) sp rs'. -Proof. - intros. eapply agree_set_mreg; eauto. unfold preg_of; rewrite H1; auto. -Qed. -Hint Resolve agree_set_mireg: ppcgen. - -Lemma agree_set_mfreg: - forall ms sp rs r v (rs': regset), - agree ms sp rs -> - Val.lessdef v (rs'#(freg_of r)) -> - mreg_type r = Tfloat -> - (forall r', is_data_reg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') -> - agree (Regmap.set r v ms) sp rs'. -Proof. - intros. eapply agree_set_mreg; eauto. unfold preg_of; rewrite H1; auto. -Qed. - -Lemma agree_set_other: - forall ms sp rs r v, - agree ms sp rs -> - is_data_reg r = false -> - agree ms sp (rs#r <- v). -Proof. - intros. apply agree_exten with rs. - auto. intros. apply Pregmap.gso. congruence. -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_undef_regs: - forall rl ms sp rs rs', - agree ms sp rs -> - (forall r, is_data_reg r = true -> ~In r (List.map preg_of rl) -> rs'#r = rs#r) -> - agree (undef_regs rl ms) sp rs'. -Proof. - induction rl; simpl; intros. - apply agree_exten with rs; auto. - apply IHrl with (rs#(preg_of a) <- (rs'#(preg_of a))). - apply agree_set_mreg with rs; auto with ppcgen. - intros. unfold Pregmap.set. destruct (PregEq.eq r' (preg_of a)). - congruence. auto. - intros. unfold Pregmap.set. destruct (PregEq.eq r (preg_of a)). - congruence. apply H0; auto. intuition congruence. -Qed. - -Lemma agree_undef_temps: - forall ms sp rs rs', - agree ms sp rs -> - (forall r, is_nontemp_reg r = true -> rs'#r = rs#r) -> - agree (undef_temps ms) sp rs'. -Proof. - unfold undef_temps. intros. apply agree_undef_regs with rs; auto. - simpl. unfold preg_of; simpl. intros. intuition. - apply H0. destruct r; simpl in *; auto. - destruct i; intuition. destruct f; intuition. -Qed. -Hint Resolve agree_undef_temps: ppcgen. - -Lemma agree_set_mreg_undef_temps: - forall ms sp rs r v rs', - agree ms sp rs -> - Val.lessdef v (rs'#(preg_of r)) -> - (forall r', is_nontemp_reg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') -> - agree (Regmap.set r v (undef_temps ms)) sp rs'. -Proof. - intros. apply agree_set_mreg with (rs'#(preg_of r) <- (rs#(preg_of r))). - apply agree_undef_temps with rs; auto. - intros. unfold Pregmap.set. destruct (PregEq.eq r0 (preg_of r)). - congruence. apply H1; auto. - auto. - intros. rewrite Pregmap.gso; auto. -Qed. - -Lemma agree_set_twice_mireg: - forall ms sp rs r v v1 v', - agree (Regmap.set r v1 ms) sp rs -> - mreg_type r = Tint -> - Val.lessdef v v' -> - agree (Regmap.set r v ms) sp (rs#(ireg_of r) <- v'). -Proof. - intros. inv H. - split. rewrite Pregmap.gso. auto. - generalize (ireg_of_not_GPR1 r); congruence. - auto. - intros. generalize (agree_mregs0 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. - -(** 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. +(** Useful properties of the GPR0 registers. *) Lemma gpr_or_zero_not_zero: forall rs r, r <> GPR0 -> gpr_or_zero rs r = rs#r. @@ -416,154 +115,40 @@ Lemma gpr_or_zero_zero: Proof. intros. reflexivity. Qed. -Hint Resolve gpr_or_zero_not_zero gpr_or_zero_zero: ppcgen. - -(** Connection between Mach and Asm calling conventions for external - functions. *) +Hint Resolve gpr_or_zero_not_zero gpr_or_zero_zero: asmgen. -Lemma extcall_arg_match: - forall ms sp rs m m' l v, - agree ms sp rs -> - Mem.extends m m' -> - Machsem.extcall_arg ms m sp l v -> - exists v', Asm.extcall_arg rs m' l v' /\ Val.lessdef v v'. +Lemma ireg_of_not_GPR0: + forall m r, ireg_of m = OK r -> IR r <> IR GPR0. Proof. - intros. inv H1. - exists (rs#(preg_of r)); split. constructor. eapply preg_val; eauto. - unfold load_stack in H2. - exploit Mem.loadv_extends; eauto. intros [v' [A B]]. - rewrite (sp_val _ _ _ H) in A. - exists v'; split; auto. - destruct ty; econstructor. - reflexivity. assumption. - reflexivity. assumption. + intros. erewrite <- ireg_of_eq; eauto with asmgen. Qed. +Hint Resolve ireg_of_not_GPR0: asmgen. -Lemma extcall_args_match: - forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' -> - forall ll vl, - list_forall2 (Machsem.extcall_arg ms m sp) ll vl -> - exists vl', list_forall2 (Asm.extcall_arg rs m') ll vl' /\ Val.lessdef_list vl vl'. +Lemma ireg_of_not_GPR0': + forall m r, ireg_of m = OK r -> r <> GPR0. Proof. - induction 3; intros. - exists (@nil val); split. constructor. constructor. - exploit extcall_arg_match; eauto. intros [v1' [A B]]. - destruct IHlist_forall2 as [vl' [C D]]. - exists (v1' :: vl'); split; constructor; auto. + intros. generalize (ireg_of_not_GPR0 _ _ H). congruence. Qed. +Hint Resolve ireg_of_not_GPR0': asmgen. -Lemma extcall_arguments_match: - forall ms m m' sp rs sg args, - agree ms sp rs -> Mem.extends m m' -> - Machsem.extcall_arguments ms m sp sg args -> - exists args', Asm.extcall_arguments rs m' sg args' /\ Val.lessdef_list args args'. -Proof. - unfold Machsem.extcall_arguments, Asm.extcall_arguments; intros. - eapply extcall_args_match; eauto. -Qed. +(** Useful simplification tactic *) -(** Translation of arguments to annotations. *) +Ltac Simplif := + ((rewrite nextinstr_inv by eauto with asmgen) + || (rewrite nextinstr_inv1 by eauto with asmgen) + || (rewrite Pregmap.gss) + || (rewrite nextinstr_pc) + || (rewrite Pregmap.gso by eauto with asmgen)); auto with asmgen. -Lemma annot_arg_match: - forall ms sp rs m m' p v, - agree ms sp rs -> - Mem.extends m m' -> - Machsem.annot_arg ms m sp p v -> - exists v', Asm.annot_arg rs m' (transl_annot_param p) v' /\ Val.lessdef v v'. -Proof. - intros. inv H1; simpl. -(* reg *) - exists (rs (preg_of r)); split. constructor. eapply preg_val; eauto. -(* stack *) - exploit Mem.load_extends; eauto. intros [v' [A B]]. - exists v'; split; auto. - inv H. econstructor; eauto. -Qed. +Ltac Simpl := repeat Simplif. -Lemma annot_arguments_match: - forall ms sp rs m m', agree ms sp rs -> Mem.extends m m' -> - forall pl vl, - Machsem.annot_arguments ms m sp pl vl -> - exists vl', Asm.annot_arguments rs m' (map transl_annot_param pl) vl' - /\ Val.lessdef_list vl vl'. -Proof. - induction 3; intros. - exists (@nil val); split. constructor. constructor. - exploit annot_arg_match; eauto. intros [v1' [A B]]. - destruct IHlist_forall2 as [vl' [C D]]. - exists (v1' :: vl'); split; constructor; auto. -Qed. - -(** * Execution of straight-line code *) +(** * Correctness of PowerPC constructor functions *) -Section STRAIGHTLINE. +Section CONSTRUCTORS. 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 *) - -Ltac SIMP := - (rewrite nextinstr_inv || rewrite Pregmap.gss || rewrite Pregmap.gso); auto with ppcgen. - (** Properties of comparisons. *) Lemma compare_float_spec: @@ -578,7 +163,7 @@ Proof. split. reflexivity. split. reflexivity. split. reflexivity. - intros. unfold compare_float. repeat SIMP. + intros. unfold compare_float. Simpl. Qed. Lemma compare_sint_spec: @@ -593,7 +178,7 @@ Proof. split. reflexivity. split. reflexivity. split. reflexivity. - intros. unfold compare_sint. repeat SIMP. + intros. unfold compare_sint. Simpl. Qed. Lemma compare_uint_spec: @@ -608,7 +193,7 @@ Proof. split. reflexivity. split. reflexivity. split. reflexivity. - intros. unfold compare_uint. repeat SIMP. + intros. unfold compare_uint. Simpl. Qed. (** Loading a constant. *) @@ -616,35 +201,25 @@ Qed. Lemma loadimm_correct: forall r n k rs m, exists rs', - exec_straight (loadimm r n k) rs m k rs' m + exec_straight ge fn (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_zero_l. auto. - reflexivity. - split. repeat SIMP. intros; repeat SIMP. + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + rewrite Int.add_zero_l. intuition Simpl. (* 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. repeat SIMP. intros; repeat SIMP. + econstructor; split. apply exec_straight_one. simpl; eauto. auto. + rewrite <- H. rewrite Int.add_commut. rewrite low_high_s. + intuition Simpl. (* 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_zero_l. reflexivity. - simpl. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - unfold Val.or. rewrite low_high_u. reflexivity. - reflexivity. reflexivity. - unfold rs1. split. repeat SIMP. intros; repeat SIMP. + econstructor; split. eapply exec_straight_two. + simpl; eauto. simpl; eauto. auto. auto. + split. Simpl. rewrite Int.add_zero_l. unfold Val.or. rewrite low_high_u. auto. + intros; Simpl. Qed. (** Add integer immediate. *) @@ -654,37 +229,31 @@ Lemma addimm_correct: r1 <> GPR0 -> r2 <> GPR0 -> exists rs', - exec_straight (addimm r1 r2 n k) rs m k rs' m + exec_straight ge fn (addimm 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. (* 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. repeat SIMP. intros. repeat SIMP. + econstructor; split. apply exec_straight_one. + simpl. rewrite gpr_or_zero_not_zero; eauto. + reflexivity. + intuition Simpl. (* 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. repeat SIMP. intros; repeat SIMP. + econstructor; split. apply exec_straight_one. + simpl. rewrite gpr_or_zero_not_zero; auto. auto. + split. Simpl. + generalize (low_high_s n). rewrite H1. rewrite Int.add_zero. congruence. + intros; Simpl. (* 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. - unfold rs1; split. repeat SIMP. intros; repeat SIMP. + econstructor; split. eapply exec_straight_two. + simpl. rewrite gpr_or_zero_not_zero; eauto. + simpl. rewrite gpr_or_zero_not_zero; eauto. + auto. auto. + split. Simpl. rewrite Val.add_assoc. simpl. rewrite low_high_s. auto. + intros; Simpl. Qed. (** And integer immediate. *) @@ -694,10 +263,10 @@ Lemma andimm_base_correct: r2 <> GPR0 -> let v := Val.and rs#r2 (Vint n) in exists rs', - exec_straight (andimm_base r1 r2 n k) rs m k rs' m + exec_straight ge fn (andimm_base r1 r2 n k) rs m k rs' m /\ rs'#r1 = v /\ rs'#CR0_2 = Val.cmp Ceq v Vzero - /\ forall r', is_data_reg r' = true -> r' <> r1 -> rs'#r' = rs#r'. + /\ forall r', data_preg r' = true -> r' <> r1 -> rs'#r' = rs#r'. Proof. intros. unfold andimm_base. case (Int.eq (high_u n) Int.zero). @@ -706,9 +275,9 @@ Proof. generalize (compare_sint_spec (rs#r1 <- v) v Vzero). intros [A [B [C D]]]. split. apply exec_straight_one. reflexivity. reflexivity. - split. rewrite D; auto with ppcgen. SIMP. + split. rewrite D; auto with asmgen. Simpl. split. auto. - intros. rewrite D; auto with ppcgen. SIMP. + intros. rewrite D; auto with asmgen. Simpl. (* andis *) generalize (Int.eq_spec (low_u n) Int.zero); case (Int.eq (low_u n) Int.zero); intro. @@ -718,9 +287,9 @@ Proof. split. apply exec_straight_one. simpl. generalize (low_high_u n). rewrite H0. rewrite Int.or_zero. intro. rewrite H1. reflexivity. reflexivity. - split. rewrite D; auto with ppcgen. SIMP. + split. rewrite D; auto with asmgen. Simpl. split. auto. - intros. rewrite D; auto with ppcgen. SIMP. + intros. rewrite D; auto with asmgen. Simpl. (* loadimm + and *) generalize (loadimm_correct GPR0 n (Pand_ r1 r2 GPR0 :: k) rs m). intros [rs1 [EX1 [RES1 OTHER1]]]. @@ -731,25 +300,24 @@ Proof. apply exec_straight_one. simpl. rewrite RES1. rewrite (OTHER1 r2). reflexivity. congruence. congruence. reflexivity. - split. rewrite D; auto with ppcgen. SIMP. + split. rewrite D; auto with asmgen. Simpl. split. auto. - intros. rewrite D; auto with ppcgen. SIMP. + intros. rewrite D; auto with asmgen. Simpl. Qed. Lemma andimm_correct: forall r1 r2 n k (rs : regset) m, r2 <> GPR0 -> exists rs', - exec_straight (andimm r1 r2 n k) rs m k rs' m + exec_straight ge fn (andimm r1 r2 n k) rs m k rs' m /\ rs'#r1 = Val.and rs#r2 (Vint n) - /\ forall r', is_data_reg r' = true -> r' <> r1 -> rs'#r' = rs#r'. + /\ forall r', data_preg r' = true -> r' <> r1 -> rs'#r' = rs#r'. Proof. intros. unfold andimm. destruct (is_rlw_mask n). (* turned into rlw *) - exists (nextinstr (rs#r1 <- (Val.and rs#r2 (Vint n)))). - split. apply exec_straight_one. simpl. rewrite Val.rolm_zero. auto. reflexivity. - split. SIMP. apply Pregmap.gss. - intros. SIMP. apply Pregmap.gso; auto with ppcgen. + econstructor; split. eapply exec_straight_one. + simpl. rewrite Val.rolm_zero. eauto. auto. + intuition Simpl. (* andimm_base *) destruct (andimm_base_correct r1 r2 n k rs m) as [rs' [A [B [C D]]]]; auto. exists rs'; auto. @@ -761,7 +329,7 @@ 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 + exec_straight ge fn (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. @@ -770,8 +338,7 @@ Proof. (* ori *) exists (nextinstr (rs#r1 <- v)). split. apply exec_straight_one. reflexivity. reflexivity. - split. repeat SIMP. - intros. repeat SIMP. + intuition Simpl. (* oris *) generalize (Int.eq_spec (low_u n) Int.zero); case (Int.eq (low_u n) Int.zero); intro. @@ -779,12 +346,11 @@ Proof. split. apply exec_straight_one. simpl. generalize (low_high_u n). rewrite H. rewrite Int.or_zero. intro. rewrite H0. reflexivity. reflexivity. - split. repeat SIMP. - intros. repeat SIMP. + intuition Simpl. (* oris + ori *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. - split. repeat rewrite nextinstr_inv; auto with ppcgen. repeat rewrite Pregmap.gss. rewrite Val.or_assoc. simpl. rewrite low_high_u. reflexivity. - intros. repeat SIMP. + intuition Simpl. + rewrite Val.or_assoc. simpl. rewrite low_high_u. reflexivity. Qed. (** Xor integer immediate. *) @@ -793,7 +359,7 @@ 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 + exec_straight ge fn (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. @@ -802,20 +368,19 @@ Proof. (* xori *) exists (nextinstr (rs#r1 <- v)). split. apply exec_straight_one. reflexivity. reflexivity. - split. repeat SIMP. intros. repeat SIMP. + intuition Simpl. (* 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. + generalize (low_high_u n). rewrite H. rewrite Int.or_zero. intro. rewrite H0. reflexivity. reflexivity. - split. repeat SIMP. intros. repeat SIMP. + intuition Simpl. (* xoris + xori *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. - split. repeat rewrite nextinstr_inv; auto with ppcgen. repeat rewrite Pregmap.gss. + intuition Simpl. rewrite Val.xor_assoc. simpl. rewrite low_high_u_xor. reflexivity. - intros. repeat SIMP. Qed. (** Rotate and mask. *) @@ -824,95 +389,108 @@ Lemma rolm_correct: forall r1 r2 amount mask k (rs : regset) m, r1 <> GPR0 -> exists rs', - exec_straight (rolm r1 r2 amount mask k) rs m k rs' m + exec_straight ge fn (rolm r1 r2 amount mask k) rs m k rs' m /\ rs'#r1 = Val.rolm rs#r2 amount mask - /\ forall r', is_data_reg r' = true -> r' <> r1 -> rs'#r' = rs#r'. + /\ forall r', data_preg r' = true -> r' <> r1 -> rs'#r' = rs#r'. Proof. intros. unfold rolm. destruct (is_rlw_mask mask). (* rlwinm *) - exists (nextinstr (rs#r1 <- (Val.rolm rs#r2 amount mask))). - split. apply exec_straight_one; auto. - split. SIMP. apply Pregmap.gss. - intros. SIMP. apply Pregmap.gso; auto. + econstructor; split. eapply exec_straight_one; simpl; eauto. + intuition Simpl. (* rlwinm ; andimm *) set (rs1 := nextinstr (rs#r1 <- (Val.rolm rs#r2 amount Int.mone))). destruct (andimm_base_correct r1 r1 mask k rs1 m) as [rs' [A [B [C D]]]]; auto. exists rs'. split. eapply exec_straight_step; eauto. auto. auto. - split. rewrite B. unfold rs1. SIMP. rewrite Pregmap.gss. - destruct (rs r2); simpl; auto. unfold Int.rolm. rewrite Int.and_assoc. + split. rewrite B. unfold rs1. rewrite nextinstr_inv; auto with asmgen. + rewrite Pregmap.gss. destruct (rs r2); simpl; auto. + unfold Int.rolm. rewrite Int.and_assoc. decEq; decEq; decEq. rewrite Int.and_commut. apply Int.and_mone. - intros. rewrite D; auto. unfold rs1; SIMP. apply Pregmap.gso; auto. + intros. rewrite D; auto. unfold rs1; Simpl. Qed. (** Indexed memory loads. *) Lemma loadind_correct: - forall (base: ireg) ofs ty dst k (rs: regset) m v, + forall (base: ireg) ofs ty dst k (rs: regset) m v c, + loadind base ofs ty dst k = OK c -> 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 + exec_straight ge fn c rs m k rs' m /\ rs'#(preg_of dst) = v /\ forall r, r <> PC -> r <> preg_of dst -> r <> GPR0 -> rs'#r = rs#r. Proof. - intros. unfold loadind. destruct (Int.eq (high_s ofs) Int.zero). -(* one load *) - exists (nextinstr (rs#(preg_of dst) <- v)); split. - unfold preg_of. rewrite H0. - destruct ty; apply exec_straight_one; auto with ppcgen; simpl. - unfold load1. rewrite gpr_or_zero_not_zero; auto. - simpl in *. rewrite H. auto. - unfold load1. rewrite gpr_or_zero_not_zero; auto. - simpl in *. rewrite H. auto. - split. repeat SIMP. intros. repeat SIMP. -(* loadimm + one load *) +Opaque Int.eq. + unfold loadind; intros. destruct ty; monadInv H; simpl in H0. +(* integer *) + rewrite (ireg_of_eq _ _ EQ). + destruct (Int.eq (high_s ofs) Int.zero). + (* one load *) + econstructor; split. apply exec_straight_one. simpl. + unfold load1. rewrite gpr_or_zero_not_zero; auto. simpl. rewrite H0. eauto. auto. + intuition Simpl. + (* loadimm + load *) + exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [A [B C]]]. + exists (nextinstr (rs'#x <- v)); split. + eapply exec_straight_trans. eexact A. apply exec_straight_one; auto. + simpl. unfold load2. rewrite C; auto with asmgen. rewrite B. rewrite H0. auto. + intuition Simpl. +(* float *) + rewrite (freg_of_eq _ _ EQ). + destruct (Int.eq (high_s ofs) Int.zero). + (* one load *) + econstructor; split. apply exec_straight_one. simpl. + unfold load1. rewrite gpr_or_zero_not_zero; auto. simpl. rewrite H0. eauto. auto. + intuition Simpl. + (* loadimm + load *) exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [A [B C]]]. - exists (nextinstr (rs'#(preg_of dst) <- v)); split. - eapply exec_straight_trans. eexact A. - unfold preg_of. rewrite H0. - destruct ty; apply exec_straight_one; auto with ppcgen; simpl. - unfold load2. rewrite B. rewrite C; auto with ppcgen. simpl in H. rewrite H. auto. - unfold load2. rewrite B. rewrite C; auto with ppcgen. simpl in H. rewrite H. auto. - split. repeat SIMP. - intros. repeat SIMP. + exists (nextinstr (rs'#x <- v)); split. + eapply exec_straight_trans. eexact A. apply exec_straight_one; auto. + simpl. unfold load2. rewrite C; auto with asmgen. rewrite B. rewrite H0. auto. + intuition Simpl. Qed. (** Indexed memory stores. *) Lemma storeind_correct: - forall (base: ireg) ofs ty src k (rs: regset) m m', + forall (base: ireg) ofs ty src k (rs: regset) m m' c, + storeind src base ofs ty k = OK c -> 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' + exec_straight ge fn c rs m k rs' m' /\ forall r, r <> PC -> r <> GPR0 -> rs'#r = rs#r. Proof. - intros. unfold storeind. destruct (Int.eq (high_s ofs) Int.zero). -(* one store *) - exists (nextinstr rs); split. - destruct ty; apply exec_straight_one; auto with ppcgen; simpl. - unfold store1. rewrite gpr_or_zero_not_zero; auto. - simpl in *. unfold preg_of in H; rewrite H0 in H. rewrite H. auto. - unfold store1. rewrite gpr_or_zero_not_zero; auto. - simpl in *. unfold preg_of in H; rewrite H0 in H. rewrite H. auto. - intros. apply nextinstr_inv; auto. -(* loadimm + one store *) + unfold storeind; intros. + assert (preg_of src <> GPR0) by auto with asmgen. + destruct ty; monadInv H; simpl in H0. +(* integer *) + rewrite (ireg_of_eq _ _ EQ) in *. + destruct (Int.eq (high_s ofs) Int.zero). + (* one store *) + econstructor; split. apply exec_straight_one. simpl. + unfold store1. rewrite gpr_or_zero_not_zero; auto. simpl. rewrite H0. eauto. auto. + intros; Simpl. + (* loadimm + store *) + exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [A [B C]]]. + exists (nextinstr rs'); split. + eapply exec_straight_trans. eexact A. apply exec_straight_one; auto. + simpl. unfold store2. rewrite B. rewrite ! C; auto with asmgen. rewrite H0. auto. + intuition Simpl. +(* float *) + rewrite (freg_of_eq _ _ EQ) in *. + destruct (Int.eq (high_s ofs) Int.zero). + (* one store *) + econstructor; split. apply exec_straight_one. simpl. + unfold store1. rewrite gpr_or_zero_not_zero; auto. simpl. rewrite H0. eauto. auto. + intuition Simpl. + (* loadimm + store *) exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [A [B C]]]. - assert (rs' base = rs base). apply C; auto with ppcgen. - assert (rs' (preg_of src) = rs (preg_of src)). apply C; auto with ppcgen. - exists (nextinstr rs'). - split. eapply exec_straight_trans. eexact A. - destruct ty; apply exec_straight_one; auto with ppcgen; simpl. - unfold store2. replace (IR (ireg_of src)) with (preg_of src). - rewrite H2; rewrite H3. rewrite B. simpl in H. rewrite H. auto. - unfold preg_of; rewrite H0; auto. - unfold store2. replace (FR (freg_of src)) with (preg_of src). - rewrite H2; rewrite H3. rewrite B. simpl in H. rewrite H. auto. - unfold preg_of; rewrite H0; auto. - intros. rewrite nextinstr_inv; auto. + exists (nextinstr rs'); split. + eapply exec_straight_trans. eexact A. apply exec_straight_one; auto. + simpl. unfold store2. rewrite B. rewrite ! C; auto with asmgen. rewrite H0. auto. + intuition Simpl. Qed. (** Float comparisons. *) @@ -920,7 +498,7 @@ Qed. 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 + exec_straight ge fn (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 @@ -938,10 +516,10 @@ Proof. case cmp; tauto. unfold floatcomp. elim H; intro; clear H. exists rs1. - split. generalize H0; intros [EQ|[EQ|[EQ|EQ]]]; subst cmp; + split. destruct H0 as [EQ|[EQ|[EQ|EQ]]]; subst cmp; apply exec_straight_one; reflexivity. split. - generalize H0; intros [EQ|[EQ|[EQ|EQ]]]; subst cmp; simpl; auto. + destruct H0 as [EQ|[EQ|[EQ|EQ]]]; subst cmp; simpl; auto. rewrite Val.negate_cmpf_eq. auto. auto. (* two instrs *) @@ -958,155 +536,132 @@ Proof. split. elim H0; intro; subst cmp; simpl. reflexivity. reflexivity. - intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. + intros. Simpl. 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. - -Ltac UseTypeInfo := - match goal with - | T: (mreg_type ?r = ?t), H: context[preg_of ?r] |- _ => - unfold preg_of in H; UseTypeInfo - | T: (mreg_type ?r = ?t), H: context[mreg_type ?r] |- _ => - rewrite T in H; UseTypeInfo - | T: (mreg_type ?r = ?t) |- context[preg_of ?r] => - unfold preg_of; UseTypeInfo - | T: (mreg_type ?r = ?t) |- context[mreg_type ?r] => - rewrite T; UseTypeInfo - | _ => idtac - end. - (** Translation of conditions. *) +Ltac ArgsInv := + repeat (match goal with + | [ H: Error _ = OK _ |- _ ] => discriminate + | [ H: match ?args with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct args + | [ H: bind _ _ = OK _ |- _ ] => monadInv H + | [ H: assertion _ = OK _ |- _ ] => monadInv H + end); + subst; + repeat (match goal with + | [ H: ireg_of _ = OK _ |- _ ] => simpl in *; rewrite (ireg_of_eq _ _ H) in * + | [ H: freg_of _ = OK _ |- _ ] => simpl in *; rewrite (freg_of_eq _ _ H) in * + end). + Lemma transl_cond_correct_1: - forall cond args k rs m, - map mreg_type args = type_of_condition cond -> + forall cond args k rs m c, + transl_cond cond args k = OK c -> exists rs', - exec_straight (transl_cond cond args k) rs m k rs' m + exec_straight ge fn c rs m k rs' m /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) = (if snd (crbit_for_cond cond) then Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m) else Val.notbool (Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m))) - /\ forall r, is_data_reg r = true -> rs'#r = rs#r. + /\ forall r, data_preg r = true -> rs'#r = rs#r. Proof. intros. Opaque Int.eq. - destruct cond; simpl in H; TypeInv; simpl; UseTypeInfo. + unfold transl_cond in H; destruct cond; ArgsInv; simpl. (* Ccomp *) - fold (Val.cmp c (rs (ireg_of m0)) (rs (ireg_of m1))). - destruct (compare_sint_spec rs (rs (ireg_of m0)) (rs (ireg_of m1))) - as [A [B [C D]]]. + fold (Val.cmp c0 (rs x) (rs x0)). + destruct (compare_sint_spec rs (rs x) (rs x0)) as [A [B [C D]]]. econstructor; split. apply exec_straight_one. simpl; reflexivity. reflexivity. split. - case c; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto. - auto with ppcgen. + case c0; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto. + auto with asmgen. (* Ccompu *) - fold (Val.cmpu (Mem.valid_pointer m) c (rs (ireg_of m0)) (rs (ireg_of m1))). - destruct (compare_uint_spec rs m (rs (ireg_of m0)) (rs (ireg_of m1))) - as [A [B [C D]]]. + fold (Val.cmpu (Mem.valid_pointer m) c0 (rs x) (rs x0)). + destruct (compare_uint_spec rs m (rs x) (rs x0)) as [A [B [C D]]]. econstructor; split. apply exec_straight_one. simpl; reflexivity. reflexivity. split. - case c; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto. - auto with ppcgen. + case c0; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto. + auto with asmgen. (* Ccompimm *) - fold (Val.cmp c (rs (ireg_of m0)) (Vint i)). - case (Int.eq (high_s i) Int.zero). - destruct (compare_sint_spec rs (rs (ireg_of m0)) (Vint i)) - as [A [B [C D]]]. + fold (Val.cmp c0 (rs x) (Vint i)). + destruct (Int.eq (high_s i) Int.zero); inv EQ0. + destruct (compare_sint_spec rs (rs x) (Vint i)) as [A [B [C D]]]. econstructor; split. - apply exec_straight_one. simpl. eauto. reflexivity. + apply exec_straight_one. simpl; reflexivity. reflexivity. split. - case c; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto. - auto with ppcgen. - generalize (loadimm_correct GPR0 i (Pcmpw (ireg_of m0) GPR0 :: k) rs m). - intros [rs1 [EX1 [RES1 OTH1]]]. - destruct (compare_sint_spec rs1 (rs (ireg_of m0)) (Vint i)) - as [A [B [C D]]]. - assert (rs1 (ireg_of m0) = rs (ireg_of m0)). - apply OTH1; auto with ppcgen. - exists (nextinstr (compare_sint rs1 (rs1 (ireg_of m0)) (Vint i))). + case c0; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto. + auto with asmgen. + destruct (loadimm_correct GPR0 i (Pcmpw x GPR0 :: k) rs m) as [rs1 [EX1 [RES1 OTH1]]]. + destruct (compare_sint_spec rs1 (rs x) (Vint i)) as [A [B [C D]]]. + assert (SAME: rs1 x = rs x) by (apply OTH1; eauto with asmgen). + exists (nextinstr (compare_sint rs1 (rs1 x) (Vint i))). split. eapply exec_straight_trans. eexact EX1. - apply exec_straight_one. simpl. rewrite RES1; rewrite H; auto. + apply exec_straight_one. simpl. rewrite RES1; rewrite SAME; auto. reflexivity. - split. rewrite H. - case c; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto. - intros. rewrite H; rewrite D; auto with ppcgen. + split. rewrite SAME. + case c0; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto. + intros. rewrite SAME; rewrite D; auto with asmgen. (* Ccompuimm *) - fold (Val.cmpu (Mem.valid_pointer m) c (rs (ireg_of m0)) (Vint i)). - case (Int.eq (high_u i) Int.zero). - destruct (compare_uint_spec rs m (rs (ireg_of m0)) (Vint i)) - as [A [B [C D]]]. + fold (Val.cmpu (Mem.valid_pointer m) c0 (rs x) (Vint i)). + destruct (Int.eq (high_u i) Int.zero); inv EQ0. + destruct (compare_uint_spec rs m (rs x) (Vint i)) as [A [B [C D]]]. econstructor; split. - apply exec_straight_one. simpl. eauto. reflexivity. + apply exec_straight_one. simpl; reflexivity. reflexivity. split. - case c; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto. - auto with ppcgen. - generalize (loadimm_correct GPR0 i (Pcmplw (ireg_of m0) GPR0 :: k) rs m). - intros [rs1 [EX1 [RES1 OTH1]]]. - destruct (compare_uint_spec rs1 m (rs (ireg_of m0)) (Vint i)) - as [A [B [C D]]]. - assert (rs1 (ireg_of m0) = rs (ireg_of m0)). apply OTH1; auto with ppcgen. - exists (nextinstr (compare_uint rs1 m (rs1 (ireg_of m0)) (Vint i))). + case c0; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto. + auto with asmgen. + destruct (loadimm_correct GPR0 i (Pcmplw x GPR0 :: k) rs m) as [rs1 [EX1 [RES1 OTH1]]]. + destruct (compare_uint_spec rs1 m (rs x) (Vint i)) as [A [B [C D]]]. + assert (SAME: rs1 x = rs x) by (apply OTH1; eauto with asmgen). + exists (nextinstr (compare_uint rs1 m (rs1 x) (Vint i))). split. eapply exec_straight_trans. eexact EX1. - apply exec_straight_one. simpl. rewrite RES1; rewrite H; auto. + apply exec_straight_one. simpl. rewrite RES1; rewrite SAME; auto. reflexivity. - split. rewrite H. - case c; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto. - intros. rewrite H; rewrite D; auto with ppcgen. + split. rewrite SAME. + case c0; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto. + intros. rewrite SAME; rewrite D; auto with asmgen. (* Ccompf *) - fold (Val.cmpf c (rs (freg_of m0)) (rs (freg_of m1))). - destruct (floatcomp_correct c (freg_of m0) (freg_of m1) k rs m) - as [rs' [EX [RES OTH]]]. + fold (Val.cmpf c0 (rs x) (rs x0)). + destruct (floatcomp_correct c0 x x0 k rs m) as [rs' [EX [RES OTH]]]. exists rs'. split. auto. split. apply RES. - auto with ppcgen. + auto with asmgen. (* Cnotcompf *) rewrite Val.notbool_negb_3. rewrite Val.notbool_idem4. - fold (Val.cmpf c (rs (freg_of m0)) (rs (freg_of m1))). - destruct (floatcomp_correct c (freg_of m0) (freg_of m1) k rs m) - as [rs' [EX [RES OTH]]]. + fold (Val.cmpf c0 (rs x) (rs x0)). + destruct (floatcomp_correct c0 x x0 k rs m) as [rs' [EX [RES OTH]]]. exists rs'. split. auto. - split. rewrite RES. destruct (snd (crbit_for_fcmp c)); auto. - auto with ppcgen. + split. rewrite RES. destruct (snd (crbit_for_fcmp c0)); auto. + auto with asmgen. (* Cmaskzero *) - destruct (andimm_base_correct GPR0 (ireg_of m0) i k rs m) - as [rs' [A [B [C D]]]]. auto with ppcgen. + destruct (andimm_base_correct GPR0 x i k rs m) as [rs' [A [B [C D]]]]. + eauto with asmgen. exists rs'. split. assumption. - split. rewrite C. destruct (rs (ireg_of m0)); auto. - auto with ppcgen. + split. rewrite C. destruct (rs x); auto. + auto with asmgen. (* Cmasknotzero *) - destruct (andimm_base_correct GPR0 (ireg_of m0) i k rs m) - as [rs' [A [B [C D]]]]. auto with ppcgen. + destruct (andimm_base_correct GPR0 x i k rs m) as [rs' [A [B [C D]]]]. + eauto with asmgen. exists rs'. split. assumption. - split. rewrite C. destruct (rs (ireg_of m0)); auto. + split. rewrite C. destruct (rs x); auto. fold (option_map negb (Some (Int.eq (Int.and i0 i) Int.zero))). rewrite Val.notbool_negb_3. rewrite Val.notbool_idem4. auto. - auto with ppcgen. + auto with asmgen. Qed. Lemma transl_cond_correct_2: - forall cond args k rs m b, - map mreg_type args = type_of_condition cond -> + forall cond args k rs m b c, + transl_cond cond args k = OK c -> eval_condition cond (map rs (map preg_of args)) m = Some b -> exists rs', - exec_straight (transl_cond cond args k) rs m k rs' m + exec_straight ge fn c rs m k rs' m /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) = (if snd (crbit_for_cond cond) then Val.of_bool b else Val.notbool (Val.of_bool b)) - /\ forall r, is_data_reg r = true -> rs'#r = rs#r. + /\ forall r, data_preg r = true -> rs'#r = rs#r. Proof. intros. replace (Val.of_bool b) @@ -1115,14 +670,14 @@ Proof. rewrite H0; auto. Qed. -Lemma transl_cond_correct: - forall cond args k ms sp rs m b m', - map mreg_type args = type_of_condition cond -> +Lemma transl_cond_correct_3: + forall cond args k ms sp rs m b m' c, + transl_cond cond args k = OK c -> agree ms sp rs -> eval_condition cond (map ms args) m = Some b -> Mem.extends m m' -> exists rs', - exec_straight (transl_cond cond args k) rs m' k rs' m' + exec_straight ge fn c 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 @@ -1184,66 +739,60 @@ Transparent Int.eq. Qed. Lemma transl_cond_op_correct: - forall cond args r k rs m, - mreg_type r = Tint -> - map mreg_type args = type_of_condition cond -> + forall cond args r k rs m c, + transl_cond_op cond args r k = OK c -> exists rs', - exec_straight (transl_cond_op cond args r k) rs m k rs' m - /\ rs'#(ireg_of r) = Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m) - /\ forall r', is_data_reg r' = true -> r' <> ireg_of r -> rs'#r' = rs#r'. + exec_straight ge fn c rs m k rs' m + /\ rs'#(preg_of r) = Val.of_optbool (eval_condition cond (map rs (map preg_of args)) m) + /\ forall r', data_preg r' = true -> r' <> preg_of r -> rs'#r' = rs#r'. Proof. intros until args. unfold transl_cond_op. - destruct (classify_condition cond args); - intros until m; intros TY1 TY2; simpl in TY2. + destruct (classify_condition cond args); intros; monadInv H; simpl; + erewrite ! ireg_of_eq; eauto. (* eq 0 *) - inv TY2. simpl. unfold preg_of; rewrite H0. econstructor; split. eapply exec_straight_two; simpl; reflexivity. - split. repeat SIMP. destruct (rs (ireg_of r)); simpl; auto. + split. Simpl. destruct (rs x0); simpl; auto. apply add_carry_eq0. - intros; repeat SIMP. + intros; Simpl. (* ne 0 *) - inv TY2. simpl. unfold preg_of; rewrite H0. econstructor; split. eapply exec_straight_two; simpl; reflexivity. - split. repeat SIMP. rewrite gpr_or_zero_not_zero; auto with ppcgen. - destruct (rs (ireg_of r)); simpl; auto. + rewrite gpr_or_zero_not_zero; eauto with asmgen. + split. Simpl. destruct (rs x0); simpl; auto. apply add_carry_ne0. - intros; repeat SIMP. + intros; Simpl. (* ge 0 *) - inv TY2. simpl. unfold preg_of; rewrite H0. econstructor; split. eapply exec_straight_two; simpl; reflexivity. - split. repeat SIMP. rewrite Val.rolm_ge_zero. auto. - intros; repeat SIMP. + split. Simpl. rewrite Val.rolm_ge_zero. auto. + intros; Simpl. (* lt 0 *) - inv TY2. simpl. unfold preg_of; rewrite H0. econstructor; split. apply exec_straight_one; simpl; reflexivity. - split. repeat SIMP. rewrite Val.rolm_lt_zero. auto. - intros; repeat SIMP. + split. Simpl. rewrite Val.rolm_lt_zero. auto. + intros; Simpl. (* default *) - set (bit := fst (crbit_for_cond c)). - set (isset := snd (crbit_for_cond c)). + set (bit := fst (crbit_for_cond c)) in *. + set (isset := snd (crbit_for_cond c)) in *. set (k1 := - Pmfcrbit (ireg_of r) bit :: + Pmfcrbit x bit :: (if isset then k - else Pxori (ireg_of r) (ireg_of r) (Cint Int.one) :: k)). - generalize (transl_cond_correct_1 c rl k1 rs m TY2). + else Pxori x x (Cint Int.one) :: k)). + generalize (transl_cond_correct_1 c rl k1 rs m c0 EQ0). fold bit; fold isset. intros [rs1 [EX1 [RES1 AG1]]]. destruct isset. (* bit set *) econstructor; split. eapply exec_straight_trans. eexact EX1. - unfold k1. apply exec_straight_one; simpl; reflexivity. - split. repeat SIMP. intros; repeat SIMP. + unfold k1. apply exec_straight_one; simpl; reflexivity. + intuition Simpl. (* bit clear *) econstructor; split. eapply exec_straight_trans. eexact EX1. - unfold k1. eapply exec_straight_two; simpl; reflexivity. - split. repeat SIMP. rewrite RES1. - destruct (eval_condition c rs ## (preg_of ## rl) m). destruct b; auto. auto. - intros; repeat SIMP. + unfold k1. eapply exec_straight_two; simpl; reflexivity. + intuition Simpl. + rewrite RES1. destruct (eval_condition c rs ## (preg_of ## rl) m). destruct b; auto. auto. Qed. (** Translation of arithmetic operations. *) @@ -1251,137 +800,123 @@ Qed. Ltac TranslOpSimpl := econstructor; split; [ apply exec_straight_one; [simpl; eauto | reflexivity] - | split; intros; (repeat SIMP; fail) ]. + | split; intros; Simpl; fail ]. Lemma transl_op_correct_aux: - forall op args res k (rs: regset) m v, - wt_instr (Mop op args res) -> + forall op args res k (rs: regset) m v c, + transl_op op args res k = OK c -> eval_operation ge (rs#GPR1) op (map rs (map preg_of args)) m = Some v -> exists rs', - exec_straight (transl_op op args res k) rs m k rs' m + exec_straight ge fn c rs m k rs' m /\ rs'#(preg_of res) = v /\ forall r, - match op with Omove => is_data_reg r = true | _ => is_nontemp_reg r = true end -> + match op with Omove => data_preg r = true | _ => nontemp_preg r = true end -> r <> preg_of res -> rs'#r = rs#r. Proof. - intros until v; intros WT EV. - inv WT. +Opaque Int.eq. Opaque Int.repr. + intros. unfold transl_op in H; destruct op; ArgsInv; simpl in H0; try (inv H0); try TranslOpSimpl. (* Omove *) - simpl in *. inv EV. - exists (nextinstr (rs#(preg_of res) <- (rs#(preg_of r1)))). - split. unfold preg_of. rewrite <- H0. - destruct (mreg_type r1); apply exec_straight_one; auto. - split. repeat SIMP. intros; repeat SIMP. - (* Other instructions *) -Opaque Int.eq. - destruct op; simpl; simpl in H3; injection H3; clear H3; intros; - TypeInv; simpl in *; UseTypeInfo; inv EV; try (TranslOpSimpl). + destruct (preg_of res) eqn:RES; destruct (preg_of m0) eqn:ARG; inv H. + TranslOpSimpl. + TranslOpSimpl. (* Ointconst *) - destruct (loadimm_correct (ireg_of res) i k rs m) as [rs' [A [B C]]]. - exists rs'. split. auto. split. auto. auto with ppcgen. + destruct (loadimm_correct x i k rs m) as [rs' [A [B C]]]. + exists rs'. auto with asmgen. (* Oaddrsymbol *) change (symbol_address ge i i0) with (symbol_offset ge i i0). set (v' := symbol_offset ge i i0). - caseEq (symbol_is_small_data i i0); intro SD. + destruct (symbol_is_small_data i i0) eqn:SD. (* small data *) econstructor; split. apply exec_straight_one; simpl; reflexivity. - split. repeat SIMP. - rewrite (small_data_area_addressing _ _ _ SD). unfold v', symbol_offset. + split. Simpl. rewrite (small_data_area_addressing _ _ _ SD). unfold v', symbol_offset. destruct (Genv.find_symbol ge i); auto. rewrite Int.add_zero; auto. - intros; repeat SIMP. + intros; Simpl. (* not small data *) Opaque Val.add. econstructor; split. eapply exec_straight_two; simpl; reflexivity. - split. repeat SIMP. rewrite gpr_or_zero_zero. - rewrite gpr_or_zero_not_zero; auto with ppcgen. repeat SIMP. + split. Simpl. rewrite gpr_or_zero_zero. + rewrite gpr_or_zero_not_zero; eauto with asmgen. Simpl. rewrite (Val.add_commut Vzero). rewrite high_half_zero. rewrite Val.add_commut. rewrite low_high_half. auto. - intros; repeat SIMP. + intros; Simpl. (* Oaddrstack *) - destruct (addimm_correct (ireg_of res) GPR1 i k rs m) as [rs' [EX [RES OTH]]]. - auto with ppcgen. congruence. - exists rs'; auto with ppcgen. + destruct (addimm_correct x GPR1 i k rs m) as [rs' [EX [RES OTH]]]; eauto with asmgen. + exists rs'; auto with asmgen. (* Oaddimm *) - destruct (addimm_correct (ireg_of res) (ireg_of m0) i k rs m) as [rs' [A [B C]]]; auto with ppcgen. - exists rs'; auto with ppcgen. + destruct (addimm_correct x0 x i k rs m) as [rs' [A [B C]]]; eauto with asmgen. + exists rs'; auto with asmgen. (* Osubimm *) case (Int.eq (high_s i) Int.zero). TranslOpSimpl. - destruct (loadimm_correct GPR0 i (Psubfc (ireg_of res) (ireg_of m0) GPR0 :: k) rs m) as [rs1 [EX [RES OTH]]]. + destruct (loadimm_correct GPR0 i (Psubfc x0 x GPR0 :: k) rs m) as [rs1 [EX [RES OTH]]]. econstructor; split. eapply exec_straight_trans. eexact EX. apply exec_straight_one; simpl; reflexivity. - split. repeat SIMP. rewrite RES. rewrite OTH; auto with ppcgen. - intros; repeat SIMP. + split. Simpl. rewrite RES. rewrite OTH; eauto with asmgen. + intros; Simpl. (* Omulimm *) case (Int.eq (high_s i) Int.zero). TranslOpSimpl. - destruct (loadimm_correct GPR0 i (Pmullw (ireg_of res) (ireg_of m0) GPR0 :: k) rs m) as [rs1 [EX [RES OTH]]]. + destruct (loadimm_correct GPR0 i (Pmullw x0 x GPR0 :: k) rs m) as [rs1 [EX [RES OTH]]]. econstructor; split. eapply exec_straight_trans. eexact EX. apply exec_straight_one; simpl; reflexivity. - split. repeat SIMP. rewrite RES. rewrite OTH; auto with ppcgen. - intros; repeat SIMP. + split. Simpl. rewrite RES. rewrite OTH; eauto with asmgen. + intros; Simpl. (* Odivs *) - replace v with (Val.maketotal (Val.divs (rs (ireg_of m0)) (rs (ireg_of m1)))). + replace v with (Val.maketotal (Val.divs (rs x) (rs x0))). TranslOpSimpl. - rewrite H2; auto. + rewrite H1; auto. (* Odivu *) - replace v with (Val.maketotal (Val.divu (rs (ireg_of m0)) (rs (ireg_of m1)))). + replace v with (Val.maketotal (Val.divu (rs x) (rs x0))). TranslOpSimpl. - rewrite H2; auto. + rewrite H1; auto. (* Oand *) - set (v' := Val.and (rs (ireg_of m0)) (rs (ireg_of m1))) in *. - pose (rs1 := rs#(ireg_of res) <- v'). - generalize (compare_sint_spec rs1 v' Vzero). - intros [A [B [C D]]]. + set (v' := Val.and (rs x) (rs x0)) in *. + pose (rs1 := rs#x1 <- v'). + destruct (compare_sint_spec rs1 v' Vzero) as [A [B [C D]]]. econstructor; split. apply exec_straight_one; simpl; reflexivity. - split. rewrite D; auto with ppcgen. unfold rs1. SIMP. - intros. rewrite D; auto with ppcgen. unfold rs1. SIMP. + split. rewrite D; auto with asmgen. unfold rs1; Simpl. + intros. rewrite D; auto with asmgen. unfold rs1; Simpl. (* Oandimm *) - destruct (andimm_correct (ireg_of res) (ireg_of m0) i k rs m) as [rs' [A [B C]]]; auto with ppcgen. - exists rs'; auto with ppcgen. + destruct (andimm_correct x0 x i k rs m) as [rs' [A [B C]]]; eauto with asmgen. + exists rs'; auto with asmgen. (* Oorimm *) - destruct (orimm_correct (ireg_of res) (ireg_of m0) i k rs m) as [rs' [A [B C]]]. - exists rs'; auto with ppcgen. + destruct (orimm_correct x0 x i k rs m) as [rs' [A [B C]]]. + exists rs'; auto with asmgen. (* Oxorimm *) - destruct (xorimm_correct (ireg_of res) (ireg_of m0) i k rs m) as [rs' [A [B C]]]. - exists rs'; auto with ppcgen. + destruct (xorimm_correct x0 x i k rs m) as [rs' [A [B C]]]. + exists rs'; auto with asmgen. (* Onor *) - replace (Val.notint (rs (ireg_of m0))) - with (Val.notint (Val.or (rs (ireg_of m0)) (rs (ireg_of m0)))). + replace (Val.notint (rs x)) + with (Val.notint (Val.or (rs x) (rs x))). TranslOpSimpl. - destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.or_idem. auto. + destruct (rs x); simpl; auto. rewrite Int.or_idem. auto. (* Oshrximm *) econstructor; split. eapply exec_straight_two; simpl; reflexivity. - split. repeat SIMP. apply Val.shrx_carry. auto. - intros; repeat SIMP. + split. Simpl. apply Val.shrx_carry. auto. + intros; Simpl. (* Orolm *) - destruct (rolm_correct (ireg_of res) (ireg_of m0) i i0 k rs m) as [rs' [A [B C]]]; auto with ppcgen. - exists rs'; auto with ppcgen. - (* Oroli *) - destruct (mreg_eq m0 res). subst m0. - TranslOpSimpl. - econstructor; split. - eapply exec_straight_three; simpl; reflexivity. - split. repeat SIMP. intros; repeat SIMP. + destruct (rolm_correct x0 x i i0 k rs m) as [rs' [A [B C]]]; eauto with asmgen. + exists rs'; auto with asmgen. (* Ointoffloat *) - replace v with (Val.maketotal (Val.intoffloat (rs (freg_of m0)))). + replace v with (Val.maketotal (Val.intoffloat (rs x))). TranslOpSimpl. - rewrite H2; auto. + rewrite H1; auto. (* Ocmp *) - destruct (transl_cond_op_correct c args res k rs m) as [rs' [A [B C]]]; auto. - exists rs'; auto with ppcgen. + destruct (transl_cond_op_correct c0 args res k rs m c) as [rs' [A [B C]]]; auto. + exists rs'; auto with asmgen. Qed. Lemma transl_op_correct: - forall op args res k ms sp rs m v m', - wt_instr (Mop op args res) -> + forall op args res k ms sp rs m v m' c, + transl_op op args res k = OK c -> agree ms sp rs -> eval_operation ge sp op (map ms args) m = Some v -> Mem.extends m m' -> exists rs', - exec_straight (transl_op op args res k) rs m' k rs' m' - /\ agree (Regmap.set res v (undef_op op ms)) sp rs'. + exec_straight ge fn c rs m' k rs' m' + /\ agree (Regmap.set res v (undef_op op ms)) sp rs' + /\ forall r, op = Omove -> data_preg r = true -> r <> preg_of res -> rs'#r = rs#r. Proof. intros. exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eauto. @@ -1389,74 +924,67 @@ Proof. exploit transl_op_correct_aux; eauto. intros [rs' [P [Q R]]]. rewrite <- Q in B. exists rs'; split. eexact P. - unfold undef_op. destruct op; - (apply agree_set_mreg_undef_temps with rs || apply agree_set_mreg with rs); + split. unfold undef_op. destruct op; + (apply agree_set_undef_mreg with rs || apply agree_set_mreg with rs); auto. + intros. subst op. auto. Qed. -Lemma transl_load_store_correct: - forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction) - addr args (temp: ireg) k ms sp rs m ms' m', +(** Translation of memory accesses *) + +Lemma transl_memory_access_correct: + forall (P: regset -> Prop) mk1 mk2 addr args temp k c (rs: regset) a m m', + transl_memory_access mk1 mk2 addr args temp k = OK c -> + eval_addressing ge (rs#GPR1) addr (map rs (map preg_of args)) = Some a -> + temp <> GPR0 -> (forall cst (r1: ireg) (rs1: regset) k, - eval_addressing ge sp addr (map rs (map preg_of args)) = - Some(Val.add (gpr_or_zero rs1 r1) (const_low ge cst)) -> - (forall (r: preg), r <> PC -> r <> temp -> rs1 r = rs r) -> + Val.add (gpr_or_zero rs1 r1) (const_low ge cst) = a -> + (forall r, r <> PC -> r <> temp -> rs1 r = rs r) -> exists rs', - exec_straight (mk1 cst r1 :: k) rs1 m k rs' m' /\ - agree ms' sp rs') -> - (forall (r1 r2: ireg) k, - eval_addressing ge sp addr (map rs (map preg_of args)) = Some(Val.add rs#r1 rs#r2) -> + exec_straight ge fn (mk1 cst r1 :: k) rs1 m k rs' m' /\ P rs') -> + (forall (r1 r2: ireg) (rs1: regset) k, + Val.add rs1#r1 rs1#r2 = a -> + (forall r, r <> PC -> r <> temp -> rs1 r = rs r) -> exists rs', - exec_straight (mk2 r1 r2 :: k) rs m k rs' m' /\ - agree ms' sp rs') -> - agree ms sp rs -> - map mreg_type args = type_of_addressing addr -> - temp <> GPR0 -> + exec_straight ge fn (mk2 r1 r2 :: k) rs1 m k rs' m' /\ P rs') -> exists rs', - exec_straight (transl_load_store mk1 mk2 addr args temp k) rs m - k rs' m' - /\ agree ms' sp rs'. + exec_straight ge fn c rs m k rs' m' /\ P rs'. Proof. - intros. destruct addr; simpl in H2; TypeInv; simpl. + intros until m'; intros TR ADDR TEMP MK1 MK2. + unfold transl_memory_access in TR; destruct addr; ArgsInv; simpl in ADDR; inv ADDR. (* Aindexed *) case (Int.eq (high_s i) Int.zero). (* Aindexed short *) - apply H. - simpl. UseTypeInfo. rewrite gpr_or_zero_not_zero; auto with ppcgen. - auto. + apply MK1. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. (* Aindexed long *) - set (rs1 := nextinstr (rs#temp <- (Val.add (rs (ireg_of m0)) (Vint (Int.shl (high_s i) (Int.repr 16)))))). - exploit (H (Cint (low_s i)) temp rs1 k). - simpl. UseTypeInfo. rewrite gpr_or_zero_not_zero; auto. - unfold rs1; repeat SIMP. rewrite Val.add_assoc. + set (rs1 := nextinstr (rs#temp <- (Val.add (rs x) (Vint (Int.shl (high_s i) (Int.repr 16)))))). + exploit (MK1 (Cint (low_s i)) temp rs1 k). + simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. + unfold rs1; Simpl. rewrite Val.add_assoc. Transparent Val.add. simpl. rewrite low_high_s. auto. - intros; unfold rs1; repeat SIMP. + intros; unfold rs1; Simpl. intros [rs' [EX' AG']]. exists rs'. split. apply exec_straight_step with rs1 m. - simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen. auto. + simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. auto. auto. (* Aindexed2 *) - apply H0. - simpl. UseTypeInfo; auto. + apply MK2; auto. (* Aglobal *) - case_eq (symbol_is_small_data i i0); intro SISD. + destruct (symbol_is_small_data i i0) eqn:SISD; inv TR. (* Aglobal from small data *) - apply H. rewrite gpr_or_zero_zero. simpl const_low. - rewrite small_data_area_addressing; auto. simpl. + apply MK1. simpl. rewrite small_data_area_addressing; auto. unfold symbol_address, symbol_offset. destruct (Genv.find_symbol ge i); auto. rewrite Int.add_zero. auto. auto. (* Aglobal general case *) set (rs1 := nextinstr (rs#temp <- (const_high ge (Csymbol_high i i0)))). - exploit (H (Csymbol_low i i0) temp rs1 k). - simpl. rewrite gpr_or_zero_not_zero; auto. - 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. rewrite low_high_half. auto. - discriminate. - intros; unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + exploit (MK1 (Csymbol_low i i0) temp rs1 k). + simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. + unfold rs1. Simpl. + unfold const_high, const_low. + rewrite Val.add_commut. rewrite low_high_half. auto. + intros; unfold rs1; Simpl. intros [rs' [EX' AG']]. exists rs'. split. apply exec_straight_step with rs1 m. unfold exec_instr. rewrite gpr_or_zero_zero. @@ -1465,27 +993,24 @@ Transparent Val.add. reflexivity. reflexivity. assumption. assumption. (* Abased *) - set (rs1 := nextinstr (rs#temp <- (Val.add (rs (ireg_of m0)) (const_high ge (Csymbol_high i i0))))). - exploit (H (Csymbol_low i i0) temp rs1 k). - simpl. rewrite gpr_or_zero_not_zero; auto. - unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss. + set (rs1 := nextinstr (rs#temp <- (Val.add (rs x) (const_high ge (Csymbol_high i i0))))). + exploit (MK1 (Csymbol_low i i0) temp rs1 k). + simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. + unfold rs1. Simpl. rewrite Val.add_assoc. unfold const_high, const_low. - set (v := symbol_offset ge i i0). - symmetry. rewrite Val.add_commut. decEq. decEq. - unfold v. rewrite Val.add_commut. rewrite low_high_half. auto. - UseTypeInfo. auto. discriminate. - intros. unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + symmetry. rewrite Val.add_commut. f_equal. f_equal. + rewrite Val.add_commut. rewrite low_high_half. auto. + intros; unfold rs1; Simpl. intros [rs' [EX' AG']]. exists rs'. split. apply exec_straight_step with rs1 m. - unfold exec_instr. rewrite gpr_or_zero_not_zero; auto with ppcgen. auto. + unfold exec_instr. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. assumption. assumption. (* Ainstack *) - case (Int.eq (high_s i) Int.zero). - apply H. simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen. - rewrite (sp_val ms sp rs); auto. auto. - set (rs1 := nextinstr (rs#temp <- (Val.add sp (Vint (Int.shl (high_s i) (Int.repr 16)))))). - exploit (H (Cint (low_s i)) temp rs1 k). + destruct (Int.eq (high_s i) Int.zero); inv TR. + apply MK1. simpl. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. + set (rs1 := nextinstr (rs#temp <- (Val.add rs#GPR1 (Vint (Int.shl (high_s i) (Int.repr 16)))))). + exploit (MK1 (Cint (low_s i)) temp rs1 k). simpl. rewrite gpr_or_zero_not_zero; auto. unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss. rewrite Val.add_assoc. simpl. rewrite low_high_s. auto. @@ -1493,120 +1018,149 @@ Transparent Val.add. intros. unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. intros [rs' [EX' AG']]. exists rs'. split. apply exec_straight_step with rs1 m. - unfold exec_instr. rewrite gpr_or_zero_not_zero; auto with ppcgen. - rewrite <- (sp_val ms sp rs); auto. auto. + unfold exec_instr. rewrite gpr_or_zero_not_zero; eauto with asmgen. auto. assumption. assumption. Qed. -(** Translation of memory loads. *) +(** Translation of loads *) Lemma transl_load_correct: - forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction) - chunk addr args k ms sp rs m 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 -> + forall chunk addr args dst k c (rs: regset) m a v, + transl_load chunk addr args dst k = OK c -> + eval_addressing ge (rs#GPR1) addr (map rs (map preg_of args)) = Some a -> Mem.loadv chunk m a = Some v -> - Mem.extends m m' -> exists rs', - exec_straight (transl_load_store mk1 mk2 addr args GPR12 k) rs m' - k rs' m' - /\ agree (Regmap.set dst v (undef_temps ms)) sp rs'. + exec_straight ge fn c 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. - exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. - unfold PregEq.t. - intros [a' [A B]]. - exploit Mem.loadv_extends; eauto. intros [v' [C D]]. - apply transl_load_store_correct with ms; auto. -(* mk1 *) - intros. exists (nextinstr (rs1#(preg_of dst) <- v')). - split. apply exec_straight_one. rewrite H. - unfold load1. rewrite A in H6. inv H6. rewrite C. auto. - unfold nextinstr. SIMP. decEq. SIMP. apply sym_not_equal; auto with ppcgen. - apply agree_set_mreg with rs1. - apply agree_undef_temps with rs; auto with ppcgen. - repeat SIMP. - intros; repeat SIMP. -(* mk2 *) - intros. exists (nextinstr (rs#(preg_of dst) <- v')). - split. apply exec_straight_one. rewrite H0. - unfold load2. rewrite A in H6. inv H6. rewrite C. auto. - unfold nextinstr. SIMP. decEq. SIMP. apply sym_not_equal; auto with ppcgen. - apply agree_set_mreg with rs. - apply agree_undef_temps with rs; auto with ppcgen. - repeat SIMP. - intros; repeat SIMP. -(* not GPR0 *) - congruence. -Qed. - -(** Translation of memory stores. *) + assert (BASE: forall mk1 mk2 k' chunk' v', + transl_memory_access mk1 mk2 addr args GPR12 k' = OK c -> + Mem.loadv chunk' m a = Some 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) -> + exists rs', + exec_straight ge fn c rs m k' rs' m + /\ rs'#(preg_of dst) = v' + /\ forall r, r <> PC -> r <> GPR12 -> r <> preg_of dst -> rs' r = rs r). + { + intros. eapply transl_memory_access_correct; eauto. congruence. + intros. econstructor; split. apply exec_straight_one. + rewrite H4. unfold load1. rewrite H6. rewrite H3. eauto. + unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso; auto with asmgen. + intuition Simpl. + intros. econstructor; split. apply exec_straight_one. + rewrite H5. unfold load2. rewrite H6. rewrite H3. eauto. + unfold nextinstr. rewrite Pregmap.gss. rewrite Pregmap.gso; auto with asmgen. + intuition Simpl. + } + destruct chunk; monadInv H. +- (* Mint8signed *) + assert (exists v1, Mem.loadv Mint8unsigned m a = Some v1 /\ v = Val.sign_ext 8 v1). + { + destruct a; simpl in *; try discriminate. + rewrite Mem.load_int8_signed_unsigned in H1. + destruct (Mem.load Mint8unsigned m b (Int.unsigned i)); simpl in H1; inv H1. + exists v0; auto. + } + destruct H as [v1 [LD SG]]. clear H1. + exploit BASE; eauto; erewrite ireg_of_eq by eauto; auto. + intros [rs1 [A [B C]]]. + econstructor; split. + eapply exec_straight_trans. eexact A. apply exec_straight_one. simpl; eauto. auto. + split. Simpl. congruence. intros. Simpl. +- (* Mint8unsigned *) + eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto. +- (* Mint816signed *) + eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto. +- (* Mint16unsigned *) + eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto. +- (* Mint32 *) + eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto. +- (* Mfloat32 *) + eapply BASE; eauto; erewrite freg_of_eq by eauto; auto. +- (* Mfloat64 *) + apply Mem.loadv_float64al32 in H1. eapply BASE; eauto; erewrite freg_of_eq by eauto; auto. +- (* Mfloat64al32 *) + eapply BASE; eauto; erewrite freg_of_eq by eauto; auto. +Qed. + +(** Translation of 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' m1, - (forall cst (r1: ireg) (rs1 rs2: regset) (m2: mem), - store1 ge chunk (preg_of src) cst r1 rs1 m1 = OK rs2 m2 -> - exists rs3, - exec_instr ge fn (mk1 cst r1) rs1 m1 = OK rs3 m2 - /\ (forall (r: preg), r <> FPR13 -> rs3 r = rs2 r)) -> - (forall (r1 r2: ireg) (rs1 rs2: regset) (m2: mem), - store2 chunk (preg_of src) r1 r2 rs1 m1 = OK rs2 m2 -> - exists rs3, - exec_instr ge fn (mk2 r1 r2) rs1 m1 = OK rs3 m2 - /\ (forall (r: preg), r <> FPR13 -> rs3 r = rs2 r)) -> - 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' -> - Mem.extends m m1 -> - exists m1', - Mem.extends m' m1' - /\ exists rs', - exec_straight (transl_load_store mk1 mk2 addr args (int_temp_for src) k) rs m1 - k rs' m1' - /\ agree (undef_temps ms) sp rs'. + forall chunk addr args src k c (rs: regset) m a m', + transl_store chunk addr args src k = OK c -> + eval_addressing ge (rs#GPR1) addr (map rs (map preg_of args)) = Some a -> + Mem.storev chunk m a (rs (preg_of src)) = Some m' -> + exists rs', + exec_straight ge fn c rs m k rs' m' + /\ forall r, r <> PC -> r <> GPR11 -> r <> GPR12 -> r <> FPR13 -> rs' r = rs r. Proof. intros. - exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. - unfold PregEq.t. - intros [a' [A B]]. - assert (Z: Val.lessdef (ms src) (rs (preg_of src))). eapply preg_val; eauto. - exploit Mem.storev_extends; eauto. intros [m1' [C D]]. - exists m1'; split; auto. - apply transl_load_store_correct with ms; auto. -(* mk1 *) - intros. - exploit (H cst r1 rs1 (nextinstr rs1) m1'). - unfold store1. rewrite A in H6. inv H6. - replace (rs1 (preg_of src)) with (rs (preg_of src)). - rewrite C. auto. - symmetry. apply H7. auto with ppcgen. - apply sym_not_equal. apply int_temp_for_diff. - intros [rs3 [U V]]. - exists rs3; split. - apply exec_straight_one. auto. rewrite V; auto with ppcgen. - apply agree_undef_temps with rs. auto. - intros. rewrite V; auto with ppcgen. SIMP. apply H7; auto with ppcgen. - unfold int_temp_for. destruct (mreg_eq src IT2); auto with ppcgen. -(* mk2 *) - intros. - exploit (H0 r1 r2 rs (nextinstr rs) m1'). - unfold store2. rewrite A in H6. inv H6. rewrite C. auto. - intros [rs3 [U V]]. - exists rs3; split. - apply exec_straight_one. auto. rewrite V; auto with ppcgen. - eapply agree_undef_temps; eauto. intros. - rewrite V; auto with ppcgen. - unfold int_temp_for. destruct (mreg_eq src IT2); congruence. -Qed. - -End STRAIGHTLINE. + assert (TEMP0: int_temp_for src = GPR11 \/ int_temp_for src = GPR12). + unfold int_temp_for. destruct (mreg_eq src IT2); auto. + assert (TEMP1: int_temp_for src <> GPR0). + destruct TEMP0; congruence. + assert (TEMP2: IR (int_temp_for src) <> preg_of src). + unfold int_temp_for. destruct (mreg_eq src IT2). + subst src; simpl; congruence. + change (IR GPR12) with (preg_of IT2). red; intros; elim n. + eapply preg_of_injective; eauto. + assert (BASE: forall mk1 mk2 chunk', + transl_memory_access mk1 mk2 addr args (int_temp_for src) k = OK c -> + Mem.storev chunk' m a (rs (preg_of src)) = Some 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) -> + exists rs', + exec_straight ge fn c rs m k rs' m' + /\ forall r, r <> PC -> r <> GPR11 -> r <> GPR12 -> r <> FPR13 -> rs' r = rs r). + { + intros. eapply transl_memory_access_correct; eauto. + intros. econstructor; split. apply exec_straight_one. + rewrite H4. unfold store1. rewrite H6. rewrite H7; auto with asmgen. rewrite H3. eauto. auto. + intros; Simpl. apply H7; auto. destruct TEMP0; congruence. + intros. econstructor; split. apply exec_straight_one. + rewrite H5. unfold store2. rewrite H6. rewrite H7; auto with asmgen. rewrite H3. eauto. auto. + intros; Simpl. apply H7; auto. destruct TEMP0; congruence. + } + destruct chunk; monadInv H. +- (* Mint8signed *) + assert (Mem.storev Mint8unsigned m a (rs (preg_of src)) = Some m'). + rewrite <- H1. destruct a; simpl; auto. symmetry. apply Mem.store_signed_unsigned_8. + clear H1. eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto. +- (* Mint8unsigned *) + eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto. +- (* Mint16signed *) + assert (Mem.storev Mint16unsigned m a (rs (preg_of src)) = Some m'). + rewrite <- H1. destruct a; simpl; auto. symmetry. apply Mem.store_signed_unsigned_16. + clear H1. eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto. +- (* Mint16unsigned *) + eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto. +- (* Mint32 *) + eapply BASE; eauto; erewrite ireg_of_eq by eauto; auto. +- (* Mfloat32 *) + rewrite (freg_of_eq _ _ EQ) in H1. + eapply transl_memory_access_correct. eauto. eauto. eauto. + intros. econstructor; split. apply exec_straight_one. + simpl. unfold store1. rewrite H. rewrite H2; auto with asmgen. rewrite H1. eauto. auto. + intros. Simpl. apply H2; auto with asmgen. destruct TEMP0; congruence. + intros. econstructor; split. apply exec_straight_one. + simpl. unfold store2. rewrite H. rewrite H2; auto with asmgen. rewrite H1. eauto. auto. + intros. Simpl. apply H2; auto with asmgen. destruct TEMP0; congruence. +- (* Mfloat64 *) + apply Mem.storev_float64al32 in H1. eapply BASE; eauto; erewrite freg_of_eq by eauto; auto. +- (* Mfloat64al32 *) + eapply BASE; eauto; erewrite freg_of_eq by eauto; auto. +Qed. + +End CONSTRUCTORS. -- cgit v1.2.3