1-- Copyright 2018, Data61, CSIRO
2--
3-- This software may be distributed and modified according to the terms of
4-- the GNU General Public License version 2. Note that NO WARRANTY is provided.
5-- See "LICENSE_GPLv2.txt" for details.
6--
7-- @TAG(DATA61_GPL)
8
9-- This module contains operations on machine-specific object types.
10
11module SEL4.Object.ObjectType.RISCV64 where
12
13import Prelude hiding (Word)
14import SEL4.Machine.RegisterSet
15import SEL4.Machine.Hardware.RISCV64
16import SEL4.Model
17import SEL4.Model.StateData.RISCV64
18import SEL4.API.Types
19import SEL4.API.Failures
20import SEL4.API.Invocation.RISCV64 as ArchInv
21import SEL4.Object.Structures
22import SEL4.Kernel.VSpace.RISCV64
23
24import Data.Bits
25import Data.Word(Word16)
26import Data.Array
27
28-- The architecture-specific types and structures are qualified with the
29-- "Arch.Types" and "Arch.Structures" prefixes, respectively. This is to avoid
30-- namespace conflicts with the platform-independent modules.
31
32import qualified SEL4.API.Types.RISCV64 as Arch.Types
33
34{- Copying and Mutating Capabilities -}
35
36deriveCap :: PPtr CTE -> ArchCapability -> KernelF SyscallError Capability
37-- It is not possible to copy a page table or page directory capability unless
38-- it has been mapped.
39deriveCap _ (c@PageTableCap { capPTMappedAddress = Just _ }) = return $ ArchObjectCap c
40deriveCap _ (PageTableCap { capPTMappedAddress = Nothing })
41    = throw IllegalOperation
42-- Page capabilities are copied without their mapping information, to allow
43-- them to be mapped in multiple locations.
44deriveCap _ (c@FrameCap {})
45    = return $ ArchObjectCap $ c { capFMappedAddress = Nothing }
46-- ASID capabilities can be copied without modification
47deriveCap _ c@ASIDControlCap = return $ ArchObjectCap c
48deriveCap _ (c@ASIDPoolCap {}) = return $ ArchObjectCap c
49
50isCapRevocable :: Capability -> Capability -> Bool
51isCapRevocable newCap srcCap = False
52
53updateCapData :: Bool -> Word -> ArchCapability -> Capability
54updateCapData _ _ c = ArchObjectCap c
55
56-- these seem to refer to extraction of fields from seL4_CNode_CapData
57
58cteRightsBits :: Int
59cteRightsBits = 0
60
61cteGuardBits :: Int
62cteGuardBits = 58
63
64-- Page capabilities have read and write permission bits, which are used to
65-- restrict virtual memory accesses to their contents. Note that the ability to
66-- map objects into a page table or page directory is granted by possession of
67-- a capability to it; there is no specific permission bit restricting this
68-- ability.
69
70maskCapRights :: CapRights -> ArchCapability -> Capability
71maskCapRights r c@(FrameCap {}) = ArchObjectCap $ c {
72    capFVMRights = maskVMRights (capFVMRights c) r }
73maskCapRights _ c = ArchObjectCap c
74
75{- Deleting Capabilities -}
76
77postCapDeletion :: ArchCapability -> Kernel ()
78postCapDeletion c = return ()
79
80finaliseCap :: ArchCapability -> Bool -> Kernel (Capability, Capability)
81
82finaliseCap (ASIDPoolCap { capASIDBase = b, capASIDPool = ptr }) True = do
83    deleteASIDPool b ptr
84    return (NullCap, NullCap)
85
86finaliseCap (PageTableCap {
87        capPTMappedAddress = Just (asid, vptr),
88        capPTBasePtr = pte }) True = do
89
90    catchFailure
91        (do
92            vroot <- findVSpaceForASID asid
93            when (vroot == pte) (withoutFailure $ deleteASID asid pte))
94        (\_ -> unmapPageTable asid vptr pte)
95
96    return (NullCap, NullCap)
97
98finaliseCap (FrameCap {
99        capFMappedAddress = Just (asid, v),
100        capFSize = s,
101        capFBasePtr = ptr }) _ = do
102    unmapPage s asid v ptr
103    return (NullCap, NullCap)
104
105finaliseCap _ _ = return (NullCap, NullCap)
106
107{- Identifying Capabilities -}
108
109sameRegionAs :: ArchCapability -> ArchCapability -> Bool
110sameRegionAs (a@FrameCap {}) (b@FrameCap {}) =
111    (botA <= botB) && (topA >= topB) && (botB <= topB)
112    where
113        botA = capFBasePtr a
114        botB = capFBasePtr b
115        topA = botA + mask (pageBitsForSize $ capFSize a)
116        topB = botB + mask (pageBitsForSize $ capFSize b)
117sameRegionAs (a@PageTableCap {}) (b@PageTableCap {}) =
118    capPTBasePtr a == capPTBasePtr b
119sameRegionAs ASIDControlCap ASIDControlCap = True
120sameRegionAs (a@ASIDPoolCap {}) (b@ASIDPoolCap {}) =
121    capASIDPool a == capASIDPool b
122sameRegionAs _ _ = False
123
124isPhysicalCap :: ArchCapability -> Bool
125isPhysicalCap ASIDControlCap = False
126isPhysicalCap _ = True
127
128sameObjectAs :: ArchCapability -> ArchCapability -> Bool
129sameObjectAs (a@FrameCap { capFBasePtr = ptrA }) (b@FrameCap {}) =
130    (ptrA == capFBasePtr b) && (capFSize a == capFSize b)
131        && (ptrA <= ptrA + mask (pageBitsForSize $ capFSize a))
132        && (capFIsDevice a == capFIsDevice b)
133sameObjectAs a b = sameRegionAs a b
134
135{- Creating New Capabilities -}
136
137-- Create an architecture-specific object.
138
139-- % FIXME: it is not clear whether we can have large/huge device pages
140
141placeNewDataObject :: PPtr () -> Int -> Bool -> Kernel ()
142placeNewDataObject regionBase sz isDevice = if isDevice
143    then placeNewObject regionBase UserDataDevice sz
144    else placeNewObject regionBase UserData sz
145
146-- FIXME RISCV: C code missing AUXUPD, TODO in later stages of project
147
148createObject :: ObjectType -> PPtr () -> Int -> Bool -> Kernel ArchCapability
149createObject t regionBase _ isDevice =
150    let funupd = (\f x v y -> if y == x then v else f y) in
151    let pointerCast = PPtr . fromPPtr
152    in case t of
153        Arch.Types.APIObjectType _ ->
154            fail "Arch.createObject got an API type"
155        Arch.Types.SmallPageObject -> do
156            placeNewDataObject regionBase 0 isDevice
157            modify (\ks -> ks { gsUserPages =
158              funupd (gsUserPages ks)
159                     (fromPPtr regionBase) (Just RISCVSmallPage)})
160            return $! FrameCap (pointerCast regionBase)
161                  VMReadWrite RISCVSmallPage isDevice Nothing
162        Arch.Types.LargePageObject -> do
163            placeNewDataObject regionBase 0 isDevice
164            modify (\ks -> ks { gsUserPages =
165              funupd (gsUserPages ks)
166                     (fromPPtr regionBase) (Just RISCVLargePage)})
167            return $! FrameCap (pointerCast regionBase)
168                  VMReadWrite RISCVLargePage isDevice Nothing
169        Arch.Types.HugePageObject -> do
170            placeNewDataObject regionBase 0 isDevice
171            modify (\ks -> ks { gsUserPages =
172              funupd (gsUserPages ks)
173                     (fromPPtr regionBase) (Just RISCVHugePage)})
174            return $! FrameCap (pointerCast regionBase)
175                  VMReadWrite RISCVHugePage isDevice Nothing
176        Arch.Types.PageTableObject -> do
177            let ptSize = ptBits - objBits (makeObject :: PTE)
178            placeNewObject regionBase (makeObject :: PTE) ptSize
179            return $! PageTableCap (pointerCast regionBase) Nothing
180
181{- Capability Invocation -}
182
183-- The only Arch invocations on RISCV are MMU invocations
184
185decodeInvocation :: Word -> [Word] -> CPtr -> PPtr CTE ->
186        ArchCapability -> [(Capability, PPtr CTE)] ->
187        KernelF SyscallError ArchInv.Invocation
188decodeInvocation = decodeRISCVMMUInvocation
189
190performInvocation :: ArchInv.Invocation -> KernelP [Word]
191performInvocation = performRISCVMMUInvocation
192
193{- Helper Functions -}
194
195capUntypedPtr :: ArchCapability -> PPtr ()
196capUntypedPtr (FrameCap { capFBasePtr = PPtr p }) = PPtr p
197capUntypedPtr (PageTableCap { capPTBasePtr = PPtr p }) = PPtr p
198capUntypedPtr ASIDControlCap = error "ASID control has no pointer"
199capUntypedPtr (ASIDPoolCap { capASIDPool = PPtr p }) = PPtr p
200
201asidPoolBits :: Int
202asidPoolBits = 12
203
204capUntypedSize :: ArchCapability -> Word
205capUntypedSize (FrameCap {capFSize = sz}) = bit $ pageBitsForSize sz
206capUntypedSize (PageTableCap {}) = bit ptBits
207capUntypedSize (ASIDControlCap {}) = 0
208capUntypedSize (ASIDPoolCap {}) = bit asidPoolBits
209
210-- No arch-specific thread deletion operations needed on RISC-V platform.
211
212prepareThreadDelete :: PPtr TCB -> Kernel ()
213prepareThreadDelete _ = return ()
214