diff options
Diffstat (limited to 'backend/Linearizeproof.v')
| -rw-r--r-- | backend/Linearizeproof.v | 462 |
1 files changed, 223 insertions, 239 deletions
diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index d368311..2548580 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -12,10 +12,11 @@ (** Correctness proof for code linearization *) +Require Import FSets. Require Import Coqlib. Require Import Maps. Require Import Ordered. -Require Import FSets. +Require Import Lattice. Require Import AST. Require Import Integers. Require Import Values. @@ -27,17 +28,15 @@ Require Import Smallstep. Require Import Op. Require Import Locations. Require Import LTL. -Require Import LTLtyping. -Require Import LTLin. +Require Import Linear. Require Import Linearize. -Require Import Lattice. Module NodesetFacts := FSetFacts.Facts(Nodeset). Section LINEARIZATION. Variable prog: LTL.program. -Variable tprog: LTLin.program. +Variable tprog: Linear.program. Hypothesis TRANSF: transf_program prog = OK tprog. @@ -70,7 +69,7 @@ Proof (Genv.find_var_info_transf_partial transf_fundef _ TRANSF). Lemma sig_preserved: forall f tf, transf_fundef f = OK tf -> - LTLin.funsig tf = LTL.funsig f. + Linear.funsig tf = LTL.funsig f. Proof. unfold transf_fundef, transf_partial_fundef; intros. destruct f. monadInv H. monadInv EQ. reflexivity. @@ -80,7 +79,7 @@ Qed. Lemma stacksize_preserved: forall f tf, transf_function f = OK tf -> - LTLin.fn_stacksize tf = LTL.fn_stacksize f. + Linear.fn_stacksize tf = LTL.fn_stacksize f. Proof. intros. monadInv H. auto. Qed. @@ -117,8 +116,8 @@ Qed. (** The successors of a reachable instruction are reachable. *) Lemma reachable_successors: - forall f pc pc' i, - f.(LTL.fn_code)!pc = Some i -> In pc' (successors_instr i) -> + forall f pc pc' b, + f.(LTL.fn_code)!pc = Some b -> In pc' (successors_block b) -> (reachable f)!!pc = true -> (reachable f)!!pc' = true. Proof. @@ -222,7 +221,7 @@ Qed. (** * Properties related to labels *) -(** If labels are globally unique and the LTLin code [c] contains +(** If labels are globally unique and the Linear code [c] contains a subsequence [Llabel lbl :: c1], then [find_label lbl c] returns [c1]. *) @@ -284,13 +283,13 @@ Proof. intros. unfold add_branch. destruct (starts_with s k); auto. Qed. -Lemma find_label_lin_instr: +Lemma find_label_lin_block: forall lbl k b, - find_label lbl (linearize_instr b k) = find_label lbl k. + find_label lbl (linearize_block 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); simpl; auto. + induction b; simpl; auto. destruct a; simpl; auto. + case (starts_with s1 k); simpl; auto. Qed. Remark linearize_body_cons: @@ -298,7 +297,7 @@ Remark linearize_body_cons: linearize_body f (pc :: enum) = match f.(LTL.fn_code)!pc with | None => linearize_body f enum - | Some b => Llabel pc :: linearize_instr b (linearize_body f enum) + | Some b => Llabel pc :: linearize_block b (linearize_body f enum) end. Proof. intros. unfold linearize_body. rewrite list_fold_right_eq. @@ -309,7 +308,7 @@ 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_instr b k). + exists k, find_label pc (linearize_body f enum) = Some (linearize_block b k). Proof. induction enum; intros. elim H. @@ -320,7 +319,7 @@ Proof. assert (In pc enum). simpl in H. tauto. destruct (IHenum pc b H1 H0) as [k FIND]. exists k. destruct (LTL.fn_code f)!a. - simpl. rewrite peq_false. rewrite find_label_lin_instr. auto. auto. + simpl. rewrite peq_false. rewrite find_label_lin_block. auto. auto. auto. Qed. @@ -330,7 +329,7 @@ Lemma find_label_lin: f.(LTL.fn_code)!pc = Some b -> (reachable f)!!pc = true -> exists k, - find_label pc (fn_code tf) = Some (linearize_instr b k). + find_label pc (fn_code tf) = Some (linearize_block b k). Proof. intros. monadInv H. simpl. rewrite find_label_add_branch. apply find_label_lin_rec. @@ -343,25 +342,12 @@ Lemma find_label_lin_inv: f.(LTL.fn_code)!pc = Some b -> (reachable f)!!pc = true -> find_label pc (fn_code tf) = Some k -> - exists k', k = linearize_instr b k'. + exists k', k = linearize_block b k'. Proof. intros. exploit find_label_lin; eauto. intros [k' FIND]. exists k'. congruence. Qed. -Lemma find_label_lin_succ: - forall f tf s, - transf_function f = OK tf -> - valid_successor f s -> - (reachable f)!!s = true -> - exists k, - find_label s (fn_code tf) = Some k. -Proof. - intros. destruct H0 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_add_branch: @@ -372,16 +358,16 @@ Proof. destruct (starts_with s k); simpl; intuition congruence. Qed. -Lemma label_in_lin_instr: +Lemma label_in_lin_block: forall lbl k b, - In (Llabel lbl) (linearize_instr b k) -> In (Llabel lbl) k. + In (Llabel lbl) (linearize_block b k) -> In (Llabel lbl) k. Proof. - 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. + induction b; simpl; intros. auto. + destruct a; simpl in H; try (intuition congruence). + apply label_in_add_branch with s; intuition congruence. + destruct (starts_with s1 k); simpl in H. + apply label_in_add_branch with s1; intuition congruence. + apply label_in_add_branch with s2; intuition congruence. Qed. Lemma label_in_lin_rec: @@ -392,7 +378,7 @@ Proof. simpl; auto. rewrite linearize_body_cons. destruct (LTL.fn_code f)!a. simpl. intros [A|B]. left; congruence. - right. apply IHenum. eapply label_in_lin_instr; eauto. + right. apply IHenum. eapply label_in_lin_block; eauto. intro; right; auto. Qed. @@ -404,12 +390,13 @@ Proof. destruct (starts_with lbl k); simpl; intuition. Qed. -Lemma unique_labels_lin_instr: +Lemma unique_labels_lin_block: forall k b, - unique_labels k -> unique_labels (linearize_instr b k). + unique_labels k -> unique_labels (linearize_block b k). Proof. - induction b; intro; simpl; auto; try (apply unique_labels_add_branch; auto). - case (starts_with n k); simpl; apply unique_labels_add_branch; auto. + induction b; intros; simpl. auto. + destruct a; auto; try (apply unique_labels_add_branch; auto). + case (starts_with s1 k); simpl; apply unique_labels_add_branch; auto. Qed. Lemma unique_labels_lin_rec: @@ -423,8 +410,8 @@ Proof. intro. 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_instr with i. auto. - apply unique_labels_lin_instr. apply IHenum. inversion H; auto. + apply label_in_lin_block with b. auto. + apply unique_labels_lin_block. apply IHenum. inversion H; auto. apply IHenum. inversion H; auto. Qed. @@ -458,6 +445,17 @@ Proof. auto. eauto with coqlib. Qed. +Lemma is_tail_lin_block: + forall b c1 c2, + is_tail (linearize_block b c1) c2 -> is_tail c1 c2. +Proof. + induction b; simpl; intros. + auto. + destruct a; eauto with coqlib. + eapply is_tail_add_branch; eauto. + destruct (starts_with s1 c1); eapply is_tail_add_branch; eauto with coqlib. +Qed. + Lemma add_branch_correct: forall lbl c k s f tf sp ls m, transf_function f = OK tf -> @@ -475,12 +473,11 @@ Qed. (** * Correctness of linearization *) -(** The proof of semantic preservation is a simulation argument - based on diagrams of the following form: +(** The proof of semantic preservation is a simulation argument of the "star" kind: << st1 --------------- st2 | | - t| +|t + t| t| + or ( 0 \/ |st1'| < |st1| ) | | v v st1'--------------- st2' @@ -492,273 +489,260 @@ Qed. 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 := +Inductive match_stackframes: LTL.stackframe -> Linear.stackframe -> Prop := | match_stackframe_intro: - forall res f sp pc ls tf c, + forall f sp bb ls tf c, transf_function f = OK tf -> - (reachable f)!!pc = true -> - valid_successor f pc -> - is_tail c (fn_code tf) -> - wt_function f -> + (forall pc, In pc (successors_block bb) -> (reachable f)!!pc = true) -> + is_tail c tf.(fn_code) -> match_stackframes - (LTL.Stackframe res f sp ls pc) - (LTLin.Stackframe res tf sp ls (add_branch pc c)). + (LTL.Stackframe f sp ls bb) + (Linear.Stackframe tf sp ls (linearize_block bb c)). -Inductive match_states: LTL.state -> LTLin.state -> Prop := - | match_states_intro: +Inductive match_states: LTL.state -> Linear.state -> Prop := + | match_states_add_branch: forall s f sp pc ls m tf ts c (STACKS: list_forall2 match_stackframes s ts) (TRF: transf_function f = OK tf) (REACH: (reachable f)!!pc = true) - (AT: find_label pc (fn_code tf) = Some c) - (WTF: wt_function f), + (TAIL: is_tail c tf.(fn_code)), match_states (LTL.State s f sp pc ls m) - (LTLin.State ts tf sp c ls m) + (Linear.State ts tf sp (add_branch pc c) ls m) + | match_states_cond_taken: + forall s f sp pc ls m tf ts cond args c + (STACKS: list_forall2 match_stackframes s ts) + (TRF: transf_function f = OK tf) + (REACH: (reachable f)!!pc = true) + (JUMP: eval_condition cond (reglist ls args) m = Some true), + match_states (LTL.State s f sp pc (undef_regs (destroyed_by_cond cond) ls) m) + (Linear.State ts tf sp (Lcond cond args pc :: c) ls m) + | match_states_jumptable: + forall s f sp pc ls m tf ts arg tbl c n + (STACKS: list_forall2 match_stackframes s ts) + (TRF: transf_function f = OK tf) + (REACH: (reachable f)!!pc = true) + (ARG: ls (R arg) = Vint n) + (JUMP: list_nth_z tbl (Int.unsigned n) = Some pc), + match_states (LTL.State s f sp pc (undef_regs destroyed_by_jumptable ls) m) + (Linear.State ts tf sp (Ljumptable arg tbl :: c) ls m) + | match_states_block: + forall s f sp bb ls m tf ts c + (STACKS: list_forall2 match_stackframes s ts) + (TRF: transf_function f = OK tf) + (REACH: forall pc, In pc (successors_block bb) -> (reachable f)!!pc = true) + (TAIL: is_tail c tf.(fn_code)), + match_states (LTL.Block s f sp bb ls m) + (Linear.State ts tf sp (linearize_block bb c) ls m) | match_states_call: forall s f ls m tf ts, list_forall2 match_stackframes s ts -> transf_fundef f = OK tf -> - wt_fundef f -> match_states (LTL.Callstate s f ls m) - (LTLin.Callstate ts tf ls m) + (Linear.Callstate ts tf ls m) | match_states_return: forall s ls m ts, list_forall2 match_stackframes s ts -> match_states (LTL.Returnstate s ls m) - (LTLin.Returnstate ts ls m). + (Linear.Returnstate ts ls m). -Hypothesis wt_prog: wt_program prog. +Definition measure (S: LTL.state) : nat := + match S with + | LTL.State s f sp pc ls m => 0%nat + | LTL.Block s f sp bb ls m => 1%nat + | _ => 0%nat + end. + +Remark match_parent_locset: + forall s ts, list_forall2 match_stackframes s ts -> parent_locset ts = LTL.parent_locset s. +Proof. + induction 1; simpl. auto. inv H; auto. +Qed. 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. - induction 1; intros; try (inv MS); - try (generalize (wt_instrs _ WTF _ _ H); intro WTI). - (* Lnop *) - destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. - simpl in EQ. subst c. - assert (REACH': (reachable f)!!pc' = true). - eapply reachable_successors; eauto. simpl; auto. - 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. + (exists s2', plus Linear.step tge s1' t s2' /\ match_states s2 s2') + \/ (measure s2 < measure s1 /\ t = E0 /\ match_states s2 s1')%nat. +Proof. + induction 1; intros; try (inv MS). + + (* start of block, at an [add_branch] *) + exploit find_label_lin; eauto. intros [k F]. + left; econstructor; split. + eapply add_branch_correct; eauto. + econstructor; eauto. + intros; eapply reachable_successors; eauto. + eapply is_tail_lin_block; eauto. eapply is_tail_find_label; eauto. + + (* start of block, target of an [Lcond] *) + exploit find_label_lin; eauto. intros [k F]. + left; econstructor; split. + apply plus_one. eapply exec_Lcond_true; eauto. + econstructor; eauto. + intros; eapply reachable_successors; eauto. + eapply is_tail_lin_block; eauto. eapply is_tail_find_label; eauto. + + (* start of block, target of an [Ljumptable] *) + exploit find_label_lin; eauto. intros [k F]. + left; econstructor; split. + apply plus_one. eapply exec_Ljumptable; eauto. econstructor; eauto. + intros; eapply reachable_successors; eauto. + eapply is_tail_lin_block; eauto. eapply is_tail_find_label; eauto. + (* Lop *) - destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. - simpl in EQ. subst c. - assert (REACH': (reachable f)!!pc' = true). - eapply reachable_successors; eauto. simpl; auto. - 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. + left; econstructor; split. simpl. + apply plus_one. econstructor; eauto. + instantiate (1 := v); rewrite <- H; apply eval_operation_preserved. + exact symbols_preserved. + econstructor; eauto. + (* Lload *) - destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. - simpl in EQ. subst c. - assert (REACH': (reachable f)!!pc' = true). - eapply reachable_successors; eauto. simpl; auto. - exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT']. - econstructor; split. - eapply plus_left'. - apply exec_Lload with a. - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. - eauto. - eapply add_branch_correct; eauto. - eapply is_tail_add_branch. eapply is_tail_cons_left. - eapply is_tail_find_label. eauto. - traceEq. + left; econstructor; split. simpl. + apply plus_one. econstructor. + instantiate (1 := a). rewrite <- H; apply eval_addressing_preserved. + exact symbols_preserved. eauto. eauto. + econstructor; eauto. + + (* Lgetstack *) + left; econstructor; split. simpl. + apply plus_one. econstructor; eauto. + econstructor; eauto. + + (* Lsetstack *) + left; econstructor; split. simpl. + apply plus_one. econstructor; eauto. econstructor; eauto. + (* Lstore *) - destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. - simpl in EQ. subst c. - assert (REACH': (reachable f)!!pc' = true). - eapply reachable_successors; eauto. simpl; auto. - exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT']. - econstructor; split. - eapply plus_left'. - apply exec_Lstore with a. - rewrite <- H0. apply eval_addressing_preserved. exact symbols_preserved. - eauto. - eapply add_branch_correct; eauto. - eapply is_tail_add_branch. eapply is_tail_cons_left. - eapply is_tail_find_label. eauto. - traceEq. + left; econstructor; split. simpl. + apply plus_one. econstructor. + instantiate (1 := a). rewrite <- H; apply eval_addressing_preserved. + exact symbols_preserved. eauto. eauto. econstructor; eauto. + (* Lcall *) - destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. - simpl in EQ. subst c. - assert (REACH': (reachable f)!!pc' = true). - eapply reachable_successors; eauto. simpl; auto. - assert (VALID: valid_successor f pc'). inv WTI; auto. - exploit find_function_translated; eauto. intros [tf' [A B]]. - econstructor; split. - apply plus_one. eapply exec_Lcall with (f' := tf'); eauto. - symmetry; apply sig_preserved; auto. - 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. + exploit find_function_translated; eauto. intros [tfd [A B]]. + left; econstructor; split. simpl. + apply plus_one. econstructor; eauto. + symmetry; eapply sig_preserved; eauto. + econstructor; eauto. constructor; auto. econstructor; eauto. (* Ltailcall *) - destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. - simpl in EQ. subst c. - exploit find_function_translated; eauto. intros [tf' [A B]]. - econstructor; split. - apply plus_one. eapply exec_Ltailcall with (f' := tf'); eauto. - symmetry; apply sig_preserved; auto. - rewrite (stacksize_preserved _ _ TRF). eauto. + exploit find_function_translated; eauto. intros [tfd [A B]]. + left; econstructor; split. simpl. + apply plus_one. econstructor; eauto. + rewrite (match_parent_locset _ _ STACKS). eauto. + symmetry; eapply sig_preserved; eauto. + rewrite (stacksize_preserved _ _ TRF); eauto. + rewrite (match_parent_locset _ _ 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. (* Lbuiltin *) - destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. - simpl in EQ. subst c. - assert (REACH': (reachable f)!!pc' = true). - eapply reachable_successors; eauto. simpl; auto. - exploit find_label_lin_succ; eauto. inv WTI; auto. intros [c'' AT']. - econstructor; split. - eapply plus_left'. - eapply exec_Lbuiltin. - eapply external_call_symbols_preserved; eauto. + left; econstructor; split. simpl. + apply plus_one. eapply exec_Lbuiltin; eauto. + eapply external_call_symbols_preserved'; eauto. + exact symbols_preserved. exact varinfo_preserved. + econstructor; eauto. + + (* Lannot *) + left; econstructor; split. simpl. + apply plus_one. eapply exec_Lannot; eauto. + eapply external_call_symbols_preserved'; eauto. exact symbols_preserved. exact varinfo_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. + (* Lbranch *) + assert ((reachable f)!!pc = true). apply REACH; simpl; auto. + right; split. simpl; omega. split. auto. simpl. econstructor; eauto. + (* Lcond *) - destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. - simpl in EQ. subst c. + assert (REACH1: (reachable f)!!pc1 = true) by (apply REACH; simpl; auto). + assert (REACH2: (reachable f)!!pc2 = true) by (apply REACH; simpl; auto). + simpl linearize_block. + destruct (starts_with pc1 c). + (* branch if cond is false *) + assert (DC: destroyed_by_cond (negate_condition cond) = destroyed_by_cond cond). + destruct cond; reflexivity. destruct b. - (* true *) - assert (REACH': (reachable f)!!ifso = true). - eapply reachable_successors; eauto. simpl; auto. - exploit find_label_lin_succ; eauto. inv WTI; eauto. intros [c'' AT']. - destruct (starts_with ifso c'). - econstructor; split. - eapply plus_left'. - eapply exec_Lcond_false; eauto. - rewrite eval_negate_condition; rewrite H0; 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. - (* false *) - assert (REACH': (reachable f)!!ifnot = true). - eapply reachable_successors; eauto. simpl; auto. - 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. - rewrite eval_negate_condition; rewrite H0; 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. + (* cond is true: no branch *) + left; econstructor; split. + apply plus_one. eapply exec_Lcond_false. + rewrite eval_negate_condition. rewrite H. auto. eauto. + rewrite DC. econstructor; eauto. + (* cond is false: branch is taken *) + right; split. simpl; omega. split. auto. rewrite <- DC. econstructor; eauto. + rewrite eval_negate_condition. rewrite H. auto. + (* branch if cond is true *) + destruct b. + (* cond is true: branch is taken *) + right; split. simpl; omega. split. auto. econstructor; eauto. + (* cond is false: no branch *) + left; econstructor; split. + apply plus_one. eapply exec_Lcond_false. eauto. eauto. econstructor; eauto. (* Ljumptable *) - destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. - simpl in EQ. subst c. - assert (REACH': (reachable f)!!pc' = true). - eapply reachable_successors; eauto. simpl. eapply list_nth_z_in; eauto. - exploit find_label_lin_succ; eauto. - inv WTI. apply H6. eapply list_nth_z_in; eauto. - intros [c'' AT']. - econstructor; split. - apply plus_one. eapply exec_Ljumptable; eauto. - econstructor; eauto. + assert (REACH': (reachable f)!!pc = true). + apply REACH. simpl. eapply list_nth_z_in; eauto. + right; split. simpl; omega. split. auto. econstructor; eauto. (* Lreturn *) - destruct (find_label_lin_inv _ _ _ _ _ TRF H REACH AT) as [c' EQ]. - simpl in EQ. subst c. - econstructor; split. - apply plus_one. eapply exec_Lreturn; eauto. + left; econstructor; split. + simpl. apply plus_one. econstructor; eauto. rewrite (stacksize_preserved _ _ TRF). eauto. - econstructor; eauto. - - (* internal function *) + rewrite (match_parent_locset _ _ STACKS). econstructor; eauto. + + (* internal functions *) assert (REACH: (reachable f)!!(LTL.fn_entrypoint f) = true). apply reachable_entrypoint. - inv H7. monadInv H6. - exploit find_label_lin_succ; eauto. inv H1; auto. intros [c'' AT']. - generalize EQ; intro. monadInv EQ0. econstructor; simpl; split. - eapply plus_left'. - eapply exec_function_internal; eauto. - simpl. eapply add_branch_correct. eauto. - simpl. eapply is_tail_add_branch. constructor. eauto. - traceEq. - econstructor; eauto. + monadInv H7. + left; econstructor; split. + apply plus_one. eapply exec_function_internal; eauto. + rewrite (stacksize_preserved _ _ EQ). eauto. + generalize EQ; intro EQ'; monadInv EQ'. simpl. + econstructor; eauto. simpl. eapply is_tail_add_branch. constructor. (* external function *) - monadInv H6. econstructor; split. + monadInv H8. left; econstructor; split. apply plus_one. eapply exec_function_external; eauto. - eapply external_call_symbols_preserved; eauto. + eapply external_call_symbols_preserved'; eauto. exact symbols_preserved. exact varinfo_preserved. econstructor; eauto. (* return *) inv H3. 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. + left; econstructor; split. + apply plus_one. econstructor. + econstructor; eauto. Qed. Lemma transf_initial_states: forall st1, LTL.initial_state prog st1 -> - exists st2, LTLin.initial_state tprog st2 /\ match_states st1 st2. + exists st2, Linear.initial_state tprog st2 /\ match_states st1 st2. Proof. intros. inversion H. exploit function_ptr_translated; eauto. intros [tf [A B]]. - exists (Callstate nil tf nil m0); split. + exists (Callstate nil tf (Locmap.init Vundef) m0); split. econstructor; eauto. eapply Genv.init_mem_transf_partial; eauto. replace (prog_main tprog) with (prog_main prog). rewrite symbols_preserved. eauto. symmetry. apply (transform_partial_program_main transf_fundef _ TRANSF). rewrite <- H3. apply sig_preserved. auto. constructor. constructor. auto. - eapply Genv.find_funct_ptr_prop; eauto. Qed. Lemma transf_final_states: forall st1 st2 r, - match_states st1 st2 -> LTL.final_state st1 r -> LTLin.final_state st2 r. + match_states st1 st2 -> LTL.final_state st1 r -> Linear.final_state st2 r. Proof. - intros. inv H0. inv H. inv H4. constructor. + intros. inv H0. inv H. inv H6. econstructor; eauto. Qed. Theorem transf_program_correct: - forward_simulation (LTL.semantics prog) (LTLin.semantics tprog). + forward_simulation (LTL.semantics prog) (Linear.semantics tprog). Proof. - eapply forward_simulation_plus. + eapply forward_simulation_star. eexact symbols_preserved. eexact transf_initial_states. eexact transf_final_states. |