From 0f5087bea45be49e105727d6cee4194598474fee Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 5 Jul 2011 04:13:33 +0000 Subject: Back from Oregon commit. powerpc/*: better compilation of some comparisons; revised asmgenproof1. common/*: added Mem.storebytes; used to give semantics to memcpy builtin. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1679 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- common/Events.v | 116 +++++- common/Memdata.v | 13 +- common/Memory.v | 689 ++++++++++++++++++++++++++++++++++- common/Memtype.v | 169 +++++++++ common/Values.v | 6 + lib/Coqlib.v | 14 + lib/Integers.v | 10 + powerpc/Asm.v | 23 +- powerpc/Asmgen.v | 56 ++- powerpc/Asmgenproof.v | 72 ++-- powerpc/Asmgenproof1.v | 948 ++++++++++++++++++++++-------------------------- powerpc/Asmgenretaddr.v | 9 +- powerpc/PrintAsm.ml | 6 + 13 files changed, 1533 insertions(+), 598 deletions(-) diff --git a/common/Events.v b/common/Events.v index ac6c1a04..2e57922f 100644 --- a/common/Events.v +++ b/common/Events.v @@ -901,16 +901,122 @@ Qed. (** ** Semantics of [memcpy] operations. *) -(** To be done once [storebytes] is added to the [Memtype] interface. *) - -Definition extcall_memcpy_sem (sz al: Z) (F V: Type) (ge: Genv.t F V): list val -> mem -> trace -> val -> mem -> Prop := - fun vargs m1 t vres m2 => False. +Inductive extcall_memcpy_sem (sz al: Z) (F V: Type) (ge: Genv.t F V): list val -> mem -> trace -> val -> mem -> Prop := + | extcall_memcpy_sem_intro: forall bdst odst bsrc osrc m bytes m', + al = 1 \/ al = 2 \/ al = 4 -> sz > 0 -> + (al | sz) -> (al | Int.unsigned osrc) -> (al | Int.unsigned odst) -> + bsrc <> bdst \/ Int.unsigned osrc = Int.unsigned odst + \/ Int.unsigned osrc + sz <= Int.unsigned odst + \/ Int.unsigned odst + sz <= Int.unsigned osrc -> + Mem.loadbytes m bsrc (Int.unsigned osrc) sz = Some bytes -> + Mem.storebytes m bdst (Int.unsigned odst) bytes = Some m' -> + extcall_memcpy_sem sz al ge (Vptr bdst odst :: Vptr bsrc osrc :: nil) m E0 Vundef m'. Lemma extcall_memcpy_ok: forall sz al, extcall_properties (extcall_memcpy_sem sz al) (mksignature (Tint :: Tint :: nil) None). Proof. - intros. unfold extcall_memcpy_sem; constructor; contradiction. + intros. constructor. +(* return type *) + intros. inv H. constructor. +(* arity *) + intros. inv H. auto. +(* change of globalenv *) + intros. inv H1. econstructor; eauto. +(* valid blocks *) + intros. inv H. eauto with mem. +(* bounds *) + intros. inv H. eapply Mem.bounds_storebytes; eauto. +(* extensions *) + intros. inv H. + inv H1. inv H13. inv H14. inv H10. inv H11. + exploit Mem.loadbytes_length; eauto. intros LEN. +(* + destruct (zle sz 0). + (* empty copy *) + rewrite nat_of_Z_neg in LEN; auto. + assert (bytes = nil). destruct bytes; simpl in LEN; congruence. + subst. rewrite Mem.storebytes_empty in H8. inv H8. + exists Vundef; exists m1'. + split. econstructor; eauto. rewrite Mem.loadbytes_empty; eauto. + apply Mem.storebytes_empty. + split. constructor. split. auto. red; auto. + (* nonempty copy *) +*) + exploit Mem.loadbytes_extends; eauto. intros [bytes2 [A B]]. + exploit Mem.storebytes_within_extends; eauto. intros [m2' [C D]]. + exists Vundef; exists m2'. + split. econstructor; eauto. + split. constructor. + split. auto. + red; split; intros. + eauto with mem. + exploit Mem.loadbytes_length. eexact H8. intros. + rewrite <- H1. eapply Mem.load_storebytes_other; eauto. + destruct (eq_block b bdst); auto. subst b; right. + exploit Mem.range_perm_in_bounds. eapply Mem.storebytes_range_perm. eexact H9. + rewrite H10. rewrite nat_of_Z_eq. omega. omega. + intros [P Q]. + exploit list_forall2_length; eauto. intros R. rewrite R in Q. + apply (Intv.range_disjoint' (ofs, ofs + size_chunk chunk) + (Int.unsigned odst, Int.unsigned odst + Z_of_nat (length bytes2))); simpl. + red; intros. generalize (H x H11). unfold loc_out_of_bounds, Intv.In; simpl. omega. + generalize (size_chunk_pos chunk); omega. + rewrite <- R; rewrite H10. rewrite nat_of_Z_eq. omega. omega. +(* injections *) + intros. inv H0. inv H2. inv H14. inv H15. inv H11. inv H12. + exploit Mem.loadbytes_length; eauto. intros LEN. +(* + destruct (zle sz 0). + (* empty copy *) + rewrite nat_of_Z_neg in LEN; auto. + assert (bytes = nil). destruct bytes; simpl in LEN; congruence. + subst. rewrite Mem.storebytes_empty in H9. inv H9. + exists f; exists Vundef; exists m1'. + split. econstructor; eauto. +*) + assert (RPSRC: Mem.range_perm m1 bsrc (Int.unsigned osrc) (Int.unsigned osrc + sz) Nonempty). + eapply Mem.range_perm_implies. eapply Mem.loadbytes_range_perm; eauto. auto with mem. + assert (RPDST: Mem.range_perm m1 bdst (Int.unsigned odst) (Int.unsigned odst + sz) Nonempty). + replace sz with (Z_of_nat (length bytes)). + eapply Mem.range_perm_implies. eapply Mem.storebytes_range_perm; eauto. auto with mem. + rewrite LEN. apply nat_of_Z_eq. omega. + assert (PSRC: Mem.perm m1 bsrc (Int.unsigned osrc) Nonempty). + apply RPSRC. omega. + assert (PDST: Mem.perm m1 bdst (Int.unsigned odst) Nonempty). + apply RPDST. omega. + exploit Mem.address_inject. eauto. eexact PSRC. eauto. intros EQ1. + exploit Mem.address_inject. eauto. eexact PDST. eauto. intros EQ2. + exploit Mem.loadbytes_inject; eauto. intros [bytes2 [A B]]. + exploit Mem.storebytes_mapped_inject; eauto. intros [m2' [C D]]. + exists f; exists Vundef; exists m2'. + split. econstructor; try rewrite EQ1; try rewrite EQ2; eauto. + eapply Mem.aligned_area_inject with (m := m1); eauto. + eapply Mem.aligned_area_inject with (m := m1); eauto. + eapply Mem.disjoint_or_equal_inject with (m := m1); eauto. + split. constructor. + split. auto. + split. red; split; intros. eauto with mem. + rewrite <- H2. eapply Mem.load_storebytes_other; eauto. + destruct (eq_block b bdst); auto. subst b. + assert (loc_unmapped f bdst ofs). apply H0. generalize (size_chunk_pos chunk); omega. + red in H12. congruence. + split. red; split; intros. eauto with mem. + rewrite <- H2. eapply Mem.load_storebytes_other; eauto. + destruct (eq_block b b0); auto. subst b0; right. + rewrite <- (list_forall2_length B). rewrite LEN. rewrite nat_of_Z_eq; try omega. + apply (Intv.range_disjoint' (ofs, ofs + size_chunk chunk) + (Int.unsigned odst + delta0, Int.unsigned odst + delta0 + sz)); simpl. + red; intros. generalize (H0 x H12). unfold loc_out_of_reach, Intv.In; simpl. + intros. exploit H14; eauto. + exploit Mem.range_perm_in_bounds. eexact RPDST. omega. + omega. + generalize (size_chunk_pos chunk); omega. + omega. + split. apply inject_incr_refl. + red; intros; congruence. +(* determinism *) + intros. inv H; inv H0. split. auto. split. auto. congruence. Qed. (** ** Semantics of system calls. *) diff --git a/common/Memdata.v b/common/Memdata.v index c0e1f500..16adb237 100644 --- a/common/Memdata.v +++ b/common/Memdata.v @@ -69,10 +69,10 @@ Qed. multiple of the natural alignment for the chunk being addressed. This natural alignment is defined by the following [align_chunk] function. Some target architectures - (e.g. the PowerPC) have no alignment constraints, which we could + (e.g. PowerPC and x86) have no alignment constraints, which we could reflect by taking [align_chunk chunk = 1]. However, other architectures have stronger alignment requirements. The following definition is - appropriate for PowerPC and ARM. *) + appropriate for PowerPC, ARM and x86. *) Definition align_chunk (chunk: memory_chunk) : Z := match chunk with @@ -1053,9 +1053,12 @@ Proof. constructor. Qed. -Lemma memval_inject_id: - forall mv, memval_inject inject_id mv mv. +Definition memval_lessdef: memval -> memval -> Prop := memval_inject inject_id. + +Lemma memval_lessdef_refl: + forall mv, memval_lessdef mv mv. Proof. - destruct mv; econstructor. unfold inject_id; reflexivity. rewrite Int.add_zero; auto. + red. destruct mv; econstructor. + unfold inject_id; reflexivity. rewrite Int.add_zero; auto. Qed. diff --git a/common/Memory.v b/common/Memory.v index d7d1d7b5..b456191a 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -562,25 +562,29 @@ Proof. intros. apply getN_exten. intros. apply setN_outside. omega. Qed. +Lemma setN_noread_undef: + forall m b ofs bytes (RP: range_perm m b ofs (ofs + Z_of_nat (length bytes)) Writable), + forall b' ofs', + perm m b' ofs' Readable \/ + update b (setN bytes ofs (mem_contents m b)) (mem_contents m) b' ofs' = Undef. +Proof. + intros. unfold update. destruct (zeq b' b). subst b'. + assert (ofs <= ofs' < ofs + Z_of_nat (length bytes) + \/ ofs' < ofs + \/ ofs' >= ofs + Z_of_nat (length bytes)) by omega. + destruct H. left. apply perm_implies with Writable; auto with mem. + rewrite setN_outside; auto. apply noread_undef; auto. + apply noread_undef; auto. +Qed. + Lemma store_noread_undef: forall m ch b ofs (VA: valid_access m ch b ofs Writable) v, - forall b' ofs', - perm m b' ofs' Readable \/ - update b (setN (encode_val ch v) ofs (mem_contents m b)) (mem_contents m) b' ofs' = Undef. + forall b' ofs', + perm m b' ofs' Readable \/ + update b (setN (encode_val ch v) ofs (mem_contents m b)) (mem_contents m) b' ofs' = Undef. Proof. - intros. - destruct VA as [? _]. - unfold update. - destruct (zeq b' b). - subst b'. - assert (ofs <= ofs' < ofs + size_chunk ch \/ (ofs' < ofs \/ ofs' >= ofs + size_chunk ch)) by omega. - destruct H0. - exploit (H ofs'); auto; intro. - eauto with mem. - rewrite setN_outside. - destruct (noread_undef m b ofs'); auto. - rewrite encode_val_length. rewrite <- size_chunk_conv; auto. - destruct (noread_undef m b' ofs'); auto. + intros. destruct VA. apply setN_noread_undef. + rewrite encode_val_length. rewrite <- size_chunk_conv. auto. Qed. (** [store chunk m b ofs v] perform a write in memory state [m]. @@ -612,6 +616,26 @@ Definition storev (chunk: memory_chunk) (m: mem) (addr v: val) : option mem := | _ => None end. +(** [storebytes m b ofs bytes] stores the given list of bytes [bytes] + starting at location [(b, ofs)]. Returns updated memory state + or [None] if the accessed locations are not writable. *) + +Definition storebytes (m: mem) (b: block) (ofs: Z) (bytes: list memval) : option mem := + match range_perm_dec m b ofs (ofs + Z_of_nat (length bytes)) Writable with + | left RP => + Some (mkmem + (update b (setN bytes ofs (m.(mem_contents) b)) m.(mem_contents)) + m.(mem_access) + m.(bounds) + m.(nextblock) + m.(nextblock_pos) + m.(nextblock_noaccess) + m.(bounds_noaccess) + (setN_noread_undef m b ofs bytes RP)) + | right _ => + None + end. + (** [drop_perm m b lo hi p] sets the permissions of the byte range [(b, lo) ... (b, hi - 1)] to [p]. These bytes must have permissions at least [p] in the initial memory state [m]. @@ -754,6 +778,25 @@ Proof. rewrite pred_dec_false; auto. Qed. +(** ** Properties related to [loadbytes] *) + +Theorem range_perm_loadbytes: + forall m b ofs len, + range_perm m b ofs (ofs + len) Readable -> + exists bytes, loadbytes m b ofs len = Some bytes. +Proof. + intros. econstructor. unfold loadbytes. rewrite pred_dec_true; eauto. +Qed. + +Theorem loadbytes_range_perm: + forall m b ofs len bytes, + loadbytes m b ofs len = Some bytes -> + range_perm m b ofs (ofs + len) Readable. +Proof. + intros until bytes. unfold loadbytes. + destruct (range_perm_dec m b ofs (ofs + len) Readable). auto. congruence. +Qed. + Theorem loadbytes_load: forall chunk m b ofs bytes, loadbytes m b ofs (size_chunk chunk) = Some bytes -> @@ -796,6 +839,14 @@ Proof. inv H. apply getN_length. Qed. +Theorem loadbytes_empty: + forall m b ofs n, + n <= 0 -> loadbytes m b ofs n = Some nil. +Proof. + intros. unfold loadbytes. rewrite pred_dec_true. rewrite nat_of_Z_neg; auto. + red; intros. omegaContradiction. +Qed. + Lemma getN_concat: forall c n1 n2 p, getN (n1 + n2)%nat p c = getN n1 p c ++ getN n2 (p + Z_of_nat n1) c. @@ -1350,6 +1401,269 @@ Theorem store_float32_truncate: store Mfloat32 m b ofs (Vfloat n). Proof. intros. apply store_similar_chunks. simpl. decEq. apply encode_float32_cast. Qed. +(** ** Properties related to [storebytes]. *) + +Theorem range_perm_storebytes: + forall m1 b ofs bytes, + range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Writable -> + { m2 : mem | storebytes m1 b ofs bytes = Some m2 }. +Proof. + intros. + exists (mkmem + (update b (setN bytes ofs (m1.(mem_contents) b)) m1.(mem_contents)) + m1.(mem_access) + m1.(bounds) + m1.(nextblock) + m1.(nextblock_pos) + m1.(nextblock_noaccess) + m1.(bounds_noaccess) + (setN_noread_undef m1 b ofs bytes H)). + unfold storebytes. + destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Writable). + decEq. decEq. apply proof_irr. + contradiction. +Qed. + +Theorem storebytes_store: + forall m1 b ofs chunk v m2, + storebytes m1 b ofs (encode_val chunk v) = Some m2 -> + (align_chunk chunk | ofs) -> + store chunk m1 b ofs v = Some m2. +Proof. + unfold storebytes, store. intros. + destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length (encode_val chunk v))) Writable); inv H. + destruct (valid_access_dec m1 chunk b ofs Writable). + decEq. decEq. apply proof_irr. + elim n. constructor; auto. + rewrite encode_val_length in r. rewrite size_chunk_conv. auto. +Qed. + +Theorem store_storebytes: + forall m1 b ofs chunk v m2, + store chunk m1 b ofs v = Some m2 -> + storebytes m1 b ofs (encode_val chunk v) = Some m2. +Proof. + unfold storebytes, store. intros. + destruct (valid_access_dec m1 chunk b ofs Writable); inv H. + destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length (encode_val chunk v))) Writable). + decEq. decEq. apply proof_irr. + destruct v0. elim n. + rewrite encode_val_length. rewrite <- size_chunk_conv. auto. +Qed. + +Theorem storebytes_empty: + forall m b ofs, storebytes m b ofs nil = Some m. +Proof. + intros. unfold storebytes. simpl. + destruct (range_perm_dec m b ofs (ofs + 0) Writable). + decEq. destruct m; simpl; apply mkmem_ext; auto. + apply extensionality. unfold update; intros. destruct (zeq x b); congruence. + elim n. red; intros; omegaContradiction. +Qed. + +Section STOREBYTES. +Variable m1: mem. +Variable b: block. +Variable ofs: Z. +Variable bytes: list memval. +Variable m2: mem. +Hypothesis STORE: storebytes m1 b ofs bytes = Some m2. + +Lemma storebytes_access: mem_access m2 = mem_access m1. +Proof. + unfold storebytes in STORE. + destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Writable); + inv STORE. + auto. +Qed. + +Lemma storebytes_mem_contents: + mem_contents m2 = update b (setN bytes ofs (m1.(mem_contents) b)) m1.(mem_contents). +Proof. + unfold storebytes in STORE. + destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Writable); + inv STORE. + auto. +Qed. + +Theorem perm_storebytes_1: + forall b' ofs' p, perm m1 b' ofs' p -> perm m2 b' ofs' p. +Proof. + intros. unfold perm in *. rewrite storebytes_access; auto. +Qed. + +Theorem perm_storebytes_2: + forall b' ofs' p, perm m2 b' ofs' p -> perm m1 b' ofs' p. +Proof. + intros. unfold perm in *. rewrite storebytes_access in H; auto. +Qed. + +Hint Local Resolve perm_storebytes_1 perm_storebytes_2: mem. + +Theorem storebytes_valid_access_1: + forall chunk' b' ofs' p, + valid_access m1 chunk' b' ofs' p -> valid_access m2 chunk' b' ofs' p. +Proof. + intros. inv H. constructor; try red; auto with mem. +Qed. + +Theorem storebytes_valid_access_2: + forall chunk' b' ofs' p, + valid_access m2 chunk' b' ofs' p -> valid_access m1 chunk' b' ofs' p. +Proof. + intros. inv H. constructor; try red; auto with mem. +Qed. + +Hint Local Resolve storebytes_valid_access_1 storebytes_valid_access_2: mem. + +Theorem nextblock_storebytes: + nextblock m2 = nextblock m1. +Proof. + intros. + unfold storebytes in STORE. + destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Writable); + inv STORE. + auto. +Qed. + +Theorem storebytes_valid_block_1: + forall b', valid_block m1 b' -> valid_block m2 b'. +Proof. + unfold valid_block; intros. rewrite nextblock_storebytes; auto. +Qed. + +Theorem storebytes_valid_block_2: + forall b', valid_block m2 b' -> valid_block m1 b'. +Proof. + unfold valid_block; intros. rewrite nextblock_storebytes in H; auto. +Qed. + +Hint Local Resolve storebytes_valid_block_1 storebytes_valid_block_2: mem. + +Theorem storebytes_range_perm: + range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Writable. +Proof. + intros. + unfold storebytes in STORE. + destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Writable); + inv STORE. + auto. +Qed. + +Theorem bounds_storebytes: + forall b', bounds m2 b' = bounds m1 b'. +Proof. + intros. + unfold storebytes in STORE. + destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Writable); + inv STORE. + auto. +Qed. + +Theorem loadbytes_storebytes_same: + loadbytes m2 b ofs (Z_of_nat (length bytes)) = Some bytes. +Proof. + intros. unfold storebytes in STORE. unfold loadbytes. + destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Writable); + try discriminate. + rewrite pred_dec_true. + decEq. inv STORE; simpl. rewrite update_s. rewrite nat_of_Z_of_nat. + apply getN_setN_same. + red; eauto with mem. +Qed. + +Theorem loadbytes_storebytes_other: + forall b' ofs' len, + len >= 0 -> + b' <> b + \/ ofs' + len <= ofs + \/ ofs + Z_of_nat (length bytes) <= ofs' -> + loadbytes m2 b' ofs' len = loadbytes m1 b' ofs' len. +Proof. + intros. unfold loadbytes. + destruct (range_perm_dec m1 b' ofs' (ofs' + len) Readable). + rewrite pred_dec_true. + rewrite storebytes_mem_contents. decEq. + unfold update. destruct (zeq b' b). subst b'. + apply getN_setN_outside. rewrite nat_of_Z_eq; auto. intuition congruence. + auto. + red; auto with mem. + apply pred_dec_false. + red; intros; elim n. red; auto with mem. +Qed. + +Theorem load_storebytes_other: + forall chunk b' ofs', + b' <> b + \/ ofs' + size_chunk chunk <= ofs + \/ ofs + Z_of_nat (length bytes) <= ofs' -> + load chunk m2 b' ofs' = load chunk m1 b' ofs'. +Proof. + intros. unfold load. + destruct (valid_access_dec m1 chunk b' ofs' Readable). + rewrite pred_dec_true. + rewrite storebytes_mem_contents. decEq. + unfold update. destruct (zeq b' b). subst b'. + rewrite getN_setN_outside. auto. rewrite <- size_chunk_conv. intuition congruence. + auto. + destruct v; split; auto. red; auto with mem. + apply pred_dec_false. + red; intros; elim n. destruct H0. split; auto. red; auto with mem. +Qed. + +End STOREBYTES. + +Lemma setN_concat: + forall bytes1 bytes2 ofs c, + setN (bytes1 ++ bytes2) ofs c = setN bytes2 (ofs + Z_of_nat (length bytes1)) (setN bytes1 ofs c). +Proof. + induction bytes1; intros. + simpl. decEq. omega. + simpl length. rewrite inj_S. simpl. rewrite IHbytes1. decEq. omega. +Qed. + +Theorem storebytes_concat: + forall m b ofs bytes1 m1 bytes2 m2, + storebytes m b ofs bytes1 = Some m1 -> + storebytes m1 b (ofs + Z_of_nat(length bytes1)) bytes2 = Some m2 -> + storebytes m b ofs (bytes1 ++ bytes2) = Some m2. +Proof. + intros. generalize H; intro ST1. generalize H0; intro ST2. + unfold storebytes; unfold storebytes in ST1; unfold storebytes in ST2. + destruct (range_perm_dec m b ofs (ofs + Z_of_nat(length bytes1)) Writable); try congruence. + destruct (range_perm_dec m1 b (ofs + Z_of_nat(length bytes1)) (ofs + Z_of_nat(length bytes1) + Z_of_nat(length bytes2)) Writable); try congruence. + destruct (range_perm_dec m b ofs (ofs + Z_of_nat (length (bytes1 ++ bytes2))) Writable). + inv ST1; inv ST2; simpl. decEq. apply mkmem_ext; auto. + apply extensionality; intros. unfold update. destruct (zeq x b); auto. + subst x. rewrite zeq_true. apply setN_concat. + elim n. + rewrite app_length. rewrite inj_plus. red; intros. + destruct (zlt ofs0 (ofs + Z_of_nat(length bytes1))). + apply r. omega. + eapply perm_storebytes_2; eauto. apply r0. omega. +Qed. + +Theorem storebytes_split: + forall m b ofs bytes1 bytes2 m2, + storebytes m b ofs (bytes1 ++ bytes2) = Some m2 -> + exists m1, + storebytes m b ofs bytes1 = Some m1 + /\ storebytes m1 b (ofs + Z_of_nat(length bytes1)) bytes2 = Some m2. +Proof. + intros. + destruct (range_perm_storebytes m b ofs bytes1) as [m1 ST1]. + red; intros. exploit storebytes_range_perm; eauto. rewrite app_length. + rewrite inj_plus. omega. + destruct (range_perm_storebytes m1 b (ofs + Z_of_nat (length bytes1)) bytes2) as [m2' ST2]. + red; intros. eapply perm_storebytes_1; eauto. exploit storebytes_range_perm. + eexact H. instantiate (1 := ofs0). rewrite app_length. rewrite inj_plus. omega. + auto. + assert (Some m2 = Some m2'). + rewrite <- H. eapply storebytes_concat; eauto. + inv H0. + exists m1; split; auto. +Qed. + (** ** Properties related to [alloc]. *) Section ALLOC. @@ -1997,6 +2311,18 @@ Proof. apply A. simpl; omega. Qed. +Lemma range_perm_inj: + forall f m1 m2 b1 lo hi p b2 delta, + mem_inj f m1 m2 -> + range_perm m1 b1 lo hi p -> + f b1 = Some(b2, delta) -> + range_perm m2 b2 (lo + delta) (hi + delta) p. +Proof. + intros; red; intros. + replace ofs with ((ofs - delta) + delta) by omega. + eapply perm_inj; eauto. apply H0. omega. +Qed. + (** Preservation of loads. *) Lemma getN_inj: @@ -2036,6 +2362,25 @@ Proof. rewrite <- size_chunk_conv. exploit load_valid_access; eauto. intros [A B]. auto. Qed. +Lemma loadbytes_inj: + forall f m1 m2 len b1 ofs b2 delta bytes1, + mem_inj f m1 m2 -> + loadbytes m1 b1 ofs len = Some bytes1 -> + f b1 = Some (b2, delta) -> + exists bytes2, loadbytes m2 b2 (ofs + delta) len = Some bytes2 + /\ list_forall2 (memval_inject f) bytes1 bytes2. +Proof. + intros. unfold loadbytes in *. + destruct (range_perm_dec m1 b1 ofs (ofs + len) Readable); inv H0. + exists (getN (nat_of_Z len) (ofs + delta) (m2.(mem_contents) b2)). + split. apply pred_dec_true. + replace (ofs + delta + len) with ((ofs + len) + delta) by omega. + eapply range_perm_inj; eauto with mem. + apply getN_inj; auto. + destruct (zle 0 len). rewrite nat_of_Z_eq; auto. omega. + rewrite nat_of_Z_neg. simpl. red; intros; omegaContradiction. omega. +Qed. + (** Preservation of stores. *) Lemma setN_inj: @@ -2172,6 +2517,99 @@ Proof. eauto with mem. Qed. +Lemma storebytes_mapped_inj: + forall f m1 b1 ofs bytes1 n1 m2 b2 delta bytes2, + mem_inj f m1 m2 -> + storebytes m1 b1 ofs bytes1 = Some n1 -> + meminj_no_overlap f m1 -> + f b1 = Some (b2, delta) -> + list_forall2 (memval_inject f) bytes1 bytes2 -> + exists n2, + storebytes m2 b2 (ofs + delta) bytes2 = Some n2 + /\ mem_inj f n1 n2. +Proof. + intros. inversion H. + assert (range_perm m2 b2 (ofs + delta) (ofs + delta + Z_of_nat (length bytes2)) Writable). + replace (ofs + delta + Z_of_nat (length bytes2)) + with ((ofs + Z_of_nat (length bytes1)) + delta). + eapply range_perm_inj; eauto with mem. + eapply storebytes_range_perm; eauto. + rewrite (list_forall2_length H3). omega. + destruct (range_perm_storebytes _ _ _ _ H4) as [n2 STORE]. + exists n2; split. eauto. + constructor. +(* access *) + intros. + eapply storebytes_valid_access_1; [apply STORE |]. + eapply mi_access0; eauto. + eapply storebytes_valid_access_2; [apply H0 |]. auto. +(* mem_contents *) + intros. + assert (perm m1 b0 ofs0 Nonempty). eapply perm_storebytes_2; eauto. + rewrite (storebytes_mem_contents _ _ _ _ _ H0). + rewrite (storebytes_mem_contents _ _ _ _ _ STORE). + unfold update. + destruct (zeq b0 b1). subst b0. + (* block = b1, block = b2 *) + assert (b3 = b2) by congruence. subst b3. + assert (delta0 = delta) by congruence. subst delta0. + rewrite zeq_true. + apply setN_inj with (access := fun ofs => perm m1 b1 ofs Nonempty); auto. + destruct (zeq b3 b2). subst b3. + (* block <> b1, block = b2 *) + rewrite setN_other. auto. + intros. + assert (b2 <> b2 \/ ofs0 + delta0 <> (r - delta) + delta). + eapply meminj_no_overlap_perm; eauto. + exploit storebytes_range_perm. eexact H0. + instantiate (1 := r - delta). + rewrite (list_forall2_length H3). omega. + eauto with mem. + destruct H9. congruence. omega. + (* block <> b1, block <> b2 *) + eauto. +Qed. + +Lemma storebytes_unmapped_inj: + forall f m1 b1 ofs bytes1 n1 m2, + mem_inj f m1 m2 -> + storebytes m1 b1 ofs bytes1 = Some n1 -> + f b1 = None -> + mem_inj f n1 m2. +Proof. + intros. inversion H. + constructor. +(* access *) + intros. eapply mi_access0; eauto. eapply storebytes_valid_access_2; eauto. +(* mem_contents *) + intros. + rewrite (storebytes_mem_contents _ _ _ _ _ H0). + rewrite update_o. eapply mi_memval0; eauto. eapply perm_storebytes_2; eauto. + congruence. +Qed. + +Lemma storebytes_outside_inj: + forall f m1 m2 b ofs bytes2 m2', + mem_inj f m1 m2 -> + (forall b' delta ofs', + f b' = Some(b, delta) -> + perm m1 b' ofs' Nonempty -> + ofs' + delta < ofs \/ ofs' + delta >= ofs + Z_of_nat (length bytes2)) -> + storebytes m2 b ofs bytes2 = Some m2' -> + mem_inj f m1 m2'. +Proof. + intros. inversion H. constructor. +(* access *) + intros. eapply storebytes_valid_access_1; eauto with mem. +(* mem_contents *) + intros. + rewrite (storebytes_mem_contents _ _ _ _ _ H1). + unfold update. destruct (zeq b2 b). subst b2. + rewrite setN_outside. auto. + eapply H0; eauto. + eauto with mem. +Qed. + (** Preservation of allocations *) Lemma alloc_right_inj: @@ -2414,8 +2852,7 @@ Proof. intros. constructor. auto. constructor. intros. unfold inject_id in H; inv H. replace (ofs + 0) with ofs by omega. auto. intros. unfold inject_id in H; inv H. replace (ofs + 0) with ofs by omega. - apply memval_inject_id. -(* intros. omega. *) + apply memval_lessdef_refl. Qed. Theorem load_extends: @@ -2442,6 +2879,17 @@ Proof. congruence. Qed. +Theorem loadbytes_extends: + forall m1 m2 b ofs len bytes1, + extends m1 m2 -> + loadbytes m1 b ofs len = Some bytes1 -> + exists bytes2, loadbytes m2 b ofs len = Some bytes2 + /\ list_forall2 memval_lessdef bytes1 bytes2. +Proof. + intros. inv H. + replace ofs with (ofs + 0) by omega. eapply loadbytes_inj; eauto. +Qed. + Theorem store_within_extends: forall chunk m1 m2 b ofs v1 m1' v2, extends m1 m2 -> @@ -2504,6 +2952,52 @@ Proof. congruence. Qed. +Theorem storebytes_within_extends: + forall m1 m2 b ofs bytes1 m1' bytes2, + extends m1 m2 -> + storebytes m1 b ofs bytes1 = Some m1' -> + list_forall2 memval_lessdef bytes1 bytes2 -> + exists m2', + storebytes m2 b ofs bytes2 = Some m2' + /\ extends m1' m2'. +Proof. + intros. inversion H. + exploit storebytes_mapped_inj; eauto. + unfold inject_id; red; intros. inv H3; inv H4. auto. + unfold inject_id; reflexivity. + intros [m2' [A B]]. + exists m2'; split. + replace (ofs + 0) with ofs in A by omega. auto. + split; auto. + rewrite (nextblock_storebytes _ _ _ _ _ H0). + rewrite (nextblock_storebytes _ _ _ _ _ A). + auto. +(* + intros. + rewrite (bounds_store _ _ _ _ _ _ H0). + rewrite (bounds_store _ _ _ _ _ _ A). + auto. +*) +Qed. + +Theorem storebytes_outside_extends: + forall m1 m2 b ofs bytes2 m2', + extends m1 m2 -> + storebytes m2 b ofs bytes2 = Some m2' -> + ofs + Z_of_nat (length bytes2) <= low_bound m1 b \/ high_bound m1 b <= ofs -> + extends m1 m2'. +Proof. + intros. inversion H. constructor. + rewrite (nextblock_storebytes _ _ _ _ _ H0). auto. + eapply storebytes_outside_inj; eauto. + unfold inject_id; intros. inv H2. + exploit perm_in_bounds; eauto. omega. +(* + intros. + rewrite (bounds_store _ _ _ _ _ _ H0). auto. +*) +Qed. + Theorem alloc_extends: forall m1 m2 lo1 hi1 b m1' lo2 hi2, extends m1 m2 -> @@ -2702,6 +3196,15 @@ Proof. intros. inv H0. eapply perm_inj; eauto. Qed. +Theorem range_perm_inject: + forall f m1 m2 b1 b2 delta lo hi p, + f b1 = Some(b2, delta) -> + inject f m1 m2 -> + range_perm m1 b1 lo hi p -> range_perm m2 b2 (lo + delta) (hi + delta) p. +Proof. + intros. inv H0. eapply range_perm_inj; eauto. +Qed. + Theorem valid_access_inject: forall f m1 m2 chunk b1 ofs b2 delta p, f b1 = Some(b2, delta) -> @@ -2824,6 +3327,53 @@ Proof. apply (H1 (Int.unsigned ofs2)). omega. Qed. +Theorem disjoint_or_equal_inject: + forall f m m' b1 b1' delta1 b2 b2' delta2 ofs1 ofs2 sz, + inject f m m' -> + f b1 = Some(b1', delta1) -> + f b2 = Some(b2', delta2) -> + range_perm m b1 ofs1 (ofs1 + sz) Nonempty -> + range_perm m b2 ofs2 (ofs2 + sz) Nonempty -> + sz > 0 -> + b1 <> b2 \/ ofs1 = ofs2 \/ ofs1 + sz <= ofs2 \/ ofs2 + sz <= ofs1 -> + b1' <> b2' \/ ofs1 + delta1 = ofs2 + delta2 + \/ ofs1 + delta1 + sz <= ofs2 + delta2 + \/ ofs2 + delta2 + sz <= ofs1 + delta1. +Proof. + intros. + exploit range_perm_in_bounds. eexact H2. omega. intros [LO1 HI1]. + exploit range_perm_in_bounds. eexact H3. omega. intros [LO2 HI2]. + destruct (eq_block b1 b2). + assert (b1' = b2') by congruence. assert (delta1 = delta2) by congruence. subst. + destruct H5. congruence. right. destruct H5. left; congruence. right. omega. + exploit mi_no_overlap; eauto. intros [P | P]. auto. right. omega. +Qed. + +Theorem aligned_area_inject: + forall f m m' b ofs al sz b' delta, + inject f m m' -> + al = 1 \/ al = 2 \/ al = 4 -> sz > 0 -> + (al | sz) -> + range_perm m b ofs (ofs + sz) Nonempty -> + (al | ofs) -> + f b = Some(b', delta) -> + (al | ofs + delta). +Proof. + intros. + assert (P: al > 0) by omega. + assert (Q: Zabs al <= Zabs sz). apply Zdivide_bounds; auto. omega. + rewrite Zabs_eq in Q; try omega. rewrite Zabs_eq in Q; try omega. + assert (R: exists chunk, al = align_chunk chunk /\ al = size_chunk chunk). + destruct H0. subst; exists Mint8unsigned; auto. + destruct H0. subst; exists Mint16unsigned; auto. + subst; exists Mint32; auto. + destruct R as [chunk [A B]]. + assert (valid_access m chunk b ofs Nonempty). + split. red; intros; apply H3. omega. congruence. + exploit valid_access_inject; eauto. intros [C D]. + congruence. +Qed. + (** Preservation of loads *) Theorem load_inject: @@ -2851,6 +3401,17 @@ Proof. auto. symmetry. eapply address_inject'; eauto with mem. Qed. +Theorem loadbytes_inject: + forall f m1 m2 b1 ofs len b2 delta bytes1, + inject f m1 m2 -> + loadbytes m1 b1 ofs len = Some bytes1 -> + f b1 = Some (b2, delta) -> + exists bytes2, loadbytes m2 b2 (ofs + delta) len = Some bytes2 + /\ list_forall2 (memval_inject f) bytes1 bytes2. +Proof. + intros. inv H. eapply loadbytes_inj; eauto. +Qed. + (** Preservation of stores *) Theorem store_mapped_inject: @@ -2951,6 +3512,87 @@ Proof. symmetry. eapply address_inject'; eauto with mem. Qed. +Theorem storebytes_mapped_inject: + forall f m1 b1 ofs bytes1 n1 m2 b2 delta bytes2, + inject f m1 m2 -> + storebytes m1 b1 ofs bytes1 = Some n1 -> + f b1 = Some (b2, delta) -> + list_forall2 (memval_inject f) bytes1 bytes2 -> + exists n2, + storebytes m2 b2 (ofs + delta) bytes2 = Some n2 + /\ inject f n1 n2. +Proof. + intros. inversion H. + exploit storebytes_mapped_inj; eauto. intros [n2 [STORE MI]]. + exists n2; split. eauto. constructor. +(* inj *) + auto. +(* freeblocks *) + intros. apply mi_freeblocks0. red; intros; elim H3; eapply storebytes_valid_block_1; eauto. +(* mappedblocks *) + intros. eapply storebytes_valid_block_1; eauto. +(* no overlap *) + red; intros. + repeat rewrite (bounds_storebytes _ _ _ _ _ H0). + eauto. +(* range offset *) + eauto. +(* range blocks *) + intros. rewrite (bounds_storebytes _ _ _ _ _ STORE). eauto. +Qed. + +Theorem storebytes_unmapped_inject: + forall f m1 b1 ofs bytes1 n1 m2, + inject f m1 m2 -> + storebytes m1 b1 ofs bytes1 = Some n1 -> + f b1 = None -> + inject f n1 m2. +Proof. + intros. inversion H. + constructor. +(* inj *) + eapply storebytes_unmapped_inj; eauto. +(* freeblocks *) + intros. apply mi_freeblocks0. red; intros; elim H2; eapply storebytes_valid_block_1; eauto. +(* mappedblocks *) + eauto with mem. +(* no overlap *) + red; intros. + repeat rewrite (bounds_storebytes _ _ _ _ _ H0). + eauto. +(* range offset *) + eauto. +(* range blocks *) + auto. +Qed. + +Theorem storebytes_outside_inject: + forall f m1 m2 b ofs bytes2 m2', + inject f m1 m2 -> + (forall b' delta, + f b' = Some(b, delta) -> + high_bound m1 b' + delta <= ofs + \/ ofs + Z_of_nat (length bytes2) <= low_bound m1 b' + delta) -> + storebytes m2 b ofs bytes2 = Some m2' -> + inject f m1 m2'. +Proof. + intros. inversion H. constructor. +(* inj *) + eapply storebytes_outside_inj; eauto. + intros. exploit perm_in_bounds; eauto. intro. + exploit H0; eauto. omega. +(* freeblocks *) + auto. +(* mappedblocks *) + intros. eapply storebytes_valid_block_1; eauto. +(* no overlap *) + auto. +(* range offset *) + auto. +(* range blocks *) + intros. rewrite (bounds_storebytes _ _ _ _ _ H1). eauto. +Qed. + (* Preservation of allocations *) Theorem alloc_right_inject: @@ -3328,7 +3970,7 @@ End Mem. Notation mem := Mem.mem. -Global Opaque Mem.alloc Mem.free Mem.store Mem.load. +Global Opaque Mem.alloc Mem.free Mem.store Mem.load Mem.storebytes Mem.loadbytes. Hint Resolve Mem.valid_not_valid_diff @@ -3340,6 +3982,7 @@ Hint Resolve Mem.valid_access_perm Mem.valid_access_load Mem.load_valid_access + Mem.loadbytes_range_perm Mem.valid_access_store Mem.perm_store_1 Mem.perm_store_2 @@ -3349,6 +3992,14 @@ Hint Resolve Mem.store_valid_access_1 Mem.store_valid_access_2 Mem.store_valid_access_3 + Mem.storebytes_range_perm + Mem.perm_storebytes_1 + Mem.perm_storebytes_2 + Mem.storebytes_valid_access_1 + Mem.storebytes_valid_access_2 + Mem.nextblock_storebytes + Mem.storebytes_valid_block_1 + Mem.storebytes_valid_block_2 Mem.nextblock_alloc Mem.alloc_result Mem.valid_block_alloc diff --git a/common/Memtype.v b/common/Memtype.v index 09736434..40e03a38 100644 --- a/common/Memtype.v +++ b/common/Memtype.v @@ -126,6 +126,11 @@ Definition storev (chunk: memory_chunk) (m: mem) (addr v: val) : option mem := [None] is returned if the accessed addresses are not readable. *) Parameter loadbytes: forall (m: mem) (b: block) (ofs n: Z), option (list memval). +(** [storebytes m b ofs bytes] stores the given list of bytes [bytes] + starting at location [(b, ofs)]. Returns updated memory state + or [None] if the accessed locations are not writable. *) +Parameter storebytes: forall (m: mem) (b: block) (ofs: Z) (bytes: list memval), option mem. + (** [free_list] frees all the given (block, lo, hi) triples. *) Fixpoint free_list (m: mem) (l: list (block * Z * Z)) {struct l}: option mem := match l with @@ -305,6 +310,18 @@ Axiom load_int16_signed_unsigned: (** ** Properties of [loadbytes]. *) +(** [loadbytes] succeeds if and only if we have read permissions on the accessed + memory area. *) + +Axiom range_perm_loadbytes: + forall m b ofs len, + range_perm m b ofs (ofs + len) Readable -> + exists bytes, loadbytes m b ofs len = Some bytes. +Axiom loadbytes_range_perm: + forall m b ofs len bytes, + loadbytes m b ofs len = Some bytes -> + range_perm m b ofs (ofs + len) Readable. + (** If [loadbytes] succeeds, the corresponding [load] succeeds and returns a value that is determined by the bytes read by [loadbytes]. *) @@ -329,6 +346,10 @@ Axiom loadbytes_length: loadbytes m b ofs n = Some bytes -> length bytes = nat_of_Z n. +Axiom loadbytes_empty: + forall m b ofs n, + n <= 0 -> loadbytes m b ofs n = Some nil. + (** Composing or decomposing [loadbytes] operations at adjacent addresses. *) Axiom loadbytes_concat: forall m b ofs n1 n2 bytes1 bytes2, @@ -473,6 +494,96 @@ Axiom store_float32_truncate: store Mfloat32 m b ofs (Vfloat (Float.singleoffloat n)) = store Mfloat32 m b ofs (Vfloat n). +(** ** Properties of [storebytes]. *) + +(** [storebytes] preserves block validity, permissions, access validity, and bounds. + Moreover, a [storebytes] succeeds if and only if we have write permissions + on the addressed memory area. *) + +Axiom range_perm_storebytes: + forall m1 b ofs bytes, + range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Writable -> + { m2 : mem | storebytes m1 b ofs bytes = Some m2 }. +Axiom storebytes_range_perm: + forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 -> + range_perm m1 b ofs (ofs + Z_of_nat (length bytes)) Writable. +Axiom perm_storebytes_1: + forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 -> + forall b' ofs' p, perm m1 b' ofs' p -> perm m2 b' ofs' p. +Axiom perm_storebytes_2: + forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 -> + forall b' ofs' p, perm m2 b' ofs' p -> perm m1 b' ofs' p. +Axiom storebytes_valid_access_1: + forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 -> + forall chunk' b' ofs' p, + valid_access m1 chunk' b' ofs' p -> valid_access m2 chunk' b' ofs' p. +Axiom storebytes_valid_access_2: + forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 -> + forall chunk' b' ofs' p, + valid_access m2 chunk' b' ofs' p -> valid_access m1 chunk' b' ofs' p. +Axiom nextblock_storebytes: + forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 -> + nextblock m2 = nextblock m1. +Axiom storebytes_valid_block_1: + forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 -> + forall b', valid_block m1 b' -> valid_block m2 b'. +Axiom storebytes_valid_block_2: + forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 -> + forall b', valid_block m2 b' -> valid_block m1 b'. +Axiom bounds_storebytes: + forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 -> + forall b', bounds m2 b' = bounds m1 b'. + +(** Connections between [store] and [storebytes]. *) + +Axiom storebytes_store: + forall m1 b ofs chunk v m2, + storebytes m1 b ofs (encode_val chunk v) = Some m2 -> + (align_chunk chunk | ofs) -> + store chunk m1 b ofs v = Some m2. + +Axiom store_storebytes: + forall m1 b ofs chunk v m2, + store chunk m1 b ofs v = Some m2 -> + storebytes m1 b ofs (encode_val chunk v) = Some m2. + +(** Load-store properties. *) + +Axiom loadbytes_storebytes_same: + forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 -> + loadbytes m2 b ofs (Z_of_nat (length bytes)) = Some bytes. +Axiom loadbytes_storebytes_other: + forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 -> + forall b' ofs' len, + len >= 0 -> + b' <> b + \/ ofs' + len <= ofs + \/ ofs + Z_of_nat (length bytes) <= ofs' -> + loadbytes m2 b' ofs' len = loadbytes m1 b' ofs' len. +Axiom load_storebytes_other: + forall m1 b ofs bytes m2, storebytes m1 b ofs bytes = Some m2 -> + forall chunk b' ofs', + b' <> b + \/ ofs' + size_chunk chunk <= ofs + \/ ofs + Z_of_nat (length bytes) <= ofs' -> + load chunk m2 b' ofs' = load chunk m1 b' ofs'. + +(** Composing or decomposing [storebytes] operations at adjacent addresses. *) + +Axiom storebytes_concat: + forall m b ofs bytes1 m1 bytes2 m2, + storebytes m b ofs bytes1 = Some m1 -> + storebytes m1 b (ofs + Z_of_nat(length bytes1)) bytes2 = Some m2 -> + storebytes m b ofs (bytes1 ++ bytes2) = Some m2. +Axiom storebytes_split: + forall m b ofs bytes1 bytes2 m2, + storebytes m b ofs (bytes1 ++ bytes2) = Some m2 -> + exists m1, + storebytes m b ofs bytes1 = Some m1 + /\ storebytes m1 b (ofs + Z_of_nat(length bytes1)) bytes2 = Some m2. +Axiom storebytes_empty: + forall m b ofs, storebytes m b ofs nil = Some m. + (** ** Properties of [alloc]. *) (** The identifier of the freshly allocated block is the next block @@ -717,6 +828,13 @@ Axiom loadv_extends: Val.lessdef addr1 addr2 -> exists v2, loadv chunk m2 addr2 = Some v2 /\ Val.lessdef v1 v2. +Axiom loadbytes_extends: + forall m1 m2 b ofs len bytes1, + extends m1 m2 -> + loadbytes m1 b ofs len = Some bytes1 -> + exists bytes2, loadbytes m2 b ofs len = Some bytes2 + /\ list_forall2 memval_lessdef bytes1 bytes2. + Axiom store_within_extends: forall chunk m1 m2 b ofs v1 m1' v2, extends m1 m2 -> @@ -743,6 +861,22 @@ Axiom storev_extends: storev chunk m2 addr2 v2 = Some m2' /\ extends m1' m2'. +Axiom storebytes_within_extends: + forall m1 m2 b ofs bytes1 m1' bytes2, + extends m1 m2 -> + storebytes m1 b ofs bytes1 = Some m1' -> + list_forall2 memval_lessdef bytes1 bytes2 -> + exists m2', + storebytes m2 b ofs bytes2 = Some m2' + /\ extends m1' m2'. + +Axiom storebytes_outside_extends: + forall m1 m2 b ofs bytes2 m2', + extends m1 m2 -> + storebytes m2 b ofs bytes2 = Some m2' -> + ofs + Z_of_nat (length bytes2) <= low_bound m1 b \/ high_bound m1 b <= ofs -> + extends m1 m2'. + Axiom alloc_extends: forall m1 m2 lo1 hi1 b m1' lo2 hi2, extends m1 m2 -> @@ -891,6 +1025,14 @@ Axiom loadv_inject: val_inject f a1 a2 -> exists v2, loadv chunk m2 a2 = Some v2 /\ val_inject f v1 v2. +Axiom loadbytes_inject: + forall f m1 m2 b1 ofs len b2 delta bytes1, + inject f m1 m2 -> + loadbytes m1 b1 ofs len = Some bytes1 -> + f b1 = Some (b2, delta) -> + exists bytes2, loadbytes m2 b2 (ofs + delta) len = Some bytes2 + /\ list_forall2 (memval_inject f) bytes1 bytes2. + Axiom store_mapped_inject: forall f chunk m1 b1 ofs v1 n1 m2 b2 delta v2, inject f m1 m2 -> @@ -927,6 +1069,33 @@ Axiom storev_mapped_inject: exists n2, storev chunk m2 a2 v2 = Some n2 /\ inject f n1 n2. +Axiom storebytes_mapped_inject: + forall f m1 b1 ofs bytes1 n1 m2 b2 delta bytes2, + inject f m1 m2 -> + storebytes m1 b1 ofs bytes1 = Some n1 -> + f b1 = Some (b2, delta) -> + list_forall2 (memval_inject f) bytes1 bytes2 -> + exists n2, + storebytes m2 b2 (ofs + delta) bytes2 = Some n2 + /\ inject f n1 n2. + +Axiom storebytes_unmapped_inject: + forall f m1 b1 ofs bytes1 n1 m2, + inject f m1 m2 -> + storebytes m1 b1 ofs bytes1 = Some n1 -> + f b1 = None -> + inject f n1 m2. + +Axiom storebytes_outside_inject: + forall f m1 m2 b ofs bytes2 m2', + inject f m1 m2 -> + (forall b' delta, + f b' = Some(b, delta) -> + high_bound m1 b' + delta <= ofs + \/ ofs + Z_of_nat (length bytes2) <= low_bound m1 b' + delta) -> + storebytes m2 b ofs bytes2 = Some m2' -> + inject f m1 m2'. + Axiom alloc_right_inject: forall f m1 m2 lo hi b2 m2', inject f m1 m2 -> diff --git a/common/Values.v b/common/Values.v index ceff3339..4dc74b2d 100644 --- a/common/Values.v +++ b/common/Values.v @@ -227,6 +227,12 @@ Definition modu (v1 v2: val): val := | _, _ => Vundef end. +Definition add_carry (v1 v2 cin: val): val := + match v1, v2, cin with + | Vint n1, Vint n2, Vint c => Vint(Int.add_carry n1 n2 c) + | _, _, _ => Vundef + end. + Definition and (v1 v2: val): val := match v1, v2 with | Vint n1, Vint n2 => Vint(Int.and n1 n2) diff --git a/lib/Coqlib.v b/lib/Coqlib.v index 4fc922b1..f4d50e82 100644 --- a/lib/Coqlib.v +++ b/lib/Coqlib.v @@ -606,6 +606,13 @@ Definition nat_of_Z (z: Z) : nat := | Zneg p => O end. +Lemma nat_of_Z_of_nat: + forall n, nat_of_Z (Z_of_nat n) = n. +Proof. + intros. unfold Z_of_nat. destruct n. auto. + simpl. rewrite nat_of_P_o_P_of_succ_nat_eq_succ. auto. +Qed. + Lemma nat_of_Z_max: forall z, Z_of_nat (nat_of_Z z) = Zmax z 0. Proof. @@ -1133,6 +1140,13 @@ Proof. induction 1; intros; simpl. auto. constructor; auto. Qed. +Lemma list_forall2_length: + forall l1 l2, + list_forall2 l1 l2 -> length l1 = length l2. +Proof. + induction 1; simpl; congruence. +Qed. + End FORALL2. Lemma list_forall2_imply: diff --git a/lib/Integers.v b/lib/Integers.v index 30f692a8..6e7a6cb6 100644 --- a/lib/Integers.v +++ b/lib/Integers.v @@ -167,6 +167,11 @@ Definition divu (x y: int) : int := Definition modu (x y: int) : int := repr (Zmod (unsigned x) (unsigned y)). +Definition add_carry (x y cin: int): int := + if zlt (unsigned x + unsigned y + unsigned cin) modulus + then zero + else one. + (** For bitwise operations, we need to convert between Coq integers [Z] and their bit-level representations. Bit-level representations are represented as characteristic functions, that is, functions [f] @@ -746,6 +751,11 @@ Proof. rewrite Zplus_0_r. apply repr_unsigned. Qed. +Theorem add_zero_l: forall x, add zero x = x. +Proof. + intros. rewrite add_commut. apply add_zero. +Qed. + Theorem add_assoc: forall x y z, add (add x y) z = add x (add y z). Proof. intros; unfold add. diff --git a/powerpc/Asm.v b/powerpc/Asm.v index d876144b..7ae5112a 100644 --- a/powerpc/Asm.v +++ b/powerpc/Asm.v @@ -127,9 +127,11 @@ Definition label := positive. Inductive instruction : Type := | Padd: ireg -> ireg -> ireg -> instruction (**r integer addition *) + | Padde: ireg -> ireg -> ireg -> instruction (**r integer addition with carry *) | Paddi: ireg -> ireg -> constant -> instruction (**r add immediate *) + | Paddic: ireg -> ireg -> constant -> instruction (**r add immediate and set carry *) | Paddis: ireg -> ireg -> constant -> instruction (**r add immediate high *) - | Paddze: ireg -> ireg -> instruction (**r add Carry bit *) + | Paddze: ireg -> ireg -> instruction (**r add carry *) | Pallocframe: Z -> int -> instruction (**r allocate new stack frame *) | Pand_: ireg -> ireg -> ireg -> instruction (**r bitwise and *) | Pandc: ireg -> ireg -> ireg -> instruction (**r bitwise and-complement *) @@ -211,6 +213,7 @@ Inductive instruction : Type := | Pstw: ireg -> constant -> ireg -> instruction (**r store 32-bit int *) | Pstwx: ireg -> ireg -> ireg -> instruction (**r same, with 2 index regs *) | Psubfc: ireg -> ireg -> ireg -> instruction (**r reversed integer subtraction *) + | Psubfe: ireg -> ireg -> ireg -> instruction (**r reversed integer subtraction with carry *) | Psubfic: ireg -> ireg -> constant -> instruction (**r integer subtraction from immediate *) | Pxor: ireg -> ireg -> ireg -> instruction (**r bitwise xor *) | Pxori: ireg -> ireg -> constant -> instruction (**r bitwise xor with immediate *) @@ -527,12 +530,19 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome match i with | Padd rd r1 r2 => OK (nextinstr (rs#rd <- (Val.add rs#r1 rs#r2))) m + | Padde rd r1 r2 => + OK (nextinstr (rs #rd <- (Val.add (Val.add rs#r1 rs#r2) rs#CARRY) + #CARRY <- (Val.add_carry rs#r1 rs#r2 rs#CARRY))) m | Paddi rd r1 cst => OK (nextinstr (rs#rd <- (Val.add (gpr_or_zero rs r1) (const_low cst)))) m + | Paddic rd r1 cst => + OK (nextinstr (rs#rd <- (Val.add (gpr_or_zero rs r1) (const_low cst)) + #CARRY <- (Val.add_carry (gpr_or_zero rs r1) (const_low cst) Vzero))) m | Paddis rd r1 cst => OK (nextinstr (rs#rd <- (Val.add (gpr_or_zero rs r1) (const_high cst)))) m | Paddze rd r1 => - OK (nextinstr (rs#rd <- (Val.add rs#r1 rs#CARRY))) m + OK (nextinstr (rs#rd <- (Val.add rs#r1 rs#CARRY) + #CARRY <- (Val.add_carry rs#r1 Vzero rs#CARRY))) m | Pallocframe sz ofs => let (m1, stk) := Mem.alloc m 0 sz in let sp := Vptr stk Int.zero in @@ -736,9 +746,14 @@ Definition exec_instr (c: code) (i: instruction) (rs: regset) (m: mem) : outcome | Pstwx rd r1 r2 => store2 Mint32 rd r1 r2 rs m | Psubfc rd r1 r2 => - OK (nextinstr (rs#rd <- (Val.sub rs#r2 rs#r1) #CARRY <- Vundef)) m + OK (nextinstr (rs#rd <- (Val.sub rs#r2 rs#r1) + #CARRY <- (Val.add_carry rs#r2 (Val.notint rs#r1) Vone))) m + | Psubfe rd r1 r2 => + OK (nextinstr (rs#rd <- (Val.add (Val.add rs#r2 (Val.notint rs#r1)) rs#CARRY) + #CARRY <- (Val.add_carry rs#r2 (Val.notint rs#r1) rs#CARRY))) m | Psubfic rd r1 cst => - OK (nextinstr (rs#rd <- (Val.sub (const_low cst) rs#r1) #CARRY <- Vundef)) m + OK (nextinstr (rs#rd <- (Val.sub (const_low cst) rs#r1) + #CARRY <- (Val.add_carry (const_low cst) (Val.notint rs#r1) Vone))) m | Pxor rd r1 r2 => OK (nextinstr (rs#rd <- (Val.xor rs#r1 rs#r2))) m | Pxori rd r1 cst => diff --git a/powerpc/Asmgen.v b/powerpc/Asmgen.v index cecc13e9..790b2b9b 100644 --- a/powerpc/Asmgen.v +++ b/powerpc/Asmgen.v @@ -213,6 +213,10 @@ Definition crbit_for_cond (cond: condition) := (** Recognition of comparisons [>= 0] and [< 0]. *) Inductive condition_class: condition -> list mreg -> Type := + | condition_eq0: + forall n r, n = Int.zero -> condition_class (Ccompimm Ceq n) (r :: nil) + | condition_ne0: + forall n r, n = Int.zero -> condition_class (Ccompimm Cne n) (r :: nil) | condition_ge0: forall n r, n = Int.zero -> condition_class (Ccompimm Cge n) (r :: nil) | condition_lt0: @@ -222,6 +226,16 @@ Inductive condition_class: condition -> list mreg -> Type := Definition classify_condition (c: condition) (args: list mreg): condition_class c args := match c as z1, args as z2 return condition_class z1 z2 with + | Ccompimm Ceq n, r :: nil => + match Int.eq_dec n Int.zero with + | left EQ => condition_eq0 n r EQ + | right _ => condition_default (Ccompimm Ceq n) (r :: nil) + end + | Ccompimm Cne n, r :: nil => + match Int.eq_dec n Int.zero with + | left EQ => condition_ne0 n r EQ + | right _ => condition_default (Ccompimm Cne n) (r :: nil) + end | Ccompimm Cge n, r :: nil => match Int.eq_dec n Int.zero with | left EQ => condition_ge0 n r EQ @@ -236,6 +250,33 @@ Definition classify_condition (c: condition) (args: list mreg): condition_class condition_default x y end. +(** Translation of a condition operator. The generated code sets + the [r] target register to 0 or 1 depending on the truth value of the + condition. *) + +Definition transl_cond_op + (cond: condition) (args: list mreg) (r: mreg) (k: code) := + match classify_condition cond args with + | condition_eq0 _ a _ => + Psubfic GPR0 (ireg_of a) (Cint Int.zero) :: + Padde (ireg_of r) GPR0 (ireg_of a) :: k + | condition_ne0 _ a _ => + Paddic GPR0 (ireg_of a) (Cint Int.mone) :: + Psubfe (ireg_of r) GPR0 (ireg_of a) :: k + | condition_ge0 _ a _ => + Prlwinm (ireg_of r) (ireg_of a) Int.one Int.one :: + Pxori (ireg_of r) (ireg_of r) (Cint Int.one) :: k + | condition_lt0 _ a _ => + Prlwinm (ireg_of r) (ireg_of a) Int.one Int.one :: k + | condition_default _ _ => + let p := crbit_for_cond cond in + transl_cond cond args + (Pmfcrbit (ireg_of r) (fst p) :: + if snd p + then k + else Pxori (ireg_of r) (ireg_of r) (Cint Int.one) :: k) + end. + (** Translation of the arithmetic operation [r <- op(args)]. The corresponding instructions are prepended to [k]. *) @@ -350,20 +391,7 @@ Definition transl_op | Ofloatofwords, a1 :: a2 :: nil => Pfmake (freg_of r) (ireg_of a1) (ireg_of a2) :: k | Ocmp cmp, _ => - match classify_condition cmp args with - | condition_ge0 _ a _ => - Prlwinm (ireg_of r) (ireg_of a) Int.one Int.one :: - Pxori (ireg_of r) (ireg_of r) (Cint Int.one) :: k - | condition_lt0 _ a _ => - Prlwinm (ireg_of r) (ireg_of a) Int.one Int.one :: k - | condition_default _ _ => - let p := crbit_for_cond cmp in - transl_cond cmp args - (Pmfcrbit (ireg_of r) (fst p) :: - if snd p - then k - else Pxori (ireg_of r) (ireg_of r) (Cint Int.one) :: k) - end + transl_cond_op cmp args r k | _, _ => k (**r never happens for well-typed code *) end. diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 97b04bb5..1d270e5d 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -417,28 +417,15 @@ Proof. Qed. Hint Rewrite transl_cond_label: labels. -Remark transl_op_cmp_label: +Remark transl_cond_op_label: forall c args r k, - find_label lbl - (match classify_condition c args with - | condition_ge0 _ a _ => - Prlwinm (ireg_of r) (ireg_of a) Int.one Int.one - :: Pxori (ireg_of r) (ireg_of r) (Cint Int.one) :: k - | condition_lt0 _ a _ => - Prlwinm (ireg_of r) (ireg_of a) Int.one Int.one :: k - | condition_default _ _ => - transl_cond c args - (Pmfcrbit (ireg_of r) (fst (crbit_for_cond c)) - :: (if snd (crbit_for_cond c) - then k - else Pxori (ireg_of r) (ireg_of r) (Cint Int.one) :: k)) - end) = find_label lbl k. + find_label lbl (transl_cond_op c args r k) = find_label lbl k. Proof. - intros. destruct (classify_condition c args); auto. - autorewrite with labels. - case (snd (crbit_for_cond c)); auto. + intros c args. + unfold transl_cond_op. destruct (classify_condition c args); intros; auto. + autorewrite with labels. destruct (snd (crbit_for_cond c)); auto. Qed. -Hint Rewrite transl_op_cmp_label: labels. +Hint Rewrite transl_cond_op_label: labels. Remark transl_op_label: forall op args r k, find_label lbl (transl_op op args r k) = find_label lbl k. @@ -719,11 +706,7 @@ Proof. intros [rs2 [EX [RES OTH]]]. left; eapply exec_straight_steps; eauto with coqlib. simpl. exists rs2; split. auto. - apply agree_exten_2 with (rs#(preg_of dst) <- v'). - auto with ppcgen. - intros. unfold Pregmap.set. destruct (PregEq.eq r0 (preg_of dst)). - subst r0. auto. - apply OTH; auto. + apply agree_set_mreg with rs; auto with ppcgen. congruence. Qed. Lemma exec_Msetstack_prop: @@ -748,7 +731,7 @@ Proof. intros [rs2 [EX OTH]]. left; eapply exec_straight_steps; eauto with coqlib. exists rs2; split; auto. - apply agree_exten_2 with rs; auto. + apply agree_exten with rs; auto with ppcgen. Qed. Lemma exec_Mgetparam_prop: @@ -782,12 +765,11 @@ Proof. simpl. unfold load1. simpl. rewrite gpr_or_zero_not_zero. rewrite <- (sp_val _ _ _ AG). rewrite A. auto. congruence. auto. auto. - assert (agree (Regmap.set IT1 Vundef ms) sp rs1). - unfold rs1. change (IR GPR11) with (preg_of IT1). auto with ppcgen. - apply agree_exten_2 with (rs1#(preg_of dst) <- v'). - auto with ppcgen. - intros. unfold Pregmap.set. destruct (PregEq.eq r (preg_of dst)). - congruence. auto. + apply agree_set_mreg with rs1; auto with ppcgen. + unfold rs1. change (IR GPR11) with (preg_of IT1). + apply agree_nextinstr. apply agree_set_mreg with rs; auto with ppcgen. + intros. apply Pregmap.gso; auto with ppcgen. + congruence. Qed. Lemma exec_Mop_prop: @@ -1123,9 +1105,9 @@ Proof. rewrite <- H0. simpl. constructor; auto. eapply code_tail_next_int; eauto. apply sym_not_equal. auto with ppcgen. - apply agree_nextinstr. apply agree_set_mreg; auto. - eapply agree_undef_temps; eauto. - intros. repeat rewrite Pregmap.gso; auto. + apply agree_nextinstr. apply agree_set_mreg_undef_temps with rs; auto. + rewrite Pregmap.gss. auto. + intros. repeat rewrite Pregmap.gso; auto with ppcgen. Qed. Lemma exec_Mannot_prop: @@ -1178,7 +1160,7 @@ Proof. simpl; auto. econstructor; eauto. eapply Mach.find_label_incl; eauto. - apply agree_exten_2 with rs; auto. + apply agree_exten with rs; auto with ppcgen. Qed. Lemma exec_Mcond_true_prop: @@ -1221,7 +1203,7 @@ Proof. traceEq. econstructor; eauto. eapply Mach.find_label_incl; eauto. - apply agree_exten_2 with rs2; auto with ppcgen. + apply agree_undef_temps with rs2; auto with ppcgen. Qed. Lemma exec_Mcond_false_prop: @@ -1245,7 +1227,7 @@ Proof. reflexivity. apply exec_straight_one. simpl. rewrite RES. reflexivity. reflexivity. - auto with ppcgen. + apply agree_nextinstr. apply agree_undef_temps with rs2; auto. Qed. Lemma exec_Mjumptable_prop: @@ -1301,11 +1283,11 @@ Proof. change label with Mach.label; rewrite H0. exact GOTO. omega. traceEq. econstructor; eauto. eapply Mach.find_label_incl; eauto. - apply agree_exten_2 with rs2; auto. - unfold rs2, rs1. apply agree_set_other; auto with ppcgen. apply agree_undef_temps with rs0; auto. - intros. rewrite Pregmap.gso; auto. rewrite nextinstr_inv; auto. - rewrite Pregmap.gso; auto. + intros. rewrite INV3; auto with ppcgen. + unfold rs2. repeat rewrite Pregmap.gso; auto with ppcgen. + unfold rs1. rewrite nextinstr_inv; auto with ppcgen. + apply Pregmap.gso; auto with ppcgen. Qed. Lemma exec_Mreturn_prop: @@ -1433,7 +1415,7 @@ Proof. eapply exec_straight_steps_1; eauto. change (Int.unsigned Int.zero) with 0. constructor. (* match states *) - econstructor; eauto with coqlib. auto with ppcgen. + econstructor; eauto with coqlib. apply agree_undef_temps with rs4; auto. Qed. Lemma exec_function_external_prop: @@ -1460,7 +1442,11 @@ Proof. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. econstructor; eauto. - unfold loc_external_result. auto with ppcgen. + unfold loc_external_result. + apply agree_set_other; auto with ppcgen. + apply agree_set_mreg with rs; auto. + rewrite Pregmap.gss; auto. + intros; apply Pregmap.gso; auto. Qed. Lemma exec_return_prop: diff --git a/powerpc/Asmgenproof1.v b/powerpc/Asmgenproof1.v index 55a74be1..42355ad0 100644 --- a/powerpc/Asmgenproof1.v +++ b/powerpc/Asmgenproof1.v @@ -115,58 +115,90 @@ Qed. (** Characterization of PPC registers that correspond to Mach registers. *) -Definition is_data_reg (r: preg) : Prop := +Definition is_data_reg (r: preg) : bool := match r with - | IR GPR0 => False - | PC => False | LR => False | CTR => False - | CR0_0 => False | CR0_1 => False | CR0_2 => False | CR0_3 => False - | CARRY => False - | _ => True + | IR GPR0 => false + | PC => false | LR => false | CTR => false + | CR0_0 => false | CR0_1 => false | CR0_2 => false | CR0_3 => false + | CARRY => false + | _ => true end. Lemma ireg_of_is_data_reg: - forall (r: mreg), is_data_reg (ireg_of r). + forall (r: mreg), is_data_reg (ireg_of r) = true. Proof. - destruct r; exact I. + destruct r; reflexivity. Qed. Lemma freg_of_is_data_reg: - forall (r: mreg), is_data_reg (ireg_of r). + forall (r: mreg), is_data_reg (ireg_of r) = true. Proof. - destruct r; exact I. + destruct r; reflexivity. Qed. Lemma preg_of_is_data_reg: - forall (r: mreg), is_data_reg (preg_of r). + forall (r: mreg), is_data_reg (preg_of r) = true. Proof. - destruct r; exact I. + destruct r; reflexivity. Qed. -Lemma ireg_of_not_GPR1: - forall r, ireg_of r <> GPR1. +Lemma data_reg_diff: + forall r r', is_data_reg r = true -> is_data_reg r' = false -> r <> r'. Proof. - intro. case r; discriminate. + intros. congruence. Qed. -Lemma ireg_of_not_GPR0: - forall r, ireg_of r <> GPR0. + +Lemma ireg_diff: + forall r r', r <> r' -> IR r <> IR r'. Proof. - intro. case r; discriminate. + intros. congruence. +Qed. + +Lemma diff_ireg: + forall r r', IR r <> IR r' -> r <> r'. +Proof. + intros. congruence. +Qed. + +Hint Resolve ireg_of_is_data_reg freg_of_is_data_reg preg_of_is_data_reg + data_reg_diff ireg_diff diff_ireg: ppcgen. + +Definition is_nontemp_reg (r: preg) : bool := + match r with + | IR GPR0 => false | IR GPR11 => false | IR GPR12 => false + | FR FPR0 => false | FR FPR12 => false | FR FPR13 => false + | PC => false | LR => false | CTR => false + | CR0_0 => false | CR0_1 => false | CR0_2 => false | CR0_3 => false + | CARRY => false + | _ => true + end. + +Remark is_nontemp_is_data: + forall r, is_nontemp_reg r = true -> is_data_reg r = true. +Proof. + destruct r; simpl; try congruence. destruct i; congruence. +Qed. + +Lemma nontemp_reg_diff: + forall r r', is_nontemp_reg r = true -> is_nontemp_reg r' = false -> r <> r'. +Proof. + intros. congruence. Qed. -Hint Resolve ireg_of_not_GPR1 ireg_of_not_GPR0: ppcgen. -Lemma preg_of_not: - forall r1 r2, ~(is_data_reg r2) -> preg_of r1 <> r2. +Hint Resolve is_nontemp_is_data nontemp_reg_diff: ppcgen. + +Lemma ireg_of_not_GPR1: + forall r, ireg_of r <> GPR1. Proof. - intros; red; intro. subst r2. elim H. apply preg_of_is_data_reg. + intro. case r; discriminate. Qed. -Hint Resolve preg_of_not: ppcgen. Lemma preg_of_not_GPR1: forall r, preg_of r <> GPR1. Proof. intro. case r; discriminate. Qed. -Hint Resolve preg_of_not_GPR1: ppcgen. +Hint Resolve ireg_of_not_GPR1 preg_of_not_GPR1: ppcgen. Lemma int_temp_for_diff: forall r, IR(int_temp_for r) <> preg_of r. @@ -229,79 +261,63 @@ Proof. intros. elim H; auto. Qed. -Lemma agree_exten_1: +Lemma agree_exten: forall ms sp rs rs', agree ms sp rs -> - (forall r, is_data_reg r -> rs'#r = rs#r) -> + (forall r, is_data_reg r = true -> rs'#r = rs#r) -> agree ms sp rs'. Proof. - intros. inv H. constructor. - apply H0. exact I. - auto. - intros. rewrite H0. auto. apply preg_of_is_data_reg. -Qed. - -Lemma agree_exten_2: - forall ms sp rs rs', - agree ms sp rs -> - (forall r, - r <> IR GPR0 -> - r <> PC -> r <> LR -> r <> CTR -> - r <> CR0_0 -> r <> CR0_1 -> r <> CR0_2 -> r <> CR0_3 -> - r <> CARRY -> - rs'#r = rs#r) -> - agree ms sp rs'. -Proof. - intros. apply agree_exten_1 with rs. auto. - intros. apply H0; (red; intro; subst r; elim H1). + intros. inv H. constructor; auto. + intros. rewrite H0; auto with ppcgen. Qed. (** Preservation of register agreement under various assignments. *) Lemma agree_set_mreg: - forall ms sp rs r v v', + forall ms sp rs r v rs', agree ms sp rs -> - Val.lessdef v v' -> - agree (Regmap.set r v ms) sp (rs#(preg_of r) <- v'). + Val.lessdef v (rs'#(preg_of r)) -> + (forall r', is_data_reg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') -> + agree (Regmap.set r v ms) sp rs'. Proof. - intros. inv H. constructor. - rewrite Pregmap.gso. auto. apply sym_not_eq. apply preg_of_not_GPR1. - auto. - intros. unfold Regmap.set. case (RegEq.eq r0 r); intro. - subst r0. rewrite Pregmap.gss. auto. - rewrite Pregmap.gso. auto. red; intro. - elim n. apply preg_of_injective; auto. + intros. inv H. constructor; auto with ppcgen. + intros. unfold Regmap.set. destruct (RegEq.eq r0 r). + subst r0. auto. + rewrite H1; auto with ppcgen. red; intros; elim n; apply preg_of_injective; auto. Qed. Hint Resolve agree_set_mreg: ppcgen. Lemma agree_set_mireg: - forall ms sp rs r v, - agree ms sp (rs#(preg_of r) <- v) -> + forall ms sp rs r v (rs': regset), + agree ms sp rs -> + Val.lessdef v (rs'#(ireg_of r)) -> mreg_type r = Tint -> - agree ms sp (rs#(ireg_of r) <- v). + (forall r', is_data_reg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') -> + agree (Regmap.set r v ms) sp rs'. Proof. - intros. unfold preg_of in H. rewrite H0 in H. auto. + intros. eapply agree_set_mreg; eauto. unfold preg_of; rewrite H1; auto. Qed. Hint Resolve agree_set_mireg: ppcgen. Lemma agree_set_mfreg: - forall ms sp rs r v, - agree ms sp (rs#(preg_of r) <- v) -> + forall ms sp rs r v (rs': regset), + agree ms sp rs -> + Val.lessdef v (rs'#(freg_of r)) -> mreg_type r = Tfloat -> - agree ms sp (rs#(freg_of r) <- v). + (forall r', is_data_reg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') -> + agree (Regmap.set r v ms) sp rs'. Proof. - intros. unfold preg_of in H. rewrite H0 in H. auto. + intros. eapply agree_set_mreg; eauto. unfold preg_of; rewrite H1; auto. Qed. -Hint Resolve agree_set_mfreg: ppcgen. Lemma agree_set_other: forall ms sp rs r v, agree ms sp rs -> - ~(is_data_reg r) -> + is_data_reg r = false -> agree ms sp (rs#r <- v). Proof. - intros. apply agree_exten_1 with rs. - auto. intros. apply Pregmap.gso. red; intro; subst r0; contradiction. + intros. apply agree_exten with rs. + auto. intros. apply Pregmap.gso. congruence. Qed. Hint Resolve agree_set_other: ppcgen. @@ -313,24 +329,49 @@ Proof. Qed. Hint Resolve agree_nextinstr: ppcgen. -Lemma agree_set_mireg_twice: - forall ms sp rs r v v' v1, +Lemma agree_undef_regs: + forall rl ms sp rs rs', agree ms sp rs -> - mreg_type r = Tint -> - Val.lessdef v v' -> - agree (Regmap.set r v ms) sp (rs #(ireg_of r) <- v1 #(ireg_of r) <- v'). -Proof. - intros. replace (IR (ireg_of r)) with (preg_of r). inv H. - split. repeat (rewrite Pregmap.gso; auto with ppcgen). auto. - intros. case (mreg_eq r r0); intro. - subst r0. rewrite Regmap.gss. rewrite Pregmap.gss. auto. - assert (preg_of r <> preg_of r0). - red; intro. elim n. apply preg_of_injective. auto. - rewrite Regmap.gso; auto. - repeat (rewrite Pregmap.gso; auto). - unfold preg_of. rewrite H0. auto. + (forall r, is_data_reg r = true -> ~In r (List.map preg_of rl) -> rs'#r = rs#r) -> + agree (undef_regs rl ms) sp rs'. +Proof. + induction rl; simpl; intros. + apply agree_exten with rs; auto. + apply IHrl with (rs#(preg_of a) <- (rs'#(preg_of a))). + apply agree_set_mreg with rs; auto with ppcgen. + intros. unfold Pregmap.set. destruct (PregEq.eq r' (preg_of a)). + congruence. auto. + intros. unfold Pregmap.set. destruct (PregEq.eq r (preg_of a)). + congruence. apply H0; auto. intuition congruence. +Qed. + +Lemma agree_undef_temps: + forall ms sp rs rs', + agree ms sp rs -> + (forall r, is_nontemp_reg r = true -> rs'#r = rs#r) -> + agree (undef_temps ms) sp rs'. +Proof. + unfold undef_temps. intros. apply agree_undef_regs with rs; auto. + simpl. unfold preg_of; simpl. intros. intuition. + apply H0. destruct r; simpl in *; auto. + destruct i; intuition. destruct f; intuition. +Qed. +Hint Resolve agree_undef_temps: ppcgen. + +Lemma agree_set_mreg_undef_temps: + forall ms sp rs r v rs', + agree ms sp rs -> + Val.lessdef v (rs'#(preg_of r)) -> + (forall r', is_nontemp_reg r' = true -> r' <> preg_of r -> rs'#r' = rs#r') -> + agree (Regmap.set r v (undef_temps ms)) sp rs'. +Proof. + intros. apply agree_set_mreg with (rs'#(preg_of r) <- (rs#(preg_of r))). + apply agree_undef_temps with rs; auto. + intros. unfold Pregmap.set. destruct (PregEq.eq r0 (preg_of r)). + congruence. apply H1; auto. + auto. + intros. rewrite Pregmap.gso; auto. Qed. -Hint Resolve agree_set_mireg_twice: ppcgen. Lemma agree_set_twice_mireg: forall ms sp rs r v v1 v', @@ -353,101 +394,6 @@ Proof. red; intros. elim n. apply preg_of_injective; auto. unfold preg_of. rewrite H0. auto. Qed. -Hint Resolve agree_set_twice_mireg: ppcgen. - -Lemma agree_set_commut: - forall ms sp rs r1 r2 v1 v2, - r1 <> r2 -> - agree ms sp ((rs#r2 <- v2)#r1 <- v1) -> - agree ms sp ((rs#r1 <- v1)#r2 <- v2). -Proof. - intros. apply agree_exten_1 with ((rs#r2 <- v2)#r1 <- v1). auto. - intros. - case (preg_eq r r1); intro. - subst r1. rewrite Pregmap.gss. rewrite Pregmap.gso. rewrite Pregmap.gss. - auto. auto. - case (preg_eq r r2); intro. - subst r2. rewrite Pregmap.gss. rewrite Pregmap.gso. rewrite Pregmap.gss. - auto. auto. - repeat (rewrite Pregmap.gso; auto). -Qed. -Hint Resolve agree_set_commut: ppcgen. - -Lemma agree_nextinstr_commut: - forall ms sp rs r v, - agree ms sp (rs#r <- v) -> - r <> PC -> - agree ms sp ((nextinstr rs)#r <- v). -Proof. - intros. unfold nextinstr. apply agree_set_commut. auto. - apply agree_set_other. auto. auto. -Qed. -Hint Resolve agree_nextinstr_commut: ppcgen. - -Lemma agree_set_mireg_exten: - forall ms sp rs r v (rs': regset), - agree ms sp rs -> - mreg_type r = Tint -> - Val.lessdef v rs'#(ireg_of r) -> - (forall r', - r' <> IR GPR0 -> - r' <> PC -> r' <> LR -> r' <> CTR -> - r' <> CR0_0 -> r' <> CR0_1 -> r' <> CR0_2 -> r' <> CR0_3 -> - r' <> CARRY -> - r' <> IR (ireg_of r) -> rs'#r' = rs#r') -> - agree (Regmap.set r v ms) sp rs'. -Proof. - intros. set (v' := rs'#(ireg_of r)). - apply agree_exten_2 with (rs#(ireg_of r) <- v'). - auto with ppcgen. - intros. unfold Pregmap.set. case (PregEq.eq r0 (ireg_of r)); intro. - subst r0. auto. apply H2; auto. -Qed. -Hint Resolve agree_set_mireg_exten: ppcgen. - -Lemma agree_undef_regs: - forall rl ms sp rs rs', - agree ms sp rs -> - (forall r, is_data_reg r -> ~In r (List.map preg_of rl) -> rs'#r = rs#r) -> - agree (undef_regs rl ms) sp rs'. -Proof. - induction rl; simpl; intros. - apply agree_exten_1 with rs; auto. - apply IHrl with (rs#(preg_of a) <- (rs'#(preg_of a))). - apply agree_set_mreg; auto. - intros. unfold Pregmap.set. - destruct (PregEq.eq r (preg_of a)). - congruence. - apply H0. auto. intuition congruence. -Qed. - -Lemma agree_undef_temps: - forall ms sp rs rs', - agree ms sp rs -> - (forall r, - r <> IR GPR0 -> - r <> PC -> r <> LR -> r <> CTR -> - r <> CR0_0 -> r <> CR0_1 -> r <> CR0_2 -> r <> CR0_3 -> - r <> CARRY -> - r <> IR GPR11 -> r <> IR GPR12 -> - r <> FR FPR0 -> r <> FR FPR12 -> r <> FR FPR13 -> - rs'#r = rs#r) -> - agree (undef_temps ms) sp rs'. -Proof. - unfold undef_temps. intros. apply agree_undef_regs with rs; auto. - simpl. unfold preg_of; simpl. intros. - apply H0; (red; intro; subst; simpl in H1; intuition congruence). -Qed. -Hint Resolve agree_undef_temps: ppcgen. - -Lemma agree_undef_temps_2: - forall ms sp rs, - agree ms sp rs -> - agree (undef_temps ms) sp rs. -Proof. - intros. apply agree_undef_temps with rs; auto. -Qed. -Hint Resolve agree_undef_temps_2: ppcgen. (** Useful properties of the PC and GPR0 registers. *) @@ -458,15 +404,6 @@ Proof. Qed. Hint Resolve nextinstr_inv: ppcgen. -Lemma nextinstr_set_preg: - forall rs m v, - (nextinstr (rs#(preg_of m) <- v))#PC = Val.add rs#PC Vone. -Proof. - intros. unfold nextinstr. rewrite Pregmap.gss. - rewrite Pregmap.gso. auto. apply sym_not_eq. auto with ppcgen. -Qed. -Hint Resolve nextinstr_set_preg: ppcgen. - Lemma gpr_or_zero_not_zero: forall rs r, r <> GPR0 -> gpr_or_zero rs r = rs#r. Proof. @@ -622,6 +559,19 @@ Qed. (** * Correctness of PowerPC constructor functions *) +(* +Ltac SIMP := + match goal with + | [ |- nextinstr _ _ = _ ] => rewrite nextinstr_inv; [auto | auto with ppcgen] + | [ |- Pregmap.get ?x (Pregmap.set ?x _ _) = _ ] => rewrite Pregmap.gss; auto + | [ |- Pregmap.set ?x _ _ ?x = _ ] => rewrite Pregmap.gss; auto + | [ |- Pregmap.get _ (Pregmap.set _ _ _) = _ ] => rewrite Pregmap.gso; [auto | auto with ppcgen] + | [ |- Pregmap.set _ _ _ _ = _ ] => rewrite Pregmap.gso; [auto | auto with ppcgen] + end. +*) +Ltac SIMP := + (rewrite nextinstr_inv || rewrite Pregmap.gss || rewrite Pregmap.gso); auto with ppcgen. + (** Properties of comparisons. *) Lemma compare_float_spec: @@ -630,15 +580,13 @@ Lemma compare_float_spec: rs1#CR0_0 = Val.cmpf Clt v1 v2 /\ rs1#CR0_1 = Val.cmpf Cgt v1 v2 /\ rs1#CR0_2 = Val.cmpf Ceq v1 v2 - /\ forall r', r' <> PC -> r' <> CR0_0 -> r' <> CR0_1 -> - r' <> CR0_2 -> r' <> CR0_3 -> rs1#r' = rs#r'. + /\ forall r', r' <> CR0_0 -> r' <> CR0_1 -> r' <> CR0_2 -> r' <> CR0_3 -> r' <> PC -> rs1#r' = rs#r'. Proof. intros. unfold rs1. split. reflexivity. split. reflexivity. split. reflexivity. - intros. rewrite nextinstr_inv; auto. - unfold compare_float. repeat (rewrite Pregmap.gso; auto). + intros. unfold compare_float. repeat SIMP. Qed. Lemma compare_sint_spec: @@ -647,15 +595,13 @@ Lemma compare_sint_spec: rs1#CR0_0 = Val.cmp Clt v1 v2 /\ rs1#CR0_1 = Val.cmp Cgt v1 v2 /\ rs1#CR0_2 = Val.cmp Ceq v1 v2 - /\ forall r', r' <> PC -> r' <> CR0_0 -> r' <> CR0_1 -> - r' <> CR0_2 -> r' <> CR0_3 -> rs1#r' = rs#r'. + /\ forall r', r' <> CR0_0 -> r' <> CR0_1 -> r' <> CR0_2 -> r' <> CR0_3 -> r' <> PC -> rs1#r' = rs#r'. Proof. intros. unfold rs1. split. reflexivity. split. reflexivity. split. reflexivity. - intros. rewrite nextinstr_inv; auto. - unfold compare_sint. repeat (rewrite Pregmap.gso; auto). + intros. unfold compare_sint. repeat SIMP. Qed. Lemma compare_uint_spec: @@ -664,15 +610,13 @@ Lemma compare_uint_spec: rs1#CR0_0 = Val.cmpu Clt v1 v2 /\ rs1#CR0_1 = Val.cmpu Cgt v1 v2 /\ rs1#CR0_2 = Val.cmpu Ceq v1 v2 - /\ forall r', r' <> PC -> r' <> CR0_0 -> r' <> CR0_1 -> - r' <> CR0_2 -> r' <> CR0_3 -> rs1#r' = rs#r'. + /\ forall r', r' <> CR0_0 -> r' <> CR0_1 -> r' <> CR0_2 -> r' <> CR0_3 -> r' <> PC -> rs1#r' = rs#r'. Proof. intros. unfold rs1. split. reflexivity. split. reflexivity. split. reflexivity. - intros. rewrite nextinstr_inv; auto. - unfold compare_uint. repeat (rewrite Pregmap.gso; auto). + intros. unfold compare_uint. repeat SIMP. Qed. (** Loading a constant. *) @@ -689,11 +633,9 @@ Proof. (* addi *) exists (nextinstr (rs#r <- (Vint n))). split. apply exec_straight_one. - simpl. rewrite Int.add_commut. rewrite Int.add_zero. reflexivity. + simpl. rewrite Int.add_zero_l. auto. reflexivity. - split. rewrite nextinstr_inv; auto with ppcgen. - apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + split. repeat SIMP. intros; repeat SIMP. (* addis *) generalize (Int.eq_spec (low_s n) Int.zero); case (Int.eq (low_s n) Int.zero); intro. exists (nextinstr (rs#r <- (Vint n))). @@ -701,19 +643,16 @@ Proof. simpl. rewrite Int.add_commut. rewrite <- H. rewrite low_high_s. reflexivity. reflexivity. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + split. repeat SIMP. intros; repeat SIMP. (* addis + ori *) pose (rs1 := nextinstr (rs#r <- (Vint (Int.shl (high_u n) (Int.repr 16))))). exists (nextinstr (rs1#r <- (Vint n))). split. eapply exec_straight_two. - simpl. rewrite Int.add_commut. rewrite Int.add_zero. reflexivity. + simpl. rewrite Int.add_zero_l. reflexivity. simpl. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. unfold Val.or. rewrite low_high_u. reflexivity. reflexivity. reflexivity. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. - unfold rs1. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. + unfold rs1. split. repeat SIMP. intros; repeat SIMP. Qed. (** Add integer immediate. *) @@ -734,8 +673,7 @@ Proof. split. apply exec_straight_one. simpl. rewrite gpr_or_zero_not_zero; auto. reflexivity. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + split. repeat SIMP. intros. repeat SIMP. (* addis *) generalize (Int.eq_spec (low_s n) Int.zero); case (Int.eq (low_s n) Int.zero); intro. exists (nextinstr (rs#r1 <- (Val.add rs#r2 (Vint n)))). @@ -744,8 +682,7 @@ Proof. generalize (low_high_s n). rewrite H1. rewrite Int.add_zero. intro. rewrite H2. auto. reflexivity. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + split. repeat SIMP. intros; repeat SIMP. (* addis + addi *) pose (rs1 := nextinstr (rs#r1 <- (Val.add rs#r2 (Vint (Int.shl (high_s n) (Int.repr 16)))))). exists (nextinstr (rs1#r1 <- (Val.add rs#r2 (Vint n)))). @@ -755,9 +692,7 @@ Proof. unfold rs1 at 1. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. rewrite Val.add_assoc. simpl. rewrite low_high_s. auto. reflexivity. reflexivity. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. - unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + unfold rs1; split. repeat SIMP. intros; repeat SIMP. Qed. (** And integer immediate. *) @@ -770,10 +705,7 @@ Lemma andimm_correct: exec_straight (andimm r1 r2 n k) rs m k rs' m /\ rs'#r1 = v /\ rs'#CR0_2 = Val.cmp Ceq v Vzero - /\ forall r': preg, - r' <> r1 -> r' <> GPR0 -> r' <> PC -> - r' <> CR0_0 -> r' <> CR0_1 -> r' <> CR0_2 -> r' <> CR0_3 -> - rs'#r' = rs#r'. + /\ forall r', is_data_reg r' = true -> r' <> r1 -> rs'#r' = rs#r'. Proof. intros. unfold andimm. case (Int.eq (high_u n) Int.zero). @@ -782,9 +714,9 @@ Proof. generalize (compare_sint_spec (rs#r1 <- v) v Vzero). intros [A [B [C D]]]. split. apply exec_straight_one. reflexivity. reflexivity. - split. rewrite D; try discriminate. apply Pregmap.gss. + split. rewrite D; auto with ppcgen. SIMP. split. auto. - intros. rewrite D; auto. apply Pregmap.gso; auto. + intros. rewrite D; auto with ppcgen. SIMP. (* andis *) generalize (Int.eq_spec (low_u n) Int.zero); case (Int.eq (low_u n) Int.zero); intro. @@ -794,9 +726,9 @@ Proof. split. apply exec_straight_one. simpl. generalize (low_high_u n). rewrite H0. rewrite Int.or_zero. intro. rewrite H1. reflexivity. reflexivity. - split. rewrite D; try discriminate. apply Pregmap.gss. + split. rewrite D; auto with ppcgen. SIMP. split. auto. - intros. rewrite D; auto. apply Pregmap.gso; auto. + intros. rewrite D; auto with ppcgen. SIMP. (* loadimm + and *) generalize (loadimm_correct GPR0 n (Pand_ r1 r2 GPR0 :: k) rs m). intros [rs1 [EX1 [RES1 OTHER1]]]. @@ -807,9 +739,9 @@ Proof. apply exec_straight_one. simpl. rewrite RES1. rewrite (OTHER1 r2). reflexivity. congruence. congruence. reflexivity. - split. rewrite D; try discriminate. apply Pregmap.gss. + split. rewrite D; auto with ppcgen. SIMP. split. auto. - intros. rewrite D; auto. rewrite Pregmap.gso; auto. + intros. rewrite D; auto with ppcgen. SIMP. Qed. (** Or integer immediate. *) @@ -827,8 +759,8 @@ Proof. (* ori *) exists (nextinstr (rs#r1 <- v)). split. apply exec_straight_one. reflexivity. reflexivity. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + split. repeat SIMP. + intros. repeat SIMP. (* oris *) generalize (Int.eq_spec (low_u n) Int.zero); case (Int.eq (low_u n) Int.zero); intro. @@ -836,19 +768,12 @@ Proof. split. apply exec_straight_one. simpl. generalize (low_high_u n). rewrite H. rewrite Int.or_zero. intro. rewrite H0. reflexivity. reflexivity. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + split. repeat SIMP. + intros. repeat SIMP. (* oris + ori *) - pose (rs1 := nextinstr (rs#r1 <- (Val.or rs#r2 (Vint (Int.shl (high_u n) (Int.repr 16)))))). - exists (nextinstr (rs1#r1 <- v)). - split. apply exec_straight_two with rs1 m. - reflexivity. simpl. unfold rs1 at 1. - rewrite nextinstr_inv; auto with ppcgen. - rewrite Pregmap.gss. rewrite Val.or_assoc. simpl. - rewrite low_high_u. reflexivity. reflexivity. reflexivity. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. - unfold rs1. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. + econstructor; split. eapply exec_straight_two; simpl; reflexivity. + split. repeat rewrite nextinstr_inv; auto with ppcgen. repeat rewrite Pregmap.gss. rewrite Val.or_assoc. simpl. rewrite low_high_u. reflexivity. + intros. repeat SIMP. Qed. (** Xor integer immediate. *) @@ -866,8 +791,7 @@ Proof. (* xori *) exists (nextinstr (rs#r1 <- v)). split. apply exec_straight_one. reflexivity. reflexivity. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + split. repeat SIMP. intros. repeat SIMP. (* xoris *) generalize (Int.eq_spec (low_u n) Int.zero); case (Int.eq (low_u n) Int.zero); intro. @@ -875,20 +799,12 @@ Proof. split. apply exec_straight_one. simpl. generalize (low_high_u_xor n). rewrite H. rewrite Int.xor_zero. intro. rewrite H0. reflexivity. reflexivity. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + split. repeat SIMP. intros. repeat SIMP. (* xoris + xori *) - pose (rs1 := nextinstr (rs#r1 <- (Val.xor rs#r2 (Vint (Int.shl (high_u n) (Int.repr 16)))))). - exists (nextinstr (rs1#r1 <- v)). - split. apply exec_straight_two with rs1 m. - reflexivity. simpl. unfold rs1 at 1. - rewrite nextinstr_inv; try discriminate. - rewrite Pregmap.gss. rewrite Val.xor_assoc. simpl. - rewrite low_high_u_xor. reflexivity. reflexivity. reflexivity. - split. rewrite nextinstr_inv; auto with ppcgen. - apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. - unfold rs1. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. + econstructor; split. eapply exec_straight_two; simpl; reflexivity. + split. repeat rewrite nextinstr_inv; auto with ppcgen. repeat rewrite Pregmap.gss. + rewrite Val.xor_assoc. simpl. rewrite low_high_u_xor. reflexivity. + intros. repeat SIMP. Qed. (** Indexed memory loads. *) @@ -906,24 +822,23 @@ Proof. intros. unfold loadind. destruct (Int.eq (high_s ofs) Int.zero). (* one load *) exists (nextinstr (rs#(preg_of dst) <- v)); split. + unfold preg_of. rewrite H0. destruct ty; apply exec_straight_one; auto with ppcgen; simpl. unfold load1. rewrite gpr_or_zero_not_zero; auto. - simpl in *. rewrite H. unfold preg_of; rewrite H0. auto. + simpl in *. rewrite H. auto. unfold load1. rewrite gpr_or_zero_not_zero; auto. - simpl in *. rewrite H. unfold preg_of; rewrite H0. auto. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + simpl in *. rewrite H. auto. + split. repeat SIMP. intros. repeat SIMP. (* loadimm + one load *) exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [A [B C]]]. exists (nextinstr (rs'#(preg_of dst) <- v)); split. eapply exec_straight_trans. eexact A. + unfold preg_of. rewrite H0. destruct ty; apply exec_straight_one; auto with ppcgen; simpl. - unfold load2. rewrite B. rewrite C; auto with ppcgen. simpl in H. rewrite H. - unfold preg_of; rewrite H0. auto. congruence. - unfold load2. rewrite B. rewrite C; auto with ppcgen. simpl in H. rewrite H. - unfold preg_of; rewrite H0. auto. congruence. - split. rewrite nextinstr_inv; auto with ppcgen. apply Pregmap.gss. - intros. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. + unfold load2. rewrite B. rewrite C; auto with ppcgen. simpl in H. rewrite H. auto. + unfold load2. rewrite B. rewrite C; auto with ppcgen. simpl in H. rewrite H. auto. + split. repeat SIMP. + intros. repeat SIMP. Qed. (** Indexed memory stores. *) @@ -948,7 +863,7 @@ Proof. intros. apply nextinstr_inv; auto. (* loadimm + one store *) exploit (loadimm_correct GPR0 ofs); eauto. intros [rs' [A [B C]]]. - assert (rs' base = rs base). apply C; auto with ppcgen. congruence. + assert (rs' base = rs base). apply C; auto with ppcgen. assert (rs' (preg_of src) = rs (preg_of src)). apply C; auto with ppcgen. exists (nextinstr rs'). split. eapply exec_straight_trans. eexact A. @@ -1035,17 +950,16 @@ Ltac UseTypeInfo := (** Translation of conditions. *) -Lemma transl_cond_correct_aux: - forall cond args k ms sp rs m, +Lemma transl_cond_correct_1: + forall cond args k rs m, map mreg_type args = type_of_condition cond -> - agree ms sp rs -> exists rs', exec_straight (transl_cond cond args k) rs m k rs' m /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) = (if snd (crbit_for_cond cond) then eval_condition_total cond (map rs (map preg_of args)) else Val.notbool (eval_condition_total cond (map rs (map preg_of args)))) - /\ agree ms sp rs'. + /\ forall r, is_data_reg r = true -> rs'#r = rs#r. Proof. intros. destruct cond; simpl in H; TypeInv; simpl; UseTypeInfo. @@ -1056,7 +970,7 @@ Proof. apply exec_straight_one. simpl; reflexivity. reflexivity. split. case c; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto. - apply agree_exten_2 with rs; auto. + auto with ppcgen. (* Ccompu *) destruct (compare_uint_spec rs (rs (ireg_of m0)) (rs (ireg_of m1))) as [A [B [C D]]]. @@ -1064,7 +978,7 @@ Proof. apply exec_straight_one. simpl; reflexivity. reflexivity. split. case c; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto. - apply agree_exten_2 with rs; auto. + auto with ppcgen. (* Ccompimm *) case (Int.eq (high_s i) Int.zero). destruct (compare_sint_spec rs (rs (ireg_of m0)) (Vint i)) @@ -1073,21 +987,20 @@ Proof. apply exec_straight_one. simpl. eauto. reflexivity. split. case c; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto. - apply agree_exten_2 with rs; auto. + auto with ppcgen. generalize (loadimm_correct GPR0 i (Pcmpw (ireg_of m0) GPR0 :: k) rs m). intros [rs1 [EX1 [RES1 OTH1]]]. destruct (compare_sint_spec rs1 (rs (ireg_of m0)) (Vint i)) as [A [B [C D]]]. assert (rs1 (ireg_of m0) = rs (ireg_of m0)). - apply OTH1; auto with ppcgen. decEq. auto with ppcgen. + apply OTH1; auto with ppcgen. exists (nextinstr (compare_sint rs1 (rs1 (ireg_of m0)) (Vint i))). split. eapply exec_straight_trans. eexact EX1. apply exec_straight_one. simpl. rewrite RES1; rewrite H; auto. reflexivity. split. rewrite H. case c; simpl; auto; rewrite <- Val.negate_cmp; simpl; auto. - apply agree_exten_2 with rs; auto. - intros. rewrite H; rewrite D; auto. + intros. rewrite H; rewrite D; auto with ppcgen. (* Ccompuimm *) case (Int.eq (high_u i) Int.zero). destruct (compare_uint_spec rs (rs (ireg_of m0)) (Vint i)) @@ -1096,27 +1009,25 @@ Proof. apply exec_straight_one. simpl. eauto. reflexivity. split. case c; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto. - apply agree_exten_2 with rs; auto. + auto with ppcgen. generalize (loadimm_correct GPR0 i (Pcmplw (ireg_of m0) GPR0 :: k) rs m). intros [rs1 [EX1 [RES1 OTH1]]]. destruct (compare_uint_spec rs1 (rs (ireg_of m0)) (Vint i)) as [A [B [C D]]]. - assert (rs1 (ireg_of m0) = rs (ireg_of m0)). - apply OTH1; auto with ppcgen. decEq. auto with ppcgen. + assert (rs1 (ireg_of m0) = rs (ireg_of m0)). apply OTH1; auto with ppcgen. exists (nextinstr (compare_uint rs1 (rs1 (ireg_of m0)) (Vint i))). split. eapply exec_straight_trans. eexact EX1. apply exec_straight_one. simpl. rewrite RES1; rewrite H; auto. reflexivity. split. rewrite H. case c; simpl; auto; rewrite <- Val.negate_cmpu; simpl; auto. - apply agree_exten_2 with rs; auto. - intros. rewrite H; rewrite D; auto. + intros. rewrite H; rewrite D; auto with ppcgen. (* Ccompf *) destruct (floatcomp_correct c (freg_of m0) (freg_of m1) k rs m) as [rs' [EX [RES OTH]]]. exists rs'. split. auto. split. apply RES. - apply agree_exten_2 with rs; auto. + auto with ppcgen. (* Cnotcompf *) destruct (floatcomp_correct c (freg_of m0) (freg_of m1) k rs m) as [rs' [EX [RES OTH]]]. @@ -1126,23 +1037,41 @@ Proof. intros v1 v2; unfold Val.cmpf; destruct v1; destruct v2; auto. apply Val.notbool_idem2. rewrite H. case (snd (crbit_for_fcmp c)); simpl; auto. - apply agree_exten_2 with rs; auto. + auto with ppcgen. (* Cmaskzero *) - destruct (andimm_correct GPR0 (ireg_of m0) i k rs m (ireg_of_not_GPR0 m0)) - as [rs' [A [B [C D]]]]. + destruct (andimm_correct GPR0 (ireg_of m0) i k rs m) + as [rs' [A [B [C D]]]]. auto with ppcgen. exists rs'. split. assumption. split. rewrite C. auto. - apply agree_exten_2 with rs; auto. + auto with ppcgen. (* Cmasknotzero *) - destruct (andimm_correct GPR0 (ireg_of m0) i k rs m (ireg_of_not_GPR0 m0)) - as [rs' [A [B [C D]]]]. + destruct (andimm_correct GPR0 (ireg_of m0) i k rs m) + as [rs' [A [B [C D]]]]. auto with ppcgen. exists rs'. split. assumption. split. rewrite C. rewrite Val.notbool_idem3. reflexivity. - apply agree_exten_2 with rs; auto. + auto with ppcgen. +Qed. + +Lemma transl_cond_correct_2: + forall cond args k rs m b, + map mreg_type args = type_of_condition cond -> + eval_condition cond (map rs (map preg_of args)) m = Some b -> + exists rs', + exec_straight (transl_cond cond args k) rs m k rs' m + /\ rs'#(reg_of_crbit (fst (crbit_for_cond cond))) = + (if snd (crbit_for_cond cond) + then Val.of_bool b + else Val.notbool (Val.of_bool b)) + /\ forall r, is_data_reg r = true -> rs'#r = rs#r. +Proof. + intros. + assert (eval_condition_total cond rs ## (preg_of ## args) = Val.of_bool b). + apply eval_condition_weaken with m. auto. + rewrite <- H1. eapply transl_cond_correct_1; eauto. Qed. Lemma transl_cond_correct: - forall cond args k ms sp rs m m' b, + forall cond args k ms sp rs m b m', map mreg_type args = type_of_condition cond -> agree ms sp rs -> eval_condition cond (map ms args) m = Some b -> @@ -1156,10 +1085,121 @@ Lemma transl_cond_correct: /\ agree ms sp rs'. Proof. intros. - assert (eval_condition_total cond rs ## (preg_of ## args) = Val.of_bool b). - apply eval_condition_weaken with m'. eapply eval_condition_lessdef; eauto. - eapply preg_vals; eauto. - rewrite <- H3. eapply transl_cond_correct_aux; eauto. + exploit transl_cond_correct_2. eauto. + eapply eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. + intros [rs' [A [B C]]]. + exists rs'; split. eauto. split. auto. apply agree_exten with rs; auto. +Qed. + +(** Translation of condition operators *) + +Remark add_carry_eq0: + forall i, + Vint (Int.add (Int.add (Int.sub Int.zero i) i) + (Int.add_carry Int.zero (Int.xor i Int.mone) Int.one)) = + Val.of_bool (Int.eq i Int.zero). +Proof. + intros. rewrite <- Int.sub_add_l. rewrite Int.add_zero_l. + rewrite Int.sub_idem. rewrite Int.add_zero_l. fold (Int.not i). + predSpec Int.eq Int.eq_spec i Int.zero. + subst i. reflexivity. + unfold Val.of_bool, Vfalse. decEq. + unfold Int.add_carry. rewrite Int.unsigned_zero. rewrite Int.unsigned_one. + apply zlt_true. + generalize (Int.unsigned_range (Int.not i)); intro. + assert (Int.unsigned (Int.not i) <> Int.modulus - 1). + red; intros. + assert (Int.repr (Int.unsigned (Int.not i)) = Int.mone). + rewrite H1. apply Int.mkint_eq. reflexivity. + rewrite Int.repr_unsigned in H2. + assert (Int.not (Int.not i) = Int.zero). + rewrite H2. apply Int.mkint_eq; reflexivity. + rewrite Int.not_involutive in H3. + congruence. + omega. +Qed. + +Remark add_carry_ne0: + forall i, + Vint (Int.add (Int.add i (Int.xor (Int.add i Int.mone) Int.mone)) + (Int.add_carry i Int.mone Int.zero)) = + Val.of_bool (negb (Int.eq i Int.zero)). +Proof. + intros. fold (Int.not (Int.add i Int.mone)). rewrite Int.not_neg. + rewrite (Int.add_commut (Int.neg (Int.add i Int.mone))). + rewrite <- Int.sub_add_opp. rewrite Int.sub_add_r. rewrite Int.sub_idem. + rewrite Int.add_zero_l. rewrite Int.add_neg_zero. rewrite Int.add_zero_l. + unfold Int.add_carry, Int.eq. + rewrite Int.unsigned_zero. rewrite Int.unsigned_mone. + unfold negb, Val.of_bool, Vtrue, Vfalse. + destruct (zeq (Int.unsigned i) 0); decEq. + apply zlt_true. omega. + apply zlt_false. generalize (Int.unsigned_range i). omega. +Qed. + +Lemma transl_cond_op_correct: + forall cond args r k rs m b, + mreg_type r = Tint -> + map mreg_type args = type_of_condition cond -> + eval_condition cond (map rs (map preg_of args)) m = Some b -> + exists rs', + exec_straight (transl_cond_op cond args r k) rs m k rs' m + /\ rs'#(ireg_of r) = Val.of_bool b + /\ forall r', is_data_reg r' = true -> r' <> ireg_of r -> rs'#r' = rs#r'. +Proof. + intros until args. unfold transl_cond_op. + destruct (classify_condition cond args); + intros until b; intros TY1 TY2 EV; simpl in TY2. +(* eq 0 *) + inv TY2. simpl in EV. unfold preg_of in *; rewrite H0 in *. + econstructor; split. + eapply exec_straight_two; simpl; reflexivity. + split. repeat SIMP. destruct (rs (ireg_of r)); inv EV. simpl. + apply add_carry_eq0. + intros; repeat SIMP. +(* ne 0 *) + inv TY2. simpl in EV. unfold preg_of in *; rewrite H0 in *. + econstructor; split. + eapply exec_straight_two; simpl; reflexivity. + split. repeat SIMP. rewrite gpr_or_zero_not_zero; auto with ppcgen. + destruct (rs (ireg_of r)); inv EV. simpl. + apply add_carry_ne0. + intros; repeat SIMP. +(* ge 0 *) + inv TY2. simpl in EV. unfold preg_of in *; rewrite H0 in *. + econstructor; split. + eapply exec_straight_two; simpl; reflexivity. + split. repeat SIMP. rewrite Val.rolm_ge_zero. + destruct (rs (ireg_of r)); simpl; congruence. + intros; repeat SIMP. +(* lt 0 *) + inv TY2. simpl in EV. unfold preg_of in *; rewrite H0 in *. + econstructor; split. + apply exec_straight_one; simpl; reflexivity. + split. repeat SIMP. rewrite Val.rolm_lt_zero. + destruct (rs (ireg_of r)); simpl; congruence. + intros; repeat SIMP. +(* default *) + set (bit := fst (crbit_for_cond c)). + set (isset := snd (crbit_for_cond c)). + set (k1 := + Pmfcrbit (ireg_of r) bit :: + (if isset + then k + else Pxori (ireg_of r) (ireg_of r) (Cint Int.one) :: k)). + generalize (transl_cond_correct_2 c rl k1 rs m b TY2 EV). + fold bit; fold isset. + intros [rs1 [EX1 [RES1 AG1]]]. + destruct isset. + (* bit set *) + econstructor; split. eapply exec_straight_trans. eexact EX1. + unfold k1. apply exec_straight_one; simpl; reflexivity. + split. repeat SIMP. intros; repeat SIMP. + (* bit clear *) + econstructor; split. eapply exec_straight_trans. eexact EX1. + unfold k1. eapply exec_straight_two; simpl; reflexivity. + split. repeat SIMP. rewrite RES1. destruct b; compute; reflexivity. + intros; repeat SIMP. Qed. (** Translation of arithmetic operations. *) @@ -1167,255 +1207,143 @@ Qed. Ltac TranslOpSimpl := econstructor; split; [ apply exec_straight_one; [simpl; eauto | reflexivity] - | auto 7 with ppcgen; fail ]. -(* - match goal with - | H: (Val.lessdef ?v ?v') |- - exists rs' : regset, - exec_straight ?c ?rs ?m ?k rs' ?m /\ - agree (Regmap.set ?res ?v ?ms) ?sp rs' => - - (exists (nextinstr (rs#(ireg_of res) <- v')); - split; - [ apply exec_straight_one; auto; fail - | auto with ppcgen ]) - || - (exists (nextinstr (rs#(freg_of res) <- v')); - split; - [ apply exec_straight_one; auto; fail - | auto with ppcgen ]) - end. -*) + | split; intros; (repeat SIMP; fail) ]. -Lemma transl_op_correct: - forall op args res k ms sp rs m v m', +Lemma transl_op_correct_aux: + forall op args res k (rs: regset) m v, wt_instr (Mop op args res) -> - agree ms sp rs -> - eval_operation ge sp op (map ms args) m = Some v -> - Mem.extends m m' -> + eval_operation ge (rs#GPR1) op (map rs (map preg_of args)) m = Some v -> exists rs', - exec_straight (transl_op op args res k) rs m' k rs' m' - /\ agree (Regmap.set res v (undef_op op ms)) sp rs'. + exec_straight (transl_op op args res k) rs m k rs' m + /\ rs'#(preg_of res) = v + /\ forall r, + match op with Omove => is_data_reg r = true | _ => is_nontemp_reg r = true end -> + r <> preg_of res -> rs'#r = rs#r. Proof. intros. - assert (exists v', Val.lessdef v v' /\ - eval_operation_total ge sp op (map rs (map preg_of args)) = v'). - exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eauto. - intros [v' [A B]]. exists v'; split; auto. - eapply eval_operation_weaken; eauto. - destruct H3 as [v' [LD EQ]]. clear H1 H2. + exploit eval_operation_weaken; eauto. intro EV. inv H. (* Omove *) simpl in *. exists (nextinstr (rs#(preg_of res) <- (rs#(preg_of r1)))). split. unfold preg_of. rewrite <- H2. destruct (mreg_type r1); apply exec_straight_one; auto. - auto with ppcgen. + split. repeat SIMP. intros; repeat SIMP. (* Other instructions *) destruct op; simpl; simpl in H5; injection H5; clear H5; intros; TypeInv; simpl in *; UseTypeInfo; try (TranslOpSimpl). (* Omove again *) congruence. (* Ointconst *) - destruct (loadimm_correct (ireg_of res) i k rs m') - as [rs' [A [B C]]]. - exists rs'. split. auto. - rewrite <- B in LD. eauto with ppcgen. - (* Ofloatconst *) - exists (nextinstr (rs #GPR12 <- Vundef #(freg_of res) <- (Vfloat f))). - split. apply exec_straight_one. reflexivity. reflexivity. - apply agree_nextinstr. apply agree_set_mfreg; auto. apply agree_set_mreg; auto. - eapply agree_undef_temps; eauto. - intros. apply Pregmap.gso; auto. + destruct (loadimm_correct (ireg_of res) i k rs m) as [rs' [A [B C]]]. + exists rs'. split. auto. split. auto. auto with ppcgen. (* Oaddrsymbol *) - change (find_symbol_offset ge i i0) with (symbol_offset ge i i0) in LD. + change (find_symbol_offset ge i i0) with (symbol_offset ge i i0) in *. set (v' := symbol_offset ge i i0) in *. caseEq (symbol_is_small_data i i0); intro SD. (* small data *) - exists (nextinstr (rs#(ireg_of res) <- v')); split. - apply exec_straight_one; auto. simpl. + econstructor; split. apply exec_straight_one; simpl; reflexivity. + split. repeat SIMP. rewrite (small_data_area_addressing _ _ _ SD). unfold v', symbol_offset. destruct (Genv.find_symbol ge i); auto. rewrite Int.add_zero; auto. - eauto with ppcgen. + intros; repeat SIMP. (* not small data *) - pose (rs1 := nextinstr (rs#GPR12 <- (high_half v'))). - exists (nextinstr (rs1#(ireg_of res) <- v')). - split. apply exec_straight_two with rs1 m'. - unfold exec_instr. rewrite gpr_or_zero_zero. - unfold const_high. rewrite Val.add_commut. - rewrite high_half_zero. reflexivity. - simpl. rewrite gpr_or_zero_not_zero. 2: congruence. - unfold rs1 at 1. rewrite nextinstr_inv; auto with ppcgen. - rewrite Pregmap.gss. - fold v'. rewrite Val.add_commut. unfold v'. rewrite low_high_half. - reflexivity. reflexivity. reflexivity. - unfold rs1. apply agree_nextinstr. apply agree_set_mireg; auto. - apply agree_set_mreg; auto. apply agree_nextinstr. - eapply agree_undef_temps; eauto. - intros. apply Pregmap.gso; auto. +Opaque Val.add. + econstructor; split. eapply exec_straight_two; simpl; reflexivity. + split. repeat SIMP. rewrite gpr_or_zero_zero. + rewrite gpr_or_zero_not_zero; auto with ppcgen. repeat SIMP. + rewrite (Val.add_commut Vzero). rewrite high_half_zero. + rewrite Val.add_commut. rewrite low_high_half. auto. + intros; repeat SIMP. (* Oaddrstack *) - assert (GPR1 <> GPR0). discriminate. - generalize (addimm_correct (ireg_of res) GPR1 i k rs m' (ireg_of_not_GPR0 res) H1). - intros [rs' [EX [RES OTH]]]. - exists rs'. split. auto. - apply agree_set_mireg_exten with rs; auto with ppcgen. - rewrite (sp_val ms sp rs) in LD; auto. rewrite RES; auto. + destruct (addimm_correct (ireg_of res) GPR1 i k rs m) as [rs' [EX [RES OTH]]]. + auto with ppcgen. congruence. + exists rs'; auto with ppcgen. (* Ocast8unsigned *) - econstructor; split. - apply exec_straight_one. simpl; reflexivity. reflexivity. - replace (Val.zero_ext 8 (rs (ireg_of m0))) - with (Val.rolm (rs (ireg_of m0)) Int.zero (Int.repr 255)) in LD. - auto with ppcgen. - unfold Val.rolm, Val.zero_ext. destruct (rs (ireg_of m0)); auto. + econstructor; split. apply exec_straight_one; simpl; reflexivity. + split. repeat SIMP. + destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.rolm_zero. rewrite Int.zero_ext_and. auto. compute; auto. + intros; repeat SIMP. (* Ocast16unsigned *) - econstructor; split. - apply exec_straight_one. simpl; reflexivity. reflexivity. - replace (Val.zero_ext 16 (rs (ireg_of m0))) - with (Val.rolm (rs (ireg_of m0)) Int.zero (Int.repr 65535)) in LD. - auto with ppcgen. - unfold Val.rolm, Val.zero_ext. destruct (rs (ireg_of m0)); auto. + econstructor; split. apply exec_straight_one; simpl; reflexivity. + split. repeat SIMP. + destruct (rs (ireg_of m0)); simpl; auto. rewrite Int.rolm_zero. rewrite Int.zero_ext_and. auto. compute; auto. + intros; repeat SIMP. (* Oaddimm *) - generalize (addimm_correct (ireg_of res) (ireg_of m0) i k rs m' - (ireg_of_not_GPR0 res) (ireg_of_not_GPR0 m0)). - intros [rs' [A [B C]]]. - exists rs'. split. auto. - rewrite <- B in LD. eauto with ppcgen. + destruct (addimm_correct (ireg_of res) (ireg_of m0) i k rs m) as [rs' [A [B C]]]; auto with ppcgen. + exists rs'; auto with ppcgen. (* Osubimm *) case (Int.eq (high_s i) Int.zero). + TranslOpSimpl. + destruct (loadimm_correct GPR0 i (Psubfc (ireg_of res) (ireg_of m0) GPR0 :: k) rs m) as [rs1 [EX [RES OTH]]]. econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - auto 7 with ppcgen. - generalize (loadimm_correct GPR0 i (Psubfc (ireg_of res) (ireg_of m0) GPR0 :: k) rs m'). - intros [rs1 [EX [RES OTH]]]. - econstructor; split. - eapply exec_straight_trans. eexact EX. - apply exec_straight_one. simpl; eauto. auto. - rewrite RES. rewrite OTH; auto with ppcgen. - assert (agree (undef_temps ms) sp rs1). eauto with ppcgen. - auto with ppcgen. decEq; auto with ppcgen. + eapply exec_straight_trans. eexact EX. apply exec_straight_one; simpl; reflexivity. + split. repeat SIMP. rewrite RES. rewrite OTH; auto with ppcgen. + intros; repeat SIMP. (* Omulimm *) case (Int.eq (high_s i) Int.zero). + TranslOpSimpl. + destruct (loadimm_correct GPR0 i (Pmullw (ireg_of res) (ireg_of m0) GPR0 :: k) rs m) as [rs1 [EX [RES OTH]]]. econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - auto with ppcgen. - generalize (loadimm_correct GPR0 i (Pmullw (ireg_of res) (ireg_of m0) GPR0 :: k) rs m'). - intros [rs1 [EX [RES OTH]]]. - assert (agree (undef_temps ms) sp rs1). eauto with ppcgen. - econstructor; split. - eapply exec_straight_trans. eexact EX. - apply exec_straight_one. simpl; eauto. auto. - rewrite RES. rewrite OTH; auto with ppcgen. decEq; auto with ppcgen. + eapply exec_straight_trans. eexact EX. apply exec_straight_one; simpl; reflexivity. + split. repeat SIMP. rewrite RES. rewrite OTH; auto with ppcgen. + intros; repeat SIMP. (* Oand *) set (v' := Val.and (rs (ireg_of m0)) (rs (ireg_of m1))) in *. pose (rs1 := rs#(ireg_of res) <- v'). generalize (compare_sint_spec rs1 v' Vzero). intros [A [B [C D]]]. - exists (nextinstr (compare_sint rs1 v' Vzero)). - split. apply exec_straight_one. auto. auto. - apply agree_exten_2 with rs1. unfold rs1; auto with ppcgen. - auto. + econstructor; split. apply exec_straight_one; simpl; reflexivity. + split. rewrite D; auto with ppcgen. unfold rs1. SIMP. + intros. rewrite D; auto with ppcgen. unfold rs1. SIMP. (* Oandimm *) - generalize (andimm_correct (ireg_of res) (ireg_of m0) i k rs m' - (ireg_of_not_GPR0 m0)). - intros [rs' [A [B [C D]]]]. - exists rs'. split. auto. rewrite <- B in LD. eauto with ppcgen. + destruct (andimm_correct (ireg_of res) (ireg_of m0) i k rs m) as [rs' [A [B [C D]]]]; auto with ppcgen. + exists rs'; auto with ppcgen. (* Oorimm *) - generalize (orimm_correct (ireg_of res) (ireg_of m0) i k rs m'). - intros [rs' [A [B C]]]. - exists rs'. split. auto. rewrite <- B in LD. eauto with ppcgen. + destruct (orimm_correct (ireg_of res) (ireg_of m0) i k rs m) as [rs' [A [B C]]]. + exists rs'; auto with ppcgen. (* Oxorimm *) - generalize (xorimm_correct (ireg_of res) (ireg_of m0) i k rs m'). - intros [rs' [A [B C]]]. - exists rs'. split. auto. rewrite <- B in LD. eauto with ppcgen. - (* Oxhrximm *) - pose (rs1 := nextinstr (rs#(ireg_of res) <- (Val.shr (rs (ireg_of m0)) (Vint i)) #CARRY <- (Val.shr_carry (rs (ireg_of m0)) (Vint i)))). - exists (nextinstr (rs1#(ireg_of res) <- (Val.shrx (rs (ireg_of m0)) (Vint i)))). - split. apply exec_straight_two with rs1 m'. - auto. simpl. decEq. decEq. decEq. - unfold rs1. repeat (rewrite nextinstr_inv; try discriminate). - rewrite Pregmap.gss. rewrite Pregmap.gso. rewrite Pregmap.gss. - apply Val.shrx_carry. auto with ppcgen. auto. auto. - apply agree_nextinstr. unfold rs1. apply agree_nextinstr_commut. - apply agree_set_commut. auto with ppcgen. - apply agree_set_other. apply agree_set_mireg_twice; auto with ppcgen. - compute; auto. auto with ppcgen. + destruct (xorimm_correct (ireg_of res) (ireg_of m0) i k rs m) as [rs' [A [B C]]]. + exists rs'; auto with ppcgen. + (* Oshrximm *) + econstructor; split. + eapply exec_straight_two; simpl; reflexivity. + split. repeat SIMP. apply Val.shrx_carry. + intros; repeat SIMP. (* Oroli *) destruct (mreg_eq m0 res). subst m0. TranslOpSimpl. econstructor; split. - eapply exec_straight_three. - simpl. reflexivity. - simpl. reflexivity. - simpl. reflexivity. - auto. auto. auto. - set (rs1 := nextinstr (rs # GPR0 <- (rs (ireg_of m0)))). - set (rs2 := nextinstr (rs1 # GPR0 <- - (Val.or (Val.and (rs1 GPR0) (Vint (Int.not i0))) - (Val.rolm (rs1 (ireg_of m1)) i i0)))). - apply agree_nextinstr. apply agree_set_mireg; auto. apply agree_set_mreg. - apply agree_undef_temps with rs. auto. - intros. unfold rs2. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. - unfold rs1. rewrite nextinstr_inv; auto. rewrite Pregmap.gso; auto. - unfold rs2. rewrite nextinstr_inv; auto with ppcgen. rewrite Pregmap.gss. - unfold rs1. repeat rewrite nextinstr_inv; auto with ppcgen. - rewrite Pregmap.gss. rewrite Pregmap.gso; auto with ppcgen. decEq. auto with ppcgen. - (* Ointoffloat *) - econstructor; split. - apply exec_straight_one. simpl; eauto. auto. - apply agree_nextinstr. apply agree_set_mireg; auto. apply agree_set_mreg; auto. - apply agree_undef_temps with rs; auto. intros. - repeat rewrite Pregmap.gso; auto. + eapply exec_straight_three; simpl; reflexivity. + split. repeat SIMP. intros; repeat SIMP. (* Ocmp *) - revert H1 LD; case (classify_condition c args); intros. - (* Optimization: compimm Cge 0 *) - subst n. simpl in *. inv H1. UseTypeInfo. - set (rs1 := nextinstr (rs#(ireg_of res) <- (Val.rolm (rs (ireg_of r)) Int.one Int.one))). - set (rs2 := nextinstr (rs1#(ireg_of res) <- (Val.xor (rs1#(ireg_of res)) (Vint Int.one)))). - exists rs2. - split. apply exec_straight_two with rs1 m'; auto. - rewrite <- Val.rolm_ge_zero in LD. - unfold rs2. apply agree_nextinstr. - unfold rs1. apply agree_nextinstr_commut. fold rs1. - replace (rs1 (ireg_of res)) with (Val.rolm (rs (ireg_of r)) Int.one Int.one). - apply agree_set_mireg_twice; auto with ppcgen. - unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss. auto. - auto with ppcgen. auto with ppcgen. - (* Optimization: compimm Clt 0 *) - subst n. simpl in *. inv H1. UseTypeInfo. - exists (nextinstr (rs#(ireg_of res) <- (Val.rolm (rs (ireg_of r)) Int.one Int.one))). - split. apply exec_straight_one; auto. - rewrite <- Val.rolm_lt_zero in LD. - auto with ppcgen. - (* General case *) - set (bit := fst (crbit_for_cond c0)). - set (isset := snd (crbit_for_cond c0)). - set (k1 := - Pmfcrbit (ireg_of res) bit :: - (if isset - then k - else Pxori (ireg_of res) (ireg_of res) (Cint Int.one) :: k)). - generalize (transl_cond_correct_aux c0 rl k1 ms sp rs m' H1 H0). - fold bit; fold isset. - intros [rs1 [EX1 [RES1 AG1]]]. - set (rs2 := nextinstr (rs1#(ireg_of res) <- (rs1#(reg_of_crbit bit)))). - destruct isset. - exists rs2. - split. apply exec_straight_trans with k1 rs1 m'. assumption. - unfold k1. apply exec_straight_one. - reflexivity. reflexivity. - unfold rs2. rewrite RES1. auto with ppcgen. - econstructor. - split. apply exec_straight_trans with k1 rs1 m'. assumption. - unfold k1. apply exec_straight_two with rs2 m'. - reflexivity. simpl. eauto. auto. auto. - apply agree_nextinstr. - unfold rs2 at 1. rewrite nextinstr_inv. rewrite Pregmap.gss. - rewrite RES1. rewrite <- Val.notbool_xor. - unfold rs2. auto 7 with ppcgen. - apply eval_condition_total_is_bool. - auto with ppcgen. + destruct (eval_condition c rs ## (preg_of ## args) m) as [ b | ] _eqn; try discriminate. + destruct (transl_cond_op_correct c args res k rs m b) as [rs' [A [B C]]]; auto. + exists rs'; intuition auto with ppcgen. + rewrite B. destruct b; inv H0; auto. +Qed. + +Lemma transl_op_correct: + forall op args res k ms sp rs m v m', + wt_instr (Mop op args res) -> + agree ms sp rs -> + eval_operation ge sp op (map ms args) m = Some v -> + Mem.extends m m' -> + exists rs', + exec_straight (transl_op op args res k) rs m' k rs' m' + /\ agree (Regmap.set res v (undef_op op ms)) sp rs'. +Proof. + intros. + exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eauto. + intros [v' [A B]]. rewrite (sp_val _ _ _ H0) in A. + exploit transl_op_correct_aux; eauto. intros [rs' [P [Q R]]]. + rewrite <- Q in B. + exists rs'; split. eexact P. + unfold undef_op. destruct op; + (apply agree_set_mreg_undef_temps with rs || apply agree_set_mreg with rs); + auto. Qed. Lemma transl_load_store_correct: @@ -1452,10 +1380,10 @@ Proof. set (rs1 := nextinstr (rs#temp <- (Val.add (rs (ireg_of m0)) (Vint (Int.shl (high_s i) (Int.repr 16)))))). exploit (H (Cint (low_s i)) temp rs1 k). simpl. UseTypeInfo. rewrite gpr_or_zero_not_zero; auto. - unfold rs1. rewrite nextinstr_inv. rewrite Pregmap.gss. - rewrite Val.add_assoc. simpl. rewrite low_high_s. auto. - discriminate. - intros. unfold rs1. rewrite nextinstr_inv; auto. apply Pregmap.gso; auto. + unfold rs1; repeat SIMP. rewrite Val.add_assoc. +Transparent Val.add. + simpl. rewrite low_high_s. auto. + intros; unfold rs1; repeat SIMP. intros [rs' [EX' AG']]. exists rs'. split. apply exec_straight_step with rs1 m. simpl. rewrite gpr_or_zero_not_zero; auto with ppcgen. auto. @@ -1552,15 +1480,21 @@ Proof. (* mk1 *) intros. exists (nextinstr (rs1#(preg_of dst) <- v')). split. apply exec_straight_one. rewrite H. - unfold load1. rewrite <- H6. rewrite C. auto. - auto with ppcgen. - eauto with ppcgen. + unfold load1. rewrite <- H6. rewrite C. auto. + unfold nextinstr. SIMP. decEq. SIMP. apply sym_not_equal; auto with ppcgen. + apply agree_set_mreg with rs1. + apply agree_undef_temps with rs; auto with ppcgen. + repeat SIMP. + intros; repeat SIMP. (* mk2 *) intros. exists (nextinstr (rs#(preg_of dst) <- v')). split. apply exec_straight_one. rewrite H0. unfold load2. rewrite <- H6. rewrite C. auto. - auto with ppcgen. - eauto with ppcgen. + unfold nextinstr. SIMP. decEq. SIMP. apply sym_not_equal; auto with ppcgen. + apply agree_set_mreg with rs. + apply agree_undef_temps with rs; auto with ppcgen. + repeat SIMP. + intros; repeat SIMP. (* not GPR0 *) congruence. Qed. @@ -1611,9 +1545,9 @@ Proof. intros [rs3 [U V]]. exists rs3; split. apply exec_straight_one. auto. rewrite V; auto with ppcgen. - eapply agree_undef_temps; eauto. intros. - rewrite V; auto. rewrite nextinstr_inv; auto. apply H7; auto. - unfold int_temp_for. destruct (mreg_eq src IT2); auto. + apply agree_undef_temps with rs. auto. + intros. rewrite V; auto with ppcgen. SIMP. apply H7; auto with ppcgen. + unfold int_temp_for. destruct (mreg_eq src IT2); auto with ppcgen. (* mk2 *) intros. exploit (H0 r1 r2 rs (nextinstr rs) m1'). @@ -1622,7 +1556,7 @@ Proof. exists rs3; split. apply exec_straight_one. auto. rewrite V; auto with ppcgen. eapply agree_undef_temps; eauto. intros. - rewrite V; auto. rewrite nextinstr_inv; auto. + rewrite V; auto with ppcgen. unfold int_temp_for. destruct (mreg_eq src IT2); congruence. Qed. diff --git a/powerpc/Asmgenretaddr.v b/powerpc/Asmgenretaddr.v index 5b1f7d53..adc15297 100644 --- a/powerpc/Asmgenretaddr.v +++ b/powerpc/Asmgenretaddr.v @@ -147,11 +147,18 @@ Lemma transl_cond_tail: Proof. unfold transl_cond; intros; destruct cond; IsTail. Qed. Hint Resolve transl_cond_tail: ppcretaddr. +Lemma transl_cond_op_tail: + forall cond args r k, is_tail k (transl_cond_op cond args r k). +Proof. + unfold transl_cond_op; intros. + destruct (classify_condition cond args); IsTail. +Qed. +Hint Resolve transl_cond_op_tail: ppcretaddr. + Lemma transl_op_tail: forall op args r k, is_tail k (transl_op op args r k). Proof. unfold transl_op; intros; destruct op; IsTail. - destruct (classify_condition c args); IsTail. Qed. Hint Resolve transl_op_tail: ppcretaddr. diff --git a/powerpc/PrintAsm.ml b/powerpc/PrintAsm.ml index eacf1dd0..efe5b987 100644 --- a/powerpc/PrintAsm.ml +++ b/powerpc/PrintAsm.ml @@ -504,8 +504,12 @@ let jumptables : (int * label list) list ref = ref [] let print_instruction oc = function | Padd(r1, r2, r3) -> fprintf oc " add %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Padde(r1, r2, r3) -> + fprintf oc " adde %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Paddi(r1, r2, c) -> fprintf oc " addi %a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c + | Paddic(r1, r2, c) -> + fprintf oc " addic %a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c | Paddis(r1, r2, c) -> fprintf oc " addis %a, %a, %a\n" ireg r1 ireg_or_zero r2 constant c | Paddze(r1, r2) -> @@ -724,6 +728,8 @@ let print_instruction oc = function fprintf oc " stwx %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Psubfc(r1, r2, r3) -> fprintf oc " subfc %a, %a, %a\n" ireg r1 ireg r2 ireg r3 + | Psubfe(r1, r2, r3) -> + fprintf oc " subfe %a, %a, %a\n" ireg r1 ireg r2 ireg r3 | Psubfic(r1, r2, c) -> fprintf oc " subfic %a, %a, %a\n" ireg r1 ireg r2 constant c | Pxor(r1, r2, r3) -> -- cgit