Delay reads from !Machine.config before it is properly initialized.

Several definitions in Cutil and elsewhere were accessing the default
value of !Machine.config, before it is properly initialized in Driver.
Delay evaluation of these definitions, and initialize Machine.config
to nonsensical values so that lack of initialization is caught early
(e.g. in Cutil.find_matching_*_kind).

Also, following up on commit [3b8a094], don't use "wchar_t" typedef
to type wide string literals, even if this typedef is in scope.
The risk here is to hide an inconsistency between "wchar_t"'s definition
in standard headers and CompCert's built-in definition.

7 files changed, 86 insertions, 66 deletions

diff --git a/cparser/Ceval.ml b/cparser/Ceval.ml
index 39cda58c..ba7cdabc 100644
--- a/cparser/Ceval.ml
+++ b/cparser/Ceval.ml
@@ -102,7 +102,7 @@ let cast env ty_to ty_from v =
       then v
       else raise Notconst
   | TPtr(ty, _), I n ->
-      I (normalize_int n ptr_t_ikind)
+      I (normalize_int n (ptr_t_ikind ()))
   | TPtr(ty, _), (S _ | WS _) ->
       v
   | TEnum(_, _), I n ->
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index 9093b230..9e7f102e 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -707,41 +707,34 @@ let type_of_member env fld =
 (** Special types *)
 
 let find_matching_unsigned_ikind sz =
+  assert (sz > 0);
   if sz = !config.sizeof_int then IUInt
   else if sz = !config.sizeof_long then IULong
   else if sz = !config.sizeof_longlong then IULongLong
   else assert false
 
 let find_matching_signed_ikind sz =
+  assert (sz > 0);
   if sz = !config.sizeof_int then IInt
   else if sz = !config.sizeof_long then ILong
   else if sz = !config.sizeof_longlong then ILongLong
   else assert false
 
-let wchar_ikind =
+let wchar_ikind () =
   if !config.wchar_signed
   then find_matching_signed_ikind !config.sizeof_wchar
   else find_matching_unsigned_ikind !config.sizeof_wchar
-let size_t_ikind = find_matching_unsigned_ikind !config.sizeof_size_t
-let ptr_t_ikind = find_matching_unsigned_ikind !config.sizeof_ptr
-let ptrdiff_t_ikind = find_matching_signed_ikind !config.sizeof_ptrdiff_t
-
-(** The wchar_t type.  Try to get it from a typedef in the environment,
-  otherwise use the integer type described in !config. *)
-
-let wchar_type env =
-  try
-    let (id, def) = Env.lookup_typedef env "wchar_t" in TNamed(id, [])
-  with Env.Error _ ->
-    TInt(wchar_ikind, [])
+let size_t_ikind () = find_matching_unsigned_ikind !config.sizeof_size_t
+let ptr_t_ikind () = find_matching_unsigned_ikind !config.sizeof_ptr
+let ptrdiff_t_ikind () = find_matching_signed_ikind !config.sizeof_ptrdiff_t
 
 (** The type of a constant *)
 
-let type_of_constant env = function
+let type_of_constant = function
   | CInt(_, ik, _) -> TInt(ik, [])
   | CFloat(_, fk) -> TFloat(fk, [])
   | CStr _ -> TPtr(TInt(IChar, []), [])
-  | CWStr _ -> TPtr(wchar_type env, [])
+  | CWStr _ -> TPtr(TInt(wchar_ikind(), []), [])
   | CEnum(_, _) -> TInt(IInt, [])
 
 (* Check that a C expression is a lvalue *)
@@ -829,15 +822,14 @@ let floatconst0 =
   { edesc = EConst(CFloat({hex=false; intPart="0"; fracPart="0"; exp="0"}, FDouble));
     etyp = TFloat(FDouble, []) }
 
-(* Construct the literal "0" with void * type *)
-
-let nullconst =
-  { edesc = EConst(CInt(0L, ptr_t_ikind, "0")); etyp = TPtr(TVoid [], []) }
-
 (* Construct a cast expression *)
 
 let ecast ty e = { edesc = ECast(ty, e); etyp = ty }
 
+(* Construct the literal "0" with void * type *)
+
+let nullconst = ecast (TPtr(TVoid [], [])) (intconst 0L IInt)
+
 (* Construct an assignment expression *)
 
 let eassign e1 e2 = { edesc = EBinop(Oassign, e1, e2, e1.etyp); etyp = e1.etyp }
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index 53bcfcea..bd52badf 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -156,20 +156,20 @@ val default_argument_conversion : Env.t -> typ -> typ
 (* Special types *)
 val enum_ikind : ikind
   (* Integer kind for enum values.  Always [IInt]. *)
-val wchar_ikind : ikind
-  (* Integer kind for wchar_t type.  Unsigned. *)
-val size_t_ikind : ikind
+val wchar_ikind : unit -> ikind
+  (* Integer kind for wchar_t type. *)
+val size_t_ikind : unit -> ikind
   (* Integer kind for size_t type.  Unsigned. *)
-val ptr_t_ikind : ikind
+val ptr_t_ikind : unit -> ikind
   (* Integer kind for ptr_t type.  Smallest unsigned kind large enough
      to contain a pointer without information loss. *)
-val ptrdiff_t_ikind : ikind
+val ptrdiff_t_ikind : unit -> ikind
   (* Integer kind for ptrdiff_t type.  Smallest signed kind large enough
      to contain the difference between two pointers. *)
 
 (* Helpers for type-checking *)
 
-val type_of_constant : Env.t -> constant -> typ
+val type_of_constant : constant -> typ
   (* Return the type of the given constant. *)
 val type_of_member : Env.t -> field -> typ
   (* Return the type of accessing the given field [fld].
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index faffc36f..bad92cf6 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1198,7 +1198,7 @@ let elab_expr loc env a =
 
   | CONSTANT cst ->
       let cst' = elab_constant loc cst in
-      { edesc = EConst cst'; etyp = type_of_constant env cst' }
+      { edesc = EConst cst'; etyp = type_of_constant cst' }
 
 (* 6.5.2 Postfix expressions *)
 
@@ -1339,31 +1339,31 @@ let elab_expr loc env a =
         match b1.edesc with
         | EConst(CStr s) ->
             let sz = String.length s + 1 in
-            EConst(CInt(Int64.of_int sz, size_t_ikind, ""))
+            EConst(CInt(Int64.of_int sz, size_t_ikind(), ""))
         | EConst(CWStr s) ->
             let sz = (!config).sizeof_wchar * (List.length s + 1) in
-            EConst(CInt(Int64.of_int sz, size_t_ikind, ""))
+            EConst(CInt(Int64.of_int sz, size_t_ikind(), ""))
         | _ ->
             ESizeof b1.etyp in
-      { edesc = bdesc; etyp = TInt(size_t_ikind, []) }
+      { edesc = bdesc; etyp = TInt(size_t_ikind(), []) }
 
   | TYPE_SIZEOF (spec, dcl) ->
       let (ty, env') = elab_type loc env spec dcl in
       if wrap incomplete_type loc env' ty then
         err "incomplete type %a" Cprint.typ ty;
-      { edesc = ESizeof ty; etyp = TInt(size_t_ikind, []) }
+      { edesc = ESizeof ty; etyp = TInt(size_t_ikind(), []) }
 
   | EXPR_ALIGNOF a1 ->
       let b1 = elab a1 in
       if wrap incomplete_type loc env b1.etyp then
         err "incomplete type %a" Cprint.typ b1.etyp;
-      { edesc = EAlignof b1.etyp; etyp =  TInt(size_t_ikind, []) }
+      { edesc = EAlignof b1.etyp; etyp =  TInt(size_t_ikind(), []) }
 
   | TYPE_ALIGNOF (spec, dcl) ->
       let (ty, env') = elab_type loc env spec dcl in
       if wrap incomplete_type loc env' ty then
         err "incomplete type %a" Cprint.typ ty;
-      { edesc = EAlignof ty; etyp =  TInt(size_t_ikind, []) }
+      { edesc = EAlignof ty; etyp =  TInt(size_t_ikind(), []) }
 
   | UNARY(PLUS, a1) ->
       let b1 = elab a1 in
@@ -1465,7 +1465,7 @@ let elab_expr loc env a =
                 err "illegal pointer arithmetic in binary '-'";
               if wrap sizeof loc env ty1 = Some 0 then
                 err "subtraction between two pointers to zero-sized objects";
-              (TPtr(ty1, []), TInt(ptrdiff_t_ikind, []))
+              (TPtr(ty1, []), TInt(ptrdiff_t_ikind(), []))
           | _, _ -> error "type error in binary '-'"
         end in
       { edesc = EBinop(Osub, b1, b2, tyop); etyp = tyres }
diff --git a/cparser/GCC.ml b/cparser/GCC.ml
index 1bcbbbc8..030f300b 100644
--- a/cparser/GCC.ml
+++ b/cparser/GCC.ml
@@ -35,7 +35,7 @@ let voidConstPtrType = TPtr(TVoid [AConst], [])
 let charPtrType = TPtr(TInt(IChar, []), [])
 let charConstPtrType = TPtr(TInt(IChar, [AConst]), [])
 let intPtrType = TPtr(TInt(IInt, []), [])
-let sizeType = TInt(size_t_ikind, [])
+let sizeType() = TInt(size_t_ikind(), [])
 
 let builtins = {
   Builtins.typedefs = [
@@ -43,22 +43,22 @@ let builtins = {
 ];
   Builtins.functions = [
   "__builtin___fprintf_chk",  (intType, [ voidPtrType; intType; charConstPtrType ], true) (* first argument is really FILE*, not void*, but we don't want to build in the definition for FILE *);
-  "__builtin___memcpy_chk",  (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType; sizeType ], false);
-  "__builtin___memmove_chk",  (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType; sizeType ], false);
-  "__builtin___mempcpy_chk",  (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType; sizeType ], false);
-  "__builtin___memset_chk",  (voidPtrType, [ voidPtrType; intType; sizeType; sizeType ], false);
+  "__builtin___memcpy_chk",  (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType(); sizeType() ], false);
+  "__builtin___memmove_chk",  (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType(); sizeType() ], false);
+  "__builtin___mempcpy_chk",  (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType(); sizeType() ], false);
+  "__builtin___memset_chk",  (voidPtrType, [ voidPtrType; intType; sizeType(); sizeType() ], false);
   "__builtin___printf_chk",  (intType, [ intType; charConstPtrType ], true);
-  "__builtin___snprintf_chk",  (intType, [ charPtrType; sizeType; intType; sizeType; charConstPtrType ], true);
-  "__builtin___sprintf_chk",  (intType, [ charPtrType; intType; sizeType; charConstPtrType ], true);
-  "__builtin___stpcpy_chk",  (charPtrType, [ charPtrType; charConstPtrType; sizeType ], false);
-  "__builtin___strcat_chk",  (charPtrType, [ charPtrType; charConstPtrType; sizeType ], false);
-  "__builtin___strcpy_chk",  (charPtrType, [ charPtrType; charConstPtrType; sizeType ], false);
-  "__builtin___strncat_chk",  (charPtrType, [ charPtrType; charConstPtrType; sizeType; sizeType ], false);
-  "__builtin___strncpy_chk",  (charPtrType, [ charPtrType; charConstPtrType; sizeType; sizeType ], false);
+  "__builtin___snprintf_chk",  (intType, [ charPtrType; sizeType(); intType; sizeType(); charConstPtrType ], true);
+  "__builtin___sprintf_chk",  (intType, [ charPtrType; intType; sizeType(); charConstPtrType ], true);
+  "__builtin___stpcpy_chk",  (charPtrType, [ charPtrType; charConstPtrType; sizeType() ], false);
+  "__builtin___strcat_chk",  (charPtrType, [ charPtrType; charConstPtrType; sizeType() ], false);
+  "__builtin___strcpy_chk",  (charPtrType, [ charPtrType; charConstPtrType; sizeType() ], false);
+  "__builtin___strncat_chk",  (charPtrType, [ charPtrType; charConstPtrType; sizeType(); sizeType() ], false);
+  "__builtin___strncpy_chk",  (charPtrType, [ charPtrType; charConstPtrType; sizeType(); sizeType() ], false);
   "__builtin___vfprintf_chk",  (intType, [ voidPtrType; intType; charConstPtrType; voidPtrType ], false) (* first argument is really FILE*, not void*, but we don't want to build in the definition for FILE *);
   "__builtin___vprintf_chk",  (intType, [ intType; charConstPtrType; voidPtrType ], false);
-  "__builtin___vsnprintf_chk",  (intType, [ charPtrType; sizeType; intType; sizeType; charConstPtrType; voidPtrType ], false);
-  "__builtin___vsprintf_chk",  (intType, [ charPtrType; intType; sizeType; charConstPtrType; voidPtrType ], false);
+  "__builtin___vsnprintf_chk",  (intType, [ charPtrType; sizeType(); intType; sizeType(); charConstPtrType; voidPtrType ], false);
+  "__builtin___vsprintf_chk",  (intType, [ charPtrType; intType; sizeType(); charConstPtrType; voidPtrType ], false);
 
   "__builtin_acos",  (doubleType, [ doubleType ], false);
   "__builtin_acosf",  (floatType, [ floatType ], false);
@@ -124,8 +124,8 @@ let builtins = {
   "__builtin_inf",  (doubleType, [], false);
   "__builtin_inff",  (floatType, [], false);
   "__builtin_infl",  (longDoubleType, [], false);
-  "__builtin_memcpy",  (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType ], false);
-  "__builtin_mempcpy",  (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType ], false);
+  "__builtin_memcpy",  (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType() ], false);
+  "__builtin_mempcpy",  (voidPtrType, [ voidPtrType; voidConstPtrType; sizeType() ], false);
 
   "__builtin_fmod",  (doubleType, [ doubleType ], false);
   "__builtin_fmodf",  (floatType, [ floatType ], false);
@@ -162,7 +162,7 @@ let builtins = {
   "__builtin_nansf",  (floatType, [ charConstPtrType ], false);
   "__builtin_nansl",  (longDoubleType, [ charConstPtrType ], false);
   "__builtin_next_arg",  (voidPtrType, [], false);
-  "__builtin_object_size",  (sizeType, [ voidPtrType; intType ], false);
+  "__builtin_object_size",  (sizeType(), [ voidPtrType; intType ], false);
 
   "__builtin_parity",  (intType, [ uintType ], false);
   "__builtin_parityl",  (intType, [ ulongType ], false);
@@ -196,9 +196,9 @@ let builtins = {
   "__builtin_strcmp",  (intType, [ charConstPtrType; charConstPtrType ], false);
   "__builtin_strcpy",  (charPtrType, [ charPtrType; charConstPtrType ], false);
   "__builtin_strcspn",  (uintType, [ charConstPtrType; charConstPtrType ], false);
-  "__builtin_strncat",  (charPtrType, [ charPtrType; charConstPtrType; sizeType ], false);
-  "__builtin_strncmp",  (intType, [ charConstPtrType; charConstPtrType; sizeType ], false);
-  "__builtin_strncpy",  (charPtrType, [ charPtrType; charConstPtrType; sizeType ], false);
+  "__builtin_strncat",  (charPtrType, [ charPtrType; charConstPtrType; sizeType() ], false);
+  "__builtin_strncmp",  (intType, [ charConstPtrType; charConstPtrType; sizeType() ], false);
+  "__builtin_strncpy",  (charPtrType, [ charPtrType; charConstPtrType; sizeType() ], false);
   "__builtin_strspn",  (intType, [ charConstPtrType; charConstPtrType ], false);
   "__builtin_strpbrk",  (charPtrType, [ charConstPtrType; charConstPtrType ], false);
   "__builtin_tan",  (doubleType, [ doubleType ], false);
@@ -217,9 +217,7 @@ let builtins = {
   "__builtin_va_start",  (voidType, [ voidPtrType; voidPtrType ], false);
   "__builtin_stdarg_start",  (voidType, [ voidPtrType ], false);
   (* When we parse builtin_va_arg, type argument becomes sizeof type *)
-  "__builtin_va_arg",  (voidType, [ voidPtrType; sizeType ], false);
-  "__builtin_va_copy",  (voidType, [ voidPtrType;
-                                           voidPtrType ],
-                              false)
+  "__builtin_va_arg",  (voidType, [ voidPtrType; sizeType() ], false);
+  "__builtin_va_copy",  (voidType, [ voidPtrType; voidPtrType ], false)
 ]
 }
diff --git a/cparser/Machine.ml b/cparser/Machine.ml
index 6a7f5054..b215505b 100644
--- a/cparser/Machine.ml
+++ b/cparser/Machine.ml
@@ -173,10 +173,40 @@ let gcc_extensions c =
   { c with sizeof_void = Some 1; sizeof_fun = Some 1;
            alignof_void = Some 1; alignof_fun = Some 1 }
 
-(* Default configuration *)
+(* Undefined configuration *)
 
-let config =
-  ref (match Sys.word_size with
-           | 32 -> if Sys.os_type = "Win32" then win32 else ilp32ll64
-           | 64 -> if Sys.os_type = "Win32" then win64 else i32lpll64
-           | _  -> assert false)
+let undef = {
+  name = "UNDEFINED";
+  char_signed = false;
+  sizeof_ptr = 0;
+  sizeof_short = 0;
+  sizeof_int = 0;
+  sizeof_long = 0;
+  sizeof_longlong = 0;
+  sizeof_float = 0;
+  sizeof_double = 0;
+  sizeof_longdouble = 0;
+  sizeof_void = None;
+  sizeof_fun = None;
+  sizeof_wchar = 0;
+  wchar_signed = true;
+  sizeof_size_t = 0;
+  sizeof_ptrdiff_t = 0;
+  alignof_ptr = 0;
+  alignof_short = 0;
+  alignof_int = 0;
+  alignof_long = 0;
+  alignof_longlong = 0;
+  alignof_float = 0;
+  alignof_double = 0;
+  alignof_longdouble = 0;
+  alignof_void = None;
+  alignof_fun = None;
+  bigendian = false;
+  bitfields_msb_first = false;
+  struct_return_as_int = 0
+}
+
+(* The current configuration.  Must be initialized before use. *)
+
+let config = ref undef
diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml
index 686a7d39..1f602fc1 100644
--- a/cparser/PackedStructs.ml
+++ b/cparser/PackedStructs.ml
@@ -138,7 +138,7 @@ let accessor_type loc env ty =
   match unroll env ty with
   | TInt(ik,_) -> (8 * sizeof_ikind ik, TInt(unsigned_ikind_of ik,[]))
   | TEnum(_,_) -> (8 * sizeof_ikind enum_ikind, TInt(unsigned_ikind_of enum_ikind,[]))
-  | TPtr _     -> (8 * !config.sizeof_ptr, TInt(ptr_t_ikind,[]))
+  | TPtr _     -> (8 * !config.sizeof_ptr, TInt(ptr_t_ikind(),[]))
   | _ ->
      error "%a: unsupported type for byte-swapped field access" formatloc loc;
      (32, TVoid [])