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

14 files changed, 444 insertions, 34 deletions

diff --git a/test/abi/.gitignore b/test/abi/.gitignore
index c115947e..5aa03c7c 100644
--- a/test/abi/.gitignore
+++ b/test/abi/.gitignore
@@ -2,7 +2,10 @@
 *.c
 *.h
 *.compcert
+*.cc
 *.cc2compcert
 *.compcert2cc
 *.light.c
 *.s
+!layout.c
+!staticlayout.c
diff --git a/test/abi/Makefile b/test/abi/Makefile
index eb9ca292..ef354e06 100644
--- a/test/abi/Makefile
+++ b/test/abi/Makefile
@@ -8,7 +8,10 @@ TESTS=fixed.compcert fixed.cc2compcert fixed.compcert2cc \
      vararg.compcert vararg.cc2compcert vararg.compcert2cc \
      struct.compcert struct.cc2compcert struct.compcert2cc
 
-all: $(TESTS)
+DIFFTESTS=layout.compcert layout.cc \
+          staticlayout.compcert staticlayout.cc
+
+all: $(TESTS) $(DIFFTESTS)
 
 all_s: fixed_def_compcert.s fixed_use_compcert.s \
        vararg_def_compcert.s vararg_use_compcert.s \
@@ -18,12 +21,22 @@ test:
 	@set -e; for t in $(TESTS); do \
           SIMU='$(SIMU)' ARCH=$(ARCH) MODEL=$(MODEL) ABI=$(ABI) SYSTEM=$(SYSTEM) ./Runtest $$t; \
          done
+	@set -e; for t in layout staticlayout; do \
+	  $(SIMU) ./$$t.compcert > _compcert.log; \
+	  $(SIMU) ./$$t.cc > _cc.log; \
+	 if diff -a -u  _cc.log  _compcert.log; \
+         then echo "$$t: CompCert and $CC agree"; rm _*.log; \
+	 else echo "$$t: CompCert and $CC DISAGREE"; exit 2; fi; \
+         done
 
 generator.exe: generator.ml
 	ocamlopt -g -o $@ generator.ml
 
+genlayout.exe: genlayout.ml
+	ocamlopt -g -o $@ genlayout.ml
+
 clean::
-	rm -f generator.exe *.cm[iox]
+	rm -f generator.exe genlayout.exe *.cm[iox]
 
 fixed_decl.h: generator.exe
 	./generator.exe -rnd 500 -o fixed
@@ -49,6 +62,16 @@ struct_def.c struct_use.c: struct_decl.h
 clean::
 	rm -f struct_decl.h struct_def.c struct_use.c
 
+ifeq ($(ARCH),arm)
+GENLAYOUT_OPTIONS += -stable
+endif
+ifeq ($(ARCH),aarch64)
+GENLAYOUT_OPTIONS += -stable
+endif
+
+layout.h: genlayout.exe
+	./genlayout.exe $(GENLAYOUT_OPTIONS) > layout.h
+
 struct%.o: CCOMPFLAGS += -fstruct-passing -dclight
 
 %_compcert.o: %.c
@@ -61,6 +84,19 @@ struct%.o: CCOMPFLAGS += -fstruct-passing -dclight
 %_cc.s: %.c
 	$(CC) $(CFLAGS) -S -o $@ $*.c
 
+layout.compcert: layout.c layout.h
+	$(CCOMP) $(CCOMPFLAGS) -o $@ layout.c
+layout.cc: layout.c layout.h
+	$(CC) $(CFLAGS) -o $@ layout.c
+
+staticlayout.compcert: staticlayout.c layout.h
+	$(CCOMP) $(CCOMPFLAGS) -o $@ staticlayout.c
+staticlayout.cc: staticlayout.c layout.h
+	$(CC) $(CFLAGS) -o $@ staticlayout.c
+
+%.compcert: %_def_compcert.o %_use_compcert.o
+	$(CCOMP) -o $@ $*_def_compcert.o $*_use_compcert.o
+
 %.compcert: %_def_compcert.o %_use_compcert.o
 	$(CCOMP) -o $@ $*_def_compcert.o $*_use_compcert.o
 
diff --git a/test/abi/generator.ml b/test/abi/generator.ml
index aecee7cf..529352e0 100644
--- a/test/abi/generator.ml
+++ b/test/abi/generator.ml
@@ -439,7 +439,7 @@ let _ =
        " <seed> use the given seed for randomization"
   ]
   (fun s -> raise (Arg.Bad ("don't know what to do with " ^ s)))
-  "Usage: gencalls [options]\n\nOptions are:";
+  "Usage: generator [options]\n\nOptions are:";
   let oc0 = open_out (!output_prefix ^ "_decl.h")
   and oc1 = open_out (!output_prefix ^ "_def.c")
   and oc2 = open_out (!output_prefix ^ "_use.c") in
diff --git a/test/abi/genlayout.ml b/test/abi/genlayout.ml
new file mode 100644
index 00000000..5c26ca35
--- /dev/null
+++ b/test/abi/genlayout.ml
@@ -0,0 +1,158 @@
+open Printf
+
+type typ = Bool | Char | Short | Int
+
+type field =
+  | Plain of typ
+  | Bitfield of typ * int
+  | Padding of typ * int
+
+type struct_ = field list
+
+(* Concise description of a struct *)
+
+let print_typ oc = function
+  | Bool -> fprintf oc "b"
+  | Char -> fprintf oc "c"
+  | Short -> fprintf oc "s"
+  | Int -> fprintf oc "i"
+
+let print_padding_typ oc = function
+  | Bool -> fprintf oc "B"
+  | Char -> fprintf oc "C"
+  | Short -> fprintf oc "S"
+  | Int -> fprintf oc "I"
+
+let print_field oc = function
+  | Plain t -> print_typ oc t
+  | Bitfield(t, w) -> fprintf oc "%a%d" print_typ t w
+  | Padding(t, w) -> fprintf oc "%a%d" print_padding_typ t w
+
+let rec print_struct oc = function
+  | [] -> ()
+  | f :: s -> print_field oc f; print_struct oc s
+
+(* Printing a struct in C syntax *)
+
+let c_typ oc = function
+  | Bool -> fprintf oc "_Bool"
+  | Char -> fprintf oc "char"
+  | Short -> fprintf oc "short"
+  | Int -> fprintf oc "int"
+
+let c_name oc n = fprintf oc "%c" (Char.chr (Char.code 'a' + n))
+
+let c_field oc n = function
+  | Plain t ->
+      fprintf oc "  %a %a;\n" c_typ t c_name n; 
+      n + 1
+  | Bitfield(t, w) -> 
+      fprintf oc "  %a %a:%d;\n" c_typ t c_name n w;
+      n + 1
+  | Padding(t, w) ->
+      fprintf oc "  %a :%d;\n" c_typ t w;
+      n
+
+let c_struct oc s =
+  fprintf oc "struct %a {\n" print_struct s;
+  let rec c_str n = function
+    | [] -> ()
+    | f :: s -> let n' = c_field oc n f in c_str n' s in
+  c_str 0 s;
+  fprintf oc "};\n"
+
+(* Random generation of structs *)
+
+let random_1_8 () =
+  let n1 = Random.bits() in
+  let n2 = n1 lsr 2 in
+  match n1 land 3 with
+  | 0 -> 1
+  | 1 -> 2 + (n2 land 1)   (* 2-3 *)
+  | 2 -> 4 + (n2 land 1)   (* 4-5 *)
+  | 3 -> 6 + (n2 mod 3)    (* 6-8 *)
+  | _ -> assert false
+
+let random_1_16 () =
+  let n1 = Random.bits() in
+  let n2 = n1 lsr 2 in
+  match n1 land 3 with
+  | 0 -> 1 + (n2 land 1)   (* 1-2 *)
+  | 1 -> 3 + (n2 mod 3)    (* 3-4-5 *)
+  | 2 -> 6 + (n2 land 3)   (* 6-7-8-9 *)
+  | 3 -> 10 + (n2 mod 7)   (* 10-16 *)
+  | _ -> assert false
+
+let random_1_32 () =
+  let n1 = Random.bits() in
+  let n2 = n1 lsr 2 in
+  match n1 land 3 with
+  | 0 -> 1 + (n2 land 1)   (* 1-2 *)
+  | 1 -> 3 + (n2 mod 5)    (* 3-4-5-6-7 *)
+  | 2 -> 8 + (n2 mod 8)    (* 8-15 *)
+  | 3 -> 16 + (n2 mod 17)  (* 16-32 *)
+  | _ -> assert false
+
+let random_field () =
+  let (t, w) =
+    match Random.int 9 with
+    | 0   -> (Bool, 1)
+    | 1|2 -> (Char, random_1_8())
+    | 3|4 -> (Short, random_1_16())
+    | _ -> (Int, random_1_32()) in
+  match Random.int 10 with
+  | 0 -> Padding(t, (if Random.int 3 = 0 then 0 else w))
+  | 1 | 2 -> Plain t
+  | _ -> Bitfield(t, w)
+
+let rec random_struct len =
+  if len <= 0 then [] else begin
+    let f = random_field () in
+    f :: random_struct (match f with Padding _ -> len | _ -> len - 1)
+  end
+
+(* Optional filtering of structs where padding fields can increase alignment.
+   ELF says that padding fields are ignored to determine struct alignment,
+   but ARM does otherwise. *)
+
+let alignof = function Bool -> 1 | Char -> 1 | Short -> 2 | Int -> 4
+
+let unstable_alignment str =
+  let rec alignments al_data al_padding = function
+    | [] ->
+        al_padding > al_data
+    | (Plain t | Bitfield(t, _)) :: l ->
+        alignments (max (alignof t) al_data) al_padding l
+    | Padding(t, _) :: l ->
+        alignments al_data (max (alignof t) al_padding) l
+  in
+    alignments 1 1 str
+
+(* Random testing *)
+
+let structsize = ref 4
+let ntests = ref 1000
+let stable = ref false
+
+let _ =
+  Arg.parse [
+     "-size", Arg.Int (fun n -> structsize := n),
+       " <sz> produce structs with <sz> members (default: 4)";
+     "-n", Arg.Int (fun n -> ntests := n),
+       " <num> produce <num> random structs";
+     "-seed", Arg.Int Random.init,
+       " <seed> use the given seed for randomization";
+     "-stable", Arg.Set stable,
+       " don't generate padding fields that could cause differences in alignment"
+  ]
+  (fun s -> raise (Arg.Bad ("don't know what to do with " ^ s)))
+  "Usage: genlayout [options]\n\nOptions are:";
+  for _i = 1 to !ntests do
+    let s = random_struct !structsize in
+    if not (!stable && unstable_alignment s) then begin
+      printf "{\n";
+      c_struct stdout s;
+      printf "TEST%d(%a)\n" !structsize print_struct s;
+      printf "}\n"
+    end
+  done
diff --git a/test/abi/layout.c b/test/abi/layout.c
new file mode 100644
index 00000000..ebc6a2b2
--- /dev/null
+++ b/test/abi/layout.c
@@ -0,0 +1,59 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include <assert.h>
+#include <string.h>
+#include "../endian.h"
+
+static inline int bit(void * p, unsigned bitno)
+{
+  unsigned byteno = bitno / 8;
+#ifdef ARCH_BIG_ENDIAN
+  unsigned bit_in_byte = 7 - (bitno & 7);
+#else
+  unsigned bit_in_byte = bitno & 7;
+#endif
+  return (((unsigned char *) p)[byteno] >> bit_in_byte) & 1;
+}
+
+void print_prologue(char * name, size_t al, size_t sz)
+{
+  printf("%s: align %d, sizeof %d, layout", name, (int)al, (int)sz);
+}
+
+void print_next_field(_Bool first, size_t sz, void * p)
+{
+  static unsigned pos;
+
+  if (first) pos = 0;
+  /* Find first bit set, starting with [pos] */
+  while (1) {
+    assert (pos < 8 * sz);
+    if (bit(p, pos)) break;
+    pos += 1;
+  }
+  /* Print this position */
+  printf(" %u", pos);
+  /* Skip over one bits */
+  while (pos < 8 * sz && bit(p, pos)) pos++;
+}
+
+void print_epilogue(void)
+{
+  printf("\n");
+}
+
+#define TEST4(s)                                                            \
+  struct s x;                                                               \
+  memset(&x, 0, sizeof(x));                                                 \
+  print_prologue(#s, _Alignof(struct s), sizeof(x));                        \
+  x.a = -1; print_next_field(1, sizeof(x), &x);                             \
+  x.b = -1; print_next_field(0, sizeof(x), &x);                             \
+  x.c = -1; print_next_field(0, sizeof(x), &x);                             \
+  x.d = -1; print_next_field(0, sizeof(x), &x);                             \
+  print_epilogue();
+
+int main()
+{
+#include "layout.h"
+  return 0;
+}
diff --git a/test/abi/staticlayout.c b/test/abi/staticlayout.c
new file mode 100644
index 00000000..8a655afc
--- /dev/null
+++ b/test/abi/staticlayout.c
@@ -0,0 +1,76 @@
+#include <stdio.h>
+#include "../endian.h"
+
+static inline int bit(void * p, unsigned bitno)
+{
+  unsigned byteno = bitno / 8;
+#ifdef ARCH_BIG_ENDIAN
+  unsigned bit_in_byte = 7 - (bitno & 7);
+#else
+  unsigned bit_in_byte = bitno & 7;
+#endif
+  return (((unsigned char *) p)[byteno] >> bit_in_byte) & 1;
+}
+
+void print_prologue(char * name, size_t al, size_t sz)
+{
+  printf("%s: align %d, sizeof %d, layout", name, (int)al, (int)sz);
+}
+
+#if 0
+void print_contents(size_t sz, void * p)
+{
+  int last, lastpos;
+  printf(" - ");
+  last = 0; lastpos = 0;
+  for (int i = 0; i < sz; i++) {
+    for (int b = 0; b < 8; b++) {
+      int curr = bit((char *) p + i, b);
+      int currpos = i * 8 + b;
+      if (curr != last) {
+        if (currpos > lastpos) {
+          printf("%d(%d)", last, currpos - lastpos);
+        }
+        last = curr; lastpos = currpos;
+      }
+    }
+  }
+  { int currpos = sz * 8;
+    if (currpos > lastpos) {
+      printf("%d(%d)", last, currpos - lastpos);
+    }
+  }
+}
+#else
+void print_contents(size_t sz, void * p)
+{
+  printf(" - ");
+  for (int i = 0; i < sz; i++) {
+    printf("%02x", ((unsigned char *)p)[i]);
+  }
+}
+#endif
+
+void print_epilogue (void)
+{
+  printf("\n");
+}
+
+
+#define TEST4(s)                                                            \
+  static struct s x1 = {-1, 0, 0, 0};                                       \
+  static struct s x2 = {-1, -1, 0, 0};                                      \
+  static struct s x3 = {-1, 0, -1, 0};                                      \
+  static struct s x4 = {-1, -1, -1, -1};                                    \
+  print_prologue(#s, _Alignof(struct s), sizeof(x1));                       \
+  print_contents(sizeof(x1), &x1);                                          \
+  print_contents(sizeof(x2), &x2);                                          \
+  print_contents(sizeof(x3), &x3);                                          \
+  print_contents(sizeof(x4), &x4);                                          \
+  print_epilogue();
+
+int main()
+{
+#include "layout.h"
+  return 0;
+}
diff --git a/test/clightgen/bitfields.c b/test/clightgen/bitfields.c
new file mode 100644
index 00000000..34f6a686
--- /dev/null
+++ b/test/clightgen/bitfields.c
@@ -0,0 +1,13 @@
+struct s {
+  int a: 10;
+  char : 6;
+  _Bool b : 1;
+  int : 0;
+  short c: 7;
+};
+
+int f(void)
+{
+  struct s x = { -1, 1, 2 };
+  return x.a + x.b + x.c;
+}
diff --git a/test/regression/Makefile b/test/regression/Makefile
index 0f9e368f..db0b381e 100644
--- a/test/regression/Makefile
+++ b/test/regression/Makefile
@@ -23,7 +23,7 @@ TESTS?=int32 int64 floats floats-basics floats-lit \
 # Can run, but only in compiled mode, and have reference output in Results
 
 TESTS_COMP?=attribs1 bitfields1 bitfields2 bitfields3 bitfields4 \
-  bitfields5 bitfields6 bitfields7 bitfields8 bitfields_uint_t \
+  bitfields5 bitfields6 bitfields7 bitfields8 bitfields_uint_t bitfields10 \
   builtins-common builtins-$(ARCH) packedstruct1 packedstruct2 alignas \
   varargs1 varargs2 varargs3 sections alias aligned
 
diff --git a/test/regression/Results/bitfields10 b/test/regression/Results/bitfields10
new file mode 100644
index 00000000..9dc00daf
--- /dev/null
+++ b/test/regression/Results/bitfields10
@@ -0,0 +1,14 @@
+loc_s = { a = 11, b = 2 }
+loc_t = { c = 11, d = 1, e = 2 }
+loc_u_u = { u = -5 }
+loc_u_v = { v = 3 }
+compound_s = { a = 2, b = 3 }
+compound_t = { c = 2, d = 1, e = -11 }
+compound_u = { u = 2 }
+loc_s = { a = 7, b = 2 }
+loc_t = { c = 7, d = 1, e = 50 }
+loc_u_u = { u = 7 }
+loc_u_v = { v = 2 }
+compound_s = { a = -14, b = 3 }
+compound_t = { c = 50, d = 1, e = -7 }
+compound_u = { u = 2 }
diff --git a/test/regression/Results/bitfields9 b/test/regression/Results/bitfields9
index e35c2414..ec35fc08 100644
--- a/test/regression/Results/bitfields9
+++ b/test/regression/Results/bitfields9
@@ -2,17 +2,7 @@ glob_s = { a = -12, b = 1 }
 glob_t = { c = 123, d = 1, e = -45 }
 glob_u_u = { u = -3 }
 glob_u_v = { v = 6 }
-loc_s = { a = 11, b = 2 }
-loc_t = { c = 11, d = 1, e = 2 }
-loc_u_u = { u = -5 }
-loc_u_v = { v = 3 }
-compound_s = { a = 2, b = 3 }
-compound_t = { c = 2, d = 1, e = -11 }
-compound_u = { u = 2 }
-loc_s = { a = 7, b = 2 }
-loc_t = { c = 7, d = 1, e = 50 }
-loc_u_u = { u = 7 }
-loc_u_v = { v = 2 }
-compound_s = { a = -14, b = 3 }
-compound_t = { c = 50, d = 1, e = -7 }
-compound_u = { u = 2 }
+loc_s = { a = -12, b = 1 }
+loc_t = { c = 123, d = 1, e = -45 }
+loc_u_u = { u = -3 }
+loc_u_v = { v = 6 }
diff --git a/test/regression/Runtest b/test/regression/Runtest
index f693219a..600ae045 100755
--- a/test/regression/Runtest
+++ b/test/regression/Runtest
@@ -51,7 +51,7 @@ then
       exit 0
     else
       echo "$name: WRONG OUTPUT (diff follows)"
-      diff -u "$ref" "$out"
+      diff -a -u "$ref" "$out"
       exit 2
     fi
   else
diff --git a/test/regression/bitfields10.c b/test/regression/bitfields10.c
new file mode 100644
index 00000000..0f022664
--- /dev/null
+++ b/test/regression/bitfields10.c
@@ -0,0 +1,66 @@
+#include <stdio.h>
+
+/* Dynamic initialization of bit-fields */
+/* Known not to work with the reference interpreter */
+
+struct s {
+  signed char a: 6;
+  unsigned int b: 2;
+};
+
+struct t {
+  unsigned int c: 16;
+  _Bool d: 1;
+  short e: 8;
+  int : 10;
+};
+
+union u {
+  int u: 4;
+  unsigned int v: 3;
+};
+
+void print_s(char * msg, struct s p)
+{
+  printf("%s = { a = %d, b = %d }\n", msg, p.a, p.b);
+}
+
+void print_t(char * msg, struct t p)
+{
+  printf("%s = { c = %d, d = %d, e = %d }\n", msg, p.c, p.d, p.e);
+}
+
+void print_u_u(char * msg, union u p)
+{
+  printf("%s = { u = %d }\n", msg, p.u);
+}
+
+void print_u_v(char * msg, union u p)
+{
+  printf("%s = { v = %u }\n", msg, p.v);
+}
+
+/* Local, non-static initialization */
+void f(int x, int y, int z)
+{
+  struct s loc_s = { x, y };
+  struct t loc_t = { x, z, y };
+  union u loc_u_u = { .u = x };
+  union u loc_u_v = { .v = z };
+  print_s("loc_s", loc_s);
+  print_t("loc_t", loc_t);
+  print_u_u("loc_u_u", loc_u_u);
+  print_u_v("loc_u_v", loc_u_v);
+  print_s("compound_s", (struct s) { y, x });
+  print_t("compound_t", (struct t) { y, ~z, -x });
+  print_u_u("compound_u", (union u) { y });
+}
+
+int main()
+{
+  f(11, 2, 3);
+  f(7, 50, 2);
+  return 0;
+}
+
+
diff --git a/test/regression/bitfields9.c b/test/regression/bitfields9.c
index eef20168..025216fa 100644
--- a/test/regression/bitfields9.c
+++ b/test/regression/bitfields9.c
@@ -1,6 +1,6 @@
 #include <stdio.h>
 
-/* Initialization of bit-fields */
+/* Static initialization of bit-fields */
 
 struct s {
   signed char a: 6;
@@ -39,27 +39,23 @@ void print_u_v(char * msg, union u p)
   printf("%s = { v = %u }\n", msg, p.v);
 }
 
-
 /* Global initialization */
 struct s glob_s = { -12, 1 };
 struct t glob_t = { 123, 2, -45 };
 union u glob_u_u = { -3 };
 union u glob_u_v = { .v = 6 };
 
-/* Local initialization */
-void f(int x, int y, int z)
+/* Local, static initialization */
+void f(void)
 {
-  struct s loc_s = { x, y };
-  struct t loc_t = { x, z, y };
-  union u loc_u_u = { .u = x };
-  union u loc_u_v = { .v = z };
+  static struct s loc_s = { -12, 1 };
+  static struct t loc_t = { 123, 2, -45 };
+  static union u loc_u_u = { -3 };
+  static union u loc_u_v = { .v = 6 };
   print_s("loc_s", loc_s);
   print_t("loc_t", loc_t);
   print_u_u("loc_u_u", loc_u_u);
   print_u_v("loc_u_v", loc_u_v);
-  print_s("compound_s", (struct s) { y, x });
-  print_t("compound_t", (struct t) { y, ~z, -x });
-  print_u_u("compound_u", (union u) { y });
 }
 
 int main()
@@ -68,8 +64,7 @@ int main()
   print_t("glob_t", glob_t);
   print_u_u("glob_u_u", glob_u_u);
   print_u_v("glob_u_v", glob_u_v);
-  f(11, 2, 3);
-  f(7, 50, 2);
+  f();
   return 0;
 }
 
diff --git a/test/regression/sizeof1.c b/test/regression/sizeof1.c
index ca494622..5bd4d739 100644
--- a/test/regression/sizeof1.c
+++ b/test/regression/sizeof1.c
@@ -17,8 +17,8 @@ char tbl[sizeof(struct s)];
 */
 
 struct bits1 {
-  unsigned a: 1;
-  unsigned b: 6;
+  unsigned char a: 1;
+  unsigned char b: 6;
 };
 
 char b1[sizeof(struct bits1)];  /* should be 1 */