aarch64 haskell+design squash: PR suggestions

Signed-off-by: Corey Lewis <[email protected]>
seL4 · Dec 17, 2024 · 52a23eb · 52a23eb
1 parent 9ac07ad
commit 52a23eb
Show file tree

Hide file tree

Showing 5 changed files with 7 additions and 4 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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.