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

arm-hyp haskell: check idx earlier in vgicMaintenance to avoid C overflow

This commit is contained in:
Gerwin Klein 2017-04-29 22:09:57 +10:00 committed by Alejandro Gomez-Londono
parent cb35836c7b
commit e76a15d71d
1 changed files with 6 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
spec/haskell/src/SEL4/Object/VCPU/ARM_HYP.lhs
View File

@ -314,17 +314,17 @@ For initialisation, see makeVCPUObject.
> eisr1 <- doMachineOp $ get_gic_vcpu_ctrl_eisr1
> flags <- doMachineOp $ get_gic_vcpu_ctrl_misr
> let vgic_misr_eoi = 1 -- defined to be VGIC_HCR_EN
> let irq_idx = irqIndex eisr0 eisr1
>
> gic_vcpu_num_list_regs <- gets (armKSGICVCPUNumListRegs . ksArchState)
> fault <-
> if (flags .&. vgic_misr_eoi /= 0)
> then
> if (eisr0 == 0 && eisr1 == 0) -- irq_idx invalid
> if (eisr0 == 0 && eisr1 == 0 ||
> irq_idx >= gic_vcpu_num_list_regs) -- irq_idx invalid
> then return $ VGICMaintenance Nothing
> else (do
> let irq_idx = irqIndex eisr0 eisr1
> gic_vcpu_num_list_regs <-
> gets (armKSGICVCPUNumListRegs . ksArchState)
> when (irq_idx < gic_vcpu_num_list_regs) (badIndex irq_idx)
> setIndex irq_idx
> return $ VGICMaintenance $ Just $ fromIntegral irq_idx
> )
> else return $ VGICMaintenance Nothing
@ -336,7 +336,7 @@ For initialisation, see makeVCPUObject.
> irqIndex eisr0 eisr1 =
> if eisr0 /= 0 then countTrailingZeros eisr0
> else (countTrailingZeros eisr1) + 32
> badIndex irq_idx = doMachineOp $ (do
> setIndex irq_idx = doMachineOp $ (do
> virq <- get_gic_vcpu_ctrl_lr (fromIntegral irq_idx)
> set_gic_vcpu_ctrl_lr (fromIntegral irq_idx) $ virqSetEOIIRQEN virq 0
> )