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