From c677f108ff340c5bca67b428aa6e56b47f62da8c Mon Sep 17 00:00:00 2001
From: xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e>
Date: Fri, 28 Mar 2014 08:20:14 +0000
Subject: C: Support array initializers that are too short + default init for
 remainder. Elab: Handle C99 designated initializers. C2C, Initializers: more
 precise intermediate AST for initializers.

git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@2439 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
---
 cfrontend/Initializersproof.v | 67 ++++++++++++++++++++++---------------------
 1 file changed, 34 insertions(+), 33 deletions(-)

(limited to 'cfrontend/Initializersproof.v')

diff --git a/cfrontend/Initializersproof.v b/cfrontend/Initializersproof.v
index c39f5f5..f11901d 100644
--- a/cfrontend/Initializersproof.v
+++ b/cfrontend/Initializersproof.v
@@ -561,6 +561,16 @@ Proof.
   rewrite IHd1. omega.
 Qed.
 
+Remark union_field_size:
+  forall f ty fl, field_type f fl = OK ty -> sizeof ty <= sizeof_union fl.
+Proof.
+  induction fl; simpl; intros. 
+- inv H.
+- destruct (ident_eq f i). 
+  + inv H. xomega. 
+  + specialize (IHfl H). xomega. 
+Qed.
+
 Lemma transl_init_size:
   forall i ty data,
   transl_init ty i = OK data ->
@@ -575,32 +585,28 @@ with transl_init_list_size:
   (forall id ty fl pos data,
    transl_init_struct id ty fl il pos = OK data ->
    sizeof_struct fl pos <= sizeof ty ->
-   idlsize data + pos = sizeof ty)
-  /\
-  (forall id ty ty1 data,
-   transl_init_union id ty ty1 il = OK data ->
-   sizeof ty1 <= sizeof ty ->
-   idlsize data = sizeof ty).
+   idlsize data + pos = sizeof ty).
 
 Proof.
 - induction i; intros. 
 + (* single *)
   monadInv H. simpl. erewrite transl_init_single_size by eauto. omega. 
-+ (* compound *)
++ (* array *)
   simpl in H. destruct ty; try discriminate.
-* (* compound array *)
   simpl. eapply (proj1 (transl_init_list_size il)); eauto.
-* (* compound struct *)
++ (* struct *)
+  simpl in H. destruct ty; try discriminate.
   replace (idlsize data) with (idlsize data + 0) by omega.
-  eapply (proj1 (proj2 (transl_init_list_size il))). eauto.
+  eapply (proj2 (transl_init_list_size il)). eauto.
 Local Opaque alignof.
   simpl. apply align_le. apply alignof_pos.
-* (* compound union *)
-  set (sz := sizeof (Tunion i f a)) in *.
-  destruct f.
-  inv H. simpl. assert (sz >= 0) by (apply sizeof_pos). xomega. 
-  eapply (proj2 (proj2 (transl_init_list_size il))). eauto. 
-  simpl. eapply Zle_trans. 2: apply align_le. xomega. apply alignof_pos. 
++ (* union *)
+  simpl in H. destruct ty; try discriminate.
+  set (sz := sizeof (Tunion i0 f0 a)) in *.
+  monadInv H. rewrite idlsize_app. rewrite (IHi _ _ EQ1). 
+  rewrite padding_size. omega. unfold sz. simpl. 
+  apply Zle_trans with (sizeof_union f0). eapply union_field_size; eauto.
+  apply align_le. apply alignof_pos. 
 
 - induction il.
 + (* base cases *)
@@ -614,11 +620,9 @@ Local Opaque alignof.
   zify; omega.
 * (* structs *)
   destruct fl; inv H.
-  simpl in H0. rewrite padding_size by omega. omega. 
-* (* unions *)
-  inv H.
+  simpl in H0. rewrite padding_size by omega. omega.
 + (* inductive cases *)
-  destruct IHil as [A [B C]]. split; [idtac|split].
+  destruct IHil as [A B]. split.
 * (* arrays *)
   intros. monadInv H.
   rewrite idlsize_app.
@@ -633,11 +637,6 @@ Local Opaque alignof.
   rewrite (transl_init_size _ _ _ EQ). 
   rewrite <- (B _ _ _ _ _ EQ1). omega.
   auto. apply align_le. apply alignof_pos. 
-* (* unions *)
-  intros. simpl in H. monadInv H. 
-  rewrite idlsize_app.
-  rewrite (transl_init_size _ _ _ EQ). 
-  rewrite padding_size. omega. auto.
 Qed.
 
 (** A semantics for general initializers *)
@@ -659,15 +658,16 @@ Inductive exec_init: mem -> block -> Z -> type -> initializer -> mem -> Prop :=
       access_mode ty = By_value chunk ->
       Mem.store chunk m' b ofs v = Some m'' ->
       exec_init m b ofs ty (Init_single a) m''
-  | exec_init_compound_array: forall m b ofs ty sz a il m',
+  | exec_init_array_: forall m b ofs ty sz a il m',
       exec_init_array m b ofs ty sz il m' ->
-      exec_init m b ofs (Tarray ty sz a) (Init_compound il) m'
-  | exec_init_compound_struct: forall m b ofs id fl a il m',
+      exec_init m b ofs (Tarray ty sz a) (Init_array il) m'
+  | exec_init_struct: forall m b ofs id fl a il m',
       exec_init_list m b ofs (fields_of_struct id (Tstruct id fl a) fl 0) il m' ->
-      exec_init m b ofs (Tstruct id fl a) (Init_compound il) m'
-  | exec_init_compound_union: forall m b ofs id id1 ty1 fl a i m',
-      exec_init m b ofs ty1 i m' ->
-      exec_init m b ofs (Tunion id (Fcons id1 ty1 fl) a) (Init_compound (Init_cons i Init_nil)) m'
+      exec_init m b ofs (Tstruct id fl a) (Init_struct il) m'
+  | exec_init_union: forall m b ofs id fl a f i ty m',
+      field_type f fl = OK ty ->
+      exec_init m b ofs ty i m' ->
+      exec_init m b ofs (Tunion id fl a) (Init_union f i) m'
 
 with exec_init_array: mem -> block -> Z -> type -> Z -> initializer_list -> mem -> Prop :=
   | exec_init_array_nil: forall m b ofs ty sz,
@@ -740,7 +740,8 @@ Local Opaque sizeof.
 - (* struct *)
   replace ofs with (ofs + 0) by omega. eauto.
 - (* union *)
-  monadInv H1. eapply store_init_data_list_app. eauto.
+  rewrite H in H2. monadInv H2. inv EQ.  
+  eapply store_init_data_list_app. eauto.
   apply store_init_data_list_padding. 
 
 - (* array, empty *)
-- 
cgit v1.2.3