adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

aarch64 haskell: simplify checkIRQ 

We are on an Arm board, where <= maxIRQ implies != irqInvalid, so use
original ARM version.

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
This commit is contained in:
Rafal Kolanski 2022-02-09 15:51:37 +11:00 committed by Gerwin Klein
parent 103d7cfa12
commit 92745f3e5b
1 changed files with 4 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
spec/haskell/src/SEL4/Object/Interrupt/AARCH64.hs
View File

@ -81,7 +81,8 @@ maskIrqSignal _ = return ()
initInterruptController :: Kernel ()
initInterruptController = error "Unimplemented. Init code."
-- This check takes a different form on architectures where the invalid IRQ is
-- in the [minIRQ,maxIRQ] range. On Arm platforms, irqInvalid is outside
-- that range, hence the rangeCheck implicitly checks for irqInvalid
checkIRQ :: Word -> KernelF SyscallError ()
checkIRQ irqW = when (irqW > fromIntegral (fromEnum maxIRQ) ||
irqW == fromIntegral (fromEnum irqInvalid)) $
throw $ RangeError 1 (fromIntegral (fromEnum maxIRQ))
checkIRQ irq = rangeCheck irq (fromEnum minIRQ) (fromEnum maxIRQ)