Added builtin for the dcbi instruction.

5 files changed, 11 insertions, 4 deletions

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index 4eedfba4..f1e84146 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -161,10 +161,11 @@ Inductive instruction : Type :=
   | Pcmplwi: ireg -> constant -> instruction                  (**r same, with immediate argument *)
   | Pcmpw: ireg -> ireg -> instruction                        (**r signed integer comparison *)
   | Pcmpwi: ireg -> constant -> instruction                   (**r same, with immediate argument *)
-  | Pcntlzw: ireg -> ireg -> instruction                       (**r count leading zeros *)
+  | Pcntlzw: ireg -> ireg -> instruction                      (**r count leading zeros *)
   | Pcreqv: crbit -> crbit -> crbit -> instruction            (**r not-xor between condition bits *)
   | Pcror: crbit -> crbit -> crbit -> instruction             (**r or between condition bits *)
   | Pcrxor: crbit -> crbit -> crbit -> instruction            (**r xor between condition bits *)
+  | Pdcbi: ireg -> ireg -> instruction                        (**r data cache invalidate *)
   | Pdivw: ireg -> ireg -> ireg -> instruction                (**r signed division *)
   | Pdivwu: ireg -> ireg -> ireg -> instruction               (**r unsigned division *)
   | Peieio: instruction                                       (**r EIEIO barrier *)
@@ -858,6 +859,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pcntlzw _ _
   | Pcreqv _ _ _
   | Pcrxor _ _ _
+  | Pdcbi _ _
   | Peieio
   | Pfctiw _ _
   | Pfctiwz _ _
@@ -1064,6 +1066,4 @@ Definition data_preg (r: preg) : bool :=
   | CR0_0 => false | CR0_1 => false | CR0_2 => false | CR0_3 => false
   | CARRY => false
   | _ => true
-  end.
-
-
+  end.
\ No newline at end of file
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml
index 6419e489..81ffd500 100644
--- a/powerpc/AsmToJSON.ml
+++ b/powerpc/AsmToJSON.ml
@@ -175,6 +175,7 @@ let p_instruction oc ic =
   | Pcreqv (cr1,cr2,cr3) -> fprintf oc "{\"Instruction Name\":\"Pcreqv\",\"Args\":[%a,%a,%a]}" p_crbit cr1 p_crbit cr2 p_crbit cr3
   | Pcror (cr1,cr2,cr3) -> fprintf oc "{\"Instruction Name\":\"Pcror\",\"Args\":[%a,%a,%a]}" p_crbit cr1 p_crbit cr2 p_crbit cr3
   | Pcrxor (cr1,cr2,cr3) -> fprintf oc "{\"Instruction Name\":\"Pcrxor\",\"Args\":[%a,%a,%a]}" p_crbit cr1 p_crbit cr2 p_crbit cr3
+  | Pdcbi (ir1,ir2) -> fprintf oc "{\"Instruction Name\":\"Pdcbi\",\"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\":[]}"
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 5c4aad9d..87c0ac3e 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -424,6 +424,8 @@ let expand_builtin_inline name args res =
   | "__builtin_va_start", [IR a], _ ->
       expand_builtin_va_start a
   (* Catch-all *)
+  | "__builtin_dcbi", [IR a1],_ ->
+      emit (Pdcbi (GPR0,a1))
   | "__builtin_icbi", [IR a1],_ ->
       emit (Picbi(GPR0,a1))
   | _ ->
diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml
index 672fb719..e774614e 100644
--- a/powerpc/CBuiltins.ml
+++ b/powerpc/CBuiltins.ml
@@ -88,6 +88,8 @@ let builtins = {
     "__builtin_trap",
       (TVoid [], [], false);
     (* Cache isntructions *)
+    "__builtin_dcbi",
+      (TVoid [],[TPtr(TVoid [], [])],false);
     "__builtin_icbi",
       (TVoid [],[TPtr(TVoid [], [])],false)
   ]
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index 0ec5a3e5..cb3ce87a 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -469,6 +469,8 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	cror	%a, %a, %a\n" crbit c1 crbit c2 crbit c3
       | Pcrxor(c1, c2, c3) ->
           fprintf oc "	crxor	%a, %a, %a\n" crbit c1 crbit c2 crbit c3
+      | Pdcbi (r1,r2) ->
+          fprintf oc "	dcbi	%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) ->