aarch64 haskell: add simplified FPU

Adds FPU state to UserContext, uses 64 general-purpose registers as seen
on TX2.
Abstracts FPU operations to fpuThreadDelete required for thread
deletion, thereby not including intricacies of lazy FPU switching.

Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>

spec/haskell/src/SEL4/Machine/Hardware/AARCH64.hs

@@ -327,3 +327,8 @@ read_stval = error "Unimplemented - machine op"
 
 plic_complete_claim :: IRQ -> MachineMonad ()
 plic_complete_claim = error "Unimplemented - machine op"
+
+{- FPU Operations -}
+
+fpuThreadDeleteOp :: Word -> MachineMonad ()
+fpuThreadDeleteOp tcbPtr = error "Unimplemented callback"

spec/haskell/src/SEL4/Machine/RegisterSet/AARCH64.hs

@@ -73,21 +73,34 @@ nextInstructionRegister = NextIP
 
 {- User-level Context -}
 
--- On RISC-V the representation of the user-level context of a thread is an array
--- of machine words, indexed by register name for the user registers.
+-- The FPU state consists of an array of 64 general registers, as well as special
+-- registers. We use an array for the general registers, with the convention that
+-- all unused entries map to 0.
+data FPUState = FPUState { fpuRegs :: Array Int Data.Word.Word64
+                         , fpuSr :: Data.Word.Word32
+                         , fpuCr :: Data.Word.Word32 }
+  deriving Show
 
-data UserContext = UC { fromUC :: Array Register Word }
+-- The representation of the user-level context of a thread is an array of
+-- machine words, indexed by register name for the user registers, plus the
+-- state of the FPU. There are no operations on the FPU state apart from save
+-- and restore at kernel entry and exit.
+data UserContext = UC { fromUC :: Array Register Word,
+                        fpuState :: FPUState }
   deriving Show
 
 -- A new user-level context is a list of values for the machine's registers.
 -- Registers are generally initialised to 0, but there may be machine-specific
--- initial values for certain registers.
+-- initial values for certain registers. The FPU state is zeroed.
+
+newFPUState :: FPUState
+newFPUState = FPUState (funPartialArray (const 0) (0,63)) 0 0
 
 newContext :: UserContext
-newContext = UC $ (funArray $ const 0)//initContext
+newContext = UC ((funArray $ const 0)//initContext) newFPUState
 
 -- Functions are provided to get and set a single register.
 
 getRegister r = gets $ (!r) . fromUC
 
-setRegister r v = modify $ UC . (//[(r, v)]) . fromUC
+setRegister r v = modify (\ uc -> UC (fromUC uc //[(r, v)]) (fpuState uc))

spec/haskell/src/SEL4/Object/ObjectType/AARCH64.hs

@@ -207,7 +207,11 @@ capUntypedSize (PageTableCap {}) = bit ptBits
 capUntypedSize (ASIDControlCap {}) = 0
 capUntypedSize (ASIDPoolCap {}) = bit asidPoolBits
 
--- No arch-specific thread deletion operations needed on RISC-V platform.
+-- Thread deletion requires associated FPU cleanup
+
+fpuThreadDelete :: PPtr TCB -> Kernel ()
+fpuThreadDelete threadPtr =
+    doMachineOp $ fpuThreadDeleteOp (fromPPtr threadPtr)
 
 prepareThreadDelete :: PPtr TCB -> Kernel ()
-prepareThreadDelete _ = return ()
+prepareThreadDelete thread = fpuThreadDelete thread