From c677f108ff340c5bca67b428aa6e56b47f62da8c Mon Sep 17 00:00:00 2001 From: xleroy 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/C2C.ml | 8 +++--- cfrontend/Initializers.v | 26 ++++++----------- cfrontend/Initializersproof.v | 67 ++++++++++++++++++++++--------------------- 3 files changed, 47 insertions(+), 54 deletions(-) (limited to 'cfrontend') 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 *) -- cgit v1.2.3