Merge branch 'mppa_k1c' into mppa_postpass

4 files changed, 80 insertions, 79 deletions

diff --git a/mppa_k1c/Asm.v b/mppa_k1c/Asm.v
index 520bc453..23b11a03 100644
--- a/mppa_k1c/Asm.v
+++ b/mppa_k1c/Asm.v
@@ -181,7 +181,7 @@ Definition basic_to_instruction (b: basic) :=
   (* RR *)

   | PArithRR Asmblock.Pmv rd rs     => Pmv rd rs

   | PArithRR Asmblock.Pnegw rd rs   => Pnegw rd rs

-  | PArithRR Asmblock.Pnegl rd rs   => Pfnegd rd rs

+  | PArithRR Asmblock.Pnegl rd rs   => Pnegl rd rs

   | PArithRR Asmblock.Pcvtl2w rd rs => Pcvtl2w rd rs

   | PArithRR Asmblock.Pmvw2l rd rs  => Pmvw2l rd rs

   | PArithRR Asmblock.Pfnegd rd rs  => Pfnegd rd rs

diff --git a/mppa_k1c/Asmblockgen.v b/mppa_k1c/Asmblockgen.v
index a4d0526d..9a564117 100644
--- a/mppa_k1c/Asmblockgen.v
+++ b/mppa_k1c/Asmblockgen.v
@@ -398,19 +398,19 @@ Definition transl_op
   | Omulhu, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Pmulhuw rd rs1 rs2 :: k)
-  | Odiv, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pdivw rd rs1 rs2 :: k)
-  | Odivu, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Pdivuw rd rs1 rs2 :: k)
-  | Omod, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Premw rd rs1 rs2 :: k)
-  | Omodu, a1 :: a2 :: nil =>
-      do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
-      OK (Premuw rd rs1 rs2 :: k)
-*)| Oand, a1 :: a2 :: nil =>
+*)| Odiv, a1 :: a2 :: nil => Error(msg "32-bits division not supported yet. Please use 64-bits.")
+      (* do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
+      OK (Pdivw rd rs1 rs2 :: k) *)
+  | Odivu, a1 :: a2 :: nil => Error(msg "32-bits division not supported yet. Please use 64-bits.")
+      (* do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
+      OK (Pdivuw rd rs1 rs2 :: k) *)
+  | Omod, a1 :: a2 :: nil => Error(msg "32-bits modulo not supported yet. Please use 64-bits.")
+      (* do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
+      OK (Premw rd rs1 rs2 :: k) *)
+  | Omodu, a1 :: a2 :: nil => Error(msg "32-bits modulo not supported yet. Please use 64-bits.")
+      (* do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
+      OK (Premuw rd rs1 rs2 :: k) *)
+  | Oand, a1 :: a2 :: nil =>
       do rd <- ireg_of res; do rs1 <- ireg_of a1; do rs2 <- ireg_of a2;
       OK (Pandw rd rs1 rs2 ::i k)
   | Oandimm n, a1 :: nil =>
diff --git a/mppa_k1c/CBuiltins.ml b/mppa_k1c/CBuiltins.ml
index a5bdaa28..147bbb55 100644
--- a/mppa_k1c/CBuiltins.ml
+++ b/mppa_k1c/CBuiltins.ml
@@ -59,6 +59,7 @@ let builtins = {
       "__builtin_k1_lwzu", (TInt(IUInt, []), [TPtr(TVoid [], [])], false);
 
       (* ALU Instructions *)
+      "__builtin_clzll", (TInt(IULongLong, []), [TInt(IULongLong, [])], false);
       (* "__builtin_k1_addhp", (TInt(IInt, []), [TInt(IInt, []); TInt(IInt, [])], false); *)
       (* "__builtin_k1_adds", (TInt(IInt, []), [TInt(IInt, []); TInt(IInt, [])], false); *)
       (* "__builtin_k1_bwlu", (TInt(IUInt, []), 
diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml
index 7db82f6f..cd36b502 100644
--- a/mppa_k1c/TargetPrinter.ml
+++ b/mppa_k1c/TargetPrinter.ml
@@ -127,9 +127,9 @@ module Target (*: TARGET*) =
     let loadsymbol oc r id ofs =
       if Archi.pic_code () then begin
         assert (ofs = Integers.Ptrofs.zero);
-        fprintf oc "	make	%a = %s\n" ireg r (extern_atom id)
+        fprintf oc "	make	%a = %s\n;;\n" ireg r (extern_atom id)
       end else begin
-        fprintf oc "	make	%a = %a\n" ireg r symbol_offset (id, ofs)
+        fprintf oc "	make	%a = %a\n;;\n" ireg r symbol_offset (id, ofs)
       end
     
 (* Emit .file / .loc debugging directives *)
@@ -221,51 +221,51 @@ module Target (*: TARGET*) =
           | _ ->
               assert false
          end
-      | Pnop -> fprintf oc "	nop\n"
-      | Psemi -> fprintf oc ";;\n"
+      | Pnop -> fprintf oc "	nop\n;;\n"
+      | Psemi -> fprintf oc ""
 
-      | Pclzll (rd, rs) -> fprintf oc "	clzd %a = %a\n" ireg rd ireg rs
-      | Pstsud (rd, rs1, rs2) -> fprintf oc "	stsud %a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+      | Pclzll (rd, rs) -> fprintf oc "	clzd %a = %a\n;;\n" ireg rd ireg rs
+      | Pstsud (rd, rs1, rs2) -> fprintf oc "	stsud %a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
 
 
       (* Control flow instructions *)
       | Pget (rd, rs) ->
-         fprintf oc "	get	%a = %a\n" ireg rd preg rs
+         fprintf oc "	get	%a = %a\n;;\n" ireg rd preg rs
       | Pset (rd, rs) ->
-         fprintf oc "	set	%a = %a\n" preg rd ireg rs
+         fprintf oc "	set	%a = %a\n;;\n" preg rd ireg rs
       | Pret ->
-         fprintf oc "	ret	\n"
+         fprintf oc "	ret	\n;;\n"
       | Pcall(s) ->
-         fprintf oc "	call	%a\n" symbol s
+         fprintf oc "	call	%a\n;;\n" symbol s
       | Pgoto(s) ->
-         fprintf oc "	goto	%a\n" symbol s
+         fprintf oc "	goto	%a\n;;\n" symbol s
       | Pj_l(s) ->
-         fprintf oc "	goto	%a\n" print_label s
+         fprintf oc "	goto	%a\n;;\n" print_label s
       | Pcb (bt, r, lbl) | Pcbu (bt, r, lbl) ->
-         fprintf oc "	cb.%a	%a?%a\n" bcond bt ireg r print_label lbl
+         fprintf oc "	cb.%a	%a?%a\n;;\n" bcond bt ireg r print_label lbl
 
       (* Load/Store instructions *)
       | Plb(rd, ra, ofs) ->
-         fprintf oc "	lbs	%a = %a[%a]\n" ireg rd offset ofs ireg ra
+         fprintf oc "	lbs	%a = %a[%a]\n;;\n" ireg rd offset ofs ireg ra
       | Plbu(rd, ra, ofs) ->
-         fprintf oc "	lbz	%a = %a[%a]\n" ireg rd offset ofs ireg ra
+         fprintf oc "	lbz	%a = %a[%a]\n;;\n" ireg rd offset ofs ireg ra
       | Plh(rd, ra, ofs) ->
-         fprintf oc "	lhs	%a = %a[%a]\n" ireg rd offset ofs ireg ra
+         fprintf oc "	lhs	%a = %a[%a]\n;;\n" ireg rd offset ofs ireg ra
       | Plhu(rd, ra, ofs) ->
-         fprintf oc "	lhz	%a = %a[%a]\n" ireg rd offset ofs ireg ra
+         fprintf oc "	lhz	%a = %a[%a]\n;;\n" ireg rd offset ofs ireg ra
       | Plw(rd, ra, ofs) | Plw_a(rd, ra, ofs) | Pfls(rd, ra, ofs) ->
-         fprintf oc "	lws	%a = %a[%a]\n" ireg rd offset ofs ireg ra
+         fprintf oc "	lws	%a = %a[%a]\n;;\n" ireg rd offset ofs ireg ra
       | Pld(rd, ra, ofs) | Pfld(rd, ra, ofs) | Pld_a(rd, ra, ofs) -> assert Archi.ptr64;
-         fprintf oc "	ld	%a = %a[%a]\n" ireg rd offset ofs ireg ra
+         fprintf oc "	ld	%a = %a[%a]\n;;\n" ireg rd offset ofs ireg ra
     
       | Psb(rd, ra, ofs) ->
-         fprintf oc "	sb	%a[%a] = %a\n" offset ofs ireg ra ireg rd
+         fprintf oc "	sb	%a[%a] = %a\n;;\n" offset ofs ireg ra ireg rd
       | Psh(rd, ra, ofs) ->
-         fprintf oc "	sh	%a[%a] = %a\n" offset ofs ireg ra ireg rd
+         fprintf oc "	sh	%a[%a] = %a\n;;\n" offset ofs ireg ra ireg rd
       | Psw(rd, ra, ofs) | Psw_a(rd, ra, ofs) | Pfss(rd, ra, ofs) ->
-         fprintf oc "	sw	%a[%a] = %a\n" offset ofs ireg ra ireg rd
+         fprintf oc "	sw	%a[%a] = %a\n;;\n" offset ofs ireg ra ireg rd
       | Psd(rd, ra, ofs) | Psd_a(rd, ra, ofs) | Pfsd(rd, ra, ofs) -> assert Archi.ptr64;
-         fprintf oc "	sd	%a[%a] = %a\n" offset ofs ireg ra ireg rd
+         fprintf oc "	sd	%a[%a] = %a\n;;\n" offset ofs ireg ra ireg rd
 
       (* Arith R instructions *)
       | Pcvtw2l(rd) -> assert false 
@@ -273,102 +273,102 @@ module Target (*: TARGET*) =
 
       (* Arith RR instructions *)
       | Pmv(rd, rs) | Pmvw2l(rd, rs) ->
-         fprintf oc "	addd	%a = %a, 0\n"     ireg rd ireg rs
+         fprintf oc "	addd	%a = %a, 0\n;;\n"     ireg rd ireg rs
       | Pcvtl2w(rd, rs) -> assert false
       | Pnegl(rd, rs) -> assert Archi.ptr64;
-         fprintf oc "	negd	%a = %a\n" ireg rd ireg rs
+         fprintf oc "	negd	%a = %a\n;;\n" ireg rd ireg rs
       | Pnegw(rd, rs) ->
-         fprintf oc "	negw	%a = %a\n" ireg rd ireg rs
+         fprintf oc "	negw	%a = %a\n;;\n" ireg rd ireg rs
       | Pfnegd(rd, rs) ->
-         fprintf oc "	fnegd	%a = %a\n" ireg rs ireg rd
+         fprintf oc "	fnegd	%a = %a\n;;\n" ireg rs ireg rd
 
       (* Arith RI32 instructions *)
       | Pmake (rd, imm) ->
-         fprintf oc "	make	%a, %a\n" ireg rd coqint imm
+         fprintf oc "	make	%a, %a\n;;\n" ireg rd coqint imm
 
       (* Arith RI64 instructions *)
       | Pmakel (rd, imm) ->
-         fprintf oc "	make	%a, %a\n" ireg rd coqint64 imm
+         fprintf oc "	make	%a, %a\n;;\n" ireg rd coqint64 imm
 
       (* Arith RRR instructions *)
       | Pcompw (it, rd, rs1, rs2) ->
-         fprintf oc "	compw.%a	%a = %a, %a\n" icond it ireg rd ireg rs1 ireg rs2
+         fprintf oc "	compw.%a	%a = %a, %a\n;;\n" icond it ireg rd ireg rs1 ireg rs2
       | Pcompl (it, rd, rs1, rs2) ->
-         fprintf oc "	compd.%a	%a = %a, %a\n" icond it ireg rd ireg rs1 ireg rs2
+         fprintf oc "	compd.%a	%a = %a, %a\n;;\n" icond it ireg rd ireg rs1 ireg rs2
 
       | Paddw (rd, rs1, rs2) ->
-         fprintf oc "	addw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+         fprintf oc "	addw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
       | Psubw (rd, rs1, rs2) ->
-         fprintf oc "	sbfw	%a = %a, %a\n" ireg rd ireg rs2 ireg rs1
+         fprintf oc "	sbfw	%a = %a, %a\n;;\n" ireg rd ireg rs2 ireg rs1
       | Pmulw (rd, rs1, rs2) ->
-         fprintf oc "	mulw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+         fprintf oc "	mulw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
       | Pandw (rd, rs1, rs2) ->
-         fprintf oc "	andw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+         fprintf oc "	andw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
       | Porw (rd, rs1, rs2) -> 
-         fprintf oc "	orw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+         fprintf oc "	orw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
       | Pxorw (rd, rs1, rs2) -> 
-         fprintf oc "	xorw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+         fprintf oc "	xorw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
       | Psraw (rd, rs1, rs2) ->
-         fprintf oc "	sraw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+         fprintf oc "	sraw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
       | Psrlw (rd, rs1, rs2) ->
-         fprintf oc "	srlw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+         fprintf oc "	srlw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
       | Psllw (rd, rs1, rs2) ->
-         fprintf oc "	sllw	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+         fprintf oc "	sllw	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
 
       | Paddl (rd, rs1, rs2) -> assert Archi.ptr64;
-         fprintf oc "	addd	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+         fprintf oc "	addd	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
       | Psubl (rd, rs1, rs2) ->
-         fprintf oc "	sbfd	%a = %a, %a\n" ireg rd ireg rs2 ireg rs1
+         fprintf oc "	sbfd	%a = %a, %a\n;;\n" ireg rd ireg rs2 ireg rs1
       | Pandl (rd, rs1, rs2) -> assert Archi.ptr64;
-         fprintf oc "	andd	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+         fprintf oc "	andd	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
       | Porl (rd, rs1, rs2) -> assert Archi.ptr64;
-         fprintf oc "	ord	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+         fprintf oc "	ord	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
       | Pxorl (rd, rs1, rs2) -> assert Archi.ptr64;
-         fprintf oc "	xord	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+         fprintf oc "	xord	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
       | Pmull (rd, rs1, rs2) ->
-         fprintf oc "	muld	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+         fprintf oc "	muld	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
       | Pslll  (rd, rs1, rs2) ->
-         fprintf oc "	slld	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+         fprintf oc "	slld	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
       | Psrll  (rd, rs1, rs2) ->
-         fprintf oc "	srld	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+         fprintf oc "	srld	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
       | Psral   (rd, rs1, rs2) ->
-         fprintf oc "	srad	%a = %a, %a\n" ireg rd ireg rs1 ireg rs2
+         fprintf oc "	srad	%a = %a, %a\n;;\n" ireg rd ireg rs1 ireg rs2
 
       (* Arith RRI32 instructions *)
       | Pcompiw (it, rd, rs, imm) ->
-         fprintf oc "	compw.%a	%a = %a, %a\n" icond it ireg rd ireg rs coqint64 imm
+         fprintf oc "	compw.%a	%a = %a, %a\n;;\n" icond it ireg rd ireg rs coqint64 imm
       | Paddiw (rd, rs, imm) ->
-         fprintf oc "	addw	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
+         fprintf oc "	addw	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
       | Pandiw (rd, rs, imm) ->
-         fprintf oc "	andw	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
+         fprintf oc "	andw	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
       | Poriw (rd, rs, imm) -> 
-         fprintf oc "	orw	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
+         fprintf oc "	orw	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
       | Pxoriw (rd, rs, imm) -> 
-         fprintf oc "	xorw	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
+         fprintf oc "	xorw	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
       | Psraiw (rd, rs, imm) ->
-         fprintf oc "	sraw	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
+         fprintf oc "	sraw	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
       | Psrliw (rd, rs, imm) ->
-         fprintf oc "	srlw	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
+         fprintf oc "	srlw	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
       | Pslliw (rd, rs, imm) ->
-         fprintf oc "	sllw	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
+         fprintf oc "	sllw	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
       | Psllil (rd, rs, imm) ->
-         fprintf oc "	slld	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
+         fprintf oc "	slld	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
       | Psrlil (rd, rs, imm) ->
-         fprintf oc "	srld	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
+         fprintf oc "	srld	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
       | Psrail (rd, rs, imm) ->
-         fprintf oc "	srad	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
+         fprintf oc "	srad	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
 
     (* Arith RRI64 instructions *)
       | Pcompil (it, rd, rs, imm) ->
-         fprintf oc "	compd.%a	%a = %a, %a\n" icond it ireg rd ireg rs coqint64 imm
+         fprintf oc "	compd.%a	%a = %a, %a\n;;\n" icond it ireg rd ireg rs coqint64 imm
       | Paddil (rd, rs, imm) -> assert Archi.ptr64;
-         fprintf oc "	addd	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
+         fprintf oc "	addd	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
       | Pandil (rd, rs, imm) -> assert Archi.ptr64;
-         fprintf oc "	andd	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
+         fprintf oc "	andd	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
       | Poril (rd, rs, imm) -> assert Archi.ptr64;
-         fprintf oc "	ord	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
+         fprintf oc "	ord	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
       | Pxoril (rd, rs, imm) -> assert Archi.ptr64;
-         fprintf oc "	xord	%a = %a, %a\n" ireg rd ireg rs coqint64 imm
+         fprintf oc "	xord	%a = %a, %a\n;;\n" ireg rd ireg rs coqint64 imm
 
     let get_section_names name =
       let (text, lit) =