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/Ctypes.v | 116 ++++++++++++++++++++++++++--------------------------- 1 file changed, 58 insertions(+), 58 deletions(-) (limited to 'cfrontend/Ctypes.v') diff --git a/cfrontend/Ctypes.v b/cfrontend/Ctypes.v index 1f55da7f..78345b42 100644 --- a/cfrontend/Ctypes.v +++ b/cfrontend/Ctypes.v @@ -24,7 +24,7 @@ Require Archi. (** * Syntax of types *) (** Compcert C types are similar to those of C. They include numeric types, - pointers, arrays, function types, and composite types (struct and + pointers, arrays, function types, and composite types (struct and union). Numeric types (integers and floats) fully specify the bit size of the type. An integer type is a pair of a signed/unsigned flag and a bit size: 8, 16, or 32 bits, or the special [IBool] size @@ -140,7 +140,7 @@ Definition attr_union (a1 a2: attr) : attr := | None, al => al | al, None => al | Some n1, Some n2 => Some (N.max n1 n2) - end + end |}. Definition merge_attributes (ty: type) (a: attr) : type := @@ -184,7 +184,7 @@ Definition type_int32s := Tint I32 Signed noattr. Definition type_bool := Tint IBool Signed noattr. (** The usual unary conversion. Promotes small integer types to [signed int32] - and degrades array types and function types to pointer types. + and degrades array types and function types to pointer types. Attributes are erased. *) Definition typeconv (ty: type) : type := @@ -272,7 +272,7 @@ Remark align_attr_two_p: (exists n, al = two_power_nat n) -> (exists n, align_attr a al = two_power_nat n). Proof. - intros. unfold align_attr. destruct (attr_alignas a). + intros. unfold align_attr. destruct (attr_alignas a). exists (N.to_nat n). rewrite two_power_nat_two_p. rewrite N_nat_Z. auto. auto. Qed. @@ -309,7 +309,7 @@ Qed. (** In the ISO C standard, size is defined only for complete types. However, it is convenient that [sizeof] is a total function. For [void] and function types, we follow GCC and define - their size to be 1. For undefined structures and unions, the size is + their size to be 1. For undefined structures and unions, the size is arbitrarily taken to be 0. *) @@ -355,16 +355,16 @@ Fixpoint naturally_aligned (t: type) : Prop := Lemma sizeof_alignof_compat: forall env t, naturally_aligned t -> (alignof env t | sizeof env t). Proof. - induction t; intros [A B]; unfold alignof, align_attr; rewrite A; simpl. + induction t; intros [A B]; unfold alignof, align_attr; rewrite A; simpl. - apply Zdivide_refl. - destruct i; apply Zdivide_refl. -- exists (8 / Archi.align_int64); reflexivity. -- destruct f. apply Zdivide_refl. exists (8 / Archi.align_float64); reflexivity. +- exists (8 / Archi.align_int64); reflexivity. +- destruct f. apply Zdivide_refl. exists (8 / Archi.align_float64); reflexivity. - apply Zdivide_refl. -- apply Z.divide_mul_l; auto. +- apply Z.divide_mul_l; auto. - apply Zdivide_refl. -- destruct (env!i). apply co_sizeof_alignof. apply Zdivide_0. -- destruct (env!i). apply co_sizeof_alignof. apply Zdivide_0. +- destruct (env!i). apply co_sizeof_alignof. apply Zdivide_0. +- destruct (env!i). apply co_sizeof_alignof. apply Zdivide_0. Qed. (** ** Size and alignment for composite definitions *) @@ -399,7 +399,7 @@ Fixpoint sizeof_union (env: composite_env) (m: members) : Z := Lemma alignof_composite_two_p: forall env m, exists n, alignof_composite env m = two_power_nat n. Proof. - induction m as [|[id t]]; simpl. + induction m as [|[id t]]; simpl. - exists 0%nat; auto. - apply Z.max_case; auto. apply alignof_two_p. Qed. @@ -408,8 +408,8 @@ Lemma alignof_composite_pos: forall env m a, align_attr a (alignof_composite env m) > 0. Proof. intros. - exploit align_attr_two_p. apply (alignof_composite_two_p env m). - instantiate (1 := a). intros [n EQ]. + exploit align_attr_two_p. apply (alignof_composite_two_p env m). + instantiate (1 := a). intros [n EQ]. rewrite EQ; apply two_power_nat_pos. Qed. @@ -418,10 +418,10 @@ Lemma sizeof_struct_incr: Proof. induction m as [|[id t]]; simpl; intros. - omega. -- apply Zle_trans with (align cur (alignof env t)). +- apply Zle_trans with (align cur (alignof env t)). apply align_le. apply alignof_pos. apply Zle_trans with (align cur (alignof env t) + sizeof env t). - generalize (sizeof_pos env t); omega. + generalize (sizeof_pos env t); omega. apply IHm. Qed. @@ -457,7 +457,7 @@ Fixpoint field_type (id: ident) (fld: members) {struct fld} : res type := | (id', t) :: fld' => if ident_eq id id' then OK t else field_type id fld' end. -(** Some sanity checks about field offsets. First, field offsets are +(** Some sanity checks about field offsets. First, field offsets are within the range of acceptable offsets. *) Remark field_offset_rec_in_range: @@ -470,9 +470,9 @@ Proof. - destruct (ident_eq id i); intros. inv H. inv H0. split. apply align_le. apply alignof_pos. apply sizeof_struct_incr. - exploit IHfld; eauto. intros [A B]. split; auto. + exploit IHfld; eauto. intros [A B]. split; auto. eapply Zle_trans; eauto. apply Zle_trans with (align pos (alignof env t)). - apply align_le. apply alignof_pos. generalize (sizeof_pos env t). omega. + apply align_le. apply alignof_pos. generalize (sizeof_pos env t). omega. Qed. Lemma field_offset_in_range: @@ -496,11 +496,11 @@ Proof. induction fld as [|[i t]]; simpl; intros. - discriminate. - destruct (ident_eq id1 i); destruct (ident_eq id2 i). -+ congruence. ++ congruence. + subst i. inv H; inv H0. - exploit field_offset_rec_in_range. eexact H1. eauto. tauto. + exploit field_offset_rec_in_range. eexact H1. eauto. tauto. + subst i. inv H1; inv H2. - exploit field_offset_rec_in_range. eexact H. eauto. tauto. + exploit field_offset_rec_in_range. eexact H. eauto. tauto. + eapply IHfld; eauto. Qed. @@ -512,10 +512,10 @@ Lemma field_offset_prefix: field_offset env id fld1 = OK ofs -> field_offset env id (fld1 ++ fld2) = OK ofs. Proof. - intros until fld1. unfold field_offset. generalize 0 as pos. + intros until fld1. unfold field_offset. generalize 0 as pos. induction fld1 as [|[i t]]; simpl; intros. - discriminate. -- destruct (ident_eq id i); auto. +- destruct (ident_eq id i); auto. Qed. (** Fourth, the position of each field respects its alignment. *) @@ -525,7 +525,7 @@ Lemma field_offset_aligned: field_offset env id fld = OK ofs -> field_type id fld = OK ty -> (alignof env ty | ofs). Proof. - intros until ty. unfold field_offset. generalize 0 as pos. revert fld. + intros until ty. unfold field_offset. generalize 0 as pos. revert fld. induction fld as [|[i t]]; simpl; intros. - discriminate. - destruct (ident_eq id i). @@ -613,18 +613,18 @@ Proof. assert (X: forall co, let a := Zmin 8 (co_alignof co) in a = 1 \/ a = 2 \/ a = 4 \/ a = 8). { - intros. destruct (co_alignof_two_p co) as [n EQ]. unfold a; rewrite EQ. + intros. destruct (co_alignof_two_p co) as [n EQ]. unfold a; rewrite EQ. destruct n; auto. destruct n; auto. destruct n; auto. right; right; right. apply Z.min_l. - rewrite two_power_nat_two_p. rewrite ! inj_S. + rewrite two_power_nat_two_p. rewrite ! inj_S. change 8 with (two_p 3). apply two_p_monotone. omega. } induction ty; simpl; auto. destruct i; auto. destruct f; auto. - destruct (env!i); auto. + destruct (env!i); auto. destruct (env!i); auto. Qed. @@ -644,9 +644,9 @@ Proof. destruct n. apply Zdivide_refl. destruct n. apply Zdivide_refl. destruct n. apply Zdivide_refl. - apply Z.min_case. - exists (two_p (Z.of_nat n)). - change 8 with (two_p 3). + apply Z.min_case. + exists (two_p (Z.of_nat n)). + change 8 with (two_p 3). rewrite <- two_p_is_exp by omega. rewrite two_power_nat_two_p. rewrite !inj_S. f_equal. omega. apply Zdivide_refl. @@ -659,8 +659,8 @@ Proof. apply Zdivide_refl. apply Z.divide_mul_l. auto. apply Zdivide_refl. - destruct (env!i). apply X. apply Zdivide_0. - destruct (env!i). apply X. apply Zdivide_0. + destruct (env!i). apply X. apply Zdivide_0. + destruct (env!i). apply X. apply Zdivide_0. Qed. (** Type ranks *) @@ -761,7 +761,7 @@ Qed. The size and alignment of the composite are determined at this time. The alignment takes into account the [__Alignas] attributes associated with the definition. The size is rounded up to a multiple - of the alignment. + of the alignment. The conversion fails if a type of a member is not complete. This rules out incorrect recursive definitions such as @@ -800,7 +800,7 @@ Program Definition composite_of_def co_sizeof_alignof := _ |} end. Next Obligation. - apply Zle_ge. eapply Zle_trans. eapply sizeof_composite_pos. + apply Zle_ge. eapply Zle_trans. eapply sizeof_composite_pos. apply align_le; apply alignof_composite_pos. Defined. Next Obligation. @@ -842,9 +842,9 @@ Lemma alignof_stable: forall t, complete_type env t = true -> alignof env' t = alignof env t. Proof. induction t; simpl; intros; f_equal; auto. - destruct (env!i) as [co|] eqn:E; try discriminate. + destruct (env!i) as [co|] eqn:E; try discriminate. erewrite extends by eauto. auto. - destruct (env!i) as [co|] eqn:E; try discriminate. + destruct (env!i) as [co|] eqn:E; try discriminate. erewrite extends by eauto. auto. Qed. @@ -853,9 +853,9 @@ Lemma sizeof_stable: Proof. induction t; simpl; intros; auto. rewrite IHt by auto. auto. - destruct (env!i) as [co|] eqn:E; try discriminate. + destruct (env!i) as [co|] eqn:E; try discriminate. erewrite extends by eauto. auto. - destruct (env!i) as [co|] eqn:E; try discriminate. + destruct (env!i) as [co|] eqn:E; try discriminate. erewrite extends by eauto. auto. Qed. @@ -863,9 +863,9 @@ Lemma complete_type_stable: forall t, complete_type env t = true -> complete_type env' t = true. Proof. induction t; simpl; intros; auto. - destruct (env!i) as [co|] eqn:E; try discriminate. + destruct (env!i) as [co|] eqn:E; try discriminate. erewrite extends by eauto. auto. - destruct (env!i) as [co|] eqn:E; try discriminate. + destruct (env!i) as [co|] eqn:E; try discriminate. erewrite extends by eauto. auto. Qed. @@ -873,16 +873,16 @@ Lemma rank_type_stable: forall t, complete_type env t = true -> rank_type env' t = rank_type env t. Proof. induction t; simpl; intros; auto. - destruct (env!i) as [co|] eqn:E; try discriminate. + destruct (env!i) as [co|] eqn:E; try discriminate. erewrite extends by eauto. auto. - destruct (env!i) as [co|] eqn:E; try discriminate. + destruct (env!i) as [co|] eqn:E; try discriminate. erewrite extends by eauto. auto. Qed. Lemma alignof_composite_stable: forall m, complete_members env m = true -> alignof_composite env' m = alignof_composite env m. Proof. - induction m as [|[id t]]; simpl; intros. + induction m as [|[id t]]; simpl; intros. auto. InvBooleans. rewrite alignof_stable by auto. rewrite IHm by auto. auto. Qed. @@ -892,7 +892,7 @@ Lemma sizeof_struct_stable: Proof. induction m as [|[id t]]; simpl; intros. auto. - InvBooleans. rewrite alignof_stable by auto. rewrite sizeof_stable by auto. + InvBooleans. rewrite alignof_stable by auto. rewrite sizeof_stable by auto. rewrite IHm by auto. auto. Qed. @@ -907,8 +907,8 @@ Qed. Lemma sizeof_composite_stable: forall su m, complete_members env m = true -> sizeof_composite env' su m = sizeof_composite env su m. Proof. - intros. destruct su; simpl. - apply sizeof_struct_stable; auto. + intros. destruct su; simpl. + apply sizeof_struct_stable; auto. apply sizeof_union_stable; auto. Qed. @@ -937,7 +937,7 @@ Lemma add_composite_definitions_incr: Proof. induction defs; simpl; intros. - inv H; auto. -- destruct a; monadInv H. +- destruct a; monadInv H. eapply IHdefs; eauto. rewrite PTree.gso; auto. red; intros; subst id0. unfold composite_of_def in EQ. rewrite H0 in EQ; discriminate. Qed. @@ -974,22 +974,22 @@ Proof. eapply IHdefs; eauto. set (env1 := PTree.set id x env0) in *. unfold composite_of_def in EQ. - destruct (env0!id) eqn:E; try discriminate. + destruct (env0!id) eqn:E; try discriminate. destruct (complete_members env0 m) eqn:C; inversion EQ; clear EQ. assert (forall id1 co1, env0!id1 = Some co1 -> env1!id1 = Some co1). { intros. unfold env1. rewrite PTree.gso; auto. congruence. } red; intros. unfold env1 in H2; rewrite PTree.gsspec in H2; destruct (peq id0 id). -+ subst id0. inversion H2; clear H2. subst co. ++ subst id0. inversion H2; clear H2. subst co. (* assert (A: alignof_composite env1 m = alignof_composite env0 m) by (apply alignof_composite_stable; assumption). *) rewrite <- H1; constructor; simpl. -* eapply complete_members_stable; eauto. -* f_equal. symmetry. apply alignof_composite_stable; auto. -* f_equal. symmetry. apply sizeof_composite_stable; auto. +* eapply complete_members_stable; eauto. +* f_equal. symmetry. apply alignof_composite_stable; auto. +* f_equal. symmetry. apply sizeof_composite_stable; auto. * symmetry. apply rank_members_stable; auto. -+ exploit H0; eauto. intros [P Q R S]. ++ exploit H0; eauto. intros [P Q R S]. constructor; intros. * eapply complete_members_stable; eauto. * rewrite Q. f_equal. symmetry. apply alignof_composite_stable; auto. @@ -1005,13 +1005,13 @@ Theorem build_composite_env_charact: In (Composite id su m a) defs -> exists co, env!id = Some co /\ co_members co = m /\ co_attr co = a /\ co_su co = su. Proof. - intros until defs. unfold build_composite_env. generalize (PTree.empty composite) as env0. + intros until defs. unfold build_composite_env. generalize (PTree.empty composite) as env0. revert defs. induction defs as [|d1 defs]; simpl; intros. - contradiction. - destruct d1; monadInv H. - destruct H0; [idtac|eapply IHdefs;eauto]. inv H. - unfold composite_of_def in EQ. - destruct (env0!id) eqn:E; try discriminate. + destruct H0; [idtac|eapply IHdefs;eauto]. inv H. + unfold composite_of_def in EQ. + destruct (env0!id) eqn:E; try discriminate. destruct (complete_members env0 m) eqn:C; simplify_eq EQ. clear EQ; intros EQ. exists x. split. eapply add_composite_definitions_incr; eauto. apply PTree.gss. -- cgit