From 10120fe4d9980139e44012888a91716df2edf2e0 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Mon, 29 Dec 2014 11:51:25 +0100
Subject: Support "asm volatile" (closes: PR#5). The CompCert back-end already
 treats "asm" inserts as "volatile" in GCC's sense (performing unpredictable
 side-effects), so no change is required outside of the parser.

---
 cparser/Parser.vy      | 2 ++
 cparser/pre_parser.mly | 2 +-
 2 files changed, 3 insertions(+), 1 deletion(-)

(limited to 'cparser')

diff --git a/cparser/Parser.vy b/cparser/Parser.vy
index ce1beae0..a058a8d1 100644
--- a/cparser/Parser.vy
+++ b/cparser/Parser.vy
@@ -822,6 +822,8 @@ jump_statement:
 asm_statement:
 | loc = ASM LPAREN template = STRING_LITERAL RPAREN SEMICOLON
     { let '(wide, chars, _) := template in ASM wide chars loc }
+| loc = ASM VOLATILE LPAREN template = STRING_LITERAL RPAREN SEMICOLON
+    { let '(wide, chars, _) := template in ASM wide chars loc }
 
 (* 6.9 *)
 translation_unit_file:
diff --git a/cparser/pre_parser.mly b/cparser/pre_parser.mly
index 4755518b..ef356d3a 100644
--- a/cparser/pre_parser.mly
+++ b/cparser/pre_parser.mly
@@ -616,7 +616,7 @@ jump_statement:
     {}
 
 asm_statement:
-| ASM LPAREN string_literals_list RPAREN SEMICOLON
+| ASM VOLATILE? LPAREN string_literals_list RPAREN SEMICOLON
     {}
 
 translation_unit_file:
-- 
cgit 


From a4b766d7b50be79a1d983dbe5f234e951ba0aa46 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Mon, 29 Dec 2014 13:09:59 +0100
Subject: Recognize more of GCC's alternate keywords (e.g. "__signed"). Based
 on the source of GCC 4.9.2. Plus: reordered keywords in alphabetic order to
 facilitate comparison.

---
 cparser/Lexer.mll | 45 ++++++++++++++++++++++++---------------------
 1 file changed, 24 insertions(+), 21 deletions(-)

(limited to 'cparser')

diff --git a/cparser/Lexer.mll b/cparser/Lexer.mll
index 3ab83902..13c1248b 100644
--- a/cparser/Lexer.mll
+++ b/cparser/Lexer.mll
@@ -28,13 +28,34 @@ let init filename channel : Lexing.lexbuf =
   Hashtbl.clear lexicon;
   List.iter
     (fun (key, builder) -> Hashtbl.add lexicon key builder)
-    [ ("auto", fun loc -> AUTO loc);
+    [ 
+      ("_Alignas", fun loc -> ALIGNAS loc);
+      ("_Alignof", fun loc -> ALIGNOF loc);
+      ("_Bool", fun loc -> UNDERSCORE_BOOL loc);
+      ("__alignof", fun loc -> ALIGNOF loc);
+      ("__alignof__", fun loc -> ALIGNOF loc);
+      ("__asm", fun loc -> ASM loc);
+      ("__asm__", fun loc -> ASM loc);
+      ("__attribute", fun loc -> ATTRIBUTE loc);
+      ("__attribute__", fun loc -> ATTRIBUTE loc);
+      ("__builtin_va_arg", fun loc -> BUILTIN_VA_ARG loc);
+      ("__const", fun loc -> CONST loc);
+      ("__const__", fun loc -> CONST loc);
+      ("__inline", fun loc -> INLINE loc);
+      ("__inline__", fun loc -> INLINE loc);
+      ("__packed__", fun loc -> PACKED loc);
+      ("__restrict", fun loc -> RESTRICT loc);
+      ("__restrict__", fun loc -> RESTRICT loc);
+      ("__signed", fun loc -> SIGNED loc);
+      ("__signed__", fun loc -> SIGNED loc);
+      ("__volatile", fun loc -> VOLATILE loc);
+      ("__volatile__", fun loc -> VOLATILE loc);
+      ("asm", fun loc -> ASM loc);
+      ("auto", fun loc -> AUTO loc);
       ("break", fun loc -> BREAK loc);
       ("case", fun loc -> CASE loc);
       ("char", fun loc -> CHAR loc);
       ("const", fun loc -> CONST loc);
-      ("__const", fun loc -> CONST loc);
-      ("__const__", fun loc -> CONST loc);
       ("continue", fun loc -> CONTINUE loc);
       ("default", fun loc -> DEFAULT loc);
       ("do", fun loc -> DO loc);
@@ -47,14 +68,10 @@ let init filename channel : Lexing.lexbuf =
       ("goto", fun loc -> GOTO loc);
       ("if", fun loc -> IF loc);
       ("inline", fun loc -> INLINE loc);
-      ("__inline", fun loc -> INLINE loc);
-      ("__inline__", fun loc -> INLINE loc);
       ("int", fun loc -> INT loc);
       ("long", fun loc -> LONG loc);
       ("register", fun loc -> REGISTER loc);
       ("restrict", fun loc -> RESTRICT loc);
-      ("__restrict", fun loc -> RESTRICT loc);
-      ("__restrict__", fun loc -> RESTRICT loc);
       ("return", fun loc -> RETURN loc);
       ("short", fun loc -> SHORT loc);
       ("signed", fun loc -> SIGNED loc);
@@ -67,21 +84,7 @@ let init filename channel : Lexing.lexbuf =
       ("unsigned", fun loc -> UNSIGNED loc);
       ("void", fun loc -> VOID loc);
       ("volatile", fun loc -> VOLATILE loc);
-      ("__volatile", fun loc -> VOLATILE loc);
-      ("__volatile__", fun loc -> VOLATILE loc);
       ("while", fun loc -> WHILE loc);
-      ("_Alignas", fun loc -> ALIGNAS loc);
-      ("_Alignof", fun loc -> ALIGNOF loc);
-      ("__alignof", fun loc -> ALIGNOF loc);
-      ("__alignof__", fun loc -> ALIGNOF loc);
-      ("__attribute", fun loc -> ATTRIBUTE loc);
-      ("__attribute__", fun loc -> ATTRIBUTE loc);
-      ("_Bool", fun loc -> UNDERSCORE_BOOL loc);
-      ("__builtin_va_arg", fun loc -> BUILTIN_VA_ARG loc);
-      ("__packed__", fun loc -> PACKED loc);
-      ("__asm__", fun loc -> ASM loc);
-      ("__asm", fun loc -> ASM loc);
-      ("asm", fun loc -> ASM loc);
     ];
 
   push_context := begin fun () -> contexts := []::!contexts end;
-- 
cgit 


From 018ff51afad3d9c148622a50de83a2f787f6dc10 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Tue, 30 Dec 2014 12:28:37 +0100
Subject: PR#10: composite definitions must be maintained in the environment.

---
 cparser/Unblock.ml | 21 +++++++++++++++------
 1 file changed, 15 insertions(+), 6 deletions(-)

(limited to 'cparser')

diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml
index ba8e379c..8d6518bd 100644
--- a/cparser/Unblock.ml
+++ b/cparser/Unblock.ml
@@ -157,7 +157,7 @@ and expand_init islocal env i =
   let rec expand i =
     match i with
     (* The following "flattening" is not C99.  GCC documents it; whether
-       it implements it is unclear, Clang implements it.  At any rate,
+       it implements it is unclear.  Clang implements it.  At any rate,
        it makes it possible to use compound literals in static initializers,
        something that is not possible in C99 because compound literals
        are not constant expressions.
@@ -256,8 +256,8 @@ let unblock_decl loc env ((sto, id, ty, optinit) as d) =
       decls @ [(sto, id, ty, Some init')]
 
 (* Unblocking and simplification for whole files.
-   The environment is used for typedefs only, so we do not maintain
-   other declarations. *)
+   The environment is used for typedefs and composites only,
+   so we do not maintain variable and function definitions. *)
 
 let rec unblock_glob env accu = function
   | [] -> List.rev accu
@@ -273,11 +273,20 @@ let rec unblock_glob env accu = function
       | Gfundef f ->
           let f' = unblock_fundef env f in
           unblock_glob env ({g with gdesc = Gfundef f'} :: accu) gl
+      | Gcompositedecl(su, id, attr) ->
+          unblock_glob
+            (Env.add_composite env id (composite_info_decl env su attr))
+            (g :: accu) gl
+      | Gcompositedef(su, id, attr, fl) ->
+          unblock_glob
+            (Env.add_composite env id (composite_info_def env su attr fl))
+            (g :: accu) gl
       | Gtypedef(id, ty) ->
           unblock_glob (Env.add_typedef env id ty) (g :: accu) gl
-      | Gcompositedecl _
-      | Gcompositedef _
-      | Genumdef _ 
+      | Genumdef (id, attr, members) ->
+          unblock_glob
+            (Env.add_enum env id {ei_members =  members; ei_attr = attr})
+            (g :: accu) gl
       | Gpragma _ ->
           unblock_glob env (g :: accu) gl
 
-- 
cgit 


From 7cce5af2b184bbb7b037b2a32793c7bfa287da72 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Tue, 30 Dec 2014 12:53:17 +0100
Subject: PR#10 continued: disambiguate record to avoid OCaml warning

---
 cparser/Unblock.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'cparser')

diff --git a/cparser/Unblock.ml b/cparser/Unblock.ml
index 8d6518bd..405986f3 100644
--- a/cparser/Unblock.ml
+++ b/cparser/Unblock.ml
@@ -285,7 +285,7 @@ let rec unblock_glob env accu = function
           unblock_glob (Env.add_typedef env id ty) (g :: accu) gl
       | Genumdef (id, attr, members) ->
           unblock_glob
-            (Env.add_enum env id {ei_members =  members; ei_attr = attr})
+            (Env.add_enum env id {Env.ei_members =  members; Env.ei_attr = attr})
             (g :: accu) gl
       | Gpragma _ ->
           unblock_glob env (g :: accu) gl
-- 
cgit 


From e6b5004af0960958aab6cbdc9f24a06f00d104eb Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Tue, 30 Dec 2014 12:54:43 +0100
Subject: Improve printing of errors.

---
 cparser/Env.ml | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

(limited to 'cparser')

diff --git a/cparser/Env.ml b/cparser/Env.ml
index 355a9960..6610c159 100644
--- a/cparser/Env.ml
+++ b/cparser/Env.ml
@@ -266,16 +266,24 @@ let add_enum env id info =
 
 open Printf
 
+let composite_tag_name name =
+  if name = "" then "<anonymous>" else name
+
 let error_message = function
   | Unbound_identifier name -> 
       sprintf "Unbound identifier '%s'" name
   | Unbound_tag(name, kind) ->
-      sprintf "Unbound %s '%s'" kind name
+      sprintf "Unbound %s '%s'" kind (composite_tag_name name)
   | Tag_mismatch(name, expected, actual) ->
       sprintf "'%s' was declared as a %s but is used as a %s" 
-              name actual expected
+              (composite_tag_name name) actual expected
   | Unbound_typedef name ->
       sprintf "Unbound typedef '%s'" name
   | No_member(compname, compkind, memname) ->
       sprintf "%s '%s' has no member named '%s'"
-              compkind compname memname
+              compkind (composite_tag_name compname) memname
+
+let _ =
+  Printexc.register_printer
+    (function Error e -> Some (sprintf "Env.Error \"%s\"" (error_message e))
+            | _ -> None)
-- 
cgit 


From 2d32afc5daf16c75d1a34f2716c34ae2e1efcce4 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Tue, 30 Dec 2014 12:55:51 +0100
Subject: PR#11: support sizeof(struct {...}) and _Alignof(struct {...})

This is a partial fix because other cases of struct definitions within type-names are still not handled, e.g. (struct { ... } *) <expr>.  However, error reporting was improved for these cases.
---
 cparser/Elab.ml | 63 ++++++++++++++++++++++++++++++++++-----------------------
 1 file changed, 38 insertions(+), 25 deletions(-)

(limited to 'cparser')

diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 43a72a0e..dd42ae24 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -44,6 +44,10 @@ let wrap fn loc env arg =
   try fn env arg
   with Env.Error msg -> fatal_error loc "%s" (Env.error_message msg)
 
+let wrap2 fn loc env arg1 arg2 =
+  try fn env arg1 arg2
+  with Env.Error msg -> fatal_error loc "%s" (Env.error_message msg)
+
 (* Translation of locations *)
 
 let elab_loc l = (l.filename, l.lineno)
@@ -786,7 +790,7 @@ let elab_type loc env spec decl =
   let (ty, env'') = elab_type_declarator loc env' bty decl in 
   if sto <> Storage_default || inl || tydef then
     error loc "'typedef', 'extern', 'static', 'register' and 'inline' are meaningless in cast";
-  ty
+  (ty, env'')
 
 
 (* Elaboration of initializers. C99 section 6.7.8 *)
@@ -820,8 +824,8 @@ let init_int_array_wstring opt_size s =
   Init_array (add_chars (Int64.pred size) (List.rev s) [])
 
 let check_init_type loc env a ty =
-  if valid_assignment env a ty then ()
-  else if valid_cast env a.etyp ty then
+  if wrap2 valid_assignment loc env a ty then ()
+  else if wrap2 valid_cast loc env a.etyp ty then
     warning loc
       "initializer has type@ %a@ instead of the expected type @ %a"
       Cprint.typ a.etyp Cprint.typ ty
@@ -1309,16 +1313,18 @@ let elab_expr loc env a =
 (* 6.5.4 Cast operators *)
 
   | CAST ((spec, dcl), SINGLE_INIT a1) ->
-      let ty = elab_type loc env spec dcl in
+      let (ty, _) = elab_type loc env spec dcl in
       let b1 = elab a1 in
-      if not (valid_cast env b1.etyp ty) then
+      if not (wrap2 valid_cast loc env b1.etyp ty) then
         err "illegal cast from %a@ to %a" Cprint.typ b1.etyp Cprint.typ ty;
       { edesc = ECast(ty, b1); etyp = ty }
 
 (* 6.5.2.5 Compound literals *)
 
   | CAST ((spec, dcl), ie) ->
-      let ty = elab_type loc env spec dcl in
+      let (ty, _) = elab_type loc env spec dcl in
+      if wrap incomplete_type loc env ty then
+        err "incomplete type %a" Cprint.typ ty;
       begin match elab_initializer loc env "<compound literal>" ty ie with
       | (ty', Some i) -> { edesc = ECompound(ty', i); etyp = ty' }
       | (ty', None)   -> error "ill-formed compound literal"
@@ -1344,8 +1350,8 @@ let elab_expr loc env a =
       { edesc = bdesc; etyp = TInt(size_t_ikind, []) }
 
   | TYPE_SIZEOF (spec, dcl) ->
-      let ty = elab_type loc env spec dcl in
-      if wrap incomplete_type loc env ty then
+      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, []) }
 
@@ -1356,8 +1362,8 @@ let elab_expr loc env a =
       { edesc = EAlignof b1.etyp; etyp =  TInt(size_t_ikind, []) }
 
   | TYPE_ALIGNOF (spec, dcl) ->
-      let ty = elab_type loc env spec dcl in
-      if wrap incomplete_type loc env ty then
+      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, []) }
 
@@ -1544,8 +1550,8 @@ let elab_expr loc env a =
         err "left-hand side of assignment has 'const' type";
       if not (is_modifiable_lvalue env b1) then
         err "left-hand side of assignment is not a modifiable l-value";
-      if not (valid_assignment env b2 b1.etyp) then begin
-        if valid_cast env b2.etyp b1.etyp then
+      if not (wrap2 valid_assignment loc env b2 b1.etyp) then begin
+        if wrap2 valid_cast loc env b2.etyp b1.etyp then
           warning "assigning a value of type@ %a@ to a lvalue of type@ %a"
                   Cprint.typ b2.etyp Cprint.typ b1.etyp
         else
@@ -1576,8 +1582,8 @@ let elab_expr loc env a =
             err "left-hand side of assignment has 'const' type";
           if not (is_modifiable_lvalue env b1) then
             err ("left-hand side of assignment is not a modifiable l-value");
-          if not (valid_assignment env b b1.etyp) then begin
-            if valid_cast env ty b1.etyp then
+          if not (wrap2 valid_assignment loc env b b1.etyp) then begin
+            if wrap2 valid_cast loc env ty b1.etyp then
               warning "assigning a value of type@ %a@ to a lvalue of type@ %a"
                       Cprint.typ ty Cprint.typ b1.etyp
             else
@@ -1689,8 +1695,9 @@ let elab_expr loc env a =
         else (err "too many arguments in function call"; args)
     | arg1 :: argl, (_, ty_p) :: paraml ->
         let ty_a = argument_conversion env arg1.etyp in
-        if not (valid_assignment env {arg1 with etyp = ty_a} ty_p) then begin
-          if valid_cast env ty_a ty_p then
+        if not (wrap2 valid_assignment loc env {arg1 with etyp = ty_a} ty_p)
+        then begin
+          if wrap2 valid_cast loc env ty_a ty_p then
             warning
               "argument #%d of function call has type@ %a@ \
                instead of the expected type@ %a"
@@ -1770,13 +1777,18 @@ let enter_decdefs local loc env sto dl =
   if sto <> Storage_default && dl = [] then
     warning loc "Storage class specifier on empty declaration";
   let rec enter_decdef (decls, env) (s, ty, init) =
-    let isfun = is_function_type env ty in
     if sto = Storage_extern && init <> NO_INIT then
       error loc "'extern' declaration cannot have an initializer";
-    if local && isfun && (sto = Storage_static || sto = Storage_register) then
-      error loc "invalid storage class for '%s'" s;
-    (* Local function declarations are always treated as extern *)
-    let sto1 = if local && isfun then Storage_extern else sto in
+    (* Adjust storage for function declarations *)
+    let sto1 =
+      match unroll env ty, sto with
+      | TFun _, Storage_default -> 
+          Storage_extern
+      | TFun _, (Storage_static | Storage_register) ->
+          if local then error loc "invalid storage class for '%s'" s;
+          sto
+      | _, _ ->
+          sto in
     (* enter ident in environment with declared type, because
        initializer can refer to the ident *)
     let (id, sto', env1) = enter_or_refine_ident local loc env s sto1 ty in
@@ -1786,10 +1798,10 @@ let enter_decdefs local loc env sto dl =
     let env2 = Env.add_ident env1 id sto' ty' in
     (* check for incomplete type *)
     if local && sto' <> Storage_extern
-             && not isfun
+             && not (is_function_type env ty')
              && wrap incomplete_type loc env ty' then
       error loc "'%s' has incomplete type" s;
-    if local && not isfun && sto' <> Storage_extern && sto' <> Storage_static then
+    if local && sto' <> Storage_extern && sto' <> Storage_static then
       (* Local definition *)
       ((sto', id, ty', init') :: decls, env2)
     else begin
@@ -2079,8 +2091,9 @@ let rec elab_stmt env ctx s =
             "'return' without a value in a function of return type@ %a"
             Cprint.typ ctx.ctx_return_typ
       | _, Some b ->
-          if not (valid_assignment env b ctx.ctx_return_typ) then begin
-            if valid_cast env b.etyp ctx.ctx_return_typ then
+          if not (wrap2 valid_assignment loc env b ctx.ctx_return_typ)
+          then begin
+            if wrap2 valid_cast loc env b.etyp ctx.ctx_return_typ then
               warning loc
                 "return value has type@ %a@ \
                  instead of the expected type@ %a"
-- 
cgit 


From 3b8a094dafdeea5499239adadaf24d2b8bdb1f76 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Tue, 30 Dec 2014 17:10:43 +0100
Subject: PR#6: fix handling of wchar_t and assignments from wide string
 literals.

- cparser/Machine indicates whether wchar_t is signed or not
  (it is signed int in Linux and BSD, but unsigned short in Win32)
- The type of a wide string literal is "wchar_t *" if the typedef "wchar_t"
  exists in the environment (e.g. after #include <stddef.h>).  Only if
  wchar_t is not defined do we use the default from Machine.
- Permit initialization of any integer array from a wide string literal,
  not just an array of wchar_t.
---
 cparser/Cutil.ml    | 18 +++++++++++++++---
 cparser/Cutil.mli   |  2 +-
 cparser/Elab.ml     |  4 ++--
 cparser/Machine.ml  | 14 +++++++++++---
 cparser/Machine.mli |  2 ++
 5 files changed, 31 insertions(+), 9 deletions(-)

(limited to 'cparser')

diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index 9ad0b13d..7d1c2e4b 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -692,18 +692,30 @@ let find_matching_signed_ikind sz =
   else if sz = !config.sizeof_longlong then ILongLong
   else assert false
 
-let wchar_ikind = find_matching_unsigned_ikind !config.sizeof_wchar
+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, [])
+
 (** The type of a constant *)
 
-let type_of_constant = function
+let type_of_constant env = function
   | CInt(_, ik, _) -> TInt(ik, [])
   | CFloat(_, fk) -> TFloat(fk, [])
   | CStr _ -> TPtr(TInt(IChar, []), [])
-  | CWStr _ -> TPtr(TInt(wchar_ikind, []), [])
+  | CWStr _ -> TPtr(wchar_type env, [])
   | CEnum(_, _) -> TInt(IInt, [])
 
 (* Check that a C expression is a lvalue *)
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index 0de0c827..309981be 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -153,7 +153,7 @@ val ptrdiff_t_ikind : ikind
 
 (* Helpers for type-checking *)
 
-val type_of_constant : constant -> typ
+val type_of_constant : Env.t -> 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 dd42ae24..f7168eba 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1087,7 +1087,7 @@ and elab_item zi item il =
       | CStr _, _ ->
           error loc "initialization of an array of non-char elements with a string literal";
           elab_list zi il false
-      | CWStr s, TInt(ik, _) when ik = wchar_ikind ->
+      | CWStr s, TInt(ik, _) ->
           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);
@@ -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 cst' }
+      { edesc = EConst cst'; etyp = type_of_constant env cst' }
 
 (* 6.5.2 Postfix expressions *)
 
diff --git a/cparser/Machine.ml b/cparser/Machine.ml
index d8c55756..6a7f5054 100644
--- a/cparser/Machine.ml
+++ b/cparser/Machine.ml
@@ -29,6 +29,7 @@ type t = {
   sizeof_void: int option;
   sizeof_fun: int option;
   sizeof_wchar: int;
+  wchar_signed: bool;
   sizeof_size_t: int;
   sizeof_ptrdiff_t: int;
   alignof_ptr: int;
@@ -60,6 +61,7 @@ let ilp32ll64 = {
   sizeof_void = None;
   sizeof_fun = None;
   sizeof_wchar = 4;
+  wchar_signed = true;
   sizeof_size_t = 4;
   sizeof_ptrdiff_t = 4;
   alignof_ptr = 4;
@@ -91,6 +93,7 @@ let i32lpll64 = {
   sizeof_void = None;
   sizeof_fun = None;
   sizeof_wchar = 4;
+  wchar_signed = true;
   sizeof_size_t = 8;
   sizeof_ptrdiff_t = 8;
   alignof_ptr = 8;
@@ -122,6 +125,7 @@ let il32pll64 = {
   sizeof_void = None;
   sizeof_fun = None;
   sizeof_wchar = 4;
+  wchar_signed = true;
   sizeof_size_t = 8;
   sizeof_ptrdiff_t = 8;
   alignof_ptr = 8;
@@ -148,8 +152,12 @@ let x86_32 =
                    sizeof_longdouble = 12; alignof_longdouble = 4 }
 let x86_64 =
   { i32lpll64 with name = "x86_64"; char_signed = true }
+let win32 =
+  { ilp32ll64 with name = "win32"; char_signed = true;
+                   sizeof_wchar = 2; wchar_signed = false }
 let win64 =
-  { il32pll64 with name = "x86_64"; char_signed = true }
+  { il32pll64 with name = "win64"; char_signed = true;
+                   sizeof_wchar = 2; wchar_signed = false }
 let ppc_32_bigendian =
   { ilp32ll64 with name = "powerpc";
                    bigendian = true;
@@ -169,6 +177,6 @@ let gcc_extensions c =
 
 let config =
   ref (match Sys.word_size with
-           | 32 -> ilp32ll64
-           | 64 -> if Sys.os_type = "Win32" then il32pll64 else i32lpll64
+           | 32 -> if Sys.os_type = "Win32" then win32 else ilp32ll64
+           | 64 -> if Sys.os_type = "Win32" then win64 else i32lpll64
            | _  -> assert false)
diff --git a/cparser/Machine.mli b/cparser/Machine.mli
index 0381bfce..b544711f 100644
--- a/cparser/Machine.mli
+++ b/cparser/Machine.mli
@@ -29,6 +29,7 @@ type t = {
   sizeof_void: int option;
   sizeof_fun: int option;
   sizeof_wchar: int;
+  wchar_signed: bool;
   sizeof_size_t: int;
   sizeof_ptrdiff_t: int;
   alignof_ptr: int;
@@ -51,6 +52,7 @@ val i32lpll64 : t
 val il32pll64 : t
 val x86_32 : t
 val x86_64 : t
+val win32 : t
 val win64 : t
 val ppc_32_bigendian : t
 val arm_littleendian : t
-- 
cgit 


From 1379deed055fc6b1462915a0177e75f4f9a127eb Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Tue, 30 Dec 2014 19:35:47 +0100
Subject: PR#12: regression introduced in commit 2d32afc

---
 cparser/Elab.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'cparser')

diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index f7168eba..615ddd97 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1323,8 +1323,6 @@ let elab_expr loc env a =
 
   | CAST ((spec, dcl), ie) ->
       let (ty, _) = elab_type loc env spec dcl in
-      if wrap incomplete_type loc env ty then
-        err "incomplete type %a" Cprint.typ ty;
       begin match elab_initializer loc env "<compound literal>" ty ie with
       | (ty', Some i) -> { edesc = ECompound(ty', i); etyp = ty' }
       | (ty', None)   -> error "ill-formed compound literal"
-- 
cgit 


From 67b13ecb9cfd2511c1db62a6cc38cf796cfb2a14 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Wed, 31 Dec 2014 17:14:28 +0100
Subject: Add a type system for CompCert C and type-checking constructor
 functions. Use these constructor functions in C2C to rely less on the types
 produced by the unverified elaborator.

---
 cparser/Cutil.mli | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

(limited to 'cparser')

diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index 0de0c827..cc72537d 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -73,11 +73,13 @@ val sizeof : Env.t -> typ -> int option
 val alignof : Env.t -> typ -> int option
   (* Return the natural alignment of the given type, in bytes.
      Machine-dependent. [None] is returned if the type is incomplete. *)
-val sizeof_ikind: ikind -> int
-  (* Return the size of the given integer kind. *)
 val incomplete_type : Env.t -> typ -> bool
   (* Return true if the given type is incomplete, e.g.
      declared but not defined struct or union, or array type  without a size. *)
+val sizeof_ikind: ikind -> int
+  (* Return the size of the given integer kind. *)
+val is_signed_ikind: ikind -> bool
+  (* Return true if the given integer kind is signed, false if unsigned. *)
 
 (* Computing composite_info records *)
 
-- 
cgit 


From 442e3140f4a2172bbc1ee7ce260eb1a8fd79ae95 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Thu, 1 Jan 2015 11:08:12 +0100
Subject: Revised type compatibility check w.r.t. handling of attributes.

We now distinguish 3 modes (instead of 2 previously) for attributes: 1- strict compatibility, 2- ignore top-level attrs, 3- ignore all attrs recursively.
In strict mode, const/volatile/restrict attributes must be identical, but nonstandard attributes may vary.
Also: ignore top-level attrs when comparing function argument types, like GCC/Clang do.
Net result is fewer warnings and type-checking that is closer to GCC/Clang.
---
 cparser/Cutil.ml         | 96 ++++++++++++++++++++++++++++++------------------
 cparser/Cutil.mli        | 24 ++++++++++--
 cparser/Elab.ml          | 20 +++++-----
 cparser/PackedStructs.ml |  2 +-
 4 files changed, 93 insertions(+), 49 deletions(-)

(limited to 'cparser')

diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index 7d1c2e4b..9093b230 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -79,6 +79,12 @@ let rec remove_custom_attributes (names: string list)  (al: attributes) =
   | a :: tl ->
       a :: remove_custom_attributes names tl
 
+(* Is an attribute a ISO C standard attribute? *)
+
+let attr_is_standard = function
+  | AConst | AVolatile | ARestrict -> true
+  | AAlignas _ | Attr _ -> false
+
 (* Is an attribute type-related (true) or variable-related (false)? *)
 
 let attr_is_type_related = function
@@ -184,12 +190,28 @@ let alignas_attribute al =
 
 exception Incompat
 
-let combine_types ?(noattrs = false) env t1 t2 =
-
-  let comp_attr a1 a2 =
-    if a1 = a2 then a2
-    else if noattrs then add_attributes a1 a2
-    else raise Incompat
+type attr_handling =
+  | AttrCompat
+  | AttrIgnoreTop
+  | AttrIgnoreAll
+
+(* Check that [t1] and [t2] are compatible and produce a type that
+   combines the information in [t1] and [t2].  For example,
+   if [t1] is a prototyped function type and [t2] an unprototyped
+   function type, the combined type takes the prototype from [t1]. *)
+
+let combine_types mode env t1 t2 =
+
+  let comp_attr m a1 a2 =
+    if a1 = a2 then a2 else match m with
+    | AttrCompat ->
+        let (a1std, a1other) = List.partition attr_is_standard a1
+        and (a2std, a2other) = List.partition attr_is_standard a2 in
+        if a1std = a2std
+        then add_attributes a1std (add_attributes a1other a2other)
+        else raise Incompat
+    | AttrIgnoreTop | AttrIgnoreAll ->
+        add_attributes a1 a2
   and comp_base x1 x2 =
     if x1 = x2 then x2 else raise Incompat
   and comp_array_size sz1 sz2 =
@@ -211,18 +233,19 @@ let combine_types ?(noattrs = false) env t1 t2 =
         end
     | _ -> () in
 
-  let rec comp t1 t2 =
+  let rec comp m t1 t2 =
     match t1, t2 with
     | TVoid a1, TVoid a2 ->
-        TVoid(comp_attr a1 a2)
+        TVoid(comp_attr m a1 a2)
     | TInt(ik1, a1), TInt(ik2, a2) ->
-        TInt(comp_base ik1 ik2, comp_attr a1 a2)
+        TInt(comp_base ik1 ik2, comp_attr m a1 a2)
     | TFloat(fk1, a1), TFloat(fk2, a2) ->
-        TFloat(comp_base fk1 fk2, comp_attr a1 a2)
+        TFloat(comp_base fk1 fk2, comp_attr m a1 a2)
     | TPtr(ty1, a1), TPtr(ty2, a2) ->
-        TPtr(comp ty1 ty2, comp_attr a1 a2)
+        let m' = if m = AttrIgnoreTop then AttrCompat else m in
+        TPtr(comp m' ty1 ty2, comp_attr m a1 a2)
     | TArray(ty1, sz1, a1), TArray(ty2, sz2, a2) ->
-        TArray(comp ty1 ty2, comp_array_size sz1 sz2, comp_attr a1 a2)
+        TArray(comp m ty1 ty2, comp_array_size sz1 sz2, comp_attr m a1 a2)
     | TFun(ty1, params1, vararg1, a1), TFun(ty2, params2, vararg2, a2) ->
         let (params, vararg) =
           match params1, params2 with
@@ -231,26 +254,29 @@ let combine_types ?(noattrs = false) env t1 t2 =
           | Some l1, None -> List.iter comp_conv l1; (params1, vararg1)
           | Some l1, Some l2 ->
               if List.length l1 <> List.length l2 then raise Incompat;
-              (Some(List.map2 (fun (id1, ty1) (id2, ty2) -> (id2, comp ty1 ty2))
-                              l1 l2),
-               comp_base vararg1 vararg2)
+              let comp_param (id1, ty1) (id2, ty2) =
+                (id2, comp AttrIgnoreTop ty1 ty2) in
+              (Some(List.map2 comp_param l1 l2), comp_base vararg1 vararg2)
         in
-          TFun(comp ty1 ty2, params, vararg, comp_attr a1 a2)
-    | TNamed _, _ -> comp (unroll env t1) t2
-    | _, TNamed _ -> comp t1 (unroll env t2)
+        let m' = if m = AttrIgnoreTop then AttrCompat else m in
+        TFun(comp m' ty1 ty2, params, vararg, comp_attr m a1 a2)
+    | TNamed _, _ -> comp m (unroll env t1) t2
+    | _, TNamed _ -> comp m t1 (unroll env t2)
     | TStruct(s1, a1), TStruct(s2, a2) ->
-        TStruct(comp_base s1 s2, comp_attr a1 a2)
+        TStruct(comp_base s1 s2, comp_attr m a1 a2)
     | TUnion(s1, a1), TUnion(s2, a2) -> 
-        TUnion(comp_base s1 s2, comp_attr a1 a2)
+        TUnion(comp_base s1 s2, comp_attr m a1 a2)
     | TEnum(s1, a1), TEnum(s2, a2) -> 
-        TEnum(comp_base s1 s2, comp_attr a1 a2)
+        TEnum(comp_base s1 s2, comp_attr m a1 a2)
     | _, _ ->
         raise Incompat
 
-  in try Some(comp t1 t2) with Incompat -> None
+  in try Some(comp mode t1 t2) with Incompat -> None
+
+(** Check whether two types are compatible. *)
 
-let compatible_types  ?noattrs env t1 t2 =
-  match combine_types ?noattrs env t1 t2 with Some _ -> true | None -> false
+let compatible_types mode env t1 t2 =
+  match combine_types mode env t1 t2 with Some _ -> true | None -> false
 
 (* Naive placement algorithm for bit fields, might not match that
    of the compiler. *)
@@ -756,10 +782,9 @@ let is_literal_0 e =
    Custom attributes can safely be dropped but must not be added. *)
 
 let valid_assignment_attr afrom ato =
-  let is_covariant = function Attr _ -> false | _ -> true in
-  let (afrom1, afrom2) = List.partition is_covariant afrom
-  and (ato1, ato2) = List.partition is_covariant ato in
-  incl_attributes afrom1 ato1 && incl_attributes ato2 afrom2
+  let (afromstd, afromcustom) = List.partition attr_is_standard afrom
+  and (atostd, atocustom) = List.partition attr_is_standard ato in
+  incl_attributes afromstd atostd && incl_attributes atocustom afromcustom
 
 (* Check that an assignment is allowed *)
 
@@ -771,9 +796,7 @@ let valid_assignment env from tto =
       valid_assignment_attr (attributes_of_type env ty)
                             (attributes_of_type env ty')
       && (is_void_type env ty || is_void_type env ty'
-          || compatible_types env
-               (erase_attributes_type env ty)
-               (erase_attributes_type env ty'))
+          || compatible_types AttrIgnoreTop env ty ty')
   | TStruct(s, _), TStruct(s', _) -> s = s'
   | TUnion(s, _), TUnion(s', _) -> s = s'
   | _, _ -> false
@@ -781,16 +804,19 @@ let valid_assignment env from tto =
 (* Check that a cast is allowed *)
 
 let valid_cast env tfrom tto =
-  compatible_types ~noattrs:true env tfrom tto ||
-  begin match unroll env tfrom, unroll env tto with
+  match unroll env tfrom, unroll env tto with
+  (* from any type to void *)
   | _, TVoid _ -> true
   (* from any int-or-pointer (with array and functions decaying to pointers)
      to any int-or-pointer *)
-  | (TInt _ | TPtr _ | TArray _ | TFun _ | TEnum _), (TInt _ | TPtr _ | TEnum _) -> true
+  | (TInt _ | TPtr _ | TArray _ | TFun _ | TEnum _),
+    (TInt _ | TPtr _ | TEnum _) -> true
   (* between int and float types *)
   | (TInt _ | TFloat _ | TEnum _), (TInt _ | TFloat _ | TEnum _) -> true
+  (* between identical composites *)
+  | TStruct(s1, _), TStruct(s2, _) -> s1 = s2
+  | TUnion(s1, _), TUnion(s2, _) -> s1 = s2
   | _, _ -> false
-  end
 
 (* Construct an integer constant *)
 
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index 309981be..53bcfcea 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -58,12 +58,28 @@ val attr_inherited_by_members: attribute -> bool
   (* Is an attribute of a composite inherited by members of the composite? *)
 
 (* Type compatibility *)
-val compatible_types : ?noattrs: bool -> Env.t -> typ -> typ -> bool
+
+type attr_handling =
+  | AttrCompat
+  | AttrIgnoreTop
+  | AttrIgnoreAll
+
+val compatible_types : attr_handling -> Env.t -> typ -> typ -> bool
   (* Check that the two given types are compatible.  
-     If [noattrs], ignore attributes (recursively). *)
-val combine_types : ?noattrs: bool -> Env.t -> typ -> typ -> typ option
+     The attributes in the types are compared according to the first argument:
+- [AttrCompat]: the types must have the same standard attributes
+    ([const], [volatile], [restrict]) but may differ on custom attributes.
+- [AttrIgnoreTop]: the top-level attributes of the two types are ignored,
+    but attributes of e.g. types of pointed objects (for pointer types)
+    are compared as per [AttrCompat].
+- [AttrIgnoreAll]: recursively ignore the attributes in the two types. *)
+val combine_types : attr_handling -> Env.t -> typ -> typ -> typ option
   (* Like [compatible_types], but if the two types are compatible,
-     return the most precise type compatible with both. *)
+     return the most precise type compatible with both.
+     The attributes are compared according to the first argument,
+     with the same meaning as for [compatible_types].
+     When two sets of attributes are compatible, the result of
+     [combine_types] carries the union of these two sets of attributes. *)
 
 (* Size and alignment *)
 
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 615ddd97..ac82532b 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1121,7 +1121,7 @@ and elab_single zi a il =
       (* 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 ->
+  | TStruct _ | TUnion _ when compatible_types AttrIgnoreTop 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
@@ -1267,7 +1267,7 @@ let elab_expr loc env a =
       let b2 = elab a2 and b3 = elab (TYPE_SIZEOF a3) in
       let ty = match b3.edesc with ESizeof ty -> ty | _ -> assert false in
       let ty' = default_argument_conversion env ty in
-      if not (compatible_types env ty ty') then
+      if not (compatible_types AttrIgnoreTop env ty ty') then
         warning "'%a' is promoted to '%a' when passed through '...'.@ You should pass '%a', not '%a', to 'va_arg'"
                 Cprint.typ ty Cprint.typ ty'
                 Cprint.typ ty' Cprint.typ ty;
@@ -1459,7 +1459,7 @@ let elab_expr loc env a =
               (TPtr(ty, []), TPtr(ty, []))
           | (TPtr(ty1, a1) | TArray(ty1, _, a1)),
             (TPtr(ty2, a2) | TArray(ty2, _, a2)) ->
-              if not (compatible_types ~noattrs:true env ty1 ty2) then
+              if not (compatible_types AttrIgnoreAll env ty1 ty2) then
                 err "mismatch between pointer types in binary '-'";
               if not (pointer_arithmetic_ok env ty1) then
                 err "illegal pointer arithmetic in binary '-'";
@@ -1519,11 +1519,13 @@ let elab_expr loc env a =
             if is_void_type env ty1 || is_void_type env ty2 then
               TPtr(TVoid (add_attributes a1 a2), [])
             else
-              match combine_types ~noattrs:true env
+              match combine_types AttrIgnoreAll env
                                   (TPtr(ty1, a1)) (TPtr(ty2, a2)) with
               | None ->
-                  error "the second and third arguments of '? :' \
-                         have incompatible pointer types"
+                  warning "the second and third arguments of '? :' \
+                           have incompatible pointer types";
+                  (* tolerance *)
+                  TPtr(TVoid (add_attributes a1 a2), [])
               | Some ty -> ty
             in
           { edesc = EConditional(b1, b2, b3); etyp = tyres }
@@ -1532,7 +1534,7 @@ let elab_expr loc env a =
       | TInt _, TPtr(ty2, a2) when is_literal_0 b2 ->
           { edesc = EConditional(b1, nullconst, b3); etyp = TPtr(ty2, []) }
       | ty1, ty2 ->
-          match combine_types ~noattrs:true env ty1 ty2 with
+          match combine_types AttrIgnoreAll env ty1 ty2 with
           | None ->
               error ("the second and third arguments of '? :' have incompatible types")
           | Some tyres ->
@@ -1660,7 +1662,7 @@ let elab_expr loc env a =
           when is_void_type env ty2 ->
             EBinop(op, b1, b2, TPtr(ty1, []))
         | TPtr(ty1, _), TPtr(ty2, _) ->
-            if not (compatible_types ~noattrs:true env ty1 ty2) then
+            if not (compatible_types AttrIgnoreAll env ty1 ty2) then
               warning "comparison between incompatible pointer types";
             EBinop(op, b1, b2, TPtr(ty1, []))
         | TPtr _, (TInt _ | TEnum _)
@@ -1749,7 +1751,7 @@ let enter_or_refine_ident local loc env s sto ty =
       if local && Env.in_current_scope env id then
         error loc "redefinition of local variable '%s'" s;
       let new_ty =
-        match combine_types env old_ty ty with
+        match combine_types AttrCompat env old_ty ty with
         | Some new_ty ->
             new_ty
         | None ->
diff --git a/cparser/PackedStructs.ml b/cparser/PackedStructs.ml
index 3064e78d..686a7d39 100644
--- a/cparser/PackedStructs.ml
+++ b/cparser/PackedStructs.ml
@@ -147,7 +147,7 @@ let accessor_type loc env ty =
 let ecast ty e = {edesc = ECast(ty, e); etyp = ty}
 
 let ecast_opt env ty e =
-  if compatible_types ~noattrs:true env ty e.etyp then e else ecast ty e
+  if compatible_types AttrCompat env ty e.etyp then e else ecast ty e
 
 (*  (ty) __builtin_readNN_reversed(&lval)
  or (ty) __builtin_bswapNN(lval) *)
-- 
cgit 


From 61f3945316ee86b0a848fd32df7e2e688bd5bc1a Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Thu, 1 Jan 2015 11:40:20 +0100
Subject: Wrong handling of block-local function declarations (again)

Reapply commit c3b615f875ed2cf8418453c79c4621d2dc61b0a0
which was overwritten by 2d32afc5daf16c75d1a34f2716c34ae2e1efcce4
---
 cparser/Elab.ml | 19 +++++++------------
 1 file changed, 7 insertions(+), 12 deletions(-)

(limited to 'cparser')

diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index ac82532b..faffc36f 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1777,18 +1777,13 @@ let enter_decdefs local loc env sto dl =
   if sto <> Storage_default && dl = [] then
     warning loc "Storage class specifier on empty declaration";
   let rec enter_decdef (decls, env) (s, ty, init) =
+    let isfun = is_function_type env ty in
     if sto = Storage_extern && init <> NO_INIT then
       error loc "'extern' declaration cannot have an initializer";
-    (* Adjust storage for function declarations *)
-    let sto1 =
-      match unroll env ty, sto with
-      | TFun _, Storage_default -> 
-          Storage_extern
-      | TFun _, (Storage_static | Storage_register) ->
-          if local then error loc "invalid storage class for '%s'" s;
-          sto
-      | _, _ ->
-          sto in
+    if local && isfun && (sto = Storage_static || sto = Storage_register) then
+      error loc "invalid storage class for '%s'" s;
+    (* Local function declarations are always treated as extern *)
+    let sto1 = if local && isfun then Storage_extern else sto in
     (* enter ident in environment with declared type, because
        initializer can refer to the ident *)
     let (id, sto', env1) = enter_or_refine_ident local loc env s sto1 ty in
@@ -1798,10 +1793,10 @@ let enter_decdefs local loc env sto dl =
     let env2 = Env.add_ident env1 id sto' ty' in
     (* check for incomplete type *)
     if local && sto' <> Storage_extern
-             && not (is_function_type env ty')
+             && not isfun
              && wrap incomplete_type loc env ty' then
       error loc "'%s' has incomplete type" s;
-    if local && sto' <> Storage_extern && sto' <> Storage_static then
+    if local && not isfun && sto' <> Storage_extern && sto' <> Storage_static then
       (* Local definition *)
       ((sto', id, ty', init') :: decls, env2)
     else begin
-- 
cgit 


From 1e97bb4f6297b6fa7949684e522a592aab754d99 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Thu, 22 Jan 2015 19:26:05 +0100
Subject: 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.
---
 cparser/Ceval.ml         |  2 +-
 cparser/Cutil.ml         | 32 ++++++++++++--------------------
 cparser/Cutil.mli        | 12 ++++++------
 cparser/Elab.ml          | 16 ++++++++--------
 cparser/GCC.ml           | 46 ++++++++++++++++++++++------------------------
 cparser/Machine.ml       | 42 ++++++++++++++++++++++++++++++++++++------
 cparser/PackedStructs.ml |  2 +-
 7 files changed, 86 insertions(+), 66 deletions(-)

(limited to 'cparser')

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 [])
-- 
cgit