diff --git a/spec/haskell/src/SEL4/Object/FPU/AARCH64.hs b/spec/haskell/src/SEL4/Object/FPU/AARCH64.hs index ac4a4266f1..0165f78034 100644 --- a/spec/haskell/src/SEL4/Object/FPU/AARCH64.hs +++ b/spec/haskell/src/SEL4/Object/FPU/AARCH64.hs @@ -47,7 +47,7 @@ fpuRelease tcbPtr = do lazyFpuRestore :: PPtr TCB -> Kernel () lazyFpuRestore tcbPtr = do flags <- threadGet tcbFlags tcbPtr - if (tcbFlagToWord (ArchFlag FpuDisabled) .&. flags /= 0) + if (isFlagSet (ArchFlag FpuDisabled) flags) then doMachineOp disableFpu else do doMachineOp enableFpu diff --git a/spec/haskell/src/SEL4/Object/FPU/X64.hs b/spec/haskell/src/SEL4/Object/FPU/X64.hs index 10368c1051..9a4aeed494 100644 --- a/spec/haskell/src/SEL4/Object/FPU/X64.hs +++ b/spec/haskell/src/SEL4/Object/FPU/X64.hs @@ -47,7 +47,7 @@ fpuRelease tcbPtr = do lazyFpuRestore :: PPtr TCB -> Kernel () lazyFpuRestore tcbPtr = do flags <- threadGet tcbFlags tcbPtr - if (tcbFlagToWord (ArchFlag FpuDisabled) .&. flags /= 0) + if (isFlagSet (ArchFlag FpuDisabled) flags) then doMachineOp disableFpu else do doMachineOp enableFpu diff --git a/spec/haskell/src/SEL4/Object/Structures.lhs b/spec/haskell/src/SEL4/Object/Structures.lhs index 5cd0c0eefe..7fde732c62 100644 --- a/spec/haskell/src/SEL4/Object/Structures.lhs +++ b/spec/haskell/src/SEL4/Object/Structures.lhs @@ -508,3 +508,6 @@ Various operations on the free index of an Untyped cap. > tcbFlagToWord :: TcbFlag -> Word > tcbFlagToWord NoFlag = 0x0 > tcbFlagToWord (ArchFlag archFlag) = archTcbFlagToWord archFlag + +> isFlagSet :: TcbFlag -> TcbFlags -> Bool +> isFlagSet flag flags = tcbFlagToWord flag .&. flags /= 0 diff --git a/spec/haskell/src/SEL4/Object/TCB/AARCH64.hs b/spec/haskell/src/SEL4/Object/TCB/AARCH64.hs index 805ab06d3d..f77eaba7e2 100644 --- a/spec/haskell/src/SEL4/Object/TCB/AARCH64.hs +++ b/spec/haskell/src/SEL4/Object/TCB/AARCH64.hs @@ -56,7 +56,7 @@ postModifyRegisters _ _ = return () postSetFlags :: PPtr TCB -> TcbFlags -> Kernel () postSetFlags t flags = - when (tcbFlagToWord (ArchFlag FpuDisabled) .&. flags /= 0) (fpuRelease t) + when (isFlagSet (ArchFlag FpuDisabled) flags) (fpuRelease t) -- Save and clear FPU state before setting the domain of a TCB, to ensure that -- we do not later write to cross-domain state. diff --git a/spec/haskell/src/SEL4/Object/TCB/X64.lhs b/spec/haskell/src/SEL4/Object/TCB/X64.lhs index 3528f9b810..b60fe3fa86 100644 --- a/spec/haskell/src/SEL4/Object/TCB/X64.lhs +++ b/spec/haskell/src/SEL4/Object/TCB/X64.lhs @@ -64,7 +64,7 @@ Here, cur = ksCurThread > postSetFlags :: PPtr TCB -> TcbFlags -> Kernel () > postSetFlags t flags = -> when (tcbFlagToWord (ArchFlag FpuDisabled) .&. flags /= 0) (fpuRelease t) +> when (isFlagSet (ArchFlag FpuDisabled) flags) (fpuRelease t) Save and clear FPU state before setting the domain of a TCB, to ensure that we do not later write to cross-domain state.