diff options
author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-20 14:06:21 +0200 |
---|---|---|
committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-20 14:06:21 +0200 |
commit | 168393089024b5f926836cb813fddf14e6b6e4d4 (patch) | |
tree | 5d018198dc26be847544f162b87ad3dcecbab479 /test/mppa | |
parent | 633b72565b022f159526338b5bbb9fcac86dfd2b (diff) | |
parent | b3431b1d9ee5121883d307cff0b62b7e53369891 (diff) | |
download | compcert-kvx-168393089024b5f926836cb813fddf14e6b6e4d4.tar.gz compcert-kvx-168393089024b5f926836cb813fddf14e6b6e4d4.zip |
Merge remote-tracking branch 'origin/mppa-work' into mppa-fast-div
(unfinished)
Diffstat (limited to 'test/mppa')
m--------- | test/mppa/asm_coverage | 0 | ||||
-rwxr-xr-x | test/mppa/check.sh | 6 | ||||
-rwxr-xr-x[-rw-r--r--] | test/mppa/coverage.sh | 21 | ||||
-rw-r--r-- | test/mppa/coverage_helper.py | 70 | ||||
-rwxr-xr-x | test/mppa/hardcheck.sh | 6 | ||||
-rwxr-xr-x | test/mppa/hardtest.sh | 6 | ||||
-rw-r--r-- | test/mppa/instr/Makefile | 78 | ||||
-rw-r--r-- | test/mppa/instr/builtin32.c | 12 | ||||
-rw-r--r-- | test/mppa/instr/builtin64.c | 17 | ||||
-rw-r--r-- | test/mppa/instr/i32.c | 68 | ||||
-rw-r--r-- | test/mppa/instr/i64.c | 62 | ||||
-rw-r--r-- | test/mppa/interop/Makefile | 141 | ||||
-rw-r--r-- | test/mppa/interop/common.c | 10 | ||||
-rw-r--r-- | test/mppa/interop/vaarg_common.c | 12 | ||||
-rw-r--r-- | test/mppa/lib/Makefile | 4 | ||||
-rw-r--r-- | test/mppa/mmult/Makefile | 2 | ||||
-rw-r--r-- | test/mppa/prng/Makefile | 2 | ||||
-rwxr-xr-x | test/mppa/simucheck.sh | 6 | ||||
-rwxr-xr-x | test/mppa/simutest.sh (renamed from test/mppa/test.sh) | 2 | ||||
-rw-r--r-- | test/mppa/sort/Makefile | 2 |
20 files changed, 429 insertions, 98 deletions
diff --git a/test/mppa/asm_coverage b/test/mppa/asm_coverage deleted file mode 160000 -Subproject a9c62b61552a9e9fd0ebf43df5ee0d5b88bb094 diff --git a/test/mppa/check.sh b/test/mppa/check.sh deleted file mode 100755 index f25c3e31..00000000 --- a/test/mppa/check.sh +++ /dev/null @@ -1,6 +0,0 @@ -#!/bin/bash -# Tests the execution of the binaries produced by CompCert - -source do_test.sh - -do_test check $1 diff --git a/test/mppa/coverage.sh b/test/mppa/coverage.sh index 0a057ff9..42ed4182 100644..100755 --- a/test/mppa/coverage.sh +++ b/test/mppa/coverage.sh @@ -1,17 +1,24 @@ -asmdir=$1 +#!/bin/bash + +printer=../../mppa_k1c/TargetPrinter.ml +asmdir=instr/asm/ to_cover_raw=/tmp/to_cover_raw to_cover=/tmp/to_cover covered_raw=/tmp/covered_raw covered=/tmp/covered -sed -n "s/^.*fprintf oc \" \(.*\) .*/\1/p" ../../mppa_k1c/TargetPrinter.ml > $to_cover_raw -sed -n "s/^.*fprintf oc \" \(.*\)\\n.*/\1/p" ../../mppa_k1c/TargetPrinter.ml >> $to_cover_raw -python2.7 coverage_helper.py $to_cover_raw > $to_cover +# Stop at any error +set -e +# Pipes do not mask errors +set -o pipefail + +sed -n "s/^.*fprintf\s\+oc\s*\"\s*\([a-z][^[:space:]]*\)\s.*/\1/p" $printer > $to_cover_raw +python2.7 coverage_helper.py $to_cover_raw | sort -u > $to_cover rm -f $covered_raw -for asm in $(ls $asmdir/*.s); do - bash asm_coverage/asm-coverage.sh $asm >> $covered_raw +for asm in $(ls $asmdir/*.ccomp.s); do + grep -v ":" $asm | sed -n "s/^\s*\([a-z][a-z0-9.]*\).*/\1/p" | sort -u >> $covered_raw done -python2.7 coverage_helper.py $covered_raw > $covered +python2.7 coverage_helper.py $covered_raw | sort -u > $covered vimdiff $to_cover $covered diff --git a/test/mppa/coverage_helper.py b/test/mppa/coverage_helper.py index b086aca9..e5b1907c 100644 --- a/test/mppa/coverage_helper.py +++ b/test/mppa/coverage_helper.py @@ -1,35 +1,45 @@ import fileinput +import sys -occurs = {} +all_loads_stores = "lbs lbz lhz lo lq ld lhs lws sb sd sh so sq sw".split(" ") + +all_bconds = "wnez weqz wltz wgez wlez wgtz dnez deqz dltz dgez dlez dgtz".split(" ") + +all_iconds = "ne eq lt ge le gt ltu geu leu gtu".split(" ") + +all_fconds = "one ueq oeq une olt uge oge ult".split(" ") + +replaces_a = [(["cb.", "cmoved."], all_bconds), + (["compd.", "compw."], all_iconds), + (["fcompd.", "fcompw."], all_fconds), + (all_loads_stores, [".xs", ""])] +replaces_dd = [(["addx", "sbfx"], ["2d", "4d", "8d", "16d"])] +replaces_dw = [(["addx", "sbfx"], ["2w", "4w", "8w", "16w"])] + +macros_binds = {"%a": replaces_a, "%dd": replaces_dd, "%dw": replaces_dw} + +def expand_macro(fullinst, macro, replaceTable): + inst = fullinst.replace(macro, "") + for (searchlist, mods) in replaceTable: + if inst in searchlist: + return [fullinst.replace(macro, mod) for mod in mods] + raise NameError + +insts = [] for line in fileinput.input(): - line_noc = line.replace('\n', '') - if line_noc not in occurs: - occurs[line_noc] = 0 - occurs[line_noc] += 1 - -# HACK: Removing all the instructions with "%a", replacing them with all their variations -# Also removing all instructions starting with '.' -pruned_occurs = dict(occurs) -for inst in occurs: - if inst[0] == '.': - del pruned_occurs[inst] - if "%a" not in inst: - continue - inst_no_a = inst.replace(".%a", "") - if inst_no_a in ("compw", "compd"): - del pruned_occurs[inst] - for mod in ("ne", "eq", "lt", "gt", "le", "ge", "ltu", "leu", "geu", - "gtu", "all", "any", "nall", "none"): - pruned_occurs[inst_no_a + "." + mod] = 1 - elif inst_no_a in ("cb"): - del pruned_occurs[inst] - for mod in ("wnez", "weqz", "wltz", "wgez", "wlez", "wgtz", "deqz", "dnez", - "dltz", "dgez", "dlez", "dgtz"): - pruned_occurs[inst_no_a + "." + mod] = 1 - else: - assert False, "Found instruction with %a: " + inst -occurs = pruned_occurs - -for inst in sorted(occurs): + fullinst = line[:-1] + try: + for macro in macros_binds: + if macro in fullinst: + insts.extend(expand_macro(fullinst, macro, macros_binds[macro])) + break + else: + insts.append(fullinst) + except NameError: + print >> sys.stderr, fullinst + " could not be found any match for macro " + macro + sys.exit(1) + +for inst in insts: print inst +occurs = {} diff --git a/test/mppa/hardcheck.sh b/test/mppa/hardcheck.sh new file mode 100755 index 00000000..82b63182 --- /dev/null +++ b/test/mppa/hardcheck.sh @@ -0,0 +1,6 @@ +#!/bin/bash +# Tests the execution of the binaries produced by CompCert, in hardware + +source do_test.sh + +do_test hardcheck diff --git a/test/mppa/hardtest.sh b/test/mppa/hardtest.sh new file mode 100755 index 00000000..09511da6 --- /dev/null +++ b/test/mppa/hardtest.sh @@ -0,0 +1,6 @@ +#!/bin/bash +# Tests the validity of the tests, in hardware + +source do_test.sh + +do_test hardtest diff --git a/test/mppa/instr/Makefile b/test/mppa/instr/Makefile index ea86114c..37f7d0ab 100644 --- a/test/mppa/instr/Makefile +++ b/test/mppa/instr/Makefile @@ -1,11 +1,15 @@ -K1CC ?= k1-mbr-gcc +SHELL := /bin/bash + +K1CC ?= k1-cos-gcc CC ?= gcc CCOMP ?= ccomp OPTIM ?= -O2 CFLAGS ?= $(OPTIM) +CCOMPFLAGS ?= $(CFLAGS) SIMU ?= k1-mppa TIMEOUT ?= --signal=SIGTERM 120s DIFF ?= python2.7 floatcmp.py -reltol .00001 +HARDRUN ?= k1-jtag-runner DIR=./ SRCDIR=$(DIR) @@ -27,10 +31,11 @@ SIMUPATH=$(shell which $(SIMU)) TESTNAMES?=$(notdir $(subst .c,,$(wildcard $(DIR)/*.c))) X86_GCC_OUT=$(addprefix $(OUTDIR)/,$(addsuffix .x86-gcc.out,$(TESTNAMES))) -GCC_OUT=$(addprefix $(OUTDIR)/,$(addsuffix .gcc.out,$(TESTNAMES))) -CCOMP_OUT=$(addprefix $(OUTDIR)/,$(addsuffix .ccomp.out,$(TESTNAMES))) +GCC_SIMUOUT=$(addprefix $(OUTDIR)/,$(addsuffix .gcc.simu.out,$(TESTNAMES))) +CCOMP_SIMUOUT=$(addprefix $(OUTDIR)/,$(addsuffix .ccomp.simu.out,$(TESTNAMES))) +GCC_HARDOUT=$(addprefix $(OUTDIR)/,$(addsuffix .gcc.hard.out,$(TESTNAMES))) +CCOMP_HARDOUT=$(addprefix $(OUTDIR)/,$(addsuffix .ccomp.hard.out,$(TESTNAMES))) -OUT=$(X86_GCC_OUT) $(GCC_OUT) $(CCOMP_OUT) BIN=$(addprefix $(BINDIR)/,$(addsuffix .x86-gcc.bin,$(TESTNAMES)))\ $(addprefix $(BINDIR)/,$(addsuffix .gcc.bin,$(TESTNAMES)))\ $(addprefix $(BINDIR)/,$(addsuffix .ccomp.bin,$(TESTNAMES))) @@ -43,15 +48,52 @@ all: $(BIN) GREEN=\033[0;32m RED=\033[0;31m +YELLOW=\033[0;33m NC=\033[0m +.PHONY: +test: simutest + +.PHONY: +check: simucheck + .PHONY: -test: $(X86_GCC_OUT) $(GCC_OUT) +simutest: $(X86_GCC_OUT) $(GCC_SIMUOUT) @echo "Comparing x86 gcc output to k1 gcc.." + for test in $(TESTNAMES); do\ + x86out=$(OUTDIR)/$$test.x86-gcc.out;\ + gccout=$(OUTDIR)/$$test.gcc.simu.out;\ + if grep "__K1C__" -q $$test.c; then\ + printf "$(YELLOW)UNTESTED: $$test.c contains an \`#ifdef __K1C__\`\n";\ + elif $(DIFF) $$x86out $$gccout > /dev/null; test $${PIPESTATUS[0]} -ne 0; then\ + >&2 printf "$(RED)ERROR: $$x86out and $$gccout differ$(NC)\n";\ + else\ + printf "$(GREEN)GOOD: $$x86out and $$gccout concur$(NC)\n";\ + fi;\ + done + +.PHONY: +simucheck: $(GCC_SIMUOUT) $(CCOMP_SIMUOUT) + @echo "Comparing k1 gcc output to ccomp.." @for test in $(TESTNAMES); do\ + gccout=$(OUTDIR)/$$test.gcc.simu.out;\ + ccompout=$(OUTDIR)/$$test.ccomp.simu.out;\ + if $(DIFF) $$ccompout $$gccout > /dev/null; test $${PIPESTATUS[0]} -ne 0; then\ + >&2 printf "$(RED)ERROR: $$ccompout and $$gccout differ$(NC)\n";\ + else\ + printf "$(GREEN)GOOD: $$ccompout and $$gccout concur$(NC)\n";\ + fi;\ + done + +.PHONY: +hardtest: $(X86_GCC_OUT) $(GCC_HARDOUT) + @echo "Comparing x86 gcc output to k1 gcc.." + for test in $(TESTNAMES); do\ x86out=$(OUTDIR)/$$test.x86-gcc.out;\ - gccout=$(OUTDIR)/$$test.gcc.out;\ - if $(DIFF) $$x86out $$gccout > /dev/null; test $${PIPESTATUS[0]} -ne 0; then\ + gccout=$(OUTDIR)/$$test.gcc.hard.out;\ + if grep "__K1C__" -q $$test.c; then\ + printf "$(YELLOW)UNTESTED: $$test.c contains an \`#ifdef __K1C__\`\n";\ + elif $(DIFF) $$x86out $$gccout > /dev/null; test $${PIPESTATUS[0]} -ne 0; then\ >&2 printf "$(RED)ERROR: $$x86out and $$gccout differ$(NC)\n";\ else\ printf "$(GREEN)GOOD: $$x86out and $$gccout concur$(NC)\n";\ @@ -59,11 +101,11 @@ test: $(X86_GCC_OUT) $(GCC_OUT) done .PHONY: -check: $(GCC_OUT) $(CCOMP_OUT) +hardcheck: $(GCC_HARDOUT) $(CCOMP_HARDOUT) @echo "Comparing k1 gcc output to ccomp.." @for test in $(TESTNAMES); do\ - gccout=$(OUTDIR)/$$test.gcc.out;\ - ccompout=$(OUTDIR)/$$test.ccomp.out;\ + gccout=$(OUTDIR)/$$test.gcc.hard.out;\ + ccompout=$(OUTDIR)/$$test.ccomp.hard.out;\ if $(DIFF) $$ccompout $$gccout > /dev/null; test $${PIPESTATUS[0]} -ne 0; then\ >&2 printf "$(RED)ERROR: $$ccompout and $$gccout differ$(NC)\n";\ else\ @@ -89,14 +131,22 @@ $(OUTDIR)/%.x86-gcc.out: $(BINDIR)/%.x86-gcc.bin @mkdir -p $(@D) ret=0; timeout $(TIMEOUT) ./$< > $@ || { ret=$$?; }; echo $$ret >> $@ -$(OUTDIR)/%.gcc.out: $(BINDIR)/%.gcc.bin $(SIMUPATH) +$(OUTDIR)/%.gcc.simu.out: $(BINDIR)/%.gcc.bin $(SIMUPATH) @mkdir -p $(@D) ret=0; timeout $(TIMEOUT) $(SIMU) -- $< > $@ || { ret=$$?; }; echo $$ret >> $@ -$(OUTDIR)/%.ccomp.out: $(BINDIR)/%.ccomp.bin $(SIMUPATH) +$(OUTDIR)/%.ccomp.simu.out: $(BINDIR)/%.ccomp.bin $(SIMUPATH) @mkdir -p $(@D) ret=0; timeout $(TIMEOUT) $(SIMU) -- $< > $@ || { ret=$$?; }; echo $$ret >> $@ +$(OUTDIR)/%.gcc.hard.out: $(BINDIR)/%.gcc.bin $(SIMUPATH) + @mkdir -p $(@D) + ret=0; timeout $(TIMEOUT) $(HARDRUN) --exec-file=Cluster0:$< > $@ || { ret=$$?; }; echo $$ret >> $@ + +$(OUTDIR)/%.ccomp.hard.out: $(BINDIR)/%.ccomp.bin $(SIMUPATH) + @mkdir -p $(@D) + ret=0; timeout $(TIMEOUT) $(HARDRUN) --exec-file=Cluster0:$< > $@ || { ret=$$?; }; echo $$ret >> $@ + # Assembly to binary $(BINDIR)/%.x86-gcc.bin: $(ASMDIR)/%.x86-gcc.s $(LIB) $(CCPATH) @@ -109,7 +159,7 @@ $(BINDIR)/%.gcc.bin: $(ASMDIR)/%.gcc.s $(K1LIB) $(K1CCPATH) $(BINDIR)/%.ccomp.bin: $(ASMDIR)/%.ccomp.s $(K1LIB) $(CCOMPPATH) @mkdir -p $(@D) - $(CCOMP) $(CFLAGS) $(filter-out $(CCOMPPATH),$^) -o $@ + $(CCOMP) $(CCOMPFLAGS) $(filter-out $(CCOMPPATH),$^) -o $@ # Source to assembly @@ -123,4 +173,4 @@ $(ASMDIR)/%.gcc.s: $(SRCDIR)/%.c $(K1CCPATH) $(ASMDIR)/%.ccomp.s: $(SRCDIR)/%.c $(CCOMPPATH) @mkdir -p $(@D) - $(CCOMP) $(CFLAGS) -S $< -o $@ + $(CCOMP) $(CCOMPFLAGS) -S $< -o $@ diff --git a/test/mppa/instr/builtin32.c b/test/mppa/instr/builtin32.c new file mode 100644 index 00000000..c7689dc8 --- /dev/null +++ b/test/mppa/instr/builtin32.c @@ -0,0 +1,12 @@ +#include "framework.h" + +BEGIN_TEST(int) + int *ptr = &c; +#ifdef __K1C__ + int d = c; + a = __builtin_k1_alclrw(ptr); + c = d; + +#endif +END_TEST32() + diff --git a/test/mppa/instr/builtin64.c b/test/mppa/instr/builtin64.c new file mode 100644 index 00000000..dbbb1886 --- /dev/null +++ b/test/mppa/instr/builtin64.c @@ -0,0 +1,17 @@ +#include "framework.h" + +BEGIN_TEST(long long) + long long *ptr = &c; +#ifdef __K1C__ + long long d = c; + a = __builtin_k1_alclrd(ptr); + c = d; + c += a; + + c += __builtin_clzll(a); + + /* Removed the AFADDD builtin who was incorrect in CompCert, see #157 */ + // a = __builtin_k1_afaddd(ptr, a); + // a = __builtin_k1_afaddd(ptr, a); +#endif +END_TEST64() diff --git a/test/mppa/instr/i32.c b/test/mppa/instr/i32.c index c48531b1..e350931c 100644 --- a/test/mppa/instr/i32.c +++ b/test/mppa/instr/i32.c @@ -12,6 +12,14 @@ int tailsum(int a, int b){ return make(a+b); } +int fact(int a){ + int r = 1; + int i; + for (i = 1; i < a; i++) + r *= i; + return r; +} + float int2float(int v){ return v; } @@ -20,6 +28,52 @@ BEGIN_TEST(int) c = a+b; c += a&b; + /* testing if, cb version */ + if ((a & 0x1) == 1) + c += fact(1); + else + c += fact(2); + + if (a & 0x1 == 0) + c += fact(4); + else + c += fact(8); + + if (a & 0x1 == 0) + c += fact(4); + else + c += fact(8); + + b = !(a & 0x01); + if (!b) + c += fact(16); + else + c += fact(32); + + c += sum(make(a), make(b)); + c += (long long) a; + + if (0 > (a & 0x1) - 1) + c += fact(64); + else + c += fact(128); + + if (0 >= (a & 0x1)) + c += fact(256); + else + c += fact(512); + + if ((a & 0x1) > 0) + c += fact(1024); + else + c += fact(2048); + + if ((a & 0x1) - 1 >= 0) + c += fact(4096); + else + c += fact(8192); + + /* cmoved version */ if ((a & 0x1) == 1) c += 1; else @@ -30,15 +84,17 @@ BEGIN_TEST(int) else c += 8; + if (a & 0x1 == 0) + c += 4; + else + c += 8; + b = !(a & 0x01); if (!b) c += 16; else c += 32; - c += sum(make(a), make(b)); - c += (long long) a; - if (0 > (a & 0x1) - 1) c += 64; else @@ -65,6 +121,12 @@ BEGIN_TEST(int) c += (a < b); c += (a + b) / 2; c += (int) int2float(a) + (int) int2float(b) + (int) int2float(42.3); + c += (a << 4); // addx16w + c += (a << 3); // addx8w + c += (a << 2); // addx4w + c += (a << 1); // addx2w + + c += ~a & b; // andnw int j; for (j = 0 ; j < 10 ; j++) diff --git a/test/mppa/instr/i64.c b/test/mppa/instr/i64.c index 00eb159d..e869d93c 100644 --- a/test/mppa/instr/i64.c +++ b/test/mppa/instr/i64.c @@ -30,6 +30,14 @@ long long random_op(long long a, long long b){ return op(a, b); } +long fact(long a){ + long r = 1; + long i; + for (i = 1; i < a; i++) + r *= i; + return r; +} + double long2double(long v){ return v; } @@ -43,6 +51,12 @@ BEGIN_TEST(long long) c += a >> (b & 0x8LL); c += a >> (b & 0x8ULL); c += a % b; + c += (a << 4); // addx16d + c += (a << 3); // addx8d + c += (a << 2); // addx4d + c += (a << 1); // addx2d + + c += ~a & b; // andnd long long d = 3; long long (*op)(long long, long long); @@ -60,6 +74,49 @@ BEGIN_TEST(long long) c += a^b; c += (unsigned int) a; + /* Testing if, cb */ + if (0 != (a & 0x1LL)) + c += fact(1); + else + c += fact(2); + + if (0 > (a & 0x1LL)) + c += fact(4); + else + c += fact(8); + + if (0 >= (a & 0x1LL) - 1) + c += fact(16); + else + c += fact(32); + + if ((unsigned long long)(a & 0x1LL) >= 1) + c += fact(18); + else + c += fact(31); + + + if (a-41414141 > 0) + c += fact(13); + else + c += fact(31); + + if (a & 0x1LL > 0) + c += fact(64); + else + c += fact(128); + + if ((a & 0x1LL) - 1 >= 0) + c += fact(256); + else + c += fact(512); + + if (0 == (a & 0x1LL)) + c += fact(1024); + else + c += fact(2048); + + /* Testing if, cmoved */ if (0 != (a & 0x1LL)) c += 1; else @@ -75,6 +132,11 @@ BEGIN_TEST(long long) else c += 32; + if (a-41414141 > 0) + c += 13; + else + c += 31; + if (a & 0x1LL > 0) c += 64; else diff --git a/test/mppa/interop/Makefile b/test/mppa/interop/Makefile index a405ebd6..3a83d51c 100644 --- a/test/mppa/interop/Makefile +++ b/test/mppa/interop/Makefile @@ -1,9 +1,12 @@ -K1CC ?= k1-mbr-gcc +SHELL := /bin/bash + +K1CC ?= k1-cos-gcc CC ?= gcc CCOMP ?= ccomp CFLAGS ?= -O2 -Wno-varargs SIMU ?= k1-mppa TIMEOUT ?= --signal=SIGTERM 120s +HARDRUN ?= k1-jtag-runner DIR=./ SRCDIR=$(DIR) @@ -31,17 +34,23 @@ SIMUPATH=$(shell which $(SIMU)) TESTNAMES ?= $(filter-out $(VAARG_COMMON),$(filter-out $(COMMON),$(notdir $(subst .c,,$(wildcard $(DIR)/*.c))))) X86_GCC_OUT=$(addprefix $(OUTDIR)/,$(addsuffix .x86-gcc.out,$(TESTNAMES))) -GCC_OUT=$(addprefix $(OUTDIR)/,$(addsuffix .gcc.out,$(TESTNAMES))) -GCC_REV_OUT=$(addprefix $(OUTDIR)/,$(addsuffix .gcc.rev.out,$(TESTNAMES))) -CCOMP_OUT=$(addprefix $(OUTDIR)/,$(addsuffix .ccomp.out,$(TESTNAMES))) +GCC_SIMUOUT=$(addprefix $(OUTDIR)/,$(addsuffix .gcc.simu.out,$(TESTNAMES))) +GCC_REV_SIMUOUT=$(addprefix $(OUTDIR)/,$(addsuffix .gcc.rev.simu.out,$(TESTNAMES))) +CCOMP_SIMUOUT=$(addprefix $(OUTDIR)/,$(addsuffix .ccomp.simu.out,$(TESTNAMES))) + +GCC_HARDOUT=$(addprefix $(OUTDIR)/,$(addsuffix .gcc.hard.out,$(TESTNAMES))) +GCC_REV_HARDOUT=$(addprefix $(OUTDIR)/,$(addsuffix .gcc.rev.hard.out,$(TESTNAMES))) +CCOMP_HARDOUT=$(addprefix $(OUTDIR)/,$(addsuffix .ccomp.hard.out,$(TESTNAMES))) VAARG_X86_GCC_OUT=$(addprefix $(OUTDIR)/,$(addsuffix .x86-gcc.vaarg.out,$(TESTNAMES))) -VAARG_GCC_OUT=$(addprefix $(OUTDIR)/,$(addsuffix .gcc.vaarg.out,$(TESTNAMES))) -VAARG_GCC_REV_OUT=$(addprefix $(OUTDIR)/,$(addsuffix .gcc.rev.vaarg.out,$(TESTNAMES))) -VAARG_CCOMP_OUT=$(addprefix $(OUTDIR)/,$(addsuffix .ccomp.vaarg.out,$(TESTNAMES))) +VAARG_GCC_SIMUOUT=$(addprefix $(OUTDIR)/,$(addsuffix .gcc.vaarg.simu.out,$(TESTNAMES))) +VAARG_GCC_REV_SIMUOUT=$(addprefix $(OUTDIR)/,$(addsuffix .gcc.rev.vaarg.simu.out,$(TESTNAMES))) +VAARG_CCOMP_SIMUOUT=$(addprefix $(OUTDIR)/,$(addsuffix .ccomp.vaarg.simu.out,$(TESTNAMES))) + +VAARG_GCC_HARDOUT=$(addprefix $(OUTDIR)/,$(addsuffix .gcc.vaarg.hard.out,$(TESTNAMES))) +VAARG_GCC_REV_HARDOUT=$(addprefix $(OUTDIR)/,$(addsuffix .gcc.rev.vaarg.hard.out,$(TESTNAMES))) +VAARG_CCOMP_HARDOUT=$(addprefix $(OUTDIR)/,$(addsuffix .ccomp.vaarg.hard.out,$(TESTNAMES))) -OUT=$(X86_GCC_OUT) $(GCC_OUT) $(CCOMP_OUT) $(GCC_REV_OUT)\ - $(VAARG_GCC_OUT) $(VAARG_GCC_OUT) $(VAARG_CCOMP_OUT) $(VAARG_GCC_REV_OUT) BIN=$(addprefix $(BINDIR)/,$(addsuffix .x86-gcc.bin,$(TESTNAMES)))\ $(addprefix $(BINDIR)/,$(addsuffix .gcc.bin,$(TESTNAMES)))\ $(addprefix $(BINDIR)/,$(addsuffix .ccomp.bin,$(TESTNAMES)))\ @@ -61,14 +70,72 @@ GREEN=\033[0;32m RED=\033[0;31m NC=\033[0m +.PHONY: +test: simutest + +.PHONY: +simutest: $(X86_GCC_OUT) $(GCC_SIMUOUT) $(VAARG_X86_GCC_OUT) $(VAARG_GCC_SIMUOUT) + @echo "Comparing x86 gcc output to k1 gcc.." + @for test in $(TESTNAMES); do\ + x86out=$(OUTDIR)/$$test.x86-gcc.out;\ + gccout=$(OUTDIR)/$$test.gcc.simu.out;\ + vaarg_x86out=$(OUTDIR)/$$test.x86-gcc.vaarg.out;\ + vaarg_gccout=$(OUTDIR)/$$test.gcc.vaarg.simu.out;\ + if ! diff $$x86out $$gccout > /dev/null; then\ + >&2 printf "$(RED)ERROR: $$x86out and $$gccout differ$(NC)\n";\ + else\ + printf "$(GREEN)GOOD: $$x86out and $$gccout concur$(NC)\n";\ + fi;\ + if ! diff $$vaarg_x86out $$vaarg_gccout > /dev/null; then\ + >&2 printf "$(RED)ERROR: $$vaarg_x86out and $$vaarg_gccout differ$(NC)\n";\ + else\ + printf "$(GREEN)GOOD: $$vaarg_x86out and $$vaarg_gccout concur$(NC)\n";\ + fi;\ + done + +.PHONY: +check: simucheck + +.PHONY: +simucheck: $(GCC_SIMUOUT) $(CCOMP_SIMUOUT) $(GCC_REV_SIMUOUT) $(VAARG_GCC_SIMUOUT) $(VAARG_CCOMP_SIMUOUT) $(VAARG_GCC_REV_SIMUOUT) + @echo "Comparing k1 gcc output to ccomp.." + @for test in $(TESTNAMES); do\ + gccout=$(OUTDIR)/$$test.gcc.simu.out;\ + ccompout=$(OUTDIR)/$$test.ccomp.simu.out;\ + gccrevout=$(OUTDIR)/$$test.gcc.rev.simu.out;\ + vaarg_gccout=$(OUTDIR)/$$test.gcc.vaarg.simu.out;\ + vaarg_ccompout=$(OUTDIR)/$$test.ccomp.vaarg.simu.out;\ + vaarg_gccrevout=$(OUTDIR)/$$test.gcc.rev.vaarg.simu.out;\ + if ! diff $$ccompout $$gccout > /dev/null; then\ + >&2 printf "$(RED)ERROR: $$ccompout and $$gccout differ$(NC)\n";\ + else\ + printf "$(GREEN)GOOD: $$ccompout and $$gccout concur$(NC)\n";\ + fi;\ + if ! diff $$gccrevout $$gccout > /dev/null; then\ + >&2 printf "$(RED)ERROR: $$gccrevout and $$gccout differ$(NC)\n";\ + else\ + printf "$(GREEN)GOOD: $$gccrevout and $$gccout concur$(NC)\n";\ + fi;\ + if ! diff $$vaarg_ccompout $$vaarg_gccout > /dev/null; then\ + >&2 printf "$(RED)ERROR: $$vaarg_ccompout and $$vaarg_gccout differ$(NC)\n";\ + else\ + printf "$(GREEN)GOOD: $$vaarg_ccompout and $$vaarg_gccout concur$(NC)\n";\ + fi;\ + if ! diff $$vaarg_gccrevout $$vaarg_gccout > /dev/null; then\ + >&2 printf "$(RED)ERROR: $$vaarg_gccrevout and $$vaarg_gccout differ$(NC)\n";\ + else\ + printf "$(GREEN)GOOD: $$vaarg_gccrevout and $$vaarg_gccout concur$(NC)\n";\ + fi;\ + done + .PHONY: -test: $(X86_GCC_OUT) $(GCC_OUT) $(VAARG_X86_GCC_OUT) $(VAARG_GCC_OUT) +hardtest: $(X86_GCC_OUT) $(GCC_HARDOUT) $(VAARG_X86_GCC_OUT) $(VAARG_GCC_HARDOUT) @echo "Comparing x86 gcc output to k1 gcc.." @for test in $(TESTNAMES); do\ x86out=$(OUTDIR)/$$test.x86-gcc.out;\ - gccout=$(OUTDIR)/$$test.gcc.out;\ + gccout=$(OUTDIR)/$$test.gcc.hard.out;\ vaarg_x86out=$(OUTDIR)/$$test.x86-gcc.vaarg.out;\ - vaarg_gccout=$(OUTDIR)/$$test.gcc.vaarg.out;\ + vaarg_gccout=$(OUTDIR)/$$test.gcc.vaarg.hard.out;\ if ! diff $$x86out $$gccout > /dev/null; then\ >&2 printf "$(RED)ERROR: $$x86out and $$gccout differ$(NC)\n";\ else\ @@ -82,15 +149,15 @@ test: $(X86_GCC_OUT) $(GCC_OUT) $(VAARG_X86_GCC_OUT) $(VAARG_GCC_OUT) done .PHONY: -check: $(GCC_OUT) $(CCOMP_OUT) $(GCC_REV_OUT) $(VAARG_GCC_OUT) $(VAARG_CCOMP_OUT) $(VAARG_GCC_REV_OUT) +hardcheck: $(GCC_HARDOUT) $(CCOMP_HARDOUT) $(GCC_REV_HARDOUT) $(VAARG_GCC_HARDOUT) $(VAARG_CCOMP_HARDOUT) $(VAARG_GCC_REV_HARDOUT) @echo "Comparing k1 gcc output to ccomp.." @for test in $(TESTNAMES); do\ - gccout=$(OUTDIR)/$$test.gcc.out;\ - ccompout=$(OUTDIR)/$$test.ccomp.out;\ - gccrevout=$(OUTDIR)/$$test.gcc.rev.out;\ - vaarg_gccout=$(OUTDIR)/$$test.gcc.vaarg.out;\ - vaarg_ccompout=$(OUTDIR)/$$test.ccomp.vaarg.out;\ - vaarg_gccrevout=$(OUTDIR)/$$test.gcc.rev.vaarg.out;\ + gccout=$(OUTDIR)/$$test.gcc.hard.out;\ + ccompout=$(OUTDIR)/$$test.ccomp.hard.out;\ + gccrevout=$(OUTDIR)/$$test.gcc.rev.hard.out;\ + vaarg_gccout=$(OUTDIR)/$$test.gcc.vaarg.hard.out;\ + vaarg_ccompout=$(OUTDIR)/$$test.ccomp.vaarg.hard.out;\ + vaarg_gccrevout=$(OUTDIR)/$$test.gcc.rev.vaarg.hard.out;\ if ! diff $$ccompout $$gccout > /dev/null; then\ >&2 printf "$(RED)ERROR: $$ccompout and $$gccout differ$(NC)\n";\ else\ @@ -142,36 +209,60 @@ $(OUTDIR)/%.x86-gcc.out: $(BINDIR)/%.x86-gcc.bin @mkdir -p $(@D) ret=0; timeout $(TIMEOUT) ./$< > $@ || { ret=$$?; }; echo $$ret >> $@ -$(OUTDIR)/%.gcc.out: $(BINDIR)/%.gcc.bin $(SIMUPATH) +$(OUTDIR)/%.gcc.simu.out: $(BINDIR)/%.gcc.bin $(SIMUPATH) @mkdir -p $(@D) ret=0; timeout $(TIMEOUT) $(SIMU) -- $< > $@ || { ret=$$?; }; echo $$ret >> $@ -$(OUTDIR)/%.gcc.rev.out: $(BINDIR)/%.gcc.rev.bin $(SIMUPATH) +$(OUTDIR)/%.gcc.rev.simu.out: $(BINDIR)/%.gcc.rev.bin $(SIMUPATH) @mkdir -p $(@D) ret=0; timeout $(TIMEOUT) $(SIMU) -- $< > $@ || { ret=$$?; }; echo $$ret >> $@ -$(OUTDIR)/%.ccomp.out: $(BINDIR)/%.ccomp.bin $(SIMUPATH) +$(OUTDIR)/%.ccomp.simu.out: $(BINDIR)/%.ccomp.bin $(SIMUPATH) @mkdir -p $(@D) ret=0; timeout $(TIMEOUT) $(SIMU) -- $< > $@ || { ret=$$?; }; echo $$ret >> $@ +$(OUTDIR)/%.gcc.hard.out: $(BINDIR)/%.gcc.bin $(SIMUPATH) + @mkdir -p $(@D) + ret=0; timeout $(TIMEOUT) $(HARDRUN) --exec-file=Cluster0:$< > $@ || { ret=$$?; }; echo $$ret >> $@ + +$(OUTDIR)/%.gcc.rev.hard.out: $(BINDIR)/%.gcc.rev.bin $(SIMUPATH) + @mkdir -p $(@D) + ret=0; timeout $(TIMEOUT) $(HARDRUN) --exec-file=Cluster0:$< > $@ || { ret=$$?; }; echo $$ret >> $@ + +$(OUTDIR)/%.ccomp.hard.out: $(BINDIR)/%.ccomp.bin $(SIMUPATH) + @mkdir -p $(@D) + ret=0; timeout $(TIMEOUT) $(HARDRUN) --exec-file=Cluster0:$< > $@ || { ret=$$?; }; echo $$ret >> $@ + ## With vaarg $(OUTDIR)/%.x86-gcc.vaarg.out: $(BINDIR)/%.x86-gcc.vaarg.bin @mkdir -p $(@D) ret=0; timeout $(TIMEOUT) ./$< > $@ || { ret=$$?; }; echo $$ret >> $@ -$(OUTDIR)/%.gcc.vaarg.out: $(BINDIR)/%.gcc.vaarg.bin $(SIMUPATH) +$(OUTDIR)/%.gcc.vaarg.simu.out: $(BINDIR)/%.gcc.vaarg.bin $(SIMUPATH) @mkdir -p $(@D) ret=0; timeout $(TIMEOUT) $(SIMU) -- $< > $@ || { ret=$$?; }; echo $$ret >> $@ -$(OUTDIR)/%.gcc.rev.vaarg.out: $(BINDIR)/%.gcc.rev.vaarg.bin $(SIMUPATH) +$(OUTDIR)/%.gcc.rev.vaarg.simu.out: $(BINDIR)/%.gcc.rev.vaarg.bin $(SIMUPATH) @mkdir -p $(@D) ret=0; timeout $(TIMEOUT) $(SIMU) -- $< > $@ || { ret=$$?; }; echo $$ret >> $@ -$(OUTDIR)/%.ccomp.vaarg.out: $(BINDIR)/%.ccomp.vaarg.bin $(SIMUPATH) +$(OUTDIR)/%.ccomp.vaarg.simu.out: $(BINDIR)/%.ccomp.vaarg.bin $(SIMUPATH) @mkdir -p $(@D) ret=0; timeout $(TIMEOUT) $(SIMU) -- $< > $@ || { ret=$$?; }; echo $$ret >> $@ +$(OUTDIR)/%.gcc.vaarg.hard.out: $(BINDIR)/%.gcc.vaarg.bin $(SIMUPATH) + @mkdir -p $(@D) + ret=0; timeout $(TIMEOUT) $(HARDRUN) --exec-file=Cluster0:$< > $@ || { ret=$$?; }; echo $$ret >> $@ + +$(OUTDIR)/%.gcc.rev.vaarg.hard.out: $(BINDIR)/%.gcc.rev.vaarg.bin $(SIMUPATH) + @mkdir -p $(@D) + ret=0; timeout $(TIMEOUT) $(HARDRUN) --exec-file=Cluster0:$< > $@ || { ret=$$?; }; echo $$ret >> $@ + +$(OUTDIR)/%.ccomp.vaarg.hard.out: $(BINDIR)/%.ccomp.vaarg.bin $(SIMUPATH) + @mkdir -p $(@D) + ret=0; timeout $(TIMEOUT) $(HARDRUN) --exec-file=Cluster0:$< > $@ || { ret=$$?; }; echo $$ret >> $@ + ## # Object to binary ## diff --git a/test/mppa/interop/common.c b/test/mppa/interop/common.c index e939e0d1..05b49187 100644 --- a/test/mppa/interop/common.c +++ b/test/mppa/interop/common.c @@ -1,17 +1,21 @@ #define STACK int a[100];\ a[42] = 42; -#define ONEARG_OP(arg) (3*arg+2) +#define ONEARG_OP(arg) (3*magic(arg)+2) -#define MULTIARG_OP(arg1, arg2, arg3, arg4) (arg1 ^ arg2 << arg3 - arg4) +#define MULTIARG_OP(arg1, arg2, arg3, arg4) (arg1 ^ magic(arg2) << arg3 - arg4) #define MANYARG_OP(a0, a1, a2, a3, a4, a5, a6, a7, a8, a9,\ a10, a11, a12, a13, a14, a15, a16, a17, a18, a19,\ a20, a21, a22, a23, a24, a25, a26, a27, a28, a29)\ - (a0 * a1 * a2 * a3 * a4 * a5 * a6 * a7 * a8 * a9 *\ + (a0 * a1 * a2 * magic(a3) * a4 * a5 * a6 * a7 * a8 * a9 *\ a10 * a11 * a12 * a13 * a14 * a15 * a16 * a17 * a18 * a19 *\ a20 * a21 * a22 * a23 * a24 * a25 * a26 * a27 * a28 * a29) +int magic(long a){ + return a*42 + 26; +} + void void_void(){ STACK; } diff --git a/test/mppa/interop/vaarg_common.c b/test/mppa/interop/vaarg_common.c index 9033893b..3314959f 100644 --- a/test/mppa/interop/vaarg_common.c +++ b/test/mppa/interop/vaarg_common.c @@ -3,20 +3,24 @@ #define STACK int a[100];\ a[42] = 42; -#define ONEARG_OP(arg) (3*arg+2) +#define ONEARG_OP(arg) (3*magic(arg)+2) -#define MULTIARG_OP(arg1, arg2, arg3, arg4) (arg1 ^ arg2 << arg3 - arg4) +#define MULTIARG_OP(arg1, arg2, arg3, arg4) (arg1 ^ magic(arg2) << arg3 - arg4) #define MANYARG_OP(a0, a1, a2, a3, a4, a5, a6, a7, a8, a9,\ a10, a11, a12, a13, a14, a15, a16, a17, a18, a19,\ a20, a21, a22, a23, a24, a25, a26, a27, a28, a29)\ - (a0 + a1 * a2 + a3 * a4 + a5 + a6 + a7 - a8 + a9 +\ - a10 + a11 - a12 ^ a13 + a14 - a15 + a16 ^ a17 + a18 + a19 +\ + (a0 + a1 * a2 + magic(a3) * a4 + a5 + a6 + a7 - a8 + a9 +\ + a10 + a11 - a12 ^ a13 + a14 - magic(a15) + a16 ^ a17 + a18 + a19 +\ a20 + a21 + a22 * a23 + a24 + a25 << a26 & a27 + a28 + a29) #define VA_START(vl, arg) va_list vl; va_start(vl, arg) #define VA_END(vl) va_end(vl) +int magic(long a){ + return a*2 + 42; +} + void void_void(void){ STACK; } diff --git a/test/mppa/lib/Makefile b/test/mppa/lib/Makefile index affc1afd..08901db6 100644 --- a/test/mppa/lib/Makefile +++ b/test/mppa/lib/Makefile @@ -1,5 +1,5 @@ -K1CC ?= k1-mbr-gcc -K1AR ?= k1-mbr-ar +K1CC ?= k1-cos-gcc +K1AR ?= k1-cos-ar CC ?= gcc AR ?= gcc-ar CCOMP ?= ccomp diff --git a/test/mppa/mmult/Makefile b/test/mppa/mmult/Makefile index 5895ce3d..667faef8 100644 --- a/test/mppa/mmult/Makefile +++ b/test/mppa/mmult/Makefile @@ -1,4 +1,4 @@ -K1CC ?= k1-mbr-gcc +K1CC ?= k1-cos-gcc CC ?= gcc CCOMP ?= ccomp CFLAGS ?= -O2 diff --git a/test/mppa/prng/Makefile b/test/mppa/prng/Makefile index 4770c901..9cbb3872 100644 --- a/test/mppa/prng/Makefile +++ b/test/mppa/prng/Makefile @@ -1,4 +1,4 @@ -K1CC ?= k1-mbr-gcc +K1CC ?= k1-cos-gcc CC ?= gcc CCOMP ?= ccomp CFLAGS ?= -O2 diff --git a/test/mppa/simucheck.sh b/test/mppa/simucheck.sh new file mode 100755 index 00000000..25fb9947 --- /dev/null +++ b/test/mppa/simucheck.sh @@ -0,0 +1,6 @@ +#!/bin/bash +# Tests the execution of the binaries produced by CompCert, by simulation + +source do_test.sh + +do_test check $1 diff --git a/test/mppa/test.sh b/test/mppa/simutest.sh index 30806a6b..3b1021e6 100755 --- a/test/mppa/test.sh +++ b/test/mppa/simutest.sh @@ -1,5 +1,5 @@ #!/bin/bash -# Tests the validity of the tests +# Tests the validity of the tests, in simulator source do_test.sh diff --git a/test/mppa/sort/Makefile b/test/mppa/sort/Makefile index 5173528c..0ae9d1f6 100644 --- a/test/mppa/sort/Makefile +++ b/test/mppa/sort/Makefile @@ -1,4 +1,4 @@ -K1CC ?= k1-mbr-gcc +K1CC ?= k1-cos-gcc CC ?= gcc CCOMP ?= ccomp CFLAGS ?= -O2 |