MPPA - Added Pmull -> now able to run the sort test

mppa_k1c/Asm.v

@@ -226,6 +226,7 @@ Inductive instruction : Type :=
   | Pandl   (rd: ireg) (rs1 rs2: ireg)              (**r integer andition *)
   | Porl    (rd: ireg) (rs1 rs2: ireg)              (**r or long *)
   | Pnegl   (rd: ireg) (rs: ireg)                   (**r negate long *)
+  | Pmull   (rd: ireg) (rs1 rs2: ireg)              (**r integer mulition long (low part) *)
   | Pslll   (rd: ireg) (rs1 rs2: ireg)              (**r shift left logical long *)
   | Psrll   (rd: ireg) (rs1 rs2: ireg)              (**r shift right logical long *)
   | Psral   (rd: ireg) (rs1 rs2: ireg)              (**r shift right arithmetic long *)
@@ -807,6 +808,8 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
       Next (nextinstr (rs#d <- (Val.orl  rs###s1 rs###s2))) m
   | Pnegl d s =>
       Next (nextinstr (rs#d <- (Val.negl rs###s))) m
+  | Pmull d s1 s2 =>
+      Next (nextinstr (rs#d <- (Val.mull rs###s1 rs###s2))) m
   | Pslll d s1 s2 =>
       Next (nextinstr (rs#d <- (Val.shll rs###s1 rs###s2))) m
   | Psrll d s1 s2 =>

mppa_k1c/Asmgen.v

@@ -377,10 +377,10 @@ Definition transl_op
 (*| Osubl, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Psubl rd rs1 rs2 :: k)
-  | Omull, a1 :: a2 :: nil =>
+*)| Omull, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Pmull rd rs1 rs2 :: k)
-  | Omullhs, a1 :: a2 :: nil =>
+(*| Omullhs, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Pmulhl rd rs1 rs2 :: k)
   | Omullhu, a1 :: a2 :: nil =>

mppa_k1c/TargetPrinter.ml

@@ -216,6 +216,8 @@ module Target : TARGET =
 
       | Pmulw(rd, rs1, rs2) ->
          fprintf oc "	mulw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
+      | Pmull(rd, rs1, rs2) ->
+         fprintf oc "	muld	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
 
       | Psrliw (rd, rs, imm) ->
          fprintf oc "	srlw	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm

test/mppa/Makefile

@@ -34,7 +34,11 @@ $(DIR)/output/%.bin.exp: $(DIR)/%.c
 FORCE:
 
 .PHONY:
-check: $(TOK)
+check: $(TOK) sort
+
+.PHONY:
+sort: FORCE
+	(cd sort && make compc-check)
 
 .PHONY:
 clean:

test/mppa/sort/.gitignore

@@ -6,3 +6,4 @@ test-k1c
 merge-test-x86
 selection-test-x86
 test-x86
+test-ccomp

test/mppa/sort/Makefile

@@ -35,9 +35,9 @@ check: check-x86 check-k1c
 .PHONY:
 compc-check: test-ccomp
 	@if ! k1-cluster -- ./$<; then\
-		>&2 echo "ERROR k1c: $< failed";\
+		>&2 echo "ERROR k1c: sort $< failed";\
 	else\
-		echo "k1c: Test $< succeeded";\
+		echo "k1c: Test sort $< succeeded";\
 	fi
 
 .PHONY: