5 files changed, 10 insertions, 93 deletions
diff --git a/src/include/kernel/console.H b/src/include/kernel/console.H
index e12f66a62..964882a66 100644
--- a/src/include/kernel/console.H
+++ b/src/include/kernel/console.H
@@ -3,8 +3,9 @@
 
 #include <stdint.h>
 #include <string.h>
+#include <builtins.h>
 
-void printk(const char*, ...)  __attribute__((format (printf, 1, 2)));
+void printk(const char*, ...) FORMAT_PRINTF;
 
 class Console
 {
diff --git a/src/include/kernel/cpu.H b/src/include/kernel/cpu.H
index 81b43a57c..2f012700c 100644
--- a/src/include/kernel/cpu.H
+++ b/src/include/kernel/cpu.H
@@ -2,7 +2,8 @@
 #define __KERNEL_CPU_H
 
 #include <kernel/types.h>
-#include <kernel/ppcarch.H>
+#include <arch/ppc.H>
+#include <builtins.h>
 
 // Thread ID support only, Power7 (4 threads).
 #define KERNEL_MAX_SUPPORTED_CPUS 4
@@ -18,10 +19,10 @@ struct cpu_t
     task_t* idle_task;
 };
 
-__attribute__((always_inline))
+ALWAYS_INLINE
 inline uint64_t getCpuId()
 {
-    return ppc_getPIR() & (KERNEL_MAX_SUPPORTED_CPUS - 1);
+    return getPIR() & (KERNEL_MAX_SUPPORTED_CPUS - 1);
 }
 
 #endif
diff --git a/src/include/kernel/ppcarch.H b/src/include/kernel/ppcarch.H
deleted file mode 100644
index 3d34bf888..000000000
--- a/src/include/kernel/ppcarch.H
+++ /dev/null
@@ -1,87 +0,0 @@
-#ifndef __KERNEL_PPCARCH_H
-#define __KERNEL_PPCARCH_H
-
-#include <kernel/types.h>
-
-__attribute__((always_inline))
-inline uint64_t ppc_getSRR1() 
-{
-    register uint64_t srr1 = 0;
-    asm volatile("mfsrr1 %0" : "=r" (srr1));
-    return srr1;
-} 
-
-__attribute__((always_inline))
-inline uint64_t ppc_getPVR() 
-{
-    register uint64_t pvr = 0;
-    asm volatile("mfspr %0, 287" : "=r" (pvr));
-    return pvr;
-}
-
-__attribute__((always_inline))
-inline uint64_t ppc_getPIR() 
-{
-    register uint64_t pir = 0;
-    asm volatile("mfspr %0, 1023" : "=r" (pir));
-    return pir;
-}
-
-__attribute__((always_inline))
-inline uint64_t ppc_getSPRG3()
-{
-    register uint64_t sprg3 = 0;
-    asm volatile("mfsprg3 %0" : "=r" (sprg3));
-    return sprg3;
-}
-
-__attribute__((always_inline))
-inline void ppc_setSPRG3(uint64_t _sprg3)
-{
-    register uint64_t sprg3 = _sprg3;
-    asm volatile("mtsprg3 %0" : : "r" (sprg3));
-    return;
-}
-
-__attribute__((always_inline))
-inline uint64_t ppc_getMSR()
-{
-    register uint64_t msr = 0;
-    asm volatile("mfmsr %0" : "=r" (msr));
-    return msr;
-}
-
-__attribute__((always_inline))
-inline void ppc_setMSR(uint64_t _msr)
-{
-    register uint64_t msr = _msr;
-    asm volatile("mtmsr %0; isync" :: "r" (msr));
-}
-
-__attribute__((always_inline))
-inline uint64_t ppc_getDSISR()
-{
-    register uint64_t dsisr = 0;
-    asm volatile("mfspr %0, 18" : "=r" (dsisr));
-    return dsisr;
-}
-
-__attribute__((always_inline))
-inline uint64_t ppc_getDAR()
-{
-    register uint64_t dar = 0;
-    asm volatile("mfspr %0, 19" : "=r" (dar));
-    return dar;
-}
-
-__attribute__((always_inline))
-inline uint64_t ppc_getTB()
-{
-    register uint64_t tb = 0;
-    asm volatile("mfspr %0, 268" : "=r" (tb));
-    return tb;
-}
-
-
-
-#endif
diff --git a/src/include/kernel/ppcconsts.S b/src/include/kernel/ppcconsts.S
index 0c5e1dc3d..be7162b88 100644
--- a/src/include/kernel/ppcconsts.S
+++ b/src/include/kernel/ppcconsts.S
@@ -86,6 +86,8 @@
                 .set SDR1,25
                 .set SRR0,26
                 .set SRR1,27
+                .set HSRR0,314
+                .set HSRR1,315
                 .set SPRG0,272
                 .set SPRG1,273
                 .set SPRG2,274
diff --git a/src/include/kernel/timemgr.H b/src/include/kernel/timemgr.H
index 78de82216..acd4361c2 100644
--- a/src/include/kernel/timemgr.H
+++ b/src/include/kernel/timemgr.H
@@ -2,7 +2,7 @@
 #define __KERNEL_TIMEMGR_H
 
 #include <kernel/types.h>
-#include <kernel/ppcarch.H>
+#include <arch/ppc.H>
 
 #include <util/locked/pqueue.H>
 #include <kernel/spinlock.H>
@@ -33,7 +33,7 @@ class TimeManager
 
 	static uint64_t getCurrentTimeBase()
 	    {
-		return ppc_getTB();
+		return getTB();
 	    };
 
 	static uint64_t convertSecToTicks(uint64_t i_sec, uint64_t i_nsec);