From 4d542bc7eafadb16b845cf05d1eb4988eb55ed0f Mon Sep 17 00:00:00 2001 From: Bernhard Schommer Date: Tue, 20 Oct 2015 13:32:18 +0200 Subject: Updated PR by removing whitespaces. Bug 17450. --- backend/Selectionproof.v | 236 +++++++++++++++++++++++------------------------ 1 file changed, 118 insertions(+), 118 deletions(-) (limited to 'backend/Selectionproof.v') diff --git a/backend/Selectionproof.v b/backend/Selectionproof.v index 8ea4c56e..8051df59 100644 --- a/backend/Selectionproof.v +++ b/backend/Selectionproof.v @@ -53,20 +53,20 @@ Hypothesis TRANSFPROG: transform_partial_program (sel_fundef hf ge) prog = OK tp Lemma symbols_preserved: forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s. Proof. - intros. eapply Genv.find_symbol_transf_partial; eauto. + intros. eapply Genv.find_symbol_transf_partial; eauto. Qed. Lemma public_preserved: forall (s: ident), Genv.public_symbol tge s = Genv.public_symbol ge s. Proof. - intros. eapply Genv.public_symbol_transf_partial; eauto. + intros. eapply Genv.public_symbol_transf_partial; eauto. Qed. Lemma function_ptr_translated: forall (b: block) (f: Cminor.fundef), Genv.find_funct_ptr ge b = Some f -> exists tf, Genv.find_funct_ptr tge b = Some tf /\ sel_fundef hf ge f = OK tf. -Proof. +Proof. intros. eapply Genv.find_funct_ptr_transf_partial; eauto. Qed. @@ -75,7 +75,7 @@ Lemma functions_translated: Genv.find_funct ge v = Some f -> Val.lessdef v v' -> exists tf, Genv.find_funct tge v' = Some tf /\ sel_fundef hf ge f = OK tf. -Proof. +Proof. intros. inv H0. eapply Genv.find_funct_transf_partial; eauto. simpl in H. discriminate. @@ -84,13 +84,13 @@ Qed. Lemma sig_function_translated: forall f tf, sel_fundef hf ge f = OK tf -> funsig tf = Cminor.funsig f. Proof. - intros. destruct f; monadInv H; auto. monadInv EQ. auto. + intros. destruct f; monadInv H; auto. monadInv EQ. auto. Qed. Lemma stackspace_function_translated: forall f tf, sel_function hf ge f = OK tf -> fn_stackspace tf = Cminor.fn_stackspace f. Proof. - intros. monadInv H. auto. + intros. monadInv H. auto. Qed. Lemma varinfo_preserved: @@ -103,14 +103,14 @@ Lemma helper_declared_preserved: forall id name sg, helper_declared ge id name sg -> helper_declared tge id name sg. Proof. intros id name sg (b & A & B). - 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 b; split; auto. rewrite symbols_preserved. auto. Qed. Let HELPERS': helper_functions_declared tge hf. Proof. red in HELPERS; decompose [Logic.and] HELPERS. - red. auto 20 using helper_declared_preserved. + red. auto 20 using helper_declared_preserved. Qed. Section CMCONSTR. @@ -127,15 +127,15 @@ Lemma eval_condexpr_of_expr: Proof. intros until a. functional induction (condexpr_of_expr a); intros. (* compare *) - inv H. econstructor; eauto. + inv H. econstructor; eauto. simpl in H6. inv H6. apply Val.bool_of_val_of_optbool. auto. (* condition *) inv H. econstructor; eauto. destruct va; eauto. (* let *) inv H. econstructor; eauto. (* default *) - econstructor. constructor. eauto. constructor. - simpl. inv H0. auto. + econstructor. constructor. eauto. constructor. + simpl. inv H0. auto. Qed. Lemma eval_load: @@ -145,10 +145,10 @@ Lemma eval_load: eval_expr tge sp e m le (load chunk a) v'. Proof. intros. generalize H0; destruct v; simpl; intro; try discriminate. - unfold load. + unfold load. generalize (eval_addressing _ _ _ _ _ chunk _ _ _ _ H (refl_equal _)). - destruct (addressing chunk a). intros [vl [EV EQ]]. - eapply eval_Eload; eauto. + destruct (addressing chunk a). intros [vl [EV EQ]]. + eapply eval_Eload; eauto. Qed. Lemma eval_store: @@ -162,8 +162,8 @@ Proof. intros. generalize H1; destruct v1; simpl; intro; try discriminate. unfold store. generalize (eval_addressing _ _ _ _ _ chunk _ _ _ _ H (refl_equal _)). - destruct (addressing chunk a1). intros [vl [EV EQ]]. - eapply step_store; eauto. + destruct (addressing chunk a1). intros [vl [EV EQ]]. + eapply step_store; eauto. Qed. (** Correctness of instruction selection for operators *) @@ -269,7 +269,7 @@ Lemma expr_is_addrof_ident_correct: expr_is_addrof_ident e = Some id -> e = Cminor.Econst (Cminor.Oaddrsymbol id Int.zero). Proof. - intros e id. unfold expr_is_addrof_ident. + intros e id. unfold expr_is_addrof_ident. destruct e; try congruence. destruct c; try congruence. predSpec Int.eq Int.eq_spec i0 Int.zero; congruence. @@ -285,14 +285,14 @@ Lemma classify_call_correct: | Call_builtin ef => fd = External ef end. Proof. - unfold classify_call; intros. - destruct (expr_is_addrof_ident a) as [id|] eqn:?. + unfold classify_call; intros. + destruct (expr_is_addrof_ident a) as [id|] eqn:?. exploit expr_is_addrof_ident_correct; eauto. intros EQ; subst a. - inv H. inv H2. - destruct (Genv.find_symbol ge id) as [b|] eqn:?. - rewrite Genv.find_funct_find_funct_ptr in H0. - rewrite H0. - destruct fd. exists b; auto. + inv H. inv H2. + destruct (Genv.find_symbol ge id) as [b|] eqn:?. + rewrite Genv.find_funct_find_funct_ptr in H0. + rewrite H0. + destruct fd. exists b; auto. destruct (ef_inline e0). auto. exists b; auto. simpl in H0. discriminate. auto. @@ -344,18 +344,18 @@ Proof. inv WF. assert (eval_expr tge sp e m le (make_cmp_eq (Eletvar arg) key) (Val.of_bool (zeq i key))). { eapply eval_make_cmp_eq; eauto. constructor; auto. } - eapply eval_XEcondition with (va := zeq i key). - eapply eval_condexpr_of_expr; eauto. destruct (zeq i key); constructor; auto. - destruct (zeq i key); simpl. + eapply eval_XEcondition with (va := zeq i key). + eapply eval_condexpr_of_expr; eauto. destruct (zeq i key); constructor; auto. + destruct (zeq i key); simpl. + inv MATCH. constructor. + eapply IHt; eauto. - (* lt test *) inv WF. assert (eval_expr tge sp e m le (make_cmp_ltu (Eletvar arg) key) (Val.of_bool (zlt i key))). { eapply eval_make_cmp_ltu; eauto. constructor; auto. } - eapply eval_XEcondition with (va := zlt i key). - eapply eval_condexpr_of_expr; eauto. destruct (zlt i key); constructor; auto. - destruct (zlt i key); simpl. + eapply eval_XEcondition with (va := zlt i key). + eapply eval_condexpr_of_expr; eauto. destruct (zlt i key); constructor; auto. + destruct (zlt i key); simpl. + eapply IHt1; eauto. + eapply IHt2; eauto. - (* jump table *) @@ -366,13 +366,13 @@ Proof. set (i' := (i - ofs) mod modulus) in *. assert (eval_expr tge sp e m (v' :: le) (make_cmp_ltu (Eletvar O) sz) (Val.of_bool (zlt i' sz))). { eapply eval_make_cmp_ltu; eauto. constructor; auto. } - econstructor. eauto. + econstructor. eauto. eapply eval_XEcondition with (va := zlt i' sz). eapply eval_condexpr_of_expr; eauto. destruct (zlt i' sz); constructor; auto. destruct (zlt i' sz); simpl. + exploit (eval_make_to_int sp e m (v' :: le) (Eletvar O)). - constructor. simpl; eauto. eauto. intros (v'' & C & D). inv D. - econstructor; eauto. congruence. + constructor. simpl; eauto. eauto. intros (v'' & C & D). inv D. + econstructor; eauto. congruence. + eapply IHt; eauto. Qed. @@ -398,37 +398,37 @@ Lemma sel_switch_int_correct: eval_expr tge sp e m le arg (Vint i) -> eval_exitexpr tge sp e m le (XElet arg (sel_switch_int O t)) (switch_target (Int.unsigned i) dfl cases). Proof. - assert (INTCONST: forall n sp e m le, + assert (INTCONST: forall n sp e m le, eval_expr tge sp e m le (Eop (Ointconst n) Enil) (Vint n)). - { intros. econstructor. constructor. auto. } + { intros. econstructor. constructor. auto. } intros. eapply sel_switch_correct with (R := Rint); eauto. - intros until n; intros EVAL R RANGE. - exploit eval_comp. eexact EVAL. apply (INTCONST (Int.repr n)). - instantiate (1 := Ceq). intros (vb & A & B). - inv R. unfold Val.cmp in B. simpl in B. revert B. - predSpec Int.eq Int.eq_spec n0 (Int.repr n); intros B; inv B. - rewrite Int.unsigned_repr. unfold proj_sumbool; rewrite zeq_true; auto. + exploit eval_comp. eexact EVAL. apply (INTCONST (Int.repr n)). + instantiate (1 := Ceq). intros (vb & A & B). + inv R. unfold Val.cmp in B. simpl in B. revert B. + predSpec Int.eq Int.eq_spec n0 (Int.repr n); intros B; inv B. + rewrite Int.unsigned_repr. unfold proj_sumbool; rewrite zeq_true; auto. unfold Int.max_unsigned; omega. unfold proj_sumbool; rewrite zeq_false; auto. red; intros; elim H1. rewrite <- (Int.repr_unsigned n0). congruence. - intros until n; intros EVAL R RANGE. - exploit eval_compu. eexact EVAL. apply (INTCONST (Int.repr n)). - instantiate (1 := Clt). intros (vb & A & B). + exploit eval_compu. eexact EVAL. apply (INTCONST (Int.repr n)). + instantiate (1 := Clt). intros (vb & A & B). inv R. unfold Val.cmpu in B. simpl in B. - unfold Int.ltu in B. rewrite Int.unsigned_repr in B. - destruct (zlt (Int.unsigned n0) n); inv B; auto. + unfold Int.ltu in B. rewrite Int.unsigned_repr in B. + destruct (zlt (Int.unsigned n0) n); inv B; auto. unfold Int.max_unsigned; omega. - intros until n; intros EVAL R RANGE. exploit eval_sub. eexact EVAL. apply (INTCONST (Int.repr n)). intros (vb & A & B). - inv R. simpl in B. inv B. econstructor; split; eauto. + inv R. simpl in B. inv B. econstructor; split; eauto. replace ((Int.unsigned n0 - n) mod Int.modulus) with (Int.unsigned (Int.sub n0 (Int.repr n))). constructor. - unfold Int.sub. rewrite Int.unsigned_repr_eq. f_equal. f_equal. + unfold Int.sub. rewrite Int.unsigned_repr_eq. f_equal. f_equal. apply Int.unsigned_repr. unfold Int.max_unsigned; omega. -- intros until i0; intros EVAL R. exists v; split; auto. +- intros until i0; intros EVAL R. exists v; split; auto. inv R. rewrite Zmod_small by (apply Int.unsigned_range). constructor. -- constructor. +- constructor. - apply Int.unsigned_range. Qed. @@ -441,30 +441,30 @@ Proof. intros. eapply sel_switch_correct with (R := Rlong); eauto. - intros until n; intros EVAL R RANGE. eapply eval_cmpl. eexact EVAL. apply eval_longconst with (n := Int64.repr n). - inv R. unfold Val.cmpl. simpl. f_equal; f_equal. unfold Int64.eq. - rewrite Int64.unsigned_repr. destruct (zeq (Int64.unsigned n0) n); auto. + inv R. unfold Val.cmpl. simpl. f_equal; f_equal. unfold Int64.eq. + rewrite Int64.unsigned_repr. destruct (zeq (Int64.unsigned n0) n); auto. unfold Int64.max_unsigned; omega. -- intros until n; intros EVAL R RANGE. +- intros until n; intros EVAL R RANGE. eapply eval_cmplu. eexact EVAL. apply eval_longconst with (n := Int64.repr n). - inv R. unfold Val.cmplu. simpl. f_equal; f_equal. unfold Int64.ltu. - rewrite Int64.unsigned_repr. destruct (zlt (Int64.unsigned n0) n); auto. + inv R. unfold Val.cmplu. simpl. f_equal; f_equal. unfold Int64.ltu. + rewrite Int64.unsigned_repr. destruct (zlt (Int64.unsigned n0) n); auto. unfold Int64.max_unsigned; omega. - intros until n; intros EVAL R RANGE. exploit eval_subl. eexact EVAL. apply eval_longconst with (n := Int64.repr n). intros (vb & A & B). - inv R. simpl in B. inv B. econstructor; split; eauto. + inv R. simpl in B. inv B. econstructor; split; eauto. replace ((Int64.unsigned n0 - n) mod Int64.modulus) with (Int64.unsigned (Int64.sub n0 (Int64.repr n))). constructor. - unfold Int64.sub. rewrite Int64.unsigned_repr_eq. f_equal. f_equal. + unfold Int64.sub. rewrite Int64.unsigned_repr_eq. f_equal. f_equal. apply Int64.unsigned_repr. unfold Int64.max_unsigned; omega. -- intros until i0; intros EVAL R. - exploit eval_lowlong. eexact EVAL. intros (vb & A & B). +- intros until i0; intros EVAL R. + exploit eval_lowlong. eexact EVAL. intros (vb & A & B). inv R. simpl in B. inv B. econstructor; split; eauto. replace (Int64.unsigned n mod Int.modulus) with (Int.unsigned (Int64.loword n)). constructor. - unfold Int64.loword. apply Int.unsigned_repr_eq. -- constructor. + unfold Int64.loword. apply Int.unsigned_repr_eq. +- constructor. - apply Int64.unsigned_range. Qed. @@ -481,24 +481,24 @@ Lemma eval_unop_lessdef: eval_unop op v1 = Some v -> Val.lessdef v1 v1' -> exists v', eval_unop op v1' = Some v' /\ Val.lessdef v v'. Proof. - intros until v; intros EV LD. inv LD. + intros until v; intros EV LD. inv LD. exists v; auto. destruct op; simpl in *; inv EV; TrivialExists. Qed. Lemma eval_binop_lessdef: forall op v1 v1' v2 v2' v m m', - eval_binop op v1 v2 m = Some v -> + eval_binop op v1 v2 m = Some v -> Val.lessdef v1 v1' -> Val.lessdef v2 v2' -> Mem.extends m m' -> exists v', eval_binop op v1' v2' m' = Some v' /\ Val.lessdef v v'. Proof. intros until m'; intros EV LD1 LD2 ME. assert (exists v', eval_binop op v1' v2' m = Some v' /\ Val.lessdef v v'). - inv LD1. inv LD2. exists v; auto. + inv LD1. inv LD2. exists v; auto. destruct op; destruct v1'; simpl in *; inv EV; TrivialExists. destruct op; simpl in *; inv EV; TrivialExists. - destruct op; try (exact H). - simpl in *. TrivialExists. inv EV. apply Val.of_optbool_lessdef. + destruct op; try (exact H). + simpl in *. TrivialExists. inv EV. apply Val.of_optbool_lessdef. intros. apply Val.cmpu_bool_lessdef with (Mem.valid_pointer m) v1 v2; auto. intros; eapply Mem.valid_pointer_extends; eauto. Qed. @@ -529,7 +529,7 @@ Proof. Qed. Lemma set_params_lessdef: - forall il vl1 vl2, + forall il vl1 vl2, Val.lessdef_list vl1 vl2 -> env_lessdef (set_params vl1 il) (set_params vl2 il). Proof. @@ -558,10 +558,10 @@ Proof. (* Evar *) exploit H0; eauto. intros [v' [A B]]. exists v'; split; auto. constructor; auto. (* Econst *) - destruct cst; simpl in *; inv H. - exists (Vint i); split; auto. econstructor. constructor. auto. + destruct cst; simpl in *; inv H. + exists (Vint i); split; auto. econstructor. constructor. auto. exists (Vfloat f); split; auto. econstructor. constructor. auto. - exists (Vsingle f); split; auto. econstructor. constructor. auto. + exists (Vsingle f); split; auto. econstructor. constructor. auto. exists (Val.longofwords (Vint (Int64.hiword i)) (Vint (Int64.loword i))); split. eapply eval_Eop. constructor. EvalOp. simpl; eauto. constructor. EvalOp. simpl; eauto. constructor. auto. simpl. rewrite Int64.ofwords_recompose. auto. @@ -571,13 +571,13 @@ Proof. exploit IHeval_expr; eauto. intros [v1' [A B]]. exploit eval_unop_lessdef; eauto. intros [v' [C D]]. exploit eval_sel_unop; eauto. intros [v'' [E F]]. - exists v''; split; eauto. eapply Val.lessdef_trans; eauto. + exists v''; split; eauto. eapply Val.lessdef_trans; eauto. (* Ebinop *) exploit IHeval_expr1; eauto. intros [v1' [A B]]. exploit IHeval_expr2; eauto. intros [v2' [C D]]. exploit eval_binop_lessdef; eauto. intros [v' [E F]]. exploit eval_sel_binop. eexact A. eexact C. eauto. intros [v'' [P Q]]. - exists v''; split; eauto. eapply Val.lessdef_trans; eauto. + exists v''; split; eauto. eapply Val.lessdef_trans; eauto. (* Eload *) exploit IHeval_expr; eauto. intros [vaddr' [A B]]. exploit Mem.loadv_extends; eauto. intros [v' [C D]]. @@ -591,7 +591,7 @@ Lemma sel_exprlist_correct: env_lessdef e e' -> Mem.extends m m' -> exists v', eval_exprlist tge sp e' m' le (sel_exprlist hf a) v' /\ Val.lessdef_list v v'. Proof. - induction 1; intros; simpl. + induction 1; intros; simpl. exists (@nil val); split; auto. constructor. exploit sel_expr_correct; eauto. intros [v1' [A B]]. exploit IHeval_exprlist; eauto. intros [vl' [C D]]. @@ -606,7 +606,7 @@ Lemma sel_builtin_arg_correct: CminorSel.eval_builtin_arg tge sp e' m' (sel_builtin_arg hf a c) v' /\ Val.lessdef v v'. Proof. - intros. unfold sel_builtin_arg. + intros. unfold sel_builtin_arg. exploit sel_expr_correct; eauto. intros (v1 & A & B). exists v1; split; auto. destruct (builtin_arg_ok (builtin_arg (sel_expr hf a)) c). @@ -627,7 +627,7 @@ Lemma sel_builtin_args_correct: /\ Val.lessdef_list vl vl'. Proof. induction 3; intros; simpl. -- exists (@nil val); split; constructor. +- exists (@nil val); split; constructor. - exploit sel_builtin_arg_correct; eauto. intros (v1' & A & B). edestruct IHeval_exprlist as (vl' & C & D). exists (v1' :: vl'); split; auto. constructor; eauto. @@ -638,7 +638,7 @@ Lemma sel_builtin_res_correct: env_lessdef e e' -> Val.lessdef v v' -> env_lessdef (set_optvar oid v e) (set_builtin_res (sel_builtin_res oid) v' e'). Proof. - intros. destruct oid; simpl; auto. apply set_var_lessdef; auto. + intros. destruct oid; simpl; auto. apply set_var_lessdef; auto. Qed. (** Semantic preservation for functions and statements. *) @@ -727,12 +727,12 @@ Proof. (* tailcall *) destruct (classify_call ge e); simpl; auto. (* seq *) - exploit (IHs1 (Cminor.Kseq s2 k)). constructor; eauto. eauto. + exploit (IHs1 (Cminor.Kseq s2 k)). constructor; eauto. eauto. destruct (Cminor.find_label lbl s1 (Cminor.Kseq s2 k)) as [[sx kx] | ]; destruct (find_label lbl x (Kseq x0 k')) as [[sy ky] | ]; intuition. apply IHs2; auto. (* ifthenelse *) - exploit (IHs1 k); eauto. + exploit (IHs1 k); eauto. destruct (Cminor.find_label lbl s1 k) as [[sx kx] | ]; destruct (find_label lbl x k') as [[sy ky] | ]; intuition. apply IHs2; auto. @@ -741,7 +741,7 @@ Proof. (* block *) apply IHs. constructor; auto. auto. (* switch *) - destruct b. + destruct b. destruct (validate_switch Int64.modulus n l (compile_switch Int64.modulus n l)); inv SE. simpl; auto. destruct (validate_switch Int.modulus n l (compile_switch Int.modulus n l)); inv SE. @@ -772,10 +772,10 @@ Proof. inv MC. left; econstructor; split. econstructor. constructor; auto. - (* skip call *) exploit Mem.free_parallel_extends; eauto. intros [m2' [A B]]. - left; econstructor; split. - econstructor. inv MC; simpl in H; simpl; auto. - eauto. - erewrite stackspace_function_translated; eauto. + left; econstructor; split. + econstructor. inv MC; simpl in H; simpl; auto. + eauto. + erewrite stackspace_function_translated; eauto. constructor; auto. - (* assign *) exploit sel_expr_correct; eauto. intros [v' [A B]]. @@ -790,18 +790,18 @@ Proof. eapply eval_store; eauto. constructor; auto. - (* Scall *) - exploit classify_call_correct; eauto. + exploit classify_call_correct; eauto. destruct (classify_call ge a) as [ | id | ef]. + (* indirect *) exploit sel_expr_correct; eauto. intros [vf' [A B]]. exploit sel_exprlist_correct; eauto. intros [vargs' [C D]]. exploit functions_translated; eauto. intros (fd' & U & V). left; econstructor; split. - econstructor; eauto. econstructor; eauto. + econstructor; eauto. econstructor; eauto. apply sig_function_translated; auto. constructor; auto. constructor; auto. + (* direct *) - intros [b [U V]]. + intros [b [U V]]. exploit sel_exprlist_correct; eauto. intros [vargs' [C D]]. exploit functions_translated; eauto. intros (fd' & X & Y). left; econstructor; split. @@ -812,7 +812,7 @@ Proof. + (* turned into Sbuiltin *) intros EQ. subst fd. exploit sel_builtin_args_correct; eauto. intros [vargs' [C D]]. - right; split. simpl. omega. split. auto. + right; split. simpl. omega. split. auto. econstructor; eauto. - (* Stailcall *) exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]]. @@ -821,21 +821,21 @@ Proof. exploit sel_exprlist_correct; eauto. intros [vargs' [C D]]. exploit functions_translated; eauto. intros [fd' [E F]]. left; econstructor; split. - exploit classify_call_correct; eauto. - destruct (classify_call ge a) as [ | id | ef]; intros. + exploit classify_call_correct; eauto. + destruct (classify_call ge a) as [ | id | ef]; intros. econstructor; eauto. econstructor; eauto. apply sig_function_translated; auto. - destruct H2 as [b [U V]]. subst vf. inv B. + destruct H2 as [b [U V]]. subst vf. inv B. econstructor; eauto. econstructor; eauto. rewrite symbols_preserved; eauto. apply sig_function_translated; auto. econstructor; eauto. econstructor; eauto. apply sig_function_translated; auto. constructor; auto. apply call_cont_commut; auto. - (* Sbuiltin *) exploit sel_builtin_args_correct; eauto. intros [vargs' [P Q]]. - exploit external_call_mem_extends; eauto. + exploit external_call_mem_extends; eauto. intros [vres' [m2 [A [B [C D]]]]]. left; econstructor; split. econstructor. eauto. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. - constructor; auto. apply sel_builtin_res_correct; auto. + constructor; auto. apply sel_builtin_res_correct; auto. - (* Seq *) left; econstructor; split. constructor. constructor; auto. constructor; auto. @@ -843,7 +843,7 @@ Proof. exploit sel_expr_correct; eauto. intros [v' [A B]]. assert (Val.bool_of_val v' b). inv B. auto. inv H0. left; exists (State f' (if b then x else x0) k' sp e' m'); split. - econstructor; eauto. eapply eval_condexpr_of_expr; eauto. + econstructor; eauto. eapply eval_condexpr_of_expr; eauto. constructor; auto. destruct b; auto. - (* Sloop *) left; econstructor; split. constructor. constructor; auto. @@ -861,26 +861,26 @@ Proof. + set (ct := compile_switch Int.modulus default cases) in *. destruct (validate_switch Int.modulus default cases ct) eqn:VALID; inv TS. exploit sel_expr_correct; eauto. intros [v' [A B]]. inv B. - left; econstructor; split. - econstructor. eapply sel_switch_int_correct; eauto. + left; econstructor; split. + econstructor. eapply sel_switch_int_correct; eauto. constructor; auto. + set (ct := compile_switch Int64.modulus default cases) in *. destruct (validate_switch Int64.modulus default cases ct) eqn:VALID; inv TS. exploit sel_expr_correct; eauto. intros [v' [A B]]. inv B. left; econstructor; split. - econstructor. eapply sel_switch_long_correct; eauto. + econstructor. eapply sel_switch_long_correct; eauto. constructor; auto. - (* Sreturn None *) exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]]. erewrite <- stackspace_function_translated in P by eauto. - left; econstructor; split. - econstructor. simpl; eauto. + left; econstructor; split. + econstructor. simpl; eauto. constructor; auto. apply call_cont_commut; auto. - (* Sreturn Some *) exploit Mem.free_parallel_extends; eauto. intros [m2' [P Q]]. erewrite <- stackspace_function_translated in P by eauto. exploit sel_expr_correct; eauto. intros [v' [A B]]. - left; econstructor; split. + left; econstructor; split. econstructor; eauto. constructor; auto. apply call_cont_commut; auto. - (* Slabel *) @@ -890,39 +890,39 @@ Proof. { monadInv TF; simpl; auto. } exploit (find_label_commut lbl (Cminor.fn_body f) (Cminor.call_cont k)). apply call_cont_commut; eauto. eauto. - rewrite H. + rewrite H. destruct (find_label lbl (fn_body f') (call_cont k'0)) as [[s'' k'']|] eqn:?; intros; try contradiction. - destruct H1. + destruct H1. left; econstructor; split. - econstructor; eauto. + econstructor; eauto. constructor; auto. - (* internal function *) monadInv TF. generalize EQ; intros TF; monadInv TF. - exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. + exploit Mem.alloc_extends. eauto. eauto. apply Zle_refl. apply Zle_refl. intros [m2' [A B]]. left; econstructor; split. econstructor; simpl; eauto. constructor; simpl; auto. apply set_locals_lessdef. apply set_params_lessdef; auto. - (* external call *) monadInv TF. - exploit external_call_mem_extends; eauto. + exploit external_call_mem_extends; eauto. intros [vres' [m2 [A [B [C D]]]]]. left; econstructor; split. econstructor. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. constructor; auto. - (* external call turned into a Sbuiltin *) - exploit external_call_mem_extends; eauto. + exploit external_call_mem_extends; eauto. intros [vres' [m2 [A [B [C D]]]]]. left; econstructor; split. econstructor. eauto. eapply external_call_symbols_preserved; eauto. exact symbols_preserved. exact public_preserved. exact varinfo_preserved. constructor; auto. - (* return *) - inv MC. - left; econstructor; split. - econstructor. + inv MC. + left; econstructor; split. + econstructor. constructor; auto. destruct optid; simpl; auto. apply set_var_lessdef; auto. - (* return of an external call turned into a Sbuiltin *) right; split. simpl; omega. split. auto. constructor; auto. @@ -975,20 +975,20 @@ Proof. - auto. - apply IHgl. red. destruct a as [id1 gd1]; simpl; intros. unfold Genv.find_symbol; simpl. rewrite PTree.gsspec. destruct (peq id id1). - + subst id1. exists (Genv.genv_next ge); split; auto. + + subst id1. exists (Genv.genv_next ge); split; auto. replace gd1 with (@Gfun Cminor.fundef unit fd). - unfold Genv.find_funct_ptr; simpl. apply PTree.gss. + unfold Genv.find_funct_ptr; simpl. apply PTree.gss. destruct (globdef_of_interest gd1). rewrite PTree.gss in H0; congruence. rewrite PTree.grs in H0; congruence. + assert (m!id = Some (Gfun fd)). - { destruct (globdef_of_interest gd1). + { destruct (globdef_of_interest gd1). rewrite PTree.gso in H0; auto. rewrite PTree.gro in H0; auto. } exploit H; eauto. intros (b & A & B). exists b; split; auto. unfold Genv.find_funct_ptr; simpl. - destruct gd1; auto. rewrite PTree.gso; auto. - apply Plt_ne. eapply Genv.genv_symb_range; eauto. + destruct gd1; auto. rewrite PTree.gso; auto. + apply Plt_ne. eapply Genv.genv_symb_range; eauto. } eapply REC. red; intros. rewrite PTree.gempty in H; discriminate. Qed. @@ -1002,19 +1002,19 @@ Proof. set (P := fun (m: PTree.t globdef) res => res = Some id -> m!id = Some(Gfun(External (EF_external name sg)))). assert (P globs (PTree.fold (lookup_helper_aux name sg) globs None)). { apply PTree_Properties.fold_rec; red; intros. - - rewrite <- H0. apply H1; auto. + - rewrite <- H0. apply H1; auto. - discriminate. - assert (EITHER: k = id /\ v = Gfun (External (EF_external name sg)) \/ a = Some id). - { unfold lookup_helper_aux in H3. destruct v; auto. destruct f; auto. destruct e; auto. + { unfold lookup_helper_aux in H3. destruct v; auto. destruct f; auto. destruct e; auto. destruct (String.string_dec name name0); auto. destruct (signature_eq sg sg0); auto. inversion H3. left; split; auto. repeat f_equal; auto. } destruct EITHER as [[X Y] | X]. - subst k v. apply PTree.gss. + subst k v. apply PTree.gss. apply H2 in X. rewrite PTree.gso by congruence. auto. } - red in H0. unfold lookup_helper in H. + red in H0. unfold lookup_helper in H. destruct (PTree.fold (lookup_helper_aux name sg) globs None); inv H. auto. Qed. @@ -1040,11 +1040,11 @@ Theorem transf_program_correct: sel_program prog = OK tprog -> forward_simulation (Cminor.semantics prog) (CminorSel.semantics tprog). Proof. - intros. unfold sel_program in H. + intros. unfold sel_program in H. destruct (get_helpers prog) as [hf|] eqn:G; simpl in H; try discriminate. - apply forward_simulation_opt with (match_states := match_states prog tprog hf) (measure := measure). + apply forward_simulation_opt with (match_states := match_states prog tprog hf) (measure := measure). eapply public_preserved; eauto. apply sel_initial_states; auto. apply sel_final_states; auto. - apply sel_step_correct; auto. eapply get_helpers_correct; eauto. + apply sel_step_correct; auto. eapply get_helpers_correct; eauto. Qed. -- cgit