Merge branch 'master' of https://github.com/AbsInt/CompCert

17 files changed, 125 insertions, 32 deletions

diff --git a/configure b/configure
index 84fed376..b906e38f 100755
--- a/configure
+++ b/configure
@@ -113,7 +113,7 @@ case "$target" in
     struct_return="int1-8"
     system="diab"
     cc="${toolprefix}dcc"
-    cprepro="${toolprefix}dcc -E"
+    cprepro="${toolprefix}dcc -E -D__GNUC__"
     casm="${toolprefix}das"
     asm_supports_cfi=false
     clinker="${toolprefix}dcc"
diff --git a/cparser/Bitfields.ml b/cparser/Bitfields.ml
index 570572fa..6569bb4c 100644
--- a/cparser/Bitfields.ml
+++ b/cparser/Bitfields.ml
@@ -31,7 +31,8 @@ type bitfield_info =
     bf_pos: int;        (* start bit *)
     bf_size: int;       (* size in bit *)
     bf_signed: bool;    (* is field signed or unsigned? *)
-    bf_signed_res: bool (* is result of extracting field signed or unsigned? *)
+    bf_signed_res: bool; (* is result of extracting field signed or unsigned? *)
+    bf_bool: bool       (* does field have type _Bool? *)
   }
 
 (* invariants:
@@ -100,7 +101,13 @@ let pack_bitfields env sid ml =
               match unroll env (type_of_member env m) with
               | TInt(ik, _) -> is_signed_ikind ik
               | _ -> assert false (* should never happen, checked in Elab *) in
-            pack ((m.fld_name, pos, n, signed, signed2) :: accu) (pos + n) ms
+            let is_bool =
+              match unroll env m.fld_typ with
+              | TInt(IBool, _) -> true
+              | _ -> false in
+
+            pack ((m.fld_name, pos, n, signed, signed2, is_bool) :: accu)
+                 (pos + n) ms
           end
   in pack [] 0 ml
 
@@ -121,7 +128,7 @@ let rec transf_members env id count = function
           let carrier_typ = TInt(carrier_ikind, []) in
           (* Enter each field with its bit position, size, signedness *)
           List.iter
-            (fun (name, pos, sz, signed, signed2) ->
+            (fun (name, pos, sz, signed, signed2, is_bool) ->
               if name <> "" then begin
                 let pos' =
                   if !config.bitfields_msb_first
@@ -131,7 +138,8 @@ let rec transf_members env id count = function
                   (id, name)
                   {bf_carrier = carrier; bf_carrier_typ = carrier_typ;
                    bf_pos = pos'; bf_size = sz;
-                   bf_signed = signed; bf_signed_res = signed2}
+                   bf_signed = signed; bf_signed_res = signed2;
+                   bf_bool = is_bool}
               end)
             bitfields;
           { fld_name = carrier; fld_typ = carrier_typ; fld_bitfield = None}
@@ -208,13 +216,16 @@ unsigned int bitfield_insert(unsigned int x, int ofs, int sz, unsigned int y)
   return (x & ~mask) | ((y << ofs) & mask);
 }
 
+If the bitfield is of type _Bool, the new value (y above) must be converted
+to _Bool to normalize it to 0 or 1.
 *)
 
 let bitfield_assign env bf carrier newval =
   let msk = insertion_mask bf in
   let notmsk = {edesc = EUnop(Onot, msk); etyp = msk.etyp} in
   let newval_casted =
-    ecast (TInt(IUInt,[])) newval in
+    ecast (TInt(IUInt,[]))
+          (if bf.bf_bool then ecast (TInt(IBool,[])) newval else newval) in
   let newval_shifted =
     eshift env Oshl newval_casted (intconst (Int64.of_int bf.bf_pos) IUInt) in
   let newval_masked = ebinint env Oand newval_shifted msk
@@ -230,17 +241,22 @@ unsigned int bitfield_init(int ofs, int sz, unsigned int y)
   unsigned int mask = (1U << sz) - 1;
   return (y & mask) << ofs;
 }
+
+If the bitfield is of type _Bool, the new value (y above) must be converted
+to _Bool to normalize it to 0 or 1.
 *)
 
 let bitfield_initializer bf i =
   match i with
   | Init_single e ->
       let m = Int64.pred (Int64.shift_left 1L bf.bf_size) in
+      let e_cast =
+        if bf.bf_bool then ecast (TInt(IBool,[])) e else e in
       let e_mask =
         {edesc = EConst(CInt(m, IUInt, sprintf "0x%LXU" m));
          etyp = TInt(IUInt, [])} in
       let e_and =
-        {edesc = EBinop(Oand, e, e_mask, TInt(IUInt,[]));
+        {edesc = EBinop(Oand, e_cast, e_mask, TInt(IUInt,[]));
          etyp = TInt(IUInt,[])} in
       {edesc = EBinop(Oshl, e_and, intconst (Int64.of_int bf.bf_pos) IInt,
                       TInt(IUInt, []));
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index 221bd7cc..a3c05c34 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -721,7 +721,8 @@ let type_of_member env fld =
 
 let find_matching_unsigned_ikind sz =
   assert (sz > 0);
-  if sz = !config.sizeof_int then IUInt
+  if sz = !config.sizeof_short then IUShort
+  else 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
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index d6b79780..5533105a 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -1805,7 +1805,12 @@ let enter_or_refine_ident local loc env s sto ty =
         | Some new_ty ->
             new_ty
         | None ->
-            warning loc "redefinition of '%s' with incompatible type" s; ty in
+            error loc
+               "redefinition of '%s' with incompatible type.@ \
+                Previous type: %a.@ \
+                New type: %a"
+              s Cprint.typ old_ty Cprint.typ ty;
+            ty in
       let new_sto =
 	(* The only case not allowed is removing static *)
 	match old_sto,sto with
@@ -1894,6 +1899,18 @@ let elab_fundef env spec name body loc =
   emit_elab loc (Gdecl(Storage_static, func_id, func_ty, Some func_init));
   (* Elaborate function body *)
   let body' = !elab_funbody_f ty_ret env3 body in
+  (* Special treatment of the "main" function *)
+  let body'' =
+    if s = "main" then begin
+      match unroll env ty_ret with
+      | TInt(IInt, []) ->
+          (* Add implicit "return 0;" at end of function body *)
+          sseq no_loc body'
+            {sdesc = Sreturn(Some(intconst 0L IInt)); sloc = no_loc}
+      | _ ->
+          warning loc "return type of 'main' should be 'int'";
+          body'
+    end else body' in
   (* Build and emit function definition *)
   let fn =
     { fd_storage = sto1;
@@ -1904,7 +1921,7 @@ let elab_fundef env spec name body loc =
       fd_params = params;
       fd_vararg = vararg;
       fd_locals = [];
-      fd_body = body' } in
+      fd_body = body'' } in
   emit_elab loc (Gfundef fn);
   env1
 
diff --git a/cparser/Machine.ml b/cparser/Machine.ml
index bd6489fd..7a12c649 100644
--- a/cparser/Machine.ml
+++ b/cparser/Machine.ml
@@ -170,6 +170,10 @@ let ppc_32_bigendian =
                    bitfields_msb_first = true;
                    supports_unaligned_accesses = true }
 
+let ppc_32_diab_bigendian =
+  { ppc_32_bigendian with sizeof_wchar = 2; wchar_signed = false }
+
+
 let arm_littleendian =
   { ilp32ll64 with name = "arm" }
 
diff --git a/cparser/Machine.mli b/cparser/Machine.mli
index fb7321f9..277ac3fb 100644
--- a/cparser/Machine.mli
+++ b/cparser/Machine.mli
@@ -62,6 +62,7 @@ val x86_64 : t
 val win32 : t
 val win64 : t
 val ppc_32_bigendian : t
+val ppc_32_diab_bigendian : t
 val arm_littleendian : t
 
 val gcc_extensions : t -> t
diff --git a/cparser/StructReturn.ml b/cparser/StructReturn.ml
index 660f1d9b..5e5602f3 100644
--- a/cparser/StructReturn.ml
+++ b/cparser/StructReturn.ml
@@ -299,10 +299,15 @@ let rec transf_expr env ctx e =
       transf_call env ctx None fn args e.etyp
 
 (* Function calls returning a composite by reference: add first argument.
-    ctx = Effects:   lv = f(...)     -> f(&lv, ...)      [copy optimization]
+    ctx = Effects:   lv = f(...)     -> f(&newtemp, ...), lv = newtemp
                      f(...)          -> f(&newtemp, ...)
     ctx = Val:       lv = f(...)     -> f(&newtemp, ...), lv = newtemp
                      f(...)          -> f(&newtemp, ...), newtemp
+
+   We used to do a copy optimization:
+     ctx = Effects:   lv = f(...)     -> f(&lv, ...)
+   but it is not correct in case of overlap (see test/regression/struct12.c) 
+
    Function calls returning a composite by value:
     ctx = Effects:   lv = f(...)     -> newtemp = f(...), lv = newtemp
                      f(...)          -> f(...)
@@ -332,13 +337,14 @@ and transf_call env ctx opt_lhs fn args ty =
           | Effects, None ->
               let tmp = new_temp ~name:"_res" ty in
               {edesc = ECall(fn', eaddrof tmp :: args'); etyp = TVoid []}
-          | Effects, Some lhs ->
-              {edesc = ECall(fn', eaddrof lhs :: args'); etyp = TVoid []}
+          (* Copy optimization, turned off as explained above *)
+       (* | Effects, Some lhs ->
+              {edesc = ECall(fn', eaddrof lhs :: args'); etyp = TVoid []} *)
           | Val, None ->
               let tmp = new_temp ~name:"_res" ty in
               ecomma {edesc = ECall(fn', eaddrof tmp :: args'); etyp = TVoid []}
                      tmp
-          | Val, Some lhs ->
+          | _, Some lhs ->
               let tmp = new_temp ~name:"_res" ty in
               ecomma {edesc = ECall(fn', eaddrof tmp :: args'); etyp = TVoid []}
                      (eassign lhs tmp)
diff --git a/cparser/validator/Tuples.v b/cparser/validator/Tuples.v
index 88dc46e9..3fd2ec03 100644
--- a/cparser/validator/Tuples.v
+++ b/cparser/validator/Tuples.v
@@ -26,8 +26,11 @@ Definition arrows_right: Type -> list Type -> Type :=
   fold_right (fun A B => A -> B).
 
 (** A tuple is a heterogeneous list. For convenience, we use pairs. **)
-Definition tuple (types:list Type) : Type :=
-  fold_right prod unit types.
+Fixpoint tuple (types : list Type) : Type :=
+  match types with
+  | nil => unit
+  | t::q => prod t (tuple q)
+  end.
 
 Fixpoint uncurry {args:list Type} {res:Type}:
   arrows_left args res -> tuple args -> res :=
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 1b58fe61..1dce08ac 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -661,7 +661,9 @@ let _ =
     Printexc.record_backtrace true;
     Machine.config :=
       begin match Configuration.arch with
-      | "powerpc" -> Machine.ppc_32_bigendian
+      | "powerpc" -> if Configuration.system = "linux"
+                     then Machine.ppc_32_bigendian
+                     else Machine.ppc_32_diab_bigendian
       | "arm"     -> Machine.arm_littleendian
       | "ia32"    -> if Configuration.abi = "macosx"
                      then Machine.x86_32_macosx
diff --git a/runtime/include/stdarg.h b/runtime/include/stdarg.h
index b2e7eadd..272b6320 100644
--- a/runtime/include/stdarg.h
+++ b/runtime/include/stdarg.h
@@ -50,6 +50,10 @@ typedef __builtin_va_list __gnuc_va_list;
 typedef __builtin_va_list va_list;
 #endif
 
+#ifndef __VA_LIST
+#define __VA_LIST
+#endif
+
 #define va_start(v,l) __builtin_va_start(v,l)
 #define va_end(v) __builtin_va_end(v)
 #define va_arg(v,l) __builtin_va_arg(v,l)
diff --git a/runtime/include/stddef.h b/runtime/include/stddef.h
index 290434f4..31edf4ef 100644
--- a/runtime/include/stddef.h
+++ b/runtime/include/stddef.h
@@ -71,7 +71,7 @@ typedef signed long ptrdiff_t;
 #ifdef _TYPE_wchar_t
 _TYPE_wchar_t;
 #else
-typedef signed int wchar_t;
+typedef unsigned short wchar_t;
 #endif
 #endif
 #undef __need_wchar_t
@@ -98,7 +98,7 @@ typedef signed int wchar_t;
 #endif
 
 #if defined(_STDDEF_H) && !defined(offsetof)
-#define offsetof(ty,member) ((size_t) &(((ty)*) NULL)->member)
+#define offsetof(ty,member) ((size_t) &((ty*) NULL)->member)
 #endif
 
 #endif
diff --git a/test/regression/Makefile b/test/regression/Makefile
index da7d5755..e2d94aa9 100644
--- a/test/regression/Makefile
+++ b/test/regression/Makefile
@@ -15,7 +15,7 @@ LIBS=$(LIBMATH)
 TESTS=int32 int64 floats floats-basics \
   expr1 expr6 funptr2 initializers initializers2 initializers3 \
   volatile1 volatile2 volatile3 \
-  funct3 expr5 struct7 struct8 struct11 casts1 casts2 char1 \
+  funct3 expr5 struct7 struct8 struct11 struct12 casts1 casts2 char1 \
   sizeof1 sizeof2 binops bool for1 switch switch2 compound \
   decl1 interop1 bitfields9 ptrs3
 
diff --git a/test/regression/Results/bitfields9 b/test/regression/Results/bitfields9
index ca74f1f4..a1d0e9fd 100644
--- a/test/regression/Results/bitfields9
+++ b/test/regression/Results/bitfields9
@@ -1,10 +1,10 @@
 glob_s = { a = -12, b = 1 }
-glob_t = { c = 123, d = 0, e = -45 }
+glob_t = { c = 123, d = 1, e = -45 }
 loc_s = { a = 11, b = 2 }
 loc_t = { c = 11, d = 1, e = 2 }
 compound_s = { a = 2, b = 3 }
-compound_t = { c = 2, d = 0, e = -11 }
+compound_t = { c = 2, d = 1, e = -11 }
 loc_s = { a = 7, b = 2 }
 loc_t = { c = 7, d = 1, e = 50 }
 compound_s = { a = -14, b = 3 }
-compound_t = { c = 50, d = 0, e = -7 }
+compound_t = { c = 50, d = 1, e = -7 }
diff --git a/test/regression/Results/struct12 b/test/regression/Results/struct12
new file mode 100644
index 00000000..e69de29b
--- /dev/null
+++ b/test/regression/Results/struct12
diff --git a/test/regression/bitfields1.c b/test/regression/bitfields1.c
index c6022dd1..5f6dfdd1 100644
--- a/test/regression/bitfields1.c
+++ b/test/regression/bitfields1.c
@@ -7,7 +7,7 @@ struct s {
 
 struct t {
   unsigned int c: 16;
-  unsigned int d: 1;
+  _Bool d: 1;
   short e: 8;
 };
 
@@ -29,7 +29,7 @@ int main()
   y.c = 12345;
   y.d = 0;
   y.e = 89;
-  res = f(&x, &y, 1);
+  res = f(&x, &y, 2);
 
   printf("x = {a = %d, b = %d }\n", x.a, x.b);
   printf("y = {c = %d, d = %d, e = %d }\n", y.c, y.d, y.e);
diff --git a/test/regression/bitfields9.c b/test/regression/bitfields9.c
index b33c4064..be87057b 100644
--- a/test/regression/bitfields9.c
+++ b/test/regression/bitfields9.c
@@ -9,7 +9,7 @@ struct s {
 
 struct t {
   unsigned int c: 16;
-  unsigned int d: 1;
+  _Bool d: 1;
   short e: 8;
 };
 
@@ -25,25 +25,25 @@ void print_t(char * msg, struct t p)
 
 /* Global initialization */
 struct s glob_s = { -12, 1 };
-struct t glob_t = { 123, 0, -45 };
+struct t glob_t = { 123, 2, -45 };
 
 /* Local initialization */
-void f(int x, int y)
+void f(int x, int y, int z)
 {
   struct s loc_s = { x, y };
-  struct t loc_t = { x, 1, y };
+  struct t loc_t = { x, z, y };
   print_s("loc_s", loc_s);
   print_t("loc_t", loc_t);
   print_s("compound_s", (struct s) { y, x });
-  print_t("compound_t", (struct t) { y, 0, -x });
+  print_t("compound_t", (struct t) { y, ~z, -x });
 }
 
 int main()
 {
   print_s("glob_s", glob_s);
   print_t("glob_t", glob_t);
-  f(11, 2);
-  f(7, 50);
+  f(11, 2, 3);
+  f(7, 50, 2);
   return 0;
 }
 
diff --git a/test/regression/struct12.c b/test/regression/struct12.c
new file mode 100644
index 00000000..39e62b28
--- /dev/null
+++ b/test/regression/struct12.c
@@ -0,0 +1,39 @@
+/*  This is was originally a regression test for bug 43784 of gcc.
+    See ISO/IEC 9899:TC3 §6.8.6.4p4 and footnote 139. */
+
+#include <stdio.h>
+
+struct s {
+  unsigned char a[256];
+};
+union u {
+  struct { struct s b; int c; } d;
+  struct { int c; struct s b; } e;
+};
+
+static union u v;
+static struct s *p = &v.d.b;
+static struct s *q = &v.e.b;
+
+static struct s __attribute__((noinline)) rp(void)
+{
+  return *p;
+}
+
+static void qp(void)
+{
+  *q = rp();
+}
+
+int main()
+{
+  int i;
+  for (i = 0; i < 256; i++)
+    p->a[i] = i;
+  qp();
+  for (i = 0; i < 256; i++)
+    if (q->a[i] != i)
+      printf("ERROR at %d: %d\n", i, q->a[i]);
+  return 0;
+}
+