diff options
Diffstat (limited to 'backend')
| -rw-r--r-- | backend/Allocproof.v | 2 | ||||
| -rw-r--r-- | backend/CSEproof.v | 2 | ||||
| -rw-r--r-- | backend/Linearizeproof.v | 2 | ||||
| -rw-r--r-- | backend/Machabstr2concr.v | 6 | ||||
| -rw-r--r-- | backend/RTLgenproof.v | 2 | ||||
| -rw-r--r-- | backend/Reloadproof.v | 2 | ||||
| -rw-r--r-- | backend/Stackingproof.v | 2 | ||||
| -rw-r--r-- | backend/Tailcallproof.v | 2 | ||||
| -rw-r--r-- | backend/Tunneling.v | 51 | ||||
| -rw-r--r-- | backend/Tunnelingproof.v | 221 | ||||
| -rw-r--r-- | backend/Tunnelingtyping.v | 40 |
11 files changed, 167 insertions, 165 deletions
diff --git a/backend/Allocproof.v b/backend/Allocproof.v index e2387b5d..7e9334a8 100644 --- a/backend/Allocproof.v +++ b/backend/Allocproof.v @@ -750,7 +750,7 @@ Proof. Qed. Theorem transf_program_correct: - forall (beh: program_behavior), + forall (beh: program_behavior), not_wrong beh -> RTL.exec_program prog beh -> LTL.exec_program tprog beh. Proof. unfold RTL.exec_program, LTL.exec_program; intros. diff --git a/backend/CSEproof.v b/backend/CSEproof.v index 265bb20a..3751cec7 100644 --- a/backend/CSEproof.v +++ b/backend/CSEproof.v @@ -973,7 +973,7 @@ Proof. Qed. Theorem transf_program_correct: - forall (beh: program_behavior), + forall (beh: program_behavior), not_wrong beh -> exec_program prog beh -> exec_program tprog beh. Proof. unfold exec_program; intros. diff --git a/backend/Linearizeproof.v b/backend/Linearizeproof.v index c24d3704..1fb068d8 100644 --- a/backend/Linearizeproof.v +++ b/backend/Linearizeproof.v @@ -707,7 +707,7 @@ Proof. Qed. Theorem transf_program_correct: - forall (beh: program_behavior), + forall (beh: program_behavior), not_wrong beh -> LTL.exec_program prog beh -> LTLin.exec_program tprog beh. Proof. unfold LTL.exec_program, exec_program; intros. diff --git a/backend/Machabstr2concr.v b/backend/Machabstr2concr.v index 6e331f30..139eac75 100644 --- a/backend/Machabstr2concr.v +++ b/backend/Machabstr2concr.v @@ -905,7 +905,7 @@ Proof. Qed. Theorem exec_program_equiv: - forall (beh: program_behavior), + forall (beh: program_behavior), not_wrong beh -> Machabstr.exec_program p beh -> Machconcr.exec_program p beh. Proof. unfold Machconcr.exec_program, Machabstr.exec_program; intros. @@ -915,10 +915,10 @@ Proof. (match_states := fun st1 st2 => match_states st1 st2 /\ wt_state st1). eexact equiv_initial_states. eexact equiv_final_states. - intros. destruct H1. exploit step_equiv; eauto. + intros. destruct H2. exploit step_equiv; eauto. intros [st2' [A B]]. exists st2'; split. auto. split. auto. eapply Machtyping.subject_reduction; eauto. - auto. + auto. auto. Qed. End SIMULATION. diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 1dd2294c..df1ade9d 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -1289,7 +1289,7 @@ Proof. Qed. Theorem transf_program_correct: - forall (beh: program_behavior), + forall (beh: program_behavior), not_wrong beh -> CminorSel.exec_program prog beh -> RTL.exec_program tprog beh. Proof. unfold CminorSel.exec_program, RTL.exec_program; intros. diff --git a/backend/Reloadproof.v b/backend/Reloadproof.v index ea7c5d19..a7becc36 100644 --- a/backend/Reloadproof.v +++ b/backend/Reloadproof.v @@ -1345,7 +1345,7 @@ Proof. Qed. Theorem transf_program_correct: - forall (beh: program_behavior), + forall (beh: program_behavior), not_wrong beh -> LTLin.exec_program prog beh -> Linear.exec_program tprog beh. Proof. unfold LTLin.exec_program, Linear.exec_program; intros. diff --git a/backend/Stackingproof.v b/backend/Stackingproof.v index d5819f7e..5b6f2dc7 100644 --- a/backend/Stackingproof.v +++ b/backend/Stackingproof.v @@ -1592,7 +1592,7 @@ Proof. Qed. Theorem transf_program_correct: - forall (beh: program_behavior), + forall (beh: program_behavior), not_wrong beh -> Linear.exec_program prog beh -> Machabstr.exec_program tprog beh. Proof. unfold Linear.exec_program, Machabstr.exec_program; intros. diff --git a/backend/Tailcallproof.v b/backend/Tailcallproof.v index 791db374..1423e1e0 100644 --- a/backend/Tailcallproof.v +++ b/backend/Tailcallproof.v @@ -722,7 +722,7 @@ Qed. [Smallstep.simulation_opt_preservation]. *) Theorem transf_program_correct: - forall (beh: program_behavior), + forall (beh: program_behavior), not_wrong beh -> exec_program prog beh -> exec_program tprog beh. Proof. unfold exec_program; intros. diff --git a/backend/Tunneling.v b/backend/Tunneling.v index 32d1b595..4b1417fc 100644 --- a/backend/Tunneling.v +++ b/backend/Tunneling.v @@ -14,6 +14,7 @@ Require Import Coqlib. Require Import Maps. +Require Import UnionFind. Require Import AST. Require Import Values. Require Import Globalenvs. @@ -42,9 +43,6 @@ Require Import LTL. dead code (as the "goto L3" in the example above). *) -Definition is_goto_instr (b: option instruction) : option node := - match b with Some (Lnop s) => Some s | _ => None end. - (** [branch_target f pc] returns the node of the CFG that is at the end of the branch sequence starting at [pc]. If the instruction at [pc] is not a [goto], [pc] itself is returned. @@ -77,50 +75,44 @@ Definition is_goto_instr (b: option instruction) : option node := is simpler if we return the label of the first [goto] in the sequence. *) -Fixpoint branch_target_rec (f: LTL.function) (pc: node) (count: nat) - {struct count} : option node := - match count with - | Datatypes.O => None - | Datatypes.S count' => - match is_goto_instr f.(fn_code)!pc with - | Some s => branch_target_rec f s count' - | None => Some pc - end - end. +Module U := UnionFind.UF(PTree). -Definition branch_target (f: LTL.function) (pc: node) := - match branch_target_rec f pc 10%nat with - | Some pc' => pc' - | None => pc +Definition record_goto (uf: U.t) (pc: node) (i: instruction) : U.t := + match i with + | Lnop s => U.union uf pc s + | _ => uf end. +Definition record_gotos (f: LTL.function) : U.t := + PTree.fold record_goto f.(fn_code) U.empty. + (** The tunneling optimization simply rewrites all LTL basic blocks, replacing the destinations of the [Bgoto] and [Bcond] instructions with their final target, as computed by [branch_target]. *) -Definition tunnel_instr (f: LTL.function) (b: instruction) : instruction := +Definition tunnel_instr (uf: U.t) (b: instruction) : instruction := match b with | Lnop s => - Lnop (branch_target f s) + Lnop (U.repr uf s) | Lop op args res s => - Lop op args res (branch_target f s) + Lop op args res (U.repr uf s) | Lload chunk addr args dst s => - Lload chunk addr args dst (branch_target f s) + Lload chunk addr args dst (U.repr uf s) | Lstore chunk addr args src s => - Lstore chunk addr args src (branch_target f s) + Lstore chunk addr args src (U.repr uf s) | Lcall sig ros args res s => - Lcall sig ros args res (branch_target f s) + Lcall sig ros args res (U.repr uf s) | Ltailcall sig ros args => Ltailcall sig ros args | Lcond cond args s1 s2 => - Lcond cond args (branch_target f s1) (branch_target f s2) + Lcond cond args (U.repr uf s1) (U.repr uf s2) | Lreturn or => Lreturn or end. Lemma wf_tunneled_code: - forall (f: LTL.function), - let tc := PTree.map (fun pc b => tunnel_instr f b) (fn_code f) in + forall (f: LTL.function) (uf: U.t), + let tc := PTree.map (fun pc b => tunnel_instr uf b) (fn_code f) in forall (pc: node), Plt pc (fn_nextpc f) \/ tc!pc = None. Proof. intros. elim (fn_code_wf f pc); intro. @@ -129,14 +121,15 @@ Proof. Qed. Definition tunnel_function (f: LTL.function) : LTL.function := + let uf := record_gotos f in mkfunction (fn_sig f) (fn_params f) (fn_stacksize f) - (PTree.map (fun pc b => tunnel_instr f b) (fn_code f)) - (branch_target f (fn_entrypoint f)) + (PTree.map (fun pc b => tunnel_instr uf b) (fn_code f)) + (U.repr uf (fn_entrypoint f)) (fn_nextpc f) - (wf_tunneled_code f). + (wf_tunneled_code f uf). Definition tunnel_fundef (f: LTL.fundef) : LTL.fundef := transf_fundef tunnel_function f. diff --git a/backend/Tunnelingproof.v b/backend/Tunnelingproof.v index 08f5f6cc..eccb62dd 100644 --- a/backend/Tunnelingproof.v +++ b/backend/Tunnelingproof.v @@ -14,6 +14,7 @@ Require Import Coqlib. Require Import Maps. +Require Import UnionFind. Require Import AST. Require Import Values. Require Import Mem. @@ -25,98 +26,112 @@ Require Import Locations. Require Import LTL. Require Import Tunneling. -(** * Properties of branch target computation *) +(** * Properties of the branch map computed using union-find. *) -Lemma is_goto_instr_correct: - forall b s, - is_goto_instr b = Some s -> b = Some (Lnop s). -Proof. - unfold is_goto_instr; intros. - destruct b; try discriminate. - destruct i; discriminate || congruence. -Qed. - -Lemma branch_target_rec_1: - forall f pc n, - branch_target_rec f pc n = Some pc - \/ branch_target_rec f pc n = None - \/ exists pc', f.(fn_code)!pc = Some(Lnop pc'). -Proof. - intros. destruct n; simpl. - right; left; auto. - caseEq (is_goto_instr f.(fn_code)!pc); intros. - right; right. exists n0. apply is_goto_instr_correct; auto. - left; auto. -Qed. +(** A variant of [record_goto] that also incrementally computes a measure [f: node -> nat] + counting the number of [Lnop] instructions starting at a given [pc] that were eliminated. *) -Lemma branch_target_rec_2: - forall f n pc1 pc2 pc3, - f.(fn_code)!pc1 = Some (Lnop pc2) -> - branch_target_rec f pc1 n = Some pc3 -> - branch_target_rec f pc2 n = Some pc3. +Definition measure_edge (u: U.t) (pc s: node) (f: node -> nat) : node -> nat := + fun x => if peq (U.repr u s) pc then f x + else if peq (U.repr u x) pc then (f x + f s + 1)%nat + else f x. + +Definition record_goto' (uf: U.t * (node -> nat)) (pc: node) (i: instruction) : U.t * (node -> nat) := + match i with + | Lnop s => let (u, f) := uf in (U.union u pc s, measure_edge u pc s f) + | _ => uf + end. + +Definition branch_map_correct (c: code) (uf: U.t * (node -> nat)): Prop := + forall pc, + match c!pc with + | Some(Lnop s) => + U.repr (fst uf) pc = pc \/ (U.repr (fst uf) pc = U.repr (fst uf) s /\ snd uf s < snd uf pc)%nat + | _ => + U.repr (fst uf) pc = pc + end. + +Lemma record_gotos'_correct: + forall c, + branch_map_correct c (PTree.fold record_goto' c (U.empty, fun (x: node) => O)). Proof. - induction n. - simpl. intros; discriminate. - intros pc1 pc2 pc3 ATpc1 H. simpl in H. - unfold is_goto_instr in H; rewrite ATpc1 in H. - simpl. caseEq (is_goto_instr f.(fn_code)!pc2); intros. - apply IHn with pc2. apply is_goto_instr_correct; auto. auto. - destruct n; simpl in H. discriminate. rewrite H0 in H. auto. + intros. + apply PTree_Properties.fold_rec with (P := fun c uf => branch_map_correct c uf). + +(* extensionality *) + intros. red; intros. rewrite <- H. apply H0. + +(* base case *) + red; intros; simpl. rewrite PTree.gempty. apply U.repr_empty. + +(* inductive case *) + intros m uf pc i; intros. destruct uf as [u f]. + assert (PC: U.repr u pc = pc). + generalize (H1 pc). rewrite H. auto. + assert (record_goto' (u, f) pc i = (u, f) + \/ exists s, i = Lnop s /\ record_goto' (u, f) pc i = (U.union u pc s, measure_edge u pc s f)). + unfold record_goto'; simpl. destruct i; auto. right. exists n; auto. + destruct H2 as [B | [s [EQ B]]]. + +(* u and f are unchanged *) + rewrite B. + red. intro pc'. simpl. rewrite PTree.gsspec. destruct (peq pc' pc). subst pc'. + destruct i; auto. + apply H1. + +(* i is Lnop s, u becomes union u pc s, f becomes measure_edge u pc s f *) + rewrite B. + red. intro pc'. simpl. rewrite PTree.gsspec. destruct (peq pc' pc). subst pc'. rewrite EQ. + +(* The new instruction *) + rewrite (U.repr_union_2 u pc s); auto. rewrite U.repr_union_3. + unfold measure_edge. destruct (peq (U.repr u s) pc). auto. right. split. auto. + rewrite PC. rewrite peq_true. omega. + +(* An old instruction *) + assert (U.repr u pc' = pc' -> U.repr (U.union u pc s) pc' = pc'). + intro. rewrite <- H2 at 2. apply U.repr_union_1. congruence. + generalize (H1 pc'). simpl. destruct (m!pc'); auto. destruct i0; auto. + intros [P | [P Q]]. left; auto. right. + split. apply U.sameclass_union_2. auto. + unfold measure_edge. destruct (peq (U.repr u s) pc). auto. + rewrite P. destruct (peq (U.repr u n0) pc). omega. auto. Qed. -(** Counting the number of consecutive gotos. *) - -Fixpoint count_goto_rec (f: LTL.function) (pc: node) (count: nat) - {struct count} : nat := - match count with - | Datatypes.O => Datatypes.O - | Datatypes.S count' => - match is_goto_instr f.(fn_code)!pc with - | Some s => Datatypes.S (count_goto_rec f s count') - | None => Datatypes.O - end - end. - -Definition count_goto (f: LTL.function) (pc: node) : nat := - count_goto_rec f pc 10%nat. - -Lemma count_goto_rec_prop: - forall f n pc1 pc2 pc3, - f.(fn_code)!pc1 = Some (Lnop pc2) -> - branch_target_rec f pc1 n = Some pc3 -> - (count_goto_rec f pc2 n < count_goto_rec f pc1 n)%nat. +Definition record_gotos' (f: function) := + PTree.fold record_goto' f.(fn_code) (U.empty, fun (x: node) => O). + +Lemma record_gotos_gotos': + forall f, fst (record_gotos' f) = record_gotos f. Proof. - induction n. - simpl; intros. discriminate. - intros pc1 pc2 pc3 ATpc1 H. simpl in H. - unfold is_goto_instr in H; rewrite ATpc1 in H. - simpl. unfold is_goto_instr at 2. rewrite ATpc1. - caseEq (is_goto_instr f.(fn_code)!pc2); intros. - exploit (IHn pc2); eauto. apply is_goto_instr_correct; eauto. - omega. - omega. + intros. unfold record_gotos', record_gotos. + repeat rewrite PTree.fold_spec. + generalize (PTree.elements (fn_code f)) (U.empty) (fun _ : node => O). + induction l; intros; simpl. + auto. + unfold record_goto' at 2. unfold record_goto at 2. + destruct (snd a); apply IHl. Qed. -(** The following lemma captures the property of [branch_target] - on which the proof of semantic preservation relies. *) +Definition branch_target (f: function) (pc: node) : node := + U.repr (record_gotos f) pc. -Lemma branch_target_characterization: +Definition count_gotos (f: function) (pc: node) : nat := + snd (record_gotos' f) pc. + +Theorem record_gotos_correct: forall f pc, - branch_target f pc = pc \/ - (exists pc', f.(fn_code)!pc = Some(Lnop pc') - /\ branch_target f pc' = branch_target f pc - /\ count_goto f pc' < count_goto f pc)%nat. + match f.(fn_code)!pc with + | Some(Lnop s) => + branch_target f pc = pc \/ + (branch_target f pc = branch_target f s /\ count_gotos f s < count_gotos f pc)%nat + | _ => branch_target f pc = pc + end. Proof. - intros. unfold branch_target. - generalize (branch_target_rec_1 f pc 10%nat). - intros [A|[A|[pc' AT]]]. - rewrite A. left; auto. - rewrite A. left; auto. - caseEq (branch_target_rec f pc 10%nat). intros pcx BT. - right. exists pc'. split. auto. - split. rewrite (branch_target_rec_2 _ _ _ _ _ AT BT). auto. - unfold count_goto. eapply count_goto_rec_prop; eauto. - intro. left; auto. + intros. + generalize (record_gotos'_correct f.(fn_code) pc). simpl. + fold (record_gotos' f). unfold branch_map_correct, branch_target, count_gotos. + rewrite record_gotos_gotos'. auto. Qed. (** * Preservation of semantics *) @@ -186,7 +201,7 @@ Qed. original and transformed codes. *) Definition tunneled_code (f: function) := - PTree.map (fun pc b => tunnel_instr f b) (fn_code f). + PTree.map (fun pc b => tunnel_instr (record_gotos f) b) (fn_code f). Inductive match_stackframes: stackframe -> stackframe -> Prop := | match_stackframes_intro: @@ -219,25 +234,15 @@ Inductive match_states: state -> state -> Prop := Definition measure (st: state) : nat := match st with - | State s f sp pc ls m => count_goto f pc + | State s f sp pc ls m => count_gotos f pc | Callstate s f ls m => 0%nat | Returnstate s ls m => 0%nat end. -Lemma branch_target_identity: - forall f pc, - match f.(fn_code)!pc with Some(Lnop _) => False | _ => True end -> - branch_target f pc = pc. -Proof. - intros. - destruct (branch_target_characterization f pc) as [A | [pc' [B C]]]. - auto. rewrite B in H. contradiction. -Qed. - Lemma tunnel_function_lookup: forall f pc i, f.(fn_code)!pc = Some i -> - (tunnel_function f).(fn_code)!pc = Some (tunnel_instr f i). + (tunnel_function f).(fn_code)!pc = Some (tunnel_instr (record_gotos f) i). Proof. intros. simpl. rewrite PTree.gmap. rewrite H. auto. Qed. @@ -250,23 +255,23 @@ Lemma tunnel_step_correct: Proof. induction 1; intros; try inv MS. (* Lnop *) - destruct (branch_target_characterization f pc) as [A | [pc1 [B [C D]]]]. + generalize (record_gotos_correct f pc); rewrite H. + intros [A | [B C]]. left; econstructor; split. eapply exec_Lnop. rewrite A. rewrite (tunnel_function_lookup _ _ _ H); simpl; auto. econstructor; eauto. - assert (pc1 = pc') by congruence. subst pc1. right. split. simpl. auto. split. auto. - rewrite <- C. econstructor; eauto. + rewrite B. econstructor; eauto. (* Lop *) - rewrite (branch_target_identity f pc); [idtac | rewrite H; auto]. + generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A. left; econstructor; split. eapply exec_Lop with (v := v); eauto. rewrite (tunnel_function_lookup _ _ _ H); simpl; auto. rewrite <- H0. apply eval_operation_preserved. exact symbols_preserved. econstructor; eauto. (* Lload *) - rewrite (branch_target_identity f pc); [idtac | rewrite H; auto]. + generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A. left; econstructor; split. eapply exec_Lload with (a := a). rewrite (tunnel_function_lookup _ _ _ H); simpl; auto. @@ -274,7 +279,7 @@ Proof. eauto. econstructor; eauto. (* Lstore *) - rewrite (branch_target_identity f pc); [idtac | rewrite H; auto]. + generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A. left; econstructor; split. eapply exec_Lstore with (a := a). rewrite (tunnel_function_lookup _ _ _ H); simpl; auto. @@ -282,36 +287,36 @@ Proof. eauto. econstructor; eauto. (* Lcall *) + generalize (record_gotos_correct f pc); rewrite H; intro A. left; econstructor; split. eapply exec_Lcall with (f' := tunnel_fundef f'); eauto. - rewrite (branch_target_identity f pc); [idtac | rewrite H; auto]. - rewrite (tunnel_function_lookup _ _ _ H); simpl. + rewrite A. rewrite (tunnel_function_lookup _ _ _ H); simpl. rewrite sig_preserved. auto. apply find_function_translated; auto. econstructor; eauto. constructor; auto. constructor; auto. (* Ltailcall *) + generalize (record_gotos_correct f pc); rewrite H; intro A. left; econstructor; split. eapply exec_Ltailcall with (f' := tunnel_fundef f'); eauto. - rewrite (branch_target_identity f pc); [idtac | rewrite H; auto]. - rewrite (tunnel_function_lookup _ _ _ H); simpl. + rewrite A. rewrite (tunnel_function_lookup _ _ _ H); simpl. rewrite sig_preserved. auto. apply find_function_translated; auto. econstructor; eauto. (* cond *) - rewrite (branch_target_identity f pc); [idtac | rewrite H; auto]. + generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A. left; econstructor; split. eapply exec_Lcond_true; eauto. rewrite (tunnel_function_lookup _ _ _ H); simpl; eauto. econstructor; eauto. - rewrite (branch_target_identity f pc); [idtac | rewrite H; auto]. + generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A. left; econstructor; split. eapply exec_Lcond_false; eauto. rewrite (tunnel_function_lookup _ _ _ H); simpl; eauto. econstructor; eauto. (* return *) - rewrite (branch_target_identity f pc); [idtac | rewrite H; auto]. + generalize (record_gotos_correct f pc); rewrite H; intro A; rewrite A. left; econstructor; split. eapply exec_Lreturn; eauto. rewrite (tunnel_function_lookup _ _ _ H); simpl; eauto. @@ -355,7 +360,7 @@ Proof. Qed. Theorem transf_program_correct: - forall (beh: program_behavior), + forall (beh: program_behavior), not_wrong beh -> exec_program p beh -> exec_program tp beh. Proof. unfold exec_program; intros. diff --git a/backend/Tunnelingtyping.v b/backend/Tunnelingtyping.v index 57e1271d..91745dfb 100644 --- a/backend/Tunnelingtyping.v +++ b/backend/Tunnelingtyping.v @@ -14,6 +14,7 @@ Require Import Coqlib. Require Import Maps. +Require Import UnionFind. Require Import AST. Require Import Values. Require Import Mem. @@ -27,20 +28,26 @@ Require Import Tunnelingproof. (** Tunneling preserves typing. *) -Lemma branch_target_rec_valid: - forall f, wt_function f -> - forall count pc pc', - branch_target_rec f pc count = Some pc' -> +Lemma branch_target_valid_1: + forall f pc, wt_function f -> valid_successor f pc -> - valid_successor f pc'. + valid_successor f (branch_target f pc). Proof. - induction count; simpl. - intros; discriminate. - intros until pc'. caseEq (is_goto_instr (fn_code f)!pc); intros. - generalize (is_goto_instr_correct _ _ H0). intro. - eapply IHcount; eauto. - generalize (wt_instrs _ H _ _ H3); intro WTI; inv WTI. auto. - inv H1; auto. + intros. + assert (forall n p, + (count_gotos f p < n)%nat -> + valid_successor f p -> + valid_successor f (branch_target f p)). + induction n; intros. + omegaContradiction. + elim H2; intros i EQ. + generalize (record_gotos_correct f p). rewrite EQ. + destruct i; try congruence. + intros [A | [B C]]. congruence. + generalize (wt_instrs _ H _ _ EQ); intro WTI; inv WTI. + rewrite B. apply IHn. omega. auto. + + apply H1 with (Datatypes.S (count_gotos f pc)); auto. Qed. Lemma tunnel_valid_successor: @@ -49,7 +56,7 @@ Lemma tunnel_valid_successor: Proof. intros. destruct H as [i AT]. unfold valid_successor; simpl. rewrite PTree.gmap. rewrite AT. - simpl. exists (tunnel_instr f i); auto. + simpl. exists (tunnel_instr (record_gotos f) i); auto. Qed. Lemma branch_target_valid: @@ -58,16 +65,13 @@ Lemma branch_target_valid: valid_successor f pc -> valid_successor (tunnel_function f) (branch_target f pc). Proof. - intros. apply tunnel_valid_successor. - unfold branch_target. caseEq (branch_target_rec f pc 10); intros. - eapply branch_target_rec_valid; eauto. - auto. + intros. apply tunnel_valid_successor. apply branch_target_valid_1; auto. Qed. Lemma wt_tunnel_instr: forall f i, wt_function f -> - wt_instr f i -> wt_instr (tunnel_function f) (tunnel_instr f i). + wt_instr f i -> wt_instr (tunnel_function f) (tunnel_instr (record_gotos f) i). Proof. intros; inv H0; simpl; econstructor; eauto; eapply branch_target_valid; eauto. |