1% 2% Copyright 2014, General Dynamics C4 Systems 3% 4% This software may be distributed and modified according to the terms of 5% the GNU General Public License version 2. Note that NO WARRANTY is provided. 6% See "LICENSE_GPLv2.txt" for details. 7% 8% @TAG(GD_GPL) 9% 10 11This module defines the interface that the kernel model uses to determine the properties of the architecture of the machine being simulated, and particularly the types, names and functions of the general purpose registers. 12 13\begin{impdetails} 14 15We use the C preprocessor to select a target architecture. Also, this file makes use of the GHC extension allowing derivation of arbitrary type classes for types defined with "newtype", so GHC language extensions are enabled. 16 17> {-# LANGUAGE CPP, GeneralizedNewtypeDeriving #-} 18 19\end{impdetails} 20 21> module SEL4.Machine.RegisterSet where 22 23\begin{impdetails} 24 25> import Prelude hiding (Word) 26> import Data.Bits 27> import Data.Array 28> import Data.Helpers 29> import Foreign.Storable 30 31> import Control.Monad.State(State,liftM) 32 33\end{impdetails} 34 35The architecture-specific definitions are imported qualified with the "Arch" prefix. 36 37> import qualified SEL4.Machine.RegisterSet.TARGET as Arch 38 39\subsection{Types} 40 41The architecture must define two types: one for the type of the machine's word, and one for the set of valid register names. 42 43\subsubsection{Word Types} 44 45The type "Word" represents the native word size of the modelled machine. It must be an instance of the type classes that allow bitwise arithmetic, use as an integer, use as a foreign type (for the external simulator interface), and conversion to a string. 46 47> newtype Word = Word Arch.Word 48> deriving (Eq, Ord, Enum, Real, Num, Bits, FiniteBits, Integral, Bounded, Storable, Show) 49 50\subsubsection{Register Names} 51 52The "Register" type defines a bounded, enumerated set of register names. 53 54> newtype Register = Register Arch.Register 55> deriving (Eq, Ord, Enum, Bounded, Ix, Show) 56 57\subsubsection{Pointers} 58 59To enforce explicit casts between pointer types, "newtype" is used to 60declare types for various types of user and kernel pointers. These 61types derive a number of basic type classes allowing sorting, 62comparison for equality, pointer arithmetic and printing. 63 64\begin{impdetails} Note that they do not derive "Integral", despite 65being integers; this is to avoid allowing them to be cast using 66"fromIntegral", which does not indicate that the cast is to or from a 67pointer type. 68 69Also, these types derive "Num", which requires a GHC extension. 70\end{impdetails} 71 72The types defined here are used for kernel and user pointers. Depending on the architecture, kernel pointers may either be unmodified physical pointers, or virtual pointers into a region that is direct-mapped (with a fixed offset) to physical memory. Note that another pointer type, "PAddr", is defined by the "SEL4.Machine.Hardware" module in \autoref{sec:machine.hardware}; it always represents a physical pointer, and may or may not be equivalent to "PPtr a". 73 74> newtype PPtr a = PPtr { fromPPtr :: Word } 75> deriving (Show, Eq, Num, Bits, FiniteBits, Ord, Enum, Bounded) 76 77> newtype VPtr = VPtr { fromVPtr :: Word } 78> deriving (Show, Eq, Num, Bits, FiniteBits, Ord, Enum, Bounded) 79 80\subsection{Monads} 81 82"UserMonad" is a specialisation of "Control.Monad.State", used to execute functions that have access only to the user-level context of a single thread. 83 84> type UserContext = Arch.UserContext 85> type UserMonad = State UserContext 86 87\subsection{Functions and Constants} 88 89\subsubsection{Register Set} 90 91The following functions and constants define registers or groups of user-level registers that are used for specific purposes by the kernel. 92 93\begin{description} 94\item[The message information register] contains metadata about the contents of an IPC message, such as the length of the message and whether a capability is attached. 95 96> msgInfoRegister :: Register 97> msgInfoRegister = Register Arch.msgInfoRegister 98 99\item[Message registers] are used to hold the message being sent by an object invocation. 100 101This list may be empty, though it should contain as many registers as possible. Message words that do not fit in these registers will be transferred in a buffer in user-accessible memory. 102 103> msgRegisters :: [Register] 104> msgRegisters = map Register Arch.msgRegisters 105 106\item[The capability register] is used when performing a system call, to specify the location of the invoked capability. 107 108> capRegister :: Register 109> capRegister = Register Arch.capRegister 110 111\item[The badge register] is used to return the badge of the capability from which a message was received. This is typically the same as "capRegister". 112 113> badgeRegister :: Register 114> badgeRegister = Register Arch.badgeRegister 115 116\item[The frame registers] are the registers that are used by the architecture's function calling convention. They generally include the current instruction and stack pointers, and the argument registers. They appear at the beginning of a "ReadRegisters" or "WriteRegisters" message, and are one of the two subsets of the integer registers that can be copied by "CopyRegisters". 117 118> frameRegisters :: [Register] 119> frameRegisters = map Register Arch.frameRegisters 120 121\item[The general-purpose registers] include all registers that are not in "frameRegisters", except any kernel-reserved or constant registers (such as the MIPS "zero", "k0" and "k1" registers). They appear after the frame registers in a "ReadRegisters" or "WriteRegisters" message, and are the second of two subsets of the integer registers that can be copied by "CopyRegisters". 122 123> gpRegisters :: [Register] 124> gpRegisters = map Register Arch.gpRegisters 125 126\item[An exception message] is sent by the kernel when a hardware exception is raised by a user-level thread. The message contains registers from the current user-level state, as specified by this list. Two architecture-defined words, specifying the type and cause of the exception, are appended to the message. The reply may contain updated values for these registers. 127 128> exceptionMessage :: [Register] 129> exceptionMessage = map Register Arch.exceptionMessage 130 131\item[A syscall message] is sent by the kernel when a user thread performs a system call that is not recognised by seL4. The message contains registers from the current user-level state, as specified by this list. A word containing the system call number is appended to the message. The reply may contain updated values for these registers. 132 133> syscallMessage :: [Register] 134> syscallMessage = map Register Arch.syscallMessage 135 136> tlsBaseRegister :: Register 137> tlsBaseRegister = Register Arch.tlsBaseRegister 138 139\end{description} 140 141 142Functions for getting and setting registers. 143 144> getRegister :: Register -> UserMonad Word 145> getRegister (Register r) = do 146> w <- Arch.getRegister r 147> return (Word w) 148 149> setRegister :: Register -> Word -> UserMonad () 150> setRegister (Register r) (Word v)= Arch.setRegister r v 151 152> newContext :: UserContext 153> newContext = Arch.newContext 154 155 156\subsubsection{Miscellaneous} 157 158The "mask" function is a trivial function which, given a number of bits, returns a word with that number of low-order bits set. 159 160> mask :: (Bits w, Num w) => Int -> w 161> mask bits = bit bits - 1 162 163 164