diff options
| -rw-r--r-- | mppa_k1c/Asm.v | 4 | ||||
| -rw-r--r-- | mppa_k1c/Asmexpand.ml | 4 | ||||
| -rw-r--r-- | mppa_k1c/CBuiltins.ml | 4 | ||||
| -rw-r--r-- | mppa_k1c/TargetPrinter.ml | 4 | ||||
| -rw-r--r-- | test/mppa/instr/Makefile | 5 | ||||
| -rw-r--r-- | test/mppa/instr/builtin64.c | 10 |
6 files changed, 22 insertions, 9 deletions
diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v index 1964e5f8..a0c5e71c 100644 --- a/mppa_k1c/Asm.v +++ b/mppa_k1c/Asm.v @@ -99,8 +99,8 @@ Inductive instruction : Type := | Piinvals (addr: ireg)
| Pitouchl (addr: ireg)
| Pdzerol (addr: ireg)
- | Pafaddd (addr: ireg) (incr_res: ireg)
- | Pafaddw (addr: ireg) (incr_res: ireg)
+(*| Pafaddd (addr: ireg) (incr_res: ireg)
+ | Pafaddw (addr: ireg) (incr_res: ireg) *) (* see #157 *)
| Palclrd (dst: ireg) (addr: ireg)
| Palclrw (dst: ireg) (addr: ireg)
| Pclzll (rd rs: ireg)
diff --git a/mppa_k1c/Asmexpand.ml b/mppa_k1c/Asmexpand.ml index 65dee6c7..20d27951 100644 --- a/mppa_k1c/Asmexpand.ml +++ b/mppa_k1c/Asmexpand.ml @@ -465,14 +465,14 @@ let expand_builtin_inline name args res = let open Asmvliw in emit (Pitouchl addr) | "__builtin_k1_dzerol", [BA(IR addr)], _ -> emit (Pdzerol addr) - | "__builtin_k1_afaddd", [BA(IR addr); BA (IR incr_res)], BR(IR res) -> +(*| "__builtin_k1_afaddd", [BA(IR addr); BA (IR incr_res)], BR(IR res) -> (if res <> incr_res then (emit (Pmv(res, incr_res)); emit Psemi)); emit (Pafaddd(addr, res)) | "__builtin_k1_afaddw", [BA(IR addr); BA (IR incr_res)], BR(IR res) -> (if res <> incr_res then (emit (Pmv(res, incr_res)); emit Psemi)); - emit (Pafaddw(addr, res)) + emit (Pafaddw(addr, res)) *) (* see #157 *) | "__builtin_alclrd", [BA(IR addr)], BR(IR res) -> emit (Palclrd(res, addr)) | "__builtin_alclrw", [BA(IR addr)], BR(IR res) -> diff --git a/mppa_k1c/CBuiltins.ml b/mppa_k1c/CBuiltins.ml index 2f80c90f..a02da077 100644 --- a/mppa_k1c/CBuiltins.ml +++ b/mppa_k1c/CBuiltins.ml @@ -43,8 +43,8 @@ let builtins = { (* LSU Instructions *) (* acswapd and acswapw done using headers and assembly *) - "__builtin_k1_afaddd", (TInt(IULongLong, []), [TPtr(TVoid [], []); TInt(ILongLong, [])], false); - "__builtin_k1_afaddw", (TInt(IUInt, []), [TPtr(TVoid [], []); TInt(IInt, [])], false); +(* "__builtin_k1_afaddd", (TInt(IULongLong, []), [TPtr(TVoid [], []); TInt(ILongLong, [])], false); + "__builtin_k1_afaddw", (TInt(IUInt, []), [TPtr(TVoid [], []); TInt(IInt, [])], false); *) (* see #157 *) "__builtin_k1_alclrd", (TInt(IULongLong, []), [TPtr(TVoid [], [])], false); (* DONE *) "__builtin_k1_alclrw", (TInt(IUInt, []), [TPtr(TVoid [], [])], false); (* DONE *) "__builtin_k1_dinval", (TVoid [], [], false); (* DONE *) diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 674695d9..2621a43b 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -399,10 +399,10 @@ module Target (*: TARGET*) = fprintf oc " itouchl 0[%a]\n" ireg addr | Pdzerol addr -> fprintf oc " dzerol 0[%a]\n" ireg addr - | Pafaddd(addr, incr_res) -> +(* | Pafaddd(addr, incr_res) -> fprintf oc " afaddd 0[%a] = %a\n" ireg addr ireg incr_res | Pafaddw(addr, incr_res) -> - fprintf oc " afaddw 0[%a] = %a\n" ireg addr ireg incr_res + fprintf oc " afaddw 0[%a] = %a\n" ireg addr ireg incr_res *) (* see #157 *) | Palclrd(res, addr) -> fprintf oc " alclrd %a = 0[%a]\n" ireg res ireg addr | Palclrw(res, addr) -> diff --git a/test/mppa/instr/Makefile b/test/mppa/instr/Makefile index 33a265e3..69446796 100644 --- a/test/mppa/instr/Makefile +++ b/test/mppa/instr/Makefile @@ -46,6 +46,7 @@ all: $(BIN) GREEN=\033[0;32m RED=\033[0;31m +YELLOW=\033[0;33m NC=\033[0m .PHONY: @@ -54,7 +55,9 @@ test: $(X86_GCC_OUT) $(GCC_OUT) 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\ + 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";\ diff --git a/test/mppa/instr/builtin64.c b/test/mppa/instr/builtin64.c new file mode 100644 index 00000000..40d53dc7 --- /dev/null +++ b/test/mppa/instr/builtin64.c @@ -0,0 +1,10 @@ +#include "framework.h" + +BEGIN_TEST(long long) + long long *ptr = &c; +#ifdef __K1C__ + /* 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() |