aboutsummaryrefslogtreecommitdiffstats
path: root/test/abi
diff options
context:
space:
mode:
Diffstat (limited to 'test/abi')
-rw-r--r--test/abi/.gitignore3
-rw-r--r--test/abi/Makefile40
-rw-r--r--test/abi/generator.ml2
-rw-r--r--test/abi/genlayout.ml158
-rw-r--r--test/abi/layout.c59
-rw-r--r--test/abi/staticlayout.c76
6 files changed, 335 insertions, 3 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;
+}
generated by cgit (git 2.34.1) at 2024-06-02 19:19:58 +0000