diff options
Diffstat (limited to 'aarch64/Asmblockgenproof.v')
| -rw-r--r-- | aarch64/Asmblockgenproof.v | 2184 |
1 files changed, 1280 insertions, 904 deletions
diff --git a/aarch64/Asmblockgenproof.v b/aarch64/Asmblockgenproof.v index 41082772..0b1123f7 100644 --- a/aarch64/Asmblockgenproof.v +++ b/aarch64/Asmblockgenproof.v @@ -1,12 +1,24 @@ -(** Correctness proof for aarch64/Asmblock generation: main proof. -CURRENTLY A STUB ! -*) +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* Léo Gourdin UGA, VERIMAG *) +(* *) +(* Copyright Kalray. Copyright VERIMAG. All rights reserved. *) +(* This file is distributed under the terms of the INRIA *) +(* Non-Commercial License Agreement. *) +(* *) +(* *************************************************************) Require Import Coqlib Errors. Require Import Integers Floats AST Linking. Require Import Values Memory Events Globalenvs Smallstep. -Require Import Op Locations Machblock Conventions PseudoAsmblock Asmblock IterList. -Require Import PseudoAsmblockproof Asmblockgen. +Require Import Op Locations Machblock Conventions Asmblock IterList. +Require Import Asmblockgen Asmblockgenproof0 Asmblockgenproof1 Asmblockprops. Module MB := Machblock. Module AB := Asmblock. @@ -20,13 +32,8 @@ Proof. intros. eapply match_transform_partial_program; eauto. Qed. -Parameter next: MB.function -> Z -> Z. - Section PRESERVATION. -Lemma next_progress: forall (f:MB.function) (pos:Z), (pos < (next f pos))%Z. -Admitted. - Variable lk: aarch64_linker. Variable prog: Machblock.program. Variable tprog: Asmblock.program. @@ -34,63 +41,6 @@ Hypothesis TRANSF: match_prog prog tprog. Let ge := Genv.globalenv prog. Let tge := Genv.globalenv tprog. - -Hypothesis symbol_high_low: forall (id: ident) (ofs: ptrofs), - Val.addl (symbol_high lk id ofs) (symbol_low lk id ofs) = Genv.symbol_address tge id ofs. - -Lemma functions_bound_max_pos: forall fb f, - Genv.find_funct_ptr ge fb = Some (Internal f) -> - (max_pos next f) <= Ptrofs.max_unsigned. -Admitted. - - - -Lemma transf_program_correct: - forward_simulation (PseudoAsmblock.semantics next prog) (AB.semantics lk tprog). -Admitted. - -End PRESERVATION. - - -(* ORIGINAL aarch64/Asmgenproof file that needs to be adapted - -(* *********************************************************************) -(* *) -(* The Compcert verified compiler *) -(* *) -(* Xavier Leroy, Collège de France and INRIA Paris *) -(* *) -(* Copyright Institut National de Recherche en Informatique et en *) -(* Automatique. All rights reserved. This file is distributed *) -(* under the terms of the INRIA Non-Commercial License Agreement. *) -(* *) -(* *********************************************************************) - -(** Correctness proof for AArch64 code generation. *) - -Require Import Coqlib Errors. -Require Import Integers Floats AST Linking. -Require Import Values Memory Events Globalenvs Smallstep. -Require Import Op Locations Mach Conventions Asm. -Require Import Asmgen Asmgenproof0 Asmgenproof1. - -Definition match_prog (p: Mach.program) (tp: Asm.program) := - match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp. - -Lemma transf_program_match: - forall p tp, transf_program p = OK tp -> match_prog p tp. -Proof. - intros. eapply match_transform_partial_program; eauto. -Qed. - -Section PRESERVATION. - -Variable prog: Mach.program. -Variable tprog: Asm.program. -Hypothesis TRANSF: match_prog prog tprog. -Let ge := Genv.globalenv prog. -Let tge := Genv.globalenv tprog. - Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. Proof (Genv.find_symbol_match TRANSF). @@ -116,924 +66,1334 @@ Proof. monadInv B. rewrite H0 in EQ; inv EQ; auto. Qed. -(** * Properties of control flow *) - Lemma transf_function_no_overflow: forall f tf, - transf_function f = OK tf -> list_length_z tf.(fn_code) <= Ptrofs.max_unsigned. + transf_function f = OK tf -> size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned. Proof. - intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0. + intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0. omega. Qed. -Lemma exec_straight_exec: - 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. - intros. inv H. - eapply exec_straight_steps_1; eauto. - eapply transf_function_no_overflow; eauto. - eapply functions_transl; eauto. -Qed. +Hypothesis symbol_high_low: forall (id: ident) (ofs: ptrofs), + Val.addl (symbol_high lk id ofs) (symbol_low lk id ofs) = Genv.symbol_address tge id ofs. -Lemma exec_straight_at: - 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) fb f c' ep' tf tc'. -Proof. - intros. inv H. - exploit exec_straight_steps_2; eauto. - eapply transf_function_no_overflow; eauto. - eapply functions_transl; eauto. - intros [ofs' [PC' CT']]. - rewrite PC'. constructor; auto. -Qed. +(** * Proof of semantic preservation *) -(** The following lemmas show that the translation from Mach to Asm - preserves labels, in the sense that the following diagram commutes: +(** Semantic preservation is proved using a complex simulation diagram + of the following form. << - translation - Mach code ------------------------ Asm instr sequence - | | - | Mach.find_label lbl find_label lbl | - | | - v v - Mach code tail ------------------- Asm instr seq tail - translation + MB.step + ----------------------------------------> + header body exit + st1 -----> st2 -----> st3 ------------------> st4 + | | | | + | (A) | (B) | (C) | + match_codestate | | | | + | header | body1 | body2 | match_states + cs1 -----> cs2 -----> cs3 ------> cs4 | + | / \ exit | + match_asmstate | --------------- --->--- | + | / match_asmstate \ | + st'1 ---------------------------------------> st'2 + AB.step * >> - The proof demands many boring lemmas showing that Asm constructor - functions do not introduce new labels. + The invariant between each MB.step/AB.step is the [match_states] predicate below. + However, we also need to introduce an intermediary state [Codestate] which allows + us to reason on a finer grain, executing header, body and exit separately. + + This [Codestate] consists in a state like [Asmblock.State], except that the + code is directly stored in the state, much like [Machblock.State]. It also features + additional useful elements to keep track of while executing a bblock. *) -Section TRANSL_LABEL. +Inductive match_states: Machblock.state -> Asm.state -> Prop := + | match_states_intro: + 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) fb f c ep tf tc) + (AG: agree ms sp rs) + (DXP: ep = true -> rs#X29 = parent_sp s), + match_states (Machblock.State s fb sp c ms m) + (Asm.State rs m') + | match_states_call: + 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 Ptrofs.zero) + (ATLR: rs RA = parent_ra s), + match_states (Machblock.Callstate s fb ms m) + (Asm.State rs m') + | match_states_return: + forall s ms m m' rs + (STACKS: match_stack ge s) + (MEXT: Mem.extends m m') + (AG: agree ms (parent_sp s) rs) + (ATPC: rs PC = parent_ra s), + match_states (Machblock.Returnstate s ms m) + (Asm.State rs m'). + +Section TRANSL_LABEL. (* Lemmas on translation of MB.is_label into AB.is_label *) -Remark loadimm_z_label: forall sz rd l k, tail_nolabel k (loadimm_z sz rd l k). -Proof. - intros; destruct l as [ | [n1 p1] l]; simpl; TailNoLabel. - induction l as [ | [n p] l]; simpl; TailNoLabel. +Lemma cons_bblocks_label: + forall hd bdy ex tbb tc, + cons_bblocks hd bdy ex = tbb::tc -> + header tbb = hd. +Proof. + intros until tc. intros CONSB. unfold cons_bblocks in CONSB. + destruct ex; try destruct bdy; try destruct c; try destruct i. + all: inv CONSB; simpl; auto. Qed. -Remark loadimm_n_label: forall sz rd l k, tail_nolabel k (loadimm_n sz rd l k). -Proof. - intros; destruct l as [ | [n1 p1] l]; simpl; TailNoLabel. - induction l as [ | [n p] l]; simpl; TailNoLabel. +Lemma cons_bblocks_label2: + forall hd bdy ex tbb1 tbb2, + cons_bblocks hd bdy ex = tbb1::tbb2::nil -> + header tbb2 = nil. +Proof. + intros until tbb2. intros CONSB. unfold cons_bblocks in CONSB. + destruct ex; try destruct bdy; try destruct c; try destruct i. + all: inv CONSB; simpl; auto. Qed. -Remark loadimm_label: forall sz rd n k, tail_nolabel k (loadimm sz rd n k). +Remark in_dec_transl: + forall lbl hd, + (if in_dec lbl hd then true else false) = (if MB.in_dec lbl hd then true else false). Proof. - unfold loadimm; intros. destruct Nat.leb; [apply loadimm_z_label|apply loadimm_n_label]. + intros. destruct (in_dec lbl hd), (MB.in_dec lbl hd). all: tauto. Qed. -Hint Resolve loadimm_label: labels. -Remark loadimm32_label: forall r n k, tail_nolabel k (loadimm32 r n k). +Lemma transl_is_label: + forall lbl bb tbb f ep tc, + transl_block f bb ep = OK (tbb::tc) -> + is_label lbl tbb = MB.is_label lbl bb. Proof. - unfold loadimm32; intros. destruct (is_logical_imm32 n); TailNoLabel. + intros until tc. intros TLB. + destruct tbb as [thd tbdy tex]; simpl in *. + monadInv TLB. + unfold is_label. simpl. + apply cons_bblocks_label in H0. simpl in H0. subst. + rewrite in_dec_transl. auto. Qed. -Hint Resolve loadimm32_label: labels. -Remark loadimm64_label: forall r n k, tail_nolabel k (loadimm64 r n k). +Lemma transl_is_label_false2: + forall lbl bb f ep tbb1 tbb2, + transl_block f bb ep = OK (tbb1::tbb2::nil) -> + is_label lbl tbb2 = false. Proof. - unfold loadimm64; intros. destruct (is_logical_imm64 n); TailNoLabel. + intros until tbb2. intros TLB. + destruct tbb2 as [thd tbdy tex]; simpl in *. + monadInv TLB. apply cons_bblocks_label2 in H0. simpl in H0. subst. + apply is_label_correct_false. simpl. auto. Qed. -Hint Resolve loadimm64_label: labels. -Remark addimm_aux: forall insn rd r1 n k, - (forall rd r1 n, nolabel (insn rd r1 n)) -> - tail_nolabel k (addimm_aux insn rd r1 n k). +Lemma transl_block_nonil: + forall f c ep tc, + transl_block f c ep = OK tc -> + tc <> nil. Proof. - unfold addimm_aux; intros. - destruct Z.eqb. TailNoLabel. destruct Z.eqb; TailNoLabel. + intros. monadInv H. unfold cons_bblocks. + destruct x0; try destruct (x1 @@ x); try destruct c0; try destruct i. + all: discriminate. Qed. -Remark addimm32_label: forall rd r1 n k, tail_nolabel k (addimm32 rd r1 n k). +Lemma transl_block_limit: forall f bb ep tbb1 tbb2 tbb3 tc, + ~transl_block f bb ep = OK (tbb1 :: tbb2 :: tbb3 :: tc). Proof. - unfold addimm32; intros. - destruct Int.eq. apply addimm_aux; intros; red; auto. - destruct Int.eq. apply addimm_aux; intros; red; auto. - destruct Int.lt; eapply tail_nolabel_trans; TailNoLabel. + intros. intro. monadInv H. + unfold cons_bblocks in H0. + destruct x0; try destruct (x1 @@ x); try destruct c0; try destruct i. + all: discriminate. Qed. -Hint Resolve addimm32_label: labels. -Remark addimm64_label: forall rd r1 n k, tail_nolabel k (addimm64 rd r1 n k). +Lemma find_label_transl_false: + forall x f lbl bb ep x', + transl_block f bb ep = OK x -> + MB.is_label lbl bb = false -> + find_label lbl (x++x') = find_label lbl x'. Proof. - unfold addimm64; intros. - destruct Int64.eq. apply addimm_aux; intros; red; auto. - destruct Int64.eq. apply addimm_aux; intros; red; auto. - destruct Int64.lt; eapply tail_nolabel_trans; TailNoLabel. + intros until x'. intros TLB MBis; simpl; auto. + destruct x as [|x0 x1]; simpl; auto. + destruct x1 as [|x1 x2]; simpl; auto. + - erewrite <- transl_is_label in MBis; eauto. rewrite MBis. auto. + - destruct x2 as [|x2 x3]; simpl; auto. + + erewrite <- transl_is_label in MBis; eauto. rewrite MBis. + erewrite transl_is_label_false2; eauto. + + apply transl_block_limit in TLB. destruct TLB. Qed. -Hint Resolve addimm64_label: labels. -Remark logicalimm32_label: forall insn1 insn2 rd r1 n k, - (forall rd r1 n, nolabel (insn1 rd r1 n)) -> - (forall rd r1 r2 s, nolabel (insn2 rd r1 r2 s)) -> - tail_nolabel k (logicalimm32 insn1 insn2 rd r1 n k). +Lemma transl_blocks_label: + forall lbl f c tc ep, + transl_blocks f c ep = OK tc -> + match MB.find_label lbl c with + | None => find_label lbl tc = None + | Some c' => exists tc', find_label lbl tc = Some tc' /\ transl_blocks f c' false = OK tc' + end. Proof. - unfold logicalimm32; intros. - destruct (is_logical_imm32 n). TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. + induction c; simpl; intros. + inv H. auto. + monadInv H. + destruct (MB.is_label lbl a) eqn:MBis. + - destruct x as [|tbb tc]. { apply transl_block_nonil in EQ. contradiction. } + simpl find_label. exploit transl_is_label; eauto. intros ABis. rewrite MBis in ABis. + rewrite ABis. + eexists. eexists. split; eauto. simpl transl_blocks. + assert (MB.header a <> nil). + { apply MB.is_label_correct_true in MBis. + destruct (MB.header a). contradiction. discriminate. } + destruct (MB.header a); try contradiction. + rewrite EQ. simpl. rewrite EQ1. simpl. auto. + - apply IHc in EQ1. destruct (MB.find_label lbl c). + + destruct EQ1 as (tc' & FIND & TLBS). exists tc'; eexists; auto. + erewrite find_label_transl_false; eauto. + + erewrite find_label_transl_false; eauto. Qed. -Remark logicalimm64_label: forall insn1 insn2 rd r1 n k, - (forall rd r1 n, nolabel (insn1 rd r1 n)) -> - (forall rd r1 r2 s, nolabel (insn2 rd r1 r2 s)) -> - tail_nolabel k (logicalimm64 insn1 insn2 rd r1 n k). +Lemma find_label_nil: + forall bb lbl c, + header bb = nil -> + find_label lbl (bb::c) = find_label lbl c. Proof. - unfold logicalimm64; intros. - destruct (is_logical_imm64 n). TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. + intros. destruct bb as [hd bdy ex]; simpl in *. subst. + assert (is_label lbl {| AB.header := nil; AB.body := bdy; AB.exit := ex; AB.correct := correct |} = false). + { erewrite <- is_label_correct_false. simpl. auto. } + rewrite H. auto. Qed. -Remark move_extended_label: forall rd r1 ex a k, tail_nolabel k (move_extended rd r1 ex a k). +Theorem transl_find_label: + forall lbl f tf, + transf_function f = OK tf -> + match MB.find_label lbl f.(MB.fn_code) with + | None => find_label lbl tf.(fn_blocks) = None + | Some c => exists tc, find_label lbl tf.(fn_blocks) = Some tc /\ transl_blocks f c false = OK tc + end. Proof. - unfold move_extended, move_extended_base; intros. destruct Int.eq, ex; TailNoLabel. + intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x))); inv EQ0. clear g. + monadInv EQ. unfold make_prologue. simpl fn_blocks. repeat (rewrite find_label_nil); simpl; auto. + eapply transl_blocks_label; eauto. Qed. -Hint Resolve move_extended_label: labels. -Remark arith_extended_label: forall insnX insnS rd r1 r2 ex a k, - (forall rd r1 r2 x, nolabel (insnX rd r1 r2 x)) -> - (forall rd r1 r2 s, nolabel (insnS rd r1 r2 s)) -> - tail_nolabel k (arith_extended insnX insnS rd r1 r2 ex a k). +End TRANSL_LABEL. + +(** A valid branch in a piece of Machblock code translates to a valid ``go to'' + transition in the generated Asmblock code. *) + +Lemma find_label_goto_label: + forall f tf lbl rs m c' b ofs, + Genv.find_funct_ptr ge b = Some (Internal f) -> + transf_function f = OK tf -> + rs PC = Vptr b ofs -> + MB.find_label lbl f.(MB.fn_code) = Some c' -> + exists tc', exists rs', + goto_label tf lbl rs m = Next rs' m + /\ transl_code_at_pc ge (rs' PC) b f c' false tf tc' + /\ forall r, r <> PC -> rs'#r = rs#r. Proof. - unfold arith_extended; intros. destruct Int.ltu. - TailNoLabel. - destruct ex; simpl; TailNoLabel. + intros. exploit (transl_find_label lbl f tf); eauto. rewrite H2. + intros (tc & A & B). + exploit label_pos_code_tail; eauto. instantiate (1 := 0). + intros [pos' [P [Q R]]]. + exists tc; exists (rs#PC <- (Vptr b (Ptrofs.repr pos'))). + split. unfold goto_label. rewrite P. rewrite H1. auto. + split. rewrite Pregmap.gss. constructor; auto. + rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q. + auto. omega. + generalize (transf_function_no_overflow _ _ H0). omega. + intros. apply Pregmap.gso; auto. Qed. -Remark loadsymbol_label: forall r id ofs k, tail_nolabel k (loadsymbol r id ofs k). +(** Existence of return addresses *) + +Lemma return_address_exists: + forall b f c, is_tail (b :: c) f.(MB.fn_code) -> + exists ra, return_address_offset f c ra. Proof. - intros; unfold loadsymbol. - destruct (Archi.pic_code tt); TailNoLabel. destruct Ptrofs.eq; TailNoLabel. -Qed. -Hint Resolve loadsymbol_label: labels. + intros. eapply Asmblockgenproof0.return_address_exists; eauto. + +- intros. monadInv H0. + destruct (zlt Ptrofs.max_unsigned (size_blocks x.(fn_blocks))); inv EQ0. monadInv EQ. simpl. + exists x; exists true; split; auto. + repeat constructor. +- exact transf_function_no_overflow. +Qed. -Remark transl_cond_label: forall cond args k c, - transl_cond cond args k = OK c -> tail_nolabel k c. +(* Useful for dealing with the many cases in some proofs *) +Ltac exploreInst := + repeat match goal with + | [ H : match ?var with | _ => _ end = _ |- _ ] => destruct var + | [ H : OK _ = OK _ |- _ ] => monadInv H + | [ |- context[if ?b then _ else _] ] => destruct b + | [ |- context[match ?m with | _ => _ end] ] => destruct m + | [ |- context[match ?m as _ return _ with | _ => _ end]] => destruct m + | [ H : bind _ _ = OK _ |- _ ] => monadInv H + | [ H : Error _ = OK _ |- _ ] => inversion H + end. + +(** Some translation properties *) + +Lemma transl_blocks_distrib: + forall c f bb tbb tc ep, + transl_blocks f (bb::c) ep = OK (tbb::tc) + -> transl_block f bb (if MB.header bb then ep else false) = OK (tbb :: nil) + /\ transl_blocks f c false = OK tc. Proof. - unfold transl_cond; intros; destruct cond; TailNoLabel. -- destruct is_arith_imm32; TailNoLabel. destruct is_arith_imm32; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. -- destruct is_arith_imm32; TailNoLabel. destruct is_arith_imm32; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. -- destruct is_logical_imm32; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. -- destruct is_logical_imm32; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. -- destruct is_arith_imm64; TailNoLabel. destruct is_arith_imm64; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. -- destruct is_arith_imm64; TailNoLabel. destruct is_arith_imm64; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. -- destruct is_logical_imm64; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. -- destruct is_logical_imm64; TailNoLabel. eapply tail_nolabel_trans; TailNoLabel. + intros until ep. intros TLBS. + destruct bb as [hd bdy ex]. + monadInv TLBS. monadInv EQ. + unfold transl_block. + rewrite EQ0; simpl. + simpl in EQ; rewrite EQ; simpl. + unfold cons_bblocks in *. simpl in EQ0. + destruct ex. + - simpl in *. monadInv EQ0. + destruct (x3 @@ x1) eqn: CBDY; inv H0; inv EQ1; auto. + - simpl in *. inv EQ0. destruct (x3 @@ nil) eqn: CBDY; inv H0; inv EQ1; auto. Qed. -Remark transl_cond_branch_default_label: forall cond args lbl k c, - transl_cond_branch_default cond args lbl k = OK c -> tail_nolabel k c. +Lemma cons_bblocks_decomp: + forall thd tbdy tex tbb, + (tbdy <> nil \/ tex <> None) -> + cons_bblocks thd tbdy tex = tbb :: nil -> + header tbb = thd + /\ body tbb = tbdy + /\ exit tbb = tex. Proof. - unfold transl_cond_branch_default; intros. - eapply tail_nolabel_trans; [eapply transl_cond_label;eauto|TailNoLabel]. + intros until tbb. intros Hnonil CONSB. unfold cons_bblocks in CONSB. + destruct (tex) eqn:ECTL. + - destruct tbdy; inv CONSB; simpl; auto. + - inversion Hnonil. + + destruct tbdy as [|bi tbdy]; [ contradiction H; auto | inv CONSB; auto]. + + contradict H; simpl; auto. Qed. -Hint Resolve transl_cond_branch_default_label: labels. -Remark transl_cond_branch_label: forall cond args lbl k c, - transl_cond_branch cond args lbl k = OK c -> tail_nolabel k c. +Lemma transl_blocks_nonil: + forall f bb c tc ep, + transl_blocks f (bb::c) ep = OK tc -> + exists tbb tc', tc = tbb :: tc'. Proof. - unfold transl_cond_branch; intros; destruct args; TailNoLabel; destruct cond; TailNoLabel. -- destruct c0; TailNoLabel. -- destruct c0; TailNoLabel. -- destruct (Int.is_power2 n); TailNoLabel. -- destruct (Int.is_power2 n); TailNoLabel. -- destruct c0; TailNoLabel. -- destruct c0; TailNoLabel. -- destruct (Int64.is_power2' n); TailNoLabel. -- destruct (Int64.is_power2' n); TailNoLabel. + intros until ep. intros TLBS. monadInv TLBS. monadInv EQ. unfold cons_bblocks. + destruct (x2); + destruct (x3 @@ x1); simpl; eauto. Qed. -Remark transl_op_label: - forall op args r k c, - transl_op op args r k = OK c -> tail_nolabel k c. +Definition mb_remove_header bb := {| MB.header := nil; MB.body := MB.body bb; MB.exit := MB.exit bb |}. + +Definition mb_remove_body (bb: MB.bblock) := + {| MB.header := MB.header bb; MB.body := nil; MB.exit := MB.exit bb |}. + +Definition mbsize (bb: MB.bblock) := (length (MB.body bb) + length_opt (MB.exit bb))%nat. + +Lemma mbsize_eqz: + forall bb, mbsize bb = 0%nat -> MB.body bb = nil /\ MB.exit bb = None. Proof. - unfold transl_op; intros; destruct op; TailNoLabel. -- destruct (preg_of r); try discriminate; destruct (preg_of m); inv H; TailNoLabel. -- destruct (Float.eq_dec n Float.zero); TailNoLabel. -- destruct (Float32.eq_dec n Float32.zero); TailNoLabel. -- apply logicalimm32_label; unfold nolabel; auto. -- apply logicalimm32_label; unfold nolabel; auto. -- apply logicalimm32_label; unfold nolabel; auto. -- unfold shrx32. destruct (Int.eq _ _); try destruct (Int.eq _ _); TailNoLabel. -- apply arith_extended_label; unfold nolabel; auto. -- apply arith_extended_label; unfold nolabel; auto. -- apply logicalimm64_label; unfold nolabel; auto. -- apply logicalimm64_label; unfold nolabel; auto. -- apply logicalimm64_label; unfold nolabel; auto. -- unfold shrx64. destruct (Int.eq _ _); try destruct (Int.eq _ _); TailNoLabel. -- eapply tail_nolabel_trans. eapply transl_cond_label; eauto. TailNoLabel. -- destruct (preg_of r); try discriminate; TailNoLabel; - (eapply tail_nolabel_trans; [eapply transl_cond_label; eauto | TailNoLabel]). + intros. destruct bb as [hd bdy ex]; simpl in *. unfold mbsize in H. + remember (length _) as a. remember (length_opt _) as b. + assert (a = 0%nat) by omega. assert (b = 0%nat) by omega. subst. clear H. + inv H0. inv H1. destruct bdy; destruct ex; auto. + all: try discriminate. Qed. -Remark transl_addressing_label: - forall sz addr args insn k c, - transl_addressing sz addr args insn k = OK c -> - (forall ad, nolabel (insn ad)) -> - tail_nolabel k c. +Lemma mbsize_neqz: + forall bb, mbsize bb <> 0%nat -> (MB.body bb <> nil \/ MB.exit bb <> None). Proof. - unfold transl_addressing; intros; destruct addr; TailNoLabel; - eapply tail_nolabel_trans; TailNoLabel. - eapply tail_nolabel_trans. apply arith_extended_label; unfold nolabel; auto. TailNoLabel. + intros. destruct bb as [hd bdy ex]; simpl in *. + destruct bdy; destruct ex; try (right; discriminate); try (left; discriminate). + contradict H. unfold mbsize. simpl. auto. Qed. -Remark transl_load_label: - forall trap chunk addr args dst k c, - transl_load trap chunk addr args dst k = OK c -> tail_nolabel k c. +Record codestate := + Codestate { pstate: state; (**r projection to Asmblock.state *) + pheader: list label; + pbody1: list basic; (**r list of basic instructions coming from the translation of the Machblock body *) + pbody2: list basic; (**r list of basic instructions coming from the translation of the Machblock exit *) + pctl: option control; (**r exit instruction, coming from the translation of the Machblock exit *) + ep: bool; (**r reflects the [ep] variable used in the translation *) + rem: list AB.bblock; (**r remaining bblocks to execute *) + cur: bblock (**r current bblock to execute - to keep track of its size when incrementing PC *) + }. + +(* The part that deals with Machblock <-> Codestate agreement + * Note about DXP: the property of [ep] only matters if the current block doesn't have a header, hence the condition *) +Inductive match_codestate fb: Machblock.state -> codestate -> Prop := + | match_codestate_intro: + forall s sp ms m rs0 m0 f tc ep c bb tbb tbc1 tbc2 ex + (STACKS: match_stack ge s) + (FIND: Genv.find_funct_ptr ge fb = Some (Internal f)) + (MEXT: Mem.extends m m0) + (TBC: transl_basic_code f (MB.body bb) (if MB.header bb then ep else false) = OK tbc1) + (TIC: transl_exit f (MB.exit bb) = OK (tbc2, ex)) + (TBLS: transl_blocks f c false = OK tc) + (AG: agree ms sp rs0) + (DXP: (if MB.header bb then ep else false) = true -> rs0#X29 = parent_sp s) + , + match_codestate fb (Machblock.State s fb sp (bb::c) ms m) + {| pstate := (Asm.State rs0 m0); + pheader := (MB.header bb); + pbody1 := tbc1; + pbody2 := tbc2; + pctl := ex; + ep := ep; + rem := tc; + cur := tbb + |} +. + +(* The part ensuring that the code in Codestate actually resides at [rs PC] *) +Inductive match_asmstate fb: codestate -> Asm.state -> Prop := + | match_asmstate_some: + forall rs f tf tc m tbb ofs ep tbdy1 tbdy2 tex lhd + (FIND: Genv.find_funct_ptr ge fb = Some (Internal f)) + (TRANSF: transf_function f = OK tf) + (PCeq: rs PC = Vptr fb ofs) + (TAIL: code_tail (Ptrofs.unsigned ofs) (fn_blocks tf) (tbb::tc)) + , + match_asmstate fb + {| pstate := (Asm.State rs m); + pheader := lhd; + pbody1 := tbdy1; + pbody2 := tbdy2; + pctl := tex; + ep := ep; + rem := tc; + cur := tbb |} + (Asm.State rs m) +. + +Lemma indexed_memory_access_nonil: forall f ofs r i k, + indexed_memory_access_bc f ofs r i k <> nil. Proof. - unfold transl_load; intros; destruct trap; try discriminate; destruct chunk; TailNoLabel; eapply transl_addressing_label; eauto; unfold nolabel; auto. + intros. + unfold indexed_memory_access_bc, loadimm64, loadimm, loadimm_z, loadimm_n; + desif; try congruence. + all: destruct decompose_int; try destruct p; try congruence. Qed. -Remark transl_store_label: - forall chunk addr args src k c, - transl_store chunk addr args src k = OK c -> tail_nolabel k c. +Lemma loadimm_nonil: forall sz x n k, + loadimm sz x n k <> nil. Proof. - unfold transl_store; intros; destruct chunk; TailNoLabel; eapply transl_addressing_label; eauto; unfold nolabel; auto. + intros. + unfold loadimm. desif; + unfold loadimm_n, loadimm_z. + all: destruct decompose_int; try destruct p; try congruence. Qed. -Remark indexed_memory_access_label: - forall insn sz base ofs k, - (forall ad, nolabel (insn ad)) -> - tail_nolabel k (indexed_memory_access insn sz base ofs k). +Lemma loadimm32_nonil: forall sz x n, + loadimm32 sz x n <> nil. Proof. - unfold indexed_memory_access; intros. destruct offset_representable. - TailNoLabel. - eapply tail_nolabel_trans; TailNoLabel. + intros. + unfold loadimm32. desif; try congruence. + apply loadimm_nonil. Qed. -Remark loadind_label: - forall base ofs ty dst k c, - loadind base ofs ty dst k = OK c -> tail_nolabel k c. +Lemma loadimm64_nonil: forall sz x n, + loadimm64 sz x n <> nil. Proof. - unfold loadind; intros. - destruct ty, (preg_of dst); inv H; apply indexed_memory_access_label; intros; exact I. + intros. + unfold loadimm64. desif; try congruence. + apply loadimm_nonil. Qed. -Remark storeind_label: - forall src base ofs ty k c, - storeind src base ofs ty k = OK c -> tail_nolabel k c. +Lemma loadsymbol_nonil: forall sz x n k, + loadsymbol sz x n k <> nil. Proof. - unfold storeind; intros. - destruct ty, (preg_of src); inv H; apply indexed_memory_access_label; intros; exact I. + intros. + unfold loadsymbol. desif; try congruence. Qed. -Remark loadptr_label: - forall base ofs dst k, tail_nolabel k (loadptr base ofs dst k). +Lemma move_extended_nonil: forall x0 x1 x2 a k, + move_extended x1 x2 x0 a k <> nil. Proof. - intros. apply indexed_memory_access_label. unfold nolabel; auto. + intros. unfold move_extended, move_extended_base. + desif; try congruence. Qed. -Remark storeptr_label: - forall src base ofs k, tail_nolabel k (storeptr src base ofs k). +Lemma arith_extended_nonil: forall insnX insnS x0 x1 x2 x3 a k, + arith_extended insnX insnS x1 x2 x3 x0 a k <> nil. Proof. - intros. apply indexed_memory_access_label. unfold nolabel; auto. + intros. unfold arith_extended, move_extended_base. + desif; try congruence. Qed. -Remark make_epilogue_label: - forall f k, tail_nolabel k (make_epilogue f k). +Lemma transl_instr_basic_nonil: + forall k f bi ep x, + transl_instr_basic f bi ep k = OK x -> + x <> nil. Proof. - unfold make_epilogue; intros. - (* FIXME destruct is_leaf_function. - { TailNoLabel. } *) - eapply tail_nolabel_trans. - apply loadptr_label. - TailNoLabel. + intros until x. intros TIB. + destruct bi. + - simpl in TIB. unfold loadind in TIB; + exploreInst; try discriminate; apply indexed_memory_access_nonil. + - simpl in TIB. unfold storeind in TIB; + exploreInst; try discriminate; apply indexed_memory_access_nonil. + - simpl in TIB. monadInv TIB. unfold loadind in EQ. exploreInst; try discriminate; + unfold loadptr_bc; apply indexed_memory_access_nonil. + - simpl in TIB. unfold transl_op in TIB. exploreInst; try discriminate; + unfold addimm32, addimm64, shrx32, shrx64, + logicalimm32, logicalimm64, addimm_aux. + all: desif; try congruence; + try apply loadimm32_nonil; try apply loadimm64_nonil; try apply loadsymbol_nonil; + try apply move_extended_nonil; try apply arith_extended_nonil. + all: unfold transl_cond in *; exploreInst; try discriminate; + try apply loadimm32_nonil; try apply loadimm64_nonil. + - simpl in TIB. unfold transl_load in TIB. exploreInst; try discriminate; + unfold transl_addressing in *; exploreInst; try discriminate. + all: try apply loadimm64_nonil; try apply arith_extended_nonil; try apply loadsymbol_nonil. + - simpl in TIB. unfold transl_store in TIB. exploreInst; try discriminate; + unfold transl_addressing in *; exploreInst; try discriminate. + all: try apply loadimm64_nonil; try apply arith_extended_nonil; try apply loadsymbol_nonil. Qed. -Lemma transl_instr_label: - forall f i ep k c, - transl_instr f i ep k = OK c -> - match i with Mlabel lbl => c = Plabel lbl :: k | _ => tail_nolabel k c end. +Lemma transl_basic_code_nonil: + forall bdy f x ep, + bdy <> nil -> + transl_basic_code f bdy ep = OK x -> + x <> nil. Proof. - unfold transl_instr; intros; destruct i; TailNoLabel. -- eapply loadind_label; eauto. -- eapply storeind_label; eauto. -- destruct ep. eapply loadind_label; eauto. - eapply tail_nolabel_trans. apply loadptr_label. eapply loadind_label; eauto. -- eapply transl_op_label; eauto. -- eapply transl_load_label; eauto. -- eapply transl_store_label; eauto. -- destruct s0; monadInv H; TailNoLabel. -- destruct s0; monadInv H; (eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel]). -- eapply transl_cond_branch_label; eauto. -- eapply tail_nolabel_trans; [eapply make_epilogue_label|TailNoLabel]. + induction bdy as [|bi bdy]. + intros. contradict H0; auto. + destruct bdy as [|bi2 bdy]. + - clear IHbdy. intros f x b _ TBC. simpl in TBC. eapply transl_instr_basic_nonil; eauto. + - intros f x b Hnonil TBC. remember (bi2 :: bdy) as bdy'. + monadInv TBC. + assert (x0 <> nil). + eapply IHbdy; eauto. subst bdy'. discriminate. + eapply transl_instr_basic_nonil; eauto. 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. +Lemma transl_exit_nonil: + forall ex f bdy x, + ex <> None -> + transl_exit f ex = OK(bdy, x) -> + x <> None. Proof. - intros. exploit transl_instr_label; eauto. - destruct i; try (intros [A B]; apply B). - intros. subst c. simpl. auto. + intros ex f bdy x Hnonil TIC. + destruct ex as [ex|]. + - clear Hnonil. destruct ex. + all: try (simpl in TIC; try monadInv TIC; exploreInst; discriminate). + - contradict Hnonil; auto. Qed. -Lemma transl_code_label: - 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 - | Some c' => exists tc', find_label lbl tc = Some tc' /\ transl_code f c' false = OK tc' - end. +Theorem app_nonil: forall A (l1 l2: list A), + l1 <> nil -> + l1 @@ l2 <> nil. Proof. - induction c; simpl; intros. - inv H. auto. - 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. - eapply IHc; eauto. + induction l2. + - intros; rewrite app_nil_r; auto. + - intros. unfold not. intros. symmetry in H0. + generalize (app_cons_not_nil); intros. unfold not in H1. + generalize (H0). apply H1. Qed. -Lemma transl_find_label: - forall lbl f tf, - transf_function f = OK tf -> - match Mach.find_label lbl f.(Mach.fn_code) with - | None => find_label lbl tf.(fn_code) = None - | Some c => exists tc, find_label lbl tf.(fn_code) = Some tc /\ transl_code f c false = OK tc - end. +Theorem match_state_codestate: + forall mbs abs s fb sp bb c ms m, + (MB.body bb <> nil \/ MB.exit bb <> None) -> + mbs = (Machblock.State s fb sp (bb::c) ms m) -> + match_states mbs abs -> + exists cs fb f tbb tc ep, + match_codestate fb mbs cs /\ match_asmstate fb cs abs + /\ Genv.find_funct_ptr ge fb = Some (Internal f) + /\ transl_blocks f (bb::c) ep = OK (tbb::tc) + /\ body tbb = pbody1 cs ++ pbody2 cs + /\ exit tbb = pctl cs + /\ cur cs = tbb /\ rem cs = tc + /\ pstate cs = abs. Proof. - intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0. - monadInv EQ. rewrite transl_code'_transl_code in EQ0. unfold fn_code. - simpl. destruct (storeptr_label X30 XSP (fn_retaddr_ofs f) x) as [A B]; rewrite B. - eapply transl_code_label; eauto. + intros until m. intros Hnotempty Hmbs MS. subst. inv MS. + inv AT. clear H0. exploit transl_blocks_nonil; eauto. intros (tbb & tc' & Htc). subst. + exploit transl_blocks_distrib; eauto. intros (TLB & TLBS). clear H2. + monadInv TLB. exploit cons_bblocks_decomp; eauto. + { inversion Hnotempty. + - destruct (MB.body bb) as [|bi bdy]; try (contradict H0; simpl; auto; fail). + left. apply app_nonil. eapply transl_basic_code_nonil; eauto. + - destruct (MB.exit bb) as [ei|]; try (contradict H0; simpl; auto; fail). + right. eapply transl_exit_nonil; eauto. } + intros (Hth & Htbdy & Htexit). + exists {| pstate := (State rs m'); pheader := (Machblock.header bb); pbody1 := x1; pbody2 := x; + pctl := x0; ep := ep0; rem := tc'; cur := tbb |}, fb, f, tbb, tc', ep0. + repeat split. 1-2: econstructor; eauto. + { destruct (MB.header bb). eauto. discriminate. } eauto. + unfold transl_blocks. fold transl_blocks. unfold transl_block. rewrite EQ. simpl. rewrite EQ1; simpl. + rewrite TLBS. simpl. rewrite H2. + all: simpl; auto. Qed. -End TRANSL_LABEL. +Lemma exec_straight_body: + forall c c' rs1 m1 rs2 m2, + exec_straight tge lk c rs1 m1 c' rs2 m2 -> + exists l, + c = l ++ c' + /\ exec_body lk tge l rs1 m1 = Next rs2 m2. +Proof. + induction c; try (intros; inv H; fail). + intros until m2. intros EXES. inv EXES. + - exists (a :: nil). repeat (split; simpl; auto). rewrite H6. auto. + - eapply IHc in H7; eauto. destruct H7 as (l' & Hc & EXECB). subst. + exists (a :: l'). repeat (split; simpl; auto). + rewrite H1. auto. +Qed. -(** A valid branch in a piece of Mach code translates to a valid ``go to'' - transition in the generated Asm code. *) +Lemma exec_straight_body2: + forall c rs1 m1 c' rs2 m2, + exec_straight tge lk c rs1 m1 c' rs2 m2 -> + exists body, + exec_body lk tge body rs1 m1 = Next rs2 m2 + /\ body ++ c' = c. +Proof. + intros until m2. induction 1. + - exists (i1::nil). split; auto. simpl. rewrite H. auto. + - destruct IHexec_straight as (bdy & EXEB & BTC). + exists (i:: bdy). split; simpl. + + rewrite H. auto. + + congruence. +Qed. -Lemma find_label_goto_label: - forall f tf lbl rs m c' b ofs, - Genv.find_funct_ptr ge b = Some (Internal f) -> - transf_function f = OK tf -> - rs PC = Vptr b ofs -> - 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) b f c' false tf tc' - /\ forall r, r <> PC -> rs'#r = rs#r. +Lemma exec_straight_opt_body2: + forall c rs1 m1 c' rs2 m2, + exec_straight_opt tge lk c rs1 m1 c' rs2 m2 -> + exists body, + exec_body lk tge body rs1 m1 = Next rs2 m2 + /\ body ++ c' = c. Proof. - intros. exploit (transl_find_label lbl f tf); eauto. rewrite H2. - intros [tc [A B]]. - exploit label_pos_code_tail; eauto. instantiate (1 := 0). - intros [pos' [P [Q R]]]. - exists tc; exists (rs#PC <- (Vptr b (Ptrofs.repr pos'))). - split. unfold goto_label. rewrite P. rewrite H1. auto. - split. rewrite Pregmap.gss. constructor; auto. - rewrite Ptrofs.unsigned_repr. replace (pos' - 0) with pos' in Q. - auto. omega. - generalize (transf_function_no_overflow _ _ H0). omega. - intros. apply Pregmap.gso; auto. + intros until m2. intros EXES. + inv EXES. + - exists nil. split; auto. + - eapply exec_straight_body2. auto. Qed. -(** Existence of return addresses *) +Lemma PC_not_data_preg: forall r , + data_preg r = true -> + r <> PC. +Proof. + intros. destruct (PregEq.eq r PC); [ rewrite e in H; simpl in H; discriminate | auto ]. +Qed. -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. +Lemma X30_not_data_preg: forall r , + data_preg r = true -> + r <> X30. 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 Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0. monadInv EQ. - rewrite transl_code'_transl_code in EQ0. - exists x; exists true; split; auto. unfold fn_code. - constructor. apply (storeptr_label X30 XSP (fn_retaddr_ofs f0) x). -- exact transf_function_no_overflow. + intros. destruct (PregEq.eq r X30); [ rewrite e in H; simpl in H; discriminate | auto ]. Qed. -(** * Proof of semantic preservation *) +Lemma X16_not_data_preg: forall r , + data_preg r = true -> + r <> X16. +Proof. + intros. destruct (PregEq.eq r X16); [ rewrite e in H; simpl in H; discriminate | auto ]. +Qed. -(** Semantic preservation is proved using simulation diagrams - of the following form. -<< - st1 --------------- st2 - | | - t| *|t - | | - v v - st1'--------------- st2' ->> - The invariant is the [match_states] predicate below, which includes: -- The Asm code pointed by the PC register is the translation of - the current Mach code sequence. -- Mach register values and Asm register values agree. -*) +Ltac Simpl := + rewrite Pregmap.gso; try apply PC_not_data_preg; try apply X30_not_data_preg. + +(* See (C) in the diagram. The proofs are mostly adapted from the previous Mach->Asm proofs, but are + unfortunately quite cumbersome. To reproduce them, it's best to have a Coq IDE with you and see by + yourself the steps *) +Theorem step_simu_control: + forall bb' fb fn s sp c ms' m' rs2 m2 t S'' rs1 m1 tbb tbdy2 tex cs2, + MB.body bb' = nil -> + Genv.find_funct_ptr tge fb = Some (Internal fn) -> + pstate cs2 = (State rs2 m2) -> + pbody1 cs2 = nil -> pbody2 cs2 = tbdy2 -> pctl cs2 = tex -> + cur cs2 = tbb -> + match_codestate fb (MB.State s fb sp (bb'::c) ms' m') cs2 -> + match_asmstate fb cs2 (State rs1 m1) -> + exit_step return_address_offset ge (MB.exit bb') (MB.State s fb sp (bb'::c) ms' m') t S'' -> + (exists rs3 m3 rs4 m4, + exec_body lk tge tbdy2 rs2 m2 = Next rs3 m3 + /\ exec_exit tge fn (Ptrofs.repr (size tbb)) rs3 m3 tex t rs4 m4 + /\ match_states S'' (State rs4 m4)). +Proof. + intros until cs2. intros Hbody FIND Hpstate Hpbody1 Hpbody2 Hpctl Hcur MCS MAS ESTEP. + inv ESTEP. + - inv MCS. inv MAS. simpl in *. + inv Hpstate. + destruct ctl. + + (* MBcall *) + destruct bb' as [mhd' mbdy' mex']; simpl in *. subst. + inv TBC. inv TIC. inv H0. + + assert (f0 = f) by congruence. subst f0. + assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned). + eapply transf_function_no_overflow; eauto. + destruct s1 as [rf|fid]; simpl in H1. + * (* Indirect call *) + monadInv H1. monadInv EQ. + assert (ms' rf = Vptr f' Ptrofs.zero). + { unfold find_function_ptr in H12. destruct (ms' rf); try discriminate. + revert H12; predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence. } + assert (rs2 x = Vptr f' Ptrofs.zero). + { exploit ireg_val; eauto. rewrite H; intros LD; inv LD; auto. } + generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1. + remember (Ptrofs.add _ _) as ofs'. + assert (TCA: transl_code_at_pc ge (Vptr fb ofs') fb f c false tf tc). + { econstructor; eauto. } + assert (f1 = f) by congruence. subst f1. + exploit return_address_offset_correct; eauto. intros; subst ra. + + repeat eexists. + econstructor; eauto. econstructor. + econstructor; eauto. econstructor; eauto. + eapply agree_sp_def; eauto. simpl. eapply agree_exten; eauto. intros. + unfold incrPC; repeat Simpl; auto. + simpl. unfold incrPC; rewrite Pregmap.gso; auto; try discriminate. + rewrite !Pregmap.gss. rewrite PCeq. rewrite Heqofs'. simpl. auto. + + * (* Direct call *) + monadInv H1. + generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1. + remember (Ptrofs.add _ _) as ofs'. + assert (TCA: transl_code_at_pc ge (Vptr fb ofs') fb f c false tf tc). + econstructor; eauto. + assert (f1 = f) by congruence. subst f1. + exploit return_address_offset_correct; eauto. intros; subst ra. + repeat eexists. + econstructor; eauto. econstructor. + econstructor; eauto. econstructor; eauto. eapply agree_sp_def; eauto. simpl. eapply agree_exten; eauto. intros. + unfold incrPC; repeat Simpl; auto. unfold Genv.symbol_address. rewrite symbols_preserved. simpl in H12. rewrite H12. auto. + unfold incrPC; simpl; rewrite Pregmap.gso; try discriminate. rewrite !Pregmap.gss. + subst. unfold Val.offset_ptr. rewrite PCeq. auto. + + (* MBtailcall *) + destruct bb' as [mhd' mbdy' mex']; simpl in *. subst. + inv TBC. inv TIC. inv H0. + + assert (f0 = f) by congruence. subst f0. + assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned). + eapply transf_function_no_overflow; eauto. + exploit Mem.loadv_extends. eauto. eexact H13. auto. simpl. intros [parent' [A B]]. + destruct s1 as [rf|fid]; simpl in H11. + * monadInv H1. monadInv EQ. + assert (ms' rf = Vptr f' Ptrofs.zero). + { destruct (ms' rf); try discriminate. revert H11. predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence. } + assert (rs2 x = Vptr f' Ptrofs.zero). + { exploit ireg_val; eauto. rewrite H; intros LD; inv LD; auto. } + + assert (f = f1) by congruence. subst f1. clear FIND1. clear H12. + exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z). + exploit exec_straight_body; eauto. + intros (l & MKEPI & EXEB). + repeat eexists. rewrite app_nil_r in MKEPI. + rewrite <- MKEPI in EXEB. + eauto. econstructor. simpl. unfold incrPC. + rewrite !Pregmap.gso; try discriminate. eauto. + econstructor; eauto. + { apply agree_set_other. + - econstructor; auto with asmgen. + + apply V. + + intro r. destruct r; apply V; auto. + - eauto with asmgen. } + rewrite Pregmap.gss. rewrite Z; auto; try discriminate. + eapply ireg_of_not_X30''; eauto. + eapply ireg_of_not_X16''; eauto. + * monadInv H1. assert (f = f1) by congruence. subst f1. clear FIND1. clear H12. + exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z). + exploit exec_straight_body; eauto. + intros (l & MKEPI & EXEB). + repeat eexists. inv EQ. rewrite app_nil_r in MKEPI. + rewrite <- MKEPI in EXEB. + eauto. inv EQ. econstructor. simpl. unfold incrPC. + eauto. + econstructor; eauto. + { apply agree_set_other. + - econstructor; auto with asmgen. + + apply V. + + intro r. destruct r; apply V; auto. + - eauto with asmgen. } + { rewrite Pregmap.gss. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H11. auto. } + + (* MBbuiltin *) + destruct bb' as [mhd' mbdy' mex']; simpl in *. subst. + + assert (f0 = f) by congruence. subst f0. + assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned). + eapply transf_function_no_overflow; eauto. + generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1. + remember (Ptrofs.add _ _) as ofs'. + assert (TCA: transl_code_at_pc ge (Vptr fb ofs') fb f c false tf tc). + econstructor; eauto. + + monadInv TBC. monadInv TIC. inv H0. + + exploit builtin_args_match; eauto. intros [vargs' [P Q]]. + exploit external_call_mem_extends; eauto. + intros [vres' [m2' [A [B [C D]]]]]. + + repeat eexists. econstructor. erewrite <- sp_val by eauto. + eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply external_call_symbols_preserved; eauto. apply senv_preserved. eauto. + econstructor; eauto. + unfold incrPC. rewrite Pregmap.gss. + rewrite set_res_other. rewrite undef_regs_other_2. unfold Val.offset_ptr. rewrite PCeq. + eauto. rewrite preg_notin_charact. intros. auto with asmgen. + auto with asmgen. apply agree_nextblock. eapply agree_set_res; auto. + eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto. + intros. discriminate. + + (* MBgoto *) + destruct bb' as [mhd' mbdy' mex']; simpl in *. subst. + inv TBC. inv TIC. inv H0. + + assert (f0 = f) by congruence. subst f0. assert (f1 = f) by congruence. subst f1. clear H9. + remember (incrPC (Ptrofs.repr (size tbb)) rs2) as rs2'. + exploit functions_transl. eapply FIND0. eapply TRANSF0. intros FIND'. + assert (tf = fn) by congruence. subst tf. + exploit find_label_goto_label. + eauto. eauto. + instantiate (2 := rs2'). + { subst. unfold incrPC. rewrite Pregmap.gss. unfold Val.offset_ptr. rewrite PCeq. eauto. } + eauto. + intros (tc' & rs' & GOTO & AT2 & INV). + + eexists. eexists. repeat eexists. repeat split. + econstructor; eauto. + rewrite Heqrs2' in INV. unfold incrPC in INV. + rewrite Heqrs2' in GOTO; simpl; eauto. + econstructor; eauto. + eapply agree_exten; eauto with asmgen. + assert (forall r : preg, r <> PC -> rs' r = rs2 r). + { intros. rewrite Heqrs2' in INV. + rewrite INV; unfold incrPC; try rewrite Pregmap.gso; auto. } + eauto with asmgen. + congruence. + + (* MBcond *) + destruct bb' as [mhd' mbdy' mex']; simpl in *. subst. + inv TBC. inv TIC. inv H0. monadInv H1. monadInv EQ. + + * (* MBcond true *) + assert (f0 = f) by congruence. subst f0. + exploit eval_condition_lessdef. + eapply preg_vals; eauto. + all: eauto. + intros EC. + exploit transl_cbranch_correct_1; eauto. intros (rs', H). + destruct H as [ES [ECFI]]. + exploit exec_straight_opt_body2. eauto. intros (bdy & EXEB & BTC). + assert (PCeq': rs2 PC = rs' PC). { inv ES; auto. erewrite <- exec_straight_pc. 2: eapply H0. eauto. } + rewrite PCeq' in PCeq. + assert (f1 = f) by congruence. subst f1. + exploit find_label_goto_label. + 4: eapply H14. 1-2: eauto. instantiate (2 := (incrPC (Ptrofs.repr (size tbb)) rs')). + unfold incrPC, Val.offset_ptr. rewrite PCeq. rewrite Pregmap.gss. eauto. + intros (tc' & rs3 & GOTOL & TLPC & Hrs3). + exploit functions_transl. eapply FIND1. eapply TRANSF0. intros FIND'. + assert (tf = fn) by congruence. subst tf. + + repeat eexists. + rewrite <- BTC. simpl. rewrite app_nil_r. eauto. + rewrite <- BTC. simpl. econstructor. rewrite ECFI. eauto. + + econstructor; eauto. + eapply agree_exten with rs2; eauto with asmgen. + { intros. rewrite Hrs3; unfold incrPC. Simpl. rewrite H. all: auto. apply PC_not_data_preg; auto. } + intros. discriminate. + * (* MBcond false *) + assert (f0 = f) by congruence. subst f0. monadInv H1. monadInv EQ. + exploit eval_condition_lessdef. + eapply preg_vals; eauto. + all: eauto. + intros EC. + + exploit transl_cbranch_correct_1; eauto. intros (rs', H). + destruct H as [ES [ECFI]]. + exploit exec_straight_opt_body2. eauto. intros (bdy & EXEB & BTC). + assert (PCeq': rs2 PC = rs' PC). { inv ES; auto. erewrite <- exec_straight_pc. 2: eapply H0. eauto. } + rewrite PCeq' in PCeq. + exploit functions_transl. eapply FIND1. eapply TRANSF0. intros FIND'. + assert (tf = fn) by congruence. subst tf. + + assert (NOOV: size_blocks fn.(fn_blocks) <= Ptrofs.max_unsigned). + eapply transf_function_no_overflow; eauto. + generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1. + + repeat eexists. + rewrite <- BTC. simpl. rewrite app_nil_r. eauto. + rewrite <- BTC. simpl. econstructor. rewrite ECFI. eauto. + + econstructor; eauto. + unfold incrPC. rewrite Pregmap.gss. unfold Val.offset_ptr. rewrite PCeq. econstructor; eauto. + eapply agree_exten with rs2; eauto with asmgen. + { intros. unfold incrPC. Simpl. rewrite H. all: auto. } + intros. discriminate. + + (* MBjumptable *) + destruct bb' as [mhd' mbdy' mex']; simpl in *. subst. + inv TBC. inv TIC. inv H0. + + assert (f0 = f) by congruence. subst f0. + monadInv H1. monadInv EQ. + generalize (transf_function_no_overflow _ _ TRANSF0); intro NOOV. + assert (f1 = f) by congruence. subst f1. + exploit find_label_goto_label. 4: eapply H14. 1-2: eauto. instantiate (2 := (incrPC (Ptrofs.repr (size tbb)) rs2) # X16 <- Vundef # X17 <- Vundef). + unfold incrPC. Simpl. unfold Val.offset_ptr. rewrite PCeq. reflexivity. discriminate. + exploit functions_transl. eapply FIND0. eapply TRANSF0. intros FIND3. assert (fn = tf) by congruence. subst fn. + + intros [tc' [rs' [A [B C]]]]. + exploit ireg_val; eauto. rewrite H11. intros LD; inv LD. + + repeat eexists. econstructor. simpl. Simpl. 2: { eapply ireg_of_not_X16''; eauto. } + unfold incrPC. rewrite Pregmap.gso; try discriminate. rewrite <- H1. + simpl. unfold Mach.label in H12. unfold label. rewrite H12. eapply A. + econstructor; eauto. + eapply agree_undef_regs; eauto. intros. rewrite C; auto with asmgen. + { unfold incrPC. repeat Simpl; auto. assert (destroyed_by_jumptable = R17 :: nil) by auto. + rewrite H2 in H0. simpl in H0. destruct r'; try discriminate. + destruct d; try discriminate. destruct i; try discriminate. + destruct r; try discriminate. } + discriminate. + + (* MBreturn *) + destruct bb' as [mhd' mbdy' mex']; simpl in *. subst. + inv TBC. inv TIC. inv H0. + + assert (f0 = f) by congruence. subst f0. + assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned). + eapply transf_function_no_overflow; eauto. + exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z). + exploit exec_straight_body; eauto. + simpl. eauto. + intros EXEB. destruct EXEB as [l [MKEPI EXEB]]. + assert (f1 = f) by congruence. subst f1. + + repeat eexists. + rewrite app_nil_r in MKEPI. rewrite <- MKEPI in EXEB. eauto. + econstructor. simpl. reflexivity. + econstructor; eauto. + unfold incrPC. repeat apply agree_set_other; auto with asmgen. + + - inv MCS. inv MAS. simpl in *. subst. inv Hpstate. + destruct bb' as [hd' bdy' ex']; simpl in *. subst. + monadInv TBC. monadInv TIC. simpl in *. + simpl. repeat eexists. + econstructor. econstructor. 4: instantiate (3 := false). all:eauto. + unfold incrPC. rewrite Pregmap.gss. unfold Val.offset_ptr. rewrite PCeq. + assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned). + eapply transf_function_no_overflow; eauto. + assert (f = f0) by congruence. subst f0. econstructor; eauto. + generalize (code_tail_next_int _ _ _ _ NOOV TAIL). intro CT1. eauto. + eapply agree_exten; eauto. intros. unfold incrPC; Simpl; auto. + discriminate. +Qed. -Inductive match_states: Mach.state -> Asm.state -> Prop := - | match_states_intro: - 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) fb f c ep tf tc) - (AG: agree ms sp rs) - (DXP: ep = true -> rs#X29 = parent_sp s) - (LEAF: is_leaf_function f = true -> rs#RA = parent_ra s), - match_states (Mach.State s fb sp c ms m) - (Asm.State rs m') - | match_states_call: - 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 Ptrofs.zero) - (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) - (MEXT: Mem.extends m m') - (AG: agree ms (parent_sp s) rs) - (ATPC: rs PC = parent_ra s), - match_states (Mach.Returnstate s ms m) - (Asm.State rs m'). +(* Handling the individual instructions of theorem (B) in the above diagram. A bit less cumbersome, but still tough *) +Theorem step_simu_basic: + forall bb bb' s fb sp c ms m rs1 m1 ms' m' bi cs1 tbdy bdy, + MB.header bb = nil -> MB.body bb = bi::(bdy) -> + bb' = {| MB.header := nil; MB.body := bdy; MB.exit := MB.exit bb |} -> + basic_step ge s fb sp ms m bi ms' m' -> + pstate cs1 = (State rs1 m1) -> pbody1 cs1 = tbdy -> + match_codestate fb (MB.State s fb sp (bb::c) ms m) cs1 -> + (exists rs2 m2 l cs2 tbdy', + cs2 = {| pstate := (State rs2 m2); pheader := nil; pbody1 := tbdy'; pbody2 := pbody2 cs1; + pctl := pctl cs1; ep := it1_is_parent (ep cs1) bi; rem := rem cs1; cur := cur cs1 |} + /\ tbdy = l ++ tbdy' + /\ exec_body lk tge l rs1 m1 = Next rs2 m2 + /\ match_codestate fb (MB.State s fb sp (bb'::c) ms' m') cs2). +Proof. + intros until bdy. intros Hheader Hbody (* Hnotempty *) Hbb' BSTEP Hpstate Hpbody1 MCS. inv MCS. + simpl in *. inv Hpstate. + rewrite Hbody in TBC. monadInv TBC. + inv BSTEP. + + - (* MBgetstack *) + simpl in EQ0. + unfold Mach.load_stack in H. + exploit Mem.loadv_extends; eauto. intros [v' [A B]]. + rewrite (sp_val _ _ _ AG) in A. + exploit loadind_correct; eauto with asmgen. + intros (rs2 & EXECS & Hrs'1 & Hrs'2). + eapply exec_straight_body in EXECS. + destruct EXECS as (l & Hlbi & EXECB). + exists rs2, m1, l. + eexists. eexists. split. instantiate (1 := x). eauto. + repeat (split; auto). + remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'. + assert (Hheadereq: MB.header bb' = MB.header bb). { subst. simpl. auto. } + subst. simpl in Hheadereq. + + eapply match_codestate_intro; eauto. + eapply agree_set_mreg; eauto with asmgen. + intro Hep. simpl in Hep. discriminate. + - (* MBsetstack *) + simpl in EQ0. + unfold Mach.store_stack in H. + assert (Val.lessdef (ms src) (rs1 (preg_of src))). { eapply preg_val; eauto. } + exploit Mem.storev_extends; eauto. intros [m2' [A B]]. + exploit storeind_correct; eauto with asmgen. + rewrite (sp_val _ _ _ AG) in A. eauto. intros [rs' [P Q]]. + + eapply exec_straight_body in P. + destruct P as (l & ll & EXECB). + exists rs', m2', l. + eexists. eexists. split. instantiate (1 := x). eauto. + repeat (split; auto). + remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'. + subst. + eapply match_codestate_intro; eauto. simpl. simpl in EQ. rewrite Hheader in EQ. auto. + eapply agree_undef_regs; eauto with asmgen. + simpl; intros. rewrite Q; auto with asmgen. rewrite Hheader in DXP. auto. + - (* MBgetparam *) + simpl in EQ0. + + assert (f0 = f) by congruence; subst f0. + unfold Mach.load_stack in *. + 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 H1. auto. + intros [v' [C D]]. + + monadInv EQ0. rewrite Hheader. rewrite Hheader in DXP. + destruct ep0 eqn:EPeq. + + (* X29 contains parent *) + + exploit loadind_correct. eexact EQ1. + instantiate (2 := rs1). rewrite DXP; eauto. discriminate. + intros [rs2 [P [Q R]]]. + + eapply exec_straight_body in P. + destruct P as (l & ll & EXECB). + exists rs2, m1, l. eexists. + eexists. split. instantiate (1 := x). eauto. + repeat (split; auto). + remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'. + assert (Hheadereq: MB.header bb' = MB.header bb). { subst. simpl. auto. } + subst. + eapply match_codestate_intro; eauto. + + eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto with asmgen. + simpl; intros. rewrite R; auto with asmgen. unfold preg_of. + apply preg_of_not_X29; auto. + + (* X29 does not contain parent *) + + rewrite chunk_of_Tptr in A. + exploit loadptr_correct. eexact A. discriminate. intros [rs2 [P [Q R]]]. + exploit loadind_correct. eexact EQ1. instantiate (2 := rs2). rewrite Q. eauto. + discriminate. + intros [rs3 [S [T U]]]. + + exploit exec_straight_trans. + eapply P. + eapply S. + intros EXES. + + eapply exec_straight_body in EXES. + destruct EXES as (l & ll & EXECB). + exists rs3, m1, l. + eexists. eexists. split. instantiate (1 := x). eauto. + repeat (split; auto). + remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'. + assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. } + subst. + eapply match_codestate_intro; eauto. + eapply agree_set_mreg. eapply agree_set_mreg. eauto. eauto. + instantiate (1 := rs2#X29 <- (rs3#X29)). intros. + rewrite Pregmap.gso; auto with asmgen. + congruence. + intros. unfold Pregmap.set. destruct (PregEq.eq r' X29). congruence. auto with asmgen. + simpl; intros. rewrite U; auto with asmgen. + apply preg_of_not_X29; auto. + - (* MBop *) + simpl in EQ0. rewrite Hheader in DXP. + + assert (eval_operation tge sp op (map ms args) m' = Some v). + rewrite <- H. apply eval_operation_preserved. exact symbols_preserved. + exploit eval_operation_lessdef. + eapply preg_vals; eauto. + 2: eexact H0. + all: eauto. + intros [v' [A B]]. rewrite (sp_val _ _ _ AG) in A. + exploit transl_op_correct; eauto. intros [rs2 [P [Q R]]]. + + eapply exec_straight_body in P. + destruct P as (l & ll & EXECB). + exists rs2, m1, l. + eexists. eexists. split. instantiate (1 := x). eauto. + repeat (split; auto). + remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'. + subst. + eapply match_codestate_intro; eauto. simpl. simpl in EQ. rewrite Hheader in EQ. auto. + apply agree_set_undef_mreg with rs1; auto. + apply Val.lessdef_trans with v'; auto. + simpl; intros. destruct (andb_prop _ _ H1); clear H1. + rewrite R; auto. apply preg_of_not_X29; auto. +Local Transparent destroyed_by_op. + destruct op; simpl; auto; try discriminate. + - (* MBload *) + simpl in EQ0. rewrite Hheader in DXP. + + assert (Op.eval_addressing tge sp addr (map ms 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. + exploit Mem.loadv_extends; eauto. intros [v' [C D]]. destruct trap; try discriminate. + exploit transl_load_correct; eauto. + intros [rs2 [P [Q R]]]. + + eapply exec_straight_body in P. + destruct P as (l & ll & EXECB). + exists rs2, m1, l. + eexists. eexists. split. instantiate (1 := x). eauto. + repeat (split; auto). + remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'. + assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. } + subst. + eapply match_codestate_intro; eauto. + eapply agree_set_mreg; eauto with asmgen. + intro Hep. simpl in Hep. discriminate. + - (* MBload notrap1 *) + simpl in EQ0. unfold transl_load in EQ0. discriminate. + - (* MBload notrap2 *) + simpl in EQ0. unfold transl_load in EQ0. discriminate. + - (* MBstore *) + simpl in EQ0. rewrite Hheader in DXP. + + assert (Op.eval_addressing tge sp addr (map ms 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 (ms src) (rs1 (preg_of src))). eapply preg_val; eauto. + exploit Mem.storev_extends; eauto. intros [m2' [C D]]. + exploit transl_store_correct; eauto. intros [rs2 [P Q]]. + + eapply exec_straight_body in P. + destruct P as (l & ll & EXECB). + exists rs2, m2', l. + eexists. eexists. split. instantiate (1 := x). eauto. + repeat (split; auto). + remember {| MB.header := _; MB.body := _; MB.exit := _ |} as bb'. + assert (Hheadereq: MB.header bb' = MB.header bb). { subst. auto. } + subst. + eapply match_codestate_intro; eauto. + eapply agree_undef_regs; eauto with asmgen. + intro Hep. simpl in Hep. discriminate. +Qed. -Lemma exec_straight_steps: - forall s fb f rs1 i c ep tf tc m1' m2 m2' sp ms2, - match_stack ge s -> - Mem.extends m2 m2' -> - 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 sp rs2 - /\ (it1_is_parent ep i = true -> rs2#X29 = parent_sp s) - /\ (is_leaf_function f = true -> rs2#RA = parent_ra s)) -> - exists st', - plus step tge (State rs1 m1') E0 st' /\ - match_states (Mach.State s fb sp c ms2 m2) st'. +Lemma exec_body_trans: + forall l l' rs0 m0 rs1 m1 rs2 m2, + exec_body lk tge l rs0 m0 = Next rs1 m1 -> + exec_body lk tge l' rs1 m1 = Next rs2 m2 -> + exec_body lk tge (l++l') rs0 m0 = Next rs2 m2. Proof. - intros. inversion H2. subst. monadInv H7. - exploit H3; eauto. intros [rs2 [A [B [C D]]]]. - exists (State rs2 m2'); split. - - eapply exec_straight_exec; eauto. - - econstructor; eauto. eapply exec_straight_at; eauto. + induction l. + - simpl. induction l'. intros. + + simpl in *. congruence. + + intros. inv H. auto. + - intros until m2. intros EXEB1 EXEB2. + inv EXEB1. destruct (exec_basic _) eqn:EBI; try discriminate. + simpl. rewrite EBI. eapply IHl; eauto. Qed. -Lemma exec_straight_steps_goto: - 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' -> - 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) fb f (i :: c) ep tf tc -> - it1_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 sp rs2 - /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2' - /\ (is_leaf_function f = true -> rs2#RA = parent_ra s)) -> - exists st', - plus step tge (State rs1 m1') E0 st' /\ - match_states (Mach.State s fb sp c' ms2 m2) st'. +Lemma exec_body_control: + forall b t rs1 m1 rs2 m2 rs3 m3 fn, + exec_body lk tge (body b) rs1 m1 = Next rs2 m2 -> + exec_exit tge fn (Ptrofs.repr (size b)) rs2 m2 (exit b) t rs3 m3 -> + exec_bblock lk tge fn b rs1 m1 t rs3 m3. Proof. - intros. inversion H3. subst. monadInv H9. - exploit H5; eauto. intros [jmp [k' [rs2 [A [B [C D]]]]]]. - generalize (functions_transl _ _ _ H7 H8); intro FN. - generalize (transf_function_no_overflow _ _ H8); intro NOOV. - exploit exec_straight_steps_2; eauto. - intros [ofs' [PC2 CT2]]. - exploit find_label_goto_label; eauto. - intros [tc' [rs3 [GOTO [AT' OTH]]]]. - exists (State rs3 m2'); split. - eapply plus_right'. - eapply exec_straight_steps_1; eauto. + intros until fn. intros EXEB EXECTL. econstructor; eauto. - eapply find_instr_tail. eauto. - rewrite C. eexact GOTO. - traceEq. - econstructor; eauto. - apply agree_exten with rs2; auto with asmgen. - congruence. - rewrite OTH by congruence; auto. Qed. -Lemma exec_straight_opt_steps_goto: - 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' -> - 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) fb f (i :: c) ep tf tc -> - it1_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_opt tge tf c rs1 m1' (jmp :: k') rs2 m2' - /\ agree ms2 sp rs2 - /\ exec_instr tge tf jmp rs2 m2' = goto_label tf lbl rs2 m2' - /\ (is_leaf_function f = true -> rs2#RA = parent_ra s)) -> - exists st', - plus step tge (State rs1 m1') E0 st' /\ - match_states (Mach.State s fb sp c' ms2 m2) st'. +Inductive exec_header: codestate -> codestate -> Prop := + | exec_header_cons: forall cs1, + exec_header cs1 {| pstate := pstate cs1; pheader := nil; pbody1 := pbody1 cs1; pbody2 := pbody2 cs1; + pctl := pctl cs1; ep := (if pheader cs1 then ep cs1 else false); rem := rem cs1; + cur := cur cs1 |}. + +(* Theorem (A) in the diagram, the easiest of all *) +Theorem step_simu_header: + forall bb s fb sp c ms m rs1 m1 cs1, + pstate cs1 = (State rs1 m1) -> + match_codestate fb (MB.State s fb sp (bb::c) ms m) cs1 -> + (exists cs1', + exec_header cs1 cs1' + /\ match_codestate fb (MB.State s fb sp (mb_remove_header bb::c) ms m) cs1'). Proof. - intros. inversion H3. subst. monadInv H9. - exploit H5; eauto. intros [jmp [k' [rs2 [A [B [C D]]]]]]. - generalize (functions_transl _ _ _ H7 H8); intro FN. - generalize (transf_function_no_overflow _ _ H8); intro NOOV. - inv A. -- exploit find_label_goto_label; eauto. - intros [tc' [rs3 [GOTO [AT' OTH]]]]. - exists (State rs3 m2'); split. - apply plus_one. econstructor; eauto. - eapply find_instr_tail. eauto. - rewrite C. eexact GOTO. - econstructor; eauto. - apply agree_exten with rs2; auto with asmgen. - congruence. - rewrite OTH by congruence; auto. -- exploit exec_straight_steps_2; eauto. - intros [ofs' [PC2 CT2]]. - exploit find_label_goto_label; eauto. - intros [tc' [rs3 [GOTO [AT' OTH]]]]. - exists (State rs3 m2'); split. - eapply plus_right'. - eapply exec_straight_steps_1; eauto. + intros until cs1. intros Hpstate MCS. + eexists. split; eauto. econstructor; eauto. - eapply find_instr_tail. eauto. - rewrite C. eexact GOTO. - traceEq. + inv MCS. simpl in *. inv Hpstate. econstructor; eauto. - apply agree_exten with rs2; auto with asmgen. - congruence. - rewrite OTH by congruence; auto. Qed. -(** We need to show that, in the simulation diagram, we cannot - take infinitely many Mach transitions that correspond to zero - transitions on the Asm side. Actually, all Mach transitions - correspond to at least one Asm transition, except the - transition from [Machsem.Returnstate] to [Machsem.State]. - So, the following integer measure will suffice to rule out - the unwanted behaviour. *) - -Definition measure (s: Mach.state) : nat := - match s with - | Mach.State _ _ _ _ _ _ => 0%nat - | Mach.Callstate _ _ _ _ => 0%nat - | Mach.Returnstate _ _ _ => 1%nat - end. - -Remark preg_of_not_X29: forall r, negb (mreg_eq r R29) = true -> IR X29 <> preg_of r. +(* Theorem (B) in the diagram, using step_simu_basic + induction on the Machblock body *) +Theorem step_simu_body: + forall bb s fb sp c ms m rs1 m1 ms' cs1 m', + MB.header bb = nil -> + body_step ge s fb sp (MB.body bb) ms m ms' m' -> + pstate cs1 = (State rs1 m1) -> + match_codestate fb (MB.State s fb sp (bb::c) ms m) cs1 -> + (exists rs2 m2 cs2 ep, + cs2 = {| pstate := (State rs2 m2); pheader := nil; pbody1 := nil; pbody2 := pbody2 cs1; + pctl := pctl cs1; ep := ep; rem := rem cs1; cur := cur cs1 |} + /\ exec_body lk tge (pbody1 cs1) rs1 m1 = Next rs2 m2 + /\ match_codestate fb (MB.State s fb sp ({| MB.header := nil; MB.body := nil; MB.exit := MB.exit bb |}::c) ms' m') cs2). Proof. - intros. change (IR X29) with (preg_of R29). red; intros. - exploit preg_of_injective; eauto. intros; subst r; discriminate. + intros bb. destruct bb as [hd bdy ex]; simpl; auto. induction bdy as [|bi bdy]. + - intros until m'. intros Hheader BSTEP Hpstate MCS. + inv BSTEP. + exists rs1, m1, cs1, (ep cs1). + inv MCS. inv Hpstate. simpl in *. monadInv TBC. repeat (split; simpl; auto). + econstructor; eauto. + - intros until m'. intros Hheader BSTEP Hpstate MCS. inv BSTEP. + rename ms' into ms''. rename m' into m''. rename rs' into ms'. rename m'0 into m'. + exploit (step_simu_basic); eauto. simpl. eauto. simpl; auto. simpl; auto. + intros (rs2 & m2 & l & cs2 & tbdy' & Hcs2 & Happ & EXEB & MCS'). + simpl in *. + exploit IHbdy. auto. eapply H6. 2: eapply MCS'. all: eauto. subst; eauto. simpl; auto. + intros (rs3 & m3 & cs3 & ep & Hcs3 & EXEB' & MCS''). + exists rs3, m3, cs3, ep. + repeat (split; simpl; auto). subst. simpl in *. auto. + rewrite Happ. eapply exec_body_trans; eauto. rewrite Hcs2 in EXEB'; simpl in EXEB'. auto. Qed. -Lemma sp_val': forall ms sp rs, agree ms sp rs -> sp = rs XSP. +(* Bringing theorems (A), (B) and (C) together, for the case of the absence of builtin instruction *) +(* This more general form is easier to prove, but the actual theorem is step_simulation_bblock further below *) +Lemma step_simulation_bblock': + forall t sf f sp bb bb' bb'' rs m rs' m' s'' c S1, + bb' = mb_remove_header bb -> + body_step ge sf f sp (Machblock.body bb') rs m rs' m' -> + bb'' = mb_remove_body bb' -> + exit_step return_address_offset ge (Machblock.exit bb'') (Machblock.State sf f sp (bb'' :: c) rs' m') t s'' -> + match_states (Machblock.State sf f sp (bb :: c) rs m) S1 -> + exists S2 : state, plus (step lk) tge S1 t S2 /\ match_states s'' S2. Proof. - intros. eapply sp_val; eauto. -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 return_address_offset ge S1 t S2 -> - forall S1' (MS: match_states S1 S1') (WF: wf_state ge S1), - (exists S2', plus step tge S1' t S2' /\ match_states S2 S2') - \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat. -Proof. - induction 1; intros; inv MS. - -- (* Mlabel *) - left; eapply exec_straight_steps; eauto; intros. - monadInv TR. econstructor; split. apply exec_straight_one. simpl; eauto. auto. - split. { apply agree_nextinstr; auto. } - split. { simpl; congruence. } - rewrite nextinstr_inv by congruence; assumption. - -- (* Mgetstack *) - unfold load_stack in H. - exploit Mem.loadv_extends; eauto. intros [v' [A B]]. - rewrite (sp_val _ _ _ AG) in A. - left; eapply exec_straight_steps; eauto. intros. simpl in TR. - exploit loadind_correct; eauto with asmgen. intros [rs' [P [Q [R S]]]]. - exists rs'; split. eauto. - split. { eapply agree_set_mreg; eauto with asmgen. congruence. } - split. { simpl; congruence. } - rewrite S. assumption. - -- (* Msetstack *) - unfold store_stack in H. - assert (Val.lessdef (rs src) (rs0 (preg_of src))) by (eapply preg_val; eauto). - exploit Mem.storev_extends; eauto. intros [m2' [A B]]. - left; eapply exec_straight_steps; eauto. - rewrite (sp_val _ _ _ AG) in A. intros. simpl in TR. - exploit storeind_correct; eauto with asmgen. intros [rs' [P [Q R]]]. - exists rs'; split. eauto. - split. eapply agree_undef_regs; eauto with asmgen. - simpl; intros. - split. rewrite Q; auto with asmgen. - rewrite R. assumption. - -- (* Mgetparam *) - assert (f0 = f) by congruence; subst f0. - unfold load_stack in *. - 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 H1. auto. - intros [v' [C D]]. -Opaque loadind. - left; eapply exec_straight_steps; eauto; intros. monadInv TR. - destruct ep. -(* X30 contains parent *) - exploit loadind_correct. eexact EQ. - instantiate (2 := rs0). simpl; rewrite DXP; eauto. simpl; congruence. - intros [rs1 [P [Q [R S]]]]. - exists rs1; split. eauto. - split. eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto with asmgen. - simpl; split; intros. - { rewrite R; auto with asmgen. - apply preg_of_not_X29; auto. - } - { rewrite S; auto. } - -(* X30 does not contain parent *) - exploit loadptr_correct. eexact A. simpl; congruence. intros [rs1 [P [Q R]]]. - exploit loadind_correct. eexact EQ. instantiate (2 := rs1). simpl; rewrite Q. eauto. simpl; congruence. - intros [rs2 [S [T [U V]]]]. - exists rs2; split. eapply exec_straight_trans; eauto. - split. eapply agree_set_mreg. eapply agree_set_mreg. eauto. eauto. - instantiate (1 := rs1#X29 <- (rs2#X29)). intros. - rewrite Pregmap.gso; auto with asmgen. - congruence. - intros. unfold Pregmap.set. destruct (PregEq.eq r' X29). congruence. auto with asmgen. - split; simpl; intros. rewrite U; auto with asmgen. - apply preg_of_not_X29; auto. - rewrite V. rewrite R by congruence. auto. - -- (* Mop *) - assert (eval_operation tge sp op (map 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. - left; eapply exec_straight_steps; eauto; intros. simpl in TR. - exploit transl_op_correct; eauto. intros [rs2 [P [Q [R S]]]]. - exists rs2; split. eauto. split. - apply agree_set_undef_mreg with rs0; auto. - apply Val.lessdef_trans with v'; auto. - split; simpl; intros. InvBooleans. - rewrite R; auto. apply preg_of_not_X29; auto. -Local Transparent destroyed_by_op. - destruct op; try exact I; simpl; congruence. - rewrite S. - auto. -- (* Mload *) - destruct trap. - { - assert (Op.eval_addressing tge sp addr (map 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. - exploit Mem.loadv_extends; eauto. intros [v' [C D]]. - left; eapply exec_straight_steps; eauto; intros. simpl in TR. - exploit transl_load_correct; eauto. intros [rs2 [P [Q [R S]]]]. - exists rs2; split. eauto. - split. eapply agree_set_undef_mreg; eauto. congruence. - split. simpl; congruence. - rewrite S. assumption. - } - - (* Mload notrap1 *) - inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate. - -- (* Mload notrap *) - inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate. - -- (* Mload notrap *) - inv AT. simpl in *. unfold bind in *. destruct (transl_code _ _ _) in *; discriminate. - -- (* Mstore *) - assert (Op.eval_addressing tge sp addr (map 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))) by (eapply preg_val; eauto). - exploit Mem.storev_extends; eauto. intros [m2' [C D]]. - left; eapply exec_straight_steps; eauto. - intros. simpl in TR. exploit transl_store_correct; eauto. intros [rs2 [P [Q R]]]. - exists rs2; split. eauto. - split. eapply agree_undef_regs; eauto with asmgen. - split. simpl; congruence. - rewrite R. assumption. - -- (* Mcall *) - assert (f0 = f) by congruence. subst f0. - inv AT. - assert (NOOV: list_length_z tf.(fn_code) <= Ptrofs.max_unsigned). - { eapply transf_function_no_overflow; eauto. } - destruct ros as [rf|fid]; simpl in H; monadInv H5. -+ (* Indirect call *) - assert (rs rf = Vptr f' Ptrofs.zero). - { destruct (rs rf); try discriminate. - revert H; predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence. } - assert (rs0 x0 = Vptr f' Ptrofs.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 (Ptrofs.add ofs Ptrofs.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. Simpl. rewrite <- H2; simpl; eauto. - eapply functions_transl; eauto. eapply find_instr_tail; eauto. - simpl. eauto. - econstructor; eauto. - econstructor; eauto. - eapply agree_sp_def; eauto. - simpl. eapply agree_exten; eauto. intros. Simpl. - Simpl. rewrite <- H2. auto. -+ (* Direct call *) - generalize (code_tail_next_int _ _ _ _ NOOV H6). intro CT1. - assert (TCA: transl_code_at_pc ge (Vptr fb (Ptrofs.add ofs Ptrofs.one)) fb f c false tf x). + intros until S1. intros Hbb' BSTEP Hbb'' ESTEP MS. + destruct (mbsize bb) eqn:SIZE. + - apply mbsize_eqz in SIZE. destruct SIZE as (Hbody & Hexit). + destruct bb as [hd bdy ex]; simpl in *; subst. + inv MS. inv AT. exploit transl_blocks_nonil; eauto. intros (tbb & tc' & Htc). subst. rename tc' into tc. + monadInv H2. simpl in *. inv ESTEP. inv BSTEP. + eexists. split. + + eapply plus_one. + exploit functions_translated; eauto. intros (tf0 & FIND' & TRANSF'). monadInv TRANSF'. + assert (x = tf) by congruence. subst x. + eapply exec_step_internal; eauto. eapply find_bblock_tail; eauto. + unfold exec_bblock. simpl. + eexists; eexists; split; eauto. + econstructor. + + econstructor. + 1,2,3: eauto. + * + unfold incrPC. rewrite Pregmap.gss. + unfold Val.offset_ptr. rewrite <- H. + assert (NOOV: size_blocks tf.(fn_blocks) <= Ptrofs.max_unsigned). + { eapply transf_function_no_overflow; eauto. } 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 Genv.symbol_address. rewrite symbols_preserved. rewrite H. eauto. - econstructor; eauto. - econstructor; eauto. - eapply agree_sp_def; eauto. - simpl. eapply agree_exten; eauto. intros. Simpl. - Simpl. rewrite <- H2. auto. - -- (* Mtailcall *) - assert (f0 = f) by congruence. subst f0. - inversion AT; subst. - assert (NOOV: list_length_z tf.(fn_code) <= Ptrofs.max_unsigned). - { eapply transf_function_no_overflow; eauto. } - exploit Mem.loadv_extends. eauto. eexact H1. auto. simpl. intros [parent' [A B]]. - destruct ros as [rf|fid]; simpl in H; monadInv H7. -+ (* Indirect call *) - assert (rs rf = Vptr f' Ptrofs.zero). - { destruct (rs rf); try discriminate. - revert H; predSpec Ptrofs.eq Ptrofs.eq_spec i Ptrofs.zero; intros; congruence. } - assert (rs0 x0 = Vptr f' Ptrofs.zero). - { exploit ireg_val; eauto. rewrite H7; intros LD; inv LD; auto. } - exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z). - exploit exec_straight_steps_2; eauto using functions_transl. - intros (ofs' & P & Q). - left; econstructor; split. - (* execution *) - eapply plus_right'. eapply exec_straight_exec; eauto. - econstructor. eexact P. eapply functions_transl; eauto. eapply find_instr_tail. eexact Q. - simpl. reflexivity. - traceEq. - (* match states *) - econstructor; eauto. - apply agree_set_other; auto with asmgen. - Simpl. rewrite Z by (rewrite <- (ireg_of_eq _ _ EQ1); eauto with asmgen). assumption. -+ (* Direct call *) - exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z). - exploit exec_straight_steps_2; eauto using functions_transl. - intros (ofs' & P & Q). - left; econstructor; split. - (* execution *) - eapply plus_right'. eapply exec_straight_exec; eauto. - econstructor. eexact P. eapply functions_transl; eauto. eapply find_instr_tail. eexact Q. - simpl. reflexivity. - traceEq. - (* match states *) - econstructor; eauto. - apply agree_set_other; auto with asmgen. - Simpl. unfold Genv.symbol_address. rewrite symbols_preserved. rewrite H. auto. + generalize (code_tail_next_int _ _ _ _ NOOV H3). intro CT1. eauto. + * + eapply agree_exten; eauto. intros. unfold incrPC. rewrite Pregmap.gso; auto. + unfold data_preg in H2. destruct r; try congruence. + * + intros. discriminate. + - subst. exploit mbsize_neqz. { instantiate (1 := bb). rewrite SIZE. discriminate. } + intros Hnotempty. + + (* initial setting *) + exploit match_state_codestate. + eapply Hnotempty. + all: eauto. + intros (cs1 & fb & f0 & tbb & tc & ep & MCS & MAS & FIND & TLBS & Hbody & Hexit & Hcur & Hrem & Hpstate). + + (* step_simu_header part *) + assert (exists rs1 m1, pstate cs1 = State rs1 m1). { inv MAS. simpl. eauto. } + destruct H as (rs1 & m1 & Hpstate2). subst. + assert (f = fb). { inv MCS. auto. } subst fb. + exploit step_simu_header. + 2: eapply MCS. + all: eauto. + intros (cs1' & EXEH & MCS2). + + (* step_simu_body part *) + assert (Hpstate': pstate cs1' = pstate cs1). { inv EXEH; auto. } + exploit step_simu_body. + 2: eapply BSTEP. + 3: eapply MCS2. + all: eauto. rewrite Hpstate'. eauto. + intros (rs2 & m2 & cs2 & ep' & Hcs2 & EXEB & MCS'). + + (* step_simu_control part *) + assert (exists tf, Genv.find_funct_ptr tge f = Some (Internal tf)). + { exploit functions_translated; eauto. intros (tf & FIND' & TRANSF'). monadInv TRANSF'. eauto. } + destruct H as (tf & FIND'). + inv EXEH. simpl in *. + subst. exploit step_simu_control. + 8: eapply MCS'. all: simpl. + 9: eapply ESTEP. + all: simpl; eauto. + { inv MAS; simpl in *. inv Hpstate2. eapply match_asmstate_some; eauto. + erewrite exec_body_pc; eauto. } + intros (rs3 & m3 & rs4 & m4 & EXEB' & EXECTL' & MS'). + + (* bringing the pieces together *) + exploit exec_body_trans. + eapply EXEB. + eauto. + intros EXEB2. + exploit exec_body_control; eauto. + rewrite <- Hbody in EXEB2. eauto. + rewrite Hexit. eauto. + intros EXECB. (* inv EXECB. *) + exists (State rs4 m4). + split; auto. eapply plus_one. rewrite Hpstate2. + assert (exists ofs, rs1 PC = Vptr f ofs). + { rewrite Hpstate2 in MAS. inv MAS. simpl in *. eauto. } + destruct H as (ofs & Hrs1pc). + eapply exec_step_internal; eauto. + + (* proving the initial find_bblock *) + rewrite Hpstate2 in MAS. inv MAS. simpl in *. + assert (f1 = f0) by congruence. subst f0. + rewrite PCeq in Hrs1pc. inv Hrs1pc. + exploit functions_translated; eauto. intros (tf1 & FIND'' & TRANS''). rewrite FIND' in FIND''. + inv FIND''. monadInv TRANS''. rewrite TRANSF0 in EQ. inv EQ. + eapply find_bblock_tail; eauto. +Qed. -- (* Mbuiltin *) - inv AT. monadInv H4. - exploit functions_transl; eauto. intro FN. - generalize (transf_function_no_overflow _ _ H3); intro NOOV. - exploit builtin_args_match; eauto. intros [vargs' [P Q]]. - exploit external_call_mem_extends; eauto. - intros [vres' [m2' [A [B [C D]]]]]. - left. econstructor; split. apply plus_one. - eapply exec_step_builtin. eauto. eauto. - eapply find_instr_tail; eauto. - erewrite <- sp_val by eauto. - eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. - eapply external_call_symbols_preserved; eauto. apply senv_preserved. - eauto. - econstructor; eauto. - instantiate (2 := tf); instantiate (1 := x). - unfold nextinstr. rewrite Pregmap.gss. - rewrite set_res_other. rewrite undef_regs_other_2. - rewrite <- H1. simpl. econstructor; eauto. - eapply code_tail_next_int; eauto. - rewrite preg_notin_charact. intros. auto with asmgen. - auto with asmgen. - apply agree_nextinstr. eapply agree_set_res; auto. - eapply agree_undef_regs; eauto. intros. rewrite undef_regs_other_2; auto. - congruence. +Theorem step_simulation_bblock: + forall t sf f sp bb ms m ms' m' S2 c, + body_step ge sf f sp (Machblock.body bb) ms m ms' m' -> + exit_step return_address_offset ge (Machblock.exit bb) (Machblock.State sf f sp (bb :: c) ms' m') t S2 -> + forall S1', match_states (Machblock.State sf f sp (bb :: c) ms m) S1' -> + exists S2' : state, plus (step lk) tge S1' t S2' /\ match_states S2 S2'. +Proof. + intros until c. intros BSTEP ESTEP S1' MS. + eapply step_simulation_bblock'; eauto. + all: destruct bb as [hd bdy ex]; simpl in *; eauto. + inv ESTEP. + - econstructor. inv H; try (econstructor; eauto; fail). + - econstructor. +Qed. - Simpl. - rewrite set_res_other by trivial. - rewrite undef_regs_other. - assumption. - intro. - rewrite in_map_iff. - intros (x0 & PREG & IN). - subst r'. - intro. - apply (preg_of_not_RA x0). - congruence. - -- (* Mgoto *) - 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. - eapply functions_transl; eauto. - eapply find_instr_tail; eauto. - simpl; eauto. - econstructor; eauto. - eapply agree_exten; eauto with asmgen. - congruence. +(* Measure to prove finite stuttering, see the other backends *) +Definition measure (s: MB.state) : nat := + match s with + | MB.State _ _ _ _ _ _ => 0%nat + | MB.Callstate _ _ _ _ => 0%nat + | MB.Returnstate _ _ _ => 1%nat + end. - rewrite INV by congruence. - assumption. - -- (* 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_opt_steps_goto; eauto. - intros. simpl in TR. - exploit transl_cond_branch_correct; eauto. intros (rs' & jmp & A & B & C & D). - exists jmp; exists k; exists rs'. - split. eexact A. - split. apply agree_exten with rs0; auto with asmgen. - split. - exact B. - rewrite D. exact LEAF. - -- (* Mcond false *) - exploit eval_condition_lessdef. eapply preg_vals; eauto. eauto. eauto. intros EC. - left; eapply exec_straight_steps; eauto. intros. simpl in TR. - exploit transl_cond_branch_correct; eauto. intros (rs' & jmp & A & B & C & D). - econstructor; split. - eapply exec_straight_opt_right. eexact A. apply exec_straight_one. eexact B. auto. - split. apply agree_exten with rs0; auto. intros. Simpl. - split. - simpl; congruence. - Simpl. rewrite D. - exact LEAF. - -- (* Mjumptable *) - assert (f0 = f) by congruence. subst f0. - inv AT. monadInv H6. - exploit functions_transl; eauto. intro FN. - generalize (transf_function_no_overflow _ _ H5); intro NOOV. - exploit find_label_goto_label. eauto. eauto. - instantiate (2 := rs0#X16 <- Vundef #X17 <- Vundef). - Simpl. eauto. - eauto. - intros [tc' [rs' [A [B C]]]]. - exploit ireg_val; eauto. rewrite H. intros LD; inv LD. - left; econstructor; split. - apply plus_one. econstructor; eauto. - eapply find_instr_tail; eauto. - simpl. Simpl. rewrite <- H9. unfold Mach.label in H0; unfold label; rewrite H0. eexact A. - econstructor; eauto. - eapply agree_undef_regs; eauto. - simpl. intros. rewrite C; auto with asmgen. Simpl. +Lemma next_sep: + forall rs m rs' m', rs = rs' -> m = m' -> Next rs m = Next rs' m'. +Proof. congruence. +Qed. - rewrite C by congruence. - repeat rewrite Pregmap.gso by congruence. - assumption. - -- (* Mreturn *) - assert (f0 = f) by congruence. subst f0. - inversion AT; subst. simpl in H6; monadInv H6. - assert (NOOV: list_length_z tf.(fn_code) <= Ptrofs.max_unsigned). - eapply transf_function_no_overflow; eauto. - exploit make_epilogue_correct; eauto. intros (rs1 & m1 & U & V & W & X & Y & Z). - exploit exec_straight_steps_2; eauto using functions_transl. - intros (ofs' & P & Q). - left; econstructor; split. - (* execution *) - eapply plus_right'. eapply exec_straight_exec; eauto. - econstructor. eexact P. eapply functions_transl; eauto. eapply find_instr_tail. eexact Q. - simpl. reflexivity. - traceEq. - (* match states *) - econstructor; eauto. - apply agree_set_other; auto with asmgen. +(* The actual MB.step/AB.step simulation, using the above theorems, plus extra proofs + for the internal and external function cases *) +Theorem step_simulation: + forall S1 t S2, MB.step return_address_offset ge S1 t S2 -> + forall S1' (MS: match_states S1 S1'), + (exists S2', plus (step lk) tge S1' t S2' /\ match_states S2 S2') + \/ (measure S2 < measure S1 /\ t = E0 /\ match_states S2 S1')%nat. +Proof. + induction 1; intros. +- (* bblock *) + left. destruct (Machblock.exit bb) eqn:MBE; try destruct c0. + all: try(inversion H0; subst; inv H2; eapply step_simulation_bblock; + try (rewrite MBE; try discriminate); eauto). + + inversion H0. subst. eapply step_simulation_bblock; try (rewrite MBE; try discriminate); eauto. - (* internal function *) - + inv MS. exploit functions_translated; eauto. intros [tf [A B]]. monadInv B. generalize EQ; intros EQ'. monadInv EQ'. - destruct (zlt Ptrofs.max_unsigned (list_length_z x0.(fn_code))); inversion EQ1. clear EQ1. subst x0. - unfold store_stack in *. + destruct (zlt Ptrofs.max_unsigned (size_blocks x0.(fn_blocks))); inversion EQ1. clear EQ1. subst x0. + unfold Mach.store_stack in *. exploit Mem.alloc_extends. eauto. eauto. apply Z.le_refl. apply Z.le_refl. intros [m1' [C D]]. exploit Mem.storev_extends. eexact D. eexact H1. eauto. eauto. @@ -1041,49 +1401,70 @@ Local Transparent destroyed_by_op. simpl chunk_of_type in F. exploit Mem.storev_extends. eexact G. eexact H2. eauto. eauto. intros [m3' [P Q]]. - change (chunk_of_type Tptr) with Mint64 in *. (* Execution of function prologue *) - monadInv EQ0. rewrite transl_code'_transl_code in EQ1. - set (tfbody := Pallocframe (fn_stacksize f) (fn_link_ofs f) :: - storeptr RA XSP (fn_retaddr_ofs f) x0) in *. - set (tf := {| fn_sig := Mach.fn_sig f; fn_code := tfbody |}) in *. - set (rs2 := nextinstr (rs0#X29 <- (parent_sp s) #SP <- sp #X16 <- Vundef)). - exploit (storeptr_correct tge tf XSP (fn_retaddr_ofs f) RA x0 m2' m3' rs2). - simpl preg_of_iregsp. change (rs2 X30) with (rs0 X30). rewrite ATLR. - change (rs2 X2) with sp. eexact P. - simpl; congruence. congruence. - intros (rs3 & U & V & W). - assert (EXEC_PROLOGUE: - exec_straight tge tf - tf.(fn_code) rs0 m' - x0 rs3 m3'). - { change (fn_code tf) with tfbody; unfold tfbody. - apply exec_straight_step with rs2 m2'. - unfold exec_instr. rewrite C. fold sp. - rewrite <- (sp_val _ _ _ AG). rewrite F. reflexivity. - reflexivity. - eexact U. } - exploit exec_straight_steps_2; eauto using functions_transl. omega. constructor. - intros (ofs' & X & Y). - left; exists (State rs3 m3'); split. - eapply exec_straight_steps_1; eauto. omega. constructor. + monadInv EQ0. + set (tfbody := make_prologue f x0) in *. + set (tf := {| fn_sig := MB.fn_sig f; fn_blocks := tfbody |}) in *. + set (rs2 := rs0#X29 <- (parent_sp s) #SP <- sp #X16 <- Vundef). + exploit (storeptr_correct lk tge XSP (fn_retaddr_ofs f) RA nil m2' m3' rs2). + { rewrite chunk_of_Tptr in P. + assert (rs0 X30 = rs2 RA) by auto. + rewrite <- H3. + rewrite ATLR. + change (rs2 XSP) with sp. eexact P. } + 1-2: discriminate. + intros (rs3 & U & V). + assert (EXEC_PROLOGUE: exists rs3', + exec_straight_blocks tge lk tf + tf.(fn_blocks) rs0 m' + x0 rs3' m3' + /\ forall r, r <> PC -> r <> X16 -> rs3' r = rs3 r). + { eexists. split. + - change (fn_blocks tf) with tfbody; unfold tfbody. + econstructor; eauto. + assert (Archi.ptr64 = true) as SF; auto. + + unfold exec_bblock. simpl exec_body. + rewrite C. fold sp. rewrite <- (sp_val _ _ _ AG). rewrite chunk_of_Tptr in F. + assert (Mptr = Mint64) by auto. rewrite H3 in F. simpl in F. rewrite F. simpl. + unfold exec_store_rs_a. repeat Simpl; try discriminate. + exists rs2. exists m3'. split. + * unfold eval_addressing. Simpl; try discriminate. rewrite Pregmap.gss. + rewrite chunk_of_Tptr in P. rewrite H3 in P. + unfold Val.addl. unfold Val.offset_ptr in P. + destruct sp; simpl; try discriminate. rewrite SF; simpl. + rewrite Ptrofs.of_int64_to_int64. unfold Mem.storev in P. rewrite ATLR. + rewrite P. simpl. apply next_sep; eauto. apply SF. + * econstructor. + + eauto. + - intros. unfold incrPC. + rewrite Pregmap.gso; auto. rewrite V; auto. + } destruct EXEC_PROLOGUE as (rs3' & EXEC_PROLOGUE & Heqrs3'). + exploit exec_straight_steps_2; eauto using functions_transl. + simpl fn_blocks. simpl fn_blocks in g. omega. constructor. + intros (ofs' & X & Y). + left; exists (State rs3' m3'); split. + eapply exec_straight_steps_1; eauto. + simpl fn_blocks. simpl fn_blocks in g. omega. + constructor. econstructor; eauto. rewrite X; econstructor; eauto. apply agree_exten with rs2; eauto with asmgen. unfold rs2. - apply agree_nextinstr. apply agree_set_other; auto with asmgen. + apply agree_set_other; auto with asmgen. apply agree_change_sp with (parent_sp s). apply agree_undef_regs with rs0. auto. -Local Transparent destroyed_at_function_entry. simpl. - simpl; intros; Simpl. +Local Transparent destroyed_at_function_entry. + simpl; intros; Simpl. auto. + assert (r' <> X29). { contradict H3; rewrite H3; unfold data_preg; auto. } auto. unfold sp; congruence. - intros. rewrite V by auto with asmgen. reflexivity. - rewrite W. - unfold rs2. - Simpl. - + intros. + + rewrite Heqrs3'. rewrite V. 2-5: try apply X16_not_data_preg; try apply PC_not_data_preg; auto. + auto. + intros. rewrite Heqrs3'; try discriminate. rewrite V by auto with asmgen. reflexivity. - (* external function *) + inv MS. exploit functions_translated; eauto. intros [tf [A B]]. simpl in B. inv B. exploit extcall_arguments_match; eauto. @@ -1094,23 +1475,22 @@ Local Transparent destroyed_at_function_entry. simpl. apply plus_one. eapply exec_step_external; eauto. eapply external_call_symbols_preserved; eauto. apply senv_preserved. econstructor; eauto. - unfold loc_external_result. apply agree_set_other; auto. apply agree_set_pair; auto. - apply agree_undef_caller_save_regs; auto. + unfold loc_external_result. + apply agree_set_other; auto. + apply agree_set_pair; auto. + apply agree_undef_caller_save_regs; auto. -- (* return *) +- (* return *) + inv MS. inv STACKS. simpl in *. right. split. omega. split. auto. rewrite <- ATPC in H5. econstructor; eauto. congruence. - inv WF. - inv STACK. - inv H1. - congruence. Qed. Lemma transf_initial_states: - forall st1, Mach.initial_state prog st1 -> - exists st2, Asm.initial_state tprog st2 /\ match_states st1 st2. + forall st1, MB.initial_state prog st1 -> + exists st2, AB.initial_state tprog st2 /\ match_states st1 st2. Proof. intros. inversion H. unfold ge0 in *. econstructor; split. @@ -1122,7 +1502,7 @@ Proof. constructor. apply Mem.extends_refl. split. auto. simpl. unfold Vnullptr; destruct Archi.ptr64; congruence. - intros. rewrite Regmap.gi. auto. + intros. rewrite Mach.Regmap.gi. auto. unfold Genv.symbol_address. rewrite (match_program_main TRANSF). rewrite symbols_preserved. @@ -1131,28 +1511,24 @@ Qed. Lemma transf_final_states: forall st1 st2 r, - match_states st1 st2 -> Mach.final_state st1 r -> Asm.final_state st2 r. + match_states st1 st2 -> MB.final_state st1 r -> AB.final_state st2 r. Proof. intros. inv H0. inv H. constructor. assumption. compute in H1. inv H1. generalize (preg_val _ _ _ R0 AG). rewrite H2. intros LD; inv LD. auto. Qed. -Theorem transf_program_correct: - forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog). +Definition return_address_offset : Machblock.function -> Machblock.code -> ptrofs -> Prop := + Asmblockgenproof0.return_address_offset. + +Lemma transf_program_correct: + forward_simulation (MB.semantics return_address_offset prog) (AB.semantics lk tprog). Proof. - eapply forward_simulation_star with (measure := measure) - (match_states := fun S1 S2 => match_states S1 S2 /\ wf_state ge S1). + eapply forward_simulation_star with (measure := measure). - apply senv_preserved. - - simpl; intros. exploit transf_initial_states; eauto. - intros (s2 & A & B). - exists s2; intuition auto. apply wf_initial; auto. - - simpl; intros. destruct H as [MS WF]. eapply transf_final_states; eauto. - - simpl; intros. destruct H0 as [MS WF]. - exploit step_simulation; eauto. intros [ (s2' & A & B) | (A & B & C) ]. - + left; exists s2'; intuition auto. eapply wf_step; eauto. - + right; intuition auto. eapply wf_step; eauto. + - eexact transf_initial_states. + - eexact transf_final_states. + - exact step_simulation. Qed. End PRESERVATION. -*)
\ No newline at end of file |