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 --- arm/Asmgenproof1.v | 1240 +++++++++++++++++----------------------------------- 1 file changed, 391 insertions(+), 849 deletions(-) (limited to 'arm/Asmgenproof1.v') diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index 658fc981..8fc8a7ee 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -12,8 +12,9 @@ (** Correctness proof for ARM code generation: auxiliary results. *) -Require Import Axioms. +(*Require Import Axioms.*) Require Import Coqlib. +Require Import Errors. Require Import Maps. Require Import AST. Require Import Integers. @@ -24,455 +25,44 @@ 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. -(** * Correspondence between Mach registers and PPC registers *) +(** Useful properties of the R14 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. - -Lemma ireg_of_not_IR13: - forall r, ireg_of r <> IR13. -Proof. - destruct r; simpl; congruence. -Qed. - -Lemma ireg_of_not_IR14: - forall r, ireg_of r <> IR14. -Proof. - destruct r; simpl; congruence. -Qed. - -Lemma preg_of_not_IR13: - forall r, preg_of r <> IR13. -Proof. - unfold preg_of; intros. destruct (mreg_type r). - generalize (ireg_of_not_IR13 r); congruence. - congruence. -Qed. - -Lemma preg_of_not_IR14: - forall r, preg_of r <> IR14. -Proof. - unfold preg_of; intros. destruct (mreg_type r). - generalize (ireg_of_not_IR14 r); congruence. - congruence. -Qed. - -Lemma preg_of_not_PC: - forall r, preg_of r <> PC. -Proof. - intros. unfold preg_of. destruct (mreg_type r); congruence. -Qed. - -Lemma ireg_diff: - forall r1 r2, r1 <> r2 -> IR r1 <> IR r2. -Proof. intros; congruence. Qed. - -Hint Resolve ireg_of_not_IR13 ireg_of_not_IR14 - preg_of_not_IR13 preg_of_not_IR14 - preg_of_not_PC ireg_diff: ppcgen. - -(** Agreement between Mach register sets and ARM register sets. *) - -Record agree (ms: Mach.regset) (sp: val) (rs: Asm.regset) : Prop := mkagree { - agree_sp: rs#IR13 = 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. destruct H. auto. -Qed. - -Lemma preg_vals: - forall ms sp rs, agree ms sp rs -> - forall l, Val.lessdef_list (map ms l) (map rs (map preg_of l)). -Proof. - induction l; simpl. constructor. constructor. eapply preg_val; eauto. auto. -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. generalize (preg_val _ _ _ r H). 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. generalize (preg_val _ _ _ r H). unfold preg_of. rewrite H0. auto. -Qed. - -Lemma sp_val: - forall ms sp rs, - agree ms sp rs -> - sp = rs#IR13. -Proof. - intros. destruct H; auto. -Qed. - -Hint Resolve preg_val ireg_val freg_val sp_val: ppcgen. - -Definition important_preg (r: preg) : bool := - match r with - | IR IR14 => false - | IR _ => true - | FR _ => true - | CR _ => false - | PC => false - end. - -Lemma preg_of_important: - forall r, important_preg (preg_of r) = true. -Proof. - intros. destruct r; reflexivity. -Qed. - -Lemma important_diff: - forall r r', - important_preg r = true -> important_preg r' = false -> r <> r'. -Proof. - congruence. -Qed. -Hint Resolve important_diff: ppcgen. - -Lemma agree_exten: - forall ms sp rs rs', - agree ms sp rs -> - (forall r, important_preg r = true -> rs'#r = rs#r) -> - agree ms sp rs'. -Proof. - intros. destruct H. split. - rewrite H0; auto. auto. - intros. rewrite H0; auto. apply preg_of_important. -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', important_preg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') -> - agree (Regmap.set r v ms) sp rs'. -Proof. - intros. destruct H. split. - rewrite H1; auto. apply sym_not_equal. apply preg_of_not_IR13. - auto. - intros. unfold Regmap.set. destruct (RegEq.eq r0 r). congruence. - rewrite H1. auto. apply preg_of_important. - red; intros; elim n. eapply preg_of_injective; eauto. -Qed. - -Lemma agree_set_other: - forall ms sp rs r v, - agree ms sp rs -> - important_preg r = false -> - agree ms sp (rs#r <- v). -Proof. - intros. apply agree_exten with rs. auto. - intros. apply Pregmap.gso. congruence. -Qed. - -Lemma agree_nextinstr: - forall ms sp rs, - agree ms sp rs -> agree ms sp (nextinstr rs). +Lemma ireg_of_not_R14: + forall m r, ireg_of m = OK r -> IR r <> IR IR14. Proof. - intros. unfold nextinstr. apply agree_set_other. auto. auto. + intros. erewrite <- ireg_of_eq; eauto with asmgen. Qed. +Hint Resolve ireg_of_not_R14: asmgen. -Definition nontemp_preg (r: preg) : bool := - match r with - | IR IR14 => false - | IR IR10 => false - | IR IR12 => false - | IR _ => true - | FR FR6 => false - | FR FR7 => false - | FR _ => true - | CR _ => false - | PC => false - end. - -Lemma nontemp_diff: - forall r r', - nontemp_preg r = true -> nontemp_preg r' = false -> r <> r'. -Proof. - congruence. -Qed. - -Hint Resolve nontemp_diff: ppcgen. - -Lemma nontemp_important: - forall r, nontemp_preg r = true -> important_preg r = true. +Lemma ireg_of_not_R14': + forall m r, ireg_of m = OK r -> r <> IR14. Proof. - unfold nontemp_preg, important_preg; destruct r; auto. destruct i; auto. + intros. generalize (ireg_of_not_R14 _ _ H). congruence. Qed. +Hint Resolve ireg_of_not_R14': asmgen. -Hint Resolve nontemp_important: ppcgen. +(** Useful simplification tactic *) -Remark undef_regs_1: - forall l ms r, ms r = Vundef -> Mach.undef_regs l ms r = Vundef. -Proof. - induction l; simpl; intros. auto. apply IHl. unfold Regmap.set. - destruct (RegEq.eq r a); congruence. -Qed. +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. -Remark undef_regs_2: - forall l ms r, In r l -> Mach.undef_regs l ms r = Vundef. -Proof. - induction l; simpl; intros. contradiction. - destruct H. subst. apply undef_regs_1. apply Regmap.gss. - auto. -Qed. - -Remark undef_regs_3: - forall l ms r, ~In r l -> Mach.undef_regs l ms r = ms r. -Proof. - induction l; simpl; intros. auto. - rewrite IHl. apply Regmap.gso. intuition. intuition. -Qed. - -Lemma agree_exten_temps: - forall ms sp rs rs', - agree ms sp rs -> - (forall r, nontemp_preg r = true -> rs'#r = rs#r) -> - agree (undef_temps ms) sp rs'. -Proof. - intros. destruct H. split. - rewrite H0; auto. auto. - intros. unfold undef_temps. - destruct (In_dec mreg_eq r (int_temporaries ++ float_temporaries)). - rewrite undef_regs_2; auto. - rewrite undef_regs_3; auto. rewrite H0; auto. - simpl in n. destruct r; auto; intuition. -Qed. - -Lemma agree_set_undef_mreg: - forall ms sp rs r v rs', - agree ms sp rs -> - Val.lessdef v (rs'#(preg_of r)) -> - (forall r', nontemp_preg 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))); auto. - eapply agree_exten_temps; eauto. - intros. unfold Pregmap.set. destruct (PregEq.eq r0 (preg_of r)). - congruence. auto. - intros. rewrite Pregmap.gso; auto. -Qed. +Ltac Simpl := repeat Simplif. -Lemma agree_undef_temps: - forall ms sp rs, - agree ms sp rs -> - agree (undef_temps ms) sp rs. -Proof. - intros. eapply agree_exten_temps; eauto. -Qed. - -(** Useful properties of the PC register. *) - -Lemma nextinstr_inv: - forall r rs, - r <> PC -> - (nextinstr rs)#r = rs#r. -Proof. - intros. unfold nextinstr. apply Pregmap.gso. red; intro; subst. auto. -Qed. - -Lemma nextinstr_inv2: - forall r rs, - nontemp_preg r = true -> - (nextinstr rs)#r = rs#r. -Proof. - intros. apply nextinstr_inv. red; intro; subst; discriminate. -Qed. - -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. apply preg_of_not_PC. -Qed. - -(** Connection between Mach and Asm calling conventions for external - functions. *) - -Lemma extcall_arg_match: - forall ms sp rs m m' l v, - agree ms sp rs -> - Machsem.extcall_arg ms m sp l v -> - Mem.extends m m' -> - exists v', Asm.extcall_arg rs m' l v' /\ Val.lessdef v v'. -Proof. - intros. inv H0. - exists (rs#(preg_of r)); split. constructor. eauto with ppcgen. - 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; eauto. -Qed. - -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'. -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. -Qed. - -Lemma extcall_arguments_match: - forall ms m sp rs sg args m', - agree ms sp rs -> - Machsem.extcall_arguments ms m sp sg args -> - Mem.extends m m' -> - 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. - -(** Translation of arguments to annotations. *) - -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. - -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 ARM 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. - -Lemma exec_straight_four: - forall i1 i2 i3 i4 c rs1 m1 rs2 m2 rs3 m3 rs4 m4 rs5 m5, - 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 -> - exec_instr ge fn i4 rs4 m4 = OK rs5 m5 -> - rs2#PC = Val.add rs1#PC Vone -> - rs3#PC = Val.add rs2#PC Vone -> - rs4#PC = Val.add rs3#PC Vone -> - rs5#PC = Val.add rs4#PC Vone -> - exec_straight (i1 :: i2 :: i3 :: i4 :: c) rs1 m1 c rs5 m5. -Proof. - intros. apply exec_straight_step with rs2 m2; auto. - eapply exec_straight_three; eauto. -Qed. - -(** * Correctness of ARM constructor functions *) +Variable fn: function. (** Decomposition of an integer constant *) @@ -606,12 +196,12 @@ Lemma iterate_op_correct: forall op1 op2 (f: val -> int -> val) (rs: regset) (r: ireg) m v0 n k, (forall (rs:regset) n, exec_instr ge fn (op2 (SOimm n)) rs m = - OK (nextinstr (rs#r <- (f (rs#r) n))) m) -> + Next (nextinstr (rs#r <- (f (rs#r) n))) m) -> (forall n, exec_instr ge fn (op1 (SOimm n)) rs m = - OK (nextinstr (rs#r <- (f v0 n))) m) -> + Next (nextinstr (rs#r <- (f v0 n))) m) -> exists rs', - exec_straight (iterate_op op1 op2 (decompose_int n) k) rs m k rs' m + exec_straight ge fn (iterate_op op1 op2 (decompose_int n) k) rs m k rs' m /\ rs'#r = List.fold_left f (decompose_int n) v0 /\ forall r': preg, r' <> r -> r' <> PC -> rs'#r' = rs#r'. Proof. @@ -623,8 +213,7 @@ Proof. (* base case *) intros; simpl. econstructor. split. apply exec_straight_one. rewrite SEM1. reflexivity. reflexivity. - split. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. auto. - intros. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gso; auto with ppcgen. + intuition Simpl. (* inductive case *) intros. rewrite List.map_app. simpl. rewrite app_ass. simpl. @@ -632,9 +221,8 @@ Proof. econstructor. split. eapply exec_straight_trans. eexact A. apply exec_straight_one. rewrite SEM2. reflexivity. reflexivity. - split. rewrite fold_left_app; simpl. rewrite nextinstr_inv; auto with ppcgen. - rewrite Pregmap.gss. rewrite B. auto. - intros. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gso; auto with ppcgen. + split. rewrite fold_left_app; simpl. Simpl. rewrite B. auto. + intros; Simpl. Qed. (** Loading a constant. *) @@ -642,7 +230,7 @@ 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. @@ -667,7 +255,7 @@ Qed. Lemma addimm_correct: forall r1 r2 n k rs m, 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. @@ -693,9 +281,8 @@ Qed. Lemma andimm_correct: forall r1 r2 n k rs m, - r2 <> IR14 -> 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': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'. Proof. @@ -704,7 +291,7 @@ Proof. case (is_immed_arith n). exists (nextinstr (rs#r1 <- (Val.and rs#r2 (Vint n)))). split. apply exec_straight_one; auto. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. + split. rewrite nextinstr_inv; auto with asmgen. apply Pregmap.gss. intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. (* bic - bic* *) replace (Val.and (rs r2) (Vint n)) @@ -720,7 +307,7 @@ Qed. Lemma rsubimm_correct: forall r1 r2 n k rs m, exists rs', - exec_straight (rsubimm r1 r2 n k) rs m k rs' m + exec_straight ge fn (rsubimm r1 r2 n k) rs m k rs' m /\ rs'#r1 = Val.sub (Vint n) rs#r2 /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'. Proof. @@ -741,7 +328,7 @@ Qed. Lemma orimm_correct: forall r1 r2 n k rs m, 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 = Val.or rs#r2 (Vint n) /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'. Proof. @@ -760,7 +347,7 @@ Qed. Lemma xorimm_correct: forall r1 r2 n k rs m, 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 = Val.xor rs#r2 (Vint n) /\ forall r': preg, r' <> r1 -> r' <> PC -> rs'#r' = rs#r'. Proof. @@ -780,7 +367,7 @@ Lemma loadind_int_correct: forall (base: ireg) ofs dst (rs: regset) m v k, Mem.loadv Mint32 m (Val.add rs#base (Vint ofs)) = Some v -> exists rs', - exec_straight (loadind_int base ofs dst k) rs m k rs' m + exec_straight ge fn (loadind_int base ofs dst k) rs m k rs' m /\ rs'#dst = v /\ forall r, r <> PC -> r <> IR14 -> r <> dst -> rs'#r = rs#r. Proof. @@ -788,23 +375,21 @@ Proof. exists (nextinstr (rs#dst <- v)). split. apply exec_straight_one. simpl. unfold exec_load. rewrite H. auto. auto. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + intuition Simpl. exploit addimm_correct. intros [rs' [A [B C]]]. exists (nextinstr (rs'#dst <- v)). split. eapply exec_straight_trans. eauto. apply exec_straight_one. simpl. unfold exec_load. rewrite B. rewrite Val.add_assoc. simpl. rewrite Int.add_zero. rewrite H. auto. auto. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. + intuition Simpl. Qed. Lemma loadind_float_correct: forall (base: ireg) ofs dst (rs: regset) m v k, Mem.loadv Mfloat64al32 m (Val.add rs#base (Vint ofs)) = Some v -> exists rs', - exec_straight (loadind_float base ofs dst k) rs m k rs' m + exec_straight ge fn (loadind_float base ofs dst k) rs m k rs' m /\ rs'#dst = v /\ forall r, r <> PC -> r <> IR14 -> r <> dst -> rs'#r = rs#r. Proof. @@ -812,33 +397,29 @@ Proof. exists (nextinstr (rs#dst <- v)). split. apply exec_straight_one. simpl. unfold exec_load. rewrite H. auto. auto. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + intuition Simpl. exploit addimm_correct. eauto. intros [rs' [A [B C]]]. exists (nextinstr (rs'#dst <- v)). split. eapply exec_straight_trans. eauto. apply exec_straight_one. simpl. unfold exec_load. rewrite B. rewrite Val.add_assoc. simpl. rewrite Int.add_zero. rewrite H. auto. auto. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. + intuition Simpl. Qed. Lemma loadind_correct: - forall (base: ireg) ofs ty dst k (rs: regset) m v, + forall (base: ireg) ofs ty dst k c (rs: regset) m v, + 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 -> 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 <> IR14 -> 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. - unfold preg_of. rewrite H0. destruct ty. - apply loadind_int_correct; auto. - apply loadind_float_correct; auto. + unfold loadind; intros. + destruct ty; monadInv H. + erewrite ireg_of_eq by eauto. apply loadind_int_correct; auto. + erewrite freg_of_eq by eauto. apply loadind_float_correct; auto. Qed. (** Indexed memory stores. *) @@ -848,37 +429,36 @@ Lemma storeind_int_correct: Mem.storev Mint32 m (Val.add rs#base (Vint ofs)) (rs#src) = Some m' -> src <> IR14 -> exists rs', - exec_straight (storeind_int src base ofs k) rs m k rs' m' + exec_straight ge fn (storeind_int src base ofs k) rs m k rs' m' /\ forall r, r <> PC -> r <> IR14 -> rs'#r = rs#r. Proof. intros; unfold storeind_int. destruct (is_immed_mem_word ofs). exists (nextinstr rs). split. apply exec_straight_one. simpl. unfold exec_store. rewrite H. auto. auto. - intros. rewrite nextinstr_inv; auto. + intuition Simpl. exploit addimm_correct. eauto. intros [rs' [A [B C]]]. exists (nextinstr rs'). split. eapply exec_straight_trans. eauto. apply exec_straight_one. simpl. unfold exec_store. rewrite B. rewrite C. rewrite Val.add_assoc. simpl. rewrite Int.add_zero. rewrite H. auto. - congruence. auto with ppcgen. auto. - intros. rewrite nextinstr_inv; auto. + congruence. auto with asmgen. auto. + intuition Simpl. Qed. Lemma storeind_float_correct: forall (base: ireg) ofs (src: freg) (rs: regset) m m' k, Mem.storev Mfloat64al32 m (Val.add rs#base (Vint ofs)) (rs#src) = Some m' -> - base <> IR14 -> exists rs', - exec_straight (storeind_float src base ofs k) rs m k rs' m' + exec_straight ge fn (storeind_float src base ofs k) rs m k rs' m' /\ forall r, r <> PC -> r <> IR14 -> rs'#r = rs#r. Proof. intros; unfold storeind_float. destruct (is_immed_mem_float ofs). exists (nextinstr rs). split. apply exec_straight_one. simpl. unfold exec_store. rewrite H. auto. auto. - intros. rewrite nextinstr_inv; auto. + intuition Simpl. exploit addimm_correct. eauto. intros [rs' [A [B C]]]. exists (nextinstr rs'). split. eapply exec_straight_trans. eauto. apply exec_straight_one. @@ -886,22 +466,23 @@ Proof. rewrite C. rewrite Val.add_assoc. simpl. rewrite Int.add_zero. rewrite H. auto. congruence. congruence. - auto with ppcgen. - intros. rewrite nextinstr_inv; auto. + auto with asmgen. + intuition Simpl. Qed. Lemma storeind_correct: - forall (base: ireg) ofs ty src k (rs: regset) m m', + forall (base: ireg) ofs ty src k c (rs: regset) m m', + 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 <> IR14 -> 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 <> IR14 -> rs'#r = rs#r. Proof. - intros. unfold storeind. unfold preg_of in H. rewrite H0 in H. destruct ty. - apply storeind_int_correct. auto. auto. auto with ppcgen. - apply storeind_float_correct. auto. auto. + unfold storeind; intros. + destruct ty; monadInv H. + erewrite ireg_of_eq in H0 by eauto. apply storeind_int_correct; auto. + assert (IR x <> IR IR14) by eauto with asmgen. congruence. + erewrite freg_of_eq in H0 by eauto. apply storeind_float_correct; auto. Qed. (** Translation of shift immediates *) @@ -935,11 +516,10 @@ Lemma compare_int_spec: /\ rs1#CRlt = (Val.cmp Clt v1 v2) /\ rs1#CRgt = (Val.cmp Cgt v1 v2) /\ rs1#CRle = (Val.cmp Cle v1 v2) - /\ forall r', important_preg r' = true -> rs1#r' = rs#r'. + /\ forall r', data_preg r' = true -> rs1#r' = rs#r'. Proof. - intros. unfold rs1. intuition; try reflexivity. - rewrite nextinstr_inv; auto with ppcgen. - unfold compare_int. repeat rewrite Pregmap.gso; auto with ppcgen. + intros. unfold rs1. intuition; try reflexivity. + unfold compare_int. Simpl. Qed. Lemma compare_float_spec: @@ -955,43 +535,43 @@ Lemma compare_float_spec: /\ rs'#CRlt = (Val.notbool (Val.cmpf Cge v1 v2)) /\ rs'#CRgt = (Val.cmpf Cgt v1 v2) /\ rs'#CRle = (Val.notbool (Val.cmpf Cgt v1 v2)) - /\ forall r', important_preg r' = true -> rs'#r' = rs#r'. -Proof. - intros. unfold rs'. intuition; try reflexivity. - rewrite nextinstr_inv; auto with ppcgen. - unfold compare_float. repeat rewrite Pregmap.gso; auto with ppcgen. -Qed. - -Ltac TypeInv1 := - match goal with - | H: (List.map ?f ?x = nil) |- _ => - destruct x; inv H; TypeInv1 - | H: (List.map ?f ?x = ?hd :: ?tl) |- _ => - destruct x; simpl in H; simplify_eq H; clear H; intros; TypeInv1 - | _ => idtac - end. - -Ltac TypeInv2 := - match goal with - | H: (mreg_type _ = Tint) |- _ => try (rewrite H in *); clear H; TypeInv2 - | H: (mreg_type _ = Tfloat) |- _ => try (rewrite H in *); clear H; TypeInv2 - | _ => idtac - end. - -Ltac TypeInv := TypeInv1; simpl in *; unfold preg_of in *; TypeInv2. + /\ forall r', data_preg r' = true -> rs'#r' = rs#r'. +Proof. + intros. unfold rs'. intuition; try reflexivity. + unfold compare_float. Simpl. +Qed. + +Definition lock {A: Type} (x: A) := x. + +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 ?x = OK ?y |- _ ] => + simpl in *; rewrite (ireg_of_eq _ _ H) in * +(*; change H with (lock (ireg_of x) = OK y)*) + | [ H: freg_of ?x = OK ?y |- _ ] => + simpl in *; rewrite (freg_of_eq _ _ H) in * +(*; change H with (lock (freg_of x) = OK y)*) + end). Lemma transl_cond_correct: - 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 /\ match eval_condition cond (map rs (map preg_of args)) m with | Some b => rs'#(CR (crbit_for_cond cond)) = Val.of_bool b | None => True end - /\ forall r, important_preg r = true -> rs'#r = rs r. + /\ forall r, data_preg r = true -> rs'#r = rs r. Proof. - intros until m; intros TY. + intros until c; intros TR. assert (MATCH: forall v ob, v = Val.of_optbool ob -> match ob with Some b => v = Val.of_bool b | None => True end). @@ -1006,268 +586,251 @@ Proof. intros. destruct v1; simpl; auto; destruct v2; simpl; auto. unfold Val.cmpu, Val.cmpu_bool in H. subst v. destruct H0; subst cmp; auto. - destruct cond; simpl in TY; TypeInv; simpl. - (* Ccomp *) - generalize (compare_int_spec rs (rs (ireg_of m0)) (rs (ireg_of m1)) m). - intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. + unfold transl_cond in TR; destruct cond; ArgsInv. +- (* Ccomp *) + generalize (compare_int_spec rs (rs x) (rs x0) m). + intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. destruct c; (apply MATCH; assumption) || (apply MATCH2; auto). + split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). auto. - (* Ccompu *) - generalize (compare_int_spec rs (rs (ireg_of m0)) (rs (ireg_of m1)) m). - intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. +- (* Ccompu *) + generalize (compare_int_spec rs (rs x) (rs x0) m). + intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. destruct c; apply MATCH; assumption. + split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). auto. - (* Ccompshift *) - generalize (compare_int_spec rs (rs (ireg_of m0)) (eval_shift s (rs (ireg_of m1))) m). - intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. +- (* Ccompshift *) + generalize (compare_int_spec rs (rs x) (eval_shift s (rs x0)) m). + intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. rewrite transl_shift_correct. destruct c; (apply MATCH; assumption) || (apply MATCH2; auto). - rewrite transl_shift_correct. auto. - (* Ccompushift *) - generalize (compare_int_spec rs (rs (ireg_of m0)) (eval_shift s (rs (ireg_of m1))) m). - intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. + rewrite transl_shift_correct. + split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). + auto. +- (* Ccompushift *) + generalize (compare_int_spec rs (rs x) (eval_shift s (rs x0)) m). + intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. rewrite transl_shift_correct. destruct c; apply MATCH; assumption. - rewrite transl_shift_correct. auto. - (* Ccompimm *) + rewrite transl_shift_correct. + split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). + auto. +- (* Ccompimm *) destruct (is_immed_arith i). - generalize (compare_int_spec rs (rs (ireg_of m0)) (Vint i) m). - intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. + generalize (compare_int_spec rs (rs x) (Vint i) m). + intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. destruct c; (apply MATCH; assumption) || (apply MATCH2; auto). + split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). auto. exploit (loadimm_correct IR14). intros [rs' [P [Q R]]]. - generalize (compare_int_spec rs' (rs (ireg_of m0)) (Vint i) m). - intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. + generalize (compare_int_spec rs' (rs x) (Vint i) m). + intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. eapply exec_straight_trans. eexact P. apply exec_straight_one. simpl. - rewrite Q. rewrite R; eauto with ppcgen. auto. - split. destruct c; (apply MATCH; assumption) || (apply MATCH2; auto). - intros. rewrite K; auto with ppcgen. - (* Ccompuimm *) + rewrite Q. rewrite R; eauto with asmgen. auto. + split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). + intros. rewrite C; auto with asmgen. +- (* Ccompuimm *) destruct (is_immed_arith i). - generalize (compare_int_spec rs (rs (ireg_of m0)) (Vint i) m). - intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. + generalize (compare_int_spec rs (rs x) (Vint i) m). + intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. destruct c; apply MATCH; assumption. + split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). auto. exploit (loadimm_correct IR14). intros [rs' [P [Q R]]]. - generalize (compare_int_spec rs' (rs (ireg_of m0)) (Vint i) m). - intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. + generalize (compare_int_spec rs' (rs x) (Vint i) m). + intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. eapply exec_straight_trans. eexact P. apply exec_straight_one. simpl. - rewrite Q. rewrite R; eauto with ppcgen. auto. - split. destruct c; apply MATCH; assumption. - intros. rewrite K; auto with ppcgen. - (* Ccompf *) - generalize (compare_float_spec rs (rs (freg_of m0)) (rs (freg_of m1))). - intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. + rewrite Q. rewrite R; eauto with asmgen. auto. + split. destruct c0; (apply MATCH; assumption) || (apply MATCH2; auto). + intros. rewrite C; auto with asmgen. +- (* Ccompf *) + generalize (compare_float_spec rs (rs x) (rs x0)). + intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. case c; apply MATCH; assumption. + split. case c0; apply MATCH; assumption. auto. - (* Cnotcompf *) - generalize (compare_float_spec rs (rs (freg_of m0)) (rs (freg_of m1))). - intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. +- (* Cnotcompf *) + generalize (compare_float_spec rs (rs x) (rs x0)). + intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. rewrite <- Val.negate_cmpf_ne in B. rewrite <- Val.negate_cmpf_eq in A. - destruct c; apply MATCH; simpl; rewrite Val.notbool_negb_3; auto. + split. rewrite <- Val.negate_cmpf_ne in C2. rewrite <- Val.negate_cmpf_eq in C1. + destruct c0; apply MATCH; simpl; rewrite Val.notbool_negb_3; auto. auto. - (* Ccompfzero *) - generalize (compare_float_spec rs (rs (freg_of m0)) (Vfloat Float.zero)). - intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. +- (* Ccompfzero *) + generalize (compare_float_spec rs (rs x) (Vfloat Float.zero)). + intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. case c; apply MATCH; assumption. + split. case c0; apply MATCH; assumption. auto. - (* Cnotcompf *) - generalize (compare_float_spec rs (rs (freg_of m0)) (Vfloat Float.zero)). - intros [A [B [C [D [E [F [G [H [I [J K]]]]]]]]]]. +- (* Cnotcompf *) + generalize (compare_float_spec rs (rs x) (Vfloat Float.zero)). + intros (C1 & C2 & C3 & C4 & C5 & C6 & C7 & C8 & C9 & C10 & C). econstructor. split. apply exec_straight_one. simpl. eauto. auto. - split. rewrite <- Val.negate_cmpf_ne in B. rewrite <- Val.negate_cmpf_eq in A. - destruct c; apply MATCH; simpl; rewrite Val.notbool_negb_3; auto. + split. rewrite <- Val.negate_cmpf_ne in C2. rewrite <- Val.negate_cmpf_eq in C1. + destruct c0; apply MATCH; simpl; rewrite Val.notbool_negb_3; auto. auto. Qed. (** Translation of arithmetic operations. *) -Ltac Simpl := - match goal with - | [ |- context[nextinstr _ _] ] => rewrite nextinstr_inv; [auto | auto with ppcgen] - | [ |- context[Pregmap.get ?x (Pregmap.set ?x _ _)] ] => rewrite Pregmap.gss; auto - | [ |- context[Pregmap.set ?x _ _ ?x] ] => rewrite Pregmap.gss; auto - | [ |- context[Pregmap.get _ (Pregmap.set _ _ _)] ] => rewrite Pregmap.gso; [auto | auto with ppcgen] - | [ |- context[Pregmap.set _ _ _ _] ] => rewrite Pregmap.gso; [auto | auto with ppcgen] - end. - Ltac TranslOpSimpl := econstructor; split; [ apply exec_straight_one; [simpl; eauto | reflexivity ] | split; [try rewrite transl_shift_correct; repeat Simpl | intros; repeat Simpl] ]. Lemma transl_op_correct_same: - forall op args res k (rs: regset) m v, - wt_instr (Mop op args res) -> + forall op args res k c (rs: regset) m v, + transl_op op args res k = OK c -> eval_operation ge rs#IR13 op (map rs (map preg_of args)) m = Some v -> match op with Ocmp _ => False | _ => True end -> 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, important_preg r = true -> r <> preg_of res -> rs'#r = rs#r. + /\ forall r, data_preg r = true -> r <> preg_of res -> rs'#r = rs#r. Proof. - intros. inv H. + intros until v; intros TR EV NOCMP. + unfold transl_op in TR; destruct op; ArgsInv; simpl in EV; inv EV; try (TranslOpSimpl; fail). (* Omove *) - simpl in *. inv H0. - exists (nextinstr (rs#(preg_of res) <- (rs#(preg_of r1)))). - split. unfold preg_of; rewrite <- H3. - destruct (mreg_type r1); apply exec_straight_one; auto. - split. Simpl. Simpl. - intros. Simpl. Simpl. - (* Other instructions *) - destruct op; simpl in H6; inv H6; TypeInv; simpl in H0; inv H0; try (TranslOpSimpl; fail). + exists (nextinstr (rs#(preg_of res) <- (rs#(preg_of m0)))). + split. + destruct (preg_of res) eqn:RES; try discriminate; + destruct (preg_of m0) eqn:ARG; inv TR. + apply exec_straight_one; auto. + apply exec_straight_one; auto. + intuition Simpl. (* Ointconst *) - generalize (loadimm_correct (ireg_of res) i k rs m). intros [rs' [A [B C]]]. - exists rs'. split. auto. split. rewrite B; auto. intros. auto with ppcgen. + generalize (loadimm_correct x i k rs m). intros [rs' [A [B C]]]. + exists rs'; auto with asmgen. (* Oaddrstack *) - generalize (addimm_correct (ireg_of res) IR13 i k rs m). + generalize (addimm_correct x IR13 i k rs m). intros [rs' [EX [RES OTH]]]. - exists rs'. split. auto. split. auto. auto with ppcgen. + exists rs'; auto with asmgen. (* Oaddimm *) - generalize (addimm_correct (ireg_of res) (ireg_of m0) i k rs m). + generalize (addimm_correct x x0 i k rs m). intros [rs' [A [B C]]]. - exists rs'. split. auto. split. auto. auto with ppcgen. + exists rs'; auto with asmgen. (* Orsbimm *) - generalize (rsubimm_correct (ireg_of res) (ireg_of m0) i k rs m). + generalize (rsubimm_correct x x0 i k rs m). intros [rs' [A [B C]]]. - exists rs'. - split. eauto. split. rewrite B. auto. - auto with ppcgen. + exists rs'; auto with asmgen. (* Omul *) - destruct (ireg_eq (ireg_of res) (ireg_of m0) || ireg_eq (ireg_of res) (ireg_of m1)). + destruct (ireg_eq x x0 || ireg_eq x x1). econstructor; split. eapply exec_straight_two. simpl; eauto. simpl; eauto. auto. auto. - split. repeat Simpl. - intros. repeat Simpl. + intuition Simpl. TranslOpSimpl. (* divs *) - econstructor. split. apply exec_straight_one. simpl. rewrite H2. reflexivity. auto. - split. repeat Simpl. intros. repeat Simpl. + econstructor. split. apply exec_straight_one. simpl. rewrite H0. reflexivity. auto. + intuition Simpl. (* divu *) - econstructor. split. apply exec_straight_one. simpl. rewrite H2. reflexivity. auto. - split. repeat Simpl. intros. repeat Simpl. + econstructor. split. apply exec_straight_one. simpl. rewrite H0. reflexivity. auto. + intuition Simpl. (* Oandimm *) - generalize (andimm_correct (ireg_of res) (ireg_of m0) i k rs m - (ireg_of_not_IR14 m0)). + generalize (andimm_correct x x0 i k rs m). intros [rs' [A [B C]]]. - exists rs'; auto with ppcgen. + exists rs'; auto with asmgen. (* Oorimm *) - generalize (orimm_correct (ireg_of res) (ireg_of m0) i k rs m). + generalize (orimm_correct x x0 i k rs m). intros [rs' [A [B C]]]. - exists rs'; auto with ppcgen. + exists rs'; auto with asmgen. (* Oxorimm *) - generalize (xorimm_correct (ireg_of res) (ireg_of m0) i k rs m). + generalize (xorimm_correct x x0 i k rs m). intros [rs' [A [B C]]]. - exists rs'; auto with ppcgen. + exists rs'; auto with asmgen. (* Oshrximm *) exploit Val.shrx_shr; eauto. intros [n [i' [ARG1 [ARG2 RES]]]]. injection ARG2; intro ARG2'; subst i'; clear ARG2. set (islt := Int.lt n Int.zero) in *. set (rs1 := nextinstr (compare_int rs (Vint n) (Vint Int.zero) m)). - assert (OTH1: forall r', important_preg r' = true -> rs1#r' = rs#r'). + assert (OTH1: forall r', data_preg r' = true -> rs1#r' = rs#r'). generalize (compare_int_spec rs (Vint n) (Vint Int.zero) m). fold rs1. intros [A B]. intuition. - exploit (addimm_correct IR14 (ireg_of m0) (Int.sub (Int.shl Int.one i) Int.one)). + exploit (addimm_correct IR14 x0 (Int.sub (Int.shl Int.one i) Int.one)). intros [rs2 [EXEC2 [RES2 OTH2]]]. set (rs3 := nextinstr (if islt then rs2 else rs2#IR14 <- (Vint n))). - set (rs4 := nextinstr (rs3#(ireg_of res) <- (Val.shr rs3#IR14 (Vint i)))). + set (rs4 := nextinstr (rs3#x <- (Val.shr rs3#IR14 (Vint i)))). exists rs4; split. apply exec_straight_step with rs1 m. simpl. rewrite ARG1. auto. auto. eapply exec_straight_trans. eexact EXEC2. apply exec_straight_two with rs3 m. - simpl. rewrite OTH2. change (rs1 CRge) with (Val.cmp Cge (Vint n) (Vint Int.zero)). + simpl. rewrite OTH2; eauto with asmgen. + change (rs1 CRge) with (Val.cmp Cge (Vint n) (Vint Int.zero)). unfold Val.cmp, Val.cmp_bool. change (Int.cmp Cge n Int.zero) with (negb islt). - rewrite OTH2. rewrite OTH1. rewrite ARG1. + rewrite OTH2; eauto with asmgen. rewrite OTH1. rewrite ARG1. unfold rs3. case islt; reflexivity. - destruct m0; reflexivity. auto with ppcgen. auto with ppcgen. discriminate. discriminate. - simpl. auto. - auto. unfold rs3. case islt; auto. auto. - split. unfold rs4. repeat Simpl. unfold rs3. Simpl. destruct islt. - rewrite RES2. change (rs1 (IR (ireg_of m0))) with (rs (IR (ireg_of m0))). auto. - Simpl. rewrite <- ARG1; auto. - intros. unfold rs4; repeat Simpl. unfold rs3; repeat Simpl. - transitivity (rs2 r). destruct islt; auto. Simpl. - rewrite OTH2; auto with ppcgen. + rewrite <- (ireg_of_eq _ _ EQ1). auto with asmgen. + auto. + unfold rs3. destruct islt; auto. auto. + split. unfold rs4; Simpl. unfold rs3. destruct islt. + Simpl. rewrite RES2. unfold rs1. Simpl. + Simpl. congruence. + intros. unfold rs4, rs3; Simpl. destruct islt; Simpl; rewrite OTH2; auto with asmgen. (* intoffloat *) - econstructor; split. apply exec_straight_one; simpl. rewrite H2; simpl. eauto. auto. - split; intros; repeat Simpl. + econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto. + intuition Simpl. (* intuoffloat *) - econstructor; split. apply exec_straight_one; simpl. rewrite H2; simpl. eauto. auto. - split; intros; repeat Simpl. + econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto. + intuition Simpl. (* floatofint *) - econstructor; split. apply exec_straight_one; simpl. rewrite H2; simpl. eauto. auto. - split; intros; repeat Simpl. + econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto. + intuition Simpl. (* floatofintu *) - econstructor; split. apply exec_straight_one; simpl. rewrite H2; simpl. eauto. auto. - split; intros; repeat Simpl. + econstructor; split. apply exec_straight_one; simpl. rewrite H0; simpl. eauto. auto. + intuition Simpl. (* Ocmp *) contradiction. Qed. Lemma transl_op_correct: - forall op args res k (rs: regset) m v, - wt_instr (Mop op args res) -> + forall op args res k c (rs: regset) m v, + transl_op op args res k = OK c -> eval_operation ge rs#IR13 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 /\ Val.lessdef v rs'#(preg_of res) - /\ forall r, important_preg r = true -> r <> preg_of res -> rs'#r = rs#r. + /\ forall r, data_preg r = true -> r <> preg_of res -> rs'#r = rs#r. Proof. intros. assert (EITHER: match op with Ocmp _ => False | _ => True end \/ exists cmp, op = Ocmp cmp). - destruct op; auto. right; exists c; auto. - destruct EITHER as [A | [c A]]. + destruct op; auto. right; exists c0; auto. + destruct EITHER as [A | [cmp A]]. exploit transl_op_correct_same; eauto. intros [rs' [P [Q R]]]. subst v. exists rs'; eauto. (* Ocmp *) - subst op. inv H. simpl in H5. inv H5. simpl in H0. inv H0. - destruct (transl_cond_correct c args - (Pmov (ireg_of res) (SOimm Int.zero) - :: Pmovc (crbit_for_cond c) (ireg_of res) (SOimm Int.one) :: k) - rs m H1) - as [rs1 [A [B C]]]. - set (rs2 := nextinstr (rs1#(ireg_of res) <- (Vint Int.zero))). - set (v := match rs2#(crbit_for_cond c) with - | Vint n => if Int.eq n Int.zero then Vint Int.zero else Vint Int.one - | _ => Vundef - end). - set (rs3 := nextinstr (rs2#(ireg_of res) <- v)). + subst op. simpl in H. monadInv H. simpl in H0. inv H0. + rewrite (ireg_of_eq _ _ EQ). + exploit transl_cond_correct; eauto. instantiate (1 := rs). instantiate (1 := m). intros [rs1 [A [B C]]]. + set (rs2 := nextinstr (rs1#x <- (Vint Int.zero))). + set (rs3 := nextinstr (match rs2#(crbit_for_cond cmp) with + | Vint n => if Int.eq n Int.zero then rs2 else rs2#x <- Vone + | _ => rs2#x <- Vundef + end)). exists rs3; split. - eapply exec_straight_trans. eauto. - apply exec_straight_two with rs2 m; auto. - simpl. unfold rs3, v. - destruct (rs2 (crbit_for_cond c)) eqn:?; auto. - destruct (Int.eq i Int.zero); auto. - decEq. decEq. apply extensionality; intros. unfold Pregmap.set. - destruct (PregEq.eq x (ireg_of res)); auto. subst. - unfold rs2. Simpl. Simpl. - replace (preg_of res) with (IR (ireg_of res)). - split. unfold rs3. Simpl. Simpl. - destruct (eval_condition c rs ## (preg_of ## args) m); simpl; auto. - unfold v. unfold rs2. Simpl. Simpl. rewrite B. - destruct b; simpl; auto. - intros. unfold rs3. repeat Simpl. unfold rs2. repeat Simpl. - unfold preg_of; rewrite H2; auto. + eapply exec_straight_trans. eexact A. apply exec_straight_two with rs2 m. + auto. + simpl. unfold rs3. destruct (rs2 (crbit_for_cond cmp)); auto. destruct (Int.eq i Int.zero); auto. + auto. unfold rs3. destruct (rs2 (crbit_for_cond cmp)); auto. destruct (Int.eq i Int.zero); auto. + split. unfold rs3. Simpl. + replace (rs2 (crbit_for_cond cmp)) with (rs1 (crbit_for_cond cmp)). + destruct (eval_condition cmp rs##(preg_of##args) m) as [[]|]; simpl in *. + rewrite B. simpl. Simpl. + rewrite B. simpl. unfold rs2. Simpl. + auto. + destruct cmp; reflexivity. + intros. transitivity (rs2 r). + unfold rs3. destruct (rs2 (crbit_for_cond cmp)); Simpl. destruct (Int.eq i Int.zero); auto; Simpl. + unfold rs2. Simpl. Qed. Remark val_add_add_zero: @@ -1276,43 +839,40 @@ Proof. intros. destruct v1; destruct v2; simpl; auto; rewrite Int.add_zero; auto. Qed. -Lemma transl_load_store_correct: - forall (mk_instr_imm: ireg -> int -> instruction) +Lemma transl_memory_access_correct: + forall (P: regset -> Prop) (mk_instr_imm: ireg -> int -> instruction) (mk_instr_gen: option (ireg -> shift_addr -> instruction)) (is_immed: int -> bool) - addr args k ms sp rs m ms' m', + addr args k c (rs: regset) a m m', + transl_memory_access mk_instr_imm mk_instr_gen is_immed addr args k = OK c -> + eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a -> (forall (r1: ireg) (rs1: regset) n k, - eval_addressing ge sp addr (map rs (map preg_of args)) = Some(Val.add rs1#r1 (Vint n)) -> + Val.add rs1#r1 (Vint n) = a -> (forall (r: preg), r <> PC -> r <> IR14 -> rs1 r = rs r) -> exists rs', - exec_straight (mk_instr_imm r1 n :: k) rs1 m k rs' m' /\ - agree ms' sp rs') -> + exec_straight ge fn (mk_instr_imm r1 n :: k) rs1 m k rs' m' /\ P rs') -> match mk_instr_gen with | None => True | Some mk => (forall (r1: ireg) (sa: shift_addr) (rs1: regset) k, - eval_addressing ge sp addr (map rs (map preg_of args)) = Some(Val.add rs1#r1 (eval_shift_addr sa rs1)) -> + Val.add rs1#r1 (eval_shift_addr sa rs1) = a -> (forall (r: preg), r <> PC -> r <> IR14 -> rs1 r = rs r) -> exists rs', - exec_straight (mk r1 sa :: k) rs1 m k rs' m' /\ - agree ms' sp rs') + exec_straight ge fn (mk r1 sa :: k) rs1 m k rs' m' /\ P rs') end -> - agree ms sp rs -> - map mreg_type args = type_of_addressing addr -> exists rs', - exec_straight (transl_load_store mk_instr_imm mk_instr_gen is_immed addr args 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 EA MK1 MK2. + unfold transl_memory_access in TR; destruct addr; ArgsInv; simpl in EA; inv EA. (* Aindexed *) case (is_immed i). (* Aindexed, small displacement *) - apply H; auto. + apply MK1; auto. (* Aindexed, large displacement *) - destruct (addimm_correct IR14 (ireg_of m0) i (mk_instr_imm IR14 Int.zero :: k) rs m) + destruct (addimm_correct IR14 x i (mk_instr_imm IR14 Int.zero :: k) rs m) as [rs' [A [B C]]]. - exploit (H IR14 rs' Int.zero); eauto. + exploit (MK1 IR14 rs' Int.zero); eauto. rewrite B. rewrite Val.add_assoc. simpl Val.add. rewrite Int.add_zero. reflexivity. intros [rs'' [D E]]. exists rs''; split. @@ -1320,13 +880,12 @@ Proof. (* Aindexed2 *) destruct mk_instr_gen as [mk | ]. (* binary form available *) - apply H0; auto. + apply MK2; auto. (* binary form not available *) - set (rs' := nextinstr (rs#IR14 <- (Val.add (rs (ireg_of m0)) (rs (ireg_of m1))))). - exploit (H IR14 rs' Int.zero); eauto. - unfold rs'. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - decEq. apply val_add_add_zero. - unfold rs'. intros. repeat Simpl. + set (rs' := nextinstr (rs#IR14 <- (Val.add (rs x) (rs x0)))). + exploit (MK1 IR14 rs' Int.zero); eauto. + unfold rs'. Simpl. symmetry. apply val_add_add_zero. + intros. unfold rs'. Simpl. intros [rs'' [A B]]. exists rs''; split. eapply exec_straight_step with (rs2 := rs'); eauto. @@ -1334,189 +893,172 @@ Proof. (* Aindexed2shift *) destruct mk_instr_gen as [mk | ]. (* binary form available *) - apply H0; auto. rewrite transl_shift_addr_correct. auto. + apply MK2; auto. rewrite transl_shift_addr_correct. auto. (* binary form not available *) - set (rs' := nextinstr (rs#IR14 <- (Val.add (rs (ireg_of m0)) (eval_shift s (rs (ireg_of m1)))))). - exploit (H IR14 rs' Int.zero); eauto. - unfold rs'. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - decEq. apply val_add_add_zero. - unfold rs'; intros; repeat Simpl. + set (rs' := nextinstr (rs#IR14 <- (Val.add (rs x) (eval_shift s (rs x0))))). + exploit (MK1 IR14 rs' Int.zero); eauto. + unfold rs'. Simpl. symmetry. apply val_add_add_zero. + intros; unfold rs'; Simpl. intros [rs'' [A B]]. exists rs''; split. eapply exec_straight_step with (rs2 := rs'); eauto. simpl. rewrite transl_shift_correct. auto. auto. (* Ainstack *) - destruct (is_immed i). + destruct (is_immed i); inv TR. (* Ainstack, short displacement *) - apply H; auto. rewrite (sp_val _ _ _ H1). auto. + apply MK1; auto. (* Ainstack, large displacement *) destruct (addimm_correct IR14 IR13 i (mk_instr_imm IR14 Int.zero :: k) rs m) as [rs' [A [B C]]]. - exploit (H IR14 rs' Int.zero); eauto. - rewrite (sp_val _ _ _ H1). rewrite B. rewrite Val.add_assoc. simpl Val.add. rewrite Int.add_zero. auto. + exploit (MK1 IR14 rs' Int.zero); eauto. + rewrite B. rewrite Val.add_assoc. f_equal. simpl. rewrite Int.add_zero; auto. intros [rs'' [D E]]. exists rs''; split. eapply exec_straight_trans. eexact A. eexact D. auto. Qed. Lemma transl_load_int_correct: - forall (mk_instr: ireg -> ireg -> shift_addr -> instruction) - (is_immed: int -> bool) - (rd: mreg) addr args k ms sp rs m m' chunk a v, - (forall (c: code) (r1 r2: ireg) (sa: shift_addr) (rs1: regset), - exec_instr ge c (mk_instr r1 r2 sa) rs1 m' = - exec_load chunk (Val.add rs1#r2 (eval_shift_addr sa rs1)) r1 rs1 m') -> - agree ms sp rs -> - map mreg_type args = type_of_addressing addr -> - mreg_type rd = Tint -> - eval_addressing ge sp addr (map ms args) = Some a -> + forall mk_instr is_immed dst addr args k c (rs: regset) a chunk m v, + transl_memory_access_int mk_instr is_immed dst addr args k = OK c -> + eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a -> Mem.loadv chunk m a = Some v -> - Mem.extends m m' -> + (forall (r1 r2: ireg) (sa: shift_addr) (rs1: regset), + exec_instr ge fn (mk_instr r1 r2 sa) rs1 m = + exec_load chunk (Val.add rs1#r2 (eval_shift_addr sa rs1)) r1 rs1 m) -> exists rs', - exec_straight (transl_load_store_int mk_instr is_immed rd addr args k) rs m' - k rs' m' - /\ agree (Regmap.set rd v (undef_temps ms)) sp rs'. + exec_straight ge fn c rs m k rs' m + /\ rs'#(preg_of dst) = v + /\ forall r, nontemp_preg r = true -> r <> preg_of dst -> rs'#r = rs#r. Proof. - intros. unfold transl_load_store_int. - 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. - intros. - assert (Val.add (rs1 r1) (Vint n) = a') by congruence. - exists (nextinstr (rs1#(ireg_of rd) <- v')); split. - apply exec_straight_one. rewrite H. unfold exec_load. - simpl. rewrite H8. rewrite C. auto. auto. - apply agree_nextinstr. eapply agree_set_undef_mreg; eauto. - unfold preg_of. rewrite H2. rewrite Pregmap.gss. auto. - unfold preg_of. rewrite H2. intros. rewrite Pregmap.gso; auto. apply H7; auto with ppcgen. - intros. - assert (Val.add (rs1 r1) (eval_shift_addr sa rs1) = a') by congruence. - exists (nextinstr (rs1#(ireg_of rd) <- v')); split. - apply exec_straight_one. rewrite H. unfold exec_load. - simpl. rewrite H8. rewrite C. auto. auto. - apply agree_nextinstr. eapply agree_set_undef_mreg; eauto. - unfold preg_of. rewrite H2. rewrite Pregmap.gss. auto. - unfold preg_of. rewrite H2. intros. rewrite Pregmap.gso; auto. apply H7; auto with ppcgen. + intros. monadInv H. erewrite ireg_of_eq by eauto. + eapply transl_memory_access_correct; eauto. + intros; simpl. econstructor; split. apply exec_straight_one. + rewrite H2. unfold exec_load. simpl eval_shift_addr. rewrite H. rewrite H1. eauto. auto. + split. Simpl. intros; Simpl. + simpl; intros. + econstructor; split. apply exec_straight_one. + rewrite H2. unfold exec_load. rewrite H. rewrite H1. eauto. auto. + split. Simpl. intros; Simpl. Qed. Lemma transl_load_float_correct: - forall (mk_instr: freg -> ireg -> int -> instruction) - (is_immed: int -> bool) - (rd: mreg) addr args k ms sp rs m m' chunk a v, - (forall (c: code) (r1: freg) (r2: ireg) (n: int) (rs1: regset), - exec_instr ge c (mk_instr r1 r2 n) rs1 m' = - exec_load chunk (Val.add rs1#r2 (Vint n)) r1 rs1 m') -> - agree ms sp rs -> - map mreg_type args = type_of_addressing addr -> - mreg_type rd = Tfloat -> - eval_addressing ge sp addr (map ms args) = Some a -> + forall mk_instr is_immed dst addr args k c (rs: regset) a chunk m v, + transl_memory_access_float mk_instr is_immed dst addr args k = OK c -> + eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a -> Mem.loadv chunk m a = Some v -> - Mem.extends m m' -> + (forall (r1: freg) (r2: ireg) (n: int) (rs1: regset), + exec_instr ge fn (mk_instr r1 r2 n) rs1 m = + exec_load chunk (Val.add rs1#r2 (Vint n)) r1 rs1 m) -> exists rs', - exec_straight (transl_load_store_float mk_instr is_immed rd addr args k) rs m' - k rs' m' - /\ agree (Regmap.set rd v (undef_temps ms)) sp rs'. + exec_straight ge fn c rs m k rs' m + /\ rs'#(preg_of dst) = v + /\ forall r, nontemp_preg r = true -> r <> preg_of dst -> rs'#r = rs#r. Proof. - intros. unfold transl_load_store_int. - 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. - intros. - assert (Val.add (rs1 r1) (Vint n) = a') by congruence. - exists (nextinstr (rs1#(freg_of rd) <- v')); split. - apply exec_straight_one. rewrite H. unfold exec_load. - simpl. rewrite H8. rewrite C. auto. auto. - apply agree_nextinstr. eapply agree_set_undef_mreg; eauto. - unfold preg_of. rewrite H2. rewrite Pregmap.gss. auto. - unfold preg_of. rewrite H2. intros. rewrite Pregmap.gso; auto. apply H7; auto with ppcgen. + intros. monadInv H. erewrite freg_of_eq by eauto. + eapply transl_memory_access_correct; eauto. + intros; simpl. econstructor; split. apply exec_straight_one. + rewrite H2. unfold exec_load. rewrite H. rewrite H1. eauto. auto. + split. Simpl. intros; Simpl. + simpl; auto. Qed. Lemma transl_store_int_correct: - forall (mk_instr: ireg -> ireg -> shift_addr -> instruction) - (is_immed: int -> bool) - (rd: mreg) addr args k ms sp rs m1 chunk a m2 m1', - (forall (c: code) (r1 r2: ireg) (sa: shift_addr) (rs1: regset), - exec_instr ge c (mk_instr r1 r2 sa) rs1 m1' = - exec_store chunk (Val.add rs1#r2 (eval_shift_addr sa rs1)) r1 rs1 m1') -> - agree ms sp rs -> - map mreg_type args = type_of_addressing addr -> - mreg_type rd = Tint -> - eval_addressing ge sp addr (map ms args) = Some a -> - Mem.storev chunk m1 a (ms rd) = Some m2 -> - Mem.extends m1 m1' -> - exists m2', - Mem.extends m2 m2' /\ - exists rs', - exec_straight (transl_load_store_int mk_instr is_immed rd addr args k) rs m1' - k rs' m2' - /\ agree (undef_temps ms) sp rs'. -Proof. - intros. unfold transl_load_store_int. - exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. - unfold PregEq.t. - intros [a' [A B]]. - exploit preg_val; eauto. instantiate (1 := rd). intros C. - exploit Mem.storev_extends; eauto. unfold preg_of; rewrite H2. intros [m2' [D E]]. - exists m2'; split; auto. - apply transl_load_store_correct with ms; auto. - intros. - assert (Val.add (rs1 r1) (Vint n) = a') by congruence. - exists (nextinstr rs1); split. - apply exec_straight_one. rewrite H. simpl. rewrite H8. - unfold exec_store. rewrite H7; auto with ppcgen. rewrite D. auto. auto. - apply agree_nextinstr. apply agree_exten_temps with rs; auto with ppcgen. - intros. - assert (Val.add (rs1 r1) (eval_shift_addr sa rs1) = a') by congruence. - exists (nextinstr rs1); split. - apply exec_straight_one. rewrite H. simpl. rewrite H8. - unfold exec_store. rewrite H7; auto with ppcgen. rewrite D. auto. auto. - apply agree_nextinstr. apply agree_exten_temps with rs; auto with ppcgen. + forall mk_instr is_immed src addr args k c (rs: regset) a chunk m m', + transl_memory_access_int mk_instr is_immed src addr args k = OK c -> + eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a -> + Mem.storev chunk m a rs#(preg_of src) = Some m' -> + (forall (r1 r2: ireg) (sa: shift_addr) (rs1: regset), + exec_instr ge fn (mk_instr r1 r2 sa) rs1 m = + exec_store chunk (Val.add rs1#r2 (eval_shift_addr sa rs1)) r1 rs1 m) -> + exists rs', + exec_straight ge fn c rs m k rs' m' + /\ forall r, nontemp_preg r = true -> rs'#r = rs#r. +Proof. + intros. monadInv H. erewrite ireg_of_eq in * by eauto. + eapply transl_memory_access_correct; eauto. + intros; simpl. econstructor; split. apply exec_straight_one. + rewrite H2. unfold exec_store. simpl eval_shift_addr. rewrite H. rewrite H3; eauto with asmgen. + rewrite H1. eauto. auto. + intros; Simpl. + simpl; intros. + econstructor; split. apply exec_straight_one. + rewrite H2. unfold exec_store. rewrite H. rewrite H3; eauto with asmgen. + rewrite H1. eauto. auto. + intros; Simpl. Qed. Lemma transl_store_float_correct: - forall (mk_instr: freg -> ireg -> int -> instruction) - (is_immed: int -> bool) - (rd: mreg) addr args k ms sp rs m1 chunk a m2 m1', - (forall (c: code) (r1: freg) (r2: ireg) (n: int) (rs1: regset) m2', - exec_store chunk (Val.add rs1#r2 (Vint n)) r1 rs1 m1' = OK (nextinstr rs1) m2' -> - exists rs2, - exec_instr ge c (mk_instr r1 r2 n) rs1 m1' = OK rs2 m2' - /\ (forall (r: preg), r <> FR7 -> rs2 r = nextinstr rs1 r)) -> - agree ms sp rs -> - map mreg_type args = type_of_addressing addr -> - mreg_type rd = Tfloat -> - eval_addressing ge sp addr (map ms args) = Some a -> - Mem.storev chunk m1 a (ms rd) = Some m2 -> - Mem.extends m1 m1' -> - exists m2', - Mem.extends m2 m2' /\ - exists rs', - exec_straight (transl_load_store_float mk_instr is_immed rd addr args k) rs m1' - k rs' m2' - /\ agree (undef_temps ms) sp rs'. -Proof. - intros. unfold transl_load_store_float. - exploit eval_addressing_lessdef. eapply preg_vals; eauto. eauto. - unfold PregEq.t. - intros [a' [A B]]. - exploit preg_val; eauto. instantiate (1 := rd). intros C. - exploit Mem.storev_extends; eauto. unfold preg_of; rewrite H2. intros [m2' [D E]]. - exists m2'; split; auto. - apply transl_load_store_correct with ms; auto. - intros. - assert (Val.add (rs1 r1) (Vint n) = a') by congruence. - exploit (H fn (freg_of rd) r1 n rs1 m2'). - unfold exec_store. rewrite H8. rewrite H7; auto with ppcgen. rewrite D. auto. - intros [rs2 [P Q]]. - exists rs2; split. apply exec_straight_one. auto. rewrite Q; auto with ppcgen. - apply agree_exten_temps with rs; auto. - intros. rewrite Q; auto with ppcgen. Simpl. apply H7; auto with ppcgen. -Qed. + forall mk_instr is_immed src addr args k c (rs: regset) a chunk m m', + transl_memory_access_float mk_instr is_immed src addr args k = OK c -> + eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a -> + Mem.storev chunk m a rs#(preg_of src) = Some m' -> + (forall (r1: freg) (r2: ireg) (n: int) (rs1: regset), + exec_instr ge fn (mk_instr r1 r2 n) rs1 m = + exec_store chunk (Val.add rs1#r2 (Vint n)) r1 rs1 m) -> + exists rs', + exec_straight ge fn c rs m k rs' m' + /\ forall r, nontemp_preg r = true -> rs'#r = rs#r. +Proof. + intros. monadInv H. erewrite freg_of_eq in * by eauto. + eapply transl_memory_access_correct; eauto. + intros; simpl. econstructor; split. apply exec_straight_one. + rewrite H2. unfold exec_store. rewrite H. rewrite H3; eauto with asmgen. + rewrite H1. eauto. auto. + intros; Simpl. + simpl; auto. +Qed. + +Lemma transl_load_correct: + forall chunk addr args dst k c (rs: regset) a m v, + transl_load chunk addr args dst k = OK c -> + eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a -> + Mem.loadv chunk m a = Some v -> + exists rs', + exec_straight ge fn c rs m k rs' m + /\ rs'#(preg_of dst) = v + /\ forall r, nontemp_preg r = true -> r <> preg_of dst -> rs'#r = rs#r. +Proof. + intros. destruct chunk; simpl in H. + eapply transl_load_int_correct; eauto. + eapply transl_load_int_correct; eauto. + eapply transl_load_int_correct; eauto. + eapply transl_load_int_correct; eauto. + eapply transl_load_int_correct; eauto. + eapply transl_load_float_correct; eauto. + apply Mem.loadv_float64al32 in H1. eapply transl_load_float_correct; eauto. + eapply transl_load_float_correct; eauto. +Qed. + +Lemma transl_store_correct: + forall chunk addr args src k c (rs: regset) a m m', + transl_store chunk addr args src k = OK c -> + eval_addressing ge (rs#SP) 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, nontemp_preg r = true -> rs'#r = rs#r. +Proof. + intros. destruct chunk; simpl in H. +- 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 transl_store_int_correct; eauto. +- eapply transl_store_int_correct; eauto. +- 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 transl_store_int_correct; eauto. +- eapply transl_store_int_correct; eauto. +- eapply transl_store_int_correct; eauto. +- unfold transl_memory_access_float in H. monadInv H. rewrite (freg_of_eq _ _ EQ) in *. + eapply transl_memory_access_correct; eauto. + intros. econstructor; split. apply exec_straight_one. + simpl. unfold exec_store. rewrite H. rewrite H2; eauto with asmgen. + rewrite H1. eauto. auto. intros. Simpl. + simpl; auto. +- apply Mem.storev_float64al32 in H1. eapply transl_store_float_correct; eauto. +- eapply transl_store_float_correct; eauto. +Qed. + +End CONSTRUCTORS. -End STRAIGHTLINE. -- cgit