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

3 files changed, 47 insertions, 54 deletions

diff --git a/cfrontend/C2C.ml b/cfrontend/C2C.ml
index 3f3df2e..f767372 100644
--- a/cfrontend/C2C.ml
+++ b/cfrontend/C2C.ml
@@ -123,7 +123,7 @@ let builtins_generic = {
         (TInt(IULongLong, []),
           [TPtr(TVoid [], [])],
           false);
-    "__compcert_va_int64",
+    "__compcert_va_float64",
         (TFloat(FDouble, []),
           [TPtr(TVoid [], [])],
           false)
@@ -880,11 +880,11 @@ let rec convertInit env init =
   | C.Init_single e ->
       Init_single (convertExpr env e)
   | C.Init_array il ->
-      Init_compound (convertInitList env il)
+      Init_array (convertInitList env il)
   | C.Init_struct(_, flds) ->
-      Init_compound (convertInitList env (List.map snd flds))
+      Init_struct (convertInitList env (List.map snd flds))
   | C.Init_union(_, fld, i) ->
-      Init_compound (Init_cons(convertInit env i, Init_nil))
+      Init_union (intern_string fld.fld_name, convertInit env i)
 
 and convertInitList env il =
   match il with
diff --git a/cfrontend/Initializers.v b/cfrontend/Initializers.v
index f180f98..4054f6e 100644
--- a/cfrontend/Initializers.v
+++ b/cfrontend/Initializers.v
@@ -136,7 +136,9 @@ Fixpoint constval (a: expr) : res val :=
 
 Inductive initializer :=
   | Init_single (a: expr)
-  | Init_compound (il: initializer_list)
+  | Init_array (il: initializer_list)
+  | Init_struct (il: initializer_list)
+  | Init_union (f: ident) (i: initializer)
 with initializer_list :=
   | Init_nil
   | Init_cons (i: initializer) (il: initializer_list).
@@ -174,14 +176,14 @@ Fixpoint transl_init (ty: type) (i: initializer)
   match i, ty with
   | Init_single a, _ =>
       do d <- transl_init_single ty a; OK (d :: nil)
-  | Init_compound il, Tarray tyelt nelt _ =>
+  | Init_array il, Tarray tyelt nelt _ =>
       transl_init_array tyelt il (Zmax 0 nelt)
-  | Init_compound il, Tstruct id fl _ =>
+  | Init_struct il, Tstruct id fl _ =>
       transl_init_struct id ty fl il 0
-  | Init_compound il, Tunion _ Fnil _ =>
-      OK (Init_space (sizeof ty) :: nil)
-  | Init_compound il, Tunion id (Fcons _ ty1 _) _ =>
-      transl_init_union id ty ty1 il
+  | Init_union f i1, Tunion id fl _ =>
+      do ty1 <- field_type f fl;
+      do d <- transl_init ty1 i1;
+      OK (d ++ padding (sizeof ty1) (sizeof ty))
   | _, _ =>
       Error (msg "wrong type for compound initializer")
   end
@@ -212,16 +214,6 @@ with transl_init_struct (id: ident) (ty: type)
       OK (padding pos pos1 ++ d1 ++ d2)
   | _, _ =>
       Error (msg "wrong number of elements in struct initializer")
-  end
-
-with transl_init_union (id: ident) (ty ty1: type) (il: initializer_list)
-                       {struct il} : res (list init_data) :=
-  match il with
-  | Init_nil =>
-      Error (msg "empty union initializer")
-  | Init_cons i1 _ =>
-      do d <- transl_init ty1 i1;
-      OK (d ++ padding (sizeof ty1) (sizeof ty))
   end.
 
 
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 *)