diff options
| -rw-r--r-- | backend/RTLgen.v | 5 | ||||
| -rw-r--r-- | backend/RTLgenproof.v | 87 | ||||
| -rw-r--r-- | backend/RTLgenspec.v | 224 |
3 files changed, 211 insertions, 105 deletions
diff --git a/backend/RTLgen.v b/backend/RTLgen.v index 942dc50..ff4f81c 100644 --- a/backend/RTLgen.v +++ b/backend/RTLgen.v @@ -524,9 +524,8 @@ Fixpoint transl_stmt (map: mapping) (s: stmt) (nd: node) | Sskip => ret nd | Sassign v b => - do rt <- alloc_reg map b; - do no <- store_var map rt v nd; - transl_expr map b rt no + do r <- find_var map v; + transl_expr map b r nd | Sstore chunk addr al b => do rl <- alloc_regs map al; do r <- alloc_reg map b; diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index f4d1342..a15095b 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -197,6 +197,30 @@ Proof. symmetry. apply PMap.gso. red; intros. subst x. eauto. Qed. +(** A variant of [match_env_update_var] where a variable is optionally + assigned to, depending on the [dst] parameter. *) + +Definition assign_dest (dst: option ident) (v: val) (e: Cminor.env) : Cminor.env := + match dst with + | None => e + | Some id => PTree.set id v e + end. + +Lemma match_env_update_dest: + forall map e le rs dst r v, + map_wf map -> + reg_map_ok map r dst -> + match_env map e le rs -> + match_env map (assign_dest dst v e) le (rs#r <- v). +Proof. + intros. inv H0; simpl. + eapply match_env_update_temp; eauto. + eapply match_env_update_var; eauto. +Qed. +Hint Resolve match_env_update_dest: rtlg. + +(** Matching and [let]-bound variables. *) + Lemma match_env_bind_letvar: forall map e le rs r v, match_env map e le rs -> @@ -215,6 +239,8 @@ Proof. constructor. auto. congruence. Qed. +(** Matching between initial environments. *) + Lemma match_env_empty: forall map, map.(map_letvars) = nil -> @@ -521,15 +547,15 @@ Variable m: mem. Definition transl_expr_prop (le: letenv) (a: expr) (v: val) : Prop := - forall cs f map pr ns nd rd rs + forall cs f map pr ns nd rd rs dst (MWF: map_wf map) - (TE: tr_expr f.(fn_code) map pr a ns nd rd) + (TE: tr_expr f.(fn_code) map pr a ns nd rd dst) (ME: match_env map e le rs), exists rs', star step tge (State cs f sp ns rs m) E0 (State cs f sp nd rs' m) - /\ match_env map e le rs' + /\ match_env map (assign_dest dst v e) le rs' /\ rs'#rd = v - /\ (forall r, reg_in_map map r \/ In r pr -> rs'#r = rs#r). + /\ (forall r, In r pr -> rs'#r = rs#r). (** The simulation properties for lists of expressions and for conditional expressions are similar. *) @@ -544,7 +570,7 @@ Definition transl_exprlist_prop star step tge (State cs f sp ns rs m) E0 (State cs f sp nd rs' m) /\ match_env map e le rs' /\ rs'##rl = vl - /\ (forall r, reg_in_map map r \/ In r pr -> rs'#r = rs#r). + /\ (forall r, In r pr -> rs'#r = rs#r). Definition transl_condition_prop (le: letenv) (a: condexpr) (vb: bool) : Prop := @@ -556,7 +582,7 @@ Definition transl_condition_prop star step tge (State cs f sp ns rs m) E0 (State cs f sp (if vb then ntrue else nfalse) rs' m) /\ match_env map e le rs' - /\ (forall r, reg_in_map map r \/ In r pr -> rs'#r = rs#r). + /\ (forall r, In r pr -> rs'#r = rs#r). (** The correctness of the translation is a huge induction over the Cminor evaluation derivation for the source program. To keep @@ -572,20 +598,22 @@ Lemma transl_expr_Evar_correct: transl_expr_prop le (Evar id) v. Proof. intros; red; intros. inv TE. + exploit match_env_find_var; eauto. intro EQ. exploit tr_move_correct; eauto. intros [rs' [A [B C]]]. exists rs'; split. eauto. - destruct H2 as [D | [E F]]. + destruct H2 as [[D E] | [D E]]. (* optimized case *) - subst r. + subst r dst. simpl. assert (forall r, rs'#r = rs#r). intros. destruct (Reg.eq r rd). subst r. auto. auto. split. eapply match_env_invariant; eauto. - split. rewrite B. eapply match_env_find_var; eauto. - auto. + split. congruence. auto. (* general case *) - split. eapply match_env_invariant; eauto. - intros. apply C. congruence. - split. rewrite B. eapply match_env_find_var; eauto. + split. + apply match_env_invariant with (rs#rd <- v). + apply match_env_update_dest; auto. + intros. rewrite Regmap.gsspec. destruct (peq r0 rd). congruence. auto. + split. congruence. intros. apply C. intuition congruence. Qed. @@ -608,7 +636,7 @@ Proof. auto. exact symbols_preserved. traceEq. (* Match-env *) - split. eauto with rtlg. + split. eauto with rtlg. (* Result reg *) split. apply Regmap.gss. (* Other regs *) @@ -650,7 +678,7 @@ Lemma transl_expr_Econdition_correct: Proof. intros; red; intros; inv TE. exploit H0; eauto. intros [rs1 [EX1 [ME1 OTHER1]]]. - assert (tr_expr f.(fn_code) map pr (if vcond then ifso else ifnot) (if vcond then ntrue else nfalse) nd rd). + assert (tr_expr f.(fn_code) map pr (if vcond then ifso else ifnot) (if vcond then ntrue else nfalse) nd rd dst). destruct vcond; auto. exploit H2; eauto. intros [rs2 [EX2 [ME2 [RES2 OTHER2]]]]. exists rs2. @@ -686,11 +714,7 @@ Proof. (* Result *) split. assumption. (* Other regs *) - intros. transitivity (rs1#r0). - apply OTHER2. elim H4; intro; auto. - unfold reg_in_map, add_letvar; simpl. - unfold reg_in_map in H6; tauto. - auto. + intros. transitivity (rs1#r0); auto. Qed. Lemma transl_expr_Eletvar_correct: @@ -704,15 +728,21 @@ Proof. (* Exec *) split. eexact EX1. (* Match-env *) - split. apply match_env_invariant with rs. auto. - intros. destruct H2 as [A | [B C]]. - subst r. destruct (Reg.eq r0 rd). subst r0; auto. auto. - apply OTHER1. intuition congruence. + split. + destruct H2 as [[A B] | [A B]]. + subst r dst; simpl. + apply match_env_invariant with rs. auto. + intros. destruct (Reg.eq r rd). subst r. auto. auto. + apply match_env_invariant with (rs#rd <- v). + apply match_env_update_dest; auto. + intros. rewrite Regmap.gsspec. destruct (peq r0 rd); auto. + subst. rewrite RES1. eapply match_env_find_letvar; eauto. (* Result *) split. rewrite RES1. eapply match_env_find_letvar; eauto. (* Other regs *) - intros. destruct H2 as [A | [B C]]. - subst r. destruct (Reg.eq r0 rd). subst r0; auto. auto. + intros. + destruct H2 as [[A B] | [A B]]. + destruct (Reg.eq r0 rd); subst; auto. apply OTHER1. intuition congruence. Qed. @@ -1128,11 +1158,8 @@ Proof. inv TS. exploit transl_expr_correct; eauto. intros [rs' [A [B [C D]]]]. - exploit tr_store_var_correct; eauto. - intros [rs'' [E F]]. - rewrite C in F. econstructor; split. - right; split. eapply star_trans. eexact A. eexact E. traceEq. Lt_state. + right; split. eauto. Lt_state. econstructor; eauto. constructor. (* store *) diff --git a/backend/RTLgenspec.v b/backend/RTLgenspec.v index 51fb945..5690bb2 100644 --- a/backend/RTLgenspec.v +++ b/backend/RTLgenspec.v @@ -132,6 +132,8 @@ Ltac monadInv H := (** * Monotonicity properties of the state *) +Hint Resolve state_incr_refl: rtlg. + 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. @@ -141,7 +143,23 @@ Proof. Qed. Hint Resolve instr_at_incr: rtlg. -Hint Resolve state_incr_refl state_incr_trans: rtlg. +(** The following tactic saturates the hypotheses with + [state_incr] properties that follow by transitivity from + the known hypotheses. *) + +Ltac saturateTrans := + match goal with + | H1: state_incr ?x ?y, H2: state_incr ?y ?z |- _ => + match goal with + | H: state_incr x z |- _ => + fail 1 + | _ => + let i := fresh "INCR" in + (generalize (state_incr_trans x y z H1 H2); intro i; + saturateTrans) + end + | _ => idtac + end. (** * Validity and freshness of registers *) @@ -619,49 +637,69 @@ Inductive tr_move (c: code): c!ns = Some (Iop Omove (rs :: nil) rd nd) -> tr_move c ns rs nd rd. -(** [tr_expr c map pr expr ns nd rd] holds if the graph [c], +(** [reg_map_ok map r optid] characterizes the destination register + for an expression: if [optid] is [None], the destination is + a fresh register (not associated with any variable); + if [optid] is [Some id], the destination is the register + associated with local variable [id]. *) + +Inductive reg_map_ok: mapping -> reg -> option ident -> Prop := + | reg_map_ok_novar: forall map rd, + ~reg_in_map map rd -> + reg_map_ok map rd None + | reg_map_ok_somevar: forall map rd id, + map.(map_vars)!id = Some rd -> + reg_map_ok map rd (Some id). + +Hint Resolve reg_map_ok_novar: rtlg. + +(** [tr_expr c map pr expr ns nd rd optid] holds if the graph [c], between nodes [ns] and [nd], contains instructions that compute the value of the Cminor expression [expr] and deposit this value in register [rd]. [map] is a mapping from Cminor variables to the corresponding RTL registers. [pr] is a list of RTL registers whose values must be preserved during this computation. All registers mentioned in [map] must also be preserved during this computation. - To ensure this, we demand that the result registers of the instructions - appearing on the path from [ns] to [nd] are neither in [pr] nor in [map]. + (Exception: if [optid = Some id], the register associated with + local variable [id] can be assigned, but only at the end of the + expression evaluation.) + To ensure this property, we demand that the result registers of the + instructions appearing on the path from [ns] to [nd] are not in [pr], + and moreover that they satisfy the [reg_map_ok] predicate. *) Inductive tr_expr (c: code): - mapping -> list reg -> expr -> node -> node -> reg -> Prop := - | tr_Evar: forall map pr id ns nd r rd, + mapping -> list reg -> expr -> node -> node -> reg -> option ident -> Prop := + | tr_Evar: forall map pr id ns nd r rd dst, map.(map_vars)!id = Some r -> - (rd = r \/ ~reg_in_map map rd /\ ~In rd pr) -> + ((rd = r /\ dst = None) \/ (reg_map_ok map rd dst /\ ~In rd pr)) -> tr_move c ns r nd rd -> - tr_expr c map pr (Evar id) ns nd rd - | tr_Eop: forall map pr op al ns nd rd n1 rl, + tr_expr c map pr (Evar id) ns nd rd dst + | tr_Eop: forall map pr op al ns nd rd n1 rl dst, tr_exprlist c map pr al ns n1 rl -> c!n1 = Some (Iop op rl rd nd) -> - ~reg_in_map map rd -> ~In rd pr -> - tr_expr c map pr (Eop op al) ns nd rd - | tr_Eload: forall map pr chunk addr al ns nd rd n1 rl, + reg_map_ok map rd dst -> ~In rd pr -> + tr_expr c map pr (Eop op al) ns nd rd dst + | tr_Eload: forall map pr chunk addr al ns nd rd n1 rl dst, tr_exprlist c map pr al ns n1 rl -> c!n1 = Some (Iload chunk addr rl rd nd) -> - ~reg_in_map map rd -> ~In rd pr -> - tr_expr c map pr (Eload chunk addr al) ns nd rd - | tr_Econdition: forall map pr b ifso ifnot ns nd rd ntrue nfalse, + reg_map_ok map rd dst -> ~In rd pr -> + tr_expr c map pr (Eload chunk addr al) ns nd rd dst + | tr_Econdition: forall map pr b ifso ifnot ns nd rd ntrue nfalse dst, tr_condition c map pr b ns ntrue nfalse -> - tr_expr c map pr ifso ntrue nd rd -> - tr_expr c map pr ifnot nfalse nd rd -> - tr_expr c map pr (Econdition b ifso ifnot) ns nd rd - | tr_Elet: forall map pr b1 b2 ns nd rd n1 r, + tr_expr c map pr ifso ntrue nd rd dst -> + tr_expr c map pr ifnot nfalse nd rd dst -> + tr_expr c map pr (Econdition b ifso ifnot) ns nd rd dst + | tr_Elet: forall map pr b1 b2 ns nd rd n1 r dst, ~reg_in_map map r -> - tr_expr c map pr b1 ns n1 r -> - tr_expr c (add_letvar map r) pr b2 n1 nd rd -> - tr_expr c map pr (Elet b1 b2) ns nd rd - | tr_Eletvar: forall map pr n ns nd rd r, + tr_expr c map pr b1 ns n1 r None -> + tr_expr c (add_letvar map r) pr b2 n1 nd rd dst -> + tr_expr c map pr (Elet b1 b2) ns nd rd dst + | tr_Eletvar: forall map pr n ns nd rd r dst, List.nth_error map.(map_letvars) n = Some r -> - (rd = r \/ ~reg_in_map map rd /\ ~In rd pr) -> + ((rd = r /\ dst = None) \/ (reg_map_ok map rd dst /\ ~In rd pr)) -> tr_move c ns r nd rd -> - tr_expr c map pr (Eletvar n) ns nd rd + tr_expr c map pr (Eletvar n) ns nd rd dst (** [tr_condition c map pr cond ns ntrue nfalse rd] holds if the graph [c], starting at node [ns], contains instructions that compute the truth @@ -694,7 +732,7 @@ with tr_exprlist (c: code): | tr_Enil: forall map pr n, tr_exprlist c map pr Enil n n nil | tr_Econs: forall map pr a1 al ns nd r1 rl n1, - tr_expr c map pr a1 ns n1 r1 -> + tr_expr c map pr a1 ns n1 r1 None -> tr_exprlist c map (r1 :: pr) al n1 nd rl -> tr_exprlist c map pr (Econs a1 al) ns nd (r1 :: rl). @@ -757,24 +795,24 @@ Inductive tr_stmt (c: code) (map: mapping): 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_Sassign: forall id a ns nd nexits ngoto nret rret r, + map.(map_vars)!id = Some r -> + tr_expr c map nil a ns nd r (Some id) -> 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 -> + tr_expr c map rl b n1 n2 rd None -> c!n2 = Some (Istore chunk addr rl rd nd) -> 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_expr c map nil b ns n1 rf None -> 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 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_expr c map nil b ns n1 rf None -> 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 @@ -799,13 +837,13 @@ Inductive tr_stmt (c: code) (map: mapping): 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_expr c map nil a ns n r None -> tr_switch c map r nexits t n -> 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_expr c map nil a ns nret rret None -> 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 -> @@ -850,9 +888,9 @@ Qed. Lemma tr_expr_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 + forall map pr a ns nd rd dst, + tr_expr s1.(st_code) map pr a ns nd rd dst -> + tr_expr s2.(st_code) map pr a ns nd rd dst with tr_condition_incr: forall s1 s2, state_incr s1 s2 -> forall map pr a ns ntrue nfalse, @@ -894,7 +932,7 @@ Lemma transl_expr_charact: (OK: target_reg_ok map pr a rd) (VALID: regs_valid pr s) (VALID2: reg_valid rd s), - tr_expr s'.(st_code) map pr a ns nd rd + tr_expr s'.(st_code) map pr a ns nd rd None with transl_condexpr_charact: forall a map ntrue nfalse s ns s' pr INCR @@ -913,11 +951,11 @@ with transl_exprlist_charact: tr_exprlist s'.(st_code) map pr al ns nd rl. Proof. - induction a; intros; try (monadInv TR). + induction a; intros; try (monadInv TR); saturateTrans. (* Evar *) generalize EQ; unfold find_var. caseEq (map_vars map)!i; intros; inv EQ1. econstructor; eauto. - inv OK. left; congruence. right; eauto. + inv OK. left; split; congruence. right; eauto with rtlg. eapply add_move_charact; eauto. (* Eop *) inv OK. @@ -930,15 +968,14 @@ Proof. (* Econdition *) inv OK. econstructor; eauto with rtlg. - eapply transl_condexpr_charact; eauto with rtlg. apply tr_expr_incr with s1; auto. - eapply transl_expr_charact; eauto with rtlg. constructor; auto. + eapply transl_expr_charact; eauto 2 with rtlg. constructor; auto. apply tr_expr_incr with s0; auto. - eapply transl_expr_charact; eauto with rtlg. constructor; auto. + eapply transl_expr_charact; eauto 2 with rtlg. constructor; auto. (* Elet *) inv OK. econstructor. eapply new_reg_not_in_map; eauto with rtlg. - eapply transl_expr_charact; eauto with rtlg. + eapply transl_expr_charact; eauto 3 with rtlg. apply tr_expr_incr with s1; auto. eapply transl_expr_charact. eauto. apply add_letvar_valid; eauto with rtlg. @@ -952,12 +989,12 @@ Proof. generalize EQ; unfold find_letvar. caseEq (nth_error (map_letvars map) n); intros; inv EQ0. monadInv EQ1. econstructor; eauto with rtlg. - inv OK. left; congruence. right; eauto. + inv OK. left; split; congruence. right; eauto with rtlg. eapply add_move_charact; eauto. monadInv EQ1. (* Conditions *) - induction a; intros; try (monadInv TR). + induction a; intros; try (monadInv TR); saturateTrans. (* CEtrue *) constructor. @@ -976,7 +1013,7 @@ Proof. (* Lists *) - induction al; intros; try (monadInv TR). + induction al; intros; try (monadInv TR); saturateTrans. (* Enil *) destruct rl; inv TR. constructor. @@ -991,6 +1028,49 @@ Proof. red; intros; apply VALID2; auto with coqlib. Qed. +(** A variant of [transl_expr_charact], for use when the destination + register is the one associated with a variable. *) + +Lemma transl_expr_assign_charact: + forall id a map rd nd s ns s' INCR + (TR: transl_expr map a rd nd s = OK ns s' INCR) + (WF: map_valid map s) + (OK: reg_map_ok map rd (Some id)), + tr_expr s'.(st_code) map nil a ns nd rd (Some id). +Proof. + induction a; intros; monadInv TR; saturateTrans. + (* Evar *) + generalize EQ; unfold find_var. caseEq (map_vars map)!i; intros; inv EQ1. + econstructor; eauto. + eapply add_move_charact; eauto. + (* Eop *) + econstructor; eauto with rtlg. + eapply transl_exprlist_charact; eauto with rtlg. + (* Eload *) + econstructor; eauto with rtlg. + eapply transl_exprlist_charact; eauto with rtlg. + (* Econdition *) + econstructor; eauto with rtlg. + eapply transl_condexpr_charact; eauto with rtlg. + apply tr_expr_incr with s1; auto. + eapply IHa1; eauto 2 with rtlg. + apply tr_expr_incr with s0; auto. + eapply IHa2; eauto 2 with rtlg. + (* Elet *) + econstructor. eapply new_reg_not_in_map; eauto with rtlg. + eapply transl_expr_charact; eauto 3 with rtlg. + apply tr_expr_incr with s1; auto. + eapply IHa2; eauto. + apply add_letvar_valid; eauto with rtlg. + inv OK. constructor. auto. + (* Eletvar *) + generalize EQ; unfold find_letvar. caseEq (nth_error (map_letvars map) n); intros; inv EQ0. + monadInv EQ1. + econstructor; eauto with rtlg. + eapply add_move_charact; eauto. + monadInv EQ1. +Qed. + Lemma tr_store_var_incr: forall s1 s2, state_incr s1 s2 -> forall map rs id ns nd, @@ -1084,17 +1164,18 @@ Lemma transl_switch_charact: transl_switch r nexits t s = OK ns s' incr -> tr_switch s'.(st_code) map r nexits t ns. Proof. - induction t; simpl; intros. + induction t; simpl; intros; saturateTrans. + exploit transl_exit_charact; eauto. intros [A B]. econstructor; eauto. monadInv H1. exploit transl_exit_charact; eauto. intros [A B]. subst s1. - econstructor; eauto with rtlg. + econstructor; eauto 2 with rtlg. apply tr_switch_incr with s0; eauto with rtlg. monadInv H1. - econstructor; eauto with rtlg. + econstructor; eauto 2 with rtlg. apply tr_switch_incr with s1; eauto with rtlg. apply tr_switch_incr with s0; eauto with rtlg. @@ -1115,39 +1196,38 @@ Lemma transl_stmt_charact: (OK: return_reg_ok s map rret), tr_stmt s'.(st_code) map stmt ns nd nexits ngoto nret rret. Proof. - induction stmt; intros; simpl in TR; try (monadInv TR). + induction stmt; intros; simpl in TR; try (monadInv TR); saturateTrans. (* Sskip *) constructor. (* Sassign *) - econstructor. eapply transl_expr_charact; eauto with rtlg. - apply tr_store_var_incr with s1; auto with rtlg. - eapply store_var_charact; eauto. + revert EQ. unfold find_var. case_eq (map_vars map)!i; intros; monadInv EQ. + econstructor. eauto. + eapply transl_expr_assign_charact; eauto with rtlg. + constructor. auto. (* Sstore *) econstructor; eauto with rtlg. - eapply transl_exprlist_charact; eauto with rtlg. - apply tr_expr_incr with s3; eauto with rtlg. - eapply transl_expr_charact; eauto with rtlg. + eapply transl_exprlist_charact; eauto 3 with rtlg. + apply tr_expr_incr with s3; auto. + eapply transl_expr_charact; eauto 4 with rtlg. (* Scall *) - assert (state_incr s0 s2) by eauto with rtlg. - assert (state_incr s2 s4) by eauto with rtlg. - assert (state_incr s4 s6) by eauto with rtlg. - econstructor; eauto with rtlg. - eapply transl_expr_charact; eauto with rtlg. + econstructor; eauto 4 with rtlg. + eapply transl_expr_charact; eauto 3 with rtlg. apply tr_exprlist_incr with s6. auto. - eapply transl_exprlist_charact; eauto with rtlg. - eapply alloc_regs_target_ok with (s1 := s1); eauto with rtlg. - apply regs_valid_cons; eauto with rtlg. - apply regs_valid_incr with s1; eauto with rtlg. - apply regs_valid_cons; eauto with rtlg. - apply tr_store_optvar_incr with s4; eauto with rtlg. + eapply transl_exprlist_charact; eauto 3 with rtlg. + eapply alloc_regs_target_ok with (s1 := s1); eauto 3 with rtlg. + apply regs_valid_cons; eauto 3 with rtlg. + apply regs_valid_incr with s1; eauto 3 with rtlg. + apply regs_valid_cons; eauto 3 with rtlg. + apply regs_valid_incr with s2; eauto 3 with rtlg. + apply tr_store_optvar_incr with s4; auto. eapply store_optvar_charact; eauto with rtlg. (* Stailcall *) assert (RV: regs_valid (x :: nil) s1). - apply regs_valid_cons; eauto with rtlg. - econstructor; eauto with rtlg. - eapply transl_expr_charact; eauto with rtlg. + apply regs_valid_cons; eauto 3 with rtlg. + econstructor; eauto 3 with rtlg. + eapply transl_expr_charact; eauto 3 with rtlg. apply tr_exprlist_incr with s4; auto. - eapply transl_exprlist_charact; eauto with rtlg. + eapply transl_exprlist_charact; eauto 4 with rtlg. (* Sseq *) econstructor. apply tr_stmt_incr with s0; auto. |