DONT_TRANSLATE more inline asm functions.

The c-parser can now parse these functions, but it does it by
discarding the inline ASM block, creating a misleading and likely
malformed function body. It is better to not translate these
with a DONT_TRANSLATE comment.

This change has been made for the current verification platform
only, and should probably be extended to any other verification
targets as necessary.

include/arch/arm/arch/machine.h

@@ -62,6 +62,7 @@ void setNextPC(tcb_t *thread, word_t v);
 /* Architecture specific machine operations */
 
 /** MODIFIES: [*] */
+/** DONT_TRANSLATE */
 static inline uint32_t getProcessorID(void)
 {
     uint32_t processor_id;
@@ -69,6 +70,7 @@ static inline uint32_t getProcessorID(void)
     return processor_id;
 }
 
+/** DONT_TRANSLATE */
 static inline uint32_t readSystemControlRegister(void)
 {
     uint32_t scr;
@@ -76,11 +78,13 @@ static inline uint32_t readSystemControlRegister(void)
     return scr;
 }
 
+/** DONT_TRANSLATE */
 static inline void writeSystemControlRegister(uint32_t scr)
 {
     MCR("p15, 0, %0, c1, c0, 0", scr);
 }
 
+/** DONT_TRANSLATE */
 static inline uint32_t readAuxiliaryControlRegister(void)
 {
     uint32_t acr;
@@ -88,12 +92,14 @@ static inline uint32_t readAuxiliaryControlRegister(void)
     return acr;
 }
 
+/** DONT_TRANSLATE */
 static inline void writeAuxiliaryControlRegister(uint32_t acr)
 {
     MCR("p15, 0, %0, c1, c0, 1", acr);
 }
 
 /** MODIFIES: [*] */
+/** DONT_TRANSLATE */
 static inline void clearExMonitor(void)
 {
     word_t tmp;
@@ -101,12 +107,14 @@ static inline void clearExMonitor(void)
 }
 
 /** MODIFIES: [*] */
+/** DONT_TRANSLATE */
 static inline void flushBTAC(void)
 {
     asm volatile("mcr p15, 0, %0, c7, c5, 6" : : "r"(0));
 }
 
 /** MODIFIES: [*] */
+/** DONT_TRANSLATE */
 static inline void writeContextID(word_t id)
 {
     asm volatile("mcr p15, 0, %0, c13, c0, 1" : : "r"(id));
@@ -118,6 +126,7 @@ void setHardwareASID(hw_asid_t hw_asid);
 
 /* Address space control */
 /** MODIFIES: [*] */
+/** DONT_TRANSLATE */
 static inline void setCurrentPD(paddr_t addr)
 {
     /* Mask supplied address (retain top 19 bits).  Set the lookup cache bits:
@@ -131,6 +140,7 @@ static inline void setCurrentPD(paddr_t addr)
 
 /* TLB control */
 /** MODIFIES: [*] */
+/** DONT_TRANSLATE */
 static inline void invalidateTLB(void)
 {
     dsb();
@@ -139,6 +149,7 @@ static inline void invalidateTLB(void)
     isb();
 }
 /** MODIFIES: [*] */
+/** DONT_TRANSLATE */
 static inline void invalidateTLB_ASID(hw_asid_t hw_asid)
 {
     dsb();
@@ -147,6 +158,7 @@ static inline void invalidateTLB_ASID(hw_asid_t hw_asid)
     isb();
 }
 /** MODIFIES: [*] */
+/** DONT_TRANSLATE */
 static inline void invalidateTLB_VAASID(word_t mva_plus_asid)
 {
     dsb();
@@ -158,6 +170,7 @@ static inline void invalidateTLB_VAASID(word_t mva_plus_asid)
 void lockTLBEntry(vptr_t vaddr);
 
 /** MODIFIES: [*] */
+/** DONT_TRANSLATE */
 static inline void cleanByVA(vptr_t vaddr, paddr_t paddr)
 {
 #ifdef ARM_CORTEX_A8
@@ -194,6 +207,7 @@ static inline void cleanByVA_PoU(vptr_t vaddr, paddr_t paddr)
 }
 /* D-Cache invalidate to PoC (v6/v7 common) */
 /** MODIFIES: [*] */
+/** DONT_TRANSLATE */
 static inline void invalidateByVA(vptr_t vaddr, paddr_t paddr)
 {
 #ifdef ARM_CORTEX_A8
@@ -206,6 +220,7 @@ static inline void invalidateByVA(vptr_t vaddr, paddr_t paddr)
     dmb();
 }
 /** MODIFIES: [*] */
+/** DONT_TRANSLATE */
 /* I-Cache invalidate to PoU (L2 cache) (v6/v7 common) */
 static inline void invalidateByVA_I(vptr_t vaddr, paddr_t paddr)
 {
@@ -218,6 +233,7 @@ static inline void invalidateByVA_I(vptr_t vaddr, paddr_t paddr)
     isb();
 }
 /** MODIFIES: [*] */
+/** DONT_TRANSLATE */
 /* I-Cache invalidate all to PoU (L2 cache) (v6/v7 common) */
 static inline void invalidate_I_PoU(void)
 {
@@ -229,6 +245,7 @@ static inline void invalidate_I_PoU(void)
     isb();
 }
 /** MODIFIES: [*] */
+/** DONT_TRANSLATE */
 /* D-Cache clean & invalidate to PoC (v6/v7 common) */
 static inline void cleanInvalByVA(vptr_t vaddr, paddr_t paddr)
 {
@@ -244,6 +261,7 @@ static inline void cleanInvalByVA(vptr_t vaddr, paddr_t paddr)
     dsb();
 }
 /** MODIFIES: [*] */
+/** DONT_TRANSLATE */
 /* Invalidate branch predictors by VA (v6/v7 common) */
 static inline void branchFlush(vptr_t vaddr, paddr_t paddr)
 {
@@ -274,6 +292,7 @@ void cleanInvalidateL1Caches(void);
 
 /* Fault status */
 /** MODIFIES: */
+/** DONT_TRANSLATE */
 static inline word_t PURE getIFSR(void)
 {
     word_t IFSR;
@@ -281,6 +300,7 @@ static inline word_t PURE getIFSR(void)
     return IFSR;
 }
 /** MODIFIES: */
+/** DONT_TRANSLATE */
 static inline word_t PURE getDFSR(void)
 {
     word_t DFSR;
@@ -288,6 +308,7 @@ static inline word_t PURE getDFSR(void)
     return DFSR;
 }
 /** MODIFIES: */
+/** DONT_TRANSLATE */
 static inline word_t PURE getFAR(void)
 {
     word_t FAR;

include/arch/arm/armv/armv6/armv/fastpath.h

@@ -17,6 +17,7 @@
 #include <plat/machine/hardware.h>
 #include <arch/machine.h>
 
+/** DONT_TRANSLATE */
 static inline void dsb_fp(void)
 {
     /*
@@ -31,6 +32,7 @@ static inline void dsb_fp(void)
 }
 
 /* Change the translation root by updating TTBR0. */
+/** DONT_TRANSLATE */
 static inline void
 setCurrentPD_fp(word_t pd_addr)
 {
@@ -43,6 +45,7 @@ setCurrentPD_fp(word_t pd_addr)
 }
 
 /* Change the current hardware ASID. */
+/** DONT_TRANSLATE */
 static inline void
 setHardwareASID_fp(hw_asid_t asid)
 {

include/arch/arm/armv/armv6/armv/machine.h

@@ -12,18 +12,21 @@
 #define __ARCH_ARMV6_MACHINE_H
 
 /** MODIFIES: [*] */
+/** DONT_TRANSLATE */
 static inline void dsb(void)
 {
     asm volatile("mcr p15, 0, %0, c7, c10, 4" : : "r"(0) : "memory");
 }
 
 /** MODIFIES: [*] */
+/** DONT_TRANSLATE */
 static inline void dmb(void)
 {
     asm volatile("mcr p15, 0, %0, c7, c10, 5" : : "r"(0) : "memory");
 }
 
 /** MODIFIES: [*] */
+/** DONT_TRANSLATE */
 static inline void isb(void)
 {
     asm volatile("mcr p15, 0, %0, c7, c5, 4" : : "r"(0) : "memory");

src/arch/arm/armv/armv6/cache.c

@@ -10,6 +10,7 @@
 
 #include <arch/machine/hardware.h>
 
+/** DONT_TRANSLATE */
 void
 clean_D_PoU(void)
 {
@@ -17,6 +18,7 @@ clean_D_PoU(void)
     asm volatile("mcr p15, 0, %0, c7, c10, 0" : : "r"(0));
 }
 
+/** DONT_TRANSLATE */
 void
 cleanInvalidate_D_PoC(void)
 {

src/arch/arm/fastpath/fastpath.c

@@ -75,6 +75,7 @@ lookup_fp(cap_t cap, cptr_t cptr)
     return cap;
 }
 
+/** DONT_TRANSLATE */
 static inline void
 clearExMonitor_fp(void)
 {