From 353b3cee4d08b5820bf62b7228afb67be69f10e6 Mon Sep 17 00:00:00 2001 From: xleroy Date: Mon, 4 Mar 2013 15:28:28 +0000 Subject: Finished backtracking (cf previous commit) for ARM and PowerPC. ARM: slightly shorter code generated for indirect memory accesses. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2137 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- Changelog | 3 +- arm/Asmgen.v | 167 ++++++++-------- arm/Asmgenproof.v | 464 ++++++++++++++++++++----------------------- arm/Asmgenproof1.v | 183 +++++++---------- backend/Asmgenproof0.v | 27 +-- ia32/Asmgenproof.v | 45 +---- powerpc/Asmgenproof.v | 519 +++++++++++++++++++++---------------------------- 7 files changed, 593 insertions(+), 815 deletions(-) diff --git a/Changelog b/Changelog index 431f8ba..670a6d0 100644 --- a/Changelog +++ b/Changelog @@ -15,7 +15,8 @@ Development version generated in the assembly file. - ARM and PowerPC ports: more efficient access to function parameters that are passed on the call stack. - +- ARM port; slightly better code generated for some indirect memory + accesses. Release 1.12.1, 2013-01-29 ========================== diff --git a/arm/Asmgen.v b/arm/Asmgen.v index 562cf22..c7d7712 100644 --- a/arm/Asmgen.v +++ b/arm/Asmgen.v @@ -54,14 +54,23 @@ Definition is_immed_arith (x: int) : bool := Definition is_immed_mem_word (x: int) : bool := Int.lt x (Int.repr 4096) && Int.lt (Int.repr (-4096)) x. + +Definition mk_immed_mem_word (x: int) : int := + Int.sign_ext 13 x. Definition is_immed_mem_small (x: int) : bool := Int.lt x (Int.repr 256) && Int.lt (Int.repr (-256)) x. +Definition mk_immed_mem_small (x: int) : int := + Int.sign_ext 9 x. + Definition is_immed_mem_float (x: int) : bool := Int.eq (Int.and x (Int.repr 3)) Int.zero && Int.lt x (Int.repr 1024) && Int.lt (Int.repr (-1024)) x. +Definition mk_immed_mem_float (x: int) : int := + Int.and (Int.sign_ext 11 x) (Int.repr 4294967288). (**r 0xfffffff8 *) + (** Decomposition of a 32-bit integer into a list of immediate arguments, whose sum or "or" or "xor" equals the integer. *) @@ -390,7 +399,42 @@ Definition transl_op Error(msg "Asmgen.transl_op") end. -(** Translation of memory accesses: loads and stores. *) +(** Accessing data in the stack frame. *) + +Definition indexed_memory_access + (mk_instr: ireg -> int -> instruction) + (mk_immed: int -> int) + (base: ireg) (n: int) (k: code) := + let n1 := mk_immed n in + if Int.eq n n1 + then mk_instr base n :: k + else addimm IR14 base (Int.sub n n1) (mk_instr IR14 n1 :: k). + +Definition loadind_int (base: ireg) (ofs: int) (dst: ireg) (k: code) := + indexed_memory_access (fun base n => Pldr dst base (SAimm n)) mk_immed_mem_word base ofs k. + +Definition loadind_float (base: ireg) (ofs: int) (dst: freg) (k: code) := + indexed_memory_access (Pfldd dst) mk_immed_mem_float base ofs k. + +Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) := + match ty with + | Tint => do r <- ireg_of dst; OK (loadind_int base ofs r k) + | Tfloat => do r <- freg_of dst; OK (loadind_float base ofs r k) + end. + +Definition storeind_int (src: ireg) (base: ireg) (ofs: int) (k: code) := + indexed_memory_access (fun base n => Pstr src base (SAimm n)) mk_immed_mem_word base ofs k. + +Definition storeind_float (src: freg) (base: ireg) (ofs: int) (k: code) := + indexed_memory_access (Pfstd src) mk_immed_mem_float base ofs k. + +Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) := + match ty with + | Tint => do r <- ireg_of src; OK (storeind_int r base ofs k) + | Tfloat => do r <- freg_of src; OK (storeind_float r base ofs k) + end. + +(** Translation of memory accesses *) Definition transl_shift_addr (s: shift) (r: ireg) : shift_addr := match s with @@ -403,141 +447,90 @@ Definition transl_shift_addr (s: shift) (r: ireg) : shift_addr := Definition transl_memory_access (mk_instr_imm: ireg -> int -> instruction) (mk_instr_gen: option (ireg -> shift_addr -> instruction)) - (is_immed: int -> bool) + (mk_immed: int -> int) (addr: addressing) (args: list mreg) (k: code) := match addr, args with | Aindexed n, a1 :: nil => do r1 <- ireg_of a1; - OK (if is_immed n then - mk_instr_imm r1 n :: k - else - addimm IR14 r1 n - (mk_instr_imm IR14 Int.zero :: k)) + OK (indexed_memory_access mk_instr_imm mk_immed r1 n k) | Aindexed2, a1 :: a2 :: nil => - do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (match mk_instr_gen with - | Some f => - f r1 (SAreg r2) :: k - | None => - Padd IR14 r1 (SOreg r2) :: - mk_instr_imm IR14 Int.zero :: k - end) + match mk_instr_gen with + | Some f => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (f r1 (SAreg r2) :: k) + | None => + Error (msg "Asmgen.Aindexed2") + end | Aindexed2shift s, a1 :: a2 :: nil => - do r1 <- ireg_of a1; do r2 <- ireg_of a2; - OK (match mk_instr_gen with - | Some f => - f r1 (transl_shift_addr s r2) :: k - | None => - Padd IR14 r1 (transl_shift s r2) :: - mk_instr_imm IR14 Int.zero :: k - end) + match mk_instr_gen with + | Some f => + do r1 <- ireg_of a1; do r2 <- ireg_of a2; + OK (f r1 (transl_shift_addr s r2) :: k) + | None => + Error (msg "Asmgen.Aindexed2shift") + end | Ainstack n, nil => - OK (if is_immed n then - mk_instr_imm IR13 n :: k - else - addimm IR14 IR13 n (mk_instr_imm IR14 Int.zero :: k)) + OK (indexed_memory_access mk_instr_imm mk_immed IR13 n k) | _, _ => Error(msg "Asmgen.transl_memory_access") end. Definition transl_memory_access_int (mk_instr: ireg -> ireg -> shift_addr -> instruction) - (is_immed: int -> bool) + (mk_immed: int -> int) (dst: mreg) (addr: addressing) (args: list mreg) (k: code) := do rd <- ireg_of dst; transl_memory_access (fun r n => mk_instr rd r (SAimm n)) (Some (mk_instr rd)) - is_immed addr args k. + mk_immed addr args k. Definition transl_memory_access_float (mk_instr: freg -> ireg -> int -> instruction) - (is_immed: int -> bool) + (mk_immed: int -> int) (dst: mreg) (addr: addressing) (args: list mreg) (k: code) := do rd <- freg_of dst; transl_memory_access (mk_instr rd) None - is_immed addr args k. + mk_immed addr args k. Definition transl_load (chunk: memory_chunk) (addr: addressing) (args: list mreg) (dst: mreg) (k: code) := match chunk with | Mint8signed => - transl_memory_access_int Pldrsb is_immed_mem_small dst addr args k + transl_memory_access_int Pldrsb mk_immed_mem_small dst addr args k | Mint8unsigned => - transl_memory_access_int Pldrb is_immed_mem_word dst addr args k + transl_memory_access_int Pldrb mk_immed_mem_word dst addr args k | Mint16signed => - transl_memory_access_int Pldrsh is_immed_mem_small dst addr args k + transl_memory_access_int Pldrsh mk_immed_mem_small dst addr args k | Mint16unsigned => - transl_memory_access_int Pldrh is_immed_mem_small dst addr args k + transl_memory_access_int Pldrh mk_immed_mem_small dst addr args k | Mint32 => - transl_memory_access_int Pldr is_immed_mem_word dst addr args k + transl_memory_access_int Pldr mk_immed_mem_word dst addr args k | Mfloat32 => - transl_memory_access_float Pflds is_immed_mem_float dst addr args k + transl_memory_access_float Pflds mk_immed_mem_float dst addr args k | Mfloat64 | Mfloat64al32 => - transl_memory_access_float Pfldd is_immed_mem_float dst addr args k + transl_memory_access_float Pfldd mk_immed_mem_float dst addr args k end. Definition transl_store (chunk: memory_chunk) (addr: addressing) (args: list mreg) (src: mreg) (k: code) := match chunk with | Mint8signed => - transl_memory_access_int Pstrb is_immed_mem_small src addr args k + transl_memory_access_int Pstrb mk_immed_mem_small src addr args k | Mint8unsigned => - transl_memory_access_int Pstrb is_immed_mem_word src addr args k + transl_memory_access_int Pstrb mk_immed_mem_word src addr args k | Mint16signed => - transl_memory_access_int Pstrh is_immed_mem_small src addr args k + transl_memory_access_int Pstrh mk_immed_mem_small src addr args k | Mint16unsigned => - transl_memory_access_int Pstrh is_immed_mem_small src addr args k + transl_memory_access_int Pstrh mk_immed_mem_small src addr args k | Mint32 => - transl_memory_access_int Pstr is_immed_mem_word src addr args k + transl_memory_access_int Pstr mk_immed_mem_word src addr args k | Mfloat32 => - transl_memory_access_float Pfsts is_immed_mem_float src addr args k + transl_memory_access_float Pfsts mk_immed_mem_float src addr args k | Mfloat64 | Mfloat64al32 => - transl_memory_access_float Pfstd is_immed_mem_float src addr args k - end. - -(** Accessing data in the stack frame. *) - -Definition loadind_int (base: ireg) (ofs: int) (dst: ireg) (k: code) := - if is_immed_mem_word ofs then - Pldr dst base (SAimm ofs) :: k - else - addimm IR14 base ofs - (Pldr dst IR14 (SAimm Int.zero) :: k). - -Definition loadind_float (base: ireg) (ofs: int) (dst: freg) (k: code) := - if is_immed_mem_float ofs then - Pfldd dst base ofs :: k - else - addimm IR14 base ofs - (Pfldd dst IR14 Int.zero :: k). - -Definition loadind (base: ireg) (ofs: int) (ty: typ) (dst: mreg) (k: code) := - match ty with - | Tint => do r <- ireg_of dst; OK (loadind_int base ofs r k) - | Tfloat => do r <- freg_of dst; OK (loadind_float base ofs r k) - end. - -Definition storeind_int (src: ireg) (base: ireg) (ofs: int) (k: code) := - if is_immed_mem_word ofs then - Pstr src base (SAimm ofs) :: k - else - addimm IR14 base ofs - (Pstr src IR14 (SAimm Int.zero) :: k). - -Definition storeind_float (src: freg) (base: ireg) (ofs: int) (k: code) := - if is_immed_mem_float ofs then - Pfstd src base ofs :: k - else - addimm IR14 base ofs - (Pfstd src IR14 Int.zero :: k). - -Definition storeind (src: mreg) (base: ireg) (ofs: int) (ty: typ) (k: code) := - match ty with - | Tint => do r <- ireg_of src; OK (storeind_int r base ofs k) - | Tfloat => do r <- freg_of src; OK (storeind_float r base ofs k) + transl_memory_access_float Pfstd mk_immed_mem_float src addr args k end. (** Translation of arguments to annotations *) diff --git a/arm/Asmgenproof.v b/arm/Asmgenproof.v index 21becf1..dcae740 100644 --- a/arm/Asmgenproof.v +++ b/arm/Asmgenproof.v @@ -85,8 +85,8 @@ Proof. Qed. Lemma exec_straight_exec: - forall f c ep tf tc c' rs m rs' m', - transl_code_at_pc ge (rs PC) f c ep tf tc -> + forall fb f c ep tf tc c' rs m rs' m', + transl_code_at_pc ge (rs PC) fb f c ep tf tc -> exec_straight tge tf tc rs m c' rs' m' -> plus step tge (State rs m) E0 (State rs' m'). Proof. @@ -97,11 +97,11 @@ Proof. Qed. Lemma exec_straight_at: - forall f c ep tf tc c' ep' tc' rs m rs' m', - transl_code_at_pc ge (rs PC) f c ep tf tc -> + forall fb f c ep tf tc c' ep' tc' rs m rs' m', + transl_code_at_pc ge (rs PC) fb f c ep tf tc -> transl_code f c' ep' = OK tc' -> exec_straight tge tf tc rs m tc' rs' m' -> - transl_code_at_pc ge (rs' PC) f c' ep' tf tc'. + transl_code_at_pc ge (rs' PC) fb f c' ep' tf tc'. Proof. intros. inv H. exploit exec_straight_steps_2; eauto. @@ -162,176 +162,166 @@ Qed. Section TRANSL_LABEL. -Variable lbl: label. - Remark iterate_op_label: forall op1 op2 l k, - (forall so, is_label lbl (op1 so) = false) -> - (forall so, is_label lbl (op2 so) = false) -> - find_label lbl (iterate_op op1 op2 l k) = find_label lbl k. + (forall so, nolabel (op1 so)) -> + (forall so, nolabel (op2 so)) -> + tail_nolabel k (iterate_op op1 op2 l k). Proof. intros. unfold iterate_op. destruct l as [ | hd tl]. - simpl. rewrite H. auto. - simpl. rewrite H. - induction tl; simpl. auto. rewrite H0; auto. + TailNoLabel. + TailNoLabel. induction tl; simpl; TailNoLabel. Qed. Hint Resolve iterate_op_label: labels. Remark loadimm_label: - forall r n k, find_label lbl (loadimm r n k) = find_label lbl k. + forall r n k, tail_nolabel k (loadimm r n k). Proof. intros. unfold loadimm. destruct (NPeano.leb (length (decompose_int n)) (length (decompose_int (Int.not n)))); auto with labels. Qed. -Hint Rewrite loadimm_label: labels. +Hint Resolve loadimm_label: labels. Remark addimm_label: - forall r1 r2 n k, find_label lbl (addimm r1 r2 n k) = find_label lbl k. + forall r1 r2 n k, tail_nolabel k (addimm r1 r2 n k). Proof. intros; unfold addimm. destruct (NPeano.leb (length (decompose_int n)) (length (decompose_int (Int.neg n)))); auto with labels. Qed. -Hint Rewrite addimm_label: labels. +Hint Resolve addimm_label: labels. Remark andimm_label: - forall r1 r2 n k, find_label lbl (andimm r1 r2 n k) = find_label lbl k. + forall r1 r2 n k, tail_nolabel k (andimm r1 r2 n k). Proof. intros; unfold andimm. - destruct (is_immed_arith n). reflexivity. auto with labels. + destruct (is_immed_arith n); TailNoLabel. Qed. -Hint Rewrite andimm_label: labels. +Hint Resolve andimm_label: labels. Remark rsubimm_label: - forall r1 r2 n k, find_label lbl (rsubimm r1 r2 n k) = find_label lbl k. + forall r1 r2 n k, tail_nolabel k (rsubimm r1 r2 n k). Proof. intros; unfold rsubimm. auto with labels. Qed. -Hint Rewrite rsubimm_label: labels. +Hint Resolve rsubimm_label: labels. Remark orimm_label: - forall r1 r2 n k, find_label lbl (orimm r1 r2 n k) = find_label lbl k. + forall r1 r2 n k, tail_nolabel k (orimm r1 r2 n k). Proof. intros; unfold orimm. auto with labels. Qed. -Hint Rewrite orimm_label: labels. +Hint Resolve orimm_label: labels. Remark xorimm_label: - forall r1 r2 n k, find_label lbl (xorimm r1 r2 n k) = find_label lbl k. + forall r1 r2 n k, tail_nolabel k (xorimm r1 r2 n k). Proof. intros; unfold xorimm. auto with labels. Qed. -Hint Rewrite xorimm_label: labels. +Hint Resolve xorimm_label: labels. -Remark loadind_int_label: - forall base ofs dst k, find_label lbl (loadind_int base ofs dst k) = find_label lbl k. +Remark indexed_memory_access_label: + forall mk_instr mk_immed base ofs k, + (forall r n, nolabel (mk_instr r n)) -> + tail_nolabel k (indexed_memory_access mk_instr mk_immed base ofs k). Proof. - intros; unfold loadind_int. - destruct (is_immed_mem_word ofs); autorewrite with labels; auto. + intros. unfold indexed_memory_access. + destruct (Int.eq ofs (mk_immed ofs)). + TailNoLabel. + eapply tail_nolabel_trans; TailNoLabel. Qed. +Hint Resolve indexed_memory_access_label. Remark loadind_label: - forall base ofs ty dst k c, loadind base ofs ty dst k = OK c -> find_label lbl c = find_label lbl k. -Proof. - intros. destruct ty; monadInv H. - apply loadind_int_label. - unfold loadind_float. - destruct (is_immed_mem_float ofs); autorewrite with labels; auto. -Qed. - -Remark storeind_int_label: - forall base ofs src k, find_label lbl (storeind_int src base ofs k) = find_label lbl k. + forall base ofs ty dst k c, loadind base ofs ty dst k = OK c -> tail_nolabel k c. Proof. - intros; unfold storeind_int. - destruct (is_immed_mem_word ofs); autorewrite with labels; auto. + intros. destruct ty; monadInv H. + unfold loadind_int; TailNoLabel. + unfold loadind_float; TailNoLabel. Qed. Remark storeind_label: - forall base ofs ty src k c, storeind src base ofs ty k = OK c -> find_label lbl c = find_label lbl k. + forall base ofs ty src k c, storeind src base ofs ty k = OK c -> tail_nolabel k c. Proof. - intros. destruct ty; monadInv H. - apply storeind_int_label. - unfold storeind_float. - destruct (is_immed_mem_float ofs); autorewrite with labels; auto. + intros. destruct ty; monadInv H. + unfold storeind_int; TailNoLabel. + unfold storeind_float; TailNoLabel. Qed. -Hint Rewrite loadind_int_label loadind_label storeind_int_label storeind_label: labels. - -Ltac ArgsInv := - repeat (match goal with - | [ H: Error _ = OK _ |- _ ] => discriminate - | [ H: match ?args with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct args - | [ H: bind _ _ = OK _ |- _ ] => monadInv H - | [ H: assertion _ = OK _ |- _ ] => monadInv H - end). - Remark transl_cond_label: - forall cond args k c, transl_cond cond args k = OK c -> find_label lbl c = find_label lbl k. + forall cond args k c, transl_cond cond args k = OK c -> tail_nolabel k c. Proof. - unfold transl_cond; intros; destruct cond; ArgsInv; auto. - destruct (is_immed_arith i); autorewrite with labels; auto. - destruct (is_immed_arith i); autorewrite with labels; auto. + unfold transl_cond; intros; destruct cond; TailNoLabel. + destruct (is_immed_arith i). TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. + destruct (is_immed_arith i). TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. Qed. Remark transl_op_label: - forall op args r k c, transl_op op args r k = OK c -> find_label lbl c = find_label lbl k. + forall op args r k c, transl_op op args r k = OK c -> tail_nolabel k c. Proof. - unfold transl_op; intros; destruct op; ArgsInv; autorewrite with labels; auto. - destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; auto. - destruct (ireg_eq x x0 || ireg_eq x x1); auto. - simpl. autorewrite with labels; auto. - erewrite transl_cond_label by eauto; auto. +Opaque Int.repr Int.eq. + unfold transl_op; intros; destruct op; TailNoLabel. + destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel. + destruct (ireg_eq x x0 || ireg_eq x x1); TailNoLabel. + eapply tail_nolabel_trans; TailNoLabel. + eapply tail_nolabel_trans. eapply transl_cond_label; eauto. TailNoLabel. Qed. Remark transl_memory_access_label: forall (mk_instr_imm: ireg -> int -> instruction) (mk_instr_gen: option (ireg -> shift_addr -> instruction)) - (is_immed: int -> bool) + (mk_immed: int -> int) (addr: addressing) (args: list mreg) c k, - transl_memory_access mk_instr_imm mk_instr_gen is_immed addr args k = OK c -> - (forall r n, is_label lbl (mk_instr_imm r n) = false) -> + transl_memory_access mk_instr_imm mk_instr_gen mk_immed addr args k = OK c -> + (forall r n, nolabel (mk_instr_imm r n)) -> (match mk_instr_gen with | None => True - | Some f => forall r sa, is_label lbl (f r sa) = false + | Some f => forall r sa, nolabel (f r sa) end) -> - find_label lbl c = find_label lbl k. + tail_nolabel k c. Proof. - unfold transl_memory_access; intros; destruct addr; ArgsInv; auto. - destruct (is_immed i); autorewrite with labels; simpl; rewrite H0; auto. - destruct mk_instr_gen. simpl. rewrite H1. auto. - simpl. rewrite H0. auto. - destruct mk_instr_gen. simpl. rewrite H1. auto. - simpl. rewrite H0. auto. - destruct (is_immed i); inv H; autorewrite with labels; simpl; rewrite H0; auto. + unfold transl_memory_access; intros; destruct addr; TailNoLabel. + destruct mk_instr_gen; TailNoLabel. + destruct mk_instr_gen; TailNoLabel. Qed. Lemma transl_instr_label: forall f i ep k c, transl_instr f i ep k = OK c -> - find_label lbl c = if Mach.is_label lbl i then Some k else find_label lbl k. + match i with Mlabel lbl => c = Plabel lbl :: k | _ => tail_nolabel k c end. Proof. - unfold transl_instr, Mach.is_label; intros. destruct i; try (monadInv H). - eapply loadind_label; eauto. + unfold transl_instr; intros; destruct i; TailNoLabel. + eapply loadind_label; eauto. eapply storeind_label; eauto. - destruct ep; autorewrite with labels; eapply loadind_label; eauto. + destruct ep. eapply loadind_label; eauto. + eapply tail_nolabel_trans. 2: eapply loadind_label; eauto. unfold loadind_int; TailNoLabel. eapply transl_op_label; eauto. - destruct m; simpl in H; monadInv H; eapply transl_memory_access_label; eauto; simpl; auto. - destruct m; simpl in H; monadInv H; eapply transl_memory_access_label; eauto; simpl; auto. - destruct s0; monadInv H; auto. - destruct s0; monadInv H; autorewrite with labels; auto. - auto. - auto. - simpl. auto. - auto. - erewrite transl_cond_label. 2: eauto. auto. - auto. - autorewrite with labels; auto. + unfold transl_load, transl_memory_access_int, transl_memory_access_float in H. + destruct m; monadInv H; eapply transl_memory_access_label; eauto; simpl; auto. + unfold transl_store, transl_memory_access_int, transl_memory_access_float in H. + destruct m; monadInv H; eapply transl_memory_access_label; eauto; simpl; auto. + destruct s0; monadInv H; TailNoLabel. + destruct s0; monadInv H; unfold loadind_int; eapply tail_nolabel_trans. + eapply indexed_memory_access_label; auto with labels. TailNoLabel. + eapply indexed_memory_access_label; auto with labels. TailNoLabel. + eapply tail_nolabel_trans. eapply transl_cond_label; eauto. TailNoLabel. + eapply tail_nolabel_trans. unfold loadind_int. eapply indexed_memory_access_label; auto with labels. TailNoLabel. +Qed. + +Lemma transl_instr_label': + forall lbl f i ep k c, + transl_instr f i ep k = OK c -> + find_label lbl c = if Mach.is_label lbl i then Some k else find_label lbl k. +Proof. + intros. exploit transl_instr_label; eauto. + destruct i; try (intros [A B]; apply B). + intros. subst c. simpl. auto. Qed. Lemma transl_code_label: - forall f c ep tc, + forall lbl f c ep tc, transl_code f c ep = OK tc -> match Mach.find_label lbl c with | None => find_label lbl tc = None @@ -340,7 +330,7 @@ Lemma transl_code_label: Proof. induction c; simpl; intros. inv H. auto. - monadInv H. rewrite (transl_instr_label _ _ _ _ _ EQ0). + monadInv H. rewrite (transl_instr_label' lbl _ _ _ _ _ EQ0). generalize (Mach.is_label_correct lbl a). destruct (Mach.is_label lbl a); intros. subst a. simpl in EQ. exists x; auto. @@ -348,7 +338,7 @@ Proof. Qed. Lemma transl_find_label: - forall f tf, + forall lbl f tf, transf_function f = OK tf -> match Mach.find_label lbl f.(Mach.fn_code) with | None => find_label lbl (fn_code tf) = None @@ -362,9 +352,6 @@ Qed. End TRANSL_LABEL. -(** A valid branch in a piece of Mach code translates to a valid ``go to'' - transition in the generated ARM code. *) - (** A valid branch in a piece of Mach code translates to a valid ``go to'' transition in the generated PPC code. *) @@ -376,7 +363,7 @@ Lemma find_label_goto_label: Mach.find_label lbl f.(Mach.fn_code) = Some c' -> exists tc', exists rs', goto_label tf lbl rs m = Next rs' m - /\ transl_code_at_pc ge (rs' PC) f c' false tf tc' + /\ transl_code_at_pc ge (rs' PC) b f c' false tf tc' /\ forall r, r <> PC -> rs'#r = rs#r. Proof. intros. exploit (transl_find_label lbl f tf); eauto. rewrite H2. @@ -392,6 +379,21 @@ Proof. intros. apply Pregmap.gso; auto. Qed. +(** Existence of return addresses *) + +Lemma return_address_exists: + forall f sg ros c, is_tail (Mcall sg ros :: c) f.(Mach.fn_code) -> + exists ra, return_address_offset f c ra. +Proof. + intros. eapply Asmgenproof0.return_address_exists; eauto. +- intros. exploit transl_instr_label; eauto. + destruct i; try (intros [A B]; apply A). intros. subst c0. repeat constructor. +- intros. monadInv H0. + destruct (zlt Int.max_unsigned (list_length_z (fn_code x))); inv EQ0. monadInv EQ. + exists x; exists true; split; auto. repeat constructor. +- exact transf_function_no_overflow. +Qed. + (** * Proof of semantic preservation *) (** Semantic preservation is proved using simulation diagrams @@ -412,49 +414,49 @@ Qed. Inductive match_states: Mach.state -> Asm.state -> Prop := | match_states_intro: - forall s f sp c ep ms m m' rs tf tc ra - (STACKS: match_stack ge s m m' ra sp) + forall s fb sp c ep ms m m' rs f tf tc + (STACKS: match_stack ge s) + (FIND: Genv.find_funct_ptr ge fb = Some (Internal f)) (MEXT: Mem.extends m m') - (AT: transl_code_at_pc ge (rs PC) f c ep tf tc) - (AG: agree ms (Vptr sp Int.zero) rs) - (RSA: retaddr_stored_at m m' sp (Int.unsigned f.(fn_retaddr_ofs)) ra) + (AT: transl_code_at_pc ge (rs PC) fb f c ep tf tc) + (AG: agree ms sp rs) (DXP: ep = true -> rs#IR10 = parent_sp s), - match_states (Mach.State s f (Vptr sp Int.zero) c ms m) + match_states (Mach.State s fb sp c ms m) (Asm.State rs m') | match_states_call: - forall s fd ms m m' rs fb - (STACKS: match_stack ge s m m' rs#(IR IR14) (Mem.nextblock m)) + forall s fb ms m m' rs + (STACKS: match_stack ge s) (MEXT: Mem.extends m m') (AG: agree ms (parent_sp s) rs) (ATPC: rs PC = Vptr fb Int.zero) - (FUNCT: Genv.find_funct_ptr ge fb = Some fd) - (WTRA: Val.has_type rs#(IR IR14) Tint), - match_states (Mach.Callstate s fd ms m) + (ATLR: rs RA = parent_ra s), + match_states (Mach.Callstate s fb ms m) (Asm.State rs m') | match_states_return: forall s ms m m' rs - (STACKS: match_stack ge s m m' (rs PC) (Mem.nextblock m)) + (STACKS: match_stack ge s) (MEXT: Mem.extends m m') - (AG: agree ms (parent_sp s) rs), + (AG: agree ms (parent_sp s) rs) + (ATPC: rs PC = parent_ra s), match_states (Mach.Returnstate s ms m) (Asm.State rs m'). Lemma exec_straight_steps: - forall s f rs1 i c ep tf tc m1' m2 m2' sp ms2 ra, - match_stack ge s m2 m2' ra sp -> + forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2, + match_stack ge s -> Mem.extends m2 m2' -> - retaddr_stored_at m2 m2' sp (Int.unsigned f.(fn_retaddr_ofs)) ra -> - transl_code_at_pc ge (rs1 PC) f (i :: c) ep tf tc -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> + transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc -> (forall k c (TR: transl_instr f i ep k = OK c), exists rs2, exec_straight tge tf c rs1 m1' k rs2 m2' - /\ agree ms2 (Vptr sp Int.zero) rs2 + /\ agree ms2 sp rs2 /\ (r10_is_parent ep i = true -> rs2#IR10 = parent_sp s)) -> exists st', plus step tge (State rs1 m1') E0 st' /\ - match_states (Mach.State s f (Vptr sp Int.zero) c ms2 m2) st'. + match_states (Mach.State s fb sp c ms2 m2) st'. Proof. - intros. inversion H2; subst. monadInv H7. + intros. inversion H2. subst. monadInv H7. exploit H3; eauto. intros [rs2 [A [B C]]]. exists (State rs2 m2'); split. eapply exec_straight_exec; eauto. @@ -462,23 +464,23 @@ Proof. Qed. Lemma exec_straight_steps_goto: - forall s f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c' ra, - match_stack ge s m2 m2' ra sp -> + forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c', + match_stack ge s -> Mem.extends m2 m2' -> - retaddr_stored_at m2 m2' sp (Int.unsigned f.(fn_retaddr_ofs)) ra -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> Mach.find_label lbl f.(Mach.fn_code) = Some c' -> - transl_code_at_pc ge (rs1 PC) f (i :: c) ep tf tc -> + transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc -> r10_is_parent ep i = false -> (forall k c (TR: transl_instr f i ep k = OK c), exists jmp, exists k', exists rs2, exec_straight tge tf c rs1 m1' (jmp :: k') rs2 m2' - /\ agree ms2 (Vptr sp Int.zero) rs2 + /\ agree ms2 sp rs2 /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2') -> exists st', plus step tge (State rs1 m1') E0 st' /\ - match_states (Mach.State s f (Vptr sp Int.zero) c' ms2 m2) st'. + match_states (Mach.State s fb sp c' ms2 m2) st'. Proof. - intros. inversion H3; subst. monadInv H9. + intros. inversion H3. subst. monadInv H9. exploit H5; eauto. intros [jmp [k' [rs2 [A [B C]]]]]. generalize (functions_transl _ _ _ H7 H8); intro FN. generalize (transf_function_no_overflow _ _ H8); intro NOOV. @@ -523,7 +525,7 @@ Qed. (** This is the simulation diagram. We prove it by case analysis on the Mach transition. *) Theorem step_simulation: - forall S1 t S2, Mach.step ge S1 t S2 -> + forall S1 t S2, Mach.step return_address_offset ge S1 t S2 -> forall S1' (MS: match_states S1 S1'), (exists S2', plus step tge S1' t S2' /\ match_states S2 S2') \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat. @@ -550,8 +552,6 @@ Proof. assert (Val.lessdef (rs src) (rs0 (preg_of src))). eapply preg_val; eauto. exploit Mem.storev_extends; eauto. intros [m2' [A B]]. left; eapply exec_straight_steps; eauto. - eapply match_stack_storev; eauto. - eapply retaddr_stored_at_storev; eauto. rewrite (sp_val _ _ _ AG) in A. intros. simpl in TR. exploit storeind_correct; eauto with asmgen. intros [rs' [P Q]]. exists rs'; split. eauto. @@ -559,11 +559,12 @@ Proof. simpl; intros. rewrite Q; auto with asmgen. - (* Mgetparam *) + assert (f0 = f) by congruence; subst f0. unfold load_stack in *. - exploit Mem.loadv_extends. eauto. eexact H. auto. + exploit Mem.loadv_extends. eauto. eexact H0. auto. intros [parent' [A B]]. rewrite (sp_val _ _ _ AG) in A. exploit lessdef_parent_sp; eauto. clear B; intros B; subst parent'. - exploit Mem.loadv_extends. eauto. eexact H0. auto. + exploit Mem.loadv_extends. eauto. eexact H1. auto. intros [v' [C D]]. Opaque loadind. left; eapply exec_straight_steps; eauto; intros. @@ -588,7 +589,7 @@ Opaque loadind. apply preg_of_not_R10; auto. - (* Mop *) - assert (eval_operation tge (Vptr sp0 Int.zero) op rs##args m = Some v). + assert (eval_operation tge sp op rs##args m = Some v). rewrite <- H. apply eval_operation_preserved. exact symbols_preserved. exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eexact H0. intros [v' [A B]]. rewrite (sp_val _ _ _ AG) in A. @@ -596,7 +597,7 @@ Opaque loadind. exploit transl_op_correct; eauto. intros [rs2 [P [Q R]]]. assert (S: Val.lessdef v (rs2 (preg_of res))) by (eapply Val.lessdef_trans; eauto). exists rs2; split. eauto. split. - assert (agree (Regmap.set res v (undef_temps rs)) (Vptr sp0 Int.zero) rs2). + assert (agree (Regmap.set res v (undef_temps rs)) sp rs2). eapply agree_set_undef_mreg; eauto with asmgen. unfold undef_op; destruct op; auto. change (undef_move rs) with rs. eapply agree_set_mreg; eauto. @@ -604,7 +605,7 @@ Opaque loadind. rewrite R; auto. apply preg_of_not_R10; auto. - (* Mload *) - assert (eval_addressing tge (Vptr sp0 Int.zero) addr rs##args = Some a). + assert (eval_addressing tge sp addr rs##args = Some a). rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1. intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A. @@ -616,15 +617,13 @@ Opaque loadind. simpl; congruence. - (* Mstore *) - assert (eval_addressing tge (Vptr sp0 Int.zero) addr rs##args = Some a). + assert (eval_addressing tge sp addr rs##args = Some a). rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1. intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A. assert (Val.lessdef (rs src) (rs0 (preg_of src))). eapply preg_val; eauto. exploit Mem.storev_extends; eauto. intros [m2' [C D]]. left; eapply exec_straight_steps; eauto. - eapply match_stack_storev; eauto. - eapply retaddr_stored_at_storev; eauto. intros. simpl in TR. exploit transl_store_correct; eauto. intros [rs2 [P Q]]. exists rs2; split. eauto. @@ -632,73 +631,65 @@ Opaque loadind. simpl; congruence. - (* Mcall *) + assert (f0 = f) by congruence. subst f0. inv AT. assert (NOOV: list_length_z (fn_code tf) <= Int.max_unsigned). eapply transf_function_no_overflow; eauto. - destruct ros as [rf|fid]; simpl in H; monadInv H3. + destruct ros as [rf|fid]; simpl in H; monadInv H5. + (* Indirect call *) - exploit Genv.find_funct_inv; eauto. intros [bf EQ2]. - rewrite EQ2 in H; rewrite Genv.find_funct_find_funct_ptr in H. - assert (rs0 x0 = Vptr bf Int.zero). - exploit ireg_val; eauto. rewrite EQ2; intros LD; inv LD; auto. - generalize (code_tail_next_int _ _ _ _ NOOV H4). intro CT1. - assert (TCA: transl_code_at_pc ge (Vptr b (Int.add ofs Int.one)) f c false tf x). - econstructor; eauto. + assert (rs rf = Vptr f' Int.zero). + destruct (rs rf); try discriminate. + revert H; predSpec Int.eq Int.eq_spec i Int.zero; intros; congruence. + assert (rs0 x0 = Vptr f' Int.zero). + exploit ireg_val; eauto. rewrite H5; intros LD; inv LD; auto. + generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1. + assert (TCA: transl_code_at_pc ge (Vptr fb (Int.add ofs Int.one)) fb f c false tf x). + econstructor; eauto. + exploit return_address_offset_correct; eauto. intros; subst ra. left; econstructor; split. apply plus_one. eapply exec_step_internal. eauto. eapply functions_transl; eauto. eapply find_instr_tail; eauto. simpl. eauto. econstructor; eauto. econstructor; eauto. - Simpl. rewrite <- H0; eexact TCA. - change (Mem.valid_block m sp0). eapply retaddr_stored_at_valid; eauto. + eapply agree_sp_def; eauto. simpl. eapply agree_exten; eauto. intros. Simpl. - Simpl. rewrite <- H0. exact I. + Simpl. rewrite <- H2. auto. + (* Direct call *) - destruct (Genv.find_symbol ge fid) as [bf|] eqn:FS; try discriminate. - generalize (code_tail_next_int _ _ _ _ NOOV H4). intro CT1. - assert (TCA: transl_code_at_pc ge (Vptr b (Int.add ofs Int.one)) f c false tf x). + generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1. + assert (TCA: transl_code_at_pc ge (Vptr fb (Int.add ofs Int.one)) fb f c false tf x). econstructor; eauto. + exploit return_address_offset_correct; eauto. intros; subst ra. left; econstructor; split. apply plus_one. eapply exec_step_internal. eauto. eapply functions_transl; eauto. eapply find_instr_tail; eauto. - simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite FS. eauto. + simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite H. eauto. econstructor; eauto. econstructor; eauto. - rewrite <- H0. eexact TCA. - change (Mem.valid_block m sp0). eapply retaddr_stored_at_valid; eauto. + eapply agree_sp_def; eauto. simpl. eapply agree_exten; eauto. intros. Simpl. - auto. - rewrite <- H0. exact I. + Simpl. rewrite <- H2. auto. - (* Mtailcall *) +Opaque Int.repr. + assert (f0 = f) by congruence. subst f0. inversion AT; subst. assert (NOOV: list_length_z (fn_code tf) <= Int.max_unsigned). eapply transf_function_no_overflow; eauto. - rewrite (sp_val _ _ _ AG) in *. unfold load_stack in *. - exploit Mem.loadv_extends. eauto. eexact H0. auto. simpl. intros [parent' [A B]]. + exploit Mem.loadv_extends. eauto. eexact H1. auto. + unfold chunk_of_type. rewrite (sp_val _ _ _ AG). intros [parent' [A B]]. + exploit Mem.loadv_extends. eauto. eexact H2. auto. + unfold chunk_of_type. rewrite (sp_val _ _ _ AG). intros [ra' [C D]]. exploit lessdef_parent_sp; eauto. intros. subst parent'. clear B. - assert (C: Mem.loadv Mint32 m'0 (Val.add (rs0 SP) (Vint (fn_retaddr_ofs f))) = Some ra). -Opaque Int.repr. - erewrite agree_sp; eauto. simpl. rewrite Int.add_zero_l. - eapply rsa_contains; eauto. - exploit retaddr_stored_at_can_free; eauto. intros [m2' [E F]]. - assert (M: match_stack ge s m'' m2' ra (Mem.nextblock m'')). - apply match_stack_change_bound with stk. - eapply match_stack_free_left; eauto. - eapply match_stack_free_left; eauto. - eapply match_stack_free_right; eauto. - omega. - apply Z.lt_le_incl. change (Mem.valid_block m'' stk). - eapply Mem.valid_block_free_1; eauto. eapply Mem.valid_block_free_1; eauto. - eapply retaddr_stored_at_valid; eauto. + exploit lessdef_parent_ra; eauto. intros. subst ra'. clear D. + exploit Mem.free_parallel_extends; eauto. intros [m2' [E F]]. assert (X: forall k, exists rs2, exec_straight tge tf (loadind_int IR13 (fn_retaddr_ofs f) IR14 (Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: k)) rs0 m'0 k rs2 m2' /\ rs2#SP = parent_sp s - /\ rs2#RA = ra + /\ rs2#RA = parent_ra s /\ forall r, r <> PC -> r <> SP -> r <> IR14 -> rs2#r = rs0#r). { intros. @@ -711,12 +702,13 @@ Opaque Int.repr. split. Simpl. intros. Simpl. } - destruct ros as [rf|fid]; simpl in H; monadInv H6. + destruct ros as [rf|fid]; simpl in H; monadInv H7. + (* Indirect call *) - exploit Genv.find_funct_inv; eauto. intros [bf EQ2]. - rewrite EQ2 in H; rewrite Genv.find_funct_find_funct_ptr in H. - assert (rs0 x0 = Vptr bf Int.zero). - exploit ireg_val; eauto. rewrite EQ2; intros LD; inv LD; auto. + assert (rs rf = Vptr f' Int.zero). + destruct (rs rf); try discriminate. + revert H; predSpec Int.eq Int.eq_spec i Int.zero; intros; congruence. + assert (rs0 x0 = Vptr f' Int.zero). + exploit ireg_val; eauto. rewrite H7; intros LD; inv LD; auto. destruct (X (Pbreg x0 sig :: x)) as [rs2 [P [Q [R S]]]]. exploit exec_straight_steps_2. eexact P. eauto. eauto. eapply functions_transl; eauto. eauto. intros [ofs' [Y Z]]. @@ -727,15 +719,12 @@ Opaque Int.repr. simpl. reflexivity. traceEq. econstructor; eauto. - Simpl. rewrite R; auto. - constructor; intros. Simpl. - Simpl. rewrite S; auto with asmgen. eapply preg_val; eauto. + split. Simpl. eapply parent_sp_def; eauto. + intros. Simpl. rewrite S; auto with asmgen. eapply preg_val; eauto. Simpl. rewrite S; auto with asmgen. rewrite <- (ireg_of_eq _ _ EQ1); auto with asmgen. rewrite <- (ireg_of_eq _ _ EQ1); auto with asmgen. - Simpl. rewrite R. eapply retaddr_stored_at_type; eauto. + (* Direct call *) - destruct (Genv.find_symbol ge fid) as [bf|] eqn:FS; try discriminate. destruct (X (Pbsymb fid sig :: x)) as [rs2 [P [Q [R S]]]]. exploit exec_straight_steps_2. eexact P. eauto. eauto. eapply functions_transl; eauto. eauto. intros [ofs' [Y Z]]. @@ -743,14 +732,11 @@ Opaque Int.repr. eapply plus_right'. eapply exec_straight_exec; eauto. econstructor. eauto. eapply functions_transl; eauto. eapply find_instr_tail; eauto. - simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite FS. reflexivity. + simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite H. reflexivity. traceEq. - econstructor; eauto. - Simpl. rewrite R; auto. - constructor; intros. Simpl. - Simpl. rewrite S; auto with asmgen. eapply preg_val; eauto. - Simpl. - Simpl. rewrite R. eapply retaddr_stored_at_type; eauto. + econstructor; eauto. + split. Simpl. eapply parent_sp_def; eauto. + intros. Simpl. rewrite S; auto with asmgen. eapply preg_val; eauto. - (* Mbuiltin *) inv AT. monadInv H3. @@ -764,16 +750,11 @@ Opaque Int.repr. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. econstructor; eauto. - eapply match_stack_extcall; eauto. - intros; eapply external_call_max_perm; eauto. - instantiate (2 := tf); instantiate (1 := x). Simpl. rewrite <- H0. simpl. econstructor; eauto. eapply code_tail_next_int; eauto. apply agree_nextinstr. eapply agree_set_undef_mreg; eauto. rewrite Pregmap.gss. auto. intros. Simpl. - eapply retaddr_stored_at_extcall; eauto. - intros; eapply external_call_max_perm; eauto. congruence. - (* Mannot *) @@ -789,18 +770,15 @@ Opaque Int.repr. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. eapply match_states_intro with (ep := false); eauto with coqlib. - eapply match_stack_extcall; eauto. - intros; eapply external_call_max_perm; eauto. unfold nextinstr. rewrite Pregmap.gss. rewrite <- H1; simpl. econstructor; eauto. eapply code_tail_next_int; eauto. apply agree_nextinstr. auto. - eapply retaddr_stored_at_extcall; eauto. - intros; eapply external_call_max_perm; eauto. congruence. - (* Mgoto *) - inv AT. monadInv H3. + assert (f0 = f) by congruence. subst f0. + inv AT. monadInv H4. exploit find_label_goto_label; eauto. intros [tc' [rs' [GOTO [AT2 INV]]]]. left; exists (State rs' m'); split. apply plus_one. econstructor; eauto. @@ -812,6 +790,7 @@ Opaque Int.repr. congruence. - (* Mcond true *) + assert (f0 = f) by congruence. subst f0. exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC. left; eapply exec_straight_steps_goto; eauto. intros. simpl in TR. @@ -834,9 +813,10 @@ Opaque Int.repr. simpl. congruence. - (* Mjumptable *) - inv AT. monadInv H5. + assert (f0 = f) by congruence. subst f0. + inv AT. monadInv H6. exploit functions_transl; eauto. intro FN. - generalize (transf_function_no_overflow _ _ H4); intro NOOV. + generalize (transf_function_no_overflow _ _ H5); intro NOOV. exploit find_label_goto_label. eauto. eauto. instantiate (2 := rs0#IR14 <- Vundef). Simpl. eauto. @@ -846,39 +826,30 @@ Opaque Int.repr. left; econstructor; split. apply plus_one. econstructor; eauto. eapply find_instr_tail; eauto. - simpl. rewrite <- H8. unfold Mach.label in H0; unfold label; rewrite H0. eexact A. + simpl. rewrite <- H9. unfold Mach.label in H0; unfold label; rewrite H0. eexact A. econstructor; eauto. eapply agree_exten_temps; eauto. intros. rewrite C; auto with asmgen. Simpl. congruence. - (* Mreturn *) + assert (f0 = f) by congruence. subst f0. inversion AT; subst. assert (NOOV: list_length_z (fn_code tf) <= Int.max_unsigned). eapply transf_function_no_overflow; eauto. rewrite (sp_val _ _ _ AG) in *. unfold load_stack in *. - exploit Mem.loadv_extends. eauto. eexact H. auto. simpl. intros [parent' [A B]]. + exploit Mem.loadv_extends. eauto. eexact H0. auto. simpl. intros [parent' [A B]]. exploit lessdef_parent_sp; eauto. intros. subst parent'. clear B. - assert (C: Mem.loadv Mint32 m'0 (Val.add (rs0 SP) (Vint (fn_retaddr_ofs f))) = Some ra). -Opaque Int.repr. - erewrite agree_sp; eauto. simpl. rewrite Int.add_zero_l. - eapply rsa_contains; eauto. - exploit retaddr_stored_at_can_free; eauto. intros [m2' [E F]]. - assert (M: match_stack ge s m'' m2' ra (Mem.nextblock m'')). - apply match_stack_change_bound with stk. - eapply match_stack_free_left; eauto. - eapply match_stack_free_left; eauto. - eapply match_stack_free_right; eauto. omega. - apply Z.lt_le_incl. change (Mem.valid_block m'' stk). - eapply Mem.valid_block_free_1; eauto. eapply Mem.valid_block_free_1; eauto. - eapply retaddr_stored_at_valid; eauto. - monadInv H5. + exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [ra' [C D]]. + exploit lessdef_parent_ra; eauto. intros. subst ra'. clear D. + exploit Mem.free_parallel_extends; eauto. intros [m2' [E F]]. + monadInv H6. assert (X: forall k, exists rs2, exec_straight tge tf (loadind_int IR13 (fn_retaddr_ofs f) IR14 (Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: k)) rs0 m'0 k rs2 m2' /\ rs2#SP = parent_sp s - /\ rs2#RA = ra + /\ rs2#RA = parent_ra s /\ forall r, r <> PC -> r <> SP -> r <> IR14 -> rs2#r = rs0#r). { intros. @@ -901,9 +872,8 @@ Opaque Int.repr. simpl. reflexivity. traceEq. econstructor; eauto. - Simpl. rewrite R; auto. - constructor; intros. Simpl. - Simpl. rewrite S; auto with asmgen. eapply preg_val; eauto. + split. Simpl. eapply parent_sp_def; eauto. + intros. Simpl. rewrite S; auto with asmgen. eapply preg_val; eauto. - (* internal function *) exploit functions_translated; eauto. intros [tf [A B]]. monadInv B. @@ -913,12 +883,10 @@ Opaque Int.repr. unfold store_stack in *. exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. intros [m1' [C D]]. - assert (E: Mem.extends m2 m1') by (eapply Mem.free_left_extends; eauto). - exploit Mem.storev_extends. eexact E. eexact H1. eauto. eauto. + exploit Mem.storev_extends. eexact D. eexact H1. eauto. eauto. intros [m2' [F G]]. - exploit retaddr_stored_at_can_alloc. eexact H. eauto. eauto. eauto. eauto. - auto. auto. auto. auto. eauto. - intros [m3' [P [Q R]]]. + exploit Mem.storev_extends. eexact G. eexact H2. eauto. eauto. + intros [m3' [P Q]]. (* Execution of function prologue *) set (rs2 := nextinstr (rs0#IR10 <- (parent_sp s) #IR13 <- (Vptr stk Int.zero))). set (rs3 := nextinstr rs2). @@ -932,22 +900,11 @@ Opaque Int.repr. rewrite <- (sp_val _ _ _ AG). unfold chunk_of_type in F. rewrite F. auto. simpl. auto. simpl. unfold exec_store. change (rs2 IR14) with (rs0 IR14). - rewrite Int.add_zero_l. simpl. rewrite P. auto. auto. auto. + rewrite Int.add_zero_l. simpl. unfold chunk_of_type in P. simpl in P. + rewrite Int.add_zero_l in P. rewrite ATLR. rewrite P. auto. auto. auto. left; exists (State rs3 m3'); split. eapply exec_straight_steps_1; eauto. omega. constructor. econstructor; eauto. - assert (STK: stk = Mem.nextblock m) by (eapply Mem.alloc_result; eauto). - rewrite <- STK in STACKS. simpl in F. simpl in H1. - eapply match_stack_invariant; eauto. - intros. eapply Mem.perm_alloc_4; eauto. eapply Mem.perm_free_3; eauto. - eapply Mem.perm_store_2; eauto. unfold block; omega. - intros. eapply Mem.perm_store_1; eauto. eapply Mem.perm_store_1; eauto. - eapply Mem.perm_alloc_1; eauto. - intros. erewrite Mem.load_store_other. 2: eauto. - erewrite Mem.load_store_other. 2: eauto. - eapply Mem.load_alloc_other; eauto. - left; unfold block; omega. - left; unfold block; omega. change (rs3 PC) with (Val.add (Val.add (rs0 PC) Vone) Vone). rewrite ATPC. simpl. constructor; eauto. subst x. eapply code_tail_next_int. omega. @@ -970,19 +927,14 @@ Opaque Int.repr. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. econstructor; eauto. - rewrite Pregmap.gss. apply match_stack_change_bound with (Mem.nextblock m). - eapply match_stack_extcall; eauto. - intros. eapply external_call_max_perm; eauto. - eapply external_call_nextblock; eauto. - unfold loc_external_result. eapply agree_set_mreg; eauto. rewrite Pregmap.gso; auto with asmgen. rewrite Pregmap.gss. auto. intros; Simpl. - (* return *) inv STACKS. simpl in *. - right. split. omega. split. auto. - econstructor; eauto. congruence. + right. split. omega. split. auto. + rewrite <- ATPC in H5. econstructor; eauto. congruence. Qed. Lemma transf_initial_states: @@ -990,21 +942,19 @@ Lemma transf_initial_states: exists st2, Asm.initial_state tprog st2 /\ match_states st1 st2. Proof. intros. inversion H. unfold ge0 in *. - exploit functions_translated; eauto. intros [tf [A B]]. econstructor; split. econstructor. eapply Genv.init_mem_transf_partial; eauto. replace (symbol_offset (Genv.globalenv tprog) (prog_main tprog) Int.zero) - with (Vptr b Int.zero). + with (Vptr fb Int.zero). econstructor; eauto. constructor. apply Mem.extends_refl. - split. auto. intros. rewrite Regmap.gi. auto. - reflexivity. - exact I. + split. auto. simpl. congruence. intros. rewrite Regmap.gi. auto. unfold symbol_offset. - rewrite (transform_partial_program_main _ _ TRANSF). - rewrite symbols_preserved. unfold ge; rewrite H1. auto. + rewrite (transform_partial_program_main _ _ TRANSF). + rewrite symbols_preserved. + unfold ge; rewrite H1. auto. Qed. Lemma transf_final_states: @@ -1018,7 +968,7 @@ Proof. Qed. Theorem transf_program_correct: - forward_simulation (Mach.semantics prog) (Asm.semantics tprog). + forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog). Proof. eapply forward_simulation_star with (measure := measure). eexact symbols_preserved. diff --git a/arm/Asmgenproof1.v b/arm/Asmgenproof1.v index 8fc8a7e..9d90d1f 100644 --- a/arm/Asmgenproof1.v +++ b/arm/Asmgenproof1.v @@ -12,7 +12,6 @@ (** Correctness proof for ARM code generation: auxiliary results. *) -(*Require Import Axioms.*) Require Import Coqlib. Require Import Errors. Require Import Maps. @@ -363,6 +362,35 @@ Qed. (** Indexed memory loads. *) +Lemma indexed_memory_access_correct: + forall (P: regset -> Prop) (mk_instr: ireg -> int -> instruction) + (mk_immed: int -> int) (base: ireg) n k (rs: regset) m m', + (forall (r1: ireg) (rs1: regset) n1 k, + Val.add rs1#r1 (Vint n1) = Val.add rs#base (Vint n) -> + (forall (r: preg), r <> PC -> r <> IR14 -> rs1 r = rs r) -> + exists rs', + exec_straight ge fn (mk_instr r1 n1 :: k) rs1 m k rs' m' /\ P rs') -> + exists rs', + exec_straight ge fn + (indexed_memory_access mk_instr mk_immed base n k) rs m + k rs' m' + /\ P rs'. +Proof. + intros until m'; intros SEM. + unfold indexed_memory_access. + destruct (Int.eq n (mk_immed n)). +- apply SEM; auto. +- destruct (addimm_correct IR14 base (Int.sub n (mk_immed n)) (mk_instr IR14 (mk_immed n) :: k) rs m) + as (rs1 & A & B & C). + destruct (SEM IR14 rs1 (mk_immed n) k) as (rs2 & D & E). + rewrite B. rewrite Val.add_assoc. f_equal. simpl. + rewrite Int.sub_add_opp. rewrite Int.add_assoc. + rewrite (Int.add_commut (Int.neg (mk_immed n))). + rewrite Int.add_neg_zero. rewrite Int.add_zero. auto. + auto with asmgen. + exists rs2; split; auto. eapply exec_straight_trans; eauto. +Qed. + Lemma loadind_int_correct: forall (base: ireg) ofs dst (rs: regset) m v k, Mem.loadv Mint32 m (Val.add rs#base (Vint ofs)) = Some v -> @@ -371,18 +399,10 @@ Lemma loadind_int_correct: /\ rs'#dst = v /\ forall r, r <> PC -> r <> IR14 -> r <> dst -> rs'#r = rs#r. Proof. - intros; unfold loadind_int. destruct (is_immed_mem_word ofs). - exists (nextinstr (rs#dst <- v)). - split. apply exec_straight_one. simpl. - unfold exec_load. rewrite H. auto. auto. - intuition Simpl. - exploit addimm_correct. intros [rs' [A [B C]]]. - exists (nextinstr (rs'#dst <- v)). - split. eapply exec_straight_trans. eauto. apply exec_straight_one. - simpl. unfold exec_load. rewrite B. - rewrite Val.add_assoc. simpl. rewrite Int.add_zero. - rewrite H. auto. auto. - intuition Simpl. + intros; unfold loadind_int. apply indexed_memory_access_correct; intros. + econstructor; split. + apply exec_straight_one. simpl. unfold exec_load. rewrite H0; rewrite H; eauto. auto. + split. Simpl. intros; Simpl. Qed. Lemma loadind_float_correct: @@ -393,18 +413,10 @@ Lemma loadind_float_correct: /\ rs'#dst = v /\ forall r, r <> PC -> r <> IR14 -> r <> dst -> rs'#r = rs#r. Proof. - intros; unfold loadind_float. destruct (is_immed_mem_float ofs). - exists (nextinstr (rs#dst <- v)). - split. apply exec_straight_one. simpl. - unfold exec_load. rewrite H. auto. auto. - intuition Simpl. - exploit addimm_correct. eauto. intros [rs' [A [B C]]]. - exists (nextinstr (rs'#dst <- v)). - split. eapply exec_straight_trans. eauto. apply exec_straight_one. - simpl. unfold exec_load. rewrite B. - rewrite Val.add_assoc. simpl. - rewrite Int.add_zero. rewrite H. auto. auto. - intuition Simpl. + intros; unfold loadind_float. apply indexed_memory_access_correct; intros. + econstructor; split. + apply exec_straight_one. simpl. unfold exec_load. rewrite H0; rewrite H; eauto. auto. + split. Simpl. intros; Simpl. Qed. Lemma loadind_correct: @@ -432,19 +444,11 @@ Lemma storeind_int_correct: exec_straight ge fn (storeind_int src base ofs k) rs m k rs' m' /\ forall r, r <> PC -> r <> IR14 -> rs'#r = rs#r. Proof. - intros; unfold storeind_int. destruct (is_immed_mem_word ofs). - exists (nextinstr rs). - split. apply exec_straight_one. simpl. - unfold exec_store. rewrite H. auto. auto. - intuition Simpl. - exploit addimm_correct. eauto. intros [rs' [A [B C]]]. - exists (nextinstr rs'). - split. eapply exec_straight_trans. eauto. apply exec_straight_one. - simpl. unfold exec_store. rewrite B. - rewrite C. rewrite Val.add_assoc. simpl. rewrite Int.add_zero. - rewrite H. auto. - congruence. auto with asmgen. auto. - intuition Simpl. + intros; unfold storeind_int. apply indexed_memory_access_correct; intros. + econstructor; split. + apply exec_straight_one. simpl. unfold exec_store. + rewrite H1. rewrite H2; auto with asmgen. rewrite H; eauto. auto. + intros; Simpl. Qed. Lemma storeind_float_correct: @@ -454,20 +458,11 @@ Lemma storeind_float_correct: exec_straight ge fn (storeind_float src base ofs k) rs m k rs' m' /\ forall r, r <> PC -> r <> IR14 -> rs'#r = rs#r. Proof. - intros; unfold storeind_float. destruct (is_immed_mem_float ofs). - exists (nextinstr rs). - split. apply exec_straight_one. simpl. - unfold exec_store. rewrite H. auto. auto. - intuition Simpl. - exploit addimm_correct. eauto. intros [rs' [A [B C]]]. - exists (nextinstr rs'). - split. eapply exec_straight_trans. eauto. apply exec_straight_one. - simpl. unfold exec_store. rewrite B. - rewrite C. rewrite Val.add_assoc. simpl. rewrite Int.add_zero. - rewrite H. auto. - congruence. congruence. - auto with asmgen. - intuition Simpl. + intros; unfold storeind_float. apply indexed_memory_access_correct; intros. + econstructor; split. + apply exec_straight_one. simpl. unfold exec_store. + rewrite H0. rewrite H1; auto with asmgen. rewrite H; eauto. auto. + intros; Simpl. Qed. Lemma storeind_correct: @@ -541,8 +536,6 @@ Proof. unfold compare_float. Simpl. Qed. -Definition lock {A: Type} (x: A) := x. - Ltac ArgsInv := repeat (match goal with | [ H: Error _ = OK _ |- _ ] => discriminate @@ -552,12 +545,8 @@ Ltac ArgsInv := end); subst; repeat (match goal with - | [ H: ireg_of ?x = OK ?y |- _ ] => - simpl in *; rewrite (ireg_of_eq _ _ H) in * -(*; change H with (lock (ireg_of x) = OK y)*) - | [ H: freg_of ?x = OK ?y |- _ ] => - simpl in *; rewrite (freg_of_eq _ _ H) in * -(*; change H with (lock (freg_of x) = OK y)*) + | [ H: ireg_of ?x = OK ?y |- _ ] => simpl in *; rewrite (ireg_of_eq _ _ H) in * + | [ H: freg_of ?x = OK ?y |- _ ] => simpl in *; rewrite (freg_of_eq _ _ H) in * end). Lemma transl_cond_correct: @@ -833,6 +822,8 @@ Proof. unfold rs2. Simpl. Qed. +(** Translation of loads and stores. *) + Remark val_add_add_zero: forall v1 v2, Val.add v1 v2 = Val.add (Val.add v1 v2) (Vint Int.zero). Proof. @@ -842,9 +833,9 @@ Qed. Lemma transl_memory_access_correct: forall (P: regset -> Prop) (mk_instr_imm: ireg -> int -> instruction) (mk_instr_gen: option (ireg -> shift_addr -> instruction)) - (is_immed: int -> bool) + (mk_immed: int -> int) addr args k c (rs: regset) a m m', - transl_memory_access mk_instr_imm mk_instr_gen is_immed addr args k = OK c -> + transl_memory_access mk_instr_imm mk_instr_gen mk_immed addr args k = OK c -> eval_addressing ge (rs#SP) addr (map rs (map preg_of args)) = Some a -> (forall (r1: ireg) (rs1: regset) n k, Val.add rs1#r1 (Vint n) = a -> @@ -854,11 +845,10 @@ Lemma transl_memory_access_correct: match mk_instr_gen with | None => True | Some mk => - (forall (r1: ireg) (sa: shift_addr) (rs1: regset) k, - Val.add rs1#r1 (eval_shift_addr sa rs1) = a -> - (forall (r: preg), r <> PC -> r <> IR14 -> rs1 r = rs r) -> - exists rs', - exec_straight ge fn (mk r1 sa :: k) rs1 m k rs' m' /\ P rs') + (forall (r1: ireg) (sa: shift_addr) k, + Val.add rs#r1 (eval_shift_addr sa rs) = a -> + exists rs', + exec_straight ge fn (mk r1 sa :: k) rs m k rs' m' /\ P rs') end -> exists rs', exec_straight ge fn c rs m k rs' m' /\ P rs'. @@ -866,56 +856,15 @@ Proof. intros until m'; intros TR EA MK1 MK2. unfold transl_memory_access in TR; destruct addr; ArgsInv; simpl in EA; inv EA. (* Aindexed *) - case (is_immed i). - (* Aindexed, small displacement *) - apply MK1; auto. - (* Aindexed, large displacement *) - destruct (addimm_correct IR14 x i (mk_instr_imm IR14 Int.zero :: k) rs m) - as [rs' [A [B C]]]. - exploit (MK1 IR14 rs' Int.zero); eauto. - rewrite B. rewrite Val.add_assoc. simpl Val.add. rewrite Int.add_zero. reflexivity. - intros [rs'' [D E]]. - exists rs''; split. - eapply exec_straight_trans. eexact A. eexact D. auto. + apply indexed_memory_access_correct. exact MK1. (* Aindexed2 *) - destruct mk_instr_gen as [mk | ]. - (* binary form available *) - apply MK2; auto. - (* binary form not available *) - set (rs' := nextinstr (rs#IR14 <- (Val.add (rs x) (rs x0)))). - exploit (MK1 IR14 rs' Int.zero); eauto. - unfold rs'. Simpl. symmetry. apply val_add_add_zero. - intros. unfold rs'. Simpl. - intros [rs'' [A B]]. - exists rs''; split. - eapply exec_straight_step with (rs2 := rs'); eauto. - simpl. auto. auto. + destruct mk_instr_gen as [mk | ]; monadInv TR. apply MK2. + simpl. erewrite ! ireg_of_eq; eauto. (* Aindexed2shift *) - destruct mk_instr_gen as [mk | ]. - (* binary form available *) - apply MK2; auto. rewrite transl_shift_addr_correct. auto. - (* binary form not available *) - set (rs' := nextinstr (rs#IR14 <- (Val.add (rs x) (eval_shift s (rs x0))))). - exploit (MK1 IR14 rs' Int.zero); eauto. - unfold rs'. Simpl. symmetry. apply val_add_add_zero. - intros; unfold rs'; Simpl. - intros [rs'' [A B]]. - exists rs''; split. - eapply exec_straight_step with (rs2 := rs'); eauto. - simpl. rewrite transl_shift_correct. auto. - auto. + destruct mk_instr_gen as [mk | ]; monadInv TR. apply MK2. + erewrite ! ireg_of_eq; eauto. rewrite transl_shift_addr_correct. auto. (* Ainstack *) - destruct (is_immed i); inv TR. - (* Ainstack, short displacement *) - apply MK1; auto. - (* Ainstack, large displacement *) - destruct (addimm_correct IR14 IR13 i (mk_instr_imm IR14 Int.zero :: k) rs m) - as [rs' [A [B C]]]. - exploit (MK1 IR14 rs' Int.zero); eauto. - rewrite B. rewrite Val.add_assoc. f_equal. simpl. rewrite Int.add_zero; auto. - intros [rs'' [D E]]. - exists rs''; split. - eapply exec_straight_trans. eexact A. eexact D. auto. + inv TR. apply indexed_memory_access_correct. exact MK1. Qed. Lemma transl_load_int_correct: @@ -983,8 +932,7 @@ Proof. intros; Simpl. simpl; intros. econstructor; split. apply exec_straight_one. - rewrite H2. unfold exec_store. rewrite H. rewrite H3; eauto with asmgen. - rewrite H1. eauto. auto. + rewrite H2. unfold exec_store. rewrite H. rewrite H1. eauto. auto. intros; Simpl. Qed. @@ -1003,8 +951,7 @@ Proof. intros. monadInv H. erewrite freg_of_eq in * by eauto. eapply transl_memory_access_correct; eauto. intros; simpl. econstructor; split. apply exec_straight_one. - rewrite H2. unfold exec_store. rewrite H. rewrite H3; eauto with asmgen. - rewrite H1. eauto. auto. + rewrite H2. unfold exec_store. rewrite H. rewrite H3; auto with asmgen. rewrite H1. eauto. auto. intros; Simpl. simpl; auto. Qed. diff --git a/backend/Asmgenproof0.v b/backend/Asmgenproof0.v index 324e1f7..e1a3abc 100644 --- a/backend/Asmgenproof0.v +++ b/backend/Asmgenproof0.v @@ -607,7 +607,8 @@ Qed. - the "code is tail of" property - correct translation of labels. *) -Definition tail_nolabel (k c: code) : Prop := is_tail k c /\ forall lbl, find_label lbl c = find_label lbl k. +Definition tail_nolabel (k c: code) : Prop := + is_tail k c /\ forall lbl, find_label lbl c = find_label lbl k. Lemma tail_nolabel_refl: forall c, tail_nolabel c c. @@ -616,17 +617,21 @@ Proof. Qed. Lemma tail_nolabel_trans: - forall c1 c2 c3, tail_nolabel c1 c2 -> tail_nolabel c2 c3 -> tail_nolabel c1 c3. + forall c1 c2 c3, tail_nolabel c2 c3 -> tail_nolabel c1 c2 -> tail_nolabel c1 c3. Proof. intros. destruct H; destruct H0; split. eapply is_tail_trans; eauto. - intros. rewrite H2; auto. + intros. rewrite H1; auto. Qed. +Definition nolabel (i: instruction) := + match i with Plabel _ => False | _ => True end. + +Hint Extern 1 (nolabel _) => exact I : labels. + Lemma tail_nolabel_cons: forall i c k, - match i with Plabel _ => False | _ => True end -> - tail_nolabel k c -> tail_nolabel k (i :: c). + nolabel i -> tail_nolabel k c -> tail_nolabel k (i :: c). Proof. intros. destruct H0. split. constructor; auto. @@ -635,15 +640,15 @@ Qed. Hint Resolve tail_nolabel_refl: labels. -Ltac TailNoLabels := +Ltac TailNoLabel := eauto with labels; match goal with - | [ |- tail_nolabel _ (_ :: _) ] => apply tail_nolabel_cons; [exact I | TailNoLabels] + | [ |- tail_nolabel _ (_ :: _) ] => apply tail_nolabel_cons; [auto; exact I | TailNoLabel] | [ H: Error _ = OK _ |- _ ] => discriminate - | [ H: OK _ = OK _ |- _ ] => inv H; TailNoLabels - | [ H: bind _ _ = OK _ |- _ ] => monadInv H; TailNoLabels - | [ H: (if ?x then _ else _) = OK _ |- _ ] => destruct x; TailNoLabels - | [ H: match ?x with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct x; TailNoLabels + | [ H: OK _ = OK _ |- _ ] => inv H; TailNoLabel + | [ H: bind _ _ = OK _ |- _ ] => monadInv H; TailNoLabel + | [ H: (if ?x then _ else _) = OK _ |- _ ] => destruct x; TailNoLabel + | [ H: match ?x with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct x; TailNoLabel | _ => idtac end. diff --git a/ia32/Asmgenproof.v b/ia32/Asmgenproof.v index 83918f4..860f04c 100644 --- a/ia32/Asmgenproof.v +++ b/ia32/Asmgenproof.v @@ -130,33 +130,6 @@ Qed. Section TRANSL_LABEL. -Definition nolabel (i: instruction) := - match i with Plabel _ => False | _ => True end. - -Hint Extern 1 (nolabel _) => exact I : labels. - -Lemma tail_nolabel_cons: - forall i c k, - nolabel i -> tail_nolabel k c -> tail_nolabel k (i :: c). -Proof. - intros. destruct H0. split. - constructor; auto. - intros. simpl. rewrite <- H1. destruct i; reflexivity || contradiction. -Qed. - - -Ltac TailNoLabel := - eauto with labels; - match goal with - | [ |- tail_nolabel _ (_ :: _) ] => apply tail_nolabel_cons; [auto; exact I | TailNoLabel] - | [ H: Error _ = OK _ |- _ ] => discriminate - | [ H: OK _ = OK _ |- _ ] => inv H; TailNoLabel - | [ H: bind _ _ = OK _ |- _ ] => monadInv H; TailNoLabel - | [ H: (if ?x then _ else _) = OK _ |- _ ] => destruct x; TailNoLabel - | [ H: match ?x with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct x; TailNoLabel - | _ => idtac - end. - Remark mk_mov_label: forall rd rs k c, mk_mov rd rs k = OK c -> tail_nolabel k c. Proof. @@ -192,7 +165,7 @@ Remark mk_div_label: tail_nolabel k c. Proof. unfold mk_div; intros. TailNoLabel. - eapply tail_nolabel_trans. 2: apply mk_mov2_label. TailNoLabel. + eapply tail_nolabel_trans; TailNoLabel. Qed. Hint Resolve mk_div_label: labels. @@ -202,7 +175,7 @@ Remark mk_mod_label: tail_nolabel k c. Proof. unfold mk_mod; intros. TailNoLabel. - eapply tail_nolabel_trans. 2: apply mk_mov2_label. TailNoLabel. + eapply tail_nolabel_trans; TailNoLabel. Qed. Hint Resolve mk_mod_label: labels. @@ -265,16 +238,6 @@ Proof. intros. destruct xc; simpl; TailNoLabel. Qed. -(* -Ltac ArgsInv := - match goal with - | [ H: Error _ = OK _ |- _ ] => discriminate - | [ H: match ?args with nil => _ | _ :: _ => _ end = OK _ |- _ ] => destruct args; ArgsInv - | [ H: bind _ _ = OK _ |- _ ] => monadInv H; ArgsInv - | _ => idtac - end. -*) - Remark transl_cond_label: forall cond args k c, transl_cond cond args k = OK c -> @@ -295,7 +258,7 @@ Proof. unfold transl_op; intros. destruct op; TailNoLabel. destruct (Int.eq_dec i Int.zero); TailNoLabel. destruct (Float.eq_dec f Float.zero); TailNoLabel. - eapply tail_nolabel_trans. eapply mk_setcc_label. eapply transl_cond_label. eauto. + eapply tail_nolabel_trans. eapply transl_cond_label; eauto. eapply mk_setcc_label. Qed. Remark transl_load_label: @@ -330,7 +293,7 @@ Opaque loadind. eapply transl_store_label; eauto. destruct s0; TailNoLabel. destruct s0; TailNoLabel. - eapply tail_nolabel_trans. eapply mk_jcc_label. eapply transl_cond_label; eauto. + eapply tail_nolabel_trans. eapply transl_cond_label; eauto. eapply mk_jcc_label. Qed. Lemma transl_instr_label': diff --git a/powerpc/Asmgenproof.v b/powerpc/Asmgenproof.v index 6c95744..7699fef 100644 --- a/powerpc/Asmgenproof.v +++ b/powerpc/Asmgenproof.v @@ -86,8 +86,8 @@ Proof. Qed. Lemma exec_straight_exec: - forall f c ep tf tc c' rs m rs' m', - transl_code_at_pc ge (rs PC) f c ep tf tc -> + forall fb f c ep tf tc c' rs m rs' m', + transl_code_at_pc ge (rs PC) fb f c ep tf tc -> exec_straight tge tf tc rs m c' rs' m' -> plus step tge (State rs m) E0 (State rs' m'). Proof. @@ -98,11 +98,11 @@ Proof. Qed. Lemma exec_straight_at: - forall f c ep tf tc c' ep' tc' rs m rs' m', - transl_code_at_pc ge (rs PC) f c ep tf tc -> + forall fb f c ep tf tc c' ep' tc' rs m rs' m', + transl_code_at_pc ge (rs PC) fb f c ep tf tc -> transl_code f c' ep' = OK tc' -> exec_straight tge tf tc rs m tc' rs' m' -> - transl_code_at_pc ge (rs' PC) f c' ep' tf tc'. + transl_code_at_pc ge (rs' PC) fb f c' ep' tf tc'. Proof. intros. inv H. exploit exec_straight_steps_2; eauto. @@ -112,39 +112,6 @@ Proof. rewrite PC'. constructor; auto. Qed. -(** The [find_label] function returns the code tail starting at the - given label. A connection with [code_tail] is then established. *) - -Fixpoint find_label (lbl: label) (c: code) {struct c} : option code := - match c with - | nil => None - | instr :: c' => - if is_label lbl instr then Some c' else find_label lbl c' - end. - -Lemma label_pos_code_tail: - forall lbl c pos c', - find_label lbl c = Some c' -> - exists pos', - label_pos lbl pos c = Some pos' - /\ code_tail (pos' - pos) c c' - /\ pos < pos' <= pos + list_length_z c. -Proof. - induction c. - simpl; intros. discriminate. - simpl; intros until c'. - case (is_label lbl a). - intro EQ; injection EQ; intro; subst c'. - exists (pos + 1). split. auto. split. - replace (pos + 1 - pos) with (0 + 1) by omega. constructor. constructor. - rewrite list_length_z_cons. generalize (list_length_z_pos c). omega. - intros. generalize (IHc (pos + 1) c' H). intros [pos' [A [B C]]]. - exists pos'. split. auto. split. - replace (pos' - pos) with ((pos' - (pos + 1)) + 1) by omega. - constructor. auto. - rewrite list_length_z_cons. omega. -Qed. - (** The following lemmas show that the translation from Mach to PPC preserves labels, in the sense that the following diagram commutes: << @@ -163,180 +130,169 @@ Qed. Section TRANSL_LABEL. -Variable lbl: label. - Remark loadimm_label: - forall r n k, find_label lbl (loadimm r n k) = find_label lbl k. + forall r n k, tail_nolabel k (loadimm r n k). Proof. intros. unfold loadimm. - case (Int.eq (high_s n) Int.zero). reflexivity. - case (Int.eq (low_s n) Int.zero). reflexivity. - reflexivity. + case (Int.eq (high_s n) Int.zero). TailNoLabel. + case (Int.eq (low_s n) Int.zero); TailNoLabel. Qed. -Hint Rewrite loadimm_label: labels. +Hint Resolve loadimm_label: labels. Remark addimm_label: - forall r1 r2 n k, find_label lbl (addimm r1 r2 n k) = find_label lbl k. + forall r1 r2 n k, tail_nolabel k (addimm r1 r2 n k). Proof. intros; unfold addimm. - case (Int.eq (high_s n) Int.zero). reflexivity. - case (Int.eq (low_s n) Int.zero). reflexivity. reflexivity. + case (Int.eq (high_s n) Int.zero). TailNoLabel. + case (Int.eq (low_s n) Int.zero); TailNoLabel. Qed. -Hint Rewrite addimm_label: labels. +Hint Resolve addimm_label: labels. Remark andimm_base_label: - forall r1 r2 n k, find_label lbl (andimm_base r1 r2 n k) = find_label lbl k. + forall r1 r2 n k, tail_nolabel k (andimm_base r1 r2 n k). Proof. intros; unfold andimm_base. - case (Int.eq (high_u n) Int.zero). reflexivity. - case (Int.eq (low_u n) Int.zero). reflexivity. - autorewrite with labels. reflexivity. + case (Int.eq (high_u n) Int.zero). TailNoLabel. + case (Int.eq (low_u n) Int.zero). TailNoLabel. + eapply tail_nolabel_trans; TailNoLabel. Qed. -Hint Rewrite andimm_base_label: labels. +Hint Resolve andimm_base_label: labels. Remark andimm_label: - forall r1 r2 n k, find_label lbl (andimm r1 r2 n k) = find_label lbl k. + forall r1 r2 n k, tail_nolabel k (andimm r1 r2 n k). Proof. intros; unfold andimm. - case (is_rlw_mask n). reflexivity. - autorewrite with labels. reflexivity. + case (is_rlw_mask n); TailNoLabel. Qed. -Hint Rewrite andimm_label: labels. +Hint Resolve andimm_label: labels. Remark orimm_label: - forall r1 r2 n k, find_label lbl (orimm r1 r2 n k) = find_label lbl k. + forall r1 r2 n k, tail_nolabel k (orimm r1 r2 n k). Proof. intros; unfold orimm. - case (Int.eq (high_u n) Int.zero). reflexivity. - case (Int.eq (low_u n) Int.zero). reflexivity. reflexivity. + case (Int.eq (high_u n) Int.zero). TailNoLabel. + case (Int.eq (low_u n) Int.zero); TailNoLabel. Qed. -Hint Rewrite orimm_label: labels. +Hint Resolve orimm_label: labels. Remark xorimm_label: - forall r1 r2 n k, find_label lbl (xorimm r1 r2 n k) = find_label lbl k. + forall r1 r2 n k, tail_nolabel k (xorimm r1 r2 n k). Proof. intros; unfold xorimm. - case (Int.eq (high_u n) Int.zero). reflexivity. - case (Int.eq (low_u n) Int.zero). reflexivity. reflexivity. + case (Int.eq (high_u n) Int.zero). TailNoLabel. + case (Int.eq (low_u n) Int.zero); TailNoLabel. Qed. -Hint Rewrite xorimm_label: labels. +Hint Resolve xorimm_label: labels. Remark rolm_label: - forall r1 r2 amount mask k, find_label lbl (rolm r1 r2 amount mask k) = find_label lbl k. + forall r1 r2 amount mask k, tail_nolabel k (rolm r1 r2 amount mask k). Proof. intros; unfold rolm. - case (is_rlw_mask mask). reflexivity. -Opaque Int.eq. - simpl. autorewrite with labels. auto. + case (is_rlw_mask mask); TailNoLabel. Qed. -Hint Rewrite rolm_label: labels. +Hint Resolve rolm_label: labels. Remark loadind_label: forall base ofs ty dst k c, - loadind base ofs ty dst k = OK c -> - find_label lbl c = find_label lbl k. + loadind base ofs ty dst k = OK c -> tail_nolabel k c. Proof. unfold loadind; intros. - destruct ty; destruct (Int.eq (high_s ofs) Int.zero); monadInv H; - autorewrite with labels; auto. + destruct ty; destruct (Int.eq (high_s ofs) Int.zero); + TailNoLabel; eapply tail_nolabel_trans; TailNoLabel. Qed. Remark storeind_label: forall base ofs ty src k c, - storeind base src ofs ty k = OK c -> - find_label lbl c = find_label lbl k. + storeind base src ofs ty k = OK c -> tail_nolabel k c. Proof. unfold storeind; intros. - destruct ty; destruct (Int.eq (high_s ofs) Int.zero); monadInv H; - autorewrite with labels; auto. + destruct ty; destruct (Int.eq (high_s ofs) Int.zero); + TailNoLabel; eapply tail_nolabel_trans; TailNoLabel. Qed. Remark floatcomp_label: - forall cmp r1 r2 k, find_label lbl (floatcomp cmp r1 r2 k) = find_label lbl k. + forall cmp r1 r2 k, tail_nolabel k (floatcomp cmp r1 r2 k). Proof. - intros; unfold floatcomp. destruct cmp; reflexivity. + intros; unfold floatcomp. destruct cmp; TailNoLabel. Qed. -Hint Rewrite floatcomp_label: labels. +Hint Resolve floatcomp_label: labels. Remark transl_cond_label: forall cond args k c, - transl_cond cond args k = OK c -> find_label lbl c = find_label lbl k. + transl_cond cond args k = OK c -> tail_nolabel k c. Proof. - unfold transl_cond; intros; destruct cond; - (destruct args; - [try discriminate | destruct args; - [try discriminate | destruct args; try discriminate]]); - monadInv H; autorewrite with labels; auto. - destruct (Int.eq (high_s i) Int.zero); inv EQ0; autorewrite with labels; auto. - destruct (Int.eq (high_u i) Int.zero); inv EQ0; autorewrite with labels; auto. + unfold transl_cond; intros; destruct cond; TailNoLabel; + eapply tail_nolabel_trans; TailNoLabel. Qed. Remark transl_cond_op_label: forall cond args r k c, - transl_cond_op cond args r k = OK c -> find_label lbl c = find_label lbl k. + transl_cond_op cond args r k = OK c -> tail_nolabel k c. Proof. unfold transl_cond_op; intros; destruct (classify_condition cond args); - monadInv H; auto. - erewrite transl_cond_label. 2: eauto. - destruct (snd (crbit_for_cond c0)); auto. + TailNoLabel. + eapply tail_nolabel_trans. eapply transl_cond_label; eauto. + destruct (snd (crbit_for_cond c0)); TailNoLabel. Qed. Remark transl_op_label: forall op args r k c, - transl_op op args r k = OK c -> find_label lbl c = find_label lbl k. + transl_op op args r k = OK c -> tail_nolabel k c. Proof. - unfold transl_op; intros; destruct op; try (eapply transl_cond_op_label; eauto; fail); - (destruct args; - [try discriminate | destruct args; - [try discriminate | destruct args; try discriminate]]); - try (monadInv H); autorewrite with labels; auto. - destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; auto. - destruct (symbol_is_small_data i i0); auto. - destruct (Int.eq (high_s i) Int.zero); autorewrite with labels; auto. - destruct (Int.eq (high_s i) Int.zero); autorewrite with labels; auto. +Opaque Int.eq. + unfold transl_op; intros; destruct op; TailNoLabel. + destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel. + destruct (symbol_is_small_data i i0); TailNoLabel. + destruct (Int.eq (high_s i) Int.zero); TailNoLabel; eapply tail_nolabel_trans; TailNoLabel. + destruct (Int.eq (high_s i) Int.zero); TailNoLabel; eapply tail_nolabel_trans; TailNoLabel. + eapply transl_cond_op_label; eauto. Qed. Remark transl_memory_access_label: forall (mk1: constant -> ireg -> instruction) (mk2: ireg -> ireg -> instruction) addr args temp k c, transl_memory_access mk1 mk2 addr args temp k = OK c -> - (forall c r, is_label lbl (mk1 c r) = false) -> - (forall r1 r2, is_label lbl (mk2 r1 r2) = false) -> - find_label lbl c = find_label lbl k. + (forall c r, nolabel (mk1 c r)) -> + (forall r1 r2, nolabel (mk2 r1 r2)) -> + tail_nolabel k c. Proof. - unfold transl_memory_access; intros; destruct addr; - (destruct args; - [try discriminate | destruct args; - [try discriminate | destruct args; try discriminate]]); - monadInv H; autorewrite with labels; auto. - destruct (Int.eq (high_s i) Int.zero); simpl; rewrite H0; auto. - simpl; rewrite H1; auto. - destruct (symbol_is_small_data i i0); simpl; rewrite H0; auto. - simpl; rewrite H0; auto. - destruct (Int.eq (high_s i) Int.zero); simpl; rewrite H0; auto. + unfold transl_memory_access; intros; destruct addr; TailNoLabel. + destruct (Int.eq (high_s i) Int.zero); TailNoLabel. + destruct (symbol_is_small_data i i0); TailNoLabel. + destruct (Int.eq (high_s i) Int.zero); TailNoLabel. Qed. Lemma transl_instr_label: forall f i ep k c, transl_instr f i ep k = OK c -> - find_label lbl c = if Mach.is_label lbl i then Some k else find_label lbl k. + match i with Mlabel lbl => c = Plabel lbl :: k | _ => tail_nolabel k c end. Proof. - unfold transl_instr, Mach.is_label; intros; destruct i; try (monadInv H); - autorewrite with labels; auto. + unfold transl_instr; intros; destruct i; TailNoLabel. eapply loadind_label; eauto. eapply storeind_label; eauto. - destruct ep. eapply loadind_label; eauto. - monadInv H. transitivity (find_label lbl x); eapply loadind_label; eauto. + eapply loadind_label; eauto. + eapply tail_nolabel_trans; eapply loadind_label; eauto. eapply transl_op_label; eauto. - destruct m; monadInv H; rewrite (transl_memory_access_label _ _ _ _ _ _ _ EQ0); auto. - destruct m; monadInv H; rewrite (transl_memory_access_label _ _ _ _ _ _ _ EQ0); auto. - destruct s0; monadInv H; auto. - destruct s0; monadInv H; auto. - erewrite transl_cond_label. 2: eauto. destruct (snd (crbit_for_cond c0)); auto. + destruct m; monadInv H; (eapply tail_nolabel_trans; [eapply transl_memory_access_label; TailNoLabel|TailNoLabel]). + destruct m; monadInv H; eapply transl_memory_access_label; TailNoLabel. + destruct s0; monadInv H; TailNoLabel. + destruct s0; monadInv H; TailNoLabel. + eapply tail_nolabel_trans. eapply transl_cond_label; eauto. + destruct (snd (crbit_for_cond c0)); TailNoLabel. +Qed. + +Lemma transl_instr_label': + forall lbl f i ep k c, + transl_instr f i ep k = OK c -> + find_label lbl c = if Mach.is_label lbl i then Some k else find_label lbl k. +Proof. + intros. exploit transl_instr_label; eauto. + destruct i; try (intros [A B]; apply B). + intros. subst c. simpl. auto. Qed. Lemma transl_code_label: - forall f c ep tc, + forall lbl f c ep tc, transl_code f c ep = OK tc -> match Mach.find_label lbl c with | None => find_label lbl tc = None @@ -345,7 +301,7 @@ Lemma transl_code_label: Proof. induction c; simpl; intros. inv H. auto. - monadInv H. rewrite (transl_instr_label _ _ _ _ _ EQ0). + monadInv H. rewrite (transl_instr_label' lbl _ _ _ _ _ EQ0). generalize (Mach.is_label_correct lbl a). destruct (Mach.is_label lbl a); intros. subst a. simpl in EQ. exists x; auto. @@ -353,7 +309,7 @@ Proof. Qed. Lemma transl_find_label: - forall f tf, + forall lbl f tf, transf_function f = OK tf -> match Mach.find_label lbl f.(Mach.fn_code) with | None => find_label lbl tf = None @@ -361,8 +317,7 @@ Lemma transl_find_label: end. Proof. intros. monadInv H. destruct (zlt Int.max_unsigned (list_length_z x)); inv EQ0. - monadInv EQ. simpl. - eapply transl_code_label; eauto. + monadInv EQ. simpl. eapply transl_code_label; eauto. Qed. End TRANSL_LABEL. @@ -378,7 +333,7 @@ Lemma find_label_goto_label: Mach.find_label lbl f.(Mach.fn_code) = Some c' -> exists tc', exists rs', goto_label tf lbl rs m = Next rs' m - /\ transl_code_at_pc ge (rs' PC) f c' false tf tc' + /\ transl_code_at_pc ge (rs' PC) b f c' false tf tc' /\ forall r, r <> PC -> rs'#r = rs#r. Proof. intros. exploit (transl_find_label lbl f tf); eauto. rewrite H2. @@ -394,6 +349,21 @@ Proof. intros. apply Pregmap.gso; auto. Qed. +(** Existence of return addresses *) + +Lemma return_address_exists: + forall f sg ros c, is_tail (Mcall sg ros :: c) f.(Mach.fn_code) -> + exists ra, return_address_offset f c ra. +Proof. + intros. eapply Asmgenproof0.return_address_exists; eauto. +- intros. exploit transl_instr_label; eauto. + destruct i; try (intros [A B]; apply A). intros. subst c0. repeat constructor. +- intros. monadInv H0. + destruct (zlt Int.max_unsigned (list_length_z x)); inv EQ0. monadInv EQ. + exists x; exists false; split; auto. unfold fn_code. repeat constructor. +- exact transf_function_no_overflow. +Qed. + (** * Proof of semantic preservation *) (** Semantic preservation is proved using simulation diagrams @@ -414,49 +384,49 @@ Qed. Inductive match_states: Mach.state -> Asm.state -> Prop := | match_states_intro: - forall s f sp c ep ms m m' rs tf tc ra - (STACKS: match_stack ge s m m' ra sp) + forall s fb sp c ep ms m m' rs f tf tc + (STACKS: match_stack ge s) + (FIND: Genv.find_funct_ptr ge fb = Some (Internal f)) (MEXT: Mem.extends m m') - (AT: transl_code_at_pc ge (rs PC) f c ep tf tc) - (AG: agree ms (Vptr sp Int.zero) rs) - (RSA: retaddr_stored_at m m' sp (Int.unsigned f.(fn_retaddr_ofs)) ra) + (AT: transl_code_at_pc ge (rs PC) fb f c ep tf tc) + (AG: agree ms sp rs) (DXP: ep = true -> rs#GPR11 = parent_sp s), - match_states (Mach.State s f (Vptr sp Int.zero) c ms m) + match_states (Mach.State s fb sp c ms m) (Asm.State rs m') | match_states_call: - forall s fd ms m m' rs fb - (STACKS: match_stack ge s m m' (rs LR) (Mem.nextblock m)) + forall s fb ms m m' rs + (STACKS: match_stack ge s) (MEXT: Mem.extends m m') (AG: agree ms (parent_sp s) rs) (ATPC: rs PC = Vptr fb Int.zero) - (FUNCT: Genv.find_funct_ptr ge fb = Some fd) - (WTRA: Val.has_type (rs LR) Tint), - match_states (Mach.Callstate s fd ms m) + (ATLR: rs RA = parent_ra s), + match_states (Mach.Callstate s fb ms m) (Asm.State rs m') | match_states_return: forall s ms m m' rs - (STACKS: match_stack ge s m m' (rs PC) (Mem.nextblock m)) + (STACKS: match_stack ge s) (MEXT: Mem.extends m m') - (AG: agree ms (parent_sp s) rs), + (AG: agree ms (parent_sp s) rs) + (ATPC: rs PC = parent_ra s), match_states (Mach.Returnstate s ms m) (Asm.State rs m'). Lemma exec_straight_steps: - forall s f rs1 i c ep tf tc m1' m2 m2' sp ms2 ra, - match_stack ge s m2 m2' ra sp -> + forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2, + match_stack ge s -> Mem.extends m2 m2' -> - retaddr_stored_at m2 m2' sp (Int.unsigned f.(fn_retaddr_ofs)) ra -> - transl_code_at_pc ge (rs1 PC) f (i :: c) ep tf tc -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> + transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc -> (forall k c (TR: transl_instr f i ep k = OK c), exists rs2, exec_straight tge tf c rs1 m1' k rs2 m2' - /\ agree ms2 (Vptr sp Int.zero) rs2 + /\ agree ms2 sp rs2 /\ (r11_is_parent ep i = true -> rs2#GPR11 = parent_sp s)) -> exists st', plus step tge (State rs1 m1') E0 st' /\ - match_states (Mach.State s f (Vptr sp Int.zero) c ms2 m2) st'. + match_states (Mach.State s fb sp c ms2 m2) st'. Proof. - intros. inversion H2; subst. monadInv H7. + intros. inversion H2. subst. monadInv H7. exploit H3; eauto. intros [rs2 [A [B C]]]. exists (State rs2 m2'); split. eapply exec_straight_exec; eauto. @@ -464,23 +434,23 @@ Proof. Qed. Lemma exec_straight_steps_goto: - forall s f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c' ra, - match_stack ge s m2 m2' ra sp -> + forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2 lbl c', + match_stack ge s -> Mem.extends m2 m2' -> - retaddr_stored_at m2 m2' sp (Int.unsigned f.(fn_retaddr_ofs)) ra -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> Mach.find_label lbl f.(Mach.fn_code) = Some c' -> - transl_code_at_pc ge (rs1 PC) f (i :: c) ep tf tc -> + transl_code_at_pc ge (rs1 PC) fb f (i :: c) ep tf tc -> r11_is_parent ep i = false -> (forall k c (TR: transl_instr f i ep k = OK c), exists jmp, exists k', exists rs2, exec_straight tge tf c rs1 m1' (jmp :: k') rs2 m2' - /\ agree ms2 (Vptr sp Int.zero) rs2 + /\ agree ms2 sp rs2 /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2') -> exists st', plus step tge (State rs1 m1') E0 st' /\ - match_states (Mach.State s f (Vptr sp Int.zero) c' ms2 m2) st'. + match_states (Mach.State s fb sp c' ms2 m2) st'. Proof. - intros. inversion H3; subst. monadInv H9. + intros. inversion H3. subst. monadInv H9. exploit H5; eauto. intros [jmp [k' [rs2 [A [B C]]]]]. generalize (functions_transl _ _ _ H7 H8); intro FN. generalize (transf_function_no_overflow _ _ H8); intro NOOV. @@ -524,7 +494,7 @@ Qed. (** This is the simulation diagram. We prove it by case analysis on the Mach transition. *) Theorem step_simulation: - forall S1 t S2, Mach.step ge S1 t S2 -> + forall S1 t S2, Mach.step return_address_offset ge S1 t S2 -> forall S1' (MS: match_states S1 S1'), (exists S2', plus step tge S1' t S2' /\ match_states S2 S2') \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat. @@ -551,8 +521,6 @@ Proof. assert (Val.lessdef (rs src) (rs0 (preg_of src))). eapply preg_val; eauto. exploit Mem.storev_extends; eauto. intros [m2' [A B]]. left; eapply exec_straight_steps; eauto. - eapply match_stack_storev; eauto. - eapply retaddr_stored_at_storev; eauto. rewrite (sp_val _ _ _ AG) in A. intros. simpl in TR. exploit storeind_correct; eauto with asmgen. intros [rs' [P Q]]. exists rs'; split. eauto. @@ -560,11 +528,12 @@ Proof. simpl; intros. rewrite Q; auto with asmgen. - (* Mgetparam *) + assert (f0 = f) by congruence; subst f0. unfold load_stack in *. - exploit Mem.loadv_extends. eauto. eexact H. auto. + exploit Mem.loadv_extends. eauto. eexact H0. auto. intros [parent' [A B]]. rewrite (sp_val _ _ _ AG) in A. exploit lessdef_parent_sp; eauto. clear B; intros B; subst parent'. - exploit Mem.loadv_extends. eauto. eexact H0. auto. + exploit Mem.loadv_extends. eauto. eexact H1. auto. intros [v' [C D]]. Opaque loadind. left; eapply exec_straight_steps; eauto; intros. @@ -591,7 +560,7 @@ Opaque loadind. apply preg_of_not_GPR11; auto. - (* Mop *) - assert (eval_operation tge (Vptr sp0 Int.zero) op rs##args m = Some v). + assert (eval_operation tge sp op rs##args m = Some v). rewrite <- H. apply eval_operation_preserved. exact symbols_preserved. exploit eval_operation_lessdef. eapply preg_vals; eauto. eauto. eexact H0. intros [v' [A B]]. rewrite (sp_val _ _ _ AG) in A. @@ -602,7 +571,7 @@ Opaque loadind. rewrite R; auto. apply preg_of_not_GPR11; auto. - (* Mload *) - assert (eval_addressing tge (Vptr sp0 Int.zero) addr rs##args = Some a). + assert (eval_addressing tge sp addr rs##args = Some a). rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1. intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A. @@ -615,95 +584,83 @@ Opaque loadind. simpl; congruence. - (* Mstore *) - assert (eval_addressing tge (Vptr sp0 Int.zero) addr rs##args = Some a). + assert (eval_addressing tge sp addr rs##args = Some a). rewrite <- H. apply eval_addressing_preserved. exact symbols_preserved. exploit eval_addressing_lessdef. eapply preg_vals; eauto. eexact H1. intros [a' [A B]]. rewrite (sp_val _ _ _ AG) in A. assert (Val.lessdef (rs src) (rs0 (preg_of src))). eapply preg_val; eauto. exploit Mem.storev_extends; eauto. intros [m2' [C D]]. left; eapply exec_straight_steps; eauto. - eapply match_stack_storev; eauto. - eapply retaddr_stored_at_storev; eauto. intros. simpl in TR. exploit transl_store_correct; eauto. intros [rs2 [P Q]]. exists rs2; split. eauto. split. eapply agree_exten_temps; eauto. intros; auto with asmgen. simpl; congruence. - (* Mcall *) + assert (f0 = f) by congruence. subst f0. inv AT. assert (NOOV: list_length_z tf <= Int.max_unsigned). eapply transf_function_no_overflow; eauto. - destruct ros as [rf|fid]; simpl in H; monadInv H3. + destruct ros as [rf|fid]; simpl in H; monadInv H5. + (* Indirect call *) - exploit Genv.find_funct_inv; eauto. intros [bf EQ2]. - rewrite EQ2 in H; rewrite Genv.find_funct_find_funct_ptr in H. - assert (rs0 x0 = Vptr bf Int.zero). - exploit ireg_val; eauto. rewrite EQ2; intros LD; inv LD; auto. - generalize (code_tail_next_int _ _ _ _ NOOV H4). intro CT1. + assert (rs rf = Vptr f' Int.zero). + destruct (rs rf); try discriminate. + revert H; predSpec Int.eq Int.eq_spec i Int.zero; intros; congruence. + assert (rs0 x0 = Vptr f' Int.zero). + exploit ireg_val; eauto. rewrite H5; intros LD; inv LD; auto. + generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1. generalize (code_tail_next_int _ _ _ _ NOOV CT1). intro CT2. - assert (TCA: transl_code_at_pc ge (Vptr b (Int.add (Int.add ofs Int.one) Int.one)) f c false tf x). - econstructor; eauto. + assert (TCA: transl_code_at_pc ge (Vptr fb (Int.add (Int.add ofs Int.one) Int.one)) fb f c false tf x). + econstructor; eauto. + exploit return_address_offset_correct; eauto. intros; subst ra. left; econstructor; split. eapply plus_left. eapply exec_step_internal. eauto. eapply functions_transl; eauto. eapply find_instr_tail; eauto. simpl. eauto. - apply star_one. eapply exec_step_internal. Simpl. rewrite <- H0; simpl; eauto. + apply star_one. eapply exec_step_internal. Simpl. rewrite <- H2; simpl; eauto. eapply functions_transl; eauto. eapply find_instr_tail; eauto. simpl. eauto. traceEq. econstructor; eauto. - econstructor; eauto. - Simpl. rewrite <- H0; eexact TCA. - change (Mem.valid_block m sp0). eapply retaddr_stored_at_valid; eauto. + econstructor; eauto. + eapply agree_sp_def; eauto. simpl. eapply agree_exten; eauto. intros. Simpl. - Simpl. rewrite <- H0. exact I. + Simpl. rewrite <- H2. auto. + (* Direct call *) - destruct (Genv.find_symbol ge fid) as [bf|] eqn:FS; try discriminate. - generalize (code_tail_next_int _ _ _ _ NOOV H4). intro CT1. - assert (TCA: transl_code_at_pc ge (Vptr b (Int.add ofs Int.one)) f c false tf x). + generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1. + assert (TCA: transl_code_at_pc ge (Vptr fb (Int.add ofs Int.one)) fb f c false tf x). econstructor; eauto. + exploit return_address_offset_correct; eauto. intros; subst ra. left; econstructor; split. apply plus_one. eapply exec_step_internal. eauto. eapply functions_transl; eauto. eapply find_instr_tail; eauto. - simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite FS. eauto. + simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite H. eauto. econstructor; eauto. econstructor; eauto. - rewrite <- H0. eexact TCA. - change (Mem.valid_block m sp0). eapply retaddr_stored_at_valid; eauto. + eapply agree_sp_def; eauto. simpl. eapply agree_exten; eauto. intros. Simpl. - auto. - rewrite <- H0. exact I. + Simpl. rewrite <- H2. auto. - (* Mtailcall *) +Opaque Int.repr. + assert (f0 = f) by congruence. subst f0. inversion AT; subst. assert (NOOV: list_length_z tf <= Int.max_unsigned). - eapply transf_function_no_overflow; eauto. - rewrite (sp_val _ _ _ AG) in *. unfold load_stack in *. - exploit Mem.loadv_extends. eauto. eexact H0. auto. simpl. intros [parent' [A B]]. + eapply transf_function_no_overflow; eauto. exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [parent' [A B]]. + exploit Mem.loadv_extends. eauto. eexact H2. auto. simpl. intros [ra' [C D]]. exploit lessdef_parent_sp; eauto. intros. subst parent'. clear B. - assert (C: Mem.loadv Mint32 m'0 (Val.add (rs0 GPR1) (Vint (fn_retaddr_ofs f))) = Some ra). -Opaque Int.repr. - erewrite agree_sp; eauto. simpl. rewrite Int.add_zero_l. - eapply rsa_contains; eauto. - exploit retaddr_stored_at_can_free; eauto. intros [m2' [E F]]. - assert (M: match_stack ge s m'' m2' ra (Mem.nextblock m'')). - apply match_stack_change_bound with stk. - eapply match_stack_free_left; eauto. - eapply match_stack_free_left; eauto. - eapply match_stack_free_right; eauto. - omega. - apply Z.lt_le_incl. change (Mem.valid_block m'' stk). - eapply Mem.valid_block_free_1; eauto. eapply Mem.valid_block_free_1; eauto. - eapply retaddr_stored_at_valid; eauto. - destruct ros as [rf|fid]; simpl in H; monadInv H6. + exploit lessdef_parent_ra; eauto. intros. subst ra'. clear D. + exploit Mem.free_parallel_extends; eauto. intros [m2' [E F]]. + destruct ros as [rf|fid]; simpl in H; monadInv H7. + (* Indirect call *) - exploit Genv.find_funct_inv; eauto. intros [bf EQ2]. - rewrite EQ2 in H; rewrite Genv.find_funct_find_funct_ptr in H. - assert (rs0 x0 = Vptr bf Int.zero). - exploit ireg_val; eauto. rewrite EQ2; intros LD; inv LD; auto. - set (rs2 := nextinstr (rs0#CTR <- (Vptr bf Int.zero))). - set (rs3 := nextinstr (rs2#GPR0 <- ra)). - set (rs4 := nextinstr (rs3#LR <- ra)). + assert (rs rf = Vptr f' Int.zero). + destruct (rs rf); try discriminate. + revert H; predSpec Int.eq Int.eq_spec i Int.zero; intros; congruence. + assert (rs0 x0 = Vptr f' Int.zero). + exploit ireg_val; eauto. rewrite H7; intros LD; inv LD; auto. + set (rs2 := nextinstr (rs0#CTR <- (Vptr f' Int.zero))). + set (rs3 := nextinstr (rs2#GPR0 <- (parent_ra s))). + set (rs4 := nextinstr (rs3#LR <- (parent_ra s))). set (rs5 := nextinstr (rs4#GPR1 <- (parent_sp s))). set (rs6 := rs5#PC <- (rs5 CTR)). assert (exec_straight tge tf @@ -712,21 +669,23 @@ Opaque Int.repr. rs0 m'0 (Pbctr :: x) rs5 m2'). apply exec_straight_step with rs2 m'0. - simpl. rewrite H6. auto. auto. + simpl. rewrite H9. auto. auto. apply exec_straight_step with rs3 m'0. simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low. - change (rs2 GPR1) with (rs0 GPR1). rewrite C. auto. congruence. auto. + change (rs2 GPR1) with (rs0 GPR1). rewrite <- (sp_val _ _ _ AG). + simpl. rewrite C. auto. congruence. auto. apply exec_straight_step with rs4 m'0. simpl. reflexivity. reflexivity. apply exec_straight_one. - simpl. change (rs4 GPR1) with (rs0 GPR1). rewrite A. rewrite <- (sp_val _ _ _ AG). + simpl. change (rs4 GPR1) with (rs0 GPR1). rewrite <- (sp_val _ _ _ AG). + simpl. rewrite A. rewrite E. reflexivity. reflexivity. left; exists (State rs6 m2'); split. (* execution *) eapply plus_right'. eapply exec_straight_exec; eauto. econstructor. change (rs5 PC) with (Val.add (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone) Vone). - rewrite <- H3; simpl. eauto. + rewrite <- H4; simpl. eauto. eapply functions_transl; eauto. eapply find_instr_tail. repeat (eapply code_tail_next_int; auto). eauto. @@ -734,20 +693,17 @@ Opaque Int.repr. (* match states *) econstructor; eauto. Hint Resolve agree_nextinstr agree_set_other: asmgen. - assert (AG4: agree rs (Vptr stk Int.zero) rs4). + assert (AG4: agree rs (Vptr stk soff) rs4). unfold rs4, rs3, rs2; auto 10 with asmgen. assert (AG5: agree rs (parent_sp s) rs5). unfold rs5. apply agree_nextinstr. eapply agree_change_sp. eauto. eapply parent_sp_def; eauto. unfold rs6, rs5; auto 10 with asmgen. - reflexivity. - change (rs6 LR) with ra. eapply retaddr_stored_at_type; eauto. + (* Direct call *) - destruct (Genv.find_symbol ge fid) as [bf|] eqn:FS; try discriminate. - set (rs2 := nextinstr (rs0#GPR0 <- ra)). - set (rs3 := nextinstr (rs2#LR <- ra)). + set (rs2 := nextinstr (rs0#GPR0 <- (parent_ra s))). + set (rs3 := nextinstr (rs2#LR <- (parent_ra s))). set (rs4 := nextinstr (rs3#GPR1 <- (parent_sp s))). - set (rs5 := rs4#PC <- (Vptr bf Int.zero)). + set (rs5 := rs4#PC <- (Vptr f' Int.zero)). assert (exec_straight tge tf (Plwz GPR0 (Cint (fn_retaddr_ofs f)) GPR1 :: Pmtlr GPR0 :: Pfreeframe (fn_stacksize f) (fn_link_ofs f) :: Pbs fid :: x) @@ -755,33 +711,30 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen. (Pbs fid :: x) rs4 m2'). apply exec_straight_step with rs2 m'0. simpl. unfold load1. rewrite gpr_or_zero_not_zero. unfold const_low. - rewrite C. auto. congruence. auto. + rewrite <- (sp_val _ _ _ AG). simpl. rewrite C. auto. congruence. auto. apply exec_straight_step with rs3 m'0. simpl. reflexivity. reflexivity. apply exec_straight_one. - simpl. change (rs3 GPR1) with (rs0 GPR1). rewrite A. rewrite <- (sp_val _ _ _ AG). + simpl. change (rs3 GPR1) with (rs0 GPR1). rewrite <- (sp_val _ _ _ AG). simpl. rewrite A. rewrite E. reflexivity. reflexivity. left; exists (State rs5 m2'); split. (* execution *) eapply plus_right'. eapply exec_straight_exec; eauto. econstructor. change (rs4 PC) with (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone). - rewrite <- H3; simpl. eauto. + rewrite <- H4; simpl. eauto. eapply functions_transl; eauto. eapply find_instr_tail. repeat (eapply code_tail_next_int; auto). eauto. - simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite FS. auto. traceEq. + simpl. unfold symbol_offset. rewrite symbols_preserved. rewrite H. auto. traceEq. (* match states *) econstructor; eauto. -Hint Resolve agree_nextinstr agree_set_other: asmgen. - assert (AG3: agree rs (Vptr stk Int.zero) rs3). + assert (AG3: agree rs (Vptr stk soff) rs3). unfold rs3, rs2; auto 10 with asmgen. assert (AG4: agree rs (parent_sp s) rs4). unfold rs4. apply agree_nextinstr. eapply agree_change_sp. eauto. eapply parent_sp_def; eauto. unfold rs5; auto 10 with asmgen. - reflexivity. - change (rs5 LR) with ra. eapply retaddr_stored_at_type; eauto. - (* Mbuiltin *) inv AT. monadInv H3. @@ -795,16 +748,11 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. econstructor; eauto. - eapply match_stack_extcall; eauto. - intros; eapply external_call_max_perm; eauto. - instantiate (2 := tf); instantiate (1 := x). Simpl. rewrite <- H0. simpl. econstructor; eauto. eapply code_tail_next_int; eauto. apply agree_nextinstr. eapply agree_set_undef_mreg; eauto. rewrite Pregmap.gss. auto. intros. Simpl. - eapply retaddr_stored_at_extcall; eauto. - intros; eapply external_call_max_perm; eauto. congruence. - (* Mannot *) @@ -820,18 +768,15 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. eapply match_states_intro with (ep := false); eauto with coqlib. - eapply match_stack_extcall; eauto. - intros; eapply external_call_max_perm; eauto. unfold nextinstr. rewrite Pregmap.gss. rewrite <- H1; simpl. econstructor; eauto. eapply code_tail_next_int; eauto. apply agree_nextinstr. auto. - eapply retaddr_stored_at_extcall; eauto. - intros; eapply external_call_max_perm; eauto. congruence. - (* Mgoto *) - inv AT. monadInv H3. + assert (f0 = f) by congruence. subst f0. + inv AT. monadInv H4. exploit find_label_goto_label; eauto. intros [tc' [rs' [GOTO [AT2 INV]]]]. left; exists (State rs' m'); split. apply plus_one. econstructor; eauto. @@ -843,6 +788,7 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen. congruence. - (* Mcond true *) + assert (f0 = f) by congruence. subst f0. exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC. left; eapply exec_straight_steps_goto; eauto. intros. simpl in TR. @@ -873,9 +819,10 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen. simpl. congruence. - (* Mjumptable *) - inv AT. monadInv H5. + assert (f0 = f) by congruence. subst f0. + inv AT. monadInv H6. exploit functions_transl; eauto. intro FN. - generalize (transf_function_no_overflow _ _ H4); intro NOOV. + generalize (transf_function_no_overflow _ _ H5); intro NOOV. exploit find_label_goto_label. eauto. eauto. instantiate (2 := rs0#GPR12 <- Vundef #CTR <- Vundef). Simpl. eauto. @@ -885,36 +832,27 @@ Hint Resolve agree_nextinstr agree_set_other: asmgen. left; econstructor; split. apply plus_one. econstructor; eauto. eapply find_instr_tail; eauto. - simpl. rewrite <- H8. unfold Mach.label in H0; unfold label; rewrite H0. eexact A. + simpl. rewrite <- H9. unfold Mach.label in H0; unfold label; rewrite H0. eexact A. econstructor; eauto. eapply agree_exten_temps; eauto. intros. rewrite C; auto with asmgen. Simpl. congruence. - (* Mreturn *) - inversion AT; subst. + assert (f0 = f) by congruence. subst f0. + inversion AT; subst. assert (NOOV: list_length_z tf <= Int.max_unsigned). eapply transf_function_no_overflow; eauto. rewrite (sp_val _ _ _ AG) in *. unfold load_stack in *. - exploit Mem.loadv_extends. eauto. eexact H. auto. simpl. intros [parent' [A B]]. + exploit Mem.loadv_extends. eauto. eexact H0. auto. simpl. intros [parent' [A B]]. exploit lessdef_parent_sp; eauto. intros. subst parent'. clear B. - assert (C: Mem.loadv Mint32 m'0 (Val.add (rs0 GPR1) (Vint (fn_retaddr_ofs f))) = Some ra). -Opaque Int.repr. - erewrite agree_sp; eauto. simpl. rewrite Int.add_zero_l. - eapply rsa_contains; eauto. - exploit retaddr_stored_at_can_free; eauto. intros [m2' [E F]]. - assert (M: match_stack ge s m'' m2' ra (Mem.nextblock m'')). - apply match_stack_change_bound with stk. - eapply match_stack_free_left; eauto. - eapply match_stack_free_left; eauto. - eapply match_stack_free_right; eauto. omega. - apply Z.lt_le_incl. change (Mem.valid_block m'' stk). - eapply Mem.valid_block_free_1; eauto. eapply Mem.valid_block_free_1; eauto. - eapply retaddr_stored_at_valid; eauto. - monadInv H5. - set (rs2 := nextinstr (rs0#GPR0 <- ra)). - set (rs3 := nextinstr (rs2#LR <- ra)). + exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [ra' [C D]]. + exploit lessdef_parent_ra; eauto. intros. subst ra'. clear D. + exploit Mem.free_parallel_extends; eauto. intros [m2' [E F]]. + monadInv H6. + set (rs2 := nextinstr (rs0#GPR0 <- (parent_ra s))). + set (rs3 := nextinstr (rs2#LR <- (parent_ra s))). set (rs4 := nextinstr (rs3#GPR1 <- (parent_sp s))). - set (rs5 := rs4#PC <- ra). + set (rs5 := rs4#PC <- (parent_ra s)). assert (exec_straight tge tf (Plwz GPR0 (Cint (fn_retaddr_ofs f)) GPR1 :: Pmtlr GPR0 @@ -932,7 +870,7 @@ Opaque Int.repr. eapply exec_straight_exec; eauto. econstructor. change (rs4 PC) with (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone). - rewrite <- H2. simpl. eauto. + rewrite <- H3. simpl. eauto. eapply functions_transl; eauto. eapply find_instr_tail. eapply code_tail_next_int; auto. @@ -941,7 +879,7 @@ Opaque Int.repr. reflexivity. traceEq. (* match states *) econstructor; eauto. - assert (AG3: agree rs (Vptr stk Int.zero) rs3). + assert (AG3: agree rs (Vptr stk soff) rs3). unfold rs3, rs2; auto 10 with asmgen. assert (AG4: agree rs (parent_sp s) rs4). unfold rs4. apply agree_nextinstr. eapply agree_change_sp; eauto. @@ -955,12 +893,10 @@ Opaque Int.repr. unfold store_stack in *. exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. intros [m1' [C D]]. - assert (E: Mem.extends m2 m1') by (eapply Mem.free_left_extends; eauto). - exploit Mem.storev_extends. eexact E. eexact H1. eauto. eauto. + exploit Mem.storev_extends. eexact D. eexact H1. eauto. eauto. intros [m2' [F G]]. - exploit retaddr_stored_at_can_alloc. eexact H. eauto. eauto. eauto. eauto. - auto. auto. auto. auto. eauto. - intros [m3' [P [Q R]]]. + exploit Mem.storev_extends. eexact G. eexact H2. eauto. eauto. + intros [m3' [P Q]]. (* Execution of function prologue *) monadInv EQ0. set (rs2 := nextinstr (rs0#GPR1 <- sp #GPR0 <- Vundef)). @@ -977,23 +913,11 @@ Opaque Int.repr. simpl. auto. simpl. unfold store1. rewrite gpr_or_zero_not_zero. change (rs3 GPR1) with sp. change (rs3 GPR0) with (rs0 LR). simpl. - rewrite Int.add_zero_l. rewrite P. auto. congruence. + rewrite Int.add_zero_l. simpl in P. rewrite Int.add_zero_l in P. rewrite ATLR. rewrite P. auto. congruence. auto. auto. auto. left; exists (State rs4 m3'); split. eapply exec_straight_steps_1; eauto. unfold fn_code; omega. constructor. econstructor; eauto. - assert (STK: stk = Mem.nextblock m) by (eapply Mem.alloc_result; eauto). - rewrite <- STK in STACKS. simpl in F. simpl in H1. - eapply match_stack_invariant; eauto. - intros. eapply Mem.perm_alloc_4; eauto. eapply Mem.perm_free_3; eauto. - eapply Mem.perm_store_2; eauto. unfold block; omega. - intros. eapply Mem.perm_store_1; eauto. eapply Mem.perm_store_1; eauto. - eapply Mem.perm_alloc_1; eauto. - intros. erewrite Mem.load_store_other. 2: eauto. - erewrite Mem.load_store_other. 2: eauto. - eapply Mem.load_alloc_other; eauto. - left; unfold block; omega. - left; unfold block; omega. change (rs4 PC) with (Val.add (Val.add (Val.add (rs0 PC) Vone) Vone) Vone). rewrite ATPC. simpl. constructor; eauto. subst x. unfold fn_code. eapply code_tail_next_int. omega. @@ -1019,10 +943,6 @@ Opaque Int.repr. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact varinfo_preserved. econstructor; eauto. - rewrite Pregmap.gss. apply match_stack_change_bound with (Mem.nextblock m). - eapply match_stack_extcall; eauto. - intros. eapply external_call_max_perm; eauto. - eapply external_call_nextblock; eauto. unfold loc_external_result. eapply agree_set_mreg; eauto. rewrite Pregmap.gso; auto with asmgen. rewrite Pregmap.gss. auto. @@ -1030,7 +950,8 @@ Opaque Int.repr. - (* return *) inv STACKS. simpl in *. - right. split. omega. split. auto. + right. split. omega. split. auto. + rewrite <- ATPC in H5. econstructor; eauto. congruence. Qed. @@ -1039,21 +960,19 @@ Lemma transf_initial_states: exists st2, Asm.initial_state tprog st2 /\ match_states st1 st2. Proof. intros. inversion H. unfold ge0 in *. - exploit functions_translated; eauto. intros [tf [A B]]. econstructor; split. econstructor. eapply Genv.init_mem_transf_partial; eauto. replace (symbol_offset (Genv.globalenv tprog) (prog_main tprog) Int.zero) - with (Vptr b Int.zero). + with (Vptr fb Int.zero). econstructor; eauto. constructor. apply Mem.extends_refl. - split. auto. intros. rewrite Regmap.gi. auto. - reflexivity. - exact I. + split. auto. simpl. congruence. intros. rewrite Regmap.gi. auto. unfold symbol_offset. - rewrite (transform_partial_program_main _ _ TRANSF). - rewrite symbols_preserved. unfold ge; rewrite H1. auto. + rewrite (transform_partial_program_main _ _ TRANSF). + rewrite symbols_preserved. + unfold ge; rewrite H1. auto. Qed. Lemma transf_final_states: @@ -1067,7 +986,7 @@ Proof. Qed. Theorem transf_program_correct: - forward_simulation (Mach.semantics prog) (Asm.semantics tprog). + forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog). Proof. eapply forward_simulation_star with (measure := measure). eexact symbols_preserved. -- cgit v1.2.3