diff options
| -rw-r--r-- | cfrontend/C2C.ml | 8 | ||||
| -rw-r--r-- | cfrontend/Initializers.v | 26 | ||||
| -rw-r--r-- | cfrontend/Initializersproof.v | 67 | ||||
| -rw-r--r-- | cparser/Cprint.ml | 2 | ||||
| -rw-r--r-- | cparser/Cutil.ml | 28 | ||||
| -rw-r--r-- | cparser/Cutil.mli | 5 | ||||
| -rw-r--r-- | cparser/Elab.ml | 442 | ||||
| -rw-r--r-- | cparser/Unblock.ml | 24 | ||||
| -rw-r--r-- | test/regression/Makefile | 7 | ||||
| -rw-r--r-- | test/regression/Results/initializers | 1 | ||||
| -rw-r--r-- | test/regression/Results/initializers2 | 12 | ||||
| -rw-r--r-- | test/regression/Results/initializers3 | 11 | ||||
| -rw-r--r-- | test/regression/initializers.c | 5 | ||||
| -rw-r--r-- | test/regression/initializers2.c | 74 | ||||
| -rw-r--r-- | test/regression/initializers3.c | 90 |
15 files changed, 605 insertions, 197 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 *) diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml index 0bbea68..f26025e 100644 --- a/cparser/Cprint.ml +++ b/cparser/Cprint.ml @@ -342,7 +342,7 @@ let rec init pp = function List.iter (fun (fld, i) -> fprintf pp "%a,@ " init i) il; fprintf pp "}@]" | Init_union(id, fld, i) -> - fprintf pp "@[<hov 1>{%a}@]" init i + fprintf pp "@[<hov 2>{.%s =@ %a}@]" fld.fld_name init i let simple_decl pp (id, ty) = dcl pp ty (fun pp -> fprintf pp " %a" ident id) diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml index 302c1cf..22ef187 100644 --- a/cparser/Cutil.ml +++ b/cparser/Cutil.ml @@ -840,4 +840,32 @@ let printloc oc (filename, lineno) = let formatloc pp (filename, lineno) = if filename <> "" then Format.fprintf pp "%s:%d: " filename lineno +(* Generate the default initializer for the given type *) +let rec default_init env ty = + match unroll env ty with + | TInt _ | TEnum _ -> + Init_single (intconst 0L IInt) + | TFloat(fk, _) -> + Init_single floatconst0 + | TPtr(ty, _) -> + Init_single nullconst + | TArray(ty, sz, _) -> + Init_array [] + | TStruct(id, _) -> + let rec default_init_fields = function + | [] -> [] + | f1 :: fl -> + if f1.fld_name = "" + then default_init_fields fl + else (f1, default_init env f1.fld_typ) :: default_init_fields fl in + let ci = Env.find_struct env id in + Init_struct(id, default_init_fields ci.ci_members) + | TUnion(id, _) -> + let ci = Env.find_union env id in + begin match ci.ci_members with + | [] -> assert false + | fld :: _ -> Init_union(id, fld, default_init env fld.fld_typ) + end + | _ -> + assert false diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli index 35f7338..9f59a76 100644 --- a/cparser/Cutil.mli +++ b/cparser/Cutil.mli @@ -207,3 +207,8 @@ val printloc: out_channel -> location -> unit val formatloc: Format.formatter -> location -> unit (* Printer for locations (for Format) *) +(* Initializers *) + +val default_init: Env.t -> typ -> init + (* Return a default initializer for the given type + (with zero numbers, null pointers, etc). *) diff --git a/cparser/Elab.ml b/cparser/Elab.ml index 90662a3..e468ab2 100644 --- a/cparser/Elab.ml +++ b/cparser/Elab.ml @@ -1302,16 +1302,6 @@ let elab_for_expr loc env = function (* Elaboration of initializers. C99 section 6.7.8 *) -let project_init loc il = - if il = [] then - warning loc "empty initializer braces"; - List.map - (fun (what, i) -> - if what <> NEXT_INIT then - error loc "C99 initializers are not supported"; - i) - il - let init_char_array_string opt_size s = let len = Int64.of_int (String.length s) in let size = @@ -1351,127 +1341,321 @@ let check_init_type loc env a ty = "initializer has type@ %a@ instead of the expected type @ %a" Cprint.typ a.etyp Cprint.typ ty -(* Build an initializer for type [ty], consuming initialization items - from the list [ile]. Return a pair (initializer, items not consumed). *) - -let rec elab_init loc env ty ile = - match unroll env ty with - | TArray(ty_elt, opt_sz, _) -> - let rec elab_init_array n accu rem = - match opt_sz, rem with - | Some sz, _ when n >= sz -> - (Init_array(List.rev accu), rem) - | None, [] -> - (Init_array(List.rev accu), rem) - | _, _ -> - let (i, rem') = elab_init loc env ty_elt rem in - elab_init_array (Int64.succ n) (i :: accu) rem' in - begin match ile with - (* char array = "string literal" *) - | (SINGLE_INIT (CONSTANT (CONST_STRING s)) - | COMPOUND_INIT [_, SINGLE_INIT(CONSTANT (CONST_STRING s))]) :: ile1 - when (match unroll env ty_elt with - | TInt((IChar|IUChar|ISChar), _) -> true - | _ -> false) -> - (init_char_array_string opt_sz s, ile1) - (* wchar array = L"wide string literal" *) - | (SINGLE_INIT (CONSTANT (CONST_WSTRING s)) - | COMPOUND_INIT [_, SINGLE_INIT(CONSTANT (CONST_WSTRING s))]) :: ile1 - when (match unroll env ty_elt with - | TInt _ -> true - | _ -> false) -> - (init_int_array_wstring opt_sz s, ile1) - (* array = { elt, ..., elt } *) - | COMPOUND_INIT ile1 :: ile2 -> - let (ie, rem) = elab_init_array 0L [] (project_init loc ile1) in - if rem <> [] then - warning loc "excess elements at end of array initializer"; - (ie, ile2) - (* array = elt, ..., elt (within a bigger compound initializer) *) - | _ -> - elab_init_array 0L [] ile - end - | TStruct(id, _) -> - let ci = wrap Env.find_struct loc env id in - let rec elab_init_fields fld accu rem = - match fld with - | [] -> - (Init_struct(id, List.rev accu), rem) - | {fld_name = ""} :: fld' -> - (* anonymous bitfields consume no initializer *) - elab_init_fields fld' accu rem - | fld1 :: fld' -> - let (i, rem') = elab_init loc env fld1.fld_typ rem in - elab_init_fields fld' ((fld1, i) :: accu) rem' in - begin match ile with - (* struct = { elt, ..., elt } *) - | COMPOUND_INIT ile1 :: ile2 -> - let (ie, rem) = - elab_init_fields ci.ci_members [] (project_init loc ile1) in - if rem <> [] then - warning loc "excess elements at end of struct initializer"; - (ie, ile2) - (* struct = elt, ..., elt (within a bigger compound initializer) *) - | _ -> - elab_init_fields ci.ci_members [] ile +(* Representing initialization state using zippers *) + +module I = struct + + type zipinit = + | Ztop of string * typ + + | Zarray of zipinit (* ancestor *) + * typ (* type of elements *) + * int64 option (* size *) + * init (* default initializer *) + * init list (* elements before point, reversed *) + * int64 (* position of point *) + * init list (* elements after point *) + + | Zstruct of zipinit (* ancestor *) + * ident (* struct type *) + * (field * init) list (* elements before current, reversed *) + * field (* current field *) + * (field * init) list (* elements after current *) + + | Zunion of zipinit (* ancestor *) + * ident (* union type *) + * field (* current member *) + + type state = zipinit * init (* current point & init for this point *) + + (* The initial state: default initialization, current point at top *) + let top env name ty = (Ztop(name, ty), default_init env ty) + + (* Change the initializer for the current point *) + let set (z, i) i' = (z, i') + + (* Put the current point back to the top *) + let rec to_top = function + | Ztop(name, ty), i as zi -> zi + | Zarray(z, ty, sz, dfl, before, idx, after), i -> + to_top (z, Init_array (List.rev_append before (i :: after))) + | Zstruct(z, id, before, fld, after), i -> + to_top (z, Init_struct(id, List.rev_append before ((fld, i) :: after))) + | Zunion(z, id, fld), i -> + to_top (z, Init_union(id, fld, i)) + + (* Extract the initializer corresponding to the current state *) + let to_init zi = snd (to_top zi) + + (* The type of the current point *) + let typeof = function + | Ztop(name, ty), i -> ty + | Zarray(z, ty, sz, dfl, before, idx, after), i -> ty + | Zstruct(z, id, before, fld, after), i -> fld.fld_typ + | Zunion(z, id, fld), i -> fld.fld_typ + + (* The name of the path leading to the current point, for error reporting *) + let rec zipname = function + | Ztop(name, ty) -> name + | Zarray(z, ty, sz, dfl, before, idx, after) -> + sprintf "%s[%Ld]" (zipname z) idx + | Zstruct(z, id, before, fld, after) -> + sprintf "%s.%s" (zipname z) fld.fld_name + | Zunion(z, id, fld) -> + sprintf "%s.%s" (zipname z) fld.fld_name + + let name (z, i) = zipname z + + (* Auxiliary functions to deal with arrays *) + let index_below (idx: int64) (sz: int64 option) = + match sz with None -> true | Some sz -> idx < sz + + let il_head dfl = function [] -> dfl | i1 :: il -> i1 + let il_tail = function [] -> [] | i1 :: il -> il + + (* Advance the current point to the next point in right-up order. + Return None if no next point, i.e. we are at top *) + let rec next = function + | Ztop(name, ty), i -> None + | Zarray(z, ty, sz, dfl, before, idx, after), i -> + let idx' = Int64.succ idx in + if index_below idx' sz + then Some(Zarray(z, ty, sz, dfl, i :: before, idx', il_tail after), + il_head dfl after) + else next (z, Init_array (List.rev_append before (i :: after))) + | Zstruct(z, id, before, fld, []), i -> + next (z, Init_struct(id, List.rev_append before [(fld, i)])) + | Zstruct(z, id, before, fld, (fld1, i1) :: after), i -> + Some(Zstruct(z, id, (fld, i) :: before, fld1, after), i1) + | Zunion(z, id, fld), i -> + next (z, Init_union(id, fld, i)) + + (* Move the current point "down" to the first component of an array, + struct, or union. No effect if the current point is a scalar. *) + let rec first env (z, i as zi) = + let ty = typeof zi in + match unroll env ty, i with + | TArray(ty, sz, _), Init_array il -> + if index_below 0L sz then begin + let dfl = default_init env ty in + Some(Zarray(z, ty, sz, dfl, [], 0L, il_tail il), il_head dfl il) + end + else None + | TStruct(id, _), Init_struct(id', []) -> + None + | TStruct(id, _), Init_struct(id', (fld1, i1) :: flds) -> + Some(Zstruct(z, id, [], fld1, flds), i1) + | TUnion(id, _), Init_union(id', fld, i) -> + begin match (Env.find_union env id).ci_members with + | [] -> None + | fld1 :: _ -> + Some(Zunion(z, id, fld1), + if fld.fld_name = fld1.fld_name + then i + else default_init env fld1.fld_typ) + end + | (TStruct _ | TUnion _), Init_single a -> + (* This is a previous whole-struct initialization that we + are going to overwrite. Revert to the default initializer. *) + first env (z, default_init env ty) + | _ -> + Some (z, i) + + (* Move to the [n]-th element of the current point, which must be + an array. *) + let index env (z, i as zi) n = + match unroll env (typeof zi), i with + | TArray(ty, sz, _), Init_array il -> + if n >= 0L && index_below n sz then begin + let dfl = default_init env ty in + let rec loop p before after = + if p = n then + Some(Zarray(z, ty, sz, dfl, before, n, il_tail after), + il_head dfl after) + else + loop (Int64.succ p) + (il_head dfl after :: before) + (il_tail after) + in loop 0L [] il + end else + None + | _, _ -> + None + + (* Move to the member named [name] of the current point, which must be + a struct or a union. *) + let rec member env (z, i as zi) name = + let ty = typeof zi in + match unroll env ty, i with + | TStruct(id, _), Init_struct(id', flds) -> + let rec find before = function + | [] -> None + | (fld, i as f_i) :: after -> + if fld.fld_name = name then + Some(Zstruct(z, id, before, fld, after), i) + else + find (f_i :: before) after + in find [] flds + | TUnion(id, _), Init_union(id', fld, i) -> + if fld.fld_name = name then + Some(Zunion(z, id, fld), i) + else begin + let rec find = function + | [] -> None + | fld1 :: rem -> + if fld1.fld_name = name then + Some(Zunion(z, id, fld1), default_init env fld1.fld_typ) + else + find rem + in find (Env.find_union env id).ci_members + end + | (TStruct _ | TUnion _), Init_single a -> + member env (z, default_init env ty) name + | _, _ -> + None +end + +(* Interpret the given designator, moving the initialization state [zi] + "down" accordingly. *) + +let rec elab_designator loc env zi desig = + match desig with + | NEXT_INIT -> + zi + | INFIELD_INIT(name, desig') -> + begin match I.member env zi name with + | Some zi' -> + elab_designator loc env zi' desig' + | None -> + error loc "%s has no member named %s" (I.name zi) name; + raise Exit end - | TUnion(id, _) -> - let ci = wrap Env.find_union loc env id in - let fld1 = - match ci.ci_members with [] -> assert false | hd :: tl -> hd in - begin match ile with - (* union = { elt } *) - | COMPOUND_INIT ile1 :: ile2 -> - let (i, rem) = - elab_init loc env fld1.fld_typ (project_init loc ile1) in - if rem <> [] then - warning loc "excess elements at end of union initializer"; - (Init_union(id, fld1, i), ile2) - (* union = elt (within a bigger compound initializer) *) - | _ -> - let (i, rem) = elab_init loc env fld1.fld_typ ile in - (Init_union(id, fld1, i), rem) + | ATINDEX_INIT(a, desig') -> + begin match Ceval.integer_expr env (elab_expr loc env a) with + | None -> + error loc "array element designator for %s is not a compile-time constant" + (I.name zi); + raise Exit + | Some n -> + match I.index env zi n with + | Some zi' -> + elab_designator loc env zi' desig' + | None -> + error loc "bad array element designator %Ld within %s" + n (I.name zi); + raise Exit end - | TInt _ | TFloat _ | TPtr _ | TEnum _ -> - begin match ile with - (* scalar = elt *) - | SINGLE_INIT a :: ile1 -> - let a' = elab_expr loc env a in - check_init_type loc env a' ty; - (Init_single a', ile1) - (* scalar = nothing (within a bigger compound initializer) *) - | (NO_INIT :: ile1) | ([] as ile1) -> - begin match unroll env ty with - | TInt _ | TEnum _ -> (Init_single (intconst 0L IInt), ile1) - | TFloat _ -> (Init_single floatconst0, ile1) - | TPtr _ -> (Init_single nullconst, ile1) - | _ -> assert false - end - | COMPOUND_INIT _ :: ile1 -> - fatal_error loc "compound initializer for type@ %a" Cprint.typ ty + | ATINDEXRANGE_INIT(e1, e2) -> + error loc "GCC array range designators are not supported"; + raise Exit + +(* Elaboration of an initialization expression. Return the corresponding + initializer. *) + +let elab_init loc env root ty_root ie = + +(* Perform the initializations described by the list [il] over + the initialization state [zi]. [first] is true if we are at the + beginning of a braced initializer. Returns the final initializer. *) + +let rec elab_list zi il first = + match il with + | [] -> + (* All initialization items consumed. *) + I.to_init zi + | (desig, item) :: il' -> + if desig = NEXT_INIT then begin + match (if first then I.first env zi else I.next zi) + with + | None -> + warning loc "excess elements at end of initializer for %s, ignored" + (I.name zi); + I.to_init zi + | Some zi' -> + elab_item zi' item il' + end else + elab_item (elab_designator loc env (I.to_top zi) desig) item il' + +(* Perform the initialization described by [item] for the current + subobject of state [zi]. Continue initializing with the list [il]. *) + +and elab_item zi item il = + let ty = I.typeof zi in + match item, unroll env ty with + (* Special case char array = "string literal" *) + | (SINGLE_INIT (CONSTANT (CONST_STRING s)) + | COMPOUND_INIT [_, SINGLE_INIT(CONSTANT (CONST_STRING s))]), + TArray(TInt((IChar|IUChar|ISChar), _), sz, _) -> + if not (I.index_below (Int64.of_int(String.length s - 1)) sz) then + warning loc "initializer string for array of chars %s is too long" + (I.name zi); + elab_list (I.set zi (init_char_array_string sz s)) il false + (* Special case int array = L"wide string literal" *) + | (SINGLE_INIT (CONSTANT (CONST_WSTRING s)) + | COMPOUND_INIT [_, SINGLE_INIT(CONSTANT (CONST_WSTRING s))]), + TArray(TInt(_, _), sz, _) -> + if not (I.index_below (Int64.of_int(List.length s - 1)) sz) then + warning loc "initializer string for array of wide chars %s is too long" + (I.name zi); + elab_list (I.set zi (init_int_array_wstring sz s)) il false + (* Brace-enclosed compound initializer *) + | COMPOUND_INIT il', _ -> + (* Process the brace-enclosed stuff, obtaining its initializer *) + let ini' = elab_list (I.top env (I.name zi) ty) il' true in + (* Initialize current subobject with this state, and continue *) + elab_list (I.set zi ini') il false + (* Single expression *) + | SINGLE_INIT a, _ -> + let a' = elab_expr loc env a in + elab_single zi a' il + (* No initializer: can this happen? *) + | NO_INIT, _ -> + elab_list zi il false + +(* Perform initialization by a single expression [a] for the current + subobject of state [zi], Continue initializing with the list [il']. *) + +and elab_single zi a il = + let ty = I.typeof zi in + match unroll env ty with + | TInt _ | TEnum _ | TFloat _ | TPtr _ -> + (* This is a scalar: do direct initialization and continue *) + check_init_type loc env a ty; + elab_list (I.set zi (Init_single a)) il false + | TStruct _ | TUnion _ when compatible_types ~noattrs:true env ty a.etyp -> + (* This is a composite that can be initialized directly + from the expression: do as above *) + elab_list (I.set zi (Init_single a)) il false + | TStruct _ | TUnion _ | TArray _ -> + (* This is an aggregate: we need to drill into it, recursively *) + begin match I.first env zi with + | Some zi' -> + elab_single zi' a il + | None -> + error loc "initializer for aggregate %s with no elements requires explicit braces" + (I.name zi); + raise Exit end | _ -> - fatal_error loc "impossible to initialize at type@ %a" Cprint.typ ty + error loc "impossible to initialize %s of type@ %a" + (I.name zi) Cprint.typ ty; + raise Exit -let elab_initial loc env ty ie = - match unroll env ty, ie with - | _, NO_INIT -> None - (* scalar or composite = expr *) - | (TInt _ | TFloat _ | TPtr _ | TStruct _ | TUnion _ | TEnum _), SINGLE_INIT a -> - let a' = elab_expr loc env a in - check_init_type loc env a' ty; - Some (Init_single a') - (* array = expr or - array or struct or union = { elt, ..., elt } *) - | (TArray _, SINGLE_INIT _) - | ((TArray _ | TStruct _ | TUnion _), COMPOUND_INIT _) -> - let (i, rem) = elab_init loc env ty [ie] in - if rem <> [] then - warning loc "excess elements at end of compound initializer"; - Some i - | _, _ -> - error loc "ill-formed initializer for type@ %a" Cprint.typ ty; - None +(* Start with top-level object initialized to default *) + +in elab_item (I.top env root ty_root) ie [] + +(* Elaboration of a top-level initializer *) + +let elab_initial loc env root ty ie = + match ie with + | NO_INIT -> None + | _ -> + try + Some (elab_init loc env root ty ie) + with + | Exit -> None (* error was already reported *) + | Env.Error msg -> error loc "%s" (Env.error_message msg); None (* Complete an array type with the size obtained from the initializer: "int x[] = { 1, 2, 3 }" becomes "int x[3] = ..." *) @@ -1485,8 +1669,8 @@ let fixup_typ loc env ty init = (* Entry point *) -let elab_initializer loc env ty ie = - match elab_initial loc env ty ie with +let elab_initializer loc env root ty ie = + match elab_initial loc env root ty ie with | None -> (ty, None) | Some init -> @@ -1553,7 +1737,7 @@ let rec enter_decdefs local loc env = function initializer can refer to the ident *) let (id, env1) = enter_or_refine_ident local loc env s sto' ty in (* process the initializer *) - let (ty', init') = elab_initializer loc env1 ty init in + let (ty', init') = elab_initializer loc env1 s ty init in (* update environment with refined type *) let env2 = Env.add_ident env1 id sto' ty' in (* check for incomplete type *) diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml index c40da18..34d8cf8 100644 --- a/cparser/Unblock.ml +++ b/cparser/Unblock.ml @@ -35,19 +35,23 @@ let rec local_initializer loc env path init k = { edesc = EBinop(Oassign, path, e, path.etyp); etyp = path.etyp } k | Init_array il -> - let ty_elt = + let (ty_elt, sz) = match unroll env path.etyp with - | TArray(ty_elt, _, _) -> ty_elt + | TArray(ty_elt, Some sz, _) -> (ty_elt, sz) | _ -> fatal_error "%aWrong type for array initializer" formatloc loc in - let rec array_init pos = function - | [] -> k - | i :: il -> - local_initializer loc env - { edesc = EBinop(Oindex, path, intconst pos IInt, TPtr(ty_elt, [])); - etyp = ty_elt } - i - (array_init (Int64.succ pos) il) in + let rec array_init pos il = + if pos >= sz then k else begin + let (i1, il') = + match il with + | [] -> (default_init env ty_elt, []) + | i1 :: il' -> (i1, il') in + local_initializer loc env + { edesc = EBinop(Oindex, path, intconst pos IInt, TPtr(ty_elt, [])); + etyp = ty_elt } + i1 + (array_init (Int64.succ pos) il') + end in array_init 0L il | Init_struct(id, fil) -> let field_init (fld, i) k = diff --git a/test/regression/Makefile b/test/regression/Makefile index 4d9683c..57d5db3 100644 --- a/test/regression/Makefile +++ b/test/regression/Makefile @@ -9,7 +9,8 @@ LIBS=$(LIBMATH) # and have reference output in Results TESTS=int32 int64 floats floats-basics \ - expr1 expr6 funptr2 initializers volatile1 volatile2 volatile3 \ + expr1 expr6 funptr2 initializers initializers2 initializers3 \ + volatile1 volatile2 volatile3 \ funct3 expr5 struct7 struct8 struct11 casts1 casts2 char1 \ sizeof1 sizeof2 binops bool for1 @@ -27,8 +28,8 @@ TESTS_DIFF=NaNs # Other tests: should compile to .s without errors (but expect warnings) -EXTRAS=annot1 commaprec expr2 expr3 expr4 extern1 funct2 funptr1 init1 \ - init2 init3 init4 pragmas ptrs1 ptrs2 struct1 struct2 struct3 \ +EXTRAS=annot1 commaprec expr2 expr3 expr4 extern1 funct2 funptr1 \ + pragmas ptrs1 ptrs2 struct1 struct2 struct3 \ struct4 struct5 struct6 struct9 struct10 types1 seqops # Test known to fail diff --git a/test/regression/Results/initializers b/test/regression/Results/initializers index 7474148..a263012 100644 --- a/test/regression/Results/initializers +++ b/test/regression/Results/initializers @@ -21,3 +21,4 @@ x19 = { "Hello", "world!" } x20 = { 'H', 'e', 'l', } x21 = { 'H', 'e', 'l', 'l', 'o', '!', 0, 0, 0, 0, } x22 ok +x23 = { hd = 8, tl = ok } diff --git a/test/regression/Results/initializers2 b/test/regression/Results/initializers2 new file mode 100644 index 0000000..9ba5232 --- /dev/null +++ b/test/regression/Results/initializers2 @@ -0,0 +1,12 @@ +a1 = { 0, 3, 100, 0, 0 } +a2 = { 10, 0, -2, -1, -3 } +a3 = { 1, 2, 5, 6, 7 } (size = 5) +s1 = { 0, 0.00, abc } +s2 = { 13, 4.50, xxx } +s3 = { 0, 0.00, abc } +u1.c = abc +u2.a = 15 +u3.b = 3.14 +u4.c = {0,0,1,0} +pv1 = { {1,2,3}, {11,12,13}, {0,0,0}, {0,3,0}, } +t = { {0,42,43}, {{1,0,0}, {0,1,0}, {0,0,1}, } } diff --git a/test/regression/Results/initializers3 b/test/regression/Results/initializers3 new file mode 100644 index 0000000..8742f8e --- /dev/null +++ b/test/regression/Results/initializers3 @@ -0,0 +1,11 @@ +x5 = { 1, 2, 3, 0, 0, 0, 0, 0, 0, 0, } +x17[7] = { 'H', 'e', 'l', 'l', 'o', '!', 0, } +x18 = "Hello!" +x19 = { "Hello", "world!" } +x20 = { 'H', 'e', 'l', } +x21 = { 'H', 'e', 'l', 'l', 'o', '!', 0, 0, 0, 0, } +f(0,42) = 42, f(1,42) = 43, f(2,42) = 44, f(3,42) = 44, f(4,42) = 44 +s1 = { tag = 0, a = {66,77}, u = {0,0} } +s2 = { tag = 0, a = {0,1}, u = {66,77} } +s3 = { tag = 1, a = {1,0}, u = {'H', 'e', 'l', 'l', 'o', '!', 0, 'X', } } +s4 = { tag = 0, a = {66,77}, u = {88,99} } diff --git a/test/regression/initializers.c b/test/regression/initializers.c index d0a35f3..938795a 100644 --- a/test/regression/initializers.c +++ b/test/regression/initializers.c @@ -54,6 +54,9 @@ char x21[10] = "Hello!"; char * x22 = &(x10.u.y); +/* Initializer can refer to ident just declared */ +struct list { int hd; struct list * tl; } x23 = { sizeof(x23), &x23 }; + static void print_chars(char * s, int sz) { int i; @@ -115,6 +118,8 @@ int main() printf("x22 ok\n"); else printf("x22 error\n"); + printf("x23 = { hd = %d, tl = %s }\n", + x23.hd, x23.tl == &x23 ? "ok" : "ERROR"); return 0; } diff --git a/test/regression/initializers2.c b/test/regression/initializers2.c new file mode 100644 index 0000000..f8d5caf --- /dev/null +++ b/test/regression/initializers2.c @@ -0,0 +1,74 @@ +#include <stdio.h> + +/* Examples of designated initializers from Harbison & Steele */ + +int a1[5] = { [2] = 100, [1] = 3 }; +int a2[5] = { [0] = 10, [2] = -2, -1, -3 }; +int a3[] = { 1, 2, 3, [2] = 5, 6, 7 }; + +struct S { int a; float b; char c[4]; }; +struct S s1 = { .c = "abc" }; +struct S s2 = { 13, 3.3, "xxx", .b = 4.5 }; +struct S s3 = { .c = { 'a', 'b', 'c', '\0' } }; + +union U { int a; float b; char c[4]; }; +union U u1 = { .c = "abc" }; +union U u2 = { .a = 15 }; +union U u3 = { .b = 3.14 }; +union U u4 = { .a = 42, .c[2] = 1 }; + +struct Point { int x; int y; int z; }; +typedef struct Point PointVector[4]; +PointVector pv1 = { + [0].x = 1, [0].y = 2, [0].z = 3, + [1] = { .x = 11, .y = 12, .z = 13 }, + [3] = { .y = 3 } +}; + +typedef int Vector[3]; +typedef int Matrix[3][3]; +struct Trio { Vector v; Matrix m; }; +struct Trio t = { + .m = { [0][0] = 1, [1][1] = 1, [2][2] = 1 }, + .v = { [1] = 42, 43 } +}; + +int main() +{ + int i; + + printf("a1 = { %d, %d, %d, %d, %d }\n", + a1[0], a1[1], a1[2], a1[3], a1[4]); + printf("a2 = { %d, %d, %d, %d, %d }\n", + a2[0], a2[1], a2[2], a2[3], a2[4]); + printf("a3 = { %d, %d, %d, %d, %d } (size = %d)\n", + a3[0], a3[1], a3[2], a3[3], a3[4], + sizeof(a3) / sizeof(int)); + + printf("s1 = { %d, %.2f, %s }\n", + s1.a, s1.b, s1.c); + printf("s2 = { %d, %.2f, %s }\n", + s2.a, s2.b, s2.c); + printf("s3 = { %d, %.2f, %s }\n", + s3.a, s3.b, s3.c); + + printf("u1.c = %s\n", u1.c); + printf("u2.a = %d\n", u2.a); + printf("u3.b = %.2f\n", u3.b); + printf("u4.c = {%d,%d,%d,%d}\n", u4.c[0], u4.c[1], u4.c[2], u4.c[3]); + + printf("pv1 = { "); + for (i = 0; i < 4; i++) + printf("{%d,%d,%d}, ", pv1[i].x, pv1[i].y, pv1[i].z); + printf("}\n"); + + printf("t = { {%d,%d,%d}, ", t.v[0], t.v[1], t.v[2]); + printf("{"); + for (i = 0; i < 3; i++) + printf("{%d,%d,%d}, ", t.m[i][0], t.m[i][1], t.m[i][2]); + printf("} }\n"); + + return 0; +} + + diff --git a/test/regression/initializers3.c b/test/regression/initializers3.c new file mode 100644 index 0000000..359a0f7 --- /dev/null +++ b/test/regression/initializers3.c @@ -0,0 +1,90 @@ +/* Initialization of local variables */ + +#include <stdio.h> + +static void print_chars(char * s, int sz) +{ + int i; + for (i = 0; i < sz; i++) { + if (s[i] >= 32 && s[i] < 127) + printf("'%c', ", s[i]); + else + printf("%d, ", s[i]); + } +} + +/* Initialization of local const array */ + +int f(int x, int y) +{ + const int dfl = 2; + const int tbl[3] = { y, y + 1, y + 2 }; + return tbl[x >= 0 && x < 3 ? x : dfl]; +} + +struct P { int x, y; }; + +struct S { + int tag; + struct P a; + union { + struct P b; + char c[8]; + } u; +}; + +static void print_S(char * name, struct S * s) +{ + printf("%s = { tag = %d, a = {%d,%d}, u = ", name, s->tag, s->a.x, s->a.y); + switch(s->tag) { + case 0: + printf("{%d,%d} }\n", s->u.b.x, s->u.b.y); + break; + case 1: + printf("{"); print_chars(s->u.c, 8); printf("} }\n"); + break; + default: + printf("BAD }\n"); + break; + } +} + + +int main() +{ + /* Initialization of arrays */ + const int x5[10] = { 1, 2, 3 }; + char x17[] = "Hello!"; + char * x18 = "Hello!"; + char * x19[2] = { "Hello", "world!" }; + char x20[3] = "Hello!"; + char x21[10] = "Hello!"; + printf("x5 = { "); + for (int i = 0; i < 10; i++) printf("%d, ", x5[i]); + printf("}\n"); + printf("x17[%d] = { ", (int) sizeof(x17)); + print_chars(x17, sizeof(x17)); + printf("}\n"); + printf("x18 = \"%s\"\n", x18); + printf("x19 = { \"%s\", \"%s\" }\n", x19[0], x19[1]); + printf("x20 = { "); + print_chars(x20, sizeof(x20)); + printf("}\n"); + printf("x21 = { "); + print_chars(x21, sizeof(x21)); + printf("}\n"); + /* Local const arrays */ + printf("f(0,42) = %d, f(1,42) = %d, f(2,42) = %d, f(3,42) = %d, f(4,42) = %d\n", + f(0,42), f(1, 42), f(2, 42), f(3, 42), f(4, 42)); + /* Structs/unions */ + struct P p1 = { 66, 77 }; + struct S s1 = { 0, p1 }; + print_S("s1", &s1); + struct S s2 = { .a.y = 1, .u.c[4] = 'x', .u.b = p1 }; + print_S("s2", &s2); + struct S s3 = { .tag = 1, .a = p1, .a.x = 1, .u.c = "Hello!", .u.c[7] = 'X' }; + print_S("s3", &s3); + struct S s4 = { .tag = 0, .a.x = 1, .a = p1, .u.b = 88, 99 }; + print_S("s4", &s4); + return 0; +} |