From 355b4abcee015c3fae9ac5653c25259e104a886c Mon Sep 17 00:00:00 2001 From: xleroy Date: Sat, 4 Aug 2007 07:27:50 +0000 Subject: Fusion des modifications faites sur les branches "tailcalls" et "smallstep". En particulier: - Semantiques small-step depuis RTL jusqu'a PPC - Cminor independant du processeur - Ajout passes Selection et Reload - Ajout des langages intermediaires CminorSel et LTLin correspondants - Ajout des tailcalls depuis Cminor jusqu'a PPC git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@384 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/Linearizeproof.v | 865 ++++++++++++++++++++++------------------------- 1 file changed, 408 insertions(+), 457 deletions(-) (limited to 'backend/Linearizeproof.v') diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index 5937fc34..c7299085 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -8,10 +8,12 @@ Require Import Values. Require Import Mem. Require Import Events. Require Import Globalenvs. +Require Import Smallstep. Require Import Op. Require Import Locations. Require Import LTL. -Require Import Linear. +Require Import LTLtyping. +Require Import LTLin. Require Import Linearize. Require Import Lattice. @@ -46,6 +48,18 @@ Proof. destruct f; reflexivity. Qed. +Lemma find_function_translated: + forall ros ls f, + LTL.find_function ge ros ls = Some f -> + find_function tge ros ls = Some (transf_fundef f). +Proof. + intros until f. destruct ros; simpl. + intro. apply functions_translated; auto. + rewrite symbols_preserved. destruct (Genv.find_symbol ge i). + apply function_ptr_translated; auto. + congruence. +Qed. + (** * Correctness of reachability analysis *) (** The entry point of the function is reachable. *) @@ -62,11 +76,10 @@ Proof. intros. apply PMap.gi. Qed. -(** The successors of a reachable basic block are reachable. *) +(** The successors of a reachable instruction are reachable. *) Lemma reachable_successors: forall f pc pc', - f.(LTL.fn_code)!pc <> None -> In pc' (successors f pc) -> (reachable f)!!pc = true -> (reachable f)!!pc' = true. @@ -74,51 +87,19 @@ Proof. intro f. unfold reachable. caseEq (reachable_aux f). unfold reachable_aux. intro reach; intros. + elim (LTL.fn_code_wf f pc); intro. assert (LBoolean.ge reach!!pc' reach!!pc). change (reach!!pc) with ((fun pc r => r) pc (reach!!pc)). - eapply DS.fixpoint_solution. eexact H. - elim (fn_code_wf f pc); intro. auto. contradiction. - auto. + eapply DS.fixpoint_solution. eexact H. auto. auto. elim H3; intro. congruence. auto. + unfold successors in H0. rewrite H2 in H0. contradiction. intros. apply PMap.gi. Qed. -(* If we have a valid LTL transition from [pc] to [pc'], and - [pc] is reachable, then [pc'] is reachable. *) - -Lemma reachable_correct_1: - forall f sp pc rs m t pc' rs' m' b, - f.(LTL.fn_code)!pc = Some b -> - exec_block ge sp b rs m t (Cont pc') rs' m' -> - (reachable f)!!pc = true -> - (reachable f)!!pc' = true. -Proof. - intros. apply reachable_successors with pc; auto. - congruence. - eapply successors_correct; eauto. -Qed. - -Lemma reachable_correct_2: - forall c sp pc rs m t out rs' m', - exec_blocks ge c sp pc rs m t out rs' m' -> - forall f pc', - c = f.(LTL.fn_code) -> - out = Cont pc' -> - (reachable f)!!pc = true -> - (reachable f)!!pc' = true. -Proof. - induction 1; intros. - congruence. - eapply reachable_correct_1. rewrite <- H1; eauto. - subst out; eauto. auto. - auto. -Qed. - (** * Properties of node enumeration *) (** An enumeration of CFG nodes is correct if the following conditions hold: - All nodes for reachable basic blocks must be in the list. -- The function entry point is the first element in the list. - The list is without repetition (so that no code duplication occurs). We prove that our [enumerate] function satisfies all three. *) @@ -131,10 +112,10 @@ Lemma enumerate_complete: Proof. intros. assert (forall p, - Plt p (Psucc f.(fn_entrypoint)) -> + Plt p f.(fn_nextpc) -> (reachable f)!!p = true -> In p (enumerate f)). - unfold enumerate. pattern (Psucc (fn_entrypoint f)). + unfold enumerate. pattern (fn_nextpc f). apply positive_Peano_ind. intros. compute in H1. destruct p; discriminate. intros. rewrite positive_rec_succ. elim (Plt_succ_inv _ _ H2); intro. @@ -143,27 +124,15 @@ Proof. elim (LTL.fn_code_wf f pc); intro. auto. congruence. Qed. -Lemma enumerate_head: - forall f, exists l, enumerate f = f.(LTL.fn_entrypoint) :: l. -Proof. - intro. unfold enumerate. rewrite positive_rec_succ. - rewrite reachable_entrypoint. - exists (positive_rec (list node) nil - (fun (pc : positive) (nodes : list node) => - if (reachable f) !! pc then pc :: nodes else nodes) - (fn_entrypoint f) ). - auto. -Qed. - Lemma enumerate_norepet: forall f, list_norepet (enumerate f). Proof. intro. - unfold enumerate. pattern (Psucc (fn_entrypoint f)). + unfold enumerate. pattern (fn_nextpc f). apply positive_Peano_ind. rewrite positive_rec_base. constructor. intros. rewrite positive_rec_succ. - case (reachable f)!!x. auto. + case (reachable f)!!x. constructor. assert (forall y, In y (positive_rec @@ -183,9 +152,9 @@ Proof. auto. Qed. -(** * Correctness of the cleanup pass *) +(** * Properties related to labels *) -(** If labels are globally unique and the Linear code [c] contains +(** If labels are globally unique and the LTLin code [c] contains a subsequence [Llabel lbl :: c1], [find_label lbl c] returns [c1]. *) @@ -196,27 +165,6 @@ Fixpoint unique_labels (c: code) : Prop := | i :: c => unique_labels c end. -Inductive is_tail: code -> code -> Prop := - | is_tail_refl: - forall c, is_tail c c - | is_tail_cons: - forall i c1 c2, is_tail c1 c2 -> is_tail c1 (i :: c2). - -Lemma is_tail_in: - forall i c1 c2, is_tail (i :: c1) c2 -> In i c2. -Proof. - induction c2; simpl; intros. - inversion H. - inversion H. tauto. right; auto. -Qed. - -Lemma is_tail_cons_left: - forall i c1 c2, is_tail (i :: c1) c2 -> is_tail c1 c2. -Proof. - induction c2; intros; inversion H. - constructor. constructor. constructor. auto. -Qed. - Lemma find_label_unique: forall lbl c1 c2 c3, is_tail (Llabel lbl :: c1) c2 -> @@ -237,163 +185,51 @@ Qed. (** Correctness of the [starts_with] test. *) Lemma starts_with_correct: - forall lbl c1 c2 c3 f sp ls m, + forall lbl c1 c2 c3 s f sp ls m, is_tail c1 c2 -> unique_labels c2 -> starts_with lbl c1 = true -> find_label lbl c2 = Some c3 -> - exec_instrs tge f sp (cleanup_code c1) ls m - E0 (cleanup_code c3) ls m. + plus step tge (State s f sp c1 ls m) + E0 (State s f sp c3 ls m). Proof. induction c1. simpl; intros; discriminate. simpl starts_with. destruct a; try (intros; discriminate). - intros. apply exec_trans with E0 (cleanup_code c1) ls m E0. - simpl. - constructor. constructor. + intros. + apply plus_left with E0 (State s f sp c1 ls m) E0. + simpl. constructor. destruct (peq lbl l). subst l. replace c3 with c1. constructor. apply find_label_unique with lbl c2; auto. + apply plus_star. apply IHc1 with c2; auto. eapply is_tail_cons_left; eauto. traceEq. Qed. -(** Code cleanup preserves the labeling of the code. *) - -Lemma find_label_cleanup_code: - forall lbl c c', - find_label lbl c = Some c' -> - find_label lbl (cleanup_code c) = Some (cleanup_code c'). -Proof. - induction c. - simpl. intros; discriminate. - generalize (is_label_correct lbl a). - simpl find_label. case (is_label lbl a); intro. - subst a. intros. injection H; intros. subst c'. - simpl. rewrite peq_true. auto. - intros. destruct a; auto. - simpl. rewrite peq_false. auto. - congruence. - case (starts_with l c). auto. simpl. auto. -Qed. - -(** One transition in the original Linear code corresponds to zero - or one transitions in the cleaned-up code. *) - -Lemma cleanup_code_correct_1: - forall f sp c1 ls1 m1 t c2 ls2 m2, - exec_instr tge f sp c1 ls1 m1 t c2 ls2 m2 -> - is_tail c1 f.(fn_code) -> - unique_labels f.(fn_code) -> - exec_instrs tge (cleanup_function f) sp - (cleanup_code c1) ls1 m1 - t (cleanup_code c2) ls2 m2. -Proof. - induction 1; simpl; intros; - try (apply exec_one; econstructor; eauto; fail). - (* goto *) - caseEq (starts_with lbl b); intro SW. - eapply starts_with_correct; eauto. - eapply is_tail_cons_left; eauto. - constructor. constructor. - unfold cleanup_function; simpl. - apply find_label_cleanup_code. auto. - (* cond, taken *) - constructor. apply exec_Lcond_true. auto. - unfold cleanup_function; simpl. - apply find_label_cleanup_code. auto. - (* cond, not taken *) - constructor. apply exec_Lcond_false. auto. -Qed. - -Lemma is_tail_find_label: - forall lbl c2 c1, - find_label lbl c1 = Some c2 -> is_tail c2 c1. -Proof. - induction c1; simpl. - intros; discriminate. - case (is_label lbl a). intro. injection H; intro. subst c2. - constructor. constructor. - intro. constructor. auto. -Qed. - -Lemma is_tail_exec_instr: - forall f sp c1 ls1 m1 t c2 ls2 m2, - exec_instr tge f sp c1 ls1 m1 t c2 ls2 m2 -> - is_tail c1 f.(fn_code) -> is_tail c2 f.(fn_code). -Proof. - induction 1; intros; - try (eapply is_tail_cons_left; eauto; fail). - eapply is_tail_find_label; eauto. - eapply is_tail_find_label; eauto. -Qed. - -Lemma is_tail_exec_instrs: - forall f sp c1 ls1 m1 t c2 ls2 m2, - exec_instrs tge f sp c1 ls1 m1 t c2 ls2 m2 -> - is_tail c1 f.(fn_code) -> is_tail c2 f.(fn_code). -Proof. - induction 1; intros. - auto. - eapply is_tail_exec_instr; eauto. - auto. -Qed. - -(** Zero, one or several transitions in the original Linear code correspond - to zero, one or several transitions in the cleaned-up code. *) - -Lemma cleanup_code_correct_2: - forall f sp c1 ls1 m1 t c2 ls2 m2, - exec_instrs tge f sp c1 ls1 m1 t c2 ls2 m2 -> - is_tail c1 f.(fn_code) -> - unique_labels f.(fn_code) -> - exec_instrs tge (cleanup_function f) sp - (cleanup_code c1) ls1 m1 - t (cleanup_code c2) ls2 m2. -Proof. - induction 1; simpl; intros. - apply exec_refl. - eapply cleanup_code_correct_1; eauto. - apply exec_trans with t1 (cleanup_code b2) rs2 m2 t2. - auto. - apply IHexec_instrs2; auto. - eapply is_tail_exec_instrs; eauto. - auto. -Qed. +(** Connection between [find_label] and linearization. *) -Lemma cleanup_function_correct: - forall f ls1 m1 t ls2 m2, - exec_function tge (Internal f) ls1 m1 t ls2 m2 -> - unique_labels f.(fn_code) -> - exec_function tge (Internal (cleanup_function f)) ls1 m1 t ls2 m2. +Lemma find_label_add_branch: + forall lbl k s, + find_label lbl (add_branch s k) = find_label lbl k. Proof. - intros. inversion H; subst. - generalize (cleanup_code_correct_2 _ _ _ _ _ _ _ _ _ H3 (is_tail_refl _) H0). - simpl. intro. - econstructor; eauto. + intros. unfold add_branch. destruct (starts_with s k); auto. Qed. -(** * Properties of linearized code *) - -(** We now state useful properties of the Linear code generated by - the naive LTL-to-Linear translation. *) - -(** Connection between [find_label] and linearization. *) - -Lemma find_label_lin_block: +Lemma find_label_lin_instr: forall lbl k b, - find_label lbl (linearize_block b k) = find_label lbl k. + find_label lbl (linearize_instr b k) = find_label lbl k. Proof. + intros lbl k. generalize (find_label_add_branch lbl k); intro. induction b; simpl; auto. - case (starts_with n k); reflexivity. + case (starts_with n k); simpl; auto. Qed. Lemma find_label_lin_rec: forall f enum pc b, In pc enum -> f.(LTL.fn_code)!pc = Some b -> - exists k, - find_label pc (linearize_body f enum) = Some (linearize_block b k). + exists k, find_label pc (linearize_body f enum) = Some (linearize_instr b k). Proof. induction enum; intros. elim H. @@ -403,7 +239,7 @@ Proof. assert (In pc enum). simpl in H. tauto. elim (IHenum pc b H1 H0). intros k FIND. exists k. simpl. destruct (LTL.fn_code f)!a. - simpl. rewrite peq_false. rewrite find_label_lin_block. auto. auto. + simpl. rewrite peq_false. rewrite find_label_lin_instr. auto. auto. auto. Qed. @@ -412,20 +248,56 @@ Lemma find_label_lin: f.(LTL.fn_code)!pc = Some b -> (reachable f)!!pc = true -> exists k, - find_label pc (fn_code (linearize_function f)) = Some (linearize_block b k). + find_label pc (fn_code (transf_function f)) = Some (linearize_instr b k). Proof. - intros. unfold linearize_function; simpl. apply find_label_lin_rec. + intros. unfold transf_function; simpl. + rewrite find_label_add_branch. apply find_label_lin_rec. eapply enumerate_complete; eauto. auto. Qed. +Lemma find_label_lin_inv: + forall f pc b k , + f.(LTL.fn_code)!pc = Some b -> + (reachable f)!!pc = true -> + find_label pc (fn_code (transf_function f)) = Some k -> + exists k', k = linearize_instr b k'. +Proof. + intros. exploit find_label_lin; eauto. intros [k' FIND]. + exists k'. congruence. +Qed. + +Lemma find_label_lin_succ: + forall f s, + valid_successor f s -> + (reachable f)!!s = true -> + exists k, + find_label s (fn_code (transf_function f)) = Some k. +Proof. + intros. destruct H as [i AT]. + exploit find_label_lin; eauto. intros [k FIND]. + exists (linearize_instr i k); auto. +Qed. + (** Unique label property for linearized code. *) -Lemma label_in_lin_block: +Lemma label_in_add_branch: + forall lbl s k, + In (Llabel lbl) (add_branch s k) -> In (Llabel lbl) k. +Proof. + intros until k; unfold add_branch. + destruct (starts_with s k); simpl; intuition congruence. +Qed. + +Lemma label_in_lin_instr: forall lbl k b, - In (Llabel lbl) (linearize_block b k) -> In (Llabel lbl) k. + In (Llabel lbl) (linearize_instr b k) -> In (Llabel lbl) k. Proof. - induction b; simpl; try (intuition congruence). - case (starts_with n k); simpl; intuition congruence. + induction b; simpl; intros; + try (apply label_in_add_branch with n; intuition congruence); + try (intuition congruence). + destruct (starts_with n k); simpl in H. + apply label_in_add_branch with n; intuition congruence. + apply label_in_add_branch with n0; intuition congruence. Qed. Lemma label_in_lin_rec: @@ -436,16 +308,24 @@ Proof. simpl; auto. simpl. destruct (LTL.fn_code f)!a. simpl. intros [A|B]. left; congruence. - right. apply IHenum. eapply label_in_lin_block; eauto. + right. apply IHenum. eapply label_in_lin_instr; eauto. intro; right; auto. Qed. -Lemma unique_labels_lin_block: +Lemma unique_labels_add_branch: + forall lbl k, + unique_labels k -> unique_labels (add_branch lbl k). +Proof. + intros; unfold add_branch. + destruct (starts_with lbl k); simpl; intuition. +Qed. + +Lemma unique_labels_lin_instr: forall k b, - unique_labels k -> unique_labels (linearize_block b k). + unique_labels k -> unique_labels (linearize_instr b k). Proof. - induction b; simpl; auto. - case (starts_with n k); simpl; auto. + induction b; intro; simpl; auto; try (apply unique_labels_add_branch; auto). + case (starts_with n k); simpl; apply unique_labels_add_branch; auto. Qed. Lemma unique_labels_lin_rec: @@ -458,268 +338,339 @@ Proof. intro. simpl. destruct (LTL.fn_code f)!a. simpl. split. red. intro. inversion H. elim H3. apply label_in_lin_rec with f. - apply label_in_lin_block with b. auto. - apply unique_labels_lin_block. apply IHenum. inversion H; auto. + apply label_in_lin_instr with i. auto. + apply unique_labels_lin_instr. apply IHenum. inversion H; auto. apply IHenum. inversion H; auto. Qed. -Lemma unique_labels_lin_function: +Lemma unique_labels_transf_function: forall f, - unique_labels (fn_code (linearize_function f)). + unique_labels (fn_code (transf_function f)). Proof. - intros. unfold linearize_function; simpl. + intros. unfold transf_function; simpl. + apply unique_labels_add_branch. apply unique_labels_lin_rec. apply enumerate_norepet. Qed. -(** * Correctness of linearization *) +(** Correctness of [add_branch]. *) + +Lemma is_tail_find_label: + forall lbl c2 c1, + find_label lbl c1 = Some c2 -> is_tail c2 c1. +Proof. + induction c1; simpl. + intros; discriminate. + case (is_label lbl a). intro. injection H; intro. subst c2. + constructor. constructor. + intro. constructor. auto. +Qed. -(** The outcome of an LTL [exec_block] or [exec_blocks] execution - is valid if it corresponds to a reachable, existing basic block. - All outcomes occurring in an LTL program execution are actually - valid, but we will prove that along with the main simulation proof. *) +Lemma is_tail_add_branch: + forall lbl c1 c2, is_tail (add_branch lbl c1) c2 -> is_tail c1 c2. +Proof. + intros until c2. unfold add_branch. destruct (starts_with lbl c1). + auto. eauto with coqlib. +Qed. -Definition valid_outcome (f: LTL.function) (out: outcome) := - match out with - | Cont s => - (reachable f)!!s = true /\ exists b, f.(LTL.fn_code)!s = Some b - | Return => True - end. +Lemma add_branch_correct: + forall lbl c k s f sp ls m, + is_tail k (transf_function f).(fn_code) -> + find_label lbl (transf_function f).(fn_code) = Some c -> + plus step tge (State s (transf_function f) sp (add_branch lbl k) ls m) + E0 (State s (transf_function f) sp c ls m). +Proof. + intros. unfold add_branch. + caseEq (starts_with lbl k); intro SW. + eapply starts_with_correct; eauto. + apply unique_labels_transf_function. + apply plus_one. apply exec_Lgoto. auto. +Qed. -(** Auxiliary lemma used to establish the [valid_outcome] property. *) +(** * Correctness of linearization *) -Lemma exec_blocks_valid_outcome: - forall c sp pc ls1 m1 t out ls2 m2, - exec_blocks ge c sp pc ls1 m1 t out ls2 m2 -> - forall f, - c = f.(LTL.fn_code) -> - (reachable f)!!pc = true -> - valid_outcome f out -> - valid_outcome f (Cont pc). +(** The proof of semantic preservation is a simulation argument + based on diagrams of the following form: +<< + st1 --------------- st2 + | | + t| +|t + | | + v v + st1'--------------- st2' +>> + The invariant (horizontal lines above) is the [match_states] + predicate defined below. It captures the fact that the flow + of data is the same in the source and linearized codes. + Moreover, whenever the source state is at node [pc] in its + control-flow graph, the transformed state is at a code + sequence [c] that starts with the label [pc]. *) + +Inductive match_stackframes: LTL.stackframe -> LTLin.stackframe -> Prop := + | match_stackframe_intro: + forall res f sp pc ls c, + (reachable f)!!pc = true -> + valid_successor f pc -> + is_tail c (fn_code (transf_function f)) -> + wt_function f -> + match_stackframes + (LTL.Stackframe res f sp ls pc) + (LTLin.Stackframe res (transf_function f) sp ls (add_branch pc c)). + +Inductive match_states: LTL.state -> LTLin.state -> Prop := + | match_states_intro: + forall s f sp pc ls m ts c + (STACKS: list_forall2 match_stackframes s ts) + (REACH: (reachable f)!!pc = true) + (AT: find_label pc (fn_code (transf_function f)) = Some c) + (WTF: wt_function f), + match_states (LTL.State s f sp pc ls m) + (LTLin.State ts (transf_function f) sp c ls m) + | match_states_call: + forall s f ls m ts, + list_forall2 match_stackframes s ts -> + wt_fundef f -> + match_states (LTL.Callstate s f ls m) + (LTLin.Callstate ts (transf_fundef f) ls m) + | match_states_return: + forall s sig ls m ts, + list_forall2 match_stackframes s ts -> + match_states (LTL.Returnstate s sig ls m) + (LTLin.Returnstate ts sig ls m). + +Remark parent_locset_match: + forall s ts, + list_forall2 match_stackframes s ts -> + parent_locset ts = LTL.parent_locset s. Proof. - induction 1. - auto. - intros. simpl. split. auto. exists b. congruence. - intros. apply IHexec_blocks1. auto. auto. - apply IHexec_blocks2. auto. - eapply reachable_correct_2. eexact H. auto. auto. auto. - auto. + induction 1; simpl; auto. inv H; auto. Qed. -(** Correspondence between an LTL outcome and a fragment of generated - Linear code. *) - -Inductive cont_for_outcome: LTL.function -> outcome -> code -> Prop := - | co_return: - forall f k, - cont_for_outcome f Return (Lreturn :: k) - | co_goto: - forall f s k, - find_label s (linearize_function f).(fn_code) = Some k -> - cont_for_outcome f (Cont s) k. - -(** The simulation properties used in the inductive proof. - They are parameterized by an LTL execution, and state - that a matching execution is possible in the generated Linear code. *) - -Definition exec_instr_prop - (sp: val) (b1: block) (ls1: locset) (m1: mem) - (t: trace) (b2: block) (ls2: locset) (m2: mem) : Prop := - forall f k, - exec_instr tge (linearize_function f) sp - (linearize_block b1 k) ls1 m1 - t (linearize_block b2 k) ls2 m2. - -Definition exec_instrs_prop - (sp: val) (b1: block) (ls1: locset) (m1: mem) - (t: trace) (b2: block) (ls2: locset) (m2: mem) : Prop := - forall f k, - exec_instrs tge (linearize_function f) sp - (linearize_block b1 k) ls1 m1 - t (linearize_block b2 k) ls2 m2. - -Definition exec_block_prop - (sp: val) (b: block) (ls1: locset) (m1: mem) - (t: trace) (out: outcome) (ls2: locset) (m2: mem): Prop := - forall f k, - valid_outcome f out -> - exists k', - exec_instrs tge (linearize_function f) sp - (linearize_block b k) ls1 m1 - t k' ls2 m2 - /\ cont_for_outcome f out k'. - -Definition exec_blocks_prop - (c: LTL.code) (sp: val) (pc: node) (ls1: locset) (m1: mem) - (t: trace) (out: outcome) (ls2: locset) (m2: mem): Prop := - forall f k, - c = f.(LTL.fn_code) -> - (reachable f)!!pc = true -> - find_label pc (fn_code (linearize_function f)) = Some k -> - valid_outcome f out -> - exists k', - exec_instrs tge (linearize_function f) sp - k ls1 m1 - t k' ls2 m2 - /\ cont_for_outcome f out k'. - -Definition exec_function_prop - (f: LTL.fundef) (ls1: locset) (m1: mem) (t: trace) - (ls2: locset) (m2: mem): Prop := - exec_function tge (transf_fundef f) ls1 m1 t ls2 m2. - -Scheme exec_instr_ind5 := Minimality for LTL.exec_instr Sort Prop - with exec_instrs_ind5 := Minimality for LTL.exec_instrs Sort Prop - with exec_block_ind5 := Minimality for LTL.exec_block Sort Prop - with exec_blocks_ind5 := Minimality for LTL.exec_blocks Sort Prop - with exec_function_ind5 := Minimality for LTL.exec_function Sort Prop. - -(** The obligatory proof by structural induction on the LTL evaluation - derivation. *) - -Lemma transf_function_correct: - forall f ls1 m1 t ls2 m2, - LTL.exec_function ge f ls1 m1 t ls2 m2 -> - exec_function_prop f ls1 m1 t ls2 m2. +Hypothesis wt_prog: wt_program prog. + +Theorem transf_step_correct: + forall s1 t s2, LTL.step ge s1 t s2 -> + forall s1' (MS: match_states s1 s1'), + exists s2', plus LTLin.step tge s1' t s2' /\ match_states s2 s2'. Proof. - apply (exec_function_ind5 ge - exec_instr_prop - exec_instrs_prop - exec_block_prop - exec_blocks_prop - exec_function_prop); - intros; red; intros; simpl. - (* getstack *) - constructor. - (* setstack *) - constructor. - (* op *) - constructor. rewrite <- H. apply eval_operation_preserved. - exact symbols_preserved. - (* load *) - apply exec_Lload with a. - rewrite <- H. apply eval_addressing_preserved. - exact symbols_preserved. - auto. - (* store *) - apply exec_Lstore with a. - rewrite <- H. apply eval_addressing_preserved. - exact symbols_preserved. - auto. - (* call *) - apply exec_Lcall with (transf_fundef f). - generalize H. destruct ros; simpl. - intro; apply functions_translated; auto. - rewrite symbols_preserved. destruct (Genv.find_symbol ge i). - intro; apply function_ptr_translated; auto. congruence. - generalize (sig_preserved f). congruence. - apply H2. - (* alloc *) - eapply exec_Lalloc; eauto. - (* instr_refl *) - apply exec_refl. - (* instr_one *) - apply exec_one. apply H0. - (* instr_trans *) - apply exec_trans with t1 (linearize_block b2 k) rs2 m2 t2. - apply H0. apply H2. auto. - (* goto *) - elim H1. intros REACH [b2 AT2]. - generalize (H0 f k). simpl. intro. - elim (find_label_lin f s b2 AT2 REACH). intros k2 FIND. - exists (linearize_block b2 k2). - split. - eapply exec_trans. eexact H2. constructor. constructor. auto. traceEq. - constructor. auto. - (* cond, true *) - elim H2. intros REACH [b2 AT2]. - elim (find_label_lin f ifso b2 AT2 REACH). intros k2 FIND. - exists (linearize_block b2 k2). - split. - generalize (H0 f k). simpl. - case (starts_with ifso k); intro. - eapply exec_trans. eexact H3. - eapply exec_trans. apply exec_one. apply exec_Lcond_false. - change false with (negb true). apply eval_negate_condition. auto. - apply exec_one. apply exec_Lgoto. auto. reflexivity. traceEq. - eapply exec_trans. eexact H3. - apply exec_one. apply exec_Lcond_true. - auto. auto. traceEq. - constructor; auto. - (* cond, false *) - elim H2. intros REACH [b2 AT2]. - elim (find_label_lin f ifnot b2 AT2 REACH). intros k2 FIND. - exists (linearize_block b2 k2). - split. - generalize (H0 f k). simpl. - case (starts_with ifso k); intro. - eapply exec_trans. eexact H3. - apply exec_one. apply exec_Lcond_true. - change true with (negb false). apply eval_negate_condition. auto. - auto. traceEq. - eapply exec_trans. eexact H3. - eapply exec_trans. apply exec_one. apply exec_Lcond_false. auto. - apply exec_one. apply exec_Lgoto. auto. reflexivity. traceEq. - constructor; auto. - (* return *) - exists (Lreturn :: k). split. - exact (H0 f k). constructor. - (* refl blocks *) - exists k. split. apply exec_refl. constructor. auto. - (* one blocks *) - subst c. elim (find_label_lin f pc b H H3). intros k' FIND. - assert (k = linearize_block b k'). congruence. subst k. - elim (H1 f k' H5). intros k'' [EXEC CFO]. - exists k''. tauto. - (* trans blocks *) - assert ((reachable f)!!pc2 = true). - eapply reachable_correct_2. eexact H. auto. auto. auto. - assert (valid_outcome f (Cont pc2)). - eapply exec_blocks_valid_outcome; eauto. - generalize (H0 f k H4 H5 H6 H9). intros [k1 [EX1 CFO2]]. - inversion CFO2. - generalize (H2 f k1 H4 H8 H12 H7). intros [k2 [EX2 CFO3]]. - exists k2. split. eapply exec_trans; eauto. auto. - (* internal function -- TA-DA! *) - assert (REACH0: (reachable f)!!(fn_entrypoint f) = true). + induction 1; intros; try (inv MS); + try (generalize (wt_instrs _ WTF _ _ H); intro WTI). + (* Lnop *) + destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ]. + simpl in EQ. subst c. + assert (REACH': (reachable f)!!pc' = true). + eapply reachable_successors; eauto. + unfold successors; rewrite H; auto with coqlib. + exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT']. + econstructor; split. + eapply add_branch_correct; eauto. + eapply is_tail_add_branch. eapply is_tail_find_label. eauto. + econstructor; eauto. + (* Lop *) + destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ]. + simpl in EQ. subst c. + assert (REACH': (reachable f)!!pc' = true). + eapply reachable_successors; eauto. + unfold successors; rewrite H; auto with coqlib. + exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT']. + econstructor; split. + eapply plus_left'. + eapply exec_Lop with (v := v); eauto. + rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. + eapply add_branch_correct; eauto. + eapply is_tail_add_branch. eapply is_tail_cons_left. + eapply is_tail_find_label. eauto. + traceEq. + econstructor; eauto. + (* Lload *) + destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ]. + simpl in EQ. subst c. + assert (REACH': (reachable f)!!pc' = true). + eapply reachable_successors; eauto. + unfold successors; rewrite H; auto with coqlib. + exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT']. + econstructor; split. + eapply plus_left'. + eapply exec_Lload; eauto. + rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + eapply add_branch_correct; eauto. + eapply is_tail_add_branch. eapply is_tail_cons_left. + eapply is_tail_find_label. eauto. + traceEq. + econstructor; eauto. + (* Lstore *) + destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ]. + simpl in EQ. subst c. + assert (REACH': (reachable f)!!pc' = true). + eapply reachable_successors; eauto. + unfold successors; rewrite H; auto with coqlib. + exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT']. + econstructor; split. + eapply plus_left'. + eapply exec_Lstore; eauto. + rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. + eapply add_branch_correct; eauto. + eapply is_tail_add_branch. eapply is_tail_cons_left. + eapply is_tail_find_label. eauto. + traceEq. + econstructor; eauto. + (* Lcall *) + unfold rs1 in *. inv MS. fold rs1. + generalize (wt_instrs _ WTF _ _ H); intro WTI. + destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ]. + simpl in EQ. subst c. + assert (REACH': (reachable f)!!pc' = true). + eapply reachable_successors; eauto. + unfold successors; rewrite H; auto with coqlib. + assert (VALID: valid_successor f pc'). inv WTI; auto. + econstructor; split. + apply plus_one. eapply exec_Lcall with (f' := transf_fundef f'); eauto. + apply find_function_translated; auto. + symmetry; apply sig_preserved. + econstructor; eauto. + constructor; auto. econstructor; eauto. + eapply is_tail_add_branch. eapply is_tail_cons_left. + eapply is_tail_find_label. eauto. + destruct ros; simpl in H0. + eapply Genv.find_funct_prop; eauto. + destruct (Genv.find_symbol ge i); try discriminate. + eapply Genv.find_funct_ptr_prop; eauto. + + (* Ltailcall *) + unfold rs2, rs1 in *. inv MS. fold rs1; fold rs2. + destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ]. + simpl in EQ. subst c. + econstructor; split. + apply plus_one. eapply exec_Ltailcall with (f' := transf_fundef f'); eauto. + apply find_function_translated; auto. + symmetry; apply sig_preserved. + rewrite (parent_locset_match _ _ STACKS). + econstructor; eauto. + destruct ros; simpl in H0. + eapply Genv.find_funct_prop; eauto. + destruct (Genv.find_symbol ge i); try discriminate. + eapply Genv.find_funct_ptr_prop; eauto. + + (* Lalloc *) + destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ]. + simpl in EQ. subst c. + assert (REACH': (reachable f)!!pc' = true). + eapply reachable_successors; eauto. + unfold successors; rewrite H; auto with coqlib. + exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT']. + econstructor; split. + eapply plus_left'. + eapply exec_Lalloc; eauto. + eapply add_branch_correct; eauto. + eapply is_tail_add_branch. eapply is_tail_cons_left. + eapply is_tail_find_label. eauto. + traceEq. + econstructor; eauto. + (* Lcond true *) + destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ]. + simpl in EQ. subst c. + assert (REACH': (reachable f)!!ifso = true). + eapply reachable_successors; eauto. + unfold successors; rewrite H; auto with coqlib. + exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT']. + destruct (starts_with ifso c'). + econstructor; split. + eapply plus_left'. + eapply exec_Lcond_false; eauto. + change false with (negb true). apply eval_negate_condition; auto. + eapply add_branch_correct; eauto. + eapply is_tail_add_branch. eapply is_tail_cons_left. + eapply is_tail_find_label. eauto. + traceEq. + econstructor; eauto. + econstructor; split. + apply plus_one. eapply exec_Lcond_true; eauto. + econstructor; eauto. + (* Lcond false *) + destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ]. + simpl in EQ. subst c. + assert (REACH': (reachable f)!!ifnot = true). + eapply reachable_successors; eauto. + unfold successors; rewrite H; auto with coqlib. + exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT']. + destruct (starts_with ifso c'). + econstructor; split. + apply plus_one. eapply exec_Lcond_true; eauto. + change true with (negb false). apply eval_negate_condition; auto. + econstructor; eauto. + econstructor; split. + eapply plus_left'. + eapply exec_Lcond_false; eauto. + eapply add_branch_correct; eauto. + eapply is_tail_add_branch. eapply is_tail_cons_left. + eapply is_tail_find_label. eauto. + traceEq. + econstructor; eauto. + (* Lreturn *) + destruct (find_label_lin_inv _ _ _ _ H REACH AT) as [c' EQ]. + simpl in EQ. subst c. + econstructor; split. + apply plus_one. eapply exec_Lreturn; eauto. + rewrite (parent_locset_match _ _ STACKS). + econstructor; eauto. + (* internal function *) + assert (REACH: (reachable f)!!(LTL.fn_entrypoint f) = true). apply reachable_entrypoint. - assert (VO2: valid_outcome f Return). simpl; auto. - assert (VO1: valid_outcome f (Cont (fn_entrypoint f))). - eapply exec_blocks_valid_outcome; eauto. - assert (exists k, fn_code (linearize_function f) = Llabel f.(fn_entrypoint) :: k). - unfold linearize_function; simpl. - elim (enumerate_head f). intros tl EN. rewrite EN. - simpl. elim VO1. intros REACH [b EQ]. rewrite EQ. - exists (linearize_block b (linearize_body f tl)). auto. - elim H2; intros k EQ. - assert (find_label (fn_entrypoint f) (fn_code (linearize_function f)) = - Some k). - rewrite EQ. simpl. rewrite peq_true. auto. - generalize (H1 f k (refl_equal _) REACH0 H3 VO2). - intros [k' [EX CO]]. - inversion CO. subst k'. - unfold transf_function. apply cleanup_function_correct. - econstructor. eauto. rewrite EQ. eapply exec_trans. - apply exec_one. constructor. eauto. traceEq. - apply unique_labels_lin_function. + inv H6. + exploit find_label_lin_succ; eauto. inv H1; auto. intros [c'' AT']. + simpl. econstructor; split. + eapply plus_left'. + eapply exec_function_internal; eauto. + simpl. eapply add_branch_correct. + simpl. eapply is_tail_add_branch. constructor. eauto. + traceEq. + econstructor; eauto. (* external function *) + simpl. econstructor; split. + apply plus_one. eapply exec_function_external; eauto. + econstructor; eauto. + (* return *) + inv H4. inv H1. + exploit find_label_lin_succ; eauto. intros [c' AT]. + econstructor; split. + eapply plus_left'. + eapply exec_return; eauto. + eapply add_branch_correct; eauto. traceEq. econstructor; eauto. Qed. -End LINEARIZATION. +Lemma transf_initial_states: + forall st1, LTL.initial_state prog st1 -> + exists st2, LTLin.initial_state tprog st2 /\ match_states st1 st2. +Proof. + intros. inversion H. + exists (Callstate nil (transf_fundef f) (Locmap.init Vundef) (Genv.init_mem tprog)); split. + econstructor; eauto. + change (prog_main tprog) with (prog_main prog). + rewrite symbols_preserved. eauto. + apply function_ptr_translated; auto. + rewrite <- H2. apply sig_preserved. + replace (Genv.init_mem tprog) with (Genv.init_mem prog). + constructor. constructor. + eapply Genv.find_funct_ptr_prop; eauto. + symmetry. unfold tprog, transf_program. apply Genv.init_mem_transf. +Qed. + +Lemma transf_final_states: + forall st1 st2 r, + match_states st1 st2 -> LTL.final_state st1 r -> LTLin.final_state st2 r. +Proof. + intros. inv H0. inv H. inv H6. constructor. auto. +Qed. Theorem transf_program_correct: - forall (p: LTL.program) (t: trace) (r: val), - LTL.exec_program p t r -> - Linear.exec_program (transf_program p) t r. + forall (beh: program_behavior), + LTL.exec_program prog beh -> LTLin.exec_program tprog beh. Proof. - intros p t r [b [f [ls [m [FIND1 [FIND2 [SIG [EX RES]]]]]]]]. - red. exists b; exists (transf_fundef f); exists ls; exists m. - split. change (prog_main (transf_program p)) with (prog_main p). - rewrite symbols_preserved; auto. - split. apply function_ptr_translated. auto. - split. generalize (sig_preserved f); congruence. - split. apply transf_function_correct. - unfold transf_program. rewrite Genv.init_mem_transf. auto. - rewrite sig_preserved. exact RES. + unfold LTL.exec_program, exec_program; intros. + eapply simulation_plus_preservation; eauto. + eexact transf_initial_states. + eexact transf_final_states. + eexact transf_step_correct. Qed. +End LINEARIZATION. -- cgit