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 --- cparser/Cprint.ml | 2 +- cparser/Cutil.ml | 28 ++++ cparser/Cutil.mli | 5 + cparser/Elab.ml | 442 +++++++++++++++++++++++++++++++++++++---------------- cparser/Unblock.ml | 24 +-- 5 files changed, 361 insertions(+), 140 deletions(-) (limited to 'cparser') diff --git a/cparser/Cprint.ml b/cparser/Cprint.ml index 0bbea683..f26025e9 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 "@[{%a}@]" init i + fprintf pp "@[{.%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 302c1cfe..22ef187a 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 35f7338f..9f59a764 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 90662a3e..e468ab29 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 c40da18e..34d8cf8e 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 = -- cgit