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

5 files changed, 361 insertions, 140 deletions

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 =