init commit for imx31-new-qemu support

haskell/SEL4.cabal

@@ -25,7 +25,7 @@ Library
     exposed-modules:        SEL4
                             SEL4.Machine.Target
 
-    build-depends:          mtl, base, array, containers
+    build-depends:          mtl==2.1.3.1, base, array, containers
     if flag(FFI)
     -- be fixed.
         build-depends:      unix
@@ -42,6 +42,7 @@ Library
                             SEL4.API.Types.Universal
                             SEL4.API.Invocation
                             SEL4.Kernel
+                            SEL4.Kernel.BootInfo
                             SEL4.Kernel.VSpace
                             SEL4.Kernel.CSpace
                             SEL4.Kernel.Init

haskell/src/SEL4/API/Failures.lhs

@@ -42,6 +42,12 @@ The procedure for handling faults is defined in \autoref{sec:kernel.faulthandler
 >             userExceptionErrorCode :: Word }
 >         deriving Show
 
+\subsection{Kernel Init Failure}
+
+Data type InitFailure can be thrown during SysInit
+
+> data InitFailure = InitFailure
+
 \subsection{System Call Errors}
 
 The following data type defines the set of errors that can be returned from a kernel object method call.

haskell/src/SEL4/API/Types.lhs

@@ -28,7 +28,7 @@ We use the C preprocessor to select a target architecture. Also, this file makes
 > import SEL4.Machine
 
 > import Data.Bits
-> import Data.Word(Word8)
+> import Data.Word(Word8 , Word32)
 
 \end{impdetails}
 
@@ -203,86 +203,44 @@ The top-level structure is "BootInfo", which contains an IPC buffer pointer,
 information about the initial untyped capabilities, and an array of virtual
 address space regions.
 
-> data BootInfo = BootInfo {
->         biIPCBuffer :: VPtr,
->         -- insert (length biRegions) here
->         biRegions :: [BootRegion] }
->     deriving Show
-
-> wordsFromBootInfo :: BootInfo -> [Word]
-> wordsFromBootInfo bi = [
->         fromVPtr $ biIPCBuffer bi,
->         fromIntegral $ length $ biRegions bi ]
->         ++ (concat $ map wordsFromBootRegion $ biRegions bi)
-
-Each region descriptor has start and end pointers (with the latter pointing to
-the last address in the region, rather than the first address after it), a
-type, and some data whose use depends on the type.
-
-> data BootRegion = BootRegion {
->         brBase :: CPtr,
->         brEnd :: CPtr,
->         brType :: BootRegionType,
->         brData :: Word }
->     deriving Show
-
-> wordsFromBootRegion :: BootRegion -> [Word]
-> wordsFromBootRegion br = [
->         fromCPtr $ brBase br,
->         fromCPtr $ brEnd br,
->         fromIntegral $ fromEnum $ brType br,
->         brData br ]
-
-The boot regions are of various types, and are used for three separate purposes: describing what \emph{can} appear in a specific region of the address space, describing what \emph{is} in the initial task's address space, and describing the structure of the capability table. Regions with different purposes may overlap as noted below.
-
-> data BootRegionType
-
-\begin{description}
-
-\item[Empty] regions are not used by capabilities or virtual memory mappings in the initial task's address space.
-
->         = BREmpty
-
-\item[RootTask] regions contain the root task's mapped text or data, backed by one or more page-sized frames.
-
->         | BRRootTask
-
-\item[CapsOnly] regions cannot be used for virtual memory mappings, but are still usable for capabilities. This may be, for example, because the kernel maps its own data at these addresses, or because the hardware MMU does not implement addressing of the region. This may overlap any region other than "BRRootTask".
-
->         | BRCapsOnly
-
-\item[NodeL1] appears once, and represents the area covered by the initial thread's root page table node. The data word contains the radix of the node.
-
->         | BRNodeL1
-
-\item[NodeL2] regions represent second-level nodes in the initial capability table. Again, the data word contains the radix of the node. They all occur within the "BRNodeL1" region.
-
->         | BRNodeL2
-
-Regions of any of the types below only appear in "BRNodeL2" regions.
-
-\item[FreeSlots] regions contain empty capability slots accessible in the root task's CSpace, which may be used to bootstrap the system's capability management. The data word gives the CSpace depth required by the Retype call to locate the CNode containing the slots.
-
->         | BRFreeSlots
-
-\item[InitCaps] is the region containing the root task's six guaranteed initial capabilities; it always appears exactly once with a base address of zero. Address 0 contains a null capability (which should not be replaced with a valid one). It is followed by the initial thread's TCB, CSpace root, VSpace root, and reply endpoint, and then .
-
->         | BRInitCaps
-
-\item[SmallBlocks] regions are filled with untyped memory objects of a single size, generally the platform's standard page size. The minimum number of page-sized untyped blocks that will be provided to the root task by the kernel is fixed at compile time. The data word contains the block size, in address bits.
-
->         | BRSmallBlocks
-
-\item[LargeBlocks] regions are filled with untyped memory objects of varying sizes. The kernel provides large blocks for any physical memory not already covered by other memory regions. The blocks are in order from smallest to largest, with at most one of each size; the sizes present have the corresponding bits in the region's data word set. In spite of the name, some of these blocks may have sizes less than one page. There may be multiple large block regions.
+> newtype Region = Region { fromRegion :: (PPtr Word, PPtr Word) }
+>     deriving (Show, Eq)
 
->         | BRLargeBlocks
+> ptrFromPAddrRegion :: (PAddr, PAddr) -> Region
+> ptrFromPAddrRegion (start, end) = Region (ptrFromPAddr start, ptrFromPAddr end)
 
-\item[DeviceCaps] regions each contain the capabilities required to access one hardware device. The meaning of the data word is implementation-defined.
+> newtype SlotRegion = SlotRegion (Word, Word)
+>     deriving (Show, Eq)
 
->         | BRDeviceCaps
+> data BIDeviceRegion = BIDeviceRegion {
+>         bidrBasePAddr :: PAddr,
+>         bidrFrameSizeBits :: Word32,
+>         bidrFrameCaps :: SlotRegion }
+>     deriving (Show, Eq)
 
-\end{description}
+> data BIFrameData = BIFrameData {
+>         bifNodeID :: Word32, --Word?
+>         bifNumNodes :: Word32, --Int?
+>         bifNumIOPTLevels :: Word32, --Int?
+>         bifIPCBufVPtr :: VPtr,
+>         bifNullCaps :: [Word],
+>         bifSharedFrameCaps :: [Word],
+>         bifUIFrameCaps :: [Word],
+>         bifUIPTCaps :: [Word],
+>         bifUntypedObjCaps :: [Word],
+>         bifUntypedObjPAddrs :: [PAddr],
+>         bifUntypedObjSizeBits :: [Word8], --combine these into one list?
+>         bifITCNodeSizeBits :: Word8,
+>         bifNumDeviceRegions :: Word32,
+>         bifDeviceRegions :: [BIDeviceRegion] }
+>     deriving (Show, Eq)
 
->     deriving (Show, Enum)
+> data InitData = InitData {
+>     initFreeMemory :: [Region], -- Filled in initFreemem
+>     initSlotPosCur :: Word, --Word?
+>     initSlotPosMax :: Word, -- Filled in makeRootCNode ?
+>     initBootInfo :: BIFrameData,
+>     initBootInfoFrame :: PAddr } --PAddr?
+>     deriving (Show, Eq)
 
 

haskell/src/SEL4/Kernel/BootInfo.lhs

+% @LICENSE(OKL_CORE)
+
+This module contains functions that maintaining the bootinfo structure for init-thread .
+
+> module SEL4.Kernel.BootInfo where
+
+\begin{impdetails}
+
+> import Data.Bits
+> import Control.Monad.State
+
+> import SEL4.API.Types
+> import SEL4.Object.Structures
+> import SEL4.Machine
+
+> import SEL4.Model.StateData
+
+> import {-# SOURCE #-} SEL4.Kernel.Init
+
+
+\subsection{Constant}
+
+> biCapNull :: Word
+> biCapNull = 0
+
+> itASID :: ASID
+> itASID = 1
+
+> biCapITTCB :: Word
+> biCapITTCB = 1
+
+> biCapITCNode :: Word
+> biCapITCNode = 2
+
+> biCapITPD :: Word
+> biCapITPD = 3
+
+> biCapIRQControl :: Word
+> biCapIRQControl = 4
+
+> biCapASIDControl :: Word
+> biCapASIDControl = 5
+
+> biCapITASIDPool :: Word
+> biCapITASIDPool = 6
+
+> biCapIOPort :: Word
+> biCapIOPort = 7
+
+> biCapIOSpace :: Word
+> biCapIOSpace = 8
+
+> biCapBIFrame :: Word
+> biCapBIFrame = 9
+
+> biCapITIPCBuf :: Word
+> biCapITIPCBuf = 10
+
+> biCapDynStart :: Word
+> biCapDynStart = 11
+
+> biFrameSizeBits :: Int
+> biFrameSizeBits = pageBits
+
+Warning: rootCNodeSizeBits should be rootCNodeSize + objBits (undefined::CTE)
+
+> rootCNodeSizeBits :: Int
+> rootCNodeSizeBits = 12 -- FIXME: duplication (maybe, check)
+
+
+
+\subsection{Default Bootinfo}
+
+> nopBIFrameData :: BIFrameData
+> nopBIFrameData = BIFrameData {
+>         bifNodeID = 0,        -- Initialized in createIPCBufferFrame
+>         bifNumNodes = 0,      -- Initialized in createIPCBufferFrame 
+>         bifNumIOPTLevels = 0, -- Initialized with 0 if fine
+>         bifIPCBufVPtr =0,     -- Initialized in createIPCBufferFrame
+>         bifNullCaps = [],
+>         bifSharedFrameCaps = [], -- ARM no multikernel
+>         bifUIFrameCaps = [], -- Initialized in createFramesOfRegion
+>         bifUIPTCaps = [], -- Initialized in createITPDPTs
+>         bifUntypedObjCaps = [],
+>         bifUntypedObjPAddrs = [],
+>         bifUntypedObjSizeBits = [],
+>         bifITCNodeSizeBits = fromIntegral rootCNodeSizeBits, -- Initialized here is fine
+>         bifNumDeviceRegions = 0,
+>         bifDeviceRegions = [] 
+>         }
+
+
+Functions for serialize BIFrameData into Memory
+
+> data SerialData = SerialData {ptrCursor::PPtr Word,value::Word}
+> type Serializer = StateT SerialData MachineMonad
+
+> serializeStore :: Word -> Int -> Serializer ()
+> serializeStore value intsize = do
+>    forM_ [0 .. intsize-1] $ \size -> do
+
+Warning: For little endian system we should use this size instead of intsize - size - 1
+
+>        byte <- return $ (value `shiftR` (8 * (intsize - size -1))) .&. ((bit 8) - 1)
+>        serializeByte byte
+
+> serializeByte :: Word -> Serializer ()
+> serializeByte input = do
+>    ptr <- gets ptrCursor
+>    byte <- gets value
+>    value <- return $ input .|. ((fromIntegral byte) `shiftL` 8)
+>    if (ptr .&. 3) == 3
+>      then do
+>        lift $ storeWordVM ((ptr `shiftR` 2) `shiftL` 2) value
+>        modify (\st -> st {ptrCursor = ptr + 1, value = 0})
+>      else
+>        modify (\st -> st {ptrCursor = ptr + 1, value = value})
+
+> paddingTo :: PPtr Word -> Serializer()
+> paddingTo pptr = do
+>    ptr <- gets ptrCursor
+>    (flip mapM_) [ptr .. pptr-1] $ \_ -> (serializeByte 0)
+
+> maxBIUntypedCaps :: Word
+> maxBIUntypedCaps = 167
+
+> maxBIDeviceRegions :: Word
+> maxBIDeviceRegions = 200
+
+> serialBIDeviceRegion :: BIDeviceRegion -> Serializer ()
+> serialBIDeviceRegion biDeviceRegion = do
+>    serializeStore (fromPAddr $ bidrBasePAddr biDeviceRegion) 4
+>    serializeStore (fromIntegral $ bidrFrameSizeBits biDeviceRegion) 4
+>    slotRegion <- return $ bidrFrameCaps biDeviceRegion
+>    let (a,b) = case slotRegion of SlotRegion (a,b) -> (a,b)
+>    serializeStore a 4
+>    serializeStore b 4
+>    return ()
+
+The function syncBIFrame is used as the last step in KernelInit. 
+It will write boot info back into the memory.
+
+> syncBIFrame :: KernelInit ()
+> syncBIFrame = do
+>    frameData <- gets $ initBootInfo
+>    frame <- gets $ initBootInfoFrame
+>    doKernelOp $ doMachineOp $ do
+>        (flip runStateT) (SerialData {ptrCursor = ptrFromPAddr $ frame,value = 0}) $ do
+>            serializeStore (fromIntegral (bifNodeID frameData)) 4
+>            serializeStore (fromIntegral (bifNumNodes frameData)) 4
+>            serializeStore (fromIntegral (bifNumIOPTLevels frameData)) 4
+>            serializeStore (fromIntegral $ fromVPtr $ (bifIPCBufVPtr frameData)) 4
+>            let serializeRange = \ls -> if ls == []
+>                       then do
+>                         serializeStore 0 4
+>                         serializeStore 0 4
+>                       else do
+>                         serializeStore (head ls) 4
+>                         serializeStore (last ls) 4
+>            serializeRange $ bifNullCaps frameData
+>            serializeRange $ bifSharedFrameCaps frameData
+>            serializeRange $ bifUIFrameCaps frameData
+>            serializeRange $ bifUIPTCaps frameData
+>            serializeRange $ bifUntypedObjCaps frameData
+
+>            ptr <- gets ptrCursor
+>            ptr <- return $ ptr + (PPtr $ maxBIUntypedCaps `shiftL` 2)
+>            untypedAddrs <- return $ bifUntypedObjPAddrs frameData
+>            (flip mapM_) untypedAddrs $ \addr -> do
+>                serializeStore (fromPAddr addr) 4
+>            paddingTo ptr
+>            ptr <- return $ ptr + (PPtr maxBIUntypedCaps)
+>            untypedSizeBits <- return $ bifUntypedObjSizeBits frameData
+>            (flip mapM_) untypedSizeBits $ \bits -> do
+>                serializeStore (fromIntegral bits) 1
+>            paddingTo ptr
+>            serializeStore (fromIntegral $ bifITCNodeSizeBits frameData) 1
+>            serializeStore (fromIntegral $ bifNumDeviceRegions frameData) 4
+>            (flip mapM_) (bifDeviceRegions frameData) $ \region -> do
+>                serialBIDeviceRegion region
+>        return ()
+
+The KernelInit monad can fail - however, we do not care what type of failure occurred, only that a failure has happened.
+
+> isAligned x n = x .&. mask n == 0
+

haskell/src/SEL4/Kernel/VSpace.lhs

@@ -31,6 +31,7 @@ We use the C preprocessor to select a target architecture.
 > import SEL4.Model
 > import SEL4.Object
 > import SEL4.API.Failures
+> import SEL4.API.Types
 > import {-# SOURCE #-} SEL4.Kernel.Init
 
 \end{impdetails}
@@ -48,12 +49,42 @@ This module defines architecture-specific virtual memory management procedures.
 \item preparing the virtual memory environment, if any, that the kernel requires to run;
 
 > initKernelVM :: Kernel ()
-> initKernelVM = Arch.initKernelVM
+> initKernelVM = Arch.mapKernelWindow
 
-\item creating the initial address space, given the slot containing the root CSpace capability and an empty slot in which the root VSpace capability should be placed;
+> initPlatform :: Kernel ()
+> initPlatform = do
+>   doMachineOp $ configureTimer
+>   initL2Cache
+
+> initL2Cache = return ()
+
+> initCPU :: Kernel ()
+> initCPU = Arch.activateGlobalPD
+
+
+> createIPCBufferFrame :: Capability -> VPtr -> KernelInit Capability
+> createIPCBufferFrame  = Arch.createIPCBufferFrame
+
+> createBIFrame  = Arch.createBIFrame
+
+> createFramesOfRegion :: Capability -> Region -> Bool -> VPtr -> KernelInit () 
+> createFramesOfRegion = Arch.createFramesOfRegion
+
+> createITPDPTs :: Capability -> VPtr -> VPtr -> KernelInit Capability
+> createITPDPTs = Arch.createITPDPTs
+
+> writeITPDPTs :: Capability -> Capability -> KernelInit ()
+> writeITPDPTs = Arch.writeITPDPTs 
+
+> createITASIDPool :: Capability -> KernelInit Capability
+> createITASIDPool = Arch.createITASIDPool
+
+> writeITASIDPool :: Capability -> Capability -> Kernel ()
+> writeITASIDPool = Arch.writeITASIDPool
+
+> createDeviceFrames :: Capability -> KernelInit ()
+> createDeviceFrames = Arch.createDeviceFrames
 
-> initVSpace :: PPtr CTE -> PPtr CTE -> KernelInit ()
-> initVSpace = Arch.initVSpace
 
 \item handling virtual memory faults, given the current thread, the faulting address, and a boolean value that is true for write accesses;
 
@@ -75,13 +106,5 @@ This module defines architecture-specific virtual memory management procedures.
 > lookupIPCBuffer :: Bool -> PPtr TCB -> Kernel (Maybe (PPtr Word))
 > lookupIPCBuffer = Arch.lookupIPCBuffer
 
-\item and creating new capabilities to virtual memory pages and devices mapped by the bootstrap code.
-
-> createInitPage :: PAddr -> Kernel Capability
-> createInitPage = Arch.createInitPage
-> 
-> createDeviceCap :: (PAddr, PAddr) -> Kernel Capability
-> createDeviceCap = Arch.createDeviceCap
-
 \end{itemize}
 

haskell/src/SEL4/Machine/Hardware.lhs

@@ -55,6 +55,8 @@ Depending on the architecture, real physical addresses may be the same as the ad
 > addrFromPPtr :: PPtr a -> PAddr
 > addrFromPPtr = Arch.addrFromPPtr
 
+> fromPAddr = Arch.fromPAddr
+
 \subsubsection{Interrupts}
 
 An interrupt request from an external device, or from the CPU's timer, is represented by the type "IRQ".

haskell/src/SEL4/Model/Failures.lhs

@@ -40,6 +40,7 @@ All four of the failure types must have an instance of the "Error" class to be u
 > instance Error Fault
 > instance Error SyscallError
 > instance Error LookupFailure
+> instance Error InitFailure
 
 \subsection{Failure Handling}
 

haskell/src/SEL4/Model/PSpace.lhs

@@ -75,7 +75,7 @@ The default definitions are sufficient for most kernel objects. There is one exc
 >     loadObject :: (Monad m) => Word -> Word -> Maybe Word ->
 >                                 KernelObject -> m a
 >     loadObject ptr ptr' next obj = do
->         unless (ptr == ptr') $ fail "no object at address given in pspace"
+>         unless (ptr == ptr') $ fail $ "no object at address given in pspace,target=" ++ (show ptr) ++",lookup=" ++ (show ptr')
 >         val <- projectKO obj 
 >         alignCheck ptr (objBits val)
 >         sizeCheck ptr next (objBits val)
@@ -84,7 +84,7 @@ The default definitions are sufficient for most kernel objects. There is one exc
 >     updateObject :: (Monad m) => a -> KernelObject -> Word ->
 >                         Word -> Maybe Word -> m KernelObject
 >     updateObject val oldObj ptr ptr' next = do 
->         unless (ptr == ptr') $ fail "no object at address given in pspace"
+>         unless (ptr == ptr') $ fail $ "no object at address given in pspace,target=" ++ (show ptr) ++",lookup=" ++ (show ptr')
 >         liftM (asTypeOf val) $ projectKO oldObj -- for the type error
 >         alignCheck ptr (objBits val)
 >         sizeCheck ptr next (objBits val)
@@ -230,7 +230,7 @@ No type checks are performed when deleting objects; "deleteObjects" simply delet
 >             "Object deletion would leave dangling pointers"
 >         doMachineOp $ freeMemory (PPtr (fromPPtr ptr)) bits
 >         ps <- gets ksPSpace
->         let inRange = (\x -> x .&. (- mask bits) - 1 == fromPPtr ptr)
+>         let inRange = (\x -> x .&. ((- mask bits) - 1) == fromPPtr ptr)
 >         let map' = Data.Map.filterWithKey
 >                         (\x _ -> not (inRange x))
 >                         (psMap ps)

haskell/src/SEL4/Object/Interrupt.lhs

@@ -141,20 +141,22 @@ When the last IRQ handler capability for a given IRQ is deleted, the capability
 
 This function is called during bootstrap to set up the initial state of the interrupt controller. It allocates a frame and converts its contents to capability slots, which are used as a table endpoints that are notified of incoming interrupts. It also sets the global interrupt controller state, which contains a pointer to each slot and a Boolean flag indicating whether a handler capability has been generated for each IRQ. An interrupt controller capability is provided to the initial thread.
 
-> initInterruptController :: KernelInit Capability
-> initInterruptController = do
+> initInterruptController :: Capability -> Word -> KernelInit Capability
+> initInterruptController rootCNCap biCapIRQC= do
 >     frame <- allocFrame
 >     doKernelOp $ do
 >         assert (length [minBound..(maxBound::IRQ)]
 >                `shiftL` (objBits (makeObject :: CTE)) <= bit pageBits)
 >             "Interrupt vector slots must fit in one frame"
 >         placeNewObject (ptrFromPAddr frame) (makeObject :: CTE)
->               (bit pageBits `shiftR` objBits (makeObject :: CTE))
+>               (pageBits - objBits (makeObject :: CTE))
 >         doMachineOp $ mapM_ (maskInterrupt True) [minBound .. maxBound]
 >         let irqTable = funArray $ const IRQInactive
 >         setInterruptState $ InterruptState (ptrFromPAddr frame) irqTable
 >         timerIRQ <- doMachineOp configureTimer
 >         setIRQState IRQTimer timerIRQ
+>         slot <- locateSlot (capCNodePtr rootCNCap) biCapIRQC
+>         insertInitCap slot IRQControlCap
 >     return IRQControlCap
 
 \subsubsection{Handling Interrupts}