diff options
Diffstat (limited to 'aarch64/TO_MERGE/Asmgenproof.v')
-rw-r--r-- | aarch64/TO_MERGE/Asmgenproof.v | 2787 |
1 files changed, 2787 insertions, 0 deletions
diff --git a/aarch64/TO_MERGE/Asmgenproof.v b/aarch64/TO_MERGE/Asmgenproof.v new file mode 100644 index 00000000..8af013fd --- /dev/null +++ b/aarch64/TO_MERGE/Asmgenproof.v @@ -0,0 +1,2787 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* Léo Gourdin UGA, VERIMAG *) +(* Justus Fasse UGA, VERIMAG *) +(* Xavier Leroy INRIA Paris-Rocquencourt *) +(* David Monniaux CNRS, VERIMAG *) +(* Cyril Six Kalray *) +(* *) +(* 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 Asm Asmblock. +Require Machblockgenproof Asmblockgenproof PostpassSchedulingproof. +Require Import Asmgen. +Require Import Axioms. +Require Import IterList. +Require Import Ring Lia. + +Module Asmblock_PRESERVATION. + +Import Asmblock_TRANSF. + +Definition match_prog (p: Asmblock.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: Asmblock.program. +Variable tprog: Asm.program. +Hypothesis TRANSF: match_prog prog tprog. +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + +Definition lk :aarch64_linker := {| Asmblock.symbol_low:=Asm.symbol_low tge; Asmblock.symbol_high:=Asm.symbol_high tge|}. + +Lemma symbols_preserved: + forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. +Proof (Genv.find_symbol_match TRANSF). + +Lemma symbol_addresses_preserved: + forall (s: ident) (ofs: ptrofs), + Genv.symbol_address tge s ofs = Genv.symbol_address ge s ofs. +Proof. + intros; unfold Genv.symbol_address; rewrite symbols_preserved; reflexivity. +Qed. + +Lemma senv_preserved: + Senv.equiv ge tge. +Proof (Genv.senv_match TRANSF). + +Lemma symbol_high_low: forall (id: ident) (ofs: ptrofs), + Val.addl (Asmblock.symbol_high lk id ofs) (Asmblock.symbol_low lk id ofs) = Genv.symbol_address ge id ofs. +Proof. + unfold lk; simpl. intros; rewrite Asm.symbol_high_low; unfold Genv.symbol_address; + rewrite symbols_preserved; reflexivity. +Qed. + +Lemma functions_translated: + forall b f, + Genv.find_funct_ptr ge b = Some f -> + exists tf, + Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf. +Proof (Genv.find_funct_ptr_transf_partial TRANSF). + +Lemma internal_functions_translated: + forall b f, + Genv.find_funct_ptr ge b = Some (Internal f) -> + exists tf, + Genv.find_funct_ptr tge b = Some (Internal tf) /\ transf_function f = OK tf. +Proof. + intros; exploit functions_translated; eauto. + intros (x & FIND & TRANSf). + apply bind_inversion in TRANSf. + destruct TRANSf as (tf & TRANSf & X). + inv X. + eauto. +Qed. + +Lemma internal_functions_unfold: + forall b f, + Genv.find_funct_ptr ge b = Some (Internal f) -> + exists tc, + Genv.find_funct_ptr tge b = Some (Internal (Asm.mkfunction (fn_sig f) tc)) + /\ unfold (fn_blocks f) = OK tc + /\ list_length_z tc <= Ptrofs.max_unsigned. +Proof. + intros. + exploit internal_functions_translated; eauto. + intros (tf & FINDtf & TRANStf). + unfold transf_function in TRANStf. + monadInv TRANStf. + destruct (zlt _ _); try congruence. + inv EQ. inv EQ0. + eexists; intuition eauto. + lia. +Qed. + + +Inductive is_nth_inst (bb: bblock) (n:Z) (i:Asm.instruction): Prop := + | is_nth_label l: + list_nth_z (header bb) n = Some l -> + i = Asm.Plabel l -> + is_nth_inst bb n i + | is_nth_basic bi: + list_nth_z (body bb) (n - list_length_z (header bb)) = Some bi -> + basic_to_instruction bi = OK i -> + is_nth_inst bb n i + | is_nth_ctlflow cfi: + (exit bb) = Some cfi -> + n = size bb - 1 -> + i = control_to_instruction cfi -> + is_nth_inst bb n i. + +(* Asmblock and Asm share the same definition of state *) +Definition match_states (s1 s2 : state) := s1 = s2. + +Inductive match_internal: forall n, state -> state -> Prop := + | match_internal_intro n rs1 m1 rs2 m2 + (MEM: m1 = m2) + (AG: forall r, r <> PC -> rs1 r = rs2 r) + (AGPC: Val.offset_ptr (rs1 PC) (Ptrofs.repr n) = rs2 PC) + : match_internal n (State rs1 m1) (State rs2 m2). + +Lemma match_internal_set_parallel: + forall n rs1 m1 rs2 m2 r val, + match_internal n (State rs1 m1) (State rs2 m2) -> + r <> PC -> + match_internal n (State (rs1#r <- val) m1) (State (rs2#r <- val ) m2). +Proof. + intros n rs1 m1 rs2 m2 r v MI. + inversion MI; constructor; auto. + - intros r' NOTPC. + unfold Pregmap.set; rewrite AG. reflexivity. assumption. + - unfold Pregmap.set; destruct (PregEq.eq PC r); congruence. +Qed. + +Lemma agree_match_states: + forall rs1 m1 rs2 m2, + match_states (State rs1 m1) (State rs2 m2) -> + forall r : preg, rs1#r = rs2#r. +Proof. + intros. + unfold match_states in *. + assert (rs1 = rs2) as EQ. { congruence. } + rewrite EQ. reflexivity. +Qed. + +Lemma match_states_set_parallel: + forall rs1 m1 rs2 m2 r v, + match_states (State rs1 m1) (State rs2 m2) -> + match_states (State (rs1#r <- v) m1) (State (rs2#r <- v) m2). +Proof. + intros; unfold match_states in *. + assert (rs1 = rs2) as RSEQ. { congruence. } + assert (m1 = m2) as MEQ. { congruence. } + rewrite RSEQ in *; rewrite MEQ in *; unfold Pregmap.set; reflexivity. +Qed. + +(* match_internal from match_states *) +Lemma mi_from_ms: + forall rs1 m1 rs2 m2 b ofs, + match_states (State rs1 m1) (State rs2 m2) -> + rs1#PC = Vptr b ofs -> + match_internal 0 (State rs1 m1) (State rs2 m2). +Proof. + intros rs1 m1 rs2 m2 b ofs MS PCVAL. + inv MS; constructor; auto; unfold Val.offset_ptr; + rewrite PCVAL; rewrite Ptrofs.add_zero; reflexivity. +Qed. + +Lemma transf_initial_states: + forall s1, Asmblock.initial_state prog s1 -> + exists s2, Asm.initial_state tprog s2 /\ match_states s1 s2. +Proof. + intros ? INIT_s1. + inversion INIT_s1 as (m, ?, ge0, rs). unfold ge0 in *. + econstructor; split. + - econstructor. + eapply (Genv.init_mem_transf_partial TRANSF); eauto. + - rewrite (match_program_main TRANSF); rewrite symbol_addresses_preserved. + unfold rs; reflexivity. +Qed. + +Lemma transf_final_states: + forall s1 s2 r, + match_states s1 s2 -> Asmblock.final_state s1 r -> Asm.final_state s2 r. +Proof. + intros s1 s2 r MATCH FINAL_s1. + inv FINAL_s1; inv MATCH; constructor; assumption. +Qed. + +Definition max_pos (f : Asm.function) := list_length_z f.(Asm.fn_code). + +Lemma functions_bound_max_pos: forall fb f tf, + Genv.find_funct_ptr ge fb = Some (Internal f) -> + transf_function f = OK tf -> +<<<<<<< HEAD + max_pos tf <= Ptrofs.max_unsigned. +Proof. + intros fb f tf FINDf TRANSf. + unfold transf_function in TRANSf. + apply bind_inversion in TRANSf. + destruct TRANSf as (c & TRANSf). + destruct TRANSf as (_ & TRANSf). + destruct (zlt _ _). + - inversion TRANSf. + - unfold max_pos. + assert (Asm.fn_code tf = c) as H. { inversion TRANSf as (H'); auto. } + rewrite H; lia. +Qed. +======= + Genv.find_funct_ptr tge fb = Some (Internal tf). +Proof. + intros. exploit functions_translated; eauto. intros [tf' [A B]]. + 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. +Proof. + intros. monadInv H. destruct (zlt Ptrofs.max_unsigned (list_length_z x.(fn_code))); inv EQ0. + lia. +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. + +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. + +(** The following lemmas show that the translation from Mach to Asm + preserves labels, in the sense that the following diagram commutes: +<< + translation + Mach code ------------------------ Asm instr sequence + | | + | Mach.find_label lbl find_label lbl | + | | + v v + Mach code tail ------------------- Asm instr seq tail + translation +>> + The proof demands many boring lemmas showing that Asm constructor + functions do not introduce new labels. +*) +>>>>>>> master + +Lemma one_le_max_unsigned: + 1 <= Ptrofs.max_unsigned. +Proof. + unfold Ptrofs.max_unsigned; simpl; unfold Ptrofs.wordsize; + unfold Wordsize_Ptrofs.wordsize; destruct Archi.ptr64; simpl; lia. +Qed. + +(* NB: does not seem useful anymore, with the [exec_header_simulation] proof below +Lemma match_internal_exec_label: + forall n rs1 m1 rs2 m2 l fb f tf, + Genv.find_funct_ptr ge fb = Some (Internal f) -> + transf_function f = OK tf -> + match_internal n (State rs1 m1) (State rs2 m2) -> + n >= 0 -> + (* There is no step if n is already max_pos *) + n < (max_pos tf) -> + exists rs2' m2', Asm.exec_instr tge tf (Asm.Plabel l) rs2 m2 = Next rs2' m2' + /\ match_internal (n+1) (State rs1 m1) (State rs2' m2'). +Proof. + intros. (* XXX auto generated names *) + unfold Asm.exec_instr. + eexists; eexists; split; eauto. + inversion H1; constructor; auto. + - intros; unfold Asm.nextinstr; unfold Pregmap.set; + destruct (PregEq.eq r PC); auto; contradiction. + - unfold Asm.nextinstr; rewrite Pregmap.gss; unfold Ptrofs.one. + rewrite <- AGPC; rewrite Val.offset_ptr_assoc; unfold Ptrofs.add; + rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr; trivial. + + split. + * apply Z.le_0_1. + * apply one_le_max_unsigned. + + split. + * apply Z.ge_le; assumption. + * rewrite <- functions_bound_max_pos; eauto; lia. +Qed. +*) + +Lemma incrPC_agree_but_pc: + forall rs r ofs, + r <> PC -> + (incrPC ofs rs)#r = rs#r. +Proof. + intros rs r ofs NOTPC. + unfold incrPC; unfold Pregmap.set; destruct (PregEq.eq r PC). + - contradiction. + - reflexivity. +Qed. + +Lemma bblock_non_empty bb: body bb <> nil \/ exit bb <> None. +Proof. + destruct bb. simpl. + unfold non_empty_bblockb in correct. + unfold non_empty_body, non_empty_exit, Is_true in correct. + destruct body, exit. + - right. discriminate. + - contradiction. + - right. discriminate. + - left. discriminate. +Qed. + +Lemma list_length_z_aux_increase A (l: list A): forall acc, + list_length_z_aux l acc >= acc. +Proof. + induction l; simpl; intros. + - lia. + - generalize (IHl (Z.succ acc)). lia. +Qed. + +Lemma bblock_size_aux_pos bb: list_length_z (body bb) + Z.of_nat (length_opt (exit bb)) >= 1. +Proof. + destruct (bblock_non_empty bb), (body bb) as [|hd tl], (exit bb); simpl; + try (congruence || lia); + unfold list_length_z; simpl; + generalize (list_length_z_aux_increase _ tl 1); lia. +Qed. + + +Lemma list_length_add_acc A (l : list A) acc: + list_length_z_aux l acc = (list_length_z l) + acc. +Proof. + unfold list_length_z, list_length_z_aux. simpl. + fold list_length_z_aux. + rewrite (list_length_z_aux_shift l acc 0). + lia. +Qed. + +Lemma list_length_z_cons A hd (tl : list A): + list_length_z (hd :: tl) = list_length_z tl + 1. +Proof. + unfold list_length_z; simpl; rewrite list_length_add_acc; reflexivity. +Qed. + +Lemma bblock_size_aux bb: size bb = list_length_z (header bb) + list_length_z (body bb) + Z.of_nat (length_opt (exit bb)). +Proof. + unfold size. + repeat (rewrite list_length_z_nat). repeat (rewrite Nat2Z.inj_add). reflexivity. +Qed. + +Lemma header_size_lt_block_size bb: + list_length_z (header bb) < size bb. +Proof. + rewrite bblock_size_aux. + generalize (bblock_non_empty bb); intros NEMPTY; destruct NEMPTY as [HDR|EXIT]. + - destruct (body bb); try contradiction; rewrite list_length_z_cons; + repeat rewrite list_length_z_nat; lia. + - destruct (exit bb); try contradiction; simpl; repeat rewrite list_length_z_nat; lia. +Qed. + +Lemma body_size_le_block_size bb: + list_length_z (body bb) <= size bb. +Proof. + rewrite bblock_size_aux; repeat rewrite list_length_z_nat; lia. +Qed. + + +Lemma bblock_size_pos bb: size bb >= 1. +Proof. + rewrite (bblock_size_aux bb). + generalize (bblock_size_aux_pos bb). + generalize (list_length_z_pos (header bb)). + lia. +Qed. + +Lemma unfold_car_cdr bb bbs tc: + unfold (bb :: bbs) = OK tc -> + exists tbb tc', unfold_bblock bb = OK tbb + /\ unfold bbs = OK tc' + /\ unfold (bb :: bbs) = OK (tbb ++ tc'). +Proof. + intros UNFOLD. + assert (UF := UNFOLD). + unfold unfold in UNFOLD. + apply bind_inversion in UNFOLD. destruct UNFOLD as (? & UBB). destruct UBB as (UBB & REST). + apply bind_inversion in REST. destruct REST as (? & UNFOLD'). + fold unfold in UNFOLD'. destruct UNFOLD' as (UNFOLD' & UNFOLD). + rewrite <- UNFOLD in UF. + eauto. +Qed. + +Lemma unfold_cdr bb bbs tc: + unfold (bb :: bbs) = OK tc -> + exists tc', unfold bbs = OK tc'. +Proof. +<<<<<<< HEAD + intros; exploit unfold_car_cdr; eauto. intros (_ & ? & _ & ? & _). + eexists; eauto. +Qed. +======= + intros; unfold loadsymbol. + destruct (SelectOp.symbol_is_relocatable id); TailNoLabel. destruct Ptrofs.eq; TailNoLabel. +Qed. +Hint Resolve loadsymbol_label: labels. +>>>>>>> master + +Lemma unfold_car bb bbs tc: + unfold (bb :: bbs) = OK tc -> + exists tbb, unfold_bblock bb = OK tbb. +Proof. + intros; exploit unfold_car_cdr; eauto. intros (? & _ & ? & _ & _). + eexists; eauto. +Qed. + +Lemma all_blocks_translated: + forall bbs tc, + unfold bbs = OK tc -> + forall bb, In bb bbs -> + exists c, unfold_bblock bb = OK c. +Proof. + induction bbs as [| bb bbs IHbbs]. + - contradiction. + - intros ? UNFOLD ? IN. + (* unfold proceeds by unfolding the basic block at the head of the list and + * then recurring *) + exploit unfold_car_cdr; eauto. intros (? & ? & ? & ? & _). + (* basic block is either in head or tail *) + inversion IN as [EQ | NEQ]. + + rewrite <- EQ; eexists; eauto. + + eapply IHbbs; eauto. +Qed. + +Lemma entire_body_translated: + forall lbi tc, + unfold_body lbi = OK tc -> + forall bi, In bi lbi -> + exists bi', basic_to_instruction bi = OK bi'. +Proof. + induction lbi as [| a lbi IHlbi]. + - intros. contradiction. + - intros tc UNFOLD_BODY bi IN. + unfold unfold_body in UNFOLD_BODY. apply bind_inversion in UNFOLD_BODY. + destruct UNFOLD_BODY as (? & TRANSbi & REST). + apply bind_inversion in REST. destruct REST as (? & UNFOLD_BODY' & ?). + fold unfold_body in UNFOLD_BODY'. + + inversion IN as [EQ | NEQ]. + + rewrite <- EQ; eauto. + + eapply IHlbi; eauto. +Qed. + +Lemma bblock_in_bblocks bbs bb: forall + tc pos + (UNFOLD: unfold bbs = OK tc) + (FINDBB: find_bblock pos bbs = Some bb), + In bb bbs. +Proof. + induction bbs as [| b bbs IH]. + - intros. inversion FINDBB. + - destruct pos. + + intros. inversion FINDBB as (EQ). rewrite <- EQ. apply in_eq. + + intros. + exploit unfold_cdr; eauto. intros (tc' & UNFOLD'). + unfold find_bblock in FINDBB. simpl in FINDBB. + fold find_bblock in FINDBB. + apply in_cons. eapply IH; eauto. + + intros. inversion FINDBB. +Qed. + +Lemma blocks_translated tc pos bbs bb: forall + (UNFOLD: unfold bbs = OK tc) + (FINDBB: find_bblock pos bbs = Some bb), + exists tbb, unfold_bblock bb = OK tbb. +Proof. + intros; exploit bblock_in_bblocks; eauto; intros; + eapply all_blocks_translated; eauto. +Qed. + +Lemma size_header b pos f bb: forall + (FINDF: Genv.find_funct_ptr ge b = Some (Internal f)) + (FINDBB: find_bblock pos (fn_blocks f) = Some bb), + list_length_z (header bb) <= 1. +Proof. + intros. + exploit internal_functions_unfold; eauto. + intros (tc & FINDtf & TRANStf & ?). + exploit blocks_translated; eauto. intros TBB. + + unfold unfold_bblock in TBB. + destruct (zle (list_length_z (header bb)) 1). + - assumption. + - destruct TBB as (? & TBB). discriminate TBB. +Qed. + +Lemma list_nth_z_neg A (l: list A): forall n, + n < 0 -> list_nth_z l n = None. +Proof. + induction l; simpl; auto. + intros n H; destruct (zeq _ _); (try eapply IHl); lia. +Qed. + +Lemma find_bblock_neg bbs: forall pos, + pos < 0 -> find_bblock pos bbs = None. +Proof. + induction bbs; simpl; auto. + intros. destruct (zlt pos 0). { reflexivity. } + destruct (zeq pos 0); contradiction. +Qed. + +Lemma equal_header_size bb: + length (header bb) = length (unfold_label (header bb)). +Proof. + induction (header bb); auto. + simpl. rewrite IHl. auto. +Qed. + +Lemma equal_body_size: + forall bb tb, + unfold_body (body bb) = OK tb -> + length (body bb) = length tb. +Proof. + intros bb. induction (body bb). + - simpl. intros ? H. inversion H. auto. + - intros tb H. simpl in H. apply bind_inversion in H. destruct H as (? & BI & TAIL). + apply bind_inversion in TAIL. destruct TAIL as (tb' & BODY' & CONS). inv CONS. + simpl. specialize (IHl tb' BODY'). rewrite IHl. reflexivity. +Qed. + +Lemma equal_exit_size bb: + length_opt (exit bb) = length (unfold_exit (exit bb)). +Proof. + destruct (exit bb); trivial. +Qed. + +Lemma bblock_size_preserved bb tb: + unfold_bblock bb = OK tb -> + size bb = list_length_z tb. +Proof. + unfold unfold_bblock. intros UNFOLD_BBLOCK. + destruct (zle (list_length_z (header bb)) 1). 2: { inversion UNFOLD_BBLOCK. } + apply bind_inversion in UNFOLD_BBLOCK. destruct UNFOLD_BBLOCK as (? & UNFOLD_BODY & CONS). + inversion CONS. + unfold size. + rewrite equal_header_size, equal_exit_size. + erewrite equal_body_size; eauto. + rewrite list_length_z_nat. + repeat (rewrite app_length). + rewrite plus_assoc. auto. +Qed. + +Lemma size_of_blocks_max_pos_aux: + forall bbs tbbs pos bb, + find_bblock pos bbs = Some bb -> + unfold bbs = OK tbbs -> + pos + size bb <= list_length_z tbbs. +Proof. + induction bbs as [| bb ? IHbbs]. + - intros tbbs ? ? FINDBB; inversion FINDBB. + - simpl; intros tbbs pos bb' FINDBB UNFOLD. + apply bind_inversion in UNFOLD; destruct UNFOLD as (tbb & UNFOLD_BBLOCK & H). + apply bind_inversion in H; destruct H as (tbbs' & UNFOLD & CONS). + inv CONS. + destruct (zlt pos 0). { discriminate FINDBB. } + destruct (zeq pos 0). + + inv FINDBB. + exploit bblock_size_preserved; eauto; intros SIZE; rewrite SIZE. + repeat (rewrite list_length_z_nat). rewrite app_length, Nat2Z.inj_add. + lia. + + generalize (IHbbs tbbs' (pos - size bb) bb' FINDBB UNFOLD). intros IH. + exploit bblock_size_preserved; eauto; intros SIZE. + repeat (rewrite list_length_z_nat); rewrite app_length. + rewrite Nat2Z.inj_add; repeat (rewrite <- list_length_z_nat). + lia. +Qed. + +Lemma size_of_blocks_max_pos pos f tf bi: + find_bblock pos (fn_blocks f) = Some bi -> + transf_function f = OK tf -> + pos + size bi <= max_pos tf. +Proof. + unfold transf_function, max_pos. + intros FINDBB UNFOLD. + apply bind_inversion in UNFOLD. destruct UNFOLD as (? & UNFOLD & H). + destruct (zlt Ptrofs.max_unsigned (list_length_z x)). { discriminate H. } + inv H. simpl. + eapply size_of_blocks_max_pos_aux; eauto. +Qed. + +Lemma unfold_bblock_not_nil bb: + unfold_bblock bb = OK nil -> False. +Proof. + intros. + exploit bblock_size_preserved; eauto. unfold list_length_z; simpl. intros SIZE. + generalize (bblock_size_pos bb). intros SIZE'. lia. +Qed. + +(* same proof as list_nth_z_range (Coqlib) *) +Lemma find_instr_range: + forall c n i, + Asm.find_instr n c = Some i -> 0 <= n < list_length_z c. +Proof. + induction c; simpl; intros. + discriminate. + rewrite list_length_z_cons. destruct (zeq n 0). + generalize (list_length_z_pos c); lia. + exploit IHc; eauto. lia. +Qed. + +Lemma find_instr_tail: + forall tbb pos c i, + Asm.find_instr pos c = Some i -> + Asm.find_instr (pos + list_length_z tbb) (tbb ++ c) = Some i. +Proof. + induction tbb as [| ? ? IHtbb]. + - intros. unfold list_length_z; simpl. rewrite Z.add_0_r. assumption. + - intros. rewrite list_length_z_cons. simpl. + destruct (zeq (pos + (list_length_z tbb + 1)) 0). + + exploit find_instr_range; eauto. intros POS_RANGE. + generalize (list_length_z_pos tbb). lia. + + replace (pos + (list_length_z tbb + 1) - 1) with (pos + list_length_z tbb) by lia. + eapply IHtbb; eauto. +Qed. + +Lemma size_of_blocks_bounds fb pos f bi: + Genv.find_funct_ptr ge fb = Some (Internal f) -> + find_bblock pos (fn_blocks f) = Some bi -> + pos + size bi <= Ptrofs.max_unsigned. +Proof. + intros; exploit internal_functions_translated; eauto. + intros (tf & _ & TRANSf). + assert (pos + size bi <= max_pos tf). { eapply size_of_blocks_max_pos; eauto. } + assert (max_pos tf <= Ptrofs.max_unsigned). { eapply functions_bound_max_pos; eauto. } + lia. +Qed. + +Lemma find_instr_bblock_tail: + forall tbb bb pos c i, + Asm.find_instr pos c = Some i -> + unfold_bblock bb = OK tbb -> + Asm.find_instr (pos + size bb ) (tbb ++ c) = Some i. +Proof. + induction tbb. + - intros. exploit unfold_bblock_not_nil; eauto. intros. contradiction. + - intros. simpl. + destruct (zeq (pos + size bb) 0). + + (* absurd *) + exploit find_instr_range; eauto. intros POS_RANGE. + generalize (bblock_size_pos bb). intros SIZE. lia. + + erewrite bblock_size_preserved; eauto. + rewrite list_length_z_cons. + replace (pos + (list_length_z tbb + 1) - 1) with (pos + list_length_z tbb) by lia. + apply find_instr_tail; auto. +Qed. + +Lemma list_nth_z_find_label: + forall (ll : list label) il n l, + list_nth_z ll n = Some l -> + Asm.find_instr n ((unfold_label ll) ++ il) = Some (Asm.Plabel l). +Proof. + induction ll. + - intros. inversion H. + - intros. simpl. + destruct (zeq n 0) as [Z | NZ]. + + inversion H as (H'). rewrite Z in H'. simpl in H'. inv H'. reflexivity. + + simpl in H. destruct (zeq n 0). { contradiction. } + apply IHll; auto. +Qed. + +Lemma list_nth_z_find_bi: + forall lbi bi tlbi n bi' exit, + list_nth_z lbi n = Some bi -> + unfold_body lbi = OK tlbi -> + basic_to_instruction bi = OK bi' -> + Asm.find_instr n (tlbi ++ exit) = Some bi'. +Proof. + induction lbi. + - intros. inversion H. + - simpl. intros. + apply bind_inversion in H0. destruct H0 as (? & ? & ?). + apply bind_inversion in H2. destruct H2 as (? & ? & ?). + destruct (zeq n 0) as [Z | NZ]. + + destruct n. + * inversion H as (BI). rewrite BI in *. + inversion H3. simpl. congruence. + * (* absurd *) congruence. + * (* absurd *) congruence. + + inv H3. simpl. destruct (zeq n 0). { contradiction. } + eapply IHlbi; eauto. +Qed. + +Lemma list_nth_z_find_bi_with_header: + forall ll lbi bi tlbi n bi' (rest : list Asm.instruction), + list_nth_z lbi (n - list_length_z ll) = Some bi -> + unfold_body lbi = OK tlbi -> + basic_to_instruction bi = OK bi' -> + Asm.find_instr n ((unfold_label ll) ++ (tlbi) ++ (rest)) = Some bi'. +Proof. + induction ll. + - unfold list_length_z. simpl. intros. + replace (n - 0) with n in H by lia. eapply list_nth_z_find_bi; eauto. + - intros. simpl. destruct (zeq n 0). + + rewrite list_length_z_cons in H. rewrite e in H. + replace (0 - (list_length_z ll + 1)) with (-1 - (list_length_z ll)) in H by lia. + generalize (list_length_z_pos ll). intros. + rewrite list_nth_z_neg in H; try lia. inversion H. + + rewrite list_length_z_cons in H. + replace (n - (list_length_z ll + 1)) with (n -1 - (list_length_z ll)) in H by lia. + eapply IHll; eauto. +Qed. + +(* XXX unused *) +Lemma range_list_nth_z: + forall (A: Type) (l: list A) n, + 0 <= n < list_length_z l -> + exists x, list_nth_z l n = Some x. +Proof. + induction l. + - intros. unfold list_length_z in H. simpl in H. lia. + - intros n. destruct (zeq n 0). + + intros. simpl. destruct (zeq n 0). { eauto. } contradiction. + + intros H. rewrite list_length_z_cons in H. + simpl. destruct (zeq n 0). { contradiction. } + replace (Z.pred n) with (n - 1) by lia. + eapply IHl; lia. +Qed. + +Lemma list_nth_z_n_too_big: + forall (A: Type) (l: list A) n, + 0 <= n -> + list_nth_z l n = None -> + n >= list_length_z l. +Proof. + induction l. + - intros. unfold list_length_z. simpl. lia. + - intros. rewrite list_length_z_cons. + simpl in H0. + destruct (zeq n 0) as [N | N]. + + inversion H0. + + (* XXX there must be a more elegant way to prove this simple fact *) + assert (n > 0). { lia. } + assert (0 <= n - 1). { lia. } + generalize (IHl (n - 1)). intros IH. + assert (n - 1 >= list_length_z l). { auto. } + assert (n > list_length_z l); lia. +Qed. + +Lemma find_instr_past_header: + forall labels n rest, + list_nth_z labels n = None -> + Asm.find_instr n (unfold_label labels ++ rest) = + Asm.find_instr (n - list_length_z labels) rest. +Proof. + induction labels as [| label labels' IH]. + - unfold list_length_z; simpl; intros; rewrite Z.sub_0_r; reflexivity. + - intros. simpl. destruct (zeq n 0) as [N | N]. + + rewrite N in H. inversion H. + + rewrite list_length_z_cons. + replace (n - (list_length_z labels' + 1)) with (n - 1 - list_length_z labels') by lia. + simpl in H. destruct (zeq n 0). { contradiction. } + replace (Z.pred n) with (n - 1) in H by lia. + apply IH; auto. +Qed. + +(* very similar to find_instr_past_header *) +Lemma find_instr_past_body: + forall lbi n tlbi rest, + list_nth_z lbi n = None -> + unfold_body lbi = OK tlbi -> + Asm.find_instr n (tlbi ++ rest) = + Asm.find_instr (n - list_length_z lbi) rest. +Proof. + induction lbi. + - unfold list_length_z; simpl; intros ? ? ? ? H. inv H; rewrite Z.sub_0_r; reflexivity. + - intros n tlib ? NTH UNFOLD_BODY. + unfold unfold_body in UNFOLD_BODY. apply bind_inversion in UNFOLD_BODY. + destruct UNFOLD_BODY as (? & BI & H). + apply bind_inversion in H. destruct H as (? & UNFOLD_BODY' & CONS). + fold unfold_body in UNFOLD_BODY'. inv CONS. + simpl; destruct (zeq n 0) as [N|N]. + + rewrite N in NTH; inversion NTH. + + rewrite list_length_z_cons. + replace (n - (list_length_z lbi + 1)) with (n - 1 - list_length_z lbi) by lia. + simpl in NTH. destruct (zeq n 0). { contradiction. } + replace (Z.pred n) with (n - 1) in NTH by lia. + apply IHlbi; auto. +Qed. + +Lemma n_beyond_body: + forall bb n, + 0 <= n < size bb -> + list_nth_z (header bb) n = None -> + list_nth_z (body bb) (n - list_length_z (header bb)) = None -> + n >= Z.of_nat (length (header bb) + length (body bb)). +Proof. + intros. + assert (0 <= n). { lia. } + generalize (list_nth_z_n_too_big label (header bb) n H2 H0). intros. + generalize (list_nth_z_n_too_big _ (body bb) (n - list_length_z (header bb))). intros. + unfold size in H. + + assert (0 <= n - list_length_z (header bb)). { lia. } + assert (n - list_length_z (header bb) >= list_length_z (body bb)). { apply H4; auto. } + + assert (n >= list_length_z (header bb) + list_length_z (body bb)). { lia. } + rewrite Nat2Z.inj_add. + repeat (rewrite <- list_length_z_nat). assumption. +Qed. + +Lemma exec_arith_instr_dont_move_PC ai rs rs': forall + (BASIC: exec_arith_instr lk ai rs = rs'), + rs PC = rs' PC. +Proof. + destruct ai; simpl; intros; + try (rewrite <- BASIC; rewrite Pregmap.gso; auto; discriminate). + - destruct i; simpl in BASIC; + try destruct (negb _); rewrite <- BASIC; + repeat rewrite Pregmap.gso; try discriminate; reflexivity. + - destruct i; simpl in BASIC. + 1,2: rewrite <- BASIC; repeat rewrite Pregmap.gso; try discriminate; reflexivity. + destruct sz; + try (unfold compare_single in BASIC || unfold compare_float in BASIC); + destruct (rs r1), (rs r2); + try (rewrite <- BASIC; repeat rewrite Pregmap.gso; try (discriminate || reflexivity)). + - destruct i; simpl in BASIC; + destruct is; + try (unfold compare_int in BASIC || unfold compare_long in BASIC); + try (rewrite <- BASIC; repeat rewrite Pregmap.gso; try (discriminate || reflexivity)). + - destruct i; simpl in BASIC; destruct sz; + try (unfold compare_single in BASIC || unfold compare_float in BASIC); + destruct (rs r1); + try (rewrite <- BASIC; repeat rewrite Pregmap.gso; try (discriminate || reflexivity)). + - destruct fsz; rewrite <- BASIC; rewrite Pregmap.gso; try (discriminate || reflexivity). + - destruct fsz; rewrite <- BASIC; rewrite Pregmap.gso; try (discriminate || reflexivity). +Qed. + +Lemma exec_basic_dont_move_PC bi rs m rs' m': forall + (BASIC: exec_basic lk ge bi rs m = Next rs' m'), + rs PC = rs' PC. +Proof. + destruct bi; simpl; intros. + - inv BASIC. exploit exec_arith_instr_dont_move_PC; eauto. + - unfold exec_load in BASIC. + destruct ld. + + unfold exec_load_rd_a in BASIC. + destruct Mem.loadv. 2: { discriminate BASIC. } + inv BASIC. rewrite Pregmap.gso; try discriminate; auto. + + unfold exec_load_double, is_pair_addressing_mode_correct in BASIC. + destruct a; try discriminate BASIC. + do 2 (destruct Mem.loadv; try discriminate BASIC). + inv BASIC. rewrite Pregmap.gso; try discriminate; auto. + - unfold exec_store in BASIC. + destruct st. + + unfold exec_store_rs_a in BASIC. + destruct Mem.storev. 2: { discriminate BASIC. } + inv BASIC; reflexivity. + + unfold exec_store_double in BASIC. + destruct a; try discriminate BASIC. + do 2 (destruct Mem.storev; try discriminate BASIC). + inv BASIC; reflexivity. + - destruct Mem.alloc, Mem.store. 2: { discriminate BASIC. } + inv BASIC. repeat (rewrite Pregmap.gso; try discriminate). reflexivity. + - destruct Mem.loadv. 2: { discriminate BASIC. } + destruct rs, Mem.free; try discriminate BASIC. + inv BASIC; rewrite Pregmap.gso; try discriminate; auto. + - inv BASIC; rewrite Pregmap.gso; try discriminate; auto. + - inv BASIC; rewrite Pregmap.gso; try discriminate; auto. + - inv BASIC; rewrite Pregmap.gso; try discriminate; auto. + - inv BASIC; rewrite Pregmap.gso; try discriminate; auto. + - inv BASIC; auto. +Qed. + +Lemma exec_body_dont_move_PC_aux: + forall bis rs m rs' m' + (BODY: exec_body lk ge bis rs m = Next rs' m'), + rs PC = rs' PC. +Proof. + induction bis. + - intros; inv BODY; reflexivity. + - simpl; intros. + remember (exec_basic lk ge a rs m) as bi eqn:BI; destruct bi. 2: { discriminate BODY. } + symmetry in BI; destruct s in BODY, BI; simpl in BODY, BI. + exploit exec_basic_dont_move_PC; eauto; intros AGPC; rewrite AGPC. + eapply IHbis; eauto. +Qed. + +Lemma exec_body_dont_move_PC bb rs m rs' m': forall + (BODY: exec_body lk ge (body bb) rs m = Next rs' m'), + rs PC = rs' PC. +Proof. apply exec_body_dont_move_PC_aux. Qed. + +Lemma find_instr_bblock: + forall n lb pos bb tlb + (FINDBB: find_bblock pos lb = Some bb) + (UNFOLD: unfold lb = OK tlb) + (SIZE: 0 <= n < size bb), + exists i, is_nth_inst bb n i /\ Asm.find_instr (pos+n) tlb = Some i. +Proof. + induction lb as [| b lb IHlb]. + - intros. inversion FINDBB. + - intros pos bb tlb FINDBB UNFOLD SIZE. + destruct pos. + + inv FINDBB. simpl. + exploit unfold_car_cdr; eauto. intros (tbb & tlb' & UNFOLD_BBLOCK & UNFOLD' & UNFOLD_cons). + rewrite UNFOLD in UNFOLD_cons. inversion UNFOLD_cons. + unfold unfold_bblock in UNFOLD_BBLOCK. + destruct (zle (list_length_z (header bb)) 1). 2: { inversion UNFOLD_BBLOCK. } + apply bind_inversion in UNFOLD_BBLOCK. + destruct UNFOLD_BBLOCK as (? & UNFOLD_BODY & H). + inversion H as (UNFOLD_BBLOCK). + remember (list_nth_z (header bb) n) as label_opt eqn:LBL. destruct label_opt. + * (* nth instruction is a label *) + eexists; split. { eapply is_nth_label; eauto. } + inversion UNFOLD_cons. + symmetry in LBL. + rewrite <- app_assoc. + apply list_nth_z_find_label; auto. + * remember (list_nth_z (body bb) (n - list_length_z (header bb))) as bi_opt eqn:BI. + destruct bi_opt. + -- (* nth instruction is a basic instruction *) + exploit list_nth_z_in; eauto. intros INBB. + exploit entire_body_translated; eauto. intros BI'. + destruct BI'. + eexists; split. + ++ eapply is_nth_basic; eauto. + ++ repeat (rewrite <- app_assoc). eapply list_nth_z_find_bi_with_header; eauto. + -- (* nth instruction is the exit instruction *) + generalize n_beyond_body. intros TEMP. + assert (n >= Z.of_nat (Datatypes.length (header bb) + + Datatypes.length (body bb))) as NGE. { auto. } clear TEMP. + remember (exit bb) as exit_opt eqn:EXIT. destruct exit_opt. + ++ rewrite <- app_assoc. rewrite find_instr_past_header; auto. + rewrite <- app_assoc. erewrite find_instr_past_body; eauto. + assert (SIZE' := SIZE). + unfold size in SIZE. rewrite <- EXIT in SIZE. simpl in SIZE. + destruct SIZE as (LOWER & UPPER). + repeat (rewrite Nat2Z.inj_add in UPPER). + repeat (rewrite <- list_length_z_nat in UPPER). repeat (rewrite Nat2Z.inj_add in NGE). + repeat (rewrite <- list_length_z_nat in NGE). simpl in UPPER. + assert (n = list_length_z (header bb) + list_length_z (body bb)). { lia. } + assert (n = size bb - 1). { + unfold size. rewrite <- EXIT. simpl. + repeat (rewrite Nat2Z.inj_add). repeat (rewrite <- list_length_z_nat). simpl. lia. + } + symmetry in EXIT. + eexists; split. + ** eapply is_nth_ctlflow; eauto. + ** simpl. + destruct (zeq (n - list_length_z (header bb) - list_length_z (body bb)) 0). { reflexivity. } + (* absurd *) lia. + ++ (* absurd *) + unfold size in SIZE. rewrite <- EXIT in SIZE. simpl in SIZE. + destruct SIZE as (? & SIZE'). rewrite Nat.add_0_r in SIZE'. lia. + + unfold find_bblock in FINDBB; simpl in FINDBB; fold find_bblock in FINDBB. + inversion UNFOLD as (UNFOLD'). + apply bind_inversion in UNFOLD'. destruct UNFOLD' as (? & (UNFOLD_BBLOCK' & UNFOLD')). + apply bind_inversion in UNFOLD'. destruct UNFOLD' as (? & (UNFOLD' & TLB)). + inversion TLB. + generalize (IHlb _ _ _ FINDBB UNFOLD'). intros IH. + destruct IH as (? & (IH_is_nth & IH_find_instr)); eauto. + eexists; split. + * apply IH_is_nth. + * replace (Z.pos p + n) with (Z.pos p + n - size b + size b) by lia. + eapply find_instr_bblock_tail; try assumption. + replace (Z.pos p + n - size b) with (Z.pos p - size b + n) by lia. + apply IH_find_instr. + + (* absurd *) + generalize (Pos2Z.neg_is_neg p). intros. exploit (find_bblock_neg (b :: lb)); eauto. + rewrite FINDBB. intros CONTRA. inversion CONTRA. +Qed. + +Lemma exec_header_simulation b ofs f bb rs m: forall + (ATPC: rs PC = Vptr b ofs) + (FINDF: Genv.find_funct_ptr ge b = Some (Internal f)) + (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb), + exists s', star Asm.step tge (State rs m) E0 s' + /\ match_internal (list_length_z (header bb)) (State rs m) s'. +Proof. + intros. + exploit internal_functions_unfold; eauto. + intros (tc & FINDtf & TRANStf & _). + assert (BNDhead: list_length_z (header bb) <= 1). { eapply size_header; eauto. } + destruct (header bb) as [|l[|]] eqn: EQhead. + + (* header nil *) + eexists; split. + - eapply star_refl. + - split; eauto. + unfold list_length_z; rewrite !ATPC; simpl. + rewrite Ptrofs.add_zero; auto. + + (* header one *) + assert (Lhead: list_length_z (header bb) = 1). { rewrite EQhead; unfold list_length_z; simpl. auto. } + exploit (find_instr_bblock 0); eauto. + { generalize (bblock_size_pos bb). lia. } + intros (i & NTH & FIND_INSTR). + inv NTH. + * rewrite EQhead in H; simpl in H. inv H. + replace (Ptrofs.unsigned ofs + 0) with (Ptrofs.unsigned ofs) in FIND_INSTR by lia. + eexists. split. + - eapply star_one. + eapply Asm.exec_step_internal; eauto. + simpl; eauto. + - unfold list_length_z; simpl. split; eauto. + intros r; destruct r; simpl; congruence || auto. + * (* absurd case *) + erewrite list_nth_z_neg in * |-; [ congruence | rewrite Lhead; lia]. + * (* absurd case *) + rewrite bblock_size_aux, Lhead in *. generalize (bblock_size_aux_pos bb). lia. + + (* absurd case *) + unfold list_length_z in BNDhead. simpl in *. + generalize (list_length_z_aux_increase _ l1 2); lia. +Qed. + +Lemma eval_addressing_preserved a rs1 rs2: + (forall r : preg, r <> PC -> rs1 r = rs2 r) -> + eval_addressing lk a rs1 = Asm.eval_addressing tge a rs2. +Proof. + intros EQ. + destruct a; simpl; try (rewrite !EQ; congruence). + auto. +Qed. + +Ltac next_stuck_cong := try (unfold Next, Stuck in *; congruence). + +Ltac inv_ok_eq := + repeat match goal with + | [EQ: OK ?x = OK ?y |- _ ] + => inversion EQ; clear EQ; subst + end. + +Ltac reg_rwrt := + match goal with + | [e: DR _ = DR _ |- _ ] + => rewrite e in * + end. + +Ltac destruct_reg_inv := + repeat match goal with + | [ H : match ?reg with _ => _ end = _ |- _ ] + => simpl in *; destruct reg; try congruence; try inv_ok_eq; try reg_rwrt + end. + +Ltac destruct_ireg_inv := + repeat match goal with + | [ H : match ?reg with _ => _ end = _ |- _ ] + => destruct reg as [[r|]|]; try congruence; try inv_ok_eq; subst + end. + +Ltac destruct_reg_size := + simpl in *; + match goal with + | [ |- context [ match ?reg with _ => _ end ] ] + => destruct reg; try congruence + end. + +Ltac find_rwrt_ag := + simpl in *; + match goal with + | [ AG: forall r, r <> ?PC -> _ r = _ r |- _ ] + => repeat rewrite <- AG; try congruence + end. + +Ltac inv_matchi := + match goal with + | [ MATCHI : match_internal _ _ _ |- _ ] + => inversion MATCHI; subst; find_rwrt_ag + end. + +Ltac destruct_ir0_reg := + match goal with + | [ |- context [ ir0 _ _ ?r ] ] + => unfold ir0 in *; destruct r; find_rwrt_ag; eauto + end. + +Ltac pc_not_sp := + match goal with + | [ |- ?PC <> ?SP ] + => destruct (PregEq.eq SP PC); repeat congruence; discriminate + end. + +Ltac update_x_access_x := + subst; rewrite !Pregmap.gss; auto. + +Ltac update_x_access_r := + rewrite !Pregmap.gso; auto. + +Lemma nextinstr_agree_but_pc rs1 rs2: forall + (AG: forall r, r <> PC -> rs1 r = rs2 r), + forall r, r <> PC -> rs1 r = Asm.nextinstr rs2 r. +Proof. + intros; unfold Asm.nextinstr in *; rewrite Pregmap.gso in *; eauto. +Qed. + +Lemma ptrofs_nextinstr_agree rs1 rs2 n: forall + (BOUNDED : 0 <= n <= Ptrofs.max_unsigned) + (AGPC : Val.offset_ptr (rs1 PC) (Ptrofs.repr n) = rs2 PC), + Val.offset_ptr (rs1 PC) (Ptrofs.repr (n + 1)) = Asm.nextinstr rs2 PC. +Proof. + intros; unfold Asm.nextinstr; rewrite Pregmap.gss. + rewrite <- Ptrofs.unsigned_one; rewrite <- (Ptrofs.unsigned_repr n); eauto; + rewrite <- Ptrofs.add_unsigned; rewrite <- Val.offset_ptr_assoc; rewrite AGPC; eauto. +Qed. + +Lemma load_rd_a_preserved n rs1 m1 rs1' m1' rs2 m2 rd chk f a: forall + (BOUNDED: 0 <= n <= Ptrofs.max_unsigned) + (MATCHI: match_internal n (State rs1 m1) (State rs2 m2)) + (HLOAD: exec_load_rd_a lk chk f a rd rs1 m1 = Next rs1' m1'), + exists (rs2' : regset) (m2' : mem), Asm.exec_load tge chk f a rd rs2 m2 = Next rs2' m2' + /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2'). +Proof. + intros. + unfold exec_load_rd_a, Asm.exec_load in *. + inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst. + rewrite <- (eval_addressing_preserved a rs1 rs2); auto. + destruct (Mem.loadv _ _ _). + + inversion HLOAD; auto. repeat (econstructor; eauto). + * eapply nextinstr_agree_but_pc; intros. + destruct (PregEq.eq r rd); try update_x_access_x; try update_x_access_r. + * eapply ptrofs_nextinstr_agree; eauto. + + next_stuck_cong. +Qed. + +Lemma load_double_preserved n rs1 m1 rs1' m1' rs2 m2 rd1 rd2 chk1 chk2 f a: forall + (BOUNDED: 0 <= n <= Ptrofs.max_unsigned) + (MATCHI: match_internal n (State rs1 m1) (State rs2 m2)) + (HLOAD: exec_load_double lk chk1 chk2 f a rd1 rd2 rs1 m1 = Next rs1' m1'), + exists (rs2' : regset) (m2' : mem), Asm.exec_load_double tge chk1 chk2 f a rd1 rd2 rs2 m2 = Next rs2' m2' + /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2'). +Proof. + intros. + unfold exec_load_double, Asm.exec_load_double in *. + inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst. + erewrite <- !eval_addressing_preserved; eauto. + destruct (is_pair_addressing_mode_correct a); try discriminate. + destruct (Mem.loadv _ _ _); + destruct (Mem.loadv chk2 m2 + (eval_addressing lk + (get_offset_addr a match chk1 with + | Mint32 | Mfloat32| Many32 => 4 + | _ => 8 + end) rs1)); + inversion HLOAD; auto. + repeat (econstructor; eauto). + * eapply nextinstr_agree_but_pc; intros. + destruct (PregEq.eq r rd2); destruct (PregEq.eq r rd1). + - try update_x_access_x. + - try update_x_access_x. + - subst; repeat rewrite Pregmap.gso, Pregmap.gss; auto. + - try update_x_access_r. + * eapply ptrofs_nextinstr_agree; eauto. +Qed. + +<<<<<<< HEAD +Lemma store_rs_a_preserved n rs1 m1 rs1' m1' rs2 m2 v chk a: forall + (BOUNDED: 0 <= n <= Ptrofs.max_unsigned) + (MATCHI: match_internal n (State rs1 m1) (State rs2 m2)) + (HSTORE: exec_store_rs_a lk chk a v rs1 m1 = Next rs1' m1'), + exists (rs2' : regset) (m2' : mem), Asm.exec_store tge chk a v rs2 m2 = Next rs2' m2' + /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2'). +Proof. + intros. + unfold exec_store_rs_a, Asm.exec_store in *. + inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst. + rewrite <- (eval_addressing_preserved a rs1 rs2); auto. + destruct (Mem.storev _ _ _ _). + + inversion HSTORE; auto. repeat (econstructor; eauto). + * eapply nextinstr_agree_but_pc; intros. + subst. apply EQR. auto. + * eapply ptrofs_nextinstr_agree; subst; eauto. + + next_stuck_cong. +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. +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. lia. + generalize (transf_function_no_overflow _ _ H0). lia. + intros. apply Pregmap.gso; auto. +Qed. + +(** Existence of return addresses *) +>>>>>>> master + +Lemma store_double_preserved n rs1 m1 rs1' m1' rs2 m2 v1 v2 chk1 chk2 a: forall + (BOUNDED: 0 <= n <= Ptrofs.max_unsigned) + (MATCHI: match_internal n (State rs1 m1) (State rs2 m2)) + (HSTORE: exec_store_double lk chk1 chk2 a v1 v2 rs1 m1 = Next rs1' m1'), + exists (rs2' : regset) (m2' : mem), Asm.exec_store_double tge chk1 chk2 a v1 v2 rs2 m2 = Next rs2' m2' + /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2'). +Proof. + intros. + unfold exec_store_double, Asm.exec_store_double in *. + inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst. + erewrite <- !eval_addressing_preserved; eauto. + destruct (is_pair_addressing_mode_correct a); try discriminate. + destruct (Mem.storev _ _ _ _); + try destruct (Mem.storev chk2 m + (eval_addressing lk + (get_offset_addr a + match chk1 with + | Mint32 | Mfloat32 | Many32 => 4 + | _ => 8 + end) rs1) v2); + inversion HSTORE; auto. + repeat (econstructor; eauto). + * eapply nextinstr_agree_but_pc; intros. + subst. apply EQR. auto. + * eapply ptrofs_nextinstr_agree; subst; eauto. +Qed. + +Lemma next_inst_preserved n rs1 m1 rs1' m1' rs2 m2 (x: dreg) v: forall + (BOUNDED: 0 <= n <= Ptrofs.max_unsigned) + (MATCHI: match_internal n (State rs1 m1) (State rs2 m2)) + (NEXTI: Next rs1 # x <- v m1 = Next rs1' m1'), + exists (rs2' : regset) (m2' : mem), + Next (Asm.nextinstr rs2 # x <- v) m2 = Next rs2' m2' + /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2'). +Proof. + intros. + inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst. + inversion NEXTI. repeat (econstructor; eauto). + * eapply nextinstr_agree_but_pc; intros. + destruct (PregEq.eq r x); try update_x_access_x; try update_x_access_r. + * eapply ptrofs_nextinstr_agree; eauto. +Qed. + +Lemma match_internal_nextinstr_switch: + forall n s rs2 m2 r v, + r <> PC -> + match_internal n s (State ((Asm.nextinstr rs2)#r <- v) m2) -> + match_internal n s (State (Asm.nextinstr (rs2#r <- v)) m2). +Proof. + unfold Asm.nextinstr; intros n s rs2 m2 r v NOTPC1 MI. + inversion MI; subst; constructor; auto. + - eapply nextinstr_agree_but_pc; intros. + rewrite AG; try congruence. + destruct (PregEq.eq r r0); try update_x_access_x; try update_x_access_r. + - rewrite !Pregmap.gss, !Pregmap.gso; try congruence. + rewrite AGPC. + rewrite Pregmap.gso, Pregmap.gss; try congruence. +Qed. + +Lemma match_internal_nextinstr_set_parallel: + forall n rs1 m1 rs2 m2 r v1 v2, + r <> PC -> + match_internal n (State rs1 m1) (State (Asm.nextinstr rs2) m2) -> + v1 = v2 -> + match_internal n (State (rs1#r <- v1) m1) (State (Asm.nextinstr (rs2#r <- v2)) m2). +Proof. + intros; subst; eapply match_internal_nextinstr_switch; eauto. + intros; eapply match_internal_set_parallel; eauto. +Qed. + +Lemma exec_basic_simulation: + forall tf n rs1 m1 rs1' m1' rs2 m2 bi tbi + (BOUNDED: 0 <= n <= Ptrofs.max_unsigned) + (BASIC: exec_basic lk ge bi rs1 m1 = Next rs1' m1') + (MATCHI: match_internal n (State rs1 m1) (State rs2 m2)) + (TRANSBI: basic_to_instruction bi = OK tbi), + exists rs2' m2', Asm.exec_instr tge tf tbi + rs2 m2 = Next rs2' m2' + /\ match_internal (n + 1) (State rs1' m1') (State rs2' m2'). +Proof. + intros. + destruct bi. + { (* PArith *) + simpl in *; destruct i. + 1: { + destruct i. + 1,2,3: + try (destruct sumbool_rec; try congruence); + try (monadInv TRANSBI); + try (destruct_reg_inv); + try (inv_matchi); + try (exploit next_inst_preserved; eauto); + try (repeat destruct_reg_size); + try (destruct_ir0_reg). + 1,2: (* Special case for Pfmovimmd / Pfmovimms *) + try (monadInv TRANSBI); + try (destruct_reg_inv); + try (inv_matchi); + inversion BASIC; clear BASIC; subst; + try (destruct (is_immediate_float64 _)); + try (destruct (is_immediate_float32 _)); + eexists; eexists; split; eauto; + repeat (eapply match_internal_nextinstr_set_parallel; try congruence); + try (econstructor; eauto); + try (eapply nextinstr_agree_but_pc; eauto); + try (eapply ptrofs_nextinstr_agree; eauto). + } + 1,2,3,4,5: (* PArithP, PArithPP, PArithPPP, PArithRR0R, PArithRR0, PArithARRRR0 *) + destruct i; + try (destruct sumbool_rec; try congruence); + try (monadInv TRANSBI); + try (destruct_reg_inv); + try (inv_matchi); + try (exploit next_inst_preserved; eauto); + try (repeat destruct_reg_size); + try (destruct_ir0_reg). + { (* PArithComparisonPP *) + destruct i; + try (monadInv TRANSBI); + try (inv_matchi); + try (destruct_reg_inv); + simpl in *. + 1,2: (* compare_long *) + inversion BASIC; clear BASIC; subst; + eexists; eexists; split; eauto; + unfold compare_long; + repeat (eapply match_internal_nextinstr_set_parallel; [ congruence | idtac | try (rewrite !AG; congruence)]); + try (econstructor; eauto); + try (eapply nextinstr_agree_but_pc; eauto); + try (eapply ptrofs_nextinstr_agree; eauto). + + destruct sz. + - (* compare_single *) + unfold compare_single in BASIC. + destruct (rs1 x), (rs1 x0); + inversion BASIC; + eexists; eexists; split; eauto; + repeat (eapply match_internal_nextinstr_set_parallel; [ congruence | idtac | try (rewrite !AG; congruence)]); + try (econstructor; eauto); + try (eapply nextinstr_agree_but_pc; eauto); + try (eapply ptrofs_nextinstr_agree; eauto). + - (* compare_float *) + unfold compare_float in BASIC. + destruct (rs1 x), (rs1 x0); + inversion BASIC; + eexists; eexists; split; eauto; + repeat (eapply match_internal_nextinstr_set_parallel; [ congruence | idtac | try (rewrite !AG; congruence)]); + try (econstructor; eauto); + try (eapply nextinstr_agree_but_pc; eauto); + try (eapply ptrofs_nextinstr_agree; eauto). } + 1,2: (* PArithComparisonR0R, PArithComparisonP *) + destruct i; + try (monadInv TRANSBI); + try (inv_matchi); + try (destruct_reg_inv); + try (destruct_reg_size); + simpl in *; + inversion BASIC; clear BASIC; subst; + eexists; eexists; split; eauto; + unfold compare_long, compare_int, compare_float, compare_single; + try (destruct_reg_size); + repeat (eapply match_internal_nextinstr_set_parallel; [ congruence | idtac | try (rewrite !AG; congruence)]); + try (econstructor; eauto); + try (destruct_ir0_reg); + try (eapply nextinstr_agree_but_pc; eauto); + try (eapply ptrofs_nextinstr_agree; eauto). + { (* Pcset *) + try (monadInv TRANSBI); + try (inv_matchi). + try (exploit next_inst_preserved; eauto); + try (simpl in *; intros; + unfold if_opt_bool_val in *; unfold eval_testcond in *; + rewrite <- !AG; try congruence; eauto). } + { (* Pfmovi *) + try (monadInv TRANSBI); + try (inv_matchi); + try (destruct_reg_size); + try (destruct_ir0_reg); + try (exploit next_inst_preserved; eauto). } + { (* Pcsel *) + try (destruct_reg_inv); + try (monadInv TRANSBI); + try (destruct_reg_inv); + try (inv_matchi); + try (exploit next_inst_preserved; eauto); + simpl in *; intros; + unfold if_opt_bool_val in *; unfold eval_testcond in *; + rewrite <- !AG; try congruence; eauto. } + { (* Pfnmul *) + try (monadInv TRANSBI); + try (inv_matchi); + try (destruct_reg_size); + try (exploit next_inst_preserved; eauto); + try (find_rwrt_ag). } } + { (* PLoad *) + destruct ld. + - destruct ld; monadInv TRANSBI; try destruct_ireg_inv; exploit load_rd_a_preserved; eauto; + intros; simpl in *; destruct sz; eauto. + - destruct ld; monadInv TRANSBI; destruct rd1 as [[rd1'|]|]; destruct rd2 as [[rd2'|]|]; + inv EQ; inv EQ1; exploit load_double_preserved; eauto. } + { (* PStore *) + destruct st. + - destruct st; monadInv TRANSBI; try destruct_ireg_inv; exploit store_rs_a_preserved; eauto; + simpl in *; inv_matchi; find_rwrt_ag. + - destruct st; monadInv TRANSBI; destruct rs0 as [[rs0'|]|]; destruct rs3 as [[rs3'|]|]; + inv EQ; inv EQ1; exploit store_double_preserved; eauto; + simpl in *; inv_matchi; find_rwrt_ag. } + { (* Pallocframe *) + monadInv TRANSBI; + inv_matchi; try pc_not_sp; + destruct sz eqn:EQSZ; + destruct Mem.alloc eqn:EQALLOC; + destruct Mem.store eqn:EQSTORE; inversion BASIC; try pc_not_sp; + eexists; eexists; split; eauto; + repeat (eapply match_internal_nextinstr_set_parallel; [ try (pc_not_sp; congruence) | idtac | try (reflexivity)]); + try (econstructor; eauto); + try (eapply nextinstr_agree_but_pc; eauto); + try (eapply ptrofs_nextinstr_agree; eauto). } + { (* Pfreeframe *) + monadInv TRANSBI; + inv_matchi; try pc_not_sp; + destruct sz eqn:EQSZ; + destruct Mem.loadv eqn:EQLOAD; + destruct (rs1 SP) eqn:EQRS1SP; + try (destruct Mem.free eqn:EQFREE); + inversion BASIC; try pc_not_sp; + eexists; eexists; split; eauto; + repeat (eapply match_internal_nextinstr_set_parallel; [ try (pc_not_sp; congruence) | idtac | try (reflexivity)]); + try (econstructor; eauto); + try (eapply nextinstr_agree_but_pc; eauto); + try (eapply ptrofs_nextinstr_agree; eauto). } + 1,2,3,4: (* Ploadsymbol, Pcvtsw2x, Pcvtuw2x, Pcvtx2w *) + try (monadInv TRANSBI); + try (inv_matchi); + try (exploit next_inst_preserved; eauto); + rewrite symbol_addresses_preserved; eauto; + try (find_rwrt_ag). + { (* Pnop *) + monadInv TRANSBI; inv_matchi. + inversion BASIC. + repeat (econstructor; eauto). + eapply nextinstr_agree_but_pc; intros; + try rewrite <- H0, AG; auto. + try eapply ptrofs_nextinstr_agree; auto; rewrite <- H0; + assumption. } +Qed. + +Lemma find_basic_instructions b ofs f bb tc: forall + (FINDF: Genv.find_funct_ptr ge b = Some (Internal f)) + (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb) + (UNFOLD: unfold (fn_blocks f) = OK tc), + forall n, + (n < length (body bb))%nat -> + exists (i : Asm.instruction) (bi : basic), + list_nth_z (body bb) (Z.of_nat n) = Some bi + /\ basic_to_instruction bi = OK i + /\ Asm.find_instr (Ptrofs.unsigned ofs + + (list_length_z (header bb)) + + Z.of_nat n) tc + = Some i. +Proof. + intros until n; intros NLT. + exploit internal_functions_unfold; eauto. + intros (tc' & FINDtf & TRANStf & _). + assert (tc' = tc) by congruence; subst. + exploit (find_instr_bblock (list_length_z (header bb) + Z.of_nat n)); eauto. + { unfold size; split. + - rewrite list_length_z_nat; lia. + - repeat (rewrite list_length_z_nat). repeat (rewrite Nat2Z.inj_add). lia. } + intros (i & NTH & FIND_INSTR). + exists i; intros. + inv NTH. + - (* absurd *) apply list_nth_z_range in H; lia. + - exists bi; + rewrite Z.add_simpl_l in H; + rewrite Z.add_assoc in FIND_INSTR; + intuition. + - (* absurd *) rewrite bblock_size_aux in H0; + rewrite H in H0; simpl in H0; repeat rewrite list_length_z_nat in H0; lia. +Qed. + +(* TODO: remplacer find_basic_instructions directement par ce lemme ? *) +Lemma find_basic_instructions_alt b ofs f bb tc n: forall + (FINDF: Genv.find_funct_ptr ge b = Some (Internal f)) + (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb) + (UNFOLD: unfold (fn_blocks f) = OK tc) + (BOUND: 0 <= n < list_length_z (body bb)), + exists (i : Asm.instruction) (bi : basic), + list_nth_z (body bb) n = Some bi + /\ basic_to_instruction bi = OK i + /\ Asm.find_instr (Ptrofs.unsigned ofs + + (list_length_z (header bb)) + + n) tc + = Some i. +Proof. + intros; assert ((Z.to_nat n) < length (body bb))%nat. + { rewrite Nat2Z.inj_lt, <- list_length_z_nat, Z2Nat.id; try lia. } + exploit find_basic_instructions; eauto. + rewrite Z2Nat.id; try lia. intros (i & bi & X). + eexists; eexists; intuition eauto. +Qed. + +Lemma header_body_tail_bound: forall (a: basic) (li: list basic) bb ofs + (BOUNDBB : Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned) + (BDYLENPOS : 0 <= list_length_z (body bb) - list_length_z (a :: li) < + list_length_z (body bb)), +0 <= list_length_z (header bb) + list_length_z (body bb) - list_length_z (a :: li) <= +Ptrofs.max_unsigned. +Proof. + intros. + assert (HBBPOS: list_length_z (header bb) >= 0) by eapply list_length_z_pos. + assert (HBBSIZE: list_length_z (header bb) < size bb) by eapply header_size_lt_block_size. + assert (OFSBOUND: 0 <= Ptrofs.unsigned ofs <= Ptrofs.max_unsigned) by eapply Ptrofs.unsigned_range_2. + assert (BBSIZE: size bb <= Ptrofs.max_unsigned) by lia. + unfold size in BBSIZE. + rewrite !Nat2Z.inj_add in BBSIZE. + rewrite <- !list_length_z_nat in BBSIZE. + lia. +Qed. + +(* A more general version of the exec_body_simulation_plus lemma below. + This generalization is necessary for the induction proof inside the body. +*) +Lemma exec_body_simulation_plus_gen li: forall b ofs f bb rs m s2 rs' m' + (BLI: is_tail li (body bb)) + (ATPC: rs PC = Vptr b ofs) + (FINDF: Genv.find_funct_ptr ge b = Some (Internal f)) + (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb) + (NEMPTY_BODY: li <> nil) + (MATCHI: match_internal ((list_length_z (header bb)) + (list_length_z (body bb)) - (list_length_z li)) (State rs m) s2) + (BODY: exec_body lk ge li rs m = Next rs' m'), + exists s2', plus Asm.step tge s2 E0 s2' + /\ match_internal (size bb - (Z.of_nat (length_opt (exit bb)))) (State rs' m') s2'. +Proof. + induction li as [|a li]; simpl; try congruence. + intros. + assert (BDYLENPOS: 0 <= (list_length_z (body bb) - list_length_z (a::li)) < list_length_z (body bb)). { + assert (Z.of_nat O < list_length_z (a::li) <= list_length_z (body bb)); try lia. + rewrite !list_length_z_nat; split. + - rewrite <- Nat2Z.inj_lt. simpl. lia. + - rewrite <- Nat2Z.inj_le; eapply is_tail_bound; eauto. + } + exploit internal_functions_unfold; eauto. + intros (tc & FINDtf & TRANStf & _). + exploit find_basic_instructions_alt; eauto. + intros (tbi & (bi & (NTHBI & TRANSBI & FIND_INSTR))). + exploit is_tail_list_nth_z; eauto. + rewrite NTHBI; simpl. + intros X; inversion X; subst; clear X NTHBI. + destruct (exec_basic _ _ _ _ _) eqn:EXEC_BASIC; next_stuck_cong. + destruct s as (rs1 & m1); simpl in *. + destruct s2 as (rs2 & m2); simpl in *. + assert (BOUNDBBMAX: Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned) + by (eapply size_of_blocks_bounds; eauto). + exploit header_body_tail_bound; eauto. intros BDYTAIL. + exploit exec_basic_simulation; eauto. + intros (rs_next' & m_next' & EXEC_INSTR & MI_NEXT). + exploit exec_basic_dont_move_PC; eauto. intros AGPC. + inversion MI_NEXT as [A B C D E M_NEXT_AGREE RS_NEXT_AGREE ATPC_NEXT PC_OFS_NEXT RS RS']. + subst A. subst B. subst C. subst D. subst E. + rewrite ATPC in AGPC. symmetry in AGPC, ATPC_NEXT. + + inv MATCHI. symmetry in AGPC0. + rewrite ATPC in AGPC0. + unfold Val.offset_ptr in AGPC0. + + simpl in FIND_INSTR. + (* Execute internal step. *) + exploit (Asm.exec_step_internal tge b); eauto. + { + rewrite Ptrofs.add_unsigned. + repeat (rewrite Ptrofs.unsigned_repr); try lia. + 2: { + assert (BOUNDOFS: 0 <= Ptrofs.unsigned ofs <= Ptrofs.max_unsigned) by eapply Ptrofs.unsigned_range_2. + assert (list_length_z (body bb) <= size bb) by eapply body_size_le_block_size. + assert (list_length_z (header bb) <= 1). { eapply size_header; eauto. } + lia. } + try rewrite list_length_z_nat; try split; + simpl; rewrite <- !list_length_z_nat; + replace (Ptrofs.unsigned ofs + (list_length_z (header bb) + list_length_z (body bb) - + list_length_z (a :: li))) with (Ptrofs.unsigned ofs + list_length_z (header bb) + + (list_length_z (body bb) - list_length_z (a :: li))) by lia; + try assumption; try lia. } + + (* This is our STEP hypothesis. *) + intros STEP_NEXT. + destruct li as [|a' li]; simpl in *. + - (* case of a single instruction in li: this our base case in the induction *) + inversion BODY; subst. + eexists; split. + + apply plus_one. eauto. + + constructor; auto. + rewrite ATPC_NEXT. + apply f_equal. + apply f_equal. + rewrite bblock_size_aux, list_length_z_cons; simpl. + lia. + - exploit (IHli b ofs f bb rs1 m_next' (State rs_next' m_next')); congruence || eauto. + + exploit is_tail_app_def; eauto. + intros (l3 & EQ); rewrite EQ. + exploit (is_tail_app_right (l3 ++ a::nil)). + rewrite <- app_assoc; simpl; eauto. + + constructor; auto. + rewrite ATPC_NEXT. + apply f_equal. + apply f_equal. + rewrite! list_length_z_cons; simpl. + lia. + + intros (s2' & LAST_STEPS & LAST_MATCHS). + eexists. split; eauto. + eapply plus_left'; eauto. +Qed. + +Lemma exec_body_simulation_plus b ofs f bb rs m s2 rs' m': forall + (ATPC: rs PC = Vptr b ofs) + (FINDF: Genv.find_funct_ptr ge b = Some (Internal f)) + (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb) + (NEMPTY_BODY: body bb <> nil) + (MATCHI: match_internal (list_length_z (header bb)) (State rs m) s2) + (BODY: exec_body lk ge (body bb) rs m = Next rs' m'), + exists s2', plus Asm.step tge s2 E0 s2' + /\ match_internal (size bb - (Z.of_nat (length_opt (exit bb)))) (State rs' m') s2'. +Proof. + intros. + exploit exec_body_simulation_plus_gen; eauto. + - constructor. + - replace (list_length_z (header bb) + list_length_z (body bb) - list_length_z (body bb)) with (list_length_z (header bb)); auto. + lia. +Qed. + +Lemma exec_body_simulation_star b ofs f bb rs m s2 rs' m': forall + (ATPC: rs PC = Vptr b ofs) + (FINDF: Genv.find_funct_ptr ge b = Some (Internal f)) + (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb) + (MATCHI: match_internal (list_length_z (header bb)) (State rs m) s2) + (BODY: exec_body lk ge (body bb) rs m = Next rs' m'), + exists s2', star Asm.step tge s2 E0 s2' + /\ match_internal (size bb - (Z.of_nat (length_opt (exit bb)))) (State rs' m') s2'. +Proof. + intros. + destruct (body bb) eqn: Hbb. + - simpl in BODY. inv BODY. + eexists. split. + eapply star_refl; eauto. + assert (EQ: (size bb - Z.of_nat (length_opt (exit bb))) = list_length_z (header bb)). + { rewrite bblock_size_aux. rewrite Hbb; unfold list_length_z; simpl. lia. } + rewrite EQ; eauto. + - exploit exec_body_simulation_plus; congruence || eauto. + { rewrite Hbb; eauto. } + intros (s2' & PLUS & MATCHI'). + eexists; split; eauto. + eapply plus_star; eauto. +Qed. + +Lemma list_nth_z_range_exceeded A (l : list A) n: + n >= list_length_z l -> + list_nth_z l n = None. +Proof. + intros N. + remember (list_nth_z l n) as opt eqn:H. symmetry in H. + destruct opt; auto. + exploit list_nth_z_range; eauto. lia. +Qed. + +Lemma label_in_header_list lbl a: + is_label lbl a = true -> list_length_z (header a) <= 1 -> header a = lbl :: nil. +Proof. + intros. + eapply is_label_correct_true in H. + destruct (header a). + - eapply in_nil in H. contradiction. + - rewrite list_length_z_cons in H0. + assert (list_length_z l0 >= 0) by eapply list_length_z_pos. + assert (list_length_z l0 = 0) by lia. + rewrite list_length_z_nat in H2. + assert (Datatypes.length l0 = 0%nat) by lia. + eapply length_zero_iff_nil in H3. subst. + unfold In in H. destruct H. + + subst; eauto. + + destruct H. +Qed. + +Lemma no_label_in_basic_inst: forall a lbl x, + basic_to_instruction a = OK x -> Asm.is_label lbl x = false. +Proof. + intros. + destruct a; simpl in *; + repeat destruct i; + repeat destruct ld; repeat destruct st; + simpl in *; + try (try destruct_reg_inv; monadInv H; simpl in *; reflexivity). +Qed. + +Lemma label_pos_body bdy: forall c1 c2 z ex lbl + (HUNF : unfold_body bdy = OK c2), + Asm.label_pos lbl (z + Z.of_nat ((Datatypes.length bdy) + length_opt ex)) c1 = Asm.label_pos lbl (z) ((c2 ++ unfold_exit ex) ++ c1). +Proof. + induction bdy. + - intros. inversion HUNF. simpl in *. + destruct ex eqn:EQEX. + + simpl in *. unfold Asm.is_label. destruct c; simpl; try congruence. + destruct i; simpl; try congruence. + + simpl in *. ring_simplify (z + 0). auto. + - intros. inversion HUNF; clear HUNF. monadInv H0. simpl in *. + erewrite no_label_in_basic_inst; eauto. rewrite <- IHbdy; eauto. + erewrite Zpos_P_of_succ_nat. + apply f_equal2; auto. lia. +Qed. + +Lemma asm_label_pos_header: forall z a x0 x1 lbl + (HUNF: unfold_body (body a) = OK x1), + Asm.label_pos lbl (z + size a) x0 = + Asm.label_pos lbl (z + list_length_z (header a)) ((x1 ++ unfold_exit (exit a)) ++ x0). +Proof. + intros. + unfold size. + rewrite <- plus_assoc. rewrite Nat2Z.inj_add. + rewrite list_length_z_nat. + replace (z + (Z.of_nat (Datatypes.length (header a)) + Z.of_nat (Datatypes.length (body a) + length_opt (exit a)))) with (z + Z.of_nat (Datatypes.length (header a)) + Z.of_nat (Datatypes.length (body a) + length_opt (exit a))) by lia. + eapply (label_pos_body (body a) x0 x1 (z + Z.of_nat (Datatypes.length (header a))) (exit a) lbl). auto. +Qed. + +Lemma header_size_cons_nil: forall (l0: label) (l1: list label) + (HSIZE: list_length_z (l0 :: l1) <= 1), + l1 = nil. +Proof. + intros. + destruct l1; try congruence. rewrite !list_length_z_cons in HSIZE. + assert (list_length_z l1 >= 0) by eapply list_length_z_pos. + assert (list_length_z l1 + 1 + 1 >= 2) by lia. + assert (2 <= 1) by lia. contradiction H1. lia. +Qed. + +Lemma label_pos_preserved_gen bbs: forall lbl c z + (HUNF: unfold bbs = OK c), + label_pos lbl z bbs = Asm.label_pos lbl z c. +Proof. + induction bbs. + - intros. simpl in *. inversion HUNF. simpl. reflexivity. + - intros. simpl in *. monadInv HUNF. unfold unfold_bblock in EQ. + destruct (zle _ _); try congruence. monadInv EQ. + destruct (is_label _ _) eqn:EQLBL. + + erewrite label_in_header_list; eauto. + simpl in *. destruct (peq lbl lbl); try congruence. + + erewrite IHbbs; eauto. + rewrite (asm_label_pos_header z a x0 x1 lbl); auto. + unfold is_label in *. + destruct (header a). + * replace (z + list_length_z (@nil label)) with (z); eauto. + unfold list_length_z. simpl. lia. + * eapply header_size_cons_nil in l as HL1. + subst. simpl in *. destruct (in_dec _ _); try congruence. + simpl in *. + destruct (peq _ _); try intuition congruence. +Qed. + +Lemma label_pos_preserved f lbl z tf: forall + (FINDF: transf_function f = OK tf), + label_pos lbl z (fn_blocks f) = Asm.label_pos lbl z (Asm.fn_code tf). +Proof. + intros. + eapply label_pos_preserved_gen. + unfold transf_function in FINDF. monadInv FINDF. + destruct zlt; try congruence. inversion EQ0. eauto. +Qed. + +Lemma goto_label_preserved bb rs1 m1 rs1' m1' rs2 m2 lbl f tf v: forall + (FINDF: transf_function f = OK tf) + (BOUNDED: size bb <= Ptrofs.max_unsigned) + (MATCHI: match_internal (size bb - 1) (State rs1 m1) (State rs2 m2)) + (HGOTO: goto_label f lbl (incrPC v rs1) m1 = Next rs1' m1'), + exists (rs2' : regset) (m2' : mem), Asm.goto_label tf lbl rs2 m2 = Next rs2' m2' + /\ match_states (State rs1' m1') (State rs2' m2'). +Proof. + intros. + unfold goto_label, Asm.goto_label in *. + rewrite <- (label_pos_preserved f); auto. + inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst. + destruct label_pos; next_stuck_cong. + destruct (incrPC v rs1 PC) eqn:INCRPC; next_stuck_cong. + inversion HGOTO; auto. repeat (econstructor; eauto). + rewrite <- EQPC. + unfold incrPC in *. + rewrite !Pregmap.gss in *. + destruct (rs1 PC) eqn:EQRS1; simpl in *; try congruence. + replace (rs2 # PC <- (Vptr b0 (Ptrofs.repr z))) with ((rs1 # PC <- (Vptr b0 (Ptrofs.add i0 v))) # PC <- (Vptr b (Ptrofs.repr z))); auto. + eapply functional_extensionality. intros. + destruct (PregEq.eq x PC); subst. + rewrite !Pregmap.gss. congruence. + rewrite !Pregmap.gso; auto. +Qed. + +Lemma next_inst_incr_pc_preserved bb rs1 m1 rs1' m1' rs2 m2 f tf: forall + (FINDF: transf_function f = OK tf) + (BOUNDED: size bb <= Ptrofs.max_unsigned) + (MATCHI: match_internal (size bb - 1) (State rs1 m1) (State rs2 m2)) + (NEXT: Next (incrPC (Ptrofs.repr (size bb)) rs1) m2 = Next rs1' m1'), + exists (rs2' : regset) (m2' : mem), + Next (Asm.nextinstr rs2) m2 = Next rs2' m2' + /\ match_states (State rs1' m1') (State rs2' m2'). +Proof. + intros; simpl in *; unfold incrPC in NEXT; + inv_matchi; + assert (size bb >= 1) by eapply bblock_size_pos; + assert (0 <= size bb - 1 <= Ptrofs.max_unsigned) by lia; + inversion NEXT; subst; + eexists; eexists; split; eauto. + assert (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size bb))) = Asm.nextinstr rs2). { + unfold Pregmap.set. apply functional_extensionality. + intros x. destruct (PregEq.eq x PC). + -- unfold Asm.nextinstr. rewrite <- AGPC. + rewrite Val.offset_ptr_assoc. rewrite Ptrofs.add_unsigned. + rewrite (Ptrofs.unsigned_repr (size bb - 1)); try lia. + rewrite Ptrofs.unsigned_one. + replace (size bb - 1 + 1) with (size bb) by lia. + rewrite e. rewrite Pregmap.gss. + reflexivity. + -- eapply nextinstr_agree_but_pc; eauto. } + rewrite H1. econstructor. +Qed. + +Lemma pc_reg_overwrite: forall (r: ireg) rs1 m1 rs2 m2 bb + (MATCHI: match_internal (size bb - 1) (State rs1 m1) (State rs2 m2)), + rs2 # PC <- (rs2 r) = + (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size bb)))) # PC <- + (rs1 r). +Proof. + intros. + unfold Pregmap.set; apply functional_extensionality. + intros x; destruct (PregEq.eq x PC) as [X | X]; try discriminate; inv_matchi. +Qed. + +Lemma exec_cfi_simulation: + forall bb f tf rs1 m1 rs1' m1' rs2 m2 cfi + (SIZE: size bb <= Ptrofs.max_unsigned) + (FINDF: transf_function f = OK tf) + (* Warning: Asmblock's PC is assumed to be already pointing on the next instruction ! *) + (CFI: exec_cfi ge f cfi (incrPC (Ptrofs.repr (size bb)) rs1) m1 = Next rs1' m1') + (MATCHI: match_internal (size bb - 1) (State rs1 m1) (State rs2 m2)), + exists rs2' m2', Asm.exec_instr tge tf (cf_instruction_to_instruction cfi) + rs2 m2 = Next rs2' m2' + /\ match_states (State rs1' m1') (State rs2' m2'). +Proof. + intros. + assert (BBPOS: size bb >= 1) by eapply bblock_size_pos. + destruct cfi; inv CFI; simpl. + - (* Pb *) + exploit goto_label_preserved; eauto. + - (* Pbc *) + inv_matchi. + unfold eval_testcond in *. destruct c; + erewrite !incrPC_agree_but_pc in H0; try rewrite <- !AG; try congruence. + all: + destruct_reg_size; + try destruct b eqn:EQB. + 1,4,7,10,13,16,19,22,25,28,31,34: + exploit goto_label_preserved; eauto. + 1,3,5,7,9,11,13,15,17,19,21,23: + exploit next_inst_incr_pc_preserved; eauto. + all: repeat (econstructor; eauto). + - (* Pbl *) + eexists; eexists; split; eauto. + assert ( ((incrPC (Ptrofs.repr (size bb)) rs1) # X30 <- (incrPC (Ptrofs.repr (size bb)) rs1 PC)) + # PC <- (Genv.symbol_address ge id Ptrofs.zero) + = (rs2 # X30 <- (Val.offset_ptr (rs2 PC) Ptrofs.one)) + # PC <- (Genv.symbol_address tge id Ptrofs.zero) + ) as EQRS. { + unfold incrPC. unfold Pregmap.set. simpl. apply functional_extensionality. + intros x. destruct (PregEq.eq x PC). + * rewrite symbol_addresses_preserved. reflexivity. + * destruct (PregEq.eq x X30). + -- inv MATCHI. rewrite <- AGPC. rewrite Val.offset_ptr_assoc. + unfold Ptrofs.add, Ptrofs.one. repeat (rewrite Ptrofs.unsigned_repr); try lia. + replace (size bb - 1 + 1) with (size bb) by lia. reflexivity. + -- inv MATCHI; rewrite AG; try assumption; reflexivity. + } rewrite EQRS; inv MATCHI; reflexivity. + - (* Pbs *) + eexists; eexists; split; eauto. + assert ( (incrPC (Ptrofs.repr (size bb)) rs1) # PC <- + (Genv.symbol_address ge id Ptrofs.zero) + = rs2 # PC <- (Genv.symbol_address tge id Ptrofs.zero) + ) as EQRS. { + unfold incrPC, Pregmap.set. rewrite symbol_addresses_preserved. inv MATCHI. + apply functional_extensionality. intros x. destruct (PregEq.eq x PC); auto. + } rewrite EQRS; inv MATCHI; reflexivity. + - (* Pblr *) + eexists; eexists; split; eauto. + unfold incrPC. rewrite Pregmap.gss. rewrite Pregmap.gso; try discriminate. + assert ( (rs2 # X30 <- (Val.offset_ptr (rs2 PC) Ptrofs.one)) # PC <- (rs2 r) + = ((rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size bb)))) + # X30 <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr (size bb)))) + # PC <- (rs1 r) + ) as EQRS. { + unfold Pregmap.set. apply functional_extensionality. + intros x; destruct (PregEq.eq x PC) as [X | X]. + - inv_matchi; rewrite AG; auto. + - destruct (PregEq.eq x X30) as [X' | X']. + + inversion MATCHI; subst. rewrite <- AGPC. + rewrite Val.offset_ptr_assoc. unfold Ptrofs.one. + rewrite Ptrofs.add_unsigned. rewrite Ptrofs.unsigned_repr; try lia. rewrite Ptrofs.unsigned_repr; try lia. + rewrite Z.sub_add; reflexivity. + + inv_matchi. + } rewrite EQRS. inv_matchi. + - (* Pbr *) + eexists; eexists; split; eauto. + unfold incrPC. rewrite Pregmap.gso; try discriminate. + rewrite (pc_reg_overwrite r rs1 m1' rs2 m2 bb); auto. + inv_matchi. + - (* Pret *) + eexists; eexists; split; eauto. + unfold incrPC. rewrite Pregmap.gso; try discriminate. + rewrite (pc_reg_overwrite r rs1 m1' rs2 m2 bb); auto. + inv_matchi. + - (* Pcbnz *) + inv_matchi. + unfold eval_neg_branch in *. + erewrite incrPC_agree_but_pc in H0; try congruence. + destruct eval_testzero; next_stuck_cong. + destruct b. + * exploit next_inst_incr_pc_preserved; eauto. + * exploit goto_label_preserved; eauto. + - (* Pcbz *) + inv_matchi. + unfold eval_branch in *. + erewrite incrPC_agree_but_pc in H0; try congruence. + destruct eval_testzero; next_stuck_cong. + destruct b. + * exploit goto_label_preserved; eauto. + * exploit next_inst_incr_pc_preserved; eauto. + - (* Ptbnbz *) + inv_matchi. + unfold eval_branch in *. + erewrite incrPC_agree_but_pc in H0; try congruence. + destruct eval_testbit; next_stuck_cong. + destruct b. + * exploit goto_label_preserved; eauto. + * exploit next_inst_incr_pc_preserved; eauto. + - (* Ptbz *) + inv_matchi. + unfold eval_neg_branch in *. + erewrite incrPC_agree_but_pc in H0; try congruence. + destruct eval_testbit; next_stuck_cong. + destruct b. + * exploit next_inst_incr_pc_preserved; eauto. + * exploit goto_label_preserved; eauto. + - (* Pbtbl *) + assert (rs2 # X16 <- Vundef r1 = (incrPC (Ptrofs.repr (size bb)) rs1) # X16 <- Vundef r1) + as EQUNDEFX16. { + unfold incrPC, Pregmap.set. + destruct (PregEq.eq r1 X16) as [X16 | X16]; auto. + destruct (PregEq.eq r1 PC) as [PC' | PC']; try discriminate. + inv MATCHI; rewrite AG; auto. + } rewrite <- EQUNDEFX16 in H0. + destruct_reg_inv; next_stuck_cong. + unfold goto_label, Asm.goto_label in *. + rewrite <- (label_pos_preserved f); auto. + inversion MATCHI; subst. + destruct label_pos; next_stuck_cong. + destruct ((incrPC (Ptrofs.repr (size bb)) rs1) # X16 <- Vundef PC) eqn:INCRPC; next_stuck_cong. + inversion H0; auto. repeat (econstructor; eauto). + rewrite !Pregmap.gso; try congruence. + rewrite <- AGPC. + unfold incrPC in *. + destruct (rs1 PC) eqn:EQRS1; simpl in *; try discriminate. + replace ((rs2 # X16 <- Vundef) # PC <- (Vptr b0 (Ptrofs.repr z))) with + (((rs1 # PC <- (Vptr b0 (Ptrofs.add i1 (Ptrofs.repr (size bb))))) # X16 <- + Vundef) # PC <- (Vptr b (Ptrofs.repr z))); auto. + eapply functional_extensionality; intros x. + destruct (PregEq.eq x PC); subst. + + rewrite Pregmap.gso in INCRPC; try congruence. + rewrite Pregmap.gss in INCRPC. + rewrite !Pregmap.gss in *; congruence. + + rewrite Pregmap.gso; auto. + rewrite (Pregmap.gso (i := x) (j := PC)); auto. + destruct (PregEq.eq x X16); subst. + * rewrite !Pregmap.gss; auto. + * rewrite !Pregmap.gso; auto. +Qed. + +Lemma last_instruction_cannot_be_label bb: + list_nth_z (header bb) (size bb - 1) = None. +Proof. + assert (list_length_z (header bb) <= size bb - 1). { + rewrite bblock_size_aux. generalize (bblock_size_aux_pos bb). lia. + } + remember (list_nth_z (header bb) (size bb - 1)) as label_opt; destruct label_opt; auto; + exploit list_nth_z_range; eauto; lia. +Qed. + +Lemma pc_ptr_exec_step: forall ofs bb b rs m _rs _m + (ATPC : rs PC = Vptr b ofs) + (MATCHI : match_internal (size bb - 1) + {| _rs := rs; _m := m |} + {| _rs := _rs; _m := _m |}), + _rs PC = Vptr b (Ptrofs.add ofs (Ptrofs.repr (size bb - 1))). +Proof. + intros; inv MATCHI. rewrite <- AGPC; rewrite ATPC; unfold Val.offset_ptr; eauto. +Qed. + +Lemma find_instr_ofs_somei: forall ofs bb f tc asmi rs m _rs _m + (BOUNDOFS : Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned) + (FIND_INSTR : Asm.find_instr (Ptrofs.unsigned ofs + (size bb - 1)) tc = + Some (asmi)) + (MATCHI : match_internal (size bb - 1) + {| _rs := rs; _m := m |} + {| _rs := _rs; _m := _m |}), + Asm.find_instr (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr (size bb - 1)))) + (Asm.fn_code {| Asm.fn_sig := fn_sig f; Asm.fn_code := tc |}) = + Some (asmi). +Proof. + intros; simpl. + replace (Ptrofs.unsigned (Ptrofs.add ofs (Ptrofs.repr (size bb - 1)))) + with (Ptrofs.unsigned ofs + (size bb - 1)); try assumption. + generalize (bblock_size_pos bb); generalize (Ptrofs.unsigned_range_2 ofs); intros. + unfold Ptrofs.add. + rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr; try lia. + rewrite Ptrofs.unsigned_repr; lia. +Qed. + +Lemma eval_builtin_arg_match: forall rs _m _rs a1 b1 + (AG : forall r : preg, r <> PC -> rs r = _rs r) + (EVAL : eval_builtin_arg tge (fun r : dreg => rs r) (rs SP) _m a1 b1), + eval_builtin_arg tge _rs (_rs SP) _m (map_builtin_arg DR a1) b1. +Proof. + intros; induction EVAL; simpl in *; try rewrite AG; try rewrite AG in EVAL; try discriminate; try congruence; eauto with barg. + econstructor. rewrite <- AG; try discriminate; auto. +Qed. + +Lemma eval_builtin_args_match: forall bb rs m _rs _m args vargs + (MATCHI : match_internal (size bb - 1) + {| _rs := rs; _m := m |} + {| _rs := _rs; _m := _m |}) + (EVAL : eval_builtin_args tge (fun r : dreg => rs r) (rs SP) m args vargs), + eval_builtin_args tge _rs (_rs SP) _m (map (map_builtin_arg DR) args) vargs. +Proof. + intros; inv MATCHI. + induction EVAL; subst. + - econstructor. + - econstructor. + + eapply eval_builtin_arg_match; eauto. + + eauto. +Qed. + +Lemma pc_both_sides: forall (rs _rs: regset) v + (AG : forall r : preg, r <> PC -> rs r = _rs r), + rs # PC <- v = _rs # PC <- v. +Proof. + intros; unfold Pregmap.set; apply functional_extensionality; intros y. + destruct (PregEq.eq y PC); try rewrite AG; eauto. +Qed. + +Lemma set_buitin_res_sym res: forall vres rs _rs r + (NPC: r <> PC) + (AG : forall r : preg, r <> PC -> rs r = _rs r), + set_res res vres rs r = set_res res vres _rs r. +Proof. + induction res; simpl; intros; unfold Pregmap.set; try rewrite AG; eauto. +Qed. + +Lemma set_builtin_res_dont_move_pc_gen res: forall vres rs _rs v1 v2 + (HV: v1 = v2) + (AG : forall r : preg, r <> PC -> rs r = _rs r), + (set_res res vres rs) # PC <- v1 = + (set_res res vres _rs) # PC <- v2. +Proof. + intros. rewrite HV. generalize res vres rs _rs AG v2. + clear res vres rs _rs AG v1 v2 HV. + induction res. + - simpl; intros. apply pc_both_sides; intros. + unfold Pregmap.set; try rewrite AG; eauto. + - simpl; intros; apply pc_both_sides; eauto. + - simpl; intros. + erewrite IHres2; eauto; intros. + eapply set_buitin_res_sym; eauto. +Qed. + +Lemma set_builtin_map_not_pc (res: builtin_res dreg): forall vres rs, + set_res (map_builtin_res DR res) vres rs PC = rs PC. +Proof. + induction res. + - intros; simpl. unfold Pregmap.set. destruct (PregEq.eq PC x); try congruence. + - intros; simpl; congruence. + - intros; simpl in *. rewrite IHres2. rewrite IHres1. reflexivity. +Qed. + +Lemma undef_reg_preserved (rl: list mreg): forall rs _rs r + (NPC: r <> PC) + (AG : forall r : preg, r <> PC -> rs r = _rs r), + undef_regs (map preg_of rl) rs r = undef_regs (map preg_of rl) _rs r. +Proof. + induction rl. + - simpl; auto. + - simpl; intros. erewrite IHrl; eauto. + intros. unfold Pregmap.set. destruct (PregEq.eq r0 (preg_of a)); try rewrite AG; eauto. +Qed. + +Lemma undef_regs_other: + forall r rl rs, + (forall r', In r' rl -> r <> r') -> + undef_regs rl rs r = rs r. +Proof. + induction rl; simpl; intros. auto. + rewrite IHrl by auto. rewrite Pregmap.gso; auto. +Qed. + +Fixpoint preg_notin (r: preg) (rl: list mreg) : Prop := + match rl with + | nil => True + | r1 :: nil => r <> preg_of r1 + | r1 :: rl => r <> preg_of r1 /\ preg_notin r rl + end. + +<<<<<<< HEAD +Remark preg_notin_charact: + forall r rl, + preg_notin r rl <-> (forall mr, In mr rl -> r <> preg_of mr). +Proof. + induction rl; simpl; intros. + tauto. + destruct rl. + simpl. split. intros. intuition congruence. auto. + rewrite IHrl. split. + intros [A B]. intros. destruct H. congruence. auto. + auto. +======= +Remark preg_of_not_X29: forall r, negb (mreg_eq r R29) = true -> IR X29 <> preg_of r. +Proof. + intros. change (IR X29) with (preg_of R29). red; intros. + exploit preg_of_injective; eauto. intros; subst r; discriminate. +Qed. + +Lemma sp_val': forall ms sp rs, agree ms sp rs -> sp = rs XSP. +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'), + (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. simpl; congruence. + +- (* 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]]]. + exists rs'; split. eauto. + split. eapply agree_set_mreg; eauto with asmgen. congruence. + simpl; congruence. + +- (* 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]]. + exists rs'; split. eauto. + split. eapply agree_undef_regs; eauto with asmgen. + simpl; intros. rewrite Q; auto with asmgen. + +- (* Mgetparam *) + assert (f0 = f) by congruence; subst f0. + unfold load_stack in *. + exploit Mem.loadv_extends. eauto. eexact 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]]]. + exists rs1; split. eauto. + split. eapply agree_set_mreg. eapply agree_set_mreg; eauto. congruence. auto with asmgen. + simpl; intros. rewrite R; auto with asmgen. + apply preg_of_not_X29; 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]]]. + 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. + simpl; intros. rewrite U; auto with asmgen. + apply preg_of_not_X29; 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]]]. + exists rs2; split. eauto. split. + apply agree_set_undef_mreg with rs0; auto. + apply Val.lessdef_trans with v'; auto. + simpl; intros. InvBooleans. + rewrite R; auto. apply preg_of_not_X29; auto. +Local Transparent destroyed_by_op. + destruct op; try exact I; simpl; congruence. + +- (* Mload *) + 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]]]. + exists rs2; split. eauto. + split. eapply agree_set_undef_mreg; eauto. congruence. + simpl; congruence. + +- (* 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]]. + exists rs2; split. eauto. + split. eapply agree_undef_regs; eauto with asmgen. + simpl; congruence. + +- (* 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). + 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. + +- (* 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. + rewrite <- H1. simpl. econstructor; eauto. + eapply code_tail_next_int; eauto. + simpl; intros. destruct H4. congruence. destruct H4. congruence. + exploit list_in_map_inv; eauto. intros (mr & U & V). subst. + auto with asmgen. + auto with asmgen. + apply agree_nextinstr. eapply agree_set_res; auto. + eapply agree_undef_regs; eauto. intros. + simpl. rewrite undef_regs_other_2; auto. Simpl. + 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. + +- (* 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). + exists jmp; exists k; exists rs'. + split. eexact A. + split. apply agree_exten with rs0; auto with asmgen. + exact B. + +- (* 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). + 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. + simpl; congruence. + +- (* 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). + 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. + congruence. + +- (* 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. + +- (* internal function *) + + 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 *. + 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. + intros [m2' [F G]]. + 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). + 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. lia. constructor. + intros (ofs' & X & Y). + left; exists (State rs3 m3'); split. + eapply exec_straight_steps_1; eauto. lia. 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_change_sp with (parent_sp s). + apply agree_undef_regs with rs0. auto. +Local Transparent destroyed_at_function_entry. simpl. + simpl; intros; Simpl. + unfold sp; congruence. + intros. rewrite V by auto with asmgen. reflexivity. + +- (* external function *) + exploit functions_translated; eauto. + intros [tf [A B]]. simpl in B. inv B. + exploit extcall_arguments_match; eauto. + intros [args' [C D]]. + exploit external_call_mem_extends; eauto. + intros [res' [m2' [P [Q [R S]]]]]. + left; econstructor; split. + 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. + +- (* return *) + inv STACKS. simpl in *. + right. split. lia. split. auto. + rewrite <- ATPC in H5. + econstructor; eauto. congruence. +>>>>>>> master +Qed. + +Lemma undef_regs_other_2: + forall r rl rs, + preg_notin r rl -> + undef_regs (map preg_of rl) rs r = rs r. +Proof. + intros. apply undef_regs_other. intros. + exploit list_in_map_inv; eauto. intros [mr [A B]]. subst. + rewrite preg_notin_charact in H. auto. +Qed. + +Lemma exec_exit_simulation_plus b ofs f bb s2 t rs m rs' m': forall + (FINDF: Genv.find_funct_ptr ge b = Some (Internal f)) + (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb) + (NEMPTY_EXIT: exit bb <> None) + (MATCHI: match_internal (size bb - Z.of_nat (length_opt (exit bb))) (State rs m) s2) + (EXIT: exec_exit ge f (Ptrofs.repr (size bb)) rs m (exit bb) t rs' m') + (ATPC: rs PC = Vptr b ofs), + plus Asm.step tge s2 t (State rs' m'). +Proof. + intros. + exploit internal_functions_unfold; eauto. + intros (tc & FINDtf & TRANStf & _). + + exploit (find_instr_bblock (size bb - 1)); eauto. + { generalize (bblock_size_pos bb). lia. } + intros (i' & NTH & FIND_INSTR). + + inv NTH. + + rewrite last_instruction_cannot_be_label in *. discriminate. + + destruct (exit bb) as [ctrl |] eqn:NEMPTY_EXIT'. 2: { contradiction. } + rewrite bblock_size_aux in *. rewrite NEMPTY_EXIT' in *. simpl in *. + (* XXX: Is there a better way to simplify this expression i.e. automatically? *) + replace (list_length_z (header bb) + list_length_z (body bb) + 1 - 1 - + list_length_z (header bb)) with (list_length_z (body bb)) in H by lia. + rewrite list_nth_z_range_exceeded in H; try lia. discriminate. + + assert (Ptrofs.unsigned ofs + size bb <= Ptrofs.max_unsigned). { + eapply size_of_blocks_bounds; eauto. + } + assert (size bb <= Ptrofs.max_unsigned). { generalize (Ptrofs.unsigned_range_2 ofs); lia. } + destruct cfi. + * (* control flow instruction *) + destruct s2. + rewrite H in EXIT. (* exit bb is a cfi *) + inv EXIT. + rewrite H in MATCHI. simpl in MATCHI. + exploit internal_functions_translated; eauto. + rewrite FINDtf. + intros (tf & FINDtf' & TRANSf). inversion FINDtf'; subst; clear FINDtf'. + exploit exec_cfi_simulation; eauto. + (* extract exec_cfi_simulation's conclusion as separate hypotheses *) + intros (rs2' & m2' & EXECI & MATCHS); rewrite MATCHS. + apply plus_one. + eapply Asm.exec_step_internal; eauto. + - eapply pc_ptr_exec_step; eauto. + - eapply find_instr_ofs_somei; eauto. + * (* builtin *) + destruct s2. + rewrite H in EXIT. + rewrite H in MATCHI. simpl in MATCHI. + simpl in FIND_INSTR. + inversion EXIT. + apply plus_one. + eapply external_call_symbols_preserved in H10; try (apply senv_preserved). + eapply eval_builtin_args_preserved in H6; try (apply symbols_preserved). + eapply Asm.exec_step_builtin; eauto. + - eapply pc_ptr_exec_step; eauto. + - eapply find_instr_ofs_somei; eauto. + - eapply eval_builtin_args_match; eauto. + - inv MATCHI; eauto. + - inv MATCHI. + unfold Asm.nextinstr, incrPC. + assert (HPC: Val.offset_ptr (rs PC) (Ptrofs.repr (size bb)) + = Val.offset_ptr (_rs PC) Ptrofs.one). + { rewrite <- AGPC. rewrite ATPC. unfold Val.offset_ptr. + rewrite Ptrofs.add_assoc. unfold Ptrofs.add. + assert (BBPOS: size bb >= 1) by eapply bblock_size_pos. + rewrite (Ptrofs.unsigned_repr (size bb - 1)); try lia. + rewrite Ptrofs.unsigned_one. + replace (size bb - 1 + 1) with (size bb) by lia. + reflexivity. } + apply set_builtin_res_dont_move_pc_gen. + -- erewrite !set_builtin_map_not_pc. + erewrite !undef_regs_other. + rewrite HPC; auto. + all: intros; simpl in *; destruct H3 as [HX16 | [HX30 | HDES]]; subst; try discriminate; + exploit list_in_map_inv; eauto; intros [mr [A B]]; subst; discriminate. + -- intros. eapply undef_reg_preserved; eauto. + intros. destruct (PregEq.eq X16 r0); destruct (PregEq.eq X30 r0); subst. + rewrite Pregmap.gso, Pregmap.gss; try congruence. + do 2 (rewrite Pregmap.gso, Pregmap.gss; try discriminate; auto). + rewrite 2Pregmap.gss; auto. + rewrite !Pregmap.gso; auto. +Qed. + +Lemma exec_exit_simulation_star b ofs f bb s2 t rs m rs' m': forall + (FINDF: Genv.find_funct_ptr ge b = Some (Internal f)) + (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb) + (MATCHI: match_internal (size bb - Z.of_nat (length_opt (exit bb))) (State rs m) s2) + (EXIT: exec_exit ge f (Ptrofs.repr (size bb)) rs m (exit bb) t rs' m') + (ATPC: rs PC = Vptr b ofs), + star Asm.step tge s2 t (State rs' m'). +Proof. + intros. + destruct (exit bb) eqn: Hex. + - eapply plus_star. + eapply exec_exit_simulation_plus; try rewrite Hex; congruence || eauto. + - inv MATCHI. + inv EXIT. + assert (X: rs2 = incrPC (Ptrofs.repr (size bb)) rs). { + unfold incrPC. unfold Pregmap.set. + apply functional_extensionality. intros x. + destruct (PregEq.eq x PC) as [X|]. + - rewrite X. rewrite <- AGPC. simpl. + replace (size bb - 0) with (size bb) by lia. reflexivity. + - rewrite AG; try assumption. reflexivity. + } + destruct X. + subst; eapply star_refl; eauto. +Qed. + +Lemma exec_bblock_simulation b ofs f bb t rs m rs' m': forall + (ATPC: rs PC = Vptr b ofs) + (FINDF: Genv.find_funct_ptr ge b = Some (Internal f)) + (FINDBB: find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb) + (EXECBB: exec_bblock lk ge f bb rs m t rs' m'), + plus Asm.step tge (State rs m) t (State rs' m'). +Proof. + intros; destruct EXECBB as (rs1 & m1 & BODY & CTL). + exploit exec_header_simulation; eauto. + intros (s0 & STAR & MATCH0). + eapply star_plus_trans; traceEq || eauto. + destruct (bblock_non_empty bb). + - (* body bb <> nil *) + exploit exec_body_simulation_plus; eauto. + intros (s1 & PLUS & MATCH1). + eapply plus_star_trans; traceEq || eauto. + eapply exec_exit_simulation_star; eauto. + erewrite <- exec_body_dont_move_PC; eauto. + - (* exit bb <> None *) + exploit exec_body_simulation_star; eauto. + intros (s1 & STAR1 & MATCH1). + eapply star_plus_trans; traceEq || eauto. + eapply exec_exit_simulation_plus; eauto. + erewrite <- exec_body_dont_move_PC; eauto. +Qed. + +Lemma step_simulation s t s': + Asmblock.step lk ge s t s' -> plus Asm.step tge s t s'. +Proof. + intros STEP. + inv STEP; simpl; exploit functions_translated; eauto; + intros (tf0 & FINDtf & TRANSf); + monadInv TRANSf. + - (* internal step *) eapply exec_bblock_simulation; eauto. + - (* external step *) + apply plus_one. + exploit external_call_symbols_preserved; eauto. apply senv_preserved. + intros ?. + eapply Asm.exec_step_external; eauto. +Qed. + +Lemma transf_program_correct: + forward_simulation (Asmblock.semantics lk prog) (Asm.semantics tprog). +Proof. + eapply forward_simulation_plus. + - apply senv_preserved. + - eexact transf_initial_states. + - eexact transf_final_states. + - unfold match_states. + simpl; intros; subst; eexists; split; eauto. + eapply step_simulation; eauto. +Qed. + +End PRESERVATION. + +End Asmblock_PRESERVATION. + + +Local Open Scope linking_scope. + +Definition block_passes := + mkpass Machblockgenproof.match_prog + ::: mkpass Asmblockgenproof.match_prog + ::: mkpass PostpassSchedulingproof.match_prog + ::: mkpass Asmblock_PRESERVATION.match_prog + ::: pass_nil _. + +Definition match_prog := pass_match (compose_passes block_passes). + +Lemma transf_program_match: + forall p tp, Asmgen.transf_program p = OK tp -> match_prog p tp. +Proof. + intros p tp H. + unfold Asmgen.transf_program in H. apply bind_inversion in H. destruct H. + inversion_clear H. apply bind_inversion in H1. destruct H1. + inversion_clear H. + unfold Compopts.time in *. remember (Machblockgen.transf_program p) as mbp. + unfold match_prog; simpl. + exists mbp; split. apply Machblockgenproof.transf_program_match; auto. + exists x; split. apply Asmblockgenproof.transf_program_match; auto. + exists x0; split. apply PostpassSchedulingproof.transf_program_match; auto. + exists tp; split. apply Asmblock_PRESERVATION.transf_program_match; auto. auto. +Qed. + +(** Return Address Offset *) + +Definition return_address_offset: Mach.function -> Mach.code -> ptrofs -> Prop := + Machblockgenproof.Mach_return_address_offset (Asmblockgenproof.return_address_offset). + +Lemma return_address_exists: + forall f sg ros c, is_tail (Mach.Mcall sg ros :: c) f.(Mach.fn_code) -> + exists ra, return_address_offset f c ra. +Proof. + intros; unfold return_address_offset; eapply Machblockgenproof.Mach_return_address_exists; eauto. + intros; eapply Asmblockgenproof.return_address_exists; 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. + +Theorem transf_program_correct: + forward_simulation (Mach.semantics return_address_offset prog) (Asm.semantics tprog). +Proof. + unfold match_prog in TRANSF. simpl in TRANSF. + inv TRANSF. inv H. inv H1. inv H. inv H2. inv H. inv H3. inv H. + eapply compose_forward_simulations. + { exploit Machblockgenproof.transf_program_correct; eauto. } + + eapply compose_forward_simulations. + + apply Asmblockgenproof.transf_program_correct; eauto. + { intros. + unfold Genv.symbol_address. + erewrite <- PostpassSchedulingproof.symbols_preserved; eauto. + erewrite Asmblock_PRESERVATION.symbol_high_low; eauto. + reflexivity. + } + + eapply compose_forward_simulations. + - apply PostpassSchedulingproof.transf_program_correct; eauto. + - apply Asmblock_PRESERVATION.transf_program_correct; eauto. +Qed. + +End PRESERVATION. + +Instance TransfAsm: TransfLink match_prog := pass_match_link (compose_passes block_passes). + +(*******************************************) +(* Stub actually needed by driver/Compiler *) + +Module Asmgenproof0. + +Definition return_address_offset := return_address_offset. + +End Asmgenproof0. |