From 611e7b09253dbbb98e9cd4ca4e07a60b50e693fd Mon Sep 17 00:00:00 2001 From: xleroy Date: Tue, 8 Jul 2008 12:04:42 +0000 Subject: Fusion partielle de la branche contsem: - semantiques a continuation pour Cminor et CminorSel - goto dans Cminor Suppression de backend/RTLbigstep.v, devenu inutile. git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@692 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e --- backend/RTLgenspec.v | 340 +++++++++++++++++++++------------------------------ 1 file changed, 140 insertions(+), 200 deletions(-) (limited to 'backend/RTLgenspec.v') diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index b8061a3f..59a5dd7e 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -136,39 +136,27 @@ Lemma instr_at_incr: forall s1 s2 n i, state_incr s1 s2 -> s1.(st_code)!n = Some i -> s2.(st_code)!n = Some i. Proof. - intros. inversion H. - rewrite H3. auto. elim (st_wf s1 n); intro. - assumption. congruence. + intros. inv H. + destruct (H3 n); congruence. Qed. Hint Resolve instr_at_incr: rtlg. -(** The following relation between two states is a weaker version of - [state_incr]. It permits changing the contents at an already reserved - graph node, but only from [None] to [Some i]. *) +(* +(** A useful tactic to reason over transitivity and reflexivity of [state_incr]. *) -Definition state_extends (s1 s2: state): Prop := - forall pc, - s1.(st_code)!pc = None \/ s2.(st_code)!pc = s1.(st_code)!pc. +Ltac Show_state_incr := + eauto; + match goal with + | |- (state_incr ?c ?c) => + apply state_incr_refl + | |- (state_incr ?c1 ?c2) => + eapply state_incr_trans; [eauto; fail | idtac]; Show_state_incr + end. -Lemma instr_at_extends: - forall s1 s2 pc i, - state_extends s1 s2 -> - s1.(st_code)!pc = Some i -> s2.(st_code)!pc = Some i. -Proof. - intros. elim (H pc); intro. congruence. congruence. -Qed. +Hint Extern 2 (state_incr _ _) => Show_state_incr : rtlg. +*) -Lemma state_incr_extends: - forall s1 s2, - state_incr s1 s2 -> state_extends s1 s2. -Proof. - unfold state_extends; intros. inversion H. - case (plt pc s1.(st_nextnode)); intro. - right; apply H2; auto. - left. elim (s1.(st_wf) pc); intro. - elim (n H5). auto. -Qed. -Hint Resolve state_incr_extends: rtlg. +Hint Resolve state_incr_refl state_incr_trans: rtlg. (** * Validity and freshness of registers *) @@ -273,70 +261,18 @@ Proof. Qed. Hint Resolve add_instr_at: rtlg. -(** Properties of [update_instr] and [add_loop]. The following diagram - shows the evolutions of the code component of the state during [add_loop]. - The vertical bar materializes the [st_nextnode] pointer. -<< - s1: I1 I2 ... In |None None None None None None None -reserve_instr - s2: I1 I2 ... In None|None None None None None None -body n - s3: I1 I2 ... In None Ip ... Iq |None None None -update_instr - s4: I1 I2 ... In Inop Ip ... Iq |None None None ->> - It is apparent that [state_incr s1 s2] and [state_incr s1 s4] hold. - Moreover, [state_extends s3 s4] holds but not [state_incr s3 s4]. -*) +(** Properties of [update_instr]. *) -Lemma update_instr_extends: - forall s1 s2 s3 i n, - reserve_instr s1 = (n, s2) -> - state_incr s2 s3 -> - state_extends s3 (update_instr n i s3). +Lemma update_instr_at: + forall n i s1 s2 incr u, + update_instr n i s1 = OK u s2 incr -> s2.(st_code)!n = Some i. Proof. - intros. injection H. intros EQ1 EQ2. - unfold update_instr. destruct (plt n (st_nextnode s3)). - red; simpl; intros. rewrite PTree.gsspec. - case (peq pc n); intro. - subst pc. left. inversion H0. subst s0 s4. rewrite H3. - rewrite <- EQ1; simpl. - destruct (s1.(st_wf) n). - rewrite <- EQ2 in H4. elim (Plt_strict _ H4). - auto. - rewrite <- EQ1; rewrite <- EQ2; simpl. apply Plt_succ. - auto. - red; intros; auto. -Qed. - -Lemma add_loop_inversion: - forall f s1 nbody s4 i, - add_loop f s1 = OK nbody s4 i -> - exists nloop, exists s2, exists s3, exists i', - state_incr s1 s2 - /\ f nloop s2 = OK nbody s3 i' - /\ state_extends s3 s4 - /\ s4.(st_code)!nloop = Some(Inop nbody). -Proof. - intros until i. unfold add_loop. - unfold reserve_instr; simpl. - set (s2 := mkstate (st_nextreg s1) (Psucc (st_nextnode s1)) (st_code s1) - (reserve_instr_wf s1)). - set (nloop := st_nextnode s1). - case_eq (f nloop s2). intros; discriminate. - intros n s3 i' EQ1 EQ2. inv EQ2. - exists nloop; exists s2; exists s3; exists i'. - split. - unfold s2; constructor; simpl. - apply Ple_succ. apply Ple_refl. auto. - split. auto. - split. apply update_instr_extends with s1 s2; auto. - unfold update_instr. destruct (plt nloop (st_nextnode s3)). - simpl. apply PTree.gss. - elim n. apply Plt_Ple_trans with (st_nextnode s2). - unfold nloop, s2; simpl; apply Plt_succ. - inversion i'; auto. + intros. unfold update_instr in H. + destruct (plt n (st_nextnode s1)); try discriminate. + destruct (check_empty_node s1 n); try discriminate. + inv H. simpl. apply PTree.gss. Qed. +Hint Resolve update_instr_at: rtlg. (** Properties of [new_reg]. *) @@ -819,76 +755,84 @@ Inductive tr_switch its value is deposited in register [rret]. *) Inductive tr_stmt (c: code) (map: mapping): - stmt -> node -> node -> list node -> node -> option reg -> Prop := - | tr_Sskip: forall ns nexits nret rret, - tr_stmt c map Sskip ns ns nexits nret rret - | tr_Sassign: forall id a ns nd nexits nret rret rt n, + stmt -> node -> node -> list node -> labelmap -> node -> option reg -> Prop := + | tr_Sskip: forall ns nexits ngoto nret rret, + tr_stmt c map Sskip ns ns nexits ngoto nret rret + | tr_Sassign: forall id a ns nd nexits ngoto nret rret rt n, tr_expr c map nil a ns n rt -> tr_store_var c map rt id n nd -> - tr_stmt c map (Sassign id a) ns nd nexits nret rret - | tr_Sstore: forall chunk addr al b ns nd nexits nret rret rd n1 rl n2, + tr_stmt c map (Sassign id a) ns nd nexits ngoto nret rret + | tr_Sstore: forall chunk addr al b ns nd nexits ngoto nret rret rd n1 rl n2, tr_exprlist c map nil al ns n1 rl -> tr_expr c map rl b n1 n2 rd -> c!n2 = Some (Istore chunk addr rl rd nd) -> - tr_stmt c map (Sstore chunk addr al b) ns nd nexits nret rret - | tr_Scall: forall optid sig b cl ns nd nexits nret rret rd n1 rf n2 n3 rargs, + tr_stmt c map (Sstore chunk addr al b) ns nd nexits ngoto nret rret + | tr_Scall: forall optid sig b cl ns nd nexits ngoto nret rret rd n1 rf n2 n3 rargs, tr_expr c map nil b ns n1 rf -> tr_exprlist c map (rf :: nil) cl n1 n2 rargs -> c!n2 = Some (Icall sig (inl _ rf) rargs rd n3) -> tr_store_optvar c map rd optid n3 nd -> ~reg_in_map map rd -> - tr_stmt c map (Scall optid sig b cl) ns nd nexits nret rret - | tr_Salloc: forall id a ns nd nexits nret rret rd n1 n2 r, + tr_stmt c map (Scall optid sig b cl) ns nd nexits ngoto nret rret + | tr_Stailcall: forall sig b cl ns nd nexits ngoto nret rret n1 rf n2 rargs, + tr_expr c map nil b ns n1 rf -> + tr_exprlist c map (rf :: nil) cl n1 n2 rargs -> + c!n2 = Some (Itailcall sig (inl _ rf) rargs) -> + tr_stmt c map (Stailcall sig b cl) ns nd nexits ngoto nret rret + | tr_Salloc: forall id a ns nd nexits ngoto nret rret rd n1 n2 r, tr_expr c map nil a ns n1 r -> c!n1 = Some (Ialloc r rd n2) -> tr_store_var c map rd id n2 nd -> ~reg_in_map map rd -> - tr_stmt c map (Salloc id a) ns nd nexits nret rret - | tr_Sseq: forall s1 s2 ns nd nexits nret rret n, - tr_stmt c map s2 n nd nexits nret rret -> - tr_stmt c map s1 ns n nexits nret rret -> - tr_stmt c map (Sseq s1 s2) ns nd nexits nret rret - | tr_Sifthenelse: forall a strue sfalse ns nd nexits nret rret ntrue nfalse, - tr_stmt c map strue ntrue nd nexits nret rret -> - tr_stmt c map sfalse nfalse nd nexits nret rret -> + tr_stmt c map (Salloc id a) ns nd nexits ngoto nret rret + | tr_Sseq: forall s1 s2 ns nd nexits ngoto nret rret n, + tr_stmt c map s2 n nd nexits ngoto nret rret -> + tr_stmt c map s1 ns n nexits ngoto nret rret -> + tr_stmt c map (Sseq s1 s2) ns nd nexits ngoto nret rret + | tr_Sifthenelse: forall a strue sfalse ns nd nexits ngoto nret rret ntrue nfalse, + tr_stmt c map strue ntrue nd nexits ngoto nret rret -> + tr_stmt c map sfalse nfalse nd nexits ngoto nret rret -> tr_condition c map nil a ns ntrue nfalse -> - tr_stmt c map (Sifthenelse a strue sfalse) ns nd nexits nret rret - | tr_Sloop: forall sbody ns nd nexits nret rret nloop, - tr_stmt c map sbody ns nloop nexits nret rret -> - c!nloop = Some(Inop ns) -> - tr_stmt c map (Sloop sbody) ns nd nexits nret rret - | tr_Sblock: forall sbody ns nd nexits nret rret, - tr_stmt c map sbody ns nd (nd :: nexits) nret rret -> - tr_stmt c map (Sblock sbody) ns nd nexits nret rret - | tr_Sexit: forall n ns nd nexits nret rret, + tr_stmt c map (Sifthenelse a strue sfalse) ns nd nexits ngoto nret rret + | tr_Sloop: forall sbody ns nd nexits ngoto nret rret nloop, + tr_stmt c map sbody nloop ns nexits ngoto nret rret -> + c!ns = Some(Inop nloop) -> + tr_stmt c map (Sloop sbody) ns nd nexits ngoto nret rret + | tr_Sblock: forall sbody ns nd nexits ngoto nret rret, + tr_stmt c map sbody ns nd (nd :: nexits) ngoto nret rret -> + tr_stmt c map (Sblock sbody) ns nd nexits ngoto nret rret + | tr_Sexit: forall n ns nd nexits ngoto nret rret, nth_error nexits n = Some ns -> - tr_stmt c map (Sexit n) ns nd nexits nret rret - | tr_Sswitch: forall a cases default ns nd nexits nret rret n r t, + tr_stmt c map (Sexit n) ns nd nexits ngoto nret rret + | tr_Sswitch: forall a cases default ns nd nexits ngoto nret rret n r t, validate_switch default cases t = true -> tr_expr c map nil a ns n r -> tr_switch c r nexits t n -> - tr_stmt c map (Sswitch a cases default) ns nd nexits nret rret - | tr_Sreturn_none: forall nret nd nexits, - tr_stmt c map (Sreturn None) nret nd nexits nret None - | tr_Sreturn_some: forall a ns nd nexits nret rret, + tr_stmt c map (Sswitch a cases default) ns nd nexits ngoto nret rret + | tr_Sreturn_none: forall nret nd nexits ngoto, + tr_stmt c map (Sreturn None) nret nd nexits ngoto nret None + | tr_Sreturn_some: forall a ns nd nexits ngoto nret rret, tr_expr c map nil a ns nret rret -> - tr_stmt c map (Sreturn (Some a)) ns nd nexits nret (Some rret) - | tr_Stailcall: forall sig b cl ns nd nexits nret rret n1 rf n2 rargs, - tr_expr c map nil b ns n1 rf -> - tr_exprlist c map (rf :: nil) cl n1 n2 rargs -> - c!n2 = Some (Itailcall sig (inl _ rf) rargs) -> - tr_stmt c map (Stailcall sig b cl) ns nd nexits nret rret. + tr_stmt c map (Sreturn (Some a)) ns nd nexits ngoto nret (Some rret) + | tr_Slabel: forall lbl s ns nd nexits ngoto nret rret n, + ngoto!lbl = Some n -> + c!n = Some (Inop ns) -> + tr_stmt c map s ns nd nexits ngoto nret rret -> + tr_stmt c map (Slabel lbl s) ns nd nexits ngoto nret rret + | tr_Sgoto: forall lbl ns nd nexits ngoto nret rret, + ngoto!lbl = Some ns -> + tr_stmt c map (Sgoto lbl) ns nd nexits ngoto nret rret. (** [tr_function f tf] specifies the RTL function [tf] that [RTLgen.transl_function] returns. *) Inductive tr_function: CminorSel.function -> RTL.function -> Prop := | tr_function_intro: - forall f code rparams map1 s1 i1 rvars map2 s2 i2 nentry nret rret orret nextnode wfcode, - add_vars init_mapping f.(CminorSel.fn_params) init_state = OK (rparams, map1) s1 i1 -> + forall f code rparams map1 s0 s1 i1 rvars map2 s2 i2 nentry ngoto nret rret orret nextnode wfcode, + add_vars init_mapping f.(CminorSel.fn_params) s0 = OK (rparams, map1) s1 i1 -> add_vars map1 f.(CminorSel.fn_vars) s1 = OK (rvars, map2) s2 i2 -> orret = ret_reg f.(CminorSel.fn_sig) rret -> - tr_stmt code map2 f.(CminorSel.fn_body) nentry nret nil nret orret -> + tr_stmt code map2 f.(CminorSel.fn_body) nentry nret nil ngoto nret orret -> code!nret = Some(Ireturn orret) -> tr_function f (RTL.mkfunction f.(CminorSel.fn_sig) @@ -918,18 +862,17 @@ Definition tr_expr_condition_exprlist_ind3 (conj (tr_condition_ind3 c P P0 P1 a b c' d e f g h i j k l) (tr_exprlist_ind3 c P P0 P1 a b c' d e f g h i j k l)). -Lemma tr_move_extends: - forall s1 s2, state_extends s1 s2 -> +Lemma tr_move_incr: + forall s1 s2, state_incr s1 s2 -> forall ns rs nd rd, tr_move s1.(st_code) ns rs nd rd -> tr_move s2.(st_code) ns rs nd rd. Proof. - induction 2; econstructor; eauto. - eapply instr_at_extends; eauto. + induction 2; econstructor; eauto with rtlg. Qed. -Lemma tr_expr_condition_exprlist_extends: - forall s1 s2, state_extends s1 s2 -> +Lemma tr_expr_condition_exprlist_incr: + forall s1 s2, state_incr s1 s2 -> (forall map pr a ns nd rd, tr_expr s1.(st_code) map pr a ns nd rd -> tr_expr s2.(st_code) map pr a ns nd rd) @@ -941,10 +884,10 @@ Lemma tr_expr_condition_exprlist_extends: tr_exprlist s2.(st_code) map pr al ns nd rl). Proof. intros s1 s2 EXT. - pose (AT := fun pc i => instr_at_extends s1 s2 pc i EXT). + pose (AT := fun pc i => instr_at_incr s1 s2 pc i EXT). apply tr_expr_condition_exprlist_ind3; intros; econstructor; eauto. - eapply tr_move_extends; eauto. - eapply tr_move_extends; eauto. + eapply tr_move_incr; eauto. + eapply tr_move_incr; eauto. Qed. Lemma tr_expr_incr: @@ -954,8 +897,8 @@ Lemma tr_expr_incr: tr_expr s2.(st_code) map pr a ns nd rd. Proof. intros. - exploit tr_expr_condition_exprlist_extends. - apply state_incr_extends; eauto. intros [A [B C]]. eauto. + exploit tr_expr_condition_exprlist_incr; eauto. + intros [A [B C]]. eauto. Qed. Lemma tr_condition_incr: @@ -965,8 +908,8 @@ Lemma tr_condition_incr: tr_condition s2.(st_code) map pr a ns ntrue nfalse. Proof. intros. - exploit tr_expr_condition_exprlist_extends. - apply state_incr_extends; eauto. intros [A [B C]]. eauto. + exploit tr_expr_condition_exprlist_incr; eauto. + intros [A [B C]]. eauto. Qed. Lemma tr_exprlist_incr: @@ -976,8 +919,8 @@ Lemma tr_exprlist_incr: tr_exprlist s2.(st_code) map pr al ns nd rl. Proof. intros. - exploit tr_expr_condition_exprlist_extends. - apply state_incr_extends; eauto. intros [A [B C]]. eauto. + exploit tr_expr_condition_exprlist_incr; eauto. + intros [A [B C]]. eauto. Qed. Scheme expr_ind3 := Induction for expr Sort Prop @@ -1117,63 +1060,51 @@ Proof. intros. eapply B; eauto with rtlg. Qed. -Lemma tr_store_var_extends: - forall s1 s2, state_extends s1 s2 -> +Lemma tr_store_var_incr: + forall s1 s2, state_incr s1 s2 -> forall map rs id ns nd, tr_store_var s1.(st_code) map rs id ns nd -> tr_store_var s2.(st_code) map rs id ns nd. Proof. intros. destruct H0 as [rv [A B]]. - econstructor; split. eauto. eapply tr_move_extends; eauto. + econstructor; split. eauto. eapply tr_move_incr; eauto. Qed. -Lemma tr_store_optvar_extends: - forall s1 s2, state_extends s1 s2 -> +Lemma tr_store_optvar_incr: + forall s1 s2, state_incr s1 s2 -> forall map rs optid ns nd, tr_store_optvar s1.(st_code) map rs optid ns nd -> tr_store_optvar s2.(st_code) map rs optid ns nd. Proof. intros until nd. destruct optid; simpl. - apply tr_store_var_extends; auto. + apply tr_store_var_incr; auto. auto. Qed. -Lemma tr_switch_extends: - forall s1 s2, state_extends s1 s2 -> +Lemma tr_switch_incr: + forall s1 s2, state_incr s1 s2 -> forall r nexits t ns, tr_switch s1.(st_code) r nexits t ns -> tr_switch s2.(st_code) r nexits t ns. Proof. induction 2; econstructor; eauto with rtlg. - eapply instr_at_extends; eauto. - eapply instr_at_extends; eauto. -Qed. - -Lemma tr_stmt_extends: - forall s1 s2, state_extends s1 s2 -> - forall map s ns nd nexits nret rret, - tr_stmt s1.(st_code) map s ns nd nexits nret rret -> - tr_stmt s2.(st_code) map s ns nd nexits nret rret. -Proof. - intros s1 s2 EXT. - destruct (tr_expr_condition_exprlist_extends s1 s2 EXT) as [A [B C]]. - pose (AT := fun pc i => instr_at_extends s1 s2 pc i EXT). - pose (STV := tr_store_var_extends s1 s2 EXT). - pose (STOV := tr_store_optvar_extends s1 s2 EXT). - induction 1; econstructor; eauto. - eapply tr_switch_extends; eauto. Qed. Lemma tr_stmt_incr: forall s1 s2, state_incr s1 s2 -> - forall map s ns nd nexits nret rret, - tr_stmt s1.(st_code) map s ns nd nexits nret rret -> - tr_stmt s2.(st_code) map s ns nd nexits nret rret. + forall map s ns nd nexits ngoto nret rret, + tr_stmt s1.(st_code) map s ns nd nexits ngoto nret rret -> + tr_stmt s2.(st_code) map s ns nd nexits ngoto nret rret. Proof. - intros. eapply tr_stmt_extends; eauto with rtlg. + intros s1 s2 EXT. + destruct (tr_expr_condition_exprlist_incr s1 s2 EXT) as [A [B C]]. + pose (AT := fun pc i => instr_at_incr s1 s2 pc i EXT). + pose (STV := tr_store_var_incr s1 s2 EXT). + pose (STOV := tr_store_optvar_incr s1 s2 EXT). + induction 1; econstructor; eauto. + eapply tr_switch_incr; eauto. Qed. - Lemma store_var_charact: forall map rs id nd s ns s' incr, store_var map rs id nd s = OK ns s' incr -> @@ -1215,27 +1146,27 @@ Proof. monadInv H. exploit transl_exit_charact; eauto. intros [A B]. subst s1. econstructor; eauto with rtlg. - apply tr_switch_extends with s0; eauto with rtlg. + apply tr_switch_incr with s0; eauto with rtlg. monadInv H. econstructor; eauto with rtlg. - apply tr_switch_extends with s1; eauto with rtlg. - apply tr_switch_extends with s0; eauto with rtlg. + apply tr_switch_incr with s1; eauto with rtlg. + apply tr_switch_incr with s0; eauto with rtlg. Qed. Lemma transl_stmt_charact: - forall map stmt nd nexits nret rret s ns s' INCR - (TR: transl_stmt map stmt nd nexits nret rret s = OK ns s' INCR) + forall map stmt nd nexits ngoto nret rret s ns s' INCR + (TR: transl_stmt map stmt nd nexits ngoto nret rret s = OK ns s' INCR) (WF: map_valid map s) (OK: return_reg_ok s map rret), - tr_stmt s'.(st_code) map stmt ns nd nexits nret rret. + tr_stmt s'.(st_code) map stmt ns nd nexits ngoto nret rret. Proof. induction stmt; intros; simpl in TR; try (monadInv TR). (* Sskip *) constructor. (* Sassign *) econstructor. eapply transl_expr_charact; eauto with rtlg. - apply tr_store_var_extends with s1; auto with rtlg. + apply tr_store_var_incr with s1; auto with rtlg. eapply store_var_charact; eauto. (* Sstore *) destruct transl_expr_condexpr_list_charact as [P1 [P2 P3]]. @@ -1256,12 +1187,20 @@ Proof. apply regs_valid_incr with s1; eauto with rtlg. apply regs_valid_cons; eauto with rtlg. apply regs_valid_incr with s2; eauto with rtlg. - apply tr_store_optvar_extends with s4; eauto with rtlg. + apply tr_store_optvar_incr with s4; eauto with rtlg. eapply store_optvar_charact; eauto with rtlg. + (* Stailcall *) + destruct transl_expr_condexpr_list_charact as [A [B C]]. + assert (RV: regs_valid (x :: nil) s1). + apply regs_valid_cons; eauto with rtlg. + econstructor; eauto with rtlg. + eapply A; eauto with rtlg. + apply tr_exprlist_incr with s4; auto. + eapply C; eauto with rtlg. (* Salloc *) econstructor; eauto with rtlg. eapply transl_expr_charact; eauto with rtlg. - apply tr_store_var_extends with s2; eauto with rtlg. + apply tr_store_var_incr with s2; eauto with rtlg. eapply store_var_charact; eauto with rtlg. (* Sseq *) econstructor. @@ -1283,12 +1222,10 @@ Proof. eapply IHstmt2; eauto with rtlg. eapply transl_condexpr_charact; eauto with rtlg. (* Sloop *) - exploit add_loop_inversion; eauto. - intros [nloop [s2 [s3 [INCR23 [INCR02 [EQ [EXT CODEAT]]]]]]]. econstructor. - apply tr_stmt_extends with s3; auto. - eapply IHstmt; eauto with rtlg. - auto. + apply tr_stmt_incr with s1; auto. + eapply IHstmt; eauto with rtlg. + eauto with rtlg. (* Sblock *) econstructor. eapply IHstmt; eauto with rtlg. @@ -1302,7 +1239,7 @@ Proof. monadInv TR. econstructor; eauto with rtlg. eapply transl_expr_charact; eauto with rtlg. - apply tr_switch_extends with s1; auto with rtlg. + apply tr_switch_incr with s1; auto with rtlg. eapply transl_switch_charact; eauto with rtlg. monadInv TR. (* Sreturn *) @@ -1312,14 +1249,15 @@ Proof. eapply transl_expr_charact; eauto with rtlg. constructor. auto. simpl; tauto. constructor. - (* Stailcall *) - destruct transl_expr_condexpr_list_charact as [A [B C]]. - assert (RV: regs_valid (x :: nil) s1). - apply regs_valid_cons; eauto with rtlg. - econstructor; eauto with rtlg. - eapply A; eauto with rtlg. - apply tr_exprlist_incr with s4; auto. - eapply C; eauto with rtlg. + (* Slabel *) + generalize EQ0; clear EQ0. case_eq (ngoto!l); intros; monadInv EQ0. + generalize EQ1; clear EQ1. unfold handle_error. + case_eq (update_instr n (Inop ns) s0); intros; inv EQ1. + econstructor. eauto. eauto with rtlg. + eapply tr_stmt_incr with s0; eauto with rtlg. + (* Sgoto *) + generalize TR; clear TR. case_eq (ngoto!l); intros; monadInv TR. + econstructor. auto. Qed. Lemma transl_function_charact: @@ -1327,8 +1265,10 @@ Lemma transl_function_charact: transl_function f = Errors.OK tf -> tr_function f tf. Proof. - intros until tf. unfold transl_function. - caseEq (transl_fun f init_state). congruence. + intros until tf. unfold transl_function. + caseEq (reserve_labels (fn_body f) (PTree.empty node, init_state)). + intros ngoto s0 RESERVE. + caseEq (transl_fun f ngoto s0). congruence. intros [nentry rparams] sfinal INCR TR E. inv E. monadInv TR. exploit add_vars_valid. eexact EQ. apply init_mapping_valid. -- cgit