From 883341719d7d6868f8165541e7e13ac45192a358 Mon Sep 17 00:00:00 2001 From: Xavier Leroy Date: Thu, 27 Oct 2016 11:06:09 +0200 Subject: Make Archi.ptr64 always computable, and reorganize files accordingly: ia32 -> x86/x86_32/x86_64 Having Archi.ptr64 as an opaque Parameter that is determined at run-time depending on compcert.ini is problematic for applications such as VST where functions such as Ctypes.sizeof must compute within Coq. This commit introduces two versions of the Archi.v file, one for x86 32 bits (with ptr64 := false), one for x86 64 bits (with ptr64 := true). Unlike previous approaches, no other file is duplicated between these two variants of x86. While we are at it, I renamed "ia32" into "x86" everywhere. "ia32" is Intel speak for the 32-bit architecture. It is not a good name to describe both the 32 and 64 bit architectures. Finally, .depend is no longer under version control and is regenerated when the target architecture changes. That's because the location of Archi.v differs between the ports that have 32/64 bit variants (x86 so far) and the ports that have only one bitsize (ARM and PowerPC so far). --- test/regression/Results/builtins-ia32 | 19 ----------- test/regression/Results/builtins-x86 | 19 +++++++++++ test/regression/Runtest | 14 +++----- test/regression/builtins-ia32.c | 61 ----------------------------------- test/regression/builtins-x86.c | 61 +++++++++++++++++++++++++++++++++++ 5 files changed, 84 insertions(+), 90 deletions(-) delete mode 100644 test/regression/Results/builtins-ia32 create mode 100644 test/regression/Results/builtins-x86 delete mode 100644 test/regression/builtins-ia32.c create mode 100644 test/regression/builtins-x86.c (limited to 'test') diff --git a/test/regression/Results/builtins-ia32 b/test/regression/Results/builtins-ia32 deleted file mode 100644 index 393ac1fd..00000000 --- a/test/regression/Results/builtins-ia32 +++ /dev/null @@ -1,19 +0,0 @@ -bswap(12345678) = 78563412 -bswap16(1234) = 3412 -bswap64(123456789abcdef0) = f0debc9a78563412 -clz(12345678) = 3 -clzll(12345678) = 35 -clzll(1234567812345678) = 3 -clzll(78563412) = 33 -ctz(1234) = 2 -ctzll(1234567812345678) = 3 -ctzll(1234567800000000) = 35 -ctzll(78563412) = 1 -fsqrt(3.141590) = 1.772453 -fmin(3.141590, 2.718000) = 2.718000 -fmax(3.141590, 2.718000) = 3.141590 -read_16_rev = 3412 -read_32_rev = efbeadde -after write_16_rev: 9a78 -after write_32_rev: 78563412 -CSE write_32_rev: ok diff --git a/test/regression/Results/builtins-x86 b/test/regression/Results/builtins-x86 new file mode 100644 index 00000000..393ac1fd --- /dev/null +++ b/test/regression/Results/builtins-x86 @@ -0,0 +1,19 @@ +bswap(12345678) = 78563412 +bswap16(1234) = 3412 +bswap64(123456789abcdef0) = f0debc9a78563412 +clz(12345678) = 3 +clzll(12345678) = 35 +clzll(1234567812345678) = 3 +clzll(78563412) = 33 +ctz(1234) = 2 +ctzll(1234567812345678) = 3 +ctzll(1234567800000000) = 35 +ctzll(78563412) = 1 +fsqrt(3.141590) = 1.772453 +fmin(3.141590, 2.718000) = 2.718000 +fmax(3.141590, 2.718000) = 3.141590 +read_16_rev = 3412 +read_32_rev = efbeadde +after write_16_rev: 9a78 +after write_32_rev: 78563412 +CSE write_32_rev: ok diff --git a/test/regression/Runtest b/test/regression/Runtest index 7cc6330b..9051b5b7 100755 --- a/test/regression/Runtest +++ b/test/regression/Runtest @@ -9,19 +9,13 @@ out="test$$.log" rm -f $out trap "rm -f $out" 0 INT QUIT -# The architecture and the model +# The architecture and the bitsize arch=`sed -n -e 's/^ARCH=//p' ../../Makefile.config` -model=`sed -n -e 's/^MODEL=//p' ../../Makefile.config` - -# Its bit size -case "$arch,$model" in - ia32,64) bits=64;; - *) bits=32;; -esac +bits=`sed -n -e 's/^BITSIZE=//p' ../../Makefile.config` # The reference output -if test -f "Results/$name-$arch-$model"; then - ref="Results/$name-$arch-$model" +if test -f "Results/$name-$arch-$bits"; then + ref="Results/$name-$arch-$bits" elif test -f "Results/$name-$arch"; then ref="Results/$name-$arch" elif test -f "Results/$name-$bits"; then diff --git a/test/regression/builtins-ia32.c b/test/regression/builtins-ia32.c deleted file mode 100644 index 1ba213e7..00000000 --- a/test/regression/builtins-ia32.c +++ /dev/null @@ -1,61 +0,0 @@ -/* Fun with builtin functions */ - -#include - -int main(int argc, char ** argv) -{ - unsigned int x = 0x12345678; - unsigned int y = 0xDEADBEEF; - unsigned long long xx = 0x1234567812345678ULL; - unsigned long long yy = 0x1234567800000000ULL; - unsigned long long zz = 0x123456789ABCDEF0ULL; - unsigned z; - double a = 3.14159; - double b = 2.718; - double c = 1.414; - unsigned short s = 0x1234; - - printf("bswap(%x) = %x\n", x, __builtin_bswap(x)); - printf("bswap16(%x) = %x\n", s, __builtin_bswap16(s)); - printf("bswap64(%llx) = %llx\n", zz, __builtin_bswap64(zz)); - printf("clz(%x) = %d\n", x, __builtin_clz(x)); - printf("clzll(%llx) = %d\n", (unsigned long long) x, __builtin_clzll(x)); - printf("clzll(%llx) = %d\n", xx, __builtin_clzll(xx)); - z = __builtin_bswap(x); - printf("clzll(%lx) = %d\n", z, __builtin_clzll(z)); - printf("ctz(%x) = %d\n", s, __builtin_ctz(s)); - printf("ctzll(%llx) = %d\n", xx, __builtin_ctzll(xx)); - printf("ctzll(%llx) = %d\n", yy, __builtin_ctzll(yy)); - printf("ctzll(%lx) = %d\n", z, __builtin_ctzll(z)); - - printf("fsqrt(%f) = %f\n", a, __builtin_fsqrt(a)); - printf("fmin(%f, %f) = %f\n", a, b, __builtin_fmin(a, b)); - printf("fmax(%f, %f) = %f\n", a, b, __builtin_fmax(a, b)); - -#ifdef FMA3 - printf("fmadd(%f, %f, %f) = %f\n", a, b, c, __builtin_fmadd(a, b, c)); - printf("fmsub(%f, %f, %f) = %f\n", a, b, c, __builtin_fmsub(a, b, c)); - printf("fnmadd(%f, %f, %f) = %f\n", a, b, c, __builtin_fnmadd(a, b, c)); - printf("fnmsub(%f, %f, %f) = %f\n", a, b, c, __builtin_fnmsub(a, b, c)); -#endif - - printf ("read_16_rev = %x\n", __builtin_read16_reversed(&s)); - printf ("read_32_rev = %x\n", __builtin_read32_reversed(&y)); - __builtin_write16_reversed(&s, 0x789A); - printf ("after write_16_rev: %x\n", s); - __builtin_write32_reversed(&y, 0x12345678); - printf ("after write_32_rev: %x\n", y); - y = 0; - __builtin_write32_reversed(&y, 0x12345678); - printf ("CSE write_32_rev: %s\n", y == 0x78563412 ? "ok" : "ERROR"); - /* Make sure that ignoring the result of a builtin - doesn't cause an internal error */ - (void) __builtin_bswap(x); - (void) __builtin_fsqrt(a); - return 0; -} - - - - - diff --git a/test/regression/builtins-x86.c b/test/regression/builtins-x86.c new file mode 100644 index 00000000..1ba213e7 --- /dev/null +++ b/test/regression/builtins-x86.c @@ -0,0 +1,61 @@ +/* Fun with builtin functions */ + +#include + +int main(int argc, char ** argv) +{ + unsigned int x = 0x12345678; + unsigned int y = 0xDEADBEEF; + unsigned long long xx = 0x1234567812345678ULL; + unsigned long long yy = 0x1234567800000000ULL; + unsigned long long zz = 0x123456789ABCDEF0ULL; + unsigned z; + double a = 3.14159; + double b = 2.718; + double c = 1.414; + unsigned short s = 0x1234; + + printf("bswap(%x) = %x\n", x, __builtin_bswap(x)); + printf("bswap16(%x) = %x\n", s, __builtin_bswap16(s)); + printf("bswap64(%llx) = %llx\n", zz, __builtin_bswap64(zz)); + printf("clz(%x) = %d\n", x, __builtin_clz(x)); + printf("clzll(%llx) = %d\n", (unsigned long long) x, __builtin_clzll(x)); + printf("clzll(%llx) = %d\n", xx, __builtin_clzll(xx)); + z = __builtin_bswap(x); + printf("clzll(%lx) = %d\n", z, __builtin_clzll(z)); + printf("ctz(%x) = %d\n", s, __builtin_ctz(s)); + printf("ctzll(%llx) = %d\n", xx, __builtin_ctzll(xx)); + printf("ctzll(%llx) = %d\n", yy, __builtin_ctzll(yy)); + printf("ctzll(%lx) = %d\n", z, __builtin_ctzll(z)); + + printf("fsqrt(%f) = %f\n", a, __builtin_fsqrt(a)); + printf("fmin(%f, %f) = %f\n", a, b, __builtin_fmin(a, b)); + printf("fmax(%f, %f) = %f\n", a, b, __builtin_fmax(a, b)); + +#ifdef FMA3 + printf("fmadd(%f, %f, %f) = %f\n", a, b, c, __builtin_fmadd(a, b, c)); + printf("fmsub(%f, %f, %f) = %f\n", a, b, c, __builtin_fmsub(a, b, c)); + printf("fnmadd(%f, %f, %f) = %f\n", a, b, c, __builtin_fnmadd(a, b, c)); + printf("fnmsub(%f, %f, %f) = %f\n", a, b, c, __builtin_fnmsub(a, b, c)); +#endif + + printf ("read_16_rev = %x\n", __builtin_read16_reversed(&s)); + printf ("read_32_rev = %x\n", __builtin_read32_reversed(&y)); + __builtin_write16_reversed(&s, 0x789A); + printf ("after write_16_rev: %x\n", s); + __builtin_write32_reversed(&y, 0x12345678); + printf ("after write_32_rev: %x\n", y); + y = 0; + __builtin_write32_reversed(&y, 0x12345678); + printf ("CSE write_32_rev: %s\n", y == 0x78563412 ? "ok" : "ERROR"); + /* Make sure that ignoring the result of a builtin + doesn't cause an internal error */ + (void) __builtin_bswap(x); + (void) __builtin_fsqrt(a); + return 0; +} + + + + + -- cgit