haskell: removed outdated platforms
HaskellCPU and Alpha implementations have fallen far behind the current kernel structure, haven't been used for years, and are not included in the build. Removing them to avoid confusion.
This commit is contained in:
Gerwin Klein
parent
2678131125
commit
0a7c0dce9d
|
|
@ -1,208 +0,0 @@
|
|||
%
|
||||
% Copyright 2014, General Dynamics C4 Systems
|
||||
%
|
||||
% This software may be distributed and modified according to the terms of
|
||||
% the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
||||
% See "LICENSE_GPLv2.txt" for details.
|
||||
%
|
||||
% @TAG(GD_GPL)
|
||||
%
|
||||
|
||||
> module HaskellCPU where
|
||||
|
||||
> import SEL4.Kernel
|
||||
> import SEL4.Object
|
||||
> import SEL4.Machine
|
||||
> import SEL4.Model
|
||||
> import SEL4.API
|
||||
> import qualified SEL4.Machine.Hardware.HaskellCPU as H
|
||||
> import qualified SEL4.Machine.RegisterSet.HaskellCPU as R
|
||||
|
||||
> import Control.Monad.State
|
||||
> import Data.Map as Map
|
||||
> import Data.Bits
|
||||
|
||||
> data Instruction
|
||||
> = Arithmetic Register (Word -> Word -> Word) Register Register
|
||||
> | ArithmeticI Register (Word -> Word) Register
|
||||
> | Compare Register (Word -> Word -> Bool) Register Register
|
||||
> | CompareI Register (Word -> Bool) Register
|
||||
> | LoadImmediate Word Register
|
||||
> | Load Word Register Register
|
||||
> | Store Register Word Register
|
||||
> | Push Register
|
||||
> | Pop Register
|
||||
> | Move Register Register
|
||||
> | Branch Word
|
||||
> | BranchIf Register Word
|
||||
> | Jump Register
|
||||
> | JumpLinked Register Register
|
||||
> | Syscall Int
|
||||
> | DebugPrintf String [Register]
|
||||
> | IllegalInstruction
|
||||
> | Halt
|
||||
|
||||
> type UserText = Map.Map PPtr Instruction
|
||||
|
||||
> intSize :: Word
|
||||
> intSize = fromIntegral $ finiteBitSize (undefined::Word) `div` 8
|
||||
|
||||
> onMachine :: State H.MachineState () -> IO ()
|
||||
> onMachine program = do
|
||||
> let finalState = program `execState` newMachineState
|
||||
> mapM_ putStrLn $ H.msConsoleOutput finalState
|
||||
> where newMachineState = H.MS Map.empty Map.empty []
|
||||
|
||||
> mainLoop :: UserText -> KernelMonad ()
|
||||
> mainLoop text = do
|
||||
> ev <- executeInstructions text 10000
|
||||
> case ev of
|
||||
> Just event -> do
|
||||
> callKernel event
|
||||
> mainLoop text
|
||||
> Nothing -> return ()
|
||||
|
||||
> executeInstructions :: UserText -> Int ->
|
||||
> KernelMonad (Maybe Event)
|
||||
|
||||
> executeInstructions _ 0 = return $ Just TimerInterrupt
|
||||
|
||||
> executeInstructions text time = do
|
||||
> thread <- getCurThread
|
||||
> pc <- asUser thread $ getRegister $ Register R.PC
|
||||
> ppc <- tlbLookup (VPtr pc) False
|
||||
> case ppc of
|
||||
> Just addr -> do
|
||||
> asUser thread $ setRegister (Register R.PC) (pc+4)
|
||||
> ev <- executeInstruction thread $
|
||||
> Map.findWithDefault IllegalInstruction addr text
|
||||
> case ev of
|
||||
> Just ev -> return ev
|
||||
> Nothing -> executeInstructions text (time-1)
|
||||
> _ -> return $ Just $ VMFault (VPtr pc) False
|
||||
|
||||
> executeInstruction :: ThreadPtr -> Instruction ->
|
||||
> KernelMonad (Maybe (Maybe Event))
|
||||
|
||||
> executeInstruction tp (Arithmetic ra f rb rd) = asUser tp $ do
|
||||
> a <- getRegister ra
|
||||
> b <- getRegister rb
|
||||
> setRegister rd $ f a b
|
||||
> return Nothing
|
||||
|
||||
> executeInstruction tp (ArithmeticI ra f rd) = asUser tp $ do
|
||||
> a <- getRegister ra
|
||||
> setRegister rd $ f a
|
||||
> return Nothing
|
||||
|
||||
> executeInstruction tp (Compare ra f rb rd) =
|
||||
> executeInstruction tp $
|
||||
> Arithmetic ra (\a b -> fromIntegral $ fromEnum $ f a b) rb rd
|
||||
|
||||
> executeInstruction tp (CompareI ra f rd) =
|
||||
> executeInstruction tp $
|
||||
> ArithmeticI ra (fromIntegral . fromEnum . f) rd
|
||||
|
||||
> executeInstruction tp (LoadImmediate i rd) =
|
||||
> asUser tp $ setRegister rd i >> return Nothing
|
||||
|
||||
> executeInstruction tp (Load i ra rb) = do
|
||||
> a <- asUser tp $ getRegister ra
|
||||
> doLoad tp (VPtr $ i+a) rb
|
||||
|
||||
> executeInstruction tp (Store ra i rb) = do
|
||||
> b <- asUser tp $ getRegister rb
|
||||
> doStore tp ra (VPtr $ i+b)
|
||||
|
||||
> executeInstruction tp (Push ra) = do
|
||||
> sp <- asUser tp $ getRegister $ Register R.SP
|
||||
> asUser tp $ setRegister (Register R.SP) $ sp-intSize
|
||||
> doStore tp ra (VPtr $ sp-intSize)
|
||||
|
||||
> executeInstruction tp (Pop ra) = do
|
||||
> sp <- asUser tp $ getRegister $ Register R.SP
|
||||
> asUser tp $ setRegister (Register R.SP) $ sp+intSize
|
||||
> doLoad tp (VPtr sp) ra
|
||||
|
||||
> executeInstruction tp (Move ra rb) = asUser tp $ do
|
||||
> a <- getRegister ra
|
||||
> setRegister rb a
|
||||
> return Nothing
|
||||
|
||||
> executeInstruction tp (Branch a) = asUser tp $ do
|
||||
> pc <- getRegister $ Register R.PC
|
||||
> setRegister (Register R.PC) $ pc+(a*intSize)-intSize
|
||||
> return Nothing
|
||||
|
||||
> executeInstruction tp (BranchIf ra b) = do
|
||||
> a <- asUser tp $ getRegister ra
|
||||
> if a/=0
|
||||
> then executeInstruction tp $ Branch b
|
||||
> else return Nothing
|
||||
|
||||
> executeInstruction tp (Jump ra) = asUser tp $ do
|
||||
> newpc <- getRegister ra
|
||||
> setRegister (Register R.PC) $ newpc-intSize
|
||||
> return Nothing
|
||||
|
||||
> executeInstruction tp (JumpLinked ra rl) = do
|
||||
> asUser tp $ do
|
||||
> pc <- getRegister (Register R.PC)
|
||||
> setRegister rl (pc+intSize)
|
||||
> executeInstruction tp $ Jump ra
|
||||
|
||||
> executeInstruction _ (Syscall n)
|
||||
> | n>=0 && n <= (fromIntegral $ fromEnum (maxBound :: Syscall)) =
|
||||
> return $ Just $ Just $ SyscallEvent $ toEnum $ fromIntegral n
|
||||
> | otherwise = return $ Just $ Just $ UnknownSyscall $ fromIntegral n
|
||||
|
||||
> executeInstruction tp (DebugPrintf msg regs) = do
|
||||
> values <- asUser tp $ mapM getRegister regs
|
||||
> doMachineOp $ debugPrint $ formatError msg values
|
||||
> return Nothing
|
||||
|
||||
> executeInstruction _ IllegalInstruction =
|
||||
> return $ Just $ Just $ UserLevelFault 0
|
||||
|
||||
> executeInstruction _ Halt =
|
||||
> return $ Just $ Nothing
|
||||
|
||||
> doLoad :: ThreadPtr -> VPtr -> Register ->
|
||||
> KernelMonad (Maybe (Maybe Event))
|
||||
> doLoad tp ptr reg = do
|
||||
> pptr <- tlbLookup ptr False
|
||||
> case pptr of
|
||||
> Just addr -> do
|
||||
> val <- doMachineOp $ loadWord addr
|
||||
> asUser tp $ setRegister reg val
|
||||
> return Nothing
|
||||
> _ -> return $ Just $ Just $ VMFault ptr False
|
||||
|
||||
> doStore :: ThreadPtr -> Register -> VPtr ->
|
||||
> KernelMonad (Maybe (Maybe Event))
|
||||
> doStore tp reg ptr = do
|
||||
> pptr <- tlbLookup ptr True
|
||||
> case pptr of
|
||||
> Just addr -> do
|
||||
> val <- asUser tp $ getRegister reg
|
||||
> doMachineOp $ storeWord addr val
|
||||
> return Nothing
|
||||
> _ -> return $ Just $ Just $ VMFault ptr True
|
||||
|
||||
> tlbLookup :: VPtr -> Bool -> KernelMonad (Maybe PPtr)
|
||||
> tlbLookup vaddr write = do
|
||||
> tlb <- doMachineOp $ gets H.msTLB
|
||||
> let vpn = vPtrToVPN vaddr
|
||||
> let entry = Map.lookup vpn tlb
|
||||
> return $! case entry of
|
||||
> Just (pfn, writable) -> if writable || not write
|
||||
> then Just $ findPPtr vaddr pfn
|
||||
> else Nothing
|
||||
> Nothing -> Nothing
|
||||
|
||||
> formatError :: String -> [Word] -> String
|
||||
> formatError "" _ = ""
|
||||
> formatError ('%':chars) (i:values) = (show i) ++ (formatError chars values)
|
||||
> formatError (x:chars) values = x : (formatError chars values)
|
||||
|
||||
|
||||
|
|
@ -1,17 +0,0 @@
|
|||
%
|
||||
% Copyright 2014, General Dynamics C4 Systems
|
||||
%
|
||||
% This software may be distributed and modified according to the terms of
|
||||
% the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
||||
% See "LICENSE_GPLv2.txt" for details.
|
||||
%
|
||||
% @TAG(GD_GPL)
|
||||
%
|
||||
|
||||
This module contains an instance of the machine-specific kernel API for the Haskell-based CPU simulator. This simulator is for the machine-independent API, and defines no additional object types; so this module re-exports the definitions of the universal object types.
|
||||
|
||||
> module SEL4.API.Types.HaskellCPU (module SEL4.API.Types.Universal) where
|
||||
|
||||
> import SEL4.API.Types.Universal
|
||||
|
||||
|
||||
|
|
@ -1,86 +0,0 @@
|
|||
%
|
||||
% Copyright 2014, General Dynamics C4 Systems
|
||||
%
|
||||
% This software may be distributed and modified according to the terms of
|
||||
% the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
||||
% See "LICENSE_GPLv2.txt" for details.
|
||||
%
|
||||
% @TAG(GD_GPL)
|
||||
%
|
||||
|
||||
This module contains definitions of the VSpace functions for platforms that do not define specific data structures for virtual memory page tables. On these platforms, the kernel uses CSpace structures to represent virtual memory address spaces.
|
||||
|
||||
> module SEL4.Kernel.VSpace.CSpace where
|
||||
|
||||
\begin{impdetails}
|
||||
|
||||
> import SEL4.Machine
|
||||
> import SEL4.Model
|
||||
> import SEL4.Object
|
||||
> import SEL4.Kernel.CSpace
|
||||
> import SEL4.API.Types
|
||||
> import SEL4.API.Failures
|
||||
> import {-# SOURCE #-} SEL4.Kernel.Init
|
||||
|
||||
> import Data.Bits
|
||||
|
||||
\end{impdetails}
|
||||
|
||||
> initVSpace :: PPtr CTE -> PPtr CTE -> KernelInit ()
|
||||
> initVSpace cRootSlot vRootSlot = doKernelOp $ do
|
||||
> cRootCap <- getSlotCap cRootSlot
|
||||
> cteInsert cRootCap cRootSlot vRootSlot
|
||||
|
||||
> lookupVPtr :: PPtr TCB -> VPtr -> Bool -> KernelF LookupFailure (PPtr Word)
|
||||
> lookupVPtr thread vptr isWrite = do
|
||||
> threadRootSlot <- withoutFailure $ getThreadVSpaceRoot thread
|
||||
> threadRoot <- withoutFailure $ getSlotCap threadRootSlot
|
||||
|
||||
> let cptr = CPtr $ fromVPtr vptr
|
||||
> let bits = finiteBitSize cptr
|
||||
> (slot,endBits) <-
|
||||
> resolveAddressBits threadRoot cptr bits
|
||||
> cap <- withoutFailure $ getSlotCap slot
|
||||
|
||||
> case (isWrite, cap) of
|
||||
> (_, FrameCap { capVPSizeBits = sizeBits })
|
||||
> | sizeBits /= endBits -> throw $ DepthMismatch {
|
||||
> depthMismatchBitsLeft = endBits,
|
||||
> depthMismatchBitsFound = sizeBits }
|
||||
> (True, FrameCap { capVPCanWrite = True }) -> return ()
|
||||
> (False, FrameCap { capVPCanRead = True }) -> return ()
|
||||
> _ -> throw $ MissingCapability { missingCapBitsLeft = 0 }
|
||||
>
|
||||
> let offset = fromVPtr vptr .&. mask (capVPSizeBits cap)
|
||||
> return $! capVPBasePtr cap + PPtr offset
|
||||
|
||||
> handleVMFault :: PPtr TCB -> VMFaultType -> KernelF Fault ()
|
||||
> handleVMFault thread (vptr, isWrite) = do
|
||||
> pptr <- lookupVPtr thread vptr isWrite `catchFailure`
|
||||
> \lf -> throwFault $ VMFault vptr isWrite $ msgFromLookupFailure lf
|
||||
> withoutFailure $ doMachineOp $
|
||||
> insertMapping pptr vptr pageBits isWrite
|
||||
|
||||
> isValidVTableRoot :: Capability -> Bool
|
||||
> isValidVTableRoot (CNodeCap {}) = True
|
||||
> isValidVTableRoot _ = False
|
||||
|
||||
> createInitPage :: PAddr -> Kernel Capability
|
||||
> createInitPage addr = do
|
||||
> let ptr = ptrFromPAddr addr
|
||||
> reserveFrame ptr False
|
||||
> return $ FrameCap ptr pageBits True True
|
||||
>
|
||||
> createDeviceCap :: (PAddr, PAddr) -> Kernel Capability
|
||||
> createDeviceCap (addr, end) = do
|
||||
> let wptr = ptrFromPAddr addr
|
||||
> -- need to figure out size in bits based on start and end addresses
|
||||
> let rawsize = end - addr
|
||||
> let size = find (\sz -> rawsize == bit (pageBitsForSize sz))
|
||||
> [minBound .. maxBound]
|
||||
> size <- case sz of
|
||||
> Just size -> return size
|
||||
> Nothing -> fail "Couldn't find appropriate size for device"
|
||||
> return $ FrameCap wptr (pageBitsForSize size) True True
|
||||
|
||||
|
||||
|
|
@ -1,19 +0,0 @@
|
|||
%
|
||||
% Copyright 2014, General Dynamics C4 Systems
|
||||
%
|
||||
% This software may be distributed and modified according to the terms of
|
||||
% the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
||||
% See "LICENSE_GPLv2.txt" for details.
|
||||
%
|
||||
% @TAG(GD_GPL)
|
||||
%
|
||||
|
||||
The generic Haskell-based CPU uses the capability space for virtual memory.
|
||||
|
||||
> module SEL4.Kernel.VSpace.HaskellCPU (
|
||||
> module SEL4.Kernel.VSpace.CSpace
|
||||
> ) where
|
||||
|
||||
> import SEL4.Kernel.VSpace.CSpace
|
||||
|
||||
|
||||
|
|
@ -1,112 +0,0 @@
|
|||
%
|
||||
% Copyright 2014, General Dynamics C4 Systems
|
||||
%
|
||||
% This software may be distributed and modified according to the terms of
|
||||
% the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
||||
% See "LICENSE_GPLv2.txt" for details.
|
||||
%
|
||||
% @TAG(GD_GPL)
|
||||
%
|
||||
|
||||
> module SEL4.Machine.Arch.Alpha (
|
||||
> Register(..), Word, MachineMonad, MachineData, CallbackData,
|
||||
> initMachine
|
||||
> ) where
|
||||
|
||||
> import SEL4.Machine
|
||||
> import SEL4.API
|
||||
> import SEL4.Model
|
||||
> import SEL4.Object
|
||||
> import SEL4.Kernel
|
||||
|
||||
> import qualified Data.Word
|
||||
> import Data.Bits
|
||||
> import Data.Ix
|
||||
> import Data.Typeable
|
||||
> import qualified Foreign.Storable
|
||||
> import Foreign.Ptr
|
||||
> import Control.Monad.Reader
|
||||
|
||||
> data Register = PC | NPC |
|
||||
> V0 | T0 | T1 | T2 | T3 | T4 | T5 | T6 | T7 | S0 | S1 | S2 | S3 | S4 |
|
||||
> S5 | FP | A0 | A1 | A2 | A3 | A4 | A5 | T8 | T9 | T10 | T11 | RA | T12 |
|
||||
> AT | GP | SP
|
||||
> deriving (Eq, Enum, Bounded, Ord, Ix, Typeable)
|
||||
|
||||
> instance RegisterName Register
|
||||
|
||||
> newtype Word = Word Data.Word.Word64
|
||||
> deriving (Show,Eq,Ord,Num,Enum,Real,Integral,Bits,Typeable,MachineWord,
|
||||
> Foreign.Storable.Storable)
|
||||
|
||||
> type MachineMonad = ReaderT MachineData IO
|
||||
|
||||
> initMachine :: PPtr Word -> [(PPtr Word, Int)] -> Ptr CallbackData ->
|
||||
> MachineData
|
||||
> initMachine = MachineData
|
||||
|
||||
> data CallbackData
|
||||
|
||||
> data MachineData = MachineData {
|
||||
> sdMemoryTop :: PPtr Word,
|
||||
> sdDeviceRegions :: [(PPtr Word, PPtr Word)],
|
||||
> sdCallbackPtr :: Ptr CallbackData }
|
||||
|
||||
> instance Hardware Register Word MachineMonad where
|
||||
> getMemoryTop = asks sdMemoryTop
|
||||
> getDeviceRegions = asks sdDeviceRegions
|
||||
|
||||
> loadWord ptr = do
|
||||
> cbptr <- asks sdCallbackPtr
|
||||
> lift $ loadWordCallback cbptr ptr
|
||||
> storeWord ptr val = do
|
||||
> cbptr <- asks sdCallbackPtr
|
||||
> lift $ storeWordCallback cbptr ptr val
|
||||
> storeWordVM ptr val = storeWord ptr val
|
||||
> tlbInsertEntry pptr vptr isWrite = do
|
||||
> cbptr <- asks sdCallbackPtr
|
||||
> lift $ tlbInsertCallback cbptr pptr vptr isWrite
|
||||
> tlbFlushAll = do
|
||||
> cbptr <- asks sdCallbackPtr
|
||||
> lift $ tlbFlushCallback cbptr
|
||||
|
||||
> debugPrint str = lift $ putStrLn str
|
||||
|
||||
> foreign import ccall "alpha_load_word" loadWordCallback ::
|
||||
> Ptr CallbackData -> PPtr Word -> IO Word
|
||||
|
||||
> foreign import ccall "alpha_store_word" storeWordCallback ::
|
||||
> Ptr CallbackData -> PPtr Word -> Word -> IO ()
|
||||
|
||||
> foreign import ccall "alpha_tlb_insert" tlbInsertCallback ::
|
||||
> Ptr CallbackData -> PFN Word -> VPN Word -> Bool -> IO ()
|
||||
|
||||
> foreign import ccall "alpha_tlb_flush" tlbFlushCallback ::
|
||||
> Ptr CallbackData -> IO ()
|
||||
|
||||
> instance Machine Register Word APIObjectType MachineMonad where
|
||||
> retypeRegion = retypeRegionAPI
|
||||
> detypeObject = detypeObjectAPI
|
||||
> invokeMachineObject = error "No machine-specific object types defined"
|
||||
> lookupVPage = lookupVPageWithCNodes
|
||||
> isValidVTableRoot (CNodeCap {}) = True
|
||||
> isValidVTableRoot _ = False
|
||||
|
||||
> instance Storable (UserData Word) Register Word APIObjectType
|
||||
> where
|
||||
> objBits _ = 13
|
||||
> makeObject = UserData
|
||||
|
||||
> instance RegisterSet Register Word where
|
||||
> msgInfoRegister = A1
|
||||
> msgRegisters = [A2 .. T8]
|
||||
> capRegister = A0
|
||||
> badgeRegister = A0
|
||||
> frameRegisters = PC : NPC : SP : V0 : [A0 .. T8]
|
||||
> gpRegisters = [T0 .. FP] ++ [T9 .. GP]
|
||||
> getFaultingPC = getRegister PC
|
||||
> setNextPC addr = do
|
||||
> setRegister PC addr
|
||||
> setRegister NPC $ addr + 4
|
||||
|
||||
|
||||
|
|
@ -1,70 +0,0 @@
|
|||
%
|
||||
% Copyright 2014, General Dynamics C4 Systems
|
||||
%
|
||||
% This software may be distributed and modified according to the terms of
|
||||
% the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
||||
% See "LICENSE_GPLv2.txt" for details.
|
||||
%
|
||||
% @TAG(GD_GPL)
|
||||
%
|
||||
|
||||
> module SEL4.Machine.Hardware.HaskellCPU where
|
||||
|
||||
> import SEL4.Machine.RegisterSet
|
||||
> import qualified SEL4.Machine.RegisterSet.HaskellCPU as HaskellCPU
|
||||
|
||||
> import Data.Bits
|
||||
> import qualified Data.Map as Map
|
||||
> import Control.Monad.State
|
||||
> import Control.Monad.Error
|
||||
|
||||
> type MachineMonad = State MachineState
|
||||
|
||||
> data MachineState = MS {
|
||||
> msMemory :: Map.Map PPtr Word,
|
||||
> msTLB :: Map.Map VPN (PFN, Bool),
|
||||
> msConsoleOutput :: [String] }
|
||||
|
||||
> pageBits :: Int
|
||||
> pageBits = 12
|
||||
|
||||
> intSize :: Word
|
||||
> intSize = fromIntegral $ finiteBitSize (undefined::Word) `div` 8
|
||||
|
||||
> getMemoryTop :: MachineMonad PPtr
|
||||
> getMemoryTop = return maxBound
|
||||
|
||||
> getDeviceRegions :: MachineMonad [(PPtr, PPtr)]
|
||||
> getDeviceRegions = return []
|
||||
|
||||
> loadWord :: PPtr -> MachineMonad Word
|
||||
> loadWord address = do
|
||||
> when (address .&. PPtr (intSize-1) /= 0) $
|
||||
> fail "unaligned access"
|
||||
> gets $ Map.findWithDefault 0 address . msMemory
|
||||
|
||||
> storeWord :: PPtr -> Word -> MachineMonad ()
|
||||
> storeWord address value = do
|
||||
> when (address .&. PPtr (intSize-1) /= 0) $
|
||||
> fail "unaligned access"
|
||||
> modify (\ms -> ms {
|
||||
> msMemory = Map.insert address value $ msMemory ms })
|
||||
|
||||
> storeWordVM :: PPtr -> Word -> MachineMonad ()
|
||||
> storeWordVM address value = return
|
||||
|
||||
> debugPrint :: String -> MachineMonad ()
|
||||
> debugPrint str = modify (\ms -> ms {
|
||||
> msConsoleOutput = msConsoleOutput ms ++ [str] })
|
||||
|
||||
> tlbInsertEntry :: PFN -> VPN -> Bool -> MachineMonad ()
|
||||
> tlbInsertEntry pptr vptr writable = modify (\ms -> ms {
|
||||
> msTLB = Map.insert vptr (pptr, writable) $ msTLB ms })
|
||||
|
||||
> tlbFlushAll :: MachineMonad ()
|
||||
> tlbFlushAll = modify (\ms -> ms { msTLB = Map.empty })
|
||||
|
||||
> getFaultingPC = getRegister (Register HaskellCPU.PC)
|
||||
> setNextPC = setRegister (Register HaskellCPU.PC)
|
||||
|
||||
|
||||
|
|
@ -1,36 +0,0 @@
|
|||
%
|
||||
% Copyright 2014, General Dynamics C4 Systems
|
||||
%
|
||||
% This software may be distributed and modified according to the terms of
|
||||
% the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
||||
% See "LICENSE_GPLv2.txt" for details.
|
||||
%
|
||||
% @TAG(GD_GPL)
|
||||
%
|
||||
|
||||
> module SEL4.Machine.RegisterSet.HaskellCPU where
|
||||
|
||||
> import qualified Data.Word
|
||||
> import Data.Array
|
||||
|
||||
> data Register =
|
||||
> PC | SP |
|
||||
> -- syscall argument registers
|
||||
> AR0 | AR1 | AR2 | AR3 | AR4 | AR5 | AR6 | AR7 |
|
||||
> -- general purpose integer registers
|
||||
> R0 | R1 | R2 | R3 | R4 | R5 | R6 | R7 |
|
||||
> R8 | R9 | R10 | R11 | R12 | R13 | R14 | R15 |
|
||||
> R16 | R17 | R18 | R19 | R20 | R21 | R22 | R23 |
|
||||
> R24 | R25 | R26 | R27 | R28 | R29 | R30 | R31
|
||||
> deriving (Eq, Enum, Bounded, Ord, Ix, Show)
|
||||
|
||||
> type Word = Data.Word.Word32
|
||||
|
||||
> msgInfoRegister = AR1
|
||||
> msgRegisters = [AR2 .. AR7]
|
||||
> capRegister = AR0
|
||||
> badgeRegister = AR0
|
||||
> frameRegisters = PC : SP : [AR0 .. AR7]
|
||||
> gpRegisters = [R0 .. R31]
|
||||
|
||||
|
||||
|
|
@ -1,30 +0,0 @@
|
|||
%
|
||||
% Copyright 2014, General Dynamics C4 Systems
|
||||
%
|
||||
% This software may be distributed and modified according to the terms of
|
||||
% the GNU General Public License version 2. Note that NO WARRANTY is provided.
|
||||
% See "LICENSE_GPLv2.txt" for details.
|
||||
%
|
||||
% @TAG(GD_GPL)
|
||||
%
|
||||
|
||||
This module contains operations on machine-specific object types for the Haskell-based CPU simulator. Since there are no such object types, the functions here are all undefined, and should never be called.
|
||||
|
||||
> module SEL4.Object.ObjectType.HaskellCPU where
|
||||
|
||||
> import SEL4.Machine
|
||||
> import SEL4.Model.StateData
|
||||
> import SEL4.API.Types
|
||||
> import SEL4.Object.Types
|
||||
|
||||
> retypeRegion :: PPtr -> Int -> ObjectType -> Kernel Int
|
||||
> retypeRegion = undefined
|
||||
|
||||
> detypeObject :: PPtr -> Int -> ObjectType -> Kernel (Maybe ThreadSuicide)
|
||||
> detypeObject = undefined
|
||||
|
||||
> invokeObject :: Word -> [Word] -> CPtr -> CTEPtr -> Capability ->
|
||||
> KernelF Fault (Maybe (Word, [Word]))
|
||||
> invokeObject = undefined
|
||||
|
||||
|
||||
Loading…
Reference in New Issue