From ac8b7ae094cf7741fec63effd8fcfd1467fb2edf Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Thu, 7 Jan 2021 13:05:18 +0100 Subject: directory postpass_lib --- scheduling/postpass_lib/ForwardSimulationBlock.v | 387 +++++++++++ scheduling/postpass_lib/Machblock.v | 387 +++++++++++ scheduling/postpass_lib/Machblockgen.v | 221 ++++++ scheduling/postpass_lib/Machblockgenproof.v | 824 +++++++++++++++++++++++ 4 files changed, 1819 insertions(+) create mode 100644 scheduling/postpass_lib/ForwardSimulationBlock.v create mode 100644 scheduling/postpass_lib/Machblock.v create mode 100644 scheduling/postpass_lib/Machblockgen.v create mode 100644 scheduling/postpass_lib/Machblockgenproof.v (limited to 'scheduling/postpass_lib') diff --git a/scheduling/postpass_lib/ForwardSimulationBlock.v b/scheduling/postpass_lib/ForwardSimulationBlock.v new file mode 100644 index 00000000..cc6ecdd8 --- /dev/null +++ b/scheduling/postpass_lib/ForwardSimulationBlock.v @@ -0,0 +1,387 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* 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. *) +(* *) +(* *************************************************************) + +(*** + +Auxiliary lemmas on starN and forward_simulation +in order to prove the forward simulation of Mach -> Machblock. + +***) + +Require Import Relations. +Require Import Wellfounded. +Require Import Coqlib. +Require Import Events. +Require Import Globalenvs. +Require Import Smallstep. +Require Import Lia. + +Local Open Scope nat_scope. + + +(** Auxiliary lemma on starN *) +Section starN_lemma. + +Variable L: semantics. + +Local Hint Resolve starN_refl starN_step Eapp_assoc: core. + +Lemma starN_split n s t s': + starN (step L) (globalenv L) n s t s' -> + forall m k, n=m+k -> + exists (t1 t2:trace) s0, starN (step L) (globalenv L) m s t1 s0 /\ starN (step L) (globalenv L) k s0 t2 s' /\ t=t1**t2. +Proof. + induction 1; cbn. + + intros m k H; assert (X: m=0); try lia. + assert (X0: k=0); try lia. + subst; repeat (eapply ex_intro); intuition eauto. + + intros m; destruct m as [| m']; cbn. + - intros k H2; subst; repeat (eapply ex_intro); intuition eauto. + - intros k H2. inversion H2. + exploit (IHstarN m' k); eauto. intro. + destruct H3 as (t5 & t6 & s0 & H5 & H6 & H7). + repeat (eapply ex_intro). + instantiate (1 := t6); instantiate (1 := t1 ** t5); instantiate (1 := s0). + intuition eauto. subst. auto. +Qed. + +Lemma starN_tailstep n s t1 s': + starN (step L) (globalenv L) n s t1 s' -> + forall (t t2:trace) s'', + Step L s' t2 s'' -> t = t1 ** t2 -> starN (step L) (globalenv L) (S n) s t s''. +Proof. + induction 1; cbn. + + intros t t1 s0; autorewrite with trace_rewrite. + intros; subst; eapply starN_step; eauto. + autorewrite with trace_rewrite; auto. + + intros. eapply starN_step; eauto. + intros; subst; autorewrite with trace_rewrite; auto. +Qed. + +End starN_lemma. + + + +(** General scheme from a "match_states" relation *) + +Section ForwardSimuBlock_REL. + +Variable L1 L2: semantics. + + +(** Hypothèses de la preuve *) + +Variable dist_end_block: state L1 -> nat. + +Hypothesis simu_mid_block: + forall s1 t s1', Step L1 s1 t s1' -> (dist_end_block s1)<>0 -> t = E0 /\ dist_end_block s1=S (dist_end_block s1'). + +Hypothesis public_preserved: + forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id. + +Variable match_states: state L1 -> state L2 -> Prop. + +Hypothesis match_initial_states: + forall s1, initial_state L1 s1 -> exists s2, match_states s1 s2 /\ initial_state L2 s2. + +Hypothesis match_final_states: + forall s1 s2 r, final_state L1 s1 r -> match_states s1 s2 -> final_state L2 s2 r. + +Hypothesis final_states_end_block: + forall s1 t s1' r, Step L1 s1 t s1' -> final_state L1 s1' r -> dist_end_block s1 = 0. + +Hypothesis simu_end_block: + forall s1 t s1' s2, starN (step L1) (globalenv L1) (S (dist_end_block s1)) s1 t s1' -> match_states s1 s2 -> exists s2', Step L2 s2 t s2' /\ match_states s1' s2'. + + +(** Introduction d'une sémantique par bloc sur L1 appelée "memoL1" *) + +Local Hint Resolve starN_refl starN_step: core. + +Definition follows_in_block (head current: state L1): Prop := + dist_end_block head >= dist_end_block current + /\ starN (step L1) (globalenv L1) (minus (dist_end_block head) (dist_end_block current)) head E0 current. + +Lemma follows_in_block_step (head previous next: state L1): + forall t, follows_in_block head previous -> Step L1 previous t next -> (dist_end_block previous)<>0 -> follows_in_block head next. +Proof. + intros t [H1 H2] H3 H4. + destruct (simu_mid_block _ _ _ H3 H4) as [H5 H6]; subst. + constructor 1. + + lia. + + replace (dist_end_block head - dist_end_block next) with (S (dist_end_block head - dist_end_block previous)). + - eapply starN_tailstep; eauto. + - lia. +Qed. + +Lemma follows_in_block_init (head current: state L1): + forall t, Step L1 head t current -> (dist_end_block head)<>0 -> follows_in_block head current. +Proof. + intros t H3 H4. + destruct (simu_mid_block _ _ _ H3 H4) as [H5 H6]; subst. + constructor 1. + + lia. + + replace (dist_end_block head - dist_end_block current) with 1. + - eapply starN_tailstep; eauto. + - lia. +Qed. + + +Record memostate := { + real: state L1; + memorized: option (state L1); + memo_star: forall head, memorized = Some head -> follows_in_block head real; + memo_final: forall r, final_state L1 real r -> memorized = None +}. + +Definition head (s: memostate): state L1 := + match memorized s with + | None => real s + | Some s' => s' + end. + +Lemma head_followed (s: memostate): follows_in_block (head s) (real s). +Proof. + destruct s as [rs ms Hs]. cbn. + destruct ms as [ms|]; unfold head; cbn; auto. + constructor 1. + lia. + replace (dist_end_block rs - dist_end_block rs)%nat with O. + + apply starN_refl; auto. + + lia. +Qed. + +Inductive is_well_memorized (s s': memostate): Prop := + | StartBloc: + dist_end_block (real s) <> O -> + memorized s = None -> + memorized s' = Some (real s) -> + is_well_memorized s s' + | MidBloc: + dist_end_block (real s) <> O -> + memorized s <> None -> + memorized s' = memorized s -> + is_well_memorized s s' + | ExitBloc: + dist_end_block (real s) = O -> + memorized s' = None -> + is_well_memorized s s'. + +Local Hint Resolve StartBloc MidBloc ExitBloc: core. + +Definition memoL1 := {| + state := memostate; + genvtype := genvtype L1; + step := fun ge s t s' => + step L1 ge (real s) t (real s') + /\ is_well_memorized s s' ; + initial_state := fun s => initial_state L1 (real s) /\ memorized s = None; + final_state := fun s r => final_state L1 (real s) r; + globalenv:= globalenv L1; + symbolenv:= symbolenv L1 +|}. + + +(** Preuve des 2 forward simulations: L1 -> memoL1 et memoL1 -> L2 *) + +Lemma discr_dist_end s: + {dist_end_block s = O} + {dist_end_block s <> O}. +Proof. + destruct (dist_end_block s); cbn; intuition. +Qed. + +Lemma memo_simulation_step: + forall s1 t s1', Step L1 s1 t s1' -> + forall s2, s1 = (real s2) -> exists s2', Step memoL1 s2 t s2' /\ s1' = (real s2'). +Proof. + intros s1 t s1' H1 [rs2 ms2 Hmoi] H2. cbn in H2; subst. + destruct (discr_dist_end rs2) as [H3 | H3]. + + refine (ex_intro _ {|real:=s1'; memorized:=None |} _); cbn. + intuition. + + destruct ms2 as [s|]. + - refine (ex_intro _ {|real:=s1'; memorized:=Some s |} _); cbn. + intuition. + - refine (ex_intro _ {|real:=s1'; memorized:=Some rs2 |} _); cbn. + intuition. + Unshelve. + * intros; discriminate. + * intros; auto. + * intros head X; injection X; clear X; intros; subst. + eapply follows_in_block_step; eauto. + * intros r X; erewrite final_states_end_block in H3; intuition eauto. + * intros head X; injection X; clear X; intros; subst. + eapply follows_in_block_init; eauto. + * intros r X; erewrite final_states_end_block in H3; intuition eauto. +Qed. + +Lemma forward_memo_simulation_1: forward_simulation L1 memoL1. +Proof. + apply forward_simulation_step with (match_states:=fun s1 s2 => s1 = (real s2)); auto. + + intros s1 H; eapply ex_intro with (x:={|real:=s1; memorized:=None |}); cbn. + intuition. + + intros; subst; auto. + + intros; exploit memo_simulation_step; eauto. + Unshelve. + * intros; discriminate. + * auto. +Qed. + +Lemma forward_memo_simulation_2: forward_simulation memoL1 L2. +Proof. + unfold memoL1; cbn. + apply forward_simulation_opt with (measure:=fun s => dist_end_block (real s)) (match_states:=fun s1 s2 => match_states (head s1) s2); cbn; auto. + + intros s1 [H0 H1]; destruct (match_initial_states (real s1) H0). + unfold head; rewrite H1. + intuition eauto. + + intros s1 s2 r X H0; unfold head in X. + erewrite memo_final in X; eauto. + + intros s1 t s1' [H1 H2] s2 H; subst. + destruct H2 as [ H0 H2 H3 | H0 H2 H3 | H0 H2]. + - (* StartBloc *) + constructor 2. destruct (simu_mid_block (real s1) t (real s1')) as [H5 H4]; auto. + unfold head in * |- *. rewrite H2 in H. rewrite H3. rewrite H4. intuition. + - (* MidBloc *) + constructor 2. destruct (simu_mid_block (real s1) t (real s1')) as [H5 H4]; auto. + unfold head in * |- *. rewrite H3. rewrite H4. intuition. + destruct (memorized s1); cbn; auto. tauto. + - (* EndBloc *) + constructor 1. + destruct (simu_end_block (head s1) t (real s1') s2) as (s2' & H3 & H4); auto. + * destruct (head_followed s1) as [H4 H3]. + replace (dist_end_block (head s1) - dist_end_block (real s1)) with (dist_end_block (head s1)) in H3; try lia. + eapply starN_tailstep; eauto. + * unfold head; rewrite H2; cbn. intuition eauto. +Qed. + +Lemma forward_simulation_block_rel: forward_simulation L1 L2. +Proof. + eapply compose_forward_simulations. + eapply forward_memo_simulation_1. + apply forward_memo_simulation_2. +Qed. + + +End ForwardSimuBlock_REL. + + + +(* An instance of the previous scheme, when there is a translation from L1 states to L2 states + +Here, we do not require that the sequence of S2 states does exactly match the sequence of L1 states by trans_state. +This is because the exact matching is broken in Machblock on "goto" instruction (due to the find_label). + +However, the Machblock state after a goto remains "equivalent" to the trans_state of the Mach state in the sense of "equiv_on_next_step" below... + +*) + + +Section ForwardSimuBlock_TRANS. + +Variable L1 L2: semantics. + +Variable trans_state: state L1 -> state L2. + +Definition equiv_on_next_step (P Q: Prop) s2_a s2_b: Prop := + (P -> (forall t s', Step L2 s2_a t s' <-> Step L2 s2_b t s')) /\ (Q -> (forall r, (final_state L2 s2_a r) <-> (final_state L2 s2_b r))). + +Definition match_states s1 s2: Prop := + equiv_on_next_step (exists t s1', Step L1 s1 t s1') (exists r, final_state L1 s1 r) s2 (trans_state s1). + +Lemma match_states_trans_state s1: match_states s1 (trans_state s1). +Proof. + unfold match_states, equiv_on_next_step. intuition. +Qed. + +Variable dist_end_block: state L1 -> nat. + +Hypothesis simu_mid_block: + forall s1 t s1', Step L1 s1 t s1' -> (dist_end_block s1)<>0 -> t = E0 /\ dist_end_block s1=S (dist_end_block s1'). + +Hypothesis public_preserved: + forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id. + +Hypothesis match_initial_states: + forall s1, initial_state L1 s1 -> exists s2, match_states s1 s2 /\ initial_state L2 s2. + +Hypothesis match_final_states: + forall s1 r, final_state L1 s1 r -> final_state L2 (trans_state s1) r. + +Hypothesis final_states_end_block: + forall s1 t s1' r, Step L1 s1 t s1' -> final_state L1 s1' r -> dist_end_block s1 = 0. + +Hypothesis simu_end_block: + forall s1 t s1', starN (step L1) (globalenv L1) (S (dist_end_block s1)) s1 t s1' -> exists s2', Step L2 (trans_state s1) t s2' /\ match_states s1' s2'. + +Lemma forward_simulation_block_trans: forward_simulation L1 L2. +Proof. + eapply forward_simulation_block_rel with (dist_end_block:=dist_end_block) (match_states:=match_states); try tauto. + + (* final_states *) intros s1 s2 r H1 [H2 H3]. rewrite H3; eauto. + + (* simu_end_block *) + intros s1 t s1' s2 H1 [H2a H2b]. exploit simu_end_block; eauto. + intros (s2' & H3 & H4); econstructor 1; intuition eauto. + rewrite H2a; auto. + inversion_clear H1. eauto. +Qed. + +End ForwardSimuBlock_TRANS. + + +(* another version with a relation [trans_state_R] instead of a function [trans_state] *) +Section ForwardSimuBlock_TRANS_R. + +Variable L1 L2: semantics. + +Variable trans_state_R: state L1 -> state L2 -> Prop. + +Definition match_states_R s1 s2: Prop := + exists s2', trans_state_R s1 s2' /\ equiv_on_next_step _ (exists t s1', Step L1 s1 t s1') (exists r, final_state L1 s1 r) s2 s2'. + +Lemma match_states_trans_state_R s1 s2: trans_state_R s1 s2 -> match_states_R s1 s2. +Proof. + unfold match_states, equiv_on_next_step. firstorder. +Qed. + +Variable dist_end_block: state L1 -> nat. + +Hypothesis simu_mid_block: + forall s1 t s1', Step L1 s1 t s1' -> (dist_end_block s1)<>0 -> t = E0 /\ dist_end_block s1=S (dist_end_block s1'). + +Hypothesis public_preserved: + forall id, Senv.public_symbol (symbolenv L2) id = Senv.public_symbol (symbolenv L1) id. + +Hypothesis match_initial_states: + forall s1, initial_state L1 s1 -> exists s2, match_states_R s1 s2 /\ initial_state L2 s2. + +Hypothesis match_final_states: + forall s1 s2 r, final_state L1 s1 r -> trans_state_R s1 s2 -> final_state L2 s2 r. + +Hypothesis final_states_end_block: + forall s1 t s1' r, Step L1 s1 t s1' -> final_state L1 s1' r -> dist_end_block s1 = 0. + +Hypothesis simu_end_block: + forall s1 t s1' s2, starN (step L1) (globalenv L1) (S (dist_end_block s1)) s1 t s1' -> trans_state_R s1 s2 -> exists s2', Step L2 s2 t s2' /\ match_states_R s1' s2'. + +Lemma forward_simulation_block_trans_R: forward_simulation L1 L2. +Proof. + eapply forward_simulation_block_rel with (dist_end_block:=dist_end_block) (match_states:=match_states_R); try tauto. + + (* final_states *) intros s1 s2 r H1 (s2' & H2 & H3 & H4). rewrite H4; eauto. + + (* simu_end_block *) + intros s1 t s1' s2 H1 (s2' & H2 & H2a & H2b). exploit simu_end_block; eauto. + intros (x & Hx & (y & H3 & H4 & H5)). repeat (econstructor; eauto). + rewrite H2a; eauto. + inversion_clear H1. eauto. +Qed. + +End ForwardSimuBlock_TRANS_R. + diff --git a/scheduling/postpass_lib/Machblock.v b/scheduling/postpass_lib/Machblock.v new file mode 100644 index 00000000..404c2a96 --- /dev/null +++ b/scheduling/postpass_lib/Machblock.v @@ -0,0 +1,387 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* 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. *) +(* *) +(* *************************************************************) + +(** Abstract syntax and semantics of a Mach variant, structured with basic-blocks. *) + +Require Import Coqlib. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Values. +Require Import Memory. +Require Import Globalenvs. +Require Import Events. +Require Import Smallstep. +Require Import Op. +Require Import Locations. +Require Import Conventions. +Require Stacklayout. +Require Import Mach. +Require Import Linking. + +(** * Abstract Syntax *) + +(** ** basic instructions (ie no control-flow) *) +Inductive basic_inst: Type := + | MBgetstack: ptrofs -> typ -> mreg -> basic_inst + | MBsetstack: mreg -> ptrofs -> typ -> basic_inst + | MBgetparam: ptrofs -> typ -> mreg -> basic_inst + | MBop: operation -> list mreg -> mreg -> basic_inst + | MBload: trapping_mode -> memory_chunk -> addressing -> list mreg -> mreg -> basic_inst + | MBstore: memory_chunk -> addressing -> list mreg -> mreg -> basic_inst + . + +Definition bblock_body := list basic_inst. + +(** ** control flow instructions *) +Inductive control_flow_inst: Type := + | MBcall: signature -> mreg + ident -> control_flow_inst + | MBtailcall: signature -> mreg + ident -> control_flow_inst + | MBbuiltin: external_function -> list (builtin_arg mreg) -> builtin_res mreg -> control_flow_inst + | MBgoto: label -> control_flow_inst + | MBcond: condition -> list mreg -> label -> control_flow_inst + | MBjumptable: mreg -> list label -> control_flow_inst + | MBreturn: control_flow_inst + . + +(** ** basic block *) +Record bblock := mk_bblock { + header: list label; + body: bblock_body; + exit: option control_flow_inst +}. + +Lemma bblock_eq: + forall b1 b2, + header b1 = header b2 -> + body b1 = body b2 -> + exit b1 = exit b2 -> + b1 = b2. +Proof. + intros. destruct b1. destruct b2. + cbn in *. subst. auto. +Qed. + +Definition length_opt {A} (o: option A) : nat := + match o with + | Some o => 1 + | None => 0 + end. + +Definition size (b:bblock): nat := (length (header b))+(length (body b))+(length_opt (exit b)). + +Lemma size_null b: + size b = 0%nat -> + header b = nil /\ body b = nil /\ exit b = None. +Proof. + destruct b as [h b e]. cbn. unfold size. cbn. + intros H. + assert (length h = 0%nat) as Hh; [ omega |]. + assert (length b = 0%nat) as Hb; [ omega |]. + assert (length_opt e = 0%nat) as He; [ omega|]. + repeat split. + destruct h; try (cbn in Hh; discriminate); auto. + destruct b; try (cbn in Hb; discriminate); auto. + destruct e; try (cbn in He; discriminate); auto. +Qed. + +(** ** programs *) + +Definition code := list bblock. + +Record function: Type := mkfunction + { fn_sig: signature; + fn_code: code; + fn_stacksize: Z; + fn_link_ofs: ptrofs; + fn_retaddr_ofs: ptrofs }. + +Definition fundef := AST.fundef function. + +Definition program := AST.program fundef unit. + +Definition genv := Genv.t fundef unit. + +(** * Operational (blockstep) semantics ***) + +Lemma in_dec (lbl: label) (l: list label): { List.In lbl l } + { ~(List.In lbl l) }. +Proof. + apply List.in_dec. + apply Pos.eq_dec. +Qed. + +Definition is_label (lbl: label) (bb: bblock) : bool := + if in_dec lbl (header bb) then true else false. + +Lemma is_label_correct_true lbl bb: + List.In lbl (header bb) <-> is_label lbl bb = true. +Proof. + unfold is_label; destruct (in_dec lbl (header bb)); cbn; intuition. +Qed. + +Lemma is_label_correct_false lbl bb: + ~(List.In lbl (header bb)) <-> is_label lbl bb = false. +Proof. + unfold is_label; destruct (in_dec lbl (header bb)); cbn; intuition. +Qed. + + +Local Open Scope nat_scope. + +Fixpoint find_label (lbl: label) (c: code) {struct c} : option code := + match c with + | nil => None + | bb1 :: bbl => if is_label lbl bb1 then Some c else find_label lbl bbl + end. + +Section RELSEM. + +Variable rao:function -> code -> ptrofs -> Prop. +Variable ge:genv. + +Definition find_function_ptr + (ge: genv) (ros: mreg + ident) (rs: regset) : option block := + match ros with + | inl r => + match rs r with + | Vptr b ofs => if Ptrofs.eq ofs Ptrofs.zero then Some b else None + | _ => None + end + | inr symb => + Genv.find_symbol ge symb + end. + +(** ** Machblock execution states. *) + +Inductive stackframe: Type := + | Stackframe: + forall (f: block) (**r pointer to calling function *) + (sp: val) (**r stack pointer in calling function *) + (retaddr: val) (**r Asm return address in calling function *) + (c: code), (**r program point in calling function *) + stackframe. + +Inductive state: Type := + | State: + forall (stack: list stackframe) (**r call stack *) + (f: block) (**r pointer to current function *) + (sp: val) (**r stack pointer *) + (c: code) (**r current program point *) + (rs: regset) (**r register state *) + (m: mem), (**r memory state *) + state + | Callstate: + forall (stack: list stackframe) (**r call stack *) + (f: block) (**r pointer to function to call *) + (rs: regset) (**r register state *) + (m: mem), (**r memory state *) + state + | Returnstate: + forall (stack: list stackframe) (**r call stack *) + (rs: regset) (**r register state *) + (m: mem), (**r memory state *) + state. + +Definition parent_sp (s: list stackframe) : val := + match s with + | nil => Vnullptr + | Stackframe f sp ra c :: s' => sp + end. + +Definition parent_ra (s: list stackframe) : val := + match s with + | nil => Vnullptr + | Stackframe f sp ra c :: s' => ra + end. + +Inductive basic_step (s: list stackframe) (fb: block) (sp: val) (rs: regset) (m:mem): basic_inst -> regset -> mem -> Prop := + | exec_MBgetstack: + forall ofs ty dst v, + load_stack m sp ty ofs = Some v -> + basic_step s fb sp rs m (MBgetstack ofs ty dst) (rs#dst <- v) m + | exec_MBsetstack: + forall src ofs ty m' rs', + store_stack m sp ty ofs (rs src) = Some m' -> + rs' = undef_regs (destroyed_by_setstack ty) rs -> + basic_step s fb sp rs m (MBsetstack src ofs ty) rs' m' + | exec_MBgetparam: + forall ofs ty dst v rs' f, + Genv.find_funct_ptr ge fb = Some (Internal f) -> + load_stack m sp Tptr f.(fn_link_ofs) = Some (parent_sp s) -> + load_stack m (parent_sp s) ty ofs = Some v -> + rs' = (rs # temp_for_parent_frame <- Vundef # dst <- v) -> + basic_step s fb sp rs m (MBgetparam ofs ty dst) rs' m + | exec_MBop: + forall op args v rs' res, + eval_operation ge sp op rs##args m = Some v -> + rs' = ((undef_regs (destroyed_by_op op) rs)#res <- v) -> + basic_step s fb sp rs m (MBop op args res) rs' m + | exec_MBload: + forall addr args a v rs' trap chunk dst, + eval_addressing ge sp addr rs##args = Some a -> + Mem.loadv chunk m a = Some v -> + rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- v) -> + basic_step s fb sp rs m (MBload trap chunk addr args dst) rs' m + | exec_MBload_notrap1: + forall addr args rs' chunk dst, + eval_addressing ge sp addr rs##args = None -> + rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- (default_notrap_load_value chunk)) -> + basic_step s fb sp rs m (MBload NOTRAP chunk addr args dst) rs' m + | exec_MBload_notrap2: + forall addr args a rs' chunk dst, + eval_addressing ge sp addr rs##args = Some a -> + Mem.loadv chunk m a = None -> + rs' = ((undef_regs (destroyed_by_load chunk addr) rs)#dst <- (default_notrap_load_value chunk)) -> + basic_step s fb sp rs m (MBload NOTRAP chunk addr args dst) rs' m + | exec_MBstore: + forall chunk addr args src m' a rs', + eval_addressing ge sp addr rs##args = Some a -> + Mem.storev chunk m a (rs src) = Some m' -> + rs' = undef_regs (destroyed_by_store chunk addr) rs -> + basic_step s fb sp rs m (MBstore chunk addr args src) rs' m' + . + + +Inductive body_step (s: list stackframe) (f: block) (sp: val): bblock_body -> regset -> mem -> regset -> mem -> Prop := + | exec_nil_body: + forall rs m, + body_step s f sp nil rs m rs m + | exec_cons_body: + forall rs m bi p rs' m' rs'' m'', + basic_step s f sp rs m bi rs' m' -> + body_step s f sp p rs' m' rs'' m'' -> + body_step s f sp (bi::p) rs m rs'' m'' + . + +Inductive cfi_step: control_flow_inst -> state -> trace -> state -> Prop := + | exec_MBcall: + forall s fb sp sig ros c b rs m f f' ra, + find_function_ptr ge ros rs = Some f' -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> + rao f c ra -> + cfi_step (MBcall sig ros) (State s fb sp (b::c) rs m) + E0 (Callstate (Stackframe fb sp (Vptr fb ra) c :: s) + f' rs m) + | exec_MBtailcall: + forall s fb stk soff sig ros c rs m f f' m', + find_function_ptr ge ros rs = Some f' -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> + load_stack m (Vptr stk soff) Tptr f.(fn_link_ofs) = Some (parent_sp s) -> + load_stack m (Vptr stk soff) Tptr f.(fn_retaddr_ofs) = Some (parent_ra s) -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> + cfi_step (MBtailcall sig ros) (State s fb (Vptr stk soff) c rs m) + E0 (Callstate s f' rs m') + | exec_MBbuiltin: + forall s f sp rs m ef args res b c vargs t vres rs' m', + eval_builtin_args ge rs sp m args vargs -> + external_call ef ge vargs m t vres m' -> + rs' = set_res res vres (undef_regs (destroyed_by_builtin ef) rs) -> + cfi_step (MBbuiltin ef args res) (State s f sp (b :: c) rs m) + t (State s f sp c rs' m') + | exec_MBgoto: + forall s fb f sp lbl c rs m c', + Genv.find_funct_ptr ge fb = Some (Internal f) -> + find_label lbl f.(fn_code) = Some c' -> + cfi_step (MBgoto lbl) (State s fb sp c rs m) + E0 (State s fb sp c' rs m) + | exec_MBcond_true: + forall s fb f sp cond args lbl c rs m c' rs', + eval_condition cond rs##args m = Some true -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> + find_label lbl f.(fn_code) = Some c' -> + rs' = undef_regs (destroyed_by_cond cond) rs -> + cfi_step (MBcond cond args lbl) (State s fb sp c rs m) + E0 (State s fb sp c' rs' m) + | exec_MBcond_false: + forall s f sp cond args lbl b c rs m rs', + eval_condition cond rs##args m = Some false -> + rs' = undef_regs (destroyed_by_cond cond) rs -> + cfi_step (MBcond cond args lbl) (State s f sp (b :: c) rs m) + E0 (State s f sp c rs' m) + | exec_MBjumptable: + forall s fb f sp arg tbl c rs m n lbl c' rs', + rs arg = Vint n -> + list_nth_z tbl (Int.unsigned n) = Some lbl -> + Genv.find_funct_ptr ge fb = Some (Internal f) -> + find_label lbl f.(fn_code) = Some c' -> + rs' = undef_regs destroyed_by_jumptable rs -> + cfi_step (MBjumptable arg tbl) (State s fb sp c rs m) + E0 (State s fb sp c' rs' m) + | exec_MBreturn: + forall s fb stk soff c rs m f m', + Genv.find_funct_ptr ge fb = Some (Internal f) -> + load_stack m (Vptr stk soff) Tptr f.(fn_link_ofs) = Some (parent_sp s) -> + load_stack m (Vptr stk soff) Tptr f.(fn_retaddr_ofs) = Some (parent_ra s) -> + Mem.free m stk 0 f.(fn_stacksize) = Some m' -> + cfi_step MBreturn (State s fb (Vptr stk soff) c rs m) + E0 (Returnstate s rs m') + . + +Inductive exit_step: option control_flow_inst -> state -> trace -> state -> Prop := + | exec_Some_exit: + forall ctl s t s', + cfi_step ctl s t s' -> + exit_step (Some ctl) s t s' + | exec_None_exit: + forall stk f sp b lb rs m, + exit_step None (State stk f sp (b::lb) rs m) E0 (State stk f sp lb rs m) + . + +Inductive step: state -> trace -> state -> Prop := + | exec_bblock: + forall sf f sp bb c rs m rs' m' t s', + body_step sf f sp (body bb) rs m rs' m' -> + exit_step (exit bb) (State sf f sp (bb::c) rs' m') t s' -> + step (State sf f sp (bb::c) rs m) t s' + | exec_function_internal: + forall s fb rs m f m1 m2 m3 stk rs', + Genv.find_funct_ptr ge fb = Some (Internal f) -> + Mem.alloc m 0 f.(fn_stacksize) = (m1, stk) -> + let sp := Vptr stk Ptrofs.zero in + store_stack m1 sp Tptr f.(fn_link_ofs) (parent_sp s) = Some m2 -> + store_stack m2 sp Tptr f.(fn_retaddr_ofs) (parent_ra s) = Some m3 -> + rs' = undef_regs destroyed_at_function_entry rs -> + step (Callstate s fb rs m) + E0 (State s fb sp f.(fn_code) rs' m3) + | exec_function_external: + forall s fb rs m t rs' ef args res m', + Genv.find_funct_ptr ge fb = Some (External ef) -> + extcall_arguments rs m (parent_sp s) (ef_sig ef) args -> + external_call ef ge args m t res m' -> + rs' = set_pair (loc_result (ef_sig ef)) res (undef_caller_save_regs rs) -> + step (Callstate s fb rs m) + t (Returnstate s rs' m') + | exec_return: + forall s f sp ra c rs m, + step (Returnstate (Stackframe f sp ra c :: s) rs m) + E0 (State s f sp c rs m) + . + +End RELSEM. + +Inductive initial_state (p: program): state -> Prop := + | initial_state_intro: forall fb m0, + let ge := Genv.globalenv p in + Genv.init_mem p = Some m0 -> + Genv.find_symbol ge p.(prog_main) = Some fb -> + initial_state p (Callstate nil fb (Regmap.init Vundef) m0). + +Inductive final_state: state -> int -> Prop := + | final_state_intro: forall rs m r retcode, + loc_result signature_main = One r -> + rs r = Vint retcode -> + final_state (Returnstate nil rs m) retcode. + +Definition semantics (rao: function -> code -> ptrofs -> Prop) (p: program) := + Semantics (step rao) (initial_state p) final_state (Genv.globalenv p). diff --git a/scheduling/postpass_lib/Machblockgen.v b/scheduling/postpass_lib/Machblockgen.v new file mode 100644 index 00000000..5a2f2a61 --- /dev/null +++ b/scheduling/postpass_lib/Machblockgen.v @@ -0,0 +1,221 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* 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. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Values. +Require Import Memory. +Require Import Globalenvs. +Require Import Events. +Require Import Smallstep. +Require Import Op. +Require Import Locations. +Require Import Conventions. +Require Stacklayout. +Require Import Mach. +Require Import Linking. +Require Import Machblock. + +(** * Tail-recursive (greedy) translation from Mach code to Machblock code *) + +Inductive Machblock_inst: Type := +| MB_label (lbl: label) +| MB_basic (bi: basic_inst) +| MB_cfi (cfi: control_flow_inst). + +Definition trans_inst (i:Mach.instruction) : Machblock_inst := + match i with + | Mcall sig ros => MB_cfi (MBcall sig ros) + | Mtailcall sig ros => MB_cfi (MBtailcall sig ros) + | Mbuiltin ef args res => MB_cfi (MBbuiltin ef args res) + | Mgoto lbl => MB_cfi (MBgoto lbl) + | Mcond cond args lbl => MB_cfi (MBcond cond args lbl) + | Mjumptable arg tbl => MB_cfi (MBjumptable arg tbl) + | Mreturn => MB_cfi (MBreturn) + | Mgetstack ofs ty dst => MB_basic (MBgetstack ofs ty dst) + | Msetstack src ofs ty => MB_basic (MBsetstack src ofs ty) + | Mgetparam ofs ty dst => MB_basic (MBgetparam ofs ty dst) + | Mop op args res => MB_basic (MBop op args res) + | Mload trap chunk addr args dst=> MB_basic (MBload trap chunk addr args dst) + | Mstore chunk addr args src => MB_basic (MBstore chunk addr args src) + | Mlabel l => MB_label l + end. + +Definition empty_bblock:={| header := nil; body := nil; exit := None |}. +Extraction Inline empty_bblock. + +Definition add_label l bb:={| header := l::(header bb); body := (body bb); exit := (exit bb) |}. +Extraction Inline add_label. + +Definition add_basic bi bb :={| header := nil; body := bi::(body bb); exit := (exit bb) |}. +Extraction Inline add_basic. + +Definition cfi_bblock cfi:={| header := nil; body := nil; exit := Some cfi |}. +Extraction Inline cfi_bblock. + +Definition add_to_new_bblock (i:Machblock_inst) : bblock := + match i with + | MB_label l => add_label l empty_bblock + | MB_basic i => add_basic i empty_bblock + | MB_cfi i => cfi_bblock i + end. + +(** Adding an instruction to the beginning of a bblock list by + +- either adding the instruction to the head of the list, + +- or creating a new bblock with the instruction +*) +Definition add_to_code (i:Machblock_inst) (bl:code) : code := + match bl with + | bh::bl0 => match i with + | MB_label l => add_label l bh::bl0 + | MB_cfi i0 => cfi_bblock i0::bl + | MB_basic i0 => match header bh with + |_::_ => add_basic i0 empty_bblock::bl + | nil => add_basic i0 bh::bl0 + end + end + | _ => add_to_new_bblock i::nil + end. + +Fixpoint trans_code_rev (c: Mach.code) (bl:code) : code := + match c with + | nil => bl + | i::c0 => + trans_code_rev c0 (add_to_code (trans_inst i) bl) + end. + +Function trans_code (c: Mach.code) : code := + trans_code_rev (List.rev_append c nil) nil. + +Definition transf_function (f: Mach.function) : function := + {| fn_sig:=Mach.fn_sig f; + fn_code:=trans_code (Mach.fn_code f); + fn_stacksize := Mach.fn_stacksize f; + fn_link_ofs := Mach.fn_link_ofs f; + fn_retaddr_ofs := Mach.fn_retaddr_ofs f + |}. + +Definition transf_fundef (f: Mach.fundef) : fundef := + transf_fundef transf_function f. + +Definition transf_program (src: Mach.program) : program := + transform_program transf_fundef src. + + +(** * Abstracting trans_code with a simpler inductive relation *) + +Inductive is_end_block: Machblock_inst -> code -> Prop := + | End_empty mbi: is_end_block mbi nil + | End_basic bi bh bl: header bh <> nil -> is_end_block (MB_basic bi) (bh::bl) + | End_cfi cfi bl: bl <> nil -> is_end_block (MB_cfi cfi) bl. + +Local Hint Resolve End_empty End_basic End_cfi: core. + +Inductive is_trans_code: Mach.code -> code -> Prop := + | Tr_nil: is_trans_code nil nil + | Tr_end_block i c bl: + is_trans_code c bl -> + is_end_block (trans_inst i) bl -> + is_trans_code (i::c) (add_to_new_bblock (trans_inst i)::bl) + | Tr_add_label i l bh c bl: + is_trans_code c (bh::bl) -> + i = Mlabel l -> + is_trans_code (i::c) (add_label l bh::bl) + | Tr_add_basic i bi bh c bl: + is_trans_code c (bh::bl) -> + trans_inst i = MB_basic bi -> + header bh = nil -> + is_trans_code (i::c) (add_basic bi bh::bl). + +Local Hint Resolve Tr_nil Tr_end_block: core. + +Lemma add_to_code_is_trans_code i c bl: + is_trans_code c bl -> + is_trans_code (i::c) (add_to_code (trans_inst i) bl). +Proof. + destruct bl as [|bh0 bl]; cbn. + - intro H. inversion H. subst. eauto. + - remember (trans_inst i) as ti. + destruct ti as [l|bi|cfi]. + + intros; eapply Tr_add_label; eauto. destruct i; cbn in * |- *; congruence. + + intros. remember (header bh0) as hbh0. destruct hbh0 as [|b]. + * eapply Tr_add_basic; eauto. + * replace (add_basic bi empty_bblock) with (add_to_new_bblock (MB_basic bi)); auto. + rewrite Heqti; eapply Tr_end_block; eauto. + rewrite <- Heqti. eapply End_basic. congruence. + + intros. + replace (cfi_bblock cfi) with (add_to_new_bblock (MB_cfi cfi)); auto. + rewrite Heqti. eapply Tr_end_block; eauto. + rewrite <- Heqti. eapply End_cfi. congruence. +Qed. + +Local Hint Resolve add_to_code_is_trans_code: core. + +Lemma trans_code_is_trans_code_rev c1: forall c2 mbi, + is_trans_code c2 mbi -> + is_trans_code (rev_append c1 c2) (trans_code_rev c1 mbi). +Proof. + induction c1 as [| i c1]; cbn; auto. +Qed. + +Lemma trans_code_is_trans_code c: is_trans_code c (trans_code c). +Proof. + unfold trans_code. + rewrite <- rev_alt. + rewrite <- (rev_involutive c) at 1. + rewrite rev_alt at 1. + apply trans_code_is_trans_code_rev; auto. +Qed. + +Lemma add_to_code_is_trans_code_inv i c bl: + is_trans_code (i::c) bl -> exists bl0, is_trans_code c bl0 /\ bl = add_to_code (trans_inst i) bl0. +Proof. + intro H; inversion H as [|H0 H1 bl0| | H0 bi bh H1 bl0]; clear H; subst; (repeat econstructor); eauto. + + (* case Tr_end_block *) inversion H3; subst; cbn; auto. + * destruct (header bh); congruence. + * destruct bl0; cbn; congruence. + + (* case Tr_add_basic *) rewrite H3. cbn. destruct (header bh); congruence. +Qed. + +Lemma trans_code_is_trans_code_rev_inv c1: forall c2 mbi, + is_trans_code (rev_append c1 c2) mbi -> + exists mbi0, is_trans_code c2 mbi0 /\ mbi=trans_code_rev c1 mbi0. +Proof. + induction c1 as [| i c1]; cbn; eauto. + intros; exploit IHc1; eauto. + intros (mbi0 & H1 & H2); subst. + exploit add_to_code_is_trans_code_inv; eauto. + intros. destruct H0 as [mbi1 [H2 H3]]. + exists mbi1. split; congruence. +Qed. + +Local Hint Resolve trans_code_is_trans_code: core. + +Theorem is_trans_code_inv c bl: is_trans_code c bl <-> bl=(trans_code c). +Proof. + constructor; intros; subst; auto. + unfold trans_code. + exploit (trans_code_is_trans_code_rev_inv (rev_append c nil) nil bl); eauto. + * rewrite <- rev_alt. + rewrite <- rev_alt. + rewrite (rev_involutive c). + apply H. + * intros. + destruct H0 as [mbi [H0 H1]]. + inversion H0. subst. reflexivity. +Qed. diff --git a/scheduling/postpass_lib/Machblockgenproof.v b/scheduling/postpass_lib/Machblockgenproof.v new file mode 100644 index 00000000..fc722887 --- /dev/null +++ b/scheduling/postpass_lib/Machblockgenproof.v @@ -0,0 +1,824 @@ +(* *************************************************************) +(* *) +(* The Compcert verified compiler *) +(* *) +(* Sylvain Boulmé Grenoble-INP, VERIMAG *) +(* 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. +Require Import Maps. +Require Import AST. +Require Import Integers. +Require Import Values. +Require Import Memory. +Require Import Globalenvs. +Require Import Events. +Require Import Smallstep. +Require Import Op. +Require Import Locations. +Require Import Conventions. +Require Stacklayout. +Require Import Mach. +Require Import Linking. +Require Import Machblock. +Require Import Machblockgen. +Require Import ForwardSimulationBlock. + +Ltac subst_is_trans_code H := + rewrite is_trans_code_inv in H; + rewrite <- H in * |- *; + rewrite <- is_trans_code_inv in H. + +Definition inv_trans_rao (rao: function -> code -> ptrofs -> Prop) (f: Mach.function) (c: Mach.code) := + rao (transf_function f) (trans_code c). + +Definition match_prog (p: Mach.program) (tp: Machblock.program) := + match_program (fun _ f tf => tf = transf_fundef f) eq p tp. + +Lemma transf_program_match: forall p tp, transf_program p = tp -> match_prog p tp. +Proof. + intros. rewrite <- H. eapply match_transform_program; eauto. +Qed. + +Definition trans_stackframe (msf: Mach.stackframe) : stackframe := + match msf with + | Mach.Stackframe f sp retaddr c => Stackframe f sp retaddr (trans_code c) + end. + +Fixpoint trans_stack (mst: list Mach.stackframe) : list stackframe := + match mst with + | nil => nil + | msf :: mst0 => (trans_stackframe msf) :: (trans_stack mst0) + end. + +Definition trans_state (ms: Mach.state): state := + match ms with + | Mach.State s f sp c rs m => State (trans_stack s) f sp (trans_code c) rs m + | Mach.Callstate s f rs m => Callstate (trans_stack s) f rs m + | Mach.Returnstate s rs m => Returnstate (trans_stack s) rs m + end. + +Section PRESERVATION. + +Local Open Scope nat_scope. + +Variable prog: Mach.program. +Variable tprog: Machblock.program. +Hypothesis TRANSF: match_prog prog tprog. +Let ge := Genv.globalenv prog. +Let tge := Genv.globalenv tprog. + + +Variable rao: function -> code -> ptrofs -> Prop. + +Definition match_states: Mach.state -> state -> Prop + := ForwardSimulationBlock.match_states (Mach.semantics (inv_trans_rao rao) prog) (Machblock.semantics rao tprog) trans_state. + +Lemma match_states_trans_state s1: match_states s1 (trans_state s1). +Proof. + apply match_states_trans_state. +Qed. + +Local Hint Resolve match_states_trans_state: core. + +Lemma symbols_preserved: + forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. +Proof (Genv.find_symbol_match TRANSF). + +Lemma senv_preserved: + Senv.equiv ge tge. +Proof (Genv.senv_match TRANSF). + +Lemma init_mem_preserved: + forall m, + Genv.init_mem prog = Some m -> + Genv.init_mem tprog = Some m. +Proof (Genv.init_mem_transf TRANSF). + +Lemma prog_main_preserved: + prog_main tprog = prog_main prog. +Proof (match_program_main TRANSF). + +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 = tf. +Proof. + intros. + exploit (Genv.find_funct_ptr_match TRANSF); eauto. intro. + destruct H0 as (cunit & tf & A & B & C). + eapply ex_intro. intuition; eauto. subst. eapply A. +Qed. + +Lemma find_function_ptr_same: + forall s rs, + Mach.find_function_ptr ge s rs = find_function_ptr tge s rs. +Proof. + intros. unfold Mach.find_function_ptr. unfold find_function_ptr. + destruct s; auto. + rewrite symbols_preserved; auto. +Qed. + +Lemma find_funct_ptr_same: + forall f f0, + Genv.find_funct_ptr ge f = Some (Internal f0) -> + Genv.find_funct_ptr tge f = Some (Internal (transf_function f0)). +Proof. + intros. exploit (Genv.find_funct_ptr_transf TRANSF); eauto. +Qed. + +Lemma find_funct_ptr_same_external: + forall f f0, + Genv.find_funct_ptr ge f = Some (External f0) -> + Genv.find_funct_ptr tge f = Some (External f0). +Proof. + intros. exploit (Genv.find_funct_ptr_transf TRANSF); eauto. +Qed. + +Lemma parent_sp_preserved: + forall s, + Mach.parent_sp s = parent_sp (trans_stack s). +Proof. + unfold parent_sp. unfold Mach.parent_sp. destruct s; cbn; auto. + unfold trans_stackframe. destruct s; cbn; auto. +Qed. + +Lemma parent_ra_preserved: + forall s, + Mach.parent_ra s = parent_ra (trans_stack s). +Proof. + unfold parent_ra. unfold Mach.parent_ra. destruct s; cbn; auto. + unfold trans_stackframe. destruct s; cbn; auto. +Qed. + +Lemma external_call_preserved: + forall ef args m t res m', + external_call ef ge args m t res m' -> + external_call ef tge args m t res m'. +Proof. + intros. eapply external_call_symbols_preserved; eauto. + apply senv_preserved. +Qed. + +Lemma Mach_find_label_split l i c c': + Mach.find_label l (i :: c) = Some c' -> + (i=Mlabel l /\ c' = c) \/ (i <> Mlabel l /\ Mach.find_label l c = Some c'). +Proof. + intros H. + destruct i; try (constructor 2; split; auto; discriminate ). + destruct (peq l0 l) as [P|P]. + - constructor. subst l0; split; auto. + revert H. unfold Mach.find_label. cbn. rewrite peq_true. + intros H; injection H; auto. + - constructor 2. split. + + intro F. injection F. intros. contradict P; auto. + + revert H. unfold Mach.find_label. cbn. rewrite peq_false; auto. +Qed. + +Lemma find_label_is_end_block_not_label i l c bl: + is_end_block (trans_inst i) bl -> + is_trans_code c bl -> + i <> Mlabel l -> find_label l (add_to_new_bblock (trans_inst i) :: bl) = find_label l bl. +Proof. + intros H H0 H1. + unfold find_label. + remember (is_label l _) as b. + cutrewrite (b = false); auto. + subst; unfold is_label. + destruct i; cbn in * |- *; try (destruct (in_dec l nil); intuition). + inversion H. + destruct (in_dec l (l0::nil)) as [H6|H6]; auto. + cbn in H6; intuition try congruence. +Qed. + +Lemma find_label_at_begin l bh bl: + In l (header bh) + -> find_label l (bh :: bl) = Some (bh::bl). +Proof. + unfold find_label; rewrite is_label_correct_true; intro H; rewrite H; cbn; auto. +Qed. + +Lemma find_label_add_label_diff l bh bl: + ~(In l (header bh)) -> + find_label l (bh::bl) = find_label l bl. +Proof. + unfold find_label; rewrite is_label_correct_false; intro H; rewrite H; cbn; auto. +Qed. + +Definition concat (h: list label) (c: code): code := + match c with + | nil => {| header := h; body := nil; exit := None |}::nil + | b::c' => {| header := h ++ (header b); body := body b; exit := exit b |}::c' + end. + +Lemma find_label_transcode_preserved: + forall l c c', + Mach.find_label l c = Some c' -> + exists h, In l h /\ find_label l (trans_code c) = Some (concat h (trans_code c')). +Proof. + intros l c. remember (trans_code _) as bl. + rewrite <- is_trans_code_inv in * |-. + induction Heqbl. + + (* Tr_nil *) + intros; exists (l::nil); cbn in * |- *; intuition. + discriminate. + + (* Tr_end_block *) + intros. + exploit Mach_find_label_split; eauto. + clear H0; destruct 1 as [(H0&H2)|(H0&H2)]. + - subst. rewrite find_label_at_begin; cbn; auto. + inversion H as [mbi H1 H2| | ]. + subst. + inversion Heqbl. + subst. + exists (l :: nil); cbn; eauto. + - exploit IHHeqbl; eauto. + destruct 1 as (h & H3 & H4). + exists h. + split; auto. + erewrite find_label_is_end_block_not_label;eauto. + + (* Tr_add_label *) + intros. + exploit Mach_find_label_split; eauto. + clear H0; destruct 1 as [(H0&H2)|(H0&H2)]. + - subst. + inversion H0 as [H1]. + clear H0. + erewrite find_label_at_begin; cbn; eauto. + subst_is_trans_code Heqbl. + exists (l :: nil); cbn; eauto. + - subst; assert (H: l0 <> l); try congruence; clear H0. + exploit IHHeqbl; eauto. + clear IHHeqbl Heqbl. + intros (h & H3 & H4). + cbn; unfold is_label, add_label; cbn. + destruct (in_dec l (l0::header bh)) as [H5|H5]; cbn in H5. + * destruct H5; try congruence. + exists (l0::h); cbn; intuition. + rewrite find_label_at_begin in H4; auto. + apply f_equal. inversion H4 as [H5]. clear H4. + destruct (trans_code c'); cbn in * |- *; + inversion H5; subst; cbn; auto. + * exists h. intuition. + erewrite <- find_label_add_label_diff; eauto. + + (* Tr_add_basic *) + intros. + exploit Mach_find_label_split; eauto. + destruct 1 as [(H2&H3)|(H2&H3)]. + rewrite H2 in H. unfold trans_inst in H. congruence. + exploit IHHeqbl; eauto. + clear IHHeqbl Heqbl. + intros (h & H4 & H5). + rewrite find_label_add_label_diff; auto. + rewrite find_label_add_label_diff in H5; eauto. + rewrite H0; auto. +Qed. + +Lemma find_label_preserved: + forall l f c, + Mach.find_label l (Mach.fn_code f) = Some c -> + exists h, In l h /\ find_label l (fn_code (transf_function f)) = Some (concat h (trans_code c)). +Proof. + intros. cutrewrite ((fn_code (transf_function f)) = trans_code (Mach.fn_code f)); eauto. + apply find_label_transcode_preserved; auto. +Qed. + +Lemma mem_free_preserved: + forall m stk f, + Mem.free m stk 0 (Mach.fn_stacksize f) = Mem.free m stk 0 (fn_stacksize (transf_function f)). +Proof. + intros. auto. +Qed. + +Local Hint Resolve symbols_preserved senv_preserved init_mem_preserved prog_main_preserved functions_translated + parent_sp_preserved: core. + + +Definition dist_end_block_code (c: Mach.code) := + match trans_code c with + | nil => 0 + | bh::_ => (size bh-1)%nat + end. + +Definition dist_end_block (s: Mach.state): nat := + match s with + | Mach.State _ _ _ c _ _ => dist_end_block_code c + | _ => 0 + end. + +Local Hint Resolve exec_nil_body exec_cons_body: core. +Local Hint Resolve exec_MBgetstack exec_MBsetstack exec_MBgetparam exec_MBop exec_MBload exec_MBstore: core. + +Lemma size_add_label l bh: size (add_label l bh) = size bh + 1. +Proof. + unfold add_label, size; cbn; omega. +Qed. + +Lemma size_add_basic bi bh: header bh = nil -> size (add_basic bi bh) = size bh + 1. +Proof. + intro H. unfold add_basic, size; rewrite H; cbn. omega. +Qed. + + +Lemma size_add_to_newblock i: size (add_to_new_bblock i) = 1. +Proof. + destruct i; auto. +Qed. + + +Lemma dist_end_block_code_simu_mid_block i c: + dist_end_block_code (i::c) <> 0 -> + (dist_end_block_code (i::c) = Datatypes.S (dist_end_block_code c)). +Proof. + unfold dist_end_block_code. + remember (trans_code (i::c)) as bl. + rewrite <- is_trans_code_inv in Heqbl. + inversion Heqbl as [|bl0 H| |]; subst; clear Heqbl. + - rewrite size_add_to_newblock; omega. + - rewrite size_add_label; + subst_is_trans_code H. + omega. + - rewrite size_add_basic; auto. + subst_is_trans_code H. + omega. +Qed. + +Local Hint Resolve dist_end_block_code_simu_mid_block: core. + + +Lemma size_nonzero c b bl: + is_trans_code c (b :: bl) -> size b <> 0. +Proof. + intros H; inversion H; subst. + - rewrite size_add_to_newblock; omega. + - rewrite size_add_label; omega. + - rewrite size_add_basic; auto; omega. +Qed. + +Inductive is_header: list label -> Mach.code -> Mach.code -> Prop := + | header_empty : is_header nil nil nil + | header_not_label i c: (forall l, i <> Mlabel l) -> is_header nil (i::c) (i::c) + | header_is_label l h c c0: is_header h c c0 -> is_header (l::h) ((Mlabel l)::c) c0 + . + +Inductive is_body: list basic_inst -> Mach.code -> Mach.code -> Prop := + | body_empty : is_body nil nil nil + | body_not_bi i c: (forall bi, (trans_inst i) <> (MB_basic bi)) -> is_body nil (i::c) (i::c) + | body_is_bi i lbi c0 c1 bi: (trans_inst i) = MB_basic bi -> is_body lbi c0 c1 -> is_body (bi::lbi) (i::c0) c1 + . + +Inductive is_exit: option control_flow_inst -> Mach.code -> Mach.code -> Prop := + | exit_empty: is_exit None nil nil + | exit_not_cfi i c: (forall cfi, (trans_inst i) <> MB_cfi cfi) -> is_exit None (i::c) (i::c) + | exit_is_cfi i c cfi: (trans_inst i) = MB_cfi cfi -> is_exit (Some cfi) (i::c) c + . + +Lemma Mlabel_is_not_basic i: + forall bi, trans_inst i = MB_basic bi -> forall l, i <> Mlabel l. +Proof. +intros. +unfold trans_inst in H. +destruct i; congruence. +Qed. + +Lemma Mlabel_is_not_cfi i: + forall cfi, trans_inst i = MB_cfi cfi -> forall l, i <> Mlabel l. +Proof. +intros. +unfold trans_inst in H. +destruct i; congruence. +Qed. + +Lemma MBbasic_is_not_cfi i: + forall cfi, trans_inst i = MB_cfi cfi -> forall bi, trans_inst i <> MB_basic bi. +Proof. +intros. +unfold trans_inst in H. +unfold trans_inst. +destruct i; congruence. +Qed. + + +Local Hint Resolve Mlabel_is_not_cfi: core. +Local Hint Resolve MBbasic_is_not_cfi: core. + +Lemma add_to_new_block_is_label i: + header (add_to_new_bblock (trans_inst i)) <> nil -> exists l, i = Mlabel l. +Proof. + intros. + unfold add_to_new_bblock in H. + destruct (trans_inst i) eqn : H1. + + exists lbl. + unfold trans_inst in H1. + destruct i; congruence. + + unfold add_basic in H; cbn in H; congruence. + + unfold cfi_bblock in H; cbn in H; congruence. +Qed. + +Local Hint Resolve Mlabel_is_not_basic: core. + +Lemma trans_code_decompose c: forall b bl, + is_trans_code c (b::bl) -> + exists c0 c1 c2, is_header (header b) c c0 /\ is_body (body b) c0 c1 /\ is_exit (exit b) c1 c2 /\ is_trans_code c2 bl. +Proof. + induction c as [|i c]. + { (* nil => absurd *) intros b bl H; inversion H. } + intros b bl H; remember (trans_inst i) as ti. + destruct ti as [lbl|bi|cfi]; + inversion H as [|d0 d1 d2 H0 H1| |]; subst; + try (rewrite <- Heqti in * |- *); cbn in * |- *; + try congruence. + + (* label at end block *) + inversion H1; subst. inversion H0; subst. + assert (X:i=Mlabel lbl). { destruct i; cbn in Heqti; congruence. } + subst. repeat econstructor; eauto. + + (* label at mid block *) + exploit IHc; eauto. + intros (c0 & c1 & c2 & H1 & H2 & H3 & H4). + repeat econstructor; eauto. + + (* basic at end block *) + inversion H1; subst. + lapply (Mlabel_is_not_basic i bi); auto. + intro H2. + - inversion H0; subst. + assert (X:(trans_inst i) = MB_basic bi ). { repeat econstructor; congruence. } + repeat econstructor; congruence. + - exists (i::c), c, c. + repeat econstructor; eauto; inversion H0; subst; repeat econstructor; cbn; try congruence. + * exploit (add_to_new_block_is_label i0); eauto. + intros (l & H8); subst; cbn; congruence. + * exploit H3; eauto. + * exploit (add_to_new_block_is_label i0); eauto. + intros (l & H8); subst; cbn; congruence. + + (* basic at mid block *) + inversion H1; subst. + exploit IHc; eauto. + intros (c0 & c1 & c2 & H3 & H4 & H5 & H6). + exists (i::c0), c1, c2. + repeat econstructor; eauto. + rewrite H2 in H3. + inversion H3; econstructor; eauto. + + (* cfi at end block *) + inversion H1; subst; + repeat econstructor; eauto. +Qed. + + +Lemma step_simu_header st f sp rs m s c h c' t: + is_header h c c' -> + starN (Mach.step (inv_trans_rao rao)) (Genv.globalenv prog) (length h) (Mach.State st f sp c rs m) t s -> + s = Mach.State st f sp c' rs m /\ t = E0. +Proof. + induction 1; cbn; intros hs; try (inversion hs; tauto). + inversion hs as [|n1 s1 t1 t2 s2 t3 s3 H1]. inversion H1. subst. auto. +Qed. + + + +Lemma step_simu_basic_step (i: Mach.instruction) (bi: basic_inst) (c: Mach.code) s f sp rs m (t:trace) (s':Mach.state): + trans_inst i = MB_basic bi -> + Mach.step (inv_trans_rao rao) ge (Mach.State s f sp (i::c) rs m) t s' -> + exists rs' m', s'=Mach.State s f sp c rs' m' /\ t=E0 /\ basic_step tge (trans_stack s) f sp rs m bi rs' m'. +Proof. + destruct i; cbn in * |-; + (discriminate + || (intro H; inversion_clear H; intro X; inversion_clear X; eapply ex_intro; eapply ex_intro; intuition eauto)). + - eapply exec_MBgetparam; eauto. exploit (functions_translated); eauto. intro. + destruct H3 as (tf & A & B). subst. eapply A. + all: cbn; rewrite <- parent_sp_preserved; auto. + - eapply exec_MBop; eauto. rewrite <- H. destruct o; cbn; auto. destruct (rs ## l); cbn; auto. + unfold Genv.symbol_address; rewrite symbols_preserved; auto. + - eapply exec_MBload; eauto; rewrite <- H; destruct a; cbn; auto; destruct (rs ## l); cbn; auto; + unfold Genv.symbol_address; rewrite symbols_preserved; auto. + - eapply exec_MBload_notrap1; eauto; rewrite <- H; destruct a; cbn; auto; destruct (rs ## l); cbn; auto; + unfold Genv.symbol_address; rewrite symbols_preserved; auto. + - eapply exec_MBload_notrap2; eauto; rewrite <- H; destruct a; cbn; auto; destruct (rs ## l); cbn; auto; + unfold Genv.symbol_address; rewrite symbols_preserved; auto. + - eapply exec_MBstore; eauto; rewrite <- H; destruct a; cbn; auto; destruct (rs ## l); cbn; auto; + unfold Genv.symbol_address; rewrite symbols_preserved; auto. +Qed. + + +Lemma star_step_simu_body_step s f sp c bdy c': + is_body bdy c c' -> forall rs m t s', + starN (Mach.step (inv_trans_rao rao)) ge (length bdy) (Mach.State s f sp c rs m) t s' -> + exists rs' m', s'=Mach.State s f sp c' rs' m' /\ t=E0 /\ body_step tge (trans_stack s) f sp bdy rs m rs' m'. +Proof. + induction 1; cbn. + + intros. inversion H. exists rs. exists m. auto. + + intros. inversion H0. exists rs. exists m. auto. + + intros. inversion H1; subst. + exploit (step_simu_basic_step ); eauto. + destruct 1 as [ rs1 [ m1 Hs]]. + destruct Hs as [Hs1 [Hs2 Hs3]]. + destruct (IHis_body rs1 m1 t2 s') as [rs2 Hb]. rewrite <- Hs1; eauto. + destruct Hb as [m2 [Hb1 [Hb2 Hb3]]]. + exists rs2, m2. + rewrite Hs2, Hb2; eauto. + Qed. + +Local Hint Resolve exec_MBcall exec_MBtailcall exec_MBbuiltin exec_MBgoto exec_MBcond_true exec_MBcond_false exec_MBjumptable exec_MBreturn exec_Some_exit exec_None_exit: core. +Local Hint Resolve eval_builtin_args_preserved external_call_symbols_preserved find_funct_ptr_same: core. + + +Lemma match_states_concat_trans_code st f sp c rs m h: + match_states (Mach.State st f sp c rs m) (State (trans_stack st) f sp (concat h (trans_code c)) rs m). +Proof. + intros; constructor 1; cbn. + + intros (t0 & s1' & H0) t s'. + remember (trans_code _) as bl. + destruct bl as [|bh bl]. + { rewrite <- is_trans_code_inv in Heqbl; inversion Heqbl; inversion H0; congruence. } + clear H0. + cbn; constructor 1; + intros X; inversion X as [d1 d2 d3 d4 d5 d6 d7 rs' m' d10 d11 X1 X2| | | ]; subst; cbn in * |- *; + eapply exec_bblock; eauto; cbn; + inversion X2 as [cfi d1 d2 d3 H1|]; subst; eauto; + inversion H1; subst; eauto. + + intros H r; constructor 1; intro X; inversion X. +Qed. + +Lemma step_simu_cfi_step (i: Mach.instruction) (cfi: control_flow_inst) (c: Mach.code) (blc:code) stk f sp rs m (t:trace) (s':Mach.state) b: + trans_inst i = MB_cfi cfi -> + is_trans_code c blc -> + Mach.step (inv_trans_rao rao) ge (Mach.State stk f sp (i::c) rs m) t s' -> + exists s2, cfi_step rao tge cfi (State (trans_stack stk) f sp (b::blc) rs m) t s2 /\ match_states s' s2. +Proof. + destruct i; cbn in * |-; + (intro H; intro Htc;apply is_trans_code_inv in Htc;rewrite Htc;inversion_clear H;intro X; inversion_clear X). + * eapply ex_intro. + intuition auto. + eapply exec_MBcall;eauto. + rewrite <-H; exploit (find_function_ptr_same); eauto. + * eapply ex_intro. + intuition auto. + eapply exec_MBtailcall;eauto. + - rewrite <-H; exploit (find_function_ptr_same); eauto. + - cbn; rewrite <- parent_sp_preserved; auto. + - cbn; rewrite <- parent_ra_preserved; auto. + * eapply ex_intro. + intuition auto. + eapply exec_MBbuiltin ;eauto. + * exploit find_label_transcode_preserved; eauto. + intros (x & X1 & X2). + eapply ex_intro; constructor 1; [ idtac | eapply match_states_concat_trans_code ]; eauto. + * exploit find_label_transcode_preserved; eauto. + intros (x & X1 & X2). + eapply ex_intro; constructor 1; [ idtac | eapply match_states_concat_trans_code ]; eauto. + * eapply ex_intro; constructor 1; [ idtac | eapply match_states_trans_state ]; eauto. + eapply exec_MBcond_false; eauto. + * exploit find_label_transcode_preserved; eauto. intros (h & X1 & X2). + eapply ex_intro; constructor 1; [ idtac | eapply match_states_concat_trans_code ]; eauto. + * eapply ex_intro; constructor 1; [ idtac | eapply match_states_trans_state ]; eauto. + eapply exec_MBreturn; eauto. + rewrite parent_sp_preserved in H0; subst; auto. + rewrite parent_ra_preserved in H1; subst; auto. +Qed. + +Lemma step_simu_exit_step stk f sp rs m t s1 e c c' b blc: + is_exit e c c' -> is_trans_code c' blc -> + starN (Mach.step (inv_trans_rao rao)) (Genv.globalenv prog) (length_opt e) (Mach.State stk f sp c rs m) t s1 -> + exists s2, exit_step rao tge e (State (trans_stack stk) f sp (b::blc) rs m) t s2 /\ match_states s1 s2. +Proof. + destruct 1. + - (* None *) + intros H0 H1. inversion H1. exists (State (trans_stack stk) f sp blc rs m). + split; eauto. + apply is_trans_code_inv in H0. + rewrite H0. + apply match_states_trans_state. + - (* None *) + intros H0 H1. inversion H1. exists (State (trans_stack stk) f sp blc rs m). + split; eauto. + apply is_trans_code_inv in H0. + rewrite H0. + apply match_states_trans_state. + - (* Some *) + intros H0 H1. + inversion H1; subst. + exploit (step_simu_cfi_step); eauto. + intros [s2 [Hcfi1 Hcfi3]]. + inversion H4. subst; cbn. + autorewrite with trace_rewrite. + exists s2. + split;eauto. +Qed. + +Lemma simu_end_block: + forall s1 t s1', + starN (Mach.step (inv_trans_rao rao)) ge (Datatypes.S (dist_end_block s1)) s1 t s1' -> + exists s2', step rao tge (trans_state s1) t s2' /\ match_states s1' s2'. +Proof. + destruct s1; cbn. + + (* State *) + remember (trans_code _) as tc. + rewrite <- is_trans_code_inv in Heqtc. + intros t s1 H. + destruct tc as [|b bl]. + { (* nil => absurd *) + inversion Heqtc. subst. + unfold dist_end_block_code; cbn. + inversion_clear H; + inversion_clear H0. + } + assert (X: Datatypes.S (dist_end_block_code c) = (size b)). + { + unfold dist_end_block_code. + subst_is_trans_code Heqtc. + lapply (size_nonzero c b bl); auto. + omega. + } + rewrite X in H; unfold size in H. + (* decomposition of starN in 3 parts: header + body + exit *) + destruct (starN_split (Mach.semantics (inv_trans_rao rao) prog) _ _ _ _ H _ _ refl_equal) as (t3&t4&s1'&H0&H3&H4). + subst t; clear X H. + destruct (starN_split (Mach.semantics (inv_trans_rao rao) prog) _ _ _ _ H0 _ _ refl_equal) as (t1&t2&s1''&H&H1&H2). + subst t3; clear H0. + exploit trans_code_decompose; eauto. clear Heqtc. + intros (c0&c1&c2&Hc0&Hc1&Hc2&Heqtc). + (* header steps *) + exploit step_simu_header; eauto. + clear H; intros [X1 X2]; subst. + (* body steps *) + exploit (star_step_simu_body_step); eauto. + clear H1; intros (rs'&m'&H0&H1&H2). subst. + autorewrite with trace_rewrite. + (* exit step *) + exploit step_simu_exit_step; eauto. + clear H3; intros (s2' & H3 & H4). + eapply ex_intro; intuition eauto. + eapply exec_bblock; eauto. + + (* Callstate *) + intros t s1' H; inversion_clear H. + eapply ex_intro; constructor 1; eauto. + inversion H1; subst; clear H1. + inversion_clear H0; cbn. + - (* function_internal*) + cutrewrite (trans_code (Mach.fn_code f0) = fn_code (transf_function f0)); eauto. + eapply exec_function_internal; eauto. + rewrite <- parent_sp_preserved; eauto. + rewrite <- parent_ra_preserved; eauto. + - (* function_external *) + autorewrite with trace_rewrite. + eapply exec_function_external; eauto. + apply find_funct_ptr_same_external; auto. + rewrite <- parent_sp_preserved; eauto. + + (* Returnstate *) + intros t s1' H; inversion_clear H. + eapply ex_intro; constructor 1; eauto. + inversion H1; subst; clear H1. + inversion_clear H0; cbn. + eapply exec_return. +Qed. + + +Lemma cfi_dist_end_block i c: +(exists cfi, trans_inst i = MB_cfi cfi) -> +dist_end_block_code (i :: c) = 0. +Proof. + unfold dist_end_block_code. + intro H. destruct H as [cfi H]. + destruct i;cbn in H;try(congruence); ( + remember (trans_code _) as bl; + rewrite <- is_trans_code_inv in Heqbl; + inversion Heqbl; subst; cbn in * |- *; try (congruence)). +Qed. + +Theorem transf_program_correct: + forward_simulation (Mach.semantics (inv_trans_rao rao) prog) (Machblock.semantics rao tprog). +Proof. + apply forward_simulation_block_trans with (dist_end_block := dist_end_block) (trans_state := trans_state). +(* simu_mid_block *) + - intros s1 t s1' H1 H2. + destruct H1; cbn in * |- *; omega || (intuition auto); + destruct H2; eapply cfi_dist_end_block; cbn; eauto. +(* public_preserved *) + - apply senv_preserved. +(* match_initial_states *) + - intros. cbn. + eapply ex_intro; constructor 1. + eapply match_states_trans_state. + destruct H. split. + apply init_mem_preserved; auto. + rewrite prog_main_preserved. rewrite <- H0. apply symbols_preserved. +(* match_final_states *) + - intros. cbn. destruct H. split with (r := r); auto. +(* final_states_end_block *) + - intros. cbn in H0. + inversion H0. + inversion H; cbn; auto. + all: try (subst; discriminate). + apply cfi_dist_end_block; exists MBreturn; eauto. +(* simu_end_block *) + - apply simu_end_block. +Qed. + +End PRESERVATION. + +(** Auxiliary lemmas used to prove existence of a Mach return adress from a Machblock return address. *) + + + +Lemma is_trans_code_monotonic i c b l: + is_trans_code c (b::l) -> + exists l' b', is_trans_code (i::c) (l' ++ (b'::l)). +Proof. + intro H; destruct c as [|i' c]. { inversion H. } + remember (trans_inst i) as ti. + destruct ti as [lbl|bi|cfi]. + - (*i=lbl *) cutrewrite (i = Mlabel lbl). 2: ( destruct i; cbn in * |- *; try congruence ). + exists nil; cbn; eexists. eapply Tr_add_label; eauto. + - (*i=basic*) + destruct i'. + 10: { exists (add_to_new_bblock (MB_basic bi)::nil). exists b. + cutrewrite ((add_to_new_bblock (MB_basic bi) :: nil) ++ (b::l)=(add_to_new_bblock (MB_basic bi) :: (b::l)));eauto. + rewrite Heqti. + eapply Tr_end_block; eauto. + rewrite <-Heqti. + eapply End_basic. inversion H; try(cbn; congruence). + cbn in H5; congruence. } + all: try(exists nil; cbn; eexists; eapply Tr_add_basic; eauto; inversion H; try(eauto || congruence)). + - (*i=cfi*) + destruct i; try(cbn in Heqti; congruence). + all: exists (add_to_new_bblock (MB_cfi cfi)::nil); exists b; + cutrewrite ((add_to_new_bblock (MB_cfi cfi) :: nil) ++ (b::l)=(add_to_new_bblock (MB_cfi cfi) :: (b::l)));eauto; + rewrite Heqti; + eapply Tr_end_block; eauto; + rewrite <-Heqti; + eapply End_cfi; congruence. +Qed. + +Lemma trans_code_monotonic i c b l: + (b::l) = trans_code c -> + exists l' b', trans_code (i::c) = (l' ++ (b'::l)). +Proof. + intro H; rewrite <- is_trans_code_inv in H. + destruct (is_trans_code_monotonic i c b l H) as (l' & b' & H0). + subst_is_trans_code H0. + eauto. +Qed. + +(* FIXME: these two lemma should go into [Coqlib.v] *) +Lemma is_tail_app A (l1: list A): forall l2, is_tail l2 (l1 ++ l2). +Proof. + induction l1; cbn; auto with coqlib. +Qed. +Hint Resolve is_tail_app: coqlib. + +Lemma is_tail_app_inv A (l1: list A): forall l2 l3, is_tail (l1 ++ l2) l3 -> is_tail l2 l3. +Proof. + induction l1; cbn; auto with coqlib. + intros l2 l3 H; inversion H; eauto with coqlib. +Qed. +Hint Resolve is_tail_app_inv: coqlib. + + +Lemma Mach_Machblock_tail sg ros c c1 c2: c1=(Mcall sg ros :: c) -> is_tail c1 c2 -> + exists b, is_tail (b :: trans_code c) (trans_code c2). +Proof. + intros H; induction 1. + - intros; subst. + remember (trans_code (Mcall _ _::c)) as tc2. + rewrite <- is_trans_code_inv in Heqtc2. + inversion Heqtc2; cbn in * |- *; subst; try congruence. + subst_is_trans_code H1. + eapply ex_intro; eauto with coqlib. + - intros; exploit IHis_tail; eauto. clear IHis_tail. + intros (b & Hb). inversion Hb; clear Hb. + * exploit (trans_code_monotonic i c2); eauto. + intros (l' & b' & Hl'); rewrite Hl'. + exists b'; cbn; eauto with coqlib. + * exploit (trans_code_monotonic i c2); eauto. + intros (l' & b' & Hl'); rewrite Hl'. + cbn; eapply ex_intro. + eapply is_tail_trans; eauto with coqlib. +Qed. + +Section Mach_Return_Address. + +Variable return_address_offset: function -> code -> ptrofs -> Prop. + +Hypothesis ra_exists: forall (b: bblock) (f: function) (c : list bblock), + is_tail (b :: c) (fn_code f) -> exists ra : ptrofs, return_address_offset f c ra. + +Definition Mach_return_address_offset (f: Mach.function) (c: Mach.code) (ofs: ptrofs) : Prop := + return_address_offset (transf_function f) (trans_code c) ofs. + +Lemma Mach_return_address_exists: + forall f sg ros c, is_tail (Mcall sg ros :: c) f.(Mach.fn_code) -> + exists ra, Mach_return_address_offset f c ra. +Proof. + intros. + exploit Mach_Machblock_tail; eauto. + destruct 1. + eapply ra_exists; eauto. +Qed. + +End Mach_Return_Address. -- cgit