New builtin for dcbz instruction.

This commit adds a builtin for the dcbz instructions. Additionally
the dcbt,dcbtst,dcbtls and icbtls instruction are changed to their
actually form all taking one additional register in Asm.v.

5 files changed, 33 insertions, 24 deletions

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 32c7ba70..6444baf9 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -167,9 +167,10 @@ Inductive instruction : Type :=
   | Pcrxor: crbit -> crbit -> crbit -> instruction            (**r xor between condition bits *)
   | Pdcbf: ireg -> ireg -> instruction                        (**r data cache flush *)
   | Pdcbi: ireg -> ireg -> instruction                        (**r data cache invalidate *)
-  | Pdcbt: int -> ireg -> instruction                         (**r data cache block touch *)
-  | Pdcbtst: int -> ireg -> instruction                       (**r data cache block touch *)
-  | Pdcbtls: int -> ireg -> instruction                       (**r data cache block touch and lock set *)
+  | Pdcbt: int -> ireg -> ireg -> instruction                 (**r data cache block touch *)
+  | Pdcbtst: int -> ireg -> ireg -> instruction               (**r data cache block touch *)
+  | Pdcbtls: int -> ireg -> ireg -> instruction               (**r data cache block touch and lock *)
+  | Pdcbz: ireg -> ireg -> instruction                        (**r data cache block zero *)
   | Pdivw: ireg -> ireg -> ireg -> instruction                (**r signed division *)
   | Pdivwu: ireg -> ireg -> ireg -> instruction               (**r unsigned division *)
   | Peieio: instruction                                       (**r EIEIO barrier *)
@@ -207,7 +208,7 @@ Inductive instruction : Type :=
   | Pfsel: freg -> freg -> freg -> freg -> instruction        (**r FP conditional move *)
   | Pisync: instruction                                       (**r ISYNC barrier *)
   | Picbi: ireg -> ireg -> instruction                        (**r instruction cache invalidate *)
-  | Picbtls: int -> ireg -> instruction                       (**r instruction cache block touch and lock set *)
+  | Picbtls: int -> ireg -> ireg -> instruction               (**r instruction cache block touch and lock set *)
   | Plbz: ireg -> constant -> ireg -> instruction             (**r load 8-bit unsigned int *)
   | Plbzx: ireg -> ireg -> ireg -> instruction                (**r same, with 2 index regs *)
   | Plfd: freg -> constant -> ireg -> instruction             (**r load 64-bit float *)
@@ -874,9 +875,10 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pcrxor _ _ _
   | Pdcbf _ _
   | Pdcbi _ _
-  | Pdcbt _ _
-  | Pdcbtst _ _
-  | Pdcbtls _ _
+  | Pdcbt _ _ _
+  | Pdcbtst _ _ _
+  | Pdcbtls _ _ _
+  | Pdcbz _ _
   | Peieio
   | Pfctiw _ _
   | Pfctiwz _ _
@@ -891,7 +893,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Plwarx _ _ _
   | Plwbrx _ _ _
   | Picbi _ _
-  | Picbtls _ _
+  | Picbtls _ _ _
   | Pisync
   | Plwsync
   | Plhbrx _ _ _
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml
index 8493f168..83d01dc5 100644
--- a/powerpc/AsmToJSON.ml
+++ b/powerpc/AsmToJSON.ml
@@ -177,9 +177,10 @@ let p_instruction oc ic =
   | Pcrxor (cr1,cr2,cr3) -> fprintf oc "{\"Instruction Name\":\"Pcrxor\",\"Args\":[%a,%a,%a]}" p_crbit cr1 p_crbit cr2 p_crbit cr3
   | Pdcbf (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pdcbf\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2
   | Pdcbi (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pdcbi\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2
-  | Pdcbt (n,ir1) -> fprintf oc "{\"Instruction Name\":\"Pdcbt\",\"Args\":[%a,%a]}" p_int_constant n p_ireg ir1
-  | Pdcbtst (n,ir1) -> fprintf oc "{\"Instruction Name\":\"Pdcbtst\",\"Args\":[%a,%a]}" p_int_constant n p_ireg ir1
-  | Pdcbtls (n,ir1) -> fprintf oc "{\"Instruction Name\":\"Pdcbtls\",\"Args\":[%a,%a]}" p_int_constant n p_ireg ir1
+  | Pdcbt (n,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pdcbt\",\"Args\":[%a,%a,%a]}" p_int_constant n p_ireg ir1 p_ireg ir2
+  | Pdcbtst (n,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pdcbtst\",\"Args\":[%a,%a,%a]}" p_int_constant n p_ireg ir1 p_ireg ir2
+  | Pdcbtls (n,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pdcbtls\",\"Args\":[%a,%a,%a]}" p_int_constant n p_ireg ir1 p_ireg ir2
+  | Pdcbz (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pdcbz\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2
   | Pdivw (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pdivw\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
   | Pdivwu (ir1,ir2,ir3) -> fprintf oc "{\"Instruction Name\":\"Pdivwu\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_ireg ir2 p_ireg ir3
   | Peieio -> fprintf oc "{\"Instruction Name\":\"Peieio,\"Args\":[]}"
@@ -216,7 +217,7 @@ let p_instruction oc ic =
   | Pfres (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfres\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2
   | Pfsel (fr1,fr2,fr3,fr4) -> fprintf oc "{\"Instruction Name\":\"Pfsel\",\"Args\":[%a,%a,%a,%a]}" p_freg fr1 p_freg fr2 p_freg fr3 p_freg fr4
   | Picbi (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Picbi\",\"Args\":[%a,%a]}" p_ireg ir1 p_ireg ir2
-  | Picbtls (n,ir1) -> fprintf oc "{\"Instruction Name\":\"Picbtls\",\"Args\":[%a,%a]}" p_int_constant n p_ireg ir1
+  | Picbtls (n,ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Picbtls\",\"Args\":[%a,%a,%a]}" p_int_constant n p_ireg ir1 p_ireg ir2
   | Pisync -> fprintf oc "{\"Instruction Name\":\"Pisync\",\"Args\":[]}"
   | Plwsync -> fprintf oc "{\"Instruction Name\":\"Plwsync\",\"Args\":[]}"
   | Plbz (ir1,c,ir2) -> fprintf oc "{\"Instruction Name\":\"Plbz\",\"Args\":[%a,%a,%a]}" p_ireg ir1 p_constant c p_ireg ir2
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 43d8fc6e..f266f3ec 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -354,9 +354,9 @@ let expand_builtin_prefetch addr rw loc =
     raise (Error "the last argument of __builtin_prefetch must be a constant between 0 and 2");
   let emit_prefetch_instr addr =
     if Int.eq rw _0 then begin
-      emit (Pdcbt (loc,addr));
+      emit (Pdcbt (loc,GPR0,addr));
     end else if Int.eq rw _1 then begin
-      emit (Pdcbtst (loc,addr));
+      emit (Pdcbtst (loc,GPR0,addr));
     end else
       raise (Error "the second argument of __builtin_prefetch must be either 0 or 1")
   in
@@ -365,13 +365,13 @@ let expand_builtin_prefetch addr rw loc =
 let expand_builtin_dcbtls addr loc =
   if not ((loc == _0) || (loc = _2)) then
     raise (Error "the second argument of __builtin_dcbtls must be a constant between 0 and 2");
-  let emit_inst addr = emit (Pdcbtls (loc,addr)) in
+  let emit_inst addr = emit (Pdcbtls (loc,GPR0,addr)) in
   expand_builtin_cache_common addr emit_inst
 
 let expand_builtin_icbtls addr loc =
   if not ((loc == _0) || (loc = _2)) then
     raise (Error "the second argument of __builtin_icbtls must be a constant between 0 and 2");
-  let emit_inst addr = emit (Picbtls (loc,addr)) in
+  let emit_inst addr = emit (Picbtls (loc,GPR0,addr)) in
   expand_builtin_cache_common addr emit_inst
 
 (* Handling of compiler-inlined builtins *)
@@ -490,6 +490,8 @@ let expand_builtin_inline name args res =
       expand_builtin_prefetch a1 rw loc
   | "__builtin_prefetch" ,_,_ ->
       raise (Error "the second and third argument of __builtin_prefetch must be a constant")
+  | "__builtin_dcbz",[BA (IR a1)],_ ->
+      emit (Pdcbz (GPR0,a1))
   (* Special registers *)
   | "__builtin_get_spr", [BA_int n], BR(IR res) ->
       emit (Pmfspr(res, n))
diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml
index 012e4d32..0785c7fa 100644
--- a/powerpc/CBuiltins.ml
+++ b/powerpc/CBuiltins.ml
@@ -100,6 +100,8 @@ let builtins = {
       (TVoid[], [TPtr (TVoid [],[]);TInt (IInt,[])],false);
     "__builtin_icbtls",
       (TVoid[], [TPtr (TVoid [],[]);TInt (IInt,[])],false);
+    "__builtin_dcbz",
+      (TVoid[], [TPtr (TVoid [],[])],false);
     (* Access to special registers *)
     "__builtin_get_spr",
       (TInt(IUInt, []), [TInt(IInt, [])], false);
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index 6a583cca..ffd01b69 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -462,12 +462,14 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	dcbf	%a, %a\n" ireg r1 ireg r2
       | Pdcbi (r1,r2) ->
           fprintf oc "	dcbi	%a, %a\n" ireg r1 ireg r2
-      | Pdcbt (c,r1) ->
-          fprintf oc "	dcbt	%ld, %a, %a\n" (camlint_of_coqint c) ireg GPR0  ireg r1
-      | Pdcbtst (c,r1) ->
-          fprintf oc "	dcbtst	%ld, %a, %a\n"  (camlint_of_coqint c) ireg GPR0 ireg r1
-      | Pdcbtls (c,r1) ->
-          fprintf oc "	dcbtls	%ld, %a, %a\n" (camlint_of_coqint c) ireg GPR0 ireg r1
+      | Pdcbt (c,r1,r2) ->
+          fprintf oc "	dcbt	%ld, %a, %a\n" (camlint_of_coqint c) ireg r1  ireg r2
+      | Pdcbtst (c,r1,r2) ->
+          fprintf oc "	dcbtst	%ld, %a, %a\n"  (camlint_of_coqint c) ireg r1 ireg r2
+      | Pdcbtls (c,r1,r2) ->
+          fprintf oc "	dcbtls	%ld, %a, %a\n" (camlint_of_coqint c) ireg r1 ireg r2
+      | Pdcbz (r1,r2) ->
+          fprintf oc "	dcbz	%a, %a\n" ireg r1 ireg r2
       | Pdivw(r1, r2, r3) ->
           fprintf oc "	divw	%a, %a, %a\n" ireg r1 ireg r2 ireg r3
       | Pdivwu(r1, r2, r3) ->
@@ -536,8 +538,8 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	fsel	%a, %a, %a, %a\n" freg r1 freg r2 freg r3 freg r4
       | Picbi (r1,r2) ->
           fprintf oc "	icbi	%a,%a\n" ireg r1 ireg r2
-      | Picbtls (n,r1) ->
-          fprintf oc "	icbtls	%ld, %a, %a\n" (camlint_of_coqint n) ireg GPR0 ireg r1
+      | Picbtls (n,r1,r2) ->
+          fprintf oc "	icbtls	%ld, %a, %a\n" (camlint_of_coqint n) ireg r1 ireg r2
       | Pisync ->
           fprintf oc "	isync\n"
       | Plwsync ->