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