From 7fe3c745283dcfd7cd304bca68ae2cc3ea7cd4a5 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Mon, 17 Aug 2015 16:11:47 +0200
Subject: Added builtin for the dcbf instruction

---
 powerpc/Asm.v            | 2 ++
 powerpc/AsmToJSON.ml     | 1 +
 powerpc/Asmexpand.ml     | 2 ++
 powerpc/CBuiltins.ml     | 2 ++
 powerpc/TargetPrinter.ml | 2 ++
 5 files changed, 9 insertions(+)

(limited to 'powerpc')

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index f1e84146..b7656dc4 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -165,6 +165,7 @@ Inductive instruction : Type :=
   | 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 *)
+  | Pdcbf: ireg -> ireg -> instruction                        (**r data cache flush *)
   | Pdcbi: ireg -> ireg -> instruction                        (**r data cache invalidate *)
   | Pdivw: ireg -> ireg -> ireg -> instruction                (**r signed division *)
   | Pdivwu: ireg -> ireg -> ireg -> instruction               (**r unsigned division *)
@@ -859,6 +860,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pcntlzw _ _
   | Pcreqv _ _ _
   | Pcrxor _ _ _
+  | Pdcbf _ _
   | Pdcbi _ _
   | Peieio
   | Pfctiw _ _
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml
index 81ffd500..d66dd163 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
+  | 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
   | 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
diff --git a/powerpc/Asmexpand.ml b/powerpc/Asmexpand.ml
index 976f4e77..ae4d694a 100644
--- a/powerpc/Asmexpand.ml
+++ b/powerpc/Asmexpand.ml
@@ -394,6 +394,8 @@ let expand_builtin_inline name args res =
   | "__builtin_va_start", [IR a], _ ->
       expand_builtin_va_start a
   (* Catch-all *)
+  | "__builtin_dcbf", [IR a1],_ ->
+      emit (Pdcbf (GPR0,a1))
   | "__builtin_dcbi", [IR a1],_ ->
       emit (Pdcbi (GPR0,a1))
   | "__builtin_icbi", [IR a1],_ ->
diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml
index e774614e..06a7e395 100644
--- a/powerpc/CBuiltins.ml
+++ b/powerpc/CBuiltins.ml
@@ -88,6 +88,8 @@ let builtins = {
     "__builtin_trap",
       (TVoid [], [], false);
     (* Cache isntructions *)
+    "__builtin_dcbf",
+      (TVoid [],[TPtr(TVoid [], [])],false);
     "__builtin_dcbi",
       (TVoid [],[TPtr(TVoid [], [])],false);
     "__builtin_icbi",
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index cb3ce87a..8610f750 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
+      | Pdcbf (r1,r2) ->
+          fprintf oc "	dcbf	%a, %a\n" ireg r1 ireg r2
       | Pdcbi (r1,r2) ->
           fprintf oc "	dcbi	%a, %a\n" ireg r1 ireg r2
       | Pdivw(r1, r2, r3) ->
-- 
cgit