Index: trunk/src/VBox/Devices/Bus/DevIommuIntel.cpp
===================================================================
--- trunk/src/VBox/Devices/Bus/DevIommuIntel.cpp	(revision 88590)
+++ trunk/src/VBox/Devices/Bus/DevIommuIntel.cpp	(revision 88591)
@@ -596,9 +596,25 @@
 
 /**
+ * Writes a 32-bit register with the exactly the supplied value.
+ *
+ * @param   pThis   The shared DMAR device state.
+ * @param   offReg  The MMIO offset of the register.
+ * @param   uReg    The 32-bit value to write.
+ */
+static void dmarRegWriteRaw32(PDMAR pThis, uint16_t offReg, uint32_t uReg)
+{
+    uint8_t idxGroup;
+    uint8_t *pabRegs = dmarRegGetGroup(pThis, offReg, sizeof(uint32_t), &idxGroup);
+    NOREF(idxGroup);
+    *(uint32_t *)(pabRegs + offReg) = uReg;
+}
+
+
+/**
  * Writes a 64-bit register with the exactly the supplied value.
  *
- * @param   pThis       The shared DMAR device state.
- * @param   offReg      The MMIO offset of the register.
- * @param   uReg        The 64-bit value to write.
+ * @param   pThis   The shared DMAR device state.
+ * @param   offReg  The MMIO offset of the register.
+ * @param   uReg    The 64-bit value to write.
  */
 static void dmarRegWriteRaw64(PDMAR pThis, uint16_t offReg, uint64_t uReg)
@@ -612,26 +628,8 @@
 
 /**
- * Writes a 32-bit register with the exactly the supplied value.
- *
- * @param   pThis       The shared DMAR device state.
- * @param   offReg      The MMIO offset of the register.
- * @param   uReg        The 32-bit value to write.
- */
-static void dmarRegWriteRaw32(PDMAR pThis, uint16_t offReg, uint32_t uReg)
-{
-    uint8_t idxGroup;
-    uint8_t *pabRegs = dmarRegGetGroup(pThis, offReg, sizeof(uint32_t), &idxGroup);
-    NOREF(idxGroup);
-    *(uint32_t *)(pabRegs + offReg) = uReg;
-}
-
-
-/**
  * Reads a 32-bit register with exactly the value it contains.
  *
- * @param   pThis       The shared DMAR device state.
- * @param   offReg      The MMIO offset of the register.
- * @param   fAndMask    The AND mask (applied first).
- * @param   fOrMask     The OR mask.
+ * @param   pThis   The shared DMAR device state.
+ * @param   offReg  The MMIO offset of the register.
  */
 static uint32_t dmarRegReadRaw32(PCDMAR pThis, uint16_t offReg)
@@ -647,6 +645,6 @@
  * Reads a 64-bit register with exactly the value it contains.
  *
- * @param   pThis       The shared DMAR device state.
- * @param   offReg      The MMIO offset of the register.
+ * @param   pThis   The shared DMAR device state.
+ * @param   offReg  The MMIO offset of the register.
  */
 static uint32_t dmarRegReadRaw64(PCDMAR pThis, uint16_t offReg)
@@ -706,4 +704,32 @@
 
 /**
+ * Writes a 32-bit register as it would be when written by software.
+ * This will preserve read-only bits, mask off reserved bits and clear RW1C bits.
+ *
+ * @returns The value that's actually written to the register.
+ * @param   pThis   The shared DMAR device state.
+ * @param   offReg  The MMIO offset of the register.
+ * @param   uReg    The 32-bit value to write.
+ */
+static uint32_t dmarRegWrite32(PDMAR pThis, uint16_t offReg, uint32_t uReg)
+{
+    /* Read current value from the 32-bit register. */
+    uint32_t uCurReg;
+    uint32_t fRwMask;
+    uint32_t fRw1cMask;
+    dmarRegReadRaw32Ex(pThis, offReg, &uCurReg, &fRwMask, &fRw1cMask);
+
+    uint32_t const fRoBits   = uCurReg & ~fRwMask;      /* Preserve current read-only and reserved bits. */
+    uint32_t const fRwBits   = uReg & fRwMask;          /* Merge newly written read/write bits. */
+    uint32_t const fRw1cBits = uReg & fRw1cMask;        /* Clear 1s written to RW1C bits. */
+    uint32_t const uNewReg   = (fRoBits | fRwBits) & ~fRw1cBits;
+
+    /* Write new value to the 32-bit register. */
+    dmarRegWriteRaw32(pThis, offReg, uNewReg);
+    return uNewReg;
+}
+
+
+/**
  * Writes a 64-bit register as it would be when written by software.
  * This will preserve read-only bits, mask off reserved bits and clear RW1C bits.
@@ -734,28 +760,13 @@
 
 /**
- * Writes a 32-bit register as it would be when written by software.
- * This will preserve read-only bits, mask off reserved bits and clear RW1C bits.
- *
- * @returns The value that's actually written to the register.
+ * Reads a 32-bit register as it would be when read by software.
+ *
+ * @returns The 32-bit register value.
  * @param   pThis   The shared DMAR device state.
  * @param   offReg  The MMIO offset of the register.
- * @param   uReg    The 32-bit value to write.
- */
-static uint32_t dmarRegWrite32(PDMAR pThis, uint16_t offReg, uint32_t uReg)
-{
-    /* Read current value from the 32-bit register. */
-    uint32_t uCurReg;
-    uint32_t fRwMask;
-    uint32_t fRw1cMask;
-    dmarRegReadRaw32Ex(pThis, offReg, &uCurReg, &fRwMask, &fRw1cMask);
-
-    uint32_t const fRoBits   = uCurReg & ~fRwMask;      /* Preserve current read-only and reserved bits. */
-    uint32_t const fRwBits   = uReg & fRwMask;          /* Merge newly written read/write bits. */
-    uint32_t const fRw1cBits = uReg & fRw1cMask;        /* Clear 1s written to RW1C bits. */
-    uint32_t const uNewReg   = (fRoBits | fRwBits) & ~fRw1cBits;
-
-    /* Write new value to the 32-bit register. */
-    dmarRegWriteRaw32(pThis, offReg, uNewReg);
-    return uNewReg;
+ */
+static uint32_t dmarRegRead32(PCDMAR pThis, uint16_t offReg)
+{
+    return dmarRegReadRaw32(pThis, offReg);
 }
 
@@ -771,17 +782,4 @@
 {
     return dmarRegReadRaw64(pThis, offReg);
-}
-
-
-/**
- * Reads a 32-bit register as it would be when read by software.
- *
- * @returns The 32-bit register value.
- * @param   pThis   The shared DMAR device state.
- * @param   offReg  The MMIO offset of the register.
- */
-static uint32_t dmarRegRead32(PCDMAR pThis, uint16_t offReg)
-{
-    return dmarRegReadRaw32(pThis, offReg);
 }
 
