From f5bb397acd12292f6b41438778f2df7391d6f2fe Mon Sep 17 00:00:00 2001 From: Michael Schmidt Date: Wed, 14 Oct 2015 15:26:56 +0200 Subject: bug 17392: remove trailing whitespace in source files --- backend/RTLgenproof.v | 232 +++++++++++++++++++++++++------------------------- 1 file changed, 116 insertions(+), 116 deletions(-) (limited to 'backend/RTLgenproof.v') diff --git a/backend/RTLgenproof.v b/backend/RTLgenproof.v index 19f6f1f4..f458de8b 100644 --- a/backend/RTLgenproof.v +++ b/backend/RTLgenproof.v @@ -59,25 +59,25 @@ Qed. Lemma add_var_wf: forall s1 s2 map name r map' i, - add_var map name s1 = OK (r,map') s2 i -> + add_var map name s1 = OK (r,map') s2 i -> map_wf map -> map_valid map s1 -> map_wf map'. Proof. - intros. monadInv H. + intros. monadInv H. apply mk_map_wf; simpl. intros until r0. repeat rewrite PTree.gsspec. destruct (peq id1 name); destruct (peq id2 name). congruence. - intros. inv H. elimtype False. - apply valid_fresh_absurd with r0 s1. + intros. inv H. elimtype False. + apply valid_fresh_absurd with r0 s1. apply H1. left; exists id2; auto. eauto with rtlg. - intros. inv H2. elimtype False. - apply valid_fresh_absurd with r0 s1. + intros. inv H2. elimtype False. + apply valid_fresh_absurd with r0 s1. apply H1. left; exists id1; auto. eauto with rtlg. inv H0. eauto. intros until r0. rewrite PTree.gsspec. - destruct (peq id name). + destruct (peq id name). intros. inv H. apply valid_fresh_absurd with r0 s1. apply H1. right; auto. @@ -90,7 +90,7 @@ Lemma add_vars_wf: add_vars map names s1 = OK (rl,map') s2 i -> map_wf map -> map_valid map s1 -> map_wf map'. Proof. - induction names; simpl; intros; monadInv H. + induction names; simpl; intros; monadInv H. auto. exploit add_vars_valid; eauto. intros [A B]. eapply add_var_wf; eauto. @@ -174,7 +174,7 @@ Lemma match_env_update_temp: match_env map e le (rs#r <- v). Proof. intros. apply match_env_invariant with rs; auto. - intros. case (Reg.eq r r0); intro. + intros. case (Reg.eq r r0); intro. subst r0; contradiction. apply Regmap.gso; auto. Qed. @@ -200,7 +200,7 @@ Proof. exists r'; split. auto. rewrite PMap.gso; auto. red; intros. subst r'. elim n. eauto. erewrite list_map_exten. eauto. - intros. symmetry. apply PMap.gso. red; intros. subst x. eauto. + intros. symmetry. apply PMap.gso. red; intros. subst x. eauto. Qed. (** A variant of [match_env_update_var] where a variable is optionally @@ -214,8 +214,8 @@ Lemma match_env_update_dest: match_env map e le rs -> match_env map (set_optvar dst v e) le (rs#r <- tv). Proof. - intros. inv H1; simpl. - eapply match_env_update_temp; eauto. + intros. inv H1; simpl. + eapply match_env_update_temp; eauto. eapply match_env_update_var; eauto. Qed. Hint Resolve match_env_update_dest: rtlg. @@ -253,7 +253,7 @@ Lemma match_env_unbind_letvar: match_env (add_letvar map r) e (v :: le) rs -> match_env map e le rs. Proof. - unfold add_letvar; intros. inv H. simpl in *. + unfold add_letvar; intros. inv H. simpl in *. constructor. auto. inversion me_letvars0. auto. Qed. @@ -282,13 +282,13 @@ Lemma match_set_params_init_regs: Proof. induction il; intros. - inv H. split. apply match_env_empty. auto. intros. + inv H. split. apply match_env_empty. auto. intros. simpl. apply Regmap.gi. monadInv H. simpl. exploit add_vars_valid; eauto. apply init_mapping_valid. intros [A B]. exploit add_var_valid; eauto. intros [A' B']. clear B'. - monadInv EQ1. + monadInv EQ1. destruct H0 as [ | v1 tv1 vs tvs]. (* vl = nil *) destruct (IHil _ _ _ _ nil nil _ EQ) as [ME UNDEF]. constructor. inv ME. split. @@ -306,13 +306,13 @@ Proof. intros id v. repeat rewrite PTree.gsspec. destruct (peq id a); intros. subst a. inv H. inv H1. exists x1; split. auto. rewrite Regmap.gss. constructor. inv H1. eexists; eauto. - exploit me_vars0; eauto. intros [r' [C D]]. + exploit me_vars0; eauto. intros [r' [C D]]. exists r'; split. auto. rewrite Regmap.gso. auto. apply valid_fresh_different with s. apply B. left; exists id; auto. - eauto with rtlg. + eauto with rtlg. destruct (map_letvars x0). auto. simpl in me_letvars0. inversion me_letvars0. - intros. rewrite Regmap.gso. apply UNDEF. + intros. rewrite Regmap.gso. apply UNDEF. apply reg_fresh_decr with s2; eauto with rtlg. apply sym_not_equal. apply valid_fresh_different with s2; auto. Qed. @@ -330,15 +330,15 @@ Proof. inv H2. auto. - monadInv H2. - exploit IHil; eauto. intro. + monadInv H2. + exploit IHil; eauto. intro. monadInv EQ1. constructor. - intros id v. simpl. repeat rewrite PTree.gsspec. - destruct (peq id a). subst a. intro. + intros id v. simpl. repeat rewrite PTree.gsspec. + destruct (peq id a). subst a. intro. exists x1. split. auto. inv H3. constructor. eauto with rtlg. - intros. eapply me_vars; eauto. + intros. eapply me_vars; eauto. simpl. eapply me_letvars; eauto. Qed. @@ -406,7 +406,7 @@ Lemma sig_transl_function: Proof. intros until tf. unfold transl_fundef, transf_partial_fundef. case f; intro. - unfold transl_function. + unfold transl_function. destruct (reserve_labels (fn_body f0) (PTree.empty node, init_state)) as [ngoto s0]. case (transl_fun f0 ngoto s0); simpl; intros. discriminate. @@ -429,10 +429,10 @@ Lemma tr_move_correct: rs'#r2 = rs#r1 /\ (forall r, r <> r2 -> rs'#r = rs#r). Proof. - intros. inv H. + intros. inv H. exists rs; split. constructor. auto. - exists (rs#r2 <- (rs#r1)); split. - apply star_one. eapply exec_Iop. eauto. auto. + exists (rs#r2 <- (rs#r1)); split. + apply star_one. eapply exec_Iop. eauto. auto. split. apply Regmap.gss. intros; apply Regmap.gso; auto. Qed. @@ -475,7 +475,7 @@ Variable m: mem. We formalize this simulation property by the following predicate parameterized by the CminorSel evaluation (left arrow). *) -Definition transl_expr_prop +Definition transl_expr_prop (le: letenv) (a: expr) (v: val) : Prop := forall tm cs f map pr ns nd rd rs dst (MWF: map_wf map) @@ -489,7 +489,7 @@ Definition transl_expr_prop /\ (forall r, In r pr -> rs'#r = rs#r) /\ Mem.extends m tm'. -Definition transl_exprlist_prop +Definition transl_exprlist_prop (le: letenv) (al: exprlist) (vl: list val) : Prop := forall tm cs f map pr ns nd rl rs (MWF: map_wf map) @@ -503,7 +503,7 @@ Definition transl_exprlist_prop /\ (forall r, In r pr -> rs'#r = rs#r) /\ Mem.extends m tm'. -Definition transl_condexpr_prop +Definition transl_condexpr_prop (le: letenv) (a: condexpr) (v: bool) : Prop := forall tm cs f map pr ns ntrue nfalse rs (MWF: map_wf map) @@ -531,22 +531,22 @@ Lemma transl_expr_Evar_correct: Proof. intros; red; intros. inv TE. exploit match_env_find_var; eauto. intro EQ. - exploit tr_move_correct; eauto. intros [rs' [A [B C]]]. + exploit tr_move_correct; eauto. intros [rs' [A [B C]]]. exists rs'; exists tm; split. eauto. destruct H2 as [[D E] | [D E]]. (* optimized case *) subst r dst. simpl. assert (forall r, rs'#r = rs#r). - intros. destruct (Reg.eq r rd). subst r. auto. auto. + intros. destruct (Reg.eq r rd). subst r. auto. auto. split. eapply match_env_invariant; eauto. split. congruence. split; auto. (* general case *) split. apply match_env_invariant with (rs#rd <- (rs#r)). - apply match_env_update_dest; auto. - intros. rewrite Regmap.gsspec. destruct (peq r0 rd). congruence. auto. - split. congruence. + apply match_env_update_dest; auto. + intros. rewrite Regmap.gsspec. destruct (peq r0 rd). congruence. auto. + split. congruence. split. intros. apply C. intuition congruence. auto. Qed. @@ -560,7 +560,7 @@ Lemma transl_expr_Eop_correct: transl_expr_prop le (Eop op args) v. Proof. intros; red; intros. inv TE. -(* normal case *) +(* normal case *) exploit H0; eauto. intros [rs1 [tm1 [EX1 [ME1 [RR1 [RO1 EXT1]]]]]]. edestruct eval_operation_lessdef as [v' []]; eauto. exists (rs1#rd <- v'); exists tm1. @@ -599,13 +599,13 @@ Proof. apply eval_addressing_preserved. exact symbols_preserved. auto. traceEq. (* Match-env *) - split. eauto with rtlg. + split. eauto with rtlg. (* Result *) split. rewrite Regmap.gss. auto. (* Other regs *) split. intros. rewrite Regmap.gso. auto. intuition congruence. (* Mem *) - auto. + auto. Qed. Lemma transl_expr_Econdition_correct: @@ -618,7 +618,7 @@ Lemma transl_expr_Econdition_correct: transl_expr_prop le (Econdition a ifso ifnot) v. Proof. intros; red; intros; inv TE. - exploit H0; eauto. intros [rs1 [tm1 [EX1 [ME1 [OTHER1 EXT1]]]]]. + exploit H0; eauto. intros [rs1 [tm1 [EX1 [ME1 [OTHER1 EXT1]]]]]. assert (tr_expr f.(fn_code) map pr (if va then ifso else ifnot) (if va then ntrue else nfalse) nd rd dst). destruct va; auto. exploit H2; eauto. intros [rs2 [tm2 [EX2 [ME2 [RES2 [OTHER2 EXT2]]]]]]. @@ -643,10 +643,10 @@ Lemma transl_expr_Elet_correct: transl_expr_prop (v1 :: le) a2 v2 -> transl_expr_prop le (Elet a1 a2) v2. Proof. - intros; red; intros; inv TE. + intros; red; intros; inv TE. exploit H0; eauto. intros [rs1 [tm1 [EX1 [ME1 [RES1 [OTHER1 EXT1]]]]]]. assert (map_wf (add_letvar map r)). - eapply add_letvar_wf; eauto. + eapply add_letvar_wf; eauto. exploit H2; eauto. eapply match_env_bind_letvar; eauto. intros [rs2 [tm2 [EX2 [ME3 [RES2 [OTHER2 EXT2]]]]]]. exists rs2; exists tm2. @@ -673,9 +673,9 @@ Proof. (* Exec *) split. eexact EX1. (* Match-env *) - split. + split. destruct H2 as [[A B] | [A B]]. - subst r dst; simpl. + 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 <- (rs#r)). @@ -684,9 +684,9 @@ Proof. intros. rewrite Regmap.gsspec. destruct (peq r0 rd); auto. congruence. (* Result *) - split. rewrite RES1. eapply match_env_find_letvar; eauto. + split. rewrite RES1. eapply match_env_find_letvar; eauto. (* Other regs *) - split. intros. + split. intros. destruct H2 as [[A B] | [A B]]. destruct (Reg.eq r0 rd); subst; auto. apply OTHER1. intuition congruence. @@ -712,7 +712,7 @@ Lemma transl_expr_Ebuiltin_correct: Proof. intros; red; intros. inv TE. exploit H0; eauto. intros [rs1 [tm1 [EX1 [ME1 [RR1 [RO1 EXT1]]]]]]. - exploit external_call_mem_extends; eauto. + exploit external_call_mem_extends; eauto. intros [v' [tm2 [A [B [C [D E]]]]]]. exists (rs1#rd <- v'); exists tm2. (* Exec *) @@ -720,7 +720,7 @@ Proof. change (rs1#rd <- v') with (regmap_setres (BR rd) v' rs1). eapply exec_Ibuiltin; eauto. eapply eval_builtin_args_trivial. - eapply external_call_symbols_preserved; eauto. + eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. reflexivity. (* Match-env *) @@ -745,9 +745,9 @@ Lemma transl_expr_Eexternal_correct: Proof. intros; red; intros. inv TE. exploit H3; eauto. intros [rs1 [tm1 [EX1 [ME1 [RR1 [RO1 EXT1]]]]]]. - exploit external_call_mem_extends; eauto. + exploit external_call_mem_extends; eauto. intros [v' [tm2 [A [B [C [D E]]]]]]. - exploit function_ptr_translated; eauto. simpl. intros [tf [P Q]]. inv Q. + exploit function_ptr_translated; eauto. simpl. intros [tf [P Q]]. inv Q. exists (rs1#rd <- v'); exists tm2. (* Exec *) split. eapply star_trans. eexact EX1. @@ -756,7 +756,7 @@ Proof. eapply star_left. eapply exec_function_external. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. - apply star_one. apply exec_return. + apply star_one. apply exec_return. reflexivity. reflexivity. reflexivity. (* Match-env *) split. eauto with rtlg. @@ -794,7 +794,7 @@ Proof. exploit H2; eauto. intros [rs2 [tm2 [EX2 [ME2 [RES2 [OTHER2 EXT2]]]]]]. exists rs2; exists tm2. (* Exec *) - split. eapply star_trans. eexact EX1. eexact EX2. auto. + split. eapply star_trans. eexact EX1. eexact EX2. auto. (* Match-env *) split. assumption. (* Results *) @@ -803,7 +803,7 @@ Proof. auto. (* Other regs *) split. intros. transitivity (rs1#r). - apply OTHER2; auto. simpl; tauto. + apply OTHER2; auto. simpl; tauto. apply OTHER1; auto. (* Mem *) auto. @@ -816,16 +816,16 @@ Lemma transl_condexpr_CEcond_correct: eval_condition cond vl m = Some vb -> transl_condexpr_prop le (CEcond cond al) vb. Proof. - intros; red; intros. inv TE. + intros; red; intros. inv TE. exploit H0; eauto. intros [rs1 [tm1 [EX1 [ME1 [RES1 [OTHER1 EXT1]]]]]]. exists rs1; exists tm1. (* Exec *) - split. eapply plus_right. eexact EX1. eapply exec_Icond. eauto. + split. eapply plus_right. eexact EX1. eapply exec_Icond. eauto. eapply eval_condition_lessdef; eauto. auto. traceEq. (* Match-env *) split. assumption. (* Other regs *) - split. assumption. + split. assumption. (* Mem *) auto. Qed. @@ -838,7 +838,7 @@ Lemma transl_condexpr_CEcondition_correct: transl_condexpr_prop le (if va then b else c) v -> transl_condexpr_prop le (CEcondition a b c) v. Proof. - intros; red; intros. inv TE. + intros; red; intros. inv TE. exploit H0; eauto. intros [rs1 [tm1 [EX1 [ME1 [OTHER1 EXT1]]]]]. assert (tr_condition (fn_code f) map pr (if va then b else c) (if va then n2 else n3) ntrue nfalse). destruct va; auto. @@ -849,7 +849,7 @@ Proof. (* Match-env *) split. assumption. (* Other regs *) - split. intros. rewrite OTHER2; auto. + split. intros. rewrite OTHER2; auto. (* Mem *) auto. Qed. @@ -862,11 +862,11 @@ Lemma transl_condexpr_CElet_correct: transl_condexpr_prop (v1 :: le) b v2 -> transl_condexpr_prop le (CElet a b) v2. Proof. - intros; red; intros. inv TE. + intros; red; intros. inv TE. exploit H0; eauto. intros [rs1 [tm1 [EX1 [ME1 [RES1 [OTHER1 EXT1]]]]]]. assert (map_wf (add_letvar map r)). - eapply add_letvar_wf; eauto. - exploit H2; eauto. eapply match_env_bind_letvar; eauto. + eapply add_letvar_wf; eauto. + exploit H2; eauto. eapply match_env_bind_letvar; eauto. intros [rs2 [tm2 [EX2 [ME3 [OTHER2 EXT2]]]]]. exists rs2; exists tm2. (* Exec *) @@ -874,7 +874,7 @@ Proof. (* Match-env *) split. eapply match_env_unbind_letvar; eauto. (* Other regs *) - split. intros. rewrite OTHER2; auto. + split. intros. rewrite OTHER2; auto. (* Mem *) auto. Qed. @@ -950,7 +950,7 @@ Proof (** Exit expressions. *) -Definition transl_exitexpr_prop +Definition transl_exitexpr_prop (le: letenv) (a: exitexpr) (x: nat) : Prop := forall tm cs f map ns nexits rs (MWF: map_wf map) @@ -981,21 +981,21 @@ Proof. auto. - (* XEcondition *) exploit transl_condexpr_correct; eauto. intros (rs1 & tm1 & EXEC1 & ME1 & RES1 & EXT1). - exploit IHeval_exitexpr; eauto. + exploit IHeval_exitexpr; eauto. instantiate (2 := if va then n2 else n3). destruct va; eauto. intros (nd & rs2 & tm2 & EXEC2 & EXIT2 & ME2 & EXT2). - exists nd, rs2, tm2. + exists nd, rs2, tm2. split. eapply star_trans. apply plus_star. eexact EXEC1. eexact EXEC2. traceEq. auto. - (* XElet *) exploit transl_expr_correct; eauto. intros (rs1 & tm1 & EXEC1 & ME1 & RES1 & PRES1 & EXT1). assert (map_wf (add_letvar map r)). - eapply add_letvar_wf; eauto. + eapply add_letvar_wf; eauto. exploit IHeval_exitexpr; eauto. eapply match_env_bind_letvar; eauto. intros (nd & rs2 & tm2 & EXEC2 & EXIT2 & ME2 & EXT2). exists nd, rs2, tm2. - split. eapply star_trans. eexact EXEC1. eexact EXEC2. traceEq. - split. auto. + split. eapply star_trans. eexact EXEC1. eexact EXEC2. traceEq. + split. auto. split. eapply match_env_unbind_letvar; eauto. auto. Qed. @@ -1010,20 +1010,20 @@ Lemma eval_exprlist_append: Proof. induction al1; simpl; intros vl1 al2 vl2 E1 E2; inv E1. - auto. -- simpl. constructor; eauto. +- simpl. constructor; eauto. Qed. Lemma invert_eval_builtin_arg: forall a v, eval_builtin_arg ge sp e m a v -> - exists vl, + exists vl, eval_exprlist ge sp e m nil (exprlist_of_expr_list (params_of_builtin_arg a)) vl /\ Events.eval_builtin_arg ge (fun v => v) sp m (fst (convert_builtin_arg a vl)) v /\ (forall vl', convert_builtin_arg a (vl ++ vl') = (fst (convert_builtin_arg a vl), vl')). Proof. induction 1; simpl; econstructor; intuition eauto with evalexpr barg. - constructor. - constructor. + constructor. + constructor. repeat constructor. Qed. @@ -1040,7 +1040,7 @@ Proof. destruct IHlist_forall2 as (vl2 & D & E). exists (vl1 ++ vl2); split. apply eval_exprlist_append; auto. - rewrite C; simpl. constructor; auto. + rewrite C; simpl. constructor; auto. Qed. Lemma transl_eval_builtin_arg: @@ -1055,18 +1055,18 @@ Proof. induction a; simpl; intros until v; intros LD EV; try (now (inv EV; econstructor; eauto with barg)). - destruct rl; simpl in LD; inv LD; inv EV; simpl. - econstructor; eauto with barg. + econstructor; eauto with barg. exists (rs#p); intuition auto. constructor. - destruct (convert_builtin_arg a1 vl) as [a1' vl1] eqn:CV1; simpl in *. destruct (convert_builtin_arg a2 vl1) as [a2' vl2] eqn:CV2; simpl in *. destruct (convert_builtin_arg a1 rl) as [a1'' rl1] eqn:CV3; simpl in *. destruct (convert_builtin_arg a2 rl1) as [a2'' rl2] eqn:CV4; simpl in *. - inv EV. - exploit IHa1; eauto. rewrite CV1; simpl; eauto. + inv EV. + exploit IHa1; eauto. rewrite CV1; simpl; eauto. rewrite CV1, CV3; simpl. intros (v1' & A1 & B1 & C1). exploit IHa2. eexact C1. rewrite CV2; simpl; eauto. rewrite CV2, CV4; simpl. intros (v2' & A2 & B2 & C2). - exists (Val.longofwords v1' v2'); split. constructor; auto. + exists (Val.longofwords v1' v2'); split. constructor; auto. split; auto. apply Val.longofwords_lessdef; auto. Qed. @@ -1081,8 +1081,8 @@ Proof. induction al; simpl; intros until vl; intros LD EV. - inv EV. exists (@nil val); split; constructor. - destruct (convert_builtin_arg a vl1) as [a1' vl2] eqn:CV1; simpl in *. - inv EV. - exploit transl_eval_builtin_arg. eauto. instantiate (2 := a). rewrite CV1; simpl; eauto. + inv EV. + exploit transl_eval_builtin_arg. eauto. instantiate (2 := a). rewrite CV1; simpl; eauto. rewrite CV1; simpl. intros (v1' & A1 & B1 & C1). exploit IHal. eexact C1. eauto. intros (vl' & A2 & B2). destruct (convert_builtin_arg a rl) as [a1'' rl2]; simpl in *. @@ -1145,10 +1145,10 @@ Lemma lt_state_wf: well_founded lt_state. Proof. unfold lt_state. apply wf_inverse_image with (f := measure_state). - apply wf_lex_ord. apply lt_wf. apply lt_wf. + apply wf_lex_ord. apply lt_wf. apply lt_wf. Qed. -(** ** Semantic preservation for the translation of statements *) +(** ** Semantic preservation for the translation of statements *) (** The simulation diagram for the translation of statements and functions is a "star" diagram of the form: @@ -1180,7 +1180,7 @@ Inductive tr_fun (tf: function) (map: mapping) (f: CminorSel.function) tf.(fn_stacksize) = f.(fn_stackspace) -> tr_fun tf map f ngoto nret rret. -Inductive tr_cont: RTL.code -> mapping -> +Inductive tr_cont: RTL.code -> mapping -> CminorSel.cont -> node -> list node -> labelmap -> node -> option reg -> list RTL.stackframe -> Prop := | tr_Kseq: forall c map s k nd nexits ngoto nret rret cs n, @@ -1269,7 +1269,7 @@ Proof. (* seq *) caseEq (find_label lbl s1 (Kseq s2 k)); intros. inv H1. inv H2. eapply IHs1; eauto. econstructor; eauto. - inv H2. eapply IHs2; eauto. + inv H2. eapply IHs2; eauto. (* ifthenelse *) caseEq (find_label lbl s1 k); intros. inv H1. inv H2. eapply IHs1; eauto. @@ -1308,22 +1308,22 @@ Proof. econstructor; eauto. constructor. (* skip return *) - inv TS. + inv TS. assert ((fn_code tf)!ncont = Some(Ireturn rret) /\ match_stacks k cs). - inv TK; simpl in H; try contradiction; auto. + inv TK; simpl in H; try contradiction; auto. destruct H1. assert (fn_stacksize tf = fn_stackspace f). - inv TF. auto. + inv TF. auto. edestruct Mem.free_parallel_extends as [tm' []]; eauto. econstructor; split. left; apply plus_one. eapply exec_Ireturn. eauto. rewrite H3. eauto. constructor; auto. - + (* assign *) inv TS. - exploit transl_expr_correct; eauto. + exploit transl_expr_correct; eauto. intros [rs' [tm' [A [B [C [D E]]]]]]. econstructor; split. right; split. eauto. Lt_state. @@ -1367,8 +1367,8 @@ Proof. exploit functions_translated; eauto. intros [tf' [P Q]]. econstructor; split. left; eapply plus_right. eexact E. - eapply exec_Icall; eauto. simpl. rewrite symbols_preserved. rewrite H4. - rewrite Genv.find_funct_find_funct_ptr in P. eauto. + eapply exec_Icall; eauto. simpl. rewrite symbols_preserved. rewrite H4. + rewrite Genv.find_funct_find_funct_ptr in P. eauto. apply sig_transl_function; auto. traceEq. constructor; auto. econstructor; eauto. @@ -1400,19 +1400,19 @@ Proof. edestruct Mem.free_parallel_extends as [tm''' []]; eauto. econstructor; split. left; eapply plus_right. eexact E. - eapply exec_Itailcall; eauto. simpl. rewrite symbols_preserved. rewrite H5. - rewrite Genv.find_funct_find_funct_ptr in P. eauto. + eapply exec_Itailcall; eauto. simpl. rewrite symbols_preserved. rewrite H5. + rewrite Genv.find_funct_find_funct_ptr in P. eauto. apply sig_transl_function; auto. rewrite H; eauto. traceEq. constructor; auto. (* builtin *) - inv TS. + inv TS. exploit invert_eval_builtin_args; eauto. intros (vparams & P & Q). exploit transl_exprlist_correct; eauto. intros [rs' [tm' [E [F [G [J K]]]]]]. - exploit transl_eval_builtin_args; eauto. + exploit transl_eval_builtin_args; eauto. intros (vargs' & U & V). exploit (@eval_builtin_args_lessdef _ ge (fun r => rs'#r) (fun r => rs'#r)); eauto. intros (vargs'' & X & Y). @@ -1421,31 +1421,31 @@ Proof. econstructor; split. left. eapply plus_right. eexact E. eapply exec_Ibuiltin. eauto. - eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. + eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved. eapply external_call_symbols_preserved. eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. - traceEq. + traceEq. econstructor; eauto. constructor. eapply match_env_update_res; eauto. - + (* seq *) - inv TS. + inv TS. econstructor; split. right; split. apply star_refl. Lt_state. - econstructor; eauto. econstructor; eauto. + econstructor; eauto. econstructor; eauto. (* ifthenelse *) - inv TS. + inv TS. exploit transl_condexpr_correct; eauto. intros [rs' [tm' [A [B [C D]]]]]. econstructor; split. left. eexact A. - destruct b; econstructor; eauto. + destruct b; econstructor; eauto. (* loop *) inversion TS; subst. econstructor; split. - left. apply plus_one. eapply exec_Inop; eauto. - econstructor; eauto. + left. apply plus_one. eapply exec_Inop; eauto. + econstructor; eauto. econstructor; eauto. econstructor; eauto. @@ -1456,7 +1456,7 @@ Proof. econstructor; eauto. econstructor; eauto. (* exit seq *) - inv TS. inv TK. + inv TS. inv TK. econstructor; split. right; split. apply star_refl. Lt_state. econstructor; eauto. econstructor; eauto. @@ -1475,11 +1475,11 @@ Proof. (* switch *) inv TS. - exploit transl_exitexpr_correct; eauto. - intros (nd & rs' & tm' & A & B & C & D). + exploit transl_exitexpr_correct; eauto. + intros (nd & rs' & tm' & A & B & C & D). econstructor; split. - right; split. eexact A. Lt_state. - econstructor; eauto. constructor; auto. + right; split. eexact A. Lt_state. + econstructor; eauto. constructor; auto. (* return none *) inv TS. @@ -1511,11 +1511,11 @@ Proof. (* goto *) inv TS. inversion TF; subst. - exploit tr_find_label; eauto. eapply tr_cont_call_cont; eauto. + exploit tr_find_label; eauto. eapply tr_cont_call_cont; eauto. intros [ns2 [nd2 [nexits2 [A [B C]]]]]. econstructor; split. left; apply plus_one. eapply exec_Inop; eauto. - econstructor; eauto. + econstructor; eauto. (* internal call *) monadInv TF. exploit transl_function_charact; eauto. intro TRF. @@ -1536,19 +1536,19 @@ Proof. inversion MS; subst; econstructor; eauto. (* external call *) - monadInv TF. + monadInv TF. edestruct external_call_mem_extends as [tvres [tm' [A [B [C D]]]]]; eauto. econstructor; split. - left; apply plus_one. eapply exec_function_external; eauto. + left; apply plus_one. eapply exec_function_external; eauto. eapply external_call_symbols_preserved. eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. constructor; auto. (* return *) inv MS. - econstructor; split. - left; apply plus_one; constructor. - econstructor; eauto. constructor. + econstructor; split. + left; apply plus_one; constructor. + econstructor; eauto. constructor. eapply match_env_update_dest; eauto. Qed. @@ -1582,8 +1582,8 @@ Proof. eexact public_preserved. eexact transl_initial_states. eexact transl_final_states. - apply lt_state_wf. - exact transl_step_correct. + apply lt_state_wf. + exact transl_step_correct. Qed. End CORRECTNESS. -- cgit