haskell: removed Lyrebird target
Consolidating to one simulator to get simulator builds running again. The source setup is still for multiple potential targets so it remains reasonably easy to add different architectures like x86 to the Haskell model if needed.
This commit is contained in:
Gerwin Klein
parent
0a7c0dce9d
commit
eb3ef2a026
|
|
@ -21,23 +21,23 @@ To build it:
|
|||
- install `Cabal 1.18` or later. This is included with GHC 7.8.
|
||||
- configure the sources:
|
||||
|
||||
runhaskell Setup.hs configure --with-target=<arch>-<platform>
|
||||
|
||||
Valid target options are: `arm-qemu`, `arm-lyrebird`
|
||||
|
||||
runhaskell Setup.hs configure --with-target=arm-qemu
|
||||
|
||||
Further target options may be supported again in the future.
|
||||
|
||||
- build the library:
|
||||
|
||||
runhaskell Setup.hs build
|
||||
|
||||
|
||||
- install:
|
||||
|
||||
runhaskell Setup.hs install --user
|
||||
|
||||
|
||||
After that, you can compile Haskell programs using the simulator by adding
|
||||
`-package SEL4` to the `ghc` command line. Note that the qemu and lyrebird
|
||||
targets require some callback functions to be accessible via the FFI, so
|
||||
it is not possible to load a model compiled for those targets in GHCi.
|
||||
`-package SEL4` to the `ghc` command line. Note that the qemu target requires
|
||||
some callback functions to be accessible via the FFI, so it is not possible to
|
||||
load a model compiled for those targets in GHCi.
|
||||
|
||||
Currently, the simulator interface is out of date, so this model is currently
|
||||
only useful as documentation and as intermediate artefact in the seL4
|
||||
|
|
|
|||
|
|
@ -13,7 +13,7 @@ version: 1.4-pre
|
|||
cabal-version: >= 1.8
|
||||
build-type: Simple
|
||||
license: AllRightsReserved
|
||||
author: Philip Derrin et. al.
|
||||
author: Philip Derrin et. al., NICTA
|
||||
synopsis: Executable specification for the seL4 Kernel
|
||||
tested-with: GHC == 7.8.3
|
||||
|
||||
|
|
|
|||
|
|
@ -10,8 +10,6 @@
|
|||
-- @TAG(GD_GPL)
|
||||
--
|
||||
|
||||
-- This is to shut GHC up about defaultUserHooks.
|
||||
|
||||
module Main where
|
||||
import Control.Applicative((<$>))
|
||||
import Distribution.Simple
|
||||
|
|
@ -28,8 +26,7 @@ import Data.List(isPrefixOf, find)
|
|||
import Control.Monad(unless, liftM)
|
||||
|
||||
targets =
|
||||
[ ("arm-qemu", ("ARM", "QEmu"))
|
||||
, ("arm-lyrebird", ("ARM", "Lyrebird"))]
|
||||
[ ("arm-qemu", ("ARM", "QEmu")) ]
|
||||
|
||||
bootModules =
|
||||
[ "Kernel/CSpace"
|
||||
|
|
@ -86,10 +83,6 @@ main = do
|
|||
let targetArg = find (targetPrefix `isPrefixOf`) args
|
||||
let targetName = liftM (drop (length targetPrefix)) targetArg
|
||||
let args' = filter (not . isPrefixOf targetPrefix) args
|
||||
-- n.b. GHC 7.0.3 whinges about defaultUserHooks being
|
||||
-- deprecated, and demands simpleUserHooks or autoconfUserHooks
|
||||
-- instead. Neither of those actually works here, so I'm stuck
|
||||
-- with defaultUserHooks.
|
||||
let hooks = simpleUserHooks {
|
||||
preBuild = \args flags -> do
|
||||
generateHSBoot
|
||||
|
|
|
|||
|
|
@ -1,119 +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)
|
||||
--
|
||||
|
||||
{-# LANGUAGE EmptyDataDecls, ForeignFunctionInterface,
|
||||
GeneralizedNewtypeDeriving #-}
|
||||
|
||||
module SEL4.Machine.Hardware.ARM.Lyrebird where
|
||||
|
||||
import SEL4.Machine.RegisterSet
|
||||
import Foreign.Ptr
|
||||
import Data.Ix
|
||||
import Data.Word(Word8)
|
||||
import Data.Bits
|
||||
|
||||
data CallbackData
|
||||
|
||||
data IRQ = TimerInterrupt
|
||||
deriving (Enum, Bounded, Ord, Ix, Eq, Show)
|
||||
|
||||
newtype PAddr = PAddr { fromPAddr :: Word }
|
||||
deriving (Show, Eq, Ord, Bounded, Real, Enum, Integral, Num, Bits, FiniteBits)
|
||||
|
||||
ptrFromPAddr :: PAddr -> PPtr a
|
||||
ptrFromPAddr (PAddr addr) = PPtr addr
|
||||
|
||||
addrFromPPtr :: PPtr a -> PAddr
|
||||
addrFromPPtr (PPtr ptr) = PAddr ptr
|
||||
|
||||
pageColourBits :: Int
|
||||
pageColourBits = 0
|
||||
|
||||
foreign import ccall "arm_get_mem_top"
|
||||
getMemorySize :: Ptr CallbackData -> IO Int
|
||||
|
||||
getMemoryRegions :: Ptr CallbackData -> IO [(PAddr, PAddr)]
|
||||
getMemoryRegions env = do
|
||||
size <- getMemorySize env
|
||||
return [(PAddr 0, PAddr (bit size))]
|
||||
|
||||
getDeviceRegions :: Ptr CallbackData -> IO [(PAddr, PAddr)]
|
||||
getDeviceRegions _ = return []
|
||||
|
||||
getKernelDevices :: Ptr CallbackData -> IO [(PAddr, PPtr Word)]
|
||||
getKernelDevices _ = return []
|
||||
|
||||
maskInterrupt :: Ptr CallbackData -> Bool -> IRQ -> IO ()
|
||||
maskInterrupt env bool _ = maskIRQCallback env bool
|
||||
|
||||
ackInterrupt :: Ptr CallbackData -> IRQ -> IO ()
|
||||
ackInterrupt env _ = ackIRQCallback env
|
||||
|
||||
foreign import ccall "arm_check_interrupt"
|
||||
getInterruptState :: Ptr CallbackData -> IO Bool
|
||||
|
||||
foreign import ccall "arm_mask_interrupt"
|
||||
maskIRQCallback :: Ptr CallbackData -> Bool -> IO ()
|
||||
|
||||
foreign import ccall "arm_ack_interrupt"
|
||||
ackIRQCallback :: Ptr CallbackData -> IO ()
|
||||
|
||||
getActiveIRQ :: Ptr CallbackData -> IO (Maybe IRQ)
|
||||
getActiveIRQ env = do
|
||||
timer_irq <- getInterruptState env
|
||||
return $ if timer_irq then Just TimerInterrupt else Nothing
|
||||
|
||||
configureTimer :: Ptr CallbackData -> IO IRQ
|
||||
configureTimer _ = return TimerInterrupt
|
||||
|
||||
resetTimer :: Ptr CallbackData -> IO ()
|
||||
resetTimer _ = return ()
|
||||
|
||||
foreign import ccall unsafe "arm_load_word"
|
||||
loadWordCallback :: Ptr CallbackData -> PAddr -> IO Word
|
||||
|
||||
foreign import ccall unsafe "arm_store_word"
|
||||
storeWordCallback :: Ptr CallbackData -> PAddr -> Word -> IO ()
|
||||
|
||||
foreign import ccall unsafe "arm_tlb_flush"
|
||||
invalidateTLBCallback :: Ptr CallbackData -> IO ()
|
||||
|
||||
foreign import ccall unsafe "arm_tlb_flush_asid"
|
||||
invalidateHWASIDCallback :: Ptr CallbackData -> Word8 -> IO ()
|
||||
|
||||
foreign import ccall unsafe "arm_tlb_flush_vptr"
|
||||
invalidateMVACallback :: Ptr CallbackData -> Word -> IO ()
|
||||
|
||||
cacheCleanMVACallback :: Ptr CallbackData -> PPtr a -> IO ()
|
||||
cacheCleanMVACallback _cptr _mva = return ()
|
||||
|
||||
cacheCleanRangeCallback :: Ptr CallbackData -> PPtr a -> PPtr a -> IO ()
|
||||
cacheCleanRangeCallback _cptr _vbase _vtop = return ()
|
||||
|
||||
cacheCleanCallback :: Ptr CallbackData -> IO ()
|
||||
cacheCleanCallback _cptr = return ()
|
||||
|
||||
cacheInvalidateRangeCallback :: Ptr CallbackData -> PPtr a -> PPtr a -> IO ()
|
||||
cacheInvalidateRangeCallback _cptr _vbase _vtop = return ()
|
||||
|
||||
foreign import ccall unsafe "arm_set_asid"
|
||||
setHardwareASID :: Ptr CallbackData -> Word8 -> IO ()
|
||||
|
||||
foreign import ccall unsafe "arm_set_table_root"
|
||||
setCurrentPD :: Ptr CallbackData -> PAddr -> IO ()
|
||||
|
||||
foreign import ccall unsafe "arm_get_ifsr"
|
||||
getIFSR :: Ptr CallbackData -> IO Word
|
||||
|
||||
foreign import ccall unsafe "arm_get_dfsr"
|
||||
getDFSR :: Ptr CallbackData -> IO Word
|
||||
|
||||
foreign import ccall unsafe "arm_get_far"
|
||||
getFAR :: Ptr CallbackData -> IO VPtr
|
||||
Loading…
Reference in New Issue