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. --- cfrontend/Initializersproof.v | 162 +++++++++++++++++++++--------------------- 1 file changed, 81 insertions(+), 81 deletions(-) (limited to 'cfrontend/Initializersproof.v') diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v index 790877bd..3a7b5593 100644 --- a/cfrontend/Initializersproof.v +++ b/cfrontend/Initializersproof.v @@ -143,7 +143,7 @@ with eval_simple_rvalue: expr -> val -> Prop := eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some true -> eval_simple_rvalue (Eseqor r1 r2 ty) (Vint Int.one) | esr_condition: forall r1 r2 r3 ty v v1 b v', - eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some b -> + eval_simple_rvalue r1 v1 -> bool_val v1 (typeof r1) m = Some b -> eval_simple_rvalue (if b then r2 else r3) v' -> sem_cast v' (typeof (if b then r2 else r3)) ty = Some v -> eval_simple_rvalue (Econdition r1 r2 r3 ty) v @@ -190,7 +190,7 @@ Qed. Lemma rred_simple: forall r m t r' m', rred ge r m t r' m' -> simple r -> simple r'. Proof. - induction 1; simpl; intuition. destruct b; auto. + induction 1; simpl; intuition. destruct b; auto. Qed. Lemma rred_compat: @@ -199,20 +199,20 @@ Lemma rred_compat: m = m' /\ compat_eval RV e r r' m. Proof. intros until m'; intros RED SIMP. inv RED; simpl in SIMP; try contradiction; split; auto; split; auto; intros vx EV. - inv EV. econstructor. constructor. auto. auto. + inv EV. econstructor. constructor. auto. auto. inv EV. econstructor. constructor. - inv EV. econstructor; eauto. constructor. + inv EV. econstructor; eauto. constructor. inv EV. econstructor; eauto. constructor. constructor. inv EV. econstructor; eauto. constructor. inv EV. eapply esr_seqand_true; eauto. constructor. inv EV. eapply esr_seqand_false; eauto. constructor. inv EV. eapply esr_seqor_true; eauto. constructor. inv EV. eapply esr_seqor_false; eauto. constructor. - inv EV. eapply esr_condition; eauto. constructor. + inv EV. eapply esr_condition; eauto. constructor. inv EV. constructor. inv EV. constructor. econstructor; eauto. constructor. - inv EV. econstructor. constructor. auto. + inv EV. econstructor. constructor. auto. Qed. Lemma compat_eval_context: @@ -225,19 +225,19 @@ Proof. try (generalize (IHcontext CE); intros [TY EV]; red; split; simpl; auto; intros). inv H0. constructor; auto. inv H0. - eapply esl_field_struct; eauto. rewrite TY; eauto. + eapply esl_field_struct; eauto. rewrite TY; eauto. eapply esl_field_union; eauto. rewrite TY; eauto. inv H0. econstructor. eauto. auto. auto. - inv H0. econstructor; eauto. + inv H0. econstructor; eauto. inv H0. econstructor; eauto. congruence. inv H0. econstructor; eauto. congruence. inv H0. econstructor; eauto. congruence. inv H0. econstructor; eauto. congruence. - inv H0. - eapply esr_seqand_true; eauto. rewrite TY; auto. + inv H0. + eapply esr_seqand_true; eauto. rewrite TY; auto. eapply esr_seqand_false; eauto. rewrite TY; auto. - inv H0. - eapply esr_seqor_false; eauto. rewrite TY; auto. + inv H0. + eapply esr_seqor_false; eauto. rewrite TY; auto. eapply esr_seqor_true; eauto. rewrite TY; auto. inv H0. eapply esr_condition; eauto. congruence. inv H0. @@ -249,19 +249,19 @@ Proof. red; split; intros. auto. inv H0. red; split; intros. auto. inv H0. inv H0. econstructor; eauto. - inv H0. econstructor; eauto. congruence. + inv H0. econstructor; eauto. congruence. Qed. Lemma simple_context_1: forall a from to C, context from to C -> simple (C a) -> simple a. Proof. - induction 1; simpl; tauto. + induction 1; simpl; tauto. Qed. Lemma simple_context_2: forall a a', simple a' -> forall from to C, context from to C -> simple (C a) -> simple (C a'). Proof. - induction 2; simpl; try tauto. + induction 2; simpl; try tauto. Qed. Lemma compat_eval_steps_aux f r e m r' m' s2 : @@ -296,16 +296,16 @@ Qed. Lemma compat_eval_steps: forall f r e m r' m', star step ge (ExprState f r Kstop e m) E0 (ExprState f r' Kstop e m') -> - simple r -> + simple r -> m' = m /\ compat_eval RV e r r' m. Proof. - intros. + intros. remember (ExprState f r Kstop e m) as S1. remember E0 as t. remember (ExprState f r' Kstop e m') as S2. revert S1 t S2 H r m r' m' HeqS1 Heqt HeqS2 H0. induction 1; intros; subst. - (* base case *) + (* base case *) inv HeqS2. split. auto. red; auto. (* inductive case *) destruct (app_eq_nil t1 t2); auto. subst. inv H. @@ -313,7 +313,7 @@ Proof. exploit compat_eval_steps_aux; eauto. intros [r1 [A [B C]]]. subst s2. exploit IHstar; eauto. intros [D E]. - split. auto. destruct B; destruct E. split. congruence. auto. + split. auto. destruct B; destruct E. split. congruence. auto. (* statement steps *) inv H1. Qed. @@ -324,7 +324,7 @@ Theorem eval_simple_steps: simple r -> m' = m /\ ty = typeof r /\ eval_simple_rvalue e m r v. Proof. - intros. exploit compat_eval_steps; eauto. intros [A [B C]]. + intros. exploit compat_eval_steps; eauto. intros [A [B C]]. intuition. apply C. constructor. Qed. @@ -344,7 +344,7 @@ Lemma mem_empty_not_valid_pointer: forall b ofs, Mem.valid_pointer Mem.empty b ofs = false. Proof. intros. unfold Mem.valid_pointer. destruct (Mem.perm_dec Mem.empty b ofs Cur Nonempty); auto. - eelim Mem.perm_empty; eauto. + eelim Mem.perm_empty; eauto. Qed. Lemma mem_empty_not_weak_valid_pointer: @@ -362,7 +362,7 @@ Lemma sem_cast_match: Val.inject inj v2' v2. Proof. intros. unfold do_cast in H0. destruct (sem_cast v1' ty1 ty2) as [v2''|] eqn:E; inv H0. - exploit sem_cast_inject. eexact E. eauto. + exploit sem_cast_inject. eexact E. eauto. intros [v' [A B]]. congruence. Qed. @@ -395,14 +395,14 @@ Proof. (* val *) destruct v; monadInv CV; constructor. (* rval *) - inv H1; rewrite H2 in CV; try congruence. eauto. eauto. + inv H1; rewrite H2 in CV; try congruence. eauto. eauto. (* addrof *) eauto. (* unop *) destruct (sem_unary_operation op x (typeof r1) Mem.empty) as [v1'|] eqn:E; inv EQ0. exploit (sem_unary_operation_inj inj Mem.empty m). intros. rewrite mem_empty_not_weak_valid_pointer in H2; discriminate. - eexact E. eauto. + eexact E. eauto. intros [v' [A B]]. congruence. (* binop *) destruct (sem_binary_operation ge op x (typeof r1) x0 (typeof r2) Mem.empty) as [v1'|] eqn:E; inv EQ2. @@ -411,34 +411,34 @@ Proof. intros. rewrite mem_empty_not_weak_valid_pointer in H3; discriminate. intros. rewrite mem_empty_not_weak_valid_pointer in H3; discriminate. intros. rewrite mem_empty_not_valid_pointer in H3; discriminate. - eauto. eauto. eauto. + eauto. eauto. eauto. intros [v' [A B]]. congruence. (* cast *) - eapply sem_cast_match; eauto. + eapply sem_cast_match; eauto. (* sizeof *) constructor. (* alignof *) constructor. (* seqand *) - destruct (bool_val x (typeof r1) Mem.empty) as [b|] eqn:E; inv EQ2. + destruct (bool_val x (typeof r1) Mem.empty) as [b|] eqn:E; inv EQ2. exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'. assert (b = true) by congruence. subst b. eapply sem_cast_match; eauto. - destruct (bool_val x (typeof r1) Mem.empty) as [b|] eqn:E; inv EQ2. + destruct (bool_val x (typeof r1) Mem.empty) as [b|] eqn:E; inv EQ2. exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'. assert (b = false) by congruence. subst b. inv H2. auto. (* seqor *) - destruct (bool_val x (typeof r1) Mem.empty) as [b|] eqn:E; inv EQ2. + destruct (bool_val x (typeof r1) Mem.empty) as [b|] eqn:E; inv EQ2. exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'. - assert (b = false) by congruence. subst b. + assert (b = false) by congruence. subst b. eapply sem_cast_match; eauto. - destruct (bool_val x (typeof r1) Mem.empty) as [b|] eqn:E; inv EQ2. + destruct (bool_val x (typeof r1) Mem.empty) as [b|] eqn:E; inv EQ2. exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'. assert (b = true) by congruence. subst b. inv H2. auto. (* conditional *) destruct (bool_val x (typeof r1) Mem.empty) as [b'|] eqn:E; inv EQ3. exploit bool_val_match. eexact E. eauto. instantiate (1 := m). intros E'. - assert (b' = b) by congruence. subst b'. + assert (b' = b) by congruence. subst b'. destruct b; eapply sem_cast_match; eauto. (* comma *) auto. @@ -450,14 +450,14 @@ Proof. (* var local *) unfold empty_env in H. rewrite PTree.gempty in H. congruence. (* var_global *) - econstructor. unfold inj. rewrite H0. eauto. auto. + econstructor. unfold inj. rewrite H0. eauto. auto. (* deref *) eauto. (* field struct *) - rewrite H0 in CV. monadInv CV. unfold lookup_composite in EQ; rewrite H1 in EQ; monadInv EQ. + rewrite H0 in CV. monadInv CV. unfold lookup_composite in EQ; rewrite H1 in EQ; monadInv EQ. exploit constval_rvalue; eauto. intro MV. inv MV. - simpl. replace x0 with delta by congruence. econstructor; eauto. - rewrite ! Int.add_assoc. f_equal. apply Int.add_commut. + simpl. replace x0 with delta by congruence. econstructor; eauto. + rewrite ! Int.add_assoc. f_equal. apply Int.add_commut. simpl. auto. (* field union *) rewrite H0 in CV. eauto. @@ -481,7 +481,7 @@ Theorem constval_steps: constval ge r = OK v -> m' = m /\ ty = typeof r /\ Val.inject inj v v'. Proof. - intros. exploit eval_simple_steps; eauto. eapply constval_simple; eauto. + intros. exploit eval_simple_steps; eauto. eapply constval_simple; eauto. intros [A [B C]]. intuition. eapply constval_rvalue; eauto. Qed. @@ -498,33 +498,33 @@ Theorem transl_init_single_steps: Mem.store chunk m' b ofs v = Some m'' -> Genv.store_init_data ge m b ofs data = Some m''. Proof. - intros. monadInv H. + intros. monadInv H. exploit constval_steps; eauto. intros [A [B C]]. subst m' ty1. exploit sem_cast_match; eauto. intros D. - unfold Genv.store_init_data. - inv D. + unfold Genv.store_init_data. + inv D. (* int *) - destruct ty; try discriminate. + destruct ty; try discriminate. destruct i0; inv EQ2. destruct s; simpl in H2; inv H2. rewrite <- Mem.store_signed_unsigned_8; auto. auto. destruct s; simpl in H2; inv H2. rewrite <- Mem.store_signed_unsigned_16; auto. auto. simpl in H2; inv H2. assumption. - simpl in H2; inv H2. assumption. + simpl in H2; inv H2. assumption. inv EQ2. simpl in H2; inv H2. assumption. (* long *) destruct ty; inv EQ2. simpl in H2; inv H2. assumption. (* float *) - destruct ty; try discriminate. + destruct ty; try discriminate. destruct f1; inv EQ2; simpl in H2; inv H2; assumption. (* single *) - destruct ty; try discriminate. + destruct ty; try discriminate. destruct f1; inv EQ2; simpl in H2; inv H2; assumption. (* pointer *) unfold inj in H. assert (data = Init_addrof b1 ofs1 /\ chunk = Mint32). destruct ty; inv EQ2; inv H2. destruct i; inv H5. intuition congruence. auto. - destruct H4; subst. destruct (Genv.find_symbol ge b1); inv H. + destruct H4; subst. destruct (Genv.find_symbol ge b1); inv H. rewrite Int.add_zero in H3. auto. (* undef *) discriminate. @@ -537,9 +537,9 @@ Lemma transl_init_single_size: transl_init_single ge ty a = OK data -> Genv.init_data_size data = sizeof ge ty. Proof. - intros. monadInv H. destruct x0. + intros. monadInv H. destruct x0. - monadInv EQ2. -- destruct ty; try discriminate. +- destruct ty; try discriminate. destruct i0; inv EQ2; auto. inv EQ2; auto. - destruct ty; inv EQ2; auto. @@ -557,15 +557,15 @@ Notation idlsize := Genv.init_data_list_size. Remark padding_size: forall frm to, frm <= to -> idlsize (padding frm to) = to - frm. Proof. - unfold padding; intros. destruct (zlt frm to). - simpl. xomega. + unfold padding; intros. destruct (zlt frm to). + simpl. xomega. simpl. omega. Qed. Remark idlsize_app: forall d1 d2, idlsize (d1 ++ d2) = idlsize d1 + idlsize d2. Proof. - induction d1; simpl; intros. + induction d1; simpl; intros. auto. rewrite IHd1. omega. Qed. @@ -573,11 +573,11 @@ Qed. Remark union_field_size: forall f ty fl, field_type f fl = OK ty -> sizeof ge ty <= sizeof_union ge fl. Proof. - induction fl as [|[i t]]; simpl; intros. + induction fl as [|[i t]]; simpl; intros. - inv H. -- destruct (ident_eq f i). - + inv H. xomega. - + specialize (IHfl H). xomega. +- destruct (ident_eq f i). + + inv H. xomega. + + specialize (IHfl H). xomega. Qed. Hypothesis ce_consistent: composite_env_consistent ge. @@ -599,9 +599,9 @@ with transl_init_list_size: idlsize data + pos = sizeof ge ty). Proof. -- induction i; intros. +- induction i; intros. + (* single *) - monadInv H. simpl. erewrite transl_init_single_size by eauto. omega. + monadInv H. simpl. erewrite transl_init_single_size by eauto. omega. + (* array *) simpl in H. destruct ty; try discriminate. simpl. eapply (proj1 (transl_init_list_size il)); eauto. @@ -611,19 +611,19 @@ Proof. replace (idlsize data) with (idlsize data + 0) by omega. eapply (proj2 (transl_init_list_size il)). eauto. unfold lookup_composite in EQ. simpl. destruct (ge.(genv_cenv)!i) as [co|] eqn:?; inv EQ. - erewrite co_consistent_sizeof by (eapply ce_consistent; eauto). + erewrite co_consistent_sizeof by (eapply ce_consistent; eauto). unfold sizeof_composite. rewrite Heqs. apply align_le. destruct (co_alignof_two_p x) as [n EQ]. rewrite EQ. apply two_power_nat_pos. + (* union *) simpl in H. destruct ty; try discriminate. monadInv H. destruct (co_su x) eqn:?; try discriminate. - monadInv EQ0. + monadInv EQ0. rewrite idlsize_app. rewrite (IHi _ _ EQ0). unfold lookup_composite in EQ. simpl. destruct (ge.(genv_cenv)!i0) as [co|] eqn:?; inv EQ. rewrite padding_size. omega. - apply Zle_trans with (sizeof_union ge (co_members x)). + apply Zle_trans with (sizeof_union ge (co_members x)). eapply union_field_size; eauto. - erewrite co_consistent_sizeof by (eapply ce_consistent; eauto). + erewrite co_consistent_sizeof by (eapply ce_consistent; eauto). unfold sizeof_composite. rewrite Heqs. apply align_le. destruct (co_alignof_two_p x) as [n EQ]. rewrite EQ. apply two_power_nat_pos. @@ -631,9 +631,9 @@ Proof. + (* base cases *) simpl. intuition auto. * (* arrays *) - destruct (zeq sz 0). inv H. simpl; ring. - destruct (zle 0 sz); inv H. simpl. - rewrite Z.mul_comm. + destruct (zeq sz 0). inv H. simpl; ring. + destruct (zle 0 sz); inv H. simpl. + rewrite Z.mul_comm. assert (0 <= sizeof ge ty * sz). { apply Zmult_gt_0_le_0_compat. omega. generalize (sizeof_pos ge ty); omega. } zify; omega. @@ -645,17 +645,17 @@ Proof. * (* arrays *) intros. monadInv H. rewrite idlsize_app. - rewrite (transl_init_size _ _ _ EQ). + rewrite (transl_init_size _ _ _ EQ). rewrite (A _ _ _ EQ1). ring. * (* structs *) intros. simpl in H. destruct fl as [|[i1 t1]]; monadInv H. - rewrite ! idlsize_app. - simpl in H0. + rewrite ! idlsize_app. + simpl in H0. rewrite padding_size. - rewrite (transl_init_size _ _ _ EQ). + rewrite (transl_init_size _ _ _ EQ). rewrite <- (B _ _ _ _ EQ1). omega. - auto. apply align_le. apply alignof_pos. + auto. apply align_le. apply alignof_pos. Qed. (** A semantics for general initializers *) @@ -671,7 +671,7 @@ Fixpoint fields_of_struct (fl: members) (pos: Z) : list (Z * type) := Inductive exec_init: mem -> block -> Z -> type -> initializer -> mem -> Prop := | exec_init_single: forall m b ofs ty a v1 ty1 chunk m' v m'', - star step ge (ExprState dummy_function a Kstop empty_env m) + star step ge (ExprState dummy_function a Kstop empty_env m) E0 (ExprState dummy_function (Eval v1 ty1) Kstop empty_env m') -> sem_cast v1 ty1 ty = Some v -> access_mode ty = By_value chunk -> @@ -713,7 +713,7 @@ Scheme exec_init_ind3 := Minimality for exec_init Sort Prop Combined Scheme exec_init_scheme from exec_init_ind3, exec_init_array_ind3, exec_init_list_ind3. Remark exec_init_array_length: - forall m b ofs ty sz il m', + forall m b ofs ty sz il m', exec_init_array m b ofs ty sz il m' -> sz >= 0. Proof. induction 1; omega. @@ -725,7 +725,7 @@ Lemma store_init_data_list_app: Genv.store_init_data_list ge m' b (ofs + idlsize data1) data2 = Some m'' -> Genv.store_init_data_list ge m b ofs (data1 ++ data2) = Some m''. Proof. - induction data1; simpl; intros. + induction data1; simpl; intros. inv H. rewrite Zplus_0_r in H0. auto. destruct (Genv.store_init_data ge m b ofs a); try discriminate. rewrite Zplus_assoc in H0. eauto. @@ -735,7 +735,7 @@ Remark store_init_data_list_padding: forall frm to b ofs m, Genv.store_init_data_list ge m b ofs (padding frm to) = Some m. Proof. - intros. unfold padding. destruct (zlt frm to); auto. + intros. unfold padding. destruct (zlt frm to); auto. Qed. Lemma transl_init_sound_gen: @@ -757,33 +757,33 @@ Local Opaque sizeof. monadInv H3. simpl. erewrite transl_init_single_steps by eauto. auto. - (* array *) replace (Z.max 0 sz) with sz in H1. eauto. - assert (sz >= 0) by (eapply exec_init_array_length; eauto). xomega. + assert (sz >= 0) by (eapply exec_init_array_length; eauto). xomega. - (* struct *) - unfold lookup_composite in H3. rewrite H in H3. simpl in H3. rewrite H0 in H3. + unfold lookup_composite in H3. rewrite H in H3. simpl in H3. rewrite H0 in H3. replace ofs with (ofs + 0) by omega. eauto. - (* union *) - unfold lookup_composite in H4. rewrite H in H4. simpl in H4. rewrite H0 in H4. - monadInv H4. assert (x = ty) by congruence. subst x. + unfold lookup_composite in H4. rewrite H in H4. simpl in H4. rewrite H0 in H4. + monadInv H4. assert (x = ty) by congruence. subst x. eapply store_init_data_list_app. eauto. - apply store_init_data_list_padding. + apply store_init_data_list_padding. - (* array, empty *) destruct (zeq sz 0). inv H0. auto. rewrite zle_true in H0 by omega. inv H0. auto. - (* array, nonempty *) - monadInv H3. + monadInv H3. eapply store_init_data_list_app. eauto. rewrite (transl_init_size _ _ _ EQ). eauto. - (* struct, empty *) - destruct fl as [|[i t]]; simpl in H0; inv H0. + destruct fl as [|[i t]]; simpl in H0; inv H0. apply store_init_data_list_padding. - (* struct, nonempty *) destruct fl as [|[i t]]; simpl in H4; monadInv H4. simpl in H3; inv H3. eapply store_init_data_list_app. apply store_init_data_list_padding. - rewrite padding_size. + rewrite padding_size. replace (ofs + pos0 + (align pos0 (alignof ge t) - pos0)) with (ofs + align pos0 (alignof ge t)) by omega. eapply store_init_data_list_app. @@ -801,7 +801,7 @@ Theorem transl_init_sound: transl_init (prog_comp_env p) ty i = OK data -> Genv.store_init_data_list (globalenv p) m b 0 data = Some m'. Proof. - intros. + intros. set (ge := globalenv p) in *. change (prog_comp_env p) with (genv_cenv ge) in H0. destruct (transl_init_sound_gen ge) as (A & B & C). -- cgit