From c6e03d61ee776aacc859fd162e47cb7ba0fb3079 Mon Sep 17 00:00:00 2001
From: Bernhard Schommer <bernhardschommer@gmail.com>
Date: Fri, 14 Aug 2015 16:30:02 +0200
Subject: Added builitin for the icbi instruction.

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

(limited to 'powerpc')

diff --git a/powerpc/Asm.v b/powerpc/Asm.v
index cd4c8d00..4eedfba4 100644
--- a/powerpc/Asm.v
+++ b/powerpc/Asm.v
@@ -201,6 +201,7 @@ Inductive instruction : Type :=
   | Pfres: freg -> freg -> instruction                        (**r approximate inverse *)
   | Pfsel: freg -> freg -> freg -> freg -> instruction        (**r FP conditional move *)
   | Pisync: instruction                                       (**r ISYNC barrier *)
+  | Picbi: ireg -> ireg -> instruction                        (**r instruction cache invalidate *)
   | 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 *)
@@ -870,6 +871,7 @@ Definition exec_instr (f: function) (i: instruction) (rs: regset) (m: mem) : out
   | Pfsel _ _ _ _
   | Plwarx _ _ _
   | Plwbrx _ _ _
+  | Picbi _ _
   | Pisync
   | Plwsync
   | Plhbrx _ _ _
diff --git a/powerpc/AsmToJSON.ml b/powerpc/AsmToJSON.ml
index ea627b9b..6419e489 100644
--- a/powerpc/AsmToJSON.ml
+++ b/powerpc/AsmToJSON.ml
@@ -210,6 +210,7 @@ let p_instruction oc ic =
   | Pfrsqrte (fr1,fr2) -> fprintf oc "{\"Instruction Name\":\"Pfsqrte\",\"Args\":[%a,%a]}" p_freg fr1 p_freg fr2
   | 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
   | 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 487aaaae..5c4aad9d 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_icbi", [IR a1],_ ->
+      emit (Picbi(GPR0,a1))
   | _ ->
       invalid_arg ("unrecognized builtin " ^ name)
 
diff --git a/powerpc/CBuiltins.ml b/powerpc/CBuiltins.ml
index f1f57644..672fb719 100644
--- a/powerpc/CBuiltins.ml
+++ b/powerpc/CBuiltins.ml
@@ -86,7 +86,10 @@ let builtins = {
     "__builtin_lwsync",
       (TVoid [], [], false);
     "__builtin_trap",
-      (TVoid [], [], false)
+      (TVoid [], [], false);
+    (* Cache isntructions *)
+    "__builtin_icbi",
+      (TVoid [],[TPtr(TVoid [], [])],false)
   ]
 }
 
diff --git a/powerpc/TargetPrinter.ml b/powerpc/TargetPrinter.ml
index cffb4496..0ec5a3e5 100644
--- a/powerpc/TargetPrinter.ml
+++ b/powerpc/TargetPrinter.ml
@@ -535,6 +535,8 @@ module Target (System : SYSTEM):TARGET =
           fprintf oc "	fres	%a, %a\n" freg r1 freg r2    
       | Pfsel(r1, r2, r3, r4) ->
           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
       | Pisync ->
           fprintf oc "	isync\n"
       | Plwsync ->
-- 
cgit