aarch64 aspec+haskell+design: make virq depend on GIC version

Adjust accessor functions in ASpec and Haskell to be dependent on GIC version. For GIC_v3 the encoding of the virq type changes. Although all of the fields are still present, they are at different bit positions and the IRQ field is larger. Signed-off-by: Gerwin Klein <[email protected]>
seL4 · Jan 5, 2025 · 8711fdb · 8711fdb
1 parent 5a21940
commit 8711fdb
Show file tree

Hide file tree

Showing 7 changed files with 47 additions and 22 deletions.
diff --git a/spec/abstract/AARCH64/ArchInterrupt_A.thy b/spec/abstract/AARCH64/ArchInterrupt_A.thy
@@ -17,7 +17,7 @@ definition virqSetEOIIRQEN :: "virq \<Rightarrow> machine_word \<Rightarrow> vir
   "virqSetEOIIRQEN virq v \<equiv>
      if virq_type virq = 3
      then virq
-     else (virq && ~~0x80000) || ((v << 19) && 0x80000)"
+     else (virq && ~~(1 << eoiirqen_shift)) || ((v << eoiirqen_shift) && (1 << eoiirqen_shift))"
 
 definition vgic_maintenance :: "(unit,'z::state_ext) s_monad" where
   "vgic_maintenance = do

diff --git a/spec/abstract/AARCH64/VCPU_A.thy b/spec/abstract/AARCH64/VCPU_A.thy
@@ -106,20 +106,30 @@ definition
 
 text \<open>VCPU : inject IRQ\<close>
 
+(* bit position of type field in virq bitfield struct *)
+definition virq_type_shift :: nat where
+  "virq_type_shift \<equiv> if config_ARM_GIC_V3 then 62 else 28"
+
+(* bit position of eoiirqen field in virq bitfield struct *)
+definition eoiirqen_shift :: nat where
+  "eoiirqen_shift \<equiv> if config_ARM_GIC_V3 then 32+9 else 19"
+
 (* This following function does not correspond to exactly what the C does, but
    it is the value that is stored inside of lr in the vgic  *)
 definition make_virq :: "obj_ref \<Rightarrow> obj_ref \<Rightarrow> obj_ref \<Rightarrow> virq" where
   "make_virq grp prio irq \<equiv>
     let
-      groupShift = 30;
-      prioShift = 23;
-      irqPending = 1 << 28;
-      eoiirqen = 1 << 19
-    in ((grp && 1) << groupShift) || ((prio && 0x1F) << prioShift) || (irq && 0x3FF)
+      groupShift = if config_ARM_GIC_V3 then 60 else 30;
+      prioShift = if config_ARM_GIC_V3 then 48 else 23;
+      irqPending = 1 << virq_type_shift;
+      eoiirqen = 1 << eoiirqen_shift;
+      irqMask = mask (if config_ARM_GIC_V3 then 32 else 10);
+      prioMask = mask (if config_ARM_GIC_V3 then 8 else 5)
+    in ((grp && 1) << groupShift) || ((prio && prioMask) << prioShift) || (irq && irqMask)
        || irqPending || eoiirqen"
 
 definition virq_type :: "virq \<Rightarrow> nat" where
-  "virq_type virq \<equiv> unat ((virq >> 28) && 3)"
+  "virq_type virq \<equiv> unat ((virq >> virq_type_shift) && 3)"
 
 definition is_virq_active :: "virq \<Rightarrow> bool" where
   "is_virq_active virq \<equiv> virq_type virq = 2"

diff --git a/spec/design/skel/AARCH64/ArchHypervisor_H.thy b/spec/design/skel/AARCH64/ArchHypervisor_H.thy
@@ -18,9 +18,9 @@ begin
 context Arch begin arch_global_naming (H)
 
 #INCLUDE_HASKELL SEL4/Object/VCPU/AARCH64.hs CONTEXT AARCH64_H decls_only \
-  ONLY countTrailingZeros irqVPPIEventIndex
+  ONLY countTrailingZeros irqVPPIEventIndex virqTypeShift eoiirqenShift
 #INCLUDE_HASKELL SEL4/Object/VCPU/AARCH64.hs CONTEXT AARCH64_H bodies_only \
-  ONLY countTrailingZeros irqVPPIEventIndex
+  ONLY countTrailingZeros irqVPPIEventIndex virqTypeShift eoiirqenShift
 #INCLUDE_HASKELL SEL4/Object/VCPU/AARCH64.hs CONTEXT AARCH64_H ArchInv=Arch \
   ONLY vcpuUpdate vgicUpdate vgicUpdateLR vcpuSaveReg vcpuRestoreReg \
     vcpuSaveRegRange vcpuRestoreRegRange vcpuWriteReg vcpuReadReg saveVirtTimer \

diff --git a/spec/design/skel/AARCH64/Hardware_H.thy b/spec/design/skel/AARCH64/Hardware_H.thy
@@ -37,7 +37,9 @@ context Arch begin arch_global_naming (H)
   enableFpuEL01 \
   getFAR getDFSR getIFSR getHSR setHCR getESR  getSCTLR setSCTLR \
   addressTranslateS1 \
-  readVCPUHardwareReg writeVCPUHardwareReg vcpuBits
+  readVCPUHardwareReg writeVCPUHardwareReg vcpuBits \
+  config_DISABLE_WFI_WFE_TRAPS \
+  config_ARM_GIC_V3
 
 end
 

diff --git a/spec/design/skel/AARCH64/VCPU_H.thy b/spec/design/skel/AARCH64/VCPU_H.thy
@@ -22,8 +22,8 @@ context Arch begin arch_global_naming (H)
     vcpuSaveRegRange vcpuRestoreRegRange vcpuWriteReg vcpuReadReg saveVirtTimer \
     restoreVirtTimer vcpuDisable vcpuEnable vcpuRestore vcpuSave vcpuSwitch \
     vcpuInvalidateActive vcpuCleanInvalidateActive countTrailingZeros virqType \
-    virqSetEOIIRQEN vgicMaintenance vppiEvent irqVPPIEventIndex armvVCPUSave \
-    curVCPUActive
+    virqTypeShift eoiirqenShift virqSetEOIIRQEN vgicMaintenance vppiEvent \
+    irqVPPIEventIndex armvVCPUSave curVCPUActive
 
 end
 end
diff --git a/spec/haskell/src/SEL4/Machine/Hardware/AARCH64.hs b/spec/haskell/src/SEL4/Machine/Hardware/AARCH64.hs
@@ -464,12 +464,16 @@ vgicHCREN = (0x1 :: Word32) -- VGIC_HCR_EN
 gicVCPUMaxNumLR = (64 :: Int)
 
 
-{- Config parameter -}
+{- Config parameters -}
 
 -- The size of the physical address space in hyp mode can be configured on some platforms.
 config_ARM_PA_SIZE_BITS_40 :: Bool
 config_ARM_PA_SIZE_BITS_40 = error "generated from CMake config"
 
--- Wether to trap WFI/WFE instructions or not in hyp mode
+-- Whether to trap WFI/WFE instructions or not in hyp mode.
 config_DISABLE_WFI_WFE_TRAPS :: Bool
 config_DISABLE_WFI_WFE_TRAPS = error "generated from CMake config"
+
+-- Whether to use the GICv3. Defaults to GICv2 when set to False.
+config_ARM_GIC_V3 :: Bool
+config_ARM_GIC_V3 = error "generated from CMake config"
diff --git a/spec/haskell/src/SEL4/Object/VCPU/AARCH64.hs b/spec/haskell/src/SEL4/Object/VCPU/AARCH64.hs
@@ -206,18 +206,26 @@ invokeVCPUWriteReg vcpuPtr reg val = do
 
 {- VCPU: inject IRQ -}
 
+-- bit position of type field in virq bitfield struct
+virqTypeShift = if config_ARM_GIC_V3 then 62 else 28
+
+-- bit position of eoiirqen field in virq bitfield struct
+eoiirqenShift = if config_ARM_GIC_V3 then 32+9 else 19
+
 -- analogous to virq_virq_pending_new in C, with virqEOIIRQEN set
 makeVIRQ :: Word -> Word -> Word -> VIRQ
 makeVIRQ grp prio irq =
-    ((grp .&. 1) `shiftL` groupShift) .|. ((prio .&. 0x1F) `shiftL` prioShift) .|.
-    (irq .&. 0x3FF) .|. irqPending .|. eoiirqen
-    where groupShift = 30
-          prioShift = 23
-          irqPending = bit 28
-          eoiirqen = bit 19
+    ((grp .&. 1) `shiftL` groupShift) .|.((prio .&. prioMask) `shiftL` prioShift) .|.
+    (irq .&. irqMask) .|. irqPending .|. eoiirqen
+    where groupShift = if config_ARM_GIC_V3 then 60 else 30
+          prioShift = if config_ARM_GIC_V3 then 48 else 23
+          irqPending = bit virqTypeShift
+          eoiirqen = bit eoiirqenShift
+          irqMask = mask (if config_ARM_GIC_V3 then 32 else 10)
+          prioMask = mask (if config_ARM_GIC_V3 then 8 else 5)
 
 virqType :: Word -> Int
-virqType virq = fromIntegral $ (virq `shiftR` 28) .&. 3
+virqType virq = fromIntegral $ (virq `shiftR` virqTypeShift) .&. 3
 
 -- combination of virq_get_virqType and virq_virq_active
 isVIRQActive :: VIRQ -> Bool
@@ -229,7 +237,8 @@ virqSetEOIIRQEN :: VIRQ -> Word -> VIRQ
 virqSetEOIIRQEN virq v =
     if virqType virq == 3
     then virq
-    else (virq .&. complement 0x80000) .|. ((v `shiftL` 19) .&. 0x80000)
+    else (virq .&. complement (bit eoiirqenShift)) .|.
+         ((v `shiftL` eoiirqenShift) .&. bit eoiirqenShift)
 
 decodeVCPUInjectIRQ :: [Word] -> ArchCapability ->
         KernelF SyscallError ArchInv.Invocation